rs_exists_iff_defect_zero
plain-language theorem explainer
The equivalence shows that a positive real satisfies the RS existence predicate exactly when its defect vanishes. Researchers formalizing the operational ontology of Recognition Science cite this when reducing existence to J-cost stability. The proof is a direct constructor on the biconditional that matches the two conjuncts of the RSExists definition against the positivity hypothesis and the defect equality.
Claim. For any real number $x > 0$, the predicate RSExists($x$) holds if and only if defect($x$) = 0.
background
The OntologyPredicates module defines RSExists($x$) as the conjunction $0 < x$ and defect($x$) = 0. Here defect coincides with the J functional, so the predicate selects configurations that are stable under cost minimization. The module presents this as the operational content of the selection rule: existence is the outcome of coercive projection rather than a primitive notion.
proof idea
The term proof applies constructor to the biconditional. The left-to-right direction extracts the defect equality from the definition of RSExists. The right-to-left direction pairs the supplied positivity hypothesis with the defect equality to rebuild the RSExists conjunction.
why it matters
This supplies the first key theorem listed in the module documentation, directly tying RSExists to vanishing defect and thereby to J-cost minimization. It supports the meta-principle that nothing cannot recognize itself by excluding the zero configuration. In the forcing chain it reinforces the uniqueness property of the J function as the selector of stable points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.