Pipeline-generated

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.

✓ 5 results · all verified · 4 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Harmonic Functions and Mean Values in Rn — Examples

1 · Prerequisites

2 · Summary

Examples distinguish global mean-value structure from isolated identities and classical smoothness from distributional harmonicity.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Affine functions and mixed quadratic monomials are harmonic

Example

Let $n \geq 1$ , $a \in R$ , and $b \in R^{n}$ . Every affine function $x \mapsto a + b \cdot x$ is harmonic on $R^{n}$ . If $n \geq 2$ and $i, j \in {0, \dots, n - 1}$ are distinct, then $x \mapsto x_{i} x_{j}$ is harmonic on $R^{n}$ .

Verification

Given: the displayed dimension, coefficients, coordinate indices, and the classical Laplacian The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field.

1.1

All second partial derivatives of $a + b \cdot x$ vanish [given].

2.1

For $i \neq j$ , each diagonal second derivative of $x_{i} x_{j}$ vanishes [given]. ∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-07Open item page →

Real and imaginary parts of holomorphic monomials

Example

For $z = x + i y$ , the components $Re z^{2} = x^{2} - y^{2}$ and $Im z^{2} = 2 x y$ , and likewise those of every $z^{m}$ , are harmonic on $R^{2}$ .

Verification

Given: $m \geq 0$ .

1.1

Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero makes $z^{m}$ entire [given].

2.1

The $C^{2}$ real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair makes its two components harmonic [step 1.1]. ∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Radial harmonic functions away from the origin

Example

Let $n \geq 1$ and $U \in C^{2} ((0, \infty))$ . The radial function $u : R^{n} ∖ {0} \to R$ given by $u (x) = U (∣ x ∣)$ is harmonic precisely when $U^{''} (r) + \frac{n - 1}{r} U^{'} (r) = 0 (r > 0) .$ Thus the families are $U (r) = a + b r$ for $n = 1$ , $U (r) = a + b \log r$ for $n = 2$ , and $U (r) = a + b r^{2 - n}$ for $n \geq 3$ .

Verification

Given: $n \geq 1$ , $U \in C^{2} ((0, \infty))$ , and $r = ∣ x ∣ > 0$ .

1.1

Direct differentiation gives $Δ U (r) = U^{''} (r) + (n - 1) U^{'} (r) / r$ [given].

2.1

Multiplying by $r^{n - 1}$ gives $(r^{n - 1} U^{'})^{'} = 0$ , whose integrations give the listed cases [given, algebra]. ∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Harmonic on a punctured domain need not extend

Statement refuted

A function harmonic on a punctured domain need not extend harmonically across the puncture.

Counterexample

Given: $n \geq 2$ .

1.1

On $R^{2} ∖ {0}$ take $\log ∣ x ∣$ ; for $n \geq 3$ take $∣ x ∣^{2 - n}$ , both harmonic by Radial harmonic functions away from the origin [given].

2.1

Each is unbounded as $x \to 0$ , so it has no continuous, hence no harmonic, extension [given]. ∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

One centred ball-mean identity does not force harmonicity

Statement refuted

One ball-mean identity at one centre forces harmonicity.

Counterexample

Given: $n \geq 1$ , $R > 0$ , and $u : R^{n} \to R$ defined by $u (x) = ∣ x ∣^{2} (∣ x ∣^{2} - \frac{n + 2}{n + 4} R^{2}) .$

1.1

Polar coordinates Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma give $\frac{1}{∣ B_{R} ∣} \int_{B_{R}} ∣ x ∣^{2} = \frac{n}{n + 2} R^{2}$ and $\frac{1}{∣ B_{R} ∣} \int_{B_{R}} ∣ x ∣^{4} = \frac{n}{n + 4} R^{4}$ , hence $\frac{1}{∣ B_{R} ∣} \int_{B_{R}} u = 0 = u (0)$ [given, algebra].

2.1

Yet $Δ u = 4 (n + 2) ∣ x ∣^{2} - 2 n \frac{n + 2}{n + 4} R^{2}$ , which is not identically zero [given, algebra]. ∎

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-09-26 (gpt-6-sol)Open item page →

Distributional harmonicity removes an apparent interior corner

Example

Let $n \geq 1$ and define $v : R^{n} \to R$ by $v (x) = ∣ x_{1} ∣$ . This apparent corner is not distributionally harmonic on $R^{n}$ ; indeed $Δ v = 2 δ_{{x_{1} = 0}}$ , where $δ_{{x_{1} = 0}} (ϕ) = \int_{R^{n - 1}} ϕ (0, x^{'}) d x^{'}$ (the evaluation $ϕ (0)$ when $n = 1$ ). In particular, $∣ x_{1} ∣$ is not distributionally harmonic on any open set meeting the hyperplane ${x_{1} = 0}$ .

Verification

Given: $n \geq 1$ , the domain $R^{n}$ , and the distributional derivative convention Distributional harmonicity and Poisson's equation on an open subset of Rn.

1.1givenalgebra

In one variable, split the compactly supported test integral at $0$ and integrate by parts twice. The ordinary second derivative vanishes on both half-lines, and the jump of the first derivative from $- 1$ to $1$ contributes $2 ϕ (0)$ , so $(∣ t ∣)^{''} = 2 δ_{0}$ . Applying this calculation at each fixed $x^{'}$ and integrating over the remaining variables gives $Δ v (ϕ) = 2 \int_{R^{n - 1}} ϕ (0, x^{'}) d x^{'}$ ; derivatives in the other coordinates vanish.

2.1step 1.1∎

On any open set meeting the hyperplane, choose a nonnegative smooth test function supported near a meeting point and positive there. Its hyperplane integral is positive, so step 1.1 makes $Δ v$ nonzero on that open set. Thus the corner fails the distributional harmonicity test there.

Sources

PDE source treatment