Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
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 infinite line charge: logarithmic potential, flux normalization and divergent energy

Physical scope

The idealised infinite straight line charge in vacuum: the field λe^r/(2πε0ρ), the logarithmic potential, the zero-volume-source classical equations off the axis, the cylinder flux λL/ε0, the distributional identity div⁡E=ρλ/ε0 on R3, the failure of the infinity normalization and of the star-shaped hypothesis, and the logarithmically divergent energy per unit length. The line source lies outside the declared source types of the framework; the item is a mathematical idealisation with no physical realisation, equilibrium or empirical claim.

Example

Assume the Axiom of Countable Choice (ACω), inherited from the cited Lebesgue, polar, Newtonian and distribution interfaces (The Axiom of Countable Choice (ACω)). Use the one-based coordinate and derivative labels of The localized Newtonian potential and the ideal point-charge Coulomb field: xk:=x(k−1), ∂k is differentiation in that coordinate, and ek is its unit vector, for k=1,2,3. Let Ω:=R3∖{x:x1=x2=0} (the complement of the z-axis), let ρ(x):=x12+x22 and e^r(x):=(x1,x2,0)/ρ(x) for x∈Ω (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn, Open ball, closed ball and sphere in a metric space), let λ∈R be a line charge density in C m−1, let r0>0, and define, with the constants and units of Framework-local SI units, the vacuum constants and the exact/measured status of their values (The electric and magnetic fields as fixed-time spatial vector fields, Charge parameter, frame charge and current densities, volume charge and flux, and the four-current), E(x):=λ e^r(x)2πε0 ρ(x),φ(x):=−λ2πε0log⁡ρ(x)r0(x∈Ω). Then:

(a) [Gradient] E=−∇φ on Ω (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a), Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(c)=f′(c)g(c)+f(c)g′(c), and (f/g)′(c)=(f′(c)g(c)−f(c)g′(c))/g(c)2 when g(c)≠0);

(b) [Classical equations] div⁡E=0 and curl⁡E=0 pointwise on Ω; hence the fixed-time pair (E,0) satisfies the reduced smooth-branch electrostatic equations with zero volume source on Ω (The static and pure electrostatic regimes and their fixed-time reading (c), Divergence and curl of a C1 vector field);

(c) [Flux per length] for every r>0 and L>0 the flux of E through the lateral cylinder surface {x:ρ(x)=r, ∣x3∣≤L/2} in the outward orientation is Φr=λL/ε0; the parametrization (θ,z)↦(rRe⁡eiθ,rIm⁡eiθ,z) over the rectangle [0,2π]×[−L/2,L/2] is an admissible regular surface patch (Regular parametrized surface patches on compact Jordan parameter regions, Unit normal fields, orientations, and flux through a regular surface patch, The complex exponential by its power series, Real and imaginary parts, complex conjugation, and modulus, The complex exponential is entire and its complex derivative is itself, exp⁡(x+iy)=ex(cos⁡y+isin⁡y), ∣exp⁡(x+iy)∣=ex, and eiπ+1=0, The surface area density is the norm of the cross product of the parameter tangents);

