`LedgerVecState`

definition

show as: view math explainer →

module: IndisputableMonolith.LedgerParityAdjacency
domain: LedgerParityAdjacency
line: 95 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.LedgerParityAdjacency on GitHub at line 95.

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

  92
  93/-- A minimal ledger-state model: state is an integer vector, step is `coordAtomicStep`,
  94and the observation is parity. -/
  95abbrev LedgerVecState (d : Nat) : Type := Fin d → ℤ
  96
  97/-- The canonical atomic step relation on a ledger-vector state. -/
  98abbrev ledgerVecStep (d : Nat) : LedgerVecState d → LedgerVecState d → Prop :=
  99  fun x y => coordAtomicStep (d := d) x y
 100
 101/-- The canonical parity observation on a ledger-vector state. -/
 102abbrev ledgerVecParity (d : Nat) : LedgerVecState d → Pattern d :=
 103  fun x => parityPattern x
 104
 105theorem ledgerVecStep_oneBitDiff {d : Nat} {x y : LedgerVecState d} (h : ledgerVecStep d x y) :
 106    OneBitDiff (ledgerVecParity d x) (ledgerVecParity d y) := by
 107  simpa [ledgerVecStep, ledgerVecParity] using
 108    (coordAtomicStep_oneBitDiff (d := d) (x := x) (y := y) h)
 109
 110end LedgerParityAdjacency
 111end IndisputableMonolith

papers checked against this theorem

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