CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Classical Neumann solutions differ by componentwise constants

Statement

Assume ${A C}_{ω}$ when $n \geq 2$ . Assume $Ω \subset R^{n}$ , $n \geq 1$ , is a bounded $C^{1}$ domain with finitely many connected components. If $u, v \in C^{2} (\overline{Ω})$ solve the same Poisson equation and have the same outward normal derivative on $\partial Ω$ , then $u - v$ is constant on each connected component. In particular it is constant when $Ω$ is connected.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ . The set $Ω$ is a bounded $C^{1}$ open set with finitely many connected components, each a bounded $C^{1}$ domain; $u, v \in C^{2} (\overline{Ω})$ have equal Laplacians and equal outward normal derivatives.

[A1]

Countable Choice, written ${A C}_{ω}$ , says that every sequence of nonempty sets has a choice function. (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For $n \geq 2$ , real $a \in C^{2} (\overline{U})$ and $b \in C^{1} (\overline{U})$ on a bounded $C^{1}$ domain, the first Green identity is $\int_{U} (b Δ a + D a \cdot D b) d x = \int_{\partial U} b \partial_{ν} a d S$ . (First Green identity).

[F2]

The classical normal derivative is $\partial_{ν} a = D a \cdot ν$ , with the continuous interior gradient and the outward unit normal. (Classical normal derivative).

[F3]

For a differentiable map on a nonempty connected open Euclidean set, zero derivative is equivalent to constancy. (A differentiable map on a connected open Euclidean set has zero derivative exactly when it is constant).

[F4]

If a real function is continuous on $[a, b]$ and differentiable on $(a, b)$ , then $f (b) - f (a) = f^{'} (c) (b - a)$ for some $c \in (a, b)$ . (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F5]

A subset of $R$ is connected exactly when it is order-convex. (A subset of $R$ is connected if and only if it is order-convex, that is, an interval).

[F6]

Sums and scalar multiples of differentiable maps have the corresponding sum and scalar-multiple derivatives. (Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives).

[F7]

For a $C^{2}$ scalar function, the Laplacian is the trace of the derivative of its gradient. (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

Proof

technique · direct

1.1givenF2F6F7algebra

First take real-valued functions and put $w = u - v$ . By [F6], $D (\nabla w) = D (\nabla u) - D (\nabla v)$ ; taking traces and using [F7] gives $Δ w = 0$ on every component. By [F2] and the same derivative linearity, $\partial_{ν} w = \partial_{ν} u - \partial_{ν} v = 0$ on its boundary. For complex-valued functions, apply this real argument separately to their real and imaginary parts.

2.1step 1.1A1F1F3algebra

Suppose $n \geq 2$ and fix a connected component $U$ . Apply [F1] with $a = b = w$ on $U$ . The volume integrand is $w Δ w + ∣ D w ∣^{2} = ∣ D w ∣^{2}$ and the boundary integrand is $w \partial_{ν} w = 0$ , so $\int_{U} ∣ D w ∣^{2} d x = 0$ . Continuity of $D w$ forces $D w = 0$ throughout $U$ : if it were nonzero at one point, it would be bounded away from zero on a small ball of positive measure. By [F3], $w$ is constant on $U$ . The invocation of [F1] uses precisely the Countable Choice assumption [A1].

2.2step 1.1F3F4F5

Suppose $n = 1$ . By [F5], each connected component $U$ is an interval; boundedness makes it an interval with finite endpoints $a < b$ . The equation in step 1.1 is $w^{''} = 0$ . For any $x < y$ in $U$ , the mean value theorem [F4] applied to $w^{'}$ on $[x, y]$ gives $w^{'} (y) - w^{'} (x) = w^{''} (c) (y - x) = 0$ , so $w^{'}$ is constant on $U$ . Its continuous trace at the right endpoint is zero because the outward normal there is $+ 1$ and $\partial_{ν} w = 0$ . Thus $w^{'} = 0$ on $U$ , and [F3] gives that $w$ is constant there.

3.1step 2.1step 2.2A1F1cases∎

The components are handled independently, so their constants need not agree. If there is only one component, the conclusion is one constant on all of $Ω$ ; zero difference is included. In dimensions at least two, the only use of ${A C}_{ω}$ is through [F1] under [A1]; the interval proof in dimension one uses no choice.

Source notes

Hunter §2.5, Theorem 2.23, equations (2.10)–(2.11), printed p. 32. The energy argument is the Neumann uniqueness corollary of that identity; the one-dimensional case is derived directly to respect the cited theorem's stated $n \geq 2$ hypothesis.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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

John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)