nullAxisWave_ne_zero
plain-language theorem explainer
The concrete null probe covector (1,1,0,0) on Minkowski 4-space is nonzero. Anyone instantiating the null Lorentzian TT residual identity against an explicit wave axis cites this. The proof is a one-step component extraction: the time slot equals 1, so the vector cannot be identically zero.
Claim. The covector $m = (1,1,0,0) \in \mathbb{R}^{4}$ is not the zero map $\mathrm{Fin}\,4 \to \mathbb{R}$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: transverse-traceless splitting of symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case. Signature is $(-+++)$. Covectors are lowered by default; the Minkowski pairing is $\mathrm{minkowskiDot},a,b = -(a_0)(b_0)+\sum_{i=1}^{3}a_i b_i$.
For null waves one needs $m\cdot m=0$ with $m\neq 0$, plus an auxiliary null partner $\ell$ with $m\cdot\ell\neq 0$, to build the projector $P_{ij}=\eta_{ij}-(m_i\ell_j+\ell_i m_j)/(m\cdot\ell)$. The definition nullAxisWave supplies the explicit probe $m=\mathrm{vec4},1,1,0,0$, i.e. components $(1,1,0,0)$, used as a residual identity axis in the null TT decomposition theorem.
proof idea
Assume for contradiction that the probe equals the zero function. Apply congruence of the evaluation map $v\mapsto v_0$ to both sides. Unfolding the definitions of the probe and of vec4 yields $1=0$ at the time slot, which is absurd. No external lemmas beyond definitional simplification are required.
why it matters
The null TT residual identity (exists_nullLorentzTTDecomposition) needs a nonzero null wave axis; this lemma discharges the $m\neq 0$ side condition for the standard lightlike probe $(1,1,0,0)$. It sits in the Lorentzian linear-algebra layer that closes the ledger name edge_tt_decomposition without claiming Regge EDGE perturbation decomposition, Einstein-Hilbert recovery, or polarization normalization. No downstream consumers are wired yet in the graph; the result is infrastructure for explicit null-case instantiations rather than a forcing-chain landmark (T0-T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.