Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass
How statement and proof provenance work

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

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

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

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

Statement

At a phase-fixed periodic point x∗ with period T, let M=DxϕT(x∗), let f∗=f(x∗)≠0, and let c=Dψ(x∗) for the affine phase ψ(x)=c⊤(x−xref). The derivative of the phase-bordered shooting residual is J=[M−Idf∗c⊤0]. It is invertible if and only if 1 is an algebraically simple eigenvalue of M and c⊤f∗≠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 KW=∥((M−Id)∣W)−1∥2→2. All vector and matrix norms below are Euclidean and induced Euclidean norms, and the product norm on (u,τ)∈Rd×R is Euclidean. Then ∥J−1∥2→2≤KW∥Q∥2+∥w∥2+∥f∗∥2(1+∥c∥2KW∥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−xref) (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).

[F5]

The monodromy is the state derivative of the flow (Local periodic-orbit, Poincare-return, and Floquet data). For the C2 field in [F1], the finite-regularity maximal-flow theorem supplies a C2 flow with time derivative ∂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∘f)(a)=Dg(f(a))∘Df(a)).

[F7]

For linear maps between finite-dimensional spaces of equal dimension, injectivity is equivalent to surjectivity (Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T).

Proof

1.1F1F5F6

By [F1] and [F5], differentiating in x gives M−Id, 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 Rf∗ and rank-nullity gives rank⁡R(M−Id)=d−1. Choose a real basis v1,…,vd−1 of range⁡(M−Id). The d−1 real linear forms w↦vj⊤w are independent: if a linear combination vanishes for every w, then the row (∑jajvj)⊤ is zero, so ∑jajvj=0 and basis independence forces every coefficient aj to vanish. Rank-nullity therefore gives a nonzero real w0 with vj⊤w0=0 for every j. Thus w0⊤(M−Id)=0. It is a compatible left eigenvector with the real right eigenvector f∗, so [F3], applied over C, gives w0⊤f∗≠0. This pairing is real; normalize w=w0/(w0⊤f∗), so w is real, w⊤M=w⊤, and w⊤f∗=1. For Q=I−f∗w⊤ and W=ker⁡w⊤, one has Qf∗=0, Q∣W=IW, and QM=M−f∗w⊤M=M−f∗w⊤=M−Mf∗w⊤=MQ. Hence Q is the projection onto W, M preserves W, and M−Id 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=uW+αf∗ with uW∈W; applying Q to the first row and using its commutation with M gives uW=((M−Id)∣W)−1Qr, and the phase row gives α=(s−c⊤uW)/(c⊤f∗). Thus nonzero c⊤f∗ gives a unique solution for every right-hand side, so J is invertible. Moreover, ∣τ∣≤∥w∥2∥r∥2, ∥uW∥2≤KW∥Q∥2∥r∥2, and ∣α∣≤(∣s∣+∥c∥2KW∥Q∥2∥r∥2)/∣c⊤f∗∣. By the triangle inequality and ∥r∥2,∣s∣≤∥(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−Id, its complex kernel consists exactly of u+iv with u and v in the real kernel. Choose a real v∈ker⁡(M−Id) 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−Id), 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−Id)v=f∗ over C. Since M−Id 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−Id)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.

Depends on

Used by

Dependency tree · two levels

54 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