Basic Definitions

Core type definitions for the formalization:

• SpaceTime = EuclideanSpace ℝ (Fin 4), the Euclidean 4-space ℝ⁴
• TestFunction / TestFunctionℂ = real/complex Schwartz functions on ℝ⁴
• FieldConfiguration = tempered distributions S'(ℝ⁴) (WeakDual of Schwartz space)
• distributionPairing / distributionPairingℂReal = ⟨ω, f⟩ pairings
• GJGeneratingFunctional = Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω)

@[reducible, inline]

abbrev STDimension : ℕ

Spacetime dimension. Currently set to 4 (Euclidean ℝ⁴). Changing this value requires corresponding changes throughout the project; see docs/dimension_dependence.md for a detailed inventory.

Equations

• STDimension = 4

@[reducible, inline]

abbrev SpaceTime : Type

The SpaceTime declaration.

Equations

• SpaceTime = EuclideanSpace ℝ (Fin STDimension)

@[implicit_reducible]

noncomputable instance instInnerProductSpaceRealSpaceTime : InnerProductSpace ℝ SpaceTime

Equations

• instInnerProductSpaceRealSpaceTime = inferInstance

@[reducible, inline]

abbrev getTimeComponent (x : SpaceTime) : ℝ

The getTimeComponent declaration.

Equations

• getTimeComponent x = x.ofLp ⟨0, getTimeComponent._proof_2⟩

@[reducible, inline]

noncomputable abbrev μ : MeasureTheory.Measure SpaceTime

The μ declaration.

Equations

• μ = MeasureTheory.volume

@[reducible, inline]

abbrev TestFunction : Type

The TestFunction declaration.

Equations

• TestFunction = SchwartzMap SpaceTime ℝ

@[reducible, inline]

abbrev TestFunction𝕜 {𝕜 : Type} [RCLike 𝕜] : Type

Test functions over an arbitrary scalar field.

Equations

• TestFunction𝕜 = SchwartzMap SpaceTime 𝕜

@[reducible, inline]

abbrev TestFunctionℂ : Type

The TestFunctionℂ declaration.

Equations

• TestFunctionℂ = TestFunction𝕜

noncomputable def pointwiseMulCLM : ℂ →L[ℂ] ℂ →L[ℂ] ℂ

Continuous bilinear pointwise multiplication on complex scalars.

Equations

• pointwiseMulCLM = ContinuousLinearMap.mul ℂ ℂ

noncomputable def schwartzMul (g : TestFunctionℂ) : TestFunctionℂ →L[ℂ] TestFunctionℂ

Multiplication lifted to the Schwartz space.

Equations

• schwartzMul g = SchwartzMap.bilinLeftCLM pointwiseMulCLM ⋯

Glimm-Jaffe Distribution Framework

The proper mathematical foundation for quantum field theory uses tempered distributions as field configurations, following Glimm and Jaffe. This section adds the distribution-theoretic definitions alongside the existing L2 framework for comparison and gradual transition.

@[reducible, inline]

abbrev FieldConfiguration : Type

Field configurations as tempered distributions (dual to Schwartz space). This follows the Glimm-Jaffe approach where the field measure is supported on the space of distributions, not L2 functions.

Using WeakDual gives the correct weak-* topology on the dual space.

Equations

• FieldConfiguration = WeakDual ℝ (SchwartzMap SpaceTime ℝ)

noncomputable def distributionPairing (ω : FieldConfiguration) (f : TestFunction) : ℝ

The fundamental pairing between a field configuration (distribution) and a test function. This is ⟨ω, f⟩ in the Glimm-Jaffe notation.

Note: FieldConfiguration = WeakDual ℝ (SchwartzMap SpaceTime ℝ) has the correct weak-* topology, making evaluation maps x ↦ ω(x) continuous for each test function x.

Equations

• distributionPairing ω f = ω f

@[simp]

theorem distributionPairing_add (ω₁ ω₂ : FieldConfiguration) (a : TestFunction) : distributionPairing (ω₁ + ω₂) a = distributionPairing ω₁ a + distributionPairing ω₂ a

@[simp]

theorem distributionPairing_smul (s : ℝ) (ω : FieldConfiguration) (a : TestFunction) : distributionPairing (s • ω) a = s * distributionPairing ω a

theorem pairing_smul_real (ω : FieldConfiguration) (s : ℝ) (a : TestFunction) : ω (s • a) = s * ω a

noncomputable def distributionPairingCLM (a : TestFunction) : FieldConfiguration →L[ℝ] ℝ

The distributionPairingCLM declaration.

Equations

• distributionPairingCLM a = { toFun := fun (ω : FieldConfiguration) => distributionPairing ω a, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem distributionPairingCLM_apply (a : TestFunction) (ω : FieldConfiguration) : (distributionPairingCLM a) ω = distributionPairing ω a

Glimm-Jaffe Generating Functional

The generating functional in the distribution framework: Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω) where the integral is over field configurations ω (distributions).

