exists_unique_of_sum_univ_eq_one
plain-language theorem explainer
If a function from a finite set of indices to the natural numbers sums to exactly one, then exactly one index maps to one and all others map to zero. Ledger modelers invoke the result to certify that an atomic posting step touches precisely one account coordinate. The proof isolates a nonzero entry with the finite-set sum lemma, decomposes the total after erasure, and uses additivity of one together with non-negativity to force the remaining entries to zero.
Claim. Let $f : [d] → ℕ$ satisfy $∑_{i=0}^{d-1} f(i) = 1$. Then there exists a unique $k ∈ [d]$ such that $f(k) = 1$ and $f(i) = 0$ for all $i ≠ k$.
background
The LedgerPostingAdjacency module models a ledger state as a pair of debit and credit vectors over d accounts. An atomic tick posts exactly one unit to one side of one account, inducing a one-bit change in the parity vector. The present lemma supplies the uniqueness that converts a LegalAtomicTick into an explicit PostingStep. It relies on the non-negativity result zero_le from ArithmeticFromLogic, which feeds the sum-zero characterization used on the erased index set.
proof idea
The tactic proof opens in classical logic and shows the sum is nonzero. It applies Finset.exists_ne_zero_of_sum_ne_zero to locate an index k with f k ≠ 0. The sum is rewritten via Finset.add_sum_erase as f k plus the sum over the erased set. Nat.add_eq_one_iff splits the cases; the f k = 0 branch is ruled out by the choice of k. The remaining sum on the erased set is zero, and Finset.sum_eq_zero_iff_of_nonneg (invoking zero_le) forces every entry on that set to zero. The witness is then assembled.
why it matters
The lemma is the direct combinatorial engine inside legalAtomicTick_implies_PostingStep, which translates a legal atomic tick into a PostingStep. In the Recognition framework it supplies the missing link between the ledger posting model and the parity one-bit adjacency theorem of LedgerParityAdjacency. It thereby supports the claim that a single tick flips exactly one bit, consistent with the eight-tick octave and the phi-ladder structure. The result is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.