exponential_exceeds_bound
plain-language theorem explainer
For any real a > 1 and arbitrary real M, some natural N satisfies a^N > M. Growth bounds in the Recognition Science foundation cite this result to guarantee that exponential terms on the phi-ladder surpass any fixed bound. The argument reduces the claim to Bernoulli's inequality via a linear comparison and selects N large enough by the archimedean property of the reals.
Claim. Let $a, M$ be real numbers with $a > 1$. Then there exists a natural number $N$ such that $a^N > M$.
background
The module GrowthBounds supplies pure real-analysis facts showing exponential growth eventually dominates polynomials. These facts support comparisons between the phi-ladder and cubic volume growth that close the Fermi chain in the Recognition framework. The key upstream lemma is exp_ge_linear, which states Bernoulli's inequality: for a ≥ 1, a^n ≥ 1 + n*(a-1). The present theorem generalizes the base case to strict inequality a > 1 and arbitrary upper bound M.
proof idea
The proof derives 0 < a-1 from the hypothesis a > 1. It then obtains N larger than (M-1)/(a-1) by the existence of naturals exceeding any real. Application of exp_ge_linear yields a^N ≥ 1 + N*(a-1), which exceeds M once the linear term surpasses M-1. Linear arithmetic closes the comparison.
why it matters
This result supplies the general exponential bound that phi_pow_exceeds instantiates for the golden ratio. It thereby ensures that powers of phi eventually exceed any prescribed mass or energy scale on the Recognition ladder. The module's purpose is to close the Fermi chain by showing exponential growth defeats cubic volume terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.