pointwise_eq_implies_null_cut_eq
plain-language theorem explainer
Pointwise equality of two real 4×4 matrices implies their quadratic contractions agree on every Minkowski-null four-vector. Cited as the trivial direction in the algebraic Clausius–Einstein hinge (Jacobson-style null-cut comparison). Proof is substitution of the matrix equality followed by simplification.
Claim. Let $A,B$ be real $4\times 4$ matrices with $A=B$. Then for every four-vector $k\in\mathbb{R}^4$ that is null for the standard Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$ (i.e. $-k_0^2+k_1^2+k_2^2+k_3^2=0$), the quadratic contractions agree: $A_{\mu\nu}k^\mu k^\nu=B_{\mu\nu}k^\mu k^\nu$.
background
The module isolates the finite-dimensional linear algebra behind Jacobson's thermodynamic derivation of the Einstein equation. Equality of two symmetric quadratic forms on every Minkowski-null direction fixes their difference only up to a scalar multiple of the metric, so an all-null local Clausius balance has the algebraic shape of Einstein's equation with the metric term free.
MinkowskiNull k is the predicate $-(k_0)^2+(k_1)^2+(k_2)^2+(k_3)^2=0$ for the standard $(-,+,+,+)$ metric. The quadratic contraction quadContr A k is the scalar $A_{\mu\nu}k^\mu k^\nu$ used as the null-cut probe. The module deliberately stays independent of continuum horizons, stress-energy identification, and conservation-law fixing of the free scalar.
proof idea
Term/tactic proof in two steps: substitute $B$ by $A$ from the hypothesis $A=B$, then simplify. No external lemmas are required; the goal reduces to reflexivity of equality of the same contraction on both sides.
why it matters
This is the easy inclusion in the Clausius–Einstein algebraic hinge: pointwise tensor equality is strictly stronger than agreement of null cuts. The companion observation in the module is that null-cut equality is weaker (the Minkowski metric and the zero tensor agree on every null vector), which is exactly why the Einstein equation retains a free multiple of $g_{\mu\nu}$.
No downstream theorems currently depend on it (used_by is empty), so it sits as a local lemma clearing the trivial direction before the nontrivial characterization of the null-cut kernel. It does not touch the T0–T8 forcing chain, RCL, or the phi-ladder mass formula; it is pure 4D Minkowski linear algebra supporting the gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.