NullConeEquivalent
plain-language theorem explainer
Two real 4×4 matrices are null-cone equivalent when they return the same quadratic scalar on every Minkowski-null covector. Anyone citing the Phase 5 algebraic rigidity package (symmetric matrices modulo η from null data) uses this relation. The definition is a plain universal equality; reflexivity, symmetry, and transitivity are immediate one-line consequences.
Claim. Matrices $A,B\in M_4(\mathbb{R})$ are null-cone equivalent if, for every covector $k\in\mathbb{R}^4$ that is null for the Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$, the quadratic contractions agree: $A(k,k)=B(k,k)$.
background
This module is finite-dimensional real linear algebra serving as an algebraic prerequisite for Phase 5 gravity work. The setting is the standard Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$ on $\mathbb{R}^4$. A covector $k$ is Minkowski-null when $\eta(k,k)=0$. The quadratic contraction of a matrix $A$ against $k$ is the scalar $A(k,k)$ (the bilinear form associated to $A$ evaluated on the pair $(k,k)$).
The module's thesis is rigidity: the values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix only up to adding a scalar multiple of $\eta$. Antisymmetric parts are invisible to the null quadratic map. The package is explicitly not a geometric curvature tensor and does not close the Einstein equation.
Null-cone equivalence is the raw comparison relation underlying that class: two matrices (not yet reduced modulo $\eta$) induce identical null quadratic scalars.
proof idea
Pure definition: the body is the proposition $\forall k,,(\text{Minkowski-null }k)\Rightarrow \mathrm{quadContr}(A,k)=\mathrm{quadContr}(B,k)$. No lemmas are invoked.
Immediately after, three structure theorems are proved by elementary equality reasoning: reflexivity by rfl; symmetry by applying .symm to the scalar equality; transitivity by chaining the two equalities with .trans. No matrix algebra beyond the definition is required.
why it matters
This relation is the comparison primitive for the null-cone quadratic tensor class. Downstream siblings (symmetrization modulo $\eta$, vanishing of the antisymmetric part under quadratic contraction, reconstruction of the symmetric class from null data) all speak in terms of agreement of null quadratic scalars; this definition names that agreement.
In the Recognition framework it sits strictly on the algebraic side of Phase 5. The module doc is explicit: Tier A remains open until a symmetric $G$ is built from Recognition area/focusing ancestry independently of any fixed stress tensor. The definition supplies no geometric ancestry, no Ricci identification, and no EFE closure. It only equips the later theorems that classify matrices by their null-cone quadratic maps.
No downstream consumers are recorded yet in the graph; the declaration is infrastructure for the rigidity package itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.