Apoth3osis
Home/Paper → Proof → Code/Certified Lattice GFF EDMD

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. 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?

VERIFIED0 SORRY · 0 AXIOMSLean 4 + Mathlib + OSforGFFGitHubOSforGFF upstream
10
Modules
Lean 4 files
88
Theorems
machine-checked
2,251
Lines
Lean source
0
Sorry
none
11
Audits
hostile rounds
>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED88 theorems • 0 sorry10 modules0 SORRY

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.

88 THEOREMS VERIFIED10 MODULES2,251 LINES0 SORRY

Certified Lattice GFF EDMD • Lean 4 + Mathlib • Apoth3osis Labs

Paper ↔ Proof Correspondence

How our Lean modules map to the mathematics of Douglas et al. (arXiv:2603.15770) and our original EDMD estimation theory.

Mathematical ContentStatusModule
OS0–OS4 (Osterwalder-Schrader Axioms)BRIDGEDOSforGFFBridge
Schwinger Functions & Clustering (OS4)BRIDGEDOSforGFFKoopmanBridge
Quantitative Mass GapBRIDGED + EXTENDEDOSforGFFQuantitativeGap
Sub-Gaussian ConcentrationORIGINALEDMDConcentration
EDMD Quotient Identity & Fixed-Regressor TheoremORIGINALEDMDRatioSpecialization
Lattice Mass-Gap SpectrumORIGINALLatticeMassGap
Lattice OU Innovation ModelORIGINALLatticeOUModel
Certificate SurfaceORIGINALLatticeCertificate
Restricted Koopman CorrelationsORIGINALGeneratingObservables

Key Mathematics

EDMD Quotient Estimator
a^=∑i=1nzˉizi′∑i=1n∣zi∣2\hat{a} = \frac{\sum_{i=1}^n \bar{z}_i z'_i}{\sum_{i=1}^n |z_i|^2}
Conservative Runtime Radius
r(δ)=2σ2log⁡(8/δ)Deffr(\delta) = \sqrt{\frac{2\sigma^2 \log(8/\delta)}{D_{\text{eff}}}}
Lattice OU Multiplier
decaym=exp⁡(−Δt⋅λm)\text{decay}_m = \exp(-\Delta t \cdot \lambda_m)
Innovation Variance
σm2=1−exp⁡(−2Δt⋅λm)λm\sigma^2_m = \frac{1 - \exp(-2\Delta t \cdot \lambda_m)}{\lambda_m}
Capstone Tail Bound
μ{ω:∥a^(ω)−a∥≥r(δ)}≤δ2\mu\bigl\{\omega : \|\hat{a}(\omega) - a\| \geq r(\delta)\bigr\} \leq \frac{\delta}{2}

Product-measure independence + sub-Gaussian concentration → certified error radius for each Fourier mode

Module Explorer

Click any module to expand its definitions and theorems. Toggle between Mathematics and Lean 4 views.

Concentration Foundations

EDMD Specialization

Lattice Model

Certificate Surface

Continuum Bridge

Verified Artifacts

LEAN 4 PROOFS

10 Lean source files, 88 theorems, 2,251 lines. Zero sorry, zero axioms.

Download lean-proofs.tar.gz
VERIFIED C

7 C source files + header. Compiles with gcc -Wall -Werror\texttt{gcc -Wall -Werror} — zero warnings.

Download verified-c.tar.gz
SAFE RUST

6 Rust modules + lib.rs. 13 tests pass, zero warnings. cargo build && cargo test\texttt{cargo build \&\& cargo test}.

Download safe-rust.tar.gz

Provenance Chain

Douglas et al. (arXiv:2603.15770)→Lean 4 + Mathlib v4.24→Verified C (gcc -Wall -Werror)→Safe Rust (cargo test ✓)

Related

RELATED PPC PAGE
SafEDMD Koopman — Verified Controller Synthesis
Nucleus-bottleneck autoencoders with SafEDMD error bounds (Strässer et al.)
UPSTREAM FORMALIZATION
mrdouglasny/OSforGFF — OS Axioms for GFF
~32,000 lines Lean 4, all five Osterwalder-Schrader axioms (Douglas, Hoback, Mei, Nissim)
RESEARCH PROJECT PAGE
Certified Lattice GFF EDMD — Research Details
Heritage researcher profiles, project overview, key results
SOURCE PAPER
arXiv:2603.15770 — Formalization of QFT
Douglas, Hoback, Mei & Nissim (March 2026)