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.
The local mapping of complex squaring at zero and at one
Example
For , the point has local degree and is a branch point: every sufficiently small nonzero value has two distinct nearby preimages. The point has local degree , and is biholomorphic on a sufficiently small neighbourhood of .
Facts & Assumptions
Given: The entire function , the algebra of complex polynomial derivatives (Linearity, product, reciprocal, and quotient rules for complex derivatives), and the fact that a nonzero complex number has exactly two square roots (The -th roots of a complex number and the distinct roots of unity for every ).
If is a complex domain, is nonconstant and holomorphic, and , then the local degree is (Local degree of a nonconstant holomorphic map).
If is a complex domain, is nonconstant and holomorphic, , and , then every neighbourhood of contains an open neighbourhood for which some gives exactly preimages in for , while has only the preimage , counted with multiplicity (A local degree-m holomorphic map has m nearby sheets).
If is nonconstant and holomorphic on a complex domain and , then , , local injectivity at , and biholomorphy between neighbourhoods of and are equivalent (Holomorphic inverse function theorem and local-degree criterion).
Verification
At , one has , so [L1] gives . By [L2], every sufficiently small nonzero has exactly two local preimages; explicitly they are the distinct roots and , while has only the preimage with multiplicity .
At , and the factor is nonzero at , so [L1] gives . Hence [L3] makes biholomorphic between neighbourhoods of and .
The injectivity can also be seen explicitly on . If lie in that disc and , then or ; the second alternative would give , which is impossible.
Depends on
- Local degree of a nonconstant holomorphic map
- A local degree-m holomorphic map has m nearby sheets
- Holomorphic inverse function theorem and local-degree criterion
- The $n$-th roots of a complex number and the $n$ distinct roots of unity for every $n\ge1$
- Linearity, product, reciprocal, and quotient rules for complex derivatives
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
23 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
- J. Lebl, Guide to Cultivating Complex Analysis, §5.1 (standard reference, not scraped)
- B. V. Shabat, Introduction to Complex Analysis, §1.2 (standard reference, not scraped)