target_cell_injection_holds
plain-language theorem explainer
Bundles the cell-injection dichotomy on the forced D=3 eight-vertex cube: every single-vertex bulk flip changes the six-face boundary record, yet the record map has a 16-element kernel of global parity moves, so unrecorded distinctions are only half-cell or larger. Holography and complementarity workers cite it as the machine-checked first step of the entropy-fork program. The proof is a structure constructor packing six already-decided component theorems.
Claim. The target cell-injection property holds on the $D=3$ eight-vertex recognition cell: every single-vertex flip of an $8$-bit bulk configuration changes the six-face boundary record (and exactly the three faces incident to that vertex); the record map is non-injective with kernel size $16$; $|\mathrm{image}|\cdot|\mathrm{kernel}|=256$; and any two distinct configurations with the same boundary record differ in at least four vertices.
background
The module runs the cell-injection test that opens the entropy-fork program: flip one interior bit of the forced $D=3$ cell and ask whether the boundary record must change. The substrate is fixed by the eight-tick octave and $D=3$: the cell is the cube $2^3$ (eight vertices, six faces). A bulk configuration is one recognition bit per vertex, so there are $2^8=256$ states. The boundary record is the six face-closure parities, one per face.
The local theoretical setting is a sharp dichotomy, not a yes/no. Every single bulk flip posts: it changes the record from every base configuration, and it changes exactly the three faces incident to the flipped vertex. Nonetheless the record map is non-injective: its blind set is a rank-$4$ subgroup of $16$ moves (whole-face flips, global complement, inscribed tetrahedra). Blindness is only global: equal records force Hamming distance at least $4$, half the cell; the bound is tight via weight-$4$ face flips.
Rank-nullity at whole-cell grain gives $|\mathrm{image}|=16=2^4$ and $|\mathrm{kernel}|=16=2^4$, so posted cost and fiber degeneracy coincide. The headline upstream fact is that any two distinct same-record configurations differ on at least four vertices, so the record misses nothing local and only a $4$-bit group of cell-global parity moves.
proof idea
Term-mode structure constructor. The target is a bundled proposition whose six fields are filled by already-proved component theorems: single-vertex flips always post; they post on exactly three incident faces; the record map is non-injective; the kernel has cardinality $16$; image size times kernel size equals $256$; and same-record distinct pairs have weight at least $4$. No new reasoning: the proof is the angle-bracket packing of those six results.
why it matters
This is the verify-target discharge for the holography cell-injection loop. Downstream, the certificate handle simply aliases this theorem so the holography stack can gate on #print axioms with a single name.
In the framework it is the first greenlit step of the entropy-fork program: if bulk degeneracy were unrecorded (as in boundary-fiber degeneracy elsewhere), recognition complementarity would stay an axiom; if every bulk distinction posted, complementarity would move toward a theorem. The machine answer is the middle path: nothing local is missed, yet a $4$-bit global kernel remains, so complementarity is constrained rather than settled.
The setup sits on forced landmarks only: the eight-tick octave (period $2^3$) and $D=3$ spatial dimensions, with no extra modeling freedom. At whole-cell grain, posted rank and nullity both equal $4$ and multiply to $256$, separating the per-face / glued-surface entropy fork from the cell-level picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.