head

formal source

  17
  18variable {M : RecognitionStructure} (ch : Chain M)
  19
  20def head : M.U := by
  21  have hpos : 0 < ch.n + 1 := Nat.succ_pos _
  22  exact ch.f ⟨0, hpos⟩
  23
  24def last : M.U := by
  25  have hlt : ch.n < ch.n + 1 := Nat.lt_succ_self _
  26  exact ch.f ⟨ch.n, hlt⟩
  27
  28end Chain
  29
  30class AtomicTick (M : RecognitionStructure) where
  31  postedAt : Nat → M.U → Prop
  32  unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u
  33
  34structure Ledger (M : RecognitionStructure) where
  35  debit : M.U → ℤ
  36  credit : M.U → ℤ
  37
  38def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
  39
  40def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
  41  phi L (ch.last) - phi L (ch.head)
  42
  43class Conserves {M} (L : Ledger M) : Prop where
  44  conserve : ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0
  45
  46/-- ## T2 (Atomicity): unique posting per tick implies no collision at a tick. -/
  47theorem T2_atomicity {M} [AtomicTick M] :
  48  ∀ t u v, AtomicTick.postedAt (M:=M) t u → AtomicTick.postedAt (M:=M) t v → u = v := by
  49  intro t u v hu hv
  50  rcases (AtomicTick.unique_post (M:=M) t) with ⟨w, hw, huniq⟩