Cycle-spectrum reduction and canonical hitting-time identities

Every fixed power of a map on a finite state type is determined by the eventual cycle length of its argument: past the state-space cardinality, an exponent may be reduced modulo the cycle length (iterate_eq_card_add_mod). The cycle length is recovered from the finite set of cycle lengths (cycleSpectrum) by a divisibility test (spectrum_test, cycleSpectrum_test), and a permutation is inverted by the power one below the cycle length (perm_symm_eq_iterate).

Given a linear order on the states, canonicalTime f x is the first time at which the trajectory of x visits the least state of its eventual cycle (canonicalCycle f x). Off the cycles, one step lowers canonicalTime by one (canonicalTime_apply). Past the transient depth, f^[T] x is f^[a] (canonicalCycle f x) iff a + canonicalTime f x ≡ T [MOD cycleLength f x] (iterate_eq_canonical_iff).

Main definitions

• Cslib.FunctionalGraph.cycleSpectrum: the finite set of cycle lengths of f.

Main results

• Cslib.FunctionalGraph.iterate_add_cycleLength_mul: adding whole cycles past the transient preserves the state.
• Cslib.FunctionalGraph.iterate_eq_card_add_mod: exponent reduction past Fintype.card α.
• Cslib.FunctionalGraph.cycle_test_iff, Cslib.FunctionalGraph.spectrum_test, Cslib.FunctionalGraph.cycleSpectrum_test: recovering cycleLength f x as the least candidate period dividing a return at Fintype.card α.
• Cslib.FunctionalGraph.injective_cycle_test_iff, Cslib.FunctionalGraph.injective_spectrum_test, Cslib.FunctionalGraph.perm_symm_eq_iterate: specializations to injective maps and permutations.
• Cslib.FunctionalGraph.canonicalTime_apply: one transient step decrements canonicalTime.
• Cslib.FunctionalGraph.iterate_eq_canonical_iff: characterization of states past the transient relative to canonicalCycle.

References

• Adapted from lean/Proofs/{Spectrum,PhaseIdentities}.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

Cycle-spectrum reduction

theorem Cslib.FunctionalGraph.iterate_add_cycleLength_mul {α : Type u} [Finite α] (f : α → α) (x : α) {a : ℕ} (ha : transientDepth f x ≤ a) (q : ℕ) : f^[a + cycleLength f x * q] x = f^[a] x

Past the transient depth, adding whole multiples of the cycle length does not change the state.

theorem Cslib.FunctionalGraph.iterate_eq_card_add_mod {α : Type u} [Fintype α] (f : α → α) (x : α) {T : ℕ} (hT : Fintype.card α ≤ T) : f^[T] x = f^[Fintype.card α + (T - Fintype.card α) % cycleLength f x] x

Spectrum reduction. Every exponent T at least Fintype.card α can be replaced by Fintype.card α + (T - Fintype.card α) % cycleLength f x.

theorem Cslib.FunctionalGraph.cycle_test_iff {α : Type u} [Fintype α] (f : α → α) (x : α) (ℓ : ℕ) : f^[Fintype.card α + ℓ] x = f^[Fintype.card α] x ↔ cycleLength f x ∣ ℓ

The cycle-length divisibility test. f^[Fintype.card α + ℓ] x = f^[Fintype.card α] x holds iff cycleLength f x ∣ ℓ.

noncomputable def Cslib.FunctionalGraph.cycleSpectrum {α : Type u} [Fintype α] (f : α → α) : Finset ℕ

The finite set of distinct cycle lengths of f.

theorem Cslib.FunctionalGraph.cycleLength_mem_cycleSpectrum {α : Type u} [Fintype α] (f : α → α) (x : α) : cycleLength f x ∈ cycleSpectrum f

Every cycle length belongs to the cycle spectrum.

