couplingPhase_zero
plain-language theorem explainer
At vanishing wavevector the Bloch phase of any unit-cell edge-pair coupling is identically zero. Gravity analysts cite this when specializing the exact midpoint Hessian symbol to the zero mode. The proof unfolds the four-term phase sum and cancels by zero-multiplication and empty-sum identities.
Claim. For every unit-cell edge-pair coupling $c$, the phase $\sum_{i=0}^{3} k_i\,\delta_i(c)$ evaluated at the zero wavevector $k\equiv 0$ equals $0$.
background
The module names the Stage-1 unit-cell exact flat Hessian as a finite trigonometric polynomial over a fixed table of 1208 couplings. Each coupling records integer edge increments and a doubled midpoint offset; the associated phase is the real linear form $\sum_{i:F_4} k_i,\delta_i(c)$ on a four-component wavevector.
Zero wavevector is the constant map $k\equiv 0$. The phase definition is a plain Finset sum of products, so the zero-mode evaluation is pure arithmetic: each product vanishes and the sum of zeros is zero. Upstream arithmetic supplies the zero-multiplication lemmas used by simplification.
The broader setting is the exact midpoint Bloch symbol whose centered Tendsto to the cosine two-jet is obtained by specializing a generic trig-polynomial limit through weight/phase wrappers, avoiding Fin-1208 elaboration blowup.
proof idea
Term-mode one-liner after unfold. Expand couplingPhase to the four-term sum $\sum_i k_i\cdot\delta_i(c)$. With $k\equiv 0$ every summand is a zero product; zero_mul and Finset.sum_const_zero finish the goal. No case split on the coupling data is required.
why it matters
Feeds the indexed wrapper couplingPhaseIdx_zero, which lifts the same identity to the CouplingIdx enumeration used by the named Bloch symbol. Zero-mode vanishing is the base case for the exact midpoint symbol at $k=0$ and for the algebraic normalization that recovers the frozen $-1/4$ factor via the norm gate.
In the Recognition gravity stack this sits inside the continuum-symbol Tendsto gate for the 4D Regge exact flat Hessian. The ledger items S_RS_converges_EH_4d and gap_action_recovery remain open; mesh geometric Tendsto is the stated ledger gate. The result itself is pure linear algebra on the phase, independent of those open recoveries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.