(d) [Distributional line source] extend E by 0 on the axis and let ρλ(ψ):=λ∫Rψ(0,0,z) dz be the line-charge distribution on R3 (Distribution, Test function space d of an open set). Then, with distributional derivatives and the regular distribution of E (Regular distribution from a locally integrable function, Locally integrable functions embed in distributions), div⁡E=1ε0ρλ,curl⁡E=0in D′(R3), by superposition of the point-charge identities of The localized Newtonian potential and the ideal point-charge Coulomb field (d) along the axis (Fubini's theorem for L^1 functions on a sigma-finite product); the line density fixed by the field in this weak sense is exactly λ;

(e) [Normalization] for fixed r0, φ(ρ)→−∞ as ρ→∞ if λ>0 and →+∞ if λ<0, while changing r0 to r0′ shifts φ by λ2πε0log⁡(r0′/r0) and leaves E unchanged. For λ≠0 the infinity normalization of The localized Newtonian potential and the ideal point-charge Coulomb field (b) is therefore unavailable; for λ=0 the field, potential and line source are zero and all cutoff energies and fluxes vanish; and Ω is not star-shaped (for every a∈Ω the segment from a to −a passes through the axis, which is not in Ω), so Scalar potential and the Poisson equation in a star-shaped electrostatic region does not apply to Ω, although the displayed φ still satisfies E=−∇φ (Star-shaped open subsets of Euclidean space);

(f) [Energy per length] for 0<δ<r<R and L>0, ε02∫{δ<ρ<R, ∣x3∣<L/2}∣E∣2 dλ3=λ2L4πε0log⁡Rδ, which for λ≠0 diverges both as δ↓0 and as R→∞; there is no finite energy per unit length (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, The polar surface set function on the unit sphere, Agreement with the existing polar sphere measure, The closed form for the volume of the unit n-ball);

(g) [Scope and idealization] the line charge ρλ is not a source type of Distributional Maxwell equations with point and stationary-sheet sources: only point sources and stationary sheets are declared there, and no line current, moving sheet or other distribution is included. The item therefore verifies classical, flux and distributional identities for an explicitly specified distribution ρλ on R3 with a noncompact singularity; it is not a framework postulate covering infinite line charges, asserts no physical realisation, equilibrium or empirical content, and is not a compact-source Coulomb corollary. Real line-like distributions have finite length and transverse size, and their far fields and energies require their own hypotheses.

Facts & Assumptions

Given: The Axiom of Countable Choice, the open set Ω=R3∖{axis}, the transverse radius ρ(x)=x12+x22, the radial unit vector e^r(x)=(x1,x2,0)/ρ(x), real λ and r0>0, and the fields E,φ displayed above.

[F1]

The transverse radius is continuous and positive exactly on Ω, so Ω is open; on it ρ is smooth with ∂iρ=xi/ρ for i=1,2 and ∂3ρ=0 (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, Metric continuity characterisations, with countable choice for the sequential converse, The finite and reverse triangle inequalities for a norm; and for n≥1 every norm N on Rn satisfies N(x)≤C∥x∥1 and is Lipschitz, hence continuous, for d2, Continuity and derivatives of positive-base real powers, For a natural n≥1 the function x↦xn is differentiable everywhere with derivative ι(n) x n−1; for n=0 it is the constant 1, with derivative 0; for a natural n≥1 the function x↦x−n is differentiable at every x≠0 with derivative −ι(n) x−n−1; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a), Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(c)=f′(c)g(c)+f(c)g′(c), and (f/g)′(c)=(f′(c)g(c)−f(c)g′(c))/g(c)2 when g(c)≠0, Directional derivatives and partial derivatives of a map U⊆Rm→Rn, Ck Euclidean maps and diffeomorphisms).

[F3]

The complex exponential is entire with derivative equal to itself, so the real-parameter map θ↦eiθ has derivative ieiθ; its real and imaginary parts and modulus satisfy ∣eiθ∣=1 and Euler's identity (The complex exponential by its power series, The complex exponential is entire and its complex derivative is itself, exp⁡(x+iy)=ex(cos⁡y+isin⁡y), ∣exp⁡(x+iy)∣=ex, and eiπ+1=0, Real and imaginary parts, complex conjugation, and modulus).

[F4]

For a regular patch the outward-oriented flux is the integral of F⋅(φu×φv) over the parameter region; the cross product and its norm are those of the Euclidean structure, and a compact Jordan parameter region D is a compact Jordan measurable set equal to the closure of its nonempty connected interior. It is admissible when the parametrization is C1 on a neighbourhood of D, the cross product is nonzero on D∘, and no point of D∘ shares its image with a distinct point of the whole region D; boundary seam identifications are permitted (Unit normal fields, orientations, and flux through a regular surface patch, Regular parametrized surface patches on compact Jordan parameter regions, The surface area density is the norm of the cross product of the parameter tangents, The cross product in R3, The Riemann integral of a bounded function over a bounded Jordan measurable set, A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included).

[F5]

The polar formula computes integrals in every dimension; the transverse plane is R2 with σ(S1)=2π from ∣Sn−1∣=n∣B1∣ and ∣B1∣=π in dimension two (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, The polar surface set function on the unit sphere, The closed form for the volume of the unit n-ball, Agreement with the existing polar sphere measure).

[F6]

On sigma-finite products, Tonelli equates the product integral and both iterated integrals of every nonnegative product-measurable function, allowing infinite values; Fubini equates the integrals of a complex-valued product-measurable function only after its absolute product integral is finite (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product). For every m,n≥1, the Euclidean Borel sigma-algebra on Rm+n equals the product Borel sigma-algebra, and λm×λn agrees with λm+n on Borel sets (The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}, On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}); each factor is sigma-finite by its exhaustion by finite-measure boxes [F8].

[F7]

Distributions, their derivatives, test functions and the embedding of locally integrable functions are as in the cited interfaces, and the ideal point charge with charge parameter q at x0 has div⁡Eq=(q/ε0)δx0 and curl⁡Eq=0 in D′(R3) (Distribution, Distributional derivative, Test function space d of an open set, Regular distribution from a locally integrable function, Locally integrable functions embed in distributions, The localized Newtonian potential and the ideal point-charge Coulomb field).

[F10]

The z-axis is Lebesgue null: it lies in the coordinate hyperplane x1=0 (A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in Rn).

