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.
After a linear coordinate change, every nonzero germ is regular in the last variable
Statement
Let and let be nonzero. Then there is an invertible complex-linear map and an integer such that the pulled-back germ is regular in the last variable of order .
Facts & Assumptions
Given: A nonzero germ .
On a sufficiently small polydisc around , a holomorphic representative of has an absolutely convergent power-series expansion (A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc).
Such a multivariable power-series expansion has uniquely determined coefficients (The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique).
Regularity in the last variable is the one-variable exact-order condition of Regular holomorphic germs in the last variable.
Proof
Choose a holomorphic representative of on a small polydisc, and expand it by [L1] as Because is nonzero, some coefficient is nonzero. Let be the smallest total degree for which , and put Then is a nonzero homogeneous polynomial of degree .
If for every , then the polynomial function vanishes identically on all of ; applying [L2] to that finite power series would force every coefficient with to be , contradicting step 1.1. Therefore choose with .
Choose an invertible complex-linear map sending the last basis vector to . Along the last axis one then has The bracketed factor is holomorphic and nonzero at because . Hence [L3] makes regular in the last variable of order .
Depends on
Regular holomorphic germs in the last variable
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