observableSetoid
plain-language theorem explainer
Packages equality of weighted ledger cost as a setoid on defect ledgers: two finite multiplicity maps are equivalent exactly when they share the same total cost. Anyone working the Recognition ledger floor or the kernel-gap fix cites this. The proof is the standard equality setoid (refl, symm, trans) on the cost kernel.
Claim. For a weight $w : I \to \mathbb{R}$, the relation $\Gamma \sim_w \Delta$ on defect ledgers given by $\mathrm{cost}_w(\Gamma) = \mathrm{cost}_w(\Delta)$ is an equivalence relation, hence defines a setoid on the free commutative monoid of finitely supported multiplicities $I \to_0 \mathbb{N}$.
background
The module builds the free additive cost floor that closes the T-1/T0 audit gaps. A defect ledger is a finitely supported map $I \to_0 \mathbb{N}$: multiplicities of primitive distinctions, the free commutative monoid on $I$. Recognition cost under a per-distinction weight $w$ is the total weighted multiplicity.
Observational sameness is defined as equality of that cost: two ledgers are the same when no weighted cost separates them. The module doc stresses that this equivalence is the kernel of the cost functional, derived from cost rather than imposed as an external gauge or setoid (the kernel gap / audit Loophole 2).
The dual cokernel gap is handled by unconditional additivity and multiplicity on the same carrier; this definition supplies only the setoid half of that package.
proof idea
One-line Setoid construction: the relation field is observational sameness (cost equality). Equivalence is the standard triple for propositional equality of real costs: reflexivity by rfl, symmetry by Eq.symm, transitivity by Eq.trans. No ledger-specific lemmas are needed beyond the definition of the relation.
why it matters
This is the object that answers the kernel gap in the Recognition ledger floor: observable equivalence is generated by the cost functional, not assumed. Downstream, cost is constant on classes by construction (ledgerCost_constant_on_classes), so gauge invariance is automatic rather than postulated. That feeds the non-vacuity criterion (the kernel is proper exactly when some weight is positive) and the assembly into the universal CostFromDistinction configuration. In the broader forcing picture it underwrites a clean two-state Boolean floor as the $n\in{0,1}$ truncation under unit weight, without smuggling an external gauge group into T0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.