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.
A function with vanishing Laplacian has zero boundary flux of its gradient on the unit box
Example
Let on the closed unit box . Then , so Green's first identity with gives zero boundary flux for . Directly, the six face contributions are , so they do sum to .
Facts & Assumptions
Given: The function , the constant function , and the closed unit box with the six-patch presentation of The closed unit box, with its six faces, is an elementary solid region.
For a finite gluing of elementary solid regions, with of class and of class on an open neighbourhood of the union, Green's first identity reads (Green's first identity on a glued elementary solid region).
The Laplacian is (The Laplacian of a function and of a vector field).
The closed unit box has the six outward faces of The closed unit box, with its six faces, is an elementary solid region. [ex-the-closed-unit-box-is-an-elementary-solid-region]
The divergence theorem is (The divergence theorem on an elementary solid region).
The gradient is the vector of partial derivatives (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).
The divergence is the sum of the coordinate partial derivatives (Divergence and curl of a vector field).
For a bounded Jordan set and an integrable function whose sections are integrable outside a content-zero exceptional set, Jordan Fubini computes the multiple integral by iterated section integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).
If , is differentiable on , and is integrable there, then (The second fundamental theorem: if is differentiable on with and is integrable, then ).
Sums and products differentiate termwise in the usual way (Sums, scalar multiples, products and quotients: , , , and when ).
Verification
One has , hence by [F1], [F2], [F3], and [L6].
Since and , [L1] gives on the unit box of [L2], viewed as the one-piece gluing of that elementary solid region; this is the same conclusion [L3] would give for the field .
On the face the outward unit normal is , so and the flux contribution is by [L4] and [L5]; on the face it is .
On the face the outward unit normal is , so and the contribution is ; on the face it is .
The third component of is , so the two faces and contribute nothing.
The six face values add to , agreeing with step 2.1. This is a check of Green's identity on one harmonic polynomial, not a proof of the identity.
Remarks
- The example is deliberately asymmetric: the cancellation comes from the opposite signs of the and second derivatives, not from any symmetry between opposite faces.
Depends on
- Green's first identity on a glued elementary solid region
- The Laplacian of a $C^2$ function and of a $C^2$ vector field
- The closed unit box, with its six faces, is an elementary solid region
- The divergence theorem on an elementary solid region
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- Divergence and curl of a $C^1$ vector field
- Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
64 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
- J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus, chapter 4 (standard reference, not scraped)
- M. Corral, Vector Calculus, section 4.4 (standard reference, not scraped)