LemmaStatement: AI-adaptedProof: AI-adaptedprecheck pass

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.

Curl-field energy identity for Newtonian potentials of divergence-free compact currents

Statement

Assume Countable Choice ( ${A C}_{ω}$ ), with the exact meaning of The Axiom of Countable Choice ( ${A C}_{ω}$ ). Let $μ_{0} > 0$ be a real scalar parameter, let $J \in C_{c}^{\infty} (R^{3}; R^{3})$ ( $C^{k}$ Euclidean maps and diffeomorphisms) with $div J = 0$ (Divergence and curl of a $C^{1}$ vector field), and define componentwise $A : = μ_{0} N (J), A_{i} = μ_{0} N (J_{i}), N f (x) = \int_{R^{3}} \frac{f (y)}{4 π ∣ x - y ∣} d λ_{3} (y),$ the Newtonian vector potential attached to Newtonian potential of compactly supported data in dimension three. Then:

(a) $A \in C^{\infty} (R^{3}; R^{3})$ with $div A = 0$ and $- Δ A = μ_{0} J$ pointwise on $R^{3}$ , componentwise (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field);

(b) there is $C > 0$ with $∣ curl A (x) ∣ \leq C / (1 + ∣ x ∣^{2})$ for every $x \in R^{3}$ ; hence $curl A \in L^{2} (R^{3}; R^{3})$ and $⟨ A, J ⟩ \in L^{1} (R^{3})$ , both in the ordinary Lebesgue sense (Integral over a measurable subset);

(c) the curl-field energy identity $\int_{R^{3}} ∣ curl A ∣^{2} d λ_{3} = μ_{0} \int_{R^{3}} ⟨ A, J ⟩ d λ_{3}$ holds, and equivalently $\frac{1}{2} \int_{R^{3}} ⟨ A, J ⟩ d λ_{3} = \frac{1}{2 μ_{0}} \int_{R^{3}} ∣ curl A ∣^{2} d λ_{3} \geq 0$ .

The identity is stated for the explicit smooth compact currents and the Newtonian construction; no uniqueness, no decay of $A$ itself beyond the curl bound of (b), and no extension to singular currents is claimed.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ , let $μ_{0} > 0$ and let $J \in C_{c}^{\infty} (R^{3}; R^{3})$ satisfy $div J = 0$ , with $A = μ_{0} N (J)$ componentwise as in the Statement.

[A1]

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

[F1]

Assume ${A C}_{ω}$ , let $ε_{0} > 0$ and $f \in C_{c}^{\infty} (R^{3}; R)$ with $N f (x) = \int_{R^{3}} f (y) / (4 π ∣ x - y ∣) d y$ . Then $N f \in C^{\infty} (R^{3})$ , $- Δ N f = f$ pointwise, and for every multi-index $α$ one has $D^{α} N f = N (D^{α} f)$ . (Newtonian potential of smooth compact data is smooth and solves the Poisson equation pointwise).

[F2]

For a measurable compactly supported $f$ , the Newtonian potential is $N f (x) = \int_{R^{n}} Φ (x - y) f (y) d y$ at each $x$ where the integral is absolutely finite. (Newtonian potential of compactly supported data).

[F3]

Assume Countable Choice, let $n \geq 3$ , let $f$ be integrable and zero outside $B_{R} (0)$ , and put $M = \int f$ . For $r = ∣ x ∣ > 2 R$ , $∣ N f (x) - \frac{M r^{2 - n}}{(n - 2) ω_{n - 1}} ∣ \leq \frac{2^{n - 1} R}{ω_{n - 1}} ∥ f ∥_{1} r^{1 - n}$ . (Far-field asymptotics of compact-source Newtonian potentials).

[F4]

Assume ${A C}_{ω}$ , let $n \geq 3$ , let $f \in L^{1} (R^{n})$ vanish outside a closed ball of radius $R$ , and let $N f$ be the Newtonian potential. Then for every $x$ with $∣ x ∣ > 2 R$ the gradient is absolutely convergent and $∣ \nabla (N f) (x) ∣ \leq \frac{2^{n - 1} ∥ f ∥_{1}}{ω_{n - 1} ∣ x ∣^{n - 1}}$ . (The far-field gradient of a compactly supported Newtonian potential).

[F5]

