Proof of the Planar Pólya–Szegő Buckling Conjecture

The Faber–Krahn inequality |Ω|λ₁ᴰ(Ω) ≥ π q² holds for every open set of finite positive area, and 'its equality characterization gives a disk B of area |Ω| such that Ω and B agree almost everywhere'.

The only sources cited are Faber (1923) and Krahn (1925). Neither treats arbitrary open sets of finite measure with H¹₀ defined as the closure of C_c^∞, nor the almost-everywhere rigidity in the equality case (which in the modern literature rests on Brothers–Ziemer-type rigidity for the Pólya–Szegő inequality and is stated as 'Ω is a ball up to a set of zero capacity'). The statement used is true and standard, and the paper correctly isolates the a.e.-versus-open-set distinction in Lemma 7.1, but the result should be stated precisely and attributed to a source that actually proves it in this generality (e.g. Henrot's monograph or Kesavan).

Several closed-form identities are asserted as the outcome of 'direct differentiation' or 'direct expansion', e.g. f_tt = (p³/S²)[a₀φ − cz − (p/r²)g], 𝒱′ = −(cp/ρ²)(1−2η)² + (2/r)[(ηc_θ − s_θ/r)² − η²s_θ²], and 𝒱(k−) = 1/4 − 1/k².

These identities carry the one-variable inequalities on which positivity of M depends, but their derivations are omitted. I was able to reproduce the Riccati identities (2.3)–(2.4), (Videntity), (Gode), (bidentity), the three kernel identities of Proposition 2.4, the divergence algebra of Proposition 7.2 (the coefficient match with M is correct), S′+S/r = p(u/r²−c), the endpoint values G(0)=2λ−K, G(k)=0, G_r(k)=−2K/(3k), [r²]G, and the expansions of g, z, b at r=k; the remaining asserted formulas (notably (ph:Vprime), the formula for 𝒱 in terms of η, the bracket evaluation in Lemma 3.3, and the δ³-order computation behind 𝒱(k−)) I could not fully reproduce from the text. A reader can in principle check them by computer algebra, but the paper should supply the intermediate steps or an explicit reference to a verification script.

Integers A,B are given with A/10⁸ < S_{ν,31}(x) < S_{ν,30}(x) < B/10⁸ at fourteen rational points; from these follow K > .654, B(κ₃) > .634, B(q₂) < .640, J₁(q₂)² < .116, and the final margin 3L(κ_n) − φ(κ_n)φ_r(κ_n) > 431/250000.

The positivity of all Taylor coefficients a_m of −G (hence concavity of G, hence d>0 and the bound d<2G) hinges on the margin 431/250000 ≈ 0.0017, and the inputs are tight: K ≈ 0.65444 against the bound .654, B(κ₃) ≈ 0.6343 against .634. The tabulated 8-digit values of 31-term partial sums are asserted ('obtained by substitution') and cannot be checked by hand; the proof is therefore computer-assisted at this point without the paper saying so or providing the computation. My own rough evaluation agrees with the stated values, and the argument is logically correct given them, but the registry should treat these table entries as requiring independent recomputation.

'An independent Lean 4 formalization of the main results ... is publicly available and registered in the Palomar Registry (PALOMAR-2026-10-18-000008)', including 'separate proofs of the Faber–Krahn inequality, its equality characterization'.

This claim cannot be checked from the submission, and the paper itself concedes the formal development 'is not a line-by-line transcription' and verifies 'the stated mathematical results, rather than ... every individual step of the informal proof'. A formalization of Faber–Krahn with equality case, Bessel-zero localisation and the residue argument of Section 6 would be far beyond existing library coverage, so the claim is extraordinary. It should carry no evidential weight in assessing the informal proof, which must stand on its own.

"The Faber--Krahn inequality \cite{Faber,Krahn} gives |Ω|λ₁ᴰ(Ω) ≥ πq² for every open set of finite positive area... Its equality characterization gives a disk B of area |Ω| such that Ω and B agree almost everywhere."

Faber's and Krahn's original papers do not treat arbitrary (possibly unbounded, irregular) open sets of finite measure, and they do not give the measure-theoretic equality characterization used here. The inequality for general open sets is standard via Schwarz symmetrization. The rigidity statement (equality forces Ω to coincide with a disk up to a null or capacity-zero set) is a later and more delicate result. The paper should state it precisely and cite an appropriate source. This affects only the 'equality iff open disk' part of Corollary 1.3, not the inequality the registered problem asks for.

The abstract says an independent Lean 4 formalization of the main results is publicly available and 'verified and registered in the Palomar Registry'. The paper itself says the formalization 'is not a line-by-line transcription' and 'establishes the stated mathematical results, rather than verifying every individual step of the informal proof presented here'.

Nothing in the submission lets a reader check that the Lean statements match Theorem 1.2 and Corollary 1.3, including the H₀^m closure definitions, the Faber–Krahn input and the equality rigidity. By the authors' own description, the formalization does not certify the argument written in this paper. The curator should evaluate the resolution claim on the informal proof alone. The abstract's wording should not be read as an endorsement of that proof.

"Adding these two expressions to K(|D²U|²−P²)−(|∇F|²−λF²) produces exactly (X,Y,P)M(s)(X,Y,P)^T+(2K−g²−d)Z²."

This identity carries the entire reduction from the PDE inequality to one-variable Bessel estimates, but it is asserted without the expansion. I checked the structure on reading. ∇F = z∇U + g∇P gives |∇F|² = (zP+gX)²+g²Z². The cofactor divergence gives (2G−sG_s)(XY−Z²)+PG_sY. The resulting coefficients do match a, d, L_A, L_C, H and the Z² term. The parity relation M(−s)=DM(s)D is also consistent with f, G even and b odd. The P b(s)∇U divergence and the full assembly should still be written out, since the whole claim rests on them.