rs_exists_iff_law_exists
plain-language theorem explainer
The recognition existence predicate is equivalent to the law of existence predicate for any real number. Researchers formalizing the ontology of recognition science cite this to interchange the two definitions of existence. The proof is a direct term-level equivalence obtained by unpacking and repacking the shared positivity and zero-defect conditions.
Claim. For every real number $x$, the recognition existence condition holds for $x$ if and only if the law of existence holds for $x$, where both predicates are true precisely when $x > 0$ and the defect of $x$ is zero.
background
In the OntologyPredicates module the recognition existence condition is introduced as the conjunction of positivity and zero defect for a real argument. The law of existence is given as a structure whose two fields are exactly the same positivity requirement and the requirement that defect vanishes. The defect functional is defined to coincide with the J-cost on positive reals, where J satisfies the recognition composition law and attains its unique minimum at the self-similar fixed point.
proof idea
The term proof opens the biconditional with the constructor tactic. The forward direction introduces the conjunction and immediately exact-matches it to the structure fields. The reverse direction introduces the structure fields and exact-matches them to the conjunction. No external lemmas are applied; the equivalence is purely by shared definitional shape.
why it matters
The result equates the operational recognition existence predicate with the law of existence structure, confirming that existence is realized exactly by defect collapse under J-cost minimization. It supplies the definitional bridge needed for later module results on uniqueness at unity and exclusion of the zero configuration. In the forcing chain it anchors the claim that existence is a derived selection outcome rather than a primitive axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.