recordKernel_card
plain-language theorem explainer
The kernel of the six-face boundary record on the D=3 eight-vertex cell has exactly 16 elements. Anyone citing the cell-injection dichotomy (every single bulk flip posts, yet the record map is non-injective) needs this cardinality. The proof is a pure finite decision on the explicit Finset of configurations that leave all six face parities fixed.
Claim. The set of bulk bit-configurations of the eight-vertex cube that leave all six face-closure parities unchanged has cardinality $16$.
background
The module runs the cell-injection test on the forced D=3 eight-tick cell: the cube $2^3$ with eight vertices and six faces. A configuration is one recognition bit per vertex, so the configuration space is $\mathrm{Fin},256$. The boundary record is the six face-closure parities (one per face), exactly the per-face closed functional read on a single cell.
The record map sends each configuration to that six-bit face record. Its kernel (the blind set) is the set of bulk moves that leave every face parity unchanged. Module context identifies this set as the rank-4 GF(2) subgroup generated by the six whole-face flips, containing the global complement $255$ and the two inscribed tetrahedra $105={0,3,5,6}$ and $150={1,2,4,7}$.
This sits inside the entropy-fork program: if bulk degeneracy is unrecorded, complementarity stays an axiom; if every bulk distinction posts, complementarity moves toward a theorem. The local setting is forced substrate only (T7 eight-tick octave, T8 $D=3$), with no new modeling freedom.
proof idea
One-line tactic proof: by decide. The kernel is an explicit finite set of configurations in Fin 256, so Lean’s decision procedure enumerates it and checks that its cardinality equals 16. No intermediate lemmas are invoked; the equality is pure finite computation on the already-constructed Finset.
why it matters
This cardinality is one of the six conjuncts packaged by target_cell_injection_holds, the verify-target certificate for the holography loop. Together with the companion facts (single flips always post and change exactly three incident faces; the record map is non-injective; image times kernel equals 256; blindness is only global, differing on at least four vertices), it closes the sharp dichotomy of the cell-injection test.
In framework terms it pins the whole-cell rank-nullity balance: $|\mathrm{image}|=16=2^4$ and $|\mathrm{kernel}|=16=2^4$, so record cost and fiber degeneracy coincide at cell granularity. That coincidence is invisible in the per-face entropy fork of CoefficientBridge (rank 1 vs nullity 3 per face). The result is a machine-checked, axiom-clean step toward deciding whether recognition complementarity is forced or remains axiomatic, on the forced eight-tick $D=3$ cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.