ledgerCost_eq_zero_iff
plain-language theorem explainer
With strictly positive per-distinction weights, the free defect ledger has total recognition cost zero if and only if it is the empty ledger. Anyone citing the recognition-work dichotomy on the free floor, or assembling ledgerCost into a CostFunction, needs this kernel characterization. The proof is a short sum argument: a nonempty support contributes a strictly positive summand, so cost vanishes only for the zero Finsupp.
Claim. Let $I$ be a type of primitive distinctions and $w:I\to\mathbb{R}$ a strictly positive weight. For any finitely supported multiplicity ledger $\Gamma:I\to_0\mathbb{N}$, the weighted total cost $\sum_i \Gamma(i)\,w(i)$ equals zero if and only if $\Gamma$ is the zero ledger.
background
The module builds the free additive cost floor that closes the T-1/T0 audit gaps: the kernel gap (observable equivalence should be the cost kernel, not an external setoid) and the cokernel gap (independent defects must accumulate with multiplicity). The carrier is DefectLedger I := I →₀ ℕ, the free commutative monoid of finitely supported multiplicities of primitive distinctions.
Recognition cost of a ledger under weight $w$ is the total weighted multiplicity of performed distinctions. Strict positivity of $w$ is the standing hypothesis that makes the floor non-vacuous. Upstream cost notions (J-cost on ratios, defect $= J$ on positives, observer and multiplicative-recognizer costs) supply the conceptual lineage; here the cost is purely the free weighted sum on multiplicities, with unconditional additivity and no restricted independence relation.
proof idea
Split the biconditional. Forward: assume cost zero and $\Gamma\neq 0$. Nonempty Finsupp support yields some $i$ with $\Gamma(i)\neq 0$. Then $(\Gamma(i):\mathbb{R})\cdot w(i)>0$ by mul_pos and Nat.pos_of_ne_zero. Every support term is nonnegative, so Finset.single_le_sum gives $(\Gamma(i))\cdot w(i)\le$ total cost, and linarith contradicts cost zero. Reverse: substitute $\Gamma=0$ and simplify the empty sum to zero.
why it matters
This is the recognition-work dichotomy on the free floor: costless means empty. It discharges the dichotomy field when packaging ledgerCost as a CostFunction (ledgerCostFunction), so the free ledger sits inside the existing CostFromDistinction abstraction with universal independence. Downstream, ledger_floor_t0_bridge uses the floor machinery (including zero-cost emptiness) to identify the Phase-2 ledger floor with the T0 two-state Boolean floor for every distinction witness and every strictly positive weight.
In the forcing chain, T0 is the Boolean recognition floor; this lemma shows the free monoid floor has the same zero-cost kernel property before truncation to $n\in{0,1}$. It is the kernel half of the dual fix that also represents multiplicity (two_independent_same_defects), closing audit Loopholes 2, 8, and 9 without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.