record_image_card
plain-language theorem explainer
The boundary-record map on the forced D=3 eight-vertex cell hits exactly 16 distinct records, i.e. four posted bits. Anyone citing the cell rank-nullity or the holographic bound on physical states needs this cardinality. The proof is a pure finite decision: image the 256 configurations under the six face-parity map and count.
Claim. Let a cell configuration be one bit on each of the $8=2^3$ vertices of the forced $D=3$ cube (so there are $256$ configurations). Let the boundary record of a configuration be the six face-closure parities. The image of the full configuration set under this record map has cardinality $16=2^4$.
background
The module runs the cell-injection test for recognition holography on the forced eight-tick $D=3$ cell (cube $2^3$: eight vertices, six faces). A configuration CellCfg packs one recognition bit per vertex into Fin 256. The ledger posts only the boundary record: six face-closure parities, one per cube face, each the XOR-style closed functional on the four vertices of that face.
The module verdict is a dichotomy: every single-vertex bulk flip changes the record, yet the record map is still non-injective. Its blind set is a rank-4 GF(2) subgroup of size 16 (whole-face flips, global complement, and the two inscribed tetrahedra). Rank-nullity at whole-cell grain then reads $|\mathrm{image}|=16=2^4$ and $|\mathrm{kernel}|=16=2^4$, with product $256$.
This declaration isolates the image half of that count: how many distinct six-bit face records actually occur.
proof idea
One-line term proof by decide. Lean exhaustively evaluates Finset.univ.image faceRecord over the finite type CellCfg = Fin 256 and checks that the resulting finset has cardinality 16. No intermediate lemmas are invoked; the computation is the argument.
why it matters
This is the image side of the cell rank-nullity package in the entropy-fork / holography program: four posted bits at whole-cell grain, matching the four free kernel bits. Downstream, physState_records_card re-exports it as "16 posted records = 16 physical states = 4 posted bits" and feeds the holographic bound under weak complementarity (physical states embed into the posted-record set, strictly inside the naive 6-bit boundary).
In framework terms it sits on the forced $D=3$ eight-tick cell (T7/T8 landmarks): bulk distinctions that survive as single flips always post, but global rank-4 blindness remains, so complementarity is not yet a pure injectivity theorem. The coincidence of record cost and fiber degeneracy at cell scale contrasts with the per-face / domino entropy fork (rank 1 vs nullity 3; rank 2 vs nullity 4), which is invisible at this granularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.