classBit
plain-language theorem explainer
For each of the 15 nonzero Freudenthal edge classes on the 4-cube, reports whether coordinate i belongs to that class's 0/1 displacement. Downstream Regge/Bloch work cites it whenever a class mask must be unpacked into coordinate support (classDisp, midpoint phases, axis-TT coefficients). Definition is a one-line bit test of the class mask.
Claim. Given an edge class $d\in\{0,\ldots,14\}$ and a spacetime coordinate index $i\in\{0,1,2,3\}$, return whether bit $i$ is set in the integer mask $d+1\in\{1,\ldots,15\}$. Equivalently: whether the $i$-th entry of the associated $\{0,1\}^4$ displacement is $1$.
background
The module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style edge classes, namely the nonzero displacement vectors in ${0,1}^4$, indexed by Fin 15 via bit masks. Each class $d$ has mask $d+1\in{1,\ldots,15}$ (maskOf). A spacetime displacement is a 4-vector $(\Delta t,\Delta x_1,\Delta x_2,\Delta x_3)$.
This predicate is the coordinate-wise readout of that mask. It is the Boolean building block behind the 0/1 displacement vector of a class, the squared-length class coefficient $D^T H D$, midpoint phase factors, and the provisional finite TT quadratic aggregate (all-ones weights; true 4D Regge weights remain OPEN).
proof idea
Pure definition: evaluate Nat.testBit on maskOf d at bit position i.val. No lemmas, no tactics; the body is the standard natural-number bit test of the class mask $d+1$.
why it matters
Local primitive for every class-support query in the 4D edge stencil. Downstream, Bloch-fold theorems such as classCoeff_axisTTPlus_mask_1/2/3 simp through it to show axis-TT coefficients vanish on low masks; dispTurns sums the first three bits to count midpoint quarter-turns; waveStar_dot_classDisp reduces the plane-wave dot product to that turn count; M2-symbol phase helpers (phase2Nat, gauge coefficients) read the same bits.
It does not close the OPEN weight problem or the EH-convergence ledger items flagged in the module doc. It only makes the 15-class packaging coordinate-addressable so later exact identities (polarization in $H$, pure-gauge load formula, nonvacuity decoys) can be stated class-by-class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.