defectIterate_succ
plain-language theorem explainer
The recurrence d_{n+1} = 2 d_n (d_n + 2) holds for the iterated defect d_n(t) = cosh(2^n t) - 1. Number theorists bounding zeta zero deviations cite it to derive the quadrupling step and exponential growth. The proof unfolds the definition, rewrites the power via pow_succ, invokes the cosh double-angle formula, and closes the equality with linarith after two algebraic auxiliaries.
Claim. For all real $t$ and natural numbers $n$, let $d_k = $cosh$(2^k t) - 1$. Then $d_{n+1} = 2 d_n (d_n + 2)$.
background
The module derives the composition law for zeta zero defects from the Recognition Composition Law (RCL) satisfied by J(x) = ½(x + x^{-1}) - 1. For a nontrivial zero ρ with deviation η = Re(ρ) - 1/2, the base defect is d_0 = J(e^{2η}) = cosh(2η) - 1. The function defectIterate t n is defined by defectIterate t n := cosh(2^n t) - 1, so that t = 2η yields the iterated defects under RCL self-composition.
proof idea
The tactic proof unfolds defectIterate, rewrites 2^{n+1} t = 2 · (2^n t) by pow_succ and ring, invokes Real.cosh_two_mul for the double-angle identity and Real.cosh_sq for the square relation, sets c := cosh(2^n t), then establishes two auxiliary equalities (one by linarith, one by ring) before closing with linarith.
why it matters
This supplies the core recurrence used by defectIterate_four_mul_le (which proves d_{n+1} ≥ 4 d_n) and defectIterate_succ' (the squared form). It realizes the self-composition step listed as main result 1 in the module documentation, enabling the exponential lower bound defectIterate_exponential_lower and the divergence claim for off-critical zeros. In the broader framework it connects J-uniqueness (T5) to the amplification that forces D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.