LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge 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.

Scaled RATTLE equations have unique local multiplier branches

Statement

Let $C$ be a compact subset of the regular phase manifold whose configuration projection lies in a compact regular chart. For each $(q, p) \in C$ , the two scaled RATTLE equations in Scaled classical RATTLE step map have unique local roots in neighborhoods of $λ_{0} = μ_{0} = \frac{1}{2} A (q)^{- 1} (D^{2} c (q) [v, v] - J (q) M^{- 1} \nabla V (q)), v = M^{- 1} p .$ In local phase coordinates the position root depends smoothly on $(h, q, p)$ , and the momentum root depends smoothly on $(h, q, p, λ)$ when the position multiplier is treated as a parameter near its selected root. The local branches agree on overlaps after shrinking their neighborhoods. A finite cover of $C$ therefore gives a common $h_{0} (C) > 0$ for $∣ h ∣ < h_{0} (C)$ ; the derivatives of each fixed finite order are uniformly bounded on this cover, and the two multiplier Jacobians remain uniformly invertible there. The exact position roots can also be kept in an ambient neighborhood of the compact regular configuration projection where $J$ has full row rank, so their constrained positions remain in $Q_{r e g}$ . At $h = 0$ both Jacobians equal $- A (q)$ .

Facts & Assumptions

Given: A compact phase subset $C \subset M$ over a compact regular configuration chart, consistent $(q, p) \in C$ , smooth $c, V$ , and signed $h$ with $∣ h ∣ < h_{0} (C)$ .

[F1]

Scaled classical RATTLE step map: $q_{1} = q + h M^{- 1} p_{1 / 2}$ , $p_{1 / 2} = p - \frac{h}{2} \nabla V (q) - h J (q)^{T} λ$ , $p_{1} = p_{1 / 2} - \frac{h}{2} \nabla V (q_{1}) - h J (q_{1})^{T} μ$ , with residuals $c (q_{1})$ and $J (q_{1}) M^{- 1} p_{1}$ .

[F2]

The regular holonomic phase space is a symplectic cotangent bundle: $(q, p)$ has local coordinates on the smooth phase manifold, so those coordinates form an open parameter block for the implicit-function theorem.

[F3]

A $C^{k + r}$ residual vanishing through order $r - 1$ has a $C^{k}$ scaled extension: if a smooth residual and its first $r - 1$ step derivatives vanish at zero, division by $h^{r}$ has a smooth extension whose value and derivatives are determined by the first nonzero Taylor coefficients.

[F4]

The parametrized implicit function theorem with $C^{k}$ regularity: a smooth residual equation with invertible derivative in its multiplier variables has a unique smooth local multiplier branch.

[F5]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : derivatives of compositions are computed by the chain rule.

Proof

1.1F1F2F3F4algebra

Put $v = M^{- 1} p$ and $w (λ) = - M^{- 1} (\frac{1}{2} \nabla V (q) + J (q)^{T} λ)$ . Then $q_{1} = q + h v + h^{2} w (λ)$ . Since $c (q) = 0$ and $J (q) v = 0$ , [F3] extends $h^{- 2} c (q_{1})$ smoothly, with value $F_{q} (0, q, p, λ) = \frac{1}{2} D^{2} c (q) [v, v] - \frac{1}{2} J (q) M^{- 1} \nabla V (q) - A (q) λ$ . Its $λ$ derivative is $- A (q)$ , which is invertible. Since $A$ is smooth and invertible, $A^{- 1} = adj (A) / \det A$ is smooth locally, so the center $λ_{0}$ varies smoothly with the phase input. Thus [F4] gives the unique local position multiplier branch at that center.

2.1F1F2F3F4F5step 1.1algebra

Let $G (h, q, p, λ, μ) = J (q_{1}) M^{- 1} p_{1}$ . Consistency gives $G (0, q, p, λ, μ) = 0$ , and [F3] extends $h^{- 1} G$ smoothly. By [F5], its value at zero is $F_{p} (0, q, p, λ, μ) = D^{2} c (q) [v, v] - J (q) M^{- 1} \nabla V (q) - A (q) (λ + μ)$ . Its $μ$ derivative is $- A (q)$ . At $λ = λ_{0}$ , the unique zero is $μ = λ_{0}$ , so [F4] gives a unique local momentum branch.

3.1F2F4step 1.1step 2.1choose∎

The branch equations are smooth in local phase coordinates, and $A^{- 1}$ is uniformly bounded on the compact configuration projection of $C$ . Since $J$ has full row rank on that compact projection, continuity gives an ambient neighborhood where it remains full row rank. Around each point of $C$ , shrink the phase and multiplier neighborhoods so both roots remain in common IFT uniqueness neighborhoods on overlaps and exact $q_{1}$ remains in this regular neighborhood. These neighborhoods cover $C$ ; compactness gives a finite subcover and the minimum of their positive step radii is a common $h_{0} (C)$ . The smooth branch derivatives are bounded on smaller compact neighborhoods covering $C$ for $∣ h ∣ \leq h_{0} (C)$ , and continuity of the multiplier Jacobians preserves uniform invertibility after a further shrink.

Depends on

Used by

Dependency tree · two levels

20 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, Christian Lubich, and Gerhard Wanner, Geometric Numerical Integration, 2nd ed., Chapter VII.1.4, pp. 245–246 (standard reference, not scraped)
Robert I. McLachlan, Klas Modin, Olivier Verdier, and Matt Wilkins, Geometric Generalisations of SHAKE and RATTLE, Foundations of Computational Mathematics 14 (2014), 339–370, §§4.1 and 5.1.3 (standard reference, not scraped)