For $C^{1}$ fields on an open $U \subseteq R^{3}$ , $div (F \times G) = ⟨ curl F, G ⟩ - ⟨ F, curl G ⟩$ . (The divergence and curl of a cross product).

[F6]

For a $C^{2}$ field $F$ on an open $U \subseteq R^{3}$ , $curl curl F = \nabla div F - Δ F$ . (The curl of a curl is the gradient of the divergence minus the Laplacian).

[F7]

The divergence and curl are defined pointwise from first partial derivatives; for $F = (F_{x}, F_{y}, F_{z})$ one has $div F = \partial_{x} F_{x} + \partial_{y} F_{y} + \partial_{z} F_{z}$ and $curl F = (\partial_{y} F_{z} - \partial_{z} F_{y}, \partial_{z} F_{x} - \partial_{x} F_{z}, \partial_{x} F_{y} - \partial_{y} F_{x})$ . (Divergence and curl of a $C^{1}$ vector field).

[F8]

For a $C^{2}$ function the Laplacian is $Δ f = div \nabla f$ , and for a $C^{2}$ map $Δ F$ is componentwise. (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F9]

The cross product in coordinates is $(u \times v)_{x} = u_{y} v_{z} - u_{z} v_{y}$ , with the cyclic permutations for the other two coordinates. (The cross product in $R^{3}$ ).

[F10]

The Euclidean inner product is $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ , and it is symmetric. (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F11]

$B (x, r) = {y : d (x, y) < r}$ is the open ball of the metric space. (Open ball, closed ball and sphere in a metric space).

[F12]

Let $0 \leq f_{1} \leq f_{2} \leq \dots$ be measurable with $f_{n} ↑ f$ pointwise. Then $\int f_{n} d μ ↑ \int f d μ$ . (Monotone convergence for the integral).

[F13]

Let $f_{n} \to f$ almost everywhere with $∣ f_{n} ∣ \leq g$ almost everywhere for a single integrable nonnegative $g$ . Then $f \in L^{1}$ and $\int f_{n} d μ \to \int f d μ$ . (Dominated convergence).

[F14]

For measurable $f : X \to [0, + \infty]$ and $E \in A$ , $\int_{E} f d μ : = \int f χ_{E} d μ$ . (Integral over a measurable subset).

[F15]

For measurable $f, g : X \to [0, + \infty]$ with $f \leq g$ one has $\int f d μ \leq \int g d μ$ . (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F16]

For a nonnegative simple measurable function $s = \sum_{j} c_{j} χ_{E_{j}}$ the simple integral is $\int s d μ = \sum_{j} c_{j} μ (E_{j})$ . (The integral of a nonnegative simple function).

[F17]

The nonnegative integral of a nonnegative simple function equals its simple integral. (The nonnegative integral agrees with the simple integral on simple functions).

[F18]

Let $k \in N$ and let $U \subseteq R^{3}$ be open; a map on $U$ is of class $C^{k}$ when each component is, and it is smooth when it is $C^{k}$ for every $k \in N$ , in particular for every $k \geq 1$ . ( $C^{k}$ Euclidean maps and diffeomorphisms).

[F19]

Assume ${A C}_{ω}$ and $0 < ε < R$ . Then $B_{R} = {x : ∣ x ∣ < R}$ is a bounded $C^{1}$ domain with boundary $S_{R}$ and outward normal $ν (x) = x / ∣ x ∣$ , the divergence theorem applies on $B_{R}$ , and each sphere $S_{r}$ is a compact embedded $C^{1}$ hypersurface carrying a finite Borel surface measure with the standard graph charts. (Euclidean balls, annuli and spheres as bounded smooth domains and hypersurfaces).

[F20]

On a bounded $C^{1}$ Euclidean domain the divergence theorem holds with the outward normal, $\int_{Ω} div F d λ = \int_{\partial Ω} ⟨ F, ν ⟩ d S$ . (Divergence on a bounded C1 Euclidean domain).

[F21]

On a compact embedded $C^{1}$ hypersurface the surface integral is defined by finitely many graph charts, and for a bounded continuous $g$ with finite area one has $\int_{S} ∣ g ∣ d S \leq \sup_{S} ∣ g ∣ \int_{S} 1 d S$ . (Surface integration on compact C1 hypersurfaces).

[F22]

The chart surface measure on $S^{n - 1}$ equals the polar measure $σ$ , scaling by $r$ multiplies surface measure by $r^{n - 1}$ , and $∣ S^{n - 1} ∣ = n ∣ B_{1} ∣$ . (Agreement with the existing polar sphere measure).

