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 + OSforGFFGitHub OSforGFF upstream

Modules

Lean 4 files

Theorems

machine-checked

2,251

Lines

Lean source

Sorry

none

Audits

hostile rounds

>_VERIFICATION.SEAL

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 Content	Status	Module
OS0–OS4 (Osterwalder-Schrader Axioms)	BRIDGED	OSforGFFBridge
Schwinger Functions & Clustering (OS4)	BRIDGED	OSforGFFKoopmanBridge
Quantitative Mass Gap	BRIDGED + EXTENDED	OSforGFFQuantitativeGap
Sub-Gaussian Concentration	ORIGINAL	EDMDConcentration
EDMD Quotient Identity & Fixed-Regressor Theorem	ORIGINAL	EDMDRatioSpecialization
Lattice Mass-Gap Spectrum	ORIGINAL	LatticeMassGap
Lattice OU Innovation Model	ORIGINAL	LatticeOUModel
Certificate Surface	ORIGINAL	LatticeCertificate
Restricted Koopman Correlations	ORIGINAL	GeneratingObservables

Key Mathematics

EDMD Quotient Estimator

\hat{a} = \frac{\sum_{i=1}^n \bar{z}_i z'_i}{\sum_{i=1}^n |z_i|^2}

Conservative Runtime Radius

r(\delta) = \sqrt{\frac{2\sigma^2 \log(8/\delta)}{D_{\text{eff}}}}

Lattice OU Multiplier

\text{decay}_m = \exp(-\Delta t \cdot \lambda_m)

Innovation Variance

\sigma^2_m = \frac{1 - \exp(-2\Delta t \cdot \lambda_m)}{\lambda_m}

Capstone Tail Bound

\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 $\texttt{gcc -Wall -Werror}$ — zero warnings.

Download verified-c.tar.gz

SAFE RUST

6 Rust modules + lib.rs. 13 tests pass, zero warnings. $\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 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)

⊢⊣⊢⊣

>_MENTAT.JOIN

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

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

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.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS