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

exp_ge_linear

show as:
view Lean formalization →

Bernoulli's inequality states that for real a at least 1 and natural n, a^n is at least 1 plus n times (a minus 1). Growth bound arguments in the Recognition framework cite it when exponentials must dominate linear or polynomial terms on the phi-ladder. The proof runs by induction on n, multiplying the inductive hypothesis by a and closing the step with ring rewriting plus nlinarith on nonnegativity.

claimFor all real numbers $a$ with $a ≥ 1$ and all natural numbers $n$, $a^n ≥ 1 + n(a - 1)$.

background

The GrowthBounds module supplies pure real analysis results showing exponential growth dominates any polynomial, with instances for the phi-ladder versus cubic volume growth that close the Fermi chain. Bernoulli's inequality supplies the base comparison between exponential and linear terms needed for those dominance statements. The module imports ArithmeticFromLogic for successor structure and Recognition plus Cycle3 for the monolith and 3-cycle recognition structure that embed the inequality into the larger framework.

proof idea

Proof by induction on n. The zero case simplifies directly to equality. In the successor step, the inductive hypothesis is multiplied on the right by a (using nonnegativity of a), the product is rewritten by ring to a + k a (a-1), then nlinarith lowers the middle term using a ≥ 1 and nonnegativity of (a-1), after which ring and cast normalization recover the linear form for k+1.

why it matters in Recognition Science

This theorem is invoked directly by exponential_exceeds_bound (which produces N such that a^N exceeds any M) and by phi_four_power_lower (which bounds phi to the 4M against (M/2)^4). It advances the Recognition framework by enabling the demonstration that phi-exponential growth defeats polynomial growth, consistent with the eight-tick octave and D=3 in the forcing chain. No open scaffolding remains at this step.

scope and limits

Lean usage

have hge := exp_ge_linear a (le_of_lt ha) N

formal statement (Lean)

  21theorem exp_ge_linear (a : ℝ) (ha : 1 ≤ a) (n : ℕ) :
  22    a ^ n ≥ 1 + (n : ℝ) * (a - 1) := by

proof body

Tactic-mode proof.

  23  induction n with
  24  | zero => simp
  25  | succ k ih =>
  26    have ha_nonneg : 0 ≤ a := by linarith
  27    have hk_nn : (0 : ℝ) ≤ k := Nat.cast_nonneg k
  28    calc a ^ (k + 1) = a ^ k * a := pow_succ a k
  29      _ ≥ (1 + (k : ℝ) * (a - 1)) * a := by
  30          exact mul_le_mul_of_nonneg_right ih ha_nonneg
  31      _ = a + (k : ℝ) * a * (a - 1) := by ring
  32      _ ≥ a + (k : ℝ) * 1 * (a - 1) := by
  33          nlinarith [mul_nonneg hk_nn (sub_nonneg.mpr ha), sq_nonneg (a - 1)]
  34      _ = 1 + ((k : ℝ) + 1) * (a - 1) := by ring
  35      _ = 1 + (↑(k + 1) : ℝ) * (a - 1) := by push_cast; ring
  36
  37/-- For a > 1 and any M, there exists N such that a^N > M. -/

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.