exp_ge_linear
plain-language theorem explainer
Bernoulli's inequality asserts that for real a at least 1 and natural n, a to the power n is at least 1 plus n times (a minus 1). Analysts proving growth comparisons in the Recognition Science framework cite this to establish exponential dominance over linear terms ahead of phi-ladder bounds. The proof proceeds by induction on n, multiplying the inductive hypothesis by a and applying ring plus nlinarith under nonnegativity.
Claim. For all real numbers $a$ with $a ≥ 1$ and natural numbers $n$, $a^n ≥ 1 + n(a - 1)$.
background
The GrowthBounds module collects pure real analysis facts showing that exponential growth eventually dominates any polynomial. These results are applied specifically to compare phi-ladder growth against cubic volume terms, closing the Fermi chain. The present theorem is the classical Bernoulli inequality, independent of Recognition-specific objects such as the monolith M or the three-cycle structure.
proof idea
Proof by induction on n. The zero case simplifies directly. In the successor case, rewrite the power via pow_succ, multiply the inductive hypothesis by a using mul_le_mul_of_nonneg_right, expand with ring, then apply nlinarith with nonnegativity of k and (a-1) to replace the coefficient k by 1 before a final ring step.
why it matters
This result feeds exponential_exceeds_bound, which shows existence of N with a^N > M for a > 1, and phi_four_power_lower, which bounds phi^(4M) from below. It supports the module goal of exponential dominance over polynomials for the phi-ladder versus cubic growth, aligning with the self-similar fixed point phi in the forcing chain. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.