OS3 — Covariance Reflection Positivity

Proves ⟨Θf, Cf⟩ ≥ 0 for positive-time test functions f, using the mixed representation derived in OS3_MixedRep:

⟨Θf, Cf⟩ = (1/2(2π)³) ∫_{kbar} (1/ω) |∫ ftilde(t, kbar) e^{−ωt} dt|² dkbar ≥ 0

The key factorization: for f supported at positive time, |x₀+y₀| = x₀+y₀, so e^{−ω|x₀+y₀|} = e^{−ωx₀} · e^{−ωy₀} and the bilinear form becomes a perfect square ∫ (1/ω)|F_ω(kbar)|² dkbar with F_ω(kbar) = ∫ ftilde(t,kbar) e^{−ωt} dt.

Main results

• freeCovariance_reflection_positive_bilinear: ⟨Θf, Cf⟩ ≥ 0 (complex)
• freeCovariance_reflection_positive_real: real-valued version

Reflection Positivity Inner Product

The reflection positivity inner product is defined using the distributional bilinear form composed with the star operation. This is the mathematically correct formulation that avoids non-convergent pointwise integrals.

noncomputable def QFT.rpInnerProduct (m : ℝ) (f : TestFunctionℂ) : ℂ

The reflection positivity inner product using the distributional bilinear form: ⟨Θf, f⟩_C = freeCovarianceℂBilinear m (star f) f = ∫∫ conj(f(Θx)) * C(x,y) * f(y) dx dy

The star operation on TestFunctionℂ is defined as: (star f)(x) = conj(f(Θx)) (time reflection composed with conjugation)

This is the distributional formulation that is mathematically well-defined for Schwartz test functions.

Equations

• QFT.rpInnerProduct m f = freeCovarianceℂBilinear m (star f) f

Direct Proof of Reflection Positivity

The following namespace contains the complete self-contained proof of reflection positivity using the direct momentum representation approach.

Part 1: Core Definitions

noncomputable def QFT.RPProof.timeReflection (x : SpaceTime) : SpaceTime

The timeReflection declaration.

Equations

• QFT.RPProof.timeReflection x = (WithLp.equiv 2 ((i : Fin STDimension) → (fun (x : Fin STDimension) => ℝ) i)).symm (Function.update x.ofLp 0 (-x.ofLp 0))

theorem QFT.RPProof.timeReflection_involutive : Function.Involutive timeReflection

noncomputable def QFT.RPProof.spatialDot (k_spatial x_spatial : SpatialCoords) : ℝ

The spatialDot declaration.

Equations

• QFT.RPProof.spatialDot k_spatial x_spatial = ∑ i : Fin (STDimension - 1), k_spatial.ofLp i * x_spatial.ofLp i

noncomputable def QFT.RPProof.freeCovarianceℂBilinear (m : ℝ) (f g : TestFunctionℂ) : ℂ

The freeCovarianceℂBilinear declaration.

Equations

• QFT.RPProof.freeCovarianceℂBilinear m f g = ∫ (x : SpaceTime) (y : SpaceTime), f x * ↑(freeCovariance m x y) * g y

noncomputable def QFT.RPProof.weightedLaplaceFourier (m : ℝ) (f : TestFunctionℂ) (k_sp : SpatialCoords) : ℂ

The weightedLaplaceFourier declaration.

Equations

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

noncomputable def QFT.RPProof.rpInnerProduct (m : ℝ) (f : TestFunctionℂ) : ℂ

Reflection-positivity quadratic form used in the direct proof namespace.

Equations

• QFT.RPProof.rpInnerProduct m f = QFT.RPProof.freeCovarianceℂBilinear m (star f) f

Part 2: Change of Variables

theorem QFT.RPProof.star_apply (f : TestFunctionℂ) (x : SpaceTime) : (star f) x = (starRingEnd ℂ) (f (timeReflection x))

theorem QFT.RPProof.rpInnerProduct_eq_bessel_reflected (m : ℝ) (f : TestFunctionℂ) : rpInnerProduct m f = ∫ (x : SpaceTime) (y : SpaceTime), (starRingEnd ℂ) (f x) * ↑(freeCovariance m (timeReflection x) y) * f y

Part 3: Mixed Representation (Direct Approach)

