defectIterate_exponential_lower
plain-language theorem explainer
The exponential lower bound states that the n-fold iterated defect satisfies d_n ≥ 4^n d_0 for any real deviation parameter t and natural number n. Number theorists studying the composition law induced by the Recognition Composition Law on zeta zeros would cite this result to establish rapid growth of defects away from the critical line. The proof is by induction on n, with the inductive step combining algebraic rearrangement and the quadruple amplification lemma defectIterate_four_mul_le.
Claim. For all real $t$ and natural numbers $n$, $4^n d_0(t) ≤ d_n(t)$, where $d_0(t) = J(e^{2η})$ is the base defect for deviation $η$ and $d_n(t)$ is the n-fold iteration of the defect map $d_{k+1} = 2d_k(d_k + 2)$.
background
The module develops the composition law for zeta zero defects induced by the Recognition Composition Law (RCL): J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), where J(x) = (x + x^{-1})/2 - 1. For a zero with deviation η = Re(ρ) - 1/2, the base defect is d_0 = J(e^{2η}) = cosh(2η) - 1. The iteration is defined by d_{n+1} = 2 d_n (d_n + 2), which corresponds to d_n = cosh(2^{n+1} η) - 1. This theorem provides the exponential lower bound on the growth of these defects. It relies on the quadruple amplification property defectIterate_four_mul_le, which states d_{n+1} ≥ 4 d_n.
proof idea
The proof proceeds by induction on n. The base case n=0 is immediate by simplification. For the inductive step, the left side is rewritten as 4 times the n-case expression using ring, bounded above by 4 times defectIterate t n via nlinarith, and then the inductive hypothesis is applied together with defectIterate_four_mul_le t n to reach defectIterate t (n+1).
why it matters
This result is the key step establishing exponential growth of defects under iteration of the composition law. It is used directly in cascade_exponential_growth to restate the bound, in defectIterate_mono to prove monotonicity for t ≠ 0, and in defectIterate_unbounded to show that off-critical zeros (t ≠ 0) produce unbounded defect cascades, which cannot be accommodated by finite carrier budgets. In the Recognition Science framework, this closes the argument that the RCL forces divergent cost for any deviation from the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.