CorollaryStatement: 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 curl of a curl is the gradient of the divergence minus the Laplacian

Statement

Let $U \subseteq R^{3}$ be open and let $F : U \to R^{3}$ be $C^{2}$ . Then $curl curl F$ , $\nabla div F$ and $Δ F$ are all defined on $U$ and

$curl curl F = \nabla div F - Δ F .$

Here $Δ F$ is the componentwise Laplacian of The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field.

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 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]

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

[F3]

For a $C^{2}$ map $F$ , $Δ F$ is the field whose $i$ th coordinate is $Δ F_{i}$ , and $Δ f = \sum_{i < n} \partial_{i} \partial_{i} f$ for a $C^{2}$ scalar $f$ (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F4]

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

[F5]

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

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

Every component of $F$ is $C^{2}$ , so by [F5] every iterated derivative $\partial_{i} \partial_{j} F_{a}$ exists and is continuous on $U$ . Hence each coordinate of $curl F$ , being a difference of first partial derivatives of components of $F$ by [F1], has continuous first partial derivatives, so $curl F$ is $C^{1}$ and $curl curl F$ is defined; likewise $div F$ is $C^{1}$ by [F2], so $\nabla div F$ is defined by [F4]; and $Δ F$ is defined by [F3].

2.1step 1.1F1algebra

By [F1] applied twice, the first coordinate of $curl curl F$ is $\partial_{y} (curl F)_{z} - \partial_{z} (curl F)_{y} = \partial_{y} (\partial_{x} F_{y} - \partial_{y} F_{x}) - \partial_{z} (\partial_{z} F_{x} - \partial_{x} F_{z})$ , that is $\partial_{y} \partial_{x} F_{y} - \partial_{y} \partial_{y} F_{x} - \partial_{z} \partial_{z} F_{x} + \partial_{z} \partial_{x} F_{z}$ .

3.1step 2.1algebra

Adding and subtracting the single term $\partial_{x} \partial_{x} F_{x}$ rewrites step 2.1 as $(\partial_{x} \partial_{x} F_{x} + \partial_{y} \partial_{x} F_{y} + \partial_{z} \partial_{x} F_{z}) - (\partial_{x} \partial_{x} F_{x} + \partial_{y} \partial_{y} F_{x} + \partial_{z} \partial_{z} F_{x})$ .

4.1step 3.1L1F2F3F4

By [L1], $\partial_{y} \partial_{x} F_{y} = \partial_{x} \partial_{y} F_{y}$ and $\partial_{z} \partial_{x} F_{z} = \partial_{x} \partial_{z} F_{z}$ , so the first bracket of step 3.1 is $\partial_{x} (\partial_{x} F_{x} + \partial_{y} F_{y} + \partial_{z} F_{z}) = \partial_{x} div F$ , the first coordinate of $\nabla div F$ by [F2] and [F4]; the second bracket is $Δ F_{x}$ , the first coordinate of $Δ F$ by [F3]. Hence the first coordinate of $curl curl F$ is that of $\nabla div F - Δ F$ .

4.2step 2.1step 3.1L1F1F2F3F4

In the second coordinate, [F1] gives $\partial_{z} (curl F)_{x} - \partial_{x} (curl F)_{z} = \partial_{z} \partial_{y} F_{z} - \partial_{z} \partial_{z} F_{y} - \partial_{x} \partial_{x} F_{y} + \partial_{x} \partial_{y} F_{x}$ ; adding and subtracting $\partial_{y} \partial_{y} F_{y}$ and applying [L1] to $\partial_{z} \partial_{y} F_{z} = \partial_{y} \partial_{z} F_{z}$ and $\partial_{x} \partial_{y} F_{x} = \partial_{y} \partial_{x} F_{x}$ turns it into $\partial_{y} div F - Δ F_{y}$ . In the third coordinate, [F1] gives $\partial_{x} (curl F)_{y} - \partial_{y} (curl F)_{x} = \partial_{x} \partial_{z} F_{x} - \partial_{x} \partial_{x} F_{z} - \partial_{y} \partial_{y} F_{z} + \partial_{y} \partial_{z} F_{y}$ ; adding and subtracting $\partial_{z} \partial_{z} F_{z}$ and applying [L1] to $\partial_{x} \partial_{z} F_{x} = \partial_{z} \partial_{x} F_{x}$ and $\partial_{y} \partial_{z} F_{y} = \partial_{z} \partial_{y} F_{y}$ turns it into $\partial_{z} div F - Δ F_{z}$ .

5.1step 4.1step 4.2∎

All three coordinates of $curl curl F$ agree with those of $\nabla div F - Δ F$ at every point of $U$ , which is the asserted identity. The hypothesis that $F$ is $C^{2}$ is used in step 1.1, so that all three expressions are defined, and in steps 4.1 and 4.2 as the hypothesis of [L1].

Remarks

The added and subtracted term is what makes the identity close. The expansion of $(curl curl F)_{x}$ contains no pure second derivative $\partial_{x} \partial_{x} F_{x}$ , while both $\nabla div F$ and $Δ F$ do; that one term belongs to both groups and cancels between them, which is why it can be inserted at will and why neither side alone matches the expansion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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