phi_pow8_gt
plain-language theorem explainer
phi_pow8_gt establishes that 46.97 is a strict lower bound for the eighth power of the golden ratio. Mass ladder verifications and PMNS mixing derivations cite this result to control numerical intervals on the phi-ladder. The proof reduces the claim to the linear form 21 phi + 13 via the Fibonacci identity and applies linarith to the base inequality 1.618 < phi.
Claim. $46.97 < phi^8$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The Numerics.Interval.PhiBounds module develops rigorous bounds on the golden ratio using its algebraic properties and approximations to sqrt(5). The strategy starts from 2.236 < sqrt(5) < 2.237 to obtain 1.618 < phi < 1.6185 and extends these to higher powers via the recurrence relations of the golden ratio.
proof idea
The proof rewrites the target using phi_pow8_eq to replace phi^8 with the linear expression 21 phi + 13. It then invokes the lower bound phi_gt_1618 and concludes via linarith.
why it matters
This bound anchors the lower end of the phi-ladder used in mass formulas and feeds directly into phi11_gt and phi17_gt for verifying particle masses. It also supports the PMNS theta13 match by providing the necessary bound on phi^8 for the predicted mixing angle. Within the framework it reinforces the self-similar properties of phi at the T6 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.