OS3 — Reflection Positivity for the GFF

Lifts covariance reflection positivity to the full generating functional via the Schur product theorem.

Real version (complete): For positive-time real fⱼ and real coefficients cⱼ:

∑ᵢⱼ cᵢcⱼ Z[fᵢ − Θfⱼ] = ∑ᵢⱼ cᵢ'cⱼ' exp(Rᵢⱼ) ≥ 0

where Rᵢⱼ = ⟨Θfᵢ, Cfⱼ⟩ is PSD by covariance reflection positivity, cᵢ' = cᵢ exp(−½⟨fᵢ,Cfᵢ⟩), and exp(Rᵢⱼ) is PSD by the Schur product theorem (entrywise exponential of a PSD matrix is PSD).

Complex version: For positive-time complex fⱼ and complex coefficients cⱼ:

∑ᵢⱼ cbarᵢcⱼ Z_ℂ[fᵢ − star fⱼ] ≥ 0

where star f = conj ∘ f ∘ Θ. The factorisation gives Z_ℂ[fᵢ − star fⱼ] = conj(Aᵢ)·Aⱼ·exp(Rᵢⱼ) with Hermitian PSD R, requiring the complex entrywise exponential PSD theorem.

Main results

• gaussianFreeField_OS3_real: os3ReflectionPositivityReal (muGFF m)
• gaussianFreeField_OS3: os3ReflectionPositivity (muGFF m) (complex)

theorem QFT.freeCovarianceFormR_reflection_matrix_posSemidef (m : ℝ) [Fact (0 < m)] {n : ℕ} (f : Fin n → PositiveTimeTestFunction) : Matrix.PosSemidef fun (i j : Fin n) => freeCovarianceFormR m (compTimeReflectionReal ↑(f i)) ↑(f j)

Reflection matrix built from the real covariance is positive semidefinite. This is the real analogue of covariance reflection positivity.

theorem QFT.freeCovarianceFormR_reflection_expansion (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : freeCovarianceFormR m (f - compTimeReflectionReal g) (f - compTimeReflectionReal g) = freeCovarianceFormR m f f + freeCovarianceFormR m g g - 2 * freeCovarianceFormR m (compTimeReflectionReal f) g

Quadratic expansion identity for reflected arguments.

theorem QFT.gaussianFreeField_real_generating_re (m : ℝ) [Fact (0 < m)] (h : TestFunction) : (GJGeneratingFunctional (gaussianFreeFieldFree m) h).re = Real.exp (-(1 / 2) * freeCovarianceFormR m h h)

Evaluate the real generating functional of the free field on a real test function.

theorem QFT.gaussianFreeField_real_entry_factor (m : ℝ) [Fact (0 < m)] {f g : PositiveTimeTestFunction} : (GJGeneratingFunctional (gaussianFreeFieldFree m) (↑f - compTimeReflectionReal ↑g)).re = (GJGeneratingFunctional (gaussianFreeFieldFree m) ↑f).re * (GJGeneratingFunctional (gaussianFreeFieldFree m) ↑g).re * Real.exp (freeCovarianceFormR m (compTimeReflectionReal ↑f) ↑g)

Factorisation of OS3 matrix entries in the purely real setting.

theorem QFT.gaussianFreeField_OS3_matrix_real (m : ℝ) [Fact (0 < m)] {n : ℕ} (f : Fin n → PositiveTimeTestFunction) (c : Fin n → ℝ) : 0 ≤ ∑ i : Fin n, ∑ j : Fin n, c i * c j * (GJGeneratingFunctional (gaussianFreeFieldFree m) (↑(f i) - compTimeReflectionReal ↑(f j))).re

Matrix formulation of the real OS3 inequality for the Gaussian free field.

theorem QFT.gaussianFreeField_OS3_real (m : ℝ) [Fact (0 < m)] : os3ReflectionPositivityReal (gaussianFreeFieldFree m)

Main theorem: the Gaussian free field satisfies OS3_real (reflection positivity, real version).

Helper lemmas for the complex OS3 proof

theorem QFT.gaussianFreeField_OS3 (m : ℝ) [Fact (0 < m)] : os3ReflectionPositivity (gaussianFreeFieldFree m)

Main theorem: the Gaussian free field satisfies OS3 (complex reflection positivity). This is the standard Osterwalder–Schrader formulation with complex-valued test functions and complex coefficients, compatible with OS reconstruction.

The star operation is (star f)(x) = conj(f(Θx)). For real test functions, star = compTimeReflection (see star_toComplex_eq_compTimeReflection).