FUST.Physics.Lorentz

Spacetime dimension from Dζ channel decomposition #

AF channel (Φ_A): 1-dimensional — AF_coeff = 2i√3 is pure imaginary (1 real DOF). SY channel (Φ_S): 3-dimensional — rank 3 from Φ_S_rank_three. Total: 1 + 3 = 4 spacetime dimensions.

source

theorem FUST.Physics.Lorentz.AF_channel_dim :

Fintype.card (Fin 1) = 1

source

theorem FUST.Physics.Lorentz.SY_channel_dim :

Fintype.card (Fin 3) = 3

source

theorem FUST.Physics.Lorentz.spacetime_dim_from_Dζ :

Fintype.card (Fin 1) + Fintype.card (Fin 3) = 4

Metric signature from Galois norms #

The two Galois conjugations of ℚ(√5, √-3) determine the metric:

σ₁ (φ ↔ ψ): φψ = -1 → AF channel norm is NEGATIVE → timelike
σ₂ (ζ₆ ↔ ζ₆⁻¹): ζ₆·ζ₆⁻¹ = 1 → SY channel norm is POSITIVE → spacelike

source

theorem FUST.Physics.Lorentz.AF_sign_from_phi_psi :

φ * ψ = -1

source

theorem FUST.Physics.Lorentz.SY_sign_from_zeta6 :

ζ₆ * ζ₆' = 1

source

theorem FUST.Physics.Lorentz.AF_coeff_sq_negative :

(DζOperator.AF_coeff ^ 2).re < 0

source

theorem FUST.Physics.Lorentz.SY_coeff_sq_positive :

0 < 6 ^ 2

source

theorem FUST.Physics.Lorentz.signature_from_Dζ :

φ * ψ = -1 ∧ ζ₆ * ζ₆' = 1 ∧ (DζOperator.AF_coeff ^ 2).re < 0 ∧ 0 < 6 ^ 2 ∧ Fintype.card (Fin 1) + Fintype.card (Fin 3) = 4

The indefinite diagonal diag(+1,-1,-1,-1) is determined by the Dζ channel signs: AF (1D, φψ = -1) contributes the timelike (+1 in mostly-plus, but indefiniteDiagonal uses Sum.elim 1 (-1) placing +1 on Fin p and -1 on Fin q).