Jcost_mono_gt_one
plain-language theorem explainer
The recognition cost functional J is monotone on (1, ∞): if 1 < y ≤ x then J(y) ≤ J(x). Researchers resolving the Yang-Mills mass gap via the phi-ladder would cite this to confirm the minimal excitation cost occurs at the lowest rung. The proof reduces the difference J(x) − J(y) to the factored form (x − y)(xy − 1)/(2xy) and verifies non-negativity by elementary inequalities.
Claim. Let $J(z) = ½(z + z^{-1}) - 1$ for real $z > 0$. If $1 < y ≤ x$, then $J(y) ≤ J(x)$.
background
In Recognition Science the cost functional is defined by $J(x) = ½(x + x^{-1}) - 1$. This functional satisfies the Recognition Composition Law and is forced by the J-uniqueness step of the unified forcing chain. The present theorem operates inside the module establishing the Yang-Mills mass gap, where the phi-ladder supplies the discrete spectrum of excitations. The local setting is the spectral-gap analysis: the vacuum sits at J = 0 while every non-trivial rung carries positive cost bounded below by J(φ). Upstream results on the structure of J-cost supply the algebraic identity used here.
proof idea
The proof first obtains positivity of x and y from the strict inequalities. It then derives the exact difference identity J(x) − J(y) = (x − y)(xy − 1)/(2xy) by unfolding the definition and clearing denominators. Non-negativity follows by applying mul_nonneg to the factors (x − y) ≥ 0 and (xy − 1) > 0 together with positivity of the denominator.
why it matters
This monotonicity result is invoked by the spectral-gap theorem for positive rungs, which states that J(φ) ≤ J(φ^n) for all integers n ≥ 1. It fills the §3 slot in the module's outline, confirming that the minimal excitation cost on the phi-ladder occurs at |n| = 1 and equals the Yang-Mills gap Δ = (√5 − 2)/2. The result rests on the J-uniqueness and phi-forcing steps of the foundational chain and supports the claim that the gap is universal across gauge sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.