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.

The admitted implicit midpoint branch is symplectic and second order

Statement

Let $d \geq 1$ , $U \subseteq R^{2 d}$ be open, $H \in C^{2} (U)$ , $z = (q, p)$ , and $J = (\begin{array}{cc} 0 & I \\ - I & 0 \end{array})$ . Use the Euclidean norm and its induced operator norm, and define $F (q, p) = (\nabla_{p} H (q, p), - \nabla_{q} H (q, p)) = J \nabla H (q, p)$ . For a signed step $h$ , suppose a declared closed ball $\overline{B} (z, ρ) \subset U$ , with $ρ \geq 0$ , has certified bounds $∥ F ∥ \leq M$ and $∥ D F ∥ \leq L$ satisfying $∣ h ∣ M / 2 \leq ρ$ and $θ : = ∣ h ∣ L / 2 < 1$ . The exact implicit midpoint branch Local implicit midpoint step for a Hamiltonian vector field then has a unique stage root $Z$ in this ball. The exact iterates $Z_{0} = z$ , $Z_{k + 1} = z + (h / 2) F (Z_{k})$ stay in the ball, converge to $Z$ , and for every $k \in N_{0}$ satisfy $∥ Z_{k} - Z ∥ \leq b_{k} : = \frac{θ^{k} ∥ Z_{1} - Z_{0} ∥}{1 - θ}, ∥ (2 Z_{k} - z) - (2 Z - z) ∥ \leq 2 b_{k} .$ Here $θ^{0} = 1$ , including when $θ = 0$ ; if $θ = 0$ , the first update equals $Z$ and $b_{k} = 0$ for $k \geq 1$ . Also $∥ (2 Z - z) - z ∥ \leq 2 ρ$ , which supplies an output-error bound when no update is computed.

For every finite tolerance $τ > 0$ and budget $B \in N_{0}$ , the implementation in Local implicit midpoint step for a Hamiltonian vector field terminates after at most $B$ updates and at most $B$ evaluations of $F$ ; each reported error radius is a valid bound.

Assume additionally $H \in C^{3} (U)$ and that these ball hypotheses hold uniformly for initial values $z$ in a compact convex tube for all $∣ h ∣ \leq h_{0}$ , with some $h_{0} > 0$ and common $ρ, M, L$ , where $h_{0} L / 2 \leq 1 / 2$ . At every admitted initial value the selected branch is locally the restriction of a $C^{1}$ solution branch, and its exact local map $Ψ_{h} (z) = 2 Z - z$ satisfies $D Ψ_{h} (z)^{T} J D Ψ_{h} (z) = J$ .

Fix $T > 0$ . Under these additional $C^{3}$ and uniform branch hypotheses, assume also that the exact and numerical trajectories, the branch balls, and the segments used in comparison lie in a compact convex subset of $U$ whenever $n ∣ h ∣ \leq T$ , with $F$ and its first two derivatives bounded there. For an initial value $z_{0}$ in the tube, define $z_{k + 1} = Ψ_{h} (z_{k})$ for $k \in N_{0}$ and $e_{n} = ∥ z_{n} - φ_{n h} (z_{0}) ∥$ for $n \in N_{0}$ (so $e_{0} = 0$ ). Then for constants $C, L_{1}$ independent of $h, n$ , every $z$ in the tube, and every $∣ h ∣ \leq h_{0}$ with $n ∣ h ∣ \leq T$ , $∥ Ψ_{h} (z) - φ_{h} (z) ∥ \leq C ∣ h ∣^{3}, e_{n} \leq e^{L_{1} T} e_{0} + C T e^{L_{1} T} ∣ h ∣^{2} .$ Here $φ_{h}$ is the exact Hamiltonian flow. These symplecticity and trajectory-error conclusions concern the exact selected map; no such conclusion is asserted here for a finite iteration output.

Facts & Assumptions

Given: For the contraction and iteration estimates, the stated $C^{2}$ Hamiltonian, admitted closed ball, bounds, and signed-step inequalities. For the symplecticity and trajectory-error claims, assume additionally the stated $C^{3}$ regularity, uniform branch hypotheses, and controlled finite-time tube.

[A1]

