phi_pow70_lt
plain-language theorem explainer
Golden ratio to the power 70 satisfies φ^70 < 426011000000000 in the reals. Mass verification routines and phi-ladder numerics in Recognition Science cite this bound to anchor rung calculations. The tactic proof factors the exponent as 54 plus 16, substitutes the two prior power bounds, and closes the product inequality with linear arithmetic followed by normalization.
Claim. Let φ = (1 + √5)/2. Then φ^70 < 426011000000000.
background
This module supplies rigorous upper bounds on powers of the golden ratio φ using its algebraic properties and relations to Fibonacci numbers. The strategy starts from interval bounds 2.236 < √5 < 2.237, which yield 1.618 < φ < 1.6185, then extends to higher powers by multiplication and inductive identities.
proof idea
The proof rewrites the exponent via ring_nf as 70 = 54 + 16. It invokes phi_pow54_lt to bound the first factor by 192983018016 and phi_pow16_lt to bound the second by 2207.5. Positivity is established by positivity, after which nlinarith chains the product bound and norm_num confirms the final comparison to 426011000000000.
why it matters
This bound is invoked by phi70_lt in Masses.Verification (via phi_eq_goldenRatio) and by phi_pow76_lt to continue the power chain. It supplies a concrete numerical anchor for the phi-ladder mass formula, consistent with the self-similar fixed-point property of φ in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.