Canonical cycles in finite functional graphs

Every orbit of a map on a finite type ends in a cycle (cycleSet), the same for all states of the orbit (cycleSet_iterate). Past the transient, two times give the same state exactly when they agree modulo the cycle length (iterate_eq_iterate_iff_modEq). Given a linear order on the states, the least state of the cycle is a canonical representative (canonicalCycle): a periodic state is reachable from x exactly when the two have the same representative (exists_iterate_eq_iff_canonicalCycle_eq). The first visit to the representative (canonicalTime) occurs before the number of states, and before the cycle length for a periodic state; the phase of a state on its cycle is the negative of that time modulo the cycle length (phase).

These labels depend only on the map and the order, not on any representation of the states.

Main definitions

• Cslib.FunctionalGraph.cycleSet: the eventual cycle.
• Cslib.FunctionalGraph.canonicalCycle: its least state.
• Cslib.FunctionalGraph.canonicalTime: the first visit to that state.
• Cslib.FunctionalGraph.phase: the position on the cycle.

Main results

• Cslib.FunctionalGraph.iterate_eq_iterate_iff_modEq: equality past the transient.
• Cslib.FunctionalGraph.mem_cycleSet_iff: the cycle is the periodic orbit reached.
• Cslib.FunctionalGraph.exists_iterate_eq_iff_canonicalCycle_eq: reachability of periodic states.
• Cslib.FunctionalGraph.transientDepth_le_canonicalTime, Cslib.FunctionalGraph.canonicalTime_lt_card, Cslib.FunctionalGraph.canonicalTime_lt_cycleLength: bounds on the first visit.

References

• Adapted from lean/Proofs/CycleLabels.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

@[simp]

theorem Cslib.FunctionalGraph.cycleLength_iterate {α : Type u} [Finite α] (f : α → α) (x : α) (t : ℕ) : cycleLength f (f^[t] x) = cycleLength f x

Advancing along the orbit does not change the cycle length.

theorem Cslib.FunctionalGraph.minimalPeriod_at_periodic_iterate {α : Type u} [Finite α] (f : α → α) (x : α) {t : ℕ} (ht : f^[t] x ∈ Function.periodicPts f) : Function.minimalPeriod f (f^[t] x) = cycleLength f x

Every periodic state on the orbit of x has the cycle length of x as minimal period.

theorem Cslib.FunctionalGraph.iterate_eq_iterate_iff_modEq {α : Type u} [Finite α] (f : α → α) (x : α) {a b : ℕ} (ha : transientDepth f x ≤ a) (hb : transientDepth f x ≤ b) : f^[a] x = f^[b] x ↔ a ≡ b [MOD cycleLength f x]

Past the transient, two times give the same state exactly when they agree modulo the cycle length.

noncomputable def Cslib.FunctionalGraph.cycleSet {α : Type u} [Finite α] (f : α → α) (x : α) : Finset α

The eventual cycle of x, as a finite set.

@[simp]

theorem Cslib.FunctionalGraph.mem_cycleSet_iff {α : Type u} [Finite α] (f : α → α) (x y : α) : y ∈ cycleSet f x ↔ y ∈ Function.periodicOrbit f (f^[transientDepth f x] x)

The eventual cycle of x is the periodic orbit of the state at its transient depth.

theorem Cslib.FunctionalGraph.cycleSet_nonempty {α : Type u} [Finite α] (f : α → α) (x : α) : (cycleSet f x).Nonempty

The eventual cycle is nonempty.

@[simp]

theorem Cslib.FunctionalGraph.cycleSet_iterate {α : Type u} [Finite α] (f : α → α) (x : α) (t : ℕ) : cycleSet f (f^[t] x) = cycleSet f x

Advancing along the orbit does not change the eventual cycle.

theorem Cslib.FunctionalGraph.cycleSet_spec {α : Type u} [Finite α] (f : α → α) {x y : α} (hy : y ∈ cycleSet f x) : y ∈ Function.periodicPts f ∧ ∃ (t : ℕ), f^[t] x = y

Every state on the eventual cycle of x is periodic and reachable from x.

noncomputable def Cslib.FunctionalGraph.canonicalCycle {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : α

The least element of the eventual cycle in the chosen state order.

theorem Cslib.FunctionalGraph.canonicalCycle_mem {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : canonicalCycle f x ∈ cycleSet f x

The canonical representative lies on the eventual cycle.

theorem Cslib.FunctionalGraph.canonicalCycle_le {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) {y : α} (hy : y ∈ cycleSet f x) : canonicalCycle f x ≤ y

The canonical representative is at most every state of the eventual cycle.

@[simp]

theorem Cslib.FunctionalGraph.canonicalCycle_iterate {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) (t : ℕ) : canonicalCycle f (f^[t] x) = canonicalCycle f x

Advancing along the orbit does not change the canonical representative.

theorem Cslib.FunctionalGraph.canonicalCycle_periodic {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : canonicalCycle f x ∈ Function.periodicPts f

The canonical representative is periodic.

theorem Cslib.FunctionalGraph.canonicalCycle_reachable {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : ∃ (t : ℕ), f^[t] x = canonicalCycle f x

The canonical representative is reachable from x.

theorem Cslib.FunctionalGraph.exists_iterate_eq_iff_canonicalCycle_eq {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x y : α) (hy : y ∈ Function.periodicPts f) : (∃ (t : ℕ), f^[t] x = y) ↔ canonicalCycle f x = canonicalCycle f y

A canonical representative completely identifies the eventual cycle.

noncomputable def Cslib.FunctionalGraph.canonicalTime {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : ℕ

The first visit to the canonical cycle representative, always below the state count.

theorem Cslib.FunctionalGraph.canonicalTime_spec {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : f^[canonicalTime f x] x = canonicalCycle f x

At the canonical time, the orbit of x is at its canonical representative.

theorem Cslib.FunctionalGraph.canonicalTime_min {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) {j : ℕ} (hj : j < canonicalTime f x) : f^[j] x ≠ canonicalCycle f x

Before the canonical time, the orbit of x avoids its canonical representative.

theorem Cslib.FunctionalGraph.transientDepth_le_canonicalTime {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : transientDepth f x ≤ canonicalTime f x

The canonical time is at least the transient depth.

theorem Cslib.FunctionalGraph.canonicalTime_lt_cycleLength {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) (hx : x ∈ Function.periodicPts f) : canonicalTime f x < cycleLength f x

For a periodic state, the canonical time is less than the cycle length.

theorem Cslib.FunctionalGraph.canonicalTime_lt_card {α : Type u} [Finite α] (f : α → α) [LinearOrder α] [Fintype α] (x : α) : canonicalTime f x < Fintype.card α

The canonical time is less than the number of states.

noncomputable def Cslib.FunctionalGraph.phase {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : ℕ

The phase of x on its cycle: the negative of the canonical hitting time modulo the cycle length.

theorem Cslib.FunctionalGraph.phase_lt {α : Type u} [Finite α] (f : α → α) [LinearOrder α] (x : α) : phase f x < cycleLength f x

The phase is less than the cycle length.