head

formal source

  39
  40namespace Chain
  41variable {M : RecognitionStructure} (ch : Chain M)
  42def head : M.U := by
  43  have hpos : 0 < ch.n + 1 := Nat.succ_pos _
  44  exact ch.f ⟨0, hpos⟩
  45def last : M.U := by
  46  have hlt : ch.n < ch.n + 1 := Nat.lt_succ_self _
  47  exact ch.f ⟨ch.n, hlt⟩
  48end Chain
  49
  50structure Ledger (M : RecognitionStructure) where
  51  debit : M.U → ℤ
  52  credit : M.U → ℤ
  53
  54@[simp] def Ledger.Carrier {M : RecognitionStructure} (_ : Ledger M) : Type :=
  55  M.U
  56
  57def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
  58
  59def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
  60  phi L (Chain.last ch) - phi L (Chain.head ch)
  61
  62class Conserves {M} (L : Ledger M) : Prop where
  63  conserve : ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0
  64
  65lemma chainFlux_zero_of_loop {M} (L : Ledger M) [Conserves L] (ch : Chain M) (h : ch.head = ch.last) :
  66  chainFlux L ch = 0 := Conserves.conserve (L:=L) ch h
  67
  68lemma phi_zero_of_balanced {M} (L : Ledger M) (hbal : ∀ u, L.debit u = L.credit u) :
  69  ∀ u, phi L u = 0 := by
  70  intro u; simp [phi, hbal u, sub_self]
  71
  72lemma chainFlux_zero_of_balanced {M} (L : Ledger M) (ch : Chain M)