defectIterate
plain-language theorem explainer
defectIterate supplies the closed-form expression d_n(t) = cosh(2^n t) - 1 for the n-fold iterated defect of a zeta zero under the Recognition Composition Law. Researchers studying the composition law for zeta zeros cite it when deriving exponential lower bounds on defect growth away from the critical line. The definition is introduced directly to match the recurrence obtained by iterating the RCL self-composition starting from d_0 = cosh(t) - 1.
Claim. The iterated defect function is defined by $d_n(t) := 2^n t$ for real $t$ and natural number $n$, where $d_n(t) = 2^n t$ and $d_n(t) = 2^n t$.
background
In the ZeroCompositionLaw module the Recognition Composition Law (RCL) J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) with J(x) = (x + x^{-1})/2 - 1 induces a self-composition on zeta-zero defects. For a nontrivial zero ρ with deviation η = Re(ρ) - 1/2 one sets t = 2η so that the base defect is d_0 = cosh(2η) - 1; each subsequent iterate is obtained by applying the RCL to the pair (ρ, 1-ρ). The module records the resulting cascade d_n = cosh(2^n t) - 1 together with the recurrence d_{n+1} = 2d_n(d_n + 2).
proof idea
Direct definition. The expression is the unique closed form satisfying the base case d_0 = cosh(t) - 1 and the double-angle identity cosh(2u) = 2cosh^2(u) + 1 that reproduces the RCL recurrence.
why it matters
This definition is the common substrate for the CompositionClosureHypothesis and the divergence theorems (cascade_exponential_growth, composition_violates_budget) that convert a single off-critical zero into an unbounded defect sequence. It thereby supplies the concrete growth rate needed to close the argument that any finite carrier budget is violated, forcing the Riemann Hypothesis inside the Recognition framework. The same expression appears in the downstream cascade_doubly_exponential_lower bound that sharpens the growth to exp(2^n |t|)/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.