Master Theorem

Assembles OS0–OS4 into gaussianFreeField_satisfies_all_OS_axioms:

• OS0 (Analyticity): Hartogs + Fernique — OS.os0Analyticity
• OS1 (Regularity): Plancherel + momentum bound — OS.os1Regularity
• OS2 (Euclidean Invariance): C depends on |x−y| — OS.OS2_Invariance
• OS3 (Reflection Positivity): Schwinger parametrization + Schur–Hadamard — OS.os3ReflectionPositivity
• OS4 (Clustering): Gaussian factorization + convolution decay — OS.os4Clustering
• OS4 (Ergodicity): polynomial clustering α=6 → L² convergence — OS.OS4Ergodicity

Unconditional theorem: only requires m > 0.

Master OS theorem for the free GFF

theorem OSforGFF.gaussianFreeField_satisfies_all_OS_axioms (m : ℝ) [Fact (0 < m)] : SatisfiesAllOS (muGFF m)

Master theorem: the free GFF satisfies all Osterwalder-Schrader axioms.

• OS0 is supplied by QFT.gaussianFreeField_satisfies_OS0 via the holomorphic integral theorem
• OS1 is supplied by gaussianFreeField_satisfies_OS1_revised via Fourier/momentum space methods
• OS2 is supplied by gaussian_satisfies_OS2 via Euclidean invariance of the free covariance
• OS3 is supplied by QFT.gaussianFreeField_OS3 via the Schur-Hadamard argument (complex star formulation)
• OS4 Clustering is supplied by QFT.gaussianFreeField_satisfies_OS4 via Gaussian factorization
• OS4 Ergodicity is supplied by polynomial clustering (α=6) → ergodicity

This is an unconditional theorem with no assumptions beyond m > 0.