gaugeStarContrib
plain-language theorem explainer
Per-slot certificate for the decoy-gauge Bloch fold at the special wavevector m⋆: four of the 240 oriented (s,t) pairs contribute −1+√2 and the rest contribute 0. Downstream sums and geometric-match theorems cite it as the closed-form gauge table. The body is a one-line case split on the Nat-kind mask gaugeStarKind.
Claim. For each oriented slot index $s\in\{0,\ldots,23\}$ and triangle index $t\in\{0,\ldots,9\}$, the gauge-star certificate is $-1+\sqrt{2}$ when the pair $(s,t)$ is one of the four marked gauge-active pairs, and $0$ otherwise.
background
This 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 (72 oriented slots per cell, midpoint plane-wave convention). The campaign evaluates the fold at the special momentum $m^\star=(\pi/2,\pi/2,\pi/2,0)$, where every midpoint phase is a natural multiple of $\pi/4$, so each slot term collapses to an integer linear combination of $1$ and $\sqrt{2}$.
The decoy-gauge polarization is the discrete probe used to test residual gauge response at finite momentum. The upstream mask gaugeStarKind flags exactly four pairs $(s,t)\in{(7,6),(10,6),(13,6),(16,6)}$ as kind 1 and all others as kind 0. The present definition turns that Nat mask into the real certificate value that the geometric transported slot term is later shown to match.
proof idea
Pure definitional case split: if the upstream Nat-kind mask equals 1, return $-1+\sqrt{2}$; otherwise return 0. No lemmas are applied.
why it matters
This is the closed-form gauge certificate table at $m^\star$. The sum theorem folds all 240 entries to $-4+4\sqrt{2}$, which is the module's stated closing value for blochFold11 decoyGauge waveStar (nonzero, so discrete gauge invariance at finite momentum holds only up to the finite-difference identity). The geometric-match theorem transportedSlotTerm_gauge_waveStar equates the transported phased slot term on the decoy-gauge load to this certificate, closing the geometric ↔ certificate lane for gauge after the integer slot certificates are decided.
It sits inside the QG full-theory campaign for the (1,1) orbit only. It does not touch the Einstein–Hilbert / TT continuum symbol comparison, nor S_RS_converges_EH_4d, nor gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.