recognition / NumberTheory / NumberTheory.ZeroCompositionLaw / zero_composition_diverges

theorem

`zero_composition_diverges`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.ZeroCompositionLaw on GitHub at line 192.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

used by

composition_violates_budget IndisputableMonolith.NumberTheory.CompositionDivergence

formal source

 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.