IndisputableMonolith.Gravity.Connection

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Levi-Civita Connection and Christoffel Symbols
   6
   7Formalizes the Levi-Civita connection in local coordinates. We work
   8in a coordinate patch where the metric is a smooth matrix-valued
   9function g : R^4 -> R^{4×4}.
  10
  11This avoids the Mathlib abstract manifold gap (no connections in Mathlib
  12as of April 2026) while remaining mathematically rigorous -- all GR
  13computations happen in coordinate patches.
  14
  15## Key Definitions and Results
  16
  17- `MetricTensor`: symmetric nondegenerate bilinear form g_{mu nu}
  18- `christoffel`: Gamma^rho_{mu nu} = (1/2) g^{rho sigma}(d_mu g_{nu sigma} + d_nu g_{mu sigma} - d_sigma g_{mu nu})
  19- `christoffel_symmetric`: Gamma^rho_{mu nu} = Gamma^rho_{nu mu}
  20- `metric_compatibility`: nabla_lambda g_{mu nu} = 0 (covariant derivative of metric vanishes)
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Gravity
  25namespace Connection
  26
  27open Constants
  28
  29/-! ## Spacetime Dimension -/
  30
  31def spacetime_dim : ℕ := 4
  32
  33abbrev Idx := Fin 4
  34
  35/-! ## Metric Tensor in Coordinates -/
  36
  37/-- A metric tensor in local coordinates: a symmetric 4x4 matrix
  38    at each spacetime point (here abstracted as just the components). -/
  39structure MetricTensor where
  40  g : Idx → Idx → ℝ
  41  symmetric : ∀ mu nu, g mu nu = g nu mu
  42
  43/-- The inverse metric g^{mu nu} (satisfying g^{mu rho} g_{rho nu} = delta^mu_nu). -/
  44structure InverseMetric where
  45  ginv : Idx → Idx → ℝ
  46  symmetric : ∀ mu nu, ginv mu nu = ginv nu mu
  47
  48/-- The flat Minkowski metric eta = diag(-1, +1, +1, +1). -/
  49def minkowski : MetricTensor where
  50  g := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0
  51  symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
  52
  53/-- The Minkowski inverse equals the Minkowski metric itself. -/
  54def minkowski_inverse : InverseMetric where
  55  ginv := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0
  56  symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
  57
  58/-! ## Christoffel Symbols -/
  59
  60/-- The Christoffel symbols of the second kind in local coordinates.
  61    Gamma^rho_{mu nu} = (1/2) g^{rho sigma} (d_mu g_{nu sigma} + d_nu g_{mu sigma} - d_sigma g_{mu nu})
  62
  63    We represent these as a function of three indices.
  64    The partial derivatives d_mu g_{nu sigma} are provided as input
  65    (they depend on the coordinate system and the point). -/
  66structure ChristoffelData where
  67  gamma : Idx → Idx → Idx → ℝ
  68
  69/-- Construct Christoffel symbols from metric, inverse metric, and metric derivatives.
  70    dg mu nu sigma = d_mu g_{nu sigma} (partial derivative of g_{nu sigma} w.r.t. x^mu). -/
  71noncomputable def christoffel_from_metric
  72    (ginv : InverseMetric) (dg : Idx → Idx → Idx → ℝ) : ChristoffelData where
  73  gamma := fun rho mu nu =>
  74    (1/2) * ∑ sigma : Idx,
  75      ginv.ginv rho sigma * (dg mu nu sigma + dg nu mu sigma - dg sigma mu nu)
  76
  77/-- Christoffel symbols are symmetric in the lower two indices (torsion-free).
  78    This follows from the symmetry of the metric derivatives:
  79    dg mu nu sigma = d_mu g_{nu sigma} is symmetric in (nu, sigma) because
  80    g_{nu sigma} = g_{sigma nu}. -/
  81theorem christoffel_symmetric (ginv : InverseMetric)
  82    (dg : Idx → Idx → Idx → ℝ)
  83    (dg_metric_sym : ∀ mu nu sigma, dg mu nu sigma = dg mu sigma nu) :
  84    ∀ rho mu nu,
  85      (christoffel_from_metric ginv dg).gamma rho mu nu =
  86      (christoffel_from_metric ginv dg).gamma rho nu mu := by
  87  intro rho mu nu
  88  simp only [christoffel_from_metric]
  89  congr 1
  90  apply Finset.sum_congr rfl
  91  intro sigma _
  92  congr 1
  93  rw [dg_metric_sym mu nu sigma, dg_metric_sym nu mu sigma,
  94      dg_metric_sym sigma mu nu, dg_metric_sym sigma nu mu]
  95  ring
  96
  97/-! ## Metric Compatibility -/
  98
  99/-- Metric compatibility: the covariant derivative of the metric vanishes.
 100    nabla_lambda g_{mu nu} = d_lambda g_{mu nu} - Gamma^rho_{lambda mu} g_{rho nu}
 101                                                  - Gamma^rho_{lambda nu} g_{mu rho} = 0
 102
 103    This is the defining property of the Levi-Civita connection:
 104    the unique connection that is both torsion-free (symmetric Christoffel)
 105    and metric-compatible (nabla g = 0). -/
 106def metric_compatibility (met : MetricTensor) (ch : ChristoffelData)
 107    (dg : Idx → Idx → Idx → ℝ) : Prop :=
 108  ∀ lambda mu nu : Idx,
 109    dg lambda mu nu -
 110    ∑ rho : Idx, (ch.gamma rho lambda mu * met.g rho nu) -
 111    ∑ rho : Idx, (ch.gamma rho lambda nu * met.g mu rho) = 0
 112
 113/-- For flat spacetime (Minkowski metric with constant components),
 114    all Christoffel symbols vanish. -/
 115theorem flat_christoffel_vanish :
 116    ∀ rho mu nu : Idx,
 117      (christoffel_from_metric minkowski_inverse (fun _ _ _ => 0)).gamma rho mu nu = 0 := by
 118  intro rho mu nu
 119  simp only [christoffel_from_metric, minkowski_inverse]
 120  norm_num
 121
 122/-! ## Certificate -/
 123
 124structure ConnectionCert where
 125  torsion_free : ∀ (ginv : InverseMetric) (dg : Idx → Idx → Idx → ℝ),
 126    (∀ mu nu sigma, dg mu nu sigma = dg mu sigma nu) →
 127    ∀ rho mu nu,
 128      (christoffel_from_metric ginv dg).gamma rho mu nu =
 129      (christoffel_from_metric ginv dg).gamma rho nu mu
 130  flat_vanish : ∀ rho mu nu : Idx,
 131    (christoffel_from_metric minkowski_inverse (fun _ _ _ => 0)).gamma rho mu nu = 0
 132
 133theorem connection_cert : ConnectionCert where
 134  torsion_free := christoffel_symmetric
 135  flat_vanish := flat_christoffel_vanish
 136
 137end Connection
 138end Gravity
 139end IndisputableMonolith
 140