Periodic orbit classes in a cyclic skew product
Abstract
Periodic orbit equality in a cyclic additive skew product is exactly holonomy congruence.
Theorem 1.1 (Orbit equality is an integer holonomy relation).
Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewZModPeriodicOrbit.skew_periodicOrbit_eq_iff
Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewZModPeriodicOrbit.skew_periodicOrbit_eq_iff (✓ std3). ∎
Source. Repository-derived.
Commentary.
For two lifted points (x,a) and (x,b) over a periodic base point, the base coordinate forces every connecting iterate to be a multiple of the base minimal period.
Each such block adds the same Birkhoff holonomy h in the cyclic fiber. Consequently the two forward periodic orbits coincide exactly when the displacement b-a belongs to the additive subgroup generated by h.