Lorentz connection: localized so(3,1)

instance FUST.Physics.Gravity.instFreeRealSubtypeMatrixSumFinOfNatNatMemSubmoduleSo'_fUST : Module.Free ℝ ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule

theorem FUST.Physics.Gravity.finrank_connection : Module.finrank ℝ (Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule) = 24

dim(connection) = dim so(3,1) × spacetime dim = 6 × 4 = 24

Curvature: Lie bracket of connection components

Localizing the Lorentz symmetry introduces a connection ω : I4 → so(3,1). The curvature F_{μν} = [ω_μ, ω_ν] ∈ so(3,1) is the Riemann curvature.

noncomputable def FUST.Physics.Gravity.curvature (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)

Curvature of Lorentz connection = Lie bracket of components

Equations

• FUST.Physics.Gravity.curvature ω μ ν = ⁅ω μ, ω ν⁆

theorem FUST.Physics.Gravity.curvature_antisymm (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : curvature ω μ ν = -curvature ω ν μ

Curvature is antisymmetric: F_{μν} = -F_{νμ}

theorem FUST.Physics.Gravity.curvature_in_so31 (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : ↑(curvature ω μ ν) ∈ LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ

Curvature stays in so(3,1): [so(3,1), so(3,1)] ⊆ so(3,1)

theorem FUST.Physics.Gravity.curvature_preserves_minkowski (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) (v w : Lorentz.I4 → ℝ) : (Poincare.minkowskiBilin ((↑(curvature ω μ ν)).mulVec v)) w + (Poincare.minkowskiBilin v) ((↑(curvature ω μ ν)).mulVec w) = 0

Curvature preserves the Minkowski form (inherits from so(3,1))

Bianchi identity from Jacobi identity

The algebraic Bianchi identity ∇{[μ} F{νρ]} = 0 is the Jacobi identity of the Lie algebra so(3,1) applied to connection components.

theorem FUST.Physics.Gravity.bianchi_identity (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν ρ : Lorentz.I4) : ⁅ω μ, ⁅ω ν, ω ρ⁆⁆ + ⁅ω ν, ⁅ω ρ, ω μ⁆⁆ + ⁅ω ρ, ⁅ω μ, ω ν⁆⁆ = 0

Algebraic Bianchi identity: cyclic sum of [ω_μ, F_{νρ}] = 0

Dζ → so(3,1) connection: algebraic 3+1 decomposition

Dζ decomposes into (AF_coeff_eq, Φ_S_rank_three): Φ_A: 1 AF channel (temporal, AF_coeff = 2i√3) Φ_S: 3 SY sub-operators (spatial, rank 3) This determines I4 = Fin 1 ⊕ Fin 3 and indexes ω : I4 → so(3,1).

noncomputable def FUST.Physics.Gravity.Φ_A_coeff (s : ℕ) : ℝ

Φ_A eigenvalue on z^s: σ_{Diff6+Diff2-Diff4}(s)

Equations

• FUST.Physics.Gravity.Φ_A_coeff s = FUST.φ ^ (3 * s) - 4 * FUST.φ ^ (2 * s) + (3 + FUST.φ) * FUST.φ ^ s - (3 + FUST.ψ) * FUST.ψ ^ s + 4 * FUST.ψ ^ (2 * s) - FUST.ψ ^ (3 * s)

noncomputable def FUST.Physics.Gravity.Φ_S_coeff (s : ℕ) : ℝ

Φ_S eigenvalue on z^s: σ_{2·Diff5+Diff3+μ·Diff2}(s)

Equations

• FUST.Physics.Gravity.Φ_S_coeff s = 2 * FUST.DζOperator.σ_Diff5 s + FUST.DζOperator.σ_Diff3 s + 2 / (FUST.φ + 2) * FUST.DζOperator.σ_Diff2 s

theorem FUST.Physics.Gravity.Φ_A_coeff_one : Φ_A_coeff 1 = 2 * (φ - ψ)

Φ_A_coeff(1) = 2(φ-ψ) = 2√5

theorem FUST.Physics.Gravity.Φ_S_coeff_one : Φ_S_coeff 1 = √5 - 2

Φ_S_coeff(1) = √5 - 2

Dζ eigenvalue: λ(s) = 6·Φ_S(s) + 2i√3·Φ_A(s)

The Dζ eigenvalue on z^s (for active modes s ≡ 1,5 mod 6) is a single complex number. Re = 6·Φ_S, Im = 2√3·Φ_A. The mass invariant uses Re²-Im².

noncomputable def FUST.Physics.Gravity.Dζ_re (s : ℕ) : ℝ

Dζ eigenvalue real part: 6·Φ_S(s)

Equations

• FUST.Physics.Gravity.Dζ_re s = 6 * FUST.Physics.Gravity.Φ_S_coeff s

noncomputable def FUST.Physics.Gravity.Dζ_im (s : ℕ) : ℝ

Dζ eigenvalue imaginary part: 2√3·Φ_A(s)

Equations

• FUST.Physics.Gravity.Dζ_im s = 2 * √3 * FUST.Physics.Gravity.Φ_A_coeff s

theorem FUST.Physics.Gravity.Dζ_dim_matches_I4 : Fintype.card (Fin 1) + Fintype.card (Fin 3) = Fintype.card Lorentz.I4

Temporal (Fin 1) + spatial (Fin 3) = I4, matching Dζ channel structure

theorem FUST.Physics.Gravity.Dζ_connection_dim : Fintype.card Lorentz.I4 * Module.finrank ℝ ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule = 24

Connection space dim = |I4| × dim so(3,1) = 4 × 6 = 24

theorem FUST.Physics.Gravity.Dζ_bianchi (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν ρ : Lorentz.I4) : ⁅ω μ, ⁅ω ν, ω ρ⁆⁆ + ⁅ω ν, ⁅ω ρ, ω μ⁆⁆ + ⁅ω ρ, ⁅ω μ, ω ν⁆⁆ = 0

Bianchi identity for Dζ-indexed connections

Minkowski metric, Riemann/Ricci/Einstein tensors, vacuum EFE

noncomputable def FUST.Physics.Gravity.η (μ ν : Lorentz.I4) : ℝ

Minkowski metric η_{μν} = diag(1,-1,-1,-1)

Equations

• FUST.Physics.Gravity.η μ ν = LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ μ ν

theorem FUST.Physics.Gravity.η_off_diag (μ ν : Lorentz.I4) (h : μ ≠ ν) : η μ ν = 0

theorem FUST.Physics.Gravity.η_temporal : η (Sum.inl 0) (Sum.inl 0) = 1

theorem FUST.Physics.Gravity.η_spatial (i : Fin 3) : η (Sum.inr i) (Sum.inr i) = -1

theorem FUST.Physics.Gravity.η_sq_trace : ∑ μ : Lorentz.I4, ∑ ν : Lorentz.I4, η μ ν * η μ ν = 4

Tr(η²) = dim(spacetime) = 4

Riemann tensor

noncomputable def FUST.Physics.Gravity.riemann (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν ρ σ : Lorentz.I4) : ℝ

R^ρ_{σμν} := (curvature ω μ ν).val ρ σ

Equations

• FUST.Physics.Gravity.riemann ω μ ν ρ σ = ↑(FUST.Physics.Gravity.curvature ω μ ν) ρ σ

theorem FUST.Physics.Gravity.riemann_antisymm (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν ρ σ : Lorentz.I4) : riemann ω μ ν ρ σ = -riemann ω ν μ ρ σ

Riemann antisymmetry: R^ρ_{σμν} = -R^ρ_{σνμ}

theorem FUST.Physics.Gravity.riemann_diag (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ρ σ : Lorentz.I4) : riemann ω μ μ ρ σ = 0

theorem FUST.Physics.Gravity.riemann_flat (A : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν ρ σ : Lorentz.I4) : riemann (fun (x : Lorentz.I4) => A) μ ν ρ σ = 0

Flat connection → zero Riemann

Ricci tensor, scalar curvature, Einstein tensor

noncomputable def FUST.Physics.Gravity.ricci (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : ℝ

Ric_{μν} = Σ_ρ R^ρ_{μρν}

Equations

• FUST.Physics.Gravity.ricci ω μ ν = ∑ ρ : FUST.Physics.Lorentz.I4, FUST.Physics.Gravity.riemann ω ρ ν ρ μ

noncomputable def FUST.Physics.Gravity.scalarCurvature (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) : ℝ

R = Σ_{μν} η^{μν} Ric_{μν}

Equations

• FUST.Physics.Gravity.scalarCurvature ω = ∑ μ : FUST.Physics.Lorentz.I4, ∑ ν : FUST.Physics.Lorentz.I4, FUST.Physics.Gravity.η μ ν * FUST.Physics.Gravity.ricci ω μ ν

noncomputable def FUST.Physics.Gravity.einstein (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : ℝ

G_{μν} = Ric_{μν} - (1/2) η_{μν} R

Equations

• FUST.Physics.Gravity.einstein ω μ ν = FUST.Physics.Gravity.ricci ω μ ν - 1 / 2 * FUST.Physics.Gravity.η μ ν * FUST.Physics.Gravity.scalarCurvature ω

Flat connection satisfies vacuum EFE

theorem FUST.Physics.Gravity.ricci_flat (A : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : ricci (fun (x : Lorentz.I4) => A) μ ν = 0

theorem FUST.Physics.Gravity.scalarCurvature_flat (A : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) : (scalarCurvature fun (x : Lorentz.I4) => A) = 0

theorem FUST.Physics.Gravity.einstein_flat (A : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : einstein (fun (x : Lorentz.I4) => A) μ ν = 0

theorem FUST.Physics.Gravity.vacuum_einstein (A : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν : Lorentz.I4) : einstein (fun (x : Lorentz.I4) => A) μ ν = 0

Vacuum Einstein equations: constant connections satisfy G_{μν} = 0

Einstein tensor trace: η^{μν} G_{μν} = -R

theorem FUST.Physics.Gravity.einstein_trace (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) : ∑ μ : Lorentz.I4, ∑ ν : Lorentz.I4, η μ ν * einstein ω μ ν = -scalarCurvature ω

Bianchi identity in matrix entries

theorem FUST.Physics.Gravity.bianchi_entries (ω : Lorentz.I4 → ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)) (μ ν ρ α β : Lorentz.I4) : ↑⁅ω μ, ⁅ω ν, ω ρ⁆⁆ α β + ↑⁅ω ν, ⁅ω ρ, ω μ⁆⁆ α β + ↑⁅ω ρ, ⁅ω μ, ω ν⁆⁆ α β = 0