stepAt

formal source

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) =>
1033    let prev := run L0 sched t
1034    post prev (sched t).1 (sched t).2
1035
1036theorem run_step_oneBitDiff {d : Nat} (L0 : LedgerState d) (sched : Nat → PostInstr d) (t : Nat) :
1037    OneBitDiff (parity d (run L0 sched t)) (parity d (run L0 sched (t + 1))) := by
1038  -- unfold one step of `run` and apply the single-post theorem
1039  simp [run, parity_oneBitDiff_of_post, parity]
1040
1041end LedgerPostingAdjacency
1042end IndisputableMonolith