IndisputableMonolith.Relativity.Geometry.LocalRaychaudhuriReduction

   1import Mathlib.Analysis.Calculus.Deriv.Basic
   2import Mathlib.Tactic.Ring
   3import Mathlib.Tactic.NormNum
   4import Mathlib.Tactic.Linarith
   5
   6/-!
   7# Local Raychaudhuri equilibrium reduction
   8
   9This module records the scalar 4D null-congruence slope and proves the
  10local-equilibrium algebraic reduction of that slope under an explicit
  11differential-law MODEL.
  12
  13Honesty tags:
  14
  15* `LocalRaychaudhuriData.law` is an explicit MODEL interface (the twist-free
  16  null-horizon Raychaudhuri ODE for the scalar expansion);
  17* zero initial expansion and shear are equilibrium hypotheses, not derived
  18  geometric facts;
  19* this module does **not** introduce a metric, null vector, Ricci tensor,
  20  area element, ledger, stress, Unruh, all-null equality, EFE, or C-gap1 claim.
  21
  22What is proved: conditional on the MODEL law, the general initial slope at
  23`λ = 0`, and under `expansion 0 = 0` with `shearSq 0 = 0`, the initial
  24expansion derivative equals `-ricciNull 0`. Arithmetic decoys show each
  25equilibrium premise is load-bearing.
  26-/
  27
  28noncomputable section
  29
  30namespace IndisputableMonolith
  31namespace Relativity
  32namespace Geometry
  33namespace LocalRaychaudhuriReduction
  34
  35/--
  36Scalar right-hand side of the 4D null Raychaudhuri law for expansion `θ`,
  37shear-squared `σ²`, and Ricci null contraction `R_{ab}k^a k^b`:
  38
  39`dθ/dλ = -½ θ² - σ² - R_{ab}k^a k^b`.
  40
  41The three arguments are treated as real scalars; no spacetime geometry is
  42imported.
  43-/
  44def raychaudhuriSlope (theta shearSq ricciNull : ℝ) : ℝ :=
  45  -(1 / 2) * theta ^ 2 - shearSq - ricciNull
  46
  47/--
  48Local scalar Raychaudhuri data along an affine parameter. The differential law
  49is an explicit MODEL premise and is not claimed derived.
  50-/
  51structure LocalRaychaudhuriData where
  52  expansion : ℝ → ℝ
  53  shearSq : ℝ → ℝ
  54  ricciNull : ℝ → ℝ
  55  /-- MODEL: expansion obeys the twist-free null-horizon Raychaudhuri ODE. -/
  56  law :
  57    ∀ lambda : ℝ,
  58      HasDerivAt expansion
  59        (raychaudhuriSlope (expansion lambda) (shearSq lambda) (ricciNull lambda))
  60        lambda
  61
  62/--
  63General initial slope: the MODEL law specializes at `λ = 0` to the
  64Raychaudhuri right-hand side evaluated on the initial data.
  65-/
  66theorem hasDerivAt_expansion_zero (D : LocalRaychaudhuriData) :
  67    HasDerivAt D.expansion
  68      (raychaudhuriSlope (D.expansion 0) (D.shearSq 0) (D.ricciNull 0)) 0 :=
  69  D.law 0
  70
  71/--
  72Under local equilibrium `θ(0) = 0` and `σ²(0) = 0`, the MODEL law reduces to
  73`HasDerivAt expansion (-ricciNull 0) 0`.
  74-/
  75theorem hasDerivAt_expansion_eq_neg_ricciNull
  76    (D : LocalRaychaudhuriData)
  77    (hθ : D.expansion 0 = 0) (hσ : D.shearSq 0 = 0) :
  78    HasDerivAt D.expansion (-D.ricciNull 0) 0 := by
  79  have h := hasDerivAt_expansion_zero D
  80  have hslope :
  81      raychaudhuriSlope (D.expansion 0) (D.shearSq 0) (D.ricciNull 0) =
  82        -D.ricciNull 0 := by
  83    simp only [raychaudhuriSlope, hθ, hσ]
  84    ring
  85  exact h.congr_deriv hslope
  86
  87/--
  88Pointwise derivative form of the equilibrium reduction.
  89-/
  90theorem deriv_expansion_zero_eq_neg_ricciNull
  91    (D : LocalRaychaudhuriData)
  92    (hθ : D.expansion 0 = 0) (hσ : D.shearSq 0 = 0) :
  93    deriv D.expansion 0 = -D.ricciNull 0 :=
  94  (hasDerivAt_expansion_eq_neg_ricciNull D hθ hσ).deriv
  95
  96/--
  97Decoy: nonzero initial expansion with zero shear makes the Raychaudhuri
  98slope differ from `-ricciNull`. Explicit rationals `θ = 2`, `σ² = 0`, `R = 1`
  99give slope `-3 ≠ -1`.
 100-/
 101theorem decoy_nonzero_expansion_slope_ne_neg_ricciNull :
 102    raychaudhuriSlope (2 : ℝ) 0 1 ≠ -(1 : ℝ) := by
 103  have hslope : raychaudhuriSlope (2 : ℝ) 0 1 = -3 := by
 104    simp only [raychaudhuriSlope]
 105    norm_num
 106  rw [hslope]
 107  norm_num
 108
 109/--
 110Decoy: zero initial expansion with nonzero shear likewise makes the full slope
 111differ from `-ricciNull`. Explicit rationals `θ = 0`, `σ² = 1`, `R = 1`
 112give slope `-2 ≠ -1`.
 113-/
 114theorem decoy_nonzero_shear_slope_ne_neg_ricciNull :
 115    raychaudhuriSlope (0 : ℝ) 1 1 ≠ -(1 : ℝ) := by
 116  have hslope : raychaudhuriSlope (0 : ℝ) 1 1 = -2 := by
 117    simp only [raychaudhuriSlope]
 118    norm_num
 119  rw [hslope]
 120  norm_num
 121
 122/--
 123General arithmetic form of the expansion decoy: any nonzero `θ` with zero shear
 124moves the slope away from `-R`.
 125-/
 126theorem raychaudhuriSlope_ne_neg_ricciNull_of_nonzero_expansion
 127    {theta shearSq ricciNull : ℝ}
 128    (hθ : theta ≠ 0) (hσ : shearSq = 0) :
 129    raychaudhuriSlope theta shearSq ricciNull ≠ -ricciNull := by
 130  intro h
 131  have hslope :
 132      raychaudhuriSlope theta shearSq ricciNull =
 133        -(1 / 2) * theta ^ 2 - ricciNull := by
 134    simp only [raychaudhuriSlope, hσ]
 135    ring
 136  have hred : -(1 / 2) * theta ^ 2 - ricciNull = -ricciNull := by
 137    simpa [hslope] using h
 138  have hsq : -(1 / 2) * theta ^ 2 = 0 := by
 139    linarith
 140  have hhalf : (1 / 2 : ℝ) ≠ 0 := by norm_num
 141  have hneg : -((1 / 2 : ℝ) * theta ^ 2) = 0 := by
 142    simpa [neg_mul] using hsq
 143  have hprod : (1 / 2 : ℝ) * theta ^ 2 = 0 := by
 144    linarith
 145  have hpow : theta ^ 2 = 0 :=
 146    (mul_eq_zero.mp hprod).resolve_left hhalf
 147  exact hθ (sq_eq_zero_iff.mp hpow)
 148
 149/--
 150General arithmetic form of the shear decoy: any nonzero shear-squared with zero
 151expansion moves the slope away from `-R`.
 152-/
 153theorem raychaudhuriSlope_ne_neg_ricciNull_of_nonzero_shear
 154    {theta shearSq ricciNull : ℝ}
 155    (hθ : theta = 0) (hσ : shearSq ≠ 0) :
 156    raychaudhuriSlope theta shearSq ricciNull ≠ -ricciNull := by
 157  intro h
 158  have hslope :
 159      raychaudhuriSlope theta shearSq ricciNull =
 160        -shearSq - ricciNull := by
 161    simp only [raychaudhuriSlope, hθ]
 162    ring
 163  have hred : -shearSq - ricciNull = -ricciNull := by
 164    simpa [hslope] using h
 165  have : -shearSq = 0 := by linarith
 166  exact hσ (neg_eq_zero.mp this)
 167
 168end LocalRaychaudhuriReduction
 169end Geometry
 170end Relativity
 171end IndisputableMonolith
 172