phiVec_post_debit

formal source

  81      { debit := L.debit
  82      , credit := fun i => if i = k then L.credit i + 1 else L.credit i }
  83
  84@[simp] lemma phiVec_post_debit {d : Nat} (L : LedgerState d) (k : Fin d) (i : Fin d) :
  85    phiVec (d := d) (post L k Side.debit) i =
  86      (if i = k then phiVec (d := d) L i + 1 else phiVec (d := d) L i) := by
  87  by_cases hik : i = k
  88  · subst hik
  89    simp [post, phiVec, Recognition.phi]
  90    ring_nf
  91  · simp [post, phiVec, Recognition.phi, hik]
  92
  93@[simp] lemma phiVec_post_credit {d : Nat} (L : LedgerState d) (k : Fin d) (i : Fin d) :
  94    phiVec (d := d) (post L k Side.credit) i =
  95      (if i = k then phiVec (d := d) L i - 1 else phiVec (d := d) L i) := by
  96  by_cases hik : i = k
  97  · subst hik
  98    simp [post, phiVec, Recognition.phi]
  99    ring_nf
 100  · simp [post, phiVec, Recognition.phi, hik]
 101
 102/-! ## Bridge: a post induces a coord-atomic step on `phi` -/
 103
 104lemma phiVec_coordAtomicStep_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
 105    coordAtomicStep (d := d) (phiVec (d := d) L) (phiVec (d := d) (post L k side)) := by
 106  classical
 107  refine ⟨k, ?_, ?_⟩
 108  · cases side with
 109    | debit =>
 110        left
 111        -- at k, phi increases by 1
 112        simpa using (by
 113          have := (phiVec_post_debit (d := d) L k k)
 114          simpa using this)