IndisputableMonolith.Gravity.RSNullFieldEquation

   1import IndisputableMonolith.Constants
   2import IndisputableMonolith.Gravity.ClausiusEinsteinBridge
   3
   4/-!
   5# RS null scalar reduction from an assumed matrix source
   6
   7This module proves the algebraic step from an independently supplied
   8Einstein-shaped matrix equation to its null-contracted scalar equation.
   9
  10If
  11
  12`κ T = Ric + f η`
  13
  14and `k` is Minkowski-null, then the metric term vanishes and
  15
  16`Ric(k,k) = κ T(k,k)`.
  17
  18The RS specialization selects the coupling parameter
  19`κ = kappa_einstein`.
  20
  21Honesty tags:
  22
  23* THEOREM: all matrix and null-contraction algebra below.
  24* OPEN / external input: inhabiting `EinsteinShapedSource` from the RS action.
  25* This module does not construct a horizon patch, identify cut channels with
  26  spacetime covectors, or derive a sourced field equation from the ledger.
  27* The file name is retained for import compatibility; every public declaration
  28  is named as a conditional reduction rather than a derived field equation.
  29-/
  30
  31noncomputable section
  32
  33namespace IndisputableMonolith
  34namespace Gravity
  35namespace RSNullFieldReduction
  36
  37open ClausiusEinsteinBridge
  38open IndisputableMonolith.Constants
  39
  40/-- Quadratic contraction is additive in its matrix argument. -/
  41theorem quadContr_add
  42    (A B : Matrix (Fin 4) (Fin 4) ℝ)
  43    (k : Fin 4 → ℝ) :
  44    quadContr (A + B) k = quadContr A k + quadContr B k := by
  45  unfold quadContr
  46  simp only [Matrix.add_apply, add_mul, Finset.sum_add_distrib]
  47
  48/-- Quadratic contraction is homogeneous in its matrix argument. -/
  49theorem quadContr_smul
  50    (c : ℝ) (A : Matrix (Fin 4) (Fin 4) ℝ)
  51    (k : Fin 4 → ℝ) :
  52    quadContr (c • A) k = c * quadContr A k := by
  53  unfold quadContr
  54  simp only [Matrix.smul_apply, smul_eq_mul]
  55  calc
  56    (∑ i, ∑ j, c * A i j * k i * k j)
  57        = ∑ i, ∑ j, c * (A i j * k i * k j) := by
  58          refine Finset.sum_congr rfl fun i _ =>
  59            Finset.sum_congr rfl fun j _ => by ring
  60    _ = ∑ i, c * ∑ j, A i j * k i * k j := by
  61          refine Finset.sum_congr rfl fun i _ =>
  62            (Finset.mul_sum _ _ _).symm
  63    _ = c * ∑ i, ∑ j, A i j * k i * k j :=
  64      (Finset.mul_sum _ _ _).symm
  65
  66/-- Every scalar Minkowski metric term vanishes on a null probe. -/
  67theorem quadContr_metric_term_eq_zero
  68    (f : ℝ) (k : Fin 4 → ℝ)
  69    (hk : MinkowskiNull k) :
  70    quadContr (f • minkowskiEta4) k = 0 := by
  71  rw [quadContr_smul, quadContr_minkowskiEta4]
  72  rw [show -(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2 = 0 by
  73    simpa [MinkowskiNull] using hk]
  74  ring
  75
  76/--
  77An Einstein-shaped sourced equation at the matrix layer.  This is an explicit
  78input interface, not an in-tree derivation from the RS action.
  79-/
  80def EinsteinShapedSource
  81    (coupling : ℝ)
  82    (T Ric : Matrix (Fin 4) (Fin 4) ℝ) : Prop :=
  83  ∃ f : ℝ, coupling • T = Ric + f • minkowskiEta4
  84
  85/--
  86Null reduction of one Einstein-shaped equation.  The undetermined scalar
  87metric term disappears on every Minkowski-null direction.
  88-/
  89theorem null_scalar_of_einstein_shaped
  90    (coupling : ℝ)
  91    (T Ric : Matrix (Fin 4) (Fin 4) ℝ)
  92    (f : ℝ)
  93    (h : coupling • T = Ric + f • minkowskiEta4)
  94    (k : Fin 4 → ℝ)
  95    (hk : MinkowskiNull k) :
  96    quadContr Ric k = coupling * quadContr T k := by
  97  have hcontract := congrArg (fun A => quadContr A k) h
  98  change quadContr (coupling • T) k =
  99    quadContr (Ric + f • minkowskiEta4) k at hcontract
 100  rw [quadContr_smul, quadContr_add,
 101    quadContr_metric_term_eq_zero f k hk, add_zero] at hcontract
 102  exact hcontract.symm
 103
 104/-- Bundled null reduction from `EinsteinShapedSource`. -/
 105theorem null_scalar_of_source
 106    {coupling : ℝ}
 107    {T Ric : Matrix (Fin 4) (Fin 4) ℝ}
 108    (h : EinsteinShapedSource coupling T Ric) :
 109    ∀ k, MinkowskiNull k →
 110      quadContr Ric k = coupling * quadContr T k := by
 111  obtain ⟨f, hf⟩ := h
 112  intro k hk
 113  exact null_scalar_of_einstein_shaped coupling T Ric f hf k hk
 114
 115/--
 116RS-normalized specialization: an independently inhabited Einstein-shaped
 117source with the RS coupling yields its null-contracted scalar form.
 118-/
 119theorem rs_null_scalar_of_source
 120    {T Ric : Matrix (Fin 4) (Fin 4) ℝ}
 121    (h : EinsteinShapedSource kappa_einstein T Ric) :
 122    ∀ k, MinkowskiNull k →
 123      quadContr Ric k = kappa_einstein * quadContr T k :=
 124  null_scalar_of_source h
 125
 126/--
 127Componentwise source equations can be transported into the matrix interface.
 128-/
 129theorem source_of_componentwise
 130    (coupling f : ℝ)
 131    (T Ric : Matrix (Fin 4) (Fin 4) ℝ)
 132    (h : ∀ i j,
 133      coupling * T i j = Ric i j + f * minkowskiEta4 i j) :
 134    EinsteinShapedSource coupling T Ric := by
 135  refine ⟨f, ?_⟩
 136  ext i j
 137  simpa [Matrix.smul_apply, smul_eq_mul] using h i j
 138
 139/--
 140The null equation does not recover the scalar metric term: adding a nonzero
 141multiple of `η` changes the matrix while preserving every null contraction.
 142-/
 143theorem scalar_metric_term_is_null_invisible :
 144    ∃ D : Matrix (Fin 4) (Fin 4) ℝ,
 145      D ≠ 0 ∧
 146      ∀ k, MinkowskiNull k → quadContr D k = 0 := by
 147  refine ⟨minkowskiEta4, ?_, ?_⟩
 148  · intro h
 149    have h00 := congrFun (congrFun h (0 : Fin 4)) (0 : Fin 4)
 150    norm_num [minkowskiEta4] at h00
 151  · intro k hk
 152    simpa using quadContr_metric_term_eq_zero 1 k hk
 153
 154/-- Certificate for the matrix-level RS null reduction. -/
 155structure RSNullFieldReductionCert : Prop where
 156  metric_term_vanishes :
 157    ∀ (f : ℝ) (k : Fin 4 → ℝ), MinkowskiNull k →
 158      quadContr (f • minkowskiEta4) k = 0
 159  source_reduces :
 160    ∀ {T Ric : Matrix (Fin 4) (Fin 4) ℝ},
 161      EinsteinShapedSource kappa_einstein T Ric →
 162      ∀ k, MinkowskiNull k →
 163        quadContr Ric k = kappa_einstein * quadContr T k
 164  metric_term_not_recovered :
 165    ∃ D : Matrix (Fin 4) (Fin 4) ℝ,
 166      D ≠ 0 ∧
 167      ∀ k, MinkowskiNull k → quadContr D k = 0
 168
 169theorem rsNullFieldReductionCert : RSNullFieldReductionCert where
 170  metric_term_vanishes := quadContr_metric_term_eq_zero
 171  source_reduces := rs_null_scalar_of_source
 172  metric_term_not_recovered := scalar_metric_term_is_null_invisible
 173
 174end RSNullFieldReduction
 175end Gravity
 176end IndisputableMonolith
 177