`config_exists`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Core on GitHub at line 62.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  59
  60/-- **THEOREM**: A configuration space has at least one element.
  61    Replaces the vacuous `∃ c : C, True` with a constructive witness. -/
  62theorem config_exists (C : Type*) [cs : ConfigSpace C] : ∃ c : C, c = ConfigSpace.witness C :=
  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" ++

papers checked against this theorem

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