record_nullity_eq_four
plain-language theorem explainer
The whole-cell boundary record map has nullity four: its kernel has size 16, so log base two of that cardinality is exactly 4 free bits. Cite this for the global rank-nullity half of the cell-injection / entropy-fork dichotomy in D=3 holography. Proof is a one-line finite decision on the filtered kernel finset.
Claim. Let $K$ be the set of $8$-vertex cell configurations whose six face-closure parities equal those of the empty cell. Then $\log_2 |K| = 4$ (equivalently $|K| = 16 = 2^4$).
background
The cell-injection module tests whether a bulk flip on the forced D=3 eight-tick cell necessarily changes the boundary record. The cell is the cube $2^3$: eight vertices, six faces. A configuration puts one recognition bit on each vertex, so the configuration space has $256$ elements.
The boundary record is the six face-closure parities. The record kernel is the finset of configurations that share the empty cell's record (all six faces closed); these are the bulk states invisible to the ledger at whole-cell granularity.
Module verdict is a dichotomy: every single-vertex flip posts (and hits exactly the three incident faces), yet the record map is non-injective, with a rank-4 blind set. At whole-cell scale rank equals nullity; the entropy fork appears only per face and under gluing.
proof idea
One-line finite decision. The kernel is the universe of configurations filtered by equality of face records with the empty cell. Lean evaluates Nat.log2 of that finset's cardinality and checks it equals 4, i.e. the kernel has size $16 = 2^4$. No algebraic lemmas; pure decide on a small finite set.
why it matters
Pins the nullity half of the cell record map's rank-nullity identity: $|\mathrm{image}| = 16 = 2^4$, $|\mathrm{kernel}| = 16 = 2^4$, and $16 \cdot 16 = 256$. Doc-comment states the point: at whole-cell granularity rank equals nullity (both four bits); the entropy fork of CoefficientBridge (rank 1 vs nullity 3 per face; rank 2 vs nullity 4 on a domino) is a per-face / glued-surface effect, invisible here.
Together with single-flip posting and the global-only blindness bound, this closes the machine-checked dichotomy of the holography cell-injection test (panel holo_bigger_discovery, first step of the entropy-fork program). Framework landmarks: T7 eight-tick octave and T8 $D=3$ fix the cube substrate; no new modeling freedom. No downstream dependents listed yet; the result is a leaf certificate for the nullity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.