defectIterate_four_mul_le
plain-language theorem explainer
The inequality shows each iteration of the defect at least quadruples the prior value whenever the current defect is nonnegative. Researchers deriving growth rates for zeta zero defects under the Recognition Composition Law would cite it to reach exponential bounds. The proof rewrites the successor step and closes via nonnegativity plus a quadratic estimate.
Claim. For real $t$ and natural $n$, $4 d_n(t) ≤ d_{n+1}(t)$, where $d_k(t)$ denotes the $k$-fold iterate of the defect map $d_{k+1} = 2d_k(d_k + 2)$ with $d_0 = J(t)$.
background
The module develops the composition law for zeta zeros induced by the Recognition Composition Law on $J(x) = (x + x^{-1})/2 - 1$. A nontrivial zero with deviation η yields initial defect $d_0 = J(e^{2η}) = cosh(2η) - 1$; iteration produces $d_n = cosh(2^{n+1}η) - 1$ and the recurrence $d_{n+1} = 2d_n(d_n + 2)$ from RCL self-composition. The defect functional equals $J$ on positive reals (LawOfExistence.defect). Upstream structures from PhiForcingDerived and SpectralEmergence embed the J-cost into the discrete φ-tier framework.
proof idea
The proof is a term-mode wrapper: rewrite the right-hand side with defectIterate_succ, obtain nonnegativity of defectIterate t n from defectIterate_nonneg, then close with nlinarith on the square nonnegativity of defectIterate t n.
why it matters
This supplies the amplification step required by the exponential lower bound theorem defectIterate_exponential_lower, which states $d_n ≥ 4^n d_0$. It is listed as the second main result in the module on the Composition Law for Zeta Zeros and follows directly from RCL, supporting divergence of defect for off-critical zeros. It connects to J-uniqueness (T5) and the eight-tick octave in the foundational forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.