Encyclopedia Foundation Foundation Growth Bounds Phi Exp Defeats Cubic Succ
ARTICLE 3 claims 3 theorems
Foundation Growth Bounds Phi Exp Defeats Cubic Succ
A machine-checked theorem shows that exponential growth based on the golden ratio eventually outruns any cubic growth, no matter the starting coefficient.
Growth bounds
In mathematics, exponential growth eventually dominates polynomial growth. For any positive constant C, the function aN with a > 1 will, for sufficiently large N, exceed C·Nk for any fixed power k. This is a classical fact about rates of growth, not a new claim. The specific case here takes the base a to be the golden ratio φ ≈ 1.618, the number satisfying φ² = φ + 1, and the polynomial to be a cubic in N.
The theorem phi_exp_defeats_cubic_succ states that for any positive real C, there exists a natural number N such that φN > C·(N+1)³. The proof is elementary: it uses Bernoulli's inequality to show φM grows at least linearly in M, then applies a four-power trick to convert that linear growth into a quartic lower bound, which eventually beats any cubic. The witness is explicit: take N = 4(k+1) where k+1 > 2000C.
This is a theorem in the framework's machine-checked library of formal theorems, proved with no gaps in reasoning. The shifted cubic (N+1)³ rather than N³ matters for the intended application: a density bound in the framework's model of recognition events. The result guarantees that a quantity of the form K₀·φN divided by V₀·(N+1)³ eventually exceeds any fixed threshold, because the numerator grows exponentially while the denominator only grows polynomially.
In Recognition Science, this growth bound supports the claim that recognition events, counted along a discrete ledger of steps, can outpace the volume of a surrounding cubic region. The framework models physical space as three-dimensional, so a cubic volume term V₀·(N+1)³ appears naturally. The theorem does not say how fast the threshold is crossed, only that it is crossed eventually. It does not identify what K₀ or V₀ are, nor does it prove that any particular physical process realizes this growth.
What the result changes is the shape of a proof obligation: instead of needing a delicate estimate at every scale, the framework can rely on a single, machine-checked fact that exponential growth wins in the limit. The classical lesson is portable: when comparing growth rates, the base of the exponential matters less than the fact that it is exponential at all.
THEOREM phi_exp_defeats_cubic_succ · IndisputableMonolith/Foundation/GrowthBounds.lean
/-- **φ-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 exp_ge_linear · phi_four_power_lower · IndisputableMonolith/Foundation/GrowthBounds.lean
/-- 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
/-- phi^(4*M) ≥ (M/2)^4.
Proof: phi^(4*M) = (phi^M)^4 ≥ (M*(phi-1))^4 ≥ (M/2)^4. -/
lemma phi_four_power_lower (M : ℕ) :
phi ^ (4 * M) ≥ ((M : ℝ) / 2) ^ 4 := by
have hphi_half : phi - 1 ≥ 1 / 2 := by linarith [phi_gt_onePointFive]
have hM_nn : (0 : ℝ) ≤ M := Nat.cast_nonneg M
-- Simplify: phi^(4M) = (phi^M)^4
have hpow : phi ^ (4 * M) = (phi ^ M) ^ 4 := by
rw [← pow_mul]; ring_nf
rw [hpow]
-- phi^M ≥ M/2
have hbern : phi ^ M ≥ 1 + (M : ℝ) * (phi - 1) :=
exp_ge_linear phi (le_of_lt (by linarith [phi_gt_onePointFive])) M
have hge_half : phi ^ M ≥ (M : ℝ) / 2 := by nlinarith
-- (phi^M)^4 ≥ (M/2)^4
exact pow_le_pow_left₀ (by positivity) hge_half 4
THEOREM density_exceeds_threshold · IndisputableMonolith/Foundation/GrowthBounds.lean
/-- **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 specify how large N must be for the inequality to hold, only that such an N exists. The theorem does not prove that any particular physical system exhibits this growth rate. The result does not depend on the specific value of φ beyond being greater than 1.
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:
- What physical process in the framework is modeled by counting recognition events along a discrete ledger?
- How does the framework derive the specific constants K₀ and V₀ that appear in the density bound?
- What role does the three-dimensional volume term play in the framework's derivation of spatial dimensions?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM phi_exp_defeats_cubic_succ · IndisputableMonolith/Foundation/GrowthBounds.lean
/-- **φ-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 3The theorem phi_exp_defeats_cubic_succ states that for any positive real C, there exists a natural number N such that φ<sup>N</sup> > C·(N+1)³. phi_exp_defeats_cubic_succ · IndisputableMonolith/Foundation/GrowthBounds.leanTHEOREM exp_ge_linear · phi_four_power_lower · IndisputableMonolith/Foundation/GrowthBounds.lean
/-- 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/-- phi^(4*M) ≥ (M/2)^4. Proof: phi^(4*M) = (phi^M)^4 ≥ (M*(phi-1))^4 ≥ (M/2)^4. -/ lemma phi_four_power_lower (M : ℕ) : phi ^ (4 * M) ≥ ((M : ℝ) / 2) ^ 4 := by have hphi_half : phi - 1 ≥ 1 / 2 := by linarith [phi_gt_onePointFive] have hM_nn : (0 : ℝ) ≤ M := Nat.cast_nonneg M -- Simplify: phi^(4M) = (phi^M)^4 have hpow : phi ^ (4 * M) = (phi ^ M) ^ 4 := by rw [← pow_mul]; ring_nf rw [hpow] -- phi^M ≥ M/2 have hbern : phi ^ M ≥ 1 + (M : ℝ) * (phi - 1) := exp_ge_linear phi (le_of_lt (by linarith [phi_gt_onePointFive])) M have hge_half : phi ^ M ≥ (M : ℝ) / 2 := by nlinarith -- (phi^M)^4 ≥ (M/2)^4 exact pow_le_pow_left₀ (by positivity) hge_half 4The proof uses Bernoulli's inequality and a four-power trick to convert linear growth into a quartic lower bound. exp_ge_linear · phi_four_power_lower · IndisputableMonolith/Foundation/GrowthBounds.leanTHEOREM density_exceeds_threshold · IndisputableMonolith/Foundation/GrowthBounds.lean
/-- **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 linarithThe result guarantees that a quantity of the form K₀·φ<sup>N</sup> divided by V₀·(N+1)³ eventually exceeds any fixed threshold. density_exceeds_threshold · IndisputableMonolith/Foundation/GrowthBounds.lean