noncomputable def GJGeneratingFunctional (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (J : TestFunction) : ℂ

The Glimm-Jaffe generating functional: Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω) This is the fundamental object in constructive QFT.

Equations

• GJGeneratingFunctional dμ_config J = ∫ (ω : FieldConfiguration), Complex.exp (Complex.I * ↑(distributionPairing ω J)) ∂↑dμ_config

noncomputable def schwartzCompCLM (f : TestFunctionℂ) (L : ℂ →L[ℝ] ℝ) : TestFunction

Helper function to create a Schwartz map from a complex test function by applying a continuous linear map. This factors out the common pattern for extracting real/imaginary parts.

Equations

• schwartzCompCLM f L = { toFun := fun (x : SpaceTime) => L (f x), smooth' := ⋯, decay' := ⋯ }

@[simp]

theorem schwartz_comp_clm_apply (f : TestFunctionℂ) (L : ℂ →L[ℝ] ℝ) (x : SpaceTime) : (schwartzCompCLM f L) x = L (f x)

Evaluate schwartzCompCLM pointwise.

noncomputable def complexTestFunctionDecompose (f : TestFunctionℂ) : TestFunction × TestFunction

Decompose a complex test function into its real and imaginary parts as real test functions. This is more efficient than separate extraction functions.

Equations

• complexTestFunctionDecompose f = (schwartzCompCLM f Complex.reCLM, schwartzCompCLM f Complex.imCLM)

@[simp]

theorem complex_testfunction_decompose_fst_apply (f : TestFunctionℂ) (x : SpaceTime) : (complexTestFunctionDecompose f).1 x = (f x).re

First component of the decomposition evaluates to the real part pointwise.

@[simp]

theorem complex_testfunction_decompose_snd_apply (f : TestFunctionℂ) (x : SpaceTime) : (complexTestFunctionDecompose f).2 x = (f x).im

Second component of the decomposition evaluates to the imaginary part pointwise.

theorem complex_testfunction_decompose_fst_apply_coe (f : TestFunctionℂ) (x : SpaceTime) : ↑((complexTestFunctionDecompose f).1 x) = ↑(f x).re

Coerced-to-ℂ version (useful for complex-side algebra).

theorem complex_testfunction_decompose_snd_apply_coe (f : TestFunctionℂ) (x : SpaceTime) : ↑((complexTestFunctionDecompose f).2 x) = ↑(f x).im

Coerced-to-ℂ version (useful for complex-side algebra).

theorem complex_testfunction_decompose_recompose (f : TestFunctionℂ) (x : SpaceTime) : f x = ↑((complexTestFunctionDecompose f).1 x) + Complex.I * ↑((complexTestFunctionDecompose f).2 x)

Recomposition at a point via the decomposition.

noncomputable def distributionPairingℂReal (ω : FieldConfiguration) (f : TestFunctionℂ) : ℂ

Complex version of the pairing: real field configuration with complex test function We extend the pairing by treating the complex test function as f(x) = f_re(x) + if_im(x) and defining ⟨ω, f⟩ = ⟨ω, f_re⟩ + i⟨ω, f_im⟩

Equations

• distributionPairingℂReal ω f = match complexTestFunctionDecompose f with | (f_re, f_im) => ↑(ω f_re) + Complex.I * ↑(ω f_im)

noncomputable def GJGeneratingFunctionalℂ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (J : TestFunctionℂ) : ℂ

Complex version of the generating functional

Equations

• GJGeneratingFunctionalℂ dμ_config J = ∫ (ω : FieldConfiguration), Complex.exp (Complex.I * distributionPairingℂReal ω J) ∂↑dμ_config

noncomputable def GJMean (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (φ : TestFunction) : ℝ

The mean field in the Glimm-Jaffe framework

Equations

• GJMean dμ_config φ = ∫ (ω : FieldConfiguration), distributionPairing ω φ ∂↑dμ_config

Spatial Geometry and Energy Operators

@[reducible, inline]

abbrev SpatialCoords : Type

Spatial coordinates: ℝ^{d-1} (space without time) as EuclideanSpace for L2 norm

Equations

• SpatialCoords = EuclideanSpace ℝ (Fin (STDimension - 1))

@[reducible, inline]

noncomputable abbrev SpatialL2 : AddSubgroup (SpatialCoords →ₘ[MeasureTheory.volume] ℝ)

L² space on spatial slices (real-valued)

Equations

• SpatialL2 = MeasureTheory.Lp ℝ 2 MeasureTheory.volume

noncomputable def spatialPart (x : SpaceTime) : SpatialCoords

Extract spatial part of spacetime coordinate

Equations

• spatialPart x = (EuclideanSpace.equiv (Fin (STDimension - 1)) ℝ).symm fun (i : Fin (STDimension - 1)) => x.ofLp ⟨↑i + 1, ⋯⟩

noncomputable def spatialEnergy (m : ℝ) (k : SpatialCoords) : ℝ

The energy function spatialEnergy m k = √(‖k‖² + m²) on spatial momentum space.

Equations

• spatialEnergy m k = √(‖k‖ ^ 2 + m ^ 2)