recordCost
plain-language theorem explainer
For any finite map f, the record cost is log₂ of the size of its image: the number of independent binary distinctions the map actually performs. Holography and ledger-floor arguments cite it as the image-side half of the rank–nullity split that selects Bekenstein–Hawking S = A/4 over the microstate reading. The body is a one-line definition via image cardinality and Nat.log2.
Claim. For types $\alpha$ (finite) and $\beta$ (with decidable equality) and any map $f : \alpha \to \beta$, the record cost of $f$ is $\log_2 |\mathrm{im}(f)|$, i.e. the base-2 logarithm of the number of distinct values $f$ attains.
background
The module RecordCostAsymmetry reframes the holography selector that decides whether horizon entropy attaches to the closure map's rank ($\log_2|\mathrm{image}|$) or its nullity ($\log_2|\mathrm{kernel}|$). Pure counting is symmetric: $|\mathrm{image}|\cdot|\mathrm{kernel}|=|\mathrm{domain}|$ (here $2\cdot 8=16$ for the face-closure map), so it cannot prefer one side.
The ledger floor breaks that symmetry. Cost sums posted generators — distinctions the map actually performs ($f(x)\neq f(y)$). Non-distinctions (kernel pairs with $f(x)=f(y)$) are never charged. Record cost is therefore the image-sided quantity: how many independent binary records the map produces. Its counterpart, microstate cost, is $\log_2$ of a fiber cardinality (free bits the map does not distinguish).
In the local pixel model, the closed fiber of size 8 collapses to a single posted record, so the ledger sees one performed distinction, not three free bits.
proof idea
Pure definition, not a proved theorem. The body takes the finite image of $f$ over the universe of $\alpha$, reads its cardinality, and applies $\mathrm{Nat.log2}$. No lemmas are invoked; the mathematical content is exactly that expression.
why it matters
This is the image-side primitive the whole record-cost asymmetry argument hangs on. Downstream, HorizonEntropyIsRecordCost identifies horizon thermodynamic entropy with this quantity on the boundary closure map (plaquette multiplicity $=1$), making $S=A/4$ a theorem modulo that single named premise. The certificate bekenstein_tag_b_cert packages the fork: record-cost premise forces $1/4$; the counterfactual microstate premise forces $3/4$.
fiber_posts_one_record and the factor-three theorem in KeystoneFactorThree use it to show the closed fiber performs one record while microstate cost is three times larger — the $3$ in "$3\cdot(A/4)$" is computed, not hand-typed. Module certificates (recordCostAsymmetryCert, recordCost_closed, recordCost_domino) and equality lemmas at multiplicity one and two all reduce through this definition. It is the concrete realization of the T0 posting arrow: cost counts performed distinctions, which is what selects rank over nullity for the Bekenstein–Hawking coefficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.