TheoremStatement: Literature-sourcedProof: 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.

Total deterministic Ewald and particle-mesh error certificate

Statement

Assume Countable Choice and a neutral finite point-source configuration on $A Z^{3}$ from Neutral point sources and Fourier data on a three-dimensional torus. Fix $α > 0$ , real and reciprocal cutoffs $R, K_{c} \geq 1$ , a mesh with integers $M_{r} \geq 1$ and order $P \geq 2$ , and a finite symmetric retained set $K \subseteq {k \in Z^{3} ∖ {0} : ∣ κ_{k} ∣ \leq K_{c}}$ that is injective modulo $(M_{1}, M_{2}, M_{3})$ and has $∣ k_{r} ∣ < M_{r} / 2$ and $D (k) \neq 0$ for every $k \in K$ . Put $Q = \sum_{i} ∣ q_{i} ∣$ and let $B_{K_{c}} = {k \in Z^{3} ∖ {0} : ∣ κ_{k} ∣ \leq K_{c}}, M_{K_{c}} = B_{K_{c}} ∖ K .$ This in-ball omitted set is finite. Write $M_{R} = ⌊ R ⌋$ , $M_{K} = ⌊ K_{c} ⌋$ , $C_{R} = C_{A}$ , and $C_{K} = C_{2 π A^{- T}}$ for the shell constants in Uniform lattice-shell counts and explicit Gaussian tail controllers. Choose integers $J_{R} \geq M_{R}$ , $J_{K} \geq M_{K}$ such that $2 α^{2} J_{R} (J_{R} + 1) \geq 3$ and $\frac{1}{2 α^{2}} J_{K} (J_{K} + 1) \geq 3$ . Let $U_{3} (β, M, J)$ be that supplier's finite upper controller for $\sum_{m = M}^{\infty} (m + 1)^{3} e^{- β m^{2}}$ , and put $\begin{aligned} {\overline{B}}_{R}^{U} & = \frac{Q C_{R}}{\sqrt{π} α} U_{3} (α^{2}, M_{R}, J_{R}), & {\overline{B}}_{R}^{E} & = \frac{Q^{2} C_{R}}{2 \sqrt{π} α} U_{3} (α^{2}, M_{R}, J_{R}), & {\overline{B}}_{R}^{F, i} & = \frac{∣ q_{i} ∣ Q C_{R}}{\sqrt{π}} (2 α + α^{- 1}) U_{3} (α^{2}, M_{R}, J_{R}), \\ {\overline{B}}_{K}^{U} & = \frac{4 π Q C_{K}}{V} U_{3} ((4 α^{2})^{- 1}, M_{K}, J_{K}), & {\overline{B}}_{K}^{E} & = \frac{2 π Q^{2} C_{K}}{V} U_{3} ((4 α^{2})^{- 1}, M_{K}, J_{K}), & {\overline{B}}_{K}^{F, i} & = \frac{4 π ∣ q_{i} ∣ Q C_{K}}{V} U_{3} ((4 α^{2})^{- 1}, M_{K}, J_{K}) . \end{aligned}$

For $ϕ_{s} (r) = erfc (α r) / r$ , define the finite real-space potential at an off-source point by $S_{R} (x) = \sum_{i} q_{i} \sum_{\begin{array}{c} λ \in Λ \\ ∣ x - x_{i} + λ ∣ \leq R \end{array}} ϕ_{s} (∣ x - x_{i} + λ ∣),$ and the finite real energy by $E_{R} = \frac{1}{2} \sum_{i} \sum_{j} \sum_{\begin{array}{c} λ \in Λ \\ ∣ x_{i} - x_{j} + λ ∣ \leq R \end{array}}^{'} q_{i} q_{j} ϕ_{s} (∣ x_{i} - x_{j} + λ ∣),$ where the prime omits exactly $(j, λ) = (i, 0)$ . Let $F_{R, i} = - q_{i} \sum_{\begin{array}{c} 1 \leq j \leq n, λ \in Λ \\ (j, λ) \neq (i, 0), ∣ x_{i} - x_{j} + λ ∣ \leq R \end{array}} q_{j} ϕ_{s}^{'} (∣ x_{i} - x_{j} + λ ∣) \frac{x_{i} - x_{j} + λ}{∣ x_{i} - x_{j} + λ ∣} .$ The cutoff index set is held fixed in this force sum; the cutoff indicator is not differentiated. Set $\tilde{U} (x) = S_{R} (x) + U_{M, K} (x),$ ${\tilde{E}}^{χ} = E_{R} + E_{M, K}^{χ} - \frac{α}{\sqrt{π}} \sum_{i} q_{i}^{2}, {\tilde{F}}_{i}^{χ} = F_{R, i} + F_{M, i}^{χ},$ where $χ = u n c o r r$ uses the uncorrected energy and force of Deterministic reciprocal particle-mesh Ewald potential, energy, and force bounds, and $χ = c o r r$ uses its optional diagonal self-corrected branch. For the uncorrected branch suppose the derivative/gather residuals are $H_{k}$ ; the corrected branch uses the energy-gradient gather, so $H_{k} = 0$ .

