Spacetime Structure from Dζ: Dimension, Signature, and Poincaré Group

The 4D Lorentzian spacetime I4 = Fin 1 ⊕ Fin 3 with signature (1,3) is determined by the algebraic structure of Dζ. The symmetry group is O(3,1) = LorentzGroup 3 (PhysLean, with Group instance). ISO(3,1) = ℝ⁴ ⋊ O(3,1) is constructed as a semidirect product.

theorem FUST.SpacetimeUniqueness.lorentz_bilin_invariance (Λ : ↑(LorentzGroup 3)) (v w : Physics.Lorentz.I4 → ℝ) : (Physics.Poincare.minkowskiBilin ((↑Λ).mulVec v)) ((↑Λ).mulVec w) = (Physics.Poincare.minkowskiBilin v) w

Lorentz invariance of the Minkowski bilinear form

Semidirect product ISO(3,1) = ℝ⁴ ⋊ O(3,1)

O(3,1) acts on ℝ⁴ by matrix-vector multiplication. The Poincaré group is the semidirect product of translations ℝ⁴ and Lorentz transformations O(3,1).

noncomputable def FUST.SpacetimeUniqueness.lorentzAddEquiv (Λ : ↑(LorentzGroup 3)) : (Physics.Lorentz.I4 → ℝ) ≃+ (Physics.Lorentz.I4 → ℝ)

Each Lorentz transformation Λ gives an additive automorphism of ℝ⁴

Equations

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

noncomputable def FUST.SpacetimeUniqueness.lorentzAction : ↑(LorentzGroup 3) →* MulAut (Multiplicative (Physics.Lorentz.I4 → ℝ))

Lorentz group action on Multiplicative(ℝ⁴) as group automorphisms

Equations

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

@[reducible, inline]

abbrev FUST.SpacetimeUniqueness.PoincareGroup : Type

Poincaré group ISO(3,1) = ℝ⁴ ⋊ O(3,1) as a semidirect product

Equations

• FUST.SpacetimeUniqueness.PoincareGroup = (Multiplicative (FUST.Physics.Lorentz.I4 → ℝ) ⋊[FUST.SpacetimeUniqueness.lorentzAction] ↑(LorentzGroup 3))

noncomputable instance FUST.SpacetimeUniqueness.instGroupPoincareGroup : Group PoincareGroup

Equations

• FUST.SpacetimeUniqueness.instGroupPoincareGroup = inferInstance

theorem FUST.SpacetimeUniqueness.spacetime_from_Dζ : (DζOperator.AF_coeff.re = 0 ∧ DζOperator.AF_coeff.im > 0) ∧ DζOperator.σ_Diff5 1 * (DζOperator.σ_Diff3 5 * DζOperator.σ_Diff2 7 - DζOperator.σ_Diff2 5 * DζOperator.σ_Diff3 7) - DζOperator.σ_Diff3 1 * (DζOperator.σ_Diff5 5 * DζOperator.σ_Diff2 7 - DζOperator.σ_Diff2 5 * DζOperator.σ_Diff5 7) + DζOperator.σ_Diff2 1 * (DζOperator.σ_Diff5 5 * DζOperator.σ_Diff3 7 - DζOperator.σ_Diff3 5 * DζOperator.σ_Diff5 7) ≠ 0 ∧ DζOperator.Φ_A id 1 ≠ 0 ∧ (∀ (a : ℝ), a ≠ 0 → ((6 * ↑a + DζOperator.AF_coeff * 0) ^ 2).re > 0) ∧ (∀ (b : ℝ), b ≠ 0 → ((6 * 0 + DζOperator.AF_coeff * ↑b) ^ 2).re < 0) ∧ (∀ (Λ : ↑(LorentzGroup 3)) (v w : Physics.Lorentz.I4 → ℝ), (Physics.Poincare.minkowskiBilin ((↑Λ).mulVec v)) ((↑Λ).mulVec w) = (Physics.Poincare.minkowskiBilin v) w) ∧ (∀ (t : ℝ), Real.exp (t + Real.log φ) = φ * Real.exp t) ∧ LinearIndependent ℝ fun (μ : Physics.Lorentz.I4) => Physics.Poincare.phiTranslation μ

Dζ determines spacetime structure and Poincaré group. Part A: Dζ channel algebra (AF_coeff_eq, Φ_S_rank_three) → 1+3, signature (1,3). Part B: I4 geometry justified by Part A.

theorem FUST.SpacetimeUniqueness.gauge_spacetime_independence : (∀ (c : ℂ), c ≠ 0 → ∀ (f g : ℂ → ℂ) (z : ℂ), FζOperator.derivDefect (fun (w : ℂ) => c * f w) (fun (w : ℂ) => c⁻¹ * g w) z = FζOperator.derivDefect f g z) ∧ (∀ (Λ : ↑(LorentzGroup 3)) (v w : Physics.Lorentz.I4 → ℝ), (Physics.Poincare.minkowskiBilin ((↑Λ).mulVec v)) ((↑Λ).mulVec w) = (Physics.Poincare.minkowskiBilin v) w) ∧ starRingEnd ℂ ≠ RingHom.id ℂ ∧ (∀ (x : ℝ), (starRingEnd ℝ) x = x) ∧ Module.finrank ℝ (↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule × (Physics.Lorentz.I4 → ℝ)) = 10 ∧ 8 + 3 + 1 = 12 ∧ 12 + 10 = 22

Gauge groups and Poincaré group use independent degrees of freedom. Gauge: derivDefect factorization ambiguity (ℂ-linearity of Fζ). Spacetime: eigenvalue structure of Dζ (Lorentz invariance of η). Separation: gauge acts on ℂⁿ (star=conj≠id), spacetime acts on ℝⁿ (star=id).