zero_composition_diverges
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.
claimLet $ρ ∈ ℂ$ 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 in Recognition Science
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.
scope and limits
- Does not prove the Riemann Hypothesis itself.
- Does not apply to zeros on the critical line.
- Does not quantify divergence rate beyond the 4^n lower bound.
- Does not address zero multiplicity or clustering.
Lean usage
zero_composition_diverges ρ hρ Bformal statement (Lean)
192theorem zero_composition_diverges (ρ : ℂ) (hρ : ¬OnCriticalLine ρ) (C : ℝ) :
193 ∃ n : ℕ, C < defectIterate (zeroDeviation ρ) n := by
proof body
Term-mode proof.
194 apply defectIterate_unbounded
195 exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).not.mpr hρ
196
197end
198
199end NumberTheory
200end IndisputableMonolith