rs_exists_one
plain-language theorem explainer
The declaration shows that unity satisfies the RS existence predicate: it is positive and has vanishing defect under the J-cost function. Foundational work in Recognition Science cites this when establishing that existence is uniquely realized at 1 or when deriving consequences of the meta-principle. The proof proceeds by a direct term construction that invokes numerical normalization for positivity together with the lemma that defect vanishes at 1.
Claim. The number 1 is RS-existent, that is, $1 > 0$ and the defect of 1 vanishes: defect$(1) = 0$.
background
In the OntologyPredicates module, RSExists x is defined as the conjunction of x being positive and having zero defect, where defect measures deviation from the J-cost minimum. This operationalizes existence as a cost-minimization outcome rather than a primitive. The result relies on the upstream theorem defect_at_one, which states that defect 1 = 0, and on the definition of RSExists from CostFirstExistence as Jcost x = 0.
proof idea
The proof is a term-mode construction that directly supplies the two conjuncts of the RSExists definition. It uses norm_num to confirm positivity of 1 and applies the defect_at_one lemma to obtain the zero-defect condition.
why it matters
This result supplies the base case for uniqueness of the RS-existent value and for the meta-principle forcing existence. It is invoked in rs_exists_unique to show there is exactly one such value and in mp_forces_existence to witness the existential claim. In the framework it anchors the selection rule that only unity is stable under J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.