IndisputableMonolith.Relativity.Geometry.Curvature

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry.Tensor
   3import IndisputableMonolith.Relativity.Geometry.Metric
   4import IndisputableMonolith.Relativity.Calculus.Derivatives
   5
   6namespace IndisputableMonolith
   7namespace Relativity
   8namespace Geometry
   9
  10open Calculus
  11
  12/-- **Christoffel Symbols** derived from the metric. -/
  13noncomputable def christoffel (g : MetricTensor) : (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ :=
  14  fun x rho mu nu =>
  15    (1/2 : ℝ) * Finset.univ.sum (fun (lambda : Fin 4) =>
  16      (inverse_metric g) x (fun _ => rho) (fun _ => lambda) * (
  17        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else lambda)) nu x) +
  18        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then nu else lambda)) mu x) -
  19        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else nu)) lambda x)
  20      ))
  21
  22/-- Christoffel symbols are symmetric in the lower indices (torsion-free). -/
  23theorem christoffel_symmetric (g : MetricTensor) (x : Fin 4 → ℝ) (rho mu nu : Fin 4) :
  24    christoffel g x rho mu nu = christoffel g x rho nu mu := by
  25  unfold christoffel
  26  congr 1
  27  apply Finset.sum_congr rfl
  28  intro lambda _
  29  ring_nf
  30  -- Symmetry of g indices: ∂_ν g_{μλ} + ∂_μ g_{νλ} - ∂_λ g_{μν} = ∂_μ g_{νλ} + ∂_ν g_{μλ} - ∂_λ g_{νμ}
  31  have h_sym : (fun y => g.g y (fun _ => 0) (fun i : Fin 2 => if i.val = 0 then mu else nu)) =
  32               (fun y => g.g y (fun _ => 0) (fun i : Fin 2 => if i.val = 0 then nu else mu)) := by
  33    funext y
  34    exact g.symmetric y (fun _ => 0) (fun i : Fin 2 => if i.val = 0 then mu else nu)
  35  rw [h_sym]
  36
  37/-- **Riemann Curvature Tensor** $R^{\rho}_{\sigma\mu\nu}$. -/
  38noncomputable def riemann_tensor (g : MetricTensor) : Tensor 1 3 :=
  39  fun x up low =>
  40    let rho := up 0
  41    let sigma := low 0
  42    let mu := low 1
  43    let nu := low 2
  44    let Γ := christoffel g
  45    (partialDeriv_v2 (fun y => Γ y rho nu sigma) mu x) -
  46    (partialDeriv_v2 (fun y => Γ y rho mu sigma) nu x) +
  47    Finset.univ.sum (fun (lambda : Fin 4) => Γ x rho mu lambda * Γ x lambda nu sigma) -
  48    Finset.univ.sum (fun (lambda : Fin 4) => Γ x rho nu lambda * Γ x lambda mu sigma)
  49
  50/-- **Ricci Tensor** $R_{\mu\nu} = R^{\rho}_{\mu\rho\nu}$. -/
  51noncomputable def ricci_tensor (g : MetricTensor) : BilinearForm :=
  52  fun x _ low =>
  53    let mu := low 0
  54    let nu := low 1
  55    Finset.univ.sum (fun (rho : Fin 4) =>
  56      riemann_tensor g x (fun _ => rho) (fun i => if i.val = 0 then mu else if i.val = 1 then rho else nu))
  57
  58/-- **THEOREM (Riemann Antisymmetry)**: The Riemann tensor is antisymmetric in its last two indices.
  59    R^ρ_{σμν} = -R^ρ_{σνμ}
  60
  61    This follows directly from the definition of the Riemann tensor in terms of
  62    Christoffel symbols. -/
  63theorem riemann_antisymmetric_last_two (g : MetricTensor) (x : Fin 4 → ℝ) (ρ σ μ ν : Fin 4) :
  64    riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then σ else if i.val = 1 then μ else ν) =
  65    -riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then σ else if i.val = 1 then ν else μ) := by
  66  -- The Riemann tensor definition: ∂μ Γ^ρ_νσ - ∂ν Γ^ρ_μσ + Γ^ρ_μλ Γ^λ_νσ - Γ^ρ_νλ Γ^λ_μσ
  67  -- Swapping μ ↔ ν gives: ∂ν Γ^ρ_μσ - ∂μ Γ^ρ_νσ + Γ^ρ_νλ Γ^λ_μσ - Γ^ρ_μλ Γ^λ_νσ
  68  -- Which is exactly the negation of the original
  69  unfold riemann_tensor
  70  -- Simplify the index functions - the pattern is:
  71  -- LHS: low 0 = σ, low 1 = μ, low 2 = ν
  72  -- RHS: low 0 = σ, low 1 = ν, low 2 = μ
  73  -- The Riemann structure: ∂_{low 1} Γ_{low 2, low 0} - ∂_{low 2} Γ_{low 1, low 0} + quadratic terms
  74  -- Swapping low 1 ↔ low 2 negates the expression
  75  simp only [Fin.val_zero, Fin.val_one, Fin.val_two,
  76             show (0 : ℕ) ≠ 1 from by decide,
  77             show (1 : ℕ) ≠ 0 from by decide,
  78             show (2 : ℕ) ≠ 0 from by decide, show (2 : ℕ) ≠ 1 from by decide,
  79             if_true, if_false]
  80  ring
  81
  82/-! **AXIOMS DISCHARGED 2026-04-17.**
  83
  84The previous `riemann_pair_exchange` and `ricci_tensor_symmetric` axiom
  85declarations have been deleted.  They are now provided as conditional
  86theorems in `RiemannSymmetries.lean`:
  87
  88- `riemann_pair_exchange_proof` (from `riemann_lowered_eq_explicit_hypothesis`)
  89- `riemann_pair_exchange_from_definition` (clean interface)
  90- `ricci_tensor_symmetric_thm` (from `riemann_trace_vanishes_hypothesis`)
  91- `ricci_tensor_symmetric_proof` (clean interface, `∀ μ ν` version)
  92- `curvature_axioms_hold` (bundle with both)
  93- `riemann_trace_vanishes_of_smooth` (discharges the trace hypothesis from
  94  the standard Schwarz-theorem-style smoothness condition `MetricSmooth`)
  95
  96The conditional form is the honest one: pair exchange and Ricci symmetry
  97hold for connections satisfying the standard explicit-form / trace-vanishing
  98identities of Wald §3.2.  Stating them as universal axioms over arbitrary
  99`MetricTensor` was an over-claim.  The §XXIII.B' RS-internal axiom count
 100drops by 2 with this discharge.  Downstream code that needs the symmetries
 101should either supply the discharge hypothesis or use the smoothness bridge. -/
 102
 103/-- **Ricci Scalar** $R = g^{\mu\nu} R_{\mu\nu}$. -/
 104noncomputable def ricci_scalar (g : MetricTensor) (x : Fin 4 → ℝ) : ℝ :=
 105  Finset.univ.sum (fun (mu : Fin 4) =>
 106    Finset.univ.sum (fun (nu : Fin 4) =>
 107      inverse_metric g x (fun _ => mu) (fun _ => nu) * ricci_tensor g x (fun _ => 0) (fun i => if i.val = 0 then mu else nu)))
 108
 109/-- **Einstein Tensor** $G_{\mu\nu} = R_{\mu\nu} - \frac{1}{2} g_{\mu\nu} R$. -/
 110noncomputable def einstein_tensor (g : MetricTensor) : BilinearForm :=
 111  fun x up low =>
 112    ricci_tensor g x up low - (1/2 : ℝ) * g.g x up low * ricci_scalar g x
 113
 114/-! The previous `ricci_tensor_symmetric'` wrapper depended on the deleted
 115`ricci_tensor_symmetric` axiom.  Use `RiemannSymmetries.ricci_tensor_symmetric_proof`
 116(which takes the trace-vanishing hypothesis explicitly) or
 117`RiemannSymmetries.curvature_axioms_hold` (bundled). -/
 118
 119/-! ## Minkowski Space Theorems -/
 120
 121/-- The Minkowski metric η doesn't depend on x, so its derivatives vanish. -/
 122lemma eta_deriv_zero (μ ν κ : Fin 4) (x : Fin 4 → ℝ) :
 123    partialDeriv_v2 (fun y => eta y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) κ x = 0 := by
 124  apply partialDeriv_v2_const (c := eta x (fun _ => 0) (fun i => if i.val = 0 then μ else ν))
 125  intro y; unfold eta; rfl
 126
 127/-- Christoffel symbols vanish for the Minkowski metric. -/
 128theorem minkowski_christoffel_zero_proper (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) :
 129    christoffel minkowski_tensor x ρ μ ν = 0 := by
 130  unfold christoffel minkowski_tensor
 131  dsimp
 132  simp only [eta_deriv_zero, add_zero, sub_zero, mul_zero, Finset.sum_const_zero]
 133
 134/-- Riemann tensor vanishes for Minkowski space. -/
 135theorem minkowski_riemann_zero (x : Fin 4 → ℝ) (up : Fin 1 → Fin 4) (low : Fin 3 → Fin 4) :
 136    riemann_tensor minkowski_tensor x up low = 0 := by
 137  unfold riemann_tensor
 138  have hΓ : ∀ y r m n, christoffel minkowski_tensor y r m n = 0 := by
 139    intro y r m n; exact minkowski_christoffel_zero_proper y r m n
 140  have h_deriv : ∀ f μ x, (∀ y, f y = 0) → partialDeriv_v2 f μ x = 0 := by
 141    intro f μ x h; apply partialDeriv_v2_const (c := 0); exact h
 142  simp [hΓ, h_deriv, Finset.sum_const_zero]
 143
 144/-- Ricci tensor vanishes for Minkowski space. -/
 145theorem minkowski_ricci_zero (x : Fin 4 → ℝ) (up : Fin 0 → Fin 4) (low : Fin 2 → Fin 4) :
 146    ricci_tensor minkowski_tensor x up low = 0 := by
 147  unfold ricci_tensor
 148  simp [minkowski_riemann_zero, Finset.sum_const_zero]
 149
 150/-- Ricci scalar vanishes for Minkowski space. -/
 151theorem minkowski_ricci_scalar_zero (x : Fin 4 → ℝ) : ricci_scalar minkowski_tensor x = 0 := by
 152  unfold ricci_scalar
 153  simp [minkowski_ricci_zero, Finset.sum_const_zero]
 154
 155/-- Einstein tensor vanishes for Minkowski space. -/
 156theorem minkowski_einstein_zero (x : Fin 4 → ℝ) (up : Fin 0 → Fin 4) (low : Fin 2 → Fin 4) :
 157    einstein_tensor minkowski_tensor x up low = 0 := by
 158  unfold einstein_tensor
 159  simp only [minkowski_ricci_zero, minkowski_ricci_scalar_zero, mul_zero, sub_zero]
 160
 161end Geometry
 162end Relativity
 163end IndisputableMonolith
 164