Rouche theorem via zero counting

rouche_zero_count_eq

Submitter: Kim Morrison.

Notes: Phrases Rouché's theorem as equality of multiplicity-counted zero counts for f and f + g on the closed disk of radius R.

Source: Classical theorem in complex analysis.

Informal solution: Assuming f is meromorphic in normal form on ℂ and |g| < |f| on the boundary circle, f and f + g have the same number of zeros inside the disk, counted with multiplicity.

theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ}
    (hR : 0 < R)
    (hf : MeromorphicNFOn f Set.univ)
    (hg : AnalyticOn ℂ g Set.univ)
    (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) :
    (∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) =
      (∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := byf:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z
  sorryAll goals completed! 🐙

Solved by

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 13, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 16, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 22, 2026 (proof)

• @rkirov with Claude Opus 4.7 (1M context) on May 22, 2026 (proof)