target_cell_injection
plain-language theorem explainer
Bundles the six machine-checked claims of the D=3 cell-injection test into one Prop: every single-vertex flip changes the six-face boundary record (on exactly three faces); the record map is non-injective with a 16-element kernel; rank-nullity 16·16=256 holds; and any two configs sharing a record differ in at least four vertices. Downstream certificate and holds theorems cite it. Pure definition packaging already-proved conjuncts.
Claim. The following six statements hold simultaneously: (1) for every 8-vertex cell configuration $c$ and every vertex $i$, flipping bit $i$ changes the six-face boundary record of $c$; (2) that flip alters exactly three of the six face-closure parities; (3) the face-record map is not injective; (4) its kernel has cardinality $16$; (5) $|\mathrm{im}(\mathrm{faceRecord})| \cdot |\ker| = 256$; (6) any two distinct configurations with the same face record differ in Hamming weight at least $4$.
background
The module runs the cell-injection test: flip one interior bit of the forced D=3 cell and ask whether the boundary record must change. The cell is the cube $2^3$ (eight vertices, six faces). A configuration is one recognition bit per vertex, packed as CellCfg = Fin 256. The boundary record is the list of six face-closure parities (one per face), exactly the per-face closed functional on the cell.
Local flip means toggling a single vertex bit. The record kernel is the set of bulk moves invisible to the face record; weight is the Hamming weight of the XOR of two configurations. The module is the first step of the entropy-fork program: if every bulk distinction posts, recognition complementarity moves toward a theorem rather than remaining an axiom.
Upstream pieces used in the bundle are the face-record map, the single-vertex flip, the kernel finset, and the XOR weight on pairs of configurations.
proof idea
Definition only: no proof body. The Prop is the six-way conjunction of already-named sibling results (every local flip posts; every local flip posts on exactly three faces; record map non-injective; kernel card 16; image card times kernel card equals 256; blindness only global with min weight 4). The companion theorem target_cell_injection_holds discharges it by packing those six lemmas into one pair constructor.
why it matters
This is the named verify-target for the holography cell-injection loop. target_cell_injection_holds proves it, and cellInjectionCert re-exports that proof as the #print axioms-gated certificate handle.
In the Recognition framework it records the sharp dichotomy of the D=3 eight-tick cell (T7/T8 substrate): every local bulk flip posts on three incident faces, yet the record map still has a rank-4 blind group of 16 moves (whole-face flips, global complement, inscribed tetrahedra). Blindness is only global (min invisible weight 4). At whole-cell grain, posted rank and fiber nullity coincide at 4 bits; the entropy fork of CoefficientBridge (rank-vs-nullity mismatch per face or domino) is invisible here. The bundle freezes that verdict so the complementarity program can cite one Prop rather than six scattered lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.