Source authenticated

Strict Dirichlet Pólya inequality on simply connected planar domains

Theorem 1.1 of arXiv:2610.13139: for every bounded nonempty simply connected planar domain $\Omega$ , with no boundary regularity assumed, $|\Omega|\lambda_j(\Omega)>4\pi j$ for all $j\ge1$ , equivalently $N_D(E)<|\Omega|E/(4\pi)$ for $E>0$ (eigenvalues counted with multiplicity, endpoint included). This is the strict form of Pólya's Dirichlet inequality on the whole simply connected planar class. Previously it was known for tiling domains (Pólya 1961), disks and sectors (Filonov, Levitin, Polterovich and Sher 2023), annuli and a few further families. Multiply connected planar domains and higher dimensions remain open. The companion strict Neumann result for simply connected Lipschitz domains is a separate entry.

Exact FrontierDelta

Prior state unknown→proved

Scope and record

Occurred: Oct 9, 2026

Delta type: SOURCE CLAIM

Assumptions: VibeMathed verification: lean-checked. Publication: preprint. AI contribution: ai-assisted. VibeMathed editorial classifications, scores, notes, relations, and dataset structure are CC BY 4.0. Source statements and linked content retain their own rights.

Canonical aliases: Strict Dirichlet Pólya inequality on simply connected planar domains · Strict Dirichlet Pólya inequality

Confidence: Not scored

Registry verification: lean checked · preprint · partial

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

ChatGPT
model · ai model contributor · maker attribution ambiguous: OpenAI, Harmonic

Aristotle
model · ai model contributor · maker attribution ambiguous: OpenAI, Harmonic

Codex
model · ai model contributor · maker attribution ambiguous: OpenAI, Harmonic

Quanyu Tang
human · human collaborator

Zuoqin Wang
human · human collaborator

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: Strict Dirichlet Pólya inequality on simply connected planar domains

specialist registry · passed

No independent mathematician has checked this yet. Read by this site on 15 October 2026, not rebuilt. The Palomar record PALOMAR-2026-10-09-000003 v1 was fetched from the registry's data API: registered commit ba3690b, Comparator theorem PalomarDirichlet.main_result, checked with the Lean, nanoda and con-ron kernels, automated review neutral with no warnings, trust level high. Challenge.lean at that commit (identical on main; later commits touch only documentation) was read: Mathlib only, bounded open simply connected Omega in C, and lambda_j defined by min-max of the Rayleigh quotient over j-dimensional spaces of smooth compactly supported functions in Omega, which is the standard Dirichlet eigenvalue. The registered snapshot (about 27,000 lines) was grepped: the only sorry is the Challenge statement hole; no admit, axiom declarations, native_decide, unsafe or implemented_by. The repository's GitHub Actions build and audit passed on the registered commit; the audit asserts only propext, Classical.choice and Quot.sound. A separate check written here on disks and squares (3,000 eigenvalues each) agrees with the strict inequality; it says nothing about general domains. The informal proof was not read. Lean-checked, not Lean-verified: the statement audit is this site's alone and nothing was rebuilt here.

Source ↗

Companion Dirichlet paper, arXiv:2610.13139

paper · pending

Primary source named by the VibeMathed record. Presence in this import is not an independent mathematical verification.

Source ↗

Palomar Registry: PALOMAR-2026-10-09-000003 v1

witness · pending

palomar link supplied by the VibeMathed registry.

Source ↗

Lean formalization (GitHub)

lean artifact · pending

lean-proof link supplied by the VibeMathed registry.