Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

A stable planar cycle can have a singular phase slice

Statement

On the annulus U={(x,y):1/2<x2+y2<3/2} consider

x˙=(1−r)x−y,y˙=(1−r)y+x,r=x2+y2.

The unit circle is an orbitally asymptotically stable periodic orbit of period 2π. At x∗=(1,0) the affine phase ψb(x,y)=x−1 has a singular phase-bordered shooting Jacobian, while ψg(x,y)=y is transverse and gives an invertible phase-bordered shooting Jacobian.

Facts & Assumptions

Given: The smooth autonomous field on the annulus, the unit-circle candidate orbit, and the two affine phase functions.

[F1]

The phase-bordered residual for phase covector c is (ϕT(x)−x,ψ(x)), and its Jacobian has period column f(x∗) (The phase-bordered periodic-orbit BVP residual).

[F2]

The bordered Jacobian is singular when c⊤f(x∗)=0 and is invertible when the neutral multiplier is simple and the phase is transverse (A simple neutral multiplier and transverse phase make the shooting Jacobian invertible).

Proof

1.1givenalgebra

The identities r˙=(xx′+yy′)/r and ϑ˙=(xy′−yx′)/r2 give r˙=r(1−r) and ϑ˙=1. Thus r=1 is invariant and ϑ(t)=ϑ(0)+t, so the least period is 2π. Differentiating r(1−r) at r=1 gives the radial variational equation ρ˙=−ρ, whose multiplier is e−2π<1; the angular variational equation is α˙=0, whose multiplier is 1. Because the polar-coordinate Jacobian at times 0 and 2π is the same invertible matrix, the Cartesian monodromy is conjugate to diag⁡(e−2π,1). For r<1 the radial derivative is positive, and for r>1 it is negative, so each nearby radius moves monotonically toward 1 and remains between its initial value and 1. It has a limit rˉ; if rˉ(1−rˉ)≠0, then r˙=r(1−r) is eventually bounded away from zero, contradicting convergence. Hence rˉ is an equilibrium, and the interval between the initial radius and 1 contains only the equilibrium 1, so r(t)→1. These bounds also give Lyapunov stability of the unit circle. Thus the orbit is orbitally asymptotically stable and its neutral multiplier is simple.

2.1F1F2step 1.1algebra∎

At (1,0) the vector field is (0,1). For ψb=x−1, cb=(1,0) and cb⊤f(x∗)=0, so [F2] gives a singular shooting Jacobian. For ψg=y, cg=(0,1) and cg⊤f(x∗)=1; the phase multiplier is simple by step 1.1, so [F2] gives an invertible Jacobian.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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