Orbits of a self-map on a finite type

The quantitative facts every fixed-point iteration in this library rests on, stated for a bare self-map f : α → α with no logic in sight:

• once an orbit plateaus it is constant (DescriptiveComplexity.iterate_eq_of_isFixedPt);
• an orbit on a finite type repeats within Nat.card α steps (DescriptiveComplexity.exists_iterate_eq_of_finite), so if it ever reaches a fixed point, the Nat.card α-th iterate already is one (DescriptiveComplexity.isFixedPt_iterate_card_iff) – the pigeonhole behind the partial fixed-point semantics;
• an inflationary map on the subsets of a finite type reaches a fixed point within Nat.card X steps – the height of the subset lattice, not its size (DescriptiveComplexity.isFixedPt_iterate_card_of_subset), via the plateau of any monotone chain of subsets (DescriptiveComplexity.exists_succ_eq_of_monotone_subset, with the dual DescriptiveComplexity.exists_succ_eq_of_antitone_subset for descending refinement chains).

Consumers: the stages of DescriptiveComplexity.derivesIn (DescriptiveComplexity.FixedPoint), the inflationary and partial iterations of DescriptiveComplexity.StepDef (DescriptiveComplexity.FixedPointStep), and any future exponential iteration (SO(LFP), SO(PFP)). Everything is stated over an arbitrary starting point, so ascending chains from ⊥ and descending chains from ⊤ are both instances.

Constancy from a plateau

theorem DescriptiveComplexity.iterate_eq_of_isFixedPt {α : Type u_1} {f : α → α} {a : α} {N : ℕ} (h : Function.IsFixedPt f (f^[N] a)) {n : ℕ} (hn : N ≤ n) : f^[n] a = f^[N] a

Once an orbit reaches a fixed point, it stays there: the orbit is constant from any index whose value is a fixed point.

Pigeonhole: repeats and eventual periodicity

theorem DescriptiveComplexity.exists_iterate_eq_of_finite {α : Type u_1} [Finite α] (f : α → α) (a : α) : ∃ (i : ℕ) (j : ℕ), i < j ∧ j ≤ Nat.card α ∧ f^[i] a = f^[j] a

An orbit on a finite type repeats within Nat.card α steps.

theorem DescriptiveComplexity.isFixedPt_iterate_card_iff {α : Type u_1} [Finite α] (f : α → α) (a : α) : Function.IsFixedPt f (f^[Nat.card α] a) ↔ ∃ (n : ℕ), Function.IsFixedPt f (f^[n] a)

If an orbit on a finite type ever reaches a fixed point, the Nat.card α-th iterate already is one. This is what bounds the partial fixed-point iteration: convergence, if it happens at all, happens within the number of states.

Monotone chains of subsets plateau within the cardinality

The bound here is Nat.card X – the height of the subset lattice – rather than the 2 ^ Nat.card X states a bare pigeonhole would give.

theorem DescriptiveComplexity.exists_succ_eq_of_monotone_subset {X : Type u_2} [Finite X] {c : ℕ → Set X} (hc : ∀ (n : ℕ), c n ⊆ c (n + 1)) : ∃ N ≤ Nat.card X, c (N + 1) = c N

A monotone chain of subsets of a finite type plateaus within Nat.card X steps.

theorem DescriptiveComplexity.exists_succ_eq_of_antitone_subset {X : Type u_2} [Finite X] {c : ℕ → Set X} (hc : ∀ (n : ℕ), c (n + 1) ⊆ c n) : ∃ N ≤ Nat.card X, c (N + 1) = c N

An antitone chain of subsets of a finite type plateaus within Nat.card X steps: the dual of DescriptiveComplexity.exists_succ_eq_of_monotone_subset, for descending refinement chains.

theorem DescriptiveComplexity.isFixedPt_iterate_card_of_subset {X : Type u_2} [Finite X] {f : Set X → Set X} (hf : ∀ (s : Set X), s ⊆ f s) (s : Set X) : Function.IsFixedPt f (f^[Nat.card X] s)

An inflationary map on the subsets of a finite type reaches a fixed point within Nat.card X steps, from any starting point: the chain of iterates can only grow Nat.card X many times.