Orbits in finite functional graphs

Iterating f : α → α from a state x traces a path in the functional graph of f. On a finite type every orbit eventually enters a cycle: its transient depth is the first time it reaches a periodic point, and its cycle length is the minimal period of that point. The transient and one complete cycle contain no repeated state (orbit_prefix_injective), so their total length is at most the number of states (transientDepth_add_cycleLength_le_card).

A repeat f^[i] x = f^[j] x with i < j makes f^[i] x periodic with period j - i and reduces every later time modulo j - i (iterate_add_mod_sub). Consequently every reachable target has a first visit before the number of states (exists_first_visit), and the map that stops at a target finds it after that many steps (absorb_iterate_card).

The state type may live in any universe. Finiteness is required only where stated.

Main definitions

• Cslib.FunctionalGraph.absorb: stop at states satisfying a predicate.
• Cslib.FunctionalGraph.transientDepth: the first time an orbit is periodic.
• Cslib.FunctionalGraph.cycleLength: the period of the eventual cycle.

Main results

• Cslib.FunctionalGraph.exists_first_visit: first visits occur before the state count.
• Cslib.FunctionalGraph.absorb_iterate_card_eq_iff: the absorbing map decides reachability.
• Cslib.FunctionalGraph.iterate_mem_periodicPts_iff: periodicity begins exactly at the transient depth.
• Cslib.FunctionalGraph.orbit_prefix_injective: the transient and one cycle are repeat-free.
• Cslib.FunctionalGraph.exists_iterate_eq_iff_of_not_mem_periodicPts: a transient target is reached only at the difference of transient depths.

References

• Adapted from lean/Proofs/{Reconstruction,FiniteOrbit,OrbitStructure}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

Repeats

theorem Cslib.FunctionalGraph.isPeriodicPt_of_iterate_eq {α : Type u} {f : α → α} {x : α} {i j : ℕ} (hij : i ≤ j) (heq : f^[i] x = f^[j] x) : Function.IsPeriodicPt f (j - i) (f^[i] x)

A repeat f^[i] x = f^[j] x with i ≤ j makes f^[i] x periodic with period j - i.

theorem Cslib.FunctionalGraph.iterate_add_mod_sub {α : Type u} {f : α → α} {x : α} {i j T : ℕ} (hij : i ≤ j) (heq : f^[i] x = f^[j] x) (hT : i ≤ T) : f^[i + (T - i) % (j - i)] x = f^[T] x

After a repeat, every later time can be reduced modulo the repeat interval.

theorem Cslib.FunctionalGraph.iterate_eq_iterate_of_mod_eq {α : Type u} {f : α → α} {x : α} {i j r T : ℕ} (hij : i ≤ j) (heq : f^[i] x = f^[j] x) (hr : i ≤ r) (hT : i ≤ T) (hmod : r % (j - i) = T % (j - i)) : f^[r] x = f^[T] x

After a repeat, two later times that agree modulo the repeat interval give the same state.

First visits

theorem Cslib.FunctionalGraph.exists_first_visit {α : Type u} (f : α → α) [Fintype α] (P : α → Prop) (x : α) (h : ∃ (t : ℕ), P (f^[t] x)) : ∃ t < Fintype.card α, P (f^[t] x) ∧ ∀ k < t, ¬P (f^[k] x)

Every reachable target has a first visit before the number of states.

def Cslib.FunctionalGraph.absorb {α : Type u} (f : α → α) (P : α → Prop) [DecidablePred P] (x : α) : α

The map that stops at states satisfying P and otherwise applies f.

theorem Cslib.FunctionalGraph.absorb_iterate_of_forall_not {α : Type u} (f : α → α) (P : α → Prop) [DecidablePred P] (x : α) (t : ℕ) (h : ∀ j < t, ¬P (f^[j] x)) : (absorb f P)^[t] x = f^[t] x

Before any visit to P, the absorbing map agrees with f: if no f^[j] x with j < t satisfies P, then (absorb f P)^[t] x = f^[t] x.

theorem Cslib.FunctionalGraph.absorb_iterate_of_pos {α : Type u} (f : α → α) (P : α → Prop) [DecidablePred P] {x : α} (hx : P x) (t : ℕ) : (absorb f P)^[t] x = x

The absorbing map fixes every state satisfying P, under any number of iterations.

theorem Cslib.FunctionalGraph.absorb_iterate_of_first_visit {α : Type u} (f : α → α) (P : α → Prop) [DecidablePred P] (x : α) {t T : ℕ} (ht : P (f^[t] x)) (hfirst : ∀ j < t, ¬P (f^[j] x)) (hle : t ≤ T) : (absorb f P)^[T] x = f^[t] x

After the first visit at time t, the absorbing map stays at the target.

theorem Cslib.FunctionalGraph.absorb_iterate_card {α : Type u} (f : α → α) [Fintype α] (P : α → Prop) [DecidablePred P] (x : α) (h : ∃ (t : ℕ), P (f^[t] x)) : ∃ t < Fintype.card α, P (f^[t] x) ∧ (∀ j < t, ¬P (f^[j] x)) ∧ (absorb f P)^[Fintype.card α] x = f^[t] x

