Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources

Statement

Assume Countable Choice (The Axiom of Countable Choice (ACω)), as used by the declared polar/surface and change-of-variables suppliers. Let c>0, μ0>0, a>0 and t0<T be constants, let ρ∈C∞(R3×R) and J∈C∞(R3×R;R3) satisfy (H1) ρ(y,v)=J(y,v)=0 whenever ∣y∣>a or v∉[t0,T], and (H2) ∂vρ+div⁡yJ=0 on R3×R. Here and below Ba:={y∈R3:∣y∣<a} and B‾a:={y∈R3:∣y∣≤a} are the open and closed Euclidean balls of radius a about the origin, and S2={n∈R3:∣n∣=1} is the unit sphere. On the open exterior U:={x∈R3:∣x∣>a} define the retarded scalar and vector potentials φ(x,t):=μ0c24π∫R3ρ(y,t−∣x−y∣/c)∣x−y∣ dy,A(x,t):=μ04π∫R3J(y,t−∣x−y∣/c)∣x−y∣ dy, and the fields E:=−∇φ−∂tA, B:=∇×A, where ∇f=(∂1f,∂2f,∂3f), div⁡F=∑j=13∂jFj and ∇×F=(∂2F3−∂3F2,∂3F1−∂1F3,∂1F2−∂2F1) are the spatial operators of The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case and Divergence and curl of a C1 vector field. The fields are defined on U×R using these ordinary derivatives; the conclusions below use r:=∣x∣≥2a. Every displayed spatial integrand is evaluated on B‾a and extended by zero outside it, including at y=x, so no quotient 0/0 is used. All vector-valued integrals are componentwise scalar Lebesgue integrals.

(a) (Fields as retarded integrals.) On the open set {∣x∣>2a} the potentials φ,A are of class C∞ in (x,t), and there E(x,t)=μ04π∫R3[NR2c2ρ(y,t−Rc)+c NRρt(y,t−Rc)−Jt(y,t−Rc)R]dy,B(x,t)=−μ04π∫R3N×[J(y,t−Rc)R2+Jt(y,t−Rc)cR]dy, where R:=∣x−y∣, N:=(x−y)/R, and ρt,Jt are the partial derivatives in the second variable. Moreover, on {∣x∣≥2a}×[t0,T], φ and each component of A coincide with the corresponding solution constructed in the wave Cauchy problem of The three-dimensional wave Cauchy problem: Kirchhoff representation, uniqueness, domain of dependence and compact support for zero Cauchy data at t0 and scalar source h=μ0c2ρ, respectively h=μ0Jk.

(b) (Uniform far-zone expansion.) For n∈S2 and u∈[t0,T] put I(n,u):=∫BaJ(y,u+n⋅y/c) dy and V(n,u):=∂uI(n,u)=∫BaJt(y,u+n⋅y/c) dy. Then ∫Baρt(y,u+n⋅y/c) dy=1c n⋅V(n,u), and there are constants ΓE,ΓB, depending only on a,c,μ0 and on the suprema of ∣ρ∣,∣ρt∣,∣ρtt∣,∣J∣,∣Jt∣,∣Jtt∣ on B‾a×[t0,T], such that for every n∈S2, u∈[t0,T] and r≥2a, with Elead(n,u,r):=μ04πrn×(n×V(n,u)), ∣E(rn,u+rc)−Elead(n,u,r)∣≤ΓEr2,∣B(rn,u+rc)−n×Elead(n,u,r)c∣≤ΓBr2.

(c) (Retarded-time flux limit.) Let S:=μ0−1E×B and let dΩ be the surface measure on S2 (Surface integration on compact C1 hypersurfaces). Then for every u∈[t0,T], lim⁡r→∞∫S2r2 n⋅S(rn,u+rc) dΩ(n)=μ016π2c∫S2∣n×V(n,u)∣2 dΩ(n). This is a limit at fixed retarded time u, not at fixed observation time t; no decay or boundary condition at spatial infinity is assumed beyond the compact spatial support in (H1).

Facts & Assumptions

