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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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)