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.
Uniqueness in Weierstrass preparation
Statement
Suppose is regular in of order and
with units and Weierstrass polynomials of degree . Then and .
Facts & Assumptions
Given: A regular germ of order with two preparations .
Units are exactly the germs with nonzero value at (A germ is a unit exactly when its value at is nonzero, so is local).
A degree- Weierstrass polynomial is monic in and has central slice (Weierstrass polynomials in the last variable).
A holomorphic function on a domain that vanishes on a nonempty open subset vanishes identically (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).
Proof
By [L1], after shrinking to a common neighbourhood the unit factors and are nowhere zero. Therefore for each fixed nearby parameter , the slice zeros of coincide, with multiplicity, with the slice zeros of and also with those of .
Fix such a parameter . By [L2], both and are monic degree- one-variable polynomials with the same multiset of roots, counted with multiplicity. Over , a monic polynomial is the product of its linear factors, so these two polynomials are equal. Since this holds for every nearby , the germs satisfy .
With , the two preparations give . On the nonempty open set where one therefore has . Applying [L3] to the holomorphic function on the connected neighbourhood shows everywhere there, and hence as germs.
Depends on
Used by
Dependency tree · two levels
22 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
- Jiří Lebl, Tasty Bits of Several Complex Variables, Theorem 6.2.3 (standard reference, not scraped)
- Jaap Korevaar and Jan Wiegerinck, Several Complex Variables, Theorem 4.4.1 (standard reference, not scraped)