axisWave
plain-language theorem explainer
The reference Euclidean wave covector on Fin 4 with components (1,0,0,0). Gravity analysts cite it as the fixed nonzero momentum against which the two unnormalized TT polarizations (plus and cross) and the longitudinal decoy are checked. It is a pure case-split definition with no proof obligation.
Claim. Define the axis wave covector $m \in \mathbb{R}^{4}$ by $m_{0}=1$ and $m_{i}=0$ for $i=1,2,3$. Equivalently, $m=e_{0}$ in the standard basis of $\mathbb{R}^{4}$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra transverse-traceless splitting of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer (Euclidean trace, Euclidean transversality, symmetry) with no Frobenius pin; Minkowski/null specialization is deferred.
A matrix $H$ is algebraically TT against $m$ when it is symmetric, Euclidean-traceless, and transverse to $m$. The squared Euclidean momentum of $m$ must be nonzero for the projectors and residual-trace terms in the decomposition to be well-defined. The axis wave is the canonical unnormalized integer choice used throughout the nondegeneracy section.
proof idea
Definition by exhaustive pattern match on $\mathrm{Fin},4$: index $0$ maps to $1$, and indices $1,2,3$ map to $0$. No lemmas, tactics, or proof body.
why it matters
Anchors the explicit two-polarization claim in 4D. Downstream, axisWave_momentumSq shows its Euclidean momentum squared equals $1$, so every projector hypothesis momentumSq m ≠ 0 holds on this choice. The plus and cross matrices are proved TT against it (axisTTPlus_isTT, axisTTCross_isTT), giving the independent unnormalized TT pair advertised in the module doc. The longitudinal decoy is built as a pure gauge part along the same axis, then shown non-transverse until ttProject restores TT. Closer-module equalities identify gauge decoys with this construction. This is scaffolding for the algebraic edge TT layer only; it does not touch continuum Lorentzian polarizations, Regge edge perturbations, or S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.