Pipeline-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.

✓ 3 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Fast multipole expansions and error — Examples

1 · Prerequisites

Fast multipole expansions and error

2 · Summary

Two separated planar charge clusters checks an order-one M2L polynomial and both certified 2D tails for two separated charges. Near/far split with exact near evaluation and truncated far error adds a same-leaf near charge and verifies that direct near evaluation contributes no truncation error. A clustered point set makes tree depth enter the work fixes two points and increases their separation depth to show why tree size and traversal counts must appear in the work hypotheses.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passOpen item page →

A clustered point set makes tree depth enter the work

Example

This example shows why the operation theorem records tree depth, node count, and list counts explicitly. In the square $[- 1 / 2, 1 / 2]^{2}$ , place two distinct unit charges at $z_{1} = 0$ and $z_{2} = 2^{- M}$ for an integer $M \geq 3$ , and refine a dyadic quadtree until every leaf has occupancy at most $1$ .

Facts & Assumptions

Given: The dyadic square partition, the two distinct points above, leaf occupancy $1$ , and the per-node passes of the planar FMM.

[F1]

Finite planar quadtree and separated interaction lists: dyadic bisection halves every cell side length, and the level-restricted linear-size hypothesis explicitly bounds the number $T$ of nonempty cells by a constant times $N$ .

[F2]

Fixed-order planar Laplace fast multipole procedure: the upward and downward passes visit every nonempty leaf and every parent-child edge whose two cells are nonempty.

[F3]

Planar FMM operation count under explicit linear-size tree and list bounds: the $O (N p^{2})$ conclusion requires $T, V, K, J = O (N)$ .

Verification

1.1givenF1algebra

At depth $h$ the cell along the corner path containing $0$ has side length $2^{- h}$ . For every $h < M$ , $2^{- M} < 2^{- h}$ , so both $0$ and $2^{- M}$ lie in that same cell; at the next split the second point is on the midpoint boundary and is assigned to the upper child, while $0$ is assigned to the lower child. Therefore the tree has a nonempty path through depth $M$ and at least $M + 1$ nonempty cells, although $N = 2$ .

2.1givenF2F3step 1.1algebra∎

With fixed $p = 1$ , $N p^{2} = 2$ is constant as $M$ varies, whereas [F2] makes the passes visit at least the $M$ nonempty parent-child edges on the path from step 1.1. This family violates the uniform node bound $T \leq C_{T} N$ required in [F3], so the theorem's hypotheses do not give a uniform $O (N p^{2})$ bound over arbitrarily clustered inputs.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passOpen item page →

Two separated planar charge clusters

Example

Use the dyadic root square $H = [0, 4]^{2}$ . Put $P = [0, 2] \times [0, 2]$ and $Q = [2, 4] \times [0, 2]$ ; the other two root children are empty. Within $P$ name its lower-left and lower-right children $C_{0} = [0, 1] \times [0, 1]$ and $C = [1, 2] \times [0, 1]$ . Within $Q$ name its lower-left, lower-right, and upper-left children $D_{0} = [2, 3] \times [0, 1]$ , $D = [3, 4] \times [0, 1]$ , and $D_{1} = [2, 3] \times [1, 2]$ ; its upper-right child is empty. Let the leaf threshold be $s = 2$ and split each cell with more than two labels. Put unit charges at $c \pm \frac{1}{4}$ in $C$ , where $c = \frac{3}{2} + \frac{1}{2} i$ . Put zero-charge labels at $\frac{1}{2} + \frac{1}{2} i$ in $C_{0}$ , $d = \frac{7}{2} + \frac{1}{2} i$ in $D$ , $\frac{5}{2} + \frac{1}{2} i$ in $D_{0}$ , and $\frac{5}{2} + \frac{3}{2} i$ in $D_{1}$ . Thus $P$ and $Q$ have three labels each and split; their named children are leaves. In the recursive ordered cell pair $(P, Q)$ , splitting the source exposes $(C, Q)$ , and then splitting $Q$ exposes the separated pair $(C, D)$ . The far difference disk has center $2$ and radius $\sqrt{2}$ , so use its analytic logarithm real at $2$ . Take order $p = 1$ .

Facts & Assumptions

Given: The six labels and their charges/positions above, the recursive cell-pair list rule, and the order-one planar FMM.

[F1]

