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

Leapfrog changes the energy of an exact harmonic test mode

Statement

As a scalar diagnostic, consider the separable harmonic Hamiltonian $H (q, p) = \frac{1}{2} (p^{2} + q^{2})$ and one kick-drift-kick step with $Δ t = 1 / 2$ from $(q_{0}, p_{0}) = (1, 0)$ . It returns $(q_{1}, p_{1}) = (\frac{7}{8}, - \frac{15}{32}), H (q_{1}, p_{1}) = \frac{1009}{2048} \neq \frac{1}{2} = H (q_{0}, p_{0}) .$ The exact oscillator conserves $H$ . This abstract quadratic test is not claimed to be a trajectory of the periodic electrostatic potential $U_{h}$ from Matched variational Hamiltonian branch for periodic PIC; it shows why symplecticity or reversibility alone cannot imply exact preservation of an arbitrary Hamiltonian. On the separate PIC branch, Leapfrog geometry and finite-time order for the matched periodic PIC Hamiltonian proves its own reversible/symplectic and conditional order-two properties. The exact semidiscrete energy result there is The matched periodic PIC grid force is a gradient and its ODE conserves energy.

Facts & Assumptions

Given: $H (q, p) = \frac{1}{2} (p^{2} + q^{2})$ , the kick-drift-kick convention, and the initial state $(1, 0)$ .

[F1]

One-step leapfrog map as force and drift shears: kick and drift shears are $K_{a} (q, p) = (q, p - a \nabla U (q))$ and $D_{b} (q, p) = (q + b p, p)$ , and leapfrog composes them as a half kick, full drift, half kick.

[F2]

The matched periodic PIC grid force is a gradient and its ODE conserves energy: the exact semidiscrete PIC Hamiltonian flow conserves its continuous Hamiltonian; this is a separate model from the scalar test here.

[F3]

Leapfrog geometry and finite-time order for the matched periodic PIC Hamiltonian: on the periodic PIC Hamiltonian, leapfrog is reversible and symplectic and has a conditional order-two error bound, with no discrete exact-energy claim.

Proof

1.1givenalgebra

The half kick gives $p_{1 / 2} = p_{0} - (Δ t / 2) q_{0} = - 1 / 4$ . The drift gives $q_{1} = q_{0} + Δ t p_{1 / 2} = 1 - (1 / 2) (1 / 4) = 7 / 8$ . The final half kick gives $p_{1} = p_{1 / 2} - (Δ t / 2) q_{1} = - 1 / 4 - 7 / 32 = - 15 / 32$ .

2.1F1F2F3step 1.1algebra∎

For the oscillator, $\dot{q} = p$ and $\dot{p} = - q$ , so $\frac{d}{d t} H = q p - p q = 0$ . The kick and drift matrices for the test are $K_{1 / 4} = (\begin{array}{cc} 1 & 0 \\ - 1 / 4 & 1 \end{array}), D_{1 / 2} = (\begin{array}{cc} 1 & 1 / 2 \\ 0 & 1 \end{array}) .$ Each has determinant one. Direct multiplication gives $A^{T} J A = (\det A) J = J$ for every real $2 \times 2$ matrix $A$ , where $J = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ , so their composition is symplectic. The shears have inverses $K_{- 1 / 4}$ and $D_{- 1 / 2}$ ; reversing the palindromic composition with these inverses proves the step reversible. The exact Hamiltonian at the updated point is $H (q_{1}, p_{1}) = \frac{1}{2} (\frac{49}{64} + \frac{225}{1024}) = \frac{1}{2} \frac{1009}{1024} = \frac{1009}{2048},$ while $H (q_{0}, p_{0}) = 1 / 2 = 1024 / 2048$ . Their difference is $- 15 / 2048$ . Therefore this reversible symplectic step does not preserve its Hamiltonian exactly. The separate PIC results [F2] and [F3] concern their own variational force and tube hypotheses and are not transferred to this scalar test.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Nikolaj Nordkvist and Poul G. Hjorth, Classical Mechanics and Symplectic Integration, §3.5 (standard reference, not scraped)
R. W. Hockney and J. W. Eastwood, Computer Simulation Using Particles, Chapter 4 (standard reference, not scraped)