pith. machine review for the scientific record. sign in
theorem proved tactic proof high

exponential_exceeds_bound

show as:
view Lean formalization →

For any real a > 1 and arbitrary real M, some natural N satisfies a^N > M. Growth bounds in the Recognition Science foundation cite this result to guarantee that exponential terms on the phi-ladder surpass any fixed bound. The argument reduces the claim to Bernoulli's inequality via a linear comparison and selects N large enough by the archimedean property of the reals.

claimLet $a, M$ be real numbers with $a > 1$. Then there exists a natural number $N$ such that $a^N > M$.

background

The module GrowthBounds supplies pure real-analysis facts showing exponential growth eventually dominates polynomials. These facts support comparisons between the phi-ladder and cubic volume growth that close the Fermi chain in the Recognition framework. The key upstream lemma is exp_ge_linear, which states Bernoulli's inequality: for a ≥ 1, a^n ≥ 1 + n*(a-1). The present theorem generalizes the base case to strict inequality a > 1 and arbitrary upper bound M.

proof idea

The proof derives 0 < a-1 from the hypothesis a > 1. It then obtains N larger than (M-1)/(a-1) by the existence of naturals exceeding any real. Application of exp_ge_linear yields a^N ≥ 1 + N*(a-1), which exceeds M once the linear term surpasses M-1. Linear arithmetic closes the comparison.

why it matters in Recognition Science

This result supplies the general exponential bound that phi_pow_exceeds instantiates for the golden ratio. It thereby ensures that powers of phi eventually exceed any prescribed mass or energy scale on the Recognition ladder. The module's purpose is to close the Fermi chain by showing exponential growth defeats cubic volume terms.

scope and limits

Lean usage

theorem phi_pow_exceeds (M : ℝ) : ∃ N : ℕ, phi ^ N > M := exponential_exceeds_bound phi one_lt_phi M

formal statement (Lean)

  38theorem exponential_exceeds_bound (a : ℝ) (ha : 1 < a) (M : ℝ) :
  39    ∃ N : ℕ, a ^ N > M := by

proof body

Tactic-mode proof.

  40  have ha_sub : 0 < a - 1 := by linarith
  41  obtain ⟨N, hN⟩ := exists_nat_gt ((M - 1) / (a - 1))
  42  refine ⟨N, ?_⟩
  43  have hge := exp_ge_linear a (le_of_lt ha) N
  44  have hN_bound : (N : ℝ) * (a - 1) > M - 1 := by
  45    have := (div_lt_iff₀ ha_sub).mp hN
  46    linarith
  47  linarith
  48
  49/-- φ eventually exceeds any bound. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.