null_cut_eq_not_pointwise_eq
plain-language theorem explainer
Null-cut equality of symmetric 4×4 tensors is strictly weaker than pointwise equality: the Minkowski metric and the zero tensor share the same quadratic contraction on every Minkowski-null vector, yet are distinct. Anyone working the algebraic Clausius–Einstein hinge needs this separation before claiming rigidity. The proof is an explicit counterexample, not an abstract existence argument.
Claim. There exist symmetric real $4\times 4$ matrices $A$ and $B$ such that $A_{\mu\nu} k^\mu k^\nu = B_{\mu\nu} k^\mu k^\nu$ for every vector $k$ that is null for the standard $(-,+,+,+)$ Minkowski metric, yet $A \neq B$.
background
The module isolates the finite-dimensional linear algebra behind Jacobson's thermodynamic route to Einstein's equation. Equality of two symmetric quadratic forms on every Minkowski-null direction fixes their difference only up to a scalar multiple of the metric; an all-null local Clausius balance therefore has the algebraic shape of Einstein's equation with the metric term free.
Symmetric4 is componentwise symmetry of a real covariant 2-tensor on $\mathrm{Fin},4$. The standard Minkowski metric $\eta$ is the diagonal matrix $\mathrm{diag}(-1,1,1,1)$. A four-vector $k$ is Minkowski-null when $-k_0^2+k_1^2+k_2^2+k_3^2=0$. Quadratic contraction is the scalar $A_{\mu\nu}k^\mu k^\nu$. A companion lemma records that $\eta$'s contraction on $k$ is exactly that Minkowski quadratic form.
The sibling implication (pointwise equality implies null-cut equality) is immediate; this declaration supplies the converse failure.
proof idea
Explicit counterexample: take $A=\eta$ (the standard Minkowski metric) and $B=0$. Symmetry of $\eta$ is checked by cases on diagonal versus off-diagonal entries; symmetry of zero is immediate. For any Minkowski-null $k$, the contraction identity for $\eta$ reduces $\eta_{\mu\nu}k^\mu k^\nu$ to the null quadratic form, which vanishes, matching the zero tensor's contraction. Distinctness is the $(0,0)$ entry: $\eta_{00}=-1\neq 0$.
why it matters
In the Clausius–Einstein bridge, one must not confuse agreement of quadratic forms on the null cone with full tensor equality. This lemma records that null-cut equality is strictly weaker, so the free scalar multiple of the metric cannot be killed by null probes alone. The module deliberately stays independent of the refuted ledger-deficit-to-signed-hinge bridge: it does not build horizons, identify heat with stress-energy, or fix the free scalar by conservation. Downstream rigidity (null-contraction zero implies a multiple of $\eta$) is the positive half of the same hinge; this negative half keeps the logical gap honest. No parent theorems currently cite it (used_by is empty); it is local scaffolding for the algebraic reading of Jacobson's argument inside Recognition gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.