CounterexampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 periodic Poisson source without neutralization is incompatible

Statement

Take the one-dimensional periodic grid with $L = 1$ and odd $N \geq 3$ , one particle of charge $q = 1$ , and any nonnegative normalized assignment shape. If the deposited density $s_{j} = h^{- 1} w_{j} (X)$ is sent directly to $A_{h} ϕ = s$ without subtracting the neutralizing background $1 / L$ , then the equation has no solution.

Facts & Assumptions

Given: A periodic grid, a charge-one particle, normalized assignment weights, and the periodic centered Poisson operator.

[F1]

Periodic uniform PIC grid and inner product: $\overset{ˉ}{u} = L^{- 1} h \sum_{j} u_{j}$ and $A_{h}$ is the periodic negative centered Laplacian.

[F2]

Periodic centered-difference Poisson solvability and zero-mean gauge: every output of $A_{h}$ has zero mean, and its range is exactly the zero-mean subspace.

[F3]

Periodic PIC deposition shape and gather operators: an admissible algebraic assignment shape has $\sum_{j} w_{j} (x) = 1$ at every particle location.

Proof

1.1F1F3givenalgebra

The deposited source has total grid charge $h \sum_{j} s_{j} = \sum_{j} w_{j} (X) = 1$ by [F3]. Since $L = 1$ , its grid mean is $\overset{ˉ}{s} = L^{- 1} h \sum_{j} s_{j} = 1$ .

2.1F1F2step 1.1∎

By [F2], every solvable source for $A_{h} ϕ = s$ must have zero mean. Step 1.1 gives $\overset{ˉ}{s} = 1$ , so this unneutralized Poisson equation is incompatible. Subtracting the uniform background $1 / L = 1$ would instead make the source mean zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

3 results within one dependency step 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

R. W. Hockney and J. W. Eastwood, Computer Simulation Using Particles, Chapter 2 (standard reference, not scraped)
A. Myers, P. Colella, and B. Van Straalen, A 4th-Order Particle-in-Cell Method with Phase-Space Remapping for the Vlasov–Poisson Equation, Section 2.2 (standard reference, not scraped)