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.

✓ 15 results · all verified · 6 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 9 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Periodic orbit shooting collocation and Floquet error

1 · Prerequisites

2 · Summary

Objective

This page fixes an autonomous phase by adding the unknown period and one scalar phase condition to the periodic endpoint equations. It records the neutral Floquet multiplier, the exact shooting Jacobian, and the equivalence between a simple neutral multiplier plus a transverse phase and invertibility of that bordered Jacobian. For the autonomous flow rescaled to $[0, 1]$ , it defines single/multiple-shooting and midpoint-collocation residuals, proves an explicit bounded-inverse estimate for the continuous phase-bordered BVP, and gives explicit residual and $h^{2}$ midpoint-error constants on a local branch.

Candidate solvers have finite budgets and never certify a root by their residual alone. A rational range-oracle interface encloses the flow and variational equation with explicit Euler defects; Krawczyk strict inclusion, its separate contraction bound, and a nonstationarity range certify a unique phase-fixed periodic solution within a box. A left/right-conditioned finite bound handles an isolated simple multiplier. For clusters, the page uses a verified resolvent cover, explicit midpoint quadrature error, a rational $π$ interval, and the argument principle to count multipliers with algebraic multiplicity. Orbital stability is concluded only when the neutral cluster count is one and every other complete cluster enclosure is strictly inside the unit circle. A unit-circle overlap leaves the verdict inconclusive.

The C2 common-tube flow theorem proves the required shooting-map regularity from the field hypothesis and supplies the second variation equation. Pseudo-arclength continuation corrects the parameterized phase-bordered residual with a validated section equation; a fold in the parameter projection does not itself make the full branch residual singular. The AUTO manual is used as an algorithm and notation source, not as a replacement for the local proofs. Exact supplier interfaces and remaining cross-batch checks are listed in the batch notes and dependency evidence.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck pendingjudge pass (gpt-6-luna)Open item page →

Exact range-oracle contract for validated flow and monodromy enclosures

Definition

