TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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 divergence-free $C^{1}$ field on a star-shaped open subset of $R^{3}$ has a vector potential

Statement

Let $U \subseteq R^{3}$ be open and star-shaped with star centre $a$ , and let $B : U \to R^{3}$ be $C^{1}$ with $div B = 0$ on $U$ . Then $B$ has a vector potential on $U$ in the sense of Vector potentials of a continuous field on an open subset of $R^{3}$ : the map

$A (x) : = \int_{0}^{1} t B (a + t (x - a)) \times (x - a) d t (x \in U),$

understood coordinatewise, is $C^{1}$ on $U$ and satisfies $curl A = B$ .

Facts & Assumptions

Given: The star-shaped open set $U \subseteq R^{3}$ with centre $a$ , and the $C^{1}$ field $B : U \to R^{3}$ with $div B = 0$ on $U$ . Throughout, $w : = x - a$ and $z_{t} : = a + t w$ .

[F1]

Given a continuous $B$ on an open $U \subseteq R^{3}$ , a map $A$ is a vector potential for $B$ when $A$ is $C^{1}$ on $U$ and $curl A = B$ (Vector potentials of a continuous field on an open subset of $R^{3}$ ).

[F2]

A nonempty open $U \subseteq R^{n}$ is star-shaped with respect to $a \in U$ when $a + t (x - a) \in U$ for every $x \in U$ and $0 \leq t \leq 1$ (Star-shaped open subsets of Euclidean space).

[F3]

For $u = (u_{x}, u_{y}, u_{z})$ and $v = (v_{x}, v_{y}, v_{z})$ in $R^{3}$ , $u \times v = (u_{y} v_{z} - u_{z} v_{y}, u_{z} v_{x} - u_{x} v_{z}, u_{x} v_{y} - u_{y} v_{x})$ (The cross product in $R^{3}$ ).

[F4]

The divergence of a $C^{1}$ field $F$ on an open $U \subseteq R^{n}$ is $div F = \sum_{i < n} \partial_{i} F_{i}$ , and for $n = 3$ its curl is $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).

[F5]

If every partial derivative $\partial_{j} f_{i} (a)$ of $f$ exists, the Jacobian matrix is $J f (a) = (\partial_{j} f_{i} (a))_{i < n, j < m}$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L1]

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

[L2]

Let $α < β$ and $c < d$ , let $g, h : [α, β] \times [c, d] \to R$ be continuous, and suppose for every fixed $t$ that $s \mapsto g (s, t)$ is differentiable on $(α, β)$ with derivative $h (s, t)$ . Then $G (s) = \int_{c}^{d} g (s, t) d t$ is differentiable on $[α, β]$ with $G^{'} (s) = \int_{c}^{d} h (s, t) d t$ (Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral).

[L3]

If $G$ is continuous on $[α, β]$ and differentiable on $(α, β)$ , and $f$ is Riemann integrable on $[α, β]$ with $f = G^{'}$ on $(α, β)$ , then $\int_{α}^{β} f = G (β) - G (α)$ (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[L4]

If $f$ is totally differentiable at $p$ and $g$ at $f (p)$ , then $D (g \circ f) (p) = D g (f (p)) \circ D f (p)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L5]

If $f$ is totally differentiable at $p$ then $D_{v} f (p) = D f (p) v$ for every $v$ ; in particular $\partial_{j} f (p) = D f (p) e_{j}$ , and the matrix of $D f (p)$ is $J f (p)$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L6]

If every partial derivative of $f$ exists on a neighbourhood of $p$ and is continuous at $p$ , then $f$ is totally differentiable at $p$ and $D f (p)$ is the linear map with matrix $J f (p)$ (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L7]

For real functions of one real variable differentiable at a point, $f g$ is differentiable there and $(f g)^{'} = f^{'} g + f g^{'}$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L8]

A continuous map from a compact metric space to a metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous); a closed bounded subset of $R^{m}$ is compact (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).

[L9]

If $f$ and $g$ are integrable between $u$ and $v$ and $∣ f - g ∣ \leq η$ throughout the closed interval with those endpoints, then $∣ \int_{u}^{v} f - \int_{u}^{v} g ∣ \leq η ∣ v - u ∣$ (Uniformly close integrable functions have integrals differing by at most the interval length times their uniform error); a continuous function on a closed bounded interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

Proof

technique · constructive

1.1

Take $A$ to be the map displayed in the Statement. By [F2] every $z_{t} = a + t w$ with $0 \leq t \leq 1$ lies in $U$ when $x \in U$ , so $B (z_{t})$ is defined there; by [L9] each coordinate of the integrand, being continuous in $t$ , is integrable on $[0, 1]$ , so $A (x)$ is defined for every $x \in U$ .

givenF2L9construct

1.2

By [F3] each coordinate of $t B (z_{t}) \times w$ is a sum of terms $\pm t B_{k} (z_{t}) w_{l}$ . The map $(x, t) \mapsto z_{t}$ is continuous, so each such term is continuous in $(x, t)$ ; and since $B$ is $C^{1}$ , [L6], [L4] and [L5] give $\partial_{j} (B_{k} (z_{t})) = t (\partial_{j} B_{k}) (z_{t})$ , which is again continuous in $(x, t)$ , while $\partial_{j} w_{l}$ is $1$ if $l = j$ and $0$ otherwise. Hence each coordinate of the integrand has, in each coordinate of $x$ , a partial derivative that is continuous in $(x, t)$ .

givenF3L4L5L6

2.1

