IndisputableMonolith.Gravity.ClausiusEinsteinBridge

   1import Mathlib
   2
   3/-!
   4# The algebraic Clausius-to-Einstein hinge
   5
   6This module isolates the finite-dimensional linear algebra used in Jacobson's
   7thermodynamic derivation.  Equality of two symmetric quadratic forms on every
   8Minkowski-null direction determines their difference only up to a scalar
   9multiple of the metric.  Thus an all-null local Clausius balance has the
  10algebraic shape of the Einstein equation, with the metric term left free.
  11
  12The result is deliberately independent of the repository's refuted raw
  13ledger-deficit-to-signed-hinge bridge.  It does not construct local horizons,
  14identify posted record heat with stress-energy flux, prove continuum focusing,
  15or fix the free scalar by a conservation law.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Gravity
  20namespace ClausiusEinsteinBridge
  21
  22/-- A componentwise symmetry predicate for real covariant 2-tensors in four dimensions. -/
  23def Symmetric4 (A : Matrix (Fin 4) (Fin 4) ℝ) : Prop :=
  24  ∀ i j, A i j = A j i
  25
  26/-- The `(-,+,+,+)` Minkowski metric in the standard basis. -/
  27def minkowskiEta4 : Matrix (Fin 4) (Fin 4) ℝ :=
  28  fun i j => if i = j then if i = 0 then -1 else 1 else 0
  29
  30/-- The quadratic contraction `A_{\mu nu} k^mu k^nu`. -/
  31def quadContr (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ) : ℝ :=
  32  ∑ i, ∑ j, A i j * k i * k j
  33
  34/-- Nullness for the standard `(-,+,+,+)` Minkowski metric. -/
  35def MinkowskiNull (k : Fin 4 → ℝ) : Prop :=
  36  -(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2 = 0
  37
  38/-- A four-vector with named components, used for the finite null probes below. -/
  39def vec4 (a b c d : ℝ) : Fin 4 → ℝ :=
  40  fun i => if i = 0 then a else if i = 1 then b else if i = 2 then c else d
  41
  42@[simp] lemma vec4_zero (a b c d : ℝ) : vec4 a b c d 0 = a := by
  43  simp [vec4]
  44
  45@[simp] lemma vec4_one (a b c d : ℝ) : vec4 a b c d 1 = b := by
  46  rw [vec4, if_neg (by decide), if_pos rfl]
  47
  48@[simp] lemma vec4_two (a b c d : ℝ) : vec4 a b c d 2 = c := by
  49  rw [vec4, if_neg (by decide), if_neg (by decide), if_pos rfl]
  50
  51@[simp] lemma vec4_three (a b c d : ℝ) : vec4 a b c d 3 = d := by
  52  rw [vec4, if_neg (by decide), if_neg (by decide), if_neg (by decide)]
  53
  54private lemma sum_fin_four {α : Type*} [AddCommMonoid α] (f : Fin 4 → α) :
  55    ∑ i, f i = f 0 + f 1 + f 2 + f 3 := by
  56  have hu : Finset.univ = ({0, 1, 2, 3} : Finset (Fin 4)) := by decide
  57  rw [hu]
  58  simp
  59  abel
  60
  61/-- The matrix definition of `minkowskiEta4` has the expected quadratic form. -/
  62theorem quadContr_minkowskiEta4 (k : Fin 4 → ℝ) :
  63    quadContr minkowskiEta4 k =
  64      -(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2 := by
  65  simp only [quadContr, sum_fin_four]
  66  simp [minkowskiEta4]
  67  ring
  68
  69/-- Pointwise tensor equality implies equality on every null cut. -/
  70theorem pointwise_eq_implies_null_cut_eq
  71    (A B : Matrix (Fin 4) (Fin 4) ℝ) (hAB : A = B) :
  72    ∀ k, MinkowskiNull k → quadContr A k = quadContr B k := by
  73  subst B
  74  simp
  75
  76/--
  77Null-cut equality is strictly weaker than pointwise equality: the Minkowski
  78metric and zero agree quadratically on every Minkowski-null vector.
  79-/
  80theorem null_cut_eq_not_pointwise_eq :
  81    ∃ A B : Matrix (Fin 4) (Fin 4) ℝ,
  82      Symmetric4 A ∧ Symmetric4 B ∧
  83      (∀ k, MinkowskiNull k → quadContr A k = quadContr B k) ∧
  84      A ≠ B := by
  85  refine ⟨minkowskiEta4, 0, ?_, ?_, ?_, ?_⟩
  86  · intro i j
  87    simp only [minkowskiEta4]
  88    by_cases hij : i = j
  89    · subst j
  90      simp
  91    · have hji : j ≠ i := fun h => hij h.symm
  92      simp [hij, hji]
  93  · intro i j
  94    simp
  95  · intro k hk
  96    rw [quadContr_minkowskiEta4]
  97    simpa [quadContr, MinkowskiNull] using hk
  98  · intro h
  99    have h00 := congrFun (congrFun h (0 : Fin 4)) (0 : Fin 4)
 100    norm_num [minkowskiEta4] at h00
 101
 102/--
 103Four-dimensional Lorentzian null-contraction rigidity.
 104
 105If a symmetric covariant tensor has zero quadratic contraction on every
 106Minkowski-null vector, it is a scalar multiple of the Minkowski metric.
 107-/
 108theorem null_quadratic_zero_eq_scalar_eta
 109    (D : Matrix (Fin 4) (Fin 4) ℝ)
 110    (hD : Symmetric4 D)
 111    (hnull : ∀ k, MinkowskiNull k → quadContr D k = 0) :
 112    ∃ f : ℝ, D = f • minkowskiEta4 := by
 113  have h01p := hnull (vec4 1 1 0 0) (by norm_num [MinkowskiNull])
 114  have h01m := hnull (vec4 1 (-1) 0 0) (by norm_num [MinkowskiNull])
 115  have h02p := hnull (vec4 1 0 1 0) (by norm_num [MinkowskiNull])
 116  have h02m := hnull (vec4 1 0 (-1) 0) (by norm_num [MinkowskiNull])
 117  have h03p := hnull (vec4 1 0 0 1) (by norm_num [MinkowskiNull])
 118  have h03m := hnull (vec4 1 0 0 (-1)) (by norm_num [MinkowskiNull])
 119  simp only [quadContr, sum_fin_four] at h01p h01m h02p h02m h03p h03m
 120  norm_num at h01p h01m h02p h02m h03p h03m
 121
 122  have hs01 : D 1 0 = D 0 1 := hD 1 0
 123  have hs02 : D 2 0 = D 0 2 := hD 2 0
 124  have hs03 : D 3 0 = D 0 3 := hD 3 0
 125  have hz01 : D 0 1 = 0 := by linarith
 126  have hz02 : D 0 2 = 0 := by linarith
 127  have hz03 : D 0 3 = 0 := by linarith
 128  have hd11 : D 1 1 = -D 0 0 := by linarith
 129  have hd22 : D 2 2 = -D 0 0 := by linarith
 130  have hd33 : D 3 3 = -D 0 0 := by linarith
 131
 132  have h12 := hnull (vec4 5 3 4 0) (by norm_num [MinkowskiNull])
 133  have h13 := hnull (vec4 5 3 0 4) (by norm_num [MinkowskiNull])
 134  have h23 := hnull (vec4 5 0 3 4) (by norm_num [MinkowskiNull])
 135  simp only [quadContr, sum_fin_four] at h12 h13 h23
 136  norm_num at h12 h13 h23
 137
 138  have hs10 : D 1 0 = D 0 1 := hD 1 0
 139  have hs20 : D 2 0 = D 0 2 := hD 2 0
 140  have hs30 : D 3 0 = D 0 3 := hD 3 0
 141  have hs21 : D 2 1 = D 1 2 := hD 2 1
 142  have hs31 : D 3 1 = D 1 3 := hD 3 1
 143  have hs32 : D 3 2 = D 2 3 := hD 3 2
 144  have hz12 : D 1 2 = 0 := by linarith
 145  have hz13 : D 1 3 = 0 := by linarith
 146  have hz23 : D 2 3 = 0 := by linarith
 147
 148  refine ⟨-D 0 0, ?_⟩
 149  ext i j
 150  fin_cases i <;> fin_cases j <;>
 151    simp [minkowskiEta4] <;>
 152    linarith [hD 0 1, hD 0 2, hD 0 3, hD 1 2, hD 1 3, hD 2 3]
 153
 154/--
 155Equality of symmetric quadratic contractions on every null direction
 156determines the two tensors up to a scalar metric term.
 157-/
 158theorem null_quadratic_eq_of_diff_scalar_eta
 159    (A B : Matrix (Fin 4) (Fin 4) ℝ)
 160    (hA : Symmetric4 A)
 161    (hB : Symmetric4 B)
 162    (hnull : ∀ k, MinkowskiNull k → quadContr A k = quadContr B k) :
 163    ∃ f : ℝ, A = B + f • minkowskiEta4 := by
 164  let D : Matrix (Fin 4) (Fin 4) ℝ := A - B
 165  have hD : Symmetric4 D := by
 166    intro i j
 167    simp only [D, Matrix.sub_apply]
 168    rw [hA i j, hB i j]
 169  have hDnull : ∀ k, MinkowskiNull k → quadContr D k = 0 := by
 170    intro k hk
 171    specialize hnull k hk
 172    simpa [D, quadContr, Matrix.sub_apply, sub_mul, Finset.sum_sub_distrib] using
 173      sub_eq_zero.mpr hnull
 174  obtain ⟨f, hf⟩ := null_quadratic_zero_eq_scalar_eta D hD hDnull
 175  refine ⟨f, ?_⟩
 176  ext i j
 177  have hij := congrFun (congrFun hf i) j
 178  change A i j = B i j + (f • minkowskiEta4) i j
 179  simp only [D, Matrix.sub_apply] at hij
 180  linarith
 181
 182/--
 183The algebraic Einstein-shaped consequence of local Clausius balance.
 184
 185Here "Clausius" names an assumed null-cut interface: a stress-like symmetric
 186tensor and a Ricci-like symmetric tensor have equal contractions on every
 187local null direction.  The theorem does not derive that interface from
 188thermodynamics.  Its conclusion leaves a free scalar metric term, as in
 189Jacobson's argument before conservation fixes the cosmological term.
 190-/
 191theorem einstein_equation_shaped_of_local_clausius
 192    (coupling : ℝ)
 193    (T Ric : Matrix (Fin 4) (Fin 4) ℝ)
 194    (hT : Symmetric4 T)
 195    (hRic : Symmetric4 Ric)
 196    (hClausius :
 197      ∀ k, MinkowskiNull k →
 198        quadContr (coupling • T) k = quadContr Ric k) :
 199    ∃ f : ℝ, coupling • T = Ric + f • minkowskiEta4 := by
 200  apply null_quadratic_eq_of_diff_scalar_eta
 201  · intro i j
 202    change coupling * T i j = coupling * T j i
 203    rw [hT i j]
 204  · exact hRic
 205  · exact hClausius
 206
 207end ClausiusEinsteinBridge
 208end Gravity
 209end IndisputableMonolith
 210