`PostInstr`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.LedgerPostingAdjacency on GitHub at line 1027.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

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

papers checked against this theorem

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