ledgerCost_zero
plain-language theorem explainer
The recognition cost of the empty defect ledger is zero for every real weight function on primitive distinctions. Workers on the free additive ledger floor, the observable cost kernel, or the T0 bridge use this as the base case of the weighted multiplicity sum. The proof is a one-line simplification of the Finsupp sum defining ledger cost.
Claim. For any type $I$ of primitive distinctions and any weight $w:I\to\mathbb{R}$, if $\Gamma=0$ is the zero element of the free commutative monoid of finitely supported multiplicities $I\to_0\mathbb{N}$, then the ledger cost $\sum_i n_i\,w(i)$ equals $0$.
background
The module builds the free additive cost floor that closes the two real gaps from the T-1/T0 audit: the kernel gap (observable equivalence should be the cost kernel, not an external setoid) and the cokernel gap (independent defects must accumulate with multiplicity).
A defect ledger is the free commutative monoid $\mathrm{DefectLedger},I:=I\to_0\mathbb{N}$: finitely supported multiplicities of primitive distinctions. Its recognition cost under a per-distinction weight $w$ is the total weighted multiplicity $$\mathrm{ledgerCost},w,\Gamma=\Gamma.\mathrm{sum},(i,n)\mapsto (n:\mathbb{R})\cdot w(i).$$
Upstream cost notions (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen multiset cost, PRC quotient J-cost) all specialize the same idea: cost is a non-negative functional of performed distinctions. Here the carrier is free and additive, so the empty ledger is the monoid zero.
proof idea
Term-mode one-liner: simp [ledgerCost]. Unfolding the definition reduces the claim to the standard fact that the Finsupp sum of the zero function is zero, independent of $w$. No positivity or finiteness side conditions are needed beyond the type of $\Gamma$.
why it matters
This is the unit law for the free ledger cost. Downstream, observable_floor_iff_pos_weight uses the zero ledger when characterizing non-vacuity of the cost kernel: observably distinct ledgers exist exactly when some weight is strictly positive. The T0 bridge ledger_floor_t0_bridge likewise routes through the zero shadow (ledgerShadow_zero) when identifying the free floor with the Boolean two-state floor under unit weight.
In the Recognition forcing chain this sits under the T0 minimal-distinction floor: the Boolean $n\in{0,1}$ truncation is recovered from this free monoid, and unconditional additivity (the sibling ledgerCost_add) removes the restricted-independence evasion of the audit. The empty-cost identity is the base case that makes the kernel and multiplicity stories well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.