Interval labels for finite functional forests

Cut the outgoing edge of each periodic state. For any state x, forestPath f x is the reversed orbit segment from its first periodic point (f^[transientDepth f x] x) down to x. A state y is reached from x before cycle entry (∃ t ≤ transientDepth f x, f^[t] x = y) if and only if forestPath f y is a prefix of forestPath f x (forestPath_prefix).

Under the lexicographic order on root-to-vertex paths, the extensions of any prefix form an order-convex interval (list_prefix_interval). Ranking the |α| root paths (forestRank) and taking the maximum descendant rank (forestUpper) therefore assigns two labels in Fin (Nat.card α) to every state such that ancestry before cycle entry is equivalent to interval containment (forest_interval_spec, exists_forest_intervals).

Main definitions

• Cslib.FunctionalGraph.forestTrace: the first k states of the orbit of x.
• Cslib.FunctionalGraph.forestPath: the root-to-vertex path from f^[transientDepth f x] x to x.
• Cslib.FunctionalGraph.forestRank: the lexicographic rank of forestPath f x in Fin (Fintype.card α).
• Cslib.FunctionalGraph.forestDescendantRanks: the set of ranks of states whose root path has forestPath f x as a prefix.
• Cslib.FunctionalGraph.forestUpper: the inclusive upper endpoint of the subtree interval of x.

Main results

• Cslib.FunctionalGraph.forestPath_prefix: forestPath f y <+: forestPath f x iff y is reached from x within transientDepth f x steps.
• Cslib.FunctionalGraph.list_prefix_interval: lists sharing a prefix form a lexicographic interval.
• Cslib.FunctionalGraph.forest_interval_spec: forestRank and forestUpper characterize ancestry before cycle entry.
• Cslib.FunctionalGraph.exists_forest_intervals: interval labels in Fin (Nat.card α) exist over any finite type [Finite α].

References

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

def Cslib.FunctionalGraph.forestTrace {α : Type u} (f : α → α) (x : α) (k : ℕ) : List α

The first k states of an orbit (List.iterate f x k).

@[simp]

theorem Cslib.FunctionalGraph.length_forestTrace {α : Type u} (f : α → α) (x : α) (k : ℕ) : (forestTrace f x k).length = k

The trace of length k has k states.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestTrace {α : Type u} (f : α → α) (x y : α) (k : ℕ) : y ∈ forestTrace f x k ↔ ∃ i < k, f^[i] x = y

A state lies on the trace of length k exactly when it is f^[i] x for some i < k.

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

The path from cycle entry to x, with the forest edges read backwards.

@[simp]

theorem Cslib.FunctionalGraph.length_forestPath {α : Type u} [Finite α] (f : α → α) (x : α) : (forestPath f x).length = transientDepth f x + 1

The root path of x has one more state than the transient depth of x.

theorem Cslib.FunctionalGraph.forestPath_last {α : Type u} [Finite α] (f : α → α) (x : α) : (forestPath f x).getLast? = some x

The root path of x ends at x.

theorem Cslib.FunctionalGraph.forestPath_injective {α : Type u} [Finite α] (f : α → α) : Function.Injective (forestPath f)

Distinct states have distinct root paths.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestPath {α : Type u} [Finite α] (f : α → α) (x y : α) : y ∈ forestPath f x ↔ ∃ i ≤ transientDepth f x, f^[i] x = y

A state lies on the root path of x exactly when it is f^[i] x for some i ≤ transientDepth f x.

theorem Cslib.FunctionalGraph.self_mem_forestPath {α : Type u} [Finite α] (f : α → α) (x : α) : x ∈ forestPath f x

Every state lies on its own root path.

theorem Cslib.FunctionalGraph.forestPath_prefix {α : Type u} [Finite α] (f : α → α) (x y : α) : forestPath f y <+: forestPath f x ↔ ∃ t ≤ transientDepth f x, f^[t] x = y

Prefixes of root paths are exactly the ancestors before cycle entry.

theorem Cslib.FunctionalGraph.list_prefix_interval {α : Type u} [LinearOrder α] {p a b c : List α} (ha : p <+: a) (hb : p <+: b) (hac : a ≤ c) (hcb : c ≤ b) : p <+: c

Lists with a common prefix form a lexicographic interval.

theorem Cslib.FunctionalGraph.list_prefix_le {α : Type u} [LinearOrder α] {a b : List α} (h : a <+: b) : a ≤ b

A list is lexicographically at most every list it is a prefix of.

noncomputable def Cslib.FunctionalGraph.forestRank {α : Type u} [Finite α] (f : α → α) [Fintype α] [LinearOrder α] (x : α) : Fin (Fintype.card α)

The rank of the root path in the lexicographic order of all root paths.

theorem Cslib.FunctionalGraph.forestRank_le {α : Type u} [Finite α] (f : α → α) [Fintype α] [LinearOrder α] (x y : α) : forestRank f x ≤ forestRank f y ↔ forestPath f x ≤ forestPath f y

Ranks compare exactly as the root paths compare lexicographically.

noncomputable def Cslib.FunctionalGraph.forestDescendantRanks {α : Type u} [Finite α] (f : α → α) [Fintype α] [LinearOrder α] (x : α) : Finset (Fin (Fintype.card α))

All descendant ranks, including the vertex's own rank.

@[simp]

theorem Cslib.FunctionalGraph.mem_forestDescendantRanks {α : Type u} [Finite α] (f : α → α) [Fintype α] [LinearOrder α] (x : α) (r : Fin (Fintype.card α)) : r ∈ forestDescendantRanks f x ↔ ∃ (y : α), forestPath f x <+: forestPath f y ∧ forestRank f y = r

A rank is a descendant rank of x exactly when it is the rank of a state whose root path extends that of x.

theorem Cslib.FunctionalGraph.forestDescendantRanks_nonempty {α : Type u} [Finite α] (f : α → α) [Fintype α] [LinearOrder α] (x : α) : (forestDescendantRanks f x).Nonempty

Every state has a descendant rank, namely its own.

noncomputable def Cslib.FunctionalGraph.forestUpper {α : Type u} [Finite α] (f : α → α) [Fintype α] [LinearOrder α] (x : α) : Fin (Fintype.card α)

The inclusive upper endpoint of a subtree's rank interval.

theorem Cslib.FunctionalGraph.forest_interval_spec {α : Type u} [Finite α] (f : α → α) [Fintype α] [LinearOrder α] (x y : α) : forestRank f y ≤ forestRank f x ∧ forestRank f x ≤ forestUpper f y ↔ ∃ t ≤ transientDepth f x, f^[t] x = y

Two bounded labels suffice to test ancestry in the cut functional forest.

theorem Cslib.FunctionalGraph.exists_forest_intervals {α : Type u} [Finite α] (f : α → α) : ∃ (low : α → Fin (Nat.card α)) (high : α → Fin (Nat.card α)), ∀ (x y : α), low y ≤ low x ∧ low x ≤ high y ↔ ∃ t ≤ transientDepth f x, f^[t] x = y

Interval labels exist over every finite universe, without an input order.