phi_four_power_lower
plain-language theorem explainer
The inequality states that phi raised to 4M is at least (M/2) to the fourth for any natural number M. It is cited in analytic steps showing phi-exponential growth defeats cubic polynomials within the Recognition framework. The argument applies Bernoulli's inequality to bound phi^M from below by M/2 then raises both sides to the fourth power.
Claim. For any natural number $M$, $phi^{4M} geq (M/2)^4$.
background
The GrowthBounds module supplies pure real analysis results that exponential growth eventually dominates any polynomial. Specific instances compare the phi-ladder against cubic volume growth to close the Fermi chain. Upstream, phi_gt_onePointFive establishes the tighter bound phi > 1.5. exp_ge_linear records Bernoulli's inequality: for a real a at least 1 and natural n, a^n is at least 1 plus n times (a minus 1). PhiLadderLattice.that supplies a hypothesis structure for phi-ladder Poisson summation that downstream results may assume and later discharge.
proof idea
The proof first invokes phi_gt_onePointFive to obtain phi > 1.5. It applies exp_ge_linear to phi and M, yielding phi^M at least 1 plus M times (phi minus 1). Linear arithmetic tightens the bound to phi^M at least M/2. Monotonicity of the fourth power for positive bases then lifts the inequality to the fourth powers.
why it matters
This lemma supports phi_exp_defeats_cubic and phi_exp_defeats_cubic_succ, which establish that for any positive C there exists N such that phi^N exceeds C times N cubed. It supplies the concrete lower bound needed to witness exponential dominance over cubic terms on the phi-ladder. The module positions these bounds as closing the Fermi chain, where the eight-tick octave and D equals 3 rely on such growth comparisons. It touches the open scaffolding around the phi-ladder lattice hypothesis from PhiLadderLattice.that.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.