phi_pow4_gt
plain-language theorem explainer
This theorem proves that the fourth power of the golden ratio exceeds 6.854. Researchers establishing lower bounds on high powers of φ for Recognition Science numerics would cite it when chaining to larger exponents. The proof rewrites φ^4 via the recurrence to 3φ + 2 then applies linear arithmetic to the known lower bound φ > 1.618.
Claim. $6.854 < phi^4$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties of its minimal polynomial. It establishes intervals such as 1.618 < φ < 1.6185 by comparing squares to 5 and extends these to powers via recurrence relations.
proof idea
The proof rewrites goldenRatio ^ 4 to 3 * goldenRatio + 2 using phi_pow4_eq. It then invokes the lower bound from phi_gt_1618 and concludes via linarith.
why it matters
This result feeds phi_pow58_gt, which combines the bound with a lower estimate on φ^54 to reach φ^58 > 1.3219e12. It supports the phi-ladder constructions in Recognition Science where powers of φ enter mass formulas and the eight-tick octave (T7). The bound aligns with the self-similar fixed point property of φ at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.