defectIterate_zero_eq_zeroDefect
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.