CellCfg
plain-language theorem explainer
A full-cell configuration is an element of the 256-point set that packs one recognition bit on each of the eight vertices of the forced D=3 cube. Anyone working the cell-injection or boundary-record lemmas cites this as the ambient type. The declaration is a one-line type abbreviation, not a proved statement.
Claim. A cell configuration is an element of $\mathrm{Fin}\,256$, equivalently an 8-bit string placing one recognition bit on each vertex of the forced $D=3$ cube $2^3$. Vertex $v\in\mathrm{Fin}\,8$ carries coordinate bits $(v\bmod 2,\,\lfloor v/2\rfloor\bmod 2,\,\lfloor v/4\rfloor\bmod 2)$.
background
The 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 configuration places one recognition bit on each vertex. Packing those eight bits into a single natural number below 256 gives a finite type on which every later map (face-closure parity, boundary record, single-bit flip) is decidable by exhaustion.
Upstream geometry supplies the periodic cubic vertex type and a Bool-to-nat bit coercion; here those are specialized to the single 8-vertex cell, with vertex index $v$ decoded by the three low bits $(v&1,v&2,v&4)$.
proof idea
Pure type abbreviation: the name is defined to be $\mathrm{Fin},256$. No proof obligations, tactics, or lemmas are involved.
why it matters
This is the ambient configuration space for the entire cell-injection program. Downstream definitions build the empty cell, the global complement, whole-face flips, per-face closed-loop parities, and the six-component boundary record on top of it. The machine-checked dichotomy (every single-vertex flip posts; the record map still has a rank-4 kernel of weight-at-least-4 moves) is stated entirely in this type.
In the Recognition framework the type encodes the forced eight-tick D=3 cell with no extra modeling freedom. It lets the entropy-fork question (does bulk degeneracy stay unrecorded, or does every bulk distinction post?) be answered by finite decide proofs rather than by axiom. Parent results such as the local-injection theorem, face-flip invisibility, and rank-nullity of the record map all quantify over this 256-element set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.