ledgerCostFunction
plain-language theorem explainer
For any strictly positive weight on primitive distinctions, the free defect ledger carries a genuine recognition-work cost function with universal independence. Anyone proving the recognition-work constraint on the free additive floor cites this packaging. The definition simply assembles three already-proved facts (nonnegativity, zero-cost dichotomy, unconditional additivity) into the CostFunction structure.
Claim. Let $I$ be a type of primitive distinctions and $w:I\to\mathbb{R}$ strictly positive. The free defect ledger $\mathrm{DefectLedger}\,I:=I\to_0\mathbb{N}$ (finitely supported multiplicities) equipped with $C(\Gamma)=\sum_i n_i\,w(i)$ is a cost function: $C\ge 0$, $C(\Gamma)=0$ iff $\Gamma$ is empty (consistent), and $C$ is additive on independent join.
background
The module builds the free additive cost floor that closes two audit gaps from T-1/T0: the kernel gap (observable equivalence must be the kernel of cost, not an external setoid) and the cokernel gap (independent defects must accumulate with multiplicity). The carrier is the free commutative monoid
$$\mathrm{DefectLedger},I:=I\to_0\mathbb{N}$$
on a type $I$ of primitive distinctions. Recognition cost under a weight $w$ is the total weighted multiplicity
$$\mathrm{ledgerCost},w(\Gamma)=\sum_i n_i,w(i).$$
Upstream, CostFromDistinction.CostFunction is the recognition-work bridge abstraction: a map $C$ on a configuration space that is nonnegative, satisfies dichotomy (zero cost iff consistent), and is additive on independent join. The free ledger is designed so additivity holds unconditionally (no restricted independence relation), and the observable equivalence is exactly the kernel of $C$.
proof idea
Structure construction, not a deep argument. The cost field is set to ledgerCost w. Nonnegativity is ledgerCost_nonneg applied to the weak inequality $0\le w,i$ implied by strict positivity. Dichotomy is a one-line appeal to ledgerCost_eq_zero_iff (zero cost characterises the empty ledger under strictly positive weights). Additivity is a one-line appeal to ledgerCost_add, which holds for every pair of ledgers with no side condition on independence.
why it matters
This is the packaging step that lets the free ledger inhabit the existing recognition-work API. Downstream, ledger_recognition_work_constraint is the one-line application of CostFunction.recognition_work_constraint_theorem to this object, certifying that the free ledger satisfies the recognition-work constraint with multiplicity represented and independence universal.
In the T0 forcing chain, the two-state Boolean floor is recovered as the $n\in{0,1}$ truncation under unit weight. By placing a genuine CostFunction on the free monoid, the construction answers both the kernel gap (observable equivalence is the cost kernel) and the cokernel gap (two independent copies of the same defect cost $2w(i)$). It is the bridge from the ledger floor into the broader CostFromDistinction layer that feeds later recognition-work theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.