defectIterate_unbounded
plain-language theorem explainer
Off-critical zeta zeros force the iterated defect sequence to diverge under the Recognition Composition Law. Number theorists applying Recognition Science to the Riemann hypothesis cite this to show that any deviation from the critical line produces unbounded cost. The argument combines positivity of the base defect with an exponential lower bound of 4^n and a ceiling construction to exceed any fixed C.
Claim. For every real number $t$ with $t ≠ 0$ and every real number $C$, there exists a natural number $n$ such that $C < cosh(2^n t) - 1$.
background
The defectIterate function, defined as defectIterate t n := cosh(2^n t) - 1, captures the n-fold iteration of the defect under the Recognition Composition Law for a zeta zero with deviation parameter t. The module derives this from the RCL J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), which produces the recurrence d_{n+1} = 2d_n(d_n + 2) and the explicit form d_n = cosh(2^n t) - 1. Upstream, defect from LawOfExistence equals J, while defectIterate_zero_pos states that defectIterate t 0 > 0 for t ≠ 0 and defectIterate_exponential_lower gives the bound 4^n · defectIterate t 0 ≤ defectIterate t n.
proof idea
The term proof first applies defectIterate_zero_pos ht to obtain a positive base defect d0. It invokes defectIterate_exponential_lower to reduce the goal to finding n with C < 4^n d0. The construction sets k := ceil(C / d0) + 1, applies nat_succ_le_pow_four to bound the ceiling term by 4^k, then uses field_simp and mul_lt_mul_of_pos_right to conclude C < 4^k d0 ≤ defectIterate t k.
why it matters
This theorem supplies the divergence step that zero_composition_diverges applies directly to conclude that any off-critical zero ρ generates arbitrarily large defectIterate (zeroDeviation ρ) n. It realizes the obstruction stated in the module: the RCL forces exponential growth d_n ≥ 4^n d_0 with d_0 > 0, which cannot fit any finite carrier budget. In the forcing chain this corresponds to J-uniqueness (T5) and the eight-tick octave (T7) that generate the self-similar amplification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.