phi_gt_one
plain-language theorem explainer
The theorem establishes that the golden ratio φ exceeds 1. Researchers deriving beta functions or mass ladders on the RS φ-ladder cite this inequality to guarantee positive scaling. The proof unfolds the definition of φ and applies the strict monotonicity of the square root to compare 1 and sqrt(5), then closes with linarith.
Claim. $1 < phi$, where $phi = (1 + sqrt(5))/2$ is the positive fixed point of the self-similarity equation.
background
The module develops renormalization group flow and running couplings from the RS φ-ladder. The golden ratio φ is the self-similar fixed point forced at T6 of the UnifiedForcingChain. Upstream results supply rung as an integer label on the ladder for fermions, quarks, and ore classes, together with the PrimitiveDistinction theorem that extracts four structural conditions from seven axioms.
proof idea
The proof unfolds φ. It rewrites 1 as sqrt(1) and invokes sqrt monotonicity to obtain 1 < sqrt(5). Linarith then yields the target inequality.
why it matters
This inequality is required for every subsequent ladder derivative in the module, including the beta-function structure β(g) = (1/ln φ) dg/dr and the asymptotic-freedom criteria for QCD. It anchors the positive scaling used in the eight-tick octave and the RS anchor scale μ* = 182.201 GeV.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.