`run_step_oneBitDiff`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.LedgerPostingAdjacency on GitHub at line 1036.

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

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.