accountAt

formal source

 999/-! ## Workstream B tightening: RS AtomicTick ⇒ PostingStep (legality predicate) -/
1000
1001/-- Choose the unique posted account at tick `t` from an RS `AtomicTick` instance. -/
1002noncomputable def accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) : Fin d :=
1003  Classical.choose (ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t))
1004
1005lemma postedAt_accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) :
1006    AtomicTick.postedAt (M := AccountRS d) t (accountAt (d := d) t) := by
1007  have hex : ∃ u : Fin d, AtomicTick.postedAt (M := AccountRS d) t u :=
1008    ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t)
1009  simpa [accountAt] using (Classical.choose_spec hex)
1010
1011/-- An RS-atomic tick step, parameterized by an explicit debit/credit side schedule. -/
1012noncomputable def stepAt {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1013    LedgerState d :=
1014  post L (accountAt (d := d) t) (sideAt t)
1015
1016lemma stepAt_isPostingStep {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1017    PostingStep (d := d) L (stepAt (d := d) sideAt t L) := by
1018  refine ⟨accountAt (d := d) t, sideAt t, rfl⟩
1019
1020theorem stepAt_oneBitDiff {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1021    OneBitDiff (parity d L) (parity d (stepAt (d := d) sideAt t L)) :=
1022  postingStep_oneBitDiff (stepAt_isPostingStep (d := d) sideAt t L)
1023
1024/-! ## A per-tick posting schedule induces an adjacent walk in parity space -/
1025
1026/-- A per-tick posting instruction: (account index, side). -/
1027abbrev PostInstr (d : Nat) : Type := Fin d × Side
1028
1029/-- Run a ledger forward under a per-tick posting schedule. -/
1030noncomputable def run {d : Nat} (L0 : LedgerState d) (sched : Nat → PostInstr d) : Nat → LedgerState d
1031| 0 => L0
1032| (t + 1) =>