Jcost_phi_pos
plain-language theorem explainer
The lemma establishes that the J-cost of the golden ratio is strictly positive. Researchers deriving the mass gap or uniform failure floor in Recognition Science cite this to secure the base positivity on the phi-ladder. The proof is a direct one-line term application of the general J-cost positivity result for arguments greater than zero and unequal to one.
Claim. $0 < J(phi)$, where $J(x)$ is the J-cost function satisfying $J(x) > 0$ whenever $x > 0$ and $x ≠ 1$, and $phi$ is the golden ratio obeying $phi > 1$.
background
In the Constants module the symbol phi stands for the golden ratio, the unique self-similar fixed point forced by the Recognition Science framework. The J-cost function, imported from the Cost module, is the quadratic deviation $J(x) = (x-1)^2 / x$ (after the square rewrite) that vanishes only at unity. The module itself fixes the fundamental RS time quantum at one tick. This lemma depends on the upstream fact phi_ne_one : phi ≠ 1 (itself from one_lt_phi) and on the general lemma Jcost_pos_of_ne_one, whose doc-comment states: 'J(x) > 0 for x ≠ 1 and x > 0'.
proof idea
The proof is a one-line term wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, supplying the already-established facts phi_pos and phi_ne_one as the two required hypotheses.
why it matters
The result supplies the base positivity J(phi) > 0 that is invoked verbatim in UniformFailureFloor.KTheta_pos and in the Yang-Mills mass-gap statement, where the downstream doc-comment labels it the 'fundamental gap inequality'. It therefore anchors the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain and guarantees that the mass formula on the phi-ladder begins from a positive defect. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.