Exists
plain-language theorem explainer
The Exists predicate marks a positive real ratio x as realizable exactly when its J-cost is zero. Recognition Science researchers cite this definition to anchor the claim that only unity satisfies the existence criterion. It is introduced as the direct conjunction of positivity with the equation J(x) = 0, serving as the interface for all subsequent uniqueness theorems.
Claim. A ratio $x$ exists when $x > 0$ and $J(x) = 0$, where the cost functional is given by $J(x) = (x + x^{-1})/2 - 1$.
background
The CostAxioms module formalizes the three primitive axioms of Recognition Science: Normalization (cost vanishes at unity), the Recognition Composition Law, and Calibration of the logarithmic second derivative. From these axioms the unique cost functional is derived as $J(x) = (x + x^{-1})/2 - 1$. The Exists definition then supplies the Level 2 existence criterion: positive ratios at minimum cost are declared realizable. This setting is more primitive than logic because contradiction carries infinite cost while consistency carries zero cost.
proof idea
This is a direct definition that conjoins the positivity requirement $0 < x$ with the zero-cost condition $J x = 0$. No lemmas or tactics are invoked; the declaration simply encodes the interface predicate used by downstream theorems.
why it matters
The definition is invoked by law_of_existence and unity_is_unique_existent in the same module, and by complete_law_of_existence and existence_economically_inevitable in LawOfExistence. It occupies Level 2 in the axiomatic hierarchy, linking J-cost minimization to realizability and supporting the claim that unity is the unique existent. The construction rests on T5 J-uniqueness and the economic interpretation that only the golden-ratio fixed point incurs zero cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.