Physics theoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Controlled electric-dipole far field and retarded-time radiated power of a compact smooth source

Physical scope

Far-zone electric-dipole radiation of a prescribed smooth conserved source of compact spatial support and compact time support: the dipole moment identities, the explicit absolute dipole-replacement error $D (u)$ , the uniform leading far fields and the retarded-time radiated power with its absolute error. Excluded: point charges; sources without the compact smooth branch; claims that slowness alone controls $D (u)$ ; observation-time power and signal-speed readings; self-force, radiation reaction and every empirical or measurement claim.

Statement

Assume the setting and hypotheses of Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources and ${A C}_{ω}$ as carried by its suppliers: $c > 0$ , $μ_{0} > 0$ , $a > 0$ , $t_{0} < T$ , jointly $C^{\infty}$ fields $ρ, J$ vanishing outside ${\overline{B}}_{a} (0) \times [t_{0}, T]$ and satisfying $\partial_{t} ρ + div J = 0$ ; let $φ, A$ be the retarded potentials and $E : = - \nabla φ - \partial_{t} A$ , $B : = \nabla \times A$ the fields, with $S : = E \times B / μ_{0}$ (Vacuum electromagnetic energy density and energy flux (the Poynting vector), Local and fixed-volume electromagnetic energy balance). Adopt the causal selection Adopted retarded solution selection: the physical branch carries no incoming free field: these retarded fields are the fields of the source model (the compact smooth instance established by Retarded potentials, Lorenz gauge and Maxwell fields of a compactly supported conserved smooth source). Define the time-dependent electric dipole moment

$p (u) : = \int_{B_{a}} y ρ (y, u) d y \in R^{3}$

(componentwise, about the fixed chart origin of Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields; it is the fixed-time analogue of the static source moment of Total charge, dipole moment, Cartesian moments and traceless quadrupole of a static charge distribution), and, as in the asymptotic theorem, $I (n, u) : = \int_{B_{a}} J (y, u + n \cdot y / c) d y$ , $V (n, u) : = \partial_{u} I (n, u) = \int_{B_{a}} J_{t} (y, u + n \cdot y / c) d y$ and

$D (u) : = \frac{a}{c} \int_{B_{a}} \sup_{∣ v - u ∣ \leq a / c} ∣ J_{t t} (y, v) ∣ d y .$

Then:

