Alphabeta Math
CorollaryStatement: Literature-sourcedProof: 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 normal component of the curl is the limiting circulation per unit area of shrinking discs

Statement

Let O⊆R3 be open, let F:O→R3 be C1, let p∈O and let n∈R3 have ∥n∥2=1. Then there are a,b∈R3 with

∥a∥2=∥b∥2=1,⟨a,b⟩=⟨a,n⟩=⟨b,n⟩=0,a×b=n,

and a real r0>0 such that for every r with 0<r≤r0 the map

φr(ρ,θ):=p+ρcos⁡θ a+ρsin⁡θ b((ρ,θ)∈Dr:=[0,r]×[0,2π])

is a C2 patch over a finite elementary Green region whose image lies in O, with φr,ρ×φr,θ=ρ n; the circulation of F around its induced boundary chain is the vector line integral of F along the circle Cr(t):=p+rcos⁡t a+rsin⁡t b on [0,2π]; and

lim⁡r→0+1πr2∫CrF⋅dr=⟨curl⁡F(p),n⟩,

meaning: for every real ε>0 there is a real δ>0 such that every r with 0<r≤r0 and r<δ satisfies ∣1πr2∫CrF⋅dr−⟨curl⁡F(p),n⟩∣≤ε.

Facts & Assumptions

Given: The open O⊆R3, the C1 field F on O, the point p∈O, the unit vector n, and the notation Dr=[0,r]×[0,2π] of the Statement.

[F1]

For x,y∈Rm, ⟨x,y⟩=∑i<mxiyi and ∥x∥2=⟨x,x⟩; the inner product is symmetric and bilinear, and ⟨x,x⟩=0 only for x=0 (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn). The standard unit vector ek has kth coordinate 1 and the others 0 (The standard list e:n→Fn with ei(i)=1F and ei(j)=0F for j≠i is an ordered basis of Fn; hence dim⁡FFn=n, and F0 is the zero space with basis ∅ and dimension 0).

[F2]

For u,v∈R3, u×v=(uyvz−uzvy, uzvx−uxvz, uxvy−uyvx) (The cross product in R3); the curl of a C1 field is that of Divergence and curl of a C1 vector field.

[F3]

