vbit
plain-language theorem explainer
Extracts the recognition bit on vertex i of an 8-vertex D=3 cell configuration packed as Fin 256. Anyone reading face-closure parities, Hamming weight, or single-vertex flips on the cube cites this accessor. The body is a one-line Nat.testBit on the underlying natural.
Claim. Given a full-cell configuration $c \in \{0,\ldots,255\}$ (one bit per vertex of the forced $2^3$ cube) and a vertex index $i \in \{0,\ldots,7\}$, the vertex bit is the $i$-th binary digit of $c$: $\mathrm{vbit}(c,i) = \mathrm{testBit}(c,i) \in \{\mathrm{true},\mathrm{false}\}$.
background
The CellInjection module runs the cell-injection test: flip one interior bit of the forced D=3 cell and ask whether the boundary record must change. The substrate is fixed by the forcing chain (T7 eight-tick octave, T8 D=3): the cell is the cube $2^3$ with eight vertices and six faces.
A cell configuration packs one recognition bit on each vertex into Fin 256. Vertex $v$ has coordinate bits $(v&1, v&2, v&4)$. The boundary record is the six face-closure parities (even XOR on the four vertices of each face), exactly the per-face closed-loop condition of the pixel ledger.
This accessor is the bit-level interface to that packing. Sibling face- and domino-level modules use the same pattern on Fin 16 and Fin 64.
proof idea
Pure definition, not a theorem. Unpack the Fin 256 value of the configuration and read bit $i$ via Nat.testBit on the underlying natural and the Fin 8 index. No lemmas, no tactics.
why it matters
Primitive for the entire cell-injection stack. Downstream, face ledger-closure (closedOn) is the negated four-bit XOR of these vertex bits; Hamming weight counts how many are set; single-flip posting theorems and the rank-nullity analysis of the record map all read configurations through it.
Parallel accessors on the unit face and glued domino reuse the same bit-test pattern, so face, plaquette, and cell layers share one vocabulary. In the entropy-fork program this is the bulk side of the dichotomy: every local bulk flip posts on the boundary, yet the record map still has a rank-4 kernel of global moves. Without a stable vertex-bit read, none of those decide-checked statements type-check.
Framework landmarks: T7 (eight-tick / $2^3$ cell) and T8 (D=3) fix the eight indices; the ledger-closure reading is the holographic posting that the injection test audits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.