defectIterate_zero_eq_zeroDefect
plain-language theorem explainer
The base case equates the level-zero iterated defect on a zeta zero's deviation to its zero-location defect. Researchers examining the Riemann hypothesis via the Recognition Composition Law would cite this identity to anchor the defect cascade. The proof is a one-line rewrite reducing both sides to the same J-log expression.
Claim. For a nontrivial zero ρ of ζ(s), the level-zero iterated defect applied to the deviation of ρ equals the zero-location defect of ρ, i.e., the value J(e^{2η}) where η = Re(ρ) − 1/2.
background
The module derives a composition law for zeta-zero defects from the Recognition Composition Law satisfied by J(x) = ½(x + x^{-1}) − 1. The defect functional equals J on positive reals and measures deviation from unity; upstream results define the cost of any recognition event as its J-cost and establish defect as the core functional from the law of existence. The local setting is the self-composition induced by ξ(s) = ξ(1−s) on a zero ρ with deviation η, yielding the recurrence d_{n+1} = 2 d_n (d_n + 2).
proof idea
One-line wrapper that rewrites both sides via the lemmas equating defectIterate at zero to the J-log form and zeroDefect to the same J-log form.
why it matters
This identity supplies the base case for the composition law on zeta zeros, which forces off-critical zeros to produce exponentially growing defect via the RCL. It supports the module's main results on the recurrence, the four-fold amplification, and the exponential lower bound. In the framework it connects the forcing chain (T5 J-uniqueness) to the divergence claim for zeros off the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.