fixedSymmetricStress_determinesAlgebraicNullQuadraticClass
plain-language theorem explainer
Any fixed symmetric 4×4 stress matrix T determines an algebraic null-quadratic class: its direction-indexed flux agrees with the quadratic contraction of T on all Minkowski-null covectors, and any other symmetric matrix with the same null values differs from T by a scalar multiple of η. Gravity and Clausius–Einstein bridge work cite this to attach the fixed-stress scalar map to the Phase 5 rigidity package. The proof is a one-line unfold of fixedStressFlux into quadContr plus the general symmetric-matrix class theorem.
Claim. Let $T$ be a real $4\times 4$ matrix that is symmetric ($T_{ij}=T_{ji}$). Write $\varphi_T(k)=T^{\mu\nu}k_\mu k_\nu$ for the quadratic contraction (fixed stress flux). Then $\varphi_T$ determines the algebraic null-quadratic class of $T$: $T$ is symmetric, $\varphi_T(k)$ equals that contraction on every Minkowski-null covector $k$, and if $B$ is any other symmetric matrix with the same null values then $T-B=\lambda\,\eta$ for some $\lambda\in\mathbb{R}$, where $\eta=\mathrm{diag}(-1,1,1,1)$.
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 modulo a scalar multiple of the Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$. It is a rigidity package only. It does not construct an independently geometric tensor $G$, horizons, Unruh temperature, or the Einstein equation; Tier A remains open until such a $G$ is built from Recognition area/focusing ancestry.
Symmetric4 is the componentwise symmetry predicate $A_{ij}=A_{ji}$ on real $4\times 4$ matrices (from the Clausius–Einstein bridge). The quadratic contraction quadContr A k is the scalar $A^{\mu\nu}k_\mu k_\nu$. The local map fixedStressFlux T is definitionally that contraction, packaged to match the fixed-stress flux shape used by horizon-indexed record flux without importing that heavier module.
DeterminesAlgebraicNullQuadraticClass $\varphi$ $A$ asserts three facts: $A$ is symmetric; $\varphi$ agrees with quadContr A on every Minkowski-null covector; and any other symmetric $B$ with the same null values differs from $A$ by $\lambda\eta$. The upstream theorem determinesAlgebraicNullQuadraticClass_quadContr already shows every symmetric matrix determines its own class via quadContr.
proof idea
One-line wrapper. Unfold fixedStressFlux (definitionally quadContr T) by simpa, then apply determinesAlgebraicNullQuadraticClass_quadContr T hT. That upstream result packages symmetry of $T$, reflexivity of the null-cone identity, and the reconstruction lemma null_quadratic_eq_implies_diff_scalar_eta that forces $T-B=\lambda\eta$ whenever $B$ is symmetric and matches on the null cone.
why it matters
Closes the fixed-stress instantiation branch of the null-cone quadratic tensor class package: every symmetric stress matrix, via its direction-indexed flux, is an algebraic null-quadratic class. Downstream it feeds nullConeQuadraticTensorClassCert, which bundles future-to-all null equality, reconstruction, the converse, and antisymmetry-invisibility into a single certificate.
The doc-comment notes the statement specializes immediately to HorizonIndexedRecordFlux.witnessFixedStress once Symmetric4 is known, without re-importing that module here. Framework role is strictly algebraic Phase 5 prerequisite: it does not identify matrices with Ricci or stress-energy, does not set $G:=T$, and does not close the Einstein field equation. Tier A (independent geometric $G$ from Recognition area/focusing ancestry) remains open; this lemma only supplies the stress-side algebraic class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.