[F23]

For every $n \geq 1$ , $V_{n} (1) = π^{n / 2} / Γ (n / 2 + 1)$ . (The closed form for the volume of the unit $n$ -ball).

[F24]

For every $s > 0$ , $Γ (s + 1) = s Γ (s)$ . (The real Gamma functional equation $Γ (s + 1) = s Γ (s)$ ).

[F25]

$Γ (1 / 2) = \sqrt{π}$ . ( $Γ (1 / 2) = \sqrt{π}$ from the Gaussian integral).

[F26]

A subset of $R^{n}$ is compact if and only if it is closed and bounded for the Euclidean metric. (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F27]

Every continuous $f : A \to R$ on a nonempty compact $A \subseteq R^{n}$ attains a maximum and a minimum on $A$ . (For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent).

[F28]

Closed balls $\overset{ˉ}{B} (x, r)$ in a metric space are closed. (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).

[F29]

A subset $A$ of a metric space is bounded if $A = \emptyset$ or there are $x_{0}$ and $r > 0$ with $A \subseteq B (x_{0}, r)$ . (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[F30]

Every compact subset of a metric space is closed and bounded. (A compact subset of a metric space is closed and bounded).

[F31]

For $f : R^{n} \to R$ the support is $supp f = \overline{{x : f (x) \neq 0}}$ , and $f$ is compactly supported when that support is compact. (The support of a function on $R^{n}$ and its compactly supported Riemann integral).

[F32]

The Lebesgue integral is linear on $L^{1} (μ)$ . (The Lebesgue integral is linear on $L^{1} (μ)$ ).

[F33]

For $n \geq 1$ the Euclidean distance $d_{2}$ is a metric on $R^{n}$ . ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it).

[F34]

Under Countable Choice every continuous map $R^{n} \to R^{m}$ is Borel measurable. (Continuous functions on Euclidean spaces are Borel measurable).

[F35]

Assume ${A C}_{ω}$ , let $n \geq 1$ , $x \in R^{n}$ and $r > 0$ ; then the Euclidean ball $B (x, r)$ is Lebesgue measurable with $0 < λ_{n} (B (x, r)) < \infty$ . (Euclidean balls have positive finite Lebesgue measure).

Proof

technique · direct

1.1F11F29F30F31F33algebra

The supports of the components $J_{i}$ are compact by [F31] and bounded by [F30], [F33] and [F29]. Fix $R > 0$ with $supp J \subseteq B_{R} (0) = B (0, R)$ , an open ball in the sense of [F11] (for the empty case any $R$ works), and put $r_{0} : = \max {2 R, 1}$ .

1.2F1F2F6F7F8F18F32algebra

By [F1] applied to each component $J_{i}$ (with [F18] supplying the smoothness of the components of $J$ ), each $A_{i} = μ_{0} N (J_{i})$ lies in $C^{\infty} (R^{3})$ and satisfies $- Δ A_{i} = μ_{0} J_{i}$ and $D^{α} A_{i} = μ_{0} N (D^{α} J_{i})$ for every multi-index $α$ ; in particular $A$ is $C^{\infty}$ , hence $C^{2}$ for [F6], and [F8] gives $- Δ A = μ_{0} J$ componentwise. Moreover $div A = \sum_{i} \partial_{i} A_{i} = μ_{0} \sum_{i} N (\partial_{i} J_{i}) = μ_{0} N (div J) = 0$ pointwise, where the middle equality uses [F1] with $α = e_{i}$ and the linearity [F32] (with [F2] supplying the integral representation).

1.3F3F4F26F27F28F33algebra

For $r > r_{0} \geq 2 R$ and each $i$ , [F3] with $n = 3$ gives $∣ N J_{i} (x) - \frac{M_{i}}{4 π r} ∣ \leq \frac{R ∥ J_{i} ∥_{1}}{π r^{2}}$ , where $M_{i} = \int J_{i}$ and $r = ∣ x ∣$ ; hence $∣ A_{i} (x) ∣ \leq μ_{0} (\frac{∣ M_{i} ∣}{4 π} + \frac{R ∥ J_{i} ∥_{1}}{π}) \frac{1}{r}$ , and [F4] with $n = 3$ gives $∣ \nabla A_{i} (x) ∣ \leq \frac{μ_{0} ∥ J_{i} ∥_{1}}{π r^{2}}$ . By [F28], [F26], [F33] and [F27], the closed ball ${\overset{ˉ}{B}}_{r_{0}} (0)$ is compact and each of the continuous functions $A_{i}$ and $\partial_{k} A_{i}$ attains a finite maximum on it, so there are finite constants $c_{1}, c_{2}$ with $∣ A (x) ∣ \leq c_{1}$ and $∣ \partial_{k} A_{i} (x) ∣ \leq c_{2}$ for all $x$ and $i, k$ ; consequently $A$ and all its first partials are bounded on $R^{3}$ .

