NullConeQuadraticTensorClassCert
plain-language theorem explainer
Bundles the Phase-5 algebraic rigidity package: two real 4×4 matrices agree as quadratic forms on the Minkowski null cone if and only if their symmetrizations differ by a scalar multiple of η. Anyone citing null-cone reconstruction of symmetric tensors modulo the metric will use this certificate. It is a Prop-structure of named fields, not a proved theorem; the companion instance theorem fills the fields.
Claim. A certificate asserting six algebraic facts in $4$D Minkowski space with $\eta=\mathrm{diag}(-1,1,1,1)$: (i) agreement of quadratic contractions $A_{\mu\nu}k^\mu k^\nu$ on future nonzero null $k$ extends to all null $k$; (ii) if symmetric $A,B$ agree on all null $k$, then $A-B=\lambda\eta$ for some $\lambda\in\mathbb{R}$; (iii) the converse; (iv) the antisymmetric part is invisible to the quadratic contraction; (v) general matrices agree on the null cone iff their symmetrizations differ by $\lambda\eta$; (vi) every fixed symmetric stress matrix determines an algebraic null-quadratic class for the corresponding scalar map.
background
The module is finite-dimensional real linear algebra on $\mathbb{R}^{1,3}$: values of a symmetric quadratic form on Minkowski-null covectors determine the symmetric matrix modulo a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$. It is an algebraic prerequisite for Phase 5 gravity, not a geometric curvature construction.
Upstream from ClausiusEinsteinBridge: minkowskiEta4 is the standard $(-,+,+,+)$ metric; MinkowskiNull k means $-(k^0)^2+(k^1)^2+(k^2)^2+(k^3)^2=0$; quadContr A k is the quadratic contraction $A_{\mu\nu}k^\mu k^\nu$. Sibling helpers include symmetrize4 and the fact that antisymmetrization contributes zero to quadContr.
DeterminesAlgebraicNullQuadraticClass $\varphi$ $A$ means $A$ is symmetric, $\varphi$ matches quadContr A on null vectors, and any other symmetric $B$ with the same null values differs from $A$ by $\lambda\eta$. The doc stresses this is only an algebraic equivalence class with no geometric ancestry.
proof idea
No proof body: this is a structure ... : Prop packaging six named hypotheses. The companion theorem nullConeQuadraticTensorClassCert builds an instance by assigning each field to a proved lemma: future_to_all from all_null_quad_eq_of_future_nonzero_null_quad_eq; reconstruction from null_quadratic_eq_implies_diff_scalar_eta; converse from diff_scalar_eta_implies_null_quadratic_eq; antisym_invisible from quadContr_eq_quadContr_symmetrize4; the remaining fields are filled analogously from the module's null-cone and fixed-stress lemmas. Treat the structure as the interface type those lemmas inhabit.
why it matters
Phase 5 needs a clean algebraic statement that null-cone quadratic data fix a symmetric tensor only up to $\lambda\eta$, before any geometric $G$ or Einstein equation is attempted. This certificate is that interface. Downstream, nullConeQuadraticTensorClassCert is the theorem that discharges every field.
Module honesty tags mark THEOREM status for null-cone reconstruction, converse, antisymmetry invisibility, the general symmetrized class, and fixed-stress algebraic instantiation. OPEN remain: independently constructed symmetric $G$ with Recognition area/focusing ancestry, geometric curvature, continuum Ricci, C-gap1, and EFE closure. The certificate deliberately omits those claims.
In the broader RS gravity bridge this sits under the Clausius–Einstein line: algebraic rigidity of null quadratic forms, not identification of matrices with Ricci or stress-energy, and not eight-tick or $D=3$ forcing (those live in the T0–T8 chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.