`Distinguishable`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Indistinguishable
domain: RecogGeom
line: 134 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Indistinguishable on GitHub at line 134.

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

 131/-! ## Distinguishability -/
 132
 133/-- Two configurations are distinguishable if they produce different events -/
 134def Distinguishable {C E : Type*} (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
 135  r.R c₁ ≠ r.R c₂
 136
 137/-- Distinguishability is the negation of indistinguishability -/
 138theorem distinguishable_iff_not_indistinguishable {c₁ c₂ : C} :
 139    Distinguishable r c₁ c₂ ↔ ¬(c₁ ~[r] c₂) := Iff.rfl
 140
 141/-- There exist distinguishable configurations (by nontriviality) -/
 142theorem exists_distinguishable :
 143    ∃ c₁ c₂ : C, Distinguishable r c₁ c₂ :=
 144  r.nontrivial
 145
 146/-! ## Module Status -/
 147
 148def indistinguishable_status : String :=
 149  "✓ Indistinguishable relation defined (RG3)\n" ++
 150  "✓ Proved: reflexivity, symmetry, transitivity\n" ++
 151  "✓ Proved: indistinguishable_equivalence\n" ++
 152  "✓ ResolutionCell defined (equivalence classes)\n" ++
 153  "✓ Proved: resolutionCell_eq_fiber\n" ++
 154  "✓ Proved: resolutionCells_partition\n" ++
 155  "✓ LocalResolution defined\n" ++
 156  "✓ Distinguishable defined\n" ++
 157  "\n" ++
 158  "INDISTINGUISHABILITY (RG3) COMPLETE"
 159
 160#eval indistinguishable_status
 161
 162end RecogGeom
 163end IndisputableMonolith

papers checked against this theorem

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