cubeVertexBit
plain-language theorem explainer
Extracts the i-th Boolean coordinate of a binary-labeled cube vertex a in {0,...,7}. Downstream slot and midpoint geometry on the Freudenthal triangulation cite it as the coordinate projection of vertexBits. The body is a three-way pattern match on the Bool triple.
Claim. For each cube vertex label $a \in \{0,\ldots,7\}$ and spatial index $i \in \{0,1,2\}$, return the $i$-th Boolean coordinate of the binary cube offset of $a$ (the three-bit label of that vertex of the unit cube).
background
The module is the C-DAG1 finite-cell assembly stage for Regge transverse-traceless (TT) modes: cosine evaluators are built from integer phase keys on a periodic Freudenthal cell, without continuum certificates.
Upstream, vertexBits assigns to each $a \in \mathrm{Fin},8$ a triple in $\mathrm{Bool}^3$, the standard binary offsets of the eight corners of the unit cube (e.g. $0 \mapsto (F,F,F)$, $1 \mapsto (T,F,F)$, ...). The companion bit map sends false/true to $0/1$ in $\mathbb{N}$.
This definition is the coordinate projection of that triple: given vertex label and axis, it returns the corresponding Boolean. Local tetrahedron slots later read base vertices through the same bits when assembling edge midpoints and wrapped coordinates on the $N\times N\times N$ torus.
proof idea
Definition by cases on the coordinate index. For $i=0,1,2$ it returns the first, second, or third component of vertexBits a respectively. No lemmas; pure destructuring of the Bool triple.
why it matters
Parent uses are local to Regge TT Bloch assembly. slotBaseBit composes it with the base vertex of a local edge in tetrahedron type $t$, slot $f$. The private identity vertCoord_addVertexBits adds the bit (as $0/1$) into a cell coordinate with modular wrap. slotMidTwice_eq_geometry then equates the doubled-midpoint table to twice the base bit plus the geometric displacement, coordinatewise.
That midpoint identity is the bridge from discrete slot tables to the raw cosine Bloch fold (BlochCellSum.cellSum_cos_mul_cos) under non-aliased doubled frequencies. In the broader RS gravity stack this is scaffolding for finite-cell TT mode assembly on the eight-vertex cube that underlies the Freudenthal triangulation in $D=3$, not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.