abbrev
definition
ledgerVecStep
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.LedgerParityAdjacency on GitHub at line 98.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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