phi_pow4_lt
plain-language theorem explainer
Golden ratio fourth power satisfies φ^4 < 6.856. Numerics work on phi-ladder bounds cites this when chaining to higher exponents such as φ^58. The term proof reduces via the identity φ^4 = 3φ + 2, invokes the upstream bound φ < 1.6185, and closes with linear arithmetic.
Claim. $φ^4 < 6.856$ where $φ = (1 + √5)/2$ is the golden ratio.
background
This module supplies rigorous bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties. The strategy starts from 2.236 < √5 < 2.237 to obtain 1.618 < φ < 1.6185, then tightens the upper decimal for further power estimates. The upstream result phi_lt_16185 asserts φ < 1.6185 while phi_pow4_eq records the reduction φ^4 = 3φ + 2.
proof idea
The term proof first rewrites the goal with phi_pow4_eq. It then applies the upstream bound phi_lt_16185 and finishes with linarith.
why it matters
The bound is invoked by phi_pow58_lt to control φ^58. It contributes to the numerical infrastructure for the self-similar fixed point φ (T6) and the phi-ladder mass formula in the forcing chain. The module doc-comment notes the strategy of tightening decimal bounds for √5 to support higher-power estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.