defectIterate_mono
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove strict increase for every n.
- Does not hold when t = 0.
- Does not supply a sharper growth rate than the 4^n factor.
- Does not address zeros outside the critical strip.
Lean usage
theorem example {t : ℝ} (ht : t ≠ 0) (n : ℕ) : defectIterate t 0 ≤ defectIterate t n := defectIterate_mono ht nformal statement (Lean)
140theorem defectIterate_mono {t : ℝ} (ht : t ≠ 0) (n : ℕ) :
141 defectIterate t 0 ≤ defectIterate t n := by
proof body
Term-mode proof.
142 have h := defectIterate_exponential_lower t n
143 have hd0 : 0 < defectIterate t 0 := defectIterate_zero_pos ht
144 nlinarith [one_le_four_pow n]
145
146/-! ## §4. Divergence -/
147
148/-- Helper: n+1 ≤ 4^(n+1) for all n. -/