DefectLedger
plain-language theorem explainer
The defect ledger is the free commutative monoid of finitely supported multiplicity maps from a type of primitive distinctions I into the naturals. It is the extensive recognition ledger whose Boolean truncation is the T0 floor. Anyone citing ledger cost, shadow maps, or the ledger–T0 bridge uses this carrier. The declaration is a public re-export of the foundation abbreviation I →₀ ℕ.
Claim. For a type $I$ of primitive distinctions, the defect ledger is the free commutative monoid $\mathrm{DefectLedger}(I) := I \to_0 \mathbb{N}$ of finitely supported multiplicity maps $I \to \mathbb{N}$.
background
The Ledger Floor module is the public aggregator for the Boolean shadow of the extensive recognition ledger. The core-theory PDF cites this layer: free additive ledgers, their recognition cost, and the identification of the T0 Boolean floor as a two-state truncation of that ledger.
A defect ledger records how many times each primitive distinction has been posted. Finite support means only finitely many distinctions carry positive multiplicity, so the object is the free commutative monoid on $I$ (pointwise addition of finitely supported functions to $\mathbb{N}$). There are no negative entries, so summands cannot cancel.
Upstream, the foundation module defines the same carrier as $I \to_0 \mathbb{N}$. Related cost notions elsewhere (J-cost on recognition events, derived costs of multiplicative recognizers, multiset ratio weights) are separate; here the ledger is the extensive multiplicity object before any cost or shadow is applied.
proof idea
One-line public re-export: the aggregator abbreviation is definitionally the foundation DefectLedger, itself the Mathlib finitely supported function type $I \to_0 \mathbb{N}$. No proof obligations beyond the type synonym.
why it matters
This is the primary citation target for the extensive recognition ledger in the ledger-floor layer. Downstream, the T0 bridge builds the Boolean shadow (empty vs any posting), proves the shadow is a homomorphism from ledger addition to Boolean OR, and packages LedgerFloorT0Bridge: for a distinction witness and strictly positive weights, the lift is a surjective cost-and-join homomorphism onto the distinction-generated T0 floor, with floor cost the two-state clamp of ledger cost.
That identification is the Phase-2 claim that the T0 floor is a genuine quotient (shadow) of the extensive ledger, not an unrelated carrier. It sits under the forced-quotient slice (distinction forcing through T0) that the module exposes as the public core. The free monoid structure also underwrites unconditional cost additivity and the multiplicity fact that two independent copies of one defect cost twice the weight, not once.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.