cubeDispBit
plain-language theorem explainer
Projects the i-th Boolean coordinate of a nonzero positive unit-cube displacement labeled by Fin 7. Gravity analysts cite it when wiring Freudenthal edge displacements into local Regge TT slots. The body is a three-way pattern match that unpacks the Bool triple from dispBits.
Claim. For each nonzero positive cube displacement $d \in \{0,\ldots,6\}$ and each spatial index $i \in \{0,1,2\}$, return the $i$-th Boolean component of the displacement triple attached to $d$.
background
The module is the C-DAG1 finite-cell assembly for Regge transverse-traceless modes on a periodic Freudenthal triangulation. Cosine evaluators are built from integer phase keys of Bloch buckets, with wrapping handled by explicit integer-turn phase decomposition.
Upstream, dispBits enumerates the seven nonzero positive cube displacements as triples in $\mathrm{Bool}^3$ (the three axis unit steps and the four face/space diagonals with nonnegative components). The companion bit map sends false/true to $0/1$ when a Boolean must enter an arithmetic formula.
cubeDispBit is the coordinate selector on that table: given a displacement label and a spatial axis, it returns the corresponding Boolean step.
proof idea
Definition by cases on the spatial index in Fin 3. Index 0 returns the first component of dispBits d, index 1 the second, index 2 the third. No lemmas or tactics; pure projection of the upstream triple.
why it matters
Local geometry for the Bloch assembly is built edge-by-edge from Freudenthal cube displacements. Downstream, slotDispBit composes this selector with cubeEdgeDisp and localEdgeOf to read the displacement bit of a tetrahedron-local slot. That bit enters the doubled-midpoint identity slotMidTwice_eq_geometry, which equates the literal midpoint table to twice the base offset plus the actual displacement vector, coordinatewise. Without a clean coordinate projection, the finite-cell cosine fold cannot be matched to the geometric stencil.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.