transportedSlotTerm_waveStar_eval
plain-language theorem explainer
At the star wave vector $m^\star=(\pi/2,\pi/2,\pi/2,0)$, every transported slot contribution in the type-(1,1) Regge Bloch fold equals an integer certificate $(N_1+N_2\sqrt{2})/8$. Analysts matching geometric folds to discrete Nat-kind tables cite this master evaluation. The proof cases on the (1,1) hinge predicate, rewrites phased amplitude and kernel at $m^\star$, then clears $\sqrt{2}$ by linear combination.
Claim. Let $H$ be a $4\times 4$ real matrix whose fifteen class coefficients equal integers $c_z(d)$. For every oriented slot $(s,t)$ with $s\in\{0,\ldots,23\}$ and $t\in\{0,\ldots,9\}$, the transported slot term of $H$ at the star wave vector $m^\star=(\pi/2,\pi/2,\pi/2,0)$ equals $\bigl(N_1(c_z,s,t)+N_2(c_z,s,t)\sqrt{2}\bigr)/8$, where $N_1,N_2$ are the integer certificate components of that slot.
background
This module runs the QG full-theory campaign for the exact phase-decorated Bloch fold of the committed true-weight flat Hessian on type-(1,1) triangle hinges in one Kuhn cell, under the midpoint plane-wave convention of the 4D edge stencil. Scope is the (1,1) orbit only: 72 oriented slots per cell.
A transported slot term is the phased contribution of one oriented hinge slot after midpoint-phase decoration at a finite wave vector. The star point $m^\star=(\pi/2,\pi/2,\pi/2,0)$ is special: every midpoint phase is a natural multiple of $\pi/4$, so each slot lands in the $\mathbb{Z}[\sqrt{2}]$ lattice scaled by $1/8$. The predicate isT11 marks slots whose hinge orbit type is exactly $(1,1)$; non-$(1,1)$ slots drop out of this fold.
Upstream, the phased amplitude and kernel evaluations at $m^\star$ already reduce to integer combinations of the class coefficients of $H$. The integer certificate pair $(N_1,N_2)$ packages those reductions into a single closed form.
proof idea
Unfold the transported slot term and the two certificate components. Case on whether the slot is type $(1,1)$.
On the $(1,1)$ branch: simplify the conditional, rewrite the phased amplitude and kernel via the star evaluations (which insert the integer class coefficients of $H$), use $\sqrt{2}\cdot\sqrt{2}=2$, push casts, and finish by a linear combination that absorbs the cross term into the $(N_1+N_2\sqrt{2})/8$ shape.
On the complementary branch: both sides simplify to zero (non-$(1,1)$ slots contribute nothing to this fold).
why it matters
This is item 5 of the module's proved list: the integer Bloch symbol at $m^\star$. It is the algebraic bridge from geometric transported terms to decidable integer certificates.
Two immediate parents close the geometric $\leftrightarrow$ certificate match: the axis match equates every axis-TT-plus slot at $m^\star$ to its Nat-kind table entry, and the gauge match does the same for the decoy gauge. Both rewrite through this evaluation, then apply the decided $N_1,N_2$ table equalities.
Those matches yield the closing values of the full (1,1) Bloch fold at $m^\star$: $-3$ on axis-TT-plus (nonvacuity) and $-4+4\sqrt{2}$ on the decoy gauge (finite-momentum discrete gauge identity). The module explicitly does not yet compare the $m^2$ Taylor coefficient to the Einstein–Hilbert / TT continuum symbol, nor flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.