recognition_implies_existence

formal source

  42  exact ⟨x⟩
  43
  44/-- Constructive version: recognition implies existence. -/
  45theorem recognition_implies_existence {X : Type*}
  46    (h : ∃ (R : X → X → Prop), ∃ x, R x x) : Nonempty X :=
  47  MetaPrinciple X h
  48
  49/-- The contrapositive: emptiness implies no self-recognition. -/
  50theorem empty_has_no_self_recognition (X : Type*) (h : IsEmpty X) :
  51    ¬(∃ (R : X → X → Prop), ∃ x, R x x) := by
  52  intro ⟨_, x, _⟩
  53  exact h.elim x
  54
  55/-! ## Recognition Structure -/
  56
  57/-- A recognition structure on a type.
  58
  59This captures the minimal structure needed for "things to be recognized."
  60-/
  61structure RecognitionStructure (X : Type*) where
  62  /-- The recognition relation: R x y means "x recognizes y". -/
  63  recognizes : X → X → Prop
  64  /-- At least one thing can recognize itself (closure). -/
  65  has_self_recognition : ∃ x, recognizes x x
  66
  67/-- Any recognition structure implies nonemptiness. -/
  68theorem recognition_structure_nonempty {X : Type*}
  69    (R : RecognitionStructure X) : Nonempty X :=
  70  MetaPrinciple X ⟨R.recognizes, R.has_self_recognition⟩
  71
  72/-! ## From Recognition to Ledger -/
  73
  74/-- A minimal ledger: balanced debits and credits. -/
  75structure MinimalLedger (X : Type*) where