Fourier bounds for filling area

This project is a Lean 4 formalization of the Fourier, topology, planar area, and certificate arguments in A Fourier approach to Gromov's Filling Area Conjecture by Le Chen, Xiaolong Li, and Yimin Zhong.

Current verification boundary

The repository does not prove Gromov's conjecture. The manuscript proves lower bounds below the conjectural value 2π. Lean verifies both headline theorems at the exact Riemannian-surface and orientation interfaces stated on the formalization page.

6,762project declarations accepted by the live axiom audit

Lean 4.29pinned toolchain with mathlib 4.29 and a fixed Jordan input

MITproject license; vendored sources retain Apache-2.0

What is verified

The kernel-checked development includes exact Fourier coefficients, the Givens mixing matrix, dominant-harmonic Jordan curves, integer circle degree, finite mod-2 surface obstruction, boundary-regular Radó triangulation, faithful compact-surface polygonal classification, planar area and Jacobian inequalities, rigorous constant evaluation, off-diagonal logarithmic-sine-kernel positivity, de Sitter profile identities, finite one-high-leg Gram/Rayleigh algebra, exact scalar resonance-trace arithmetic, and end-to-end assembly of Theorems 1.1 and 1.2.

The general glued-polygon theorem now handles every fixed-point-free involutive side pairing, including orientation-reversing identifications. The lower boundary obstruction is derived automatically rather than supplied as a caller assumption.

Explore the project

• Mathematics

  Follow the argument from boundary distance profiles to Fourier maps, Jordan coverage, Jacobian budgets, and explicit constants.

  Read the mathematical map

• Formalization boundary

  See the verification scope of every numbered statement in the current manuscript.

  Inspect the claim boundary

• Lean modules

  Navigate the source by proof layer and find the canonical umbrella import.

  Browse the module map

• Verification

  Reproduce the build and understand the source scan, import check, and live axiom audit.

  Run the verification

• Reusable libraries

  See how the general topology, geometry, and analysis infrastructure can be extracted and contributed without changing the verified theorem artifact.

  Review the contribution roadmap

Current frontier

Lemma 3.4 (the earlier Lemma 5.4) and both headline surface bounds are now end-to-end verified at their exact interfaces. Theorem 1.2 uses the project-defined conventional surface orientation and derives its controlled boundary direction for the supplied parametrization or its reversal. Broader formulations remain outside the headline closures, including:

1. Riemannian eikonal and parameter-integral differentiation;
2. a standalone global differential-form Stokes/comass API;
3. an equivalence with a future generic library-level orientation API.

The repository keeps those independent boundaries visible. They are not assumptions of either headline endpoint, and the project does not replace them with custom axioms or conclusion-bearing hypotheses.

The updated orientable bound is Area(M) > 5.40154; its all-parameter parent is Theorem 4.1 of main2.tex. The Section 4 map records the exact scope and CI receipt.