theorem QFT.RPProof.mixed_representation (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : rpInnerProduct m f = ↑(1 / (2 * (2 * Real.pi) ^ (STDimension - 1))) * ∫ (k_sp : SpatialCoords) (x : SpaceTime) (y : SpaceTime), have ω := √(‖k_sp‖ ^ 2 + m ^ 2); (starRingEnd ℂ) (f x) * f y * ↑(1 / ω) * Complex.exp (-↑|-x.ofLp 0 - y.ofLp 0| * ↑ω) * Complex.exp (-Complex.I * ↑(spatialDot k_sp (spatialPart x - spatialPart y)))

The mixed representation from the Schwinger pathway. This is more direct than the k₀-inside form for proving reflection positivity, because (1/ω) exp(-ω|t|) already factorizes for positive-time test functions.

Part 4: Key Lemmas

theorem QFT.RPProof.energy_pos (m : ℝ) [Fact (0 < m)] (k_sp : SpatialCoords) : 0 < √(‖k_sp‖ ^ 2 + m ^ 2)

Part 5: Factorization Helpers

theorem QFT.RPProof.abs_neg_sum_nonneg (x0 y0 : ℝ) (hx : 0 ≤ x0) (hy : 0 ≤ y0) : |-x0 - y0| = x0 + y0

theorem QFT.RPProof.spatialDot_sub (k_sp x_sp y_sp : SpatialCoords) : spatialDot k_sp (x_sp - y_sp) = spatialDot k_sp x_sp - spatialDot k_sp y_sp

theorem QFT.RPProof.exp_spatial_phase_factor (k_sp x_sp y_sp : SpatialCoords) : Complex.exp (-Complex.I * ↑(spatialDot k_sp (x_sp - y_sp))) = Complex.exp (-Complex.I * ↑(spatialDot k_sp x_sp)) * Complex.exp (Complex.I * ↑(spatialDot k_sp y_sp))

noncomputable def QFT.RPProof.xIntegralFactor (f : TestFunctionℂ) (ω : ℝ) (k_sp : SpatialCoords) : ℂ

The xIntegralFactor declaration.

Equations

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

noncomputable def QFT.RPProof.yIntegralFactor (f : TestFunctionℂ) (ω : ℝ) (k_sp : SpatialCoords) : ℂ

The yIntegralFactor declaration.

Equations

• QFT.RPProof.yIntegralFactor f ω k_sp = ∫ (y : SpaceTime), f y * Complex.exp (-(↑ω * ↑(y.ofLp 0))) * Complex.exp (Complex.I * ↑(QFT.RPProof.spatialDot k_sp (spatialPart y)))

theorem QFT.RPProof.norm_neg_eq (k_sp : SpatialCoords) : ‖-k_sp‖ = ‖k_sp‖

theorem QFT.RPProof.spatialDot_neg_left (k_sp x_sp : SpatialCoords) : spatialDot (-k_sp) x_sp = -spatialDot k_sp x_sp

theorem QFT.RPProof.xIntegralFactor_eq_conj_neg (m : ℝ) (f : TestFunctionℂ) (k_sp : SpatialCoords) (_hf_support : ∀ (x : SpaceTime), x.ofLp 0 < 0 → f x = 0) : xIntegralFactor f (√(‖k_sp‖ ^ 2 + m ^ 2)) k_sp = (starRingEnd ℂ) (weightedLaplaceFourier m f (-k_sp))

theorem QFT.RPProof.yIntegralFactor_eq_neg (m : ℝ) (f : TestFunctionℂ) (k_sp : SpatialCoords) : yIntegralFactor f (√(‖k_sp‖ ^ 2 + m ^ 2)) k_sp = weightedLaplaceFourier m f (-k_sp)

Part 6: Factorization to Squared Norm (Direct Approach)

theorem QFT.RPProof.factorization_to_squared_norm_direct (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (k_sp : SpatialCoords) (hf_support : ∀ (x : SpaceTime), x.ofLp 0 < 0 → f x = 0) : have ω := √(‖k_sp‖ ^ 2 + m ^ 2); ∫ (x : SpaceTime) (y : SpaceTime), (starRingEnd ℂ) (f x) * f y * ↑(1 / ω) * Complex.exp (-↑|-x.ofLp 0 - y.ofLp 0| * ↑ω) * Complex.exp (-Complex.I * ↑(spatialDot k_sp (spatialPart x - spatialPart y))) = ↑(1 / ω * Complex.normSq (weightedLaplaceFourier m f (-k_sp)))

Direct factorization from the mixed representation.

For positive-time test functions, the mixed representation integrand (1/ω) exp(-ω|t|) exp(-ik_sp·r) factorizes directly because:

• |t| = |-x₀-y₀| = x₀+y₀ when x₀, y₀ ≥ 0
• exp(-ω(x₀+y₀)) = exp(-ωx₀) · exp(-ωy₀)
• exp(-ik_sp·r) = exp(-ik_sp·x_sp) · exp(+ik_sp·y_sp)

This avoids the round-trip through k₀ space that the old proof used.

Part 7: Final Representation

theorem QFT.RPProof.rp_equals_squared_norm_integral (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : rpInnerProduct m f = ↑(1 / (2 * (2 * Real.pi) ^ (STDimension - 1))) * ∫ (k_sp : SpatialCoords), ↑(1 / √(‖k_sp‖ ^ 2 + m ^ 2) * Complex.normSq (weightedLaplaceFourier m f (-k_sp)))

The RP inner product equals (1/(2(2π)^{d-1})) ∫_{k_sp} (1/ω) |F_ω(-k_sp)|².

This follows directly from the mixed representation + factorization, without going through the k₀-inside form.

Part 8: Direct Reflection Positivity

theorem QFT.RPProof.freeCovariance_reflection_positive_direct (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : 0 ≤ (rpInnerProduct m f).re

Theorem: Direct proof of reflection positivity without spatial regulator.

For test functions supported on positive time (t > 0), the RP inner product ⟨Θf, f⟩_C has non-negative real part.

Proof: By rp_equals_squared_norm_integral, ⟨Θf, f⟩C = (1/(2(2π)^{d-1})) * ∫{k_sp} (1/ω) |F_ω(-k_sp)|² dk_sp Both the prefactor and integrand are non-negative.

Bridge to Direct Proof

theorem QFT.rpInnerProduct_eq_rpProof (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : rpInnerProduct m f = RPProof.rpInnerProduct m f

Bridge Lemma: The QFT namespace rpInnerProduct equals the RPProof rpInnerProduct.

Both are defined using the same Bessel kernel C(x,y) = (m/(4π²r)) K₁(mr), so this equality holds by definition (rfl).

theorem QFT.freeCovariance_reflection_positive_bilinear (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : 0 ≤ (rpInnerProduct m f).re

Main Reflection Positivity Theorem (Bilinear Form)

For any complex test function f supported on positive time (x₀ ≥ 0), the reflection positivity inner product is non-negative:

Re⟨Θf, f⟩_C ≥ 0

where C is the unregulated Bessel covariance kernel.

Proof: Bridge to RPProof, then apply the direct proof via momentum representation and non-negativity of the integrand.

Connection to Real Test Functions

The result extends to real test functions via embedding.

theorem QFT.star_toComplex_eq_compTimeReflection (f : TestFunction) : star (toComplex f) = compTimeReflection (toComplex f)

For real test functions, star (toComplex f) = compTimeReflection (toComplex f). This is because conjugation is identity for real-valued functions.

theorem QFT.rpInnerProduct_toComplex_eq (m : ℝ) (f : TestFunction) : rpInnerProduct m (toComplex f) = freeCovarianceℂBilinear m (compTimeReflection (toComplex f)) (toComplex f)

The rpInnerProduct of a real test function equals the complex bilinear form with compTimeReflection.

theorem QFT.freeCovariance_reflection_positive_bilinear_real (m : ℝ) [Fact (0 < m)] (f : TestFunction) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : 0 ≤ ∫ (x : SpaceTime) (y : SpaceTime), (compTimeReflectionReal f) x * freeCovariance m x y * f y

For real test functions, the reflection positivity inner product is non-negative.

theorem QFT.freeCovariance_reflection_positive_real (m : ℝ) [Fact (0 < m)] (f : TestFunction) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : 0 ≤ ∫ (x : SpaceTime) (y : SpaceTime), (compTimeReflectionReal f) x * freeCovariance m x y * f y

Alias for freeCovariance_reflection_positive_bilinear_real to match expected name.