phi_gt_1618
plain-language theorem explainer
The inequality 1.618 < φ holds for the golden ratio φ in the reals. Mass spectrum calculations and resonance models cite this bound to anchor lower estimates on powers of φ. The proof unfolds the goldenRatio definition and reduces the claim to the known lower bound on √5 via linear arithmetic.
Claim. $1.618 < phi$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The module establishes rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties of square roots. The strategy compares 2.236² < 5 to obtain 2.236 < √5, which immediately yields the target lower bound on φ. The upstream theorem sqrt5_gt_2236 supplies the key fact 2.236 < √5.
proof idea
The term proof unfolds goldenRatio to expose the expression (1 + sqrt 5)/2. It invokes the lemma sqrt5_gt_2236 to obtain 2.236 < sqrt 5. Linear arithmetic then concludes the inequality.
why it matters
This bound feeds into downstream results such as alphaG_pred_lower for the fine-structure constant prediction and phi_pow_7_gt_29 for neutrino mass estimates. It anchors the phi-ladder mass formula by supplying a concrete lower estimate consistent with the self-similar fixed point property of φ. The result closes a numerical step supporting the T6 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.