phiVec_coordAtomicStep_of_post

formal source

 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)
 115    | credit =>
 116        right
 117        -- at k, phi decreases by 1
 118        simpa using (by
 119          have := (phiVec_post_credit (d := d) L k k)
 120          simpa using this)
 121  · intro i hik
 122    cases side with
 123    | debit =>
 124        -- other coordinates unchanged
 125        have := (phiVec_post_debit (d := d) L k i)
 126        simpa [hik] using this
 127    | credit =>
 128        have := (phiVec_post_credit (d := d) L k i)
 129        simpa [hik] using this
 130
 131/-! ## Main theorem: posting ⇒ parity adjacency -/
 132
 133theorem parity_oneBitDiff_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
 134    OneBitDiff (parity d L) (parity d (post L k side)) := by