record_rank_eq_four
plain-language theorem explainer
The six-face boundary record map on the forced 8-vertex D=3 cell has image size 16, so its binary rank is exactly 4 posted bits. Holography and entropy-fork arguments cite this as the rank half of whole-cell rank-nullity. Proof is a pure finite decide over Fin 256.
Claim. Let configurations of the eight-vertex cube carry one bit per vertex. The boundary record is the six-tuple of face-closure parities. Then $\log_2|\{\text{boundary records}\}|=4$, i.e. the image of the record map has cardinality $16=2^4$.
background
CellInjection asks whether a bulk flip on the forced D=3 eight-tick cell must post to the boundary. The cell is the cube $2^3$: eight vertices, six faces, one recognition bit per vertex, so the configuration space has 256 points. The boundary record is the six face-closure parities read on that cell.
The module verdict is a dichotomy: every single-vertex flip changes the record (and exactly the three incident faces), yet the record map is non-injective. Its blind set is a rank-4 subgroup of 16 moves generated by whole-face flips, including the global complement and the two inscribed tetrahedra. Blind pairs differ on at least four vertices; a weight-4 face flip is invisible from every base configuration.
At whole-cell granularity the module states rank-nullity coincidence: image size 16, kernel size 16, and $16\cdot 16=256$. The entropy fork (rank 1 vs nullity 3 per face; rank 2 vs nullity 4 on a domino) appears only after per-face or glued analysis.
proof idea
One-shot finite decision. Configurations and the face-record map are finite and decidable, so decide evaluates $\log_2$ of the cardinality of the image of the record map over the full configuration universe and confirms the value equals 4. No intermediate lemmas are applied; the computation is the certificate.
why it matters
This is the rank half of the cell-level rank-nullity identity in the module doc: $|\mathrm{image}|=16=2^4$ matches $|\mathrm{kernel}|=16=2^4$. Together they show that at whole-cell granularity the four posted bits equal the four free bits, so the entropy fork of CoefficientBridge does not open until faces are split or glued. The substrate is the forced eight-tick octave and $D=3$ (forcing chain T7, T8). Greenlit as the first step of the entropy-fork program (panel holo_bigger_discovery_20260702): if bulk distinctions always post, complementarity moves from axiom toward theorem. No recorded downstream dependents yet; the result is a machine-checked landmark for the holography side of that program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.