record_image_times_kernel
plain-language theorem explainer
Rank-nullity identity for the D=3 cell boundary record: the number of distinct six-face parity records times the size of the invisible kernel equals the full bulk configuration space, 16 · 16 = 256. Cited by anyone assembling the cell-injection dichotomy or the holography entropy-fork certificate. Proof is a pure finite decision on Finset cardinals.
Claim. Let the bulk configuration space be all assignments of one bit to each of the eight cube vertices ($2^8 = 256$ states). Let $R$ map each configuration to its six face-closure parities, and let $K$ be the fiber of the empty-cell record. Then $|\mathrm{im}(R)| \cdot |K| = 256$.
background
The CellInjection module tests whether a bulk flip on the forced D=3 eight-tick cell necessarily posts to the ledger boundary. Configurations are one recognition bit per cube vertex, so the domain is $2^8 = 256$ states. The boundary record is the six face-closure parities (one per cube face), each the XOR/parity of the four vertices on that face; that is everything ledger closure posts at the cell boundary.
The record kernel is the set of configurations that share the empty cell's boundary record (all six faces closed): the record-invisible states. Upstream, single-vertex flips always change the record and hit exactly the three incident faces, so local bulk distinctions are never silent. The residual non-injectivity is therefore a global phenomenon whose size this identity measures.
Module framing: this is the first step of the entropy-fork program. At whole-cell granularity one expects rank and nullity to balance if the record is a linear parity map on $(\mathbb{F}_2)^8$.
proof idea
One-line term proof: by decide. Lean enumerates the finite image of the face-record map over Finset.univ and the filtered kernel Finset, multiplies the two Nat cardinals, and checks equality with 256. No algebraic lemmas are invoked beyond the definitions of the record map and kernel; the identity is machine-checked exhaustively on the 256-element domain.
why it matters
Fills the rank-nullity slot of the cell-injection verdict: image cardinality $16 = 2^4$ and kernel cardinality $16 = 2^4$ coincide, so posted cost and fiber degeneracy match at whole-cell scale. Downstream it is packed into target_cell_injection_holds, the verify-target certificate for the holography loop (together with single-flip posting, non-injectivity, kernel card, and the global-blindness bound).
Framework landmarks: the substrate is the forced eight-tick octave in D=3 (T7/T8), the cube $2^3$. The dichotomy separates futures for recognition complementarity: local flips always post, yet a rank-4 group of cell-global parity moves (whole-face flips, global complement, inscribed tetrahedra) remains invisible. The entropy fork of CoefficientBridge (rank-vs-nullity mismatch on faces and dominos) is thereby isolated as a per-face or glued-surface effect, invisible once the whole cell is the unit. Closes the first-isomorphism check named in the doc-comment with no axioms beyond decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.