Finite planar quadtree and separated interaction lists: a non-admissible pair is split by the specified cell rule, a separated pair is recorded as far, and direct near pairs are recorded at leaves.

[F2]

Fixed-order planar Laplace fast multipole procedure: P2M moments are $M_{n} (C) = \sum_{j \in I_{C}} q_{j} (z_{j} - c_{C})^{n}$ , M2L uses the displayed local coefficients, and near values/derivatives are added exactly.

[F3]

Global planar FMM potential and derivative error: one far pair with ratio $ρ < 1$ has potential and derivative bounds $Q ρ^{2} / [2 (1 - ρ)]$ and $(Q / R) ρ / (1 - ρ)$ at order $p = 1$ .

Verification

1.1givenF1algebra

The root has six labels, and its nonempty children $P, Q$ each have three, so threshold $s = 2$ makes $H, P, Q$ internal while all named grandchildren are leaves. The centers of $P, Q$ are $1 + i, 3 + i$ , their radii are $\sqrt{2}$ , and their center distance is $2 < 2 \sqrt{2}$ , so $(P, Q)$ is not separated. Its equal side lengths make the rule split the source $P$ ; child $C$ has center $c = 3 / 2 + i / 2$ and radius $\sqrt{2} / 2$ . The pair $(C, Q)$ is not separated because its center distance is $\sqrt{5 / 2} < 3 \sqrt{2} / 2$ . Splitting the larger cell $Q$ exposes $D$ centered at $d = 7 / 2 + i / 2$ ; now $∣ d - c ∣ = 2 > \sqrt{2} / 2 + \sqrt{2} / 2$ . Thus the list recursion records $(C, D)$ as a far pair, and the zero-charge label at $d$ is the target at the target-cell center.

1.2givenF2algebra

The two unit source offsets give $M_{0} = 2$ and $M_{1} = 0$ . With $d - c = 2$ , [F2] gives the $(C, D)$ local coefficients $L_{0} = 2 \log 2$ and $L_{1} = 1$ . At the target center this interaction returns potential $2 \log 2$ and derivative $1$ . Other source labels have zero charge, so they add no contribution to this target.

2.1givenstep 1.2algebra

The two nonzero source-target differences are $9 / 4$ and $7 / 4$ , so the exact potential is $\log (9 / 4) + \log (7 / 4) = 2 \log 2 + \log (63 / 64)$ and the exact derivative is $4 / 9 + 4 / 7 = 64 / 63$ . Comparing with step 1.2, the absolute errors are $\log (64 / 63) < 1 / 63$ and $∣ 64 / 63 - 1 ∣ = 1 / 63$ ; the logarithmic inequality follows from $\log (1 + x) = \int_{0}^{x} (1 + t)^{- 1} d t < x$ for $x > 0$ . Zero-charge labels add no contribution.

3.1givenF3step 2.1algebra∎

For the only far interaction with nonzero source charge, $Q_{C} = 2$ , $R = 2$ , and $ρ = \sqrt{2} / 2 \in (1 / 2, 1)$ . The [F3] bounds are $ρ^{2} / (1 - ρ) > 1 / 4$ and $ρ / (1 - ρ) > 1 / 2$ ; all other far source cells have $Q_{C} = 0$ . Any direct near pairs from the zero-charge labels contribute exactly zero, so the errors in step 2.1 satisfy the theorem's global sums.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passOpen item page →

Near/far split with exact near evaluation and truncated far error

Example

Use root $H = [0, 4]^{2}$ ; its two nonempty children are $P = [0, 2] \times [0, 2]$ and $Q = [2, 4] \times [0, 2]$ . Name the lower children of $P$ by $C_{0} = [0, 1] \times [0, 1]$ and $C = [1, 2] \times [0, 1]$ . Name the lower-left, lower-right, and upper-left children of $Q$ by $D_{0} = [2, 3] \times [0, 1]$ , $D = [3, 4] \times [0, 1]$ , and $D_{1} = [2, 3] \times [1, 2]$ ; its upper-right child and the two upper root children are empty. Let leaf threshold $s = 2$ and split each cell with more than two labels. Put unit charges at $c \pm \frac{1}{4}$ in $C$ , where $c = \frac{3}{2} + \frac{1}{2} i$ , a charge $3$ at $d - 0.1$ in $D$ , where $d = \frac{7}{2} + \frac{1}{2} i$ , and a zero-charge target label at $d$ . Put zero-charge labels at $\frac{1}{2} + \frac{1}{2} i$ in $C_{0}$ , $\frac{5}{2} + \frac{1}{2} i$ in $D_{0}$ , and $\frac{5}{2} + \frac{3}{2} i$ in $D_{1}$ . Then $P$ has three labels and $Q$ has four, so both split and their named grandchildren are leaves. For the target $d$ , the recursion records $(C, D)$ as far and the charge- $3$ pair in $D$ as direct near. Use the analytic logarithm on the far difference disk that is real at $2$ ; the near difference $0.1$ uses its real logarithm. Take order $p = 1$ .

