LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pendingjudge pass (gpt-6-luna)

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.

Local relations among Weierstrass polynomials reduce to bounded degree

Statement

Let $n, q, d \geq 1$ be integers, let $U^{'} \subseteq C^{n - 1}$ and $D \subseteq C$ be polydiscs centered at $0$ , and let $w$ denote the last coordinate. For $1 \leq j \leq q$ , write $P_{j} (x^{'}, w) = w^{e_{j}} + \sum_{k = 0}^{e_{j} - 1} a_{j k} (x^{'}) w^{k},$ where $1 \leq e_{j} \leq d$ , $a_{j k} \in O (U^{'})$ , and $a_{j k} (0) = 0$ . For every $x = (x^{'}, w_{0}) \in U^{'} \times D$ , each germ in the relation sheaf of $(P_{1}, \dots, P_{q})$ at $x$ is an $O_{U^{'} \times D, x}$ -linear combination of relation germs whose components are polynomials in $w - w_{0}$ of degree at most $d$ with coefficients in $O_{U^{'}, x^{'}}$ .

Statement references

Demailly, Chapter II §3.3, Lemma 3.20

Wehler, §4.2, Theorem 4.28 proof, parts iii.2–iii.3 (bounded-degree reduction)

Facts & Assumptions

Given: The product polydisc, the monic Weierstrass polynomials $P_{j}$ , and a point $x = (x^{'}, w_{0})$ .

[F1]

Coherent module sheaves on complex manifolds: a relation germ of $(P_{1}, \dots, P_{q})$ is a tuple $g = (g_{1}, \dots, g_{q})$ of holomorphic germs satisfying $\sum_{j = 1}^{q} g_{j} P_{j} = 0$ .

[F2]

Weierstrass polynomials in the last variable: each $P_{j}$ has the stated monic polynomial form, with positive finite degree and lower coefficients vanishing at the common center $0$ .

[F3]

Weierstrass preparation theorem: a germ regular in $w$ of order $r$ is a unit times a monic Weierstrass polynomial of degree $r$ .

[F4]

Weierstrass division theorem: division by a monic Weierstrass polynomial has a unique holomorphic quotient and a unique polynomial remainder of smaller degree.

[F5]

A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc and The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique: a holomorphic germ has a convergent power series with uniquely determined coefficients; the product of two nonzero germs is nonzero because the product of their first nonzero homogeneous terms is a nonzero polynomial.

[F6]

Regular holomorphic germs in the last variable: regularity in $w - w_{0}$ of order $r$ means the restriction to the $w$ -line has a zero of exact finite order $r$ .

Proof

1.1F1F2F5givenalgebra

If $q = 1$ , a relation germ $g$ satisfies $g P_{1} = 0$ by [F1]. The polynomial $P_{1}$ is nonzero by [F2], and [F5] makes the ring of holomorphic germs an integral domain, so $g = 0$ , which is already a polynomial relation of bounded degree.

1.2F1F2givenconstructalgebra

Suppose $q \geq 2$ . If $P_{q} (x) \neq 0$ , then $P_{q}$ is a unit germ. For every relation $g = (g_{1}, \dots, g_{q})$ , [F1] gives $g_{q} = - \sum_{j < q} g_{j} P_{j} / P_{q}$ , hence $g = \sum_{j < q} (g_{j} / P_{q}) (P_{q} e_{j} - P_{j} e_{q})$ . Each vector $P_{q} e_{j} - P_{j} e_{q}$ is a relation whose component degrees are at most $d$ .

1.3F2F3F4F6givenconstruct

Suppose $P_{q} (x) = 0$ , and set $e = \deg_{w} P_{q} \leq d$ . Let $r \geq 1$ be its order of vanishing in $w - w_{0}$ ; this is finite and at most $e \leq d$ by [F2, F6]. By [F3], after shrinking near $x$ write $P_{q} = u p$ , where $u$ is a holomorphic unit and $p$ is a monic Weierstrass polynomial of degree $r$ in $w - w_{0}$ . Ordinary polynomial division of $P_{q}$ by the monic polynomial $p$ gives a polynomial quotient and a remainder of degree below $r$ . The division pair $(u, 0)$ also represents $P_{q}$ as a holomorphic germ divided by $p$ ; uniqueness in [F4] makes the polynomial remainder zero and identifies the polynomial quotient with $u$ . Since $P_{q}$ and $p$ are monic of degrees $e$ and $r$ , respectively, this polynomial $u$ has degree $e - r \leq d - r$ and remains a unit near $x$ .

2.1F1F2F4step 1.3algebra∎

Let $g = (g_{1}, \dots, g_{q})$ be a relation germ at $x$ . For $j < q$ , divide by $p$ using [F4] to write $g_{j} = t_{j} p + r_{j}$ , where $t_{j}$ is holomorphic and $r_{j}$ is a polynomial in $w - w_{0}$ of degree below $r$ . Set $α_{j} = t_{j} / u$ and $v_{j} = P_{q} e_{j} - P_{j} e_{q}$ . Then $δ = g - \sum_{j < q} α_{j} v_{j}$ is a relation whose first $q - 1$ components are $r_{j}$ . Its last component satisfies $p (u δ_{q}) = - \sum_{j < q} r_{j} P_{j}$ , whose right-hand side is a polynomial of degree at most $d + r - 1$ . Dividing this polynomial by $p$ and using uniqueness [F4] shows that $u δ_{q}$ is a polynomial of degree at most $d - 1$ . Each $u r_{j}$ also has degree at most $d - 1$ , since $\deg u = e - r \leq d - r$ and $\deg r_{j} < r$ . Thus $u δ$ is a polynomial relation with all component degrees at most $d$ , and $g = \sum_{j < q} α_{j} v_{j} + u^{- 1} (u δ)$ is generated by polynomial relation germs of the required bound.

Proof sources

Coherent module sheaves on complex manifolds

Regular holomorphic germs in the last variable

Weierstrass polynomials in the last variable

Weierstrass preparation theorem

Weierstrass division theorem

A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc

The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique

Remarks

The unit $u$ is retained throughout the relation reduction. Dividing by $p$ produces $g_{j} = t_{j} p + r_{j}$ , while the elementary relation uses $P_{q} = u p$ ; therefore its coefficient is $t_{j} / u$ . This explicit normalization is needed for the remaining components to be polynomial.