non_existence_has_positive_cost
plain-language theorem explainer
For any positive real x unequal to 1 the recognition cost is strictly positive. Pre-Big-Bang selection arguments cite the result to show that only the unit ratio sits at the global cost minimum. The proof is a direct one-line application of the core positivity lemma for the J-cost function.
Claim. Let $x$ be a positive real number with $x ≠ 1$. Then the J-cost satisfies $0 < Jcost(x)$.
background
The module encodes the cost-first selection principle: a pattern $x > 0$ counts as existing in the recognition sense precisely when its J-cost is zero, which holds if and only if $x = 1$. All other positive ratios are assigned strictly positive cost and are therefore transiently unstable. The J-cost function itself is the derived cost of a multiplicative recognizer comparator on positive ratios; its positivity away from unity is supplied by the upstream lemma Jcost_pos_of_ne_one.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module (also present in JcostCore).
why it matters
The theorem populates the non_existence_costly slot inside the CostFirstExistenceCert definition, which assembles the three structural claims of the cost-first existence principle. It thereby closes the module-level statement that existence is selected by J-minimization rather than posited. Within the Recognition Science framework the result anchors the pre-geometric cost landscape that precedes the emergence of laws and geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.