LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-6.1-sol)

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 piecewise constant cylinder field $e_{3} 1_{{ρ < a}}$ : distributional curl on the cylinder

Statement

Assume Countable Choice ( ${A C}_{ω}$ ), with the exact meaning of The Axiom of Countable Choice ( ${A C}_{ω}$ ). Let $a > 0$ , write $x = (x_{1}, x_{2}, x_{3})$ and $ρ = \sqrt{x_{1}^{2} + x_{2}^{2}}$ , let $S : = {x \in R^{3} : ρ = a}$ be the circular cylinder of radius $a$ about the third coordinate axis, with unit normal $e_{ρ} = ρ^{- 1} (x_{1}, x_{2}, 0)$ pointing from the interior region ${ρ < a}$ to the exterior region ${ρ > a}$ , and let $e_{φ} = ρ^{- 1} (- x_{2}, x_{1}, 0)$ and $e_{3} = (0, 0, 1)$ . Let $g : R^{3} \to R^{3}$ be the piecewise constant field $g (x) : = {\begin{cases} e_{3}, & ρ < a, \\ 0, & ρ > a, \end{cases}$ extended arbitrarily on the three-dimensional Lebesgue-null set $S$ , and let $T_{g}$ be its regular distribution (Regular distribution from a locally integrable function, Locally integrable functions embed in distributions). For an $R^{3}$ -valued distribution $T = (T_{1}, T_{2}, T_{3})$ whose components are scalar distributions of Distribution, a scalar test $φ \in C_{c}^{\infty} (R^{3})$ and a vector test $ψ \in C_{c}^{\infty} (R^{3}; R^{3})$ , the pairings used below are the componentwise readings of Distributional derivative: $⟨ div T, φ ⟩ : = - \sum_{i = 1}^{3} ⟨ T_{i}, \partial_{i} φ ⟩, ⟨ curl T, ψ ⟩ : = \sum_{i = 1}^{3} ⟨ T_{i}, (curl ψ)_{i} ⟩ .$ Then for every vector test $ψ$ and every scalar test $φ$ , $⟨ curl T_{g}, ψ ⟩ = \int_{S} e_{φ} \cdot ψ d S, ⟨ div T_{g}, φ ⟩ = 0,$ that is, $curl T_{g} = e_{φ} δ_{S}$ and $div T_{g} = 0$ in the distributional sense of Distributional derivative. The surface integral is that of Surface integration on compact C1 hypersurfaces; since $ψ$ has compact support it equals the integral over any compact cylinder segment containing $supp ψ \cap S$ . Equivalently, with $g_{\pm}$ the one-sided values and the normal $e_{ρ}$ from the minus to the plus side, $g_{+} - g_{-} = - e_{3}$ , $e_{ρ} \times (g_{+} - g_{-}) = e_{φ}$ and $e_{ρ} \cdot (g_{+} - g_{-}) = 0$ . No product of distributions is formed.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ ; let $a > 0$ ; let $ψ \in C_{c}^{\infty} (R^{3}; R^{3})$ and $φ \in C_{c}^{\infty} (R^{3})$ ; let $S$ , $e_{ρ}$ , $e_{φ}$ , $e_{3}$ , $g$ and $T_{g}$ be as in the Statement.

[F1]

$C_{c}^{\infty} (R^{3})$ and its finite componentwise variant $C_{c}^{\infty} (R^{3}; R^{3})$ are the test spaces of Test function space d of an open set: their members are smooth and compactly supported, and every pairing below is against such a test.

[F2]

The regular distribution $T_{h}$ of a locally integrable function acts by $⟨ T_{h}, χ ⟩ = \int h χ$ and depends only on the almost-everywhere class of $h$ ; locally integrable functions embed into distributions (Regular distribution from a locally integrable function, Locally integrable functions embed in distributions).

[F3]

Distributional derivatives act by signed differentiation of the test, $⟨ \partial^{α} u, χ ⟩ = (- 1)^{∣ α ∣} ⟨ u, \partial^{α} χ ⟩$ (Distributional derivative), and a vector distribution is a triple of scalar distributions in $D^{'} (R^{3})$ (Distribution).

[F4]

Under ${A C}_{ω}$ , Tonelli applies to the $σ$ -finite Euclidean Lebesgue products; $λ_{m} \times λ_{n}$ agrees with $λ_{m + n}$ on Borel sets for $m, n \geq 1$ , and every finite subset of $R$ is $λ_{1}$ -null (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}, Every at most countable subset of $R^{n}$ is Lebesgue null; in particular $λ_{1} (Q) = 0$ ).

[F5]

Assuming ${A C}_{ω}$ , Lebesgue measure is finite on every bounded Lebesgue measurable set, so a bounded Borel function on $R^{3}$ is locally integrable (Lebesgue measure is sigma-finite, and every metrically bounded subset of $R^{n}$ has finite outer measure). Lebesgue measure is complete (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume); hence arbitrary finite changes of a measurable function on a null set remain measurable, because each changed preimage differs by a subset of that null set.

[F6]

The cylinder $V = {ρ < a, ∣ x_{3} ∣ < R}$ , $R > a$ , has the finite piecewise $C^{1}$ presentation of Specified finite piecewise C1 boundary presentations given by the two planar disc caps and four lateral faces $X ([j π / 2, (j + 1) π / 2] \times [- R, R])$ , $j = 0, 1, 2, 3$ , where $X (θ, z) = (a \cos θ, a \sin θ, z)$ . Each angular interval lies inside an open interval of length less than $2 π$ , on which $X$ is an injective regular chart of Gram density $a$ . The edge set consists of the four vertical seams and the two rim circles. In a lateral chart these have parameter sets contained in finitely many horizontal or vertical lines, which are planar-null by [F4], so the edges are surface-null; they are null in each planar cap as well, by applying [F4] to the at-most-two-point sections of its rim circle. The actual outward normals are $e_{ρ}$ on the lateral faces and $\pm e_{3}$ on the caps.

[F7]

Under that presentation the divergence theorem of Divergence for finite piecewise C1 presentations holds: for every $C^{1}$ field $F$ on a neighborhood of the compact closure $\overline{V}$ , $\int_{V} div F d λ_{3} = \sum_{j} \int_{S_{j}} F \cdot ν_{j} d S$ , each face counted once off the edge set.

[F8]

For $u = (u_{x}, u_{y}, u_{z})$ and $v = (v_{x}, v_{y}, v_{z})$ one has $u \times v = (u_{y} v_{z} - u_{z} v_{y}, u_{z} v_{x} - u_{x} v_{z}, u_{x} v_{y} - u_{y} v_{x})$ ; in particular $A \times e_{3} = (A_{2}, - A_{1}, 0)$ , $e_{3} \times e_{ρ} = e_{φ}$ , $(ψ \times e_{3}) \cdot e_{ρ} = ψ \cdot e_{φ}$ , $e_{ρ} \times (- e_{3}) = e_{φ}$ and $e_{ρ} \cdot (- e_{3}) = 0$ (The cross product in $R^{3}$ ).

[F9]

On a $C^{1}$ field $F$ the operators are $div F = \partial_{1} F_{1} + \partial_{2} F_{2} + \partial_{3} F_{3}$ and $curl F = (\partial_{2} F_{3} - \partial_{3} F_{2}, \partial_{3} F_{1} - \partial_{1} F_{3}, \partial_{1} F_{2} - \partial_{2} F_{1})$ (Divergence and curl of a $C^{1}$ vector field).

[F10]

The surface integral over a compact Borel face contained in a regular patch of a compactly supported integrand is the chart-defined integral of Surface integration on compact C1 hypersurfaces, and it does not depend on the choice of a larger compact band containing the support of the integrand.

[F11]

${A C}_{ω}$ is the countable-choice principle invoked by the measure, surface and distribution interfaces above (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct; the nullity of the cylinder surface, the divergence theorem on the cylinder, and two coordinate computations

1.1givenF4

The cylinder $S = {x : x_{1}^{2} + x_{2}^{2} = a^{2}}$ is closed, hence Borel. For each $(x_{2}, x_{3}) \in R^{2}$ , its section $S^{(x_{2}, x_{3})} : = {x_{1} \in R : (x_{1}, x_{2}, x_{3}) \in S}$ consists of at most the two values $\pm \sqrt{a^{2} - x_{2}^{2}}$ when $∣ x_{2} ∣ \leq a$ , and is empty otherwise. Each section is $λ_{1}$ -null by [F4]. Tonelli and product-measure agreement [F4] give $λ_{3} (S) = \int_{R^{2}} λ_{1} (S^{(x_{2}, x_{3})}) d λ_{2} = 0$ .

2.1givenF1F2F3F5step 1.1

The bounded Borel function $g_{0} : = e_{3} 1_{{ρ < a}}$ agrees with $g$ off the null set $S$ of step 1.1, so completeness [F5] makes $g$ Lebesgue measurable with the same almost-everywhere class as $g_{0}$ ; by [F5] this class is locally integrable. Hence $T_{g} : = T_{g_{0}}$ is a well-defined distribution by [F2], and for the tests of [F1] the componentwise pairings of [F3] read $⟨ curl T_{g}, ψ ⟩ = \int_{R^{3}} g_{0} \cdot curl ψ d λ_{3}$ and $⟨ div T_{g}, φ ⟩ = - \int_{R^{3}} g_{0} \cdot \nabla φ d λ_{3}$ , where the componentwise sums against the vector tests are the ordinary finite sums of the stated integrals.

3.1givenstep 1.1step 2.1

Choose $R > a$ with $supp ψ \cup supp φ \subset W : = {ρ < R, ∣ x_{3} ∣ < R}$ and put $V : = {ρ < a, ∣ x_{3} ∣ < R}$ . Since $curl ψ$ and $\nabla φ$ are supported in $W$ , and $g_{0}$ equals $e_{3}$ on $V$ , equals $0$ on the open set $W ∖ \overline{V}$ , and the remaining part $W \cap \partial V$ lies in the null set $S$ of step 1.1, the two integrals of step 2.1 reduce to integrals over $V$ : $\int_{R^{3}} g_{0} \cdot curl ψ d λ_{3} = \int_{V} e_{3} \cdot curl ψ d λ_{3}$ and $\int_{R^{3}} g_{0} \cdot \nabla φ d λ_{3} = \int_{V} e_{3} \cdot \nabla φ d λ_{3}$ .

4.1step 2.1step 3.1F6F7F8F9

The field $F_{0} : = φ e_{3}$ is $C^{1}$ on $R^{3}$ , hence on a neighborhood of $\overline{V}$ , and by [F9] its divergence is $div F_{0} = \partial_{3} φ = e_{3} \cdot \nabla φ$ . The divergence theorem [F7] on the presentation [F6] gives $\int_{V} e_{3} \cdot \nabla φ d λ_{3} = \int_{\partial V} φ e_{3} \cdot ν d S$ . On the lateral face $ν = e_{ρ}$ and $e_{3} \cdot e_{ρ} = 0$ by [F8]; on the two disc caps $x_{3} = \pm R$ the test $φ$ vanishes because $supp φ \subset {∣ x_{3} ∣ < R}$ ; hence $\int_{V} e_{3} \cdot \nabla φ d λ_{3} = 0$ . With steps 2.1 and 3.1 this proves $⟨ div T_{g}, φ ⟩ = 0$ for every scalar test.

4.2step 2.1step 3.1F6F7F8F9F10

The field $G_{0} : = ψ \times e_{3}$ is $C^{1}$ on $R^{3}$ , and by [F8] its coordinates are $G_{0} = (ψ_{2}, - ψ_{1}, 0)$ , so by [F9] $div G_{0} = \partial_{1} ψ_{2} - \partial_{2} ψ_{1} = (curl ψ)_{3} = e_{3} \cdot curl ψ$ . The divergence theorem [F7] on the presentation [F6] gives $\int_{V} e_{3} \cdot curl ψ d λ_{3} = \int_{\partial V} G_{0} \cdot ν d S$ . The disc caps carry $ψ = 0$ by the support condition, while on the lateral face $ν = e_{ρ}$ and $G_{0} \cdot e_{ρ} = (ψ \times e_{3}) \cdot e_{ρ} = ψ \cdot e_{φ}$ by [F8]; therefore $\int_{V} e_{3} \cdot curl ψ d λ_{3} = \int_{ρ = a, ∣ x_{3} ∣ < R} e_{φ} \cdot ψ d S$ , and by [F10] the last integral equals $\int_{S} e_{φ} \cdot ψ d S$ because $e_{φ} \cdot ψ$ is compactly supported and vanishes off the compact band ${ρ = a, ∣ x_{3} ∣ \leq R}$ . With steps 2.1 and 3.1 this is $⟨ curl T_{g}, ψ ⟩ = \int_{S} e_{φ} \cdot ψ d S$ for every vector test, which is the claimed identification $curl T_{g} = e_{φ} δ_{S}$ .

5.1step 4.1step 4.2F2F4F8F10F11∎

The one-sided values of $g$ across $S$ are $g_{+} = 0$ and $g_{-} = e_{3}$ , so $g_{+} - g_{-} = - e_{3}$ and, by [F8], $e_{ρ} \times (g_{+} - g_{-}) = e_{ρ} \times (- e_{3}) = e_{φ}$ and $e_{ρ} \cdot (g_{+} - g_{-}) = e_{ρ} \cdot (- e_{3}) = 0$ , which is the stated equivalence. The two distributional identities of steps 4.1 and 4.2 involve only integrals of locally integrable functions against smooth tests, so no product of two distributions is formed anywhere; the only multiplication on $S$ is that of the compactly supported function $e_{φ} \cdot ψ$ with the surface measure of [F10]. Countable Choice is used in step 1.1 through the product-measure and finite-null-set suppliers [F4] and is inherited only through the cited measure, surface and distribution interfaces [F11]; no stronger choice principle occurs.

Source notes

Tong, Section 3.1.2, printed pp. 43-46, and Chew, Lecture 4 Section 4.3.3, printed pp. 46-48, present the current-sheet jump with exactly the pillbox bookkeeping carried out above at the distributional level; Griffiths, Section 5.3.3, printed pp. 226-228, computes the uniform-surface-current and infinite-solenoid fields whose interface content this lemma records as the identity $curl T_{g} = e_{φ} δ_{S}$ . The lemma itself is a pure distributional computation on the declared piecewise constant field and uses no physical assumption.

The piecewise constant cylinder field $e_{3} 1_{{ρ < a}}$ : distributional curl on the cylinder

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources

The piecewise constant cylinder field e31{ρ<a}e3​1{ρ<a}​: distributional curl on the cylinder

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources

The piecewise constant cylinder field $e_{3} 1_{{ρ < a}}$ : distributional curl on the cylinder