TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The divergence of the curl of a $C^{2}$ field vanishes

Statement

Let $U \subseteq R^{3}$ be open and let $F : U \to R^{3}$ be $C^{2}$ . Then $curl F$ is a $C^{1}$ field on $U$ and

$div (curl F) = 0 on U .$

Facts & Assumptions

Given: The open set $U \subseteq R^{3}$ and the $C^{2}$ field $F : U \to R^{3}$ of the Statement, with the three coordinates named $x, y, z$ .

[F1]

The divergence of a $C^{1}$ field $G$ on an open $U \subseteq R^{n}$ is $div G = \sum_{i < n} \partial_{i} G_{i}$ (Divergence and curl of a $C^{1}$ vector field).

[F2]

The curl of a $C^{1}$ field $F$ on an open $U \subseteq R^{3}$ 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).

[F3]

A scalar $f$ is of class $C^{k}$ on $U$ when, for every word $(i_{1}, \dots, i_{r})$ of coordinate indices with $0 \leq r \leq k$ , the iterated derivative $\partial_{i_{r}} \dots \partial_{i_{1}} f$ exists and is continuous on $U$ ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F4]

A map $f : U \to R^{q}$ is of class $C^{k}$ when each component is of class $C^{k}$ ( $C^{k}$ Euclidean maps and diffeomorphisms).

[L1]

If $f$ is $C^{2}$ on an open subset of $R^{m}$ , then $\partial_{i} \partial_{j} f = \partial_{j} \partial_{i} f$ for every pair of coordinate indices (Clairaut--Schwarz theorem for continuous second partial derivatives).

Proof

technique · direct

1.1givenF2F3F4

By [F2] each coordinate of $curl F$ is a difference of two first partial derivatives of components of $F$ . Since $F$ is $C^{2}$ , [F4] and [F3] with $k = 2$ give that every iterated derivative $\partial_{i} \partial_{j} F_{a}$ exists and is continuous on $U$ , so each coordinate of $curl F$ has continuous first partial derivatives; by [F4] again, $curl F$ is $C^{1}$ on $U$ and its divergence is defined.

2.1step 1.1F1F2algebra

By [F1] and [F2], $div (curl F) = \partial_{x} (\partial_{y} F_{z} - \partial_{z} F_{y}) + \partial_{y} (\partial_{z} F_{x} - \partial_{x} F_{z}) + \partial_{z} (\partial_{x} F_{y} - \partial_{y} F_{x})$ , which written out is the sum of the six terms $\partial_{x} \partial_{y} F_{z}$ , $- \partial_{x} \partial_{z} F_{y}$ , $\partial_{y} \partial_{z} F_{x}$ , $- \partial_{y} \partial_{x} F_{z}$ , $\partial_{z} \partial_{x} F_{y}$ and $- \partial_{z} \partial_{y} F_{x}$ .

3.1step 2.1L1

Each component of $F$ is $C^{2}$ , so [L1] gives $\partial_{x} \partial_{y} F_{z} = \partial_{y} \partial_{x} F_{z}$ , $\partial_{y} \partial_{z} F_{x} = \partial_{z} \partial_{y} F_{x}$ and $\partial_{z} \partial_{x} F_{y} = \partial_{x} \partial_{z} F_{y}$ . Pairing the six terms of step 2.1 accordingly, $\partial_{x} \partial_{y} F_{z}$ cancels $- \partial_{y} \partial_{x} F_{z}$ , $\partial_{y} \partial_{z} F_{x}$ cancels $- \partial_{z} \partial_{y} F_{x}$ , and $\partial_{z} \partial_{x} F_{y}$ cancels $- \partial_{x} \partial_{z} F_{y}$ .

4.1step 3.1∎

The six terms therefore sum to zero at every point of $U$ , so $div (curl F) = 0$ on $U$ . The hypothesis that $F$ is $C^{2}$ is used in step 1.1, so that $curl F$ is $C^{1}$ and has a divergence, and in step 3.1 as the hypothesis of [L1].

Remarks

Where the hypothesis bites. If $F$ is only $C^{1}$ , then $curl F$ is merely continuous and its partial derivatives need not exist, so $div (curl F)$ is not defined; there is nothing to assert, rather than a weaker assertion.
The converse. A divergence-free $C^{1}$ field on a star-shaped open subset of $R^{3}$ is the curl of something: that is A divergence-free $C^{1}$ field on a star-shaped open subset of $R^{3}$ has a vector potential.

Depends on

Used by

The flux of a curl through the boundary of a glued elementary solid vanishes Corollary

Dependency tree · two levels

16 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.7 (standard reference, not scraped)
M. Corral, Vector Calculus, chapter 4 (LibreTexts) (standard reference, not scraped)

The divergence of the curl of a C2C2 field vanishes