Encyclopedia Gravity Gravity Clausius Einstein Bridge Null Quadratic Zero Eq Scalar Eta

ARTICLE 3 claims 3 theorems

Gravity Clausius Einstein Bridge Null Quadratic Zero Eq Scalar Eta

A purely algebraic fact about four-dimensional spacetime: if a symmetric tensor vanishes on every lightlike direction, it must be a multiple of the metric itself.

Verify this page

The null rigidity theorem

In four-dimensional spacetime with the standard (-,+,+,+) metric, consider a symmetric 4x4 tensor. The theorem states that if its quadratic contraction A(k,k) equals zero for every lightlike (null) vector k, then the tensor must be a scalar multiple of the Minkowski metric η. This is a rigidity result: the condition of vanishing on all null directions is so strong that it pins the tensor down to a single family, parameterized by one real number.

The proof is finite-dimensional linear algebra. The quadratic contraction is Aμνkμkν, and the null condition is -k₀² + k₁² + k₂² + k₃² = 0. The theorem is proved in the framework's machine-checked library of formal theorems, with no additional axioms. It is a statement about matrices and quadratic forms, not about physics.

In Recognition Science, this algebraic fact serves as the hinge in a formal reconstruction of Jacobson's thermodynamic derivation of Einstein's equation. The framework models a local Clausius balance as an assumed null-cut interface: a stress-like symmetric tensor T and a Ricci-like symmetric tensor Ric have equal contractions on every local null direction. The theorem then shows that this equality forces the two tensors to differ only by a scalar multiple of the metric: coupling·T = Ric + f·η. This is the algebraic shape of the Einstein equation, with the metric term left free, exactly as in Jacobson's argument before a conservation law fixes the cosmological term.

The theorem is deliberately independent of an earlier, refuted bridge in the repository. It does not construct local horizons, identify posted record heat with stress-energy flux, prove continuum focusing, or fix the free scalar by a conservation law. The result is a clean algebraic lemma: equality of two symmetric quadratic forms on every null direction determines their difference only up to a scalar metric term.

What this means for the reader: the theorem gives a precise, checkable statement about the linear algebra of spacetime. It shows that a certain kind of null-direction data, if it matches everywhere, leaves exactly one free parameter: the cosmological term. The physical derivation of that term, and the bridge from thermodynamics to the null-cut interface, remain open targets.

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 theorem does not derive the Clausius interface from thermodynamics. The theorem does not construct local horizons or prove continuum focusing. The theorem does not fix the free scalar by a conservation law.

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