nothing_cannot_recognize_itself

formal source

  25abbrev NothingCannotRecognizeItself : Prop := MP
  26
  27/-- Direct alias proof of MP for the manuscript phrasing. -/
  28theorem nothing_cannot_recognize_itself : NothingCannotRecognizeItself :=
  29  mp_holds
  30
  31structure RecognitionStructure where
  32  U : Type
  33  R : U → U → Prop
  34
  35structure Chain (M : RecognitionStructure) where
  36  n : Nat
  37  f : Fin (n+1) → M.U
  38  ok : ∀ i : Fin n, M.R (f i.castSucc) (f i.succ)
  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