phi_pow51_lt
plain-language theorem explainer
The inequality φ^51 < 45537549354 holds for the golden ratio φ. Mass-scale calculations in the Recognition framework cite it to locate the Z boson and top quark on the phi-ladder. The proof rewrites the power via the Fibonacci closed form and applies a decimal upper bound on φ through linear arithmetic.
Claim. $φ^{51} < 45537549354$ where $φ = (1 + √5)/2$.
background
This module supplies rigorous decimal bounds on the golden ratio φ = (1 + √5)/2 by tightening rational approximations to √5. The strategy begins with 2.236² < 5 < 2.237², which forces 1.618 < φ < 1.6185, then refines further to φ < 1.6180340 via the theorem phi_lt_16180340. High powers reduce through the identity φ^n = F_n φ + F_{n-1} with Fibonacci numbers F_n.
proof idea
The proof invokes the equality φ^51 = 20365011074 φ + 12586269025 from phi_pow51_eq, substitutes the upper bound φ < 1.6180340 from phi_lt_16180340, and concludes the target inequality by linear arithmetic.
why it matters
This supplies the upper endpoint required by the Z-boson mass lemma in ElectroweakMasses and the structural electron mass theorem 2^{-22} φ^51 in Necessity. It also supports the top-quark order-of-magnitude check and the recursive bounds for φ^54 and φ^59. Within the framework it anchors the phi-ladder rung at 51, consistent with the self-similar fixed point property of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.