Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck 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.

Weierstrass division theorem

Statement

Let W be a Weierstrass polynomial of degree d in the variable zm. Then for every fOm,0 there exist unique germs qOm,0 and r0,,rd1Om1,0, meaning complex constants when m=1, such that

f=qW+r0+r1zm++rd1zmd1.

Equivalently, every germ has a unique quotient and a unique remainder of zm-degree <d upon division by W.

Facts & Assumptions

Given: A degree-d Weierstrass polynomial W and a germ f.

[L1]

A Weierstrass polynomial has central slice zmd, hence is regular in zm of order d (Weierstrass polynomials in the last variable).

[L2]

The zero-count lemma supplies a radius r and parameter neighbourhood V on which W(z,ζ)0 for ζ=r (Nearby slices of a regular germ have the same zero count).

[L3]

A one-variable contour integral is holomorphic in each complex parameter, and a locally bounded separately holomorphic function is holomorphic (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic, Locally bounded and separately holomorphic implies holomorphic).

[L4]

The polydisc Cauchy formula specializes to the usual one-variable Cauchy formula on a disc (The iterated Cauchy integral formula on a polydisc).

[L5]

A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

Proof

technique · direct
1.1

By [L1] and [L2], after shrinking representatives of W and f if needed there are r>0 and a neighbourhood V of 0 such that W(z,ζ)0 whenever zV and ζ=r. Define q(z,zm):=12πiζ=rf(z,ζ)W(z,ζ)(ζzm)dζ, r(z,zm):=12πiζ=rf(z,ζ)W(z,ζ)W(z,zm)W(z,ζ)(ζzm)dζ. As in the preparation proof, [L3] makes q and r holomorphic on V×{zm<r}.

L1L2L3construct
2.1

For fixed z and ζ, the quotient W(z,ζ)W(z,zm)ζzm is a polynomial in zm of degree at most d1: expand the monic polynomial W in powers of zm and factor each difference ζjzmj=(ζzm)(ζj1++zmj1). Therefore r(z,zm) is itself a polynomial in zm of degree <d with coefficients holomorphic in z.

step 1.1algebra
3.1

Adding the two integral formulas from step 1.1 gives q(z,zm)W(z,zm)+r(z,zm)=12πiζ=rf(z,ζ)ζzmdζ. By [L4], the right-hand side is exactly f(z,zm) for zm<r. Thus f=qW+r with degzmr<d.

step 1.1step 2.1L4
4.1

Suppose also f=qW+r with degzmr<d. Then rr=(qq)W. For each fixed z, the left-hand side is a one-variable polynomial of degree <d divisible by the monic degree-d polynomial W(z,). Hence r(z,)r(z,)=0 as a polynomial, so r=r. Then (qq)W=0, and on the nonempty open set where W0 one has q=q; [L5] forces q=q everywhere. Therefore both quotient and remainder are unique.

step 3.1L5algebra

Depends on

Used by

Dependency tree · two levels

43 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