axisWaveVector
plain-language theorem explainer
Defines the integer lattice momentum m = (1,0,0) along a coordinate axis of the periodic Freudenthal torus. Gravity analysts cite it as the canonical non-vacuous wave-vector witness for TT Bloch-symbol and second-variation gates. The body is a three-branch pattern match on Fin 3.
Claim. The axis integer wave vector is the map $m:\{0,1,2\}\to\mathbb{Z}$ with $m(0)=1$ and $m(1)=m(2)=0$, i.e. the lattice momentum $(1,0,0)$.
background
This module is Stage 1 of the Regge TT continuum-symbol program: the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, its flat point, and the TT Bloch symbol object built from plane-wave edge fields at commensurate momenta $k=2\pi m/N$ with $m:\mathrm{Fin},3\to\mathbb{Z}$.
A transverse-traceless (TT) polarization is a symmetric traceless $3\times 3$ matrix orthogonal to the wave vector. The continuum target asks whether the TT Bloch symbol of the true Regge action tends to $-(1/4)I_{\mathrm{TT}}$ isotropically; that target remains open, so the development needs concrete nonzero $m$ and matching TT frames as non-vacuity witnesses.
The axis choice $m=(1,0,0)$ is the simplest lattice direction. Paired polarizations are the $+$ frame $\mathrm{diag}(0,1/\sqrt{2},-1/\sqrt{2})$ and the $\times$ frame, both proved TT for this $m$.
proof idea
Pure definition by cases on the three coordinates of $\mathrm{Fin},3$: first component $1$, second and third $0$. No lemmas, tactics, or proof obligations.
why it matters
Supplies the fixed nonzero momentum that grounds every axis instance in the preflight and closer stack. Downstream, axisWaveVector_ne_zero discharges the open target's non-zero hypothesis; axisTTPolarizationPlus_isTT and axisTTPolarizationCross_isTT certify the two C10 TT frames against this $m$.
axis_plus_continuum_symbol instantiates the closed continuum-symbol receipt at (axis $m$, $+$ polarization) with value $-1/4$. The flat second-variation lane builds axisReducedSecondVariation and proves the reduced Schläfli formula applies to the plane-wave profile at commensurate momentum from this vector (GATE A2(c)), giving a model-level cross-check hook for the numerical isotropy probe without claiming the continuum limit.
In the QG campaign this is the preregistered axis direction among the 14 directions of the C10 probe; the open isotropy target still sits above it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.