`exists_distinguishable`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogGeom.Indistinguishable on GitHub at line 142.

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

 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.