nullAxisWave
plain-language theorem explainer
Canonical null wave covector m=(1,1,0,0) on Fin 4 for the (−,+,+,+) Minkowski metric. It is the fixed axis witness for the null-case algebraic TT layer: nullness, cross-dot with an auxiliary null partner, and two independent TT polarizations. Defined by packaging components through the four-vector constructor; no proof content.
Claim. Define the covector $m\in\mathbb{R}^{4}$ by $m=(1,1,0,0)$ in the ordered basis of $\mathrm{Fin}\,4$ (time, then three spatial axes).
background
This module is the Lorentzian algebraic layer of the QG campaign item edge_tt_decomposition: transverse-traceless splitting of symmetric $4\times 4$ real matrices against a Minkowski wave covector. Signature is $(-!,+,+,+)$. Covectors are lowered by default; the Minkowski pairing is $\langle a,b\rangle=-(a_0)(b_0)+a_1 b_1+a_2 b_2+a_3 b_3$.
When the wave covector is null ($\langle m,m\rangle=0$, $m\neq 0$), the non-null projector $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$ is unavailable. One introduces an auxiliary null partner $\ell$ with $m\cdot\ell\neq 0$ and uses $P_{ij}=\eta_{ij}-(m_i\ell_j+\ell_i m_j)/(m\cdot\ell)$. Lorentz TT means symmetric, Minkowski-traceless, and Lorentz-transverse (second index contracted against the raised wave covector).
Upstream, vec4 a b c d builds a $\mathrm{Fin},4\to\mathbb{R}$ map with named components, used for finite null probes.
proof idea
Pure definition: apply the four-vector constructor with components $1,1,0,0$. No tactics, no lemmas, no proof body.
why it matters
Anchors the §4 “axis null witness” block that exhibits two independent TT polarizations on a concrete null ray. Downstream facts pin nullness ($\langle m,m\rangle=0$), the cross pairing with the auxiliary null partner ($m\cdot\ell=-2$), Euclidean momentum squared equal to $2$, and that both plus and cross screen polarizations are Lorentz TT relative to this $m$.
It also supplies the counterexample axis for two negative results: the Euclidean transverse projector is defined on this ray but fails Lorentz transversality, and the naive non-null Lorentz projector hypothesis is false on the null cone. Together these close the null branch of the algebraic residual identity (TT + $m$-gauge + $\ell$-gauge − bilinear + screen-trace) without touching lattice Regge edges, $S_{\mathrm{RS}}\to\mathrm{EH}$, or polarization normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.