Fix an integer $d \geq 1$ , an open set $Ω \subset R^{d + d^{2} + 1}$ , and a continuously differentiable map $H : Ω \to R^{d + d^{2} + 1}$ . A rational box is a finite product of closed intervals with rational endpoints. A sound range provider on a compact convex rational box $K \subset Ω$ is a procedure which, on each rational box $Q \subseteq K$ , returns either a rational box $H^{#} (Q)$ satisfying

{H (y) : y \in Q} \subseteq H^{#} (Q),

or the status inconclusive. It may not report a finite box without this inclusion. The provider also supplies rational bounds $L, M \geq 0$ satisfying

∥ H (y) - H (z) ∥_{\infty} \leq L ∥ y - z ∥_{\infty}, ∥ H (y) ∥_{\infty} \leq M (y, z \in K) .

The function bounds are part of the input certificate and must hold on all of $K$ . This interface says what a successful range computation means; it does not assert that a provider succeeds on every field or box.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A positively oriented convex polygon has winding index one inside and zero outside

Statement

Let $v_{0}, \dots, v_{m - 1} \in Q + i Q$ , $m \geq 3$ , be the cyclically ordered vertices of a simple strictly convex polygon whose edges are traversed counterclockwise. Let $P$ be its filled convex hull and let $Γ$ be the concatenation of its oriented edges. For every $z \notin Γ$ , the winding number $n (Γ, z)$ is $1$ if $z \in int P$ and $0$ if $z \notin P$ .

Facts & Assumptions

Given: A simple strictly convex polygon with rational vertices, its positive boundary orientation, its filled convex hull $P$ , and the winding number of the resulting closed contour.

[F1]

For a closed contour and a point off its trace, $n (Γ, z) = (2 π i)^{- 1} \int_{Γ} (w - z)^{- 1} d w$ (The winding number of a closed contour about a point off its trace).

[F2]

The winding number is constant on each connected component of the complement of the trace (The winding number is constant on each connected component of the complement of the trace).

[F3]

The winding number is zero on the unbounded connected component of the complement (The winding number vanishes on the unbounded component of the complement of the trace).

[F4]

At a single regular arc traversed with positive real tangent, the index on the left side minus the index on the right side is one (The winding number jumps by one across a regular planar arc).

Proof

1.1givenconstructalgebra

Fix exterior points $q_{1}, q_{2} \notin P$ and choose $R > \max {\max_{u \in P} ∥ u ∥_{2}, ∥ q_{1} ∥_{2}, ∥ q_{2} ∥_{2}}$ , which exists because $P$ is compact. For each $j \in {1, 2}$ , compactness gives a nearest point $p_{j} \in P$ . For every $u \in P$ , convexity puts $p_{j} + t (u - p_{j})$ in $P$ for $0 \leq t \leq 1$ ; minimality of $p_{j}$ gives $∥ q_{j} - p_{j} ∥_{2}^{2} \leq ∥ q_{j} - p_{j} - t (u - p_{j}) ∥_{2}^{2}$ . Expanding, dividing by $t > 0$ , and letting $t ↓ 0$ yields $⟨ q_{j} - p_{j}, u - p_{j} ⟩ \leq 0$ . Hence the ray $q_{j} + s (q_{j} - p_{j})$ , $s \geq 0$ , avoids $P$ and, being unbounded, meets the circle $C_{R} = {w : ∣ w ∣ = R}$ . The circle $C_{R}$ is disjoint from $P$ and connected, so these two rays and an arc of $C_{R}$ join $q_{1}$ to $q_{2}$ in $C ∖ P$ . Thus $C ∖ P$ is path-connected and unbounded.

2.1F1F3step 1.1

By [F1], $n (Γ, q)$ is the winding index of the contour. Since $Γ \subset P$ , the exterior $C ∖ P$ lies in the unbounded component of $C ∖ Γ$ ; [F3] gives $n (Γ, q) = 0$ for every $q \notin P$ .

3.1F1F4step 2.1choosealgebra

Fix $z \in int P$ . Choose a ray from $z$ whose direction is not aimed at a vertex. Its intersection with the convex polygon is a bounded interval starting at $z$ , so the ray exits at the interior $p$ of a single edge with directed tangent $v \neq 0$ . The polygon interior lies locally to the left of this positively oriented edge. Apply the orientation-preserving similarity $ρ (w) = \overline{v} (w - p) / ∣ v ∣$ , which sends $p$ to $0$ and the edge tangent to the positive real direction. For every $a \notin Γ$ , put $c = \overline{v} / ∣ v ∣$ . Parametrizing the transformed contour and using [F1] gives $\int_{ρ \circ Γ} \frac{d ζ}{ζ - ρ (a)} = \int_{Γ} \frac{c d w}{c (w - a)} = \int_{Γ} \frac{d w}{w - a}$ , so $n (ρ \circ Γ, ρ (a)) = n (Γ, a)$ . For sufficiently small $ε > 0$ , the points $ρ^{- 1} (i ε)$ and $ρ^{- 1} (- i ε)$ lie respectively on the interior and exterior local sides of the edge. Applying [F4] to $ρ \circ Γ$ gives $n (ρ \circ Γ, i ε) - n (ρ \circ Γ, - i ε) = 1$ ; the just-proved invariance rewrites this as $n (Γ, ρ^{- 1} (i ε)) - n (Γ, ρ^{- 1} (- i ε)) = 1$ . The exterior-side index is zero by step 2.1. Thus an interior point near that edge has winding number one.

4.1F2step 2.1step 3.1∎

The interior of a convex polygon is connected. Its points avoid $Γ$ , so [F2] makes the winding number constant throughout the interior. Step 3.1 identifies this constant as one. Together with step 2.1 this proves both cases.

AlgorithmAlgorithm: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Validated forward-Euler tube for the periodic flow and variational equation

Definition

Let $f : U \to R^{d}$ be $C^{2}$ . Set $m = d + d^{2} + 1$ and define the augmented autonomous field

H (x, Z, θ) = (θ f (x), θ D f (x) Z, 0)

on an open set $Ω \subseteq R^{m}$ . The exact flow and its differentiability on a common compact tube use Initial-data sensitivity of an ODE flow on a common compact tube. Inputs are a rational initial-state box $X_{0} \subset U$ , a rational period interval $Θ = [θ_{-}, θ_{+}] \subset (0, \infty)$ , an integer $N \geq 1$ , a compact convex rational tube $K \subset Ω$ , and a sound range oracle with rational bounds $L, M$ as in Exact range-oracle contract for validated flow and monodromy enclosures. Use the maximum norm and exact rational set arithmetic. Let $h = 1 / N$ and

Y_{0} = X_{0} \times {I_{d}} \times Θ .

For $n = 0, \dots, N - 1$ , first set

Q_{n} = Y_{n} + [- M h, M h]^{m} .

If $Q_{n} \subseteq̸ K$ , return inconclusive. Then request $H^{#} (Y_{n})$ . If it is inconclusive, return inconclusive. Otherwise form

Y_{n + 1} = Y_{n} + h H^{#} (Y_{n}) + [- L M h^{2} / 2, L M h^{2} / 2]^{m} .

If any required rational set operation is unavailable or the next box is not finite, return inconclusive; otherwise continue. On success return the tube boxes $Q_{0}, \dots, Q_{N - 1}$ and endpoint box $Y_{N}$ . The first, second, and last coordinate blocks of $Y_{N}$ enclose the exact endpoint, the exact variational matrix, and the period, respectively. The procedure makes no success claim if the supplied range oracle or $L, M$ bounds are not sound on $K$ .

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

The phase-bordered periodic-orbit BVP residual

Definition

Let $f : U \to R^{d}$ be an autonomous $C^{2}$ vector field on an open set $U$ , with the autonomous ODE convention of Autonomous ordinary differential equations and the $C^{2}$ map convention of $C^{k}$ Euclidean maps and diffeomorphisms. Let $ψ (x) = c^{⊤} (x - x_{r e f})$ be an affine phase function with $c \neq 0$ . On the scaled interval $s \in [0, 1]$ , introduce the augmented state $u = (x, θ) \in U \times (0, \infty)$ and vector field

\tilde{f} (x, θ) = (θ f (x), 0) .

For endpoint states $u_{0} = (x_{0}, θ_{0})$ and $u_{1} = (x_{1}, θ_{1})$ , define the boundary map

B (u_{0}, u_{1}) = (x_{1} - x_{0}, ψ (x_{0})) \in R^{d + 1} .

This is a square nonlinear BVP in the sense of Square nonlinear two-point boundary-value problems and endpoint residuals: its state dimension and number of boundary equations are both $d + 1$ . The period coordinate is constant along solutions because its derivative is zero. The common-tube differentiability of the exact flow is given by Initial-data sensitivity of an ODE flow on a common compact tube, and monodromy/Floquet terminology follows Local periodic-orbit, Poincare-return, and Floquet data.

Whenever the exact autonomous flow $ϕ_{t}$ exists on the required interval, the associated phase-bordered shooting residual is

G (x, θ) = (ϕ_{θ} (x) - x, ψ (x)) \in R^{d + 1}, θ > 0.

It is defined only for initial data whose flow exists through time $θ$ . Phase transversality at a nonstationary periodic point $x_{*}$ means $c^{⊤} f (x_{*}) \neq 0$ . Neither existence of a zero nor invertibility of its Jacobian is part of this definition.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

An autonomous periodic orbit has a neutral Floquet multiplier

Statement

Let $f$ be an autonomous $C^{1}$ vector field, let $γ (t) = ϕ_{t} (x_{*})$ be a nonconstant periodic solution of period $T > 0$ , and let $M = D_{x} ϕ_{T} (x_{*})$ be its monodromy matrix. Then

M f (x_{*}) = f (x_{*}) .

In particular, $1$ is a Floquet multiplier.

Facts & Assumptions

Given: The autonomous vector field, its $C^{1}$ local flow on a common tube through time $T$ , and the nonconstant periodic solution $γ (T) = x_{*}$ .

[F1]

The variational derivative $D_{x} ϕ_{T} (x_{*})$ exists on a common compact tube (Initial-data sensitivity of an ODE flow on a common compact tube).

[F2]

A $C^{1}$ autonomous field has a unique maximal $C^{1}$ flow with $\partial_{t} ϕ_{t} (x) = f (ϕ_{t} (x))$ (C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade). Uniqueness gives $ϕ_{T} (ϕ_{s} (x_{*})) = ϕ_{T + s} (x_{*})$ wherever both sides are defined: as functions of the elapsed time, both sides solve the same IVP from $ϕ_{s} (x_{*})$ .

[F3]

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

[F4]

A monodromy matrix is the period-time variational fundamental matrix, and its eigenvalues are the Floquet multipliers (Local periodic-orbit, Poincare-return, and Floquet data).

Proof

1.1givenF2

Nonconstancy implies $f (x_{*}) \neq 0$ : otherwise the constant curve through $x_{*}$ is an IVP solution, and uniqueness in [F2] forces $γ$ to be that constant curve.

2.1F1F2F3F4step 1.1∎

Differentiate the flow identity in [F2] with respect to $s$ at $s = 0$ . The chain rule [F3] gives $D_{x} ϕ_{T} (x_{*}) f (x_{*})$ on the left, while the time derivative on the right is $f (ϕ_{T} (x_{*})) = f (x_{*})$ . By [F1] the left derivative is the monodromy action, hence $M f (x_{*}) = f (x_{*})$ . Since $f (x_{*}) \neq 0$ by step 1.1, this is an eigenvector with eigenvalue $1$ , which is a Floquet multiplier by [F4].

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

A $C^{2}$ vector field has a $C^{2}$ flow on a common compact tube

Statement

Let $f : U \to R^{n}$ be $C^{2}$ on an open set $U$ . Let $T_{+} > 0$ , let $W \subset U$ be open, and suppose every solution from $x \in W$ exists on an open time interval containing $[0, T_{+}]$ and stays in one compact convex set $K \subset U$ for all $t \in [0, T_{+}]$ . Write $Φ (t, x) = ϕ_{t} (x)$ . Then $Φ$ is $C^{2}$ jointly in $(t, x)$ on $(0, T_{+}) \times W$ , locally on every common-tube neighborhood in $W$ , and its derivatives extend continuously in time to $[0, T_{+}]$ . Its first state derivative $S (t, x) = D_{x} Φ (t, x)$ solves

\partial_{t} S = D f (Φ) S, S (0, x) = I_{n},

and its second state derivative is the bilinear map $H (t, x)$ determined by

\partial_{t} H [u, v] = D f (Φ) H [u, v] + D^{2} f (Φ) [S u, S v], H (0, x) [u, v] = 0.

In particular $\partial_{t} Φ = f (Φ)$ , $\partial_{t x} Φ = D f (Φ) S$ , and $\partial_{t t} Φ = D f (Φ) f (Φ)$ . The assertion is local to the stated common tube.

Facts & Assumptions

Given: The $C^{2}$ vector field, $T_{+}$ , open initial-state set $W$ , and a common compact convex tube containing all solution graphs on $[0, T_{+}]$ .

[F1]

On a common compact tube the flow is $C^{1}$ in its initial state, and $S = D_{x} Φ$ is the unique solution of the variational equation (Initial-data sensitivity of an ODE flow on a common compact tube). Its proof's difference-quotient estimate is uniform over the compact time interval.

[F2]

A classical solution of the autonomous IVP is differentiable in time and satisfies $\partial_{t} Φ = f (Φ)$ (Autonomous ordinary differential equations, First-order systems, initial value problems, and solutions on intervals).

[F3]

The $C^{2}$ convention supplies continuous first and second total derivatives; on compact $K$ , $D f$ and $D^{2} f$ are bounded and $D^{2} f$ is uniformly continuous ( $C^{k}$ Euclidean maps and diffeomorphisms, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[F4]

A continuous-coefficient linear matrix IVP has a unique solution on the compact interval; adjoining a constant coordinate also solves an affine linear equation (Linear matrix ODEs have unique global solutions on a fixed interval).

[F5]

A nonnegative solution of $u (t) \leq A + L \int_{a}^{t} u (s) d s$ is bounded by $A e^{L (t - a)}$ (Gronwall's integral inequality with variable and constant coefficients).

[F6]

Integrating a differentiable curve recovers its endpoint difference, coordinatewise for vector-valued curves, and the norm of a vector integral is at most the integral of its norm (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)$ , 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).

[F7]

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

Proof

1.1F1F2F3F5F6given

Fix a base state $x \in W$ . By [F1], $Φ$ is $C^{1}$ in $x$ and $S$ solves $S^{'} = A S$ , where $A (t) = D f (Φ (t, x))$ . The coefficient is bounded on $[0, T_{+}]$ by [F3]; integrating the variational equation by [F6] and applying [F5] bounds $S$ uniformly in $t$ . The flow itself is jointly continuous in $(t, x)$ on the common tube by [F1] and the ODE relation [F2].

2.1F3F4F5F6step 1.1algebra

For a direction $h \in R^{n}$ , define a matrix $B_{h} (t)$ by $B_{h} (t) v = D^{2} f (Φ (t, x)) [S (t, x) h, S (t, x) v]$ . It is continuous and has norm at most $C ∥ h ∥_{2}$ for a finite constant $C$ , by [F3] and the bound on $S$ . Let $H_{h}$ solve $H_{h}^{'} = A H_{h} + B_{h}$ , $H_{h} (0) = 0$ . For each column, adjoining a constant coordinate turns its inhomogeneous linear IVP into a homogeneous linear system; applying [F4] to the augmented matrix gives a unique solution on $[0, T_{+}]$ . Its integral equation from [F6] and [F5] give $∥ H_{h} ∥_{\infty} \leq C^{'} ∥ h ∥_{2}$ for a finite constant $C^{'}$ .

2.2F1F3F6F7step 1.1algebra

For small $h$ with $x + h \in W$ , put $Δ (t) = Φ (t, x + h) - Φ (t, x)$ , $S_{h} (t) = S (t, x + h)$ , and $A_{h} (t) = D f (Φ (t, x + h))$ . The uniform remainder in [F1] gives $Δ = S h + o (∥ h ∥_{2})$ uniformly on $[0, T_{+}]$ . On each segment between $Φ (t, x)$ and $Φ (t, x + h)$ , the chain rule [F7] and [F6] applied coordinatewise to $D f$ give $A_{h} - A = \int_{0}^{1} D^{2} f (Φ + s Δ) [Δ, \cdot] d s .$ Uniform continuity of $D^{2} f$ on $K$ [F3] and $Δ = S h + o (∥ h ∥)$ therefore imply $A_{h} - A = D^{2} f (Φ) [S h, \cdot] + o (∥ h ∥_{2})$ uniformly in $t$ .

3.1F1F3F5F6step 2.1step 2.2algebra

The variational equations give $S_{h}^{'} = A_{h} S_{h}$ and $S^{'} = A S$ . Subtract these and the equation for $H_{h}$ from step 2.1, setting $R_{h} = S_{h} - S - H_{h}$ , to obtain $R_{h}^{'} = A_{h} R_{h} + (A_{h} - A) S + (A_{h} - A) H_{h} - B_{h}, R_{h} (0) = 0.$ By step 2.2, $(A_{h} - A) S - B_{h} = o (∥ h ∥)$ uniformly; also $A_{h} - A = O (∥ h ∥)$ and $H_{h} = O (∥ h ∥)$ by steps 2.2 and 2.1. Thus the forcing after $A_{h} R_{h}$ is $o (∥ h ∥)$ uniformly. The coefficients $A_{h}$ are uniformly bounded on $K$ , so [F5] applied to the integral equation for $R_{h}$ from [F6] gives $∥ R_{h} ∥_{\infty} = o (∥ h ∥_{2})$ . Therefore $D_{x} S (t, x) [h] = H_{h} (t)$ , proving existence of the second state derivative.

4.1F1F3F5F6step 2.1step 3.1

If $x_{j} \to x$ , [F1] gives uniform convergence of $Φ (\cdot, x_{j})$ and $S (\cdot, x_{j})$ on $[0, T_{+}]$ . Continuity of $D^{2} f$ on $K$ then gives uniform convergence of the coefficients and forcing in the linear equations for $H_{h}$ ; subtracting their integral equations and applying [F5] proves $H_{h} (\cdot, x_{j}) \to H_{h} (\cdot, x)$ uniformly. Thus the second state derivative is continuous in $(t, x)$ .

5.1F2F7step 1.1step 4.1∎

By [F2], $\partial_{t} Φ = f (Φ)$ . Differentiating this identity in $x$ and in $t$ using [F7] gives $\partial_{t x} Φ = D f (Φ) S$ and $\partial_{t t} Φ = D f (Φ) f (Φ)$ . These derivatives and $D_{x}^{2} Φ = H$ are continuous by steps 1.1 and 4.1, so $Φ$ is jointly $C^{2}$ on the stated tube.

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Zeros of the phase-bordered BVP are phase-fixed periodic orbits

Statement

Let $f$ , $ψ$ , $G$ , and $\tilde{f}$ be as in The phase-bordered periodic-orbit BVP residual. Assume the exact flow exists uniquely on $[0, θ]$ and $f (x) \neq 0$ . Then $G (x, θ) = 0$ if and only if $s \mapsto (ϕ_{θ s} (x), θ)$ solves the augmented BVP on $[0, 1]$ , with a nonconstant periodic trajectory whose phase satisfies $ψ (x) = 0$ .

Facts & Assumptions

Given: An autonomous $C^{2}$ vector field, a phase function, a positive $θ$ , and a unique exact flow on $[0, θ]$ from the trial point.

[F1]

The augmented vector field is $(x, θ) \mapsto (θ f (x), 0)$ , its boundary map is $(x_{1} - x_{0}, ψ (x_{0}))$ , and its shooting residual is $(ϕ_{θ} (x) - x, ψ (x))$ (The phase-bordered periodic-orbit BVP residual).

[F2]

A solution of a square BVP is a differentiable curve satisfying its vector field and endpoint residual (Square nonlinear two-point boundary-value problems and endpoint residuals).

[F3]

The $C^{2}$ autonomous field has a unique maximal $C^{2}$ flow satisfying $\partial_{t} ϕ_{t} (x) = f (ϕ_{t} (x))$ (C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade). Uniqueness gives the flow law wherever both sides are defined, by comparing the shifted trajectory and the solution from its shifted initial state.

[F4]

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

Proof

1.1givenF1F2F3F4construct

Suppose $G (x, θ) = 0$ . Set $u (s) = (ϕ_{θ s} (x), θ)$ . By [F3] and [F4], $u^{'} (s) = (θ f (ϕ_{θ s} (x)), 0) = \tilde{f} (u (s))$ . Its endpoint state has the same $x$ component as its initial state, and its initial phase residual is $ψ (x) = 0$ , so [F1]–[F2] make it an augmented BVP solution.

2.1givenF1F3step 1.1

Define $γ (t) = ϕ_{t} (x)$ for $0 \leq t \leq θ$ . By [F3] it solves $γ^{'} = f (γ)$ , and $G (x, θ) = 0$ gives $γ (θ) = γ (0)$ and $ψ (γ (0)) = 0$ . Since $f (x) \neq 0$ , it is nonconstant.

3.1givenF1F2F3F4step 1.1∎

Conversely, let $γ$ be a nonconstant solution on $[0, θ]$ with $γ (θ) = γ (0)$ and $ψ (γ (0)) = 0$ . Uniqueness in [F3] identifies $γ (t) = ϕ_{t} (γ (0))$ . Thus both components of $G (γ (0), θ)$ vanish, and $u (s) = (γ (θ s), θ)$ satisfies the augmented BVP by the same chain-rule calculation as step 1.1.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The validated Euler tube encloses the exact periodic flow and monodromy matrix

Statement

Let $H$ , $K$ , the range provider, $L, M$ , and the initial box $Y_{0} = X_{0} \times {I_{d}} \times Θ$ satisfy Exact range-oracle contract for validated flow and monodromy enclosures and Validated forward-Euler tube for the periodic flow and variational equation. If that procedure returns success with boxes $Q_{0}, \dots, Q_{N - 1}$ and $Y_{N}$ , then for every $(x_{0}, θ) \in X_{0} \times Θ$ the unique solution of $y^{'} = H (y)$ from $(x_{0}, I_{d}, θ)$ exists through time $1$ , its trajectory on $[n / N, (n + 1) / N]$ lies in $Q_{n}$ , and its terminal state lies in $Y_{N}$ . Consequently the endpoint state encloses $ϕ_{θ} (x_{0})$ and the matrix block encloses $D_{x} ϕ_{θ} (x_{0})$ .

Facts & Assumptions

Given: The exact augmented IVP, a sound range provider, bounds $L, M$ on the compact convex tube $K$ , and a successful finite Euler enclosure run.

[F1]

The provider encloses every exact value of $H$ on an admitted box and supplies valid Lipschitz and magnitude bounds $L, M$ on $K$ (Exact range-oracle contract for validated flow and monodromy enclosures).

[F2]

The algorithm sets $Q_{n} = Y_{n} + [- M h, M h]^{m}$ and $Y_{n + 1} = Y_{n} + h H^{#} (Y_{n}) + [- L M h^{2} / 2, L M h^{2} / 2]^{m}$ , and success requires $Q_{n} \subseteq K$ at each step (Validated forward-Euler tube for the periodic flow and variational equation).

[F3]

A continuously differentiable vector field has a unique local IVP solution; its maximal solution is the unique extension of those local solutions (Picard-Lindelöf local existence and uniqueness for first-order systems, Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).

[F4]

A $C^{1}$ autonomous field on an open set has a jointly $C^{1}$ maximal flow on an open time-state domain; its state derivative solves the variational equation (C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade). No convexity of a tube containing an entire trajectory is required.

[F5]

Integrating a continuously differentiable curve recovers its endpoint difference (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)$ ).

[F6]

Continuous scalar integrands are integrable, and pointwise bounds between integrable functions pass to their integrals (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, 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)$ ).

Proof

1.1F1F2F3F5F6given

Fix any exact state $y_{n} \in Y_{n}$ at time $n h$ and take its maximal solution from [F3]. If $M = 0$ , [F1] gives $H (y_{n}) = 0$ , so the constant solution and uniqueness in [F3] give the claim for this cell. Suppose $M > 0$ . Then $y_{n}$ is interior to $Q_{n}$ . While the solution remains in $K$ , each coordinate derivative $H_{i} (y (t))$ is continuous; [F5] and [F6] therefore give, coordinatewise, $- M (t - n h) \leq y_{i} (t) - y_{n, i} \leq M (t - n h)$ and hence $∥ y (t) - y_{n} ∥_{\infty} \leq M (t - n h)$ . A first exit from $K$ at $τ < n h + h$ would lie strictly inside $y_{n} + [- M h, M h]^{m} \subseteq Q_{n} \subseteq K$ , hence in the interior of $K$ , contradicting first exit. Nor can the maximal solution end at a finite $b \leq n h + h$ while remaining in $K$ : the same estimate makes $y (t)$ Cauchy as $t ↑ b$ , with limit $y_{b} \in K \subset Ω$ ; local existence from $(b, y_{b})$ in [F3] extends it, since continuity of $H$ gives the matching derivative at the join. This contradicts maximality. Thus the solution exists through the cell endpoint and, by the bound and continuity, stays in $Q_{n}$ throughout the closed cell.

2.1F1F2F5F6step 1.1algebra

By [F5], the exact Euler defect on this cell has coordinate integrals $δ_{i} = \int_{n h}^{n h + h} (H_{i} (y (t)) - H_{i} (y_{n})) d t$ . By [F1] and step 1.1, each integrand lies between $- L M (t - n h)$ and $L M (t - n h)$ . Applying [F6] on $[n h, n h + h]$ gives $∣ δ_{i} ∣ \leq \int_{n h}^{n h + h} L M (t - n h) d t = L M h^{2} / 2$ for every coordinate. Also $H (y_{n}) \in H^{#} (Y_{n})$ ; hence the exact next value lies in $Y_{n} + h H^{#} (Y_{n}) + [- L M h^{2} / 2, L M h^{2} / 2]^{m} = Y_{n + 1}$ .

3.1F2F3step 1.1step 2.1induction

Initially the exact state lies in $Y_{0}$ . Apply steps 1.1 and 2.1 successively for $n = 0, \dots, N - 1$ . Induction places each exact cell in $Q_{n}$ and its endpoint in $Y_{n + 1}$ , in particular the final endpoint in $Y_{N}$ . The no-exit argument and maximal-solution property [F3] establish existence and uniqueness through all cells.

4.1F2F4step 3.1algebra∎

For $H (x, Z, θ) = (θ f (x), θ D f (x) Z, 0)$ , the state block solves $x^{'} = θ f (x)$ and the matrix block solves $Z^{'} = θ D f (x) Z$ with $Z (0) = I_{d}$ . Rescaling physical time $t = θ s$ makes the state block $ϕ_{θ s} (x_{0})$ . Step 3.1 establishes existence through that time. Since $f$ is $C^{2}$ on open $U$ , [F4] gives the state derivative there on its open maximal-flow domain, even if $X_{0}$ is degenerate or the point is on its boundary. Its variational equation and uniqueness identify $Z (s)$ with $D_{x} ϕ_{θ s} (x_{0})$ . The terminal block inclusions from step 3.1 are therefore the claimed flow and monodromy enclosures.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

The Poincare derivative has precisely the non-phase monodromy multipliers

Statement

Let $γ$ be a nonconstant periodic orbit of least period $T$ , let $x_{*} = γ (0)$ , and let $M = D_{x} ϕ_{T} (x_{*})$ . Suppose the phase multiplier $1$ is algebraically simple and $ψ (x_{*}) = 0$ with $c^{⊤} f (x_{*}) \neq 0$ , where $c = D ψ (x_{*})$ . Then the eigenvalues of the derivative of the local Poincare return map on the section $Σ = {x : ψ (x) = 0}$ , counted with algebraic multiplicity, are exactly the Floquet multipliers of $M$ other than the single phase multiplier $1$ .

Facts & Assumptions

Given: A $C^{2}$ autonomous field, a periodic solution, its flow and monodromy, and a transverse affine phase section.

[F1]

The section is a codimension-one surface transverse to $f (x_{*})$ , and its local return map is the Poincare map (Local periodic-orbit, Poincare-return, and Floquet data).

[F2]

The phase-bordered residual is $G (x, T) = (ϕ_{T} (x) - x, ψ (x))$ (The phase-bordered periodic-orbit BVP residual).

[F3]

The derivative of the flow at time $T$ sends $f (x_{*})$ to itself (An autonomous periodic orbit has a neutral Floquet multiplier).

[F4]

The parametrized implicit function theorem solves a $C^{1}$ scalar equation locally when its derivative in the solved variable is nonzero (The parametrized implicit function theorem with $C^{k}$ regularity).

[F5]

The derivative of a composition is the composition of derivatives, with the total derivative convention of The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

Proof

1.1F1F2F4F5givenconstruct

Define $Ψ (t, x) = ψ (ϕ_{t} (x))$ . At $(T, x_{*})$ , $Ψ (T, x_{*}) = 0$ and $\partial_{t} Ψ (T, x_{*}) = c^{⊤} f (x_{*}) \neq 0$ . By [F4], there is a local return-time function $τ (x)$ on the section with $τ (x_{*}) = T$ and $Ψ (τ (x), x) = 0$ . Differentiating this identity at $x_{*}$ in a tangent direction $v \in S : = \ker c^{⊤}$ gives $D τ (x_{*}) v = - c^{⊤} M v / (c^{⊤} f (x_{*}))$ .

2.1F1F3F5step 1.1givenalgebra

The local return map is $P (x) = ϕ_{τ (x)} (x)$ . The chain rule and step 1.1 give, for $v \in S$ , $D P (x_{*}) v = M v - \frac{f (x_{*}) c^{⊤} M v}{c^{⊤} f (x_{*})} = Π M v, Π = I - \frac{f (x_{*}) c^{⊤}}{c^{⊤} f (x_{*})} .$ The map $Π$ identifies the quotient $C^{d} / span {f (x_{*})}$ with $S$ : it kills the phase direction and is the identity on $S$ . Since $M f (x_{*}) = f (x_{*})$ by [F3], it induces a linear map on this quotient, and $D P (x_{*})$ is its conjugate under that identification.

3.1F3step 2.1givenalgebra∎

In a basis whose first vector is $f (x_{*})$ , the matrix of $M$ is block upper triangular with first diagonal block $1$ and remaining block the induced quotient map. Its characteristic polynomial is therefore $(λ - 1)$ times that of the quotient map. The eigenvalue $1$ is simple by hypothesis, so the quotient eigenvalues, with multiplicity, are exactly all the remaining eigenvalues of $M$ . Step 2.1 identifies these with the Poincare derivative eigenvalues.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passOpen item page →

A simple neutral multiplier and transverse phase make the shooting Jacobian invertible

Statement

At a phase-fixed periodic point $x_{*}$ with period $T$ , let $M = D_{x} ϕ_{T} (x_{*})$ , let $f_{*} = f (x_{*}) \neq 0$ , and let $c = D ψ (x_{*})$ for the affine phase $ψ (x) = c^{⊤} (x - x_{r e f})$ . The derivative of the phase-bordered shooting residual is $J = [\begin{array}{cc} M - I_{d} & f_{*} \\ c^{⊤} & 0 \end{array}] .$ It is invertible if and only if $1$ is an algebraically simple eigenvalue of $M$ and $c^{⊤} f_{*} \neq 0$ . In the simple case choose real left/right eigenvectors $w, f_{*}$ with $w^{⊤} f_{*} = 1$ , put $Q = I - f_{*} w^{⊤}$ and $W = \ker w^{⊤}$ , and let $K_{W} = ∥ ((M - I_{d}) ∣_{W})^{- 1} ∥_{2 \to 2}$ . All vector and matrix norms below are Euclidean and induced Euclidean norms, and the product norm on $(u, τ) \in R^{d} \times R$ is Euclidean. Then $∥ J^{- 1} ∥_{2 \to 2} \leq K_{W} ∥ Q ∥_{2} + ∥ w ∥_{2} + \frac{∥ f_{*} ∥_{2} (1 + ∥ c ∥_{2} K_{W} ∥ Q ∥_{2})}{∣ c^{⊤} f_{*} ∣} .$ The period column is the exact time-sensitivity $f_{*}$ .

Facts & Assumptions

Given: A nonconstant autonomous periodic orbit, the phase residual of The phase-bordered periodic-orbit BVP residual, its monodromy $M$ , and the affine phase covector $c$ .

[F1]

The phase-bordered residual is $G (x, T) = (ϕ_{T} (x) - x, ψ (x))$ , with $ψ (x) = c^{⊤} (x - x_{r e f})$ (The phase-bordered periodic-orbit BVP residual).

[F2]

The tangent vector $f_{*}$ is a right eigenvector of $M$ for eigenvalue $1$ (An autonomous periodic orbit has a neutral Floquet multiplier).

[F3]

For a simple eigenvalue, compatible left and right eigenvectors pair nontrivially and can be normalized by $w^{*} f_{*} = 1$ (For a simple eigenvalue, left and right eigenvectors pair nontrivially and may be normalized by $y^{*} x = 1$ , Compatible left and right eigenvectors for a simple eigenvalue).

[F4]

Eigenvalues are precisely the roots of the characteristic polynomial (For every finite-dimensional space, $σ_{F} (T)$ is exactly the set of roots in $F$ of $χ_{T}$ , For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix). Here algebraic multiplicity means the multiplicity of that root; over $C$ the characteristic polynomial factors into linear factors counted with multiplicity (A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity) and a finite-dimensional operator has Jordan form (Jordan form over the base field exists exactly when the characteristic polynomial splits).

[F5]

The monodromy is the state derivative of the flow (Local periodic-orbit, Poincare-return, and Floquet data). For the $C^{2}$ field in [F1], the finite-regularity maximal-flow theorem supplies a $C^{2}$ flow with time derivative $\partial_{t} ϕ_{t} (x) = f (ϕ_{t} (x))$ (C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade).

[F6]

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

[F7]

For linear maps between finite-dimensional spaces of equal dimension, injectivity is equivalent to surjectivity (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

Proof

1.1F1F5F6

By [F1] and [F5], differentiating in $x$ gives $M - I_{d}$ , differentiating in $T$ gives $f (ϕ_{T} (x_{*})) = f_{*}$ , and differentiating the phase row gives $(c^{⊤}, 0)$ . This is the displayed matrix by [F6].

2.1F2F3F4F7step 1.1givenalgebra

Suppose $1$ is algebraically simple. Then [F4] implies that the complex eigenspace for eigenvalue $1$ is one-dimensional. By [F2] its spanning eigenvector $f_{*}$ is real, so the real kernel is $R f_{*}$ and rank-nullity gives ${rank}_{R} (M - I_{d}) = d - 1$ . Choose a real basis $v_{1}, \dots, v_{d - 1}$ of $range (M - I_{d})$ . The $d - 1$ real linear forms $w \mapsto v_{j}^{⊤} w$ are independent: if a linear combination vanishes for every $w$ , then the row $(\sum_{j} a_{j} v_{j})^{⊤}$ is zero, so $\sum_{j} a_{j} v_{j} = 0$ and basis independence forces every coefficient $a_{j}$ to vanish. Rank-nullity therefore gives a nonzero real $w_{0}$ with $v_{j}^{⊤} w_{0} = 0$ for every $j$ . Thus $w_{0}^{⊤} (M - I_{d}) = 0$ . It is a compatible left eigenvector with the real right eigenvector $f_{*}$ , so [F3], applied over $C$ , gives $w_{0}^{⊤} f_{*} \neq 0$ . This pairing is real; normalize $w = w_{0} / (w_{0}^{⊤} f_{*})$ , so $w$ is real, $w^{⊤} M = w^{⊤}$ , and $w^{⊤} f_{*} = 1$ . For $Q = I - f_{*} w^{⊤}$ and $W = \ker w^{⊤}$ , one has $Q f_{*} = 0$ , $Q ∣_{W} = I_{W}$ , and $Q M = M - f_{*} w^{⊤} M = M - f_{*} w^{⊤} = M - M f_{*} w^{⊤} = M Q$ . Hence $Q$ is the projection onto $W$ , $M$ preserves $W$ , and $M - I_{d}$ maps $W$ into $W$ . Its restriction to $W$ is injective: a kernel vector there would be an eigenvector independent of $f_{*}$ , contrary to simplicity. Since $W$ is finite dimensional, [F7] makes the restriction invertible. For $J (u, τ) = (r, s)$ , left multiplication of the first row by $w^{⊤}$ gives $τ = w^{⊤} r$ . Write $u = u_{W} + α f_{*}$ with $u_{W} \in W$ ; applying $Q$ to the first row and using its commutation with $M$ gives $u_{W} = ((M - I_{d}) ∣_{W})^{- 1} Q r$ , and the phase row gives $α = (s - c^{⊤} u_{W}) / (c^{⊤} f_{*})$ . Thus nonzero $c^{⊤} f_{*}$ gives a unique solution for every right-hand side, so $J$ is invertible. Moreover, $∣ τ ∣ \leq ∥ w ∥_{2} ∥ r ∥_{2}$ , $∥ u_{W} ∥_{2} \leq K_{W} ∥ Q ∥_{2} ∥ r ∥_{2}$ , and $∣ α ∣ \leq (∣ s ∣ + ∥ c ∥_{2} K_{W} ∥ Q ∥_{2} ∥ r ∥_{2}) / ∣ c^{⊤} f_{*} ∣$ . By the triangle inequality and $∥ r ∥_{2}, ∣ s ∣ \leq ∥ (r, s) ∥_{2}$ , these bounds yield the stated estimate.

2.2F2F4step 1.1algebraconstruct

If $c^{⊤} f_{*} = 0$ , then $J (f_{*}, 0) = 0$ , so $J$ is singular. Now suppose the algebraic multiplicity of $1$ exceeds one. If the complex eigenspace has dimension at least two, its real kernel also has dimension at least two: for the real matrix $M - I_{d}$ , its complex kernel consists exactly of $u + i v$ with $u$ and $v$ in the real kernel. Choose a real $v \in \ker (M - I_{d})$ independent of $f_{*}$ . If $c^{⊤} f_{*} = 0$ the preceding argument applies; otherwise $u = v - (c^{⊤} v) / (c^{⊤} f_{*}) f_{*}$ is nonzero, lies in $\ker (M - I_{d})$ , and satisfies $c^{⊤} u = 0$ , so $J (u, 0) = 0$ . If instead the eigenspace is one-dimensional, Jordan form [F4] supplies a generalized vector which, after rescaling, satisfies $(M - I_{d}) v = f_{*}$ over $C$ . Since $M - I_{d}$ and $f_{*}$ are real, $Re v$ is a real generalized vector satisfying the same equation; replace $v$ by this real vector. If $c^{⊤} f_{*} = 0$ , $J (f_{*}, 0) = 0$ ; if not, put $u = v - (c^{⊤} v) / (c^{⊤} f_{*}) f_{*}$ . Then $c^{⊤} u = 0$ and $(M - I_{d}) u = f_{*}$ , so $J (u, - 1) = 0$ . In every nonsimple case $J$ is singular.

3.1step 2.1step 2.2∎

Steps 2.1–2.2 prove both directions of the invertibility criterion.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

A transverse phase border makes the periodic BVP linearization boundedly invertible

Statement

Let $u_{*} (s) = (γ (T s), T)$ , $0 \leq s \leq 1$ , be the augmented solution from The phase-bordered periodic-orbit BVP residual for a nonconstant $C^{2}$ autonomous periodic orbit of period $T > 0$ . Assume its phase multiplier $1$ is algebraically simple and its affine phase covector $c$ satisfies $c^{⊤} f (γ (0)) \neq 0$ . For the continuous linearized BVP operator $L : X \to Z$ of Continuous linearized BVP operator and its conditioning, define $A (s) = D \tilde{f} (u_{*} (s)), a_{0} = \sup_{0 \leq s \leq 1} ∥ A (s) ∥_{2}, B_{2} = D_{2} B (u_{*} (0), u_{*} (1)), K_{J} \geq ∥ J^{- 1} ∥_{2 \to 2},$ where $J = [\begin{array}{cc} M - I & f (γ (0)) \\ c^{⊤} & 0 \end{array}]$ and $M = D ϕ_{T} (γ (0))$ . Put $E = e^{a_{0}}$ and $K_{L} : = (1 + a_{0}) [E K_{J} (1 + ∥ B_{2} ∥_{2} E) + E] + 1.$ Then $L$ is bijective and $∥ L^{- 1} ∥_{Z \to X} \leq K_{L}$ , with the spaces and norms defined in Continuous linearized BVP operator and its conditioning. All constants are finite and explicit once the stated coefficient and shooting-inverse bounds are supplied.

Facts & Assumptions

Given: The phase-fixed periodic solution, the augmented field and boundary map, the simple neutral multiplier and transverse phase, and the coefficient bound $a_{0}$ .

[F1]

The continuous linearized operator is $L v = (v^{'} - A v, B_{1} v (0) + B_{2} v (1))$ on $X = C^{1} ([0, 1], R^{d + 1})$ and $Z = C ([0, 1], R^{d + 1}) \times R^{d + 1}$ , with the norms in its definition (Continuous linearized BVP operator and its conditioning).

[F2]

The shooting Jacobian is $J = [\begin{array}{cc} M - I & f (γ (0)) \\ c^{⊤} & 0 \end{array}]$ and is invertible under the stated simplicity and transversality hypotheses (A simple neutral multiplier and transverse phase make the shooting Jacobian invertible).

[F3]

A linear matrix IVP with continuous coefficients on a positive-length compact interval has a solution on the entire interval (Linear matrix ODEs have unique global solutions on a fixed interval). This supplies a solution of $z^{'} = C (t) z + h (t)$ for continuous real $C, h$ : use the first column of the matrix solution with coefficient $[\begin{array}{cc} C & h \\ 0 & 0 \end{array}]$ and initial first column $(z_{0}, 1)$ ; its last entry stays $1$ . Such vector solutions are unique by local IVP uniqueness, extending the coefficients constantly past the interval endpoints when applying the open-domain theorem (Picard-Lindelöf local existence and uniqueness for first-order systems).

[F4]

If $u (t) \leq C + a_{0} \int_{s}^{t} u (r) d r$ for nonnegative continuous $u$ , then $u (t) \leq C e^{a_{0} (t - s)}$ (Gronwall's integral inequality with variable and constant coefficients).

[F5]

On an arbitrary open state domain a $C^{1}$ autonomous field has a jointly $C^{1}$ maximal flow on an open time-state domain. Its state derivative is the variational fundamental matrix, and its time derivative is the vector field (C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade).

[F6]

Coordinatewise FTC recovers endpoint differences for continuously differentiable vector curves; continuous vector integrands are integrable, their integral satisfies $∥ \int g ∥_{2} \leq \int ∥ g ∥_{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)$ ).

[F7]

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

Proof

1.1givenF3F4F6

The coefficient $A$ is continuous on $[0, 1]$ . For $0 \leq s \leq t \leq 1$ , let $U (t, s)$ be the solution operator of $v^{'} = A (t) v$ . Existence on all of $[0, 1]$ and uniqueness follow from [F3] with zero forcing. For any initial vector $ξ$ , [F6] and the equation give $∥ U (t, s) ξ ∥_{2} \leq ∥ ξ ∥_{2} + a_{0} \int_{s}^{t} ∥ U (r, s) ξ ∥_{2} d r$ ; Gronwall [F4] yields $∥ U (t, s) ∥_{2} \leq e^{a_{0} (t - s)}$ . In particular $U$ exists on the full triangle $0 \leq s \leq t \leq 1$ with the stated bound.

2.1F1F2F5F7step 1.1

The homogeneous solution with initial value $ξ$ is $U (t, 0) ξ$ . Apply [F5] to the $C^{1}$ augmented field $\tilde{f} (x, θ) = (θ f (x), 0)$ on open $U \times (0, \infty)$ . The given periodic solution exists through $s = 1$ , so its endpoint variation is the derivative of that flow on its open maximal domain; no convex set spanning the orbit is needed. The first $d$ endpoint coordinates differentiate to $M v + f (γ (0)) τ$ in initial variation $(v, τ)$ : the $v$ column is monodromy, and the period column is $\partial_{T} ϕ_{T} (γ (0)) = f (γ (0))$ by [F5] and periodicity. Differentiating $B (u_{0}, u_{1}) = (x_{1} - x_{0}, ψ (x_{0}))$ by [F7] therefore gives $B_{1} + B_{2} U (1, 0) = J$ .

2.2F1F3F4F6step 1.1algebra

For data $(g, q) \in Z$ , let $p$ be the unique solution of $p^{'} = A p + g$ , $p (0) = 0$ . Existence on all of $[0, 1]$ and uniqueness follow from [F3] with $C = A$ and $h = g$ . Since $p^{'}$ is continuous, [F6] gives $∥ p (t) ∥_{2} = ∥ \int_{0}^{t} p^{'} (s) d s ∥_{2} \leq \int_{0}^{t} ∥ p^{'} (s) ∥_{2} d s$ . Pointwise, $∥ p^{'} (s) ∥_{2} \leq a_{0} ∥ p (s) ∥_{2} + ∥ g ∥_{\infty}$ , so monotonicity in [F6] gives $∥ p (t) ∥_{2} \leq ∥ g ∥_{\infty} + a_{0} \int_{0}^{t} ∥ p (s) ∥_{2} d s$ , hence $∥ p ∥_{\infty} \leq E ∥ g ∥_{\infty}$ by [F4]. Every solution with initial value $ξ$ equals $U (t, 0) ξ + p (t)$ , since their difference solves the homogeneous linear IVP with initial value $ξ$ and uniqueness [F3] applies.

3.1F1F2step 1.1step 2.1step 2.2algebra

The boundary condition for this solution is $J ξ + B_{2} p (1) = q$ by step 2.1. Thus its unique initial value is $ξ = J^{- 1} (q - B_{2} p (1))$ . Writing $D = ∥ (g, q) ∥_{Z} = \max (∥ g ∥_{\infty}, ∥ q ∥_{2})$ gives $∥ ξ ∥_{2} \leq K_{J} (1 + ∥ B_{2} ∥_{2} E) D$ and, by steps 1.1–2.2, $∥ v ∥_{\infty} \leq [E K_{J} (1 + ∥ B_{2} ∥_{2} E) + E] D$ .

4.1F1step 2.1step 2.2step 3.1algebra∎

Since $v^{'} = A v + g$ , $∥ v^{'} ∥_{\infty} \leq a_{0} ∥ v ∥_{\infty} + D$ . The definition of the $X$ norm now gives $∥ v ∥_{X} \leq K_{L} D$ . Steps 2.1–2.2 construct a solution for every $(g, q)$ ; any solution is determined by $ξ$ and the invertible matrix $J$ , so it is unique. Hence $L$ is bijective with the stated inverse bound.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Multiple-shooting and midpoint-collocation residuals for a phase-fixed periodic orbit

Definition

Use the augmented state $u = (x, θ) \in U \times (0, \infty)$ , field $\tilde{f} (u) = (θ f (x), 0)$ , and boundary residual $B (u_{0}, u_{N}) = (x_{N} - x_{0}, ψ (x_{0}))$ from The phase-bordered periodic-orbit BVP residual. On a mesh $0 = s_{0} < \dots < s_{N} = 1$ , write $u_{i} = (x_{i}, θ_{i})$ .

The endpoint-pair boundary residual and square BVP convention are those of Square nonlinear two-point boundary-value problems and endpoint residuals. The exact multiple-shooting residual has segment rows

Φ_{s_{i + 1} - s_{i}} (u_{i}) - u_{i + 1} (0 \leq i < N)

and final row $B (u_{0}, u_{N})$ , where $Φ_{h}$ is the exact flow of $\tilde{f}$ . Its finite-budget candidate procedure is Finite-budget multiple shooting for a nonlinear two-point BVP on this augmented BVP.

For uniform $h = 1 / N$ , the normalized midpoint-collocation residual has rows

\frac{u_{i + 1} - u_{i}}{h} - \tilde{f} ⁣ (\frac{u_{i} + u_{i + 1}}{2}) (0 \leq i < N)

and final row $B (u_{0}, u_{N})$ . This is Normalized implicit-midpoint collocation residual for a two-point BVP for the same augmented BVP; its finite-budget candidate procedure is Finite-budget implicit-midpoint collocation for a nonlinear BVP. Both systems are square: the state dimension is $d + 1$ , with $d + 1$ boundary equations.

DefinitionDefinition: AI-adaptedProof: Not applicableOpen item page →

Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting

Definition

Let $f (x, μ)$ be $C^{2}$ on an open set in $R^{d} \times R^{p}$ , let $q = (x, μ)$ , and set $g (q) = (f (x, μ), 0_{p})$ . Write $P q = x$ . For each fixed $μ$ , let $Φ_{θ} (q)$ be the time- $θ$ flow of $q^{'} = g (q)$ , so its parameter coordinates remain constant. For an affine phase $ψ (x) = c^{⊤} (x - x_{r e f})$ , define

G (q, θ) = [\begin{array}{c} P Φ_{θ} (q) - P q \\ ψ (P q) \end{array}] .

For $p = 0$ and $c \neq 0$ this is the shooting residual in The phase-bordered periodic-orbit BVP residual. Its Jacobian is

D G (q, θ) = [\begin{array}{cc} P M - P & f (P Φ_{θ} (q), μ) \\ c^{⊤} P & 0 \end{array}], M = D_{q} Φ_{θ} (q) .

For a rational box $Q = X \times Λ \times Θ$ with $Θ \subset (0, \infty)$ , a validated shooting jet enclosure consists of: (i) a box containing $P Φ_{θ} (q)$ for every $q, θ$ in the input; (ii) a box containing the residual $G (Q)$ ; (iii) an interval matrix $J (Q)$ containing every $D G (q, θ)$ ; and (iv) trajectory and monodromy boxes containing every scaled trajectory $P Φ_{θ s} (q)$ , $0 \leq s \leq 1$ , and the physical-state block of $M$ . The input and range-oracle boxes may have arbitrary rational endpoints, as in Exact range-oracle contract for validated flow and monodromy enclosures. The returned interval enclosures have finite dyadic endpoints under Real boxes and interval Jacobian enclosures. Before applying dyadic interval arithmetic, round every rational operand outward to finite dyadic endpoints using Directed dyadic rounding encloses with explicit underflow and overflow bounds, then use Finite real interval operations enclose their exact values; exact rational set operations in the Euler provider remain exact. If any conversion overflows or is unavailable within the supplied cap, return inconclusive. The exact derivative formula follows from Derivative of the nonlinear shooting residual, and its flow sensitivity is on the common tube of Initial-data sensitivity of an ODE flow on a common compact tube. A finite success record is admissible only when obtained by the range-oracle procedure of Validated forward-Euler tube for the periodic flow and variational equation, whose exact flow and monodromy enclosure is guaranteed by The validated Euler tube encloses the exact periodic flow and monodromy matrix, with all queries and interval operations successful and outward under Exact range-oracle contract for validated flow and monodromy enclosures. For this call instantiate that procedure and its soundness theorem with state dimension $n = d + p$ , initial state box $X \times Λ$ , field $g (q) = (f (x, μ), 0_{p})$ , and period interval $Θ$ . Its augmented field is $H_{g} (q, Z, θ) = (θ g (q), θ D g (q) Z, 0)$ with $Z \in R^{n \times n}$ ; the supplied range provider is for this $H_{g}$ on its actual compact convex rational tube $K_{g} \subset R^{n + n^{2} + 1}$ . Initialize $Y_{0} = (X \times Λ) \times {I_{n}} \times Θ$ and require every Euler tube query and inclusion check in this same $K_{g}$ to succeed. Retain the full $n \times n$ endpoint variation enclosure for $M = D_{q} Φ_{θ} (q)$ when forming $P M - P$ : its first $d$ rows include both the state and parameter sensitivity columns, while its lower parameter rows are $(0, I_{p})$ because the parameters are constant. The physical monodromy is the first $d$ rows and first $d$ columns of $M$ .

To enclose the period column, let $X_{T}$ be the first $d$ coordinate projection of the successful endpoint enclosure $Y_{N}$ . The exact augmented endpoint lies in $X_{T} \times Λ$ : its parameter equals its initial value in $Λ$ , even if a returned interval coordinate is wider. Form the rational query box $Q_{T} = (X_{T} \times Λ) \times {I_{n}} \times Θ$ and check $Q_{T} \subseteq K_{g}$ before requesting $H_{g}^{#} (Q_{T})$ from that same supplied provider. If the inclusion or query fails, return inconclusive. The first $d$ entries of its vector-field block enclose every $θ f (P Φ_{θ} (q), μ)$ ; divide these entries outward by the positive interval $Θ$ to enclose the entire period column. Thus the query includes every admitted parameter and the matching augmented identity. For $p = 0$ , $n = d$ and the parameter factor is the singleton empty tuple, giving the fixed-parameter construction. These residual/Jacobian boxes are in the named coordinate order $(q, θ) = (x, μ, θ)$ ; a section callback whose variables are ordered $(x, θ, μ)$ applies that fixed column permutation before appending its affine section row. Any unavailable query or inclusion returns inconclusive. A finite Newton, multiple-shooting, or collocation residual alone is not a validated jet enclosure.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Periodic midpoint collocation has an explicit local second-order error budget

Statement

Consider the augmented phase-fixed BVP of The phase-bordered periodic-orbit BVP residual on $[0, 1]$ , with exact solution $u_{*} \in C^{3}$ , field $\tilde{f}$ , and affine boundary map $B$ . Put $M_{2} = ∥ u_{*}^{''} ∥_{\infty}, M_{3} = ∥ u_{*}^{'''} ∥_{\infty}, L_{f} = \sup ∥ D \tilde{f} ∥_{2}, C_{0} = M_{3} / 24 + L_{f} M_{2} / 8.$ For every admitted mesh cell with midpoint $m_{i}$ , assume the segment joining $u_{*} (m_{i})$ to $(u_{*} (t_{i}) + u_{*} (t_{i + 1})) / 2$ lies in the field domain and $∥ D \tilde{f} ∥_{o p} \leq L_{f}$ on that segment. Let $G_{h}$ be the normalized midpoint residual on a uniform mesh and $Y^{*}$ the samples of $u_{*}$ . Suppose that for all $0 < h \leq h_{0}$ , $J_{h} = D G_{h} (Y^{*})$ is invertible with $∥ J_{h}^{- 1} ∥_{\infty \to \infty} \leq K$ , and on a fixed-radius ball of radius $r$ about $Y^{*}$ the maps $D G_{h}$ are $L_{G}$ -Lipschitz in the block maximum norm. Assume $2 K L_{G} r \leq 1 / 2$ , $K C_{0} h^{2} \leq r / 2$ , and $2 K^{2} L_{G} C_{0} h^{2} \leq 1 / 2$ . Then $G_{h}$ has a unique zero $Y_{h}$ in that ball. Every candidate $Y$ in the ball satisfying $∥ G_{h} (Y) ∥_{\infty} \leq ε$ obeys

∥ P_{h} Y - u_{*} ∥_{\infty} \leq 4 K ε + (2 K C_{0} + \frac{M_{2}}{8}) h^{2},

where $P_{h}$ is linear interpolation of the node values. Thus the residual and discretization constants are explicit in the supplied derivative and inverse bounds. For the augmented state, the estimate includes both the orbit coordinates and the period coordinate.

Facts & Assumptions

Given: The exact augmented solution, uniform mesh, normalized midpoint residual, bounds $M_{2}, M_{3}, L_{f}, K, L_{G}$ , and the stated radius and mesh inequalities.

[F1]

The midpoint residual has rows $(u_{i + 1} - u_{i}) / h - \tilde{f} ((u_{i} + u_{i + 1}) / 2)$ and the phase-periodic boundary row (Normalized implicit-midpoint collocation residual for a two-point BVP, Multiple-shooting and midpoint-collocation residuals for a phase-fixed periodic orbit).

[F2]

For a BVP with a boundedly invertible continuous linearization, its sampled midpoint Jacobian has a uniform inverse bound (A transverse phase border makes the periodic BVP linearization boundedly invertible, Uniform inverse bound for the sampled midpoint linearized BVP); here the explicit $K$ is assumed as a supplied upper bound for those discrete inverses.

[F3]

A contraction of a nonempty complete metric space into itself has a unique fixed point (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point). The closed ball in the node space is complete: a block-maximum Cauchy sequence is Cauchy in each of its finitely many Euclidean blocks, each block converges by $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ , and the finite maximum of the block errors tends to zero; closedness keeps the limit in the ball.

[F4]

If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz gives the componentwise integral of a continuous vector derivative. 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 bounds the Euclidean norm of that integral. Reversed integration limits use The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ . Apply these in each output block; taking the finite maximum preserves the same bound in the block maximum norm.

[F5]

If $∥ J^{- 1} (A - J) ∥ \leq 1 / 2$ , the perturbed operator is invertible with inverse norm at most $2 ∥ J^{- 1} ∥$ (Neumann series and small perturbations of bounded inverses).

[F6]

The chain rule differentiates a composition of totally differentiable maps (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F7]

The fundamental theorem of calculus applies coordinatewise to a continuously differentiable vector curve, and the norm of a Euclidean vector-valued integral is at most the integral of the norm (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)$ , 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).

Proof

1.1F1F4F6F7givenalgebra

On a mesh cell centered at $m_{i}$ , repeated vector FTC gives $u_{*}^{'} (m_{i} + s) = u_{*}^{'} (m_{i}) + s u_{*}^{''} (m_{i}) + r (s)$ , where $r (s) = \int_{0}^{s} \int_{0}^{v} u_{*}^{'''} (m_{i} + w) d w d v$ . For negative limits reverse their orientation before applying the norm inequality. Thus $∥ r (s) ∥_{2} \leq M_{3} ∣ s ∣^{2} / 2$ . Averaging over $[- h / 2, h / 2]$ cancels the odd term and gives a difference-quotient defect at most $M_{3} h^{2} / 24$ . Applying the same integral argument to $u_{*}$ at $m_{i} \pm h / 2$ bounds each first-order remainder by $M_{2} h^{2} / 8$ ; their average therefore bounds the endpoint-average displacement from $u_{*} (m_{i})$ by $M_{2} h^{2} / 8$ . Integrating $D \tilde{f}$ on the connecting segment bounds the corresponding field difference by $L_{f} M_{2} h^{2} / 8$ . The affine boundary residual is zero. Taking the maximum of the cell bounds gives $∥ G_{h} (Y^{*}) ∥_{\infty} \leq C_{0} h^{2}$ .

2.1F2F3F4F6F7step 1.1given

Define $T_{h} (Y) = Y - J_{h}^{- 1} G_{h} (Y)$ . The Jacobian Lipschitz bound gives $∥ T_{h} (Y) - T_{h} (Z) ∥_{\infty} \leq K L_{G} r ∥ Y - Z ∥_{\infty} \leq \frac{1}{4} ∥ Y - Z ∥_{\infty}$ on the ball. Also $∥ T_{h} (Y^{*}) - Y^{*} ∥_{\infty} \leq K C_{0} h^{2} \leq r / 2$ , so $T_{h}$ maps the ball into itself. By [F3], it has a unique fixed point $Y_{h}$ , and invertibility of $J_{h}$ makes fixed points exactly the zeros of $G_{h}$ . The fixed-point equation also gives $∥ Y_{h} - Y^{*} ∥_{\infty} \leq K C_{0} h^{2} / (1 - 1 / 4) \leq 2 K C_{0} h^{2}$ .

3.1F5step 2.1given

The perturbation bound $∥ D G_{h} (Y_{h}) - J_{h} ∥ \leq L_{G} ∥ Y_{h} - Y^{*} ∥$ implies $∥ J_{h}^{- 1} (D G_{h} (Y_{h}) - J_{h}) ∥ \leq 2 K^{2} L_{G} C_{0} h^{2} \leq 1 / 2$ . The small-perturbation inverse bound [F5] therefore gives $D G_{h} (Y_{h})^{- 1}$ with norm at most $2 K$ .

4.1F6F7step 3.1givenalgebra

Put $δ = Y - Y_{h}$ and define $R (t) = G_{h} (Y_{h} + t δ) - G_{h} (Y_{h}) - t D G_{h} (Y_{h}) δ$ for $0 \leq t \leq 1$ . The segment lies in the ball. By the chain rule [F6], $R' (t) = (D G_{h} (Y_{h} + t δ) - D G_{h} (Y_{h})) δ$ , so the Lipschitz bound gives $∥ R' (t) ∥_{\infty} \leq L_{G} t ∥ δ ∥_{\infty}^{2}$ . For each Euclidean block index $j$ , [F7] gives $∥ R_{j} (1) ∥_{2} \leq \int_{0}^{1} ∥ R_{j}' (t) ∥_{2} d t \leq \int_{0}^{1} ∥ R' (t) ∥_{\infty} d t$ ; taking the finite maximum over $j$ gives $∥ R (1) ∥_{\infty} \leq \int_{0}^{1} ∥ R' (t) ∥_{\infty} d t \leq (L_{G} / 2) ∥ δ ∥_{\infty}^{2}$ . Thus $G_{h} (Y) = D G_{h} (Y_{h}) (Y - Y_{h}) + R (1)$ with this remainder bound. Since both vectors lie in the radius- $r$ ball, $∥ Y - Y_{h} ∥_{\infty} \leq 2 r$ , and $2 K L_{G} r \leq 1 / 2$ yields $∥ Y - Y_{h} ∥_{\infty} \leq 2 K ε + \frac{1}{2} ∥ Y - Y_{h} ∥_{\infty}$ . Hence $∥ Y - Y_{h} ∥_{\infty} \leq 4 K ε$ .

5.1F4step 2.1step 4.1givenalgebra∎

Linear interpolation is a convex combination, so $∥ P_{h} (Y - Y_{h}) ∥_{\infty} \leq ∥ Y - Y_{h} ∥_{\infty}$ . On a cell $[a, b]$ of length $h$ , repeated FTC gives $u_{*} (t) - P_{h} Y^{*} (t) = - \int_{a}^{b} K_{t} (s) u_{*}^{''} (s) d s$ , where $K_{t} (s) = (b - t) (s - a) / h$ for $s \leq t$ and $K_{t} (s) = (t - a) (b - s) / h$ for $s \geq t$ . This kernel is nonnegative and has integral $(t - a) (b - t) / 2 \leq h^{2} / 8$ , so [F4] gives the interpolation bound $M_{2} h^{2} / 8$ . The sample error of $Y_{h}$ is at most $2 K C_{0} h^{2}$ by step 2.1. Combining these bounds with step 4.1 proves the displayed estimate.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

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.

LemmaStatement: AI-adaptedProof: AI-adaptedOpen item page →

Rational boxes admit dyadic enclosure boundaries and exact affine root charts

Statement

For nonempty closed intervals with finite rational endpoints, the exact endpoint formulas $[a, b] + [c, d] = [a + c, b + d], [a, b] - [c, d] = [a - d, b - c],$ and the four-corner minimum and maximum for multiplication enclose every corresponding exact scalar value. Division uses the reciprocal interval $[1 / d, 1 / c]$ only when $0 \notin [c, d]$ . Every endpoint obtained in a finite such expression is rational. Replacing an exact rational interval $[l, u]$ by $[rd (l), ru (u)]$ in a selected dyadic format preserves inclusion whenever both returned endpoints are finite; a failed operation, unavailable exact computation, or overflow gives no finite-enclosure claim. This applies entrywise to vectors and matrices. For a point vector enclosure with midpoint $\hat{v}$ and coordinate radii $r_{i}$ , $\sum_{i} r_{i}$ bounds the Euclidean error of $\hat{v}$ . For a point matrix enclosure with midpoint $\hat{A}$ and entry radii $s_{i j}$ , $\sum_{i, j} s_{i j}$ bounds its Euclidean operator error. If a rational matrix $V$ is checked to satisfy $V \hat{A} = \hat{A} V = I$ , then $\sum_{i, j} ∣ V_{i j} ∣$ bounds $∥ {\hat{A}}^{- 1} ∥_{o p}$ .

Let $N \geq 1$ , let $Z = \prod_{j = 1}^{N} [a_{j}, b_{j}]$ have finite rational endpoints with $a_{j} < b_{j}$ , put $D = diag (b_{j} - a_{j})$ , and set $T (u) = a + D u$ . Then $T$ maps the dyadic box $B = [0, 1]^{N}$ bijectively onto $Z$ , maps closed subboxes and their midpoints to their exact rational images and midpoints, and maps every finite covering partition of $B$ to a covering partition of $Z$ . If $F : V \to R^{N}$ is $C^{1}$ on an open convex neighborhood $V$ of $Z$ , then $\hat{F} = F \circ T$ is $C^{1}$ on the open convex neighborhood $T^{- 1} (V)$ of $B$ , with $D \hat{F} (u) = D F (T (u)) D .$ A residual enclosure for $F (T (m))$ encloses $\hat{F} (m)$ , and a physical Jacobian enclosure $J (T (A))$ on a subbox $T (A)$ gives a normalized Jacobian enclosure $J (T (A)) D$ on $A$ , evaluated by the preceding rational endpoint rules and converted outward to finite dyadic intervals. Zeros and root-free, existence, and uniqueness conclusions transfer bijectively between each subbox $A$ and $T (A)$ ; no assumption about an ordering of roots is needed. If $C$ and $C D F (T (u)) D$ are nonsingular, then $D F (T (u))$ is nonsingular as well.

Facts & Assumptions

Given: The finite rational interval data, the selected dyadic format, and, for the chart assertions, the positive side lengths, $F, V, T, B, D$ in the Statement.

[F1]

The rationals form an ordered field, so finite sums, products and division by nonzero rationals remain rational (The rationals form a totally ordered field).

[F2]

An exact rational intermediate can be converted by exact numerator/denominator comparison to the selected format's greatest lower and least upper representable values; overflow is explicit (Dyadic floating-point format and directed rounding).

[F3]

Directed roundings enclose each finite exact value; overflow does not give two finite endpoints (Directed dyadic rounding encloses with explicit underflow and overflow bounds).

[F4]

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

[F5]

Cauchy–Schwarz and the Euclidean norm imply $∣ x_{j} ∣ \leq ∥ x ∥_{2}$ and $∥ x ∥_{2} \leq \sum_{j} ∣ x_{j} ∣$ for finite real vectors (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

Proof

1.1givenF1algebrainduction

For addition and subtraction, the scalar order inequalities give the displayed endpoint bounds. For multiplication with one argument fixed, the product is affine in the other argument and lies between its two endpoint values; repeating this for the first argument bounds every product by the minimum and maximum of the four corners. On an interval not containing zero, the reciprocal function reverses order, so its values lie in $[1 / d, 1 / c]$ ; multiplication then gives division bounds. Each endpoint is rational by [F1]. Induction over a finite expression applies these bounds to every actual predecessor value, so every exact expression value lies in the computed rational enclosure. A domain failure or unavailable operation ends this assertion.

1.2givenF5algebra

An enclosed vector differs from its midpoint by coordinate errors of magnitude at most $r_{i}$ , so [F5] bounds its Euclidean error by $\sum_{i} r_{i}$ . If a matrix error $E$ has $∣ E_{i j} ∣ \leq s_{i j}$ and $∥ x ∥_{2} = 1$ , then $∣ x_{j} ∣ \leq 1$ and $∥ E x ∥_{2} \leq \sum_{i} ∣ (E x)_{i} ∣ \leq \sum_{i, j} s_{i j}$ . Taking the supremum over unit vectors proves the matrix-error bound. The same calculation for the exact inverse matrix $V$ gives $∥ V ∥_{o p} \leq \sum_{i, j} ∣ V_{i j} ∣$ ; its two checked inverse identities identify it with ${\hat{A}}^{- 1}$ . These estimates are conservative and finite, not relative-error assertions.

1.3givenF1algebra

Each $d_{j} = b_{j} - a_{j}$ is positive. The inverse $T^{- 1} (z)_{j} = (z_{j} - a_{j}) / d_{j}$ is well-defined and sends $[a_{j}, b_{j}]$ bijectively onto $[0, 1]$ . Hence $T (B) = Z$ bijectively. For a subbox $A = \prod_{j} [l_{j}, u_{j}]$ , positivity gives $T (A) = \prod_{j} [a_{j} + d_{j} l_{j}, a_{j} + d_{j} u_{j}]$ ; its endpoints are rational when those of $A$ are dyadic or rational. Affineness gives $T ((l + u) / 2) = (T (l) + T (u)) / 2$ . Images commute with unions and preserve intersections under a bijection, so finite coverage and disjoint interiors of partitions transfer, including shared bisection faces.

2.1givenF2F3step 1.1algebra

If the rational result is $[l, u]$ and both directed endpoints are finite, [F2] and [F3] give $rd (l) \leq l \leq u \leq ru (u)$ . Thus its dyadic replacement contains the full rational enclosure and every exact value established in step 1.1. Apply this separately to each coordinate or matrix entry. An overflow sentinel is not a finite interval and cannot supply the finite-return assertion.

3.1givenF4step 1.1step 2.1step 1.3algebra

The affine maps $T$ and its displayed inverse are continuously differentiable with constant derivatives $D$ and $D^{- 1}$ . Thus $T^{- 1} (V)$ is open, is convex because affine maps preserve segments, and contains $B$ . By [F4], $D \hat{F} (u) = D F (T (u)) D$ . A point residual enclosure therefore applies unchanged to $\hat{F} (m)$ . On $A$ , every physical derivative lies entrywise in $J (T (A))$ and right multiplication by $D$ multiplies column $j$ by the positive scalar $d_{j}$ ; steps 1.1 and 2.1 give the stated finite dyadic enclosure. No transformed point is queried outside the original physical box.

4.1givenstep 1.3step 3.1algebra∎

The identity $\hat{F} (u) = F (T (u))$ and the bijection in step 1.3 identify each zero in $A$ with exactly one zero in $T (A)$ . Empty-root, at-least-one-root and at-most-one-root statements therefore transfer in both directions, and finite partition coverage transfers as well. Finally write $J = D F (T (u))$ and $A = C J D$ . If $A$ and $C$ are nonsingular, then $D A^{- 1} C$ is a two-sided inverse for $J$ : $J D A^{- 1} C = C^{- 1} A A^{- 1} C = I$ and $D A^{- 1} C J = D A^{- 1} A D^{- 1} = I$ . This proves the last assertion using the explicit invertibility of $D$ , without a norm comparison between physical and normalized coordinates.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Finite-budget phase-fixed periodic-orbit correction and validation

Definition

For a state dimension $d \geq 1$ , the vector-field input is a $C^{2}$ map $f : U \to R^{d}$ in fixed-parameter mode or a $C^{2}$ one-parameter family $f : U \times V \to R^{d}$ with scalar parameter $μ \in V \subset R$ in section mode, where $U \subset R^{d}$ and $V \subset R$ are open. Also supply an affine phase with nonzero rational covector and rational reference point, a compact convex validation tube, and the sound range provider of Exact range-oracle contract for validated flow and monodromy enclosures. Supply positive finite step counts for each requested validated jet run, finite arithmetic and candidate-update budgets, a rational initial candidate, a dyadic point preconditioner $C$ , a rational inverse witness $W$ , a positive rational minimum box width $η$ , and a finite Krawczyk box budget. In fixed-parameter mode the rational candidate box is $Z = X \times Θ \subset U \times (0, \infty)$ with the parameter held fixed, so both the variable $z = (x, θ)$ and residual $F = G$ have dimension $d + 1$ . In section mode require exactly one scalar continuation parameter $μ \in R$ (the $p = 1$ case of Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting), take $Z = X \times Θ \times Λ$ with rational $Λ \subset V \subset R$ , and set $z = (x, θ, μ)$ . Then $G$ has dimension $d + 1$ , the affine section adds one scalar equation, and both $z$ and $F$ have dimension $d + 2$ . Independent validation retains every admitted rational endpoint of $Z$ and uses the exact affine dyadic unit-box chart below; non-dyadic physical endpoints are not a failure condition. Supply an open convex shooting domain containing $Z$ on which the exact flow exists through every admitted positive period, so $F$ is $C^{1}$ there. All rational point, endpoint, interval and matrix operations below are exact or return an explicit arithmetic-failure status within the supplied cap.

Write $F = G$ in fixed-parameter mode. In section mode, used for continuation, require one scalar continuation parameter $μ \in R$ and write $z = (x, θ, μ)$ and $F (z) = (G (x, θ, μ), τ^{⊤} (z - z_{p}))$ , where $G$ is the parameterized map in Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting, $τ$ is a supplied unit normal, and $z_{p}$ is a supplied predictor. Supply certified rational enclosures for the coefficients and constant term of this affine row at every requested accuracy; if they are rational use their exact values, and otherwise use outward interval arithmetic. If a finite row enclosure cannot be obtained within the arithmetic cap, return inconclusive. For the one-parameter field use the static-parameter augmentation $g (x, μ) = (f (x, μ), 0)$ in that definition and supply its sound augmented range provider and tube. For every section-mode jet query, first reorder its input $(x, θ, μ)$ to $(q, θ) = (x, μ, θ)$ . Reorder the returned Jacobian columns from $(x, μ, θ)$ to $(x, θ, μ)$ , leaving its residual rows unchanged. Then append a sound outward enclosure of the affine section row to every residual and Jacobian enclosure (the exact row when its data are rational). Apply this rule both to candidate updates and to every independent-validation callback. In fixed-parameter mode, $z = (x, θ)$ and $F = G$ both have dimension $d + 1$ ; in section mode, $z = (x, θ, μ)$ and $F = (G, τ^{⊤} (z - z_{p}))$ both have dimension $d + 2$ .

The procedure retains the following candidate modes; candidate generation alone never validates a root.

Enclosure-guided single shooting: this mode needs only the supplied range provider, not a pointwise differentiable numerical IVP evaluator. Start at the supplied rational $z_{0} \in Z$ . At each of at most the supplied number of updates, run the validated shooting-jet procedure of Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting on the singleton ${z_{k}}$ , using its validated Euler method and the supplied finite caps. If a tube, range, domain or arithmetic check fails, return its inconclusive status and the last candidate. Otherwise let $r_{k}$ and $A_{k}$ be the coordinatewise rational midpoints of the returned boxes for $F (z_{k})$ and $D F (z_{k})$ . Record $z_{k}$ as a candidate and attempt the independent validation below. If it does not validate and updates remain, call Newton correction for a square vector residual on $(A_{k}, r_{k})$ . A singular matrix returns singular-jacobian; otherwise its rational correction $u_{k}$ proposes $z_{k + 1} = z_{k} + u_{k}$ . Reject a proposal outside $Z$ with invalid-trial. The midpoint matrix is only a proposal matrix: it is not claimed to be the exact derivative of a numerical residual map. Exhaustion returns the last candidate and candidate-budget-exhausted.
Differentiable single shooting: supply, as an additional input for this mode, a certified differentiable evaluator satisfying Certified differentiable IVP approximation interface for shooting for the augmented BVP, including its approximate trajectories, $C^{1}$ endpoint map, exact numerical-map derivative, and uniform trajectory-error bound. Run Finite-budget single shooting for a nonlinear two-point BVP on the phase-bordered BVP. In section mode augment the state by the constant parameter and append the affine section condition to its boundary residual. An interval jet alone is not this additional evaluator; if it is absent, return evaluator-unavailable without making the call.
Discretized candidate: either run Finite-budget multiple shooting for a nonlinear two-point BVP on the augmented segment BVP with separately supplied certified differentiable segment evaluators satisfying the same interface, or run Finite-budget implicit-midpoint collocation for a nonlinear BVP using the pointwise field/boundary values and their exact derivatives required by its residual. Use the residuals of Multiple-shooting and midpoint-collocation residuals for a phase-fixed periodic orbit; in section mode include the constant parameter and affine section row. Missing pointwise/segment evaluation data returns evaluator-unavailable. Use the last finite tuple's first physical state and positive period (and parameter in section mode) as a shooting candidate. Reject a candidate outside $Z$ or a nonrational candidate without a supplied rational proposal; rationalization is only a new candidate, not a trajectory or residual certificate.

All modes propagate evaluator-failure, invalid-endpoint-pair, invalid-trial, singular-jacobian, inconclusive and exhausted-budget statuses. No candidate mode is assumed to succeed from arbitrary data. In particular, the first mode composes the available interval-enclosure provider directly; it does not infer a $C^{1}$ point evaluator from interval boxes.

Independent validation: retain the exact rational candidate box $Z = \prod_{j = 1}^{N} [a_{j}, b_{j}]$ in the declared physical variable order, where $N = d + 1$ or $d + 2$ . If any side is degenerate, return inconclusive for validation, retaining the candidate: a box with empty ambient interior cannot pass the strict-interior inclusion required for a unique-root return. Degenerate boxes remain admitted inputs, and candidate-generation queries may still use their rational singleton or lower-dimensional boxes. Otherwise put $D = diag (b_{j} - a_{j})$ , $T (u) = a + D u$ , $B = [0, 1]^{N}$ and $\hat{F} (u) = F (T (u))$ . Use the supplied open convex shooting domain containing $Z$ , where the exact residual is $C^{1}$ ; failure to certify that domain returns inconclusive. The chart has an open convex preimage domain, and $D \hat{F} (u) = D F (T (u)) D$ , by Rational boxes admit dyadic enclosure boundaries and exact affine root charts. Run Finite-budget multidimensional Krawczyk root certification on $\hat{F}$ and the finite dyadic box $B$ , using the supplied dyadic $C$ , rational $W$ , box budget and normalized minimum width $\hat{η} = η / \max_{j} (b_{j} - a_{j}) > 0$ . Here $C$ is used as a preconditioner for this normalized residual; no approximate-inverse quality was assumed of it. The witness check remains the exact check $W C = I$ . A normalized terminal box of maximum width at most $\hat{η}$ has physical image of maximum width at most $η$ ; the budget still bounds all processed boxes. For every processed dyadic subbox $A \subseteq B$ , let $m_{A}$ be its dyadic midpoint and set $Y = T (A)$ and $m_{Y} = T (m_{A})$ , the exact rational physical midpoint. The residual callback runs the validated shooting jet on ${m_{Y}}$ and appends the section-row enclosure when present. The Jacobian callback runs it on the rational box $Y$ , appends the physical affine section row when present, and multiplies column $j$ of this physical Jacobian enclosure by $D_{j j}$ . Exact rational endpoint operations followed by outward dyadic hull conversion give finite dyadic enclosures $F_{0} \supseteq \hat{F} (m_{A})$ and $\hat{J} (A) \supseteq D \hat{F} (A)$ . A failed conversion or overflow marks $A$ unresolved; it is never supplied as a finite interval. This uses the actual midpoint of the current normalized box, whose image is the actual midpoint of $Y$ , even when it differs from the candidate center. A failed query or tube inclusion marks that box unresolved. Normalized Krawczyk interval operations are outward under Finite real interval operations enclose their exact values. Retain the complete normalized Krawczyk output partition, including every terminal box and its status, and its exact physical image partition under $T$ . Status labels on physical images mean the corresponding root conclusions transferred by the affine bijection, not a Krawczyk computation with an unscaled physical Jacobian. Continue only if the overall Krawczyk status is complete, exactly one normalized terminal box $A_{Y}$ has status unique-root, and every other terminal box has status root-free; if there is no such unique box, more than one, or any existence-only/unresolved box, return inconclusive. Set $Y = T (A_{Y})$ . Let $X_{Y}$ and $Θ_{Y}$ be the physical-state and period projections of this rational unique-root image box, and include $Λ_{Y}$ in section mode. Form $Q_{Y} = (X_{Y} \times Λ_{Y}) \times {I_{d + p}} \times Θ_{Y}$ in section mode, or $Q_{Y} = X_{Y} \times {I_{d}} \times Θ_{Y}$ in fixed-parameter mode. Check $Q_{Y}$ is contained in the supplied augmented tube and query the same sound range provider for its augmented field enclosure. Divide the first $d$ coordinates by the positive interval $Θ_{Y}$ with exact rational endpoint arithmetic to obtain an interval box containing $f (X_{Y}, Λ_{Y})$ (or $f (X_{Y})$ in fixed-parameter mode). Require at least one component interval to exclude zero; if inclusion, query or division fails, or no component excludes zero, return inconclusive. Finally require a successful full-box jet run on $Y$ to enclose the entire trajectory and monodromy; a failed query or tube check returns inconclusive.

Return validated-root only for such a box $Y$ , and report it as the output box together with the complete terminal partition, the affine chart $(a, D)$ , unique normalized box $A_{Y}$ , the actual physical midpoint residual enclosure, physical Jacobian enclosure, normalized Jacobian enclosure, inverse witness, normalized strict inclusion and contraction inequalities, field component excluding zero, trajectory tube and monodromy enclosure. The bijection and complete mapped partition prove that $Y$ contains the only zero in the original rational box $Z$ . If subdivision was used the output box is $Y$ , not the original larger $Z$ . Otherwise return inconclusive or the precise finite candidate failure status. Candidate midpoints and correction residuals never replace the independently validated callback enclosures.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passOpen item page →

A separated simple Floquet multiplier has a left/right-conditioned finite enclosure

Statement

Let $A \in C^{n \times n}$ have an algebraically simple eigenvalue $λ_{0}$ , with right vector $v$ normalized by $∥ v ∥_{2} = 1$ and compatible left vector $w$ normalized by $w^{*} v = 1$ . Put $Q = I - v w^{*}$ , $W = \ker w^{*}$ , $q = ∥ Q ∥_{2}$ , and $κ = ∥ w ∥_{2}$ . The restriction $A_{W} = A ∣_{W}$ is well-defined. Let $D = {λ : ∣ λ - λ_{0} ∣ \leq ρ}$ be a disk such that every $λ \in D$ makes $λ I_{W} - A_{W}$ invertible and $R \geq \sup_{λ \in D} ∥ (λ I_{W} - A_{W})^{- 1} ∥_{2} < \infty .$ If $n \geq 2$ , $∥ E ∥_{2} \leq δ$ , and $R q^{2} δ < 1$ , then every eigenvalue $λ$ of $A + E$ in $D$ satisfies

∣ λ - λ_{0} ∣ \leq κ δ + \frac{κ q R δ^{2}}{1 - R q^{2} δ} .

When $A + E$ is a monodromy matrix, this bounds its Floquet multipliers lying in $D$ ; $A$ may be a numerical reference matrix. The formula is a finite nonnormal perturbation enclosure under the stated complementary-resolvent separation hypothesis; it supplies no enclosure for a cluster lacking that separation.

Facts & Assumptions

Given: A simple eigenvalue, compatible normalized left/right vectors, an isolating disk for the complementary restriction, and a perturbation norm bound.

[F1]

A simple eigenvalue admits compatible left and right eigenvectors whose pairing is nonzero and can be normalized to one (For a simple eigenvalue, left and right eigenvectors pair nontrivially and may be normalized by $y^{*} x = 1$ , Compatible left and right eigenvectors for a simple eigenvalue).

[F2]

The subspace $W = \ker w^{*}$ is invariant under $A$ , and $A$ has no eigenvalue $λ_{0}$ on $W$ because the full eigenvalue is simple (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism, Jordan form over the base field exists exactly when the characteristic polynomial splits).

[F3]

For any differentiable simple-eigenpair branch along $A + t E$ with compatible normalized eigenvectors equal to $v, w$ at $t = 0$ , the eigenvalue derivative there is $w^{*} E v$ (Along a differentiable matrix path, a simple eigenvalue satisfies $λ^{'} = y^{*} A^{'} x$ under the normalization $y^{*} x = 1$ ).

[F5]

The monodromy matrix and its eigenvalues are the Floquet data of the periodic orbit (Local periodic-orbit, Poincare-return, and Floquet data); a validated matrix enclosure is part of the shooting jet (Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting).

Proof

1.1F1F2givenalgebra

Since $w^{*} A = λ_{0} w^{*}$ , $W$ is invariant; since $A v = λ_{0} v$ and $w^{*} v = 1$ , every vector splits uniquely as $α v + y$ with $y \in W$ . The restriction has no eigenvalue $λ_{0}$ by algebraic simplicity. Also $Q$ is the projection onto $W$ . For $n \geq 2$ , its range is nonzero and $Q$ acts as the identity there, so $q \geq 1$ .

2.1givenstep 1.1algebra

Let $λ \in D$ be an eigenvalue of $A + E$ with eigenvector $x = α v + y$ , $y \in W$ . If $α = 0$ , projection onto $W$ gives $y = (λ I_{W} - A_{W})^{- 1} Q E y$ . Thus $∥ y ∥_{2} \leq R q δ ∥ y ∥_{2}$ , while $R q δ \leq R q^{2} δ < 1$ , forcing $y = 0$ , contrary to $x \neq 0$ . Hence $α \neq 0$ ; rescale the eigenvector so $α = 1$ .

3.1givenstep 2.1algebra

Projecting $(A + E) (v + y) = λ (v + y)$ onto $W$ gives $y = (λ I_{W} - A_{W})^{- 1} Q E (v + y)$ . Therefore $∥ y ∥_{2} \leq R q δ (1 + ∥ y ∥_{2})$ and $∥ y ∥_{2} \leq R q δ / (1 - R q δ)$ .

4.1F3F5step 1.1step 3.1algebra∎

Applying $w^{*}$ to the same eigen-equation gives $λ - λ_{0} = w^{*} E v + w^{*} E y$ . The first term, which [F3] identifies as the derivative along any differentiable normalized simple-eigenpair branch through $(λ_{0}, v, w)$ , has modulus at most $κ δ$ , while the second is at most $κ δ ∥ y ∥_{2}$ . Substituting step 3.1 gives the stronger denominator $1 - R q δ$ . Since $q \geq 1$ , $1 - R q^{2} δ \leq 1 - R q δ$ and both are positive, so replacing by the smaller denominator yields the stated bound. If $A + E$ is monodromy, [F5] identifies $λ$ as one of its Floquet multipliers. No monodromy property of $A$ alone is needed or sufficient for that interpretation.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Finite pseudo-arclength continuation of phase-fixed periodic orbits

Definition

Let $f (x, μ)$ be a $C^{2}$ one-parameter family in the map convention of $C^{k}$ Euclidean maps and diffeomorphisms, and let $G (x, T, μ)$ be the parameterized phase-bordered shooting map of Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting. For its static-parameter augmented field $g (x, μ) = (f (x, μ), 0)$ , supply the common-tube hypotheses of A $C^{2}$ vector field has a $C^{2}$ flow on a common compact tube on each continuation neighborhood: an open set of initial states whose solutions exist on an open interval containing the required period range and remain in one compact convex subset of the field domain. That theorem makes the shooting map $C^{2}$ on the declared neighborhood. The branch residual is $F = G : R^{d + 2} \to R^{d + 1}$ . If a fold check is requested, additionally supply a verified $C^{3}$ neighborhood of the shooting map $G$ on the fold subtube, as required by Finite-budget pseudo-arclength continuation with a certified local corrector; $C^{2}$ regularity of $f$ alone is not this evidence. Without it, retain fold status inconclusive and do not invoke the fold callback, while ordinary continuation may proceed without a fold request. A finite periodic-orbit continuation request supplies a valid certified Euclidean seed section-root ball with its isolating curve-chart neighborhood and rank certificate, as required by Finite-budget pseudo-arclength continuation with a certified local corrector, a unit orientation, step size, requested step count, finite continuation/corrector budgets, residual tolerance, angle margin, and the sound flow/jet range provider.

At a certified root, a tangent routine must certify a unit vector in $\ker D F$ and a rank- $d + 1$ condition. The predictor is advanced along that tangent. The periodic procedure Finite-budget phase-fixed periodic-orbit correction and validation in section mode supplies a separate Krawczyk certificate for the square shooting/section residual. Forward its complete finite input package: the candidate mode and any required differentiable pointwise/segment evaluators (or choose its enclosure-guided mode), rational initial candidate, arbitrary rational physical validation box and its open convex shooting domain, nonzero rational phase covector and rational reference point, validated-jet step counts and arithmetic caps, dyadic preconditioner and exact rational inverse witness for its normalized residual, physical minimum box width, and box/update budgets. It uses its affine dyadic unit-box chart for positive side lengths, retains the exact physical box and complete mapped partition, and returns inconclusive for validation on degenerate boxes while retaining their candidate use. For possibly nonrational tangent/predictor data, forward certified outward rational enclosures of the affine section row and its derivative; unavailable bounds return inconclusive. For every jet query reorder physical $(x, T, μ)$ to the jet's $(x, μ, T)$ coordinates, and return its Jacobian columns to $(x, T, μ)$ before appending a section row. Preserve this rule in candidate, Krawczyk and continuation-evaluator calls.

Run Finite-budget pseudo-arclength continuation with a certified local corrector using its actual exact-evaluation or bounded-error branch and its own certified Euclidean root balls. A periodic Krawczyk box alone is not its ball certificate. Use the generic exact-evaluation branch only with separately supplied exact physical point-evaluation data; interval jet enclosures alone use the bounded-error branch. The local inverse and chart suppliers remain A simple neutral multiplier and transverse phase make the shooting Jacobian invertible and A transverse pseudo-arclength section has a locally quadratic Newton corrector, with every generic tangent, previous-normal, chart-angle, predictor-offset and finite-budget check retained. Supply the following finite-return evaluator and ball-certificate interfaces; an unavailable input returns the generic declared failure rather than an accepted step.

Physical evaluator bridge. At each exact queried point $y = (x, T, μ)$ , obtain a certified finite rational box containing $y$ within the shooting domain and the declared physical continuation tube; use its singleton when $y$ is rational. Every augmented range-provider tube inclusion required by the jet is checked separately in its own augmented coordinates. A nonrational query requires supplied certified coordinate enclosures, not substitution of a nearby rational point. Run the validated jet on that physical box with the stated coordinate/column permutation. Its residual and physical Jacobian intervals enclose $F (y)$ and $D F (y)$ . Coordinatewise rational midpoints and the sums of the coordinate/entry radii give the generic evaluator's certified Euclidean residual error and operator-Jacobian error by Rational boxes admit dyadic enclosure boundaries and exact affine root charts. For its current affine section form the square residual $G (y) = (F (y), τ_{k}^{T} (y - z_{p}))$ and its physical Jacobian, appending sound interval enclosures of the affine row and its constant term; include all row uncertainty in the square midpoint/error data $\hat{g}, \hat{A}, ϵ_{g}, ϵ_{J}$ . These are derivatives in physical coordinates, not the normalized Krawczyk columns $D F D$ . If only normalized data are retained, undo their known positive diagonal chart exactly and enclose the physical columns before forming these bounds. Missing finite point/row/error enclosures returns root-certificate-inconclusive; a certified domain/tube exit keeps the generic tube-exit status.

Required Euclidean ball certificate. At a generic candidate $y$ , the callback supplies $R > 0$ , verifies that the whole ${\overline{B}}_{2} (y, R)$ lies in the declared smooth shooting domain, physical continuation tube and current isolating chart neighborhood $V_{k}$ , and supplies a sound finite $L \geq 0$ with $∥ D G (u) - D G (v) ∥_{o p} \leq L ∥ u - v ∥_{2}$ throughout that ball. This whole-ball bound is additional certified input, for example from a separately justified second-derivative bound on a covering tube. It is not inferred from first-derivative intervals, Krawczyk inclusion or the mere existence of a $C^{2}$ field. The callback supplies an exact rational inverse witness $V$ for the rational midpoint matrix $\hat{A}$ , checked by both products $V \hat{A} = \hat{A} V = I$ , or another sound inverse-bound certificate. For the exact witness take $\hat{β} = \sum_{i, j} ∣ V_{i j} ∣$ . Verify the actual tests of A bounded residual and derivative error give a local root certificate: $\hat{β} ϵ_{J} < 1, β = \frac{\hat{β}}{1 - \hat{β} ϵ_{J}}, ρ = ∥ \hat{g} ∥_{2} + ϵ_{g}, q = β L R < 1, β ρ \leq (1 - q) R .$ A certified upper bound for $∥ \hat{g} ∥_{2}$ may replace the norm conservatively. Only a passing ball with the full chart/angle record can be appended by the generic algorithm. Missing witness, whole-ball Lipschitz, domain, chart or error data returns root-certificate-inconclusive; finite arithmetic failures and all generic budget/status distinctions remain explicit. A small residual, an exhausted Newton budget or a successful periodic Krawczyk call alone cannot append a continuation ball. If both a generic ball and a physical Krawczyk box are claimed to represent the same section root, additionally certify inclusion of the entire ball in that Krawczyk unique-root image box, or provide another sound common-root certificate; otherwise retain them as separate records without claiming coincidence.

When the fixed-parameter phase-bordered $(x, T)$ Jacobian is certified invertible, the full derivative $D F$ has row rank $d + 1$ : its $(x, T)$ columns already span $R^{d + 1}$ . Thus a fold in the parameter projection does not by itself make the branch singular. Missing tangent/rank evidence, tube exit, failed Krawczyk inclusion, unresolved angle, or exhausted finite budgets returns the corresponding inconclusive status; no global branch-completeness claim is made. Any requested fold certificate is emitted only when the generic continuation algorithm's separate fold checks succeed.

The generic section keeps the supplied previous unit orientation fixed as its normal during each attempt, while the predictor uses the current certified tangent candidate. Forward this previous normal and certify its angle with the current true kernel, along with the generic predictor-offset/chart inequalities. Finite termination is conditional on every invoked flow/jet, tangent, section and fold callback returning in finite time; an outer work budget is not a timeout for a nonreturning callback.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Finite complex-contour validation of Floquet multiplier clusters

Definition

Input a positive integer $n$ , a nonempty complex matrix family $M$ enclosed entrywise by finite dyadic real/imaginary rectangles, a dyadic center matrix $M_{0}$ , a certified dyadic bound $δ_{A} \geq \sup_{M \in M} ∥ M - M_{0} ∥_{\infty, C}$ , and a simple positively oriented strictly convex polygon $Γ$ with dyadic vertices and filled interior $P$ . Supply the dyadic disk cover and point preconditioners required by Finite complex contour resolvent validator with cover and inconclusive statuses, a positive integer $N$ for midpoint subdivisions of each edge, a positive integer $K_{π}$ for the arctangent series, and a finite arithmetic budget. The family may be the monodromy block of a validated shooting jet; no correlation between matrix entries is required. A complex rectangle here is the product of one closed dyadic real interval and one closed dyadic imaginary interval for each matrix entry.

Write the ordered dyadic vertices as $v_{0}, \dots, v_{r - 1}$ , with indices modulo $r$ . Require $r \geq 3$ , pairwise distinct vertices, and, for every $i$ and every $k \notin {i, i + 1}$ , the exact rational determinant $Im (\overline{(v_{i + 1} - v_{i})} (v_{k} - v_{i})) > 0$ . Each directed edge is then an exposed edge of the convex hull; since there are $r$ such edges and $r$ distinct vertices, they form its simple counterclockwise boundary. If any test fails, output inconclusive. Then run the resolvent-cover validator on every edge for the entire family. If any segment is uncovered, an outward inequality is not strict, or no finite upper bound $M_{R}$ on $∥ (z I - M)^{- 1} ∥_{\infty, C}$ is returned, output inconclusive.
Subdivide each oriented edge $e_{j} = b_{j} - a_{j}$ into $N$ equal parts, with rational midpoints $z_{j k} = a_{j} + (k + 1 / 2) e_{j} / N$ . By exact rational complex elimination, compute $R_{j k}^{0} = (z_{j k} I - M_{0})^{- 1}$ ; a singular center matrix or an incomplete operation returns inconclusive. For each rational complex entry $a + i b$ of $R_{j k}^{0}$ , use rational square-root bisection to find an upper bound for $\sqrt{a^{2} + b^{2}}$ , then sum row bounds to obtain $b_{j k} \geq ∥ R_{j k}^{0} ∥_{\infty, C}$ . Use the same bisection to obtain $s_{j} \geq ∣ e_{j} ∣$ . If the finite budget does not produce these rational bounds, return inconclusive.
Form the exact center midpoint sum $S_{0} = \sum_{j} \frac{e_{j}}{N} \sum_{k = 0}^{N - 1} tr R_{j k}^{0},$ and the outward error allowance $E = \frac{n M_{R}^{2}}{2 N} \sum_{j} ∣ e_{j} ∣^{2} + \frac{n M_{R} δ_{A}}{N} \sum_{j, k} s_{j} b_{j k} .$ The first term uses the exact rational squared modulus of each rational edge; the second uses the rational upper edge length $s_{j}$ . The first term bounds midpoint quadrature error; the second bounds replacing each family resolvent by the center resolvent. All sums and products are exact rationals; if a required rational square-root upper bound is unavailable, return inconclusive.
Enclose $π$ using $π = 4 \arctan (1)$ and the alternating partial sum $4 \sum_{k = 0}^{K_{π} - 1} (- 1)^{k} / (2 k + 1)$ with tail radius $4 / (2 K_{π} + 1)$ . Require a positive lower endpoint. Using exact rational endpoint arithmetic, enclose $S_{0} / (2 π i)$ and inflate its real and imaginary intervals by $E / (2 π_{l o w})$ ; call the resulting rectangle $I$ .
Choose an integer $c$ and return certified-count(c) only if $0 \leq c \leq n$ , $Re I \subset (c - 1 / 2, c + 1 / 2)$ , $Im I \subset (- 1 / 2, 1 / 2)$ , and $0 \in Im I$ . Otherwise return inconclusive. This operation counts roots with algebraic multiplicity in $int P$ for every matrix in the supplied family; it does not classify a cluster touching the unit circle as stable or unstable.

For a simple separated multiplier, an optional left/right-conditioned finite enclosure may also be reported using A separated simple Floquet multiplier has a left/right-conditioned finite enclosure. The contour count remains the required path for clusters or unresolved individual eigenvectors.

The matrix family may be taken from the monodromy block of Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting. Resolvent bounds use the complex infinity norm The complex induced infinity matrix norm and its product inequality The complex infinity matrix norm is compatible and submultiplicative; the boundary cover is interpreted by The finite disk cover validator returns a uniform resolvent bound on success. Root counting uses The argument principle for an admissible null-homologous cycle, the inside/outside polygon index A positively oriented convex polygon has winding index one inside and zero outside, and the determinant derivative The determinant differential is $D \det (A) [H] = tr (adj (A) H)$ at every matrix, and Jacobi's formula holds on the invertible locus. The root multiplicities are those of the characteristic polynomial by A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity. The rational $π$ enclosure uses Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series and The alternating series test: if $(b_{k})$ is nonincreasing with $b_{k} \to 0$ then $\sum_{k} (- 1)^{k} b_{k}$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_{n}$ .

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

A verified contour count encloses every Floquet multiplier in a cluster

Statement

If Finite complex-contour validation of Floquet multiplier clusters returns certified-count(c) for a nonempty matrix family $M$ and a simple positively oriented convex polygon $Γ$ , then every $M \in M$ has exactly $c$ eigenvalues in $int P$ , counted with algebraic multiplicity, and no eigenvalue on $Γ$ . In particular, this holds for every exact monodromy matrix enclosed by a validated shooting jet whose interval block is contained in $M$ .

Facts & Assumptions

Given: A successful count record, its outward interval arithmetic, its resolvent-cover result, the matrix family, and the positive polygon.

[F1]

A successful resolvent-cover validation bounds $∥ (z I - M)^{- 1} ∥_{\infty, C}$ uniformly on each covered edge and for all $M \in M$ (The finite disk cover validator returns a uniform resolvent bound on success).

[F2]

For an invertible matrix $A$ , the determinant derivative in direction $H$ is $D \det (A) [H] = \det (A) tr (A^{- 1} H)$ (The determinant differential is $D \det (A) [H] = tr (adj (A) H)$ at every matrix, and Jacobi's formula holds on the invertible locus).

[F3]

The argument principle counts zeros of a holomorphic function by the logarithmic-derivative contour integral with winding-number weights (The argument principle for an admissible null-homologous cycle); for the positive convex polygon the index is one inside and zero outside (A positively oriented convex polygon has winding index one inside and zero outside).

[F4]

Eigenvalues are exactly the roots of the characteristic polynomial (For every finite-dimensional space, $σ_{F} (T)$ is exactly the set of roots in $F$ of $χ_{T}$ ). Algebraic multiplicity means the multiplicity of the corresponding polynomial root. The characteristic polynomial of an $n \times n$ matrix is monic of degree $n$ ( $χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ ), so it has $n$ complex roots counted with multiplicity (A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity).

[F5]

The identity $π = 4 \arctan (1)$ and the alternating-series remainder bound justify the rational interval for $π$ (Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series, The alternating series test: if $(b_{k})$ is nonincreasing with $b_{k} \to 0$ then $\sum_{k} (- 1)^{k} b_{k}$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_{n}$ ); all later endpoint operations are exact rational arithmetic.

[F6]

The finite procedure verifies the resolvent cover, midpoint subdivisions, sample inverses, error terms and strict integer-neighborhood test before returning a count (Finite complex-contour validation of Floquet multiplier clusters).

[F7]

The complex infinity matrix norm is submultiplicative (The complex infinity matrix norm is compatible and submultiplicative).

[F8]

Under $C ≅ R^{2}$ , a continuously differentiable complex-valued curve whose modulus of the derivative is bounded by $L$ changes by at most $L$ times the interval length (The mean value inequality: if $f : [a, b] \to R^{m}$ is continuous and differentiable on $(a, b)$ with $∥ f^{'} ∥_{2} \leq M$ , then $∥ f (b) - f (a) ∥_{2} \leq M (b - a)$ ).

Proof

1.1F1F7F8givenalgebra

Fix $M \in M$ . Along an edge $z (t) = a + t e$ , put $R_{M} (t) = (z (t) I - M)^{- 1}$ . By [F1] this inverse exists and has norm at most $m$ . For $h$ with $t, t + h \in [0, 1]$ , the resolvent identity gives $R_{M} (t + h) - R_{M} (t) = - h e R_{M} (t + h) R_{M} (t)$ . Thus [F1] and [F7] imply $∥ R_{M} (t + h) - R_{M} (t) ∥_{\infty, C} \leq ∣ h ∣ ∣ e ∣ m^{2}$ , so $R_{M}$ is continuous; dividing the identity by $h$ and taking the limit gives $R_{M}' (t) = - e R_{M} (t)^{2}$ for interior $t$ . Therefore $g (t) = e tr R_{M} (t)$ has $g' (t) = - e^{2} tr (R_{M} (t)^{2})$ . Since each diagonal entry is bounded by its row sum, $∣ tr A ∣ \leq n ∥ A ∥_{\infty, C}$ , so [F1] and [F7] give $∣ g' (t) ∣ \leq n ∣ e ∣^{2} m^{2}$ . By [F8], on each subinterval of length $1 / N$ , $∣ g (t) - g (t_{m i d}) ∣ \leq n ∣ e ∣^{2} m^{2} / (2 N)$ ; hence the integral error on that cell is at most $n ∣ e ∣^{2} m^{2} / (2 N^{2})$ . Summing all $N$ cells and edges gives the first term of $E$ .

2.1F1F5F6F7step 1.1algebra

At a sample point, the resolvent identity gives $R_{M} - R^{0} = R_{M} (M - M_{0}) R^{0}$ . Therefore $∣ tr (R_{M} - R^{0}) ∣ \leq n m b_{j k} δ_{A}$ . Multiplying by the edge weight and using $s_{j} \geq ∣ e_{j} ∣$ yields the second term of $E$ after summing samples. Thus the exact contour integral $\int_{Γ} tr (z I - M)^{- 1} d z$ lies in the complex disk centered at $S_{0}$ with radius $E$ , simultaneously for every $M \in M$ . Exact rational interval endpoint arithmetic and the valid $π$ interval [F5] make $I$ contain the normalized integral.

3.1F1F2F3F4step 2.1

For each fixed $M$ , put $p_{M} (z) = \det (z I - M)$ . The boundary is in the resolvent by [F1], so $p_{M}$ is nonzero on $Γ$ . By [F2] with $A = z I - M$ and direction $I$ , $p_{M}^{'} (z) / p_{M} (z) = tr (z I - M)^{- 1}$ . Facts [F3]–[F4] therefore identify $(2 π i)^{- 1} \int_{Γ} tr (z I - M)^{- 1} d z$ with the number of eigenvalues inside $P$ , counted with algebraic multiplicity; it is an integer from $0$ to $n$ .

4.1F5F6step 3.1∎

The successful output places the real part of every such integer strictly inside the half-unit interval around $c$ . There is only one integer in that interval, namely $c$ . Its imaginary part is zero and is contained by the checked imaginary interval. Hence every $M$ has exactly $c$ interior eigenvalues and none on the resolvent-certified boundary. If a monodromy matrix lies in $M$ , the same universal statement applies to it.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

A Krawczyk inclusion certifies a unique phase-fixed nonconstant periodic orbit

Statement

Suppose Finite-budget phase-fixed periodic-orbit correction and validation returns validated-root for a rational shooting box $Z = X \times Θ$ , with a complete Krawczyk partition of $Z$ containing exactly one unique-root box $Y$ and only root-free boxes otherwise, outward residual and Jacobian enclosures on $Y$ , a separately verified contraction bound, and a component of $f (X_{Y})$ excluding zero, where $X_{Y}$ is the physical-state projection of $Y$ . Then there is exactly one zero $(x_{*}, T_{*}) \in Z$ of the phase-bordered shooting residual, and it lies in $Y$ . It generates a nonconstant periodic solution with $ψ (x_{*}) = 0$ , period $T_{*} > 0$ , and the returned trajectory and monodromy boxes contain its exact trajectory and monodromy. No uniqueness outside $Z$ is asserted.

Facts & Assumptions

Given: The successful finite corrector record, its rational box and all interval enclosures and strict inequalities.

[F1]

Strict Krawczyk inclusion proves existence, and the separate interval norm bound $q < 1$ proves uniqueness in the box; strict inclusion alone does not prove uniqueness (Krawczyk inclusion proves existence, disjointness excludes roots, and contraction proves uniqueness).

[F2]

Provided the exact flow exists uniquely on $[0, θ]$ , a zero of the phase-bordered residual with positive period and nonzero vector field is exactly a phase-fixed nonconstant periodic solution (Zeros of the phase-bordered BVP are phase-fixed periodic orbits).

[F3]

The successful corrector returns the exact chart $T (u) = a + D u$ , a complete Krawczyk partition of $[0, 1]^{d + 1}$ and its mapped physical partition of $Z$ , with one normalized unique-root box and root-free boxes otherwise; it also returns physical residual/Jacobian, trajectory, monodromy and nonstationarity enclosures on its unique-root image box $Y$ (Finite-budget phase-fixed periodic-orbit correction and validation).

[F4]

A successful validated Euler range-oracle run establishes existence and uniqueness through scaled time $1$ and encloses the exact trajectory and variational solution (The validated Euler tube encloses the exact periodic flow and monodromy matrix).

[F5]

The positive-side rational affine chart transfers zeros, root-free/existence/uniqueness conclusions and complete partitions bijectively; its normalized derivative is $D F (T (u)) D$ (Rational boxes admit dyadic enclosure boundaries and exact affine root charts).

Proof

1.1F1F3F5given

By [F3], the actual Krawczyk run applies to $\hat{F} = F \circ T$ on the dyadic unit box, with normalized Jacobian enclosure for $D F (T (u)) D$ . Its unique normalized box $A_{Y}$ satisfies [F1], so strict inclusion gives a zero and the separate contraction bound gives at most one there. Every other normalized terminal box is root-free. By [F5], $T$ sends this complete partition onto $Z$ and bijects the zeros, so $Y = T (A_{Y})$ contains exactly one zero of the physical residual and every other physical image box is root-free. This is exactly one zero in all of $Z$ .

2.1F2F3F4step 1.1

Since $Θ \subset (0, \infty)$ , this root has positive period. The field range component excludes zero on its physical-state projection $X_{Y}$ , so $f (x_{*}) \neq 0$ . The full-box jet returned by [F3] contains a successful Euler run on $Y$ , so [F4] establishes existence and uniqueness of the exact flow through physical time $T_{*}$ . With this hypothesis verified, apply [F2] to obtain the phase-fixed nonconstant periodic solution.

3.1F1F3F4step 1.1∎

The successful run's range-oracle and interval inclusions contain each exact trajectory and variational solution by [F4]; [F3] makes these the trajectory and monodromy boxes of the root from step 1.1. Uniqueness is restricted to $Z$ , as established in step 1.1.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Strict Floquet cluster enclosures certify orbital asymptotic stability

Statement

Let an exact nonconstant phase-fixed periodic orbit and monodromy matrix $M_{*}$ be supplied by a sound periodic-orbit certificate. Suppose $M_{*}$ belongs to a matrix family with a certified complete cluster list of pairwise disjoint filled convex polygons $P_{0}, \dots, P_{s}$ : each count is certified by A verified contour count encloses every Floquet multiplier in a cluster, the counts sum to the state dimension $d$ , $1 \in int P_{0}$ , and the count in $P_{0}$ is one. Suppose also that for each $j \geq 1$ , $P_{j} \subset {z : ∣ z ∣ \leq 1 - σ}$ for one supplied $σ > 0$ . Then the periodic orbit is orbitally asymptotically stable. If any non-phase cluster enclosure meets or intersects the unit circle, these hypotheses fail and this theorem gives no stability verdict.

Facts & Assumptions

Given: A nonconstant periodic solution of positive period $T$ , its phase section, its monodromy matrix in the certified matrix family, and the complete disjoint cluster list with the stated counts and strict disk margin.

[F1]

The orbit certificate supplies an exact periodic solution, positive period, and a monodromy matrix contained in its validated family (A Krawczyk inclusion certifies a unique phase-fixed nonconstant periodic orbit).

[F2]

The phase tangent is an eigenvector of the monodromy with multiplier $1$ (An autonomous periodic orbit has a neutral Floquet multiplier).

[F3]

Every successful polygon count is valid for each matrix in the supplied family and counts algebraic multiplicities (A verified contour count encloses every Floquet multiplier in a cluster).

[F4]

For a least-period orbit with simple phase multiplier and transverse affine section, the Poincare derivative has exactly the other monodromy multipliers (The Poincare derivative has precisely the non-phase monodromy multipliers).

[F5]

For a $C^{1}$ autonomous field and a transverse section, if every eigenvalue of the $C^{1}$ Poincare return map derivative lies strictly inside the unit disk, the orbit is orbitally asymptotically stable (Hyperbolic return-map stability is orbital stability).

[F6]

The $C^{2}$ autonomous field supplied by the orbit certificate has a unique maximal $C^{2}$ flow with time derivative $f (ϕ_{t} (x))$ (C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade). Uniqueness identifies a shifted trajectory with the solution from its shifted initial state, giving the flow law on the common domain. Composition derivatives obey the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ). Eigenvectors have the meaning of Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism, and generalized vectors are supplied by Jordan form over the base field exists exactly when the characteristic polynomial splits. Algebraic multiplicity means characteristic-polynomial root multiplicity.

[F7]

The corrector's record supplies the original-box affine chart $z = a + D u$ with positive diagonal $D$ and a nonsingular preconditioner $C$ for the normalized residual. For each physical shooting Jacobian $J$ in the certified root box, its verified contraction gives $∥ I - C J D ∥_{\infty} \leq q < 1$ . The chart transfers nonsingularity of $C J D$ to $J$ (Finite-budget phase-fixed periodic-orbit correction and validation, Finite-budget multidimensional Krawczyk root certification, Rational boxes admit dyadic enclosure boundaries and exact affine root charts).

[F8]

A complex square matrix $E$ with $∥ E ∥_{\infty, C} < 1$ has $I - E$ invertible (A complex infinity-norm defect bounds the inverse norm); the phase-bordered Jacobian criterion identifies nonsingularity with a simple neutral multiplier and transverse phase (A simple neutral multiplier and transverse phase make the shooting Jacobian invertible).

[F9]

The characteristic polynomial of a $d \times d$ matrix is monic of degree $d$ ( $χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ ), its roots are exactly its eigenvalues (For every finite-dimensional space, $σ_{F} (T)$ is exactly the set of roots in $F$ of $χ_{T}$ ), and it has exactly $d$ complex roots counted with multiplicity (A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity).

Proof

1.1F1F2F3F9givenalgebra

By [F1]–[F3], exactly one multiplier of $M_{*}$ lies in $P_{0}$ , and it is $1$ by [F2]. Thus the algebraic multiplicity of $1$ for $M_{*}$ is one. Every other multiplier lies in one of the polygons $P_{j}$ , $j \geq 1$ : their counts together with the count one in $P_{0}$ sum to $d$ , while [F9] says a $d \times d$ characteristic polynomial has exactly $d$ roots counted with multiplicity. The remaining multipliers therefore all have modulus at most $1 - σ < 1$ .

2.1F1F6step 1.1givenalgebra

Nonconstancy and flow uniqueness [F6] imply $f (γ (0)) \neq 0$ , since otherwise the constant solution through $γ (0)$ would be the unique trajectory. Define $H = {t \in R : γ (t) = γ (0)}$ . Flow uniqueness makes $H$ an additive subgroup: a return to $γ (0)$ repeats the entire trajectory, so sums and differences of return times are return times. Continuity makes $H$ closed. One coordinate has nonzero derivative at zero and is strictly monotone on a sufficiently short interval; hence $H$ has no nonzero element there. Its positive infimum $S$ is therefore positive and belongs to $H$ by closedness. For any positive period $T$ , division by $S$ gives $T = k S + r$ with integer $k \geq 1$ and $0 \leq r < S$ ; the subgroup property gives $r \in H$ , so minimality forces $r = 0$ . Thus $T = k S$ , where $S$ is the least positive period.

3.1F2F6step 1.1step 2.1algebra

Let $M_{S}$ be the monodromy over $S$ . By flow composition and the chain rule [F6], $M_{*} = M_{S}^{k}$ . The phase tangent is a $1$ eigenvector of $M_{S}$ by [F2]. If $M_{S} v = α v$ with $α^{k} \neq 1$ , then $M_{*} v = α^{k} v$ is a non-phase eigenvalue of $M_{*}$ , so step 1.1 gives $∣ α ∣^{k} < 1$ and $∣ α ∣ < 1$ . If $α^{k} = 1$ and $α \neq 1$ , then $v$ and the phase tangent are independent eigenvectors of $M_{*}$ for eigenvalue $1$ , contradicting its algebraic simplicity. If $α = 1$ and there were an eigenvector independent of the phase tangent, the same contradiction follows. If the eigenvalue $1$ of $M_{S}$ had a nontrivial Jordan chain, [F6] gives a generalized vector $v$ with $(M_{S} - I) v = f (γ (0))$ after rescaling. Then $(M_{*} - I) v = (M_{S}^{k} - I) v = k f (γ (0)) \neq 0$ , contradicting the algebraic simplicity of $1$ for $M_{*}$ . Hence $1$ is simple for $M_{S}$ and every other eigenvalue of $M_{S}$ is strictly inside the unit circle.

4.1F1F4F7F8step 1.1step 2.1step 3.1

The orbit with period $S$ is least-period by step 2.1. The certificate [F1] validates the phase-bordered shooting Jacobian for the possibly repeated period $T$ , and that is the Jacobian used in the following nonsingularity check. For the exact real Jacobian $J$ at that root, [F7] gives $∥ I - C J D ∥_{\infty} < 1$ with the recorded positive diagonal scale $D$ . Regard $I - C J D$ as a complex matrix; [F8] makes $C J D$ invertible over $C$ and hence over $R$ . The affine-chart transfer in [F7] then makes $J$ invertible; explicitly, $J^{- 1} = D (C J D)^{- 1} C$ . Step 1.1 gives a simple phase multiplier, so the bordered criterion in [F8] implies $c^{⊤} f (γ (0)) \neq 0$ . The same affine phase is therefore transverse for the least-period orbit. Apply [F4] to identify the Poincare derivative eigenvalues with all non-phase eigenvalues of $M_{S}$ ; step 3.1 places them strictly inside the unit circle.

5.1F4F5F6step 2.1step 4.1∎

The certificate field is $C^{2}$ and its affine phase section is smooth; [F4]'s hypotheses therefore give a $C^{1}$ Poincare return map. Its derivative has no unit-circle multiplier, and all its eigenvalues are strictly inside by step 4.1. Shrink the section to a relatively compact patch whose closure meets the orbit only at $γ (0)$ : transversality isolates that intersection along a short orbit arc, and the remaining compact arc stays away from $γ (0)$ by the least-period property. Apply the $C^{1}$ theorem [F5] on this patch to conclude orbital asymptotic stability.

5 · Examples, counterexamples and false statements

None yet.

Periodic orbit shooting collocation and Floquet error

1 · Prerequisites

2 · Summary

Objective

3 · Logical flowchart

4 · Definitions, theorems and proofs

Exact range-oracle contract for validated flow and monodromy enclosures

Definition

A positively oriented convex polygon has winding index one inside and zero outside

Statement

Facts & Assumptions

Proof

Validated forward-Euler tube for the periodic flow and variational equation

Definition

The phase-bordered periodic-orbit BVP residual

Definition

An autonomous periodic orbit has a neutral Floquet multiplier

Statement

Facts & Assumptions

Proof

A C2C2 vector field has a C2C2 flow on a common compact tube

Statement

Facts & Assumptions

Proof

Zeros of the phase-bordered BVP are phase-fixed periodic orbits

Statement

Facts & Assumptions

Proof

The validated Euler tube encloses the exact periodic flow and monodromy matrix

Statement

Facts & Assumptions

Proof

The Poincare derivative has precisely the non-phase monodromy multipliers

Statement

Facts & Assumptions

Proof

A simple neutral multiplier and transverse phase make the shooting Jacobian invertible

Statement

Facts & Assumptions

Proof

A transverse phase border makes the periodic BVP linearization boundedly invertible

Statement

Facts & Assumptions

Proof

Multiple-shooting and midpoint-collocation residuals for a phase-fixed periodic orbit

Definition

Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting

Definition

Periodic midpoint collocation has an explicit local second-order error budget

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

Rational boxes admit dyadic enclosure boundaries and exact affine root charts

Statement

Facts & Assumptions

Proof

Finite-budget phase-fixed periodic-orbit correction and validation

Definition

A separated simple Floquet multiplier has a left/right-conditioned finite enclosure

Statement

Facts & Assumptions

Proof

Finite pseudo-arclength continuation of phase-fixed periodic orbits

Definition

Finite complex-contour validation of Floquet multiplier clusters

Definition

A verified contour count encloses every Floquet multiplier in a cluster

Statement

Facts & Assumptions

Proof

A Krawczyk inclusion certifies a unique phase-fixed nonconstant periodic orbit

Statement

Facts & Assumptions

Proof

Strict Floquet cluster enclosures certify orbital asymptotic stability

Statement

A $C^{2}$ vector field has a $C^{2}$ flow on a common compact tube