PropositionStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

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.

Depends on

Used by

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

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

E. J. Doedel and B. E. Oldeman, AUTO-07P full manual (2021) (standard reference, not scraped)
Y. A. Kuznetsov, Elements of Applied Bifurcation Theory, 2nd ed., Chapter 1, §1.5 (standard reference, not scraped)