Gravity Clausius Einstein Bridge Null Cut Eq Not Pointwise Eq

The null-cut ambiguity

In the geometry of special relativity, a null direction is a path along which light itself would travel, a trajectory with zero spacetime interval. The framework's library, a machine-checked collection of formal theorems, proves a precise statement about these directions: two symmetric four-dimensional tensors can agree on every null direction and still be different tensors. The theorem, named null_cut_eq_not_pointwise_eq, demonstrates this with an explicit example: the Minkowski metric and the zero tensor both give a zero quadratic contraction on every null vector, yet they are plainly not the same object.

This fact is not a flaw but a feature with a physical payoff. A companion theorem in the same library shows what the ambiguity is limited to: if two symmetric tensors agree on every null direction, their difference must be a scalar multiple of the Minkowski metric. In other words, the null directions determine a tensor completely except for one free number, the coefficient of the metric term. This is the algebraic shape of Einstein's equation, where the metric term is left free, exactly as in Jacobson's thermodynamic derivation of general relativity before a conservation law fixes the cosmological constant.

The theorem is deliberately narrow. It does not construct local horizons, identify a recorded heat flow with stress-energy flux, prove that spacetime focusing occurs, or fix the free scalar by a conservation law. It is a statement about finite-dimensional linear algebra, not a derivation of general relativity from thermodynamics. The library's docstring is explicit: the result is independent of the repository's refuted raw ledger-deficit-to-signed-hinge bridge, and it assumes the Clausius-like interface rather than deriving it.

What the theorem does establish is a clean, checkable hinge: if you assume a local Clausius balance, where a stress-like and a Ricci-like tensor have equal contractions on every null direction, then you are forced into the algebraic form of the Einstein equation, with the metric term free. The framework proves this shape rigorously, and the proof is axiom-clean, resting only on the standard postulates of the ambient type theory. The physical bridge from recognition events to that null-cut interface remains open; the algebra is not.

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

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

This theorem does not derive general relativity from thermodynamics. It does not construct local horizons or prove spacetime focusing. It does not identify a recorded heat flow with stress-energy flux.

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: