RSExists
plain-language theorem explainer
RSExists identifies a positive real number whose defect under the J-cost functional vanishes exactly. Researchers deriving physical existence from cost minimization cite this predicate when establishing uniqueness of the stable point. The definition is introduced directly as the conjunction of positivity and zero defect, serving as the base predicate for stability and discreteness results.
Claim. A real number $x$ satisfies the recognition existence predicate when $x > 0$ and the defect functional of $x$ equals zero, where defect coincides with the J-cost for positive arguments.
background
The OntologyPredicates module formalizes the operational ontology of Recognition Science by defining existence and truth as outcomes of cost minimization under the unique J function rather than as primitives. The defect functional is supplied by the LawOfExistence module as defect(x) := J(x), with J the cost satisfying the Recognition Composition Law. Upstream results from CostFirstExistence establish that defect vanishes only at unity and that positive values with zero defect are the stable configurations under the forcing chain.
proof idea
This declaration is a direct definition that conjoins the positivity condition with the zero-defect requirement. No lemmas or tactics are invoked beyond the identification of defect with J from the LawOfExistence import.
why it matters
This predicate supplies the existence notion used in CostFirstExistenceCert to certify that the only RS-existent value is unity and that non-unit positive reals incur positive J-cost. It underpins the DiscretenessForcing theorems by providing the stable existence concept that forces discrete configuration spaces. In the framework it operationalizes the selection rule derived from the T5 J-uniqueness and T6 self-similar fixed point, feeding the T7-T8 chain that yields D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.