ledger_add_eq_zero_iff
plain-language theorem explainer
On the free defect ledger I →₀ ℕ, the sum of two ledgers vanishes if and only if each summand vanishes. Anyone proving that the Boolean shadow of the ledger is a monoid homomorphism to OR cites this cancellation-free fact. The proof is pointwise: evaluate the sum, apply Finsupp addition, then omega on ℕ.
Claim. For any index type $I$ and defect ledgers $\Gamma,\Delta : I \to_0 \mathbb{N}$, one has $\Gamma + \Delta = 0$ if and only if $\Gamma = 0$ and $\Delta = 0$.
background
A defect ledger is the free commutative monoid of finitely supported multiplicities of primitive distinctions: $\mathrm{DefectLedger}, I := I \to_0 \mathbb{N}$. Addition is pointwise on natural-number multiplicities; there are no negative entries, so postings cannot cancel.
This module identifies the T0 floor (the two-state Boolean recognition cost forced by a distinction) with the shadow of that extensive ledger. The shadow map sends a ledger to false exactly when the ledger is the zero Finsupp, and true otherwise. Establishing that the shadow is a monoid homomorphism onto Boolean OR requires knowing when a sum of ledgers is zero.
Upstream, Finsupp addition evaluates pointwise (add_apply), and the monoid unit satisfies the usual add_zero identity.
proof idea
Bidirectional constructor. Forward: from $\Gamma+\Delta=0$, apply congruence at each index $i$ and rewrite with Finsupp add_apply to get $\Gamma i + \Delta i = 0$ in $\mathbb{N}$; omega forces each summand to zero, then ext rebuilds $\Gamma=0$ and $\Delta=0$. Backward: substitute both hypotheses and rewrite with add_zero.
why it matters
Feeds ledgerShadow_add, which states that the shadow is a homomorphism from ledger addition to Boolean OR: posting recognition in either summand lights the two-state floor. That homomorphism is one of the four legs of the bundled LedgerFloorT0Bridge theorem, closing the Phase-2 gap that turns T0 from a chosen Boolean indicator into the shadow of an extensive cost object.
In the forcing chain this sits under T0 (the recognition floor). Without cancellation-freeness of $\mathbb{N}$-valued ledgers, the kernel of the shadow would not match the cost kernel, and the monoid projection onto the T0 join would fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.