Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26
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 u(z)=log⁡∣z∣ on C∖{0}. It is harmonic there, but it has no global harmonic conjugate.

Facts & Assumptions

Given: The harmonic function u(z)=log⁡∣z∣ on C∖{0}.

[L1]

The function log⁡∣z∣ is harmonic on the punctured plane (log|z| is harmonic on the punctured plane).

[L2]

There is no continuous logarithm on all of C∖{0} (There is no continuous logarithm on all of C∖{0}).

[L3]

The complex exponential is entire, satisfies exp⁡(α−β)=exp⁡(α)/exp⁡(β), 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, 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).

[L4]

A nonconstant holomorphic function on a complex domain is an open map (Open mapping theorem for holomorphic functions).

Counterexample

technique · direct
1.1assume-contra

Suppose v were a harmonic conjugate of log⁡∣z∣ on C∖{0}. Then F(z):=log⁡∣z∣+iv(z) would be holomorphic there, and its exponential would satisfy exp⁡(F(z))=∣z∣(cos⁡v(z)+isin⁡v(z)).

2.1step 1.1L3L4algebra

The function G(z):=exp⁡(F(z))/z is holomorphic on C∖{0} by [L3], and ∣G(z)∣=∣exp⁡(F(z))∣/∣z∣=eRe⁡F(z)/∣z∣=1 by step 1.1. If G were nonconstant, [L4] would make its image open in C, impossible because G(C∖{0})⊆{ ∣w∣=1 }. Hence G is constant on C∖{0}.

3.1step 2.1L2L3

Since G is constant, for every z≠0 one has exp⁡(F(z)−F(1))=exp⁡(F(z))exp⁡(F(1))=z G(z)G(1)=z. Thus L(z):=F(z)−F(1) is a continuous logarithm on C∖{0}, contradicting [L2].

4.1step 3.1L1discharge-contradiction∎

Therefore log⁡∣z∣ has no global harmonic conjugate on C∖{0}.

Depends on

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