Jcost_phi_pos
plain-language theorem explainer
The declaration proves that the J-cost of the golden ratio is strictly positive. Researchers working on the phase-budget engine or the Yang-Mills mass gap would cite this result to establish the uniform failure floor K_Θ = J(φ)/45. The proof proceeds as a one-line wrapper invoking the general positivity lemma for the J-cost function at arguments other than one.
Claim. $0 < J(φ)$, where $J$ is the J-cost function and $φ$ is the golden ratio.
background
The Uniform Failure Floor module defines the RS floor scale K_Θ := J(φ)/45 for use in the phase-budget engine and proves only positivity results. The J-cost function satisfies J(x) > 0 whenever x > 0 and x ≠ 1. This rests on the upstream lemma Jcost_pos_of_ne_one, which rewrites Jcost via Jcost_eq_sq and applies positivity of squares together with division, plus the fact phi_ne_one : φ ≠ 1 from PhiLadderLattice.
proof idea
This is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one to the arguments phi, phi_pos, and phi_ne_one.
why it matters
This theorem supplies the fundamental gap inequality J(φ) > 0 required for the mass gap in Yang-Mills unification. It directly feeds the proof of KTheta_pos : 0 < KTheta in the same module, which supports the phase-budget engine. In the Recognition Science framework it anchors positivity at the self-similar fixed point φ, consistent with J-uniqueness (T5) and the phi fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.