phi_exp_defeats_cubic
plain-language theorem explainer
Exponential growth of phi powers surpasses any positive multiple of a cubic polynomial. Density calculations in the Recognition Science framework cite this to ensure the phi-ladder dominates volume terms. The proof picks k larger than 1024 C, sets N = 4(k+1), applies the fourth-power lower bound lemma, and finishes with nlinarith and linarith.
Claim. For every real number $C > 0$, there exists a natural number $N$ such that $phi^N > C N^3$.
background
The module supplies pure real-analysis results establishing that exponential growth eventually dominates any polynomial, with specific instances for the phi-ladder versus cubic volume growth that close the Fermi chain. The upstream lemma phi_four_power_lower asserts $phi^{4M} ge (M/2)^4$, derived by reducing to $(phi^M)^4$ and using $phi-1 ge 1/2$. This theorem operates in the foundation layer where phi-ladder sums are compared against polynomial bounds arising from volume counts and density definitions.
proof idea
The proof obtains a natural k such that k > 1024 C via exists_nat_gt, refines the witness to N = 4*(k+1), invokes phi_four_power_lower on k+1 to obtain the lower bound ((k+1)/2)^4, and applies nlinarith with linarith to confirm ((k+1)/2)^4 exceeds C*(4*(k+1))^3 under the size assumption on k+1.
why it matters
This supplies the analytic step needed to bound densities against cubic volume growth, directly supporting the density definition as phi^k. It fills the exponential-defeats-polynomial requirement in the GrowthBounds module, which closes the Fermi chain. No downstream uses are recorded, leaving open its precise integration with the eight-tick octave and D=3 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.