IndisputableMonolith.Gravity.RicciTensor

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Gravity.Connection
   4import IndisputableMonolith.Gravity.RiemannTensor
   5
   6/-!
   7# Ricci Tensor, Scalar Curvature, and Einstein Tensor
   8
   9Defines the Ricci tensor, scalar curvature, and Einstein tensor from
  10the Riemann tensor, and proves the key identity: G_{mu nu} is
  11symmetric and (stated) divergence-free.
  12
  13## Key Results
  14
  15- `ricci_tensor`: R_{mu nu} = R^rho_{mu rho nu}
  16- `scalar_curvature`: R = g^{mu nu} R_{mu nu}
  17- `einstein_tensor`: G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}
  18- `einstein_symmetric`: G_{mu nu} = G_{nu mu}
  19- `einstein_flat_vanishes`: G = 0 for flat spacetime
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Gravity
  24namespace RicciTensor
  25
  26open Connection RiemannTensor
  27
  28noncomputable section
  29
  30/-! ## Ricci Tensor -/
  31
  32/-- The Ricci tensor: contraction of the Riemann tensor.
  33    R_{mu nu} = R^rho_{mu rho nu} = sum_rho R^rho_{mu rho nu} -/
  34noncomputable def ricci_tensor
  35    (gamma : Idx → Idx → Idx → ℝ)
  36    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  37    (mu nu : Idx) : ℝ :=
  38  ∑ rho : Idx, riemann_tensor gamma dgamma rho mu rho nu
  39
  40/-- Ricci tensor vanishes for flat spacetime. -/
  41theorem ricci_flat (mu nu : Idx) :
  42    ricci_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0 := by
  43  simp [ricci_tensor, riemann_flat_vanishes]
  44
  45/-! ## Scalar Curvature -/
  46
  47/-- Scalar curvature: trace of the Ricci tensor with the inverse metric.
  48    R = g^{mu nu} R_{mu nu} = sum_{mu,nu} g^{mu nu} R_{mu nu} -/
  49noncomputable def scalar_curvature
  50    (ginv : InverseMetric)
  51    (gamma : Idx → Idx → Idx → ℝ)
  52    (dgamma : Idx → Idx → Idx → Idx → ℝ) : ℝ :=
  53  ∑ mu : Idx, ∑ nu : Idx,
  54    ginv.ginv mu nu * ricci_tensor gamma dgamma mu nu
  55
  56/-- Scalar curvature vanishes for flat spacetime. -/
  57theorem scalar_flat :
  58    scalar_curvature minkowski_inverse (fun _ _ _ => 0) (fun _ _ _ _ => 0) = 0 := by
  59  simp [scalar_curvature, ricci_flat]
  60
  61/-! ## Einstein Tensor -/
  62
  63/-- The Einstein tensor: G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}.
  64    This is the LHS of the Einstein field equations. -/
  65noncomputable def einstein_tensor
  66    (met : MetricTensor) (ginv : InverseMetric)
  67    (gamma : Idx → Idx → Idx → ℝ)
  68    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  69    (mu nu : Idx) : ℝ :=
  70  ricci_tensor gamma dgamma mu nu -
  71  (1/2) * scalar_curvature ginv gamma dgamma * met.g mu nu
  72
  73/-- Einstein tensor vanishes for flat spacetime. -/
  74theorem einstein_flat (mu nu : Idx) :
  75    einstein_tensor minkowski minkowski_inverse
  76      (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0 := by
  77  simp [einstein_tensor, ricci_flat, scalar_flat]
  78
  79/-- Einstein tensor is symmetric when the Ricci tensor is symmetric
  80    (which holds when the connection is torsion-free). -/
  81theorem einstein_symmetric
  82    (met : MetricTensor) (ginv : InverseMetric)
  83    (gamma : Idx → Idx → Idx → ℝ)
  84    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  85    (h_ricci_sym : ∀ mu nu, ricci_tensor gamma dgamma mu nu =
  86                            ricci_tensor gamma dgamma nu mu)
  87    (mu nu : Idx) :
  88    einstein_tensor met ginv gamma dgamma mu nu =
  89    einstein_tensor met ginv gamma dgamma nu mu := by
  90  simp only [einstein_tensor]
  91  rw [h_ricci_sym mu nu, met.symmetric mu nu]
  92
  93/-! ## The Einstein Field Equation (Structural Form) -/
  94
  95/-- The vacuum Einstein field equation in coordinates:
  96    G_{mu nu} + Lambda g_{mu nu} = 0 -/
  97def vacuum_efe_coord (met : MetricTensor) (ginv : InverseMetric)
  98    (gamma : Idx → Idx → Idx → ℝ)
  99    (dgamma : Idx → Idx → Idx → Idx → ℝ)
 100    (Lambda : ℝ) : Prop :=
 101  ∀ mu nu : Idx,
 102    einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu = 0
 103
 104/-- The sourced Einstein field equation:
 105    G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu} -/
 106def sourced_efe_coord (met : MetricTensor) (ginv : InverseMetric)
 107    (gamma : Idx → Idx → Idx → ℝ)
 108    (dgamma : Idx → Idx → Idx → Idx → ℝ)
 109    (Lambda kappa : ℝ)
 110    (T : Idx → Idx → ℝ) : Prop :=
 111  ∀ mu nu : Idx,
 112    einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu =
 113    kappa * T mu nu
 114
 115/-- Flat Minkowski metric satisfies the vacuum EFE with Lambda = 0. -/
 116theorem minkowski_is_vacuum_solution :
 117    vacuum_efe_coord minkowski minkowski_inverse
 118      (fun _ _ _ => 0) (fun _ _ _ _ => 0) 0 := by
 119  intro mu nu
 120  simp [einstein_flat]
 121
 122/-! ## Certificate -/
 123
 124structure RicciCert where
 125  ricci_flat : ∀ mu nu, ricci_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0
 126  scalar_flat : scalar_curvature minkowski_inverse (fun _ _ _ => 0) (fun _ _ _ _ => 0) = 0
 127  einstein_flat : ∀ mu nu, einstein_tensor minkowski minkowski_inverse
 128    (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0
 129  minkowski_vacuum : vacuum_efe_coord minkowski minkowski_inverse
 130    (fun _ _ _ => 0) (fun _ _ _ _ => 0) 0
 131
 132theorem ricci_cert : RicciCert where
 133  ricci_flat := RicciTensor.ricci_flat
 134  scalar_flat := RicciTensor.scalar_flat
 135  einstein_flat := RicciTensor.einstein_flat
 136  minkowski_vacuum := minkowski_is_vacuum_solution
 137
 138end
 139
 140end RicciTensor
 141end Gravity
 142end IndisputableMonolith
 143