phi_exp_defeats_cubic_succ
plain-language theorem explainer
Any positive real C admits a natural number N such that phi to the N exceeds C times (N plus one) cubed. Density bound proofs in the Recognition Science growth analysis cite this result to guarantee exponential dominance over cubic terms. The argument selects k large enough that k plus one exceeds 2000 C, sets N to four times that quantity, and chains a fourth-power lower bound on phi with elementary comparisons.
Claim. For every real number $C > 0$, there exists a natural number $N$ such that $phi^N > C · (N + 1)^3$.
background
The GrowthBounds module supplies real-analysis facts that exponential growth overtakes any fixed polynomial. Here phi denotes the golden ratio, fixed as the self-similar point in the Recognition framework. The upstream lemma phi_four_power_lower supplies the concrete inequality phi to the power 4M is at least (M over 2) to the fourth. This instance targets the cubic volume factor V0 times (N+1) cubed that appears in local density estimates.
proof idea
Obtain k with k+1 larger than 2000 C. Set N equal to 4 times (k+1). Invoke phi_four_power_lower on k+1 to bound phi to the N from below by ((k+1)/2) to the fourth. Verify that this quantity exceeds C times (5(k+1)) cubed via nlinarith, then note that 5(k+1) is at least N+1 so the cubic term is smaller.
why it matters
The result is invoked directly by density_exceeds_threshold to produce an N making the local density K0 phi^N over V0 (N+1)^3 surpass any positive threshold. It thereby completes the argument that density grows without bound along the phi-ladder, closing the required growth comparison in the Fermi chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.