Foundation Growth Bounds Exponential Exceeds Bound

Exponential growth outruns every bound

In mathematics, a sequence like 2, 4, 8, 16 grows without limit. The theorem exponential_exceeds_bound states this precisely: for any real number a greater than 1, and any real bound M, there exists a natural number N such that a^N > M. In words, the powers of a eventually surpass every fixed threshold. The proof is short and classical. It uses Bernoulli's inequality, which says that for a ≥ 1, a^n ≥ 1 + n(a − 1). Since the right side grows linearly in n, and a line eventually exceeds any constant, the powers must too.

This result is not new. It is a standard fact taught in introductory real analysis courses. Its importance in the Recognition Science framework is that it closes a specific gap in a larger argument. The framework models reality as maintaining a ledger, a discrete record of recognition events. In that model, the number of events grows like powers of the golden ratio φ, while the available space grows like a cube. The theorem guarantees that the exponential growth in the ledger eventually outpaces the cubic growth in volume, no matter what constants multiply the volume term.

The framework's machine-checked library of formal theorems proves this in full detail. The declaration exponential_exceeds_bound is the general statement. From it, the library derives that φ^N exceeds any bound, and then that φ^N defeats any constant times N³. A final density theorem combines these: the ratio of ledger events to volume, K₀·φ^N / (V₀·(N+1)³), eventually exceeds any positive threshold. This is what the framework uses to argue that recognition events cannot be permanently confined by spatial volume.

What the declaration does not claim is just as important. It does not say that exponential growth is fast in any practical sense. For a = 1.001, the crossing point is enormous. It does not say anything about the rate at which the exponential overtakes the polynomial, only that it eventually does. And it does not, by itself, connect to physics. The theorem is pure real analysis. The connection to the ledger, to φ, and to three-dimensional space is a separate modeling step, not part of this proof.

/-- 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

/-- φ eventually exceeds any bound. -/
theorem phi_pow_exceeds (M : ℝ) : ∃ N : ℕ, phi ^ N > M :=
  exponential_exceeds_bound phi one_lt_phi M

/-- **φ-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 state how quickly the exponential overtakes the polynomial, only that it eventually does. The theorem does not by itself connect to physics; the link to the ledger and to three dimensions is a separate modeling step. The result does not apply to bases less than or equal to 1, where powers do not grow without bound.

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: