defectIterate_unbounded
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that all nontrivial zeros lie on the critical line.
- Does not supply an explicit formula for the smallest n in terms of C and t.
- Does not apply when t = 0, where every iterate vanishes.
- Does not address the density or distribution of off-critical zeros.
- Does not quantify total cost summed over multiple zeros.
Lean usage
theorem test (t : ℝ) (ht : t ≠ 0) (C : ℝ) : ∃ n : ℕ, C < defectIterate t n := defectIterate_unbounded ht Cformal statement (Lean)
164theorem defectIterate_unbounded {t : ℝ} (ht : t ≠ 0) (C : ℝ) :
165 ∃ n : ℕ, C < defectIterate t n := by
proof body
Term-mode proof.
166 have hd0 : 0 < defectIterate t 0 := defectIterate_zero_pos ht
167 have hexp := defectIterate_exponential_lower t
168 suffices h : ∃ n : ℕ, C < (4 : ℝ) ^ n * defectIterate t 0 by
169 obtain ⟨n, hn⟩ := h
170 exact ⟨n, lt_of_lt_of_le hn (hexp n)⟩
171 set k := ⌈C / defectIterate t 0⌉₊ + 1
172 refine ⟨k, ?_⟩
173 have h1 : C / defectIterate t 0 ≤ ↑(⌈C / defectIterate t 0⌉₊) := Nat.le_ceil _
174 have h2 : (↑(⌈C / defectIterate t 0⌉₊) : ℝ) + 1 ≤ (4 : ℝ) ^ k :=
175 nat_succ_le_pow_four _
176 rw [show C = C / defectIterate t 0 * defectIterate t 0 from by
177 field_simp]
178 exact mul_lt_mul_of_pos_right (by linarith) hd0
179
180/-! ## §5. Connection to the zero-location defect -/
181
182/-- For a zeta zero ρ, the iterated defect at level 0 equals the
183 zero-location defect from ZeroLocationCost. -/