defectIterate_mono
plain-language theorem explainer
Monotonicity of the iterated defect sequence d_n(t) for t ≠ 0. Researchers on the Recognition Composition Law and zeta-zero defects cite it to confirm nondecreasing cost under RCL iteration. The proof is a short algebraic reduction that invokes the exponential lower bound, base positivity, and the inequality 1 ≤ 4^n.
Claim. Let $d_n(t) := 2^n t$ denote the n-fold iterated defect. For real $t ≠ 0$ and natural $n$, $d_0(t) ≤ d_n(t)$ where $d_k(t) = cosh(2^k t) - 1$.
background
The module derives a composition law for zeta-zero defects from the Recognition Composition Law satisfied by J(x) = (x + x^{-1})/2 - 1. For a nontrivial zero with real deviation η, set t = 2η so that d_0 = cosh(2η) - 1; each RCL self-composition then produces d_{n+1} = 2 d_n (d_n + 2), which solves explicitly as d_n(t) = cosh(2^n t) - 1. The upstream definition defectIterate supplies this closed form directly as Real.cosh ((2 : ℝ) ^ n * t) - 1, while defectIterate_exponential_lower and defectIterate_zero_pos supply the supporting bounds used here.
proof idea
Apply defectIterate_exponential_lower t n to obtain the 4^n lower bound on d_n, invoke defectIterate_zero_pos ht to secure d_0 > 0, add the fact one_le_four_pow n that 1 ≤ 4^n, and close with nlinarith.
why it matters
The result is invoked verbatim by composition_cascade_stronger_than_single_defect to establish that a single off-critical zero generates an infinite strictly increasing cascade of distinct cost values. It completes the monotonicity step required for the divergence claims listed in the module's main results (defectIterate_unbounded). In the Recognition framework it quantifies the amplification forced by T5 J-uniqueness and the RCL, supplying the growth mechanism that later feeds into the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.