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

Exact two-charge dipole potential, its moments and the explicit far-field remainder

Physical scope

The exact potential of two ideal stationary point charges of opposite sign, its distributional equations, its source moments ( $Q = 0$ , $p = q d$ , vanishing traceless quadrupole) and an explicit far-field remainder bound of order $a^{2} / r^{3}$ about the ideal-dipole potential. The source is singular; no self-energy, self-force, dynamics, bound-state, stability or empirical claim is made.

Example

Assume the Axiom of Countable Choice ( ${A C}_{ω}$ ), inherited from the cited distribution and Lebesgue interfaces (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $q \in R$ and $d \in R^{3} ∖ {0}$ , put $a : = ∣ d ∣ / 2$ , and let the source be the two stationary point charges $+ q$ at $d / 2$ and $- q$ at $- d / 2$ (charge parameters in coulombs and the constant $ε_{0}$ of Framework-local SI units, the vacuum constants and the exact/measured status of their values), with fixed-time reading $q δ_{d / 2} - q δ_{- d / 2}$ (The static and pure electrostatic regimes and their fixed-time reading (e), Dirac delta and its derivatives). Define, with arbitrary values at the two points,

$φ (x) : = \frac{q}{4 π ε_{0} ∣ x - d / 2 ∣} - \frac{q}{4 π ε_{0} ∣ x + d / 2 ∣} (x \notin {d / 2, - d / 2}) .$

Then:

(a) [Exact potential and equations] $φ$ is locally integrable on $R^{3}$ and of class $C^{\infty}$ on $R^{3} ∖ {d / 2, - d / 2}$ ; with $E : = - \nabla φ$ on that set (The electric and magnetic fields as fixed-time spatial vector fields), the pair $(E, 0)$ satisfies the distributional pure electrostatic equations

$div E = \frac{q δ_{d / 2} - q δ_{- d / 2}}{ε_{0}}, curl E = 0 in D^{'} (R^{3})$

of the fixed-time dictionary of The static and pure electrostatic regimes and their fixed-time reading (e) (The localized Newtonian potential and the ideal point-charge Coulomb field (d) for each point charge, added by linearity of distributional differentiation: Distribution, Distributional derivative, Regular distribution from a locally integrable function, Locally integrable functions embed in distributions, Test function space d of an open set, Distributional differentiation is continuous and commutes);

(b) [Moments] in the finite-sum branch of Total charge, dipole moment, Cartesian moments and traceless quadrupole of a static charge distribution (c) about the chart origin of Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields, $Q = 0$ , $p = q d$ , every even Cartesian moment vanishes, $M_{i_{1} \dots i_{2 k + 1}} = 2 q (d / 2)_{i_{1}} \dots (d / 2)_{i_{2 k + 1}}$ for every $k \geq 0$ , and the traceless quadrupole vanishes, $Q_{i j} = 0$ ;

(c) [Exact far-field comparison] for every $x$ with $r : = ∣ x ∣ \geq 2 a = ∣ d ∣$ , the exact difference obeys the expansion form of Uniform Coulomb dipole expansion of a compactly supported charge density with an explicit remainder with the point-pair total variation in place of $∥ ρ ∥_{1}$ :

$φ (x) = \frac{p \cdot x}{4 π ε_{0} r^{3}} + R (x), ∣ R (x) ∣ \leq \frac{16 a^{2} (∣ q ∣ + ∣ q ∣)}{4 π ε_{0} r^{3}} = \frac{8 ∣ q ∣ a^{2}}{π ε_{0} r^{3}};$

(d) [Comparison with the compact-density theorem] the hypothesis of Uniform Coulomb dipole expansion of a compactly supported charge density with an explicit remainder is an $L^{1}$ density; for $q \neq 0$ the point pair has no such density, while for $q = 0$ its source is the zero density. In either case the proof below computes the two kernels directly; the identity and bound of (c) are proved directly for the two kernels by the twice-fundamental-theorem computation used in that theorem's remainder, and the leading term, the $a^{2}$ decay and the appearance of the total variation agree with the compact-density expansion;

(e) [Scope] the potential and the distributional equations are stated for the idealised singular source; no self-energy, self-force, dynamics, bound-state, stability or empirical claim is made for the pair. The quadrupole in (b) is computed about the specified symmetric origin; at a general reference point $b$ its value is $- 3 (b_{i} p_{j} + b_{j} p_{i}) + 2 (b \cdot p) δ_{i j}$ , since $Q = 0$ and $Q_{i j} = 0$ .

Facts & Assumptions

Given: Assume ${A C}_{ω}$ ; let $q \in R$ , $d \in R^{3} ∖ {0}$ , $a = ∣ d ∣ / 2$ , and let $+ q$ at $d / 2$ and $- q$ at $- d / 2$ be the two stationary point charges with fixed-time reading $q δ_{d / 2} - q δ_{- d / 2}$ ; let $φ$ be the displayed function with arbitrary values at the two points.

[F1]

For a point charge $q \in R$ at $x_{0}$ with $φ_{q} (x) = \frac{q}{4 π ε_{0} ∣ x - x_{0} ∣}$ and $E_{q} (x) = \frac{q (x - x_{0})}{4 π ε_{0} ∣ x - x_{0} ∣^{3}}$ off $x_{0}$ , the potential is locally integrable, the field is locally integrable and $C^{\infty}$ off $x_{0}$ with $E_{q} = - \nabla φ_{q}$ , and $- Δ T_{φ_{q}} = \frac{q}{ε_{0}} δ_{x_{0}}$ , $div E_{q} = \frac{q}{ε_{0}} δ_{x_{0}}$ and $curl E_{q} = 0$ in $D^{'} (R^{3})$ (The localized Newtonian potential and the ideal point-charge Coulomb field).

[F2]

For a finite system of stationary point charges the moments are finite sums $Q = \sum_{k} q_{k}$ , $p = \sum_{k} q_{k} x_{k}$ , $M_{i_{1} \dots i_{l}} = \sum_{k} q_{k} x_{k, i_{1}} \dots x_{k, i_{l}}$ , $Q_{i j} = \sum_{k} q_{k} (3 x_{k, i} x_{k, j} - ∣ x_{k} ∣^{2} δ_{i j})$ , hence $Q_{i j} = 3 M_{i j} - δ_{i j} \sum_{k} q_{k} ∣ x_{k} ∣^{2}$ , computed without Choice (Total charge, dipole moment, Cartesian moments and traceless quadrupole of a static charge distribution).

[F3]

A stationary point charge at $x_{0}$ with charge parameter $q$ is the point source of the weak-source definition with constant trajectory $z \equiv x_{0}$ , whose fixed-time reading is the spatial point source $q δ_{x_{0}}$ (The static and pure electrostatic regimes and their fixed-time reading).

[F4]

Distributional differentiation is linear: the distributional derivative of a finite sum of regular distributions is the sum of the derivatives (Distributional differentiation is continuous and commutes, Distributional derivative).

[F5]

$δ_{x_{0}} (ψ) = ψ (x_{0})$ , and the point-source pairings are those of the Dirac distribution (Dirac delta and its derivatives).

[F6]

If $Q = 0$ , then the traceless quadrupole about a reference point $b$ is $Q_{i j}^{(b)} = Q_{i j} - 3 (b_{i} p_{j} + b_{j} p_{i}) + 2 (b \cdot p) δ_{i j}$ (Origin shift of the source moments: Q, the dipole p - Qb, the Cartesian expansion and the traceless quadrupole).

[F7]

If $h$ is $C^{1}$ on $[0, 1]$ , then $h (1) - h (0) = \int_{0}^{1} h^{'} (t) d t$ (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[F8]

The chain rule and the algebra of derivatives apply to the composed maps $s \mapsto ∣ x - s y ∣^{- 1}$ off the poles; the power map $r \mapsto r^{- 1}$ is $C^{\infty}$ on $(0, \infty)$ with derivative $- r^{- 2}$ , and $\int_{0}^{1} (1 - t) d t = \frac{1}{2}$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (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) \neq 0$ , Continuity and derivatives of positive-base real powers).

[F9]

If $N$ is a norm on a real vector space $V$ , then $∣ N (u) - N (w) ∣ \leq N (u - w)$ for all $u, w \in V$ ; and ${\overline{B}}_{a} (0) = {y : ∣ y ∣ \leq a}$ (The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ , Open ball, closed ball and sphere in a metric space).

[F10]

The maps involved are computed with the smooth Euclidean calculus of component maps ( $C^{k}$ Euclidean maps and diffeomorphisms).

[F11]

$∣ \int f d λ_{3} ∣ \leq \int ∣ f ∣ d λ_{3}$ , and for measurable $0 \leq u \leq w$ one has $\int u d λ_{3} \leq \int w d λ_{3}$ ; a finite continuous Riemann integral is bounded by the sup of its integrand times the length of the interval (The modulus of an integral is bounded by the integral of the modulus, Monotonicity and nonnegative homogeneity of the nonnegative integral, If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[F12]

If two locally integrable functions agree a.e., their regular distributions agree, since every compactly supported test gives integrable products with the same a.e. class (Regular distribution from a locally integrable function, Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree).

[F13]

$∣ ⟨ u, w ⟩ ∣ \leq ∣ u ∣ ∣ w ∣$ for the Euclidean structure, and the vector norm is $∣ w ∣ = (\sum_{i} (w^{i})^{2})^{1 / 2}$ in the frame basis (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[F14]

Finite sums are distributive and may be reindexed (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[F15]

The laboratory chart, its origin and the constant $ε_{0} > 0$ are those of the framework (Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields, Framework-local SI units, the vacuum constants and the exact/measured status of their values).

[F17]

Under Countable Choice there are smooth bumps $b_{z, h}$ with $0 \leq b_{z, h} \leq 1$ , equal to one on ${\overline{B}}_{h} (z)$ and supported in $B_{2 h} (z)$ (Compactly supported scaled Euclidean bumps).

[F18]

If measurable $v_{j} \to 0$ a.e. and $∣ v_{j} ∣ \leq G$ with $G \in L^{1}$ , then $\int v_{j} \to 0$ (Dominated convergence).

[F16]

The Lebesgue branches carry the declared Countable Choice of the measure interface (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The class $L^{1} (μ)$ of integrable functions, Integral over a measurable subset, Integrable real and complex functions, and their integrals).

Verification

technique · direct

1.1F1F3F4F5F12F15F16given

Prove (a). Each summand is the point-charge object of [F1] with $x_{0} = \pm d / 2$ and charge $\pm q$ ; each is locally integrable and $C^{\infty}$ off its pole, so the sum $φ$ is locally integrable and $C^{\infty}$ off ${d / 2, - d / 2}$ , with $E = - \nabla φ = E_{+ q} + E_{- q}$ there. The regular distribution of a locally integrable function is unaffected by changing it on the two-point null set [F12], and distributional differentiation is linear [F4], so adding the two identities of [F1] in $D^{'} (R^{3})$ and using [F5] gives $div E = (q δ_{d / 2} - q δ_{- d / 2}) / ε_{0}$ and $curl E = 0$ ; the dictionary identifying this spatial equation with the fixed-time reading of the source is [F3], and $E$ is the field object defined in The electric and magnetic fields as fixed-time spatial vector fields. The chart, its origin and the constant $ε_{0}$ are those of [F15], and the distributional and Lebesgue readings used here carry the declared Countable Choice and measure interface of [F16].

2.1step 1.1F2F13F14

Prove the moment and quadrupole clauses of (b). Insert the two points into the finite sums of [F2]: $Q = q + (- q) = 0$ and $p = q (d / 2) + (- q) (- d / 2) = q d$ ; for every $l \geq 1$ , $M_{i_{1} \dots i_{l}} = q \prod_{r = 1}^{l} (d / 2)_{i_{r}} + (- q) \prod_{r = 1}^{l} (- d / 2)_{i_{r}} = q (1 - (- 1)^{l}) \prod_{r = 1}^{l} (d / 2)_{i_{r}}$ , which vanishes for even $l$ and equals $2 q \prod_{r = 1}^{l} (d / 2)_{i_{r}}$ for odd $l$ , in particular $M_{i_{1} \dots i_{2 k + 1}} = 2 q (d / 2)_{i_{1}} \dots (d / 2)_{i_{2 k + 1}}$ and $M_{i j} = 0$ . Each point has $∣ x_{k} ∣ = ∣ \pm d / 2 ∣ = \frac{1}{2} ∣ d ∣ = a$ by the norm formula of [F13], and $\sum_{k} q_{k} ∣ x_{k} ∣^{2} = a^{2} (q + (- q)) = 0$ , so the second formula of [F2] gives $Q_{i j} = 3 M_{i j} - δ_{i j} \sum_{k} q_{k} ∣ x_{k} ∣^{2} = 0$ ; the identities used only finite distributivity [F14].

3.1step 2.1F6F13algebra

Prove the reference-point clause of (e). With $Q = 0$ the transformation of [F6] reads $Q_{i j}^{(b)} = Q_{i j} - 3 (b_{i} p_{j} + b_{j} p_{i}) + 2 (b \cdot p) δ_{i j}$ , and substituting $Q_{i j} = 0$ and $p = q d$ from step 2.1 gives $Q_{i j}^{(b)} = - 3 (b_{i} p_{j} + b_{j} p_{i}) + 2 (b \cdot p) δ_{i j}$ , which vanishes at $b = 0$ . If $q \neq 0$ , then $p = q d \neq 0$ ; a vanishing shifted quadrupole contracted with $p_{j}$ gives $- 3 ∣ p ∣^{2} b_{i} - (b \cdot p) p_{i} = 0$ , and its inner product with $p$ gives $- 4 ∣ p ∣^{2} (b \cdot p) = 0$ , whence $b = 0$ . If $q = 0$ then all moments and the off-pole potential vanish, and the invariance special case $Q = p = 0$ holds.

4.1step 3.1F7F8F9F10F11F13

Establish the far-field identity and bound, proving (c). Fix $y \in {d / 2, - d / 2}$ and $x$ with $r = ∣ x ∣ \geq 2 a$ , and put $h_{y} (s) : = ∣ x - s y ∣^{- 1}$ for $s \in [0, 1]$ . For all such $s$ the reverse triangle inequality gives $∣ x - s y ∣ \geq r - s ∣ y ∣ \geq r - a \geq r / 2 > 0$ [F9], so $h_{y}$ is $C^{\infty}$ on $[0, 1]$ with $h_{y} (0) = 1 / r$ ; the chain rule and the derivative of the power map give $h_{y}^{'} (s) = \frac{(x - s y) \cdot y}{∣ x - s y ∣^{3}}$ and $h_{y}^{''} (s) = - \frac{∣ y ∣^{2}}{∣ x - s y ∣^{3}} + 3 \frac{((x - s y) \cdot y)^{2}}{∣ x - s y ∣^{5}}$ , so $∣ h_{y}^{''} (s) ∣ \leq \frac{4 ∣ y ∣^{2}}{∣ x - s y ∣^{3}} \leq \frac{32 ∣ y ∣^{2}}{r^{3}}$ by [F13] [F8, F10]. The function $s \mapsto (1 - s) h_{y}^{'} (s) + h_{y} (s)$ has derivative $(1 - s) h_{y}^{''} (s)$ , so [F7] gives $h_{y} (1) - h_{y} (0) - h_{y}^{'} (0) = \int_{0}^{1} (1 - t) h_{y}^{''} (t) d t$ , whose modulus is at most $\frac{32 ∣ y ∣^{2}}{r^{3}} \cdot \frac{1}{2} = \frac{16 ∣ y ∣^{2}}{r^{3}}$ by the Riemann monotonicity in [F11] applied to $- C (1 - t) \leq (1 - t) h_{y}^{''} (t) \leq C (1 - t)$ with $C = 32 ∣ y ∣^{2} / r^{3}$ , and $\int_{0}^{1} (1 - t) d t = 1 / 2$ from [F7] applied to $t - t^{2} / 2$ ; hence $h_{y} (1) = \frac{1}{r} + \frac{x \cdot y}{r^{3}} + R_{y} (x)$ with $∣ R_{y} (x) ∣ \leq \frac{16 ∣ y ∣^{2}}{r^{3}} = \frac{16 a^{2}}{r^{3}}$ .

5.1step 4.1F13algebra

Substitute the two kernels into $φ$ , completing (c). Since $∣ y ∣ = a$ for both points and $q + (- q) = 0$ for the constant terms and $q (d / 2) \cdot x + (- q) (- d / 2) \cdot x = q d \cdot x = p \cdot x$ for the linear terms, step 4.1 gives $φ (x) = \frac{q}{4 π ε_{0}} (h_{d / 2} (1) - h_{- d / 2} (1)) = \frac{p \cdot x}{4 π ε_{0} r^{3}} + R (x)$ with $R = \frac{q}{4 π ε_{0}} (R_{d / 2} (x) - R_{- d / 2} (x))$ , so $∣ R (x) ∣ \leq \frac{∣ q ∣ (16 a^{2} + 16 a^{2})}{4 π ε_{0} r^{3}} = \frac{32 ∣ q ∣ a^{2}}{4 π ε_{0} r^{3}} = \frac{8 ∣ q ∣ a^{2}}{π ε_{0} r^{3}}$ .

6.1step 5.1F1F6F17F18∎

Draw the comparison (d) and the scope (e). The theorem of Uniform Coulomb dipole expansion of a compactly supported charge density with an explicit remainder assumes an $L^{1}$ density. For $q \neq 0$ the pair cannot be represented by even a locally integrable density: take bumps $ψ_{j}$ of [F17], centred at $d / 2$ , with radii decreasing to zero and all supports excluding $- d / 2$ . Their source pairings equal $q$ , whereas for any $g \in L_{l o c}^{1}$ the integrals $\int g ψ_{j}$ tend to zero by dominated convergence [F18], using $∣ g ∣$ on one fixed compact ball as majorant and the a.e. limit $ψ_{j} \to 0$ . This is a contradiction. For $q = 0$ the source and off-pole potential are zero and the zero density satisfies the density hypothesis; the identity and bound just proved for the two kernels are the direct twice-fundamental-theorem computation of step 4.1, and substituting the total variation $2 ∣ q ∣$ into that theorem's remainder bound $16 a^{2} ∥ ρ ∥_{1} / (4 π ε_{0} r^{3})$ would give exactly $\frac{8 ∣ q ∣ a^{2}}{π ε_{0} r^{3}}$ , in agreement with step 5.1; no self-energy, self-force, dynamics, bound-state, stability or empirical assertion is made for the singular pair, and for $q \neq 0$ the quadrupole vanishes exactly at the symmetric origin, while for $q = 0$ it vanishes at every reference point, by step 3.1, which is (e).

Exact two-charge dipole potential, its moments and the explicit far-field remainder

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources