ledgerConfigSpace
plain-language theorem explainer
The free defect ledger (finitely supported multiplicities of primitive distinctions) is equipped as a configuration space: empty configuration is the zero ledger, join is multiplicity addition, consistency means the ledger is zero, and independence holds universally for every pair. Anyone building a recognition-work cost on the ledger floor needs this instance. The monoid laws are inherited from Finsupp addition; the only nontrivial check is that a sum of two ledgers vanishes only if each vanishes, via pointwise omega on naturals.
Claim. For any type $I$ of primitive distinctions, the free commutative monoid of finitely supported multiplicity maps $I \to_0 \mathbb{N}$ forms a configuration space: the empty configuration is the zero map, join is pointwise addition of multiplicities, a configuration is consistent if and only if it is identically zero, and every pair of configurations is declared independent.
background
The module builds the free additive cost floor that closes two genuine gaps from the T-1/T0 audit: the kernel gap (observable equivalence should be the kernel of the cost, not an external setoid) and the cokernel gap (independent defects must accumulate with multiplicity rather than being excluded from independence to dodge $1=2$).
The carrier is the free commutative monoid on a type $I$ of primitive distinctions: finitely supported maps $I \to_0 \mathbb{N}$. A configuration space, from CostFromDistinction, is an abstract structure with empty configuration, binary join, a consistency predicate, and an independence relation, with join a commutative monoid under empty as identity, independence symmetric, and empty independent of everything.
A cost function on such a space must satisfy dichotomy (cost zero iff consistent) and independent additivity. This instance supplies the configuration-space half with universal independence, so additivity of ledger cost needs no restricted independence relation.
proof idea
The instance fills ConfigSpace fields directly. Empty is the zero Finsupp; join is addition; consistency is equality to zero; independence is constantly True.
Monoid laws are one-line citations of add_comm, add_assoc, and zero_add (from ArithmeticFromLogic / the Finsupp monoid). Empty-consistency and the independence symmetry/empty laws are rfl or trivial.
The two consistency-of-join obligations are the only content: if both summands are zero then the sum is zero (subst and simp); conversely, if the sum is zero and the left summand is assumed nonzero, project the sum equation at each index via Finsupp.add_apply, then omega forces each natural coordinate of the left summand to vanish, contradicting the assumption. The right-hand dual is not needed separately under the class API used here.
why it matters
This instance is the configuration-space half of the ledger floor package that answers the Anil critique of T-1/T0. With universal independence, the free ledger no longer needs a restricted independence relation to keep the Boolean floor from collapsing under $1=2$; multiplicity is represented, and two independent copies of the same defect cost twice the weight (sibling two_independent_same_defects).
Together with the companion cost-function instance, the data assemble into the existing CostFromDistinction abstraction. The two-state Boolean floor of T0 becomes the $n\in{0,1}$ truncation under unit weight. Downstream, the observable setoid is recovered as the kernel of ledger cost, so the floor is non-vacuous exactly when some weight is positive.
No used_by edges are recorded yet; the declaration is infrastructure for the ledger cost function and the kernel/cokernel closure rather than a forcing-chain landmark (T5–T8) itself. Status of the module: zero sorry, zero new axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.