DefectLedger
plain-language theorem explainer
A defect ledger on a type I of primitive distinctions is a finitely supported map I → ℕ: each distinction carries a natural multiplicity, and only finitely many are nonzero. It is the free commutative monoid on I, so independent postings add by summing multiplicities. Downstream T0-bridge and cost lemmas cite it as the extensive carrier whose Boolean shadow recovers the two-state floor. The declaration is a one-line type synonym for Mathlib's finsupp.
Claim. For a type $I$ of primitive distinctions, a defect ledger is a finitely supported function $\Gamma : I \to \mathbb{N}$ (equivalently an element of the free commutative monoid on $I$).
background
The module builds the free additive cost floor that closes two audit gaps in the T-1/T0 story: the kernel gap (observable equivalence should be the kernel of cost, not an external setoid) and the cokernel gap (independent defects must accumulate with multiplicity rather than being excluded to dodge $1=2$).
The carrier is the free commutative monoid on a type $I$ of primitive distinctions: finitely supported maps $I \to \mathbb{N}$. Addition is pointwise on multiplicities; the zero ledger posts nothing. A strictly positive weight $w : I \to \mathbb{R}$ then defines total recognition cost as the weighted sum of multiplicities (the sibling ledgerCost).
Upstream cost notions in the stack (J-cost on recognition events, derived cost of multiplicative recognizers, rung-coarsened multiset costs) all need an extensive place to post distinctions. This synonym supplies that place without imposing a restricted independence relation.
proof idea
One-line type abbreviation: DefectLedger I is definitionally I →₀ ℕ (Mathlib finitely supported functions to naturals). No proof obligations; the free commutative monoid structure and pointwise addition are inherited from finsupp.
why it matters
This is the single object that answers both genuine gaps in the T0 audit. On it, cost additivity is unconditional (ledgerCost_add), observable equivalence is the kernel of cost (observableSetoid), and two independent copies of the same defect cost $2w(i)$ (two_independent_same_defects).
The T0 Boolean floor is recovered as the $n\in{0,1}$ truncation under unit weight. Downstream, LedgerFloorT0Bridge packages a surjective cost-and-join homomorphism from this extensive ledger onto the distinction-generated T0 floor; ledgerShadow is the Boolean shadow (empty vs any posting), and ledger_add_eq_zero_iff records that there are no negative entries to cancel. The data assemble into the existing CostFromDistinction.CostFunction abstraction with universal independence.
In the forcing chain this sits under T0: the two-state floor is no longer a primitive postulate but the shadow of free multiplicity. Status in-module: 0 sorry, 0 new axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.