We construct the massive Gaussian Free Field (GFF) as a probability measure on the space of tempered distributions S'(ℝ^d), and prove that it satisfies all five Osterwalder-Schrader axioms for a Euclidean quantum field theory. The construction and proofs are formalized in Lean 4 / Mathlib, following the conventions and methods of proof in Glimm and Jaffe, Quantum Physics: A Functional Integral Point of View (Springer, 1987).
The library is dimension-generic: the spacetime dimension is a parameter
d (any d ≥ 2), and the only per-dimension input is the closed form of
the radial covariance profile, isolated behind the two-field typeclass
GFFPropagator d m (see docs/dimension_generic.md).
Four instances are provided in OSforGFF/Instances/: the four-dimensional Bessel
kernel (m/4π²r)K₁(mr), the three-dimensional Yukawa kernel e^{−mr}/(4πr), the
two-dimensional Bessel kernel (1/2π)K₀(mr), and the five-dimensional K_{3/2}
kernel (1+mr)e^{−mr}/(8π²r³).
theorem gaussianFreeField_satisfies_all_OS_axioms_generic
{d : ℕ} [Fact (2 ≤ d)] (m : ℝ) [Fact (0 < m)] [GFFPropagator d m] :
SatisfiesAllOS (gaussianFreeField_free (d := d) m)
theorem gaussianFreeField_satisfies_all_OS_axioms_dim4 (m : ℝ) [Fact (0 < m)] :
SatisfiesAllOS (μ_GFF 4 m)
theorem gaussianFreeField_satisfies_all_OS_axioms_dim3 (m : ℝ) [Fact (0 < m)] :
SatisfiesAllOS (μ_GFF 3 m)
theorem gaussianFreeField_satisfies_all_OS_axioms_dim2 (m : ℝ) [Fact (0 < m)] :
SatisfiesAllOS (μ_GFF 2 m)
theorem gaussianFreeField_satisfies_all_OS_axioms_dim5 (m : ℝ) [Fact (0 < m)] :
SatisfiesAllOS (μ_GFF 5 m)where SatisfiesAllOS bundles OS0 (analyticity), OS1 (regularity), OS2
(Euclidean invariance), OS3 (reflection positivity), OS4 (clustering) and OS4
(ergodicity). The four _dim4/_dim3/_dim2/_dim5 theorems are the closed-form
instances (Bessel K₁, Yukawa, K₀, K_{3/2}) of the first; the corollary
gaussianFreeField_satisfies_all_OS_axioms_of_dim covers every d ≥ 2 via the
canonical proper-time propagator: the OS3 proper-time Fubini domination runs at
boundary-vanishing order d, so no upper bound on the dimension is needed.
Status: Version 3.2 (general dimension d ≥ 2), August 2026. 0 sorries, 0 axioms, ~25,500 lines of Lean across 52 on-graph files (plus the off-graph OS/NonTrivial.lean and 6 off-graph Legacy/ files). Instances for d = 2, 3, 4, 5; the axiom footprint and statement type of every headline theorem (generic, all-dimensions d ≥ 2, d = 4, d = 3, d = 2, d = 5) are build-frozen in OSforGFF/Guardrails.lean.
All results are fully proved — no assumed axioms. Nuclear space structure and the Minlos theorem are provided by the external libraries bochner and gaussian-field, which are themselves axiom-free. The Minlos proof uses the external library kolmogorov_extension4.
The 52 on-graph library files (plus the off-graph OS/NonTrivial.lean and 6 off-graph
Legacy/ files, below) are organized into 7 layers, with imports flowing from
earlier to later sections (three exceptions, listed under "Cross-cutting dependencies"
below). See docs/architecture.md for dependency structure,
design choices, and proof outlines, and docs/dimension_generic.md
for the dimension-generic design. For a pedagogical, axiom-by-axiom walkthrough of the
OS proofs — ordered by complexity, with pointers into the code — see
docs/pedagogical/Overview.md. The dependency graph source is in
dependency/import_graph.dot (render with dot -Tsvg).
Pure extensions of Mathlib with no project-specific definitions.
Test functions, symmetries, and integration infrastructure.
Generating functionals and correlation functions.
The free scalar field propagator C(x,y) = Cprofile(|x−y|), isolated behind the
GFFPropagator d m typeclass and analyzed through its proper-time (Schwinger)
representation, uniformly in the dimension.
Construction of the GFF probability measure via the Minlos theorem.
Note: IsGaussian imports OS0_Analyticity because it uses the proved analyticity of
Z[z₀f + z₁g] to identify S₂(f,g) = C(f,g) via the identity theorem. The dependency
is on the OS0 result, not on OS0-specific infrastructure.
Axiom definitions, individual proofs, and master theorem.
Per-dimension closed forms of the covariance, packaged as GFFPropagator instances.
OSforGFF/Legacy/ preserves genuine proven mathematics that the on-graph library no longer
consumes: the original four-dimensional development superseded in role by the dimension-generic
machinery, and the verified-dead declarations quarantined by the library-wide sweep. These files
are not imported by OSforGFF.lean and are not compiled by lake build; each carries a
module docstring with its supersession map, and is verified in isolation with lake env lean
(build BesselK1Analytics's olean first, since Dim4Bessel depends on it).
| File | Description |
|---|---|
| Legacy/Dim4Bessel | The original 4D Bessel/momentum program: the named Bessel kernel freeCovarianceBessel/freeCovariance4, regulated-covariance / Fubini / momentum-space development, heat-kernel and Schwinger-representation defs, superseded by Covariance/Propagator.lean + Covariance/ParsevalGeneric.lean + General/BesselK.lean |
| Legacy/BesselK1Analytics | The K₁ analytic lemmas (positivity, continuity, asymptotic/near-origin bounds, radial integrability) that supported the 4D analysis |
| Legacy/UnusedGeneral | Consumer-less general-analysis lemmas (Fourier/functional-analysis side lemmas, the entire former FrobeniusPositivity.lean, the L² time-average and weighted-Minkowski programs) |
| Legacy/UnusedSpacetime | Consumer-less spacetime-layer declarations (Schwartz multiplication, spatial L², the matrix presentation of time reflection, unified Euclidean actions, openness of the positive-time set) |
| Legacy/UnusedMeasureSchwinger | Consumer-less measure/Schwinger-layer declarations (the alternative OS0_alt program, RBF/symmetry Minlos corollaries, the exponential-series expansion of the generating functional) |
| Legacy/UnusedOS | Consumer-less OS-layer declarations (OS0 side lemmas, pre-H3 OS3 chain steps incl. bilinear_to_k0_inside, the ε–δ clustering formulation, kernel isometry invariance) |
We depend on three auxiliary Lean libraries for nuclear space theory and measure construction. All are axiom-free.
bochner (BochnerMinlos)
| Module | What we use | Imported by |
|---|---|---|
Minlos.Main |
minlos_theorem — existence and uniqueness of probability measures from characteristic functionals on nuclear spaces |
Minlos |
Minlos.NuclearSpace |
IsHilbertNuclear typeclass; MeasurableSpace (WeakDual ℝ E) cylinder σ-algebra instance |
Basic, NuclearSpace |
Minlos.PietschBridge |
isHilbertNuclear_of_nuclear — bridge from Pietsch to Hilbert-Schmidt characterization |
NuclearSpace |
Bochner.PositiveDefinite |
IsPositiveDefinite structure for characteristic functionals |
Minlos |
gaussian-field (GaussianField)
| Module | What we use | Imported by |
|---|---|---|
SchwartzNuclear.HermiteNuclear |
schwartz_separableSpace — Schwartz space is separable (via Hermite basis) |
NuclearSpace |
Nuclear.NuclearSpace |
DyninMityaginSpace → NuclearSpace — proves Schwartz space is nuclear |
NuclearSpace |
kolmogorov_extension4 (transitive, via bochner)
| Module | What we use | Imported by |
|---|---|---|
KolmogorovExtension4.KolmogorovExtension |
projectiveLimit — Kolmogorov extension theorem: constructs a measure on the infinite product from a consistent projective family of finite-dimensional measures |
bochner's Minlos.ProjectiveFamily |
The import graph (dependency/import_graph.dot) is mostly layered, with three
cross-cutting dependencies:
- IsGaussian → OS0_Analyticity: Gaussianity verification uses the OS0 analyticity result to identify S₂(f,g) = C(f,g) via the identity theorem (see Section 5 note)
- GaussianMoments → Measure/Construct: the moment bounds are stated for the constructed free-field measure
- Measure/GaussianFreeField → OS/Axioms: the OS2 statement it proves lives in the axioms module
These prevent a perfectly linear ordering but do not create a circular dependency.
lake buildRequires Lean 4 and Mathlib (pinned via lake-manifest.json). The build also compiles
OSforGFF/Guardrails.lean, whose #guard_msgs blocks freeze the
axiom footprint and statement type of all six headline theorems (generic, all-dimensions
d ≥ 2, and d = 4, 3, 2, 5) — so lake build fails if any change introduces a new axiom,
leaks a sorry, or alters a headline statement.
A companion scripts/check-guardrails.sh checks the same invariant at the source level, without
needing a build:
./scripts/check-guardrails.sh # exit 0 = clean, exit 2 = violationIt scans every module reachable from OSforGFF.lean for axiom declarations, sorry/admit,
and kernel escape hatches (native_decide, unsafe, implemented_by, extern), stripping
comments first so prose that merely names them is not a false positive. The check is absolute
rather than relative to a baseline revision, so it cannot silently pass by losing its reference
point; set GUARDRAIL_BASE=<rev> to additionally report which violations a given range
introduced. OSforGFF/Legacy/ is exempt — it is deliberately off the import graph and never
compiled.
Both checks run in CI on every push and pull request (.github/workflows/ci.yml),
which also replays the built environment through an external kernel check (leanchecker).
- or4nge19/OSforGFF — A fork by Matteo Cipollina pursuing a different measure construction pipeline: finite-dimensional Gaussians → Kolmogorov extension on test functions → nuclear support → pushforward to distribution space, avoiding the Minlos theorem. Develops coordinate-free Euclidean time-direction and dimension-agnostic Hermite APIs.
The— Done. Thed = 2instance (the K₀ kernel (1/2π)K₀(mr))d = 2(K₀),d = 3(Yukawa),d = 4(Bessel K₁), andd = 5(K_{3/2}) instances are all provided, completing the dimensions discussed in docs/dimension_dependence.md.Explicit construction of the measure not using Minlos— Done. The Minlos theorem and Kolmogorov extension are now fully proved in bochner and kolmogorov_extension4.General dimension— Done. The OS3 Fubini domination now runs at boundary-vanishing orderd ≥ 2d(positive-time test functions are flat to all orders at the time boundary), so the OS theorems hold in every dimensiond ≥ 2; the program and its implementation are written up in docs/general_dimension.md.
Sergey A. Cherkis, Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim
Claude Opus 4.6, Claude Fable 5, Gemini 3 Pro, GPT-5.2 Codex
This project is licensed under the Apache License, Version 2.0. See LICENSE for details.
- Glimm, Jaffe: Quantum Physics (Springer, 1987), pp. 89–90
- Osterwalder, Schrader: Axioms for Euclidean Green's functions I & II (1973, 1975)
- Gel'fand, Vilenkin: Generalized Functions, Vol. 4 (Academic Press, 1964)
- Reed, Simon: Methods of Modern Mathematical Physics, Vol. II (1975)
- Degenne, Pfaffelhuber: Formalizing the Kolmogorov Extension Theorem in Lean (kolmogorov_extension4)