Given: ACω (The Axiom of Countable Choice (ACω)); constants c>0, μ0>0, a>0, t0<T; sources ρ∈C∞(R3×R), J∈C∞(R3×R;R3) satisfying (H1) and (H2) of the Statement; the retarded potentials and fields of the Statement, with all vector integrals read componentwise. For n∈S2, u∈[t0,T], r≥2a we write x:=rn, t:=u+r/c, R:=∣x−y∣=((r−n⋅y)2+∣y∣2−(n⋅y)2)1/2, N:=(x−y)/R, σ:=n⋅y, vy:=u+σ/c and δy:=(r−σ−R)/c, so that t−R/c=vy+δy; Γρ,Γρt,Γρtt,ΓJ,ΓJt,ΓJtt denote the suprema of ∣ρ∣,∣ρt∣,∣ρtt∣,∣J∣,∣Jt∣,∣Jtt∣ on B‾a×[t0,T], and λ(Ba) the Lebesgue measure of the ball.

[F1]

A measurable h is integrable exactly when ∫∣h∣<+∞, and then the integral is computed from the positive and negative parts or, for complex h=u+iv, as ∫u+i∫v; L1 denotes the integrable class and ∫Ef=∫fχE is the integral over a measurable set. (Integrable real and complex functions, and their integrals, The class L1(μ) of integrable functions, Integral over a measurable subset)

[F2]

The integral is linear, ∣∫f∣≤∫∣f∣, 0≤f≤g measurable implies ∫f≤∫g, ∫cf=c∫f for c≥0, and integrable functions that agree almost everywhere have the same integral. (The Lebesgue integral is linear on L1(μ), The modulus of an integral is bounded by the integral of the modulus, Monotonicity and nonnegative homogeneity of the nonnegative integral, Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree)

[F3]

Under ACω the ball Ba is Lebesgue measurable with 0<λ(Ba)<+∞; every continuous map Rn→Rm is Borel measurable; and sums, scalar multiples and pointwise products of measurable functions are measurable. (Euclidean balls have positive finite Lebesgue measure, Continuous functions on Euclidean spaces are Borel measurable, Arithmetic and lattice operations preserve measurability whenever they are defined)

[F4]

Mean value theorem: if ϕ is continuous on [p,q] and differentiable on (p,q) then ϕ(q)−ϕ(p)=ϕ′(ξ)(q−p) for some ξ∈(p,q). (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∈(a,b) with f(b)−f(a)=f′(c)(b−a))

[F5]

Parameter integrals over a fixed compact measurable set of finite measure: if K⊆Rn is compact, measurable and of finite measure, if a<b, and if the real-valued f and ∂tf are continuous on a neighbourhood of K×[a,b], then t↦∫Kf(x,t) dx is differentiable at every t∈(a,b) with derivative ∫K∂tf(x,t) dx and has the corresponding one-sided relative derivatives at the endpoints of [a,b]; the lemma is stated pointwise in its one real parameter and explicitly asserts nothing for moving parameter sets or for singularities crossing K. Applying it once per parameter direction with its parameter renamed to x1,x2,x3 or t (all other variables held fixed), and iterating on the resulting integrals, yields the corresponding partial derivatives of a parameter integral whose integrand is smooth in all variables on a neighbourhood of the fixed K. (Differentiation under the integral sign over a compact measurable set and over a compact C1 surface)

[F7]

A Ck map has continuous word partial derivatives through order k, and C∞ means this for every k (Ck Euclidean maps and diffeomorphisms). Finite sums, products and composites preserve these classes (Ck Euclidean maps are closed under componentwise algebra and composition). On (0,∞), (qα)′=αqα−1 and real powers agree with rational powers (Continuity and derivatives of positive-base real powers, The exponential definition of real powers agrees with the existing rational powers); iterating this rule makes q=q1/2 and 1/q smooth there. Closed bounded Euclidean sets are compact, continuous functions on compact sets are uniformly continuous and attain finite extrema (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F8]

Zero-data wave Cauchy problem of speed c from time t0 with source h∈C∞(R3×[t0,T]) in the extension sense: its solution is u(x,t)=c2∫t0t(t−v)Mc(t−v)h(⋅,v)(x) dv on R3×[t0,T], it is C∞ there, and it satisfies c−2∂t2u−Δu=h; here Mrh(x,v)=14π∫S2h(x+rn,v) dΩ(n). (The three-dimensional wave Cauchy problem: Kirchhoff representation, uniqueness, domain of dependence and compact support)

