Encyclopedia Gravity Gravity Clausius Einstein Bridge Sum Fin Four

ARTICLE 4 claims 4 theorems

Gravity Clausius Einstein Bridge Sum Fin Four

A small lemma about four-term sums anchors a larger claim: that a thermodynamic balance on lightlike directions has the algebraic shape of Einstein's equation.

Verify this page

The algebraic hinge

In the framework's machine-checked library of formal theorems, the declaration sum_fin_four is a modest computational fact: a sum over four indices equals the sum of its four named components. It is the sort of lemma that appears in every formal development, a routine unpacking of a finite sum. Its interest lies entirely in what it enables.

The library uses it to prove a rigidity result about the Minkowski metric, the standard spacetime metric with signature (-,+,+,+). If a symmetric tensor has zero quadratic contraction on every lightlike (null) direction, then that tensor must be a scalar multiple of the metric itself. The proof of this rigidity theorem, null_quadratic_zero_eq_scalar_eta, relies on sum_fin_four to expand the contraction over the four components. A consequence follows: if two symmetric tensors agree on every null direction, their difference is a scalar multiple of the metric. This is the algebraic heart of the bridge.

The framework's library then labels the payoff: einstein_equation_shaped_of_local_clausius. It assumes a Clausius-type balance, meaning a stress-like tensor and a Ricci-like tensor have equal contractions on every local null direction. The theorem concludes that the coupling times the stress tensor equals the Ricci tensor plus a free scalar metric term. That is the algebraic shape of the Einstein equation, with the cosmological term left undetermined. The proof is a direct application of the null-direction rigidity lemma.

In Recognition Science, this is the algebraic hinge from a thermodynamic balance to general relativity's field equation. The framework models the Einstein equation's form as a consequence of a null-cut interface, not as a postulate. The free scalar term is exactly the freedom Jacobson's argument leaves before a conservation law fixes the cosmological constant. The framework's contribution is showing that this algebraic shape is forced by the null-direction rigidity alone.

What the declaration does not claim is as important as what it proves. sum_fin_four does not construct local horizons, identify heat flux with stress-energy, prove continuum focusing, or fix the free scalar by conservation. The bridge from thermodynamics to gravity is not derived; only its algebraic skeleton is shown to be consistent. The physical recognition-to-linking bridge remains open. The library is explicit: this result is independent of a refuted raw ledger-deficit bridge, and it does not establish the physical interface from thermodynamics.

THEOREM sum_fin_four · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean
sum_fin_four · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean:54 
private lemma sum_fin_four {α : Type*} [AddCommMonoid α] (f : Fin 4 → α) :
    ∑ i, f i = f 0 + f 1 + f 2 + f 3 := by
  have hu : Finset.univ = ({0, 1, 2, 3} : Finset (Fin 4)) := by decide
  rw [hu]
  simp
  abel
THEOREM null_quadratic_zero_eq_scalar_eta · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean
null_quadratic_zero_eq_scalar_eta · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean:102 
/--
Four-dimensional Lorentzian null-contraction rigidity.