2.1F7F9F10F14F15F16F17F35step 1.2step 1.3algebra

By [F9] each coordinate of $curl A$ is a difference of two entries of $\nabla A$ , so [F7] yields $∣ curl A (x) ∣ \leq 2 \sum_{i, k} ∣ \partial_{k} A_{i} (x) ∣ \leq 18 c_{2}$ for $∣ x ∣ \leq r_{0}$ , while for $∣ x ∣ > r_{0}$ the gradient bound of step 1.3 gives $∣ curl A (x) ∣ \leq 2 \sum_{i, k} \frac{μ_{0} ∥ J_{i} ∥_{1}}{π ∣ x ∣^{2}} \leq \frac{36 μ_{0} \max_{i} ∥ J_{i} ∥_{1}}{π ∣ x ∣^{2}}$ . Hence $∣ curl A (x) ∣ \leq C / (1 + ∣ x ∣^{2})$ on all of $R^{3}$ with $C : = \max {1, 18 c_{2} (1 + r_{0}^{2}), 72 μ_{0} \max_{i} ∥ J_{i} ∥_{1} / π}$ . Moreover $⟨ A, J ⟩$ is continuous because $A$ is $C^{\infty}$ by step 1.2 and $J$ is smooth, it is supported in the compact set $supp J \subseteq B_{R} (0)$ with $R > 0$ , and it is bounded by $3 c_{1} \max_{i} ∥ J_{i} ∥_{\infty}$ : by [F10], $∣ ⟨ A, J ⟩ ∣ \leq \sum_{i} ∣ A_{i} ∣ ∣ J_{i} ∣ \leq c_{1} \sum_{i} ∣ J_{i} ∣ \leq 3 c_{1} \max_{i} ∥ J_{i} ∥_{\infty}$ , since each $∣ A_{i} ∣ \leq ∣ A ∣ \leq c_{1}$ . Since $∣ ⟨ A, J ⟩ ∣ 1_{B_{R} (0)} \leq 3 c_{1} \max_{i} ∥ J_{i} ∥_{\infty} 1_{B_{R} (0)}$ pointwise, [F14] and [F15] give $\int_{R^{3}} ∣ ⟨ A, J ⟩ ∣ d λ_{3} = \int_{B_{R} (0)} ∣ ⟨ A, J ⟩ ∣ d λ_{3} \leq 3 c_{1} \max_{i} ∥ J_{i} ∥_{\infty} \int_{B_{R} (0)} 1 d λ_{3} = 3 c_{1} \max_{i} ∥ J_{i} ∥_{\infty} λ_{3} (B_{R} (0)) < \infty,$ the middle equality being the simple integral of the indicator by [F16] and [F17], and the finiteness of $λ_{3} (B_{R} (0))$ being [F35].

2.2F5F6F10step 1.2algebra

On $R^{3}$ one has, by [F5], [F6], [F10] and step 1.2, $div (A \times curl A) = ⟨ curl A, curl A ⟩ - ⟨ A, curl curl A ⟩ = ∣ curl A ∣^{2} - μ_{0} ⟨ A, J ⟩,$ because $curl curl A = \nabla div A - Δ A = - Δ A = μ_{0} J$ . The fields $A$ and $curl A$ are $C^{1}$ by step 1.2, so [F5] applies.

3.1F19F20step 2.2

Fix $r > r_{0}$ . By [F19] the ball $B_{r} (0)$ is a bounded $C^{1}$ domain with boundary $S_{r}$ and outward normal $ν (x) = x / ∣ x ∣$ , and [F20] applied to $F = A \times curl A$ together with step 2.2 gives $\oint_{S_{r}} ⟨ A \times curl A, ν ⟩ d S = \int_{B_{r} (0)} ∣ curl A ∣^{2} d λ_{3} - μ_{0} \int_{B_{r} (0)} ⟨ A, J ⟩ d λ_{3} .$