[F9]

Polar-coordinates formula: for every nonnegative Borel f:R3→[0,∞], ∫R3f(y) dy=∫0∞∫S2f(rω)r2 dσ(ω) dr; here σ is the polar surface measure of the cited formula, which equals the chart surface measure dΩ of [F13] (Agreement with the existing polar sphere measure), so the two symbols are used interchangeably; a signed or complex f is handled by applying the formula to positive and negative parts and subtracting. (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, Agreement with the existing polar sphere measure)

[F10]

One-dimensional L1 change of variables: for a C1 diffeomorphism T:U→V of open subsets of R and f∈L1(V), ∫Vf=∫Uf∘T ∣T′∣. (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions)

[F11]

Divergence theorem for a bounded C1 Euclidean domain Ω and F∈C1(Ω‾;Rn): ∫Ωdiv⁡F dx=∫∂ΩF⋅ν dS, with the outward normal. (Divergence on a bounded C1 Euclidean domain)

[F12]

The Euclidean norm satisfies the triangle and Cauchy-Schwarz inequalities (Cauchy-Schwarz ∣⟨x,y⟩∣≤∥x∥2∥y∥2 with its equality case, the triangle inequality for ∥⋅∥2, the parallelogram law and polarisation). Cross product and inner product on R3: u×v is bilinear and antisymmetric, n⋅(u×v)=det⁡(n,u,v), and for ∣n∣=1 the identities n⋅(n×w)=0 and n×(n×w)=n(n⋅w)−w hold, so ∣n×(n×w)∣=∣n×w∣. (The cross product in R3, The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn)

[F13]

Surface integral on the compact embedded C1 hypersurface S2: for a nonnegative Borel f the integral ∫S2f dΩ is defined by finitely many regular parametrizations and an ambient partition of unity, the empty surface integrates to 0, the definition is independent of the chosen presentation, the total surface measure ∫S21 dΩ is finite, and the integral is monotone in f; the definition carries the ACω convention already declared. (Surface integration on compact C1 hypersurfaces)

[F14]

C1 change of variables for nonnegative Borel functions: under ACω, for a C1 diffeomorphism T:U→V of open subsets of Rm and every nonnegative Borel h:V→[0,∞], ∫Vh(y) dy=∫Uh(T(z))∣det⁡DT(z)∣ dz with equality in [0,∞]; in particular the translation T(z)=x+z of R3 is a C1 diffeomorphism with det⁡DT=1, and a signed integrand is handled through its positive and negative parts by linearity. (Borel change of variables from the compact-support formula and Radon uniqueness, The Lebesgue integral is linear on L1(μ))

Proof

technique · direct; part (a) differentiates the retarded integrals and identifies them with the wave Cauchy solution, part (b) expands the field integrals uniformly in the far zone and derives the continuity identity, part (c) passes to the surface integral
1.1F5F6F7F3

Smoothness of the potentials: for x∈U and y∈B‾a one has R=∣x−y∣≥∣x∣−a>0, so the maps (x,t,y)↦ρ(y,t−R/c)/R and (x,t,y)↦J(y,t−R/c)/R are C∞ on a neighbourhood of U×R×B‾a by [F6] and [F7]. Apply [F5] to the fixed compact set K=B‾a once for each parameter direction with its one real parameter renamed to x1, x2, x3 and t (the remaining variables held fixed) and iterate on the resulting integrals: every differentiated integrand is again continuous on a neighbourhood of K, so each application is covered by the lemma and φ and each component of A have continuous partial derivatives of every order on U×R, these differentiated parameter integrals are jointly continuous: on each compact parameter neighbourhood the continuous differentiated integrands are uniformly continuous on its product with K, so the integral of their difference is bounded by λ(K) times their uniformly vanishing difference [F2]. Hence the potentials are C∞ on U×R by [F7], so the derivatives defining the fields are ordinary derivatives even at ∣x∣=2a.

1.2F12F1

Elementary estimates in the far zone: for y∈Ba, r≥2a and n∈S2, expanding R2=(r−σ)2+∣y∣2−σ2 with σ=n⋅y gives ∣R−(r−σ)∣=∣∣y∣2−σ2∣/(R+r−σ)≤a2/r because R+r−σ≥r−σ+∣r−σ∣≥r; consequently ∣r−R∣≤a+a2/r, ∣N−n∣=∣(r−R)n−y∣/R≤(a+a2/r+a)/(r−a)≤5a/r, ∣1/R−1/r∣≤(a+a2/r)/(r(r−a))≤3a/r2, and ∣δy∣≤a2/(rc), all uniformly in y,n.

