determinesAlgebraicNullQuadraticClass_quadContr
plain-language theorem explainer
Every symmetric real 4×4 matrix A determines the algebraic null-quadratic class of its quadratic contraction on Minkowski-null covectors: any other symmetric B agreeing on the null cone differs from A by a scalar multiple of η. Phase-5 gravity algebra cites this as the canonical instantiation for quadContr. The proof is a short term package of symmetry, definitional null-cone agreement, and the uniqueness lemma that forces A−B=λ η.
Claim. Let $A$ be a symmetric real $4\times 4$ matrix. Then the scalar map $\varphi(k)=A_{\mu\nu}k^\mu k^\nu$ determines the algebraic null-quadratic class of $A$: $A$ is symmetric, $\varphi$ equals that quadratic contraction on every Minkowski-null covector, and if $B$ is any other symmetric matrix with the same null-cone values then there exists $\lambda\in\mathbb{R}$ such that $A-B=\lambda\,\eta$ with $\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 $\eta=\mathrm{diag}(-1,1,1,1)$. It is a rigidity package only. It does not construct geometric curvature, horizons, or close the Einstein equation.
The quadratic contraction is $\mathrm{quadContr}(A)(k)=\sum_{i,j} A_{ij} k_i k_j$. Symmetry is the componentwise predicate $A_{ij}=A_{ji}$. The predicate "determines an algebraic null-quadratic class" asserts three facts: the representative is symmetric; it reproduces the given scalar map on every null covector; and any other symmetric matrix with the same null values differs by a multiple of $\eta$. The module doc stresses this is theorem-backed equivalence without a quotient type and supplies no geometric ancestry.
Upstream, the uniqueness engine is the lemma that equal null-quadratic forms on symmetric matrices force a pure $\eta$ difference. The bridge import supplies only the contraction and the Minkowski null predicate.
proof idea
Term-mode proof via refine on the three conjuncts of the class predicate. The first conjunct is the given symmetry hypothesis. The second is definitional: on null covectors, quadContr A equals itself by rfl. The third conjunct is discharged by applying the upstream uniqueness lemma null_quadratic_eq_implies_diff_scalar_eta to $A$, $B$, their symmetries, and the assumed null-cone agreement of the two contractions. No further case analysis or computation appears.
why it matters
This is the canonical witness that every symmetric matrix, via its own quadratic contraction, instantiates an algebraic null-quadratic class. Downstream, fixedSymmetricStress_determinesAlgebraicNullQuadraticClass is a one-line specialization: any fixed symmetric stress scalar map determines its class modulo $\eta$, and that statement notes it specializes immediately to the horizon-indexed witness once symmetry is known.
In the Recognition gravity stack this closes the pure-algebra side of the null-cone reconstruction package (module honesty tag THEOREM). It does not touch the OPEN Tier-A demand for an independently constructed symmetric $G$ with Recognition area/focusing ancestry, nor continuum Ricci, C-gap1, or the Einstein field equation. The module forbids identifying the matrix with Ricci or stress-energy. Landmark contact is only the $D=3$ spatial setting already fixed upstream (T8); no new forcing-chain step is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.