Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: 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.

Neumann Poisson data require a flux compatibility equation

Statement refuted

False claim: Let n≥2 and let Ω⊂Rn be a bounded C1 domain. Every pair of smooth data, a smooth f on Ω‾ and a smooth g on ∂Ω, admits a solution u∈C2(Ω‾) of the classical Neumann problem −Δu=fin Ω,∂νu=gon ∂Ω, with no compatibility condition relating f and g.

The claim fails already at the level of a necessary equation: every such solution must satisfy ∫Ωf dx=−∫∂Ωg dS, and the smooth constant data f≡1, g≡0 violate it, because the left-hand side is λ(Ω)>0 while the right-hand side is 0. 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 n≥2, a bounded C1 domain Ω⊂Rn in the convention of Bounded C1 domains and their outward normals, and the constant data f≡1 on Ω, g≡0 on ∂Ω. Write λ for Lebesgue measure on Rn.

[A1]

Countable Choice, written ACω, says that every sequence of nonempty sets has a choice function (The Axiom of Countable Choice (ACω)). It is the only choice principle used below, through the divergence theorem and the Lebesgue-measure interfaces.

[F1]

For n≥2, a bounded C1 domain Ω and F∈C1(Ω‾;Rn), ∫Ωdiv⁡F dx=∫∂ΩF⋅ν dS, both integrals finite, with the outward normal on every boundary component (Divergence on a bounded C1 Euclidean domain).

[F2]

The Laplacian is Δu=div⁡∇u for u∈C2(Ω‾), and the classical normal derivative is ∂νu=Du⋅ν for the outward unit normal (The Laplacian of a C2 function and of a C2 vector field, Classical normal derivative).

[F3]

A bounded C1 domain is a nonempty bounded open subset of Rn with n≥2 and locally C1 boundary; for C2(Ω‾) the derivatives through order two extend continuously to Ω‾, and F∈C1(Ω‾;Rn) means F and its first derivatives extend continuously (Bounded C1 domains and their outward normals).

[F4]

A subset U of a metric space is open exactly when every x∈U has a real r>0 with B(x,r)⊆U (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 B(a,r)={y:∥y−a∥2<r} is the Euclidean metric ball (Open ball, closed ball and sphere in a metric space).

[F5]

Every Euclidean ball B(a,r) with r>0 is Lebesgue measurable and satisfies 0<λ(B(a,r))<∞, under Countable Choice (Euclidean balls have positive finite Lebesgue measure).

[F6]

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 Rn is Lebesgue measurable; in particular every open set is (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable).

[F7]

For a measurable set E the integral over E is ∫Eh dλ=∫hχE dλ (Integral over a measurable subset); the simple integral of χE=1⋅χE is 1⋅λ(E) (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 ∫E1 dλ=λ(E) for measurable E.

[F8]

If A⊆B are measurable subsets of a measure space, then μ(A)≤μ(B) (Measures are monotone).

[F9]

Surface integration on a compact embedded C1 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 C1 domain is such a hypersurface with the outward normal of [F3].

[F10]

For k∈N a map is of class Ck when all iterated partial derivatives of words of length at most k exist and are continuous (Ck maps and multi-index derivative notation in Euclidean space); a constant map has all positive-order iterated partial derivatives equal to 0 and is therefore smooth.

[L1]

The refuted claim: every pair of smooth Neumann data on a bounded C1 domain admits a C2(Ω‾) solution, with no compatibility condition between the source f and the boundary datum g.

Counterexample

technique · direct
1.1givenF3F4

By [F3] the domain Ω is a nonempty bounded open subset of Rn with n≥2; fix a point a∈Ω. Applying the openness definition [F4] to a gives r>0 with B(a,r)⊆Ω, a Euclidean metric ball in the sense of [F4].

1.2givenF3F10

The source datum f is the constant one on Ω, and the boundary datum g is the identically zero function on ∂Ω, the restriction of the zero constant function on Rn. By [F10] a constant map has every positive-order iterated partial derivative equal to 0 and is of class Ck for every k, hence smooth; both data are therefore smooth, and f is constant on the open set Ω.

1.3givenA1F1F2F3

Suppose u∈C2(Ω‾) satisfies −Δu=f in Ω and ∂νu=g on ∂Ω. By [F3] the gradient field ∇u lies in C1(Ω‾;Rn), so the divergence theorem [F1] applies to it, with Countable Choice [A1]: ∫ΩΔu dx=∫Ωdiv⁡∇u dx=∫∂Ω∇u⋅ν dS=∫∂Ωg dS, the middle identity by [F1], the first by [F2], and the last because ∇u⋅ν=∂νu=g by [F2]. Since f=−Δu pointwise, this says ∫Ωf dx=−∫∂Ωg dS: every classical solution forces the compatibility equation.

2.1step 1.1step 1.2F5F6F7F8

For the constant one datum of step 1.2, ∫Ωf dx=∫Ω1 dλ=λ(Ω): by [F7] the integral over the measurable set Ω of the constant one is the simple integral of the indicator χΩ, namely 1⋅λ(Ω). Since Ω is open it is Lebesgue measurable by [F6], and B(a,r)⊆Ω by step 1.1 with both sets measurable, so the monotonicity [F8] gives λ(Ω)≥λ(B(a,r)), while [F5] gives λ(B(a,r))>0. Hence ∫Ωf dx>0.

2.2step 1.2F3F9

For the zero datum of step 1.2 the boundary integrand y↦g(y) is identically zero on the compact C1 hypersurface ∂Ω, so by [F9] its surface integral vanishes: ∫∂Ωg dS=0, and therefore −∫∂Ωg dS=0.

3.1step 1.3step 2.1step 2.2L1algebracases∎

If a solution u∈C2(Ω‾) existed, step 1.3 would give ∫Ωf dx=−∫∂Ωg dS, whereas step 2.1 gives ∫Ωf dx>0 and step 2.2 gives −∫∂Ωg dS=0; the resulting 0<∫Ωf dx=0 is a contradiction. Hence the smooth constant data f≡1, g≡0 admit no classical solution on any bounded C1 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 ACω 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 −Δu=f. 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 f≡1, g≡0 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

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