Compactness.lean

1 import Std
2 
3 /-!
4 Finite inverse-system compactness, proved from elementary finite-list reasoning.
5 Levels need not have surjective transition maps. The proof uses classical choice.
6 Level 0 represents the manuscript's first residual level (m = 1).
7 -/
8 set_option autoImplicit false
9 namespace PaperX.Compactness
10 
11 /-- A finite family of downward-closed height predicates has an unbounded member
12 if the family has witnesses at every height. -/
13 theorem finite_unbounded_choice {X : Type} (P : X → Nat → Prop)
14     (down : ∀ x i j, i ≤ j → P x j → P x i) (xs : List X)
15     (witnesses : ∀ h, ∃ x, x ∈ xs ∧ P x h) :
16     ∃ x, x ∈ xs ∧ ∀ h, P x h := by
17   classical
18   induction xs with
19   | nil =>
20     obtain ⟨x, hx, _⟩ := witnesses 0
21     simp at hx
22   | cons a xs ih =>
23     by_cases ha : ∀ h, P a h
24     · exact ⟨a, by simp, ha⟩
25     · have bad : ∃ k, ¬ P a k := Classical.not_forall.mp ha
26       obtain ⟨k, hk⟩ := bad
27       have tail : ∀ h, ∃ x, x ∈ xs ∧ P x h := by
28         intro h
29         obtain ⟨x, hx, hp⟩ := witnesses (k+h)
30         have hx' : x = a ∨ x ∈ xs := List.mem_cons.mp hx
31         rcases hx' with hxa | hxt
32         · subst x
33           exact False.elim (hk (down a k (k+h) (by omega) hp))
34         · exact ⟨x, hxt, down x h (k+h) (by omega) hp⟩
35       obtain ⟨x, hx, hp⟩ := ih tail
36       exact ⟨x, List.mem_cons_of_mem a hx, hp⟩
37 
38 structure Tower where
39   Level : Nat → Type
40   parent : (n : Nat) → Level (n+1) → Level n
41 
42 structure Branch (T : Tower) where
43   value : (n : Nat) → T.Level n
44   compatible : ∀ n, T.parent n (value (n+1)) = value n
45 
46 /-- Finiteness is supplied by a complete finite enumeration; repetitions are allowed. -/
47 def FiniteLevels (T : Tower) : Prop :=
48   ∀ n, ∃ xs : List (T.Level n), ∀ x, x ∈ xs
49 
50 def Ext (T : Tower) (n : Nat) : Nat → T.Level n → Prop
51   | 0, _ => True
52   | h+1, x => ∃ y : T.Level (n+1), T.parent n y = x ∧ Ext T (n+1) h y
53 
54 def Live (T : Tower) (n : Nat) (x : T.Level n) : Prop := ∀ h, Ext T n h x
55 
56 theorem ext_step_down (T : Tower) (h : Nat) :
57     ∀ n (x : T.Level n), Ext T n (h+1) x → Ext T n h x := by
58   induction h with
59   | zero => intro n x _; trivial
60   | succ h ih =>
61     intro n x hx
62     obtain ⟨y, hy, he⟩ := hx
63     exact ⟨y, hy, ih (n+1) y he⟩
64 
65 theorem ext_down (T : Tower) (n : Nat) (x : T.Level n)
66     (i j : Nat) (hij : i ≤ j) (hj : Ext T n j x) : Ext T n i x := by
67   induction j with
68   | zero =>
69     have hi : i = 0 := by omega
70     subst i
71     trivial
72   | succ j ih =>
73     by_cases heq : i = j+1
74     · simpa [heq] using hj
75     · exact ih (by omega) (ext_step_down T j n x hj)
76 
77 theorem ext_somewhere (T : Tower) (nonempty : ∀ n, Nonempty (T.Level n))
78     (h : Nat) : ∀ n, ∃ x : T.Level n, Ext T n h x := by
79   induction h with
80   | zero =>
81     intro n
82     obtain ⟨x⟩ := nonempty n
83     exact ⟨x, trivial⟩
84   | succ h ih =>
85     intro n
86     obtain ⟨y, hy⟩ := ih (n+1)
87     exact ⟨T.parent n y, y, rfl, hy⟩
88 
89 theorem live_somewhere (T : Tower) (finite : FiniteLevels T)
90     (nonempty : ∀ n, Nonempty (T.Level n)) (n : Nat) :
91     ∃ x : T.Level n, Live T n x := by
92   obtain ⟨xs, cover⟩ := finite n
93   have witnesses : ∀ h, ∃ x, x ∈ xs ∧ Ext T n h x := by
94     intro h
95     obtain ⟨x, hx⟩ := ext_somewhere T nonempty h n
96     exact ⟨x, cover x, hx⟩
97   obtain ⟨x, _, hx⟩ := finite_unbounded_choice (fun x h => Ext T n h x)
98     (fun x i j hij hj => ext_down T n x i j hij hj) xs witnesses
99   exact ⟨x, hx⟩
100 
101 theorem live_child (T : Tower) (finite : FiniteLevels T)
102     (n : Nat) (x : T.Level n) (hx : Live T n x) :
103     ∃ y : T.Level (n+1), T.parent n y = x ∧ Live T (n+1) y := by
104   obtain ⟨xs, cover⟩ := finite (n+1)
105   let P : T.Level (n+1) → Nat → Prop :=
106     fun y h => T.parent n y = x ∧ Ext T (n+1) h y
107   have witnesses : ∀ h, ∃ y, y ∈ xs ∧ P y h := by
108     intro h
109     obtain ⟨y, hy, he⟩ := hx (h+1)
110     exact ⟨y, cover y, hy, he⟩
111   have down : ∀ y i j, i ≤ j → P y j → P y i := by
112     intro y i j hij hj
113     exact ⟨hj.1, ext_down T (n+1) y i j hij hj.2⟩
114   obtain ⟨y, _, hy⟩ := finite_unbounded_choice P down xs witnesses
115   exact ⟨y, (hy 0).1, fun h => (hy h).2⟩
116 
117 noncomputable def chooseChild (T : Tower) (finite : FiniteLevels T)
118     (n : Nat) (x : {x : T.Level n // Live T n x}) :
119     {y : T.Level (n+1) // Live T (n+1) y} :=
120   ⟨Classical.choose (live_child T finite n x.1 x.2),
121     (Classical.choose_spec (live_child T finite n x.1 x.2)).2⟩
122 
123 theorem chooseChild_parent (T : Tower) (finite : FiniteLevels T)
124     (n : Nat) (x : {x : T.Level n // Live T n x}) :
125     T.parent n (chooseChild T finite n x).1 = x.1 :=
126   (Classical.choose_spec (live_child T finite n x.1 x.2)).1
127 
128 noncomputable def branchNode (T : Tower) (finite : FiniteLevels T)
129     (start : {x : T.Level 0 // Live T 0 x}) :
130     (n : Nat) → {x : T.Level n // Live T n x}
131   | 0 => start
132   | n+1 => chooseChild T finite n (branchNode T finite start n)
133 
134 /-- A finite nonempty tower of sets with total reduction maps has a compatible branch. -/
135 theorem finite_branch_compactness (T : Tower) (finite : FiniteLevels T)
136     (nonempty : ∀ n, Nonempty (T.Level n)) : Nonempty (Branch T) := by
137   classical
138   obtain ⟨x, hx⟩ := live_somewhere T finite nonempty 0
139   let start : {x : T.Level 0 // Live T 0 x} := ⟨x, hx⟩
140   exact ⟨{
141     value := fun n => (branchNode T finite start n).1
142     compatible := fun n => chooseChild_parent T finite n (branchNode T finite start n)
143   }⟩
144 
145 /-- Any empty level prevents completion, not only an empty residual level. -/
146 theorem empty_level_obstruction (T : Tower) (n : Nat)
147     (empty : ¬ Nonempty (T.Level n)) : ¬ Nonempty (Branch T) := by
148   rintro ⟨b⟩
149   exact empty ⟨b.value n⟩
150 
151 /-- For finite levels, arbitrary-depth nonemptiness is equivalent to branch existence. -/
152 theorem branch_iff_levels_nonempty (T : Tower) (finite : FiniteLevels T) :
153     Nonempty (Branch T) ↔ ∀ n, Nonempty (T.Level n) := by
154   constructor
155   · rintro ⟨b⟩ n
156     exact ⟨b.value n⟩
157   · exact finite_branch_compactness T finite
158 
159 /-- Choice can assemble one compatible branch per index, without asserting that
160 any of the level-nonemptiness hypotheses is automatically satisfied. -/
161 theorem indexed_finite_completion {I : Type} (T : I → Tower)
162     (finite : ∀ i, FiniteLevels (T i))
163     (nonempty : ∀ i n, Nonempty ((T i).Level n)) :
164     Nonempty ((i : I) → Branch (T i)) := by
165   classical
166   exact ⟨fun i => Classical.choice (finite_branch_compactness (T i) (finite i) (nonempty i))⟩
167 
168 /-- One missing level in one required tower prevents an indexed completion. -/
169 theorem indexed_empty_level_obstruction {I : Type} (T : I → Tower)
170     (i : I) (n : Nat) (empty : ¬ Nonempty ((T i).Level n)) :
171     ¬ Nonempty ((j : I) → Branch (T j)) := by
172   rintro ⟨b⟩
173   exact empty ⟨(b i).value n⟩
174 
175 end PaperX.Compactness

Back to source controls