A compact Type I region is {(s,t):a≤s≤b, α(s)≤t≤β(s)} with a<b and continuous piecewise-C1 α≤β, strict on (a,b); it is compact and Jordan measurable, an elementary Green region admits both descriptions, and a finite elementary Green region is a nonempty finite union of them with the stated conditions (Type I, Type II, and elementary regions for Green's theorem).

[F4]

The positive boundary of a Type I region traverses the lower graph from left to right, the right endpoint arc upward, the upper graph from right to left, and the left endpoint arc downward, omitting zero-length arcs; the boundary integral over the resulting chain is the finite sum over its arcs (Positive orientation of elementary-region boundaries).

[F5]

A regular parametrized surface patch has a compact Jordan parameter region that is the closure of its nonempty connected interior, a parametrization C1 on an open neighbourhood of it, nonvanishing parameter cross product on the interior, and no interior parameter point sharing its image with a distinct point of the region (Regular parametrized surface patches on compact Jordan parameter regions); a C2 patch over a finite elementary Green region adds the supplied elementary decomposition and the class C2 (The induced boundary chain and circulation of a C2 patch over a finite elementary Green region).

[F6]

A vector line integral along a piecewise-C1 path is ∑i∫titi+1⟨F(γ(t)),vi(t)⟩ dt, and is 0 on a degenerate parameter interval (Scalar line integrals with respect to arc length and vector-field line integrals); reversal of a path is γ−(t)=γ(a+b−t) and constant paths are allowed (Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).

[F7]

A set is open in a metric space when each of its points has a ball around it inside the set (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement); a map is continuous at a point when every ε>0 admits a δ>0 carrying the δ-ball into the ε-ball (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form); and lim⁡x→cf(x)=L has the usual meaning (The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A). Integration over a bounded Jordan set is that of The Riemann integral of a bounded function over a bounded Jordan measurable set, and Ck is the componentwise class of Ck Euclidean maps and diffeomorphisms.

[L1]

The cross product is bilinear and alternating, ⟨u×v,w⟩=det⁡[u v w], and u×v is orthogonal to both u and v (The cross product is bilinear, alternating, and orthogonal to both factors).

[L2]

For u,v∈R3, ∥u×v∥22=∥u∥22∥v∥22−⟨u,v⟩2, and this is positive exactly when u and v are linearly independent (The squared cross-product norm is the Gram determinant of two vectors).

[L3]

(sin⁡t)′=cos⁡t, (cos⁡t)′=−sin⁡t, sin⁡0=0 and cos⁡0=1 (The derivatives of sine and cosine are cosine and minus sine); sin⁡2t+cos⁡2t=1 and sin⁡(−t)=−sin⁡t, cos⁡(−t)=cos⁡t (Parity and the Pythagorean identity for sine and cosine).

[L4]

sin⁡(s+t)=sin⁡scos⁡t+cos⁡ssin⁡t and cos⁡(s+t)=cos⁡scos⁡t−sin⁡ssin⁡t (The addition formulas for sine and cosine).

[L5]

sin⁡x=0 if and only if x=mπ for some integer m, and both sine and cosine have period 2π (The zero sets of sine and cosine and the least positive common period 2 pi); sin⁡π=0 and cos⁡π=−1 (Quarter-turn values and shifts by pi/2 and pi).

[L6]

For a bounded Jordan set E⊆Rp+q and integrable g whose sections are integrable outside a content-zero set, ∫Eg=∫h(x) dx with h(x)=∫Exgx (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[L8]

For integrable f,g on a nondegenerate rectangle and scalars α,β: αf+βg is integrable with integral α∫f+β∫g; if f≤g then ∫f≤∫g; and ∣f∣ is integrable with ∣∫f∣≤∫∣f∣ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L9]

Every continuous real function on a compact Jordan measurable set is Riemann integrable over it (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

[L10]

Vector line integrals negate under reversal (Line integrals under reversal and concatenation).

[L11]

For a C2 patch over a finite elementary Green region and a C1 field on an open set containing the patch image, the circulation around the induced boundary chain equals the flux of the curl in the induced orientation (The classical Stokes theorem for a C2 patch over a finite elementary Green region).

Proof

technique · constructive
1.1givenF1construct

Since ∑knk2=∥n∥22=1 by [F1], not all three coordinates can have nk2>1/3; fix k with nk2≤1/3. Then n and ek are linearly independent: a relation ek=λn would force ∣λ∣=1 by comparing norms, hence n=±ek and nk2=1, contradicting nk2≤1/3; and n≠0.

1.2F1F2algebra

For all u,v,w∈R3, expanding by [F1] and [F2] gives ⟨u×v,w⟩=(uyvz−uzvy)wx+(uzvx−uxvz)wy+(uxvy−uyvx)wz, ⟨w×u,v⟩=(wyuz−wzuy)vx+(wzux−wxuz)vy+(wxuy−wyux)vz, and the six signed monomials of the first expression are those of the second, matched as uyvzwx with wxuyvz, −uzvywx with −wxuzvy, uzvxwy with wyuzvx, −uxvzwy with −wyuxvz, uxvywz with wzuxvy and −uyvxwz with −wzuyvx. Hence ⟨u×v,w⟩=⟨w×u,v⟩.

1.3givenF7choose

The set O is open and p∈O, so by [F7] there is a real r0>0 with every q satisfying ∥q−p∥2≤r0 lying in O; take such an r0.

1.4givenF3L6L7L9

Fix r with 0<r≤r0. The function (ρ,θ)↦ρ is continuous on the compact Jordan rectangle Dr, hence integrable by [L9] and [F3]. Its sections in θ are the continuous functions ρ↦ρ on [0,r], so [L6] gives ∫Drρ=∫02π(∫0rρ dρ)dθ; by [L7] with G(ρ)=ρ2/2 the inner integral is r2/2, and again by [L7] with G(θ)=r2θ/2 the outer integral is πr2. So ∫Drρ=πr2.

2.1step 1.1F1L1L2construct

By step 1.1 and [L2] the number ∥n×ek∥22 is positive, so n×ek≠0; put a:=n×ek∥n×ek∥2. Then ∥a∥2=1 by [F1], and ⟨a,n⟩=0 because n×ek is orthogonal to n by [L1].

3.1step 2.1F1L1L2construct

Put b:=n×a. By [L1] it is orthogonal to n and to a, so ⟨b,n⟩=⟨b,a⟩=0; and by [L2] with step 2.1, ∥b∥22=∥n∥22∥a∥22−⟨n,a⟩2=1, so ∥b∥2=1.

4.1step 1.2step 2.1step 3.1F1L2

By step 1.2 with u=a, v=b and w=n, and then step 3.1, ⟨a×b,n⟩=⟨n×a,b⟩=⟨b,b⟩=1. By [L2] and steps 2.1 and 3.1, ∥a×b∥22=∥a∥22∥b∥22−⟨a,b⟩2=1. Hence ∥a×b−n∥22=∥a×b∥22−2⟨a×b,n⟩+∥n∥22=1−2+1=0 by [F1], and positive definiteness in [F1] gives a×b=n.

4.2step 2.1step 3.1F7L1L3L7

By [L3] and [L7] the map φr is differentiable in each parameter with φr,ρ=cos⁡θ a+sin⁡θ b and φr,θ=ρ(−sin⁡θ a+cos⁡θ b), and all its iterated parameter derivatives of order at most 2 exist and are continuous, so φr is C2 on the whole plane by [F7]. Expanding by bilinearity and the alternating law in [L1], φr,ρ×φr,θ=ρ(cos⁡2θ (a×b)−sin⁡2θ (b×a))=ρ(cos⁡2θ+sin⁡2θ)(a×b), which is ρ (a×b) by [L3].

5.1step 4.1step 4.2

Combining steps 4.1 and 4.2, φr,ρ×φr,θ=ρ n, which is nonzero exactly when ρ>0.

6.1step 1.3step 2.1step 3.1step 5.1F1F3F5L3L4L5

The rectangle Dr is a Type I and a Type II region with 0<r and constant graphs 0<2π, hence an elementary Green region and a nonempty finite elementary Green region with the one-piece decomposition, compact and Jordan measurable, and it is the closure of its nonempty convex, hence connected, interior (0,r)×(0,2π) ([F3], [F5]). The cross product of step 5.1 is nonzero on that interior. For injectivity, let (ρ,θ) be interior and (ρ′,θ′)∈Dr have the same image; pairing ρcos⁡θ a+ρsin⁡θ b=ρ′cos⁡θ′ a+ρ′sin⁡θ′ b with a and with b and using steps 2.1 and 3.1 gives ρcos⁡θ=ρ′cos⁡θ′ and ρsin⁡θ=ρ′sin⁡θ′; squaring and adding with [L3] gives ρ2=ρ′2, so ρ′=ρ>0 and cos⁡θ=cos⁡θ′, sin⁡θ=sin⁡θ′. Then [L4] and [L3] give cos⁡(θ−θ′)=cos⁡θcos⁡θ′+sin⁡θsin⁡θ′=cos⁡2θ′+sin⁡2θ′=1, so sin⁡2(θ−θ′)=0 and θ−θ′=mπ for an integer m by [L3] and [L5]; since θ∈(0,2π) and θ′∈[0,2π] we have ∣θ−θ′∣<2π, so m∈{−1,0,1}, and cos⁡(±π)=−1≠1 by [L5], leaving θ=θ′. Finally ∥φr(ρ,θ)−p∥2=ρ≤r≤r0 by [F1], steps 2.1 and 3.1 and [L3], so the image lies in O by step 1.3. Hence (Dr,φr) is a C2 patch over a finite elementary Green region with image in O.

7.1step 6.1F4F6L3L5L10

By [F4] the positive boundary chain of Dr in its Type I description, with ρ horizontal, is the four arcs σ1(t)=(t,0) on [0,r], σ2(t)=(r,t) on [0,2π], σ3(t)=(r−t,2π) on [0,r] and σ4(t)=(0,2π−t) on [0,2π]. Composing with φr and using cos⁡0=cos⁡2π=1, sin⁡0=sin⁡2π=0 from [L3] and [L5]: φr∘σ1(t)=p+t a, φr∘σ2(t)=Cr(t), φr∘σ3(t)=p+(r−t)a and φr∘σ4(t)=p. The third is the reversal of the first in the sense of [F6], so [L10] makes their integrals cancel; the fourth is constant, so its derivative extension is 0 and its integral is 0 by [F6]. Hence the circulation of F around the induced boundary chain of (Dr,φr) is ∫CrF⋅dr.

8.1step 5.1step 6.1step 7.1F1L9L11

By step 6.1 the pair (Dr,φr) satisfies the hypotheses of [L11], and F is C1 on the open O containing φr[Dr]. So [L11] and step 7.1 give ∫CrF⋅dr=∫Dr⟨(curl⁡F)∘φr, φr,ρ×φr,θ⟩=∫Drρ gr,gr(ρ,θ):=⟨(curl⁡F)(φr(ρ,θ)),n⟩, using step 5.1 and the bilinearity of the inner product in [F1]; the integrand is continuous on the compact Jordan Dr, hence integrable by [L9].

9.1step 1.4step 4.1step 6.1step 7.1step 8.1F7L8discharge-construct: the polar patch∎

Let ε>0 be real. The field curl⁡F is continuous on O and ⟨⋅,n⟩ is continuous, so [F7] gives δ0>0 such that ∣⟨curl⁡F(q),n⟩−⟨curl⁡F(p),n⟩∣≤ε for every q∈O with ∥q−p∥2<δ0; put δ:=δ0. Let 0<r≤r0 with r<δ. Every point of φr[Dr] is within r<δ0 of p by step 6.1, so ∣gr−⟨curl⁡F(p),n⟩∣≤ε on Dr; hence by [L8] and step 1.4 ∣∫Drρ gr−⟨curl⁡F(p),n⟩ πr2∣=∣∫Drρ(gr−⟨curl⁡F(p),n⟩)∣≤ε∫Drρ=ε πr2. Dividing by πr2>0 and substituting step 8.1 gives ∣1πr2∫CrF⋅dr−⟨curl⁡F(p),n⟩∣≤ε, which by [F7] is the asserted limit; with steps 4.1, 6.1 and 7.1 every clause of the Statement is established.

Remarks

  • The orthonormal pair is built, not chosen by an extension theorem. Steps 1.1, 2.1 and 3.1 write a and b down from n and one standard basis vector, and step 4.1 fixes the sign of a×b by a computation rather than by replacing b with −b after the fact. No choice principle and no basis-extension theorem is used, which matters because the general extension of an independent set to a basis in this library assumes the Axiom of Choice and would be a disproportionate hypothesis for a statement about R3.

  • The two radial edges are what make the chain a circle. The induced boundary chain of a polar patch has four arcs, and only one of them is the circle: the two radial ones are reverses of each other and the fourth is the constant path at the centre. That is why a disc-shaped patch may be used at all, since a closed disc is not an elementary Green region and cannot be a parameter region here.

  • No area comparison between the disc and its diameter is needed. The factor πr2 appears on both sides of the estimate in step 9.1 and cancels; what drives the limit is the continuity of curl⁡F at p alone.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

129 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