faceFlip_weight
plain-language theorem explainer
A whole-face flip on the forced D=3 eight-vertex cell has Hamming weight exactly four. Anyone citing the cell-injection dichotomy (blind bulk moves exist, but only at weight at least 4) needs this equality for tightness of the global-blindness bound. The proof is a one-line finite decision check on the concrete configuration.
Claim. Let the bulk configuration space be the $2^3$ cell (eight vertices). If a whole-face flip is the move that toggles all four vertices of one face, then its Hamming weight equals $4$.
background
The CellInjection module runs the first entropy-fork test on the forced substrate: the D=3 eight-tick cell is the cube $2^3$ (eight vertices, six faces), with one recognition bit per vertex, so configurations are elements of a 256-point space. The boundary record is the six face-closure parities posted by ledger closure.
Weight is the Hamming weight of a bulk move (number of vertices flipped). A whole-face flip toggles the four vertices of one face; the module treats these moves as the generators of the record kernel. The local setting is pure finite combinatorics on the forced cell: no continuum modeling freedom, all checks by decide.
Upstream scaffolding in the holography stack only supplies the cell and record primitives; this equality is definitional bookkeeping for the weight-4 tightness claim stated in the module verdict (blind pairs differ on at least half the cell).
proof idea
One-line finite decision proof. After weight and the concrete whole-face flip configuration are defined, decide evaluates the Hamming weight on the eight-bit string and closes the equality to 4. No intermediate lemmas, rewrites, or case splits appear in the proof term.
why it matters
Pins the numerical half-cell bound in the cell-injection verdict: every single-vertex flip posts (three incident face records change), yet the record map is non-injective with a rank-4 kernel of 16 moves generated by whole-face flips. The module states the bound is tight precisely because a whole-face flip has weight 4 and is invisible from every base configuration.
That tightness separates two futures for recognition complementarity: bulk degeneracy is real, but only global (at least four vertices). At whole-cell grain, posted rank and fiber nullity both equal 4, matching the eight-tick / D=3 forced cell (T7, T8). No downstream dependents are wired yet in the graph; the result is local support for the entropy-fork program rather than a bridge lemma into later modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.