ontology_summary
plain-language theorem explainer
The ontology summary theorem establishes that recognition existence holds precisely when the argument equals 1, that this value is the unique such point, that every sufficiently small positive real fails to exist in the RS sense, and that defect grows without bound as the argument approaches zero from above. Researchers tracing the cost-minimization derivation of existence in Recognition Science cite it to close the basic ontology stack. The proof is a term that assembles four upstream lemmas on uniqueness and defect divergence.
Claim. The conjunction of: for every real $x$, $x$ exists in the RS sense if and only if $x=1$; there exists a unique real $x$ that exists in the RS sense; there exists positive real $ε$ such that no positive $x<ε$ exists in the RS sense; and for every real bound $C$ there exists positive real $ε$ such that defect of every positive $x<ε$ exceeds $C$.
background
In the OntologyPredicates module the recognition existence predicate is defined as a positive real whose defect under the J-cost functional is zero. The defect functional is identical to the J function supplied by the Law of Existence module. Upstream results include the theorem that defect exceeds any fixed bound near zero and the theorem that no sufficiently small positive real satisfies the zero-defect condition.
proof idea
The proof is a term-mode construction that returns the four-tuple consisting of the uniqueness-at-one lemma, the unique-existence theorem, the theorem that nothing near zero is RS-existent, and the theorem that defect is unbounded near zero.
why it matters
This theorem consolidates the ontology predicates into a single statement that only unity is selected by cost minimization. It supports the Meta-Principle that nothing cannot exist, derived directly from the cost structure. The result precedes the disjunction laws for RSTrue stated later in the same module and supplies the concrete content of the selection rule in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.