CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-10-02

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.

Exterior Dirichlet uniqueness needs a far-field condition

Statement refuted

Let $n \geq 3$ , $R > 0$ , $a \in R^{n}$ , and $Ω = {x : ∣ x - a ∣ > R}$ . The functions $0$ and $u (x) = 1 - (R / ∣ x - a ∣)^{n - 2}$ are distinct bounded harmonic functions on $Ω$ with the same zero trace on $\partial B_{R} (a)$ ; $u$ tends to $1$ at infinity. Thus boundary data alone, and even boundedness alone, do not imply uniqueness in this exterior domain. A uniqueness class must also prescribe behavior at infinity; in particular, $u \to 0$ excludes this witness.

Facts & Assumptions

Given: an integer $n \geq 3$ , a radius $R > 0$ , a centre $a \in R^{n}$ and the exterior domain $Ω = {x \in R^{n} : ∣ x - a ∣ > R}$ .

[F1]

For $t > 0$ and real $β$ , $t^{β}$ is continuous and differentiable with derivative $β t^{β - 1}$ (Continuity and derivatives of positive-base real powers).

[F2]

On open real intervals the chain rule, sum, scalar-multiple and product rules apply to differentiable functions (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F3]

For a real $C^{2}$ function on an open subset of $R^{n}$ , $Δ v = \sum_{i < n} \partial_{i}^{2} v$ ; vanishing Laplacian means harmonicity (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field). Coordinates and derivative indices below both run from $0$ to $n - 1$ .

Counterexample

technique · direct

1.1givenF1algebra

Put $q (x) : = \sum_{i < n} (x_{i} - a_{i})^{2} = ∣ x - a ∣^{2} > 0$ on $Ω$ , $h (x) : = q (x)^{(2 - n) / 2}$ and $u (x) : = 1 - R^{n - 2} h (x) = 1 - (R / ∣ x - a ∣)^{n - 2}$ . These expressions are continuous on ${x : ∣ x - a ∣ \geq R}$ .

2.1step 1.1algebra

For $∣ x - a ∣ > R$ we have $0 < R / ∣ x - a ∣ < 1$ , so $0 < (R / ∣ x - a ∣)^{n - 2} < 1$ and $0 < u (x) < 1$ : the function $u$ is bounded on $Ω$ , while the zero function is bounded as well.

2.2step 1.1F1F2F3algebra

Harmonicity. Write $y_{i} = x_{i} - a_{i}$ . Coordinate differentiation using [F1] and [F2] gives $\partial_{i} h = (2 - n) y_{i} q^{- n / 2}$ and $\partial_{j} \partial_{i} h = (2 - n) δ_{i j} q^{- n / 2} + n (n - 2) y_{i} y_{j} q^{- (n + 2) / 2}$ . All these derivatives are continuous because $q > 0$ , so $h$ and $u$ are $C^{2}$ . Summing the pure second partials yields $Δ h = n (2 - n) q^{- n / 2} + n (n - 2) q q^{- (n + 2) / 2} = 0$ . The constant function has zero second partials, hence $Δ u = - R^{n - 2} Δ h = 0$ ; both $u$ and $0$ are harmonic by [F3]. No surface measure or choice assumption is used.

3.1step 1.1step 2.1algebra

Boundary trace. If $∣ x - a ∣ = R$ then $R / ∣ x - a ∣ = 1$ , so $u (x) = 1 - 1 = 0$ on $\partial Ω = S_{R} (a)$ ; the zero function has the same trace, and $u$ is nonzero on $Ω$ by step 2.1.

3.2step 1.1step 2.1algebra

Far-field behaviour. If $∣ x - a ∣ \to \infty$ then $(R / ∣ x - a ∣)^{n - 2} \to 0$ because $n - 2 > 0$ , so $u (x) \to 1$ , whereas the zero function tends to $0$ ; in particular $u$ does not satisfy the decay condition $u \to 0$ at infinity.

4.1step 2.1step 2.2step 3.1step 3.2F3∎

Steps 2.1, 2.2 and 3.1 exhibit two distinct bounded harmonic functions $0$ and $u$ on the exterior domain $Ω$ that agree, with value zero, on $\partial B_{R} (a)$ ; step 3.2 shows that they are separated by their far-field behaviour. Hence prescribed boundary data, and boundedness by itself, do not give uniqueness, and a far-field condition such as $u \to 0$ is needed to exclude this witness.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Leon Simon, Lectures on PDE (2015 rough draft) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)