phasedClassDot_zeroMomentum
plain-language theorem explainer
At vanishing Bloch wave covector, the phase-decorated class inner product collapses to the ordinary flat Hessian class pairing. Anyone assembling zero-momentum consistency gates for the (1,1) Regge fold cites this. The proof unfolds the midpoint plane-wave definition and uses cos(0)=1 termwise under the Fin 15 sum.
Claim. For any class weight $v:\{0,\ldots,14\}\to\mathbb{R}$, any $4\times 4$ matrix $H$, and any base point $x\in\mathbb{R}^4$, the phased class pairing of $v$ against $H$ at zero wave covector equals the unphased class pairing: $\mathrm{phasedClassDot}(v,H,0,x)=\mathrm{classDot}(v,H)$.
background
The module builds the exact phase-decorated Bloch fold of the committed true-weight flat Hessian for type-(1,1) triangle hinges in one Kuhn cell. Scope is the (1,1) orbit only (72 oriented slots per cell); it does not yet match the continuum Einstein–Hilbert / TT symbol.
The unphased pairing classDot contracts a 15-component class weight against the flat Hessian class coefficients. The phased version multiplies each class contribution by a midpoint plane-wave factor $\cos(m\cdot x+m\cdot D/2)$, where $D$ is the class displacement and the midpoint convention comes from the edge stencil. Explicitly, phasedClassDot v H m x sums $v_d$ times that cosine-weighted class perturbation over the 15 edge classes.
Zero momentum $m=0$ is the consistency gate: every finite-momentum fold must recover the already-committed zero-momentum orbit quadratic when phases drop.
proof idea
Term-mode proof by definitional reduction. Unfold phasedClassDot, classDot, the coefficient pairing, the plane-wave class perturbation, and the midpoint phase. The two sides become Finset sums over the same 15 classes; Finset.sum_congr reduces to a pointwise goal. At $m=0$ the midpoint phase is identically zero, so Real.cos_zero turns each cosine factor into $1$ and the phased sum collapses to the bare class pairing.
why it matters
This is the elementary phase-drop lemma that every zero-momentum consistency gate in the 4D Regge Bloch campaign rests on. Downstream it feeds factorizedBlochFold11_zeroMomentum (factorized (1,1) fold recovers orbitZeroMomQuadratic .t11), transportedSlotTerm_zeroMomentum, the all-orbit gate factorizedBlochFoldOrbit_zeroMomentum, and the resolved deficit identities phasedDeficitDotResolvedT11_zeroMomentum / T12. It also supports reindexing lemmas in the $m^2$ symbol lane.
In the module's proved list this is the algebraic substrate of item 1 (factorized phased fold at $m=0$ equals the committed orbit quadratic) and the zero-momentum half of item 2 (transported fold bilinearity and phase drop). It does not touch continuum EH recovery or gap_action_recovery; those remain open next-lane goals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.