IndisputableMonolith.Relativity.Geometry.LocalAreaRaychaudhuri

   1import IndisputableMonolith.Gravity.ClausiusEinsteinBridge
   2import IndisputableMonolith.Relativity.Geometry.LocalEquilibriumAreaVariation
   3
   4/-!
   5# Matrix Ricci adapter for local Raychaudhuri data
   6
   7`LocalEquilibriumAreaVariation` already proves the equilibrium second-area
   8germ from the explicit area-rate and Raychaudhuri MODEL laws. This module adds
   9only a definitional adapter from a matrix-valued Ricci field and Lorentz-null
  10probes to the scalar `ricciNull` consumed there.
  11
  12Honesty tags:
  13
  14* `MatrixRicciRaychaudhuriData.law` is MODEL: it is the twist-free null
  15  Raychaudhuri ODE with the Ricci contraction written explicitly.
  16* No theorem equates Ricci with stress, derives the probe field from the finite
  17  cut, or states an Einstein equation.
  18-/
  19
  20noncomputable section
  21
  22namespace IndisputableMonolith
  23namespace Relativity
  24namespace Geometry
  25namespace LocalAreaRaychaudhuri
  26
  27open LocalRaychaudhuriReduction
  28open LocalEquilibriumAreaVariation
  29open Gravity.ClausiusEinsteinBridge
  30
  31/--
  32Raychaudhuri data whose Ricci-null scalar is definitionally the quadratic
  33contraction of a symmetric matrix-valued Ricci field against a Lorentz-null
  34probe field.
  35
  36The structure stores the Raychaudhuri differential law but no stress tensor
  37and no Ricci-stress equality.
  38-/
  39structure MatrixRicciRaychaudhuriData where
  40  expansion : ℝ → ℝ
  41  shearSq : ℝ → ℝ
  42  ricciTensor : ℝ → Matrix (Fin 4) (Fin 4) ℝ
  43  nullProbe : ℝ → Fin 4 → ℝ
  44  ricci_symmetric :
  45    ∀ lambda, Symmetric4 (ricciTensor lambda)
  46  probe_null :
  47    ∀ lambda, MinkowskiNull (nullProbe lambda)
  48  /-- MODEL: twist-free null Raychaudhuri with explicit matrix contraction. -/
  49  law :
  50    ∀ lambda : ℝ,
  51      HasDerivAt expansion
  52        (raychaudhuriSlope (expansion lambda) (shearSq lambda)
  53          (quadContr (ricciTensor lambda) (nullProbe lambda)))
  54        lambda
  55
  56/-- Forget the matrix presentation and expose the scalar Raychaudhuri data. -/
  57def MatrixRicciRaychaudhuriData.toLocalRaychaudhuriData
  58    (D : MatrixRicciRaychaudhuriData) :
  59    LocalRaychaudhuriData where
  60  expansion := D.expansion
  61  shearSq := D.shearSq
  62  ricciNull := fun lambda =>
  63    quadContr (D.ricciTensor lambda) (D.nullProbe lambda)
  64  law := D.law
  65
  66@[simp] theorem toLocalRaychaudhuriData_ricciNull
  67    (D : MatrixRicciRaychaudhuriData) (lambda : ℝ) :
  68    D.toLocalRaychaudhuriData.ricciNull lambda =
  69      quadContr (D.ricciTensor lambda) (D.nullProbe lambda) :=
  70  rfl
  71
  72/--
  73Matrix form of the equilibrium second-area variation, obtained by definitional
  74transport of `ricciNull` rather than by storing a separate matching equality.
  75-/
  76theorem second_area_deriv_eq_neg_area_mul_quadContr
  77    (D : MatrixRicciRaychaudhuriData)
  78    (area : ℝ → ℝ)
  79    (areaLaw :
  80      ∀ lambda : ℝ,
  81        HasDerivAt area (D.expansion lambda * area lambda) lambda)
  82    (hθ : D.expansion 0 = 0)
  83    (hσ : D.shearSq 0 = 0) :
  84    deriv (deriv area) 0 =
  85      -area 0 * quadContr (D.ricciTensor 0) (D.nullProbe 0) := by
  86  let A : LocalAreaCongruenceData :=
  87    { D.toLocalRaychaudhuriData with
  88      area := area
  89      areaLaw := areaLaw }
  90  exact deriv_deriv_area_zero_eq_neg_area_mul_ricciNull A hθ hσ
  91
  92end LocalAreaRaychaudhuri
  93end Geometry
  94end Relativity
  95end IndisputableMonolith
  96