2.1step 1.1F5F6F12

Field formulas: by [F6], ∇xR=N, ∇x(t−R/c)=−N/c and ∇x×[J(y,t−R/c)]=−N×Jt(y,t−R/c)/c, while ∇x(1/R)=−N/R2; hence ∇x[ρ(y,t−R/c)/R]=−N[ρ/R2+ρt/(cR)] and ∇x×[J(y,t−R/c)/R]=−N×[J/R2+Jt/(cR)]. Each of these first derivatives of the integrands is continuous on a neighbourhood of B‾a, so by [F5] the derivatives may be taken under the integral: −∇φ−∂tA and ∇×A are given on U, in particular for ∣x∣≥2a, by the two displayed zero-extended integrals of the statement, since E=−∇φ−∂tA and B=∇×A.

2.2step 1.1F9F14F1F3

Polar-coordinates identity: fix x∈U and t∈R, and let h be either ρ or one component Jk; then y↦h(y,t−∣x−y∣/c)/∣x−y∣ vanishes off B‾a and ∣x−y∣≥∣x∣−a>0 there, so the quotient on B‾a, extended by zero elsewhere, defines a bounded compactly supported Borel function f on all of R3. The translation T(z):=x+z is a C1 diffeomorphism of R3 with det⁡DT=1, so [F14] applied to the positive and negative parts of f gives ∫R3f(y) dy=∫R3f(x+z) dz; applying [F9] to the positive and negative parts of z↦f(x+z), which at z=ρω equals h(x+ρω,t−ρ/c)/ρ and therefore has inner angular integral 1ρ∫S2h(x+ρn,t−ρ/c) dΩ(n)=4πρMρh(x,t−ρ/c), gives 14π∫R3h(y,t−∣x−y∣/c)∣x−y∣dy=∫0∞r Mrh(x,t−r/c) dr with Mrh(x,v)=14π∫S2h(x+rn,v) dΩ(n), because the inner angular integral is 4πMrh and the radial factor is r2/r=r.

2.3step 1.2F11F6F2

Continuity identity: fix n,u and let ρ0>a; the map F(y):=J(y,u+n⋅y/c) is C1 on B‾ρ0, and [F6] gives div⁡F(y)=div⁡yJ(y,vy)+nc⋅Jt(y,vy) with vy=u+n⋅y/c. By [F11] on Bρ0, whose boundary flux vanishes because J=0 for ∣y∣>a, ∫Bρ0div⁡F dy=0; substituting the chain-rule expression and using (H2), 0=∫Bρ0[−ρt(y,vy)+1cn⋅Jt(y,vy)]dy. The integrands vanish for ∣y∣>a by (H1), so [F2] lets the integrals be taken over Ba; the second is 1cn⋅V(n,u) by the definition of V, whence ∫Baρt(y,vy) dy=1cn⋅V(n,u).

3.1step 2.2F10F8F1

Identification with the Cauchy solution: fix x∈U. For t>t0 the radial integrand of step 2.2 vanishes when r>c(t−t0), because then its source time is less than t0. Apply [F10] to the affine diffeomorphism v↦c(t−v) from (t0,t) onto (0,c(t−t0)), with absolute derivative c; the integrand is bounded on this finite interval, hence integrable. Endpoint values do not affect the Lebesgue integrals, and this gives ∫0∞rMrh(x,t−r/c) dr=c2∫t0t(t−v)Mc(t−v)h(x,v) dv. At t=t0 both sides are zero by (H1), so the identity holds throughout [t0,T]. Multiplying it by μ0c2 for h=ρ, and by μ0 for h=Jk, identifies φ and Ak respectively with the zero-data Cauchy solutions of [F8] with sources μ0c2ρ and μ0Jk. This holds on U×[t0,T] and in particular at ∣x∣=2a.

3.2step 1.2step 2.3F2F3F4F12