(a) [Moment identities] $p \in C^{\infty} (R; R^{3})$ , $p^{'} (u) = \int_{B_{a}} J (y, u) d y$ , $p^{''} (u) = \int_{B_{a}} J_{t} (y, u) d y$ , $\int_{B_{a}} ρ_{t} (y, u) d y = 0$ and the total charge $\int_{B_{a}} ρ (y, u) d y$ vanishes for every $u$ .

(b) [Dipole replacement error] $∣ V (n, u) - p^{''} (u) ∣ \leq D (u)$ for every $n \in S^{2}$ and every $u \in [t_{0}, T]$ : the explicit absolute error of the dipole approximation to the source's transverse current moment.

(c) [Leading fields] With $Γ_{E}$ , $Γ_{B}$ the constants of Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources(b) (depending only on $a, c, μ_{0}$ and the listed source suprema), for every $n \in S^{2}$ , $u \in [t_{0}, T]$ , $r \geq 2 a$ :

$∣ E (r n, u + \frac{r}{c}) - \frac{μ_{0}}{4 π r} n \times (n \times p^{''} (u)) ∣ \leq \frac{Γ_{E}}{r^{2}} + \frac{μ_{0} D (u)}{4 π r}, ∣ B (r n, u + \frac{r}{c}) - \frac{n \times E (r n, u + \frac{r}{c})}{c} ∣ \leq \frac{Γ_{B} + Γ_{E} / c}{r^{2}} .$

The displayed dipole field approximates the actual leading far field $E_{l e a d} = μ_{0} n \times (n \times V) / (4 π r)$ with the stated absolute $D (u) / r$ error. Equality of these leading fields requires $n \times (n \times (V - p^{''})) = 0$ ; $V = p^{''}$ and, in particular, $D (u) = 0$ are sufficient. All errors are uniform in $n$ at fixed $u$ .

(d) [Retarded-time radiated power] The limit of Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources(c) equals $μ_{0} ∣ p^{''} (u) ∣^{2} / (6 π c) + R (u)$ with the explicit absolute error

$∣ R (u) ∣ \leq \frac{μ_{0} (2 ∣ p^{''} (u) ∣ D (u) + D (u)^{2})}{4 π c}, so \lim_{r \to \infty} \int_{S^{2}} r^{2} n \cdot S (r n, u + \frac{r}{c}) d σ = \frac{μ_{0}}{6 π c} ∣ p^{''} (u) ∣^{2} whenever D (u) = 0.$

The evaluation uses the sphere moment $\int_{S^{2}} ∣ n \times p^{''} ∣^{2} d σ = (8 π / 3) ∣ p^{''} ∣^{2}$ of Zonal and quadratic sphere moments for the polar surface measure on $S^{2}$ (d). The limit is at fixed retarded time $u$ , not at fixed observation time.

(e) [Scope] The compact smooth source branch only; the dipole error is absolute and explicitly controlled by $D (u)$ , and no assertion is made that slow or 'nonrelativistic' source motion alone makes $D (u)$ small -- that is a hypothesis on the source's time variation. No point charge, no moving point source, no radiation reaction, no self-force and no empirical or measurement content; the failure of the correspondence with an oscillator for rapidly varying sources is retained through $D (u)$ . Separately retain the sharper actual source estimate $∣ B (r n, u + r / c) - n \times E_{l e a d} (n, u, r) / c ∣ \leq Γ_{B} / r^{2}$ , with $E_{l e a d} = μ_{0} n \times (n \times V) / (4 π r)$ ; the bound against the actual E uses the combined constant displayed in (c).

Facts & Assumptions

Given: ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )); the hypotheses of Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources: constants $c > 0$ , $μ_{0} > 0$ , $a > 0$ , $t_{0} < T$ , jointly $C^{\infty}$ sources $(ρ, J)$ vanishing outside ${\overline{B}}_{a} (0) \times [t_{0}, T]$ and satisfying $\partial_{t} ρ + div J = 0$ ; the retarded potentials and fields with $S = E \times B / μ_{0}$ ; the dipole moment $p$ , the moments $I, V$ and the error coefficient $D$ of the Statement.

[F1]

Far-zone expansion of Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources (b): with $I (n, u) = \int_{B_{a}} J (y, u + n \cdot y / c) d y$ , $V = \partial_{u} I$ , $E_{l e a d} (n, u, r) = \frac{μ_{0}}{4 π r} n \times (n \times V (n, u))$ and $Γ_{E}, Γ_{B}$ constants depending only on $a, c, μ_{0}$ and the source suprema, for all $n \in S^{2}$ , $u \in [t_{0}, T]$ , $r \geq 2 a$ one has $∣ E (r n, u + r / c) - E_{l e a d} (n, u, r) ∣ \leq Γ_{E} / r^{2}$ and $∣ B (r n, u + r / c) - n \times E_{l e a d} (n, u, r) / c ∣ \leq Γ_{B} / r^{2}$ . (Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources (b))

[F2]

Retarded-time flux limit of Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources (c): for every $u \in [t_{0}, T]$ , $\lim_{r \to \infty} \int_{S^{2}} r^{2} n \cdot S (r n, u + \frac{r}{c}) d Ω (n) = \frac{μ_{0}}{16 π^{2} c} \int_{S^{2}} ∣ n \times V (n, u) ∣^{2} d Ω (n)$ , a limit at fixed retarded time; $d Ω$ is the sphere surface measure, which equals the polar measure $σ$ on $S^{2}$ . (Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources (c))

[F3]

Energy flux reading: $S = E \times B / μ_{0}$ is the Poynting energy-flux density of Vacuum electromagnetic energy density and energy flux (the Poynting vector), and the fixed-volume Poynting balance of Local and fixed-volume electromagnetic energy balance contains $- \oint S \cdot n d S$ , the negative of the outward field-energy flux, in the field-energy rate. (Vacuum electromagnetic energy density and energy flux (the Poynting vector), Local and fixed-volume electromagnetic energy balance)

[F4]

Source moments: the static dipole moment and total charge of a compactly supported charge distribution about the chart origin are those of Total charge, dipole moment, Cartesian moments and traceless quadrupole of a static charge distribution(a); the present $p (u)$ is the fixed-time analogue for the moving source. (Total charge, dipole moment, Cartesian moments and traceless quadrupole of a static charge distribution)

[F5]

