phi_pow51_gt
plain-language theorem explainer
The declaration proves 45537548334 < goldenRatio^51. Mass-scale calculations in the Recognition framework cite this to anchor the phi-ladder rung at 51 for structural predictions of the top quark and electron. The proof rewrites the power via the Fibonacci identity and closes the resulting linear inequality with a decimal lower bound on phi together with linarith.
Claim. Let $phi = (1 + sqrt(5))/2$ denote the golden ratio. Then $45537548334 < phi^{51}$.
background
This module supplies rigorous decimal bounds on the golden ratio and its powers using algebraic properties of sqrt(5). The local strategy starts from 2.2360679 < sqrt(5) < 2.2360680, which forces 1.61803395 < phi < 1.6180340. Upstream results include the identity phi^51 = 20365011074 * phi + 12586269025 obtained from the Fibonacci recurrence goldenRatio * fib(51) + fib(50) = phi^51, together with the lower bound 1.61803395 < phi proved by unfolding phi and applying the corresponding sqrt(5) inequality.
proof idea
The proof is a one-line wrapper that first rewrites the target inequality using phi_pow51_eq. It then invokes the lower bound phi_gt_161803395 on phi itself and closes the resulting linear inequality over the reals with linarith.
why it matters
This bound anchors the phi-ladder mass formula at exponent 51 and feeds directly into phi51_gt in ElectroweakMasses, the top_quark_pred_order theorem, and the structural_mass_bounds result establishing 10856 < 2^{-22} * phi^51 < 10858. It supports the Recognition Science claim that particle masses arise geometrically from the phi fixed point (T6) without free parameters. The result also closes numerical scaffolding for the higher-power lemmas phi_pow54_gt and phi_pow59_gt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.