Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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 Σout, and let F be a vector field of class C2 on an open set O⊆R3 containing E. Then

∬∂E⟨curl⁡F,n⟩=0.

The hypothesis is C2, not C1: with F only C1 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 Σout, the open O⊇E, and the C2 field F on O.

[F1]

The curl of a C1 field on an open subset of R3 is curl⁡F=(∂yFz−∂zFy, ∂zFx−∂xFz, ∂xFy−∂yFx), and the divergence of a C1 field is div⁡G=∑i<n∂iGi (Divergence and curl of a C1 vector field).

[F2]

A scalar f is of class Ck on U when, for every word (i1,…,ir) of coordinate indices with 0≤r≤k, the iterated derivative ∂ir⋯∂i1f exists and is continuous on U (Ck maps and multi-index derivative notation in Euclidean space).

[F3]

In a finite gluing the outer patches form a compatible finite patch presentation of ∂E, over which flux is the sum of the patch values, with ⟨x,y⟩=∑i<mxiyi (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⟩=∑k<nxkyk on Rn).

[L1]

For U⊆R3 open and F:U→R3 of class C2, the field curl⁡F is C1 on U and div⁡(curl⁡F)=0 on U (The divergence of the curl of a C2 field vanishes).

[L2]

For a finite gluing with union E and a C1 field G on an open set containing E whose divergence vanishes there, ∬∂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.1givenF1F2L1

Each coordinate of curl⁡F is a difference of two first partial derivatives of components of F by [F1]. Since F is C2 on O, [F2] makes every iterated derivative ∂i∂jFa exist and be continuous on O, so each coordinate of curl⁡F has continuous first partial derivatives; hence curl⁡F is a C1 field on O, which is what [L1] asserts and which is exactly the regularity [L2] requires of the field it is applied to.

2.1step 1.1F3L1L2∎

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 C1 field on O by step 1.1 with vanishing divergence there, gives ∬∂E⟨curl⁡F,n⟩=0, the flux being read over the outer presentation as in [F3].

Remarks

  • Where C2 is spent. It is used once, in step 1.1, to make curl⁡F a C1 field. Everything after that is the divergence-free corollary applied to that field. The identity div⁡curl⁡F=0 is itself a C2 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 C1 field on a star-shaped open subset of R3 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