Parameter integrals over a fixed compact set: if $f, \partial_{t} f$ are continuous on a neighbourhood of $K \times J$ with $K$ compact measurable of finite measure, then $t \mapsto \int_{K} f$ is differentiable with derivative $\int_{K} \partial_{t} f$ ; iterating gives $C^{\infty}$ dependence for $C^{\infty}$ integrands. (Differentiation under the integral sign over a compact measurable set and over a compact $C^{1}$ surface)

[F6]

Divergence theorem on a bounded $C^{1}$ domain: $\int_{Ω} div F = \int_{\partial Ω} F \cdot ν d S$ for $F \in C^{1} (\overline{Ω}; R^{3})$ . (Divergence on a bounded C1 Euclidean domain)

[F7]

Mean value theorem: if $f : [s_{1}, s_{2}] \to R$ is continuous and differentiable in the interior, then $f (s_{2}) - f (s_{1}) = f^{'} (s_{*}) (s_{2} - s_{1})$ for some interior $s_{*}$ . (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ )

[F8]

Cauchy-Schwarz: $∣ e \cdot w ∣ \leq ∣ e ∣ ∣ w ∣$ for $e, w \in R^{3}$ . (The Cauchy-Schwarz inequality for finite sums, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ )

[F9]

Integral triangle inequality and monotonicity: $∣ \int f ∣ \leq \int ∣ f ∣$ for integrable $f$ , and $0 \leq f \leq g$ gives $\int f \leq \int g$ for the nonnegative integral. (The modulus of an integral is bounded by the integral of the modulus, Monotonicity and nonnegative homogeneity of the nonnegative integral)

[F10]

Cross product identities: $u \times v$ is bilinear and alternating, $n \cdot (u \times v) = \det (n, u, v)$ , and for $∣ n ∣ = 1$ one has $n \cdot (n \times w) = 0$ , $n \times (n \times w) = n (n \cdot w) - w$ , $∣ n \times (n \times w) ∣ = ∣ n \times w ∣ \leq ∣ w ∣$ ; and for $a_{⊥} : = a - (n \cdot a) n$ one has $a \cdot b - (n \cdot a) (n \cdot b) = a_{⊥} \cdot b_{⊥}$ . (The cross product is bilinear, alternating, and orthogonal to both factors, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ )

[F11]

Shifted source moments: $V (n, u) = \int_{B_{a}} J_{t} (y, u + n \cdot y / c) d y = \partial_{u} I (n, u)$ . (Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources (a),(b))

[F12]

Sphere moment: $\int_{S^{2}} ∣ n \times a ∣^{2} d σ (n) = \frac{8 π}{3} ∣ a ∣^{2}$ for every $a \in R^{3}$ , and $σ (S^{2}) = 4 π$ . (Zonal and quadratic sphere moments for the polar surface measure on $S^{2}$ (d))

[F13]

Compact smooth branch: for the same source class the retarded fields satisfy the smooth vacuum Maxwell equations and the total charge vanishes: $\int_{B_{a}} ρ (y, u) d y = 0$ for every $u$ , and the retarded pair is the adopted selected branch. (Retarded potentials, Lorenz gauge and Maxwell fields of a compactly supported conserved smooth source (b),(f), Adopted retarded solution selection: the physical branch carries no incoming free field)

[F14]

Source support and regularity conventions: $(ρ, J)$ are the smooth source fields of Charge parameter, frame charge and current densities, volume charge and flux, and the four-current, with the support hypothesis of the Given. (Charge parameter, frame charge and current densities, volume charge and flux, and the four-current)

[F15]

A continuous function on a nonempty compact set attains finite extrema and is uniformly continuous. (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous)

Proof

technique · direct; obtain the moment identities by differentiating the dipole integral and integrating the continuity equation by parts, bound the moment replacement by the mean value theorem, transfer the far-zone expansion of [F1] to the dipole fields, and evaluate the flux limit of [F2] using the exact sphere moment [F12] and the pointwise replacement bound

1.1F4F5F6F9F13F14algebra

Moment identities (a). The moment $p (u) = \int_{B_{a}} y ρ (y, u) d y$ is the fixed-time analogue of the static source moment of [F4], a convention about which moment is computed and not a dynamical identity. Since $ρ$ is jointly $C^{\infty}$ and supported in the fixed compact set ${\overline{B}}_{a} (0) \times [t_{0}, T]$ , repeated application of [F5] to $u \mapsto p (u)$ shows $p \in C^{\infty}$ with $p^{'} (u) = \int_{B_{a}} y ρ_{t} (y, u) d y$ and $p^{''} (u) = \int_{B_{a}} y ρ_{t t} (y, u) d y$ [F14]. For the first derivative, fix $u$ and $R > a$ : the continuity equation gives $\int_{B_{a}} y_{i} ρ_{t} (y, u) d y = - \int_{B_{a}} y_{i} div J (y, u) d y$ , and since $div (y_{i} J) = J_{i} + y_{i} div J$ , the divergence theorem [F6] on $B_{R}$ gives $\int_{B_{R}} div (y_{i} J) d y = \int_{\partial B_{R}} y_{i} J \cdot ν d S = 0$ because $J$ vanishes on $\partial B_{R}$ ; hence $\int_{B_{a}} y_{i} div J d y = - \int_{B_{a}} J_{i} d y$ and $p_{i}^{'} (u) = \int_{B_{a}} J_{i} (y, u) d y$ [F9]. Differentiating this identity once more with [F5] gives $p^{''} (u) = \int_{B_{a}} J_{t} (y, u) d y$ , the displayed second moment identity. The same divergence theorem with weight $1$ gives $\int_{B_{a}} ρ_{t} (y, u) d y = - \int_{B_{a}} div J (y, u) d y = 0$ , and the vanishing of the total charge is clause (f) of [F13] for this source class. This is (a).

2.1step 1.1F7F8F9F11F14F15algebra

Dipole replacement error (b). First $D (u)$ is well defined and finite. For fixed $u$ , the function $g_{u} (y) : = \max_{∣ v - u ∣ \leq a / c} ∣ J_{t t} (y, v) ∣$ attains its maximum by [F15]. Moreover $∣ g_{u} (y) - g_{u} (y^{'}) ∣ \leq \sup_{∣ v - u ∣ \leq a / c} ∣ ∣ J_{t t} (y, v) ∣ - ∣ J_{t t} (y^{'}, v) ∣ ∣$ , so uniform continuity on ${\overline{B}}_{a} \times [u - a / c, u + a / c]$ makes $g_{u}$ continuous and bounded on ${\overline{B}}_{a}$ . It is therefore measurable and integrable on the finite-measure ball, giving the claimed finite coefficient; the same estimate after writing $v = u + w$ also makes $D$ continuous on compact time intervals. Fix $n \in S^{2}$ , $u \in [t_{0}, T]$ and $y \in B_{a}$ , and put $s_{1} : = u$ , $s_{2} : = u + n \cdot y / c$ , so $∣ s_{2} - s_{1} ∣ \leq a / c$ ; the map $s \mapsto J_{t} (y, s)$ is $C^{1}$ [F14]. If $Δ : = J_{t} (y, s_{2}) - J_{t} (y, s_{1}) \neq 0$ , apply [F7] on the closed interval between $s_{1}$ and $s_{2}$ to the scalar function $s \mapsto e \cdot J_{t} (y, s)$ with $e : = Δ / ∣ Δ ∣$ : there is $s_{*}$ between $s_{1}$ and $s_{2}$ with $e \cdot Δ = (e \cdot J_{t t} (y, s_{*})) (s_{2} - s_{1})$ ; if $Δ = 0$ the same bound holds trivially. By [F8], $∣ e \cdot J_{t t} (y, s_{*}) ∣ \leq ∣ J_{t t} (y, s_{*}) ∣$ , so $∣ Δ ∣ \leq (a / c) \sup_{∣ v - u ∣ \leq a / c} ∣ J_{t t} (y, v) ∣$ (the point $s_{*}$ lies within $a / c$ of $u$ ). Integrating over $B_{a}$ with the integral triangle inequality and monotonicity [F9], and using $V (n, u) - p^{''} (u) = \int_{B_{a}} [J_{t} (y, u + n \cdot y / c) - J_{t} (y, u)] d y$ from step 1.1 and [F11], gives $∣ V (n, u) - p^{''} (u) ∣ \leq D (u)$ . This is (b).

3.1step 2.1F1F9F10algebra

Leading fields (c). By [F1], for $n \in S^{2}$ , $u \in [t_{0}, T]$ , $r \geq 2 a$ write $E (r n, u + \frac{r}{c}) = E_{l e a d} (n, u, r) + ρ_{E}$ with $∣ ρ_{E} ∣ \leq Γ_{E} / r^{2}$ and $E_{l e a d} = μ_{0} n \times (n \times V (n, u)) / (4 π r)$ . Substituting $V = p^{''} + (V - p^{''})$ and using the identity $∣ n \times (n \times w) ∣ = ∣ n \times w ∣ \leq ∣ w ∣$ of [F10] together with the bound of step 2.1, $∣ E (r n, u + \frac{r}{c}) - \frac{μ_{0}}{4 π r} n \times (n \times p^{''} (u)) ∣ \leq \frac{Γ_{E}}{r^{2}} + \frac{μ_{0}}{4 π r} ∣ V (n, u) - p^{''} (u) ∣ \leq \frac{Γ_{E}}{r^{2}} + \frac{μ_{0} D (u)}{4 π r},$ which is the first displayed bound. For the magnetic field, [F1] gives $∣ B (r n, u + \frac{r}{c}) - n \times E_{l e a d} / c ∣ \leq Γ_{B} / r^{2}$ , and $∣ n \times (E - E_{l e a d}) ∣ / c \leq ∣ E - E_{l e a d} ∣ / c \leq Γ_{E} / (c r^{2})$ by [F10], so the triangle inequality [F9] gives the second displayed bound $(Γ_{B} + Γ_{E} / c) / r^{2}$ ; the sharper source estimate against $n \times E_{l e a d} / c$ is the supplier's own $Γ_{B} / r^{2}$ bound retained in (e). This is (c), uniformly in $n$ at fixed $u$ .

4.1step 2.1F2F3F8F9F10F12algebra∎

Retarded-time radiated power (d). By [F2], the limit of $\int_{S^{2}} r^{2} n \cdot S (r n, u + \frac{r}{c}) d σ$ as $r \to \infty$ equals $\frac{μ_{0}}{16 π^{2} c} \int_{S^{2}} ∣ n \times V (n, u) ∣^{2} d σ$ at fixed $u$ ; here the polar measure and the sphere surface measure coincide, and [F3] identifies the surface flux with the field-energy flux. For the replacement $V \mapsto p^{''}$ put $a_{\pm} : = V \pm p^{''}$ ; by [F10] the pointwise difference satisfies $∣ n \times V ∣^{2} - ∣ n \times p^{''} ∣^{2} = a_{+} \cdot a_{-} - (n \cdot a_{+}) (n \cdot a_{-}) = (a_{+})_{⊥} \cdot (a_{-})_{⊥}$ , so its absolute value is at most $∣ a_{+} ∣ ∣ a_{-} ∣ \leq (∣ V ∣ + ∣ p^{''} ∣) ∣ V - p^{''} ∣ \leq (2 ∣ p^{''} ∣ + D) D = 2 ∣ p^{''} ∣ D + D^{2}$ , using [F8], the bound of step 2.1 and monotonicity of the norm. Since $σ (S^{2}) = 4 π$ [F12], the integral changes by at most $4 π (2 ∣ p^{''} ∣ D + D^{2})$ in absolute value [F9], so the limit equals $\frac{μ_{0}}{16 π^{2} c} \int_{S^{2}} ∣ n \times p^{''} (u) ∣^{2} d σ + R (u)$ with $∣ R (u) ∣ \leq \frac{μ_{0} (2 ∣ p^{''} ∣ D + D^{2})}{4 π c}$ . The exact integral is $\int_{S^{2}} ∣ n \times p^{''} (u) ∣^{2} d σ = \frac{8 π}{3} ∣ p^{''} (u) ∣^{2}$ by [F12], so the exact term is $\frac{μ_{0}}{16 π^{2} c} \cdot \frac{8 π}{3} ∣ p^{''} (u) ∣^{2} = \frac{μ_{0}}{6 π c} ∣ p^{''} (u) ∣^{2}$ ; whenever $D (u) = 0$ the error vanishes by the displayed bound. This is (d). The scope clause (e) is bookkeeping: the limit is at fixed retarded time, the error is controlled by the source's time variation through $D (u)$ alone, and no point source, no observer-time power, no radiation reaction, no self-force and no measurement claim is introduced; the only choice assumption is ${A C}_{ω}$ , inherited from the supplier.

Controlled electric-dipole far field and retarded-time radiated power of a compact smooth source

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources