cell0
plain-language theorem explainer
The empty cell is the all-zero bulk configuration on the forced D=3 cube: eight vertex recognition bits packed as 0 in Fin 256. It is the reference base for the boundary-record kernel, global-complement invisibility, and the gauge relation on cell configurations. Construction is the literal zero of Fin 256, with the membership proof discharged by decide.
Claim. The empty cell is the configuration $0 \in \{0,\ldots,255\}$ on the forced $D=3$ eight-vertex cube, i.e. the unique full-cell state in which every vertex recognition bit is unset.
background
Module CellInjection runs the cell-injection test for the entropy-fork program: flip interior bits 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 cube $2^3$ has eight vertices and six faces, with one recognition bit per vertex.
A full-cell configuration is an element of $\mathrm{Fin},256$, packing the eight bits. Vertex $v\in\mathrm{Fin},8$ has coordinate bits $(v&1,v&2,v&4)$. The boundary record is the six face-closure parities (one per face), the per-face closed functional on the cell.
The empty cell is the zero packing: every vertex bit off. Downstream objects measure records and kernels relative to this base rather than an arbitrary origin.
proof idea
One-line definitional construction: pack the natural number 0 into $\mathrm{Fin},256$ via the subtype constructor, with the bound $0<256$ proved by decide. No lemmas are applied beyond the Fin packing of CellCfg.
why it matters
This constant anchors the holography cell calculus. The record kernel is defined as the Finset of configurations whose face record equals the empty cell's record (all six faces closed); membership is rewritten as equality of face records to that base. The global complement is invisible precisely because its face record equals the empty cell's. In RecordMonotonicity, two configurations are gauge-related iff the XOR of their bits has the empty cell's face record, so gauge classes are the cosets of that 16-element kernel.
In the module verdict, the record map is non-injective with a rank-4 blind set including the global complement and the inscribed tetrahedra; the empty cell is the identity of that kernel group. The geometry side uses the same zero packing when summing over periodic cells solving translated base-vertex equations. Framework landmarks: T7/T8 eight-tick D=3 cell; the entropy-fork question whether bulk degeneracy is unrecorded or every bulk distinction posts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.