phi_pow32_gt
plain-language theorem explainer
The inequality 4870400 < φ^32 holds for the golden ratio φ. Numerics checks in Recognition Science mass ladders cite it when confirming proton-scale predictions on the phi-ladder. The proof squares the known lower bound on φ^16 and bridges the numerical thresholds with a short calc chain.
Claim. $4870400 < φ^{32}$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous bounds on the golden ratio φ by refining approximations to √5, starting from 2.236 < √5 < 2.237 to obtain 1.618 < φ < 1.6185 and tighter variants. The upstream result phi_pow16_gt asserts 2206.9 < φ^16 by reducing via phi_pow16_eq to the base bound φ > 1.618 and applying linear arithmetic. These power bounds support verification steps in the phi-ladder mass formula.
proof idea
The tactic proof rewrites φ^32 as (φ^16)^2 via ring_nf. It invokes the lower bound phi_pow16_gt, confirms positivity of the power, and runs a calc block that first compares the target constant to (2206.9)^2 by norm_num, then lifts the inequality through the factors by two nlinarith steps.
why it matters
This bound is invoked directly in the proof of phi_pow43_gt to extend the lower-bound chain to the 43rd power. It forms part of the numerical scaffolding for mass verification on the phi-ladder, aligning with the self-similar fixed point φ and the eight-tick octave in the Recognition framework. It closes a specific gap for proton-mass checks at rung 32.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.