Coordinates on a lifted periodic orbit
Abstract
A periodic skew orbit splits into base positions and a holonomy phase subgroup.
Theorem 1.1 (Base position and holonomy phase).
Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewOrbitCoordinates.skew_orbit_coordinates
Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewOrbitCoordinates.skew_orbit_coordinates (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let x be a periodic base point with minimal period p, and let h be the Birkhoff sum of the charge over one turn. If h has finite additive order, then the map
(i,s) ↦ (f^i(x), a + s + BirkhoffSum(i,x))
is a bijection from Fin p times the subgroup generated by h onto the lifted periodic orbit through (x,a). The fiber group may be infinite.
Writing an orbit time as n = i + p k gives the remainder position i and a phase k • h. Finite holonomy order makes every integer multiple representable by a nonnegative multiple, while distinct remainders have distinct base points. Thus each base-position fiber is a translate of the same holonomy subgroup.
Dependency. SkewAdditiveReturn