physState_records_card
plain-language theorem explainer
On the forced D=3 cell, the face-record map hits exactly 16 distinct boundary records: four posted bits. Holography and entropy-fork arguments cite this as the cell-scale rank of the posted-record image. The proof is a one-line re-export of the injection-test cardinality lemma.
Claim. The image of the full bulk configuration set under the six-face boundary record map has cardinality exactly $16$ (equivalently, four posted bits).
background
Module RecordMonotonicity is step 3 of the entropy-fork chain: derive weak complementarity on the forced D=3 cell from record accounting rather than as a monolithic premise. Step 1 was the cell-injection test; step 2 the Clausius selector. Weak complementarity means an injection from physical bulk states into boundary letter space.
The face-record map posts one bit per face channel of the cell (six channels). The injection test already computed the rank of that image: sixteen distinct posted records. Physical bulk states on the eight-vertex cell are identified with those records once gauge pairs (kernel cosets) are quotiented out.
Sibling bookkeeping shows boundary heat equals posted record flux channel-by-channel, so erasures export as negative heat and zero-heat steps preserve record weight. That ledger discipline feeds the later no-protocol-separates and weak-complementarity theorems; the present fact only freezes the image cardinality.
proof idea
One-line term proof: apply the already-proved injection-test lemma record_image_card, which states that the image of the universe under the face-record map has cardinality 16. No new algebra is done here; the declaration re-exports that rank into the RecordMonotonicity namespace for downstream holographic bounds.
why it matters
Feeds two parents in the same module. First, holographic_bound_of_weak_comp rewrites the image card to 16 and concludes $16 \le 2^6$: the posted-record set sits strictly inside the six-bit boundary capacity, the cell-scale instance of the boundary access law. Second, target_record_monotonicity_holds packages this card equality with books-balance, gauge-kernel identification, no-protocol-separates, and weak complementarity as the verify-target certificate for the entropy-fork panel.
In the Recognition framework this is the concrete rank that makes weak complementarity quantitative on the forced cell (T8 forces D=3; T7 the eight-tick octave structures the discrete bulk). It replaces the manuscript's strongest complementarity premise with a finite, checkable count: 16 states = 4 posted bits. No open scaffold remains on this line; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.