`defectIterate_zero_eq_zeroDefect`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ZeroCompositionLaw
domain: NumberTheory
line: 184 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.ZeroCompositionLaw on GitHub at line 184.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 181
 182/-- For a zeta zero ρ, the iterated defect at level 0 equals the
 183    zero-location defect from ZeroLocationCost. -/
 184theorem defectIterate_zero_eq_zeroDefect (ρ : ℂ) :
 185    defectIterate (zeroDeviation ρ) 0 = zeroDefect ρ := by
 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. -/
 192theorem zero_composition_diverges (ρ : ℂ) (hρ : ¬OnCriticalLine ρ) (C : ℝ) :
 193    ∃ n : ℕ, C < defectIterate (zeroDeviation ρ) n := by
 194  apply defectIterate_unbounded
 195  exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).not.mpr hρ
 196
 197end
 198
 199end NumberTheory
 200end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.