The field and selected branch obey the domain, closed-ball, bound, and step-size conditions in the Statement. Local implicit midpoint step for a Hamiltonian vector field

[F1]

On a complete metric space, a contraction has a unique fixed point and its iterates converge with tail bound $d (Z_{k}, Z) \leq q^{k} d (Z_{1}, Z_{0}) / (1 - q)$ . A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point

[F2]

A $C^{1}$ finite-dimensional equation with invertible derivative in the unknown has a locally unique $C^{1}$ solution branch with the implicit derivative formula. The Euclidean implicit function theorem with derivative formula

[F3]

For a $C^{1}$ vector field, the local flow is $C^{1}$ in the initial state and its derivative solves the variational equation; a $C^{2}$ field gives the needed finite $C^{2}$ flow regularity. C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade

[F4]

The cited Taylor theorem is scalar. A compact convex tube $K ⋐ U$ has an open convex neighborhood contained in $U$ , so the theorem can be applied separately to each scalar coordinate function on the stipulated segments, each entry of $D F$ , and each scalar coordinate of a trajectory on its local time interval. Intermediate points may depend on the coordinate. If the coordinate remainders satisfy $∣ R_{i} ∣ \leq C_{i} r^{s}$ , their vector satisfies $∥ R ∥_{2} \leq (\sum_{i} C_{i}^{2})^{1 / 2} r^{s}$ . Multivariable Taylor formula with a Lagrange remainder along a line segment

[F5]

Under the additional $C^{3}$ hypotheses, differentiating the explicit coordinate field in the Statement gives $D F = J \nabla^{2} H$ , and the Hessian is symmetric. Continuous mixed partials of order $k$ are invariant under permutations

[F6]

Derivatives of compositions and products obey the total-derivative chain rule. The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$

[F7]

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 Cauchy sequence in a closed ball converges in $R^{2 d}$ , and if $x_{j} \to x$ with $∥ x_{j} - z ∥ \leq ρ$ , then $∥ x - z ∥ \leq ∥ x - x_{j} ∥ + ∥ x_{j} - z ∥ \leq ∥ x - x_{j} ∥ + ρ$ , so the limit remains in the ball. 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$ , Banach space

[F8]

Every bounded sequence in $R^{2 d}$ has a convergent subsequence. For $n \geq 1$ every bounded sequence in $R^{n}$ has a convergent subsequence

[F9]

For a continuous curve in a Banach space that is differentiable in the interval's interior, a bound $∥ γ^{'} (t) ∥ \leq C$ implies $∥ γ (b) - γ (a) ∥ \leq C (b - a)$ . Mean value inequality for a differentiable Banach-valued curve

Proof

technique · contraction branch, Cayley-transform pullback, and a finite-time defect recurrence

1.1A1F1F6F7F9givenalgebra

Since $H \in C^{2} (U)$ , the coordinate field $F$ is $C^{1}$ . On the admitted closed ball, $T_{z} (W) = z + (h / 2) F (W)$ maps the ball into itself because $∥ T_{z} (W) - z ∥ \leq ∣ h ∣ M / 2 \leq ρ$ . For $W, V$ in the ball, the curve $γ (t) = F (V + t (W - V))$ lies in it and [F6] gives $∥ γ^{'} (t) ∥ \leq L ∥ W - V ∥$ ; the mean-value inequality [F9] therefore gives $∥ T_{z} (W) - T_{z} (V) ∥ \leq θ ∥ W - V ∥$ , where $θ = ∣ h ∣ L / 2 < 1$ . The ball is nonempty and complete by [F7], so [F1] gives a unique fixed point $Z$ , keeps all iterates in the ball, and gives $∥ Z_{k} - Z ∥ \leq b_{k} = θ^{k} ∥ Z_{1} - Z_{0} ∥ / (1 - θ)$ . Multiplication by two gives $∥ (2 Z_{k} - z) - (2 Z - z) ∥ = 2 ∥ Z_{k} - Z ∥ \leq 2 b_{k}$ , and $Z \in \overline{B} (z, ρ)$ gives $∥ (2 Z - z) - z ∥ \leq 2 ρ$ . The convention $θ^{0} = 1$ makes the bound valid at $k = 0$ . If $θ = 0$ , $T_{z}$ is constant on the ball, hence $Z_{1} = T_{z} (z) = T_{z} (Z) = Z$ and every later iterate equals $Z$ ; thus $b_{k} = 0$ for $k \geq 1$ . These assertions require only the $C^{2}$ hypotheses.

2.1A1F2F6F8algebra

For the remaining claims, assume the additional $C^{3}$ and uniform branch hypotheses. Fix an admitted initial value $z$ and let $z_{j} \to z$ through admitted initial values with selected roots $Z_{j}$ . Since $∥ Z_{j} - z_{j} ∥ \leq ρ$ and $z_{j} \to z$ , $(Z_{j})$ is bounded. If $Z_{j}$ did not converge to $Z$ , some subsequence would stay a positive distance from $Z$ ; by [F8] it would have a convergent subsequence $Z_{j_{ℓ}} \to Z_{*}$ . The bound $∥ Z_{j_{ℓ}} - z ∥ \leq ρ + ∥ z_{j_{ℓ}} - z ∥$ puts $Z_{*}$ in $\overline{B} (z, ρ) \subset U$ , and continuity in $Z_{j_{ℓ}} = z_{j_{ℓ}} + (h / 2) F (Z_{j_{ℓ}})$ gives $Z_{*} = z + (h / 2) F (Z_{*})$ . The contraction in step 1.1 gives uniqueness of this fixed point in $\overline{B} (z, ρ)$ , so $Z_{*} = Z$ , a contradiction; hence $Z_{j} \to Z$ . Now put $G (z, Z) = Z - z - (h / 2) F (Z)$ . At the selected root, $D_{Z} G = I - (h / 2) A$ with $A = D F (Z)$ . Since $∥ (h / 2) A ∥ < 1$ , this matrix is invertible by the Neumann series, and [F2] supplies a local $C^{1}$ root branch. The continuity just proved and the IFT's local uniqueness identify the selected roots with this branch at every nearby admitted initial value. Differentiating $G = 0$ gives $D_{z} Z = (I - (h / 2) A)^{- 1}$ and hence $S : = D Ψ_{h} = (I - B)^{- 1} (I + B), B = (h / 2) A .$

2.2A1F3F4F6step 1.1givenalgebra

Put $m = 2 d$ and $δ = Z - z$ . The admitted fixed-point equation gives $∥ δ ∥ \leq ∣ h ∣ ∥ F (Z) ∥ / 2 \leq ∣ h ∣ M / 2$ , hence $δ = O (∣ h ∣)$ uniformly. Since $H \in C^{3}$ , $F \in C^{2}$ . Apply the scalar theorem [F4] to each $F_{i}$ along $[z, Z]$ : $F_{i} (z + δ) = F_{i} (z) + D F_{i} (z) δ + R_{i}$ , where $R_{i} = \frac{1}{2} D^{2} F_{i} (z + ϑ_{i} δ) [δ, δ]$ for some $ϑ_{i} \in (0, 1)$ . These points may differ with $i$ . Bounded second derivatives on the tube give $∣ R_{i} ∣ \leq C_{i} ∥ δ ∥^{2}$ , hence $∥ R ∥_{2} \leq (\sum_{i = 1}^{m} C_{i}^{2})^{1 / 2} ∥ δ ∥^{2}$ . Substitution into $δ = (h / 2) F (z + δ)$ first gives $δ = (h / 2) F (z) + O (h^{2})$ and then $δ = (h / 2) F (z) + (h^{2} / 4) D F (z) F (z) + O (∣ h ∣^{3})$ . Thus $2 Z - z = z + h F (z) + (h^{2} / 2) D F (z) F (z) + O (∣ h ∣^{3})$ . For the exact flow, write $g_{i} (t) = (φ_{t} (z))_{i}$ . By [F3] and [F6], $g_{i}^{(1)} = F_{i} (φ_{t} (z))$ , $g_{i}^{(2)} = D F_{i} (φ_{t} (z)) F (φ_{t} (z))$ , and $g_{i}^{(3)} = D^{2} F_{i} (φ_{t} (z)) [F (φ_{t} (z)), F (φ_{t} (z))] + D F_{i} (φ_{t} (z)) D F (φ_{t} (z)) F (φ_{t} (z))$ are defined, with the third derivative uniformly bounded on the controlled trajectories. Scalar Taylor in time gives $g_{i} (h) = z_{i} + h F_{i} (z) + (h^{2} / 2) (D F (z) F (z))_{i} + (h^{3} / 6) g_{i}^{(3)} (η_{i} h)$ for $h \neq 0$ , with possibly distinct $η_{i} \in (0, 1)$ . Each last term is bounded by $C_{i}^{'} ∣ h ∣^{3}$ ; summing their squares gives a Euclidean remainder bound $(\sum_{i = 1}^{m} (C_{i}^{'})^{2})^{1 / 2} ∣ h ∣^{3}$ . The case $h = 0$ is immediate. The exact flow therefore has the same terms through degree two as $2 Z - z$ , giving the uniform one-step defect $C ∣ h ∣^{3}$ for either sign of $h$ . No common Lagrange intermediate point for the vector is used.

