null_quadratic_eq_implies_diff_scalar_eta
plain-language theorem explainer
If two symmetric 4×4 real quadratic forms agree on every Minkowski-null covector, their difference is a scalar multiple of the Minkowski metric η. Phase-5 gravity workers cite this as the algebraic reconstruction step for the null-quadratic tensor class. The proof rewrites an upstream matrix identity A = B + λ·η into componentwise differences via congruence and linear arithmetic.
Claim. Let $A,B$ be symmetric $4\times 4$ real matrices. If $k^{\top} A k = k^{\top} B k$ for every Minkowski-null covector $k$, then there exists $\lambda\in\mathbb{R}$ such that $A_{ij}-B_{ij}=\lambda\,\eta_{ij}$ for all $i,j$, where $\eta=\mathrm{diag}(-1,1,1,1)$.
background
This module is the Phase-5 algebraic prerequisite: finite-dimensional real linear algebra on $4\times 4$ matrices over $\mathbb{R}$. The quadratic contraction $\mathrm{quadContr}(A,k)$ is the scalar $k^{\top} A k$. A covector $k$ is Minkowski-null when that contraction against $\eta=\mathrm{diag}(-1,1,1,1)$ vanishes. Symmetric4 means $A_{ij}=A_{ji}$.
The local claim is rigidity: null-cone values of a symmetric quadratic form determine the matrix only modulo scalar multiples of $\eta$. The module is explicit that this is not geometric curvature, not Ricci, and not an independently constructed Einstein tensor $G$.
Upstream, the proof leans on a sibling reconstruction that already produces the matrix identity $A=B+\lambda\bullet\eta$ from the same null-agreement hypothesis; the present theorem only changes the bookkeeping to componentwise differences $A-B=\lambda\eta$.
proof idea
One-step unpack of an upstream reconstruction. First obtain $\langle\lambda, h_\lambda\rangle$ from the sibling lemma that turns null-cone agreement of symmetric $A,B$ into the matrix equation $A=B+\lambda\bullet\eta$. Refine the existential with that same $\lambda$. For each index pair $(i,j)$, apply double congrFun to read the matrix identity at $(i,j)$, rewrite the scalar-multiplication notation into ordinary multiplication, and finish by linarith to rearrange into $A_{ij}-B_{ij}=\lambda,\eta_{ij}$.
why it matters
This is the reconstruction arrow of the null-cone quadratic tensor class. The module certificate wires it in as reconstruction, alongside the converse, future-to-all null extension, and antisymmetry-invisibility. Downstream, every symmetric matrix is shown to determine its algebraic null-quadratic class by calling this lemma; adding $\lambda\eta$ is shown not to change the class; the biconditional form is assembled from this direction plus the converse; fixed symmetric stress maps inherit uniqueness of the null class; and the future-null variant hands off section data to the same rigidity conclusion.
In the Recognition gravity stack this is pure algebra for Phase 5: it classifies symmetric matrices by null quadratic data modulo $\eta$. It does not construct an independent $G$ from area/focusing ancestry, does not identify matrices with Ricci or stress-energy, and does not close the Einstein field equation. Tier A remains open pending that geometric $G$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.