phi_pow_exceeds
plain-language theorem explainer
The golden ratio φ eventually exceeds any prescribed real bound M. Researchers bounding the φ-ladder against polynomial growth in Recognition Science cite this result to ensure exponential dominance. The proof is a one-line application of the general exponential-exceeds-bound theorem once φ > 1 is supplied.
Claim. For the golden ratio $φ > 1$ and any real number $M$, there exists a natural number $N$ such that $φ^N > M$.
background
The GrowthBounds module supplies pure real-analysis facts showing that exponential growth dominates any polynomial. Here φ denotes the golden ratio from Constants, satisfying the fixed-point equation that forces φ > 1. The key upstream result is the theorem exponential_exceeds_bound, which states that for any a > 1 and any real M there exists N with a^N > M. This instance specializes that general fact to the Recognition Science constant φ.
proof idea
The proof is a direct one-line wrapper that invokes exponential_exceeds_bound on base phi, using the hypothesis one_lt_phi that 1 < phi, and the target bound M.
why it matters
This result supplies the exponential growth engine required to defeat polynomial bounds in the Recognition framework. It supports the specific comparisons phi_exp_defeats_cubic and density_exceeds_threshold that close the Fermi chain. Within the T0-T8 forcing chain it underwrites the self-similar fixed point φ by guaranteeing that iterated powers remain unbounded, which is essential for the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.