waveStar
plain-language theorem explainer
Special finite-momentum wave vector m⋆ = (π/2, π/2, π/2, 0) on the 4D Brillouin torus, used as the certificate evaluation point for the type-(1,1) Regge Bloch fold. Anyone citing the closing axis-TT or decoy-gauge fold values at nonzero momentum references this point. Defined by four coordinate cases; no proof content.
Claim. The distinguished wave vector $m^\star \in \mathbb{R}^4$ is $m^\star = (\pi/2,\,\pi/2,\,\pi/2,\,0)$, i.e. three spatial half-turns and vanishing temporal component.
background
The module carries out the exact phase-decorated Bloch fold of the committed true-weight flat Hessian for type-(1,1) triangle hinges in one Kuhn cell, under the midpoint plane-wave convention of the 4D Regge edge stencil. Scope is the (1,1) orbit only (72 oriented slots per cell).
A wave vector $m \in \mathbb{R}^4$ enters the fold through midpoint phases on hinge base points and class displacements. At generic $m$ those phases are transcendental; the special point $m^\star$ forces every midpoint phase to a natural multiple of $\pi/4$, so each slot term collapses to an element of $\mathbb{Z}[\sqrt{2}]/8$ and becomes decidable by integer arithmetic.
Downstream certificate algebra (Nat-kind axis and gauge tables) and the geometric-to-certificate match are all evaluated at this single momentum.
proof idea
Pure definition by pattern match on Fin 4: coordinates 0,1,2 are Real.pi / 2 and coordinate 3 is 0. No lemmas, no tactics.
why it matters
This is the evaluation point for the module's closing theorems. blochFold11_axisTTPlus_waveStar states the honest transported (1,1) Bloch fold on the axis TT polarization at $m^\star$ equals $-3$ (nonzero, nonvacuity). blochFold11_decoyGauge_waveStar gives the pure-gauge probe value $-4 + 4\sqrt{2}$ (nonzero: discrete gauge invariance at finite momentum holds only up to the finite-difference identity).
It also feeds classMidpointPhase_waveStar (midpoint phase equals quarter-turns times $\pi/4$), the integer slot-term evaluations, and the geometric-certificate match on all 240 oriented slots. Within the QG full-theory campaign this closes the finite-momentum certificate lane for the (1,1) orbit; it does not yet compare the $m^2$ Taylor coefficient to the Einstein-Hilbert / TT continuum symbol, nor flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.