LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Logarithmic modulus is harmonic off its centre

Statement

For every $a \in C$ , the real-valued function $u_{a} (z) = \log ∣ z - a ∣$ is smooth and harmonic on $C ∖ {a}$ . No choice principle is required.

Facts & Assumptions

Given: $a \in C$ and the plane harmonicity and modulus conventions (Plane harmonic functions, Real and imaginary parts, complex conjugation, and modulus).

[F1]

The real logarithm has derivative $(\log t)^{'} = 1 / t$ on $(0, \infty)$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

Proof

technique · direct differentiation

1.1F1givenalgebra

Write $z = x + i y$ , $a = p + i q$ , $X = x - p$ , $Y = y - q$ and $R = X^{2} + Y^{2} > 0$ . Then $u_{a} = \frac{1}{2} \log R$ . Repeatedly differentiating [F1] gives $(d / d t)^{m} \log t = (- 1)^{m - 1} (m - 1)! t^{- m}$ for $m \geq 1$ ; composition with the polynomial $R$ therefore makes $u_{a}$ smooth on $R > 0$ . Its first derivatives are $u_{x} = X / R$ and $u_{y} = Y / R$ .

2.1step 1.1givenalgebra∎

A further differentiation gives $u_{x x} = (Y^{2} - X^{2}) / R^{2}$ and $u_{y y} = (X^{2} - Y^{2}) / R^{2}$ . Their sum is zero at every $z \neq a$ . Thus $u_{a}$ is harmonic on $C ∖ {a}$ by the plane harmonicity definition.

Depends on

Used by

Dependency tree · two levels

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