phiVec

formal source

  57
  58abbrev LedgerState (d : Nat) : Type := Recognition.Ledger (AccountRS d)
  59
  60abbrev phiVec {d : Nat} (L : LedgerState d) : Fin d → ℤ :=
  61  Recognition.phi L
  62
  63abbrev parity (d : Nat) (L : LedgerState d) : Pattern d :=
  64  parityPattern (phiVec (d := d) L)
  65
  66/-! ## Posting model -/
  67
  68inductive Side where
  69  | debit
  70  | credit
  71deriving DecidableEq, Repr
  72
  73/-- Apply a single unit post (either debit or credit) at account `k`. -/
  74noncomputable def post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) : LedgerState d := by
  75  classical
  76  exact match side with
  77  | Side.debit =>
  78      { debit := fun i => if i = k then L.debit i + 1 else L.debit i
  79      , credit := L.credit }
  80  | Side.credit =>
  81      { debit := L.debit
  82      , credit := fun i => if i = k then L.credit i + 1 else L.credit i }
  83
  84@[simp] lemma phiVec_post_debit {d : Nat} (L : LedgerState d) (k : Fin d) (i : Fin d) :
  85    phiVec (d := d) (post L k Side.debit) i =
  86      (if i = k then phiVec (d := d) L i + 1 else phiVec (d := d) L i) := by
  87  by_cases hik : i = k
  88  · subst hik
  89    simp [post, phiVec, Recognition.phi]
  90    ring_nf