Time Reflection Θ and Discrete Symmetries

Time reflection Θ: (t, xbar) ↦ (−t, xbar) as an orthogonal involution on ℝ⁴. Properties: self-inverse (Θ² = id), measure-preserving, isometric.

Induced actions on test functions: (Θf)(x) = f(Θx) = f(−t, xbar). Foundation for the OS3 reflection positivity axiom.

@[reducible, inline]

abbrev QFT.timeReflection (x : SpaceTime) : SpaceTime

The timeReflection declaration.

Equations

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

def QFT.timeReflectionMatrix : Matrix (Fin STDimension) (Fin STDimension) ℝ

The timeReflectionMatrix declaration.

Equations

• QFT.timeReflectionMatrix = Matrix.diagonal fun (i : Fin STDimension) => if i = 0 then -1 else 1

theorem QFT.timeReflectionMatrix_is_orthogonal : timeReflectionMatrix ∈ Matrix.orthogonalGroup (Fin STDimension) ℝ

def QFT.timeReflectionIsometry : ↥(Matrix.orthogonalGroup (Fin STDimension) ℝ)

The timeReflectionIsometry declaration.

Equations

• QFT.timeReflectionIsometry = ⟨QFT.timeReflectionMatrix, QFT.timeReflectionMatrix_is_orthogonal⟩

def QFT.timeReflectionLinear : SpaceTime →ₗ[ℝ] SpaceTime

The timeReflectionLinear declaration.

Equations

• QFT.timeReflectionLinear = { toFun := QFT.timeReflection, map_add' := QFT.timeReflectionLinear._proof_1, map_smul' := QFT.timeReflectionLinear._proof_2 }

noncomputable def QFT.timeReflectionCLM : SpaceTime →L[ℝ] SpaceTime

The timeReflectionCLM declaration.

Equations

• QFT.timeReflectionCLM = LinearMap.toContinuousLinearMap QFT.timeReflectionLinear

theorem QFT.timeReflection_inner_map (x y : SpaceTime) : inner ℝ (timeReflection x) (timeReflection y) = inner ℝ x y

Time reflection preserves inner products

@[simp]

theorem QFT.timeReflection_involutive (x : SpaceTime) : timeReflection (timeReflection x) = x

Time reflection as a linear isometry equivalence

def QFT.timeReflectionLE : SpaceTime ≃ₗᵢ[ℝ] SpaceTime

The timeReflectionLE declaration.

Equations

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

theorem QFT.timeReflection_measurePreserving : MeasureTheory.MeasurePreserving timeReflection MeasureTheory.volume MeasureTheory.volume

Time reflection preserves Lebesgue measure.

noncomputable def QFT.compTimeReflection : TestFunctionℂ →L[ℝ] TestFunctionℂ

The compTimeReflection declaration.

Equations

• QFT.compTimeReflection = SchwartzMap.compCLM ℝ QFT.compTimeReflection._proof_1 QFT.timeReflection_hg_upper✝

noncomputable def QFT.compTimeReflectionReal : TestFunction →L[ℝ] TestFunction

Composition with time reflection as a continuous linear map on real-valued test functions. This version will be used when working with positive-time subspaces defined over ℝ, so that reflection positivity can be formulated without passing through complex scalars.

Equations

• QFT.compTimeReflectionReal = SchwartzMap.compCLM ℝ QFT.compTimeReflection._proof_1 QFT.timeReflection_hg_upper✝

theorem QFT.compTimeReflectionReal_linear_combination {n : ℕ} (f : Fin n → TestFunction) (c : Fin n → ℝ) : compTimeReflectionReal (∑ i : Fin n, c i • f i) = ∑ i : Fin n, c i • compTimeReflectionReal (f i)

Time reflection is linear on real test functions.