diff_scalar_eta_implies_null_quadratic_eq
plain-language theorem explainer
A pure scalar multiple of the Minkowski metric is invisible on the null cone: if two real 4×4 matrices differ by λη, their quadratic contractions agree on every Minkowski-null covector. Gravity and rigidity arguments cite this as the converse half of null-cone reconstruction modulo η. The proof rewrites the difference as a scaled metric, expands by bilinearity, and cancels the η term via the sibling null-contraction lemma.
Claim. Let $A,B\in M_4(\mathbb{R})$ and $\lambda\in\mathbb{R}$. If $A_{ij}-B_{ij}=\lambda\,\eta_{ij}$ for all indices $i,j$, where $\eta=\mathrm{diag}(-1,1,1,1)$ is the Minkowski metric, then for every Minkowski-null covector $k$ the quadratic contractions agree: $A(k,k)=B(k,k)$.
background
This module is a finite-dimensional real linear-algebra package: values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix only modulo a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$. It is an algebraic prerequisite for Phase 5 gravity work, not a geometric curvature construction. The module imports only the Clausius–Einstein bridge (for the fixed matrix $\eta$), and explicitly does not identify matrices with Ricci or stress-energy, nor close the Einstein equation.
The quadratic contraction $\mathrm{quadContr},M,k$ is the double sum $\sum_{i,j} M_{ij} k_i k_j$. A covector $k$ is Minkowski-null when that contraction against $\eta$ vanishes. The sibling lemma $\mathrm{quadContr_smul_eta_of_null}$ records that any scalar multiple of $\eta$ has vanishing null contraction: on the light cone, $\eta$ itself is invisible to the quadratic form.
The present statement is the converse direction of the rigidity package: a pure metric difference cannot be seen by null-cone data.
proof idea
Introduce a null covector $k$. From the entrywise hypothesis, rebuild the matrix identity $A=B+\lambda\bullet\eta$ by extensionality and linear arithmetic on each entry. Apply $\mathrm{quadContr}(\cdot),k$ to both sides. Expand the right-hand side by bilinearity of the double sum (additivity of $\mathrm{quadContr}$ under matrix addition). The cross term $\mathrm{quadContr}(\lambda\bullet\eta),k$ is zero by the sibling lemma $\mathrm{quadContr_smul_eta_of_null}$ because $k$ is null. Cancel the zero summand and conclude equality of the two contractions.
why it matters
This is the converse half of the null-cone rigidity package. It is wired directly into the module certificate $\mathrm{nullConeQuadraticTensorClassCert}$ as the field $\mathrm{converse}$, and it supplies one direction of both biconditionals: the symmetric-matrix iff (null quadratic data $\Leftrightarrow$ difference is a scalar multiple of $\eta$) and the general-matrix iff (null data determines the symmetrization modulo $\eta$).
In the Recognition framework this is Phase 5 algebraic scaffolding only. The module doc is explicit that Tier A remains open until a symmetric $G$ is built from Recognition area/focusing ancestry independently of any fixed stress tensor. The result does not construct horizons, Unruh temperature, continuum Ricci, or the Einstein field equation; it only records that pure $\eta$-shifts are null-cone invisible, which is the algebraic reason the reconstruction class is well-defined modulo $\eta$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.