CorollaryStatement: AI-adaptedProof: 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.

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

Statement

Let a finite gluing of elementary solid regions be given, with union $E$ and outer boundary presentation $Σ^{o u t}$ , and let $F$ be a vector field of class $C^{2}$ on an open set $O \subseteq R^{3}$ containing $E$ . Then

$\iint_{\partial E} ⟨ curl F, n ⟩ = 0.$

The hypothesis is $C^{2}$ , not $C^{1}$ : with $F$ only $C^{1}$ the field $curl F$ need not have a divergence at any point, so neither the degree-two identity nor the divergence theorem has a hypothesis to consume.

Facts & Assumptions

Given: The finite gluing with union $E$ and outer presentation $Σ^{o u t}$ , the open $O \supseteq E$ , and the $C^{2}$ field $F$ on $O$ .

[F1]

The curl of a $C^{1}$ field on an open subset of $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})$ , and the divergence of a $C^{1}$ field is $div G = \sum_{i < n} \partial_{i} G_{i}$ (Divergence and curl of a $C^{1}$ vector field).

[F2]

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

[F3]

In a finite gluing the outer patches form a compatible finite patch presentation of $\partial E$ , over which flux is the sum of the patch values, with $⟨ x, y ⟩ = \sum_{i < m} x_{i} y_{i}$ (Finite gluings of elementary solid regions and their outward boundary presentation, Finitely patched regular surfaces, their area, scalar integrals, and flux, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L1]

For $U \subseteq R^{3}$ open and $F : U \to R^{3}$ of class $C^{2}$ , the field $curl F$ is $C^{1}$ on $U$ and $div (curl F) = 0$ on $U$ (The divergence of the curl of a $C^{2}$ field vanishes).

[L2]

For a finite gluing with union $E$ and a $C^{1}$ field $G$ on an open set containing $E$ whose divergence vanishes there, $\iint_{\partial E} ⟨ G, n ⟩ = 0$ (A field with vanishing divergence has zero outward flux through the boundary of a glued elementary solid).

Proof

technique · direct

1.1

Each coordinate of $curl F$ is a difference of two first partial derivatives of components of $F$ by [F1]. Since $F$ is $C^{2}$ on $O$ , [F2] makes every iterated derivative $\partial_{i} \partial_{j} F_{a}$ exist and be continuous on $O$ , so each coordinate of $curl F$ has continuous first partial derivatives; hence $curl F$ is a $C^{1}$ field on $O$ , which is what [L1] asserts and which is exactly the regularity [L2] requires of the field it is applied to.

givenF1F2L1

2.1

By [L1] the divergence of $curl F$ vanishes at every point of $O$ , and $O$ is an open set containing $E$ . So [L2] applied to $G = curl F$ , a $C^{1}$ field on $O$ by step 1.1 with vanishing divergence there, gives $\iint_{\partial E} ⟨ curl F, n ⟩ = 0$ , the flux being read over the outer presentation as in [F3].

step 1.1F3L1L2∎

Remarks

Where $C^{2}$ is spent. It is used once, in step 1.1, to make $curl F$ a $C^{1}$ field. Everything after that is the divergence-free corollary applied to that field. The identity $div curl F = 0$ is itself a $C^{2}$ statement, so the hypothesis cannot be weakened by rearranging the argument.
The converse is false. A field with zero outward flux through the boundary of every glued elementary solid need not be a curl on the whole of $O$ : the divergence-free field is a curl on a star-shaped open set by A divergence-free $C^{1}$ field on a star-shaped open subset of $R^{3}$ has a vector potential, and on a general open set that theorem's hypothesis is unavailable. Nothing here asserts otherwise.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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

M. Corral, Vector Calculus, chapter 4 (LibreTexts), Corollary 4.18 (standard reference, not scraped)