J_formula_pos
plain-language theorem explainer
The J-cost expression (x + 1/x)/2 - 1 is strictly positive for every positive real x not equal to 1. Researchers building the Recognition Science forcing chain or phi-ladder mass formulas would cite this to guarantee a unique minimum at unity. The proof is a one-line wrapper that applies the strict reciprocal AM-GM inequality and finishes with linear arithmetic.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. Then for all real $x > 0$ with $x ≠ 1$, $J(x) > 0$.
background
The Inequalities module collects fundamental lemmas supporting the Recognition Science framework. J-cost denotes the expression (x + 1/x)/2 - 1 that defines the J-function in the forcing chain. The key upstream lemma am_gm_reciprocal_strict states that x + 1/x > 2 whenever x > 0 and x ≠ 1, with its doc-comment reading 'Strengthened AM-GM: x + 1/x > 2 when x ≠ 1.'
proof idea
The proof calls the strict AM-GM reciprocal theorem to obtain x + 1/x > 2, then applies linear arithmetic to deduce that the J-cost expression is positive.
why it matters
This result secures strict positivity of J-cost away from the fixed point at one, supporting J-uniqueness (T5) and the self-similar fixed point phi (T6) in the forcing chain. It belongs to the foundation inequalities that prepare the eight-tick octave and D = 3 derivations. No downstream citations appear yet, leaving open its role in mass-ladder or Berry-threshold arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.