DeterminesAlgebraicNullQuadraticClass
plain-language theorem explainer
A scalar map on four-covectors and a 4×4 matrix jointly determine an algebraic null-quadratic class when the matrix is symmetric, matches the map on every Minkowski-null vector, and is unique up to adding a multiple of η. Gravity workers on the Phase-5 algebraic prerequisite cite this packaging. It is a Prop definition, three conjuncts with no proof body.
Claim. A pair $(\varphi,A)$ with $\varphi:(\mathbb{R}^4)\to\mathbb{R}$ and $A$ a real $4\times 4$ matrix determines an algebraic null-quadratic class when: (i) $A$ is symmetric; (ii) $\varphi(k)=A_{\mu\nu}k^\mu k^\nu$ for every Minkowski-null covector $k$; and (iii) any other symmetric $B$ with the same null values differs from $A$ by a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$.
background
The module is finite-dimensional real linear algebra for Phase 5: values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix modulo a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$. It is an algebraic rigidity package only. It does not construct geometric curvature, Ricci, horizons, or close the Einstein equation.
Upstream primitives from the Clausius–Einstein bridge: Symmetric4 is componentwise symmetry $A_{ij}=A_{ji}$; minkowskiEta4 is the standard $(-,+,+,+)$ metric; MinkowskiNull means $-(k_0)^2+(k_1)^2+(k_2)^2+(k_3)^2=0$; quadContr A k is the quadratic contraction $\sum_{i,j} A_{ij} k_i k_j$.
The doc-comment stresses that this is only an algebraic equivalence class, theorem-backed without a quotient type, and supplies no geometric ancestry.
proof idea
Definition, not a theorem. The body is the conjunction of three propositions: symmetry of $A$; pointwise agreement of $\varphi$ with the quadratic contraction of $A$ on the Minkowski null cone; and uniqueness of $A$ among symmetric matrices with that null-cone restriction, up to $A-B=\lambda\eta$. No tactics or lemmas are invoked at the definition site; downstream theorems discharge the uniqueness clause via the null-quadratic rigidity lemma.
why it matters
This predicate is the central packaging for the Phase-5 algebraic prerequisite. Downstream, every symmetric matrix determines its class (determinesAlgebraicNullQuadraticClass_quadContr); adding a metric multiple preserves the class (determinesAlgebraicNullQuadraticClass_add_eta); any fixed symmetric stress scalar map instantiates the class (fixedSymmetricStress_determinesAlgebraicNullQuadraticClass); and the Phase-5 certificate structure records related rigidity facts without claiming geometric $G$.
Module honesty tags keep Tier A OPEN: no independently constructed symmetric $G$ with Recognition area/focusing ancestry, no continuum Ricci, no C-gap1, no EFE closure. The definition deliberately stops at algebraic uniqueness modulo $\eta$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.