Alphabeta Math
LemmaStatement: AI-adaptedProof: 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 flux integrand of a C2 patch is a two-dimensional curl of the pulled-back field

Statement

Let O⊆R2 be open, let φ:O→R3 be C2, let U⊆R3 be open with φ[O]⊆U and let F:U→R3 be C1. Put P∗=⟨F∘φ,φu⟩ and Q∗=⟨F∘φ,φv⟩ on O. Then P∗ and Q∗ are C1 on O and, at every point of O, the difference of the two pulled-back partial derivatives equals the curl flux integrand:

∂uQ∗−∂vP∗=⟨(curl⁡F)∘φ, φu×φv⟩.

No regularity of the patch is used: the identity holds also at parameter points where φu×φv=0.

Facts & Assumptions

Given: The open sets O⊆R2 and U⊆R3, the C2 map φ:O→R3 with φ[O]⊆U, and the C1 field F:U→R3.

[F1]

In the present local setting, define the pulled-back functions directly by P∗=⟨F∘φ,φu⟩ and Q∗=⟨F∘φ,φv⟩ on O. For a regular patch over a finite elementary Green region these agree with the notation of The induced boundary chain and circulation of a C2 patch over a finite elementary Green region.

[F2]

For x,y∈Rm, ⟨x,y⟩=∑i<mxiyi (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn).

[F3]

For u,v∈R3, u×v=(uyvz−uzvy, uzvx−uxvz, uxvy−uyvx) (The cross product in R3), and the curl of a C1 field is curl⁡F=(∂yFz−∂zFy, ∂zFx−∂xFz, ∂xFy−∂yFx) (Divergence and curl of a C1 vector field).

[F4]

A map is of class Ck when each component is (Ck Euclidean maps and diffeomorphisms), and a scalar is Ck when every iterated derivative of length at most k exists and is continuous (Ck maps and multi-index derivative notation in Euclidean space).

[F5]

If every partial derivative ∂jfi(a) exists, the Jacobian matrix is Jf(a)=(∂jfi(a))i<n,j<m (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L1]

For a C1 field F on an open U⊆R3, a point p∈U and u,v∈R3, ⟨DF(p)u,v⟩−⟨DF(p)v,u⟩=⟨curl⁡F(p),u×v⟩ (The curl measures the antisymmetric part of the total derivative).

[L2]

If f is C2 on an open subset of Rm, then ∂i∂jf=∂j∂if for every pair of coordinate indices (Clairaut--Schwarz theorem for continuous second partial derivatives).

[L3]

If f is totally differentiable at a and g at f(a), then D(g∘f)(a)=Dg(f(a))∘Df(a) (The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a)).

[L4]

If f is totally differentiable at a then Dwf(a)=Df(a)w for every w, and the matrix of Df(a) is Jf(a) (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L5]

If every partial derivative of f exists on a neighbourhood of a and is continuous at a, then f is totally differentiable at a with Df(a) the linear map of matrix Jf(a) (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L6]

Proof

technique · direct
1.1givenF1F2F4L3L4L5L6

Since φ is C2 on O, [F4] makes each ∂uφi and ∂vφi a C1 function on O; and since F is C1 on U with φ[O]⊆U, [L3], [L4] and [L5] make each Fi∘φ differentiable in each parameter with ∂u(Fi∘φ)=∑j(∂jFi)(φ) ∂uφj,∂v(Fi∘φ)=∑j(∂jFi)(φ) ∂vφj, both continuous on O, so F∘φ is C1 there. By [F1], [F2] and [L6], P∗=∑iFi(φ) ∂uφi and Q∗=∑iFi(φ) ∂vφi are then C1 on O.

2.1step 1.1F2F5L4L6

Differentiating Q∗ with respect to u by [L6] and substituting step 1.1, ∂uQ∗=∑i(∑j(∂jFi)(φ) ∂uφj)∂vφi+∑iFi(φ) ∂u∂vφi, and by [F2], [F5] and [L4] the first double sum is ⟨DF(φ)φu,φv⟩ while the second is ⟨F(φ),∂u∂vφ⟩.

2.2step 1.1F2F5L4L6

The same computation for P∗ with respect to v gives ∂vP∗=∑i(∑j(∂jFi)(φ) ∂vφj)∂uφi+∑iFi(φ) ∂v∂uφi=⟨DF(φ)φv,φu⟩+⟨F(φ),∂v∂uφ⟩.

3.1step 2.1step 2.2F4L2

Each component φi is C2 on O by [F4], so [L2] gives ∂u∂vφi=∂v∂uφi for every i; hence the two terms ⟨F(φ),∂u∂vφ⟩ and ⟨F(φ),∂v∂uφ⟩ of steps 2.1 and 2.2 are equal. This is the only place where φ being C2 rather than C1 is used.

4.1step 2.1step 2.2step 3.1F3L1∎

Subtracting step 2.2 from step 2.1 and cancelling by step 3.1 leaves ∂uQ∗−∂vP∗=⟨DF(φ)φu,φv⟩−⟨DF(φ)φv,φu⟩, which by [L1] applied at the point φ with the vectors φu and φv is ⟨curl⁡F(φ),φu×φv⟩, the coordinates being those of [F3]. No step used φu×φv≠0.

Remarks

  • The right-hand side is a flux integrand, but the identity is not about flux. It is a pointwise equality of two continuous functions on O. Reading its right side as the flux integrand of curl⁡F through the patch requires the patch to be regular; the identity itself does not, which is why it also holds along the parameter boundary, where a regular patch is allowed to degenerate.

  • What each hypothesis is for. F being C1 makes curl⁡F exist and makes the chain rule of step 1.1 available; φ being C2 makes φu and φv differentiable, so that steps 2.1 and 2.2 can be written at all, and makes the two mixed second derivatives equal in step 3.1.

Depends on

Used by

Dependency tree · two levels

56 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