dispTurns
plain-language theorem explainer
Counts how many of the three spatial mask bits are set for a Regge edge class d in Fin 15. That integer is the midpoint quarter-turn contribution of the class displacement at the special wave vector m⋆ = (π/2, π/2, π/2, 0). Downstream Bloch-fold algebra cites it to convert plane-wave dots into Nat multiples of π/4. The body is a three-term Boolean sum over classBit.
Claim. For each edge class $d \in \{0,\ldots,14\}$, define $\mathrm{dispTurns}(d) \in \mathbb{N}$ as the number of set bits among coordinates $0,1,2$ in the $0/1$ displacement mask of $d$ (equivalently, $\sum_{i=0}^{2} \mathbf{1}_{\mathrm{bit}\,i\,\mathrm{set}}(d)$). The time bit is omitted.
background
The module carries out an 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 Regge edge stencil. Scope is the (1,1) orbit only (72 oriented slots per cell); continuum $m^2$ matching and full EH recovery are explicitly out of lane.
Edge classes are indexed by Fin 15. Each class has a 4-bit mask; classBit d i asks whether coordinate $i$ is set in that $0/1$ displacement. The special momentum used for certificate algebra is $m^\star=(\pi/2,\pi/2,\pi/2,0)$. Eight-tick phases are multiples $k\pi/4$, so integer quarter-turn counts are the natural bookkeeping for midpoint phases.
Because $m^\star_3=0$, only spatial bits contribute to the plane-wave dot $m^\star\cdot\mathrm{classDisp}(d)$. This definition isolates that spatial popcount.
proof idea
Pure definition: sum three Boolean-to-Nat indicators for classBit d 0, classBit d 1, and classBit d 2. No lemmas, no tactics. The fourth coordinate is intentionally dropped to match $m^\star_3=0$.
why it matters
Feeds the total midpoint quarter-turn count quarterTurns s t d := 2·baseTurns s t + dispTurns d, which packages hinge base phase with class displacement phase at $m^\star$. Also drives the private identity waveStar_dot_classDisp: $\sum_i m^\star_i,(\mathrm{classDisp},d)_i = \mathrm{dispTurns}(d)\cdot(\pi/2)$, proved by unfolding this sum and case-splitting the three bits.
Those integers underwrite the module's certificate algebra: every midpoint phase at $m^\star$ is a natural multiple of $\pi/4$, so each transported slot term is of the form $(N_1+N_2\sqrt{2})/8$ with decidable integers. That is the bridge from geometric fold to the closed values blochFold11 axisTTPlus waveStar = -3 and the gauge fold $-4+4\sqrt{2}$.
In the broader RS gravity campaign this is bookkeeping inside the finite-momentum (1,1) Bloch fold, not a forcing-chain step; it supports discrete gauge and TT nonvacuity certificates at finite momentum without claiming continuum EH recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.