3.2F9F21F22F23F24F25step 1.3step 2.1algebra

For $r > r_{0}$ the boundary term is bounded by the decay estimates: [F21] and the componentwise bound $∣ (u \times v)_{x} ∣ \leq 2 \max_{k} ∣ u_{k} ∣ \max_{k} ∣ v_{k} ∣$ from [F9] give $∣ \oint_{S_{r}} ⟨ A \times curl A, ν ⟩ d S ∣ \leq \int_{S_{r}} ∣ A \times curl A ∣ d S \leq 4 \sup_{S_{r}} ∣ A ∣ \sup_{S_{r}} ∣ curl A ∣ \int_{S_{r}} 1 d S .$ By [F22], [F23], [F24] and [F25] the sphere area is $\int_{S_{r}} 1 d S = ∣ S^{2} ∣ r^{2} = 3 V_{3} (1) r^{2} = 4 π r^{2}$ , and by steps 1.3 and 2.1, $\sup_{S_{r}} ∣ A ∣ \leq c_{1}^{'} r^{- 1}$ and $\sup_{S_{r}} ∣ curl A ∣ \leq c_{2}^{'} r^{- 2}$ for constants $c_{1}^{'}, c_{2}^{'}$ independent of $r$ . Hence the boundary term is at most $16 π c_{1}^{'} c_{2}^{'} / r$ , which tends to $0$ as $r \to \infty$ .

4.1F12F13F34step 2.1step 3.1step 3.2algebra

Let $r_{n} ↑ \infty$ with $r_{n} > r_{0}$ . The functions $∣ curl A ∣^{2} 1_{B_{r_{n}} (0)}$ are nonnegative and measurable by [F34], and increase to $∣ curl A ∣^{2}$ ; [F12] therefore gives $\int_{B_{r_{n}} (0)} ∣ curl A ∣^{2} d λ_{3} ↑ L : = \int_{R^{3}} ∣ curl A ∣^{2} d λ_{3} \in [0, + \infty] .$ The functions $⟨ A, J ⟩ 1_{B_{r_{n}} (0)}$ converge pointwise to $⟨ A, J ⟩$ and are dominated by the integrable function $∣ ⟨ A, J ⟩ ∣$ of step 2.1, so [F13] gives $\int_{B_{r_{n}} (0)} ⟨ A, J ⟩ d λ_{3} \to \int_{R^{3}} ⟨ A, J ⟩ d λ_{3}$ , a finite real number. Passing to the limit in the identity of step 3.1 using the vanishing boundary term of step 3.2 yields $L = μ_{0} \int_{R^{3}} ⟨ A, J ⟩$ , so $curl A \in L^{2} (R^{3}; R^{3})$ and the identity of (c) holds; the equivalent form follows by dividing by $2 μ_{0} > 0$ , and $L \geq 0$ gives the final inequality.

5.1A1F1F3F4F12F13F20step 1.1step 1.2step 1.3step 2.1step 4.1∎

Clauses (a), (b), (c) are now established: (a) in step 1.2, the decay bound and the $L^{1}$ statement (b) in steps 2.1 and 4.1, and the identity with its equivalent form in step 4.1. The hypothesis $div J = 0$ was used only in step 1.2; smoothness and compact support only in steps 1.1 through 1.3; no uniqueness of $A$ , no decay of $A$ beyond the curl bound, and no singular-current extension is asserted. Countable Choice enters only through the cited Newtonian, measure and surface interfaces, not through any selection.

Source notes

Hunter §2.6.1 and §2.7, printed pp. 33-37, and Teschl §5.3, equations (5.21)-(5.26), printed pp. 117-118, supply the Newtonian potential, the local kernel estimates and the far-field behaviour behind the decay steps. Neither text states the curl-field energy identity in this exact form; the present proof assembles it from the supplied smoothness and decay of the Newtonian potential, the vector-calculus identity for $div (F \times G)$ , the divergence theorem on a ball and the monotone-convergence argument. The local identities $div A = 0$ and $- Δ A = μ_{0} J$ are recorded pointwise for the explicit smooth compact currents; the fine behaviour of the fields at a singular current is not treated.

Curl-field energy identity for Newtonian potentials of divergence-free compact currents

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources