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.
log|z| has no global harmonic conjugate on C{0}
Statement refuted
Refuted claim: every harmonic function on a domain has a global harmonic conjugate.
The witness is on . It is harmonic there, but it has no global harmonic conjugate.
Facts & Assumptions
Given: The harmonic function on .
The function is harmonic on the punctured plane (log|z| is harmonic on the punctured plane).
There is no continuous logarithm on all of (There is no continuous logarithm on all of ).
The complex exponential is entire, satisfies , and compositions and quotients of holomorphic functions are holomorphic wherever the denominator is nonzero (The complex exponential is entire and its complex derivative is itself, , and the complex exponential extends the real exponential, The chain rule for complex derivatives, Linearity, product, reciprocal, and quotient rules for complex derivatives).
A nonconstant holomorphic function on a complex domain is an open map (Open mapping theorem for holomorphic functions).
Counterexample
Suppose were a harmonic conjugate of on . Then would be holomorphic there, and its exponential would satisfy
The function is holomorphic on by [L3], and by step 1.1. If were nonconstant, [L4] would make its image open in , impossible because . Hence is constant on .
Since is constant, for every one has Thus is a continuous logarithm on , contradicting [L2].
Therefore has no global harmonic conjugate on .
Depends on
- log|z| is harmonic on the punctured plane
- There is no continuous logarithm on all of $\mathbb C\setminus\{0\}$
- The complex exponential is entire and its complex derivative is itself
- $\exp(z+w)=\exp z\,\exp w$, and the complex exponential extends the real exponential
- The chain rule for complex derivatives
- Linearity, product, reciprocal, and quotient rules for complex derivatives
- Open mapping theorem for holomorphic functions
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
37 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
- Jeremy Orloff, MIT 18.04 Topic 5: Introduction to Harmonic Functions (standard reference, not scraped)