[F11]

Star-shapedness is defined through segments to a centre, and the potential construction and uniqueness up to a constant of Scalar potential and the Poisson equation in a star-shaped electrostatic region use a star-shaped region; the framework's declared source types are point and stationary-sheet sources of Distributional Maxwell equations with point and stationary-sheet sources (Star-shaped open subsets of Euclidean space, Scalar potential and the Poisson equation in a star-shaped electrostatic region, Distributional Maxwell equations with point and stationary-sheet sources).

Verification

technique · direct
1.1givenF1F5F6F7F9F10

By [F1] Ω is open and ρ is smooth and positive on it with ∂iρ=xi/ρ for i=1,2 and ∂3ρ=0; consequently E is C∞ on Ω and E∈Lloc1(Ω) with ∣E∣=∣λ∣2πε0ρ, since on every bounded set the transverse polar formula gives ∫ρ<Aρ−1 dλ2=2πA and Tonelli on R2×R multiplies this nonnegative transverse integral (with value 0 on the axis) by the finite longitudinal length of the containing cylinder to give a finite λ3-integral ([F1], [F5], [F6]). Extending E by 0 on the axis does not change its Lloc1 class or any regular distribution, because the axis is null ([F10]), and the functional ρλ(ψ)=λ∫Rψ(0,0,z) dz is a distribution: on a compact test support contained in a cylinder ρ≤A, ∣z∣≤H its absolute pairing is at most ∣λ∣ 2H∥ψ∥∞ ([F7], [F9], [F10]).

2.1step 1.1F1F2

Clause (a): the chain rule and the derivative of the logarithm [F1], [F2] give ∇φ=−λ2πε01ρ∇ρ=−λ2πε0ρe^r=−E on Ω, since ∇ρ=(x1,x2,0)/ρ=e^r.

3.1step 2.1F1F2

Clause (b): writing E=(E1,E2,0) with Ei=λxi2πε0ρ2, the quotient rule and ∂iρ=xi/ρ give ∂iEi=λ2πε0ρ2−2xi2ρ4 for i=1,2, so div⁡E=λ2πε02ρ2−2x12−2x22ρ4=0; and curl⁡E has components ∂2E3−∂3E2=0, ∂3E1−∂1E3=0 and ∂1E2−∂2E1=λ2πε0−2x1x2+2x1x2ρ4=0, because E3=0 and E does not depend on x3 ([F1], [F2]). Hence (E,0) satisfies the reduced equations with zero volume source on Ω: the pair is time independent and the reduced smooth-branch equations are exactly div⁡E=0, curl⁡E=0 [F2].

4.1step 3.1F3F4F8

Clause (c): let u(θ)=Re⁡eiθ, v(θ)=Im⁡eiθ, and let Φ(θ,z)=(ru(θ),rv(θ),z) on D=[0,2π]×[−L/2,L/2]. This compact rectangle is the closure of its nonempty connected interior and is Jordan measurable, its boundary consisting of four line segments. By [F3], Φ is C1 on a neighbourhood of D with ∂θΦ=r(u′,v′,0)=r(−v,u,0) and ∂zΦ=(0,0,1), so ∂θΦ×∂zΦ=r(u,v,0) is nonzero on the interior because r>0 and u2+v2=∣eiθ∣2=1; by ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ, equality of images forces equal z and θ−θ′∈2πZ. If 0<θ<2π and 0≤θ′≤2π, their difference lies strictly between −2π and 2π, so it is zero. Thus no interior point shares its image with a distinct point of the whole rectangle; the seam θ=0↔2π lies on the boundary. Hence (D,Φ) is an admissible regular patch for the lateral surface [F4]. Since E(Φ(θ,z))=λ2πε0r(u,v,0), the flux integrand is E⋅(∂θΦ×∂zΦ)=λ2πε0r⋅r=λ2πε0, and the flux equals λ2πε0λ2(D)=λ2πε0⋅2πL=λLε0 by the box measure and the Riemann/Lebesgue agreement for the constant integrand ([F4], [F8]).

5.1step 1.1step 4.1F5F6F7F8F9

