TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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.

A certified shooting residual gives an explicit local periodic-orbit error bound

Statement

Let $z_{*} = (x_{*}, T_{*})$ be a phase-fixed nonconstant periodic orbit, let $G$ be its phase-bordered shooting residual, and suppose $D G (z_{*})$ is invertible with $∥ D G (z_{*})^{- 1} ∥_{2} \leq K_{J}$ . Let a convex validated domain contain the segment from $z_{*}$ to a candidate $z = (x, T)$ , with $∥ z - z_{*} ∥_{2} \leq r$ , and suppose $D G$ is $L_{J}$ -Lipschitz there and $K_{J} L_{J} r \leq 1$ . If a validated residual box $R$ contains $G (z)$ and $ϵ \geq \sup_{v \in R} ∥ v ∥_{2}$ , then $∥ z - z_{*} ∥_{2} \leq 2 K_{J} ϵ .$ If both scaled trajectories $ϕ_{T s} (x)$ and $ϕ_{T_{*} s} (x_{*})$ exist and lie in one convex state tube $K \subset U$ for every $s \in [0, 1]$ , with $∥ D f ∥_{2} \leq L_{f}$ and $∥ f ∥_{2} \leq M_{f}$ on $K$ and $0 < T, T_{*} \leq T_{+}$ , then they satisfy $\sup_{0 \leq s \leq 1} ∥ ϕ_{T s} (x) - ϕ_{T_{*} s} (x_{*}) ∥_{2} \leq 2 K_{J} e^{T_{+} L_{f}} (1 + M_{f}) ϵ .$ The residual box may be taken from Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting. A residual without the stated neighborhood, inverse, and derivative bounds gives no orbit-error conclusion.

Facts & Assumptions

Given: An exact phase-fixed root $z_{*}$ , an invertible shooting derivative, a candidate in a convex tube, the local derivative bounds, and an outward residual enclosure.

[F1]

The phase-bordered shooting map is $G (x, T) = (ϕ_{T} (x) - x, ψ (x))$ (The phase-bordered periodic-orbit BVP residual); its derivative is the phase-bordered matrix in A simple neutral multiplier and transverse phase make the shooting Jacobian invertible.

[F2]

The validated jet record contains an outward box enclosing the exact shooting residual on its input (Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting).

[F3]

Coordinatewise FTC recovers endpoint differences; continuous vector integrands are integrable, their integrals satisfy $∥ \int q ∥_{2} \leq \int ∥ q ∥_{2}$ , and pointwise inequalities pass to integrals (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable, If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[F4]

Gronwall bounds a nonnegative solution of $v (s) \leq A + B \int_{0}^{s} v (r) d r$ by $A e^{B s}$ (Gronwall's integral inequality with variable and constant coefficients).

[F5]

The derivative of a composition obeys the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F6]

The phase-bordered shooting map inherits $C^{2}$ regularity on a common tube from the $C^{2}$ field and its flow (A $C^{2}$ vector field has a $C^{2}$ flow on a common compact tube).

Proof

1.1F1F2F3F5F6givenalgebra

By [F6], $G$ is $C^{2}$ on the common validation tube. Put $δ = z - z_{*}$ and define $r (t) = G (z_{*} + t δ) - G (z_{*}) - t D G (z_{*}) δ$ for $0 \leq t \leq 1$ . Then $r (0) = 0$ and the chain rule [F5] gives $r^{'} (t) = (D G (z_{*} + t δ) - D G (z_{*})) δ$ . The segment lies in the stated convex domain, so $∥ r^{'} (t) ∥_{2} \leq L_{J} t ∥ δ ∥_{2}^{2}$ . By [F3], $r (1) = \int_{0}^{1} r^{'} (t) d t$ and $∥ r (1) ∥_{2} \leq \int_{0}^{1} ∥ r^{'} (t) ∥_{2} d t \leq (L_{J} / 2) ∥ δ ∥_{2}^{2}$ . Since $G (z_{*}) = 0$ , this is the first-order remainder bound. The residual box inclusion [F2] implies $∥ G (z) ∥_{2} \leq ϵ$ . Multiplying by $D G (z_{*})^{- 1}$ and using its norm bound yields $∥ δ ∥_{2} \leq K_{J} ϵ + (K_{J} L_{J} / 2) ∥ δ ∥_{2}^{2}$ . The hypothesis $∥ δ ∥_{2} \leq r$ and $K_{J} L_{J} r \leq 1$ make the quadratic term at most $\frac{1}{2} ∥ δ ∥_{2}$ ; rearrangement proves $∥ δ ∥_{2} \leq 2 K_{J} ϵ$ .

2.1F1F3F4F5step 1.1algebra∎

Let $x (s) = ϕ_{T s} (x)$ , $x_{*} (s) = ϕ_{T_{*} s} (x_{*})$ , $w (s) = x (s) - x_{*} (s)$ , and $u (s) = ∥ w (s) ∥_{2}$ . Both states and their connecting segment lie in $K$ . Integrating $D f$ along that segment gives $∥ f (x (s)) - f (x_{*} (s)) ∥_{2} \leq L_{f} u (s)$ . The chain rule [F5] and $w^{'} = T (f (x (s)) - f (x_{*} (s))) + (T - T_{*}) f (x_{*} (s))$ therefore give $∥ w^{'} (s) ∥_{2} \leq T_{+} L_{f} u (s) + M_{f} ∣ T - T_{*} ∣$ . By [F3], $w (s) = w (0) + \int_{0}^{s} w^{'} (r) d r$ and $u (s) \leq u (0) + \int_{0}^{s} ∥ w^{'} (r) ∥_{2} d r$ . Using the derivative bound and monotonicity in [F3], $u (s) \leq u (0) + \int_{0}^{s} (T_{+} L_{f} u (r) + M_{f} ∣ T - T_{*} ∣) d r$ . Gronwall [F4], with nondecreasing $a (s) = u (0) + M_{f} ∣ T - T_{*} ∣ s$ , gives $u (s) \leq e^{T_{+} L_{f}} (u (0) + M_{f} ∣ T - T_{*} ∣)$ . Each initial-state or period difference is at most $∥ δ ∥_{2}$ , so step 1.1 proves the trajectory estimate.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

88 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

S. M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010) (standard reference, not scraped)
Y. A. Kuznetsov, Elements of Applied Bifurcation Theory, 2nd ed., Chapter 1, §1.5 (standard reference, not scraped)