single_flip_posts_three
plain-language theorem explainer
A single vertex flip on the forced D=3 eight-vertex cell changes exactly three of the six face-parity records: the three faces incident to that vertex. Holography and entropy-fork arguments cite this for local, quantized bulk-to-boundary posting. The proof is a pure finite decision over all 256 configurations and 8 vertices.
Claim. For every full-cell configuration $c$ (one bit on each of the $8=2^3$ cube vertices) and every vertex index $i\in\{0,\ldots,7\}$, the Hamming distance between the six face-closure parity records of $c$ and of the configuration obtained by flipping only vertex $i$ equals exactly $3$.
background
The module runs the cell-injection test for recognition holography: 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 cube $2^3$ has eight vertices and six faces. A cell configuration packs one recognition bit per vertex into $\mathrm{Fin},256$.
The boundary record is the six-tuple of face-closure parities (one Boolean per face), the per-face closed functional read on all six faces of one cell. Flipping a single vertex bit is the elementary bulk move. Because each vertex lies on exactly three faces of the cube, the geometric expectation is that exactly those three face parities flip; this theorem makes that count machine-checked for every base configuration.
It sharpens the coarser statement that a single flip posts at all (the boundary record changes), by fixing the change to weight three rather than merely nonzero.
proof idea
The statement is a universal claim over two finite types: $256$ configurations and $8$ vertices. The proof is the single tactic decide, which exhaustively evaluates the Boolean equality for every pair $(c,i)$: build the six face records before and after the vertex flip, zip with Boolean inequality, and count the true entries. No intermediate lemmas are invoked; finiteness of the cube and of the face list makes the decision procedure complete.
why it matters
This is clause two of the cell-injection certificate assembled by target_cell_injection_holds: every local bulk flip posts, and it posts with exact weight three. Together with the coarser posting theorem, it shows no single bulk distinction is unrecorded on the boundary.
In the entropy-fork program the dichotomy matters: local flips always post (so complementarity is not forced to stay an axiom by unrecorded single-bit bulk moves), yet the full record map is still non-injective with a rank-4 blind set of global moves (whole-face flips, global complement, inscribed tetrahedra). The exact count three matches cube incidence and makes posting local and quantized rather than diffuse.
Framework landmarks: forced eight-tick cell in $D=3$ (T7, T8). Downstream packaging feeds the holography verify-target loop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.