If a symmetric covariant tensor has zero quadratic contraction on every
Minkowski-null vector, it is a scalar multiple of the Minkowski metric.
-/
theorem null_quadratic_zero_eq_scalar_eta
    (D : Matrix (Fin 4) (Fin 4) ℝ)
    (hD : Symmetric4 D)
    (hnull : ∀ k, MinkowskiNull k → quadContr D k = 0) :
    ∃ f : ℝ, D = f • minkowskiEta4 := by
  have h01p := hnull (vec4 1 1 0 0) (by norm_num [MinkowskiNull])
  have h01m := hnull (vec4 1 (-1) 0 0) (by norm_num [MinkowskiNull])
  have h02p := hnull (vec4 1 0 1 0) (by norm_num [MinkowskiNull])
  have h02m := hnull (vec4 1 0 (-1) 0) (by norm_num [MinkowskiNull])
  have h03p := hnull (vec4 1 0 0 1) (by norm_num [MinkowskiNull])
  have h03m := hnull (vec4 1 0 0 (-1)) (by norm_num [MinkowskiNull])
  simp only [quadContr, sum_fin_four] at h01p h01m h02p h02m h03p h03m
  norm_num at h01p h01m h02p h02m h03p h03m

  have hs01 : D 1 0 = D 0 1 := hD 1 0
  have hs02 : D 2 0 = D 0 2 := hD 2 0
  have hs03 : D 3 0 = D 0 3 := hD 3 0
  have hz01 : D 0 1 = 0 := by linarith
  have hz02 : D 0 2 = 0 := by linarith
  have hz03 : D 0 3 = 0 := by linarith
  have hd11 : D 1 1 = -D 0 0 := by linarith
  have hd22 : D 2 2 = -D 0 0 := by linarith
  have hd33 : D 3 3 = -D 0 0 := by linarith

  have h12 := hnull (vec4 5 3 4 0) (by norm_num [MinkowskiNull])
  have h13 := hnull (vec4 5 3 0 4) (by norm_num [MinkowskiNull])
  have h23 := hnull (vec4 5 0 3 4) (by norm_num [MinkowskiNull])
  simp only [quadContr, sum_fin_four] at h12 h13 h23
  norm_num at h12 h13 h23

  have hs10 : D 1 0 = D 0 1 := hD 1 0
  have hs20 : D 2 0 = D 0 2 := hD 2 0
  have hs30 : D 3 0 = D 0 3 := hD 3 0
  have hs21 : D 2 1 = D 1 2 := hD 2 1
  have hs31 : D 3 1 = D 1 3 := hD 3 1
  have hs32 : D 3 2 = D 2 3 := hD 3 2
  have hz12 : D 1 2 = 0 := by linarith
  have hz13 : D 1 3 = 0 := by linarith
  have hz23 : D 2 3 = 0 := by linarith

  refine ⟨-D 0 0, ?_⟩
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [minkowskiEta4] <;>
    linarith [hD 0 1, hD 0 2, hD 0 3, hD 1 2, hD 1 3, hD 2 3]
THEOREM null_quadratic_eq_of_diff_scalar_eta · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean
null_quadratic_eq_of_diff_scalar_eta · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean:154 
/--
Equality of symmetric quadratic contractions on every null direction
determines the two tensors up to a scalar metric term.
-/
theorem null_quadratic_eq_of_diff_scalar_eta
    (A B : Matrix (Fin 4) (Fin 4) ℝ)
    (hA : Symmetric4 A)
    (hB : Symmetric4 B)
    (hnull : ∀ k, MinkowskiNull k → quadContr A k = quadContr B k) :
    ∃ f : ℝ, A = B + f • minkowskiEta4 := by
  let D : Matrix (Fin 4) (Fin 4) ℝ := A - B
  have hD : Symmetric4 D := by
    intro i j
    simp only [D, Matrix.sub_apply]
    rw [hA i j, hB i j]
  have hDnull : ∀ k, MinkowskiNull k → quadContr D k = 0 := by
    intro k hk
    specialize hnull k hk
    simpa [D, quadContr, Matrix.sub_apply, sub_mul, Finset.sum_sub_distrib] using
      sub_eq_zero.mpr hnull
  obtain ⟨f, hf⟩ := null_quadratic_zero_eq_scalar_eta D hD hDnull
  refine ⟨f, ?_⟩
  ext i j
  have hij := congrFun (congrFun hf i) j
  change A i j = B i j + (f • minkowskiEta4) i j
  simp only [D, Matrix.sub_apply] at hij
  linarith
THEOREM einstein_equation_shaped_of_local_clausius · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean
einstein_equation_shaped_of_local_clausius · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean:182 
/--
The algebraic Einstein-shaped consequence of local Clausius balance.

Here "Clausius" names an assumed null-cut interface: a stress-like symmetric
tensor and a Ricci-like symmetric tensor have equal contractions on every
local null direction.  The theorem does not derive that interface from
thermodynamics.  Its conclusion leaves a free scalar metric term, as in
Jacobson's argument before conservation fixes the cosmological term.
-/
theorem einstein_equation_shaped_of_local_clausius
    (coupling : ℝ)
    (T Ric : Matrix (Fin 4) (Fin 4) ℝ)
    (hT : Symmetric4 T)
    (hRic : Symmetric4 Ric)
    (hClausius :
      ∀ k, MinkowskiNull k →
        quadContr (coupling • T) k = quadContr Ric k) :
    ∃ f : ℝ, coupling • T = Ric + f • minkowskiEta4 := by
  apply null_quadratic_eq_of_diff_scalar_eta
  · intro i j
    change coupling * T i j = coupling * T j i
    rw [hT i j]
  · exact hRic
  · exact hClausius

What this page does not claim

The declaration does not construct local horizons or identify posted record heat with stress-energy flux. It does not prove continuum focusing or fix the free scalar by a conservation law. It is independent of the repository's refuted raw ledger-deficit-to-signed-hinge bridge.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND