IndisputableMonolith.Foundation.GrowthBounds

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Growth Bounds: Exponential Defeats Polynomial
   6
   7Pure real analysis results establishing that exponential growth
   8eventually dominates any polynomial. Specific instances for
   9the φ-ladder vs. cubic volume growth close the Fermi chain.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace GrowthBounds
  15
  16open Constants
  17
  18/-! ## §1 Bernoulli and base results -/
  19
  20/-- Bernoulli's inequality: for a ≥ 1, a^n ≥ 1 + n*(a-1). -/
  21theorem exp_ge_linear (a : ℝ) (ha : 1 ≤ a) (n : ℕ) :
  22    a ^ n ≥ 1 + (n : ℝ) * (a - 1) := by
  23  induction n with
  24  | zero => simp
  25  | succ k ih =>
  26    have ha_nonneg : 0 ≤ a := by linarith
  27    have hk_nn : (0 : ℝ) ≤ k := Nat.cast_nonneg k
  28    calc a ^ (k + 1) = a ^ k * a := pow_succ a k
  29      _ ≥ (1 + (k : ℝ) * (a - 1)) * a := by
  30          exact mul_le_mul_of_nonneg_right ih ha_nonneg
  31      _ = a + (k : ℝ) * a * (a - 1) := by ring
  32      _ ≥ a + (k : ℝ) * 1 * (a - 1) := by
  33          nlinarith [mul_nonneg hk_nn (sub_nonneg.mpr ha), sq_nonneg (a - 1)]
  34      _ = 1 + ((k : ℝ) + 1) * (a - 1) := by ring
  35      _ = 1 + (↑(k + 1) : ℝ) * (a - 1) := by push_cast; ring
  36
  37/-- For a > 1 and any M, there exists N such that a^N > M. -/
  38theorem exponential_exceeds_bound (a : ℝ) (ha : 1 < a) (M : ℝ) :
  39    ∃ N : ℕ, a ^ N > M := by
  40  have ha_sub : 0 < a - 1 := by linarith
  41  obtain ⟨N, hN⟩ := exists_nat_gt ((M - 1) / (a - 1))
  42  refine ⟨N, ?_⟩
  43  have hge := exp_ge_linear a (le_of_lt ha) N
  44  have hN_bound : (N : ℝ) * (a - 1) > M - 1 := by
  45    have := (div_lt_iff₀ ha_sub).mp hN
  46    linarith
  47  linarith
  48
  49/-- φ eventually exceeds any bound. -/
  50theorem phi_pow_exceeds (M : ℝ) : ∃ N : ℕ, phi ^ N > M :=
  51  exponential_exceeds_bound phi one_lt_phi M
  52
  53/-! ## §2 The four-power trick -/
  54
  55/-- phi^(4*M) ≥ (M/2)^4.
  56    Proof: phi^(4*M) = (phi^M)^4 ≥ (M*(phi-1))^4 ≥ (M/2)^4. -/
  57lemma phi_four_power_lower (M : ℕ) :
  58    phi ^ (4 * M) ≥ ((M : ℝ) / 2) ^ 4 := by
  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. -/
  80theorem phi_exp_defeats_cubic (C : ℝ) (_hC : 0 < C) :
  81    ∃ N : ℕ, phi ^ N > C * (N : ℝ) ^ 3 := by
  82  obtain ⟨k, hk⟩ := exists_nat_gt (1024 * C)
  83  refine ⟨4 * (k + 1), ?_⟩
  84  have hk1 : (0 : ℝ) < (k : ℝ) + 1 := by exact_mod_cast Nat.succ_pos k
  85  have hk1_gt : (k : ℝ) + 1 > 1024 * C := by
  86    have h := hk; push_cast at h ⊢; linarith
  87  have hlow : phi ^ (4 * (k + 1)) ≥ (((k : ℝ) + 1) / 2) ^ 4 := by
  88    have := phi_four_power_lower (k + 1)
  89    push_cast at this ⊢
  90    linarith
  91  have hM3_pos : (0 : ℝ) < ((k : ℝ) + 1) ^ 3 := pow_pos hk1 3
  92  have hgoal : (((k : ℝ) + 1) / 2) ^ 4 > C * (↑(4 * (k + 1)) : ℝ) ^ 3 := by
  93    push_cast
  94    nlinarith [mul_pos (show (k : ℝ) + 1 - 1024 * C > 0 by linarith) hM3_pos]
  95  linarith
  96
  97/-- **φ-EXPONENTIAL DEFEATS SHIFTED CUBIC** (zero sorry)
  98
  99    For any C > 0, ∃ N such that φ^N > C · (N+1)³.
 100    Witness: N = 4*(k+1) where k+1 > 2000*C.
 101    Needed for the density bound which uses volume V₀*(N+1)³. -/
 102theorem phi_exp_defeats_cubic_succ (C : ℝ) (hC : 0 < C) :
 103    ∃ N : ℕ, phi ^ N > C * ((N : ℝ) + 1) ^ 3 := by
 104  obtain ⟨k, hk⟩ := exists_nat_gt (2000 * C)
 105  refine ⟨4 * (k + 1), ?_⟩
 106  have hk1 : (0 : ℝ) < (k : ℝ) + 1 := by exact_mod_cast Nat.succ_pos k
 107  have hk1_gt : (k : ℝ) + 1 > 2000 * C := by
 108    have h := hk; push_cast at h ⊢; linarith
 109  have hlow : phi ^ (4 * (k + 1)) ≥ (((k : ℝ) + 1) / 2) ^ 4 := by
 110    have := phi_four_power_lower (k + 1)
 111    push_cast at this ⊢; linarith
 112  -- (4*(k+1)+1)^3 ≤ (5*(k+1))^3 since 4*(k+1)+1 ≤ 5*(k+1) iff 1 ≤ k+1, which holds
 113  have h5k1 : (4 : ℝ) * ((k : ℝ) + 1) + 1 ≤ 5 * ((k : ℝ) + 1) := by nlinarith
 114  have hM3_pos : (0 : ℝ) < ((k : ℝ) + 1) ^ 3 := pow_pos hk1 3
 115  -- (k+1)^4/16 > C*(5*(k+1))^3 = 125*C*(k+1)^3 when (k+1) > 2000*C
 116  have hgoal : (((k : ℝ) + 1) / 2) ^ 4 > C * (5 * ((k : ℝ) + 1)) ^ 3 := by
 117    nlinarith [mul_pos (show (k : ℝ) + 1 - 2000 * C > 0 by linarith) hM3_pos]
 118  have hcast : ((↑(4 * (k + 1)) : ℝ) + 1) = 4 * ((k : ℝ) + 1) + 1 := by
 119    push_cast; ring
 120  rw [hcast]
 121  calc phi ^ (4 * (k + 1))
 122      ≥ (((k : ℝ) + 1) / 2) ^ 4 := hlow
 123    _ > C * (5 * ((k : ℝ) + 1)) ^ 3 := hgoal
 124    _ ≥ C * (4 * ((k : ℝ) + 1) + 1) ^ 3 := by
 125        apply mul_le_mul_of_nonneg_left _ (le_of_lt hC)
 126        exact pow_le_pow_left₀ (by positivity) h5k1 3
 127
 128/-! ## §4 Density bound -/
 129
 130/-- **LOCAL DENSITY EVENTUALLY EXCEEDS ANY THRESHOLD**
 131
 132    K₀ * φ^N / (V₀ * (N+1)³) → ∞ as N → ∞. -/
 133theorem density_exceeds_threshold (K₀ : ℝ) (hK₀ : 0 < K₀)
 134    (V₀ : ℝ) (hV₀ : 0 < V₀) (threshold : ℝ) (hT : 0 < threshold) :
 135    ∃ N : ℕ, K₀ * phi ^ N / (V₀ * ((N : ℝ) + 1) ^ 3) > threshold := by
 136  -- Need phi^N > (threshold * V₀ / K₀) * (N+1)^3
 137  have hC : 0 < threshold * V₀ / K₀ := by positivity
 138  obtain ⟨N, hN⟩ := phi_exp_defeats_cubic_succ (threshold * V₀ / K₀) hC
 139  refine ⟨N, ?_⟩
 140  have hdenom_pos : 0 < V₀ * ((N : ℝ) + 1) ^ 3 := by positivity
 141  rw [gt_iff_lt, lt_div_iff₀ hdenom_pos]
 142  -- Goal: threshold * (V₀ * (N+1)^3) < K₀ * phi^N
 143  -- From hN: phi^N > (threshold*V₀/K₀) * (N+1)^3
 144  -- So K₀ * phi^N > K₀ * (threshold*V₀/K₀) * (N+1)^3 = threshold*V₀*(N+1)^3
 145  have hphi_pos : 0 < phi ^ N := pow_pos phi_pos N
 146  have hNN3 : 0 < ((N : ℝ) + 1) ^ 3 := by positivity
 147  have hK0phi : K₀ * phi ^ N > K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 := by
 148    have := mul_lt_mul_of_pos_left hN hK₀
 149    simp only [mul_comm, mul_assoc] at this ⊢
 150    linarith
 151  have hsimp : K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 =
 152               threshold * V₀ * ((N : ℝ) + 1) ^ 3 := by
 153    have hK0ne : K₀ ≠ 0 := ne_of_gt hK₀
 154    field_simp [hK0ne]
 155  rw [hsimp] at hK0phi
 156  linarith
 157
 158end GrowthBounds
 159end Foundation
 160end IndisputableMonolith
 161