ledgerL1Cost_post

formal source

 684          simp [post]
 685        · simp [post, hik]
 686
 687private lemma ledgerL1Cost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
 688    ledgerL1Cost (d := d) L (post L k side) = 1 := by
 689  classical
 690  cases side with
 691  | debit =>
 692      -- debit changes by +1 at k; credit unchanged
 693      have hdebit :
 694          (∑ i : Fin d, Int.natAbs ((post L k Side.debit).debit i - L.debit i)) = 1 := by
 695        -- isolate `k` and show everything else is 0
 696        let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.debit).debit i - L.debit i)
 697        have hsplit :=
 698          (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
 699        have fk : f k = 1 := by
 700          simp [f, post]
 701        have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
 702          refine Finset.sum_eq_zero ?_
 703          intro i hi
 704          have hik : i ≠ k := by
 705            simpa [Finset.mem_erase] using hi
 706          simp [f, post, hik]
 707        -- rewrite `∑ univ` using `hsplit.symm`
 708        simpa [f] using (by
 709          calc
 710            (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
 711              simpa using hsplit.symm
 712            _ = 1 := by simp [fk, hErase])
 713      have hcredit :
 714          (∑ i : Fin d, Int.natAbs ((post L k Side.debit).credit i - L.credit i)) = 0 := by
 715        -- credit is unchanged everywhere
 716        refine Finset.sum_eq_zero ?_
 717        intro i _