defectIterate_succ
The recurrence d_{n+1} = 2 d_n (d_n + 2) holds for the iterated defect d_n(t) = cosh(2^n t) - 1. Number theorists bounding zeta zero deviations cite it to derive the quadrupling step and exponential growth. The proof unfolds the definition, rewrites the power via pow_succ, invokes the cosh double-angle formula, and closes the equality with linarith after two algebraic auxiliaries.
claimFor all real $t$ and natural numbers $n$, let $d_k = $cosh$(2^k t) - 1$. Then $d_{n+1} = 2 d_n (d_n + 2)$.
background
The module derives the composition law for zeta zero defects from the Recognition Composition Law (RCL) satisfied by J(x) = ½(x + x^{-1}) - 1. For a nontrivial zero ρ with deviation η = Re(ρ) - 1/2, the base defect is d_0 = J(e^{2η}) = cosh(2η) - 1. The function defectIterate t n is defined by defectIterate t n := cosh(2^n t) - 1, so that t = 2η yields the iterated defects under RCL self-composition.
proof idea
The tactic proof unfolds defectIterate, rewrites 2^{n+1} t = 2 · (2^n t) by pow_succ and ring, invokes Real.cosh_two_mul for the double-angle identity and Real.cosh_sq for the square relation, sets c := cosh(2^n t), then establishes two auxiliary equalities (one by linarith, one by ring) before closing with linarith.
why it matters in Recognition Science
This supplies the core recurrence used by defectIterate_four_mul_le (which proves d_{n+1} ≥ 4 d_n) and defectIterate_succ' (the squared form). It realizes the self-composition step listed as main result 1 in the module documentation, enabling the exponential lower bound defectIterate_exponential_lower and the divergence claim for off-critical zeros. In the broader framework it connects J-uniqueness (T5) to the amplification that forces D = 3.
scope and limits
- Does not prove the Recognition Composition Law.
- Does not extend the identity to complex t.
- Does not supply matching upper bounds on growth.
- Does not locate the zeta zeros themselves.
- Does not derive the base defect d_0 from the zeta equation.
Lean usage
rw [defectIterate_succ]; nlinarith [sq_nonneg (defectIterate t n)]formal statement (Lean)
89theorem defectIterate_succ (t : ℝ) (n : ℕ) :
90 defectIterate t (n + 1) = 2 * defectIterate t n * (defectIterate t n + 2) := by
proof body
Tactic-mode proof.
91 simp only [defectIterate]
92 rw [show (2 : ℝ) ^ (n + 1) * t = 2 * ((2 : ℝ) ^ n * t) from by rw [pow_succ]; ring]
93 have hd := Real.cosh_two_mul ((2 : ℝ) ^ n * t)
94 have hs := Real.cosh_sq ((2 : ℝ) ^ n * t)
95 set c := Real.cosh ((2 : ℝ) ^ n * t)
96 set s := Real.sinh ((2 : ℝ) ^ n * t)
97 have lhs : Real.cosh (2 * ((2 : ℝ) ^ n * t)) - 1 = 2 * c ^ 2 - 2 := by linarith
98 have rhs_eq : 2 * (c - 1) * (c - 1 + 2) = 2 * c ^ 2 - 2 := by ring
99 linarith
100
101/-- The recurrence in "squared ratio" form:
102 dₙ₊₁ = 2(dₙ² + 2dₙ) = 2dₙ² + 4dₙ. -/