Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)=logz on C{0}. It is harmonic there, but it has no global harmonic conjugate.

Facts & Assumptions

Given: The harmonic function u(z)=logz on C{0}.

[L1]

The function logz 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)=expzexpw, 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.1

Suppose v were a harmonic conjugate of logz on C{0}. Then F(z):=logz+iv(z) would be holomorphic there, and its exponential would satisfy exp(F(z))=z(cosv(z)+isinv(z)).

assume-contra
2.1

The function G(z):=exp(F(z))/z is holomorphic on C{0} by [L3], and G(z)=exp(F(z))/z=eReF(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}.

step 1.1L3L4algebra
3.1

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

step 2.1L2L3
4.1

Therefore logz has no global harmonic conjugate on C{0}.

step 3.1L1discharge-contradiction

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