phi_pow16_gt
plain-language theorem explainer
The inequality establishes a strict lower bound of 2206.9 on the golden ratio raised to the sixteenth power. Numerics researchers cite it when propagating concrete bounds through the phi-ladder for interval arithmetic and mass formulas. The proof substitutes the algebraic identity phi^16 = 987 phi + 610 and applies linear arithmetic to the known bound 1.618 < phi.
Claim. $2206.9 < ((1 + sqrt(5))/2)^{16}$
background
The module supplies rigorous bounds on the golden ratio phi = (1 + sqrt(5))/2 using algebraic properties and relations to sqrt(5). It starts from the inequalities 2.236^2 < 5 < 2.237^2 to derive 1.618 < phi < 1.6185, then tightens them for higher powers. Upstream results include phi_gt_1618 proving 1.618 < phi and phi_pow16_eq stating phi^16 = 987 phi + 610, the latter obtained from the Fibonacci recurrence satisfied by powers of phi.
proof idea
The proof rewrites the target via phi_pow16_eq to reduce the power to the linear form 987 phi + 610. It then invokes the lower bound from phi_gt_1618 and concludes with linarith.
why it matters
This bound supports phi_pow32_gt and phi_pow70_gt for higher powers as well as phi_pow_16_in_interval for membership checks. It anchors numerical estimates on the phi-ladder in Recognition Science, where phi is the self-similar fixed point (T6) and powers enter mass formulas yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.