Clause (d), superposition representation: for a longitudinal coordinate t∈R (metres) put zt:=te3 and E1,t:R3→R3 by E1,t(x):=x−zt4πε0∣x−zt∣3 for x≠zt and set E1,t(zt):=0 (the point-charge field per unit charge at zt, obtained from [F7] by dividing the field of any nonzero charge q by q, with units V C−1 m−1). For x∈Ω, direct computation with the primitive t↦tρ2ρ2+t2 of (ρ2+t2)−3/2 shows ∫−TTdt(ρ2+t2)3/2=2Tρ2ρ2+T2→2ρ2 as T→∞ and ∫x3−Tx3+Tx3−t(ρ2+(x3−t)2)3/2dt=0 by oddness for every T ([F8]); hence, for every x∈Ω, λ∫RE1,t(x) dt=λ(x12πε0ρ2,x22πε0ρ2,0)=E(x), the first two components because ∫R(ρ2+t2)−3/2dt=2/ρ2 and the third by oddness. Moreover ∣E1,t(x)∣=14πε0(ρ2+(x3−t)2)≤14πε0(1∣x3−t∣≤ρρ2+1∣x3−t∣>ρ(x3−t)2), whose t-integral is at most 44πε0ρ=1πε0ρ, and x↦∣∇ψ(x)∣/ρ(x), extended by 0 on the axis, is integrable for every compactly supported test: ∣∇ψ∣ is bounded on a containing cylinder and step 1.1 supplies the integral of 1/ρ there ([F5], [F6], [F9]).

6.1step 1.1step 5.1F6F7F9F10

Clause (d), the distributional identities: let ψ∈Cc∞(R3) and let Ψ∈Cc∞(R3;C3). For h=∇ψ or h=curl⁡Ψ, the function gh(x,t):=∣E1,t(x)∣∣h(x)∣ is nonnegative and Borel on R3×R: it is continuous off the closed set {(x,t):x=te3} and is 0 there. By [F6] it is product-measurable, and Tonelli, applied before any Fubini interchange, gives ∫R3×Rgh d(λ3×λ1)=∫R3(∫Rgh(x,t) dt) dx≤1πε0∫Ω∣h(x)∣ρ(x) dx<∞. The bound holds off the null axis by step 5.1; the last integral is finite because h is bounded and compactly supported and step 1.1 gives the transverse majorant. Thus E1,t⋅h belongs to product L1, and Fubini [F6] now licenses both orders of integration. Using step 5.1 almost everywhere, ⟨div⁡E,ψ⟩=−∫R3E⋅∇ψ dλ3=−λ∫R(∫R3E1,t⋅∇ψ dλ3)dt=λ∫R⟨div⁡E1,t,ψ⟩ dt, and [F7] gives div⁡E1,t=1ε0δzt, so the last expression is λε0∫Rψ(0,0,t) dt=1ε0ρλ(ψ) for every test function, which is the first identity. The same justified interchange for h=curl⁡Ψ gives ⟨curl⁡E,Ψ⟩=∫E⋅curl⁡Ψ=λ∫R⟨curl⁡E1,t,Ψ⟩dt=0, since each translated unit-charge field has vanishing distributional curl by [F7]; hence curl⁡E=0 in D′(R3).

7.1step 6.1F1F2F11

Clause (e): with φ=−λ2πε0log⁡(ρ/r0), the limits ρ→∞ and the r0-shift are the elementary properties of the logarithm [F2]: replacing r0 by r0′ adds −λ2πε0log⁡(r0/r0′)=λ2πε0log⁡(r0′/r0) to φ, which cancels in ∇φ, and as ρ→∞ the potential diverges to −∞ for λ>0 and to +∞ for λ<0, so for λ≠0 no normalisation at infinity is available ([F11]). If λ=0 then E=0, φ=0, ρλ=0, and every flux and cutoff energy vanishes by the identities above. For non-star-shapedness, let a∈Ω; then −a lies in Ω and the segment s↦(1−2s)a at s=1/2 is 0, which is not in Ω, so no point of Ω is a star centre for the whole set ([F1], [F11]).

8.1step 7.1F5F6F9

Clause (f): ∣E∣2=λ24π2ε02ρ2, and the two-dimensional polar formula of [F5], applied in the transverse variables and combined with Tonelli for the nonnegative integrand in the x3-variable [F6], gives ∫{δ<ρ<R,∣x3∣<L/2}∣E∣2 dλ3=L⋅λ24π2ε02⋅2πlog⁡Rδ=λ2L2πε02log⁡Rδ; multiplying by ε02 gives the displayed identity. For λ≠0 the factor log⁡(R/δ) tends to +∞ as δ↓0 and as R→∞, so no finite energy per unit length exists ([F5], [F9]).

9.1step 8.1F7F11∎

Clause (g) records the scope: [F11] declares only point and stationary-sheet sources, so the line distribution ρλ is outside the framework's source types; the construction used the ideal point-charge identity of [F7] superimposed along the axis with the absolute majorant of step 5.1, the classical computations of steps 2.1-4.1 on the open set Ω, and the polar/Fubini computations of steps 6.1-8.1. No physical realisation, equilibrium, material model, self-force or empirical claim is made, and no compact-source corollary is asserted; this is exactly the scope stated.

Depends on

Dependency tree · 2 levels

Sources