ledgerCost
plain-language theorem explainer
Defines the recognition cost of a defect ledger as the sum of multiplicity times per-distinction weight. Anyone working the free additive cost floor, T0 bridge, or ledger-to-factorization path cites it as the extensive cost functional. The body is a one-line Finsupp sum: each primitive distinction contributes n·w(i).
Claim. For a type $I$ of primitive distinctions, a weight $w : I \to \mathbb{R}$, and a defect ledger $\Gamma : I \to_0 \mathbb{N}$ (finitely supported multiplicities), the ledger cost is $\mathrm{cost}_w(\Gamma) = \sum_{i \in I} n_i\, w(i)$, where $n_i = \Gamma(i)$.
background
The module builds the free additive cost floor that closes the T-1/T0 audit gaps: the kernel gap (observable equivalence should be the kernel of cost) and the cokernel gap (independent defects must accumulate with multiplicity). The carrier is the free commutative monoid on primitive distinctions,
$$\mathrm{DefectLedger}, I := I \to_0 \mathbb{N},$$
finitely supported maps from $I$ to natural numbers. Addition of ledgers is pointwise and unconditional; no restricted independence relation is needed.
The weight $w$ assigns a real cost to each primitive distinction. This definition turns that weight into an extensive functional on the whole ledger by summing multiplicity times weight. Downstream lemmas prove additivity, non-negativity (for $w \ge 0$), and that the cost kernel is the observable equivalence.
proof idea
Definitional one-liner: evaluate the Finsupp sum of $\Gamma$ against the map $(i,n) \mapsto (n:\mathbb{R})\cdot w(i)$. No lemmas are applied; the meaning is exactly the total weighted multiplicity of performed distinctions.
why it matters
This is the cost functional that makes the free ledger answer both audit gaps at once. Unconditional additivity (ledgerCost_add) and non-negativity feed the order-faithfulness anchor ledgerCost_le_add_right and the linear-response / posting semantics in LedgerToFactorization (discrete and free-ledger combiner structures, primitive-to-discrete posting specialization).
It is the extensive cost that the T0 bridge truncates: LedgerFloorT0Bridge and ledger_floor_t0_bridge identify the Boolean two-state floor as the $n\in{0,1}$ clamp of this ledger under strictly positive weights. In the forcing chain, that floor is the T0 minimal-distinction step; the ledger supplies the extensive parent whose kernel and cokernel are derived rather than imposed. Status of the module: zero sorry, zero new axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.