record_not_injective
plain-language theorem explainer
The six-face boundary record on the forced D=3 cell fails to separate raw bulk states: distinct 8-bit configurations can share the same face-closure parities. Holography and entropy-fork arguments cite this as the cell-level survival of the paper's countermodel. The proof is a one-line reductio: injectivity would force the all-zero cell to equal its global complement, which it does not.
Claim. The boundary record map on the $D=3$ cell is not injective: if each configuration is an assignment of bits to the eight vertices of the cube $2^3$, and the record is the six face-closure parities, then there exist distinct configurations with identical records.
background
The module runs the cell-injection test on the forced eight-tick cube in $D=3$: eight vertices, six faces, one recognition bit per vertex, so bulk states are the $256$ elements of $\mathrm{Fin},256$. The boundary record is the six-tuple of face-closure parities (the per-face closed functional of the pixel layer), exactly what ledger closure posts for one cell.
The entropy-fork program asks whether every bulk distinction posts. Single-vertex flips do post, but global moves need not. Upstream, the global complement (flip all eight vertices) is record-invisible: each face has four vertices, an even flip count, so every face parity is unchanged. Explicitly, the complement of the zero cell has the same record as the zero cell.
That equality is the countermodel seed: two distinct bulk states, one shared boundary record.
proof idea
Term-mode reductio. Assume the boundary record map is injective. Upstream complement_invisible gives equality of records for the zero cell and its global complement. Injectivity would force those two configurations to be equal. They are not (decidable inequality on the finite type), so absurd closes. No further lemmas: the whole argument is that one equality plus a decide on distinctness.
why it matters
This is clause three of the cell-injection dichotomy in the module header: every local flip posts, yet the record map is still non-injective. Downstream it is packaged into target_cell_injection_holds, the verify-target certificate for the holography loop (with single-flip posting, kernel cardinality, rank-nullity $16\cdot 16=256$, and the global-only blindness bound).
In the framework it sits on T7 (eight-tick octave) and T8 ($D=3$): the substrate is the forced $2^3$ cell, not a free model. The doc-comment states the paper countermodel survives at cell level unless record-equal states are physically identified. That identification question is exactly the fork: if bulk degeneracy stays unrecorded, complementarity remains axiomatic; if every distinction posts, it moves toward a theorem. Here the answer is mixed: local injectivity of flips, global non-injectivity of the full map, with a rank-4 blind subgroup generated by whole-face flips.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.