Iterating the absorbing map as many times as there are states returns the first visit.

theorem Cslib.FunctionalGraph.absorb_iterate_card_eq_iff {α : Type u} (f : α → α) [Fintype α] (P : α → Prop) [DecidablePred P] (x : α) : P ((absorb f P)^[Fintype.card α] x) ↔ ∃ (t : ℕ), P (f^[t] x)

The absorbing map decides reachability after as many steps as there are states.

Transient depth and cycle length

theorem Cslib.FunctionalGraph.exists_iterate_mem_periodicPts {α : Type u} (f : α → α) [Finite α] (x : α) : ∃ (t : ℕ), f^[t] x ∈ Function.periodicPts f

Every orbit of a map on a finite type reaches a periodic point.

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

The transient depth of x: the first time its orbit is periodic.

theorem Cslib.FunctionalGraph.iterate_transientDepth_mem_periodicPts {α : Type u} (f : α → α) [Finite α] (x : α) : f^[transientDepth f x] x ∈ Function.periodicPts f

The orbit of x is at a periodic point at its transient depth.

theorem Cslib.FunctionalGraph.iterate_mem_periodicPts_iff {α : Type u} (f : α → α) [Finite α] (x : α) (t : ℕ) : f^[t] x ∈ Function.periodicPts f ↔ transientDepth f x ≤ t

Periodicity begins exactly at the transient depth.

@[simp]

theorem Cslib.FunctionalGraph.transientDepth_eq_zero_iff {α : Type u} (f : α → α) [Finite α] (x : α) : transientDepth f x = 0 ↔ x ∈ Function.periodicPts f

The transient depth of x is zero exactly when x is periodic.

theorem Cslib.FunctionalGraph.transientDepth_eq_zero_of_mem_periodicPts {α : Type u} (f : α → α) [Finite α] {x : α} (hx : x ∈ Function.periodicPts f) : transientDepth f x = 0

For a periodic state, the transient depth is zero.

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

The transient depth is less than the number of states.

@[simp]

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

Advancing t steps lowers the transient depth by t, truncated at zero.

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

The cycle length of x: the minimal period of its eventual cycle.

theorem Cslib.FunctionalGraph.cycleLength_eq_minimalPeriod_of_mem_periodicPts {α : Type u} (f : α → α) [Finite α] {x : α} (hx : x ∈ Function.periodicPts f) : cycleLength f x = Function.minimalPeriod f x

For a periodic state, the cycle length is the minimal period.

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

The cycle length is positive.

theorem Cslib.FunctionalGraph.isPeriodicPt_cycleLength {α : Type u} (f : α → α) [Finite α] (x : α) : Function.IsPeriodicPt f (cycleLength f x) (f^[transientDepth f x] x)

The state at the transient depth is periodic with period the cycle length.

theorem Cslib.FunctionalGraph.minimalPeriod_iterate {α : Type u} (f : α → α) [Finite α] (x : α) {a : ℕ} (ha : transientDepth f x ≤ a) : Function.minimalPeriod f (f^[a] x) = cycleLength f x

Past the transient, every state has the cycle length as exact period.

theorem Cslib.FunctionalGraph.iterate_apply_eq_iterate_apply_iff {α : Type u} (f : α → α) [Finite α] (x : α) {a b : ℕ} (hab : a < b) : f^[a] x = f^[b] x ↔ transientDepth f x ≤ a ∧ cycleLength f x ∣ b - a

Two times give the same state exactly when the earlier is past the transient and their difference is a multiple of the cycle length.

theorem Cslib.FunctionalGraph.orbit_prefix_injective {α : Type u} (f : α → α) [Finite α] (x : α) : Function.Injective fun (i : Fin (transientDepth f x + cycleLength f x)) => f^[↑i] x

The transient and one complete cycle contain no repeated state.

theorem Cslib.FunctionalGraph.transientDepth_add_cycleLength_le_card {α : Type u} (f : α → α) [Finite α] [Fintype α] (x : α) : transientDepth f x + cycleLength f x ≤ Fintype.card α

The transient depth plus the cycle length is at most the number of states.

theorem Cslib.FunctionalGraph.transientDepth_add_cycleLength_le_of_iterate_eq {α : Type u} (f : α → α) [Finite α] (x : α) {i j : ℕ} (hij : i < j) (he : f^[i] x = f^[j] x) : transientDepth f x + cycleLength f x ≤ j

A repeat within a prefix bounds the transient depth plus the cycle length.

theorem Cslib.FunctionalGraph.exists_iterate_eq_iff_of_not_mem_periodicPts {α : Type u} (f : α → α) [Finite α] (x y : α) (hy : y ∉ Function.periodicPts f) : (∃ (t : ℕ), f^[t] x = y) ↔ transientDepth f y ≤ transientDepth f x ∧ f^[transientDepth f x - transientDepth f y] x = y

A transient target can only be reached at the difference of the transient depths.