`event_nontrivial`

proved

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Core
domain: RecogGeom
line: 66 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogGeom.Core on GitHub at line 66.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  63  ⟨ConfigSpace.witness C, rfl⟩
  64
  65/-- An event space has at least two distinct elements -/
  66theorem event_nontrivial (E : Type*) [EventSpace E] : ∃ e₁ e₂ : E, e₁ ≠ e₂ :=
  67  EventSpace.nontrivial
  68
  69/-! ## Recognition Triple -/
  70
  71/-- A recognition triple bundles a configuration space, event space,
  72    and the implicit structure connecting them. This is the basic
  73    object of study in recognition geometry. -/
  74structure RecognitionTriple where
  75  /-- The type of configurations -/
  76  Config : Type*
  77  /-- The type of events -/
  78  Event : Type*
  79  /-- Configurations form a valid configuration space -/
  80  configSpace : ConfigSpace Config
  81  /-- Events form a valid event space -/
  82  eventSpace : EventSpace Event
  83
  84/-! ## Module Status -/
  85
  86def core_status : String :=
  87  "✓ ConfigSpace defined (RG0)\n" ++
  88  "✓ EventSpace defined\n" ++
  89  "✓ Nonemptiness axiom established\n" ++
  90  "✓ Nontriviality axiom established\n" ++
  91  "✓ RecognitionTriple bundle defined\n" ++
  92  "\n" ++
  93  "CORE FOUNDATION COMPLETE"
  94
  95#eval core_status
  96

papers checked against this theorem

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