Encyclopedia Gravity Gravity Clausius Einstein Bridge

ARTICLE 3 claims 3 theorems

Gravity Clausius Einstein Bridge

A theorem in the framework's machine-checked library shows that a thermodynamic-style balance condition has the algebraic shape of Einstein's equation.

Verify this page

The algebraic hinge

The gravity Clausius-Einstein bridge is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It isolates a piece of linear algebra that appears in a thermodynamic derivation of gravity, the one associated with physicist Ted Jacobson in 1995. The classical idea is that gravity might not be a fundamental force but an emergent phenomenon, like pressure or temperature, arising from a more basic statistical account of spacetime. In that picture, a balance of something like heat across a local light cone leads to the Einstein equation, the field equation of general relativity.

The framework's module does not attempt the full physical derivation. It proves a narrower, purely algebraic claim. In four-dimensional spacetime with the standard (-,+,+,+) Minkowski metric, take two symmetric tensors: one standing in for stress-energy, one for the Ricci curvature, which encodes how spacetime bends. Suppose their quadratic contractions agree on every null direction, meaning every direction a light ray could travel. The theorem, named einstein_equation_shaped_of_local_clausius, proves that the stress-like tensor must equal the Ricci-like tensor plus a scalar multiple of the metric. That is exactly the shape of the Einstein equation, with the free scalar term left undetermined, just as in Jacobson's argument before a conservation law fixes the cosmological constant.

The result rests on a rigidity fact about four-dimensional Lorentzian geometry, also proved in the module. If a symmetric tensor has zero quadratic contraction on every Minkowski-null vector, it must be a scalar multiple of the metric. This is what forces the difference between the two tensors to be pure metric. The module proves this in the theorem null_quadratic_zero_eq_scalar_eta, and derives the Einstein-shaped conclusion as a corollary.

The module is deliberately narrow. Its docstring states plainly that it does not construct local horizons, does not identify posted record heat with stress-energy flux, and does not prove continuum focusing or fix the free scalar by a conservation law. The bridge is algebraic only: it shows that an all-null local Clausius balance has the Einstein shape, nothing more. The physical recognition-to-linking bridge, the step that would connect the framework's discrete ledger to actual spacetime geometry, remains open.

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 module does not prove that gravity emerges from thermodynamics in the physical sense. The module does not construct local horizons or prove continuum focusing. The module does not fix the cosmological constant or the free scalar term.

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