rawCellStencil_zeroMomentum
plain-language theorem explainer
At vanishing integer wave vector, the raw cell stencil equals twice the per-cell assembled constant block, for every positive torus side N and every real 3x3 polarization matrix. Regge TT analysts cite it to collapse the k=0 stencil sum to a pure per-cell object before invoking the zero-mode headline. The proof factors each term at zero momentum, extracts N^3 identical cell copies, and cancels the 2/N^3 normalization against that volume.
Claim. For every positive integer torus side $N$ and every real $3\times 3$ polarization matrix $E$, the raw cell stencil at the zero integer wave vector equals twice the per-cell assembled constant block of $E$.
background
This module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1, Lane C): the hinge-aware zero mode of the Regge TT symbol. The raw cell stencil sums Jacobian-weighted products of polarization edge coefficients over all periodic tetrahedra on the $N^3$ spatial torus. At zero integer wave vector the commensurate-momentum phase is trivial and the plane-wave tet velocities collapse, so each stencil term reduces to a pure product of a raw Jacobian coefficient with two edge-class polarization factors.
The assembled constant block is the Schlaefli-reduced per-cell $k=0$ contribution that survives after the Gate A2 reduction of the finite Hamiltonian. The module's zero-mode headline asserts that this assembled block vanishes for every polarization; the present identity isolates the volume-normalization step that converts the full torus sum into that per-cell object, leaving an explicit factor of $2$.
proof idea
Unfold the raw cell stencil. First prove a pointwise term identity: at zero momentum every stencil term equals the product of the raw Jacobian coefficient with the two polarization edge coefficients, via the zero-momentum lemmas for commensurate momentum and plane-wave tet velocity, followed by ring.
Reindex the triple sum over periodic tets as a sum over vertices times tet types. Substitute the term identity, pull out Fintype.card(Vertex) = N^3 identical copies of the remaining triple sum over tet type and edge pairs, and match the definition of the assembled constant block. The leftover scalar identity $(2/N^3)\cdot(-(N^3 S))=2\cdot(-S)$ is discharged by field_simp after a positivity check that $N^3\neq 0$.
why it matters
Sole downstream consumer is canonicalFiniteH_zeroMomentum_eq_zero, which rewrites the A2-reduced finite Hamiltonian as the raw cell stencil, applies this identity, then multiplies by the already-proved vanishing of the assembled constant block to conclude that the canonical finite value at zero integer wave vector is identically zero for every $N$ and every polarization.
That vanishing is the algebraic half of Gate C-A3. Combined with the hinge-cancellation theorems in the same module (hinge block equals the recorded stencil-only residual at the TT witness, assembled = hinge minus residual), it converts the sympy diagnostic observation that the assembled quadratic vanishes at $k=0$ into a kernel theorem with no free sign convention. It does not itself touch the forcing chain T0-T8; its role is local to the Regge TT gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.