Nontriviality of the Gaussian Free Field

The OS axiom verification in OS.Master would be trivially satisfied by the Dirac measure at ω = 0 (the "zero field"). This file closes that loophole by proving the GFF measure is strictly non-degenerate:

1. The square-root propagator embedding T : S(ℝ⁴) → L² is injective.
2. The smeared covariance C(f,f) > 0 for every nonzero test function f.
3. Every field pairing ⟨ω,f⟩ has strictly positive variance under muGFF.
4. The pointwise kernel C(x,y) → +∞ as x → y (UV divergence).

Proof strategy

Injectivity of T follows from:

• Fourier transform is injective on Schwartz space (Mathlib's FourierPair instance gives a left inverse 𝓕⁻ ∘ 𝓕 = id).
• The momentum-space weight 1/√(‖k‖² + m²) is everywhere positive, so multiplication by it cannot create new zeros.
• A continuous function that vanishes a.e. with respect to Lebesgue measure vanishes everywhere (volume is an IsOpenPosMeasure).

Main results

• toComplex_injective : embedding S(ℝ⁴,ℝ) ↪ S(ℝ⁴,ℂ) is injective
• fourierTransform_schwartz_injective : 𝓕 on Schwartz space is injective
• embeddingMap_injective : the square-root propagator embedding is injective
• freeCovarianceFormR_strictPos : C(f,f) > 0 for f ≠ 0
• gaussianFreeField_variance_pos : Var[⟨ω,f⟩] > 0 for f ≠ 0
• gaussianFreeField_not_dirac : muGFF ≠ δ₀
• besselK1_tendsto_atTop_at_zero : K₁(z) → +∞ as z → 0⁺
• freeCovariance_tendsto_atTop : C(x,y) → +∞ as x → y

References

• Glimm–Jaffe, Quantum Physics, §6.1 (nondegeneracy of the free field)
• Reed–Simon, Methods of Modern Mathematical Physics II, §IX.8

Injectivity of the real-to-complex embedding

theorem OSforGFF.toComplex_injective : Function.Injective toComplex

The embedding toComplex : S(ℝ⁴,ℝ) → S(ℝ⁴,ℂ) is injective. Follows from injectivity of ℝ → ℂ applied pointwise.

Injectivity of the Fourier transform on Schwartz space

theorem OSforGFF.fourierTransform_schwartz_injective : Function.Injective ⇑(SchwartzMap.fourierTransformCLM ℂ)

The Fourier transform is injective on complex Schwartz space. Proof: FourierPair gives 𝓕⁻(𝓕 f) = f, so 𝓕 has a left inverse.

Continuous functions that vanish a.e. vanish everywhere

Injectivity of the square-root propagator embedding

theorem OSforGFF.sqrtPropagatorMap_eq_zero_iff (m : ℝ) [Fact (0 < m)] (f : TestFunction) : (∀ (k : SpaceTime), QFT.sqrtPropagatorMap m f k = 0) ↔ f = 0

The square-root propagator map is zero pointwise only if f = 0.

sqrtPropagatorMap m f k = 𝓕(toComplex f)(k) · w(k) where w(k) > 0, so vanishing of the product forces 𝓕(toComplex f) = 0, hence f = 0 by Fourier injectivity.

theorem OSforGFF.embeddingMap_injective (m : ℝ) [Fact (0 < m)] : Function.Injective ⇑(QFT.embeddingMap m)

The embedding T : S(ℝ⁴,ℝ) → L²(ℝ⁴,ℂ) is injective.

If T f = T g then ‖T(f−g)‖ = 0, so ∫ |sqrtPropagatorMap m (f−g)|² = 0. The integrand is continuous and nonneg, so it vanishes a.e., hence everywhere (volume is IsOpenPosMeasure). Since the momentum weight is positive, the Fourier transform of f−g vanishes, giving f = g.

Strict positivity of the covariance

theorem OSforGFF.freeCovarianceFormR_strictPos (m : ℝ) [Fact (0 < m)] (f : TestFunction) (hf : f ≠ 0) : 0 < QFT.freeCovarianceFormR m f f

Strict positive definiteness: the smeared covariance C(f,f) > 0 for any nonzero test function f. This rules out the Dirac-at-zero measure as a model satisfying the OS axioms.

Proof: C(f,f) = ‖T f‖² where T is injective, so f ≠ 0 ⟹ T f ≠ 0 ⟹ ‖T f‖ > 0 ⟹ ‖T f‖² > 0.

Nontriviality of the GFF measure

theorem OSforGFF.gaussianFreeField_variance_pos (m : ℝ) [Fact (0 < m)] (f : TestFunction) (hf : f ≠ 0) : 0 < ∫ (ω : FieldConfiguration), (distributionPairingCLM f) ω ^ 2 ∂↑(muGFF m)

The variance of ⟨ω,f⟩ under the GFF is strictly positive for f ≠ 0. Equivalently, the pushforward by the pairing is a non-degenerate Gaussian.

theorem OSforGFF.gaussianFreeField_not_dirac (m : ℝ) [Fact (0 < m)] : ∃ (f : TestFunction), f ≠ 0 ∧ 0 < ∫ (ω : FieldConfiguration), (distributionPairingCLM f) ω ^ 2 ∂↑(muGFF m)

The GFF is not a Dirac measure: there exists a test function whose pairing with ω has nonzero variance. This is the formal statement that the OS axiom verification in Master.lean is nontrivial.

Any nonzero Schwartz function witnesses this. We use a standard bump function on ℝ⁴, which exists by ContDiff.exists_eq_one_of_isOpen.

UV divergence: pointwise covariance diverges at coincident points

The pointwise regularization C(x,x) = 0 in freeCovarianceBessel is a convention for the smeared (distribution) theory. The actual limit diverges, confirming that the free field has genuine UV singularity.

The smeared covariance C(f,f) = ∫∫ f(x) C(x,y) f(y) dx dy remains finite for all Schwartz functions because the 1/r² singularity of K₁(mr)/r is integrable in 4 spatial dimensions (surface area r³ compensates the kernel 1/r²).

theorem OSforGFF.besselK1_tendsto_atTop_at_zero : Filter.Tendsto besselK1 (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

K₁(z) → +∞ as z → 0⁺.

For any T > 0, K₁(z) = ∫₀^∞ e^{-z cosh t} cosh t dt ≥ T · e^{-z cosh T} since cosh t ≥ 1 on [0,T]. As z → 0⁺ the RHS → T, so K₁(z) eventually exceeds any bound.

Formal proof uses monotone convergence: the integrand e^{-z cosh t} cosh t increases monotonically to cosh t as z ↓ 0, and ∫₀^∞ cosh t dt = +∞.

theorem OSforGFF.freeCovariance_tendsto_atTop (m : ℝ) [Fact (0 < m)] (x₀ : SpaceTime) : Filter.Tendsto (fun (x : SpaceTime) => freeCovarianceBessel m x₀ x) (nhdsWithin x₀ {x₀}ᶜ) Filter.atTop

The free covariance C(x,y) → +∞ as x → y (UV divergence).

C(x,y) = (m/(4π²r)) · K₁(mr) where r = ‖x-y‖. As r → 0⁺, K₁(mr) ≥ K₁(1) > 0 for mr ≤ 1 and m/(4π²r) → +∞, so the product diverges.