rcl_positive
plain-language theorem explainer
The positivity axiom asserts that the cost function J satisfies J(x) > 0 for every real x > 0 with x ≠ 1. Researchers establishing uniqueness of the Recognition Composition Law from its three axioms would cite this result. The proof is a direct term application of the core lemma Jcost_pos_of_ne_one.
Claim. For every real number $x$ with $x > 0$ and $x ≠ 1$, the cost function satisfies $J(x) > 0$.
background
The Recognition Composition Law module certifies the three axioms that force J to be the unique cost function: normalisation J(1) = 0, reciprocal symmetry J(x) = J(x^{-1}), and positivity J(x) > 0 for x > 0, x ≠ 1. Jcost is the derived cost of the comparator in a multiplicative recognizer and equals the cost of any recognition event. The upstream lemma Jcost_pos_of_ne_one proves the identical positivity statement from the squared expression Jcost x = (x-1)^2 / (x (x-1)^2) after clearing the zero denominator.
proof idea
The proof is a one-line term wrapper that applies the lemma Jcost_pos_of_ne_one directly to the hypotheses hx and hne.
why it matters
This result supplies the positivity component of jcost_uniqueness_axioms, which populates the RCLCert record. It thereby supports the uniqueness theorem that the three axioms plus continuity force J uniquely, consistent with the Recognition Science forcing chain in which J is the self-similar fixed point T5. The module states zero sorrys and zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.