Gravity Clausius Einstein Bridge Quad Contr Minkowski Eta4

The null-cut identity

The declaration quadContr_minkowskiEta4 is a theorem in the machine-checked library of formal theorems. It states that the quadratic contraction of the standard Minkowski metric with any four-vector equals the familiar null condition: -(k0)^2 + (k1)^2 + (k2)^2 + (k3)^2. In plain words, the metric's quadratic form is exactly the expression whose vanishing defines a lightlike direction. The proof is a direct computation from the matrix definition of the metric, using the fact that a sum over four indices splits into four terms.

This identity is the hinge of a larger algebraic argument. The framework's library proves that if two symmetric tensors have equal quadratic contractions on every null direction, then their difference is a scalar multiple of the Minkowski metric. That rigidity result, tagged as a theorem, is what gives the Clausius-to-Einstein bridge its shape. The bridge assumes a local Clausius balance: a stress-like tensor and a Ricci-like tensor have equal contractions on every null direction. The conclusion is that the stress-like tensor equals the Ricci-like tensor plus a free scalar metric term, which is the algebraic form of Einstein's equation before a conservation law fixes the cosmological term.

The theorem quadContr_minkowskiEta4 itself does not construct local horizons, identify heat with stress-energy flux, prove continuum focusing, or fix the free scalar. It is deliberately independent of the repository's refuted raw ledger-deficit-to-signed-hinge bridge. The declaration is a lemma about quadratic forms, not a physical derivation. Its role is to make the null condition explicit in coordinates, so that the rigidity theorem can apply to it.

What the declaration establishes is the algebraic seed: the metric's quadratic form is the null condition. What it does not establish is any thermodynamic content. The bridge's name is inherited from Jacobson's argument, but the theorem does not derive the null-cut interface from thermodynamics. It takes that interface as an assumption and shows what algebraic shape follows. The free scalar metric term remains, exactly as in Jacobson's argument before conservation fixes it.

/-- The matrix definition of `minkowskiEta4` has the expected quadratic form. -/
theorem quadContr_minkowskiEta4 (k : Fin 4 → ℝ) :
    quadContr minkowskiEta4 k =
      -(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2 := by
  simp only [quadContr, sum_fin_four]
  simp [minkowskiEta4]
  ring

/--
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 theorem does not construct local horizons or prove continuum focusing. The theorem does not identify posted record heat with stress-energy flux. The theorem does not fix the free scalar metric term 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: