FiniteFixedPoints.lean

1 import Mathlib.Data.Finset.Card
2 import Mathlib.Data.Fintype.Card
3 
4 /-! Finite fixed-point bounds used by the source-facing Core 8.3 development.
5 Every strict increasing step adds a state; every strict decreasing step removes one.
6 No stabilization hypothesis is supplied by the caller. -/
7 namespace Komorebi.MachineTheory.FiniteFixedPoints
8 
9 variable {X : Type*}
10 
11 def sequence (f : Finset X → Finset X) (s : Finset X) : ℕ → Finset X
12   | 0 => s
13   | n + 1 => f (sequence f s n)
14 
15 @[simp] theorem sequence_zero (f : Finset X → Finset X) (s : Finset X) :
16     sequence f s 0 = s := rfl
17 
18 @[simp] theorem sequence_succ (f : Finset X → Finset X) (s : Finset X) (n : ℕ) :
19     sequence f s (n + 1) = f (sequence f s n) := rfl
20 
21 /-- A genuinely computed inflationary sequence reaches a fixed point within the
22 number of states absent from the starting set. -/
23 theorem increasing_stabilization [Fintype X] (f : Finset X → Finset X)
24     (s : Finset X) (hf : ∀ U, U ⊆ f U) :
25     ∃ n ≤ Fintype.card X - s.card, f (sequence f s n) = sequence f s n := by
26   classical
27   by_contra h
28   have hn : ∀ n, n ≤ Fintype.card X - s.card →
29       f (sequence f s n) ≠ sequence f s n := by
30     intro n hn he
31     exact h ⟨n, hn, he⟩
32   have growth : ∀ n, n ≤ Fintype.card X - s.card + 1 →
33       s.card + n ≤ (sequence f s n).card := by
34     intro n
35     induction n with
36     | zero => intro _; simp
37     | succ n ih =>
38       intro hbound
39       have hnBound : n ≤ Fintype.card X - s.card := by omega
40       have strict : sequence f s n ⊂ f (sequence f s n) :=
41         Finset.ssubset_iff_subset_ne.mpr ⟨hf _, Ne.symm (hn n hnBound)⟩
42       have hc := Finset.card_lt_card strict
43       have hi := ih (by omega)
44       simp only [sequence_succ]
45       omega
46   have final := growth (Fintype.card X - s.card + 1) (by omega)
47   have upper := Finset.card_le_univ (sequence f s (Fintype.card X - s.card + 1))
48   have initial := Finset.card_le_univ s
49   omega
50 
51 /-- A deflationary sequence reaches a fixed point in at most the initial number
52 of states. The ambient type need not be finite for this statement. -/
53 theorem decreasing_stabilization (f : Finset X → Finset X)
54     (s : Finset X) (hf : ∀ U, f U ⊆ U) :
55     ∃ n ≤ s.card, f (sequence f s n) = sequence f s n := by
56   classical
57   by_contra h
58   have hn : ∀ n, n ≤ s.card → f (sequence f s n) ≠ sequence f s n := by
59     intro n hn he
60     exact h ⟨n, hn, he⟩
61   have descent : ∀ n, n ≤ s.card + 1 →
62       n + (sequence f s n).card ≤ s.card := by
63     intro n
64     induction n with
65     | zero => intro _; simp
66     | succ n ih =>
67       intro hbound
68       have hnBound : n ≤ s.card := by omega
69       have strict : f (sequence f s n) ⊂ sequence f s n :=
70         Finset.ssubset_iff_subset_ne.mpr ⟨hf _, hn n hnBound⟩
71       have hc := Finset.card_lt_card strict
72       have hi := ih (by omega)
73       simp only [sequence_succ]
74       omega
75   have final := descent (s.card + 1) (by omega)
76   omega
77 
78 /-- Once the sequence is fixed it remains fixed, without a monotonicity premise. -/
79 theorem fixed_tail (f : Finset X → Finset X) (s : Finset X) (n : ℕ)
80     (hn : f (sequence f s n) = sequence f s n) (k : ℕ) :
81     sequence f s (n + k) = sequence f s n := by
82   induction k with
83   | zero => simp
84   | succ k ih =>
85     rw [Nat.add_succ, sequence_succ, ih, hn]
86 
87 end Komorebi.MachineTheory.FiniteFixedPoints

Back to source controls