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.

Re(1/z) is harmonic on a punctured disc and does not extend harmonically across 0

Statement refuted

Refuted claim: every harmonic function on a punctured disc extends harmonically across the puncture.

The witness is

$u (z) = Re (1 / z) .$

It is harmonic on $0 < ∣ z ∣ < 1$ , but it is unbounded near $0$ and therefore does not extend harmonically there.

Facts & Assumptions

Given: The function $f (z) = 1 / z$ on $0 < ∣ z ∣ < 1$ and its real part $u (z) = Re (f (z))$ .

[L1]

Rational functions are holomorphic wherever their denominator is nonzero (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[L2]

The real part of a holomorphic $C^{2}$ function is harmonic (The $C^{2}$ real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair).

[L3]

A bounded harmonic function near an isolated puncture does extend harmonically (A bounded harmonic function near an isolated puncture extends harmonically).

Counterexample

technique · direct

1.1L1L2

By [L1], the function $1 / z$ is holomorphic on $0 < ∣ z ∣ < 1$ , so [L2] makes $u (z) = Re (1 / z)$ harmonic there.

1.2L3algebra

On the positive real axis, $u (t) = 1 / t \to + \infty$ as $t ↓ 0$ , so $u$ is unbounded near $0$ . If $u$ had a harmonic extension across $0$ , it would be bounded on some small closed disc around $0$ , contradicting [L3].

2.1step 1.1step 1.2∎

Therefore $u$ is harmonic on the punctured disc but does not extend harmonically across the puncture.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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)