Sparse checkpoints in a functional graph

Fix L > 0. Inside a finite set S, greedily pack disjoint simple paths of L states and mark the last state of each. At most |S| / L paths fit, so there are at most |S| / L marks. Every orbit whose first L states lie in S either repeats a state among them, or meets a packed path within L steps and then reaches its mark within L - 1 further steps (exists_checkpoints_on). When S is invariant under f, this applies to every orbit starting in S (exists_checkpoints); on a finite type, to every orbit (exists_checkpoints_finite).

The state type may live in any universe and need not be finite; only S is.

Main definitions

• Cslib.FunctionalGraph.Repeats: the first L states of an orbit contain a repeat.

Main results

• Cslib.FunctionalGraph.exists_checkpoints_on: checkpoints for orbits staying in S.
• Cslib.FunctionalGraph.exists_checkpoints: checkpoints on an invariant finite set.
• Cslib.FunctionalGraph.exists_checkpoints_finite: at most card α / L checkpoints.

References

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

def Cslib.FunctionalGraph.Repeats {α : Type u} (f : α → α) (x : α) (L : ℕ) : Prop

A repeated state among the first L states of an orbit.

theorem Cslib.FunctionalGraph.exists_checkpoints_on {α : Type u} (f : α → α) {L : ℕ} (S : Finset α) (hL : 0 < L) : ∃ H ⊆ S, H.card * L ≤ S.card ∧ ∀ (x : α), (∀ (i : Fin L), f^[↑i] x ∈ S) → Repeats f x L ∨ ∃ d < 2 * L, f^[d] x ∈ H

Checkpoints on a finite set. For L > 0 there are at most |S| / L marks in S such that every orbit whose first L states lie in S repeats a state among them or reaches a mark in fewer than 2 L steps.

theorem Cslib.FunctionalGraph.exists_checkpoints {α : Type u} (f : α → α) {L : ℕ} (S : Finset α) (hS : ∀ x ∈ S, f x ∈ S) (hL : 0 < L) : ∃ H ⊆ S, H.card * L ≤ S.card ∧ ∀ x ∈ S, Repeats f x L ∨ ∃ d < 2 * L, f^[d] x ∈ H

Checkpoints on an invariant set. If S is finite and f maps S into itself, every orbit starting in S repeats a state among its first L or reaches one of at most |S| / L marks in fewer than 2 L steps.

theorem Cslib.FunctionalGraph.exists_checkpoints_finite {α : Type u} (f : α → α) {L : ℕ} [Fintype α] (hL : 0 < L) : ∃ (H : Finset α), H.card ≤ Fintype.card α / L ∧ ∀ (x : α), Repeats f x L ∨ ∃ d < 2 * L, f^[d] x ∈ H

Checkpoints on a finite type, at most card α / L of them.