nullConeQuadraticTensorClassCert
plain-language theorem explainer
Assembles the Phase-5 algebraic certificate: null-cone values of a quadratic form determine a symmetric 4×4 matrix only modulo a scalar multiple of the Minkowski metric η. Anyone citing the null-cone rigidity package or the fixed-stress algebraic class will point here. The proof is a pure structure inhabitant that wires six already-proved lemmas into the certificate fields.
Claim. There exists a certificate recording that: (i) agreement of quadratic contractions on future nonzero Minkowski-null covectors extends to the full null cone; (ii) for symmetric matrices $A,B$, equality of null-cone quadratic contractions implies $A-B=\lambda\eta$ for some $\lambda\in\mathbb{R}$; (iii) conversely any pure $\eta$-difference is invisible on the null cone; (iv) antisymmetric parts do not affect quadratic contractions; (v) in general, null-cone data determine the symmetrization modulo $\eta$; (vi) every fixed symmetric stress scalar map determines an algebraic null-quadratic class.
background
The module is finite-dimensional real linear algebra on $4\times 4$ matrices over $\mathbb{R}$, with Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$. A covector $k$ is Minkowski-null when its quadratic form against $\eta$ vanishes. The quadratic contraction $\mathrm{quadContr}(A,k)$ is the scalar $k^{\mathsf T} A k$. Two symmetric matrices that agree under $\mathrm{quadContr}$ on every null $k$ differ by a scalar multiple of $\eta$; that is the rigidity fact.
The local setting is an algebraic prerequisite for Phase 5 of the gravity bridge. It is not the independently geometric tensor $G$ required by that phase, and it does not identify matrices with Ricci or stress-energy. The certificate structure records only rigidity and future-to-all extension.
Upstream lemmas supply each field: future-to-all extension by quadratic evenness and the observation that a null vector with zero time component is zero; reconstruction of the difference as $\lambda\eta$; the converse invisibility of pure $\eta$-differences; equality of contractions after four-index symmetrization; the general-class biconditional via symmetrization; and the fixed-symmetric-stress instantiation of the algebraic class.
proof idea
Term-mode structure inhabitant. Each field of the certificate is filled by a named upstream theorem:
future_to_all← extension from future nonzero null vectors to the whole cone;reconstruction← null-cone agreement of symmetric forms yields $A-B=\lambda\eta$;converse← pure metric difference is invisible on the null cone;antisym_invisible← quadratic contraction equals contraction of the four-index symmetrization;general_class← null-cone equality iff symmetrizations differ by $\lambda\eta$;fixed_stress_algebraic_class← every fixed symmetric stress scalar map determines an algebraic null-quadratic class.
No new reasoning occurs; the proof is pure assembly of already-proved facts.
why it matters
This is the packaged algebraic prerequisite for Phase 5 of the Clausius–Einstein bridge work. It freezes the null-cone rigidity statement that any later geometric construction of a symmetric $G$ from Recognition area/focusing ancestry must respect: null-cone quadratic data fix the symmetric matrix only modulo $\eta$.
The module honesty tags mark Tier A as still OPEN until an independently constructed symmetric $G$ exists; this certificate deliberately does not supply that $G$, does not close the Einstein field equation, and does not claim continuum Ricci or Unruh temperature. With used_by currently empty, the declaration is a terminal packaging point inside the gravity domain, ready for a downstream Phase-5 consumer once geometric ancestry is available.
In the broader Recognition framework it sits downstream of the forcing chain only indirectly (via the gravity bridge import), and it does not touch T5–T8, the Recognition Composition Law, or the $\phi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.