nothing_not_rs_exists
plain-language theorem explainer
The theorem shows that no positive real sufficiently close to zero satisfies RSExists, where this predicate holds exactly when the value is positive and its defect vanishes. Researchers deriving the operational ontology of Recognition Science cite the result to establish that the meta-principle follows from the J-cost structure. The proof instantiates the unbounded defect lemma at threshold 1, assumes RSExists for a small positive argument, and reaches a contradiction by rewriting the defect equality and applying linear arithmetic.
Claim. $∃ ε > 0, ∀ x, 0 < x → x < ε → ¬RSExists x$, where RSExists x holds precisely when $x > 0$ and defect$(x) = 0$.
background
The OntologyPredicates module supplies the operational definitions of the Recognition Science ontology. RSExists x is the proposition 0 < x ∧ defect x = 0, with the defect functional defined in the LawOfExistence module as defect x := J x. The module documentation lists this theorem as one of four key results that make existence a verifiable selection outcome rather than a primitive notion.
proof idea
The proof obtains ε from the sibling lemma nothing_unbounded_defect applied at constant 1. It then assumes for contradiction that a small positive x satisfies RSExists x, which forces defect x = 0. The lemma supplies defect x > 1; rewriting the equality and invoking linarith produces the contradiction.
why it matters
The result is invoked directly inside the ontology_summary theorem, which assembles the full predicate stack: RSExists holds only at 1, the existent value is unique, and no value near zero is RSExistent. It corresponds to key theorem 3 in the module documentation and supplies the cost-theoretic content of the meta-principle that defect(0⁺) diverges. In the broader framework it confirms that existence is determined by cost minimization under the unique J function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.