OSforGFF

Osterwalder-Schrader Axioms for the Gaussian Free Field

We construct the massive Gaussian Free Field (GFF) in four spacetime dimensions as a probability measure on the space of tempered distributions S'(ℝ⁴), 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).

Master Theorem

theorem gaussianFreeField_satisfies_all_OS_axioms (m : ℝ) [Fact (0 < m)] :
  OS0_Analyticity (μ_GFF m) ∧
  OS1_Regularity (μ_GFF m) ∧
  OS2_EuclideanInvariance (μ_GFF m) ∧
  OS3_ReflectionPositivity (μ_GFF m) ∧
  OS4_Clustering (μ_GFF m) ∧
  OS4_Ergodicity (μ_GFF m)

Status: Version 2.0, March 2026. 0 sorries, 0 axioms, ~32,000 lines of Lean across 47 files.

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.

Project Structure

The 47 library files are organized into 6 layers, with imports flowing from earlier to later sections. See docs/architecture.md for dependency structure, design choices, and proof outlines. The dependency graph is in dependency/import_graph.svg.

1. General Mathematics — `OSforGFF/General/`

Pure extensions of Mathlib with no project-specific definitions.

File	Contents
FunctionalAnalysis	L² Fourier transform infrastructure, Plancherel identity
FrobeniusPositivity	Frobenius inner product, positive semidefinite matrix theory
SchurProduct	Schur product theorem (Hadamard product preserves PSD)
HadamardExp	Entrywise exponential of PSD matrices is PSD
PositiveDefinite	Positive definite functions and kernels
GaussianRBF	Gaussian RBF kernel exp(-‖x-y‖²) is positive definite
FourierTransforms	1D Fourier identities: Lorentzian ↔ exponential decay
LaplaceIntegral	Laplace integral identity (Bessel K_{1/2}): ∫ s^{-1/2} e^{-a/s-bs} ds
BesselFunction	Modified Bessel function K₁ via integral representation
QuantitativeDecay	Schwartz bilinear forms with exponentially decaying kernels have polynomial decay
SchwartzTranslationDecay	Schwartz seminorm bounds under translation
L2TimeIntegral	L² bounds for time integrals: Cauchy-Schwarz, Fubini, Minkowski

2. Spacetime — `OSforGFF/Spacetime/`

Test functions, symmetries, and integration infrastructure.

File	Contents
Basic	SpaceTime (ℝ⁴), TestFunction, FieldConfiguration, distribution pairing
Euclidean	Euclidean group E(4) = ℝ⁴ ⋊ O(4) and its action on test functions
DiscreteSymmetry	Time reflection Θ: (t,x̄) ↦ (−t,x̄)
Decomposition	Measure-preserving SpaceTime ≃ ℝ × ℝ³ decomposition
ComplexTestFunction	Complex-valued Schwartz test functions and conjugation
PositiveTimeTestFunction	Subtype of test functions supported at positive time
TimeTranslation	Time translation operators T_s on Schwartz space
ProdIntegrable	Integrability of Schwartz function products
Tonelli	Tonelli/Fubini for Schwartz integrands on spacetime

3. Schwinger — `OSforGFF/Schwinger/`

Generating functionals and correlation functions.

File	Contents
Defs	Generating functional Z[J] = ∫ e^{i⟨φ,J⟩} dμ, Schwinger n-point functions
TwoPoint	Two-point function S₂(x) as mollifier limit
GaussianMoments	Gaussian moments: all n-point functions are integrable

4. Covariance — `OSforGFF/Covariance/`

The free scalar field propagator C(x,y) = (m/4π²|x−y|) K₁(m|x−y|) and its properties.

File	Contents
Momentum	Momentum-space propagator 1/(k²+m²), decay bounds
Parseval	Parseval identity: ⟨f,Cf⟩ = ∫\|f̂(k)\|² P(k) dk
Position	Position-space covariance, Euclidean invariance, Schwinger representation
RealForm	Real covariance bilinear form, square root propagator embedding

5. Measure — `OSforGFF/Measure/`

Construction of the GFF probability measure via the Minlos theorem.

File	Contents
NuclearSpace	Schwartz space is Hilbert-nuclear and separable (bridges bochner + gaussian-field)
Minlos	Minlos theorem application, Gaussian measure construction
MinlosAnalytic	Symmetry and moments for Gaussian measures (sign-flip invariance, zero mean)
Construct	GFF measure construction: covariance → characteristic functional → μ
IsGaussian	Verification that S₂(f,g) = C(f,g) via OS0 derivative interchange
GaussianFreeField	Main GFF assembly: μ_GFF m as a ProbabilityMeasure

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.

6. OS Axioms — `OSforGFF/OS/`

Axiom definitions, individual proofs, and master theorem.

File	Contents
Axioms	Formal Lean definitions of OS0 through OS4
OS0_Analyticity	Closed-form Z[f] = exp(-½ C(f,f)) via identity theorem + Fernique
OS1_Regularity	Plancherel + momentum-space bound: \|Z[f]\| ≤ exp(‖f‖²/2m²)
OS2_Invariance	C(x,y) depends only on \|x−y\|, Lebesgue measure invariance
OS3_MixedRepInfra	Schwinger parametrization and Fubini theorems for absolute integrability
OS3_MixedRep	Mixed representation via Schwinger → heat kernel → Laplace transform
OS3_CovarianceRP	Covariance reflection positivity: ⟨Θf, Cf⟩ = ∫ (1/ω)\|F_ω\|² ≥ 0
OS3_ReflectionPositivity	Schur–Hadamard lifts covariance RP to generating functional
OS4_MGF	Shared infrastructure: MGF formula, time translation duality
OS4_Clustering	Gaussian factorization + convolution decay lemma (domain split at ‖y‖=‖x‖/2)
OS4_Ergodicity	Polynomial clustering (α=6) → L² convergence
NonTrivial	Nontriviality: C(f,f) > 0, positive variance, UV divergence C(x,y) → ∞
Master	Assembles OS0–OS4 into `gaussianFreeField_satisfies_all_OS_axioms`

External Libraries

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`

Dependencies and Cross-Cutting Concerns

The import graph (dependency/import_graph.svg) is mostly layered, with one cross-cutting dependency:

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)

This prevents a perfectly linear ordering but does not create a circular dependency.

Building

lake build

Requires Lean 4 and Mathlib (pinned via lake-manifest.json).

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.

Planned Generalizations

Other spacetime dimensions, as 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.

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)