Jcost_phi_pos
J(φ) > 0 holds for the golden ratio φ. Researchers deriving the mass gap or uniform failure floor in Recognition Science cite this result. The proof is a one-line term application of the general J-cost positivity lemma at arguments other than one.
claim$0 < J(φ)$ where $J(x) = (x-1)^2 / x$ for $x > 0$ and $φ$ is the golden ratio satisfying $φ > 1$.
background
The J-cost function quantifies recognition defect for a scaling factor x. From the Cost module, J(x) > 0 holds exactly when x > 0 and x ≠ 1, via the identity J(x) = (x-1)^2 / x together with positivity of squares for nonzero arguments. The golden ratio φ satisfies φ > 1 (hence φ ≠ 1) by the phi_pos and phi_ne_one lemmas. This lemma lives in the Constants module, which collects RS-native constants with the fundamental time quantum set to one tick. It depends on the general Jcost_pos_of_ne_one result.
proof idea
The proof is a term-mode one-line wrapper that applies Jcost_pos_of_ne_one directly to phi using phi_pos and phi_ne_one. No additional tactics appear.
why it matters in Recognition Science
This lemma supplies the fundamental gap inequality J(φ) > 0. It is invoked in UniformFailureFloor to prove KTheta_pos and in YangMillsMassGap as the base gap inequality. It closes the positivity step for the self-similar fixed point φ in the T5-T6 forcing chain of the Recognition framework.
scope and limits
- Does not prove J(x) > 0 for any x other than φ.
- Does not compute a numerical value for J(φ).
- Does not address the case x ≤ 0.
- Does not derive the algebraic definition of Jcost.
Lean usage
unfold KTheta; exact div_pos Jcost_phi_pos (by norm_num : (0 : ℝ) < 45)formal statement (Lean)
517lemma Jcost_phi_pos : 0 < Cost.Jcost phi :=
proof body
Term-mode proof.
518 Cost.Jcost_pos_of_ne_one _ phi_pos phi_ne_one
519
520end Constants
521end IndisputableMonolith