flipv
plain-language theorem explainer
Bitwise flip of vertex bit i on an 8-vertex D=3 cell configuration packed as Fin 256. Anyone citing the cell-injection test (local bulk flips must change the boundary record) uses this as the elementary bulk move. The body is a one-line XOR with a shifted mask, reduced mod 256.
Claim. For a full-cell configuration $c \in \{0,\ldots,255\}$ (one recognition bit on each of the $8=2^3$ vertices) and a vertex index $i \in \{0,\ldots,7\}$, return the configuration obtained by flipping bit $i$ of $c$.
background
The module studies the cell-injection test on the forced D=3 eight-tick cell: the cube $2^3$ with eight vertices and six faces. A configuration is one recognition bit per vertex, packed as CellCfg = Fin 256. Vertex $v$ has coordinate bits $(v&1, v&2, v&4)$.
The boundary record of a cell is the six face-closure parities (one per face). The entropy-fork program asks whether a bulk distinction is necessarily posted on that record. The elementary bulk move is a single-vertex flip; this definition supplies that move.
No new modeling freedom is introduced: the substrate is the forced eight-tick octave and $D=3$ spatial dimensions from the forcing chain (T7, T8).
proof idea
Definition, not a theorem. Unpack $c$ to its underlying natural, XOR with the single-bit mask $1 \ll i$, reduce modulo 256, and repack as Fin 256 using the standard modulus bound (discharged by decide). Equivalent to toggling bit $i$ in the 8-bit word.
why it matters
This is the bulk generator for the cell-injection bundle. Downstream, single_flip_posts states that for every configuration and every vertex, flipping that vertex changes the face record; single_flip_posts_three sharpens this to exactly the three incident faces. Both are proved by decide over the finite space, quantifying over this flip.
The bundled target target_cell_injection packages those local-posting facts with non-injectivity of the record map and the global-only blindness bound. The module verdict is the dichotomy: every local bulk flip posts, yet the record map still has a rank-4 blind kernel of weight at least 4 (whole-face flips, tetrahedra, global complement). Without a named single-vertex flip, those statements have no move to quantify over.
Framework role: first concrete step of the holography entropy-fork program separating "complementarity as axiom" from "complementarity as theorem" on the forced D=3 cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.