The forest generated by checkpoint-to-cycle paths

Cut outgoing edges at periodic states (transientDepth f x = 0). Closing a finite checkpoint set H along the remaining transient paths yields a finite directed forest checkpointHull f H whose roots are the cycle entry points reached from H (forestRoots f H) and whose leaves all lie in H (forestLeaves_subset).

Adding the roots and the branching states (forestBranches f H, states with at least two predecessors in forestSources f H) to H produces the refined mark set forestMarks f H. Because every branch and every root is paid for by a distinct leaf in H (forestBranches_roots_le_leaves), the refined set has at most 2 |H| states (forestMarks_card), and outside forestMarks f H every state in the hull has at most one hull predecessor (forestPredecessor_unique).

Main definitions

• Cslib.FunctionalGraph.checkpointHull: states reached from H up to their first periodic point.
• Cslib.FunctionalGraph.forestSources: transient states in checkpointHull f H.
• Cslib.FunctionalGraph.forestChildren: predecessors of a state in forestSources f H.
• Cslib.FunctionalGraph.forestRoots: periodic states in checkpointHull f H.
• Cslib.FunctionalGraph.forestLeaves: hull states with no predecessor in forestSources f H.
• Cslib.FunctionalGraph.forestBranches: hull states with at least two predecessors in forestSources f H.
• Cslib.FunctionalGraph.forestMarks: refined checkpoint set H ∪ (forestRoots f H ∪ forestBranches f H).

Main results

• Cslib.FunctionalGraph.forestLeaves_subset: every leaf of the checkpoint hull belongs to H.
• Cslib.FunctionalGraph.sum_forestChildren: child counts across the hull sum to |forestSources f H|.
• Cslib.FunctionalGraph.forestBranches_roots_le_leaves: branches and roots are bounded by leaves.
• Cslib.FunctionalGraph.forestMarks_card: (forestMarks f H).card ≤ 2 * H.card.
• Cslib.FunctionalGraph.forestPredecessor_unique: unmarked states have at most one predecessor in forestSources f H.

References

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

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

Follow each checkpoint in H along its orbit up to its first periodic point.

@[simp]

theorem Cslib.FunctionalGraph.mem_checkpointHull {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x : α) : x ∈ checkpointHull f H ↔ ∃ h ∈ H, ∃ t ≤ transientDepth f h, f^[t] h = x

A state lies in the checkpoint hull exactly when it is f^[t] h for some h ∈ H and t ≤ transientDepth f h.

theorem Cslib.FunctionalGraph.subset_checkpointHull {α : Type u} [Finite α] (f : α → α) (H : Finset α) : H ⊆ checkpointHull f H

Every checkpoint lies in the checkpoint hull.

theorem Cslib.FunctionalGraph.checkpointHull_subset_of_subset {α : Type u} [Finite α] (f : α → α) {H₁ H₂ : Finset α} (h : H₁ ⊆ H₂) : checkpointHull f H₁ ⊆ checkpointHull f H₂

The checkpoint hull is monotone in the checkpoint set.

theorem Cslib.FunctionalGraph.checkpointHull_iterate {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x : α} (hx : x ∈ checkpointHull f H) {t : ℕ} (ht : t ≤ transientDepth f x) : f^[t] x ∈ checkpointHull f H

The checkpoint hull contains the orbit of each of its states up to that state's transient depth.

theorem Cslib.FunctionalGraph.checkpointHull_step {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x : α} (hx : x ∈ checkpointHull f H) (ht : 0 < transientDepth f x) : f x ∈ checkpointHull f H

The checkpoint hull contains the successor of each of its transient states.

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

Sources of the forest edges after cutting outgoing edges at periodic vertices.

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

Predecessors of x in forestSources f H.

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

Periodic vertices in checkpointHull f H (the roots of the cut forest).

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

Vertices of checkpointHull f H with no predecessor in forestSources f H.

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

