TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 curl of the gradient of a $C^{2}$ function vanishes

Statement

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

$curl \nabla ϕ = 0 on U .$

Facts & Assumptions

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

[F1]

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

[F2]

For scalar-valued $f$ , its gradient is $\nabla f (a) = (\partial_{0} f (a), \dots, \partial_{m - 1} f (a))$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[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.1

By [F2] the components of $\nabla ϕ$ are the three first partial derivatives $\partial_{x} ϕ, \partial_{y} ϕ, \partial_{z} ϕ$ . Since $ϕ$ is $C^{2}$ , [F3] with $k = 2$ says that every iterated derivative $\partial_{i} \partial_{j} ϕ$ exists and is continuous on $U$ ; so each component of $\nabla ϕ$ has continuous first partial derivatives, and by [F4] the field $\nabla ϕ$ is $C^{1}$ on $U$ and its curl is defined.

givenF2F3F4

2.1

By [F1] and [F2] the first coordinate of $curl \nabla ϕ$ is $\partial_{y} (\partial_{z} ϕ) - \partial_{z} (\partial_{y} ϕ)$ , and by [L1] applied to $ϕ$ with the index pair $y, z$ these two iterated derivatives are equal, so this coordinate is zero at every point of $U$ .

step 1.1F1F2L1

2.2

By [F1] and [F2] the second coordinate of $curl \nabla ϕ$ is $\partial_{z} (\partial_{x} ϕ) - \partial_{x} (\partial_{z} ϕ)$ , and by [L1] applied with the index pair $z, x$ these are equal, so this coordinate is zero at every point of $U$ .

step 1.1F1F2L1

2.3

By [F1] and [F2] the third coordinate of $curl \nabla ϕ$ is $\partial_{x} (\partial_{y} ϕ) - \partial_{y} (\partial_{x} ϕ)$ , and by [L1] applied with the index pair $x, y$ these are equal, so this coordinate is zero at every point of $U$ .

step 1.1F1F2L1

3.1

All three coordinates vanish at every point of $U$ , so $curl \nabla ϕ = 0$ on $U$ . The hypothesis that $ϕ$ is $C^{2}$ was used twice: in step 1.1, so that $\nabla ϕ$ is $C^{1}$ and its curl is defined at all, and in steps 2.1 to 2.3 as the hypothesis of [L1].

step 2.1step 2.2step 2.3∎

Remarks

Why $C^{1}$ would not do. With $ϕ$ merely $C^{1}$ the field $\nabla ϕ$ need not be differentiable, so $curl \nabla ϕ$ need not be defined; the statement would have no content rather than a weaker one.
What the converse would say. This theorem says every gradient of a $C^{2}$ function is curl-free. Which curl-free fields are gradients is a separate question, answered on a star-shaped open set by A $C^{1}$ field with vanishing curl on a star-shaped open subset of $R^{3}$ is conservative; the hypothesis on the domain there is not decorative, and the companion examples page exhibits a curl-free field with no potential.

Depends on

Used by

Vector potentials of a continuous field on an open subset of ℝ³ Definition

Dependency tree · two levels

17 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 curl of the gradient of a C2C2 function vanishes

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Used by

Dependency tree · two levels

Sources

The curl of the gradient of a $C^{2}$ function vanishes