Fix $p \in U$ , choose a closed box $Q \subseteq U$ with $p$ in its interior, and fix indices $i, j$ . Applying [L2] with $[α, β]$ the $j$ th edge of $Q$ , the other coordinates of $x$ held at those of $p$ , and $[c, d] = [0, 1]$ , using step 1.2 for the continuity of $g$ and $h$ and for the derivative hypothesis, gives that $\partial_{j} A_{i}$ exists at $p$ with $\partial_{j} A_{i} (p) = \int_{0}^{1} \partial_{j} (t (B (z_{t}) \times w)_{i}) d t$ . The set $Q \times [0, 1]$ is closed and bounded in $R^{4}$ , hence compact by [L8], so the integrand of that formula is uniformly continuous on it by [L8]; given $ε > 0$ this supplies $δ > 0$ such that points of $Q$ within $δ$ make the two integrands differ by at most $ε$ at every $t$ , and [L9] then bounds the difference of the two integrals by $ε$ . So $\partial_{j} A_{i}$ is continuous on the interior of $Q$ , and as $p$ was arbitrary, $A$ is $C^{1}$ on $U$ and $curl A$ is defined by [F4] and [F5].

step 1.2L2L6L8L9F4F5

2.2

Fix $t$ with $0 \leq t \leq 1$ and consider the two fields $x \mapsto B (z_{t})$ and $x \mapsto w = x - a$ on $U$ . For the first, step 1.2 gives $\partial_{j} (B_{k} (z_{t})) = t (\partial_{j} B_{k}) (z_{t})$ , so by [F5] its Jacobian matrix is $t J B (z_{t})$ and by [F4] its divergence is $t \sum_{k < 3} (\partial_{k} B_{k}) (z_{t}) = t (div B) (z_{t}) = 0$ . For the second, $\partial_{j} w_{l}$ is $1$ if $l = j$ and $0$ otherwise, so its Jacobian matrix is the identity and its divergence is $3$ ; both fields are $C^{1}$ since these derivatives are continuous.

step 1.1L4L5F4F5given

3.1

Applying [L1] to those two fields at a fixed $t$ , and multiplying by $t$ , gives ${curl}_{x} (t B (z_{t}) \times w) = t (3 B (z_{t}) - 0 \cdot w + t J B (z_{t}) w - B (z_{t})) = 2 t B (z_{t}) + t^{2} J B (z_{t}) w,$ where by step 2.2 the term $(div G) F$ contributes $3 B (z_{t})$ , the term $- (div F) G$ contributes $0$ , the term $D F G$ contributes $t J B (z_{t}) w$ and the term $- D G F$ contributes $- B (z_{t})$ . At $x = a$ this reads $0 = 0$ in the second and fourth terms, since $w = 0$ there.

step 2.2L1F3algebra

4.1

By [F4] each coordinate of $curl A$ is a difference of two of the partial derivatives produced in step 2.1, and each of those is an integral over $[0, 1]$ ; subtracting the two integrals and using step 3.1 for the resulting integrand gives $curl A (x) = \int_{0}^{1} (2 t B (z_{t}) + t^{2} J B (z_{t}) w) d t,$ again coordinatewise.

step 2.1step 3.1L2

5.1

For fixed $x$ , put $Γ (t) : = t^{2} B (z_{t})$ on $[0, 1]$ . The map $t \mapsto z_{t}$ is differentiable with derivative $w$ , and $B$ is totally differentiable by [L6], so [L4] and [L5] give $\frac{d}{d t} B (z_{t}) = D B (z_{t}) w = J B (z_{t}) w$ ; with [L7] applied to the product of $t^{2}$ and each coordinate of $B (z_{t})$ this yields $Γ^{'} (t) = 2 t B (z_{t}) + t^{2} J B (z_{t}) w$ , the integrand of step 4.1, which is continuous on $[0, 1]$ and hence integrable by [L9].

step 3.1L7L4L5L6L9

6.1

By step 5.1 the function $Γ$ is continuous on $[0, 1]$ and differentiable there, and its derivative is the integrand of step 4.1, so [L3] applied coordinate by coordinate on $[0, 1]$ evaluates that integral as $Γ (1) - Γ (0) = 1^{2} B (z_{1}) - 0^{2} B (z_{0}) = B (x)$ , using $z_{1} = x$ and the factor $t^{2}$ at $t = 0$ .

step 4.1step 5.1L3

7.1

Steps 4.1 and 6.1 give $curl A = B$ on $U$ , and step 2.1 gives that $A$ is $C^{1}$ on $U$ ; by [F1] the constructed $A$ is a vector potential for $B$ .

step 2.1step 6.1F1discharge-construct: the displayed formula∎

Remarks

Where each hypothesis enters. Star-shapedness is used exactly once, in step 1.1, to know that the segment from the centre to $x$ stays in $U$ so that the integral is defined. The vanishing of $div B$ is used exactly once, in step 2.2, to kill the term $- (div F) G$ ; without it the curl of $A$ would carry an extra term $- t^{2} (div B) (z_{t}) w$ and the integrand would not be an exact derivative in $t$ .
The potential is not unique and the formula is not canonical. Adding the gradient of any $C^{2}$ function leaves the curl unchanged by The curl of the gradient of a $C^{2}$ function vanishes, so the displayed $A$ is one witness among many; it is the one that vanishes at the star centre.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

95 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 (University of British Columbia), Theorem 4.1.16 (standard reference, not scraped)

A divergence-free C1C1 field on a star-shaped open subset of R3R3 has a vector potential