phiLadder_ge_phi

The phi-ladder is the map sending each integer n to phi raised to n, where phi is the golden ratio; it supplies the discrete substrate of stable positions forced by the self-similar fixed-point condition. The module derives the Yang-Mills mass gap from the J-cost functional J(x) equals one-half times (x plus x inverse) minus 1, showing that every non-vacuum excitation on this lattice costs at least Delta equals J(phi) approximately 0.118. The present result rests on the upstream fact that phi exceeds 1, established by direct comparison with the square root of 5 in the Constants module.

The proof unfolds the ladder definition to obtain phi to the power n, rewrites phi as phi to the power 1, and applies the monotonicity lemma for real exponentiation (zpow_le_zpow_right_0) using the hypothesis that n is at least 1 together with the fact that phi exceeds 1.

This monotonicity statement is invoked by the immediate successor theorems that establish phi to the n exceeds 1 and that J(phi) is less than or equal to J(phi to the n) for positive rungs, thereby locating the minimal positive cost at the first rung. It supplies the concrete step needed for the spectral-gap theorem that every non-vacuum phi-ladder configuration costs at least Delta, which is the Recognition Science resolution of the Millennium problem via the J-cost functional and the phi-forcing chain. The result touches the open question of extending the gap statement to the full bidirectional ladder including negative rungs.