cellComplement
plain-language theorem explainer
The all-ones bulk configuration on the forced D=3 cell: every one of the eight cube vertices carries a flipped recognition bit (value 255 in the Fin 256 packing). Holography and entropy-fork arguments cite it as the global generator of the record kernel. The definition is the literal packed integer with a decide proof of the Fin bound.
Claim. Let a cell configuration be an assignment of one bit to each of the eight vertices of the cube $2^3$, packed as an element of $\{0,\ldots,255\}$. The global complement is the configuration in which every vertex bit is $1$, i.e. the packed value $255$.
background
The CellInjection module tests whether bulk distinctions on the forced eight-tick D=3 cell necessarily post to the boundary. A cell configuration packs one recognition bit per cube vertex into Fin 256; 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 of the cube.
The module's machine-checked dichotomy is that every single-vertex flip changes the record, yet the record map is still non-injective: its kernel is a rank-4 subgroup of sixteen moves generated by whole-face flips, including the global complement and the two inscribed tetrahedra. Blind pairs differ on at least four vertices.
This constant is exactly that global complement: the configuration obtained by flipping all eight vertex bits relative to the zero cell.
proof idea
Pure definitional construction. The value is the packed integer 255 (binary eight ones), wrapped as a CellCfg term; the Fin 256 bound is discharged by decide. No lemmas are applied.
why it matters
Feeds the theorem that the global complement posts nothing: flipping all eight vertices leaves every face parity unchanged, because each face has four flipped vertices (even). That fact is the first concrete witness that the boundary record map is not injective on raw bulk states, so the holography countermodel survives at cell level unless record-equal states are identified.
In the entropy-fork program this sits inside the rank-nullity balance at whole-cell granularity ($|\mathrm{image}|=16=2^4$, $|\mathrm{kernel}|=16=2^4$). The kernel is generated by whole-face flips; the global complement is the all-faces product. The forced substrate is the T7 eight-tick octave and T8 D=3 cube, with no extra modeling freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.