Mathematical architecture

The formal development turns metric boundary data into explicit planar certificates. The development includes the final passage to compact Riemannian surfaces at the boundary and orientation interfaces described below.

Distance profilesBoundary distances produce odd Fourier coordinates with exact boundary values.

Orthogonal mixingExplicit Givens rotations preserve energy and force first-harmonic dominance.

Jordan coverageDegree and mod-2 obstruction force the bounded Jordan region into the image.

Area certificatePlanar Jacobian budgets and exact boundary area yield finite and asymptotic bounds.

Boundary distance profiles

For a boundary parametrization γ, the metric profile records the distance from an interior point to every boundary point. Its odd Fourier modes have exact boundary values

\[ z_n(\gamma(s))=-\frac{4}{\pi n^2}e^{ins}, \qquad n>0\text{ odd}. \]

The Lean development proves the triangle-wave coefficients, continuity, global Lipschitz bounds, planar weak differentiation, and finite Bessel energy estimates for these genuine metric-defined maps.

Givens untwisting

Higher odd modes wind several times around the origin. The project defines an explicit orthogonal Givens product that mixes finitely many Fourier modes while preserving their derivative energy. Every mixed row satisfies strict first-harmonic dominance, so its boundary curve is injective and has degree +1.

Jordan regions and mod-2 topology

The formalization transports the Jordan curve theorem to the complex plane, identifies the bounded degree-one component containing the origin, and proves coverage from an odd boundary-degree obstruction.

The finite polygonal obstruction is fully assembled: face cuts, real lifts, integer edge turns, and the signed boundary-turn identity are constructed in Lean. The general glued-pairing theorem covers both preserving and reversing side identifications.

Finite one-high-leg ceiling

For J normalized resonances, Lean exhibits the positive odd test frequency m = 2J+1, proves its unit norm and anti-periodicity, and computes the exact occupied-coordinate symplectic cost

\[ 1+\sum_j\mu_j^2. \]

The displayed finite resonance matrix is constructed entry by entry from its convergent odd-mode series. Its quadratic form is proved equal to the boundary action series and is decomposed into a sum of nonnegative weighted squares. This gives positive semidefiniteness, shows that the largest Rayleigh value is an eigenvalue, and proves the finite ceiling whenever the ambient comass bounds the exhibited high-mode plane.

The remaining interface is analytic rather than finite-dimensional: the modeled occupied outputs must still be identified with the derivative of the full normalized nonlinear map on its infinite coefficient space and then with the global ambient comass.

Resonance trace arithmetic

The scalar series underlying the exact-trace calculation is now verified:

\[ \sum_{j,k\ge 0}\frac{16}{\pi}\frac{2k+1}{(2k+1+2j)^4} =\frac{\pi}{2}+\frac{7\zeta(3)}{\pi}+\frac{\pi^3}{24}. \]

Lean proves summability and the nonnegative Tonelli/antidiagonal regrouping, not merely the final arithmetic identity. The separate construction of the infinite matrix as a positive trace-class operator on ℓ², and the proof that its operator trace equals this scalar series, remain open.

Planar area and explicit constants

For Lipschitz maps on planar pieces, the project proves a genuine area inequality from Rademacher's theorem and mathlib's Jacobian image bound. It then composes coverage, exact Fourier area, and the common derivative-energy budget. The pointwise two-dimensional Riemannian Jacobian is now defined intrinsically between arbitrary Riemannian surfaces, proved independent of orthonormal bases and multiplicative under the manifold chain rule, and identified exactly with this planar absolute-determinant density. The chart-induced area measure, its exact weighted lintegral transfer, the local surface area inequality, and its summation over a countable covering chart family are verified. Standard smooth interior charts supply the required measurability; a finite controlled atlas is disjointified to avoid counting overlaps; exact chart-transition invariance identifies its measure with the canonical Riemannian surface-area measure. Combined with Jordan--Schönflies coverage, this proves the full orientation-free Lemma 3.4 inequality (Lemma 5.4 in the earlier draft).

The orientation-free constant is

\[ \frac{14\zeta(3)}{\pi}=5.3567723444\ldots \]

The oriented nonlinear certificate at λ = 1/25 gives the rigorous scalar conclusion

\[ \operatorname{Area}(M)>5.40154. \]

Both headline surface bounds are verified at their exact Riemannian interfaces. The oriented endpoint takes the project-defined conventional tangent-plane orientation; Lean derives the controlled boundary direction and finite certificate data internally. Broader raw-distance eikonal and global Stokes/comass formulations remain partial as independent manuscript items, not as hypotheses of the headline theorems; see the formalization page.

The revised coefficient uses cancellation of the first mixed-correlation term and the profile tail starting at frequency five. See Revised Section 4 for the exact formula and its Lean endpoints.