Encyclopedia Gravity Gravity Clausius Einstein Bridge Pointwise Eq Implies Null Cut Eq

ARTICLE 4 claims 4 theorems

Gravity Clausius Einstein Bridge Pointwise Eq Implies Null Cut Eq

A theorem in the framework's library shows that if two tensors match at every point, they also match on every lightlike slice, a small but precise step toward deriving Einstein's equation from thermodynamics.

Verify this page

The null-cut theorem

In the mathematics of spacetime, a tensor is a grid of numbers that describes a physical quantity at each point. A symmetric tensor, one whose grid reads the same when its two indices are swapped, can represent stress, energy, or curvature. The theorem named pointwise_eq_implies_null_cut_eq concerns two such symmetric tensors, call them A and B, in four-dimensional spacetime with the standard Minkowski metric of signature (-,+,+,+).

The statement is simple: if A and B are equal at every point of spacetime, then their quadratic contractions agree on every Minkowski-null vector. A null vector is a direction along which light travels, where the spacetime interval vanishes. The quadratic contraction is the number you get by sandwiching the tensor between two copies of the vector, written in symbols as Aμνkμkν. If the tensors are identical everywhere, this contraction must obviously match on every null direction; the theorem merely records that fact in the framework's machine-checked library of formal theorems.

The theorem's companion result shows why this direction is worth stating. The library also proves that equality on every null cut is strictly weaker than pointwise equality: the Minkowski metric and the zero tensor agree quadratically on every null vector, yet they are different tensors. A further theorem, null_quadratic_zero_eq_scalar_eta, sharpens this: if a symmetric tensor has zero contraction on every null vector, it must be a scalar multiple of the Minkowski metric. From there, equality of contractions on all null directions forces the two tensors to differ only by a scalar metric term, which is the algebraic shape of the Einstein equation before conservation fixes the cosmological term.

In Recognition Science, this chain of linear algebra supports a labeled bridge: if a stress-like tensor and a Ricci-like tensor have equal contractions on every local null direction, a local Clausius balance takes the form of Einstein's equation with a free scalar metric term. The framework explicitly does not claim that this bridge constructs local horizons, identifies posted record heat with stress-energy flux, proves continuum focusing, or fixes the free scalar by a conservation law. The theorem is a finite-dimensional algebraic hinge, not a derivation of general relativity from thermodynamics.

THEOREM pointwise_eq_implies_null_cut_eq · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean
pointwise_eq_implies_null_cut_eq · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean:69 
/-- Pointwise tensor equality implies equality on every null cut. -/
theorem pointwise_eq_implies_null_cut_eq
    (A B : Matrix (Fin 4) (Fin 4) ℝ) (hAB : A = B) :
    ∀ k, MinkowskiNull k → quadContr A k = quadContr B k := by
  subst B
  simp
THEOREM null_cut_eq_not_pointwise_eq · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean
null_cut_eq_not_pointwise_eq · IndisputableMonolith/Gravity/ClausiusEinsteinBridge.lean:76 
/--
Null-cut equality is strictly weaker than pointwise equality: the Minkowski
metric and zero agree quadratically on every Minkowski-null vector.
-/
theorem null_cut_eq_not_pointwise_eq :
    ∃ A B : Matrix (Fin 4) (Fin 4) ℝ,
      Symmetric4 A ∧ Symmetric4 B ∧
      (∀ k, MinkowskiNull k → quadContr A k = quadContr B k) ∧
      A ≠ B := by
  refine ⟨minkowskiEta4, 0, ?_, ?_, ?_, ?_⟩
  · intro i j
    simp only [minkowskiEta4]
    by_cases hij : i = j
    · subst j
      simp
    · have hji : j ≠ i := fun h => hij h.symm
      simp [hij, hji]
  · intro i j
    simp
  · intro k hk
    rw [quadContr_minkowskiEta4]
    simpa [quadContr, MinkowskiNull] using hk
  · intro h
    have h00 := congrFun (congrFun h (0 : Fin 4)) (0 : Fin 4)
    norm_num [minkowskiEta4] at h00
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 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 construct local horizons or identify posted record heat with stress-energy flux. The theorem does not prove continuum focusing or fix the free scalar by a conservation law. The theorem does not derive general relativity from thermodynamics; it only isolates a finite-dimensional algebraic hinge.

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