Gravity Clausius Einstein Bridge Minkowski Null

The algebraic hinge

In the geometry of special relativity, a null vector is a four-vector that points along a possible path of light: its squared length, measured with the Minkowski metric, is exactly zero. The declaration MinkowskiNull is the formal definition of that condition in four dimensions. It states that for a vector with components (a, b, c, d), the expression −a² + b² + c² + d² equals zero. This is the standard (−,+,+,+) metric of special relativity, written in coordinates where time carries a minus sign and the three space directions carry plus signs.

The declaration is a definition, not a theorem. Its content is the condition itself. The theorems that use it are where the substance lies. The central result, proved in the machine-checked library of formal theorems, is a rigidity fact: if two symmetric tensors agree when contracted on every null direction, then they differ only by a scalar multiple of the metric. In symbols, if A and B are symmetric four-by-four matrices and their quadratic contractions match on every null vector, then A = B + f·η for some real number f, where η is the Minkowski metric. A symmetric tensor here is simply a matrix whose entry in row i and column j equals the entry in row j and column i.

This algebraic fact carries a physical echo. In Jacobson's thermodynamic derivation of gravity, one assumes that a local Clausius balance holds: a stress-like tensor and a Ricci-like tensor have equal contractions on every local null direction. The theorem einstein_equation_shaped_of_local_clausius shows that this assumption forces the two tensors to be equal up to a free scalar metric term. That is the algebraic shape of the Einstein equation, with the metric term left undetermined. The declaration MinkowskiNull is the hinge: it defines the null directions on which the balance is required to hold.

What the declaration does not claim is as important as what it proves. 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 deliberately independent of the repository's refuted raw ledger-deficit-to-signed-hinge bridge. In Recognition Science, the ledger, a discrete record of recognition events, does not enter this theorem. The bridge from thermodynamics to the Einstein equation remains open; this declaration isolates only the finite-dimensional linear algebra that makes the shape possible.

/-- Nullness for the standard `(-,+,+,+)` Minkowski metric. -/
def MinkowskiNull (k : Fin 4 → ℝ) : Prop :=
  -(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2 = 0

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

/--
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 derive the Clausius balance from thermodynamics. The declaration does not construct local horizons or prove continuum focusing. The declaration 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: