fixedSymmetricStress_null_class_unique
plain-language theorem explainer
Two symmetric 4×4 real matrices that induce the same fixed-stress flux on every Minkowski-null covector differ by a scalar multiple of the Minkowski metric η. Phase-5 gravity workers cite this as algebraic uniqueness of the null-cone quadratic class for fixed symmetric stress. The proof is a one-line term applying the general null-quadratic rigidity lemma.
Claim. Let $T,B$ be symmetric $4\times 4$ real matrices. If their fixed-stress flux scalars agree on every Minkowski-null covector $k$, then there exists $\lambda\in\mathbb{R}$ such that $T_{ij}-B_{ij}=\lambda\,\eta_{ij}$ for all $i,j$, where $\eta=\mathrm{diag}(-1,1,1,1)$.
background
This module is the Phase-5 algebraic prerequisite: finite-dimensional real linear algebra on $4\times 4$ matrices over Minkowski space. A symmetric matrix defines a quadratic form; its values on Minkowski-null covectors (those $k$ with $\eta(k,k)=0$) are the null-cone data. The rigidity claim is that those values determine the matrix only up to adding a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$.
The fixed-stress flux is the scalar map that pairs a symmetric stress matrix with a null covector in the same shape used by the Clausius–Einstein bridge import. Symmetry of both matrices is an explicit hypothesis (Symmetric4). The module imports only that bridge; it does not re-import horizon-indexed witness matrices, and it does not identify any matrix with Ricci or stress-energy.
Sibling lemmas establish the supporting algebra: symmetrization is invisible to the quadratic contraction, antisymmetrization contributes zero, and agreement on future nulls extends to all nulls when a nonzero future-null witness is present.
proof idea
One-line term proof. It applies the general rigidity lemma that equal null-quadratic contractions of two symmetric matrices force their difference to be a scalar multiple of $\eta$. The fixed-stress flux hypotheses are passed through unchanged as the null-quadratic equality data; no extra case split or future-null extension is performed at this wrapper.
why it matters
This is the stress-specialized face of the module's THEOREM tag: every fixed symmetric stress scalar map instantiates an algebraic null-quadratic class, unique modulo $\eta$. It is the algebraic prerequisite Phase 5 needs before any geometric $G$ can be compared to stress on the null cone.
No downstream consumers are recorded yet. The module's OPEN residual is explicit: an independently constructed symmetric $G$ from Recognition area/focusing ancestry, with a proved future-null quadratic comparison, would then be identified modulo $\eta$ by the companion future-null rigidity theorem. Taking $G:=T$ or reusing a shared MODEL chart is forbidden and leaves Tier A open. This declaration does not touch Ricci identification, Unruh temperature, C-gap1, or Einstein-field-equation closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.