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.

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.

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)