record_zero_general
plain-language theorem explainer
Any finite map whose image has at most one element carries zero record cost: no performed distinctions means no posted records. Holography and ledger-cost arguments cite this as the base case that a non-distinguishing boundary is free. The proof is a one-line application of the elementary fact that log₂ of a cardinality at most one vanishes.
Claim. Let $f : \alpha \to \beta$ be a map between types with $\alpha$ finite and equality on $\beta$ decidable. If $|\mathrm{im}\, f| \le 1$, then the record cost of $f$ is zero: $\mathrm{recordCost}(f) = 0$.
background
In the RecordCostAsymmetry module, record cost of a finite map $f$ is $\log_2$ of the cardinality of its image: the number of independent binary distinctions the map actually performs. This is Bennett-style memory bookkeeping (posted distinctions), not Landauer erasure; the module was renamed from LandauerAsymmetry for that reason.
The local setting is the holographic rank/nullity selector for the Bekenstein–Hawking coefficient. Pure counting gives the symmetric identity $|\mathrm{image}|\cdot|\mathrm{kernel}|=|\mathrm{domain}|$ and cannot prefer rank over nullity. Cost breaks the symmetry because the recognition ledger only charges performed distinctions ($f x \neq f y$), which are image-sided; non-distinctions in the kernel are free.
Sibling infrastructure includes recordCost itself and the elementary lemma log2_eq_zero_of_le_one, which states that $\log_2 n = 0$ whenever $n \le 1$. Upstream cost notions (J-cost on recognition events, multiplicative-recognizer cost, rung-coarsen totals) supply the broader ledger language but are not invoked in this proof.
proof idea
One-line term proof: apply the sibling lemma log2_eq_zero_of_le_one to the hypothesis that the image Finset has cardinality at most one. Since recordCost f is defined as $\log_2$ of that cardinality, the conclusion is immediate. No case split, no induction, no external cost axioms.
why it matters
This is the general zero-cost base case for the record-cost reading of holography. Downstream, record_zero_of_constant specializes it to constant maps (image a subsingleton via pointwise equality), and target_record_cost_asymmetry_holds packages it as the first conjunct of the target asymmetry statement: any map with $|\mathrm{image}|\le 1$ has zero record cost.
Together with the positive-cost facts for maps that do perform distinctions (recordCost_eq_multiplicity_one/two, records_performed, fiber_posts_one_record), it feeds the selector that prefers image-rank over kernel-nullity for the BH coefficient ($\kappa=4$, $S=A/4$). That selector is the module's answer to the panel verdict that a pure counting theorem cannot break image/kernel symmetry. Framework-wise it realizes T-1 directionality: recognition is distinction, and only posted distinctions enter the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.