Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Small perturbations preserve the total local zero multiplicity

Statement

Let f be holomorphic on a neighbourhood of the closed disc D(a,r), and suppose f has no zero on the circle za=r. Let m be the total multiplicity of the zeros of f in D(a,r). If g is holomorphic on a neighbourhood of D(a,r) and

g(z)f(z)<f(z)(za=r),

then g has exactly m zeros in D(a,r), counted with multiplicity.

In particular, if a is an isolated zero of f of order m and the disc is chosen so that a is the only zero of f in D(a,r), then every such perturbation g has exactly m zeros in D(a,r) counted with multiplicity.

Facts & Assumptions

Given: A holomorphic function f on a neighbourhood of D(a,r), a holomorphic function g on the same neighbourhood, and gf<f on za=r.

[L1]

Rouché's theorem gives equal zero counts inside a closed contour when the strict boundary inequality holds (Rouche's theorem in the classical strict-inequality form).

Proof

technique · direct
1.1

Let γ(t)=a+reit for 0t2π. The hypothesis says gf<f on γ, and f has no zero there.

given
2.1

Applying [L1] to the contour γ shows that f and g have the same weighted zero count inside za<r. Because both are holomorphic, there is no pole term, so that weighted count is exactly the total multiplicity of the interior zeros. Hence g has as many zeros in the disc, counted with multiplicity, as f does.

step 1.1L1
3.1

The isolated-zero specialization is the case where that total multiplicity for f is the single local order m at a.

step 2.1

Depends on

Used by

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources