Catalog/Sparsity/NDImpliesUQW/Full.lean
| 1 | import Catalog.Sparsity.Preliminaries.Full |
| 2 | import Catalog.Sparsity.NowhereDense.Full |
| 3 | import Catalog.Sparsity.UniformQuasiWideness.Full |
| 4 | import Catalog.Sparsity.ShallowMinor.Full |
| 5 | import Catalog.Sparsity.ShallowTopologicalMinor.Full |
| 6 | import Catalog.Sparsity.OddStepReduction.Full |
| 7 | import Catalog.Sparsity.EvenStepReduction.Full |
| 8 | import Catalog.Sparsity.IterativeBipartiteRamsey.Full |
| 9 | import Catalog.Sparsity.Ramsey.Full |
| 10 | |
| 11 | namespace Catalog.Sparsity.NDImpliesUQW |
| 12 | |
| 13 | open Catalog.Sparsity.Preliminaries Catalog.Sparsity.NowhereDense Catalog.Sparsity.UniformQuasiWideness |
| 14 | open Catalog.Sparsity.ShallowMinor |
| 15 | open Catalog.Sparsity.ShallowTopologicalMinor |
| 16 | open Catalog.Sparsity.OddStepReduction Catalog.Sparsity.EvenStepReduction |
| 17 | open Catalog.Sparsity.IterativeBipartiteRamsey Catalog.Sparsity.Ramsey |
| 18 | |
| 19 | /-! ## Helper lemmas -/ |
| 20 | |
| 21 | /-- Lift an H-walk to a G-walk through composed branch sets. -/ |
| 22 | private theorem liftWalk {V W : Type} |
| 23 | {H : SimpleGraph W} {G : SimpleGraph V} {a : ℕ} |
| 24 | (MHG : ShallowMinorModel H G a) |
| 25 | {w₁ w₃ : W} (q : H.Walk w₁ w₃) : |
| 26 | ∃ qG : G.Walk (MHG.center w₁) (MHG.center w₃), |
| 27 | qG.length ≤ (2 * a + 1) * q.length ∧ |
| 28 | ∀ x ∈ qG.support, ∃ w' ∈ q.support, x ∈ MHG.branchSet w' := by |
| 29 | induction q with |
| 30 | | nil => |
| 31 | exact ⟨.nil, by simp, fun x hx => by |
| 32 | simp only [SimpleGraph.Walk.support_nil, List.mem_cons, |
| 33 | List.mem_nil_iff, or_false] at hx ⊢ |
| 34 | exact ⟨_, rfl, hx ▸ MHG.center_mem _⟩⟩ |
| 35 | | @cons wa wb wc hadj_H rest ih_rest => |
| 36 | obtain ⟨q_rest, hq_rest_len, hq_rest_sup⟩ := ih_rest |
| 37 | obtain ⟨x, hx, y, hy, hadj_G⟩ := MHG.branchEdge wa wb hadj_H |
| 38 | obtain ⟨p1, _, hp1len, hp1sup⟩ := MHG.branchRadius wa x hx |
| 39 | obtain ⟨p2, _, hp2len, hp2sup⟩ := MHG.branchRadius wb y hy |
| 40 | refine ⟨(p1.append (.cons hadj_G p2.reverse)).append q_rest, ?_, ?_⟩ |
| 41 | · simp only [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons, |
| 42 | SimpleGraph.Walk.length_reverse] |
| 43 | calc p1.length + (p2.length + 1) + q_rest.length |
| 44 | ≤ a + (a + 1) + (2 * a + 1) * rest.length := by omega |
| 45 | _ = (2 * a + 1) * rest.length + (2 * a + 1) := by omega |
| 46 | _ = (2 * a + 1) * (rest.length + 1) := by rw [Nat.mul_add, Nat.mul_one] |
| 47 | · intro z hz |
| 48 | rw [SimpleGraph.Walk.support_append] at hz |
| 49 | rcases List.mem_append.mp hz with hz | hz |
| 50 | · rw [SimpleGraph.Walk.support_append] at hz |
| 51 | rcases List.mem_append.mp hz with hz | hz |
| 52 | · exact ⟨wa, .head _, hp1sup z hz⟩ |
| 53 | · have hz' := List.tail_subset _ hz |
| 54 | rw [SimpleGraph.Walk.support_cons] at hz' |
| 55 | rcases List.mem_cons.mp hz' with rfl | hz' |
| 56 | · exact ⟨wa, .head _, hx⟩ |
| 57 | · rw [SimpleGraph.Walk.support_reverse] at hz' |
| 58 | exact ⟨wb, .tail _ (SimpleGraph.Walk.start_mem_support _), |
| 59 | hp2sup z (List.mem_reverse.mp hz')⟩ |
| 60 | · obtain ⟨w', hw', hz'⟩ := hq_rest_sup z (List.tail_subset _ hz) |
| 61 | exact ⟨w', .tail _ hw', hz'⟩ |
| 62 | |
| 63 | /-- Composition of shallow minors: if `K ⪯_b H` and `H ⪯_a G`, then |
| 64 | `K ⪯_{2ab+a+b} G`. -/ |
| 65 | private theorem shallowMinor_compose {U V W : Type} |
| 66 | {K : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ} |
| 67 | (hKH : IsShallowMinor K H b) (hHG : IsShallowMinor H G a) : |
| 68 | IsShallowMinor K G (2 * a * b + a + b) := by |
| 69 | let MKH := hKH.some; let MHG := hHG.some |
| 70 | exact ⟨{ |
| 71 | branchSet := fun u => ⋃ w ∈ MKH.branchSet u, MHG.branchSet w |
| 72 | center := fun u => MHG.center (MKH.center u) |
| 73 | center_mem := fun u => Set.mem_biUnion (MKH.center_mem u) (MHG.center_mem _) |
| 74 | branchDisjoint := fun u₁ u₂ h => |
| 75 | Set.disjoint_left.mpr fun v hv1 hv2 => by |
| 76 | simp only [Set.mem_iUnion] at hv1 hv2 |
| 77 | obtain ⟨w1, hw1, hv1⟩ := hv1; obtain ⟨w2, hw2, hv2⟩ := hv2 |
| 78 | rcases eq_or_ne w1 w2 with rfl | hne |
| 79 | · exact Set.disjoint_left.mp (MKH.branchDisjoint u₁ u₂ h) hw1 hw2 |
| 80 | · exact Set.disjoint_left.mp (MHG.branchDisjoint w1 w2 hne) hv1 hv2 |
| 81 | branchRadius := fun u v hv => by |
| 82 | classical |
| 83 | simp only [Set.mem_iUnion] at hv |
| 84 | obtain ⟨w, hw, hv⟩ := hv |
| 85 | obtain ⟨pH, _, hlenH, hsupH⟩ := MKH.branchRadius u w hw |
| 86 | obtain ⟨pG_tail, _, hlenG_tail, hsupG_tail⟩ := MHG.branchRadius w v hv |
| 87 | obtain ⟨qG, hqGlen, hqGsup⟩ := liftWalk MHG pH |
| 88 | let full := qG.append pG_tail |
| 89 | let p' := full.bypass |
| 90 | refine ⟨p', full.bypass_isPath, ?_, ?_⟩ |
| 91 | · have hfl := SimpleGraph.Walk.length_append qG pG_tail |
| 92 | have hqG_bound : qG.length ≤ 2 * a * b + b := by |
| 93 | have h1 := Nat.mul_le_mul_left (2 * a + 1) hlenH |
| 94 | have : (2 * a + 1) * b = 2 * a * b + b := by |
| 95 | rw [Nat.add_mul, Nat.one_mul, Nat.mul_assoc] |
| 96 | omega |
| 97 | calc p'.length ≤ full.length := full.length_bypass_le |
| 98 | _ = qG.length + pG_tail.length := hfl |
| 99 | _ ≤ 2 * a * b + a + b := by omega |
| 100 | · intro x hx |
| 101 | have hx' := full.support_bypass_subset hx |
| 102 | rw [SimpleGraph.Walk.support_append] at hx' |
| 103 | rcases List.mem_append.mp hx' with h | h |
| 104 | · obtain ⟨w', hw', hxw'⟩ := hqGsup x h |
| 105 | exact Set.mem_biUnion (hsupH w' hw') hxw' |
| 106 | · exact Set.mem_biUnion hw (hsupG_tail x (List.tail_subset _ h)) |
| 107 | branchEdge := fun u₁ u₂ hadj => by |
| 108 | obtain ⟨w1, hw1, w2, hw2, hadjH⟩ := MKH.branchEdge u₁ u₂ hadj |
| 109 | obtain ⟨x, hx, y, hy, hadjG⟩ := MHG.branchEdge w1 w2 hadjH |
| 110 | exact ⟨x, Set.mem_biUnion hw1 hx, y, Set.mem_biUnion hw2 hy, hadjG⟩ }⟩ |
| 111 | |
| 112 | /-- A depth-`d` minor of `deleteVerts G S` is a depth-`d` minor of `G`. -/ |
| 113 | private theorem shallowMinor_of_subgraph {U V : Type} |
| 114 | {H : SimpleGraph U} {G G' : SimpleGraph V} {d : ℕ} |
| 115 | (hsub : ∀ {u v}, G.Adj u v → G'.Adj u v) |
| 116 | (h : IsShallowMinor H G d) : |
| 117 | IsShallowMinor H G' d := by |
| 118 | let M := h.some |
| 119 | exact ⟨{ |
| 120 | branchSet := M.branchSet |
| 121 | center := M.center |
| 122 | center_mem := M.center_mem |
| 123 | branchDisjoint := M.branchDisjoint |
| 124 | branchRadius := fun v x hx => by |
| 125 | obtain ⟨p, hp, hlen, hsup⟩ := M.branchRadius v x hx |
| 126 | have hedge : ∀ e ∈ p.edges, e ∈ G'.edgeSet := by |
| 127 | intro e he |
| 128 | have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he |
| 129 | revert hmem |
| 130 | refine e.ind ?_ |
| 131 | intro a b hab |
| 132 | exact show G'.Adj a b by exact hsub hab |
| 133 | exact ⟨p.transfer G' hedge, hp.transfer hedge, |
| 134 | by rw [SimpleGraph.Walk.length_transfer]; exact hlen, |
| 135 | by rw [SimpleGraph.Walk.support_transfer]; exact hsup⟩ |
| 136 | branchEdge := fun u v hadj => by |
| 137 | obtain ⟨x, hx, y, hy, hadj'⟩ := M.branchEdge u v hadj |
| 138 | exact ⟨x, hx, y, hy, hsub hadj'⟩ }⟩ |
| 139 | |
| 140 | /-- A depth-`d` minor of `deleteVerts G S` is a depth-`d` minor of `G`. -/ |
| 141 | private theorem shallowMinor_of_deleteVerts {V W : Type} |
| 142 | {H : SimpleGraph W} {G : SimpleGraph V} {S : Set V} {d : ℕ} |
| 143 | (h : IsShallowMinor H (deleteVerts G S) d) : |
| 144 | IsShallowMinor H G d := by |
| 145 | exact shallowMinor_of_subgraph (fun {u v} h' => by |
| 146 | have h'' : G.Adj u v ∧ u ∉ S ∧ v ∉ S := by |
| 147 | simpa [deleteVerts] using h' |
| 148 | exact h''.1) h |
| 149 | |
| 150 | /-- Every set is distance-0 independent: any walk between distinct vertices has |
| 151 | length ≥ 1 > 0. -/ |
| 152 | private lemma distIndependent_zero {V : Type} (G : SimpleGraph V) (A : Set V) : |
| 153 | DistIndependent G 0 A := by |
| 154 | intro u _ v _ huv p |
| 155 | exact Nat.pos_of_ne_zero fun h => huv (SimpleGraph.Walk.eq_of_length_eq_zero h) |
| 156 | |
| 157 | /-- `deleteVerts G ∅` preserves `DistIndependent`. -/ |
| 158 | private lemma distIndependent_deleteVerts_empty {V : Type} |
| 159 | {G : SimpleGraph V} {r : ℕ} {A : Set V} |
| 160 | (h : DistIndependent G r A) : |
| 161 | DistIndependent (deleteVerts G (∅ : Set V)) r A := by |
| 162 | convert h using 1; ext u v; simp [deleteVerts] |
| 163 | |
| 164 | /-- Coercion helper: `↑(∅ : Finset V) = (∅ : Set V)`. -/ |
| 165 | private lemma finset_coe_empty {V : Type} : |
| 166 | (↑(∅ : Finset V) : Set V) = (∅ : Set V) := Finset.coe_empty |
| 167 | |
| 168 | /-- `deleteVerts` is associative: removing `S₁` then `S₂` = removing `S₁ ∪ S₂`. -/ |
| 169 | private lemma deleteVerts_deleteVerts {V : Type} (G : SimpleGraph V) (S₁ S₂ : Set V) : |
| 170 | deleteVerts (deleteVerts G S₁) S₂ = deleteVerts G (S₁ ∪ S₂) := by |
| 171 | ext u v; simp only [deleteVerts, Set.mem_union, not_or]; tauto |
| 172 | |
| 173 | /-- A clique of size `n` gives `completeGraph (Fin n)` as a depth-0 minor. -/ |
| 174 | private lemma clique_gives_minor {V : Type} [DecidableEq V] [Fintype V] |
| 175 | {G : SimpleGraph V} {n : ℕ} |
| 176 | (h : ¬G.CliqueFree n) : |
| 177 | IsShallowMinor (SimpleGraph.completeGraph (Fin n)) G 0 := by |
| 178 | rw [SimpleGraph.not_cliqueFree_iff] at h |
| 179 | obtain ⟨f⟩ := h |
| 180 | exact ⟨{ |
| 181 | branchSet := fun i => {f i} |
| 182 | center := fun i => f i |
| 183 | center_mem := fun _ => Set.mem_singleton _ |
| 184 | branchDisjoint := fun i j hij => by |
| 185 | exact Set.disjoint_singleton.mpr (fun h => hij (f.injective h)) |
| 186 | branchRadius := fun i x hx => by |
| 187 | rw [Set.mem_singleton_iff] at hx; subst hx |
| 188 | exact ⟨.nil, .nil, le_refl _, fun w hw => by |
| 189 | rw [SimpleGraph.Walk.support_nil, List.mem_cons, List.mem_nil_iff, or_false] at hw |
| 190 | rw [hw]; exact Set.mem_singleton _⟩ |
| 191 | branchEdge := fun i j hij => by |
| 192 | exact ⟨f i, Set.mem_singleton _, f j, Set.mem_singleton _, |
| 193 | (f.toHom.map_adj hij : G.Adj (f i) (f j))⟩ }⟩ |
| 194 | |
| 195 | /-- A clique in `Gᶜ` gives a distance-1 independent set in `G`. -/ |
| 196 | private lemma compl_clique_distIndep {V : Type} [DecidableEq V] [Fintype V] |
| 197 | {G : SimpleGraph V} {n : ℕ} |
| 198 | (h : ¬Gᶜ.CliqueFree n) : |
| 199 | ∃ B : Finset V, n ≤ B.card ∧ DistIndependent G 1 ↑B := by |
| 200 | rw [SimpleGraph.not_cliqueFree_iff] at h |
| 201 | obtain ⟨f⟩ := h |
| 202 | refine ⟨Finset.univ.map f.toEmbedding, ?_, ?_⟩ |
| 203 | · simp [Finset.card_map] |
| 204 | · intro u hu v hv huv p |
| 205 | simp only [Finset.coe_map, Finset.coe_univ, Set.image_univ, Set.mem_range] at hu hv |
| 206 | obtain ⟨i, rfl⟩ := hu; obtain ⟨j, rfl⟩ := hv |
| 207 | have hij : i ≠ j := fun h => huv (congrArg f h) |
| 208 | have hnadj : ¬G.Adj (f i) (f j) := by |
| 209 | have := f.toHom.map_adj (hij : (SimpleGraph.completeGraph (Fin n)).Adj i j) |
| 210 | simp only [SimpleGraph.compl_adj] at this |
| 211 | exact this.2 |
| 212 | by_contra hle; push_neg at hle |
| 213 | rcases Nat.le_one_iff_eq_zero_or_eq_one.mp hle with h0 | h1 |
| 214 | · exact huv (SimpleGraph.Walk.eq_of_length_eq_zero h0) |
| 215 | · exact hnadj (SimpleGraph.Walk.adj_of_length_eq_one h1) |
| 216 | |
| 217 | /-- From the complete bipartite data K_{t,t}, build K_t as a depth-1 minor. -/ |
| 218 | private lemma ktt_gives_minor {V : Type} [DecidableEq V] [Fintype V] |
| 219 | {G : SimpleGraph V} {X Y : Finset V} {t : ℕ} |
| 220 | (hXY : Disjoint X Y) |
| 221 | (htX : t ≤ X.card) (htY : t ≤ Y.card) |
| 222 | (hAdj : ∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) : |
| 223 | IsShallowMinor (SimpleGraph.completeGraph (Fin t)) G 1 := by |
| 224 | obtain ⟨fx, hfx⟩ := Function.Embedding.exists_of_card_le_finset |
| 225 | (α := Fin t) (s := X) (by simp; exact htX) |
| 226 | obtain ⟨fy, hfy⟩ := Function.Embedding.exists_of_card_le_finset |
| 227 | (α := Fin t) (s := Y) (by simp; exact htY) |
| 228 | exact ⟨{ |
| 229 | branchSet := fun i => {fx i, fy i} |
| 230 | center := fun i => fx i |
| 231 | center_mem := fun i => Set.mem_insert _ _ |
| 232 | branchDisjoint := fun i j hij => by |
| 233 | have hfxi : fx i ∈ X := Finset.mem_coe.mp (hfx (Set.mem_range_self i)) |
| 234 | have hfxj : fx j ∈ X := Finset.mem_coe.mp (hfx (Set.mem_range_self j)) |
| 235 | have hfyi : fy i ∈ Y := Finset.mem_coe.mp (hfy (Set.mem_range_self i)) |
| 236 | have hfyj : fy j ∈ Y := Finset.mem_coe.mp (hfy (Set.mem_range_self j)) |
| 237 | exact Set.disjoint_left.mpr fun x hx1 hx2 => by |
| 238 | simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hx1 hx2 |
| 239 | rcases hx1 with rfl | rfl <;> rcases hx2 with h | h |
| 240 | · exact hij (fx.injective h) |
| 241 | · exact Finset.disjoint_left.mp hXY hfxi (h ▸ hfyj) |
| 242 | · exact Finset.disjoint_left.mp hXY (h ▸ hfxj) hfyi |
| 243 | · exact hij (fy.injective h) |
| 244 | branchRadius := fun i x hx => by |
| 245 | rcases hx with rfl | rfl |
| 246 | · exact ⟨.nil, .nil, Nat.zero_le _, fun w hw => by |
| 247 | rw [SimpleGraph.Walk.support_nil, List.mem_cons, List.mem_nil_iff, or_false] at hw |
| 248 | rw [hw]; exact Set.mem_insert _ _⟩ |
| 249 | · have hfxi : fx i ∈ X := Finset.mem_coe.mp (hfx (Set.mem_range_self i)) |
| 250 | have hfyi : fy i ∈ Y := Finset.mem_coe.mp (hfy (Set.mem_range_self i)) |
| 251 | have hadj := hAdj (fx i) hfxi (fy i) hfyi |
| 252 | have hne : fx i ≠ fy i := fun h => |
| 253 | Finset.disjoint_left.mp hXY hfxi (h ▸ hfyi) |
| 254 | exact ⟨.cons hadj .nil, |
| 255 | ⟨⟨by simp [SimpleGraph.Walk.edges_cons]⟩, |
| 256 | by simp [SimpleGraph.Walk.support_cons, SimpleGraph.Walk.support_nil, hne]⟩, |
| 257 | le_refl _, |
| 258 | fun w hw => by |
| 259 | simp [SimpleGraph.Walk.support_cons, SimpleGraph.Walk.support_nil] at hw |
| 260 | rcases hw with rfl | rfl |
| 261 | · exact Set.mem_insert _ _ |
| 262 | · exact Set.mem_insert_of_mem _ rfl⟩ |
| 263 | branchEdge := fun i j hij => by |
| 264 | have hfxi : fx i ∈ X := Finset.mem_coe.mp (hfx (Set.mem_range_self i)) |
| 265 | have hfyj : fy j ∈ Y := Finset.mem_coe.mp (hfy (Set.mem_range_self j)) |
| 266 | exact ⟨fx i, Set.mem_insert _ _, fy j, Set.mem_insert_of_mem _ rfl, hAdj _ hfxi _ hfyj⟩ }⟩ |
| 267 | |
| 268 | /-- The bipartite no-common-neighbor condition implies distance-2 independence |
| 269 | in `deleteVerts`. -/ |
| 270 | private lemma no_common_neighbor_distIndep {V : Type} [DecidableEq V] |
| 271 | {G : SimpleGraph V} |
| 272 | {A : Finset V} {S : Finset V} |
| 273 | (hAindep : (↑A : Set V).Pairwise fun u v => ¬G.Adj u v) |
| 274 | (_hAS : Disjoint A S) |
| 275 | (hpair : (↑A : Set V).Pairwise fun u v => |
| 276 | ∀ w, w ∉ (↑S : Set V) → ¬(G.Adj u w ∧ G.Adj v w)) : |
| 277 | DistIndependent (deleteVerts G ↑S) 2 ↑A := by |
| 278 | intro u hu v hv huv p |
| 279 | by_contra hle; push_neg at hle |
| 280 | -- p has length ≤ 2 in deleteVerts G S between distinct u, v ∈ A |
| 281 | rcases Nat.lt_or_eq_of_le hle with h | h |
| 282 | · -- length ≤ 1 |
| 283 | rcases Nat.le_one_iff_eq_zero_or_eq_one.mp (by omega : p.length ≤ 1) with h0 | h1 |
| 284 | · exact huv (SimpleGraph.Walk.eq_of_length_eq_zero h0) |
| 285 | · -- length = 1: adjacent in deleteVerts → adjacent in G → contradiction |
| 286 | exact hAindep hu hv huv (SimpleGraph.Walk.adj_of_length_eq_one h1).1 |
| 287 | · -- length = 2: there exists an intermediate vertex w |
| 288 | have h2 : p.length = 2 := by omega |
| 289 | -- Extract the intermediate vertex from the walk |
| 290 | have hw0 : 0 < p.length := by omega |
| 291 | have hw1 : 1 < p.length := by omega |
| 292 | have hadj1 := p.adj_getVert_succ (by omega : 0 < p.length) |
| 293 | have hadj2 := p.adj_getVert_succ (by omega : 1 < p.length) |
| 294 | have hv0 : p.getVert 0 = u := SimpleGraph.Walk.getVert_zero p |
| 295 | have hv2 : p.getVert 2 = v := by rw [← h2]; exact SimpleGraph.Walk.getVert_length p |
| 296 | rw [hv0, show 0 + 1 = 1 from rfl] at hadj1 |
| 297 | rw [show 1 + 1 = 2 from rfl, hv2] at hadj2 |
| 298 | let w := p.getVert 1 |
| 299 | exact hpair hu hv huv w hadj1.2.2 ⟨hadj1.1, hadj2.1.symm⟩ |
| 300 | |
| 301 | /-! ## Main induction -/ |
| 302 | |
| 303 | /-- Core induction: backward from distance `r` down to distance `r - d`. |
| 304 | |
| 305 | At each level, given a set `A` that is distance-`(r-d)` independent in `G - S₀`, |
| 306 | produce a separator `S ⊇ S₀` and a set `B ⊆ A` that is distance-`r` independent |
| 307 | in `G - S`. -/ |
| 308 | private lemma stepLemma (C : GraphClass) |
| 309 | (t : ℕ → ℕ) (ht : ∀ d, HasShallowCliqueBound C d (t d)) |
| 310 | (r : ℕ) : ∀ (d : ℕ), |
| 311 | ∃ (N : ℕ → ℕ) (s : ℕ), |
| 312 | ∀ (m : ℕ) {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V), |
| 313 | C G → ∀ (S₀ A : Finset V), |
| 314 | Disjoint A S₀ → |
| 315 | DistIndependent (deleteVerts G ↑S₀) (r - d) ↑A → N m ≤ A.card → |
| 316 | ∃ (S : Finset V) (B : Finset V), |
| 317 | S₀ ⊆ S ∧ S.card ≤ S₀.card + s ∧ |
| 318 | (↑B : Set V) ⊆ ↑A \ ↑S ∧ m ≤ B.card ∧ |
| 319 | DistIndependent (deleteVerts G ↑S) r ↑B := by |
| 320 | intro d |
| 321 | induction d with |
| 322 | | zero => |
| 323 | -- Base case: r - 0 = r, A is already distance-r independent |
| 324 | refine ⟨id, 0, fun m V _ _ G _ S₀ A hAS hA hcard => ⟨S₀, A, Finset.Subset.refl _, by omega, ?_, hcard, hA⟩⟩ |
| 325 | intro x hx |
| 326 | simp only [Set.mem_diff, Finset.mem_coe] |
| 327 | exact ⟨hx, fun h => absurd h (Finset.disjoint_left.mp hAS hx)⟩ |
| 328 | | succ d ih => |
| 329 | obtain ⟨N_next, s_next, hstep_next⟩ := ih |
| 330 | -- When d+1 > r, r - (d+1) = 0 and r - d = 0; reuse IH |
| 331 | by_cases hdr : d + 1 ≤ r |
| 332 | · -- Meaningful step: reduce from distance i = r-(d+1) to i+1 = r-d |
| 333 | by_cases heven : Even (r - (d + 1)) |
| 334 | · ---- EVEN i = 2j: Odd step via OddStepReduction + Ramsey ---- |
| 335 | obtain ⟨j, hj⟩ := heven |
| 336 | have hj_eq : 2 * j = r - (d + 1) := by omega |
| 337 | have hrd : 2 * j + 1 = r - d := by omega |
| 338 | -- N = Ramsey bound (depends on m, so we use choose after ∀ m) |
| 339 | refine ⟨fun m => (ramsey (t j + 1) (N_next m)).choose, s_next, |
| 340 | fun m V _ _ G hG S₀ A hAS hA hAcard => ?_⟩ |
| 341 | classical |
| 342 | rw [show r - (d + 1) = 2 * j from hj_eq.symm] at hA |
| 343 | -- Apply OddStepReduction to deleteVerts G S₀ |
| 344 | obtain ⟨W, hWdec, hWfin, H, hHG, hHcard, hlift⟩ := |
| 345 | oddStepReduction (deleteVerts G ↑S₀) j A hA |
| 346 | -- Apply Ramsey to H |
| 347 | letI := hWdec; letI := hWfin |
| 348 | haveI : DecidableRel H.Adj := Classical.decRel _ |
| 349 | rcases (ramsey (t j + 1) (N_next m)).choose_spec H |
| 350 | (le_trans hAcard hHcard) with hclique | hindep |
| 351 | · -- Clique ⟹ contradiction with ND |
| 352 | exfalso |
| 353 | have hKG := shallowMinor_compose (clique_gives_minor hclique) |
| 354 | (shallowMinor_of_deleteVerts hHG) |
| 355 | have h_depth : 2 * j * 0 + j + 0 = j := by omega |
| 356 | rw [h_depth] at hKG |
| 357 | exact ht j G hG hKG |
| 358 | · -- Independent set ⟹ lift and apply IH |
| 359 | obtain ⟨B_ind, hB_card, hB_indep⟩ := compl_clique_distIndep hindep |
| 360 | obtain ⟨B', hB'sub, hB'card, hB'indep⟩ := |
| 361 | hlift (N_next m) ⟨B_ind, hB_card, hB_indep⟩ |
| 362 | rw [hrd] at hB'indep |
| 363 | have hAS' : Disjoint B' S₀ := by |
| 364 | rw [Finset.disjoint_left]; intro x hx |
| 365 | exact Finset.disjoint_left.mp hAS (Finset.mem_coe.mp (hB'sub hx)) |
| 366 | obtain ⟨S_f, B_f, hS₀S, hScard, hBsub_f, hBcard_f, hBindep_f⟩ := |
| 367 | hstep_next m G hG S₀ B' hAS' hB'indep hB'card |
| 368 | exact ⟨S_f, B_f, hS₀S, hScard, |
| 369 | fun x hx => by |
| 370 | have := hBsub_f hx |
| 371 | simp only [Set.mem_diff, Finset.mem_coe] at this ⊢ |
| 372 | exact ⟨Finset.mem_coe.mp (hB'sub this.1), this.2⟩, |
| 373 | hBcard_f, hBindep_f⟩ |
| 374 | · ---- ODD i = 2j+1: Even step via EvenStepReduction + IterBipRamsey ---- |
| 375 | obtain ⟨j, hj⟩ : ∃ j, r - (d + 1) = 2 * j + 1 := by |
| 376 | rcases Nat.even_or_odd (r - (d + 1)) with ⟨k, hk⟩ | ⟨k, hk⟩ |
| 377 | · exact absurd ⟨k, hk⟩ heven |
| 378 | · exact ⟨k, hk⟩ |
| 379 | have hj_eq : 2 * j + 1 = r - (d + 1) := by omega |
| 380 | have hrd : 2 * (j + 1) = r - d := by omega |
| 381 | let t_param := t (3 * j + 1) + 1 |
| 382 | refine ⟨fun m => (iterativeBipartiteRamsey (N_next m) t_param).choose, |
| 383 | s_next + (t_param - 1), |
| 384 | fun m V _ _ G hG S₀ A hAS hA hAcard => ?_⟩ |
| 385 | classical |
| 386 | rw [show r - (d + 1) = 2 * j + 1 from hj_eq.symm] at hA |
| 387 | -- Apply EvenStepReduction |
| 388 | obtain ⟨W, hWdec, hWfin, H, AW, hHG, hAWcard, hAWnonadj, hlift⟩ := |
| 389 | evenStepReduction (deleteVerts G ↑S₀) j A hA |
| 390 | letI := hWdec; letI := hWfin |
| 391 | haveI : DecidableRel H.Adj := Classical.decRel _ |
| 392 | -- Build bipartite restriction: keep only edges incident to AW |
| 393 | let B_side : Finset W := Finset.univ \ AW |
| 394 | let H_bip : SimpleGraph W := |
| 395 | { Adj := fun u v => H.Adj u v ∧ (u ∈ AW ∨ v ∈ AW) |
| 396 | symm := fun u v ⟨h1, h2⟩ => ⟨H.symm h1, h2.symm⟩ |
| 397 | loopless := ⟨fun u ⟨h, _⟩ => H.loopless.irrefl u h⟩ } |
| 398 | haveI : DecidableRel H_bip.Adj := Classical.decRel _ |
| 399 | have hBip : ∀ u v, H_bip.Adj u v → |
| 400 | (u ∈ AW ∧ v ∈ B_side) ∨ (u ∈ B_side ∧ v ∈ AW) := by |
| 401 | intro u v ⟨hadj, hor⟩ |
| 402 | have hnotboth : ¬(u ∈ AW ∧ v ∈ AW) := fun ⟨hu, hv⟩ => |
| 403 | hAWnonadj (Finset.mem_coe.mpr hu) (Finset.mem_coe.mpr hv) |
| 404 | (fun h => H.loopless.irrefl u (h ▸ hadj)) hadj |
| 405 | rcases hor with hu | hv |
| 406 | · left; exact ⟨hu, Finset.mem_sdiff.mpr |
| 407 | ⟨Finset.mem_univ _, fun hv => hnotboth ⟨hu, hv⟩⟩⟩ |
| 408 | · right; exact ⟨Finset.mem_sdiff.mpr |
| 409 | ⟨Finset.mem_univ _, fun hu => hnotboth ⟨hu, hv⟩⟩, hv⟩ |
| 410 | have hDisj_bip : Disjoint AW B_side := by |
| 411 | rw [Finset.disjoint_left]; intro x hx hxB |
| 412 | exact (Finset.mem_sdiff.mp hxB).2 hx |
| 413 | -- Apply IterBipRamsey |
| 414 | rcases (iterativeBipartiteRamsey (N_next m) t_param).choose_spec |
| 415 | H_bip AW B_side hDisj_bip hBip (le_trans hAcard hAWcard) with |
| 416 | ⟨A', S_H, hA'sub, hSsub, hA'card, hScard, hA'pair⟩ | |
| 417 | ⟨M, hMrange⟩ | |
| 418 | ⟨X, Y, hXsub, hYsub, hXcard, hYcard, hXYadj⟩ |
| 419 | · -- Outcome (a): no common neighbor → dist-2 → lift → IH |
| 420 | have hA'pair_H : (↑A' : Set W).Pairwise fun u v => |
| 421 | ∀ w, w ∉ (↑S_H : Set W) → ¬(H.Adj u w ∧ H.Adj v w) := by |
| 422 | intro u hu v hv huv w hwS ⟨huw, hvw⟩ |
| 423 | exact hA'pair hu hv huv w hwS |
| 424 | ⟨⟨huw, Or.inl (hA'sub (Finset.mem_coe.mp hu))⟩, |
| 425 | ⟨hvw, Or.inl (hA'sub (Finset.mem_coe.mp hv))⟩⟩ |
| 426 | have hA'indep : (↑A' : Set W).Pairwise fun u v => ¬H.Adj u v := |
| 427 | Set.Pairwise.mono (Finset.coe_subset.mpr hA'sub) hAWnonadj |
| 428 | have hA'S_H : Disjoint A' S_H := by |
| 429 | rw [Finset.disjoint_left]; intro x hx hxS |
| 430 | exact (Finset.mem_sdiff.mp (hSsub hxS)).2 (hA'sub hx) |
| 431 | have hA'dist2 := no_common_neighbor_distIndep hA'indep hA'S_H hA'pair_H |
| 432 | have hSH_AW : Disjoint S_H AW := by |
| 433 | rw [Finset.disjoint_left]; intro x hx |
| 434 | exact (Finset.mem_sdiff.mp (hSsub hx)).2 |
| 435 | obtain ⟨S'_V, B', hS'card, hB'sub, hB'S'disj, hB'card, hB'indep⟩ := |
| 436 | hlift S_H (N_next m) hSH_AW ⟨A', hA'sub, hA'card, hA'dist2⟩ |
| 437 | rw [deleteVerts_deleteVerts, ← Finset.coe_union] at hB'indep |
| 438 | rw [hrd] at hB'indep |
| 439 | have hAS' : Disjoint B' (S₀ ∪ S'_V) := by |
| 440 | rw [Finset.disjoint_union_right] |
| 441 | exact ⟨Finset.disjoint_of_subset_left (fun x hx => Finset.mem_coe.mp (hB'sub hx)) hAS, |
| 442 | hB'S'disj⟩ |
| 443 | obtain ⟨S_f, B_f, hS₀S, hScard_f, hBsub_f, hBcard_f, hBindep_f⟩ := |
| 444 | hstep_next m G hG (S₀ ∪ S'_V) B' hAS' hB'indep hB'card |
| 445 | exact ⟨S_f, B_f, |
| 446 | fun x hx => hS₀S (Finset.subset_union_left hx), |
| 447 | le_trans hScard_f (by |
| 448 | have := Finset.card_union_le S₀ S'_V |
| 449 | have : S'_V.card ≤ t_param - 1 := by |
| 450 | have := hS'card; have := hScard; omega |
| 451 | omega), |
| 452 | fun x hx => by |
| 453 | have := hBsub_f hx |
| 454 | simp only [Set.mem_diff, Finset.mem_coe] at this ⊢ |
| 455 | exact ⟨Finset.mem_coe.mp (hB'sub (Finset.mem_coe.mpr this.1)), this.2⟩, |
| 456 | hBcard_f, hBindep_f⟩ |
| 457 | · -- Outcome (b): topological minor → shallow minor → contradiction with ND |
| 458 | exfalso |
| 459 | have hKH_bip : IsShallowMinor (SimpleGraph.completeGraph (Fin t_param)) H_bip 1 := |
| 460 | shallowTopologicalMinor_toShallowMinor |
| 461 | (show IsShallowTopologicalMinor |
| 462 | (SimpleGraph.completeGraph (Fin t_param)) H_bip 1 from ⟨M⟩) |
| 463 | have hKH : IsShallowMinor (SimpleGraph.completeGraph (Fin t_param)) H 1 := |
| 464 | shallowMinor_of_subgraph (fun {u v} h => by |
| 465 | exact h.1) hKH_bip |
| 466 | have hHG' := shallowMinor_of_deleteVerts hHG |
| 467 | have hKG := shallowMinor_compose hKH hHG' |
| 468 | have h_depth : 2 * j * 1 + j + 1 = 3 * j + 1 := by omega |
| 469 | rw [h_depth] at hKG |
| 470 | exact ht (3 * j + 1) G hG hKG |
| 471 | · -- Outcome (c): K_{t,t} → K_t ⪯_1 H → contradiction with ND |
| 472 | exfalso |
| 473 | have hKH : IsShallowMinor (SimpleGraph.completeGraph (Fin t_param)) H 1 := |
| 474 | ktt_gives_minor |
| 475 | (Finset.disjoint_of_subset_left hXsub |
| 476 | (Finset.disjoint_of_subset_right hYsub hDisj_bip)) |
| 477 | hXcard hYcard |
| 478 | (fun x hx y hy => (hXYadj x hx y hy).1) |
| 479 | have hHG' := shallowMinor_of_deleteVerts hHG |
| 480 | have hKG := shallowMinor_compose hKH hHG' |
| 481 | have h_depth : 2 * j * 1 + j + 1 = 3 * j + 1 := by omega |
| 482 | rw [h_depth] at hKG |
| 483 | exact ht (3 * j + 1) G hG hKG |
| 484 | · -- d + 1 > r: trivially reuse IH since r-(d+1) = 0 = r-d |
| 485 | push_neg at hdr |
| 486 | exact ⟨N_next, s_next, fun m V _ _ G hG S₀ A hAS hA hcard => by |
| 487 | have h1 : r - (d + 1) = 0 := Nat.sub_eq_zero_of_le (by omega) |
| 488 | have h2 : r - d = 0 := Nat.sub_eq_zero_of_le (by omega) |
| 489 | rw [h1] at hA; rw [h2] at hstep_next |
| 490 | exact hstep_next m G hG S₀ A hAS hA hcard⟩ |
| 491 | |
| 492 | /-- Lemma 3.4: if a class `C` is nowhere dense, then `C` is uniformly |
| 493 | quasi-wide. -/ |
| 494 | theorem nd_implies_uqw (C : GraphClass) : |
| 495 | IsNowhereDense C → UniformlyQuasiWide C := by |
| 496 | intro hND r |
| 497 | -- Extract clique bounds from ND |
| 498 | choose t ht using hND |
| 499 | -- Apply step lemma with d = r (going from distance 0 to distance r) |
| 500 | obtain ⟨N, s, hstep⟩ := stepLemma C t ht r r |
| 501 | refine ⟨N, s, fun m V _ _ G hG A hAcard => ?_⟩ |
| 502 | -- Every set is distance-0 independent |
| 503 | have hA_indep : DistIndependent (deleteVerts G (↑(∅ : Finset V))) (r - r) ↑A := by |
| 504 | rw [Nat.sub_self, finset_coe_empty] |
| 505 | exact distIndependent_deleteVerts_empty (distIndependent_zero G ↑A) |
| 506 | obtain ⟨S, B, _, hScard, hBsub, hBcard, hBindep⟩ := |
| 507 | hstep m G hG ∅ A (Finset.disjoint_empty_right A) hA_indep hAcard |
| 508 | refine ⟨S, B, by simpa using hScard, ?_, hBcard, hBindep⟩ |
| 509 | intro x hx |
| 510 | have := hBsub (Finset.mem_coe.mpr hx) |
| 511 | simp only [Set.mem_diff, Finset.mem_coe] at this |
| 512 | exact Finset.mem_sdiff.mpr this |
| 513 | |
| 514 | end Catalog.Sparsity.NDImpliesUQW |
| 515 |