Encyclopedia Gravity Gravity Clausius Einstein Bridge Null Quadratic Eq Of Diff Scalar Eta

ARTICLE 3 claims 3 theorems

Gravity Clausius Einstein Bridge Null Quadratic Eq Of Diff Scalar Eta

A theorem about symmetric tensors shows when two objects that agree on light-like directions must be the same up to a metric term, echoing Einstein's equation.

Verify this page

The algebraic hinge

In four-dimensional spacetime, the Minkowski metric η has signature (-,+,+,+). A vector k is called null, or light-like, when its squared length η(k,k) = -(k₀)² + (k₁)² + (k₂)² + (k₃)² equals zero. Light rays travel along null directions. For any symmetric 4x4 tensor A, its quadratic contraction is the number A(k,k) = Σ Aμν kμ kν. The theorem null_quadratic_eq_of_diff_scalar_eta states: if two symmetric tensors A and B have equal quadratic contractions on every null direction, then their difference is a scalar multiple of the Minkowski metric. In symbols, A = B + fη for some real number f. This is a rigidity result in linear algebra.

The proof is a finite computation. The theorem first shows that if a symmetric tensor D has zero contraction on every null vector, then D must be a scalar multiple of the metric. This is the lemma null_quadratic_zero_eq_scalar_eta. Applying it to the difference A - B gives the result. The proof uses only the definitions of symmetry, the metric, and contraction, and it is verified in a machine-checked library of formal theorems. The ambient theory supplies the real numbers and matrix arithmetic.

The result matters because it isolates the algebraic shape of a famous argument. In 1995, Ted Jacobson derived Einstein's field equation from a thermodynamic assumption: that spacetime horizons obey a Clausius relation, where heat flow is proportional to area change. His derivation passes through a step where a stress-like tensor and a Ricci-like tensor have equal contractions on every local null direction. The present theorem shows that this equality, by itself, forces the two tensors to agree up to a scalar metric term. That is exactly the form of Einstein's equation, Rμν - (1/2)Rgμν + Λgμν = (8πG/c⁴)Tμν, before the cosmological constant Λ is fixed by a conservation law.

In Recognition Science, this theorem is called the algebraic Clausius-to-Einstein hinge. The framework models the physical situation as a ledger of recognition events, and it uses this linear algebra to show that a local Clausius balance has the algebraic shape of the Einstein equation. The framework's library proves the theorem cleanly, with no additional axioms beyond the standard logical ones. The free scalar f in the conclusion corresponds to the undetermined cosmological term in Jacobson's argument.

The theorem does not do the physics. It does not construct local horizons, identify heat with stress-energy flux, prove that spacetime focusing occurs, or fix the free scalar by a conservation law. It is a statement about matrices and null vectors, not about thermodynamics or gravity. The bridge from a ledger of events to a null-cut interface remains open. What the theorem establishes is narrow and precise: the algebraic consequence of an assumed equality on light-like directions.

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 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

What this page does not claim

The theorem does not derive the Clausius interface from thermodynamics. The theorem does not construct local horizons or prove focusing. The theorem does not fix the value of the cosmological constant.

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