3.1F5step 2.1algebra

By [F5], $A = J \nabla^{2} H (Z)$ and $A^{T} J + J A = 0$ ; therefore $B^{T} J + J B = 0$ . Expanding both products gives $(I + B)^{T} J (I + B) - (I - B)^{T} J (I - B) = 2 (B^{T} J + J B) = 0$ . Thus $(I - B)^{T} J (I - B) = (I + B)^{T} J (I + B)$ .

3.2A1F3F4F6F9step 2.1step 2.2algebra

From step 2.1, $S - I = h (I - B)^{- 1} D F (Z)$ , and $∥ B ∥ \leq h_{0} L / 2 \leq 1 / 2$ gives $S = I + h D F (Z) + O (h^{2})$ uniformly. Also $∥ Z - z ∥ \leq ∣ h ∣ M / 2$ ; Taylor's formula applied to the entries of $D F$ along the stipulated segments, with $D^{2} F$ uniformly bounded, gives $D F (Z) = D F (z) + O (∣ h ∣)$ . Thus $D Ψ_{h} = I + h D F (z) + O (h^{2})$ and, after decreasing $h_{0}$ if needed, $∥ D Ψ_{h} ∥ \leq 1 + L_{1} ∣ h ∣$ . For each $n$ , split $e_{n + 1}$ into the change of $Ψ_{h}$ between $z_{n}$ and $φ_{n h} (z_{0})$ and the one-step defect at $φ_{n h} (z_{0})$ . Applying [F9] on the comparison segment and the local estimate of step 2.2 gives $e_{n + 1} \leq (1 + L_{1} ∣ h ∣) e_{n} + C ∣ h ∣^{3}$ ; the flow law in [F3] identifies $φ_{h} (φ_{n h} (z_{0})) = φ_{(n + 1) h} (z_{0})$ . Iteration and $(1 + L_{1} ∣ h ∣)^{n} \leq e^{L_{1} T}$ when $n ∣ h ∣ \leq T$ give $e_{n} \leq e^{L_{1} T} e_{0} + C T e^{L_{1} T} ∣ h ∣^{2}$ .

4.1A1step 2.1step 3.1algebra

The matrices $I - B$ and $I + B$ commute. Multiplying the equality in step 3.1 on the left by $(I - B)^{- T}$ and on the right by $(I - B)^{- 1}$ yields $J = (I - B)^{- T} (I + B)^{T} J (I + B) (I - B)^{- 1} = S^{T} J S$ . This proves the exact branch is symplectic.

5.1A1step 1.1step 2.1step 4.1step 2.2step 3.2givenalgebra∎

Step 1.1 proves existence, uniqueness, convergence, and the stage and output certificates under the $C^{2}$ hypotheses. The implementation returns immediately for $B = 0$ ; for $B \geq 1$ its finite loop either meets the tolerance earlier or takes at most $B$ updates before its final inconclusive branch, and step 1.1 proves every reported radius valid. Under the additional $C^{3}$ and tube hypotheses, step 2.1 proves the exact branch's stated regularity, step 4.1 proves symplecticity, and steps 2.2 and 3.2 prove local second order and the finite-time error.

Depends on

Used by

Cited to discharge well-definedness by Local implicit midpoint step for a Hamiltonian vector field.

Dependency tree · two levels

101 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)