defectIterate_zero_eq_zeroDefect
For a zeta zero ρ the level-zero iterated defect on its deviation equals the zero-location defect. Researchers applying the Recognition Composition Law to the Riemann zeta function cite this base case to anchor the recurrence d_{n+1} = 2 d_n (d_n + 2). The proof is a one-line rewrite that reduces both sides to the same J-log expression.
claimFor a zeta zero ρ ∈ ℂ, the level-zero iterated defect on the deviation of ρ equals the zero-location defect: d₀(ρ) = zeroDefect(ρ), where d₀ is the base term of the iterated composition defect.
background
The module develops the composition law for zeta zeros induced by the Recognition Composition Law (RCL) on J(x) = ½(x + x⁻¹) − 1. For a nontrivial zero ρ with deviation η = Re(ρ) − 1/2 the base defect is defined as d₀ = J(e^{2η}) = cosh(2η) − 1. The defect functional itself is the J-cost on positive reals, as supplied by the upstream LawOfExistence.defect definition.
proof idea
The proof is a one-line rewrite that applies defectIterate_zero_eq_J_log on the left and zeroDefect_eq_J_log on the right, equating both expressions to the common J-log form.
why it matters in Recognition Science
This equality supplies the base case for the zeta-zero composition law whose recurrence, amplification, and exponential lower bound appear in the sibling results defectIterate_succ, defectIterate_four_mul_le and defectIterate_exponential_lower. It directly instantiates the RCL at the level of zeta defects and anchors the claim that off-critical zeros generate divergent cost under iteration.
scope and limits
- Does not establish divergence of the defect sequence.
- Does not treat the critical-line case η = 0.
- Does not derive the recurrence relation itself.
- Does not connect to the eight-tick octave or spatial dimension forcing.
formal statement (Lean)
184theorem defectIterate_zero_eq_zeroDefect (ρ : ℂ) :
185 defectIterate (zeroDeviation ρ) 0 = zeroDefect ρ := by
proof body
Term-mode proof.
186 rw [defectIterate_zero_eq_J_log, zeroDefect_eq_J_log]
187
188/-- **The composition law for zeta zeros, final form.**
189
190 If ρ is off the critical line, the iterated composition defect
191 diverges, generating arbitrarily large cost values from a single zero. -/