Encyclopedia Foundation Foundation Growth Bounds

ARTICLE 4 claims 4 theorems

Foundation Growth Bounds

Exponential growth always outruns polynomial growth, and in Recognition Science this simple fact closes a key gap in the framework's chain of derivations.

Verify this page

Growth bounds

Growth bounds are pure real analysis results about how fast sequences grow. The central fact is that exponential growth eventually dominates any polynomial growth. For any base a greater than 1, and any bound M, there is a point N where a^N exceeds M. This is a classical result, proved by the Bernoulli inequality: for a ≥ 1, a^n ≥ 1 + n(a-1). The proof constructs the needed N explicitly, so the statement is not just true but witnessed.

The framework's library of machine-checked formal theorems applies this to the golden ratio φ, the number satisfying φ² = φ + 1, approximately 1.618. Since φ > 1, the general theorem applies, and the library proves that φ^N eventually exceeds any bound. A more specific result shows φ^(4M) ≥ (M/2)^4, a four-power trick that converts the exponential into a quartic lower bound. This is the key step for comparing φ-powers against polynomial volume growth.

In Recognition Science, the framework models physical structure as a discrete ledger of recognition events, a record where each entry has a cost. The framework derives that particle masses sit on a φ-power ladder, and that space has three dimensions. The growth bounds module closes the Fermi chain: it proves that the number of recognition events, growing like φ^N, eventually outnumbers any polynomial bound on volume, which grows like (N+1)³. The theorem phi_exp_defeats_cubic_succ states that for any positive C, there exists N such that φ^N > C·(N+1)³.

The density bound is the payoff. The framework's library proves that the local density, K₀·φ^N divided by V₀·(N+1)³, eventually exceeds any positive threshold. This means that no matter how large the volume grows, the recognition events become dense enough to fill it. The theorem density_exceeds_threshold states this with explicit witnesses for the constants K₀ and V₀. In plain language: exponential recognition growth always wins against cubic spatial volume, so the framework's three-dimensional space cannot dilute the ledger of events.

THEOREM exponential_exceeds_bound · IndisputableMonolith/Foundation/GrowthBounds.lean
exponential_exceeds_bound · IndisputableMonolith/Foundation/GrowthBounds.lean:37 
/-- 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
THEOREM phi_pow_exceeds · IndisputableMonolith/Foundation/GrowthBounds.lean
phi_pow_exceeds · IndisputableMonolith/Foundation/GrowthBounds.lean:49 
/-- φ eventually exceeds any bound. -/
theorem phi_pow_exceeds (M : ℝ) : ∃ N : ℕ, phi ^ N > M :=
  exponential_exceeds_bound phi one_lt_phi M
THEOREM phi_exp_defeats_cubic_succ · IndisputableMonolith/Foundation/GrowthBounds.lean
phi_exp_defeats_cubic_succ · IndisputableMonolith/Foundation/GrowthBounds.lean:97 
/-- **φ-EXPONENTIAL DEFEATS SHIFTED CUBIC** (zero sorry)

    For any C > 0, ∃ N such that φ^N > C · (N+1)³.
    Witness: N = 4*(k+1) where k+1 > 2000*C.
    Needed for the density bound which uses volume V₀*(N+1)³. -/
theorem phi_exp_defeats_cubic_succ (C : ℝ) (hC : 0 < C) :
    ∃ N : ℕ, phi ^ N > C * ((N : ℝ) + 1) ^ 3 := by
  obtain ⟨k, hk⟩ := exists_nat_gt (2000 * C)
  refine ⟨4 * (k + 1), ?_⟩
  have hk1 : (0 : ℝ) < (k : ℝ) + 1 := by exact_mod_cast Nat.succ_pos k
  have hk1_gt : (k : ℝ) + 1 > 2000 * 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
  -- (4*(k+1)+1)^3 ≤ (5*(k+1))^3 since 4*(k+1)+1 ≤ 5*(k+1) iff 1 ≤ k+1, which holds
  have h5k1 : (4 : ℝ) * ((k : ℝ) + 1) + 1 ≤ 5 * ((k : ℝ) + 1) := by nlinarith
  have hM3_pos : (0 : ℝ) < ((k : ℝ) + 1) ^ 3 := pow_pos hk1 3
  -- (k+1)^4/16 > C*(5*(k+1))^3 = 125*C*(k+1)^3 when (k+1) > 2000*C
  have hgoal : (((k : ℝ) + 1) / 2) ^ 4 > C * (5 * ((k : ℝ) + 1)) ^ 3 := by
    nlinarith [mul_pos (show (k : ℝ) + 1 - 2000 * C > 0 by linarith) hM3_pos]
  have hcast : ((↑(4 * (k + 1)) : ℝ) + 1) = 4 * ((k : ℝ) + 1) + 1 := by
    push_cast; ring
  rw [hcast]
  calc phi ^ (4 * (k + 1))
      ≥ (((k : ℝ) + 1) / 2) ^ 4 := hlow
    _ > C * (5 * ((k : ℝ) + 1)) ^ 3 := hgoal
    _ ≥ C * (4 * ((k : ℝ) + 1) + 1) ^ 3 := by
        apply mul_le_mul_of_nonneg_left _ (le_of_lt hC)
        exact pow_le_pow_left₀ (by positivity) h5k1 3
THEOREM density_exceeds_threshold · IndisputableMonolith/Foundation/GrowthBounds.lean
density_exceeds_threshold · IndisputableMonolith/Foundation/GrowthBounds.lean:130 
/-- **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 growth bounds do not prove that recognition events actually fill three-dimensional space; that physical bridge remains open. The theorems do not assign numerical values to K₀ or V₀; they hold for any positive constants. The module does not prove that the golden ratio is the only base for which the density bound holds.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND