fiber_posts_one_record

The module RecordCostAsymmetry settles the rank/nullity selector for the Bekenstein–Hawking coefficient. A finite closure map on face configurations obeys the symmetric identity $|\mathrm{image}|\cdot|\mathrm{kernel}|=|\mathrm{domain}|$ (here $2\cdot 8=16$). Pure counting cannot prefer rank ($\log_2|\mathrm{image}|=1$, giving $\kappa=4$) over nullity ($\log_2|\mathrm{kernel}|=3$, giving $\kappa=4/3$).

The ledger floor breaks that symmetry: cost charges only performed distinctions (pairs the map separates), which are image-sided. The kernel is the set of pairs the map does not distinguish and is never charged. The closed fiber is the eight ledger-closed microstates among the sixteen face configs; the local closure map sends each config to a Boolean record.

This theorem states that those eight closed configs all land on the single record true. The complementary fact is that the full map performs two records (true and false), so record cost is $\log_2 2=1$.

One-line finite decision. The closed configuration set and the Boolean closure map are both fully enumerated; Lean’s decide checks that the image of the closed fiber under closure has cardinality exactly one. No algebraic lemmas are invoked.

This is the physical content of the symmetry break: the eight free bits that would support $\kappa=4/3$ post only one distinction, so the ledger floor sees rank one, not nullity three. Downstream, target_record_cost_asymmetry_holds packages this with records_performed, the two multiplicity equalities, and the Bekenstein selector, discharging the panel target that horizon entropy attaches to performed records ($S=A/4$) rather than bulk degeneracy.

In the Recognition framing, T-1 (recognition is distinction) and the double-entry posting arrow make cost directional. Static rank-nullity counting lacks that arrow; this fiber image supplies it axiom-cleanly. It closes the conditional gap left by the earlier cell-ledger multiplicity axiom: the selector is now forced by what the map actually posts.