Uniform error estimates: fix n,u,r, let ret denote the argument vy+δy and 0 the argument vy, and write Ftot:=c2Nρret/R2+cNρt,ret/R−Jt,ret/R and Flead:=1r(c n ρt,0−Jt,0), so that the field formula of step 2.1 and the definition of V give E(rn,u+r/c)−Elead(n,u,r)=μ04π∫Ba(Ftot−Flead) dy by the linearity of the integral. Every source factor is bounded by its supremum on B‾a×[t0,T], and (H1) makes ρ and J vanish on the open set R3×((−∞,t0)∪(T,∞)), hence makes all their partial derivatives vanish there too, so these suprema also dominate the retarded arguments vy+δy; the mean value theorem [F4] gives ∣ρt,ret−ρt,0∣≤Γρtt∣δy∣ and ∣Jt,ret−Jt,0∣≤ΓJtt∣δy∣: when the difference is nonzero, apply [F4] to its scalar projection onto the unit direction of that difference, and use Cauchy-Schwarz from [F12], and using R−1≤2/r, R−2≤4/r2 and ∣N/R−n/r∣≤∣N−n∣/R+∣1/R−1/r∣≤13a/r2 yields ∣Ftot−Flead∣≤ΓE′/r2, with ΓE′:=4c2Γρ+13caΓρt+a2Γρtt+3aΓJt+a2ΓJtt/c for all r≥2a; hence, by the triangle inequality for the integral and the finiteness of λ(Ba), ∣E(rn,u+r/c)−Elead(n,u,r)∣≤ΓE/r2 with ΓE:=μ04πΓE′λ(Ba). The same computation applied to B(rn,u+r/c)=−μ04π∫BaN×[Jret/R2+Jt,ret/(cR)]dy and to n×Elead/c=−μ04π∫Ba1crn×Jt,0 dy gives ∣B(rn,u+r/c)−n×Elead(n,u,r)/c∣≤ΓB/r2, for ΓB:=μ0λ(Ba)4π(4ΓJ+13aΓJt/c+a2ΓJtt/c2).

4.1step 3.2F5F6F7F12

Smoothness of the far-zone moments: the map (n,u)↦I(n,u)=∫BaJ(y,u+n⋅y/c) dy and its partial derivative ∂uI=∫BaJt(y,u+n⋅y/c) dy=V(n,u) are C∞ in (n,u)∈R3×R: apply [F5] repeatedly in the directions n1,n2,n3,u with the fixed compact set B‾a, each differentiated integrand again being continuous on a neighbourhood of B‾a; the integrals over Ba and B‾a agree because the smooth sources and all their derivatives vanish on ∣y∣=a by continuity from ∣y∣>a. In particular n↦∣n×V(n,u)∣2 is continuous for each fixed u.

4.2step 3.2F12F2

Pointwise flux asymptotics: by step 3.2 write E=Elead+ρE and B=n×Elead/c+ρB at (rn,u+r/c) with ∣ρE∣≤ΓE/r2, ∣ρB∣≤ΓB/r2; then n⋅Elead=0 and Elead×(n×Elead)=∣Elead∣2n by [F12], while ∣Elead∣=μ04πr∣n×V(n,u)∣ because ∣n×(n×V)∣=∣n×V∣. Expanding the cross product bilinearly, the error terms are O(r−3), so r2n⋅S(rn,u+r/c)=μ016π2c∣n×V(n,u)∣2+R(n,u,r) with ∣R(n,u,r)∣≤C/r for a constant C depending only on a,c,μ0 and the source suprema, uniformly in n∈S2 and u∈[t0,T].

5.1step 4.2step 4.1F13F2∎

Flux limit: by [F13] the surface integral over the compact sphere of a bounded Borel function is finite and monotone, so for every u∈[t0,T] and r≥2a the difference ∫S2r2n⋅S(rn,u+r/c) dΩ(n)−μ016π2c∫S2∣n×V(n,u)∣2 dΩ(n)=∫S2R(n,u,r) dΩ(n) has absolute value at most Cr∫S21 dΩ, which tends to 0; the function n↦∣n×V(n,u)∣2 is continuous by step 4.1, so its surface integral is the displayed finite constant. Hence the stated limit at fixed retarded time u follows; no step compares different values of u, so the limit is asserted only at fixed retarded time.

Depends on

Dependency tree · 2 levels

Sources