quadContr_smul_eta_of_null
plain-language theorem explainer
Any scalar multiple of the Minkowski metric η has vanishing quadratic form on every Minkowski-null covector. Gravity and null-cone rigidity arguments cite this to show that η-multiples are invisible to null probes. The proof rewrites via the scalar-multiple identity for quadContr(λη), then substitutes the null condition.
Claim. For every real scalar $\lambda$ and every covector $k\in\mathbb{R}^4$ that is null for the standard Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$ (i.e. $-(k_0)^2+(k_1)^2+(k_2)^2+(k_3)^2=0$), the quadratic contraction $(\lambda\eta)_{\mu\nu}k^\mu k^\nu$ equals zero.
background
This module develops finite-dimensional real linear algebra for symmetric $4\times 4$ matrices: values of a symmetric quadratic form on all Minkowski-null covectors determine the matrix only modulo a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$. It is an algebraic prerequisite for Phase 5 gravity work, not a geometric curvature construction.
The quadratic contraction is $\mathrm{quadContr}(A,k)=\sum_{i,j}A_{ij}k_i k_j$. Nullness means $-(k_0)^2+(k_1)^2+(k_2)^2+(k_3)^2=0$. The Minkowski metric $\eta$ is the diagonal matrix with $-1$ in the time slot and $+1$ on the spatial diagonal.
The immediate upstream identity is $\mathrm{quadContr}(\lambda\eta,k)=\lambda\bigl(-(k_0)^2+(k_1)^2+(k_2)^2+(k_3)^2\bigr)$, which holds for every $k$, null or not. The present result specialises that identity to the null cone.
proof idea
One short tactic proof. Rewrite the goal by the unrestricted scalar identity quadContr_smul_eta, which factors out $\lambda$ times the Minkowski quadratic form of $k$. Unpack the hypothesis MinkowskiNull k into the explicit equation $-(k_0)^2+(k_1)^2+(k_2)^2+(k_3)^2=0$. A final simp multiplies by $\lambda$ and closes the goal at zero.
why it matters
Null-cone reconstruction of symmetric matrices works only modulo multiples of $\eta$. This lemma is the elementary vanishing fact that makes those multiples invisible: adding $\lambda\eta$ never changes null-cone quadratic values.
It feeds two parent results in the same module. diff_scalar_eta_implies_null_quadratic_eq (the converse direction: a pure metric difference is invisible on the null cone) uses it to equate $\mathrm{quadContr},A$ and $\mathrm{quadContr},B$ whenever $A-B=\lambda\eta$. determinesAlgebraicNullQuadraticClass_add_eta uses it to show that adding a metric multiple does not change the algebraic null-quadratic class of a symmetric representative.
In the broader Recognition gravity stack this is Tier-A algebra only. The module doc is explicit that Phase 5 remains open until an independently constructed symmetric $G$ with Recognition area/focusing ancestry exists; this lemma does not identify matrices with Ricci or stress-energy, nor close the Einstein equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.