phi_gt_one
plain-language theorem explainer
The golden ratio φ satisfies 1 < φ. Researchers deriving particle masses on the Recognition Science phi-ladder cite this to keep rung exponents positive in formulas such as m = yardstick · φ^(rung-8+gap(Z)). The proof unfolds the definition of φ, establishes sqrt(5) > 1 by monotonicity of the square root on the interval (1,5), and closes with linear arithmetic.
Claim. $1 < φ$ where $φ = (1 + √5)/2$.
background
The ProtonRadius module derives the proton charge radius from the Recognition Science framework (paper RS_Proton_Radius_Puzzle.tex). The golden ratio φ enters mass ladders via the upstream definition m_e := mass_on_rung 2, which expresses the electron mass as E_coh · φ^2 for rung r_e = 2. The module also records the structural claim that m_p/m_e takes the form φ^k for an integer k determined by the proton rung and confinement gap.
proof idea
Unfold the definition of φ. Prove the auxiliary 1 < √5 by applying Real.sqrt_lt_sqrt to the norm_num facts 1 < 5, then simplify the left side with Real.sqrt_one. Finish with linarith.
why it matters
The inequality anchors the phi-ladder used throughout the proton-radius derivation and the muon-electron ratio φ^11. It supports the T6 forcing step that selects φ as the unique self-similar fixed point and guarantees that rung differences produce masses greater than the yardstick. No direct downstream theorems are recorded, but the result is presupposed by every mass-ratio statement in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.