Foundation Growth Bounds Phi Exp Defeats Cubic

Exponential growth

Exponential growth eventually defeats polynomial growth. No matter how large the constant multiplying a cubic term, an exponential function with a base greater than one will always surpass it. This is a standard result in real analysis: for any base a > 1 and any constant C, there is some point N where a^N exceeds C times N cubed. The proof typically uses Bernoulli's inequality, which states that for a ≥ 1, a^n ≥ 1 + n(a-1).

The golden ratio φ, approximately 1.618, is one such base. Its powers grow without bound. The formal statement, proved in the machine-checked library of formal theorems, is that for any positive constant C, there exists a natural number N such that φ^N > C·N³. The proof constructs a specific witness: choose N = 4(k+1) where k+1 is large enough, then φ^(4(k+1)) ≥ ((k+1)/2)^4 = (k+1)^4/16, which exceeds C·(4(k+1))³ = 64C(k+1)³ when k+1 > 1024C. The theorem is tagged as proved with zero unresolved axioms.

A related theorem handles a shifted version, showing φ^N > C·(N+1)³ for any positive C. This variant is needed for a density bound. The framework models a ledger, a discrete record of events, whose size grows like K₀·φ^N while the enclosing volume grows like V₀·(N+1)³. The density, the ratio of these two quantities, therefore tends to infinity as N grows. The formal statement says that for any positive constants K₀, V₀, and any positive threshold, there exists an N such that K₀·φ^N / (V₀·(N+1)³) exceeds the threshold.

The theorem does not claim that φ is the only base with this property; any base greater than one works. It does not claim that the cubic is the only polynomial defeated; the argument generalizes to any fixed degree. It also does not claim that the density bound applies to any specific physical system; it is a pure mathematical result about the growth rates of two sequences. The framework uses this result as a component in its broader account, but the theorem itself is a statement about real numbers and natural numbers, not about physics.

/-- For a > 1 and any M, there exists N such that a^N > M. -/
theorem exponential_exceeds_bound (a : ℝ) (ha : 1 < a) (M : ℝ) :
    ∃ N : ℕ, a ^ N > M := by
  have ha_sub : 0 < a - 1 := by linarith
  obtain ⟨N, hN⟩ := exists_nat_gt ((M - 1) / (a - 1))
  refine ⟨N, ?_⟩
  have hge := exp_ge_linear a (le_of_lt ha) N
  have hN_bound : (N : ℝ) * (a - 1) > M - 1 := by
    have := (div_lt_iff₀ ha_sub).mp hN
    linarith
  linarith

/-- **φ-EXPONENTIAL DEFEATS CUBIC** (zero sorry)

    For any C > 0, ∃ N such that φ^N > C · N³.
    Witness: N = 4*(k+1) where k+1 > 1024*C.
    Proof: φ^(4*(k+1)) ≥ ((k+1)/2)^4 = (k+1)^4/16 > C*(4*(k+1))^3 = 64C*(k+1)^3
           when (k+1) > 1024C. -/
theorem phi_exp_defeats_cubic (C : ℝ) (_hC : 0 < C) :
    ∃ N : ℕ, phi ^ N > C * (N : ℝ) ^ 3 := by
  obtain ⟨k, hk⟩ := exists_nat_gt (1024 * C)
  refine ⟨4 * (k + 1), ?_⟩
  have hk1 : (0 : ℝ) < (k : ℝ) + 1 := by exact_mod_cast Nat.succ_pos k
  have hk1_gt : (k : ℝ) + 1 > 1024 * C := by
    have h := hk; push_cast at h ⊢; linarith
  have hlow : phi ^ (4 * (k + 1)) ≥ (((k : ℝ) + 1) / 2) ^ 4 := by
    have := phi_four_power_lower (k + 1)
    push_cast at this ⊢
    linarith
  have hM3_pos : (0 : ℝ) < ((k : ℝ) + 1) ^ 3 := pow_pos hk1 3
  have hgoal : (((k : ℝ) + 1) / 2) ^ 4 > C * (↑(4 * (k + 1)) : ℝ) ^ 3 := by
    push_cast
    nlinarith [mul_pos (show (k : ℝ) + 1 - 1024 * C > 0 by linarith) hM3_pos]
  linarith

/-- **LOCAL DENSITY EVENTUALLY EXCEEDS ANY THRESHOLD**

    K₀ * φ^N / (V₀ * (N+1)³) → ∞ as N → ∞. -/
theorem density_exceeds_threshold (K₀ : ℝ) (hK₀ : 0 < K₀)
    (V₀ : ℝ) (hV₀ : 0 < V₀) (threshold : ℝ) (hT : 0 < threshold) :
    ∃ N : ℕ, K₀ * phi ^ N / (V₀ * ((N : ℝ) + 1) ^ 3) > threshold := by
  -- Need phi^N > (threshold * V₀ / K₀) * (N+1)^3
  have hC : 0 < threshold * V₀ / K₀ := by positivity
  obtain ⟨N, hN⟩ := phi_exp_defeats_cubic_succ (threshold * V₀ / K₀) hC
  refine ⟨N, ?_⟩
  have hdenom_pos : 0 < V₀ * ((N : ℝ) + 1) ^ 3 := by positivity
  rw [gt_iff_lt, lt_div_iff₀ hdenom_pos]
  -- Goal: threshold * (V₀ * (N+1)^3) < K₀ * phi^N
  -- From hN: phi^N > (threshold*V₀/K₀) * (N+1)^3
  -- So K₀ * phi^N > K₀ * (threshold*V₀/K₀) * (N+1)^3 = threshold*V₀*(N+1)^3
  have hphi_pos : 0 < phi ^ N := pow_pos phi_pos N
  have hNN3 : 0 < ((N : ℝ) + 1) ^ 3 := by positivity
  have hK0phi : K₀ * phi ^ N > K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 := by
    have := mul_lt_mul_of_pos_left hN hK₀
    simp only [mul_comm, mul_assoc] at this ⊢
    linarith
  have hsimp : K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 =
               threshold * V₀ * ((N : ℝ) + 1) ^ 3 := by
    have hK0ne : K₀ ≠ 0 := ne_of_gt hK₀
    field_simp [hK0ne]
  rw [hsimp] at hK0phi
  linarith

What this page does not claim

The theorem does not claim φ is the only base that defeats a cubic. The theorem does not claim the density bound applies to any specific physical system. The theorem does not derive the value of the golden ratio; it assumes it as a constant.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/GrowthBounds.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: