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.
A nonzero holomorphic function on whose zero set is an unbounded hyperplane
Statement refuted
That a nonzero holomorphic function on a domain in has isolated zeros.
Counterexample
Take given by .
Facts & Assumptions
Given: The function on .
Holomorphic functions on open subsets of are those of Holomorphic functions on an open subset of , and they are continuous and separately holomorphic (A holomorphic function of several variables is continuous and separately holomorphic).
A holomorphic function vanishing on a nonempty open subset of a connected open set in vanishes identically (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).
Refutation
The function is holomorphic on and is not identically zero, since .
Its zero set is exactly .
This zero set is unbounded, because belongs to it for every complex , and no point of it is isolated in it: if is a zero and , then is a different zero within Euclidean distance .
The zero set has empty interior, so this witness does not contradict [L2]; it shows instead that in several variables a nonzero holomorphic function can vanish on a whole positive-dimensional complex hyperplane. Therefore the refuted claim fails.
Depends on
- Holomorphic functions on an open subset of $\mathbb{C}^m$
- A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically
- A holomorphic function of several variables is continuous and separately holomorphic
- Complex $m$-space and its real coordinate dictionary
- Balls, polydiscs and the distinguished boundary in $\mathbb{C}^m$
Used by
Dependency tree · two levels
36 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, Tasty Bits of Several Complex Variables, v4.4, Ex. 1.2.21 (standard reference, not scraped)