Facts & Assumptions

Given: The seven labels, charges, and positions above, the recursive cell-pair rule, and the order-one algorithm.

[F1]

Finite planar quadtree and separated interaction lists: the recursive rule separates the far pair from direct near particle pairs in the leaves.

[F2]

Fixed-order planar Laplace fast multipole procedure: exact direct near values are added to the far local polynomial and its derivative.

[F3]

Global planar FMM potential and derivative error: the far interaction at ratio $ρ < 1$ has potential and derivative bounds $Q ρ^{2} / [2 (1 - ρ)]$ and $(Q / R) ρ / (1 - ρ)$ for $p = 1$ .

Verification

1.1givenF1algebra

The root has seven labels, and its nonempty children $P, Q$ have three and four labels, respectively; threshold $s = 2$ therefore splits all three, while the named grandchildren are leaves. The centers of $P, Q$ are $1 + i, 3 + i$ , their radii are $\sqrt{2}$ , and their center distance is $2 < 2 \sqrt{2}$ , so $(P, Q)$ is not separated. The tie rule splits source $P$ , exposing $C$ with center $c = 3 / 2 + i / 2$ and radius $\sqrt{2} / 2$ . The pair $(C, Q)$ is not separated since its center distance is $\sqrt{5 / 2} < 3 \sqrt{2} / 2$ , so the larger target cell $Q$ is split. The child $D$ has center $d = 7 / 2 + i / 2$ and radius $\sqrt{2} / 2$ , and $∣ d - c ∣ = 2 > \sqrt{2}$ ; hence $(C, D)$ is far. The distinct charge- $3$ source and zero-charge target at $d$ lie in the same leaf $D$ , so their ordered pair is direct near.

1.2givenF2algebra

The far source moments are $M_{0} = 2$ and $M_{1} = 0$ , so M2L for $(C, D)$ gives $L_{0} = 2 \log 2$ and $L_{1} = 1$ ; at $d$ the far approximation is $(2 \log 2, 1)$ . The direct near contribution of the charge- $3$ source is exactly $(3 \log (0.1), 30)$ , because $d - (d - 0.1) = 0.1$ ; direct contributions from zero-charge labels vanish.

2.1givenstep 1.2algebra

The exact far terms are $\log (9 / 4) + \log (7 / 4) = 2 \log 2 + \log (63 / 64)$ and $4 / 9 + 4 / 7 = 64 / 63$ . Adding the exact direct near values gives total $(2 \log 2 + \log (63 / 64) + 3 \log (0.1), 64 / 63 + 30)$ . The algorithm returns $(2 \log 2 + 3 \log (0.1), 1 + 30)$ , so the errors are $\log (64 / 63) < 1 / 63$ and $1 / 63$ ; the strict logarithmic bound follows from $\log (1 + x) = \int_{0}^{x} (1 + t)^{- 1} d t < x$ for $x > 0$ .

3.1givenF3step 2.1algebra∎

For the only far interaction with nonzero source charge, $Q_{C} = 2$ , $R = 2$ , and $ρ = \sqrt{2} / 2 \in (1 / 2, 1)$ , so [F3] gives bounds $ρ^{2} / (1 - ρ) > 1 / 4$ and $ρ / (1 - ρ) > 1 / 2$ . All other far source cells have zero charge, and every near pair was evaluated exactly, so the errors from step 2.1 satisfy the theorem's global sums.

Fast multipole expansions and error — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A clustered point set makes tree depth enter the work

Example

Facts & Assumptions

Verification

Two separated planar charge clusters

Example

Facts & Assumptions

Verification

Near/far split with exact near evaluation and truncated far error

Example

Facts & Assumptions

Verification

Sources