phi_pow8_lt
plain-language theorem explainer
The bound establishes that the eighth power of the golden ratio satisfies φ^8 < 46.99. Researchers deriving mass ladders or PMNS mixing angles cite it to control growth of higher powers of φ. The proof rewrites φ^8 via its Fibonacci closed form and applies the prior bound φ < 1.6185 inside linear arithmetic.
Claim. Let φ denote the golden ratio. Then φ^8 < 46.99.
background
The Numerics.Interval.PhiBounds module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2. It builds on the Interval structure, a closed interval with rational endpoints lo ≤ hi, and on the theorem phi_lt_16185 which proves φ < 1.6185 by bounding √5 < 2.237. The key algebraic identity phi_pow8_eq states that φ^8 = 21φ + 13, obtained by iterating the relation φ^2 = φ + 1.
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side using phi_pow8_eq to obtain 21φ + 13, then applies the hypothesis phi_lt_16185 that φ < 1.6185, and concludes via linarith.
why it matters
This bound feeds directly into the mass verification lemmas phi11_lt and phi17_lt, which control φ^11 and φ^17 for the phi-ladder. It also supports higher-power bounds such as phi_pow43_lt and the PMNS reactor angle match pmns_theta13_match, where the reciprocal bound on φ^{-8} is needed to match the observed sin²θ₁₃ ≈ 0.022. In the Recognition framework it closes the numerical scaffolding for the eight-tick octave and the phi-based constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.