zero_composition_diverges
plain-language theorem explainer
If a zeta zero lies off the critical line, its iterated defect under the Recognition Composition Law grows without bound. Researchers studying the Riemann Hypothesis via cost functionals would cite this as an obstruction to off-line zeros. The proof is a direct application of the general unboundedness result for defect iteration after translating the off-line assumption through the zero-deviation equivalence.
Claim. Let $ρ ∈ ℂ$ satisfy Re(ρ) ≠ 1/2. For any real $C$, there exists $n ∈ ℕ$ such that $C < cosh(2^n · 2(Re(ρ) − 1/2)) − 1$.
background
The NumberTheory.ZeroCompositionLaw module derives a composition law for zeta zeros from the Recognition Composition Law satisfied by J(x) = (x + x^{-1})/2 − 1. The critical line predicate holds precisely when Re(ρ) = 1/2. The zero deviation equals 2(Re(ρ) − 1/2), placing the deviation in the scale where the defect functional applies. The iterated defect is given by cosh(2^n t) − 1. Upstream, the unboundedness theorem shows that for any nonzero t the sequence diverges, while the equivalence theorem equates zero deviation to the critical line condition. The module doc states that the RCL forces each off-critical zero to generate a cascade of exponentially growing defect.
proof idea
The term proof applies the unboundedness theorem to the deviation t = zeroDeviation ρ. It uses the equivalence theorem to convert the hypothesis ¬OnCriticalLine ρ into t ≠ 0, then invokes the unboundedness result.
why it matters
This theorem shows that off-critical zeros generate unbounded cost under iterated RCL application, feeding directly into composition_violates_budget which states the iterated defect exceeds any fixed bound. The downstream comment notes this yields the Riemann Hypothesis from Composition Closure. It realizes the obstruction from the Recognition Composition Law in the context of zeta zeros, consistent with the forcing chain that selects three spatial dimensions and the eight-tick octave. It leaves open whether the Riemann Hypothesis holds, but provides a cost-based reason why violations would be inconsistent with finite budgets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.