Suppose the computed finite outputs $\hat{U} (x), {\hat{E}}^{χ}, {\hat{F}}_{i}^{χ}$ have certified arithmetic radii $ε_{U}, ε_{E}, ε_{F, i} \geq 0$ relative to $\tilde{U}, {\tilde{E}}^{χ}, {\tilde{F}}_{i}^{χ}$ , respectively. Define $\begin{aligned} η_{U} = & {\overline{B}}_{R}^{U} + {\overline{B}}_{K}^{U} + Q \sum_{m \in M_{K_{c}}} c_{m} + Q \sum_{k \in K} c_{k} A_{k} (2 + A_{k}) + ε_{U}, \\ η_{E}^{u n c o r r} = & {\overline{B}}_{R}^{E} + {\overline{B}}_{K}^{E} + \frac{Q^{2}}{2} \sum_{m \in M_{K_{c}}} c_{m} + \frac{Q^{2}}{2} \sum_{k \in K} c_{k} A_{k} (2 + A_{k}) + ε_{E}, \\ η_{E}^{c o r r} = & {\overline{B}}_{R}^{E} + {\overline{B}}_{K}^{E} + \frac{Q^{2}}{2} \sum_{m \in M_{K_{c}}} c_{m} + \frac{Q^{2} - \sum_{i} q_{i}^{2}}{2} \sum_{k \in K} c_{k} A_{k} (2 + A_{k}) + ε_{E}, \\ η_{F, i}^{u n c o r r} = & {\overline{B}}_{R}^{F, i} + {\overline{B}}_{K}^{F, i} + ∣ q_{i} ∣ Q \sum_{m \in M_{K_{c}}} c_{m} ∣ κ_{m} ∣ + ∣ q_{i} ∣ Q \sum_{k \in K} c_{k} [∣ κ_{k} ∣ A_{k} + (1 + A_{k}) B_{k} + (1 + A_{k}) H_{k}] + ε_{F, i}, \\ η_{F, i}^{c o r r} = & {\overline{B}}_{R}^{F, i} + {\overline{B}}_{K}^{F, i} + ∣ q_{i} ∣ Q \sum_{m \in M_{K_{c}}} c_{m} ∣ κ_{m} ∣ + ∣ q_{i} ∣ (Q - ∣ q_{i} ∣) \sum_{k \in K} c_{k} [∣ κ_{k} ∣ A_{k} + (1 + A_{k}) B_{k}] + ε_{F, i} . \end{aligned}$ Then, for every off-source $x$ and each particle $i$ , $∣ \hat{U} (x) - U_{α} (x) ∣ \leq η_{U}, ∣ {\hat{E}}^{χ} - E ∣ \leq η_{E}^{χ}, ∥ {\hat{F}}_{i}^{χ} - F_{i} ∥_{2} \leq η_{F, i}^{χ} .$ Here $U_{α}, E, F_{i}$ are the exact mean-zero periodic Ewald potential, renormalized energy, and particle force. The finite omitted-mode sums $M_{K_{c}}$ explicitly charge every mode in the radial ball that the mesh did not retain, including Nyquist modes. Missing arithmetic radii do not produce a certificate; no RMS estimate is substituted for these deterministic bounds.

For the formal exact-constant work count, let $N_{i m g}$ be the total number of candidate real-image indices inspected in the finite potential, energy, and force loops, and let $N_{c e r t}$ be the total number of mode and finite controller entries inspected in constructing the omitted-mode ledger and error certificate. Count each such outer-loop inspection as one work unit and count the transform arithmetic in the formal exact-constant model of Mixed-radix and Bluestein reductions compute every finite DFT in O(N log N) arithmetic. For fixed $P$ , the finite evaluation uses $O ⁣ (N_{g} \log (2 N_{g}) + n P^{3} + N_{i m g} + N_{c e r t})$ work units, with at most three tensor transforms before optional mesh-self correction. The correction adds $O ⁣ (N_{g} \log (2 N_{g}) + n P^{6})$ when its cyclic kernel is precomputed. These counts do not include interval precision, elementary-function evaluation, memory traffic, bit complexity, or the transform subroutine's integer factor search and phase evaluation; no operation count is used as an accuracy bound.

