Pólya's inequality for the third planar Dirichlet eigenvalue

This research preprint presents an argument for |Ω|λ₃(Ω) > 12π for every planar open set of finite positive area, with Dirichlet eigenvalues counted with multiplicity. The claimed scope includes disconnected and unbounded sets and imposes no boundary-regularity assumption. The argument uses an area-bisecting line, reflection of the two halves, and a dichotomy between that cut and a perpendicular bisector. Cross-sectional profile estimates are reduced by rearrangement and one-dimensional comparison to finite exact-rational and interval calculations. The accompanying source snapshot includes the manuscript, certificate data, checking programs and auxiliary Lean developments. This is a research preprint, not a journal-peer-reviewed publication; the complete spectral/PDE theorem is not formalized in Lean. It makes no priority claim and does not claim the all-index Pólya conjecture. Version: manuscript revision dated 2026-10-22, source commit 6093af6df8e9bbc7f9d82327d48b9291f80ed298. The Zenodo publication date records this deposit, not a claim about the earliest public availability of the work. Source repository: https://github.com/s-JoL/polya-third-eigenvalue/tree/6093af6df8e9bbc7f9d82327d48b9291f80ed298 AI-use disclosure: The included supplementary manuscript paper/k3.md states: “AI systems assisted drafting and reconstruction; human release responsibility is attributed to the account s-JoL.” This disclosure is quoted from that supplement, not from the current English PDF.