RSReal_gen_iff
The equivalence shows that x satisfies the generalized RS-real predicate for skeleton D precisely when x equals 1 and lies in D. Researchers formalizing the cost-based ontology of Recognition Science cite this when collapsing statements about arbitrary discrete skeletons to the single stable point. The proof is a one-line simp wrapper that unfolds the definition of RSReal_gen and substitutes the uniqueness of RSExists.
claimLet $Dsubseteqmathbb{R}$ be a discrete skeleton and $xinmathbb{R}$. Then $x$ is RS-real with respect to $D$ if and only if $x=1$ and $xin D$.
background
The OntologyPredicates module supplies the operational ontology of Recognition Science, where existence is a selection outcome under J-cost minimization rather than a primitive. RSExists x holds precisely when the defect of x collapses to zero, yielding a stable configuration. RSReal_gen D x is defined as the conjunction of RSExists x and membership of x in the skeleton D. The upstream theorem rs_exists_unique_one states that RSExists x holds if and only if x equals 1, obtained by showing that defect zero forces the fixed point at unity.
proof idea
The proof is a one-line wrapper that applies simp with the unfolding of RSReal_gen together with the uniqueness lemma rs_exists_unique_one. This substitution directly replaces the RSExists conjunct by the condition x=1, leaving the stated biconditional.
why it matters in Recognition Science
The result anchors the generalized RS-real predicate (Paper Eq. 8) to the unique existent value 1 already established by rs_exists_unique_one. It supports the selection rule that existence is equivalent to defect collapse under the J function and feeds the chain toward discreteness forcing and the eight-tick octave. No downstream uses appear yet, but the equivalence closes a basic reduction step in the foundation.
scope and limits
- Does not prove that 1 belongs to any given skeleton D.
- Does not address continuous or non-real domains.
- Does not treat stability under recognition iteration beyond the uniqueness of RSExists.
formal statement (Lean)
490theorem RSReal_gen_iff {D : Set ℝ} {x : ℝ} :
491 RSReal_gen D x ↔ x = 1 ∧ x ∈ D := by
proof body
One-line wrapper that applies simp.
492 simp only [RSReal_gen, rs_exists_unique_one]
493