phi_pow59_gt
plain-language theorem explainer
This theorem proves that the golden ratio raised to the 59th power exceeds 2138898000000. Mass verification code in the Recognition framework cites it to anchor higher-rung placements on the phi-ladder. The proof factors the exponent via ring_nf, invokes the two prior power bounds, and chains a numerical product inequality through nlinarith steps.
Claim. The inequality $2138898000000 < ((1 + √5)/2)^{59}$ holds.
background
The module supplies rigorous numerical bounds on powers of the golden ratio φ = (1 + √5)/2 by leveraging algebraic identities and lower bounds on φ itself. Upstream results include phi_pow51_gt establishing 45537548334 < φ^51 and phi_pow8_gt establishing 46.97 < φ^8, both obtained via linarith on simpler phi bounds like phi_gt_1618. These build on the module's strategy of tightening decimal approximations for √5 to derive φ intervals.
proof idea
The proof rewrites φ^59 = φ^51 * φ^8 via ring_nf. It retrieves phi_pow51_gt and phi_pow8_gt, proves positivity of φ^51, then applies a calc block: norm_num verifies the concrete product 45537548334 * 46.97 exceeds the target, after which nlinarith lifts the inequality first through the φ^51 factor and then through the φ^8 factor.
why it matters
This result supports the phi59_gt lemma in Masses.Verification, which rewrites Constants.phi to goldenRatio and applies the bound for mass verification. It contributes to the phi-ladder mass formula by providing a concrete lower bound at rung 59, aligning with the self-similar fixed point phi and the eight-tick octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.