one_le_four_pow
plain-language theorem explainer
The inequality 1 ≤ 4^n holds for every natural number n. It is cited inside the zeta-zero defect iteration to establish monotonicity of the sequence defectIterate t n. The proof is a direct induction on n: the base case simplifies immediately and the successor step rewrites the power then closes via linear arithmetic on the non-negative term 4^k.
Claim. $1 ≤ 4^n$ for all $n ∈ ℕ$.
background
The NumberTheory.ZeroCompositionLaw module derives the composition law for zeta zeros from the Recognition Composition Law satisfied by J(x) = ½(x + x⁻¹) − 1. For a zero with real deviation η the defect begins at d₀ = J(e^{2η}) and iterates via d_{n+1} = 2 d_n (d_n + 2), which is equivalent to d_n = cosh(2^{n+1} η) − 1. The auxiliary inequality supplies the factor 4^n that converts the recurrence into the exponential lower bound d_n ≥ 4^n d₀.
proof idea
Proof by induction on n. The zero case reduces to 1 ≤ 1 by simp. In the successor case pow_succ rewrites the goal to 4 · 4^k ≥ 1; nlinarith then uses the supplied fact that 4^k ≥ 0 to finish.
why it matters
The result is invoked inside defectIterate_mono to obtain defectIterate t 0 ≤ defectIterate t n. That monotonicity statement, together with defectIterate_exponential_lower, completes the module’s main claim that off-critical zeros produce unbounded defect. It therefore supplies the concrete amplification step d_{n+1} ≥ 4 d_n that follows from the RCL and is required for the divergent-defect conclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.