ledgerL1Cost_eq_zero_iff
plain-language theorem explainer
ledgerL1Cost between ledger states L and L' vanishes exactly when the states coincide. Workers on minimal-cost posting steps cite the equivalence to isolate zero-cost transitions when proving uniqueness under monotonicity. The tactic proof cases on the mk constructors, splits the summed absolute differences via add_eq_zero, applies sum_eq_zero_iff_of_nonneg and natAbs lemmas to each component, then recovers equality by linarith and extensionality.
Claim. Let $d$ be a natural number and let $L, L'$ be ledger states over $d$ accounts, each a pair of debit and credit vectors indexed by Fin $d$. The L1 cost, defined as the sum of absolute differences across all debit and credit entries, equals zero if and only if $L' = L$.
background
In LedgerPostingAdjacency a ledger state LedgerState $d$ is the pair of debit and credit maps from Fin $d$ to integers. ledgerL1Cost sums the absolute differences of these maps componentwise, measuring total integer displacement under an update. The module models atomic postings that change exactly one coordinate by one unit, linking such steps to one-bit parity changes in the debit-minus-credit vector.
proof idea
Classical case analysis on the mk constructors of both states splits the cost into separate debit and credit sums. The zero hypothesis yields their sum is zero, hence each vanishes separately. Finset.sum_eq_zero_iff_of_nonneg forces every absolute difference to zero; Int.natAbs_eq_zero and linarith give componentwise equality. Extensionality and substitution close the forward direction; the converse is immediate simplification.
why it matters
The result feeds the downstream theorem minCost_monotoneStep_implies_postingStep, which identifies minimal-cost monotone ledger steps with single-account postings. It supplies the zero-cost uniqueness required for the ledger-to-parity adjacency bridge. Within the Recognition framework this strengthens the explicit ledger model that connects posting steps to the one-bit adjacency used in the forcing chain toward the eight-tick octave and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.