LemmaStatement: Literature-sourcedProof: 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.

Necessary compatibility for the classical Neumann Poisson problem

Statement

Assume $Ω$ is bounded with $C^{1}$ boundary, $u \in C^{2} (\overline{Ω})$ , $f = - Δ u$ , and outward normal derivative $g = \partial_{ν} u$ . Then $\int_{Ω} f = - \int_{\partial Ω} g$ .

Facts & Assumptions

Given: Assume ${A C}_{ω}$ . Let $Ω$ be a bounded $C^{1}$ domain in the published Euclidean surface convention, let $n \geq 2$ , and let real $u \in C^{2} (\overline{Ω})$ with $f = - Δ u$ and $g = \partial_{ν} u$ . Complex-valued data are handled by real and imaginary parts.

[A1]

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

[F1]

For $n \geq 2$ , a bounded $C^{1}$ domain and $F \in C^{1} (\overline{Ω}; R^{n})$ satisfy $\int_{Ω} div F d x = \int_{\partial Ω} F \cdot ν d S$ . (Divergence on a bounded C1 Euclidean domain).

[F2]

The Laplacian is $Δ u = div \nabla u$ . (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F3]

The classical normal derivative is $\partial_{ν} u = D u \cdot ν$ for the outward unit normal. (Classical normal derivative).

[F4]

In this surface-integration convention a bounded $C^{1}$ domain is nonempty and has dimension $n \geq 2$ . (Bounded C1 domains and their outward normals).

Proof

technique · direct

1.1givenF2F3F4algebra

For real $u$ , the gradient field $F = \nabla u$ belongs to $C^{1} (\overline{Ω}; R^{n})$ by the stated $C^{2}$ closure convention. By [F2], $div F = Δ u$ , and by [F3], $F \cdot ν = g$ at each boundary point.

2.1step 1.1A1F1

Apply the divergence theorem [F1] to the field in step 1.1. It gives $\int_{Ω} Δ u d x = \int_{\partial Ω} g d S$ . This use of [F1] requires exactly the Countable Choice assumption [A1].

3.1step 2.1givenalgebra

Since $f = - Δ u$ , negating the identity in step 2.1 yields $\int_{Ω} f d x = - \int_{\partial Ω} g d S$ . For complex-valued $u, f, g$ , apply this real calculation separately to real and imaginary parts.

4.1step 3.1F3F4cases∎

If $f = 0$ , the identity says the total outward Neumann flux is zero; if also $g = 0$ , both sides vanish. The theorem applies on every boundary component with the outward orientation specified in [F3]. The domain class in [F4] excludes the empty set and dimensions zero or one. No converse or sufficiency for existence is asserted.

Source notes

Hunter §1.12, Theorem 1.46, printed pp. 17–18, gives the divergence formula; Hunter §2.5, Theorem 2.23, printed p. 32, gives the same flux identity as the first Green formula with the constant test function. The negative sign comes only from $f = - Δ u$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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)