ledgerL1Cost_eq_zero_iff
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.
claimLet $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 in Recognition Science
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$.
scope and limits
- Does not prove nonnegativity of ledgerL1Cost.
- Does not relate the L1 cost to the Jlog cost defined in the same module.
- Does not address multi-unit or non-monotone updates.
- Does not derive the cost from the Recognition Composition Law.
formal statement (Lean)
611theorem ledgerL1Cost_eq_zero_iff {d : Nat} (L L' : LedgerState d) :
612 ledgerL1Cost (d := d) L L' = 0 ↔ L' = L := by
proof body
Tactic-mode proof.
613 classical
614 cases L with
615 | mk debit credit =>
616 cases L' with
617 | mk debit' credit' =>
618 constructor
619 · intro h0
620 -- split into debit/credit sums
621 let dSum : Nat := ∑ i : Fin d, Int.natAbs (debit' i - debit i)
622 let cSum : Nat := ∑ i : Fin d, Int.natAbs (credit' i - credit i)
623 have hsplit : dSum + cSum = 0 := by
624 simpa [ledgerL1Cost, dSum, cSum] using h0
625 have hd0 : dSum = 0 ∧ cSum = 0 := Nat.add_eq_zero_iff.mp hsplit
626 have hdebit0 :
627 ∀ i : Fin d, Int.natAbs (debit' i - debit i) = 0 := by
628 have h' :
629 Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (debit' i - debit i)) = 0 := by
630 simpa [dSum] using hd0.1
631 have hall :=
632 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
633 (f := fun i => Int.natAbs (debit' i - debit i))
634 (fun _ _ => Nat.zero_le _)).1 h'
635 intro i
636 exact hall i (by simp)
637 have hcredit0 :
638 ∀ i : Fin d, Int.natAbs (credit' i - credit i) = 0 := by
639 have h' :
640 Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (credit' i - credit i)) = 0 := by
641 simpa [cSum] using hd0.2
642 have hall :=
643 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
644 (f := fun i => Int.natAbs (credit' i - credit i))
645 (fun _ _ => Nat.zero_le _)).1 h'
646 intro i
647 exact hall i (by simp)
648 have hdebitEq : debit' = debit := by
649 funext i
650 have hz : (debit' i - debit i) = 0 := Int.natAbs_eq_zero.mp (hdebit0 i)
651 linarith
652 have hcreditEq : credit' = credit := by
653 funext i
654 have hz : (credit' i - credit i) = 0 := Int.natAbs_eq_zero.mp (hcredit0 i)
655 linarith
656 subst hdebitEq hcreditEq
657 rfl
658 · intro hEq
659 cases hEq
660 simp [ledgerL1Cost]
661
662/-! ### Posting steps satisfy `LegalAtomicTick` (and conversely, by `legalAtomicTick_implies_PostingStep`) -/
663