IndisputableMonolith.Relativity.Geometry.LocalEquilibriumAreaVariation

   1import IndisputableMonolith.Relativity.Geometry.LocalRaychaudhuriReduction
   2import Mathlib.Analysis.Calculus.Deriv.Mul
   3import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
   4
   5/-!
   6# Local equilibrium area variation
   7
   8This module adds the explicit area-rate MODEL `A' = θ A` to the scalar
   9Raychaudhuri MODEL and derives the second area variation at one equilibrium
  10point.
  11
  12Honesty tags:
  13
  14* `LocalAreaCongruenceData.areaLaw` is an explicit MODEL interface;
  15* the inherited Raychaudhuri law is the twist-free null-horizon germ MODEL;
  16* zero initial expansion and shear are equilibrium hypotheses;
  17* no area law is integrated, and no stress tensor, Unruh relation, all-null
  18  matching, EFE, ledger-to-geometry bridge, or C-gap1 claim is introduced.
  19
  20The conclusion is therefore a theorem of calculus conditional on the two
  21explicit geometric MODEL laws. Arithmetic decoys show that zero expansion,
  22zero shear, and the unit normalization in `A' = θ A` are load-bearing.
  23-/
  24
  25noncomputable section
  26
  27namespace IndisputableMonolith
  28namespace Relativity
  29namespace Geometry
  30namespace LocalEquilibriumAreaVariation
  31
  32open LocalRaychaudhuriReduction
  33
  34/--
  35Local scalar Raychaudhuri data together with cross-sectional area. The
  36area-rate law is an explicit MODEL premise, not an integrated area formula.
  37-/
  38structure LocalAreaCongruenceData extends LocalRaychaudhuriData where
  39  area : ℝ → ℝ
  40  /-- MODEL: the local area rate obeys `dA/dλ = θ(λ) A(λ)`. -/
  41  areaLaw :
  42    ∀ lambda : ℝ,
  43      HasDerivAt area (expansion lambda * area lambda) lambda
  44
  45/--
  46The global pointwise derivative form of the explicit area-rate MODEL.
  47-/
  48theorem deriv_area_eq_expansion_mul_area (D : LocalAreaCongruenceData) :
  49    deriv D.area = fun lambda => D.expansion lambda * D.area lambda :=
  50  deriv_eq D.areaLaw
  51
  52/--
  53Before imposing equilibrium, the derivative of the area rate at `λ = 0` is
  54the product-rule expression obtained from the two MODEL laws.
  55-/
  56theorem hasDerivAt_areaRate_zero (D : LocalAreaCongruenceData) :
  57    HasDerivAt (fun lambda => D.expansion lambda * D.area lambda)
  58      (raychaudhuriSlope (D.expansion 0) (D.shearSq 0) (D.ricciNull 0) * D.area 0
  59        + D.expansion 0 * (D.expansion 0 * D.area 0)) 0 :=
  60  (D.law 0).mul (D.areaLaw 0)
  61
  62/--
  63At local equilibrium, the derivative of the area rate is
  64`-A(0) * ricciNull(0)`.
  65-/
  66theorem hasDerivAt_areaRate_eq_neg_area_mul_ricciNull
  67    (D : LocalAreaCongruenceData)
  68    (hθ : D.expansion 0 = 0) (hσ : D.shearSq 0 = 0) :
  69    HasDerivAt (fun lambda => D.expansion lambda * D.area lambda)
  70      (-D.area 0 * D.ricciNull 0) 0 := by
  71  have h :=
  72    (hasDerivAt_expansion_eq_neg_ricciNull
  73      D.toLocalRaychaudhuriData hθ hσ).mul (D.areaLaw 0)
  74  have hvalue :
  75      -D.ricciNull 0 * D.area 0
  76          + D.expansion 0 * (D.expansion 0 * D.area 0) =
  77        -D.area 0 * D.ricciNull 0 := by
  78    rw [hθ]
  79    ring
  80  exact h.congr_deriv hvalue
  81
  82/--
  83The same equilibrium result stated as differentiability of `deriv area`.
  84-/
  85theorem hasDerivAt_deriv_area_eq_neg_area_mul_ricciNull
  86    (D : LocalAreaCongruenceData)
  87    (hθ : D.expansion 0 = 0) (hσ : D.shearSq 0 = 0) :
  88    HasDerivAt (deriv D.area) (-D.area 0 * D.ricciNull 0) 0 := by
  89  rw [deriv_area_eq_expansion_mul_area D]
  90  exact hasDerivAt_areaRate_eq_neg_area_mul_ricciNull D hθ hσ
  91
  92/--
  93Pointwise second-area-variation formula at local equilibrium.
  94-/
  95theorem deriv_deriv_area_zero_eq_neg_area_mul_ricciNull
  96    (D : LocalAreaCongruenceData)
  97    (hθ : D.expansion 0 = 0) (hσ : D.shearSq 0 = 0) :
  98    deriv (deriv D.area) 0 = -D.area 0 * D.ricciNull 0 :=
  99  (hasDerivAt_deriv_area_eq_neg_area_mul_ricciNull D hθ hσ).deriv
 100
 101/--
 102The same second-area-variation formula in Mathlib's `iteratedDeriv` notation.
 103-/
 104theorem iteratedDeriv_two_area_zero_eq_neg_area_mul_ricciNull
 105    (D : LocalAreaCongruenceData)
 106    (hθ : D.expansion 0 = 0) (hσ : D.shearSq 0 = 0) :
 107    iteratedDeriv 2 D.area 0 = -D.area 0 * D.ricciNull 0 := by
 108  rw [show 2 = 1 + 1 by norm_num, iteratedDeriv_succ, iteratedDeriv_one]
 109  exact deriv_deriv_area_zero_eq_neg_area_mul_ricciNull D hθ hσ
 110
 111/--
 112Arithmetic value of the differentiated area-rate product under the unit
 113normalization `A' = θ A`.
 114-/
 115def areaRateSlope
 116    (theta shearSq ricciNull area : ℝ) : ℝ :=
 117  raychaudhuriSlope theta shearSq ricciNull * area
 118    + theta * (theta * area)
 119
 120/--
 121Any nonzero initial expansion and nonzero initial area obstruct the reduced
 122second-area formula, even when the initial shear vanishes.
 123-/
 124theorem areaRateSlope_ne_neg_area_mul_ricciNull_of_nonzero_expansion
 125    {theta shearSq ricciNull area : ℝ}
 126    (hθ : theta ≠ 0) (hσ : shearSq = 0) (hA : area ≠ 0) :
 127    areaRateSlope theta shearSq ricciNull area ≠ -area * ricciNull := by
 128  intro h
 129  have hzero : (1 / 2 : ℝ) * (theta ^ 2 * area) = 0 := by
 130    calc
 131      (1 / 2 : ℝ) * (theta ^ 2 * area) =
 132          areaRateSlope theta shearSq ricciNull area + area * ricciNull := by
 133            simp only [areaRateSlope, raychaudhuriSlope, hσ]
 134            ring
 135      _ = 0 := by rw [h]; ring
 136  have hprod : theta ^ 2 * area = 0 :=
 137    (mul_eq_zero.mp hzero).resolve_left (by norm_num)
 138  rcases mul_eq_zero.mp hprod with hthetaSq | harea
 139  · exact hθ (sq_eq_zero_iff.mp hthetaSq)
 140  · exact hA harea
 141
 142/--
 143Any nonzero initial shear-squared and nonzero initial area obstruct the
 144reduced second-area formula, even when the initial expansion vanishes.
 145-/
 146theorem areaRateSlope_ne_neg_area_mul_ricciNull_of_nonzero_shear
 147    {theta shearSq ricciNull area : ℝ}
 148    (hθ : theta = 0) (hσ : shearSq ≠ 0) (hA : area ≠ 0) :
 149    areaRateSlope theta shearSq ricciNull area ≠ -area * ricciNull := by
 150  intro h
 151  have hzero : shearSq * area = 0 := by
 152    calc
 153      shearSq * area =
 154          -(areaRateSlope theta shearSq ricciNull area + area * ricciNull) := by
 155            simp only [areaRateSlope, raychaudhuriSlope, hθ]
 156            ring
 157      _ = 0 := by rw [h]; ring
 158  rcases mul_eq_zero.mp hzero with hshear | harea
 159  · exact hσ hshear
 160  · exact hA harea
 161
 162/-- Concrete expansion decoy: `θ=2`, `σ²=0`, `R=1`, and `A=1`. -/
 163theorem decoy_nonzero_expansion_areaRate_ne :
 164    areaRateSlope 2 0 1 1 ≠ -(1 : ℝ) := by
 165  norm_num [areaRateSlope, raychaudhuriSlope]
 166
 167/-- Concrete shear decoy: `θ=0`, `σ²=1`, `R=1`, and `A=1`. -/
 168theorem decoy_nonzero_shear_areaRate_ne :
 169    areaRateSlope 0 1 1 1 ≠ -(1 : ℝ) := by
 170  norm_num [areaRateSlope, raychaudhuriSlope]
 171
 172/--
 173Arithmetic derivative of an area law with coefficient `c`,
 174`A' = c θ A`, evaluated using the Raychaudhuri slope.
 175-/
 176def scaledAreaRateSlope
 177    (c theta shearSq ricciNull area : ℝ) : ℝ :=
 178  c * (raychaudhuriSlope theta shearSq ricciNull * area
 179    + theta * (c * theta * area))
 180
 181/--
 182Normalization decoy: at the equilibrium witness `θ=0`, `σ²=0`, `R=1`,
 183`A=1`, coefficient `c=2` yields second-area rate `-2`, not the unit-law
 184coefficient `-1`.
 185-/
 186theorem decoy_areaLaw_coefficient_two_changes_equilibrium :
 187    scaledAreaRateSlope 2 0 0 1 1 ≠ -(1 : ℝ) := by
 188  norm_num [scaledAreaRateSlope, raychaudhuriSlope]
 189
 190end LocalEquilibriumAreaVariation
 191end Geometry
 192end Relativity
 193end IndisputableMonolith
 194