TheoremStatement: AI-adaptedProof: 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.

Local and finite-time trajectory error for symplectic Euler and leapfrog

Statement

Let $d \geq 1$ , $Q \subseteq R^{d}$ be open, $V \in C^{3} (Q)$ , and $M$ symmetric positive definite. Set $H (q, p) = \frac{1}{2} p^{T} M^{- 1} p + V (q)$ and $F (q, p) = (M^{- 1} p, - \nabla V (q))$ . Fix $T > 0$ and $h = T / N$ with $N \geq 1$ . Suppose the exact solution, numerical states, all kick/drift intermediate states, and every line segment used below lie in one compact convex tube $K ⋐ Q \times R^{d}$ , with the derivatives of $F$ through order two bounded there. For $z_{0}$ in that tube, write $e_{n}^{E}$ for the error of iterated kick-then-drift symplectic Euler and $e_{n}^{V}$ for the error of iterated local leapfrog relative to the exact solution at $t_{n} = n h$ . Write $Ψ_{h}^{E}$ and $Ψ_{h}^{V}$ for their admitted one-step maps and $φ_{h}$ for the exact flow. For sufficiently small $h$ , constants $C_{E}, C_{V}, L$ independent of $h, N, n$ satisfy $∥ Ψ_{h}^{E} (z) - φ_{h} (z) ∥ \leq C_{E} h^{2}, ∥ Ψ_{h}^{V} (z) - φ_{h} (z) ∥ \leq C_{V} h^{3}$ for admitted $z \in K$ , and whenever $n h \leq T$ , $e_{n}^{E} \leq e^{L T} e_{0} + C_{E} T e^{L T} h, e_{n}^{V} \leq e^{L T} e_{0} + C_{V} T e^{L T} h^{2} .$ Thus symplectic Euler has global order one and leapfrog has global order two on the stated controlled tube. No unconditional domain-admissibility claim is made.

Facts & Assumptions

Given: $V \in C^{3} (Q)$ , SPD $M$ , an exact Hamiltonian solution and numerical trajectories contained in the stated compact convex tube, with all method stages admitted.

[A1]

The local map is the partial kick/drift composition; symplectic Euler uses kick then drift, while leapfrog uses half-kick, full drift, half-kick. Local domain restriction for kick, drift, and leapfrog maps, Local kick-then-drift symplectic Euler step

[F1]

Since $M$ is symmetric positive definite, $M x = 0$ forces $x = 0$ , so $M$ is invertible and $(M^{- 1})^{T} = (M^{T})^{- 1} = M^{- 1}$ . Differentiating $H (q, p) = \frac{1}{2} p^{T} M^{- 1} p + V (q)$ therefore gives $\nabla H = (\nabla V (q), M^{- 1} p)$ and the coordinate field $F = (M^{- 1} p, - \nabla V (q))$ .

[F2]

The exact local flow and its variational derivative exist on admitted compact trajectory segments. C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade

[F3]

Total derivatives obey the chain rule. The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$

[F4]

Apply the scalar Taylor theorem coordinatewise on the compact convex tube; finitely many coordinate remainder bounds combine into a Euclidean bound. The same argument applies to the entries of $\nabla^{2} V$ . Multivariable Taylor formula with a Lagrange remainder along a line segment

[F5]

The Euclidean $p = 2$ norm on $R^{2 d}$ induces $d_{2}$ , and $(R^{2 d}, d_{2})$ is complete; hence this normed space is Banach. A continuous differentiable curve in it with derivative norm bounded by $C$ changes by at most $C$ times the interval length. Banach space, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page, $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ , Mean value inequality for a differentiable Banach-valued curve

Proof

technique · Taylor defect, one-step stability, and a finite geometric recurrence

1.1A1F1F2F3F4given

By [F1]–[F3], the exact solution satisfies $z^{'} = F (z)$ and $z^{''} = D F (z) F (z)$ . Since $D^{2} F$ is bounded on $K$ , [F4] gives uniformly $φ_{h} (z) = z + h F (z) + \frac{1}{2} h^{2} D F (z) F (z) + R (z, h), ∥ R (z, h) ∥ \leq C_{0} h^{3} .$

1.2A1F1F4F5algebra

The kick derivative is $I + h A_{K} (q)$ with $A_{K} = (\begin{array}{cc} 0 & 0 \\ - \nabla^{2} V (q) & 0 \end{array})$ and the drift derivative is $I + h A_{D}$ with $A_{D} = (\begin{array}{cc} 0 & M^{- 1} \\ 0 & 0 \end{array})$ . Their sum is $D F (q, p)$ . For kick-then-drift, the derivative product is $(I + h A_{D}) (I + h A_{K}) = I + h D F + O (h^{2})$ . For leapfrog it is $(I + (h / 2) A_{K} (q_{1})) (I + h A_{D}) (I + (h / 2) A_{K} (q)) = I + h D F + O (h^{2})$ ; since $q_{1} - q = O (h)$ and $D^{3} V$ is bounded, [F4] applied to each Hessian entry gives $\nabla^{2} V (q_{1}) - \nabla^{2} V (q) = O (h)$ . The remainders are uniform on $K$ , so $∥ D Ψ_{h} ∥ \leq 1 + L h$ for a fixed $L$ and small $h$ . The vector-valued mean-value inequality [F5] on the stipulated convex segments gives the same one-step Lipschitz bound for pairs of compared states.

2.1A1F1step 1.1algebra

Kick-then-drift Euler gives $p^{E} = p - h \nabla V (q)$ and $q^{E} = q + h M^{- 1} p^{E}$ . Thus $p^{E} = p - h \nabla V (q)$ and $q^{E} = q + h M^{- 1} p - h^{2} M^{- 1} \nabla V (q)$ . Comparing with the two coordinate components of step 1.1 gives a uniform one-step defect at most $C_{E} h^{2}$ .

2.2A1F1F4step 1.1algebra

For leapfrog, the intermediate momentum is $p_{1 / 2} = p - (h / 2) \nabla V (q)$ and the new position is $q_{1} = q + h M^{- 1} p_{1 / 2} = q + h M^{- 1} p - (h^{2} / 2) M^{- 1} \nabla V (q)$ . Taylor expansion of $\nabla V (q_{1})$ , using bounded third derivatives of $V$ , gives $p_{1} = p - \frac{h}{2} \nabla V (q) - \frac{h}{2} \nabla V (q_{1}) = p - h \nabla V (q) - \frac{h^{2}}{2} \nabla^{2} V (q) M^{- 1} p + O (h^{3}) .$ These are exactly the terms through degree two in step 1.1, so the leapfrog one-step defect is at most $C_{V} h^{3}$ .

3.1A1step 1.2step 2.1step 2.2algebra

For either method, if its local defect is $C h^{s + 1}$ , steps 1.2, 2.1, and 2.2 give $e_{n + 1} \leq (1 + L h) e_{n} + C h^{s + 1}$ . Iterating this inequality and using $(1 + L h)^{j} \leq e^{L T}$ and $n \leq T / h$ yields $e_{n} \leq e^{L T} e_{0} + C T e^{L T} h^{s}$ .

4.1step 3.1algebra∎

Substitution of $s = 1, C = C_{E}$ for symplectic Euler and $s = 2, C = C_{V}$ for leapfrog in step 3.1 gives the two stated bounds.

Depends on

Used by

Dependency tree · two levels

73 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

Ernst Hairer, Geometric Numerical Integration, TU München Lecture 2: Symplectic integrators (standard reference, not scraped)
Nikolaj Nordkvist and Poul G. Hjorth, Classical Mechanics and Symplectic Integration (standard reference, not scraped)