planeWaveTetVelocity_zeroMomentum
plain-language theorem explainer
At vanishing Bloch momentum every plane-wave edge velocity on a periodic tetrahedron collapses to the bare polarization coefficient of that edge's displacement class. Zero-mode and TT-symbol analysts cite it when reducing the k=0 cell stencil to assembled constant blocks. The proof unfolds the velocity definition, kills the midpoint phase by simp, then applies cos(0)=1 and a grounding identity for the slot class.
Claim. For lattice size $N\ge 1$, strain matrix $E:\mathbb{R}^{3\times 3}$, periodic tetrahedron $\tau$ in the $N^3$ torus, and edge index $f\in\{0,\ldots,5\}$, the plane-wave tetrahedron velocity at zero wavevector equals the polarization edge-class coefficient of the displacement class of slot $f$: $v_{\mathrm{pw}}(N,E,k{=}0,\tau,f)=c_{d(\tau,f)}(E)$.
background
This module is Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1, Lane C): hinge-aware zero mode for the Regge TT symbol. The assembled constant block at $k=0$ is built from per-edge plane-wave velocities contracted against the Schlaefli Hessian; those velocities are the objects simplified here.
A plane-wave tetrahedron velocity is the product of a cosine of the edge-midpoint Bloch phase with a polarization coefficient attached to the edge's displacement class. The midpoint phase is the average of the wavevector dotted into the two endpoints of the local edge of $\tau$. Displacement classes label the seven geometric edge types that appear in the Freudenthal cube triangulation; polEdgeCoeff reads the corresponding entry of the strain $E$.
The zero-momentum specialization sets the wavevector identically to zero, so every midpoint phase is expected to vanish and the cosine factor to become $1$. Downstream, the raw cell stencil at $k=0$ sums these velocities over all tets and edge pairs and normalizes by $2/N^3$.
proof idea
Term-mode proof by unfolding and rewriting. Unfold the plane-wave velocity definition. The cosine multiplies the polarization coefficient by $\cos(\mathrm{phase})$; show the midpoint phase of the local edge at $k\equiv 0$ is zero by unfolding the phase and simplifying (dot products against the zero wavevector). Rewrite with $\cos 0=1$ and $1\cdot c=c$, then apply the grounding lemma that identifies the slot displacement class of $(\tau,f)$ with the class used by the coefficient map. No case splits or induction.
why it matters
Feeds rawCellStencil_zeroMomentum, which states that the $k=0$ raw cell stencil equals twice the per-cell assembled constant block: after this identity every velocity is momentum-independent and equal to a bare edge-class coefficient, so the $N^3$ identical cell copies cancel the $2/N^3$ normalization and leave the factor $2$.
That reduction is a step toward the module headline assembledConstantBlock_eq_zero: the Schlaefli-reduced assembled constant block vanishes on the TT witness, closing the hinge-aware zero-mode gate. The sympy diagnostic had already seen assembled quadratic zero at the witness while the stencil-only residual matched the hinge term; the kernel now pins the relative-minus assembly convention without floating-point appeal.
In the broader RS gravity lane this is discrete-geometry bookkeeping for the Regge TT symbol on the eight-tick / $D=3$ lattice, not a new continuum force law. It does not itself invoke J-uniqueness or the mass ladder; it clears the $k=0$ algebraic obstruction so the TT kernel can be certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.