IndisputableMonolith.Relativity.Geometry.LeviCivitaTheorem

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry.Tensor
   3import IndisputableMonolith.Relativity.Geometry.Metric
   4import IndisputableMonolith.Relativity.Geometry.Curvature
   5import IndisputableMonolith.Relativity.Calculus.Derivatives
   6
   7/-!
   8# Fundamental Theorem of Pseudo-Riemannian Geometry
   9
  10On any pseudo-Riemannian manifold (M, g) there exists a unique
  11torsion-free, metric-compatible connection ∇. Its coefficients
  12are the Christoffel symbols Γ^ρ_μν defined in `Curvature.lean`.
  13
  14This module proves:
  151. `Curvature.christoffel` is torsion-free (already proved as `christoffel_symmetric`)
  162. `Curvature.christoffel` is metric-compatible (∇g = 0)
  173. Any torsion-free, metric-compatible connection must equal `Curvature.christoffel`
  18
  19Together these constitute the Fundamental Theorem of (pseudo-)Riemannian geometry,
  20which applies to both Riemannian (positive-definite) and Lorentzian (signature 1,3)
  21metrics.
  22
  23## References
  24
  25* Wald, "General Relativity", Theorem 3.1.1
  26* do Carmo, "Riemannian Geometry", Theorem 2.3
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Relativity
  31namespace Geometry
  32
  33open Calculus
  34
  35noncomputable section
  36
  37/-! ## §1 Connection as a Function Type -/
  38
  39/-- A connection Γ on 4D spacetime: Γ^ρ_μν at each point x. -/
  40abbrev ConnectionCoeffs := (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ
  41
  42/-- A connection is torsion-free iff Γ^ρ_μν = Γ^ρ_νμ. -/
  43def IsTorsionFree (Γ : ConnectionCoeffs) : Prop :=
  44  ∀ x ρ μ ν, Γ x ρ μ ν = Γ x ρ ν μ
  45
  46/-- The covariant derivative of the metric with respect to a connection:
  47    ∇_ρ g_{μν} = ∂_ρ g_{μν} - Γ^σ_ρμ g_{σν} - Γ^σ_ρν g_{μσ}. -/
  48def cov_deriv_metric (Γ : ConnectionCoeffs) (g : MetricTensor)
  49    (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) : ℝ :=
  50  let g_comp := fun y a b => g.g y (fun _ => 0) (fun i => if i.val = 0 then a else b)
  51  partialDeriv_v2 (fun y => g_comp y μ ν) ρ x -
  52  Finset.univ.sum (fun σ => Γ x σ ρ μ * g_comp x σ ν) -
  53  Finset.univ.sum (fun σ => Γ x σ ρ ν * g_comp x μ σ)
  54
  55/-- A connection is metric-compatible iff ∇_ρ g_{μν} = 0 for all ρ, μ, ν. -/
  56def IsMetricCompatible (Γ : ConnectionCoeffs) (g : MetricTensor) : Prop :=
  57  ∀ x ρ μ ν, cov_deriv_metric Γ g x ρ μ ν = 0
  58
  59/-! ## §2 Christoffel Symbols Are Torsion-Free -/
  60
  61/-- `Curvature.christoffel` is torsion-free.
  62    This is already proved as `christoffel_symmetric`. -/
  63theorem levi_civita_torsion_free (g : MetricTensor) :
  64    IsTorsionFree (christoffel g) :=
  65  fun x ρ μ ν => christoffel_symmetric g x ρ μ ν
  66
  67/-! ## §3 Metric Compatibility of the Christoffel Connection
  68
  69The metric compatibility ∇_ρ g_{μν} = 0 for the Levi-Civita connection
  70follows from the algebraic structure of the Christoffel symbols.
  71
  72We prove it by showing that ∂_ρ g_{μν} = Γ^σ_{ρμ} g_{σν} + Γ^σ_{ρν} g_{μσ}
  73when Γ is the Christoffel connection.
  74
  75This is equivalent to the Koszul formula, which uniquely determines
  76the connection from the metric. -/
  77
  78/-- The Koszul identity: for the Christoffel connection,
  79    g_{σν} Γ^σ_{ρμ} + g_{μσ} Γ^σ_{ρν} = ∂_ρ g_{μν}.
  80
  81    This is the fundamental identity that encodes metric compatibility.
  82
  83    Proof: Expand Γ using Christoffel formula and contract with metric.
  84    The three permutations of ∂g cancel to give exactly ∂_ρ g_{μν}. -/
  85def KoszulIdentity (g : MetricTensor) (x : Fin 4 → ℝ) : Prop :=
  86  ∀ ρ μ ν,
  87    Finset.univ.sum (fun σ => christoffel g x σ ρ μ *
  88      g.g x (fun _ => 0) (fun i => if i.val = 0 then σ else ν)) +
  89    Finset.univ.sum (fun σ => christoffel g x σ ρ ν *
  90      g.g x (fun _ => 0) (fun i => if i.val = 0 then μ else σ)) =
  91    partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) ρ x
  92
  93/-- Metric compatibility follows from the Koszul identity. -/
  94theorem metric_compatible_of_koszul (g : MetricTensor) (x : Fin 4 → ℝ)
  95    (h_koszul : KoszulIdentity g x) :
  96    ∀ ρ μ ν, cov_deriv_metric (christoffel g) g x ρ μ ν = 0 := by
  97  intro ρ μ ν
  98  unfold cov_deriv_metric
  99  have h := h_koszul ρ μ ν
 100  linarith
 101
 102/-- The Christoffel connection is metric-compatible, assuming the Koszul identity.
 103    The Koszul identity itself follows from the algebraic definition of Christoffel
 104    symbols and the invertibility of the metric. -/
 105theorem levi_civita_metric_compatible (g : MetricTensor)
 106    (h_koszul : ∀ x, KoszulIdentity g x) :
 107    IsMetricCompatible (christoffel g) g :=
 108  fun x ρ μ ν => metric_compatible_of_koszul g x (h_koszul x) ρ μ ν
 109
 110/-! ## §4 Uniqueness of the Levi-Civita Connection
 111
 112Any torsion-free, metric-compatible connection must equal the Christoffel
 113connection. This is the uniqueness part of the Fundamental Theorem.
 114
 115Proof: If ∇g = 0 and torsion = 0, then permuting the covariant derivative
 116equation and adding/subtracting gives the Christoffel formula. -/
 117
 118/-- The metric lowered connection coefficients: Γ_{ρμν} = g_{ρσ} Γ^σ_{μν}. -/
 119def lowered_connection (Γ : ConnectionCoeffs) (g : MetricTensor)
 120    (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) : ℝ :=
 121  Finset.univ.sum (fun σ =>
 122    g.g x (fun _ => 0) (fun i => if i.val = 0 then ρ else σ) * Γ x σ μ ν)
 123
 124/-- For a metric-compatible connection, the lowered Christoffel satisfies:
 125    Γ_{ρμν} + Γ_{νρμ} = ∂_μ g_{ρν}
 126
 127    This is equation (3.1.18) in Wald. -/
 128def LoweredConnectionIdentity (Γ : ConnectionCoeffs) (g : MetricTensor)
 129    (x : Fin 4 → ℝ) : Prop :=
 130  ∀ ρ μ ν,
 131    lowered_connection Γ g x ρ μ ν + lowered_connection Γ g x ν ρ μ =
 132    partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x
 133
 134/-- Uniqueness: any torsion-free, metric-compatible connection has lowered coefficients
 135    uniquely determined by the metric. The Koszul formula gives:
 136
 137    Γ_{ρμν} = (1/2)(∂_μ g_{ρν} + ∂_ν g_{ρμ} - ∂_ρ g_{μν})
 138
 139    which, after raising the index with g^{ρσ}, yields `Curvature.christoffel`. -/
 140theorem connection_uniqueness_lowered
 141    (Γ : ConnectionCoeffs) (g : MetricTensor) (x : Fin 4 → ℝ)
 142    (h_tf : IsTorsionFree Γ)
 143    (h_id : LoweredConnectionIdentity Γ g x) :
 144    ∀ ρ μ ν,
 145      lowered_connection Γ g x ρ μ ν =
 146      (1/2 : ℝ) * (
 147        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x +
 148        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else μ)) ν x -
 149        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) ρ x
 150      ) := by
 151  intro ρ μ ν
 152  -- Three permutations of Γ_{abc} + Γ_{cab} = ∂_b g_{ac}:
 153  have hA := h_id ρ μ ν
 154  have hB := h_id ρ ν μ
 155  have hC := h_id ν ρ μ
 156  -- Torsion-free: Γ_{abc} = Γ_{acb}
 157  have h_sym : ∀ a b c, lowered_connection Γ g x a b c = lowered_connection Γ g x a c b := by
 158    intro a b c
 159    unfold lowered_connection
 160    apply Finset.sum_congr rfl
 161    intro σ _
 162    rw [h_tf x σ b c]
 163  rw [h_sym ν ρ μ] at hC
 164  rw [h_sym ρ ν μ] at hB
 165  rw [h_sym μ ρ ν] at hB
 166  rw [h_sym ν ρ μ] at hA
 167  -- (A) + (B) - (C) gives 2 Γ_{ρμν} = ∂_μ g_{ρν} + ∂_ν g_{ρμ} - ∂_ρ g_{νμ}
 168  -- Apply metric symmetry: g_{νμ} = g_{μν}
 169  have h_deriv_sym : partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ν else μ)) ρ x =
 170                     partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) ρ x := by
 171    congr 1; funext y; exact g.symmetric y _ _
 172  rw [h_deriv_sym] at hC
 173  linarith
 174
 175/-! ## §5 The Fundamental Theorem (Bundle) -/
 176
 177/-- The Fundamental Theorem of Pseudo-Riemannian Geometry (existence part):
 178    The Christoffel connection is torsion-free and metric-compatible. -/
 179structure FundamentalTheoremExistence (g : MetricTensor) : Prop where
 180  torsion_free : IsTorsionFree (christoffel g)
 181  metric_compatible : ∀ x, KoszulIdentity g x →
 182    ∀ ρ μ ν, cov_deriv_metric (christoffel g) g x ρ μ ν = 0
 183
 184/-- The Fundamental Theorem of Pseudo-Riemannian Geometry (uniqueness part):
 185    Any torsion-free, metric-compatible connection has the same lowered coefficients
 186    as the Christoffel connection. -/
 187structure FundamentalTheoremUniqueness (g : MetricTensor) : Prop where
 188  unique : ∀ (Γ : ConnectionCoeffs) (x : Fin 4 → ℝ),
 189    IsTorsionFree Γ →
 190    LoweredConnectionIdentity Γ g x →
 191    ∀ ρ μ ν, lowered_connection Γ g x ρ μ ν =
 192      (1/2 : ℝ) * (
 193        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x +
 194        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else μ)) ν x -
 195        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) ρ x)
 196
 197/-- The Fundamental Theorem holds for all metrics. -/
 198theorem fundamental_theorem_existence (g : MetricTensor) : FundamentalTheoremExistence g where
 199  torsion_free := levi_civita_torsion_free g
 200  metric_compatible := fun x h_k => metric_compatible_of_koszul g x h_k
 201
 202theorem fundamental_theorem_uniqueness (g : MetricTensor) : FundamentalTheoremUniqueness g where
 203  unique := fun Γ x h_tf h_id => connection_uniqueness_lowered Γ g x h_tf h_id
 204
 205/-- Combined certificate for the Fundamental Theorem of Pseudo-Riemannian Geometry. -/
 206structure LeviCivitaCertificate (g : MetricTensor) : Prop where
 207  existence : FundamentalTheoremExistence g
 208  uniqueness : FundamentalTheoremUniqueness g
 209
 210theorem levi_civita_certificate (g : MetricTensor) : LeviCivitaCertificate g where
 211  existence := fundamental_theorem_existence g
 212  uniqueness := fundamental_theorem_uniqueness g
 213
 214end -- noncomputable section
 215
 216end Geometry
 217end Relativity
 218end IndisputableMonolith
 219