j_positive_off_fixed_point
plain-language theorem explainer
J-cost is strictly positive for every positive real except the fixed point at one. Researchers formalizing the recognition ledger's multiplicative bounds cite this when establishing cost positivity away from equilibrium. The proof is a direct one-line application of the underlying J-cost positivity lemma.
Claim. For every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $J(x) > 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
In Recognition Science the J-cost function quantifies deviation from the multiplicative fixed point in the discrete ledger. The PrimeLedgerStructure module treats natural numbers as transactions, with primes as irreducible entries, and shows that the cost function obeys the d'Alembert equation whose solutions have zeros confined to lines. The present theorem supplies the elementary positivity fact needed before the structural identification between J-cost symmetry and the zeta functional equation can be stated.
proof idea
The proof is a one-line wrapper that applies the lemma Cost.Jcost_pos_of_ne_one directly to the hypotheses 0 < x and x ≠ 1.
why it matters
The result is a prerequisite for the d'Alembert satisfaction theorems that underwrite the RS prediction of the Riemann Hypothesis (critical line as ledger balance). It closes the basic positivity step in the chain from T5 J-uniqueness through the reciprocal symmetry J(x) = J(1/x) to the structural parallel with the completed zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.