`RSExists`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OntologyPredicates
domain: Foundation
line: 61 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OntologyPredicates on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  58
  59    This is the operational definition of "existence" in RS.
  60    It's not assumed - it's the result of selection by cost minimization. -/
  61def RSExists (x : ℝ) : Prop := 0 < x ∧ defect x = 0
  62
  63/-- RSExists is equivalent to the Law of Existence predicate. -/
  64theorem rs_exists_iff_law_exists {x : ℝ} :
  65    RSExists x ↔ LawOfExistence.Exists x := by
  66  constructor
  67  · intro ⟨hpos, hdef⟩
  68    exact ⟨hpos, hdef⟩
  69  · intro ⟨hpos, hdef⟩
  70    exact ⟨hpos, hdef⟩
  71
  72/-- RSExists is equivalent to defect = 0 (for positive values). -/
  73theorem rs_exists_iff_defect_zero {x : ℝ} (hx : 0 < x) :
  74    RSExists x ↔ defect x = 0 := by
  75  constructor
  76  · intro ⟨_, hdef⟩; exact hdef
  77  · intro hdef; exact ⟨hx, hdef⟩
  78
  79/-- The only RSExistent value is 1. -/
  80theorem rs_exists_unique_one : ∀ x : ℝ, RSExists x ↔ x = 1 := by
  81  intro x
  82  constructor
  83  · intro ⟨hpos, hdef⟩
  84    exact (defect_zero_iff_one hpos).mp hdef
  85  · intro hx
  86    rw [hx]
  87    exact ⟨by norm_num, defect_at_one⟩
  88
  89/-- Unity is the unique RSExistent configuration. -/
  90theorem rs_exists_one : RSExists 1 := ⟨by norm_num, defect_at_one⟩
  91

papers checked against this theorem

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