Osterwalder-Schrader Axioms

The four OS axioms characterizing Euclidean field theories that admit analytic continuation to relativistic QFTs:

• OS-0: os0Analyticity - Complex analyticity of generating functionals
• OS-1: os1Regularity - Exponential bounds and temperedness
• OS-2: os2EuclideanInvariance - Euclidean group invariance
• OS-3: os3ReflectionPositivity - Reflection positivity (multiple formulations)
• OS-4: OS4Ergodicity - Ergodicity and clustering properties

Following Glimm-Jaffe formulation using probability measures on field configurations. Glimm and Jaffe, Quantum Physics, pp. 89-90

def os0Analyticity (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

OS0 (Analyticity): The generating functional is analytic in the test functions.

Equations

• os0Analyticity dμ_config = ∀ (n : ℕ) (J : Fin n → TestFunctionℂ), AnalyticOn ℂ (fun (z : Fin n → ℂ) => GJGeneratingFunctionalℂ dμ_config (∑ i : Fin n, z i • J i)) Set.univ

def TwoPointIntegrable (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

Two-point function local integrability condition for p = 2

Equations

• TwoPointIntegrable dμ_config = MeasureTheory.LocallyIntegrable (fun (x : SpaceTime) => SchwingerTwoPointFunction dμ_config x) MeasureTheory.volume

def os1Regularity (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

OS1 (Regularity): The complex generating functional satisfies exponential bounds.

Equations

• One or more equations did not get rendered due to their size.

def os2EuclideanInvariance (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

OS2 (Euclidean Invariance): The measure is invariant under Euclidean transformations.

Equations

• os2EuclideanInvariance dμ_config = ∀ (g : QFT.E) (f : TestFunctionℂ), GJGeneratingFunctionalℂ dμ_config f = GJGeneratingFunctionalℂ dμ_config (QFT.euclideanAction g f)

def os3ReflectionPositivity (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

OS3 (Reflection Positivity): The generating functional defines a positive semi-definite Hermitian form on positive-time test functions. This is the standard complex formulation (Osterwalder–Schrader 1975, axiom E2) using complex-valued test functions and complex coefficients with conjugation, compatible with OS reconstruction.

The star operation on TestFunctionℂ is (star f)(x) = conj(f(Θx)), combining time reflection with complex conjugation. This is required by the i factor in the characteristic function Z[J] = ∫ exp(i⟨ω,J⟩) dμ so that Z[f − star g] = ∫ exp(i⟨ω,f⟩) · conj(exp(i⟨ω,Θg⟩)) dμ.

For real positive-time test functions embedded via toComplex, star = compTimeReflection (see star_toComplex_eq_compTimeReflection), so this reduces to os3ReflectionPositivityReal.

Equations

• One or more equations did not get rendered due to their size.

def os3ReflectionPositivityReal (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

Real formulation of OS3 reflection positivity using real-valued positive-time test functions and real coefficients. This is equivalent to os3ReflectionPositivity for measures where the generating functional is real on real test functions (in particular for Gaussian measures).

Equations

• One or more equations did not get rendered due to their size.

def os4Clustering (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

OS4 (Clustering): Clustering via correlation decay.

This is an alternative formulation that directly expresses the clustering property: correlations between well-separated regions decay to zero. This is equivalent to ergodicity for translation-invariant measures.

The key identity is: Z[f + T_a g] → Z[f] · Z[g] as |a| → ∞ which says that distant test functions become statistically independent.

Translation is implemented via SchwartzMap.translate.

NOTE: This is stated for real test functions, which is the standard OS formulation. For real test functions, the generating functional satisfies |Z[f]| ≤ 1 due to positive definiteness of the covariance. The complex extension follows from analyticity (OS0) and regularity (OS1).

Equations

• One or more equations did not get rendered due to their size.

def OS4Ergodicity (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

OS4 (Ergodicity): For generating functions A(φ) = Σⱼ zⱼ e^{⟨φ,fⱼ⟩}, the time average converges to the expectation in L²(μ).

lim_{T→∞} (1/T) ∫₀ᵀ A(T_s φ) ds → 𝔼_μ[A(φ)]

This is the standard ergodicity formulation from Glimm-Jaffe.

Equations

• One or more equations did not get rendered due to their size.

def os4PolynomialClustering (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (α : ℝ) (_hα : α > 0) : Prop

OS4 (Polynomial Clustering): For any f, g ∈ S(ℝ × ℝ³) and any exponent α > 0, there exists c such that:

|𝔼_μ[e^{⟨φ,f⟩ + ⟨T_s φ, g⟩}] - 𝔼_μ[e^{⟨φ,f⟩}] 𝔼_μ[e^{⟨φ,g⟩}]| ≤ c (1 + s)^{-α}

This is a generalization of the clustering property that allows for any polynomial decay rate. For the GFF in 4D spacetime (d=3 spatial dimensions), the natural rate is α = 2d = 6 from the mass gap.

Equations

• One or more equations did not get rendered due to their size.

Bundled Axiom Conjunction

structure SatisfiesAllOS (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

A probability measure on field configurations satisfies all Osterwalder-Schrader axioms. This bundles OS0 through OS4 (clustering and ergodicity) into a single predicate.

• os0 : os0Analyticity dμ_config
• os1 : os1Regularity dμ_config
• os2 : os2EuclideanInvariance dμ_config
• os3 : os3ReflectionPositivity dμ_config
• os4_clustering : os4Clustering dμ_config
• os4_ergodicity : OS4Ergodicity dμ_config