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.
FALSE: every continuous complex-valued function on a domain has a primitive
Statement
False claim. Every continuous complex-valued function on a complex domain has a primitive.
Facts & Assumptions
Given: The punctured plane and .
A complex domain is a nonempty connected open subset of (A complex domain is a nonempty connected open subset of ).
For dimension at least two, punctured Euclidean space is polygonally connected (For , the punctured space is polygonally connected).
Around a positively oriented circle centred at , (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).
The integral of a continuous complex derivative over every closed rectifiable contour is zero (The integral of a continuous complex derivative over every closed rectifiable contour is zero).
A continuous function on a complex domain has a primitive exactly when its closed-contour integrals vanish (For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent).
For complex polynomials , the set where is open and is holomorphic there (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).
Complex differentiability at a point implies continuity there (Complex differentiability at a point implies continuity there).
Refutation
Apply [L6] to and : it makes open and holomorphic there, hence continuous by [L7]. The point lies in , and [L2] makes connected, so it is a domain by [L1].
Suppose, contrary to the desired refutation, that had a primitive on . Then [L4] would make its integral around the unit circle zero.
But [L3] gives that integral as , a contradiction. Hence the false claim fails, and [L5] gives the corrected zero-closed-contour criterion.
Depends on
- A complex domain is a nonempty connected open subset of $\mathbb C$
- For $n\ge2$, the punctured space $\mathbb{R}^n\setminus\{0\}$ is polygonally connected
- Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero
- Complex differentiability at a point implies continuity there
- On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1
- The integral of a continuous complex derivative over every closed rectifiable contour is zero
- For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 170 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- E. Stein and R. Shakarchi, Complex Analysis, Ch. 1, §3 (standard reference, not scraped)