ttWitnessWaveVector
plain-language theorem explainer
Integer lattice wave vector m = (0,0,1), i.e. k = e_z, for the reported TT polarization witness in the Regge hinge-aware zero-mode analysis. Downstream TT checks and residual cancellations cite this fixed direction. The body is a three-case pattern match on Fin 3; no proof content.
Claim. The witness wave vector is the integer map $m:\{0,1,2\}\to\mathbb{Z}$ with $m(0)=0$, $m(1)=0$, $m(2)=1$, equivalently $k=e_z$ in lattice form.
background
This module is Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1, Lane C): it closes the hinge-aware zero-mode gate for the assembled Regge TT constant block.
A same-day sympy diagnostic found that the stencil-only constant block does not vanish under TT at the reported witness (polarization $E=\mathrm{diag}(1,-1,0)/\sqrt{2}$ with $k=e_z$), leaving residual $-\pi(\sqrt{2}+4)/8$. The assembled mode cancels once the hinge term is included with relative minus sign. The wave vector here is the discrete $k$ half of that reported witness pair.
In the lattice setting, wave vectors are integer maps $\mathrm{Fin},3\to\mathbb{Z}$. The unit vector along the third axis is the conventional choice that makes transversality and the residual bookkeeping line up with the recorded diagnostic.
proof idea
Pure definition by cases: index 0 and 1 map to 0, index 2 maps to 1. No lemmas, tactics, or algebraic reduction.
why it matters
Pins the wave-vector half of the phrase "the reported TT witness" used throughout the hinge-aware zero-mode gate. The immediate consumer is ttWitness_isTT, which proves the companion polarization is symmetric, traceless, transverse, and Frobenius-normalized for this $k=e_z$. That TT certificate grounds residual identities such as hinge cancellation against the stencil-only constant residual and the assembled-block zero-mode headline. Without a fixed lattice $k$, the transversality clause of the TT predicate is undefined. Framework role is local to Gravity / Regge discrete gravity analysis rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.