Certified Lattice GFF EDMD
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Certified Lattice GFF EDMD • Lean 4 + Mathlib • Apoth3osis Labs
Certified EDMD Estimation for Lattice Gaussian Free Fields
This work builds on the landmark formalization of the Gaussian Free Field by Douglas, Hoback, Mei & Nissim (arXiv:2603.15770), who proved all five Osterwalder-Schrader axioms for the massive GFF in d=4 using Lean 4 (~32,000 lines, zero sorry). We ask a different question: given the GFF, can we formally verify that Extended Dynamic Mode Decomposition (EDMD) estimation on its lattice discretization has certified, quantified error bounds?
The certificate chain flows from the lattice OU innovation model (product-measure independence of split real/imaginary Gaussian coordinates) through sub-Gaussian concentration to a conservative runtime radius that bounds the EDMD estimator error with formally derived probability guarantees.
- • 10 sorry-free Lean 4 modules with 88 theorems
- • Certificate surface binding formal proofs to runtime diagnostics
- • Continuum bridge through restricted Koopman correlation factorization
- • 11 rounds of hostile audit passed
Each Fourier mode's estimation error bounded by certified confidence radius
Split innovation coordinates mutually independent under product measure
Restricted Koopman correlations decay exponentially via quantitative mass gap
Douglas et al. — Formalization of QFT
The upstream formalization by Douglas, Hoback, Mei & Nissim proves all five Osterwalder-Schrader axioms (OS0–OS4) for the massive Gaussian Free Field in d=4. Their ~32,000-line Lean 4 formalization is the first complete machine-checked verification of constructive QFT axioms. Our EDMD estimation lane builds on this foundation — they proved the measure exists; we prove estimation on its lattice discretization has bounded error.
Douglas, Hoback, Mei & Nissim developed the foundational GFF formalization that our EDMD estimation lane builds upon. Their work proves the measure exists; ours proves estimation on its lattice discretization has certified error bounds.
Michael R. Douglas
Senior Research Scientist
Center of Mathematical Sciences and Applications (CMSA), Harvard University
Theoretical physicist and mathematician. PhD from Caltech (1988) under John Schwarz. Former professor and director (2000-2007) of the New High Energy Theory Center at Rutgers, first permanent member of the Simons Center for Geometry and Physics at Stony Brook, and researcher at Renaissance Technologies (2012-2020). Currently senior research scientist at Harvard CMSA developing new ways to use machine learning in mathematical research. Lead author of the ~32,000-line Lean 4 formalization proving all five Osterwalder-Schrader axioms for the massive GFF in d=4.
Sarah Hoback
Graduate Student · High Energy Theory
Jefferson Physical Laboratory, Harvard University / Physical Superintelligence PBC
Graduate student in high energy theory at Harvard (NSF Fellow). Research interests include quantum gravity, string theory, quantum information, and de Sitter spacetimes. Published work on dimensional reduction of higher-point conformal blocks and Feynman rules for scalar conformal blocks (JHEP 2021-2022). Co-author of the OSforGFF formalization.
Anna Mei
Graduate Student · Theoretical High Energy Physics
Jefferson Physical Laboratory, Harvard University
Graduate student in theoretical high energy physics at Harvard. Undergraduate research at Boston University (CAS’23) in the Suarez Lab on the CMS experiment, contributing to electronics development and data analysis for particle scattering. Co-author of the OSforGFF formalization.
Ron Nissim
PhD Student · Mathematics
MIT Department of Mathematics
Fourth-year PhD student in the Mathematics Department at MIT, advised by Scott Sheffield. Research focuses on Yang-Mills lattice gauge theory and random matrix theory, with interests spanning mathematical physics and probability. Published work on sharp estimates for large-N Weingarten functions and geometric derivation of the finite-N master loop equation. Co-author of the OSforGFF formalization.
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.