lemma
proved
term proof
phiVec_coordAtomicStep_of_post
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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