faceFlip
plain-language theorem explainer
The constant configuration that flips exactly the four vertices of the cube's z=0 face. It is the canonical weight-4 whole-face move used to exhibit base-independent blindness of the boundary record map. Downstream theorems cite it to prove that XORing this pattern never changes the six face-closure parities, and that its Hamming weight is four.
Claim. Let a cell configuration be an element of $\mathrm{Fin}\,256$, packing one bit on each of the $8=2^3$ vertices of the forced $D=3$ cube. Define $\mathrm{faceFlip}$ to be the configuration whose support is exactly the four vertices of the face $z=0$ (vertex indices $\{0,1,2,3\}$), i.e. the integer $15$ as a bit mask.
background
The module runs the cell-injection test for Recognition holography: on the forced eight-tick $D=3$ cell (the cube $2^3$), place one recognition bit per vertex and ask whether bulk flips necessarily change the boundary record. Configurations are packed as CellCfg = Fin 256. The boundary record is the six face-closure parities, one per face of the cube.
Spatial dimension $D=3$ is the forced value from the T8/T9 chain (eight-tick octave, linking). Vertex $v\in\mathrm{Fin},8$ has coordinate bits $(v&1,,v&2,,v&4)$, so the face $z=0$ is precisely the set of vertices with the high bit clear: indices ${0,1,2,3}$.
Whole-face flips generate the kernel of the record map. This constant is the concrete generator for one face; the module later shows the full kernel is a rank-4 subgroup of order 16 built from such moves (plus the global complement and the two inscribed tetrahedra).
proof idea
Pure definitional construction: pack the bit mask $15=2^0+2^1+2^2+2^3$ into Fin 256 via the subtype constructor, with the bound discharged by decide. No lemmas are applied; the value is the configuration with bits $0$--$3$ set and bits $4$--$7$ clear.
why it matters
This constant is the witness that blindness of the cell record is tight and only global. It feeds face_flip_invisible_everywhere (XOR with this move leaves the six face parities unchanged from every base configuration) and faceFlip_weight (Hamming weight exactly 4). Together those results close the dichotomy of the cell-injection test: every single-vertex bulk flip posts, yet the record map has a $16$-element kernel of weight-$\ge 4$ moves, so fiber degeneracy is real but never local.
In the entropy-fork program this separates per-face rank-nullity (CoefficientBridge) from whole-cell behavior, where posted bits and free bits both equal $4$. The move sits on the forced $D=3$ eight-vertex cell from T7/T8; no new modeling freedom is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.