cellInjectionCert
plain-language theorem explainer
Certificate alias asserting the full cell-injection bundle on the forced D=3 eight-tick cube: every single-vertex bulk flip changes the six-face boundary record (exactly three faces), yet the record map is non-injective with a 16-element blind group of minimum weight 4, and rank-nullity holds (|image|·|kernel|=256). Holography and complementarity auditors cite it as the #print-axioms gate for the entropy-fork program. Proof is a one-line term alias of the packed witness theorem.
Claim. The cell-injection target holds: for every configuration $c\in\{0,1\}^8$ and every vertex $i$, flipping bit $i$ changes the six-face boundary record, and changes exactly three face parities; the face-record map is not injective; its blind set has cardinality $16$; $|\mathrm{im}|\cdot|\ker|=256$; and any two configurations with the same record differ in at least four vertices.
background
The module studies the forced 8-tick cell in $D=3$: the cube $2^3$ with eight vertices and six faces. A configuration is one recognition bit per vertex (CellCfg, cardinality 256). The boundary record is the six face-closure parities (faceRecord), one per face, read from the per-face closed functional.
The entropy-fork program asks whether bulk distinctions necessarily post to the ledger. The cell-injection test flips one interior vertex bit and checks whether the boundary record must change. Module verdict is a dichotomy: every local flip posts (exactly three incident faces), yet the global record map is non-injective, with blindness only at weight $\ge 4$ (whole-face flips and a rank-4 kernel of size 16).
Upstream, target_cell_injection packages those conjuncts into one Prop; target_cell_injection_holds assembles the machine-checked witnesses (single_flip_posts, single_flip_posts_three, record_not_injective, kernel/image cardinality, and record_blind_only_global).
proof idea
One-line term proof: the certificate is definitionally the already-proved packed witness target_cell_injection_holds. That witness is itself a six-component constructor packing single_flip_posts, single_flip_posts_three, record_not_injective, recordKernel_card, record_image_times_kernel, and record_blind_only_global. No new reasoning occurs at this declaration.
why it matters
This is the verify-target certificate handle for the holography loop, meant to be #print axioms-gated so the cell-injection bundle can be cited as a single closed unit. It sits at the first greenlit step of the entropy-fork program (panel holo_bigger_discovery): if every bulk flip posts, recognition complementarity moves from axiom toward theorem; if some bulk degeneracy is unrecorded, complementarity stays axiomatic.
Framework landmarks: the substrate is the forced eight-tick octave in $D=3$ (T7, T8). The dichotomy sharpens complementarity relative to boundary-fiber degeneracy elsewhere (e.g. record-cost asymmetry). No downstream dependents are wired yet; the cert is the export surface for later holography and CoefficientBridge rank-nullity comparisons at whole-cell granularity, where posted bits and fiber degeneracy both equal 4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.