ExampleConstruction: Literature-sourcedVerification: 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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

Leslie Greengard and Vladimir Rokhlin, A Fast Algorithm for Particle Simulations, Journal of Computational Physics 73 (1987), 325–348 (standard reference, not scraped)
James Demmel, Fast Hierarchical Methods for the N-body Problem, Part 2, CS267 Lecture 25 (1996) (standard reference, not scraped)