Encyclopedia Foundation Foundation Growth Bounds Exp Ge Linear

ARTICLE 5 claims 5 theorems

Foundation Growth Bounds Exp Ge Linear

A simple inequality about powers of numbers larger than one, and the chain of consequences that follows.

Verify this page

A growth bound

The declaration exp_ge_linear is a theorem of real analysis. It states that for any real number a at least 1, and any natural number n, the power an is at least 1 + n·(a−1). This is Bernoulli's inequality, a standard and elementary fact. The theorem is proved in the machine-checked library of formal theorems, with no unproved assumptions beyond the usual axioms of logic.

The point of the theorem is not the inequality itself, which is classical, but what it starts. Because an grows at least linearly in n when a is larger than 1, the library derives that exponential growth eventually defeats any polynomial. A separate theorem, exponential_exceeds_bound, proves that for any a > 1 and any bound M, there is a power aN greater than M. The proof uses exp_ge_linear directly: it picks N large enough that the linear lower bound exceeds M.

Within Recognition Science, the framework applies this to the golden ratio φ, which is about 1.618. The theorem phi_pow_exceeds states that φN eventually exceeds any bound. From there the library proves a stronger result: the φ-exponential defeats the cubic. For any positive constant C, there is an N such that φN > C·N³. A shifted version handles (N+1)³ instead of N³. These cubic comparisons matter because the framework models a ledger, a discrete record of events, whose volume grows like a cube in three spatial dimensions. The exponential growth of the φ-ladder outpaces that volume growth.

The final theorem in the chain, density_exceeds_threshold, combines the pieces. For positive constants K₀ and V₀, the ratio K₀·φN / (V₀·(N+1)³) eventually exceeds any positive threshold. In plain language: the local density of recognition events, measured per unit of cubic volume, grows without bound as N increases. The framework reads this as a density bound that closes the Fermi chain, a step in its derivation of physical structure.

What the declaration does not claim is just as important. It does not say that φ is the only number with this property, nor that the growth bound applies to all possible ledgers. It is a statement about real numbers and natural numbers, proved for the specific sequence of powers. It does not assert anything about physical space, about the fine-structure constant, or about the Riemann Hypothesis. Those are separate questions, with their own theorems and open targets.

THEOREM exp_ge_linear · IndisputableMonolith/Foundation/GrowthBounds.lean
exp_ge_linear · IndisputableMonolith/Foundation/GrowthBounds.lean:20 
/-- Bernoulli's inequality: for a ≥ 1, a^n ≥ 1 + n*(a-1). -/
theorem exp_ge_linear (a : ℝ) (ha : 1 ≤ a) (n : ℕ) :
    a ^ n ≥ 1 + (n : ℝ) * (a - 1) := by
  induction n with
  | zero => simp
  | succ k ih =>
    have ha_nonneg : 0 ≤ a := by linarith
    have hk_nn : (0 : ℝ) ≤ k := Nat.cast_nonneg k
    calc a ^ (k + 1) = a ^ k * a := pow_succ a k
      _ ≥ (1 + (k : ℝ) * (a - 1)) * a := by
          exact mul_le_mul_of_nonneg_right ih ha_nonneg
      _ = a + (k : ℝ) * a * (a - 1) := by ring
      _ ≥ a + (k : ℝ) * 1 * (a - 1) := by
          nlinarith [mul_nonneg hk_nn (sub_nonneg.mpr ha), sq_nonneg (a - 1)]
      _ = 1 + ((k : ℝ) + 1) * (a - 1) := by ring
      _ = 1 + (↑(k + 1) : ℝ) * (a - 1) := by push_cast; ring
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 · IndisputableMonolith/Foundation/GrowthBounds.lean
phi_exp_defeats_cubic · IndisputableMonolith/Foundation/GrowthBounds.lean:74 
/-- **φ-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
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 theorem does not claim that φ is the only base with unbounded powers. It does not assert a physical statement about space or volume on its own. It does not prove the fine-structure constant or the Riemann Hypothesis.

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