Documentation

FUST.Physics.Poincare

Module.Finite instance for so(3,1) #

source
instance FUST.Physics.Poincare.instFiniteRealSubtypeMatrixSumFinOfNatNatMemSubmoduleSo'_fUST :
Module.Finite ℝ ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule

Translation space ℝ⁴ #

source
theorem FUST.Physics.Poincare.finrank_translations :
Module.finrank ℝ (Lorentz.I4 → ℝ) = 4

dim ℝ⁴ = dim(I4 → ℝ) = 4

Poincaré algebra dimension #

source
theorem FUST.Physics.Poincare.finrank_poincare :
Module.finrank ℝ (↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule × (Lorentz.I4 → ℝ)) = 10

dim iso(3,1) = dim so(3,1) + dim ℝ⁴ = 6 + 4 = 10

Casimir invariant: Minkowski bilinear form on I4 → ℝ #

Signature (1,3): 1 positive from φψ = -1, 3 negative from ζ₆ compact structure.

source
noncomputable def FUST.Physics.Poincare.minkowskiBilin :
LinearMap.BilinForm ℝ (Lorentz.I4 → ℝ)

Minkowski bilinear form B(v,w) = v ⬝ᵥ (η *ᵥ w)

Equations
Instances For
    source
    theorem FUST.Physics.Poincare.skewAdj_sum_zero (A : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule) :
    (↑A).transpose * LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ + LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ * ↑A = 0

    Aᵀη + ηA = 0 for A ∈ so(3,1)

    source
    theorem FUST.Physics.Poincare.lorentz_infinitesimal_invariance (A : ↥(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ).toSubmodule) (v w : Lorentz.I4 → ℝ) :
    (minkowskiBilin ((↑A).mulVec v)) w + (minkowskiBilin v) ((↑A).mulVec w) = 0

    Infinitesimal Lorentz invariance: B(Av, w) + B(v, Aw) = 0

    φ-Dilation as Translation in Log-Coordinates #

    φ-scaling z → φz is multiplicative. In log-coordinates t = log z, it becomes additive translation t → t + log φ. This establishes the translation symmetry needed for the Poincaré group.

    source
    theorem FUST.Physics.Poincare.log_phi_pos :
    0 < Real.log φ
    source
    theorem FUST.Physics.Poincare.log_phi_ne_zero :
    Real.log φ ≠ 0
    source
    theorem FUST.Physics.Poincare.exp_log_phi_translate (t : ℝ) :
    Real.exp (t + Real.log φ) = φ * Real.exp t

    exp conjugacy: φ-scaling = translation by log φ in log-coordinates

    source
    theorem FUST.Physics.Poincare.exp_log_phi_translate_nat (n : ℕ) (t : ℝ) :
    Real.exp (t + ↑n * Real.log φ) = φ ^ n * Real.exp t

    Iterated φ-scaling = translation by n·log φ

    source
    noncomputable def FUST.Physics.Poincare.phiTranslation (μ : Lorentz.I4) :
    Lorentz.I4 → ℝ

    Translation vector: log φ in the μ-th direction of I4

    Equations
    Instances For
      source
      theorem FUST.Physics.Poincare.phiTranslation_apply_self (μ : Lorentz.I4) :
      phiTranslation μ μ = Real.log φ
      source
      theorem FUST.Physics.Poincare.phiTranslation_apply_ne {μ ν : Lorentz.I4} (h : ν ≠ μ) :
      phiTranslation μ ν = 0
      source
      theorem FUST.Physics.Poincare.phiTranslation_linearIndependent :
      LinearIndependent ℝ fun (μ : Lorentz.I4) => phiTranslation μ

      The 4 translation vectors span I4 → ℝ (linearly independent)

      source
      theorem FUST.Physics.Poincare.phi_dilation_is_translation :
      (∀ (t : ℝ), Real.exp (t + Real.log φ) = φ * Real.exp t) ∧ 0 < Real.log φ ∧ (LinearIndependent ℝ fun (μ : Lorentz.I4) => phiTranslation μ) ∧ Module.finrank ℝ (Lorentz.I4 → ℝ) = 4

      φ-dilation corresponds to translation in the Poincaré group