unity_is_unique_existent
plain-language theorem explainer
The theorem states that the existence predicate holds for a real number if and only if that number equals unity. Recognition Science researchers cite it when closing the existence criterion that follows from the cost functional J. The proof splits on positivity of the argument, invokes the prior law_of_existence for the positive case, and derives a contradiction from the definition of Exists otherwise.
Claim. $For all real $x$, the predicate $0 < x$ and $J(x) = 0$ holds if and only if $x = 1$.
background
The module CostAxioms formalizes three primitive axioms for the Recognition Science cost framework: normalization F(1)=0, the Recognition Composition Law, and calibration of the second logarithmic derivative at zero. From these the unique cost function J(x) = ½(x + x⁻¹) - 1 is derived, with J(1) = 0 as the sole minimum. The sibling definition Exists(x) is the predicate 0 < x ∧ J(x) = 0, which encodes that a ratio is realizable precisely when it sits at this cost minimum. The upstream theorem law_of_existence already shows that for positive x the predicate is equivalent to x = 1; the present result removes the positivity hypothesis.
proof idea
The term proof begins with an introduction of the arbitrary real x. It performs case analysis on whether 0 < x. In the positive case it applies the upstream law_of_existence directly. In the non-positive case it rewrites the Exists predicate, shows that the left-to-right direction forces positivity (contradicting the case assumption), and shows that the right-to-left direction requires x = 1 which is positive and satisfies J(1) = 0.
why it matters
This result completes the existence criterion inside the cost axioms, confirming that unity is the sole fixed point of J and therefore the unique existent. It sits at Level 2 of the axiomatic hierarchy in the module documentation and directly supports the derived Meta-Principle that nothing cannot recognize itself because J(0) diverges. The declaration feeds the uniqueness step T5 of the forcing chain and supplies the base case for later derivations of the eight-tick octave and spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.