`ConfigSpace`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Core
domain: RecogGeom
line: 33 · 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 33.

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

used by

formal source

  30    get the configuration itself; they get events.
  31
  32    RG0: There exists a nonempty configuration space. -/
  33class ConfigSpace (C : Type*) where
  34  /-- The configuration space is nonempty -/
  35  nonempty : Nonempty C
  36
  37/-- Extract a witness configuration from a ConfigSpace -/
  38noncomputable def ConfigSpace.witness (C : Type*) [cs : ConfigSpace C] : C :=
  39  cs.nonempty.some
  40
  41/-! ## Event Space -/
  42
  43/-- An event space is a type of observable outcomes.
  44    Events are things like "the needle points this direction,"
  45    "the detector clicks," or "the image matches this template." -/
  46class EventSpace (E : Type*) where
  47  /-- The event space has at least two distinct events
  48      (otherwise recognition is trivial) -/
  49  nontrivial : ∃ e₁ e₂ : E, e₁ ≠ e₂
  50
  51/-- An event space with decidable equality -/
  52class DecEventSpace (E : Type*) extends EventSpace E where
  53  /-- Decidable equality on events -/
  54  decEq : DecidableEq E
  55
  56attribute [instance] DecEventSpace.decEq
  57
  58/-! ## Basic Properties -/
  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⟩

papers checked against this theorem

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