nat_succ_le_pow_four
plain-language theorem explainer
The inequality n + 1 ≤ 4^{n+1} holds for every natural number n. Researchers proving exponential growth of zeta-zero defects under the Recognition Composition Law cite it to close the lower bound on iterated defect. The argument is a direct induction on n whose successor step reduces by power rewriting and linear arithmetic.
Claim. For every natural number $m$, $m + 1 ≤ 4^{m+1}$ holds in the reals.
background
The module derives a composition law on zeta-zero defects from the Recognition Composition Law satisfied by J(x) = ½(x + x^{-1}) − 1. Off-critical zeros with deviation η produce initial defect d₀ = J(e^{2η}) = cosh(2η) − 1; iteration yields dₙ = cosh(2^{n+1}η) − 1. The defect functional equals J on positive reals and is supplied by LawOfExistence.defect. Cost functions induced by multiplicative recognizers appear in upstream MultiplicativeRecognizerL4.cost and ObserverForcing.cost.
proof idea
Induction on m. Base case m = 0 is closed by norm_num. Successor step rewrites the power via pow_succ, pushes the natural-number cast, and applies nlinarith using nonnegativity of 4^{k+1}.
why it matters
The lemma supplies the numerical bound required by defectIterate_unbounded, which asserts that off-critical zeros generate divergent defect cascades under the RCL. It thereby obstructs any finite carrier budget and closes the exponential-lower-bound step dₙ ≥ 4ⁿ d₀. The factor 4 originates in the self-composition d_{n+1} = 2dₙ(dₙ + 2) forced by the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.