`postedAt_accountAt`

proved

show as: view math explainer →

module: IndisputableMonolith.LedgerPostingAdjacency
domain: LedgerPostingAdjacency
line: 1005 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.LedgerPostingAdjacency on GitHub at line 1005.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

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) =>
1033    let prev := run L0 sched t
1034    post prev (sched t).1 (sched t).2
1035

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.