sum_gaugeStarContrib
plain-language theorem explainer
The double sum of decoy-gauge star contributions over the 24×10 index range equals $-4+4\sqrt{2}$. Anyone citing the finite-momentum gauge verdict for the (1,1) Regge Bloch fold at the star wavevector needs this certificate. The proof factors the constant $-1+\sqrt{2}$ out of an indicator sum and applies a Nat count that exactly four slots have kind 1.
Claim. The sum of decoy-gauge star contributions over all $s\in\{0,\ldots,23\}$ and $t\in\{0,\ldots,9\}$ equals $-4+4\sqrt{2}$.
background
This sits in the Regge 4D finite-momentum Bloch-fold campaign for type-(1,1) triangle hinges in one Kuhn cell. The module builds a phase-decorated fold of the committed true-weight flat Hessian under the midpoint plane-wave convention, restricted to the 72 oriented slots of the (1,1) orbit.
At the star momentum $m^\star=(\pi/2,\pi/2,\pi/2,0)$, every midpoint phase is a natural multiple of $\pi/4$, so slot terms become integer certificates in $\mathbb{Z}[\sqrt{2}]$. The decoy-gauge probe is the pure-gauge direction used to test discrete gauge invariance at finite momentum. Each star contribution is either zero or the constant $c=-1+\sqrt{2}$, selected by a Nat-valued kind table on the $(s,t)$ pairs.
The module's certificate-algebra block records that the gauge table at $m^\star$ sums to $-4+4\sqrt{2}$; this theorem is that sum identity.
proof idea
Unfold the star contribution so each summand is the indicator if kind$(s,t)=1$ then $c$ else $0$ with $c:=-1+\sqrt{2}$. Rewrite the indicator as $c$ times a $0/1$ mask, pull $c$ out of the double sum, and reduce to counting how many pairs have kind $1$. That count is the Nat lemma gaugeStarKind_count1, cast to $\mathbb{R}$ and equal to $4$. Substitute and finish by ring: $4(-1+\sqrt{2})=-4+4\sqrt{2}$.
why it matters
Parent closing theorem blochFold11_decoyGauge_waveStar applies this sum after rewriting every transported gauge slot term at $m^\star$ via the geometric-certificate match. Its doc-comment states the gauge verdict: the fold on the pure-gauge probe equals $-4+4\sqrt{2}$ (nonzero), so discrete gauge invariance at finite momentum holds only up to the finite-difference identity.
In the module checklist this is item 4 (certificate algebra) feeding item 7 (closing values). It does not touch continuum Einstein-Hilbert matching, $S_{\mathrm{RS}}$ convergence, or gap-action recovery; those remain separate lanes. Within Recognition gravity analysis it is the exact algebraic certificate that the decoy-gauge Bloch symbol is a concrete nonzero element of $\mathbb{Q}(\sqrt{2})$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.