Checkpoints charged to long trajectories

Fix L > 0. The active states are those of transient depth at least L and the periodic states on cycles of length at least L (activeVertices). Packing checkpoints only inside the active set gives at most |active| / L of them, and still every orbit repeats among its first 4 L states or reaches a checkpoint within 4 L steps (exists_active_checkpoints). The active set need not be invariant: a short transient is skipped within 2 L steps, and a short cycle repeats.

The state type may live in any universe; it is finite.

Main definitions

• Cslib.FunctionalGraph.activeVertices: deep transient states and states of long cycles.

Main results

• Cslib.FunctionalGraph.exists_active_checkpoints: checkpoints charged to the active set.

References

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

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

The states of transient depth at least L and the periodic states on cycles of length at least L.

@[simp]

theorem Cslib.FunctionalGraph.mem_activeVertices {α : Type u} [Fintype α] (f : α → α) (L : ℕ) (x : α) : x ∈ activeVertices f L ↔ L ≤ transientDepth f x ∨ x ∈ Function.periodicPts f ∧ L ≤ cycleLength f x

A state is active exactly when its transient depth is at least L or it is periodic with cycle length at least L.

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

Active checkpoints. For L > 0 there are at most |active| / L checkpoints, all active, such that every orbit repeats a state among its first 4 L or reaches a checkpoint in fewer than 4 L steps.