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.
Neumann Poisson data require a flux compatibility equation
Statement refuted
False claim: Let and let be a bounded domain. Every pair of smooth data, a smooth on and a smooth on , admits a solution of the classical Neumann problem with no compatibility condition relating and .
The claim fails already at the level of a necessary equation: every such solution must satisfy and the smooth constant data , violate it, because the left-hand side is while the right-hand side is . The counterexample below proves both facts. Compatibility is thus necessary, not sufficient: this item asserts no existence result for compatible data.
Facts & Assumptions
Given: Countable Choice, an integer , a bounded domain in the convention of Bounded C1 domains and their outward normals, and the constant data on , on . Write for Lebesgue measure on .
Countable Choice, written , says that every sequence of nonempty sets has a choice function (The Axiom of Countable Choice ()). It is the only choice principle used below, through the divergence theorem and the Lebesgue-measure interfaces.
For , a bounded domain and , , both integrals finite, with the outward normal on every boundary component (Divergence on a bounded C1 Euclidean domain).
The Laplacian is for , and the classical normal derivative is for the outward unit normal (The Laplacian of a function and of a vector field, Classical normal derivative).
A bounded domain is a nonempty bounded open subset of with and locally boundary; for the derivatives through order two extend continuously to , and means and its first derivatives extend continuously (Bounded C1 domains and their outward normals).
A subset of a metric space is open exactly when every has a real with (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement); here is the Euclidean metric ball (Open ball, closed ball and sphere in a metric space).
Every Euclidean ball with is Lebesgue measurable and satisfies , under Countable Choice (Euclidean balls have positive finite Lebesgue measure).
The Borel -algebra is generated by the open sets (The Borel sigma-algebra of a topological space), and under Countable Choice every Borel subset of is Lebesgue measurable; in particular every open set is (Assuming countable choice, every Borel subset of is Lebesgue measurable).
For a measurable set the integral over is (Integral over a measurable subset); the simple integral of is (The integral of a nonnegative simple function), and the nonnegative integral of a nonnegative simple measurable function equals its simple integral (The nonnegative integral agrees with the simple integral on simple functions). Thus for measurable .
If are measurable subsets of a measure space, then (Measures are monotone).
Surface integration on a compact embedded hypersurface is chart integration of the signed integrand through its positive and negative parts, so an integrand that vanishes identically integrates to zero (Surface integration on compact C1 hypersurfaces); the boundary of a bounded domain is such a hypersurface with the outward normal of [F3].
For a map is of class when all iterated partial derivatives of words of length at most exist and are continuous ( maps and multi-index derivative notation in Euclidean space); a constant map has all positive-order iterated partial derivatives equal to and is therefore smooth.
The refuted claim: every pair of smooth Neumann data on a bounded domain admits a solution, with no compatibility condition between the source and the boundary datum .
Counterexample
By [F3] the domain is a nonempty bounded open subset of with ; fix a point . Applying the openness definition [F4] to gives with , a Euclidean metric ball in the sense of [F4].
The source datum is the constant one on , and the boundary datum is the identically zero function on , the restriction of the zero constant function on . By [F10] a constant map has every positive-order iterated partial derivative equal to and is of class for every , hence smooth; both data are therefore smooth, and is constant on the open set .
Suppose satisfies in and on . By [F3] the gradient field lies in , so the divergence theorem [F1] applies to it, with Countable Choice [A1]: , the middle identity by [F1], the first by [F2], and the last because by [F2]. Since pointwise, this says : every classical solution forces the compatibility equation.
For the constant one datum of step 1.2, : by [F7] the integral over the measurable set of the constant one is the simple integral of the indicator , namely . Since is open it is Lebesgue measurable by [F6], and by step 1.1 with both sets measurable, so the monotonicity [F8] gives , while [F5] gives . Hence .
For the zero datum of step 1.2 the boundary integrand is identically zero on the compact hypersurface , so by [F9] its surface integral vanishes: , and therefore .
If a solution existed, step 1.3 would give , whereas step 2.1 gives and step 2.2 gives ; the resulting is a contradiction. Hence the smooth constant data , admit no classical solution on any bounded domain, although by step 1.2 each datum is smooth, and the claim [L1] is refuted. The compatibility equation of step 1.3 is necessary only; its sufficiency for existence is not asserted, and the nonempty domain, positive radius and both boundary orientations are the ones fixed in [F3], [F4] and [F9]. The only choice principle used is of [A1], through the divergence and measure interfaces.
Source notes
Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript), §5.4 equation (5.43), printed p.128, records the Neumann compatibility identity in the present sign convention . Hunter, Notes on Partial Differential Equations (2014), §2.5 Theorem 2.24 and the surrounding Green identities, printed p.32, supplies the divergence-theorem derivation of the same identity. Neither source is used as a proof here: the necessity is derived directly from the local divergence theorem, and the violation by the constant data , is computed from the positivity of the Lebesgue measure of the nonempty open domain. The sibling corollary in this pair (draft at the time of writing) records the same compatibility equation; the derivation here is self-contained and also covers domains that are not connected, which is why no connectedness hypothesis appears. This item asserts no existence theorem for compatible data.
Depends on
- The Borel sigma-algebra of a topological space
- Bounded C1 domains and their outward normals
- $C^k$ maps and multi-index derivative notation in Euclidean space
- Classical normal derivative
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The integral of a nonnegative simple function
- Integral over a measurable subset
- The Laplacian of a $C^2$ function and of a $C^2$ vector field
- Open ball, closed ball and sphere in a metric space
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Surface integration on compact C1 hypersurfaces
- Euclidean balls have positive finite Lebesgue measure
- Measures are monotone
- The nonnegative integral agrees with the simple integral on simple functions
- Assuming countable choice, every Borel subset of $\mathbb{R}^n$ is Lebesgue measurable
- Divergence on a bounded C1 Euclidean domain
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
61 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
- Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript) (standard reference, not scraped)
- John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)