phiLadder_gt_one
plain-language theorem explainer
The theorem shows that every positive integer power of the golden ratio on the φ-ladder exceeds 1. Researchers deriving the Yang-Mills mass gap from the J-cost functional cite it to place all non-vacuum excitations strictly above the vacuum state. The argument is a one-line wrapper that chains the base inequality 1 < φ through the monotonicity result for positive rungs.
Claim. For every integer $n$ with $n ≥ 1$, $φ^n > 1$, where $φ$ is the golden ratio and $φ^n$ denotes the element at rung $n$ of the φ-ladder.
background
The module treats the Yang-Mills mass gap as an exact consequence of the recognition cost $J(x) = ½(x + x^{-1}) - 1$ evaluated on the discrete φ-lattice. The φ-ladder is the set of all elements $φ^n$ for $n ∈ ℤ$, with the sibling definition PhiLadder n := $φ^n$. The upstream lemma one_lt_phi supplies the base fact $1 < φ$ that anchors ordering on the positive side.
proof idea
The proof is a one-line wrapper that applies lt_of_lt_of_le to one_lt_phi and the monotonicity statement phiLadder_ge_phi hn. This lifts the strict inequality at the first rung to every higher positive rung without further calculation.
why it matters
It supplies the strict positivity required by the downstream theorem spectral_gap_pos_rung, which establishes $J(φ) ≤ J(φ^n)$ for $n ≥ 1$ and therefore that every non-vacuum φ-ladder configuration costs at least Δ. The step closes part of the spectral-gap argument in the Recognition Science resolution of the Millennium problem, where the gap emerges from T5 J-uniqueness and T6 phi fixed point with no free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.