phi_four_power_lower
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply for real-valued M without further assumptions.
- Does not generalize to arbitrary bases or exponents.
- Does not address the full exponential-versus-polynomial theorem.
- Does not incorporate RecognitionStructure constants or quantum units.
closing path
Discharged by completing the analytic comparison via Bernoulli's inequality and power monotonicity once phi > 1.5 is fixed.
formal statement (Lean)
57lemma phi_four_power_lower (M : ℕ) :
58 phi ^ (4 * M) ≥ ((M : ℝ) / 2) ^ 4 := by
proof body
Body contains sorry. Scaffold only; not proved.
59 have hphi_half : phi - 1 ≥ 1 / 2 := by linarith [phi_gt_onePointFive]
60 have hM_nn : (0 : ℝ) ≤ M := Nat.cast_nonneg M
61 -- Simplify: phi^(4M) = (phi^M)^4
62 have hpow : phi ^ (4 * M) = (phi ^ M) ^ 4 := by
63 rw [← pow_mul]; ring_nf
64 rw [hpow]
65 -- phi^M ≥ M/2
66 have hbern : phi ^ M ≥ 1 + (M : ℝ) * (phi - 1) :=
67 exp_ge_linear phi (le_of_lt (by linarith [phi_gt_onePointFive])) M
68 have hge_half : phi ^ M ≥ (M : ℝ) / 2 := by nlinarith
69 -- (phi^M)^4 ≥ (M/2)^4
70 exact pow_le_pow_left₀ (by positivity) hge_half 4
71
72/-! ## §3 φ-exponential defeats cubic -/
73
74/-- **φ-EXPONENTIAL DEFEATS CUBIC** (zero sorry)
75
76 For any C > 0, ∃ N such that φ^N > C · N³.
77 Witness: N = 4*(k+1) where k+1 > 1024*C.
78 Proof: φ^(4*(k+1)) ≥ ((k+1)/2)^4 = (k+1)^4/16 > C*(4*(k+1))^3 = 64C*(k+1)^3
79 when (k+1) > 1024C. -/