zeroMomentum_symbol_is_zero
plain-language theorem explainer
At vanishing wave vector the fixed-N transverse-traceless Bloch symbol of the true nonlinear Regge second variation exists and equals zero, for every lattice size N and every polarization matrix. Lattice gravity and continuum-limit workers cite it as the flat zero-mode statement on the actual Hessian, not a stencil proxy. The proof feeds the Gate A2 reduced plane-wave symbol into the already-proved vanishing of the canonical finite H at zero momentum.
Claim. For every $N \ge 1$ and every real $3\times 3$ polarization matrix $E$, the fixed-$N$ TT Bloch symbol of the nonlinear Regge action at wave vector $k=0$ exists and equals $0$.
background
This module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware zero mode of the assembled Regge TT block on the periodic Freudenthal torus. Periodic tetrahedra PeriodicTet N N N index the six Freudenthal tets in each cubic cell of the $N^3$ lattice. Polarization is a matrix $E:\mathrm{Fin},3\to\mathrm{Fin},3\to\mathbb{R}$; the zero mode is the $k=0$ (integer momentum $m\equiv 0$) sector.
The reduced A2 canonical finite value canonicalFiniteH is the normalized double sum over tets and six edge slots of the product of flat slot sqrt-edge derivatives and flat slot angle derivatives. Gate A2 already identifies the true TT Bloch symbol with this reduced expression. Upstream, planeWave_TTBlochSymbolIs_reduced supplies existence of that symbol for any commensurate momentum, while canonicalFiniteH_zeroMomentum_eq_zero (proved in this module via the assembled constant-block vanishing) evaluates the $m=0$ case to zero.
Context from the sympy diagnostic: the stencil-only constant block does not vanish under TT, but the assembled hinge-minus-stencil block does; this corollary lifts that cancellation to a statement about the actual second-variation symbol.
proof idea
Term-mode, three steps. First apply planeWave_TTBlochSymbolIs_reduced at integer momentum $m\equiv 0$: this yields that the TT Bloch symbol exists and equals canonicalFiniteH N E 0. Second, unfold the definition of canonicalFiniteH by rfl, writing it as the normalized double sum of flatSlotSqrtDeriv times flatSlotAngleDeriv over PeriodicTet and the six slots. Third, rewrite that value via canonicalFiniteH_zeroMomentum_eq_zero, which supplies canonicalFiniteH N E 0 = 0, and discharge. No new analysis: pure transport of the zero-momentum vanishing into the Gate A2 symbol predicate.
why it matters
This is the zero-mode symbol corollary for the true nonlinear Regge action: lattice flat zero mode stated on the actual second variation, through the Gate A1 existence chain and the Gate A2 reduction. It sits at the end of the hinge-aware zero-mode stack in this module (assembledConstantBlock_eq_zero, canonicalFiniteH_zeroMomentum_eq_zero, then this). Downstream it is referenced inside the module's closing narrative (below), sealing Gate C-A3 of Lane C.
In the broader Recognition gravity program it certifies that the $k=0$ TT sector of the Bloch symbol is exactly the null mode expected of diffeomorphism / flat-background invariance on the discrete torus, rather than a residual of stencil truncation. Axiom disclosure: alone in this file it rides the certified flat-deficit chain, so it inherits Lean.ofReduceBool / Lean.trustCompiler on top of the standard trio. It does not by itself give the continuum graviton propagator or the nonzero-$k$ dispersion; those remain later gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.