determinesAlgebraicNullQuadraticClass_add_eta
plain-language theorem explainer
Adding a multiple of the Minkowski metric leaves the algebraic null-quadratic class of a symmetric 4×4 matrix unchanged when the scalar map is the original quadratic contraction. Phase-5 rigidity work cites this to move freely among η-equivalent representatives. The proof checks symmetry of the shift, null-cone agreement via vanishing of η on null covectors, then applies the uniqueness lemma that equal null quadratics differ by a scalar times η.
Claim. Let $A$ be a symmetric $4\times 4$ real matrix and $\lambda\in\mathbb{R}$. Write $\varphi(k)=k^{\mathsf T} A k$ for the quadratic contraction and $\eta=\mathrm{diag}(-1,1,1,1)$. Then $\varphi$ determines the algebraic null-quadratic class of $A+\lambda\eta$: $A+\lambda\eta$ is symmetric, $\varphi$ agrees with the quadratic contraction of $A+\lambda\eta$ on every Minkowski-null covector, and any other symmetric matrix agreeing with $\varphi$ on the null cone differs from $A+\lambda\eta$ by a real multiple of $\eta$.
background
This module is the Phase-5 algebraic prerequisite: finite-dimensional real linear algebra showing that the values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix only modulo a scalar multiple of the Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$. It is a rigidity package, not a geometric curvature tensor, and does not identify matrices with Ricci or stress-energy.
The predicate DeterminesAlgebraicNullQuadraticClass packages three facts for a scalar map $\varphi$ and a matrix $A$: $A$ is symmetric; $\varphi$ equals the quadratic contraction of $A$ on every null covector; and any other symmetric matrix with the same null values differs from $A$ by a multiple of $\eta$. The quadratic contraction is the standard bilinear pairing $k\mapsto\sum_{i,j}A_{ij}k_i k_j$. A key sibling fact is that the contraction of any multiple of $\eta$ vanishes on the null cone.
The local setting is deliberately thin: the module imports only the Clausius–Einstein bridge and states algebraic class facts for every fixed symmetric stress with the same scalar-map shape, without pulling horizon or Unruh machinery.
proof idea
Three obligations are discharged in order.
First, symmetry of $A+\lambda\eta$: entrywise, additivity and scalar multiplication reduce to symmetry of $A$ plus symmetry of $\eta$, the latter by a diagonal/off-diagonal case split on the explicit formula for $\eta$.
Second, null-cone agreement: expand the quadratic contraction of the sum, then apply the sibling lemma that the contraction of $\lambda\eta$ vanishes on every Minkowski-null covector, so the extra term is zero.
Third, uniqueness: if $B$ is any other symmetric matrix whose null contraction matches $\varphi$, transport the null equality through the second step to obtain null equality between $A+\lambda\eta$ and $B$, then invoke the upstream uniqueness theorem that two symmetric matrices with identical null quadratic contractions differ by a scalar multiple of $\eta$.
why it matters
Inside the null-cone quadratic tensor class package, this lemma is the stability statement under the residual gauge $A\mapsto A+\lambda\eta$. Without it, every algebraic class fact would be pinned to a single representative rather than to the $\eta$-coset that the reconstruction theorem actually determines.
The module honesty tags mark the whole package as THEOREM for null-cone reconstruction modulo $\eta$, while Tier A remains OPEN until a symmetric $G$ is built from Recognition area/focusing ancestry independently of fixed stress. This declaration does not close that gap; it only keeps the algebraic class well-defined when one shifts by metric multiples, which is the natural freedom once the null cone is the only probe.
No downstream consumers are wired yet (used_by is empty). The natural landing sites are the fixed-stress scalar-map instantiations later in the same module and any future Phase-5 bridge that must compare two symmetric representatives of the same null data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.