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.
Periodic centered-difference Poisson solvability and zero-mean gauge
Statement
Use the grid, inner product, and operator of Periodic uniform PIC grid and inner product. Then is self-adjoint and nonnegative, consists exactly of constant arrays, and . Consequently, for every compatible source , there is a unique solution of with the gauge .
For , the Fourier character is an eigenvector with Only has eigenvalue zero.
Facts & Assumptions
Given: , odd , , the periodic grid, its weighted inner product, and .
Periodic uniform PIC grid and inner product: is the periodic negative centered Laplacian, and .
Proof
Reindex the finite periodic sums in each coordinate. For any real arrays , The right side is symmetric in and is nonnegative when . Thus is self-adjoint and nonnegative.
If , every nonnegative squared difference in step 1.1 is zero, so for every . Coordinate steps connect every pair of indices in , hence is constant. Conversely a constant is annihilated by .
For a symmetric finite-dimensional linear map, : symmetry gives , and rank-nullity makes the dimensions equal. By step 2.1, is precisely the zero-mean subspace. Therefore each zero-mean is in the range, and any two solutions differ by a constant; imposing selects exactly one.
For , substitution in the stencil from [F1] gives The characters form a basis because their finite geometric sums are orthogonal: in one coordinate is if modulo and otherwise; taking products gives independent characters. Since every , exactly when every .
Depends on
Used by
- Fourier diagonal solver for the periodic centered-difference Poisson equation Algorithm
- A periodic Poisson source without neutralization is incompatible Counterexample
- Fixed-regularization periodic PIC pair kernel Definition
- Matched variational Hamiltonian branch for periodic PIC Definition
- Fixed-regularization periodic PIC force consistency on a smooth density Theorem
- Periodic PIC deposition conserves charge and satisfies Poisson compatibility Theorem
- Periodic Poisson residual controls the gathered particle force Theorem
- The periodic PIC Poisson algorithm returns the unique gauged solution Theorem
- The periodic Poisson mean-zero pseudoinverse is linear and self-adjoint Theorem
Dependency tree · one level
1 result 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
- Benjamin Seibold, MIT 18.336 Lecture 5, Finite Difference Approximation (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)