defectIterate_succ'
plain-language theorem explainer
The theorem supplies the squared expansion of the defect recurrence for iterated zeta zero defects under the Recognition Composition Law. Number theorists studying off-critical line amplification would cite this form when deriving quadratic bounds from the hyperbolic identity. The proof is a one-line wrapper that rewrites via the prior multiplicative recurrence and normalizes the resulting polynomial identity.
Claim. Let $d_n(t) = 2^n t$ denote the scaled deviation and define the iterated defect by $d_n(t) = 2^n t - 1$. Then $d_{n+1}(t) = 2(d_n(t))^2 + 4 d_n(t)$.
background
The Recognition Composition Law (RCL) forces a self-composition on zeta zero defects. For a zero with real-part deviation η, set t = 2η and define the base defect d₀(t) = cosh(t) - 1. The upstream defectIterate definition iterates this via d_n(t) = cosh(2^n t) - 1, which vanishes identically on the critical line (t = 0). The companion theorem defectIterate_succ records the multiplicative recurrence d_{n+1}(t) = 2 d_n(t) (d_n(t) + 2) obtained by applying the double-angle formula for cosh to the pair (e^{2^n t}, e^{-2^n t}).
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side by the multiplicative recurrence defectIterate_succ, then invokes the ring tactic to expand 2 d (d + 2) into the squared form 2 d² + 4 d.
why it matters
This equivalence supplies the algebraic form needed for the amplification results listed in the module: defectIterate_four_mul_le (d_{n+1} ≥ 4 d_n) and defectIterate_exponential_lower (d_n ≥ 4^n d_0). It sits inside the RCL-driven cascade that produces divergent defect for any off-critical zero, directly supporting the claim that the functional equation forces exponential growth away from the critical line. The squared expression is the immediate precursor to the quadratic lower bound used in the eight-tick octave analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.