slotBaseBit
plain-language theorem explainer
Extracts the i-th Boolean coordinate of the base cube vertex for local tetrahedral edge slot f of type t in the one-cube Freudenthal table. Gravity analysts cite it when building doubled midpoints and periodic wrap counts for the Regge TT Bloch cell sum. The body is a pure composition: map the local slot to its global edge representative, take that edge's base vertex, then read the selected bit.
Claim. For tetrahedron type $t\in\{0,\ldots,5\}$, local edge slot $f\in\{0,\ldots,5\}$, and spatial coordinate $i\in\{0,1,2\}$, return the $i$-th Boolean bit of the base cube vertex of the global Freudenthal edge representative assigned to $(t,f)$.
background
The module is the C-DAG1 finite-cell assembly stage for Regge transverse-traceless modes on a periodic Freudenthal torus. Cosine evaluators are built from integer phase keys; periodic wrapping of local edges is handled by an explicit integer-turn phase decomposition.
A cube vertex is a label in $\mathrm{Fin},8$, decoded into three Boolean coordinates by cubeVertexBit. Each of the 19 one-cube Freudenthal edge representatives has a fixed base vertex cubeEdgeBase. The triangulation table localEdgeOf (from the cube triangulation) sends a tetrahedron type and local slot to one of those 19 global edges.
Composing these three maps yields the base-vertex bit of a local slot without reference to a particular lattice cell. Downstream definitions add the cell translation and displacement bits to obtain midpoints and wrap counts.
proof idea
Definitional composition, not a proof. Resolve the local slot $(t,f)$ to its global edge index via the Freudenthal cube triangulation table, look up that edge's base cube vertex, then project the $i$-th Boolean coordinate of that vertex. No tactics or lemmas are invoked.
why it matters
Supplies the fixed geometric offset that every cell-relative midpoint and wrap count builds on. Downstream, slotMidTwice is twice this base bit plus the displacement bit; slotWrapCount divides the cell coordinate plus this bit by the period $N$; and localEdge_phase_decomposition uses the resulting wrap turns to equate the wrapped edge-midpoint phase to the unwrapped Bloch phase plus a slot phase minus $2\pi$ times integer turns.
That decomposition is the seam-handling step that lets the normalized canonical finite Bloch value equal the raw bucket-fiber fold via BlochCellSum.cellSum_cos_mul_cos, without importing spike or continuum-certificate modules. In the broader RS gravity stack it is pure discrete geometry scaffolding for the finite TT assembly, not a forcing-chain landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.