theorem Cslib.FunctionalGraph.pos_of_mem_cycleSpectrum {α : Type u} [Fintype α] (f : α → α) {ℓ : ℕ} (hℓ : ℓ ∈ cycleSpectrum f) : 0 < ℓ

Every element of the cycle spectrum is positive.

theorem Cslib.FunctionalGraph.spectrum_test {α : Type u} [Fintype α] (f : α → α) (S : Finset ℕ) (x : α) (hS : cycleLength f x ∈ S) (hpos : ∀ ℓ ∈ S, 0 < ℓ) : IsLeast {ℓ : ℕ | ℓ ∈ S ∧ f^[Fintype.card α + ℓ] x = f^[Fintype.card α] x} (cycleLength f x)

The spectrum test. Among any set S of positive candidates containing cycleLength f x, the cycle length is the least element passing the return test at Fintype.card α.

theorem Cslib.FunctionalGraph.cycleSpectrum_test {α : Type u} [Fintype α] (f : α → α) (x : α) : IsLeast {ℓ : ℕ | ℓ ∈ cycleSpectrum f ∧ f^[Fintype.card α + ℓ] x = f^[Fintype.card α] x} (cycleLength f x)

cycleLength f x is the least element of cycleSpectrum f passing the return test at Fintype.card α.

Permutations and injective maps

theorem Cslib.FunctionalGraph.transientDepth_eq_zero_of_injective {α : Type u} [Finite α] (f : α → α) (hf : Function.Injective f) (x : α) : transientDepth f x = 0

For an injective map, every state has transient depth zero.

theorem Cslib.FunctionalGraph.cycleLength_eq_minimalPeriod_of_injective {α : Type u} [Finite α] (f : α → α) (hf : Function.Injective f) (x : α) : cycleLength f x = Function.minimalPeriod f x

For an injective map, the cycle length of x is the minimal period of x.

theorem Cslib.FunctionalGraph.injective_cycle_test_iff {α : Type u} [Finite α] (f : α → α) (hf : Function.Injective f) (x : α) (ℓ : ℕ) : f^[ℓ] x = x ↔ cycleLength f x ∣ ℓ

For an injective map, f^[ℓ] x = x holds iff cycleLength f x ∣ ℓ.

theorem Cslib.FunctionalGraph.injective_spectrum_test {α : Type u} [Finite α] (f : α → α) (hf : Function.Injective f) (S : Finset ℕ) (x : α) (hS : cycleLength f x ∈ S) (hpos : ∀ ℓ ∈ S, 0 < ℓ) : IsLeast {ℓ : ℕ | ℓ ∈ S ∧ f^[ℓ] x = x} (cycleLength f x)

The spectrum test for injective maps, without the shift by Fintype.card α.

theorem Cslib.FunctionalGraph.perm_symm_eq_iterate {α : Type u} [Finite α] (σ : Equiv.Perm α) (x : α) : (Equiv.symm σ) x = (⇑σ)^[cycleLength (⇑σ) x - 1] x

A permutation is inverted by the power one below the cycle length of its argument.

Canonical hitting-time and phase identities

theorem Cslib.FunctionalGraph.canonicalTime_apply {α : Type u} [Finite α] [LinearOrder α] (f : α → α) (x : α) (hx : x ∉ Function.periodicPts f) : canonicalTime f (f x) + 1 = canonicalTime f x

(P1) One step from a transient state lowers canonicalTime by one.

theorem Cslib.FunctionalGraph.iterate_eq_canonical_iff {α : Type u} [Finite α] [LinearOrder α] (f : α → α) (x : α) {T : ℕ} (hT : transientDepth f x ≤ T) (a : ℕ) : f^[T] x = f^[a] (canonicalCycle f x) ↔ a + canonicalTime f x ≡ T [MOD cycleLength f x]

(P2) Past the transient depth, f^[T] x is the state a steps after the least cyclic state canonicalCycle f x iff a + canonicalTime f x ≡ T [MOD cycleLength f x].