rs_exists_unique
plain-language theorem explainer
The theorem asserts that exactly one real number satisfies the RS existence predicate. Researchers deriving the Recognition Science ontology cite it when establishing that cost-minimizing stable configurations are unique. The term-mode proof supplies the witness 1 and closes uniqueness by direct appeal to the one-point lemma rs_exists_unique_one.
Claim. There exists a unique real number $x$ such that $x > 0$ and the defect of $x$ equals zero.
background
In Recognition Science the predicate RSExists selects stable positive configurations under the J-cost functional. It is defined as the conjunction of positivity and zero defect, where defect coincides with J for positive reals. This replaces primitive existence with an outcome of cost minimization under the Recognition Composition Law.
proof idea
The term-mode proof exhibits the witness 1, applies the existence lemma rs_exists_one to satisfy the existential, then invokes rs_exists_unique_one to obtain the uniqueness direction. The constructor splits the unique-existential into its two conjuncts.
why it matters
This result supplies the uniqueness half of the RS ontology stack and is invoked directly in mp_physical (the cost-derived Meta-Principle) and ontology_summary. It also feeds the Gödel dissolution theorems by guaranteeing a single stable configuration. Within the forcing chain it realizes T5 J-uniqueness by showing that the fixed point at unity is the sole point with vanishing defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.