record_zero_of_constant
plain-language theorem explainer
A finite map that is constant (no two domain points are sent to different values) has record cost exactly zero. Holography and horizon-entropy arguments cite this as the memory-bookkeeping baseline: a boundary that performs no distinctions stores nothing. The proof reduces to the general image-cardinality criterion by showing the image is a subsingleton.
Claim. Let $f : \alpha \to \beta$ with $\alpha$ finite and equality on $\beta$ decidable. If $f$ is constant (for all $x,y \in \alpha$, $f(x)=f(y)$), then the record cost of $f$ vanishes: $\mathrm{recordCost}(f)=0$.
background
In RecordCostAsymmetry, horizon entropy is forced to attach to the image side of a finite closure map rather than the kernel. The selector is not pure counting: rank-nullity gives the symmetric identity $|\mathrm{image}|\cdot|\mathrm{kernel}|=|\mathrm{domain}|$, so a bare cardinality theorem cannot prefer rank over nullity.
The symmetry-breaker is directional cost. Recognition cost charges only performed distinctions (pairs with $f x \neq f y$). The record cost of a finite map is $\log_2$ of its image cardinality: the number of independent binary distinctions the map actually posts. The kernel is exactly the set of non-distinctions and is never charged.
The sibling lemma record_zero_general states that record cost vanishes whenever the image has cardinality at most one. The constant-map form is the physically named special case: a boundary that records nothing.
proof idea
One short reduction to record_zero_general. After applying that lemma, it remains only to show $|\mathrm{image}(f)|\le 1$. Rewrite via Finset.card_le_one, take two elements of the image, unpack each as $f(x)$ and $f(y)$ by membership in the image, and finish with the constancy hypothesis $f x = f y$.
why it matters
This is the zero baseline that makes the record-versus-microstate dichotomy sharp. Downstream, record_zero_separates_readings pairs it with a nonzero microstate cost on the same constant map over a domain of size $\ge 2$: record cost is $0$ while microstate cost is $\log_2 n \ge 1$. Demanding only that a boundary distinguishing nothing holds zero entropy already selects the record reading and rules out the kernel/microstate branch (the $\kappa=4/3$ fork exhibited by kappa_four_thirds_of_microstate_cost).
In the holography chain this discharges the panel attack on conditional multiplicity axioms: cost counts posted distinctions (T0 double-entry directionality), so image/rank is forced over kernel/nullity, yielding the Bekenstein-Hawking coefficient $\kappa=4$ rather than $4/3$. Formerly named in Landauer language; the mathematics is Bennett-style memory bookkeeping on the closure map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.