recordKernel
plain-language theorem explainer
The record kernel is the set of bulk cell configurations whose six face-closure parities match the empty cell. These are the record-invisible states: bulk patterns the boundary ledger cannot distinguish from vacuum. Anyone citing the cell-injection dichotomy, rank-nullity of the face-record map, or the 16-element blind group uses this fiber. It is defined by filtering all 256 configurations for equality of face records with the empty cell.
Claim. The record kernel is the finite set of all cell configurations $c$ (one bit on each of the eight vertices of the $D=3$ cube) such that the six face-closure parities of $c$ equal those of the empty configuration. Equivalently, it is the fiber of the boundary-record map over the empty-cell record (all six faces closed).
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 full-cell configuration packs one recognition bit per vertex into an element of $\mathrm{Fin},256$. The empty cell is the zero configuration.
The boundary record of a configuration is the list of six face-closure parities, one per cube face (axis and side). Each parity is the closed-on functional on the four vertices of that face. This is everything the ledger posts at the cell boundary.
The local question is whether bulk distinctions necessarily change that record. The module answers with a dichotomy: every single-vertex flip posts, yet the record map is non-injective, with a nontrivial fiber over the empty record. That fiber is the object defined here.
proof idea
Pure definition, not a proof. Take the universe of all 256 cell configurations and retain those whose face-record list equals the face-record list of the empty cell. No lemmas are applied; the filter is the entire body.
why it matters
This set is the blind fiber that makes the cell-injection dichotomy precise. Downstream, its cardinality is 16 (nullity four free bits), it equals the explicit rank-4 GF(2) group generated by whole-face flips (including the global complement and the two inscribed tetrahedra), and the first-isomorphism check $|\mathrm{image}|\cdot|\mathrm{kernel}|=256$ uses it directly.
Shift-invariance classifies unrecorded moves exactly as membership in this kernel: a displacement is invisible from every base if and only if it lies here. The bundled cell-injection target packages non-injectivity of the record map together with local posting and the global-only blindness bound, all resting on this definition.
In the Recognition framework this sits inside the holography / entropy-fork program on the forced $D=3$ eight-tick cell (T7, T8). At whole-cell grain, posted rank and fiber nullity coincide at four bits; the fork that splits rank versus nullity appears only per face and under gluing. Complementarity remains an axiom if bulk degeneracy can stay unrecorded; this kernel is the concrete measure of that residual degeneracy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.