ledgerCost_constant_on_classes
plain-language theorem explainer
Recognition cost of a defect ledger is constant on observable equivalence classes, because the setoid is the kernel of the cost. Anyone arguing gauge invariance of ledger cost cites this. The proof is the identity: the setoid relation is definitionally cost equality, so the hypothesis is already the claim.
Claim. Let $w : I \to \mathbb{R}$ be a weight on primitive distinctions and let $\Gamma, \Delta$ be defect ledgers (finitely supported maps $I \to \mathbb{N}$). If $\Gamma$ and $\Delta$ are related by the observable setoid of $w$ (the kernel of the weighted ledger cost), then the ledger cost of $\Gamma$ under $w$ equals that of $\Delta$.
background
The module builds the free additive cost floor on defect ledgers to close two T-1/T0 audit gaps: the kernel gap (observable equivalence must come from the cost, not an external gauge) and the cokernel gap (independent defects must accumulate with multiplicity).
A defect ledger is the free commutative monoid I →₀ ℕ: finitely supported multiplicities of primitive distinctions. The ledger cost under a weight $w$ is the total weighted multiplicity of performed distinctions. The observable setoid is defined as the kernel of that cost, so two ledgers are observably the same exactly when they have equal cost.
This sits inside the broader Recognition cost story (J-cost on ratios, additive accumulation of distinctions) but here the carrier is the free monoid rather than a Boolean two-state floor.
proof idea
One-line term proof. The hypothesis states that the observable-setoid relation holds between the two ledgers. By construction that relation is equality of ledger costs under $w$, so the hypothesis is definitionally the desired equality and is returned as the proof term.
why it matters
This is the explicit gauge-invariance statement for the ledger floor: cost is constant on observable classes by construction, not by an extra assumption. It answers the kernel gap in the module doc (audit Loophole 2): observable equivalence is derived as the kernel of the cost functional rather than imposed as an external setoid or gauge group.
Together with non-vacuity of the floor when some weight is positive, additivity of ledger cost, and multiplicity of independent copies of the same defect, it packages the free monoid into the existing CostFromDistinction abstraction. The Boolean two-state floor of T0 is recovered as the $n \in {0,1}$ truncation under unit weight. No downstream users are recorded yet; the theorem is infrastructure for any later quotient-by-observables argument on ledgers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.