Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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 preparation theorem

Statement

Let fOm,0 be regular in zm of order d. Then there are a unit uOm,0 and a Weierstrass polynomial W of degree d such that

f=uW.

Facts & Assumptions

Given: A germ fOm,0 that is regular in zm of order d.

[L1]

Units in Om,0 are exactly the germs with nonzero value at 0 (A germ is a unit exactly when its value at 0 is nonzero, so Om,0 is local).

[L2]

The zero-count lemma supplies a radius r and parameter neighbourhood V for the nearby slices of f (Nearby slices of a regular germ have the same zero count).

[L3]

The power sums of those slice zeros are holomorphic, and Newton's recurrences convert them into holomorphic elementary symmetric functions (The power sums of the slice zeros vary holomorphically, Finite Newton recurrences for the slice zeros).

[L4]

A Weierstrass polynomial is monic in the last variable with lower coefficients vanishing at the origin, and the exact order of a one-variable zero is the exponent in its local factorization (Weierstrass polynomials in the last variable, The order of a zero is the exponent in its local holomorphic factorization).

[L5]

Quotients by nonvanishing holomorphic functions are holomorphic (Sums, products and nonvanishing quotients of holomorphic functions are holomorphic).

[L6]

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).

[L7]

The polydisc Cauchy formula specializes to the usual one-variable Cauchy formula when only the last variable is present (The iterated Cauchy integral formula on a polydisc).

Proof

technique · direct
1.1

Choose a representative of f on a neighbourhood of the closed cylinder V×{ζr} given by [L2]. For each zV, let λ1(z),,λd(z) be the slice zeros in ζ<r, counted with multiplicity. By [L3], the elementary symmetric functions e1(z),,ed(z) of those roots are holomorphic in z. Define W(z,ζ):=ζde1(z)ζd1++(1)ded(z). At z=0 all slice roots equal 0, so ej(0)=0 for every j; therefore W is a degree-d Weierstrass polynomial by [L4].

givenL2L3L4construct
2.1

For each fixed zV, the polynomial W(z,ζ) has exactly the zeros λ1(z),,λd(z) with their multiplicities. Since f(z,ζ) has the same zero multiset by construction, [L4] shows that at every slice zero λ the quotient f(z,ζ)/W(z,ζ) extends holomorphically across λ; away from those zeros it is holomorphic by [L5]. Thus the slice quotient qz(ζ):=f(z,ζ)W(z,ζ) is holomorphic on ζ<r.

step 1.1L4L5
3.1

Define u(z,zm):=12πiζ=rf(z,ζ)W(z,ζ)(ζzm)dζ. Because W(z,ζ)0 on ζ=r, the integrand is continuous on V×{ζ=r}×{zm<r} and holomorphic in each parameter variable. By [L6], the resulting function u is separately holomorphic and locally bounded, hence holomorphic on V×{zm<r}. For fixed z, the one-variable Cauchy formula [L7] applied to the holomorphic slice quotient qz from step 2.1 gives u(z,zm)=qz(zm), so f(z,zm)=u(z,zm)W(z,zm).

step 2.1L6L7
4.1

On the central slice, regularity gives f(0,ζ)=ζdh(ζ) with h(0)0, while step 1.1 gives W(0,ζ)=ζd. Hence step 3.1 yields u(0,0)=h(0)0. By [L1], the germ of u is a unit. Therefore the germs of u and W satisfy f=uW in Om,0, which is the required preparation.

step 1.1step 3.1L1

Depends on

Used by

Dependency tree · two levels

56 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