Facts & Assumptions

Given: Countable Choice; a neutral finite source configuration on a full-rank cell; $α > 0$ , $R, K_{c} \geq 1$ , a finite admissible retained mode set $K$ ; integer mesh dimensions and $P \geq 2$ ; valid finite Gaussian tail-controller indices $J_{R}, J_{K}$ ; and actual arithmetic radii for the finite computations.

[A1]

Countable Choice is required by the Gaussian periodization and mean-zero periodic Poisson theorem (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

$Λ = A Z^{3}$ , $V = ∣ \det A ∣$ , $κ_{k} = 2 π A^{- T} k$ , the data are neutral, and source positions are distinct (Neutral point sources and Fourier data on a three-dimensional torus).

[F2]

The exact off-source potential and renormalized energy are the absolutely convergent Ewald formulas with reciprocal coefficient $c_{k}$ and self term $- α \sum_{i} q_{i}^{2} / \sqrt{π}$ ; the exact particle force differentiates the real and reciprocal Ewald terms under the collision-free convention (The alpha-independent Ewald potential and renormalized energy, Explicit real and reciprocal Ewald potential, energy, and force tail bounds).

[F3]

The finite real/reciprocal Ewald omissions are bounded by the displayed $B_{R}^{U}, B_{R}^{E}, B_{R}^{F, i}, B_{K}^{U}, B_{K}^{E}, B_{K}^{F, i}$ formulas, and replacing each $T_{3}$ by $U_{3}$ gives a finite certified upper bound (Explicit real and reciprocal Ewald potential, energy, and force tail bounds).

[F4]

The reciprocal particle-mesh potential, energy, and force aliases have the deterministic pointwise/per-particle bounds in Deterministic reciprocal particle-mesh Ewald potential, energy, and force bounds; the optional self-corrected energy/force branch has its corresponding improved retained-mode bounds there.

[F5]

A full-rank lattice has only finitely many points in a bounded ball; equivalently $∣ κ_{k} ∣ \leq K_{c}$ implies $∣ k ∣ \leq ∥ A^{T} ∥_{2} K_{c} / (2 π)$ (Full-rank lattices, covolume, and the dual lattice).

[F6]

The radii $ε_{U}, ε_{E}, ε_{F, i}$ bound the actual finite arithmetic outputs' differences from the exact-real finite truncated expressions defined in the Statement (given arithmetic enclosure interface).

[F7]

Differentiating the finite source coefficient gives $\nabla_{x_{i}} ρ_{k} = q_{i} \nabla_{x} a_{k} (t_{i}) = - i q_{i} κ_{k} a_{k} (t_{i})$ by the chain rule and sine/cosine derivatives (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , The derivatives of sine and cosine are cosine and minus sine, Neutral point sources and Fourier data on a three-dimensional torus).

[F8]

In the formal exact-constant model, an arbitrary-length one-dimensional DFT is exact and costs $O (M \log (2 M))$ arithmetic operations at length $M$ ; integer factor search and interval/phase evaluation are excluded (Arbitrary-length mixed-radix and Bluestein DFT, Mixed-radix and Bluestein reductions compute every finite DFT in O(N log N) arithmetic).

Proof

technique · direct

1.1F1F5algebra

From [F1], $κ_{k} = 2 π A^{- T} k$ , so $∣ κ_{k} ∣ \leq K_{c}$ implies $∣ k ∣ \leq ∥ A^{T} ∥_{2} K_{c} / (2 π)$ . Only finitely many integer vectors lie in that bounded ball by [F5]. Therefore $B_{K_{c}}$ and $M_{K_{c}}$ are finite, and all missing in-ball sums in the Statement are finite.

1.2givenF3

Choose $J_{R}, J_{K}$ as in the Statement. The finite Gaussian controllers $U_{3}$ bound the exact real and reciprocal shell tails by [F3], giving ${\overline{B}}_{R}^{U}, {\overline{B}}_{R}^{E}, {\overline{B}}_{R}^{F, i}, {\overline{B}}_{K}^{U}, {\overline{B}}_{K}^{E}, {\overline{B}}_{K}^{F, i}$ .

1.3A1F1F2F5F7algebra

For each omitted in-ball mode $m \in M_{K_{c}}$ , $∣ ρ_{m} ∣ \leq Q$ and $∣ e^{i κ_{m} \cdot x} ∣ = 1$ give potential magnitude at most $c_{m} Q$ . Its energy term is $\frac{1}{2} c_{m} ∣ ρ_{m} ∣^{2} \leq \frac{1}{2} c_{m} Q^{2}$ . By [F7], differentiating its finite reciprocal energy term gives exact force $- q_{i} c_{m} Re (\overline{ρ_{m}} \nabla_{x} a_{m} (t_{i}))$ , whose magnitude is at most $∣ q_{i} ∣ c_{m} ∣ ρ_{m} ∣ ∣ κ_{m} ∣ \leq ∣ q_{i} ∣ Q c_{m} ∣ κ_{m} ∣$ . Summing these inequalities over the finite omitted set accounts for every in-ball mode, including modes excluded by Nyquist restrictions.

1.4F4

The retained-mode mesh errors are bounded by [F4]. In the uncorrected energy branch this is $\frac{1}{2} Q^{2} \sum_{k \in K} c_{k} A_{k} (2 + A_{k})$ ; in the corrected branch it is $\frac{1}{2} (Q^{2} - \sum_{i} q_{i}^{2}) \sum_{k \in K} c_{k} A_{k} (2 + A_{k})$ . The force contributions are the corresponding $∣ q_{i} ∣ Q$ and $∣ q_{i} ∣ (Q - ∣ q_{i} ∣)$ sums in [F4], and the retained potential contribution is $Q \sum_{k \in K} c_{k} A_{k} (2 + A_{k})$ .

2.1A1F2F3F4step 1.2step 1.3step 1.4algebra

The exact Ewald series is the sum of the full real-space term, all retained reciprocal modes, all in-ball omitted reciprocal modes, and the reciprocal tail beyond $K_{c}$ , with the exact self constant in the energy. The finite approximations include the real terms through $R$ , the selected mesh approximation on $K$ , and that same self constant. Thus their exact-real differences split into the real cutoff tail, the reciprocal shell tail, the finite omitted in-ball terms, and the retained mesh alias/differentiation error. Step 1.2 bounds the real and reciprocal cutoff tails, step 1.3 accounts for every omitted in-ball mode, and step 1.4 bounds the retained mesh error. By [F3], [F4], and the triangle inequality, the absolute values or norms of these parts sum to the first terms displayed in each $η$ .

3.1F6step 2.1algebra

The arithmetic assumptions [F6] give $∣ \hat{U} - \tilde{U} ∣ \leq ε_{U}$ , $∣ {\hat{E}}^{χ} - {\tilde{E}}^{χ} ∣ \leq ε_{E}$ , and $∥ {\hat{F}}_{i}^{χ} - {\tilde{F}}_{i}^{χ} ∥_{2} \leq ε_{F, i}$ . Applying the triangle inequality to step 2.1 yields the three stated certificates. If an arithmetic radius is unavailable, the corresponding inequality has no supplied numerical right-hand side and no certificate is returned.

4.1F8algebra∎

For fixed $P \geq 2$ , the finite support enclosure gives at most $P + 2 \leq 2 P$ candidates per coordinate. Thus each particle's spread and potential/force gathers use $O (P^{3})$ support tuples; grid initialization costs $O (N_{g})$ and is absorbed by the transform count. A tensor transform along coordinate $r$ consists of $N_{g} / M_{r}$ one-dimensional transforms of length $M_{r}$ . By [F8] this costs $O (N_{g} \log (2 M_{r}))$ , and summing over the three coordinates gives $O (N_{g} \log (2 N_{g}))$ . The uncorrected computation uses one forward transform and at most two inverse/gather transforms. The finite real-image and mode/controller loops contribute $N_{i m g} + N_{c e r t}$ by definition, proving the stated total count. The optional correction adds one transform to form its cyclic kernel and at most $(P + 2)^{6} = O (P^{6})$ support-pair products per particle, which gives its stated cost. The arithmetic radii are certified separately and do not follow from this operation count.

Depends on

Used by

Dependency tree · two levels

84 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Hark Lee and Wei Cai, Ewald Summation for Coulomb Interactions in a Periodic Supercell (2009 lecture notes) (standard reference, not scraped)
Markus Deserno and Christian Holm, How to mesh up Ewald sums (I): A theoretical and numerical comparison of various particle mesh routines (1998) (standard reference, not scraped)