`Recognize`

definition

show as: view math explainer →

module: IndisputableMonolith.Recognition
domain: Recognition
line: 12 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Recognition on GitHub at line 12.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

   9abbrev Nothing := Empty
  10
  11/-- Minimal recognizer→recognized pairing. -/
  12structure Recognize (A : Type) (B : Type) : Type where
  13  recognizer : A
  14  recognized : B
  15
  16/-- MP: It is impossible for Nothing to recognize itself. -/
  17def MP : Prop := ¬ ∃ _ : Recognize Nothing Nothing, True
  18
  19theorem mp_holds : MP := by
  20  intro h
  21  rcases h with ⟨⟨r, _⟩, _⟩
  22  cases r
  23
  24/-- Alias used in the manuscript: "Nonexistence cannot recognize itself." -/
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.