vertexBits
plain-language theorem explainer
Binary labeling of the eight corners of the unit cube: index a in {0,...,7} maps to the unique triple of Booleans whose binary value is a. Anyone wiring Freudenthal cells, local edges, or Bloch midpoints on the periodic torus cites this table. The body is a pure case split on Fin 8; no proof obligations.
Claim. Define a map from $\{0,\ldots,7\}$ to $\{\mathrm{false},\mathrm{true}\}^3$ by reading the index in binary: $0\mapsto(0,0,0)$, $1\mapsto(1,0,0)$, $2\mapsto(0,1,0)$, $3\mapsto(1,1,0)$, $4\mapsto(0,0,1)$, $5\mapsto(1,0,1)$, $6\mapsto(0,1,1)$, $7\mapsto(1,1,1)$. These triples are the local offsets of the eight vertices of a cube cell.
background
The module builds a typed periodic Freudenthal torus: vertices live on a product of cyclic groups, and each base cell carries a standard cube whose eight corners are labeled by binary triples. Those labels are the local offsets used to walk from a base vertex to its seven neighbors inside the cell.
vertexBits is exactly that labeling table. Index $a\in\mathrm{Fin},8$ is unpacked into three Booleans $(b_x,b_y,b_z)$, so that adding those bits (modulo the torus periods) recovers the geometric corner. Downstream helpers such as addVertexBits and the gravity-side cubeVertexBit simply project or apply this table.
The surrounding theory isolates the scalable periodic model before any concrete finite encoder into Fin nV/Fin nE/Fin nT, so a fixed, machine-checkable cube labeling is the shared coordinate language for edges, tetrahedra, and Regge midpoints.
proof idea
Definition by exhaustive pattern match on Fin 8. Each constructor is assigned the unique Boolean triple whose binary interpretation equals the index. No lemmas, tactics, or obligations; the equation compiler discharges the match.
why it matters
Every local geometric construction on the periodic Freudenthal torus starts from this table. addVertexBits translates a base vertex by the three bits; incidence theorems such as localEdgeOf_endpoints_match_tetVerts compare edge endpoints against tetrahedron vertices built from the same offsets. On the gravity side, cubeVertexBit projects a coordinate, slotMidTwice_eq_geometry equates literal midpoint tables to base bit plus displacement, and edgeMidpointPhase_grounded grounds Bloch phases on those midpoints. Axis-stencil certificates (addVertexBits_translate5, matching base cells) also commute translation past the bit offsets. Without a single shared binary cube labeling, the Regge first-variation and Bloch-assembly pipelines would not share coordinates. The module's remaining open work is the finite encoder into concrete Fin index types; this definition is already closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.