ExampleConstruction: AI-adaptedVerification: 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.

Axis field of the declared ideal circular thin loop

Physical scope

An explicit ideal-model computation: the axis field of a declared ideal circular thin loop. It involves no apparatus, no sampling, no uncertainty and no empirical claim, and it is explicitly not the field of any physical finite-radius coil.

Example

Assume Countable Choice ( ${A C}_{ω}$ ), with the exact meaning of The Axiom of Countable Choice ( ${A C}_{ω}$ ). Let $a > 0$ , $I \in R$ , let $γ (s) = a (\cos (s / a), \sin (s / a), 0)$ , $s \in [0, 2 π a]$ , be the circle of radius $a$ in the plane $x_{3} = 0$ parametrized by arc length, let the declared ideal thin-loop current of amplitude $I$ run along $γ$ in the sense of The steady-current (magnetostatic) regime, the compact smooth current class and the declared ideal noncompact models(c1), with moment $m = I π a^{2} e_{3}$ (The magnetic dipole moment of a compact conserved current and of the declared ideal thin loop(b)), and let $μ_{0}$ , $c$ , $ε_{0}$ be the constants of Framework-local SI units, the vacuum constants and the exact/measured status of their values. Then for every point $x = z e_{3}$ on the axis ( $z \in R$ , $dist (x, γ) = \sqrt{a^{2} + z^{2}} > 0$ ) the field of the ideal loop is the absolutely convergent line integral $B (z e_{3}) = \frac{μ_{0} I}{4 π} \int_{0}^{2 π a} \frac{γ^{'} (s) \times (z e_{3} - γ (s))}{∣ z e_{3} - γ (s) ∣^{3}} d s = \frac{μ_{0} I a^{2}}{2 (a^{2} + z^{2})^{3 / 2}} e_{3},$ i.e. the Biot-Savart field of Biot-Savart representation for a compact smooth conserved current and its declared thin-loop limit and the declared thin-current limit of Thin closed current: divergence-free distribution and convergence of its mollified Biot-Savart fields agree on the axis, with the sign fixed by the positive (counterclockwise) orientation of $γ$ and by the sign of $I$ ; in particular $B (0) = \frac{μ_{0} I}{2 a} e_{3}$ . This is a property of the declared idealisation; it is not the field of any physical finite-radius coil, nothing is claimed at points off the axis or on the wire, and no measurement is involved. The explicit finite Riemann axis evaluation and circle moment calculation alone are choice-free. Countable Choice is inherited by the asserted global distributional model and thin-current supplier.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ ; let $a > 0$ , $I \in R$ and the circle $γ (s) = a (\cos (s / a), \sin (s / a), 0)$ with $s \in [0, 2 π a]$ ; let the ideal loop model be the declared one of The steady-current (magnetostatic) regime, the compact smooth current class and the declared ideal noncompact models(c1) with physical adoption Physical adoption of the declared ideal magnetostatic loop, line and cylindrical-sheet models.

[F1]

The field of the declared ideal thin loop is $B_{γ} (x) = \frac{μ_{0} I}{4 π} \int_{0}^{L} \frac{γ^{'} (s) \times (x - γ (s))}{∣ x - γ (s) ∣^{3}} d s$ for $x$ off the curve: this is the Biot-Savart representation of the compact smooth class together with its declared thin-loop limit, and the ideal loop's admissibility is supplied by the strengthened thin-current supplier together with the declared adoption (Biot-Savart representation for a compact smooth conserved current and its declared thin-loop limit, Thin closed current: divergence-free distribution and convergence of its mollified Biot-Savart fields, The steady-current (magnetostatic) regime, the compact smooth current class and the declared ideal noncompact models, Physical adoption of the declared ideal magnetostatic loop, line and cylindrical-sheet models).

[F2]

The moment of clause (b) of the definition is $m = \frac{I}{2} \int_{0}^{L} γ \times γ^{'} d s$ ; for the present circle $γ \times γ^{'} = a e_{3}$ and the integral evaluates to $2 π a^{2} e_{3}$ , so $m = I π a^{2} e_{3}$ (The magnetic dipole moment of a compact conserved current and of the declared ideal thin loop).

[F3]

For $u, v \in R^{3}$ , $u \times v = (u_{2} v_{3} - u_{3} v_{2}, u_{3} v_{1} - u_{1} v_{3}, u_{1} v_{2} - u_{2} v_{1})$ (The cross product in $R^{3}$ ); components of continuous integrands on the compact interval $[0, 2 π a]$ are Riemann integrable (The Riemann integral of a bounded function over a bounded Jordan measurable set, A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

[F4]

${A C}_{ω}$ is the countable-choice principle assumed here and inherited by the asserted global distributional model and thin-current supplier (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F5]

The sine and cosine have derivatives $\cos$ and $- \sin$ , and period $2 π$ (The derivatives of sine and cosine are cosine and minus sine, The zero sets of sine and cosine and the least positive common period 2 pi). The chain rule and FTC integrate their compositions on a compact interval (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ); the substitution $s = a t$ is the $C^{1}$ monotone substitution of Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ .

Verification

technique · direct; identify the axis field with the declared line integral, evaluate the integral by the substitution $t=s/a$, and read off the center value and the moment

1.1givenF1

Every axis point $z e_{3}$ lies at distance $\sqrt{a^{2} + z^{2}} \geq a > 0$ from the circle, so it is off the curve; by [F1] the field of the declared ideal loop there is the absolutely convergent line integral $B (z e_{3}) = \frac{μ_{0} I}{4 π} \int_{0}^{2 π a} \frac{γ^{'} (s) \times (z e_{3} - γ (s))}{∣ z e_{3} - γ (s) ∣^{3}} d s$ , the same integral being the Biot-Savart field of the compact smooth currents in the declared thin-current limit.

1.2givenF3F5

Substituting $t = s / a$ , so that $d s = a d t$ and $γ^{'} (s) = (- \sin t, \cos t, 0)$ while $z e_{3} - γ (s) = (- a \cos t, - a \sin t, z)$ , one has $γ^{'} (s) \times (z e_{3} - γ (s)) = (z \cos t, z \sin t, a)$ by [F3] (the first two components are $z \cos t$ and $z \sin t$ respectively, and the third is $a \cos^{2} t + a \sin^{2} t = a$ ), and $∣ z e_{3} - γ (s) ∣ = (a^{2} + z^{2})^{1 / 2}$ is constant. Hence the component integrals are continuous functions of $t$ on the compact interval $[0, 2 π]$ .

2.1step 1.1step 1.2F3F5

By steps 1.1 and 1.2, $B (z e_{3}) = \frac{μ_{0} I}{4 π} \cdot \frac{a}{(a^{2} + z^{2})^{3 / 2}} \int_{0}^{2 π} (z \cos t, z \sin t, a) d t = \frac{μ_{0} I}{4 π} \cdot \frac{2 π a^{2}}{(a^{2} + z^{2})^{3 / 2}} e_{3} = \frac{μ_{0} I a^{2}}{2 (a^{2} + z^{2})^{3 / 2}} e_{3}$ , the first two components vanishing because $\cos$ and $\sin$ have vanishing integral over a full period. At $z = 0$ this gives $B (0) = \frac{μ_{0} I}{2 a} e_{3}$ , and the sign is the product of the orientation sign of $γ$ and the sign of $I$ .

3.1step 2.1F2F4∎

The computation also fixes the source moment: with $γ \times γ^{'} = a e_{3}$ and $\int_{0}^{2 π a} a e_{3} d s = 2 π a^{2} e_{3}$ , clause (b) of [F2] gives $m = I π a^{2} e_{3}$ , the value quoted in the Example. The whole verification is a conditional ideal-model computation on the axis only: nothing is claimed off the axis or on the wire, no apparatus, sampling model, uncertainty or empirical inference is involved, and Countable Choice enters only through the asserted global distributional model and thin-current supplier [F4].

Source notes

Griffiths, Example 5.6, printed pp. 217-218, evaluates the axis field (5.38) $μ_{0} I R^{2} / [2 (R^{2} + z^{2})^{3 / 2}]$ ; Tong, Section 3.2.3 and Section 3.3.1, printed pp. 49-56, gives the thin-wire Biot-Savart integral and the loop far field; Chew, Lecture 5 Section 5.1, printed pp. 49-52, gives the current-element form. The example verifies the declared ideal loop's axis field against those formulas; it is explicitly not a statement about any physical coil.

Axis field of the declared ideal circular thin loop

Example

Facts & Assumptions

Verification

Source notes

Depends on

Dependency tree · 2 levels

Sources