slotDispBit
plain-language theorem explainer
Extracts the Boolean displacement bit of a local tetrahedral edge slot along one spatial axis. Gravity analysts cite it when building doubled midpoints and phase keys for the finite Bloch cosine fold on the periodic Freudenthal torus. The body is a thin composition: map the slot to its global edge, read that edge's cube displacement, then take the coordinate bit.
Claim. For tetrahedron type $t\in\{0,\ldots,5\}$, local edge slot $f\in\{0,\ldots,5\}$, and coordinate $i\in\{0,1,2\}$, return the Boolean displacement bit of the corresponding one-cube Freudenthal edge along axis $i$.
background
The module is the C-DAG1 finite-cell assembly stage for Regge TT: a cosine evaluator is built from integer phase keys on a periodic Freudenthal torus, without importing spike or continuum certificates. Local tetrahedral edge slots are indexed by a type $t$ and a face/slot $f$; localEdgeOf chooses a global edge representative in the one-cube triangulation (nineteen edges).
Each such global edge carries a positive displacement code via cubeEdgeDisp (axis or diagonal directions such as $x$, $y$, $z$, $x+y$, \ldots). The sibling cubeDispBit turns that code into a per-coordinate Boolean: whether the edge steps positively in axis $i$. The present definition simply threads the slot through those two maps.
Downstream, the doubled midpoint of a slot is twice the base-offset bit plus this displacement bit, which feeds the integer-turn phase decomposition used to match the raw bucket-fiber Bloch fold.
proof idea
Pure definitional composition, not a proof. Apply the triangulation map from $(t,f)$ to a global edge index, pass that index to the cube-edge displacement table, then project to the Boolean bit in coordinate $i$ via the sibling displacement-bit extractor. No tactics or lemmas are invoked.
why it matters
This bit is the geometric half of the doubled midpoint used throughout the Bloch assembly. Parent definition slotMidTwice sets the midpoint to $2\cdot\mathrm{baseBit}+\mathrm{dispBit}$; the theorem slotMidTwice_eq_geometry then proves that table equals the actual translated edge geometry coordinatewise, which unlocks the integer-turn phase split and cosine periodicity argument in the module doc.
In the broader gravity analysis, correct per-slot displacements are what make the normalized canonical finite value equal the raw bucket-fiber Bloch fold for non-aliased commensurate wave vectors. The construction sits in the discrete $D=3$ Freudenthal scaffolding that the forcing chain (T8) selects as the spatial setting; it does not itself touch J-cost or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.