IndisputableMonolith.Gravity.RiemannTensor

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Gravity.Connection
   4
   5/-!
   6# Riemann Curvature Tensor in Coordinates
   7
   8Defines the Riemann curvature tensor from Christoffel symbols and
   9proves its algebraic symmetries and the algebraic Bianchi identity.
  10
  11## Key Results
  12
  13- `riemann_tensor`: R^rho_{sigma mu nu} in terms of Christoffel symbols and their derivatives
  14- `riemann_antisymmetric_last_two`: R^rho_{sigma mu nu} = -R^rho_{sigma nu mu}
  15- `algebraic_bianchi`: R^rho_{[sigma mu nu]} = 0
  16- `riemann_flat_vanishes`: R = 0 for flat (Minkowski) spacetime
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Gravity
  21namespace RiemannTensor
  22
  23open Connection
  24
  25/-! ## Riemann Tensor Definition -/
  26
  27/-- The Riemann curvature tensor in local coordinates:
  28    R^rho_{sigma mu nu} = d_mu Gamma^rho_{nu sigma} - d_nu Gamma^rho_{mu sigma}
  29                         + Gamma^rho_{mu lambda} Gamma^lambda_{nu sigma}
  30                         - Gamma^rho_{nu lambda} Gamma^lambda_{mu sigma}
  31
  32    Inputs:
  33    - gamma: Christoffel symbols Gamma^rho_{mu nu}
  34    - dgamma: derivatives d_lambda Gamma^rho_{mu nu} -/
  35noncomputable def riemann_tensor
  36    (gamma : Idx → Idx → Idx → ℝ)
  37    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  38    (rho sigma mu nu : Idx) : ℝ :=
  39  dgamma mu rho nu sigma - dgamma nu rho mu sigma +
  40  ∑ lambda : Idx, (gamma rho mu lambda * gamma lambda nu sigma) -
  41  ∑ lambda : Idx, (gamma rho nu lambda * gamma lambda mu sigma)
  42
  43/-! ## Algebraic Symmetries -/
  44
  45/-- R^rho_{sigma mu nu} is antisymmetric in the last two indices:
  46    R^rho_{sigma mu nu} = -R^rho_{sigma nu mu}.
  47
  48    Proof: swapping mu <-> nu negates the d_mu Gamma - d_nu Gamma terms
  49    and swaps the quadratic Gamma terms. -/
  50theorem riemann_antisymmetric_last_two
  51    (gamma : Idx → Idx → Idx → ℝ)
  52    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  53    (rho sigma mu nu : Idx) :
  54    riemann_tensor gamma dgamma rho sigma mu nu =
  55    -(riemann_tensor gamma dgamma rho sigma nu mu) := by
  56  simp only [riemann_tensor]
  57  ring
  58
  59/-- For flat spacetime (all Gamma = 0, all dGamma = 0), the Riemann tensor vanishes. -/
  60theorem riemann_flat_vanishes (rho sigma mu nu : Idx) :
  61    riemann_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) rho sigma mu nu = 0 := by
  62  simp [riemann_tensor]
  63
  64/-! ## Algebraic Bianchi Identity -/
  65
  66/-- The algebraic (first) Bianchi identity:
  67    R^rho_{sigma mu nu} + R^rho_{mu nu sigma} + R^rho_{nu sigma mu} = 0
  68
  69    This is a consequence of the torsion-free condition (symmetric Christoffel). -/
  70theorem algebraic_bianchi
  71    (gamma : Idx → Idx → Idx → ℝ)
  72    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  73    (h_sym : ∀ rho mu nu, gamma rho mu nu = gamma rho nu mu)
  74    (h_dsym : ∀ lambda rho mu nu, dgamma lambda rho mu nu = dgamma lambda rho nu mu)
  75    (rho sigma mu nu : Idx) :
  76    riemann_tensor gamma dgamma rho sigma mu nu +
  77    riemann_tensor gamma dgamma rho mu nu sigma +
  78    riemann_tensor gamma dgamma rho nu sigma mu = 0 := by
  79  have anti1 := riemann_antisymmetric_last_two gamma dgamma rho sigma mu nu
  80  have anti2 := riemann_antisymmetric_last_two gamma dgamma rho mu nu sigma
  81  have anti3 := riemann_antisymmetric_last_two gamma dgamma rho nu sigma mu
  82  simp only [riemann_tensor] at *
  83  have quad_cancel : ∀ x : Idx,
  84    (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma) +
  85    (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu) +
  86    (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu) = 0 := by
  87    intro x
  88    rw [h_sym x nu sigma, h_sym x mu sigma, h_sym x sigma mu,
  89        h_sym x nu mu, h_sym x mu nu, h_sym x sigma nu]; ring
  90  have h_sums : (∑ x : Idx, (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma)) +
  91    (∑ x : Idx, (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu)) +
  92    (∑ x : Idx, (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu)) = 0 := by
  93    rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  94    exact Finset.sum_eq_zero (fun x _ => quad_cancel x)
  95  have key : ∀ x : Idx,
  96    (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma) +
  97    (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu) +
  98    (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu) = 0 := by
  99    intro x; rw [h_sym x nu sigma, h_sym x mu sigma, h_sym x sigma mu,
 100                  h_sym x nu mu, h_sym x mu nu, h_sym x sigma nu]; ring
 101  have sum_zero :
 102    (∑ x : Idx, (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma)) +
 103    (∑ x : Idx, (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu)) +
 104    (∑ x : Idx, (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu)) = 0 := by
 105    rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
 106    exact Finset.sum_eq_zero (fun x _ => key x)
 107  have neg_flip : ∀ (f g : Idx → ℝ),
 108    ∑ x : Idx, (f x - g x) = -(∑ x : Idx, (g x - f x)) := by
 109    intros f g
 110    have : ∀ x ∈ Finset.univ, f x - g x = -(g x - f x) := by intros; ring
 111    rw [Finset.sum_congr rfl this, Finset.sum_neg_distrib]
 112  rw [h_dsym mu rho nu sigma, h_dsym nu rho mu sigma, h_dsym nu rho sigma mu,
 113      h_dsym sigma rho nu mu, h_dsym sigma rho mu nu, h_dsym mu rho sigma nu]
 114  have full_sum :
 115    (∑ x : Idx, (gamma rho mu x * gamma x nu sigma)) -
 116    (∑ x : Idx, (gamma rho nu x * gamma x mu sigma)) +
 117    ((∑ x : Idx, (gamma rho nu x * gamma x sigma mu)) -
 118     (∑ x : Idx, (gamma rho sigma x * gamma x nu mu))) +
 119    ((∑ x : Idx, (gamma rho sigma x * gamma x mu nu)) -
 120     (∑ x : Idx, (gamma rho mu x * gamma x sigma nu))) = 0 := by
 121    rw [← Finset.sum_sub_distrib, ← Finset.sum_sub_distrib, ← Finset.sum_sub_distrib,
 122        ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
 123    exact Finset.sum_eq_zero (fun x _ => key x)
 124  linarith
 125
 126/-! ## Certificate -/
 127
 128structure RiemannCert where
 129  antisymmetric : ∀ gamma dgamma rho sigma mu nu,
 130    riemann_tensor gamma dgamma rho sigma mu nu =
 131    -(riemann_tensor gamma dgamma rho sigma nu mu)
 132  flat_vanishes : ∀ rho sigma mu nu,
 133    riemann_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) rho sigma mu nu = 0
 134
 135theorem riemann_cert : RiemannCert where
 136  antisymmetric := riemann_antisymmetric_last_two
 137  flat_vanishes := riemann_flat_vanishes
 138
 139end RiemannTensor
 140end Gravity
 141end IndisputableMonolith
 142