rs_exists_unique_one
plain-language theorem explainer
The declaration proves that a real number satisfies the RS existence predicate precisely when it equals unity. Researchers tracing the cost-minimization foundation of Recognition Science cite this result to anchor the uniqueness of the stable configuration. The proof is a direct biconditional split that invokes the defect-zero characterization lemma in one direction and the explicit defect value at unity in the other.
Claim. $forall x in mathbb{R}, RSExists(x) iff x = 1$, where $RSExists(x)$ holds precisely when $x > 0$ and the defect of $x$ under the $J$-cost function vanishes.
background
The module OntologyPredicates develops the operational ontology of Recognition Science, where existence emerges from J-cost minimization rather than being assumed. RSExists x is defined as the conjunction of x > 0 and defect x = 0, with defect obtained from the J function that enforces the self-similar fixed point. This uniqueness result rests on two upstream facts: defect_at_one states that the defect at 1 is zero, while defect_zero_iff_one characterizes all positive reals with vanishing defect as exactly the number 1.
proof idea
The term proof introduces x and constructs the biconditional. The forward direction applies defect_zero_iff_one to the defect hypothesis. The reverse direction rewrites the hypothesis to substitute 1 and pairs the trivial positivity proof with defect_at_one.
why it matters
This theorem supplies the uniqueness direction for rs_exists_unique, which asserts exactly one RSExistent value, and for mp_physical, which derives the Meta-Principle as a cost theorem. It also appears in ontology_summary and the Gödel dissolution argument. Within the framework it confirms J-uniqueness by showing that only unity achieves zero defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.