Vertices of checkpointHull f H with at least two predecessors in forestSources f H.

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

The refined mark set consisting of H, the forest roots, and the branching vertices.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestSources {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x : α) : x ∈ forestSources f H ↔ x ∈ checkpointHull f H ∧ 0 < transientDepth f x

The forest sources are exactly the hull states of positive transient depth.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestChildren {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x y : α) : y ∈ forestChildren f H x ↔ y ∈ checkpointHull f H ∧ 0 < transientDepth f y ∧ f y = x

The children of x are exactly the hull states of positive transient depth that f maps to x.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestRoots {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x : α) : x ∈ forestRoots f H ↔ x ∈ checkpointHull f H ∧ transientDepth f x = 0

The forest roots are exactly the hull states of transient depth zero.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestLeaves {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x : α) : x ∈ forestLeaves f H ↔ x ∈ checkpointHull f H ∧ (forestChildren f H x).card = 0

The forest leaves are exactly the hull states with no children.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestBranches {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x : α) : x ∈ forestBranches f H ↔ x ∈ checkpointHull f H ∧ 2 ≤ (forestChildren f H x).card

The forest branches are exactly the hull states with at least two children.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestMarks {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x : α) : x ∈ forestMarks f H ↔ x ∈ H ∨ x ∈ forestRoots f H ∨ x ∈ forestBranches f H

A state is marked exactly when it is a checkpoint, a forest root, or a forest branch.

theorem Cslib.FunctionalGraph.forestLeaves_subset {α : Type u} [Finite α] (f : α → α) (H : Finset α) : forestLeaves f H ⊆ H

Every leaf of the checkpoint hull belongs to H.

theorem Cslib.FunctionalGraph.sum_forestChildren {α : Type u} [Finite α] (f : α → α) (H : Finset α) : ∑ x ∈ checkpointHull f H, (forestChildren f H x).card = (forestSources f H).card

Count each nonroot's outgoing edge at its parent.

theorem Cslib.FunctionalGraph.forestBranches_roots_le_leaves {α : Type u} [Finite α] (f : α → α) (H : Finset α) : (forestBranches f H).card + (forestRoots f H).card ≤ (forestLeaves f H).card

Branches and roots together are paid for by distinct leaves.

theorem Cslib.FunctionalGraph.subset_forestMarks {α : Type u} [Finite α] (f : α → α) (H : Finset α) : H ⊆ forestMarks f H

Every checkpoint is marked.

theorem Cslib.FunctionalGraph.forestRoots_subset_marks {α : Type u} [Finite α] (f : α → α) (H : Finset α) : forestRoots f H ⊆ forestMarks f H

Every forest root is marked.

theorem Cslib.FunctionalGraph.forestBranches_subset_marks {α : Type u} [Finite α] (f : α → α) (H : Finset α) : forestBranches f H ⊆ forestMarks f H

Every forest branch is marked.

theorem Cslib.FunctionalGraph.forestMarks_subset_hull {α : Type u} [Finite α] (f : α → α) (H : Finset α) : forestMarks f H ⊆ checkpointHull f H

Every marked state lies in the checkpoint hull.

theorem Cslib.FunctionalGraph.forestMarks_card {α : Type u} [Finite α] (f : α → α) (H : Finset α) : (forestMarks f H).card ≤ 2 * H.card

Refinement to a compressed forest needs at most twice as many marks.

theorem Cslib.FunctionalGraph.forestRoot_mem_marks {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x : α} (hx : x ∈ checkpointHull f H) (hd : transientDepth f x = 0) : x ∈ forestMarks f H

A hull state of transient depth zero is marked.

theorem Cslib.FunctionalGraph.forestPredecessor_unique {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x y z : α} (hx : x ∈ forestSources f H) (hy : y ∈ forestSources f H) (hfx : f x = z) (hfy : f y = z) (hz : z ∉ forestMarks f H) : x = y

Between marks, two hull paths cannot merge.