phasedDeficitDotResolvedT12_zeroMomentum
plain-language theorem explainer
At vanishing Bloch wavevector the type-(1,2) position-resolved phased deficit cross-term collapses to an unphased sum of four star-member class dots against the strain matrix. Analysts of the exact flat Regge Hessian symbol on the Freudenthal torus cite this as the zero-momentum member-drop for the t12 orbit. The proof unfolds the resolved symbol and applies the zero-momentum class-dot lemma under a four-term sum congruence.
Claim. For any real $4\times 4$ matrix $H$, any strain wave $x:\mathbb{R}^4\to\mathbb{R}$, and any edge index $p\in\{0,\ldots,23\}$, the type-$(1,2)$ position-resolved phased deficit cross-term evaluated at zero Bloch momentum equals $\sum_{\mu=0}^{3}\mathrm{classDot}(\mathrm{pushforwardClass}(S_\mu,p),H)$, where $S_\mu$ is the $\mu$-th assembled star member of the type-$(1,2)$ hinge kernel.
background
The module fixes the exact flat cross-term continuum symbol for 4D Regge calculus on the Freudenthal torus. At flat background, deficits vanish, so Schläfli reduces the Hessian to $S''=\sum_h(dA_h)(d\delta_h)$. Plane-wave class strains are phased by cube offsets: type-$(1,1)$ keeps star-member cube offsets, while type-$(1,2)$ (and t13/t22) uses per-edge transported origins from the star-edge-origin layer.
Here $H$ is a $4\times 4$ real matrix (class strain) and $x$ is a four-component wave amplitude. The second argument of the resolved symbol is the Bloch wavevector; setting it to the zero function is the zero-momentum specialization. The right-hand side sums class dots of the four pushforwards of the type-$(1,2)$ star-kernel members at edge $p$.
Upstream structural support includes the cost reparametrization $H=J+1$ (RCL as d'Alembert) and the closed N=5 Freudenthal signed-deficit lift; those pin the geometric bookkeeping this lemma inherits, not the algebraic step itself.
proof idea
Unfold phasedDeficitDotResolvedT12 to expose the four-term sum over star members $\mu$. Apply Finset.sum_congr with a trivial index equality, reducing to one member at a time. On each summand, invoke phasedClassDot_zeroMomentum at the pushforward class of the assembled type-$(1,2)$ star member, the matrix $H$, and the transported wave $i\mapsto x_i+\mathrm{transportOffset}(p,\mathrm{cubeOffsetT12}(\mathrm{starMemberCubeT12},\mu))_i$. Simp closes the residual equality: zero momentum kills the phase, leaving the bare class dot.
why it matters
This is one of the structural THEOREM-tier lemmas named in the module doc: homogeneity and zero-momentum member drop for the exact flat cross-term fold. It discharges the t12 half of the zero-momentum specialization that continuum-symbol preflight and the banked TT certificates (axisTTPlus / symbolDir with value $-1/4$) rely on when the Bloch wavevector is set to zero.
No downstream Lean users are wired yet (used_by empty), so the lemma presently anchors the honesty section rather than a named parent theorem. It does not close the residual e0 isotropy of the fold face, nor FoldAlongM2Tendsto / ContinuumSymbolIs for all modes, nor ledger $S_{RS}$ inhabit. Those remain OPEN as flagged in the module. Framework-wise it sits inside the gravity analysis stack that supports $D=3$ spatial geometry and the eight-tick discrete bookkeeping, but it is a local Regge-Hessian identity, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.