nullAxis_cross_dot
plain-language theorem explainer
The Minkowski pairing of the standard null wave covector (1,1,0,0) with its auxiliary null partner (1,-1,0,0) equals −2. Anyone building the null Lorentzian TT projector or residual identity cites this normalization. The proof is a one-line unfold-and-norm_num computation of the four-component pairing.
Claim. With the Minkowski pairing $\eta^{ij}a_i b_j = -a_0 b_0 + a_1 b_1 + a_2 b_2 + a_3 b_3$ on covectors in $\mathbb{R}^4$, if $m=(1,1,0,0)$ and $\ell=(1,-1,0,0)$, then $m\cdot\ell=-2$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: transverse-traceless decomposition 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 minkowskiDot, equal to $\sum_j a_j(\mathrm{raise},b)_j$.
For a null wave covector $m$ ($m\cdot m=0$, $m\neq 0$) one needs an auxiliary null partner $\ell$ with $m\cdot\ell\neq 0$. The null projector is then $P_{ij}=\eta_{ij}-(m_i\ell_j+\ell_i m_j)/(m\cdot\ell)$. The concrete axes used throughout the residual identities are $m=(1,1,0,0)$ and $\ell=(1,-1,0,0)$, built via the four-component constructor vec4.
Both axes are individually null; the cross pairing must be a fixed nonzero constant so that every subsequent projector coefficient is a pure rational.
proof idea
One-line wrapper: unfold the three definitions (minkowskiDot, the wave axis, and the auxiliary axis), simplify the vec4 case-split on Fin 4, then norm_num evaluates $-(1)(1)+(1)(-1)+0+0=-2$.
why it matters
The null Lorentzian TT residual identity (the module's main theorem exists_nullLorentzTTDecomposition) and every projector built from the standard null pair need a concrete nonzero value of $m\cdot\ell$. Fixing that value at $-2$ removes symbolic denominators from gauge and screen-trace coefficients and makes the algebraic residual identity a pure matrix identity over $\mathbb{R}$.
This sits inside Wave 4 / lane W4-1 of the QG full-theory campaign: the Lorentzian specialization of the Euclidean algebraic TT layer. It does not itself close Regge EDGE perturbations or the Einstein-Hilbert recovery goals named in the module doc; it only supplies the numerical hinge those later steps rely on when the wave covector is null.
No downstream consumers are recorded yet in the graph; the lemma is infrastructure for the null-case projector algebra in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.