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 f∈Om,0 there exist unique germs q∈Om,0 and r0,…,rd−1∈Om−1,0, meaning complex constants when m=1, such that

f=qW+r0+r1zm+⋯+rd−1zmd−1.

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.1L1L2L3construct

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 z′∈V 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}.

2.1step 1.1algebra

For fixed z′ and ζ, the quotient W(z′,ζ)−W(z′,zm)ζ−zm is a polynomial in zm of degree at most d−1: expand the monic polynomial W in powers of zm and factor each difference ζj−zmj=(ζ−zm)(ζj−1+⋯+zmj−1). Therefore r(z′,zm) is itself a polynomial in zm of degree <d with coefficients holomorphic in z′.

3.1step 1.1step 2.1L4

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

4.1step 3.1L5algebra∎

Suppose also f=q′W+r′ with deg⁡zmr′<d. Then r−r′=(q′−q)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 (q−q′)W=0, and on the nonempty open set where W≠0 one has q=q′; [L5] forces q=q′ everywhere. Therefore both quotient and remainder are unique.

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