phi_pow54_lt
plain-language theorem explainer
The inequality φ^54 < 192983018016 holds for the golden ratio φ, obtained by factoring the power and chaining prior bounds on φ^51 and φ^3. Numerics researchers in Recognition Science cite it when propagating interval estimates along the phi-ladder for mass predictions. The proof is a short tactic sequence that rewrites the exponent product, invokes the two sibling inequalities, and closes via nlinarith plus norm_num.
Claim. $φ^{54} < 192983018016$ where $φ = (1 + √5)/2$ is the golden ratio.
background
This module supplies rigorous numerical bounds on powers of the golden ratio φ = (1 + √5)/2. The strategy begins with tight bounds on √5, specifically 2.236 < √5 < 2.237, which immediately yield 1.618 < φ < 1.6185, and then refines these via algebraic identities to control higher powers. Upstream results include the identity φ^54 = φ^51 × φ^3 together with the explicit inequalities φ^51 < 45547089449 and φ^3 < 4.237.
proof idea
The proof rewrites φ^54 as the product φ^51 * φ^3 using the equality theorem. It then invokes the sibling bounds φ^51 < 45547089449 and φ^3 < 4.237, establishes positivity of both powers, and applies a calc block that chains the inequality through multiplication by the positive terms, followed by nlinarith to compare against the product of the numeric bounds and norm_num to verify the final comparison.
why it matters
This bound feeds directly into the reciprocal inequality φ^(-54) > 5.181e-12, which supports neutrino mass predictions in the Recognition framework. It also enables the subsequent bounds φ^58 < 1.324e12 and φ^70 < 4.26011e14. Within the framework it tightens the phi-ladder estimates required for the mass formula yardstick * φ^(rung - 8 + gap(Z)), closing one step in the numerical verification of the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.