Pipeline-generated

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.

Verlet: worked examples

1 · Prerequisites

2 · Summary

The oscillator calculation exhibits an exact positive quadratic invariant for steps below the stability boundary, and derives an all-step bound for oscillation of the original energy. The analytic pendulum calculation verifies the complex vector-field bounds and the compact-domain margin, then states exactly which numerical-retention and arithmetic hypotheses remain necessary. These are mathematical examples in dimensionless coordinates, with no fabricated numerical measurements.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passOpen item page →

Oscillator Verlet: a preserved quadratic form and bounded original-energy oscillation

Example

Take $d = 1$ , $U = R^{2}$ , $Π = R$ , $M = (1)$ , and $V (q) = q^{2} / 2$ in The splitting Hamiltonian $H = A + B$ , the drift and kick maps, and the velocity-Verlet map. Thus the dimensionless oscillator has $H (q, p) = (q^{2} + p^{2}) / 2$ . For each initial state $z_{0} = (q_{0}, p_{0}) \in U$ , velocity Verlet is the matrix map $z \mapsto S_{h} z$ , where

$S_{h} = (\begin{array}{cc} 1 - h^{2} / 2 & h \\ - h (1 - h^{2} / 4) & 1 - h^{2} / 2 \end{array}) .$

For $0 < h < 2$ , put $α = 1 - h^{2} / 4$ and $I_{h} (q, p) = (α q^{2} + p^{2}) / 2$ . This positive quadratic form is exactly preserved. Every iterate satisfies

$∣ H (z_{n}) - H (z_{0}) ∣ \leq \frac{h^{2}}{4 α} I_{h} (z_{0}) .$

The conclusion is an explicit exact-arithmetic all-step fact for this linear example. At $h = 2$ positivity fails; at $h > 2$ the map has a real eigenvalue of modulus greater than one.

Verification

Given: The domain, mass matrix, potential, arbitrary initial state $z_{0} \in U$ , and the velocity-Verlet kick-drift-kick formula from the splitting definition; $0 < h < 2$ .

[F1] The splitting Hamiltonian $H = A + B$ , the drift and kick maps, and the velocity-Verlet map gives $K_{h / 2} (q, p) = (q, p - h q / 2)$ and $D_{h} (q, p) = (q + h p, p)$ ; The drift, kick and velocity-Verlet maps are canonical: $(D C)^{T} J D C = J$ and $C^{*} ω = ω$ proves exact symplecticity.

1.1givenF1algebra

Matrix and invariant. Multiplying the three displayed shear matrices gives $S_{h}$ as stated. Direct multiplication gives $S_{h}^{T} diag (α, 1) S_{h} = diag (α, 1)$ , using $(1 - h^{2} / 2)^{2} + h^{2} α = 1$ . Thus $I_{h} (z_{n}) = I_{h} (z_{0})$ and $q_{j}^{2} \leq 2 I_{h} (z_{0}) / α$ .

2.1step 1.1algebra∎

Original energy and boundary. Since $H - I_{h} = h^{2} q^{2} / 8$ , $∣ H (z_{n}) - H (z_{0}) ∣ = (h^{2} / 8) ∣ q_{n}^{2} - q_{0}^{2} ∣ \leq h^{2} I_{h} (z_{0}) / (4 α)$ . At $h = 2$ the invariant matrix is singular. For $h > 2$ , $\det S_{h} = 1$ and $tr S_{h} = 2 - h^{2} < - 2$ , so the real reciprocal eigenvalues have one modulus greater than one. This explains the step restriction without asserting stability at its excluded endpoint.

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passOpen item page →

Analytic pendulum: checking the complex bounds and compact-iterate hypothesis

Example

On the dimensionless real ball $U = B_{4} (0) \subseteq R^{2}$ , take $Π = R$ , mechanical mass matrix $M = (1)$ , $A (q, p) = 1 - \cos q$ and $B (q, p) = p^{2} / 2$ , with holomorphic extensions $\tilde{A} (q, p) = 1 - \cos q$ and $\tilde{B} (q, p) = p^{2} / 2$ on $D (1)$ . Set $ρ = 1$ and $K = {\overline{B}}_{2} (0)$ . The analytic labels are potential first and kinetic second, so the splitting is velocity Verlet. These data satisfy the analytic hypotheses with the field bound $M = 5 + \cosh (1)$ . Therefore, for sufficiently small constant $h > 0$ , if the iterates lie in $K$ through $n h \leq e^{c / (2 h)}$ , their original-energy deviation is $O (h^{2})$ . Compact retention is an additional hypothesis, which this example does not infer from the estimate.

Verification

Given: The stated sets and entire functions, with dimensionless coordinates.

[F1] Analytic splitting data with uniform holomorphic neighbourhood, and the exact symmetric splitting map $Ψ_{h}$ specifies the complex neighbourhood, vector-field bound and compact margin. Analytic Verlet retains order-two energy accuracy on exponential times supplies the conditional energy estimate; Bounded per-step state perturbations add a separate linear energy term supplies its perturbed version.

1.1givenF1algebra

Analytic-data check. Both functions extend entirely. On $D (1)$ around $\overline{U}$ , $∣ p ∣ < 5$ and $∣ Im q ∣ < 1$ . Since $∣ \sin (x + i y) ∣^{2} = \sin^{2} x + \sinh^{2} y \leq \cosh^{2} (1)$ , $∥ X_{A} ∥ \leq \cosh (1)$ and $∥ X_{B} ∥ < 5$ , both bounded by $M$ . The sets are star-shaped about zero, $K$ is compact in $U$ , and its real boundary margin is $2$ . The analytic labels are potential first, kinetic second, so the composition is kick-drift-kick.

2.1step 1.1F1∎

Consequence and perturbations. Choose the theorem's sufficiently small $h_{0}$ also with $h_{0} \leq 1 / (2 M)$ , using the computed margin $δ = 2$ . Its mechanical-stage argument bounds every full internal segment by $2 M h \leq 1$ from its retained starting point in $K$ , so all stages lie in $B_{3} (0) \subset U$ and the analytic splitting equals velocity Verlet. All analytic-data hypotheses now hold, so [F1] gives the stated energy conclusion if numerical retention holds. If computed points $x_{j} \in K$ additionally have per-step state errors at most $η$ , and every comparison segment from $x_{j + 1}$ to $Ψ_{h} (x_{j})$ and from $Ψ_{h} (x_{j})$ to the modified-flow endpoint lies in $D (1 / 8)$ , the estimate instead reads $∣ H (x_{n}) - H (x_{0}) ∣ \leq 2 C_{E} h^{2} + C n h e^{- c / h} + C_{G} n η$ . Neither conclusion certifies retention or predicts empirical machine error.

5 · Examples, experiments and counterexamples

None yet.

Sources

Hairer, Geometric Numerical Integration, Lecture 3: backward error analysis, Sections 1–3 and 5; local analytic estimates supplied here