Catalog/Sparsity/AdmBoundByTopGrad/Full.lean
| 1 | import Catalog.Sparsity.ColoringNumbers.Full |
| 2 | import Catalog.Sparsity.Admissibility.Full |
| 3 | import Catalog.Sparsity.ShallowTopologicalMinor.Full |
| 4 | import Mathlib.Combinatorics.SimpleGraph.Finite |
| 5 | import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan |
| 6 | import Mathlib.Combinatorics.SimpleGraph.Operations |
| 7 | import Mathlib.Data.Nat.Find |
| 8 | import Mathlib.Tactic.Ring |
| 9 | import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph |
| 10 | |
| 11 | open Catalog.Sparsity.ColoringNumbers |
| 12 | open Catalog.Sparsity.ShallowTopologicalMinor |
| 13 | open Catalog.Sparsity.Admissibility |
| 14 | open Classical |
| 15 | |
| 16 | namespace Catalog.Sparsity.AdmBoundByTopGrad |
| 17 | |
| 18 | noncomputable section |
| 19 | |
| 20 | /-! ## Subset admissibility |
| 21 | |
| 22 | A family of paths from `v` into a subset `S`, with internal vertices outside |
| 23 | `S`, pairwise vertex-disjoint except at `v`. This is the source proof's local |
| 24 | quantity `b_r(S, v)`. -/ |
| 25 | |
| 26 | private structure IsSubsetAdmFamily {V : Type} [DecidableEq V] [Fintype V] |
| 27 | (G : SimpleGraph V) (r : ℕ) (S : Set V) (v : V) |
| 28 | {ι : Type} (paths : ι → (u : V) × G.Walk v u) : Prop where |
| 29 | target_mem : ∀ i, (paths i).1 ∈ S |
| 30 | target_ne : ∀ i, (paths i).1 ≠ v |
| 31 | isPath : ∀ i, (paths i).2.IsPath |
| 32 | length_le : ∀ i, (paths i).2.length ≤ r |
| 33 | internal_avoids : |
| 34 | ∀ i, ∀ j : ℕ, 0 < j → j < (paths i).2.length → (paths i).2.getVert j ∉ S |
| 35 | disjoint : ∀ i j, i ≠ j → |
| 36 | ∀ w, w ∈ (paths i).2.support → w ∈ (paths j).2.support → w = v |
| 37 | |
| 38 | private noncomputable def subsetAdmValue {V : Type} [DecidableEq V] [Fintype V] |
| 39 | (G : SimpleGraph V) (r : ℕ) (S : Set V) (v : V) : ℕ := |
| 40 | Finset.sup (Finset.range (Fintype.card V)) (fun k => |
| 41 | if ∃ (paths : Fin k → (u : V) × G.Walk v u), IsSubsetAdmFamily G r S v paths |
| 42 | then k else 0) |
| 43 | |
| 44 | /-! ## List-based linear order construction -/ |
| 45 | |
| 46 | private theorem idxOf_injective_of_nodup_of_mem_all {V : Type} [DecidableEq V] {l : List V} |
| 47 | (hNodup : l.Nodup) (hall : ∀ v : V, v ∈ l) : |
| 48 | Function.Injective fun v => l.idxOf v := by |
| 49 | let e := hNodup.getEquivOfForallMemList l hall |
| 50 | intro a b hab |
| 51 | apply e.symm.injective |
| 52 | apply Fin.ext |
| 53 | simpa [e, List.Nodup.getEquivOfForallMemList] using hab |
| 54 | |
| 55 | private abbrev listIndexOrder {V : Type} [DecidableEq V] {l : List V} |
| 56 | (hNodup : l.Nodup) (hall : ∀ v : V, v ∈ l) : LinearOrder V := |
| 57 | LinearOrder.lift' (fun v => l.idxOf v) (idxOf_injective_of_nodup_of_mem_all hNodup hall) |
| 58 | |
| 59 | /-! ## Trimming: admVertex ≤ 1 + subsetAdmValue |
| 60 | |
| 61 | Key lemma: given a split of `V` into `(list for S \ {x}) ++ [x] ++ (rest)`, the |
| 62 | admissibility of `x` under the list-index order is at most |
| 63 | `1 + subsetAdmValue G r S x`. |
| 64 | |
| 65 | Proof idea: any admissible family at `x` (paths to vertices below `x`) can be |
| 66 | trimmed to a subset-admissible family by stopping each path at the first vertex |
| 67 | in `S \ {x}`. -/ |
| 68 | |
| 69 | private theorem admVertex_le_one_add_subsetAdmValue_of_splitOrder |
| 70 | {V : Type} [DecidableEq V] [Fintype V] |
| 71 | (G : SimpleGraph V) (r : ℕ) (s : Finset V) (x : V) (l m : List V) |
| 72 | (hl : ∀ v, v ∈ l ↔ v ∈ s.erase x) |
| 73 | (hLnodup : (l ++ x :: m).Nodup) |
| 74 | (hall : ∀ v : V, v ∈ l ++ x :: m) : |
| 75 | let _ : LinearOrder V := listIndexOrder hLnodup hall |
| 76 | let _ : LinearOrder V := listIndexOrder hLnodup hall |
| 77 | admVertex G r x ≤ 1 + subsetAdmValue G r (s : Set V) x := by |
| 78 | letI : LinearOrder V := listIndexOrder hLnodup hall |
| 79 | change admVertex G r x ≤ 1 + subsetAdmValue G r (↑s) x |
| 80 | unfold admVertex subsetAdmValue |
| 81 | -- It suffices to show: sup of adm-family sizes ≤ sup of subset-adm-family sizes |
| 82 | suffices hAB : |
| 83 | (Finset.range (Fintype.card V)).sup |
| 84 | (fun k => |
| 85 | if ∃ paths : Fin k → (u : V) × G.Walk x u, IsAdmFamily G r x paths then k else 0) ≤ |
| 86 | (Finset.range (Fintype.card V)).sup |
| 87 | (fun k => |
| 88 | if ∃ paths : Fin k → (u : V) × G.Walk x u, |
| 89 | IsSubsetAdmFamily G r (↑s) x paths then k else 0) by |
| 90 | simpa [Nat.add_comm] using Nat.succ_le_succ hAB |
| 91 | apply Finset.sup_le |
| 92 | intro k hk |
| 93 | split_ifs with hkAdm |
| 94 | · rcases hkAdm with ⟨paths, hpaths⟩ |
| 95 | have hx_not_mem_l : x ∉ l := by |
| 96 | intro hx_in |
| 97 | have : x ∈ s.erase x := (hl x).1 hx_in |
| 98 | simp at this |
| 99 | -- Vertices below x in the ordering are exactly l = s.erase x |
| 100 | have htarget : ∀ i, (paths i).1 ∈ s.erase x := by |
| 101 | intro i |
| 102 | have hidx : (l ++ x :: m).idxOf (paths i).1 < (l ++ x :: m).idxOf x := by |
| 103 | change (paths i).1 < x |
| 104 | simpa [listIndexOrder] using hpaths.target_lt i |
| 105 | have hidxx : (l ++ x :: m).idxOf x = l.length := by |
| 106 | rw [List.idxOf_append_of_notMem hx_not_mem_l] |
| 107 | simp |
| 108 | have hmeml : (paths i).1 ∈ l := by |
| 109 | have hp : l <+: l ++ x :: m := l.prefix_append (x :: m) |
| 110 | exact (hp.mem_iff_idxOf_lt_length (paths i).1).2 (hidxx ▸ hidx) |
| 111 | exact (hl _).1 hmeml |
| 112 | -- For each path, find the first vertex in s \ {x} and trim there |
| 113 | have hConvert : ∀ i : Fin k, |
| 114 | ∃ (y : V) (q : G.Walk x y), |
| 115 | y ∈ (s : Set V) ∧ y ≠ x ∧ q.IsPath ∧ q.length ≤ r ∧ |
| 116 | (∀ idx, 0 < idx → idx < q.length → q.getVert idx ∉ (s : Set V)) ∧ |
| 117 | (∀ w, w ∈ q.support → w ∈ (paths i).2.support) := by |
| 118 | intro i |
| 119 | let p := (paths i).2 |
| 120 | -- The walk goes from x to (paths i).1 ∈ s.erase x |
| 121 | -- Find smallest j > 0 with p.getVert j ∈ s.erase x |
| 122 | have hlen_pos : 0 < p.length := by |
| 123 | rcases Nat.eq_zero_or_pos p.length with h0 | hpos |
| 124 | · exfalso |
| 125 | have : (paths i).1 = x := by |
| 126 | have := p.getVert_length |
| 127 | rw [h0, SimpleGraph.Walk.getVert_zero] at this |
| 128 | exact this.symm |
| 129 | exact (Finset.mem_erase.mp (htarget i)).1 this |
| 130 | · exact hpos |
| 131 | have hEndMem : p.getVert p.length ∈ s.erase x := by |
| 132 | rw [p.getVert_length]; exact htarget i |
| 133 | -- Predicate: j > 0 ∧ j ≤ p.length ∧ p.getVert j ∈ s.erase x |
| 134 | let P := fun j => 0 < j ∧ j ≤ p.length ∧ p.getVert j ∈ s.erase x |
| 135 | have hPex : ∃ j, P j := ⟨p.length, hlen_pos, le_refl _, hEndMem⟩ |
| 136 | let j := Nat.find hPex |
| 137 | have hj : P j := Nat.find_spec hPex |
| 138 | have hjmin : ∀ j' < j, ¬P j' := fun j' hlt => Nat.find_min hPex hlt |
| 139 | -- The trimmed walk is p.take j |
| 140 | refine ⟨p.getVert j, p.take j, ?_, ?_, ?_, ?_, ?_, ?_⟩ |
| 141 | · exact (Finset.mem_erase.mp hj.2.2).2 |
| 142 | · exact (Finset.mem_erase.mp hj.2.2).1 |
| 143 | · exact (hpaths.isPath i).take j |
| 144 | · calc (p.take j).length = min j p.length := p.take_length j |
| 145 | _ ≤ p.length := min_le_right _ _ |
| 146 | _ ≤ r := hpaths.length_le i |
| 147 | · -- Internal vertices avoid s |
| 148 | intro idx hidx0 hidxlen |
| 149 | have hidxj : idx < j := by |
| 150 | rw [p.take_length] at hidxlen |
| 151 | exact lt_of_lt_of_le hidxlen (min_le_left _ _) |
| 152 | have hgetVert : (p.take j).getVert idx = p.getVert idx := by |
| 153 | rw [p.take_getVert] |
| 154 | congr 1 |
| 155 | exact min_eq_right (le_of_lt hidxj) |
| 156 | rw [hgetVert] |
| 157 | intro hmem |
| 158 | have hidxle : idx ≤ p.length := le_trans (le_of_lt hidxj) hj.2.1 |
| 159 | -- p.getVert idx ∈ s and idx > 0, so p.getVert idx ∈ s.erase x |
| 160 | -- (since path is injective, getVert idx ≠ getVert 0 = x) |
| 161 | have hne_x : p.getVert idx ≠ x := by |
| 162 | intro heq |
| 163 | have := (hpaths.isPath i).getVert_injOn |
| 164 | (show idx ∈ {i | i ≤ p.length} from hidxle) |
| 165 | (show 0 ∈ {i | i ≤ p.length} from Nat.zero_le _) |
| 166 | (heq.trans p.getVert_zero.symm) |
| 167 | omega |
| 168 | exact hjmin idx hidxj ⟨hidx0, hidxle, Finset.mem_erase.mpr ⟨hne_x, hmem⟩⟩ |
| 169 | · -- Support subset |
| 170 | intro w hw |
| 171 | have hsub := p.take_support_eq_support_take_succ j |
| 172 | rw [hsub] at hw |
| 173 | exact List.take_subset _ _ hw |
| 174 | -- Build the converted family |
| 175 | choose y q hy hne hpath hlen hint hsub using hConvert |
| 176 | have hsubset : ∃ newPaths : Fin k → (u : V) × G.Walk x u, |
| 177 | IsSubsetAdmFamily G r (↑s) x newPaths := by |
| 178 | refine ⟨fun i => ⟨y i, q i⟩, ?_, ?_, ?_, ?_, ?_, ?_⟩ |
| 179 | · intro i; exact hy i |
| 180 | · intro i; exact hne i |
| 181 | · intro i; exact hpath i |
| 182 | · intro i; exact hlen i |
| 183 | · intro i; exact hint i |
| 184 | · intro i₁ i₂ hi w hw1 hw2 |
| 185 | exact hpaths.disjoint i₁ i₂ hi w (hsub i₁ w hw1) (hsub i₂ w hw2) |
| 186 | have hkval : |
| 187 | (if ∃ paths : Fin k → (u : V) × G.Walk x u, |
| 188 | IsSubsetAdmFamily G r (↑s) x paths then k else 0) = k := by |
| 189 | simp [hsubset] |
| 190 | calc |
| 191 | k = (if ∃ paths : Fin k → (u : V) × G.Walk x u, |
| 192 | IsSubsetAdmFamily G r (↑s) x paths then k else 0) := hkval.symm |
| 193 | _ ≤ (Finset.range (Fintype.card V)).sup |
| 194 | (fun k => |
| 195 | if ∃ paths : Fin k → (u : V) × G.Walk x u, |
| 196 | IsSubsetAdmFamily G r (↑s) x paths then k else 0) := |
| 197 | Finset.le_sup (f := fun k => |
| 198 | if ∃ paths : Fin k → (u : V) × G.Walk x u, |
| 199 | IsSubsetAdmFamily G r (↑s) x paths then k else 0) hk |
| 200 | · simp |
| 201 | |
| 202 | /-! ## Greedy peeling (Phase A) |
| 203 | |
| 204 | Build a `LinearOrder V` with bounded admissibility by repeatedly peeling the |
| 205 | vertex with minimum `subsetAdmValue` from the remaining set. -/ |
| 206 | |
| 207 | private structure PrefixData {V : Type} [DecidableEq V] [Fintype V] |
| 208 | (G : SimpleGraph V) (r : ℕ) (B : ℕ) (s : Finset V) |
| 209 | (m : List V) (hmNodup : m.Nodup) (hmMem : ∀ v : V, v ∈ m ↔ v ∉ s) where |
| 210 | list : List V |
| 211 | nodup : list.Nodup |
| 212 | mem_iff : ∀ v, v ∈ list ↔ v ∈ s |
| 213 | bound : |
| 214 | ∀ (hLnodup : (list ++ m).Nodup) (hall : ∀ v : V, v ∈ list ++ m), |
| 215 | let _ : LinearOrder V := listIndexOrder hLnodup hall |
| 216 | ∀ v ∈ s, admVertex G r v ≤ 1 + B |
| 217 | |
| 218 | private noncomputable def choosePeelVertex {V : Type} [DecidableEq V] [Fintype V] |
| 219 | (G : SimpleGraph V) (r : ℕ) {B : ℕ} |
| 220 | (hBound : |
| 221 | ∀ S : Set V, S.Nonempty → |
| 222 | ∃ v ∈ S, subsetAdmValue G r S v ≤ B) |
| 223 | (s : Finset V) (hs : s.Nonempty) : |
| 224 | {x // x ∈ s ∧ subsetAdmValue G r (s : Set V) x ≤ B} := by |
| 225 | let hx := hBound (s : Set V) ⟨hs.choose, by simpa using hs.choose_spec⟩ |
| 226 | let x : V := Classical.choose hx |
| 227 | have hx_mem : x ∈ (s : Set V) := (Classical.choose_spec hx).1 |
| 228 | have hxB : subsetAdmValue G r (s : Set V) x ≤ B := (Classical.choose_spec hx).2 |
| 229 | exact ⟨x, by simpa using hx_mem, hxB⟩ |
| 230 | |
| 231 | private theorem listIndexOrder_eq_of_eqList {V : Type} [DecidableEq V] {l l' : List V} |
| 232 | (h : l = l') (hNodup : l.Nodup) (hall : ∀ v : V, v ∈ l) |
| 233 | (hNodup' : l'.Nodup) (hall' : ∀ v : V, v ∈ l') : |
| 234 | @listIndexOrder V _ l hNodup hall = @listIndexOrder V _ l' hNodup' hall' := by |
| 235 | subst h |
| 236 | cases Subsingleton.elim hNodup hNodup' |
| 237 | cases Subsingleton.elim hall hall' |
| 238 | rfl |
| 239 | |
| 240 | private noncomputable def buildPrefixData {V : Type} [DecidableEq V] [Fintype V] |
| 241 | (G : SimpleGraph V) (r : ℕ) {B : ℕ} |
| 242 | (hBound : |
| 243 | ∀ S : Set V, S.Nonempty → |
| 244 | ∃ v ∈ S, subsetAdmValue G r S v ≤ B) |
| 245 | (s : Finset V) (m : List V) (hmNodup : m.Nodup) (hmMem : ∀ v : V, v ∈ m ↔ v ∉ s) : |
| 246 | PrefixData G r B s m hmNodup hmMem := by |
| 247 | by_cases hs : s.Nonempty |
| 248 | · let choice := choosePeelVertex G r hBound s hs |
| 249 | let x := choice.1 |
| 250 | have hx : x ∈ s := choice.2.1 |
| 251 | have hxB : subsetAdmValue G r (s : Set V) x ≤ B := choice.2.2 |
| 252 | have hxm : x ∉ m := by |
| 253 | intro hxm |
| 254 | exact ((hmMem x).1 hxm) hx |
| 255 | have hmConsNodup : (x :: m).Nodup := by |
| 256 | simp [hxm, hmNodup] |
| 257 | have hmConsMem : ∀ v : V, v ∈ x :: m ↔ v ∉ s.erase x := by |
| 258 | intro v |
| 259 | by_cases hvx : v = x |
| 260 | · subst hvx |
| 261 | simp [hx] |
| 262 | · simp [hmMem v, Finset.mem_erase, hvx] |
| 263 | let prev := |
| 264 | buildPrefixData G r hBound (s.erase x) (x :: m) hmConsNodup hmConsMem |
| 265 | refine |
| 266 | { list := prev.list ++ [x] |
| 267 | nodup := by |
| 268 | have hx_not_mem_prev : x ∉ prev.list := by |
| 269 | intro hxList |
| 270 | have : x ∈ s.erase x := (prev.mem_iff x).1 hxList |
| 271 | simp at this |
| 272 | refine List.nodup_append.2 ⟨prev.nodup, by simp, ?_⟩ |
| 273 | intro a ha b hb |
| 274 | simp at hb |
| 275 | subst b |
| 276 | exact fun hax => hx_not_mem_prev (hax ▸ ha) |
| 277 | mem_iff := by |
| 278 | intro v |
| 279 | by_cases hvx : v = x |
| 280 | · subst hvx |
| 281 | simp [hx] |
| 282 | · simp [prev.mem_iff, Finset.mem_erase, hvx] |
| 283 | bound := by |
| 284 | intro hLnodup hall |
| 285 | have hsplitNodup : (prev.list ++ x :: m).Nodup := by |
| 286 | simpa [List.append_assoc] using hLnodup |
| 287 | have hsplitAll : ∀ w : V, w ∈ prev.list ++ x :: m := by |
| 288 | simpa [List.append_assoc] using hall |
| 289 | have hboundSplit : |
| 290 | let _ : LinearOrder V := listIndexOrder hsplitNodup hsplitAll |
| 291 | ∀ v ∈ s, admVertex G r v ≤ 1 + B := by |
| 292 | letI : LinearOrder V := listIndexOrder hsplitNodup hsplitAll |
| 293 | change ∀ v ∈ s, admVertex G r v ≤ 1 + B |
| 294 | intro v hv |
| 295 | by_cases hvx : v = x |
| 296 | · subst hvx |
| 297 | exact admVertex_le_one_add_subsetAdmValue_of_splitOrder |
| 298 | G r s x prev.list m prev.mem_iff hsplitNodup hsplitAll |
| 299 | |>.trans (Nat.add_le_add_left hxB 1) |
| 300 | · have hvt : v ∈ s.erase x := by |
| 301 | simpa [Finset.mem_erase, hvx] using hv |
| 302 | exact prev.bound hsplitNodup hsplitAll v hvt |
| 303 | have hOrderEq : |
| 304 | listIndexOrder hsplitNodup hsplitAll = listIndexOrder hLnodup hall := by |
| 305 | apply listIndexOrder_eq_of_eqList (h := by simp [List.append_assoc]) |
| 306 | rw [← hOrderEq] |
| 307 | exact hboundSplit } |
| 308 | · refine |
| 309 | { list := [] |
| 310 | nodup := by simp |
| 311 | mem_iff := by |
| 312 | intro v |
| 313 | simp [Finset.not_nonempty_iff_eq_empty.mp hs] |
| 314 | bound := by |
| 315 | intro hLnodup hall |
| 316 | letI : LinearOrder V := listIndexOrder hLnodup hall |
| 317 | change ∀ v ∈ s, admVertex G r v ≤ 1 + B |
| 318 | intro v hv |
| 319 | simp [Finset.not_nonempty_iff_eq_empty.mp hs] at hv } |
| 320 | termination_by s.card |
| 321 | decreasing_by |
| 322 | simpa using |
| 323 | Finset.card_erase_lt_of_mem ((choosePeelVertex G r hBound s hs).2.1) |
| 324 | |
| 325 | private theorem exists_order_adm_le_of_subsetAdmBound |
| 326 | {V : Type} [DecidableEq V] [Fintype V] |
| 327 | (G : SimpleGraph V) (r : ℕ) {B : ℕ} |
| 328 | (hBound : |
| 329 | ∀ S : Set V, S.Nonempty → |
| 330 | ∃ v ∈ S, subsetAdmValue G r S v ≤ B) : |
| 331 | ∃ ord : LinearOrder V, |
| 332 | letI := ord; adm G r ≤ 1 + B := by |
| 333 | let data := buildPrefixData G r hBound Finset.univ [] (by simp) (by intro v; simp) |
| 334 | let hLnodup : (data.list ++ []).Nodup := by |
| 335 | simpa using data.nodup |
| 336 | let hall : ∀ v : V, v ∈ data.list ++ [] := by |
| 337 | intro v |
| 338 | simpa using (data.mem_iff v).2 (by simp) |
| 339 | refine ⟨listIndexOrder hLnodup hall, ?_⟩ |
| 340 | letI : LinearOrder V := listIndexOrder hLnodup hall |
| 341 | change adm G r ≤ 1 + B |
| 342 | rw [adm] |
| 343 | have hboundAll : ∀ v ∈ (Finset.univ : Finset V), admVertex G r v ≤ 1 + B := by |
| 344 | simpa using data.bound hLnodup hall |
| 345 | by_cases huniv : (Finset.univ : Finset V).Nonempty |
| 346 | · obtain ⟨v, hv, hsup⟩ := Finset.exists_mem_eq_sup Finset.univ huniv (fun w => admVertex G r w) |
| 347 | simpa [hsup] using hboundAll v hv |
| 348 | · simp [Finset.not_nonempty_iff_eq_empty.mp huniv] |
| 349 | |
| 350 | /-! ## Phase B: every nonempty subset has a vertex with bounded subsetAdmValue |
| 351 | |
| 352 | If all depth-`(r-1)` topological minors have edge density at most `d`, then for |
| 353 | every nonempty `S ⊆ V`, there exists `v ∈ S` with |
| 354 | `subsetAdmValue G r S v ≤ 6 * r * d ^ 3`. |
| 355 | |
| 356 | Proof (from source): if all `b_r(S, v) > ℓ = 6rd³`, build a maximal matching |
| 357 | of paths between pairs of `S`, extract an independent set from the resulting |
| 358 | graph, trim path families, assemble a topological minor that is too dense, |
| 359 | contradicting the density hypothesis. -/ |
| 360 | |
| 361 | /-! ### Helper: subsetAdmValue = 0 when r = 0 -/ |
| 362 | |
| 363 | private theorem subsetAdmValue_eq_zero_of_r_eq_zero |
| 364 | {V : Type} [DecidableEq V] [Fintype V] |
| 365 | (G : SimpleGraph V) (S : Set V) (v : V) : |
| 366 | subsetAdmValue G 0 S v = 0 := by |
| 367 | unfold subsetAdmValue |
| 368 | apply le_antisymm _ (Nat.zero_le _) |
| 369 | apply Finset.sup_le |
| 370 | intro k _ |
| 371 | split_ifs with h |
| 372 | · rcases Nat.eq_zero_or_pos k with rfl | hk |
| 373 | · exact le_refl _ |
| 374 | · exfalso |
| 375 | obtain ⟨paths, hpaths⟩ := h |
| 376 | let i : Fin k := ⟨0, hk⟩ |
| 377 | have hlen : (paths i).2.length = 0 := Nat.le_zero.mp (hpaths.length_le i) |
| 378 | have heq : (paths i).1 = v := by |
| 379 | have h1 := (paths i).2.getVert_length |
| 380 | rw [hlen, SimpleGraph.Walk.getVert_zero] at h1 |
| 381 | exact h1.symm |
| 382 | exact hpaths.target_ne i heq |
| 383 | · exact le_refl _ |
| 384 | |
| 385 | /-! ### Helper: independent set from edge bound |
| 386 | |
| 387 | A graph with at most d·|V| edges has an independent set I with |
| 388 | |V| ≤ |I|·(2d+1). Standard degeneracy/coloring argument. -/ |
| 389 | |
| 390 | private theorem exists_indepset_of_edge_bound |
| 391 | {W : Type} [DecidableEq W] [Fintype W] |
| 392 | (H : SimpleGraph W) [DecidableRel H.Adj] (d : ℕ) |
| 393 | (hEdge : H.edgeFinset.card ≤ d * Fintype.card W) : |
| 394 | ∃ I : Finset W, (∀ u ∈ I, ∀ v ∈ I, u ≠ v → ¬H.Adj u v) ∧ |
| 395 | Fintype.card W ≤ I.card * (2 * d + 1) := by |
| 396 | set n := Fintype.card W with hn_def |
| 397 | by_cases hn : n = 0 |
| 398 | · -- W is empty |
| 399 | haveI : IsEmpty W := Fintype.card_eq_zero_iff.mp hn |
| 400 | exact ⟨∅, fun u hu => absurd hu (by simp), by simp [hn]⟩ |
| 401 | · -- W is nonempty |
| 402 | have hn_pos : 0 < n := Nat.pos_of_ne_zero hn |
| 403 | haveI : Nonempty W := Fintype.card_pos_iff.mp hn_pos |
| 404 | set α := H.indepNum |
| 405 | -- α ≥ 1 (any singleton is independent) |
| 406 | have hα_pos : 1 ≤ α := by |
| 407 | have v : W := Classical.choice inferInstance |
| 408 | have : H.IsIndepSet (↑({v} : Finset W)) := by |
| 409 | rw [SimpleGraph.isIndepSet_iff] |
| 410 | intro a ha b hb hab |
| 411 | simp at ha hb; exact absurd (hb ▸ ha) hab |
| 412 | simpa using this.card_le_indepNum |
| 413 | -- Hᶜ is CliqueFree (α + 1) |
| 414 | have hCF : Hᶜ.CliqueFree (α + 1) := by |
| 415 | intro s hs |
| 416 | have hIndep : H.IsIndepSet ↑s := (SimpleGraph.isClique_compl H).mp hs.isClique |
| 417 | have h1 : s.card ≤ α := hIndep.card_le_indepNum |
| 418 | have h2 : s.card = α + 1 := hs.card_eq |
| 419 | omega |
| 420 | -- Turán bound on complement: 2α·|E(Hᶜ)| ≤ (α-1)·n² |
| 421 | have hTuran : 2 * α * Hᶜ.edgeFinset.card ≤ (α - 1) * n ^ 2 := by |
| 422 | calc 2 * α * Hᶜ.edgeFinset.card |
| 423 | ≤ 2 * α * (SimpleGraph.turanGraph n α).edgeFinset.card := by |
| 424 | apply Nat.mul_le_mul_left |
| 425 | rw [SimpleGraph.card_edgeFinset_turanGraph] |
| 426 | exact hCF.card_edgeFinset_le |
| 427 | _ ≤ (α - 1) * n ^ 2 := |
| 428 | SimpleGraph.mul_card_edgeFinset_turanGraph_le |
| 429 | -- Edge partition: |E(H)| + |E(Hᶜ)| = C(n,2) |
| 430 | have hSub : H.edgeFinset ⊆ (⊤ : SimpleGraph W).edgeFinset := |
| 431 | SimpleGraph.edgeFinset_mono le_top |
| 432 | have hCompl : Hᶜ.edgeFinset = (⊤ : SimpleGraph W).edgeFinset \ H.edgeFinset := by |
| 433 | ext e; refine Sym2.ind ?_ e; intro u v |
| 434 | simp only [Finset.mem_sdiff, SimpleGraph.mem_edgeFinset, |
| 435 | SimpleGraph.mem_edgeSet, SimpleGraph.compl_adj, SimpleGraph.top_adj] |
| 436 | have hPartition : H.edgeFinset.card + Hᶜ.edgeFinset.card = n.choose 2 := by |
| 437 | have h1 := Finset.card_sdiff_add_card_eq_card hSub |
| 438 | rw [← hCompl] at h1 |
| 439 | rw [SimpleGraph.card_edgeFinset_top_eq_card_choose_two, ← hn_def] at h1 |
| 440 | omega |
| 441 | -- Double partition: n + 2|E(H)| + 2|E(Hᶜ)| = n² |
| 442 | have hDouble : n + 2 * H.edgeFinset.card + 2 * Hᶜ.edgeFinset.card = n ^ 2 := by |
| 443 | rw [Nat.add_assoc, |
| 444 | show 2 * H.edgeFinset.card + 2 * Hᶜ.edgeFinset.card = |
| 445 | 2 * (H.edgeFinset.card + Hᶜ.edgeFinset.card) from by ring, |
| 446 | hPartition, Nat.choose_two_right, |
| 447 | Nat.mul_div_cancel' (Nat.even_mul_pred_self n).two_dvd] |
| 448 | rcases n with _ | m; · exact absurd rfl hn |
| 449 | simp; ring |
| 450 | -- Key: n² ≤ α·n·(2d+1) |
| 451 | -- Step 1: (α-1)·n² + n² = α·n² |
| 452 | have hαn : (α - 1) * n ^ 2 + n ^ 2 = α * n ^ 2 := by |
| 453 | rcases α with _ | a; · omega |
| 454 | simp; ring |
| 455 | -- Step 2: n² + 2α|E(Hᶜ)| ≤ α·n² (from Turán) |
| 456 | have h1 : n ^ 2 + 2 * α * Hᶜ.edgeFinset.card ≤ α * n ^ 2 := |
| 457 | calc n ^ 2 + 2 * α * Hᶜ.edgeFinset.card |
| 458 | ≤ n ^ 2 + (α - 1) * n ^ 2 := Nat.add_le_add_left hTuran _ |
| 459 | _ = (α - 1) * n ^ 2 + n ^ 2 := Nat.add_comm .. |
| 460 | _ = α * n ^ 2 := hαn |
| 461 | -- Step 3: α·n² = α·n + 2α|E(H)| + 2α|E(Hᶜ)| (from hDouble × α) |
| 462 | have hαDouble : α * n + 2 * α * H.edgeFinset.card + |
| 463 | 2 * α * Hᶜ.edgeFinset.card = α * n ^ 2 := by |
| 464 | calc α * n + 2 * α * H.edgeFinset.card + 2 * α * Hᶜ.edgeFinset.card |
| 465 | = α * (n + 2 * H.edgeFinset.card + 2 * Hᶜ.edgeFinset.card) := by ring |
| 466 | _ = α * n ^ 2 := by rw [hDouble] |
| 467 | -- Step 4: n² ≤ α·n + 2α|E(H)| |
| 468 | have h3 : n ^ 2 ≤ α * n + 2 * α * H.edgeFinset.card := |
| 469 | Nat.le_of_add_le_add_right (hαDouble ▸ h1) |
| 470 | -- Step 5: n² ≤ α·n·(2d+1) |
| 471 | have hKey : n * n ≤ α * n * (2 * d + 1) := by |
| 472 | calc n * n = n ^ 2 := by ring |
| 473 | _ ≤ α * n + 2 * α * H.edgeFinset.card := h3 |
| 474 | _ ≤ α * n + 2 * α * (d * n) := |
| 475 | Nat.add_le_add_left (Nat.mul_le_mul_left _ hEdge) _ |
| 476 | _ = α * n * (2 * d + 1) := by ring |
| 477 | have hKey' : n * n ≤ α * (2 * d + 1) * n := by |
| 478 | calc n * n ≤ α * n * (2 * d + 1) := hKey |
| 479 | _ = α * (2 * d + 1) * n := by ring |
| 480 | have hFinal : n ≤ α * (2 * d + 1) := Nat.le_of_mul_le_mul_right hKey' hn_pos |
| 481 | -- Extract the concrete independent set |
| 482 | obtain ⟨I, hI⟩ := SimpleGraph.exists_isNIndepSet_indepNum (G := H) |
| 483 | refine ⟨I, ?_, ?_⟩ |
| 484 | · intro u hu v hv huv |
| 485 | exact (SimpleGraph.isIndepSet_iff H).mp hI.isIndepSet hu hv huv |
| 486 | · rw [hI.card_eq]; exact hFinal |
| 487 | |
| 488 | /-! ### Raw connector infrastructure |
| 489 | |
| 490 | A `RawConnector` is a graph H on S together with a topological minor model |
| 491 | witnessing H ≼^top_{r-1} G, where branch vertices are the identity on S. |
| 492 | The maximal connector is built by iterating: start with the empty graph and |
| 493 | greedily add edges until no more short paths exist. -/ |
| 494 | |
| 495 | private structure RawConnector {V : Type} [DecidableEq V] [Fintype V] |
| 496 | (G : SimpleGraph V) (r : ℕ) (S : Set V) [Fintype S] where |
| 497 | H : SimpleGraph S |
| 498 | model : ShallowTopologicalMinorModel H G (r - 1) |
| 499 | branch_vertex : ∀ w : S, model.branchVertex w = w.1 |
| 500 | |
| 501 | private def rawConnectorInternalFinset |
| 502 | {V : Type} [DecidableEq V] [Fintype V] |
| 503 | {G : SimpleGraph V} {r : ℕ} {S : Set V} [Fintype S] |
| 504 | (M : RawConnector G r S) (e : M.H.edgeSet) : Finset V := |
| 505 | (((M.model.edgePath e).support.toFinset).erase |
| 506 | (M.model.branchVertex (M.model.edgeTail e))).erase |
| 507 | (M.model.branchVertex (Sym2.Mem.other (M.model.edgeTail_mem e))) |
| 508 | |
| 509 | private def rawConnectorK |
| 510 | {V : Type} [DecidableEq V] [Fintype V] |
| 511 | {G : SimpleGraph V} {r : ℕ} {S : Set V} [Fintype S] |
| 512 | (M : RawConnector G r S) : Finset V := |
| 513 | Finset.univ.biUnion (rawConnectorInternalFinset M) |
| 514 | |
| 515 | private def emptyRawConnector |
| 516 | {V : Type} [DecidableEq V] [Fintype V] |
| 517 | (G : SimpleGraph V) (r : ℕ) (S : Set V) [Fintype S] : |
| 518 | RawConnector G r S where |
| 519 | H := ⊥ |
| 520 | model := |
| 521 | { branchVertex := ⟨Subtype.val, fun _ _ h => Subtype.ext h⟩ |
| 522 | edgeTail := fun e => absurd e.2 (by simp) |
| 523 | edgeTail_mem := fun e => absurd e.2 (by simp) |
| 524 | edgePath := fun e => absurd e.2 (by simp) |
| 525 | edgePath_isPath := fun e => absurd e.2 (by simp) |
| 526 | edgePath_length := fun e => absurd e.2 (by simp) |
| 527 | edgePath_interior_avoids_branch := fun e _ _ _ _ _ => absurd e.2 (by simp) |
| 528 | edgePath_interior_disjoint := fun e _ _ _ _ _ _ _ _ => absurd e.2 (by simp) } |
| 529 | branch_vertex := fun _ => rfl |
| 530 | |
| 531 | private theorem rawConnectorInternalFinset_card_bound |
| 532 | {V : Type} [DecidableEq V] [Fintype V] |
| 533 | {G : SimpleGraph V} {r : ℕ} {S : Set V} [Fintype S] |
| 534 | (M : RawConnector G r S) (e : M.H.edgeSet) : |
| 535 | (rawConnectorInternalFinset M e).card ≤ 2 * r - 2 := by |
| 536 | let p := M.model.edgePath e |
| 537 | let tail := M.model.branchVertex (M.model.edgeTail e) |
| 538 | let head := M.model.branchVertex (Sym2.Mem.other (M.model.edgeTail_mem e)) |
| 539 | have hpPath : p.IsPath := M.model.edgePath_isPath e |
| 540 | have htail_mem : tail ∈ p.support.toFinset := by |
| 541 | simpa [p, tail] using p.getVert_mem_support 0 |
| 542 | have hhead_mem : head ∈ p.support.toFinset := by |
| 543 | simpa [p, head] using p.getVert_mem_support p.length |
| 544 | have htail_ne_head : tail ≠ head := by |
| 545 | intro hEq |
| 546 | exact M.H.edge_other_ne e.property (M.model.edgeTail_mem e) |
| 547 | (M.model.branchVertex.injective hEq.symm) |
| 548 | have hhead_mem_erase : head ∈ p.support.toFinset.erase tail := |
| 549 | Finset.mem_erase.mpr ⟨htail_ne_head.symm, hhead_mem⟩ |
| 550 | have hcard_support : p.support.toFinset.card = p.length + 1 := by |
| 551 | rw [List.toFinset_card_of_nodup hpPath.support_nodup, |
| 552 | SimpleGraph.Walk.length_support] |
| 553 | have hcard_internal : (rawConnectorInternalFinset M e).card = p.length - 1 := by |
| 554 | have h1 : (p.support.toFinset.erase tail).card = p.length := by |
| 555 | rw [Finset.card_erase_of_mem htail_mem, hcard_support]; omega |
| 556 | have h2 : ((p.support.toFinset.erase tail).erase head).card = p.length - 1 := by |
| 557 | rw [Finset.card_erase_of_mem hhead_mem_erase, h1] |
| 558 | simpa [rawConnectorInternalFinset, p, tail, head] using h2 |
| 559 | rw [hcard_internal] |
| 560 | have : p.length ≤ 2 * (r - 1) + 1 := by simpa [p] using M.model.edgePath_length e |
| 561 | omega |
| 562 | |
| 563 | private theorem rawConnectorK_card_bound |
| 564 | {V : Type} [DecidableEq V] [Fintype V] |
| 565 | {G : SimpleGraph V} {r : ℕ} {S : Set V} [Fintype S] |
| 566 | (M : RawConnector G r S) : |
| 567 | (rawConnectorK M).card ≤ M.H.edgeFinset.card * (2 * r - 2) := by |
| 568 | calc (rawConnectorK M).card |
| 569 | ≤ (Finset.univ : Finset M.H.edgeSet).card * (2 * r - 2) := by |
| 570 | simpa [rawConnectorK] using |
| 571 | Finset.card_biUnion_le_card_mul Finset.univ (rawConnectorInternalFinset M) |
| 572 | (2 * r - 2) (fun e _ => rawConnectorInternalFinset_card_bound M e) |
| 573 | _ = M.H.edgeFinset.card * (2 * r - 2) := by |
| 574 | rw [SimpleGraph.edgeSet_univ_card] |
| 575 | |
| 576 | private theorem rawConnector_internal_mem_K |
| 577 | {V : Type} [DecidableEq V] [Fintype V] |
| 578 | {G : SimpleGraph V} {r : ℕ} {S : Set V} [Fintype S] |
| 579 | (M : RawConnector G r S) (e : M.H.edgeSet) (i : ℕ) |
| 580 | (hi0 : 0 < i) (hil : i < (M.model.edgePath e).length) : |
| 581 | (M.model.edgePath e).getVert i ∈ rawConnectorK M := by |
| 582 | let p := M.model.edgePath e |
| 583 | have hpPath : p.IsPath := M.model.edgePath_isPath e |
| 584 | have hil' : i < p.length := hil |
| 585 | have hne_tail : p.getVert i ≠ M.model.branchVertex (M.model.edgeTail e) := by |
| 586 | intro hEq |
| 587 | have : i = 0 := (hpPath.getVert_eq_start_iff hil'.le).mp (by simpa [p] using hEq) |
| 588 | omega |
| 589 | have hne_head : p.getVert i ≠ |
| 590 | M.model.branchVertex (Sym2.Mem.other (M.model.edgeTail_mem e)) := by |
| 591 | intro hEq |
| 592 | have : i = p.length := (hpPath.getVert_eq_end_iff hil'.le).mp (by simpa [p] using hEq) |
| 593 | omega |
| 594 | exact Finset.mem_biUnion.mpr ⟨e, Finset.mem_univ _, |
| 595 | Finset.mem_erase.mpr ⟨hne_head, Finset.mem_erase.mpr |
| 596 | ⟨hne_tail, by simpa using p.getVert_mem_support i⟩⟩⟩ |
| 597 | |
| 598 | private theorem rawConnector_mem_K_of_support |
| 599 | {V : Type} [DecidableEq V] [Fintype V] |
| 600 | {G : SimpleGraph V} {r : ℕ} {S : Set V} [Fintype S] |
| 601 | (M : RawConnector G r S) (e : M.H.edgeSet) {x : V} |
| 602 | (hx : x ∈ (M.model.edgePath e).support) |
| 603 | (htail : x ≠ M.model.branchVertex (M.model.edgeTail e)) |
| 604 | (hhead : x ≠ M.model.branchVertex (Sym2.Mem.other (M.model.edgeTail_mem e))) : |
| 605 | x ∈ rawConnectorK M := by |
| 606 | let p := M.model.edgePath e |
| 607 | have hpPath : p.IsPath := M.model.edgePath_isPath e |
| 608 | rcases SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hx with ⟨i, rfl, hi_le⟩ |
| 609 | have hi0 : 0 < i := by |
| 610 | by_contra hi0 |
| 611 | exact htail (by simp_all [p, Nat.eq_zero_of_not_pos hi0]) |
| 612 | have hil : i < p.length := by |
| 613 | by_contra hil |
| 614 | exact hhead (by simp_all [p, le_antisymm hi_le (Nat.not_lt.mp hil)]) |
| 615 | simpa [p] using rawConnector_internal_mem_K M e i hi0 hil |
| 616 | |
| 617 | private theorem exists_extend_rawConnector |
| 618 | {V : Type} [DecidableEq V] [Fintype V] |
| 619 | {G : SimpleGraph V} {r : ℕ} {S : Set V} [Fintype S] |
| 620 | (M : RawConnector G r S) |
| 621 | {u v : S} (huv : u ≠ v) (hAdj : ¬ M.H.Adj u v) |
| 622 | (p : G.Walk u.1 v.1) (hpPath : p.IsPath) (hpLen : p.length ≤ 2 * r - 1) |
| 623 | (hpAvoid : ∀ i : ℕ, 0 < i → i < p.length → |
| 624 | p.getVert i ∉ (S ∪ (rawConnectorK M : Set V))) : |
| 625 | ∃ M' : RawConnector G r S, |
| 626 | M'.H.edgeFinset.card = M.H.edgeFinset.card + 1 := by |
| 627 | let H' : SimpleGraph S := M.H ⊔ SimpleGraph.edge u v |
| 628 | have mem_S_of_eq_branch (w : S) {x : V} (hEq : x = M.model.branchVertex w) : x ∈ S := by |
| 629 | rw [M.branch_vertex w] at hEq; exact hEq.symm ▸ w.2 |
| 630 | have hpInternalAvoid : |
| 631 | ∀ {x : V}, x ∈ p.support → |
| 632 | x ≠ M.model.branchVertex u → |
| 633 | x ≠ M.model.branchVertex v → |
| 634 | x ∉ (S ∪ (rawConnectorK M : Set V)) := by |
| 635 | intro x hx hxu hxv |
| 636 | rcases SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hx with ⟨i, rfl, hi_le⟩ |
| 637 | have hi0 : 0 < i := by |
| 638 | by_contra hi0 |
| 639 | exact hxu (by simp_all [M.branch_vertex u, Nat.eq_zero_of_not_pos hi0]) |
| 640 | have hil : i < p.length := by |
| 641 | by_contra hil |
| 642 | exact hxv (by simp_all [M.branch_vertex v, le_antisymm hi_le (Nat.not_lt.mp hil)]) |
| 643 | exact hpAvoid i hi0 hil |
| 644 | -- Define edge tail for H' |
| 645 | let edgeTail' : H'.edgeSet → S := fun e => |
| 646 | if hOld : (e : Sym2 S) ∈ M.H.edgeSet then M.model.edgeTail ⟨e, hOld⟩ |
| 647 | else e.1.out.1 |
| 648 | have edgeTail_mem' : ∀ e : H'.edgeSet, edgeTail' e ∈ (e : Sym2 S) := by |
| 649 | intro e |
| 650 | by_cases hOld : (e : Sym2 S) ∈ M.H.edgeSet |
| 651 | · simpa [edgeTail', hOld] using M.model.edgeTail_mem ⟨e, hOld⟩ |
| 652 | · simpa [edgeTail', hOld] using Sym2.out_fst_mem (e : Sym2 S) |
| 653 | -- For new edges, classify tail/head |
| 654 | have hnew_edge : |
| 655 | ∀ e : H'.edgeSet, ¬ (e : Sym2 S) ∈ M.H.edgeSet → |
| 656 | (e : Sym2 S) = s(u, v) ∧ |
| 657 | ((edgeTail' e = u ∧ Sym2.Mem.other (edgeTail_mem' e) = v) ∨ |
| 658 | (edgeTail' e = v ∧ Sym2.Mem.other (edgeTail_mem' e) = u)) := by |
| 659 | intro e hOld |
| 660 | have he_new : (e : Sym2 S) ∈ (SimpleGraph.edge u v).edgeSet := by |
| 661 | have : (e : Sym2 S) ∈ M.H.edgeSet ∪ (SimpleGraph.edge u v).edgeSet := by |
| 662 | simpa [H'] using e.property |
| 663 | exact this.resolve_left hOld |
| 664 | have he_uv : (e : Sym2 S) = s(u, v) := by |
| 665 | simpa [SimpleGraph.edge_edgeSet_of_ne huv] using he_new |
| 666 | have htail_mem_uv : edgeTail' e ∈ s(u, v) := by |
| 667 | simpa [he_uv] using edgeTail_mem' e |
| 668 | have htail_cases : edgeTail' e = u ∨ edgeTail' e = v := by |
| 669 | simpa using htail_mem_uv |
| 670 | refine ⟨he_uv, ?_⟩ |
| 671 | rcases htail_cases with htailu | htailv |
| 672 | · left; refine ⟨htailu, ?_⟩ |
| 673 | have hother_mem : Sym2.Mem.other (edgeTail_mem' e) ∈ s(u, v) := by |
| 674 | simpa [he_uv] using Sym2.other_mem (edgeTail_mem' e) |
| 675 | have hother_ne_u : Sym2.Mem.other (edgeTail_mem' e) ≠ u := by |
| 676 | simpa [htailu] using H'.edge_other_ne e.property (edgeTail_mem' e) |
| 677 | exact (Sym2.mem_iff.mp hother_mem).resolve_left hother_ne_u |
| 678 | · right; refine ⟨htailv, ?_⟩ |
| 679 | have hother_mem : Sym2.Mem.other (edgeTail_mem' e) ∈ s(u, v) := by |
| 680 | simpa [he_uv] using Sym2.other_mem (edgeTail_mem' e) |
| 681 | have hother_ne_v : Sym2.Mem.other (edgeTail_mem' e) ≠ v := by |
| 682 | simpa [htailv] using H'.edge_other_ne e.property (edgeTail_mem' e) |
| 683 | exact ((Sym2.mem_iff.mp hother_mem).resolve_right hother_ne_v) |
| 684 | -- Define edge paths for H' |
| 685 | let edgePath' : |
| 686 | ∀ e : H'.edgeSet, |
| 687 | G.Walk (M.model.branchVertex (edgeTail' e)) |
| 688 | (M.model.branchVertex (Sym2.Mem.other (edgeTail_mem' e))) := by |
| 689 | intro e |
| 690 | by_cases hOld : (e : Sym2 S) ∈ M.H.edgeSet |
| 691 | · -- Old edge: copy the existing path |
| 692 | let eOld : M.H.edgeSet := ⟨e, hOld⟩ |
| 693 | have htailEq : edgeTail' e = M.model.edgeTail eOld := by simp [edgeTail', eOld, hOld] |
| 694 | have hotherEq : |
| 695 | Sym2.Mem.other (M.model.edgeTail_mem eOld) = |
| 696 | Sym2.Mem.other (edgeTail_mem' e) := by |
| 697 | apply Sym2.congr_right.mp |
| 698 | have hs2 : s(M.model.edgeTail eOld, Sym2.Mem.other (edgeTail_mem' e)) = (e : Sym2 S) := |
| 699 | (congrArg (s(·, Sym2.Mem.other (edgeTail_mem' e))) htailEq.symm).trans |
| 700 | (Sym2.other_spec (edgeTail_mem' e)) |
| 701 | calc s(M.model.edgeTail eOld, Sym2.Mem.other (M.model.edgeTail_mem eOld)) |
| 702 | = (e : Sym2 S) := Sym2.other_spec (M.model.edgeTail_mem eOld) |
| 703 | _ = s(M.model.edgeTail eOld, Sym2.Mem.other (edgeTail_mem' e)) := hs2.symm |
| 704 | exact (M.model.edgePath eOld).copy |
| 705 | (congrArg M.model.branchVertex htailEq.symm) |
| 706 | (congrArg M.model.branchVertex hotherEq) |
| 707 | · -- New edge: use p or p.reverse depending on tail direction |
| 708 | by_cases htailu : edgeTail' e = u |
| 709 | · have hotherv : Sym2.Mem.other (edgeTail_mem' e) = v := by |
| 710 | obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 711 | · exact hdir.2 |
| 712 | · exact absurd (hdir.1.symm.trans htailu) (Ne.symm huv) |
| 713 | exact p.copy |
| 714 | ((M.branch_vertex u).symm.trans (congrArg M.model.branchVertex htailu.symm)) |
| 715 | ((M.branch_vertex v).symm.trans (congrArg M.model.branchVertex hotherv.symm)) |
| 716 | · have htailv : edgeTail' e = v := by |
| 717 | obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 718 | · exact absurd hdir.1 htailu |
| 719 | · exact hdir.1 |
| 720 | have hotheru : Sym2.Mem.other (edgeTail_mem' e) = u := by |
| 721 | obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 722 | · exact absurd hdir.1 htailu |
| 723 | · exact hdir.2 |
| 724 | exact p.reverse.copy |
| 725 | ((M.branch_vertex v).symm.trans (congrArg M.model.branchVertex htailv.symm)) |
| 726 | ((M.branch_vertex u).symm.trans (congrArg M.model.branchVertex hotheru.symm)) |
| 727 | -- Build the extended raw connector |
| 728 | let M' : RawConnector G r S := |
| 729 | { H := H' |
| 730 | model := |
| 731 | { branchVertex := M.model.branchVertex |
| 732 | edgeTail := edgeTail' |
| 733 | edgeTail_mem := edgeTail_mem' |
| 734 | edgePath := edgePath' |
| 735 | edgePath_isPath := by |
| 736 | intro e |
| 737 | by_cases hOld : (e : Sym2 S) ∈ M.H.edgeSet |
| 738 | · simpa [edgePath', hOld] using M.model.edgePath_isPath ⟨e, hOld⟩ |
| 739 | · by_cases htailu : edgeTail' e = u |
| 740 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 741 | · simpa [edgePath', hOld, htailu, hdir.2] using hpPath |
| 742 | · exact absurd (hdir.1.symm.trans htailu) (Ne.symm huv) |
| 743 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 744 | · exact absurd hdir.1 htailu |
| 745 | · simpa [edgePath', hOld, htailu, hdir.1, hdir.2, |
| 746 | show v ≠ u from fun h => huv h.symm] using hpPath.reverse |
| 747 | edgePath_length := by |
| 748 | intro e |
| 749 | have hpLen' : p.length ≤ 2 * (r - 1) + 1 := by omega |
| 750 | by_cases hOld : (e : Sym2 S) ∈ M.H.edgeSet |
| 751 | · simpa [edgePath', hOld] using M.model.edgePath_length ⟨e, hOld⟩ |
| 752 | · by_cases htailu : edgeTail' e = u |
| 753 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 754 | · simpa [edgePath', hOld, htailu, hdir.2] using hpLen' |
| 755 | · exact absurd (hdir.1.symm.trans htailu) (Ne.symm huv) |
| 756 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 757 | · exact absurd hdir.1 htailu |
| 758 | · simpa [edgePath', hOld, htailu, hdir.1, hdir.2, |
| 759 | show v ≠ u from fun h => huv h.symm] using hpLen' |
| 760 | edgePath_interior_avoids_branch := by |
| 761 | intro e x hx htail hhead w |
| 762 | by_cases hOld : (e : Sym2 S) ∈ M.H.edgeSet |
| 763 | · exact M.model.edgePath_interior_avoids_branch ⟨e, hOld⟩ |
| 764 | (by simpa [edgePath', hOld] using hx) |
| 765 | (by simpa [edgeTail', hOld, edgeTail_mem'] using htail) |
| 766 | (by simpa [edgeTail', hOld, edgeTail_mem'] using hhead) |
| 767 | w |
| 768 | · by_cases htailu : edgeTail' e = u |
| 769 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 770 | · have hxP : x ∈ p.support := by |
| 771 | simpa [edgePath', hOld, htailu, hdir.2] using hx |
| 772 | have htailP : x ≠ M.model.branchVertex u := by |
| 773 | simpa [edgeTail', hOld, htailu] using htail |
| 774 | have hheadP : x ≠ M.model.branchVertex v := by |
| 775 | exact fun hEq => hhead (hEq.trans (congrArg M.model.branchVertex hdir.2.symm)) |
| 776 | have hxAvoid := hpInternalAvoid hxP htailP hheadP |
| 777 | exact fun hEq => hxAvoid (Set.mem_union_left _ (mem_S_of_eq_branch w hEq)) |
| 778 | · exact absurd (hdir.1.symm.trans htailu) (Ne.symm huv) |
| 779 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 780 | · exact absurd hdir.1 htailu |
| 781 | · have hxP : x ∈ p.support := by |
| 782 | simpa [edgePath', hOld, htailu, hdir.1, hdir.2, |
| 783 | SimpleGraph.Walk.support_reverse, |
| 784 | show v ≠ u from fun h => huv h.symm] using hx |
| 785 | have htailP : x ≠ M.model.branchVertex v := by |
| 786 | simpa [edgeTail', hOld, hdir.1] using htail |
| 787 | have hheadP : x ≠ M.model.branchVertex u := by |
| 788 | exact fun hEq => |
| 789 | hhead (hEq.trans (congrArg M.model.branchVertex hdir.2.symm)) |
| 790 | have hxAvoid := hpInternalAvoid hxP hheadP htailP |
| 791 | exact fun hEq => hxAvoid (Set.mem_union_left _ (mem_S_of_eq_branch w hEq)) |
| 792 | edgePath_interior_disjoint := by |
| 793 | intro e e' x hne hx hx' htail hhead htail' hhead' |
| 794 | by_cases hOld : (e : Sym2 S) ∈ M.H.edgeSet |
| 795 | · by_cases hOld' : (e' : Sym2 S) ∈ M.H.edgeSet |
| 796 | · -- Both old edges |
| 797 | have hneOld : (⟨e.val, hOld⟩ : M.H.edgeSet) ≠ ⟨e'.val, hOld'⟩ := by |
| 798 | intro h |
| 799 | have hvalEq : (e : Sym2 S) = (e' : Sym2 S) := |
| 800 | congrArg (fun x : M.H.edgeSet => (x : Sym2 S)) h |
| 801 | exact hne (Subtype.ext hvalEq) |
| 802 | exact M.model.edgePath_interior_disjoint ⟨e, hOld⟩ ⟨e', hOld'⟩ hneOld |
| 803 | (by simpa [edgePath', hOld] using hx) |
| 804 | (by simpa [edgePath', hOld'] using hx') |
| 805 | (by simpa [edgeTail', hOld, edgeTail_mem'] using htail) |
| 806 | (by simpa [edgeTail', hOld, edgeTail_mem'] using hhead) |
| 807 | (by simpa [edgeTail', hOld', edgeTail_mem'] using htail') |
| 808 | (by simpa [edgeTail', hOld', edgeTail_mem'] using hhead') |
| 809 | · -- e old, e' new: x ∈ K from old, x ∉ K from new |
| 810 | have hxinK : x ∈ rawConnectorK M := |
| 811 | rawConnector_mem_K_of_support M ⟨e, hOld⟩ |
| 812 | (by simpa [edgePath', hOld] using hx) |
| 813 | (by simpa [edgeTail', hOld, edgeTail_mem'] using htail) |
| 814 | (by simpa [edgeTail', hOld, edgeTail_mem'] using hhead) |
| 815 | by_cases htailu' : edgeTail' e' = u |
| 816 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e' hOld' |
| 817 | · have hxP : x ∈ p.support := by |
| 818 | simpa [edgePath', hOld', htailu', hdir.2] using hx' |
| 819 | have htailP : x ≠ M.model.branchVertex u := by |
| 820 | simpa [edgeTail', hOld', htailu'] using htail' |
| 821 | have hheadP : x ≠ M.model.branchVertex v := by |
| 822 | exact fun hEq => |
| 823 | hhead' (hEq.trans (congrArg M.model.branchVertex hdir.2.symm)) |
| 824 | exact (hpInternalAvoid hxP htailP hheadP) (Or.inr hxinK) |
| 825 | · exact absurd (hdir.1.symm.trans htailu') (Ne.symm huv) |
| 826 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e' hOld' |
| 827 | · exact absurd hdir.1 htailu' |
| 828 | · have hxP : x ∈ p.support := by |
| 829 | simpa [edgePath', hOld', htailu', hdir.1, hdir.2, |
| 830 | SimpleGraph.Walk.support_reverse, |
| 831 | show v ≠ u from fun h => huv h.symm] using hx' |
| 832 | have htailP : x ≠ M.model.branchVertex v := by |
| 833 | simpa [edgeTail', hOld', hdir.1] using htail' |
| 834 | have hheadP : x ≠ M.model.branchVertex u := by |
| 835 | exact fun hEq => |
| 836 | hhead' (hEq.trans (congrArg M.model.branchVertex hdir.2.symm)) |
| 837 | exact (hpInternalAvoid hxP hheadP htailP) (Or.inr hxinK) |
| 838 | · by_cases hOld' : (e' : Sym2 S) ∈ M.H.edgeSet |
| 839 | · -- e new, e' old: symmetric |
| 840 | have hxinK : x ∈ rawConnectorK M := |
| 841 | rawConnector_mem_K_of_support M ⟨e', hOld'⟩ |
| 842 | (by simpa [edgePath', hOld'] using hx') |
| 843 | (by simpa [edgeTail', hOld', edgeTail_mem'] using htail') |
| 844 | (by simpa [edgeTail', hOld', edgeTail_mem'] using hhead') |
| 845 | by_cases htailu : edgeTail' e = u |
| 846 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 847 | · have hxP : x ∈ p.support := by |
| 848 | simpa [edgePath', hOld, htailu, hdir.2] using hx |
| 849 | have htailP : x ≠ M.model.branchVertex u := by |
| 850 | simpa [edgeTail', hOld, htailu] using htail |
| 851 | have hheadP : x ≠ M.model.branchVertex v := by |
| 852 | exact fun hEq => |
| 853 | hhead (hEq.trans (congrArg M.model.branchVertex hdir.2.symm)) |
| 854 | exact (hpInternalAvoid hxP htailP hheadP) (Or.inr hxinK) |
| 855 | · exact absurd (hdir.1.symm.trans htailu) (Ne.symm huv) |
| 856 | · obtain ⟨_, hdir | hdir⟩ := hnew_edge e hOld |
| 857 | · exact absurd hdir.1 htailu |
| 858 | · have hxP : x ∈ p.support := by |
| 859 | simpa [edgePath', hOld, htailu, hdir.1, hdir.2, |
| 860 | SimpleGraph.Walk.support_reverse, |
| 861 | show v ≠ u from fun h => huv h.symm] using hx |
| 862 | have htailP : x ≠ M.model.branchVertex v := by |
| 863 | simpa [edgeTail', hOld, hdir.1] using htail |
| 864 | have hheadP : x ≠ M.model.branchVertex u := by |
| 865 | exact fun hEq => |
| 866 | hhead (hEq.trans (congrArg M.model.branchVertex hdir.2.symm)) |
| 867 | exact (hpInternalAvoid hxP hheadP htailP) (Or.inr hxinK) |
| 868 | · -- Both new: both must be s(u,v), so e = e' |
| 869 | obtain ⟨he_uv, _⟩ := hnew_edge e hOld |
| 870 | obtain ⟨he_uv', _⟩ := hnew_edge e' hOld' |
| 871 | exact hne (Subtype.ext (he_uv.trans he_uv'.symm)) } |
| 872 | branch_vertex := M.branch_vertex } |
| 873 | refine ⟨M', ?_⟩ |
| 874 | have := SimpleGraph.card_edgeFinset_sup_edge M.H hAdj huv |
| 875 | convert this using 2 |
| 876 | ext e; simp [M', H'] |
| 877 | |
| 878 | /-! ### Helper: maximal connector model |
| 879 | |
| 880 | Builds a maximal family of short paths between S-vertex pairs (internal |
| 881 | vertices outside S). Returns the graph H on S, its decidable adjacency, |
| 882 | the kernel K of internal vertices, and: |
| 883 | - H is a depth-(r-1) topological minor of G |
| 884 | - |K| ≤ |E(H)| · (2r-2) |
| 885 | - Maximality: for non-adjacent S-pairs, no short path avoids S ∪ K -/ |
| 886 | |
| 887 | private theorem exists_maximal_connector |
| 888 | {V : Type} [DecidableEq V] [Fintype V] |
| 889 | (G : SimpleGraph V) (r : ℕ) (S : Set V) [Fintype S] : |
| 890 | ∃ (H : SimpleGraph S) (_ : DecidableRel H.Adj) (K : Finset V), |
| 891 | IsShallowTopologicalMinor H G (r - 1) ∧ |
| 892 | K.card ≤ H.edgeFinset.card * (2 * r - 2) ∧ |
| 893 | (∀ u v : S, u ≠ v → ¬H.Adj u v → |
| 894 | ¬∃ p : G.Walk u.1 v.1, |
| 895 | p.IsPath ∧ p.length ≤ 2 * r - 1 ∧ |
| 896 | ∀ i : ℕ, 0 < i → i < p.length → p.getVert i ∉ (S ∪ (K : Set V))) := by |
| 897 | let P : ℕ → Prop := fun n => |
| 898 | ∃ M : RawConnector G r S, M.H.edgeFinset.card = n |
| 899 | have hP0 : P 0 := ⟨emptyRawConnector G r S, by simp [emptyRawConnector]⟩ |
| 900 | let bound := (Fintype.card S).choose 2 |
| 901 | have hPN : P (Nat.findGreatest P bound) := Nat.findGreatest_spec (zero_le _) hP0 |
| 902 | obtain ⟨M, hMcard⟩ := hPN |
| 903 | refine ⟨M.H, inferInstance, rawConnectorK M, ⟨M.model⟩, rawConnectorK_card_bound M, ?_⟩ |
| 904 | intro u v huv hAdj hPath |
| 905 | obtain ⟨p, hpPath, hpLen, hpAvoid⟩ := hPath |
| 906 | obtain ⟨M', hM'card⟩ := exists_extend_rawConnector M huv hAdj p hpPath hpLen hpAvoid |
| 907 | have hM'bound : M'.H.edgeFinset.card ≤ bound := by |
| 908 | simpa [bound] using SimpleGraph.card_edgeFinset_le_card_choose_two (G := M'.H) |
| 909 | have hlt : Nat.findGreatest P bound < M'.H.edgeFinset.card := by |
| 910 | rw [← hMcard, hM'card]; omega |
| 911 | exact Nat.findGreatest_is_greatest hlt hM'bound ⟨M', rfl⟩ |
| 912 | |
| 913 | /-! ### Helper: maximal connector + independent set (assembly) |
| 914 | |
| 915 | Combines the maximal connector model with the density hypothesis and |
| 916 | independent set extraction. -/ |
| 917 | |
| 918 | private theorem exists_connector_and_indepset |
| 919 | {V : Type} [DecidableEq V] [Fintype V] |
| 920 | (G : SimpleGraph V) (r d : ℕ) (S : Set V) [Fintype S] |
| 921 | (hd : ∀ {W : Type} [DecidableEq W] [Fintype W] |
| 922 | (H : SimpleGraph W) [DecidableRel H.Adj], |
| 923 | IsShallowTopologicalMinor H G (r - 1) → |
| 924 | H.edgeFinset.card ≤ d * Fintype.card W) : |
| 925 | ∃ (K : Finset V) (I : Finset S), |
| 926 | K.card ≤ d * Fintype.card S * (2 * r - 2) ∧ |
| 927 | Fintype.card S ≤ I.card * (2 * d + 1) ∧ |
| 928 | (∀ u ∈ I, ∀ v ∈ I, u ≠ v → |
| 929 | ¬ ∃ p : G.Walk u.1 v.1, |
| 930 | p.IsPath ∧ p.length ≤ 2 * r - 1 ∧ |
| 931 | ∀ i : ℕ, 0 < i → i < p.length → p.getVert i ∉ (S ∪ (K : Set V))) := by |
| 932 | obtain ⟨H, instDecH, K, hMinor, hKcard, hMaximal⟩ := exists_maximal_connector G r S |
| 933 | letI : DecidableRel H.Adj := instDecH |
| 934 | have hEdge : H.edgeFinset.card ≤ d * Fintype.card S := hd H hMinor |
| 935 | have hKbound : K.card ≤ d * Fintype.card S * (2 * r - 2) := |
| 936 | le_trans hKcard (mul_le_mul_of_nonneg_right hEdge (Nat.zero_le _)) |
| 937 | obtain ⟨I, hIndep, hIcard⟩ := exists_indepset_of_edge_bound H d hEdge |
| 938 | exact ⟨K, I, hKbound, hIcard, |
| 939 | fun u hu v hv huv => hMaximal u v huv (hIndep u hu v hv huv)⟩ |
| 940 | |
| 941 | /-! ### Helper: extract a concrete path family from subsetAdmValue -/ |
| 942 | |
| 943 | private theorem exists_subsetAdmFamily_of_le_subsetAdmValue |
| 944 | {V : Type} [DecidableEq V] [Fintype V] |
| 945 | (G : SimpleGraph V) (r : ℕ) (S : Set V) (v : V) {n : ℕ} |
| 946 | (hn : 0 < n) |
| 947 | (hvn : n ≤ subsetAdmValue G r S v) : |
| 948 | ∃ paths : Fin n → (u : V) × G.Walk v u, IsSubsetAdmFamily G r S v paths := by |
| 949 | unfold subsetAdmValue at hvn |
| 950 | obtain ⟨k, _, hkLe⟩ := |
| 951 | (Finset.le_sup_iff (s := Finset.range (Fintype.card V)) |
| 952 | (f := fun k => |
| 953 | if ∃ paths : Fin k → (u : V) × G.Walk v u, IsSubsetAdmFamily G r S v paths |
| 954 | then k else 0) hn).mp hvn |
| 955 | split_ifs at hkLe with hkWitness |
| 956 | · rcases hkWitness with ⟨pathsK, hpathsK⟩ |
| 957 | exact ⟨fun i => pathsK ⟨i.1, lt_of_lt_of_le i.2 hkLe⟩, |
| 958 | ⟨fun i => hpathsK.target_mem ⟨i.1, lt_of_lt_of_le i.2 hkLe⟩, |
| 959 | fun i => hpathsK.target_ne ⟨i.1, lt_of_lt_of_le i.2 hkLe⟩, |
| 960 | fun i => hpathsK.isPath ⟨i.1, lt_of_lt_of_le i.2 hkLe⟩, |
| 961 | fun i => hpathsK.length_le ⟨i.1, lt_of_lt_of_le i.2 hkLe⟩, |
| 962 | fun i j hj0 hjlen => |
| 963 | hpathsK.internal_avoids ⟨i.1, lt_of_lt_of_le i.2 hkLe⟩ j hj0 hjlen, |
| 964 | fun i j hij => hpathsK.disjoint ⟨i.1, lt_of_lt_of_le i.2 hkLe⟩ |
| 965 | ⟨j.1, lt_of_lt_of_le j.2 hkLe⟩ (by |
| 966 | intro hEq; exact hij (Fin.ext (Fin.mk.inj hEq)))⟩⟩ |
| 967 | · omega |
| 968 | |
| 969 | /-! ### Helper: dense shallow minor from large path families |
| 970 | |
| 971 | Given that every vertex of S has subsetAdmValue ≥ n, plus a kernel set K |
| 972 | and an independent set I whose pairs admit no short path avoiding S ∪ K, |
| 973 | construct a depth-(r-1) topological minor J of G with: |
| 974 | • |V(J)| ≤ |S| + |K| |
| 975 | • |E(J)| ≥ |I| · n -/ |
| 976 | |
| 977 | private theorem exists_dense_shallow_minor |
| 978 | {V : Type} [DecidableEq V] [Fintype V] |
| 979 | (G : SimpleGraph V) (r : ℕ) (S : Set V) [Fintype S] (n : ℕ) |
| 980 | (hn : 0 < n) |
| 981 | (hLarge : ∀ v ∈ S, n ≤ subsetAdmValue G r S v) |
| 982 | (K : Finset V) (I : Finset S) |
| 983 | (hNoCross : ∀ u ∈ I, ∀ v ∈ I, u ≠ v → |
| 984 | ¬ ∃ p : G.Walk u.1 v.1, |
| 985 | p.IsPath ∧ p.length ≤ 2 * r - 1 ∧ |
| 986 | ∀ i : ℕ, 0 < i → i < p.length → p.getVert i ∉ (S ∪ (K : Set V))) : |
| 987 | ∃ (W' : Type) (_ : DecidableEq W') (_ : Fintype W') (J : SimpleGraph W') |
| 988 | (_ : DecidableRel J.Adj), |
| 989 | IsShallowTopologicalMinor J G (r - 1) ∧ |
| 990 | Fintype.card W' ≤ Fintype.card S + K.card ∧ |
| 991 | I.card * n ≤ J.edgeFinset.card := by |
| 992 | -- Set up types |
| 993 | let W := {x : V // x ∈ S ∨ x ∈ (K : Set V)} |
| 994 | let U : Set V := S ∪ (K : Set V) |
| 995 | let IV : Type := ↥I |
| 996 | let A : Type := IV × Fin n |
| 997 | -- Extract path families for each vertex in I |
| 998 | have hLargeIV : ∀ v : IV, n ≤ subsetAdmValue G r S v.1.1 := |
| 999 | fun v => hLarge v.1.1 v.1.2 |
| 1000 | choose rawPaths rawFamily using fun v : IV => |
| 1001 | exists_subsetAdmFamily_of_le_subsetAdmValue G r S v.1.1 hn (hLargeIV v) |
| 1002 | let root : IV → V := fun v => v.1.1 |
| 1003 | let rootW : IV → W := fun v => ⟨root v, Or.inl v.1.2⟩ |
| 1004 | let rawTarget : A → V := fun a => (rawPaths a.1 a.2).1 |
| 1005 | let rawWalk : ∀ a : A, G.Walk (root a.1) (rawTarget a) := fun a => (rawPaths a.1 a.2).2 |
| 1006 | -- Find first hit in U for each raw walk |
| 1007 | let hitSet : A → Finset V := fun a => |
| 1008 | Finset.univ.filter fun x => x ∈ U ∧ x ≠ root a.1 |
| 1009 | have hHitNonempty : ∀ a : A, {x ∈ hitSet a | x ∈ (rawWalk a).support}.Nonempty := by |
| 1010 | intro a |
| 1011 | refine ⟨rawTarget a, ?_⟩ |
| 1012 | have hmemS : rawTarget a ∈ S := (rawFamily a.1).target_mem a.2 |
| 1013 | have hne : rawTarget a ≠ root a.1 := (rawFamily a.1).target_ne a.2 |
| 1014 | have hsupport : rawTarget a ∈ (rawWalk a).support := |
| 1015 | (rawWalk a).end_mem_support |
| 1016 | simp [hitSet, U, hmemS, hne, hsupport] |
| 1017 | -- Extract first-hit vertex |
| 1018 | have hFirstHit : ∀ a : A, ∃ x ∈ hitSet a, ∃ (hx : x ∈ (rawWalk a).support), |
| 1019 | ∀ t ∈ hitSet a, t ∈ ((rawWalk a).takeUntil x hx).support → t = x := |
| 1020 | fun a => (rawWalk a).exists_mem_support_forall_mem_support_imp_eq (hitSet a) (hHitNonempty a) |
| 1021 | let hit : A → V := fun a => Classical.choose (hFirstHit a) |
| 1022 | have hHit_mem_set : ∀ a : A, hit a ∈ hitSet a := |
| 1023 | fun a => (Classical.choose_spec (hFirstHit a)).1 |
| 1024 | have hHit_mem_support : ∀ a : A, hit a ∈ (rawWalk a).support := |
| 1025 | fun a => (Classical.choose_spec (hFirstHit a)).2.1 |
| 1026 | have hHit_first : |
| 1027 | ∀ a : A, ∀ t ∈ hitSet a, |
| 1028 | t ∈ ((rawWalk a).takeUntil (hit a) (hHit_mem_support a)).support → t = hit a := |
| 1029 | fun a => (Classical.choose_spec (hFirstHit a)).2.2 |
| 1030 | -- Trimmed walks |
| 1031 | let q : ∀ a : A, G.Walk (root a.1) (hit a) := fun a => |
| 1032 | (rawWalk a).takeUntil (hit a) (hHit_mem_support a) |
| 1033 | have hqPath : ∀ a : A, (q a).IsPath := |
| 1034 | fun a => (rawFamily a.1).isPath a.2 |>.takeUntil (hHit_mem_support a) |
| 1035 | have hqLen : ∀ a : A, (q a).length ≤ r := |
| 1036 | fun a => le_trans ((rawWalk a).length_takeUntil_le (hHit_mem_support a)) |
| 1037 | ((rawFamily a.1).length_le a.2) |
| 1038 | have hHit_mem_union : ∀ a : A, hit a ∈ U := |
| 1039 | fun a => (show hit a ∈ U ∧ hit a ≠ root a.1 from by simpa [hitSet] using hHit_mem_set a).1 |
| 1040 | have hHit_ne_root : ∀ a : A, hit a ≠ root a.1 := |
| 1041 | fun a => (show hit a ∈ U ∧ hit a ≠ root a.1 from by simpa [hitSet] using hHit_mem_set a).2 |
| 1042 | let endW : A → W := fun a => ⟨hit a, hHit_mem_union a⟩ |
| 1043 | -- Interior of trimmed walk avoids U |
| 1044 | have hqSupportAvoid : |
| 1045 | ∀ a : A, ∀ {x : V}, x ∈ (q a).support → |
| 1046 | x ≠ root a.1 → x ≠ hit a → x ∉ U := by |
| 1047 | intro a x hx hxroot hxhit hxU |
| 1048 | have hxHitSet : x ∈ hitSet a := by simpa [hitSet, U, hxU, hxroot] |
| 1049 | exact hxhit (hHit_first a x hxHitSet hx) |
| 1050 | have hqAvoid : |
| 1051 | ∀ a : A, ∀ i : ℕ, 0 < i → i < (q a).length → (q a).getVert i ∉ U := by |
| 1052 | intro a i hi0 hil |
| 1053 | refine hqSupportAvoid a ((q a).getVert_mem_support i) ?_ ?_ |
| 1054 | · intro hEq |
| 1055 | have : i = 0 := (hqPath a).getVert_eq_start_iff (le_of_lt hil) |>.mp (by |
| 1056 | simpa [q, root] using hEq) |
| 1057 | exact hi0.ne' this |
| 1058 | · intro hEq |
| 1059 | have : i = (q a).length := (hqPath a).getVert_eq_end_iff (le_of_lt hil) |>.mp (by |
| 1060 | simpa [q] using hEq) |
| 1061 | exact (Nat.ne_of_lt hil) this |
| 1062 | -- r ≥ 1 (vacuous when A is empty) |
| 1063 | have hrPos : ∀ a : A, 1 ≤ r := by |
| 1064 | intro a |
| 1065 | by_contra hr |
| 1066 | have hr0 : r = 0 := Nat.eq_zero_of_not_pos hr |
| 1067 | have hzero : subsetAdmValue G 0 S (root a.1) = 0 := |
| 1068 | subsetAdmValue_eq_zero_of_r_eq_zero G S (root a.1) |
| 1069 | have : n ≤ 0 := by simpa [root, hr0, hzero] using hLargeIV a.1 |
| 1070 | exact (Nat.not_lt_of_ge this) hn |
| 1071 | -- hit a ≠ root b for distinct IV components |
| 1072 | have hHit_ne_other_root : |
| 1073 | ∀ a b : A, a.1 ≠ b.1 → hit a ≠ root b.1 := by |
| 1074 | intro a b hab hEq |
| 1075 | let u : S := a.1.1 |
| 1076 | let v : S := b.1.1 |
| 1077 | have huv : u ≠ v := by |
| 1078 | intro huv; exact hab (Subtype.ext huv) |
| 1079 | have hlen : (q a).length ≤ 2 * r - 1 := by |
| 1080 | exact le_trans (hqLen a) (by omega) |
| 1081 | let hp : G.Walk u.1 v.1 := (q a).copy rfl hEq |
| 1082 | exact hNoCross u a.1.2 v b.1.2 huv ⟨hp, by simpa [hp] using hqPath a, |
| 1083 | by simpa [hp] using hlen, by |
| 1084 | intro i hi0 hil |
| 1085 | simpa [hp, U] using hqAvoid a i hi0 (by simpa [hp] using hil)⟩ |
| 1086 | -- Prefix of q avoids hit at end |
| 1087 | have hTakeUntil_not_hit : |
| 1088 | ∀ {a : A} {x : V} (hx : x ∈ (q a).support), |
| 1089 | x ≠ root a.1 → x ≠ hit a → |
| 1090 | hit a ∉ ((q a).takeUntil x hx).support := by |
| 1091 | intro a x hx hxroot hxhit hmem |
| 1092 | let qa : G.Walk (root a.1) x := (q a).takeUntil x hx |
| 1093 | have hqa_lt : qa.length < (q a).length := by |
| 1094 | have hle : qa.length ≤ (q a).length := (q a).length_takeUntil_le hx |
| 1095 | by_contra hlt |
| 1096 | have hEqLen : qa.length = (q a).length := le_antisymm hle (Nat.not_lt.mp hlt) |
| 1097 | have hxEnd : x = hit a := by |
| 1098 | have htake : qa.getVert qa.length = (q a).getVert qa.length := |
| 1099 | (q a).getVert_takeUntil hx le_rfl |
| 1100 | have hxAt : (q a).getVert qa.length = x := by |
| 1101 | rw [← htake]; exact qa.getVert_length |
| 1102 | have hEnd : (q a).getVert qa.length = hit a := by |
| 1103 | simpa [hEqLen] using (q a).getVert_length |
| 1104 | exact hxAt.symm.trans hEnd |
| 1105 | exact hxhit hxEnd |
| 1106 | rcases SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hmem with ⟨j, hjEq, hjle⟩ |
| 1107 | have htake : qa.getVert j = (q a).getVert j := |
| 1108 | (q a).getVert_takeUntil hx hjle |
| 1109 | have hqEq : (q a).getVert j = hit a := by rw [← htake, hjEq] |
| 1110 | have hjEnd : j = (q a).length := |
| 1111 | (hqPath a).getVert_eq_end_iff (le_trans hjle (le_of_lt hqa_lt)) |>.mp hqEq |
| 1112 | exact (Nat.not_le_of_lt hqa_lt) (hjEnd ▸ hjle) |
| 1113 | -- Prefix of q: interior avoids U |
| 1114 | have hTakeUntil_avoid : |
| 1115 | ∀ {a : A} {x w : V} (hx : x ∈ (q a).support), |
| 1116 | x ≠ root a.1 → x ≠ hit a → |
| 1117 | w ∈ ((q a).takeUntil x hx).support → |
| 1118 | w ≠ root a.1 → w ∉ U := by |
| 1119 | intro a x w hx hxroot hxhit hw hwroot |
| 1120 | have hwq : w ∈ (q a).support := (q a).support_takeUntil_subset hx hw |
| 1121 | have hwhit : w ≠ hit a := by |
| 1122 | intro hwEq |
| 1123 | exact hTakeUntil_not_hit hx hxroot hxhit (hwEq ▸ hw) |
| 1124 | exact hqSupportAvoid a hwq hwroot hwhit |
| 1125 | -- Cross-path impossibility: paths from different IV components can't share |
| 1126 | -- an interior vertex |
| 1127 | have hNoCrossInterior : |
| 1128 | ∀ {a b : A} {x : V}, |
| 1129 | a.1 ≠ b.1 → |
| 1130 | x ∈ (q a).support → |
| 1131 | x ∈ (q b).support → |
| 1132 | x ≠ root a.1 → |
| 1133 | x ≠ hit a → |
| 1134 | x ≠ root b.1 → |
| 1135 | x ≠ hit b → |
| 1136 | False := by |
| 1137 | intro a b x hab hxa hxb hxra hxea hxrb hxeb |
| 1138 | let qa : G.Walk (root a.1) x := (q a).takeUntil x hxa |
| 1139 | let qb : G.Walk (root b.1) x := (q b).takeUntil x hxb |
| 1140 | have hqa_lt : qa.length < (q a).length := by |
| 1141 | have hle : qa.length ≤ (q a).length := (q a).length_takeUntil_le hxa |
| 1142 | by_contra hlt |
| 1143 | have hEqLen : qa.length = (q a).length := le_antisymm hle (Nat.not_lt.mp hlt) |
| 1144 | have hxEnd : x = hit a := by |
| 1145 | have htake : qa.getVert qa.length = (q a).getVert qa.length := |
| 1146 | (q a).getVert_takeUntil hxa le_rfl |
| 1147 | have hxAt : (q a).getVert qa.length = x := by rw [← htake]; exact qa.getVert_length |
| 1148 | exact hxAt.symm.trans (by simpa [hEqLen] using (q a).getVert_length) |
| 1149 | exact hxea hxEnd |
| 1150 | have hqb_lt : qb.length < (q b).length := by |
| 1151 | have hle : qb.length ≤ (q b).length := (q b).length_takeUntil_le hxb |
| 1152 | by_contra hlt |
| 1153 | have hEqLen : qb.length = (q b).length := le_antisymm hle (Nat.not_lt.mp hlt) |
| 1154 | have hxEnd : x = hit b := by |
| 1155 | have htake : qb.getVert qb.length = (q b).getVert qb.length := |
| 1156 | (q b).getVert_takeUntil hxb le_rfl |
| 1157 | have hxAt : (q b).getVert qb.length = x := by rw [← htake]; exact qb.getVert_length |
| 1158 | exact hxAt.symm.trans (by simpa [hEqLen] using (q b).getVert_length) |
| 1159 | exact hxeb hxEnd |
| 1160 | let raw : G.Walk (root a.1) (root b.1) := qa.append qb.reverse |
| 1161 | let p : G.Walk (root a.1) (root b.1) := raw.bypass |
| 1162 | have hpPath : p.IsPath := raw.bypass_isPath |
| 1163 | have hpLen : p.length ≤ 2 * r - 1 := by |
| 1164 | have hr1 : 1 ≤ r := hrPos a |
| 1165 | have hraw : raw.length ≤ 2 * r - 1 := by |
| 1166 | rw [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_reverse] |
| 1167 | have hqa_le : qa.length + 1 ≤ r := lt_of_lt_of_le hqa_lt (hqLen a) |
| 1168 | have hqb_le : qb.length + 1 ≤ r := lt_of_lt_of_le hqb_lt (hqLen b) |
| 1169 | omega |
| 1170 | exact le_trans raw.length_bypass_le hraw |
| 1171 | have hpAvoid : |
| 1172 | ∀ i : ℕ, 0 < i → i < p.length → p.getVert i ∉ U := by |
| 1173 | intro i hi0 hil |
| 1174 | have hwRaw : p.getVert i ∈ raw.support := |
| 1175 | raw.support_bypass_subset (p.getVert_mem_support i) |
| 1176 | have hwStart : p.getVert i ≠ root a.1 := by |
| 1177 | intro hEq |
| 1178 | have : i = 0 := (hpPath.getVert_eq_start_iff (le_of_lt hil)).mp (by |
| 1179 | simpa [p, root] using hEq) |
| 1180 | exact hi0.ne' this |
| 1181 | have hwEnd : p.getVert i ≠ root b.1 := by |
| 1182 | intro hEq |
| 1183 | have : i = p.length := (hpPath.getVert_eq_end_iff (le_of_lt hil)).mp (by |
| 1184 | simpa [p, root] using hEq) |
| 1185 | exact (Nat.ne_of_lt hil) this |
| 1186 | rw [SimpleGraph.Walk.mem_support_append_iff] at hwRaw |
| 1187 | rcases hwRaw with hwqa | hwqb |
| 1188 | · exact hTakeUntil_avoid hxa hxra hxea hwqa hwStart |
| 1189 | · have hwqb' : p.getVert i ∈ qb.support := |
| 1190 | List.mem_reverse.mp (by simpa [SimpleGraph.Walk.support_reverse] using hwqb) |
| 1191 | exact hTakeUntil_avoid hxb hxrb hxeb hwqb' hwEnd |
| 1192 | let u : S := a.1.1 |
| 1193 | let v : S := b.1.1 |
| 1194 | have huv : u ≠ v := by intro huv; exact hab (Subtype.ext huv) |
| 1195 | exact hNoCross u a.1.2 v b.1.2 huv ⟨p, hpPath, hpLen, by |
| 1196 | intro i hi0 hil; exact hpAvoid i hi0 hil⟩ |
| 1197 | -- Build J on W |
| 1198 | let edgeSym : A → Sym2 W := fun a => s(rootW a.1, endW a) |
| 1199 | let E : Finset (Sym2 W) := Finset.univ.image edgeSym |
| 1200 | let J : SimpleGraph W := SimpleGraph.fromEdgeSet ((E : Finset (Sym2 W)) : Set (Sym2 W)) |
| 1201 | have hEnd_ne_rootW : ∀ a : A, endW a ≠ rootW a.1 := by |
| 1202 | intro a hEq; exact hHit_ne_root a (congrArg Subtype.val hEq) |
| 1203 | -- Edge injection |
| 1204 | have hEdgeInj : Function.Injective edgeSym := by |
| 1205 | intro a b hab' |
| 1206 | rcases (Sym2.eq_iff.mp hab') with h | h |
| 1207 | · rcases h with ⟨hroot, hend⟩ |
| 1208 | have hVeq : (rootW a.1).1 = (rootW b.1).1 := congrArg Subtype.val hroot |
| 1209 | have hrootIV : a.1 = b.1 := Subtype.ext (Subtype.ext hVeq) |
| 1210 | have hhit : hit a = hit b := congrArg Subtype.val hend |
| 1211 | have hidx : a.2 = b.2 := by |
| 1212 | by_contra hne |
| 1213 | have hSupportEq : (rawPaths a.1 b.2).2.support = (rawPaths b.1 b.2).2.support := |
| 1214 | congrArg (fun v => (rawPaths v b.2).2.support) hrootIV |
| 1215 | have hbmem0 : hit a ∈ (rawPaths b.1 b.2).2.support := by |
| 1216 | simpa [hhit] using hHit_mem_support b |
| 1217 | have hbmem : hit a ∈ (rawPaths a.1 b.2).2.support := hSupportEq ▸ hbmem0 |
| 1218 | have hdisj := (rawFamily a.1).disjoint a.2 b.2 hne (hit a) |
| 1219 | (hHit_mem_support a) hbmem |
| 1220 | exact hHit_ne_root a hdisj |
| 1221 | exact Prod.ext hrootIV hidx |
| 1222 | · rcases h with ⟨ha, hb⟩ |
| 1223 | exfalso |
| 1224 | have hv : a.1 ≠ b.1 := by |
| 1225 | intro hEq |
| 1226 | have : endW b = rootW b.1 := by simpa [hEq] using ha.symm |
| 1227 | exact hEnd_ne_rootW b this |
| 1228 | exact (hHit_ne_other_root b a (by simpa using hv.symm)) ((congrArg Subtype.val ha).symm) |
| 1229 | -- Edge membership |
| 1230 | have hEdge_mem : ∀ a : A, edgeSym a ∈ J.edgeSet := by |
| 1231 | intro a |
| 1232 | have hmemE : edgeSym a ∈ ((E : Finset (Sym2 W)) : Set (Sym2 W)) := |
| 1233 | Finset.mem_image.mpr ⟨a, Finset.mem_univ _, rfl⟩ |
| 1234 | have hnotDiag : edgeSym a ∉ Sym2.diagSet := |
| 1235 | fun hdiag => hEnd_ne_rootW a hdiag.symm |
| 1236 | simpa [J, SimpleGraph.edgeSet_fromEdgeSet] using ⟨hmemE, hnotDiag⟩ |
| 1237 | let edgeEmb : A → J.edgeSet := fun a => ⟨edgeSym a, hEdge_mem a⟩ |
| 1238 | have hEdgeIndex_injective : Function.Injective edgeEmb := |
| 1239 | fun a b hEq => hEdgeInj (congrArg Subtype.val hEq) |
| 1240 | -- For the model: edge decomposition |
| 1241 | have hEdgeIndexExists : ∀ e : J.edgeSet, ∃ a : A, edgeSym a = (e : Sym2 W) := by |
| 1242 | intro e |
| 1243 | have heE : (e : Sym2 W) ∈ E := by |
| 1244 | have : (e : Sym2 W) ∈ (((E : Finset (Sym2 W)) : Set (Sym2 W)) \ Sym2.diagSet) := by |
| 1245 | simpa [J, SimpleGraph.edgeSet_fromEdgeSet] using e.2 |
| 1246 | exact this.1 |
| 1247 | exact Finset.mem_image.mp heE |>.imp fun a ha => ha.2 |
| 1248 | let edgeIndex : J.edgeSet → A := fun e => Classical.choose (hEdgeIndexExists e) |
| 1249 | have hEdgeIndex_spec : ∀ e : J.edgeSet, edgeSym (edgeIndex e) = (e : Sym2 W) := |
| 1250 | fun e => Classical.choose_spec (hEdgeIndexExists e) |
| 1251 | let edgeTail : J.edgeSet → W := fun e => rootW (edgeIndex e).1 |
| 1252 | have hEdgeTail_mem : ∀ e : J.edgeSet, edgeTail e ∈ (e : Sym2 W) := by |
| 1253 | intro e |
| 1254 | have hmem : edgeTail e ∈ edgeSym (edgeIndex e) := by simp [edgeTail, edgeSym] |
| 1255 | exact (hEdgeIndex_spec e).symm ▸ hmem |
| 1256 | have hEdgeOther : ∀ e : J.edgeSet, Sym2.Mem.other (hEdgeTail_mem e) = endW (edgeIndex e) := by |
| 1257 | intro e |
| 1258 | exact Sym2.congr_right.mp <| |
| 1259 | calc |
| 1260 | s(edgeTail e, Sym2.Mem.other (hEdgeTail_mem e)) = (e : Sym2 W) := |
| 1261 | Sym2.other_spec (hEdgeTail_mem e) |
| 1262 | _ = s(edgeTail e, endW (edgeIndex e)) := by |
| 1263 | simpa [edgeTail, edgeSym] using (hEdgeIndex_spec e).symm |
| 1264 | have hEdgeHead : ∀ e : J.edgeSet, |
| 1265 | hit (edgeIndex e) = ↑(Sym2.Mem.other (hEdgeTail_mem e)) := by |
| 1266 | intro e |
| 1267 | simpa [endW] using congrArg Subtype.val (hEdgeOther e).symm |
| 1268 | -- Build the ShallowTopologicalMinorModel |
| 1269 | let model : ShallowTopologicalMinorModel J G (r - 1) := |
| 1270 | { branchVertex := ⟨Subtype.val, Subtype.coe_injective⟩ |
| 1271 | edgeTail := edgeTail |
| 1272 | edgeTail_mem := hEdgeTail_mem |
| 1273 | edgePath := fun e => (q (edgeIndex e)).copy rfl (hEdgeHead e) |
| 1274 | edgePath_isPath := by |
| 1275 | intro e; simpa [hEdgeHead e] using hqPath (edgeIndex e) |
| 1276 | edgePath_length := by |
| 1277 | intro e |
| 1278 | have hlen : (q (edgeIndex e)).length ≤ r := hqLen (edgeIndex e) |
| 1279 | have hr : 1 ≤ r := hrPos (edgeIndex e) |
| 1280 | calc ((q (edgeIndex e)).copy rfl (hEdgeHead e)).length |
| 1281 | = (q (edgeIndex e)).length := by simp |
| 1282 | _ ≤ r := hlen |
| 1283 | _ ≤ 2 * (r - 1) + 1 := by omega |
| 1284 | edgePath_interior_avoids_branch := by |
| 1285 | intro e x hx htail hhead w |
| 1286 | have hnot : x ∉ U := by |
| 1287 | refine hqSupportAvoid (edgeIndex e) ?_ ?_ ?_ |
| 1288 | · simpa [hEdgeHead e] using hx |
| 1289 | · simpa [edgeTail] using htail |
| 1290 | · simpa [hEdgeHead e] using hhead |
| 1291 | exact fun hEq => hnot (hEq.symm ▸ w.2) |
| 1292 | edgePath_interior_disjoint := by |
| 1293 | intro e e' x hne hx hx' htail hhead htail' hhead' |
| 1294 | let a := edgeIndex e |
| 1295 | let b := edgeIndex e' |
| 1296 | have hab : a ≠ b := by |
| 1297 | intro hEq; apply hne; apply Subtype.ext |
| 1298 | simpa [a, b, hEdgeIndex_spec e, hEdgeIndex_spec e'] using congrArg edgeSym hEq |
| 1299 | by_cases hroot : a.1 = b.1 |
| 1300 | · have hidx : a.2 ≠ b.2 := by |
| 1301 | intro hEq; exact hab (Prod.ext hroot hEq) |
| 1302 | have hxRaw : x ∈ (rawWalk a).support := |
| 1303 | (rawWalk a).support_takeUntil_subset (hHit_mem_support a) |
| 1304 | (by simpa [a, hEdgeHead e] using hx) |
| 1305 | have hxRaw' : x ∈ (rawWalk b).support := |
| 1306 | (rawWalk b).support_takeUntil_subset (hHit_mem_support b) |
| 1307 | (by simpa [b, hEdgeHead e'] using hx') |
| 1308 | have hEqRoot : x = root a.1 := by |
| 1309 | have hSupportEq : (rawPaths a.1 b.2).2.support = (rawPaths b.1 b.2).2.support := |
| 1310 | congrArg (fun v => (rawPaths v b.2).2.support) hroot |
| 1311 | have hxRaw''0 : x ∈ (rawPaths b.1 b.2).2.support := by |
| 1312 | simpa [rawWalk, rawTarget] using hxRaw' |
| 1313 | have hxRaw'' : x ∈ (rawPaths a.1 b.2).2.support := hSupportEq ▸ hxRaw''0 |
| 1314 | exact (rawFamily a.1).disjoint a.2 b.2 hidx x hxRaw hxRaw'' |
| 1315 | exact htail (by simpa [a, edgeTail] using hEqRoot) |
| 1316 | · exact hNoCrossInterior hroot |
| 1317 | (by simpa [a, hEdgeHead e] using hx) |
| 1318 | (by simpa [b, hEdgeHead e'] using hx') |
| 1319 | (by simpa [a, edgeTail] using htail) |
| 1320 | (by simpa [a, hEdgeHead e] using hhead) |
| 1321 | (by simpa [b, edgeTail] using htail') |
| 1322 | (by simpa [b, hEdgeHead e'] using hhead') } |
| 1323 | -- Vertex bound: |W| ≤ |S| + |K| |
| 1324 | have hVertBound : Fintype.card W ≤ Fintype.card S + K.card := by |
| 1325 | have h1 : Fintype.card W ≤ Fintype.card S + |
| 1326 | Fintype.card {x : V // x ∈ (K : Set V)} := by |
| 1327 | convert Fintype.card_subtype_or (fun x : V => x ∈ S) (fun x => x ∈ (K : Set V)) using 1 |
| 1328 | have h2 : Fintype.card {x : V // x ∈ (K : Set V)} = K.card := by |
| 1329 | convert Fintype.card_coe K |
| 1330 | omega |
| 1331 | -- Edge bound: I.card * n ≤ |E(J)| |
| 1332 | -- Pin the Fintype instance for J.edgeSet to match the existential witness |
| 1333 | letI : Fintype J.edgeSet := J.fintypeEdgeSet |
| 1334 | have hEdgeBound : I.card * n ≤ J.edgeFinset.card := by |
| 1335 | have hAcard : I.card * n = (Finset.univ : Finset A).card := by |
| 1336 | simp [Finset.card_univ, A, IV, Fintype.card_coe, Fintype.card_fin] |
| 1337 | have hImage : (Finset.univ.image edgeSym).card = (Finset.univ : Finset A).card := |
| 1338 | Finset.card_image_of_injective _ hEdgeInj |
| 1339 | have hImageSub : Finset.univ.image edgeSym ⊆ J.edgeFinset := by |
| 1340 | intro e he |
| 1341 | rw [Finset.mem_image] at he |
| 1342 | obtain ⟨a, _, rfl⟩ := he |
| 1343 | exact SimpleGraph.mem_edgeFinset.mpr (hEdge_mem a) |
| 1344 | calc I.card * n = (Finset.univ : Finset A).card := hAcard |
| 1345 | _ = (Finset.univ.image edgeSym).card := hImage.symm |
| 1346 | _ ≤ J.edgeFinset.card := Finset.card_le_card hImageSub |
| 1347 | exact ⟨W, inferInstance, inferInstance, J, inferInstance, ⟨model⟩, hVertBound, hEdgeBound⟩ |
| 1348 | |
| 1349 | /-! ### Helper: Phase B arithmetic |
| 1350 | |
| 1351 | The key numerical fact: for d ≥ 1 and r ≥ 1, |
| 1352 | d · (2d+1) · (1 + d · (2r-2)) < 6r · d³ + 1. |
| 1353 | Equivalently: after expanding, the difference equals |
| 1354 | 2d²r(d-1) + 4d³ - d + 1 ≥ 4 > 0. -/ |
| 1355 | |
| 1356 | private theorem phase_b_arith (r d : ℕ) (hr : 1 ≤ r) (hd : 1 ≤ d) : |
| 1357 | d * (2 * d + 1) * (1 + d * (2 * r - 2)) < 6 * r * d ^ 3 + 1 := by |
| 1358 | suffices d * (2 * d + 1) * (1 + d * (2 * r - 2)) ≤ 6 * r * d ^ 3 by omega |
| 1359 | rw [show 2 * r - 2 = 2 * (r - 1) from by omega] |
| 1360 | calc d * (2 * d + 1) * (1 + d * (2 * (r - 1))) |
| 1361 | ≤ d * (3 * d) * (1 + d * (2 * (r - 1))) := |
| 1362 | Nat.mul_le_mul_right _ (Nat.mul_le_mul_left d (by omega)) |
| 1363 | _ = 3 * d ^ 2 * (1 + 2 * d * (r - 1)) := by ring |
| 1364 | _ ≤ 3 * d ^ 2 * (2 * d * r) := |
| 1365 | Nat.mul_le_mul_left _ (by |
| 1366 | calc 1 + 2 * d * (r - 1) |
| 1367 | ≤ 2 * d + 2 * d * (r - 1) := by omega |
| 1368 | _ = 2 * d * (1 + (r - 1)) := by ring |
| 1369 | _ = 2 * d * r := by congr 1; omega) |
| 1370 | _ = 6 * r * d ^ 3 := by ring |
| 1371 | |
| 1372 | /-! ### Main Phase B theorem -/ |
| 1373 | |
| 1374 | private theorem exists_bounded_subsetAdm_vertex |
| 1375 | {V : Type} [DecidableEq V] [Fintype V] |
| 1376 | (G : SimpleGraph V) (r d : ℕ) |
| 1377 | (hd : ∀ {W : Type} [DecidableEq W] [Fintype W] |
| 1378 | (H : SimpleGraph W) [DecidableRel H.Adj], |
| 1379 | IsShallowTopologicalMinor H G (r - 1) → |
| 1380 | H.edgeFinset.card ≤ d * Fintype.card W) : |
| 1381 | ∀ S : Set V, S.Nonempty → |
| 1382 | ∃ v ∈ S, subsetAdmValue G r S v ≤ 6 * r * d ^ 3 := by |
| 1383 | intro S hS |
| 1384 | -- r = 0: subsetAdmValue = 0 ≤ 0 |
| 1385 | by_cases hr0 : r = 0 |
| 1386 | · obtain ⟨v, hv⟩ := hS |
| 1387 | exact ⟨v, hv, by simp [hr0, subsetAdmValue_eq_zero_of_r_eq_zero]⟩ |
| 1388 | -- Assume for contradiction that every vertex has large subsetAdmValue |
| 1389 | by_contra hContra |
| 1390 | push_neg at hContra |
| 1391 | -- hContra : ∀ v ∈ S, 6 * r * d ^ 3 < subsetAdmValue G r S v |
| 1392 | haveI : Fintype S := Set.Finite.fintype (Set.toFinite S) |
| 1393 | haveI : Nonempty S := Set.nonempty_coe_sort.mpr hS |
| 1394 | have hrd : 1 ≤ r := Nat.pos_of_ne_zero hr0 |
| 1395 | -- Build maximal connector and extract independent set |
| 1396 | obtain ⟨K, I, hKbound, hIcard, hNoCross⟩ := |
| 1397 | exists_connector_and_indepset G r d S hd |
| 1398 | -- S is nonempty → |S| ≥ 1 → |I| ≥ 1 |
| 1399 | have hScard : 0 < Fintype.card S := Fintype.card_pos |
| 1400 | have hIpos : 0 < I.card := by |
| 1401 | rcases Nat.eq_zero_or_pos I.card with h0 | h0 |
| 1402 | · simp [h0] at hIcard |
| 1403 | · exact h0 |
| 1404 | -- Everyone has subsetAdmValue ≥ ℓ + 1 |
| 1405 | set ℓ := 6 * r * d ^ 3 with hℓ_def |
| 1406 | have hLarge : ∀ v ∈ S, ℓ + 1 ≤ subsetAdmValue G r S v := |
| 1407 | fun v hv => hContra v hv |
| 1408 | -- Build dense minor J |
| 1409 | obtain ⟨W', instW'Dec, instW'Fin, J, instJDec, hJminor, hJverts, hJedges⟩ := |
| 1410 | exists_dense_shallow_minor G r S (ℓ + 1) (by omega) hLarge K I hNoCross |
| 1411 | -- Install instances for W' and J |
| 1412 | letI : DecidableEq W' := instW'Dec |
| 1413 | letI : Fintype W' := instW'Fin |
| 1414 | letI : DecidableRel J.Adj := instJDec |
| 1415 | -- Apply density hypothesis to J |
| 1416 | have hJdensity : J.edgeFinset.card ≤ d * Fintype.card W' := hd J hJminor |
| 1417 | -- Chain: I.card * (ℓ+1) ≤ |E(J)| ≤ d * |V(J)| ≤ d * (|S| + |K|) |
| 1418 | have h1 : I.card * (ℓ + 1) ≤ d * (Fintype.card S + K.card) := |
| 1419 | calc I.card * (ℓ + 1) |
| 1420 | ≤ J.edgeFinset.card := hJedges |
| 1421 | _ ≤ d * Fintype.card W' := hJdensity |
| 1422 | _ ≤ d * (Fintype.card S + K.card) := Nat.mul_le_mul_left d hJverts |
| 1423 | -- Step-by-step to d * (2d+1) * (1 + d*(2r-2)) * I.card |
| 1424 | have h2 : d * (Fintype.card S + K.card) ≤ |
| 1425 | d * (Fintype.card S + d * Fintype.card S * (2 * r - 2)) := |
| 1426 | Nat.mul_le_mul_left d (Nat.add_le_add_left hKbound _) |
| 1427 | have h3 : d * (Fintype.card S + d * Fintype.card S * (2 * r - 2)) ≤ |
| 1428 | d * (I.card * (2 * d + 1) + d * (I.card * (2 * d + 1)) * (2 * r - 2)) := |
| 1429 | Nat.mul_le_mul_left d (Nat.add_le_add |
| 1430 | hIcard (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left d hIcard))) |
| 1431 | have h4 : d * (I.card * (2 * d + 1) + d * (I.card * (2 * d + 1)) * (2 * r - 2)) = |
| 1432 | d * (2 * d + 1) * (1 + d * (2 * r - 2)) * I.card := by |
| 1433 | generalize 2 * r - 2 = m; ring |
| 1434 | -- Combine and cancel I.card |
| 1435 | have h_chain : I.card * (ℓ + 1) ≤ |
| 1436 | d * (2 * d + 1) * (1 + d * (2 * r - 2)) * I.card := |
| 1437 | calc I.card * (ℓ + 1) |
| 1438 | ≤ d * (Fintype.card S + K.card) := h1 |
| 1439 | _ ≤ d * (Fintype.card S + d * Fintype.card S * (2 * r - 2)) := h2 |
| 1440 | _ ≤ d * (I.card * (2 * d + 1) + d * (I.card * (2 * d + 1)) * (2 * r - 2)) := h3 |
| 1441 | _ = d * (2 * d + 1) * (1 + d * (2 * r - 2)) * I.card := h4 |
| 1442 | have h_cancel : ℓ + 1 ≤ d * (2 * d + 1) * (1 + d * (2 * r - 2)) := by |
| 1443 | rw [show I.card * (ℓ + 1) = (ℓ + 1) * I.card from Nat.mul_comm ..] at h_chain |
| 1444 | exact Nat.le_of_mul_le_mul_right h_chain hIpos |
| 1445 | -- d = 0: ℓ + 1 = 1 > 0 = RHS, immediate contradiction |
| 1446 | by_cases hd0 : d = 0 |
| 1447 | · simp [hd0] at h_cancel |
| 1448 | -- d ≥ 1, r ≥ 1: use phase_b_arith for contradiction |
| 1449 | · exact Nat.lt_irrefl _ |
| 1450 | (lt_of_lt_of_le (phase_b_arith r d hrd (Nat.pos_of_ne_zero hd0)) h_cancel) |
| 1451 | |
| 1452 | /-! ## Main theorem -/ |
| 1453 | |
| 1454 | /-- Lemma 3.2/ch2: adm_r(G) ≤ 1 + 6r · d³ via a greedy ordering. -/ |
| 1455 | theorem adm_le_of_topGrad_bound |
| 1456 | {V : Type} [DecidableEq V] [Fintype V] |
| 1457 | (G : SimpleGraph V) (r d : ℕ) |
| 1458 | (hd : ∀ {W : Type} [DecidableEq W] [Fintype W] |
| 1459 | (H : SimpleGraph W) [DecidableRel H.Adj], |
| 1460 | IsShallowTopologicalMinor H G (r - 1) → |
| 1461 | H.edgeFinset.card ≤ d * Fintype.card W) : |
| 1462 | ∃ (ord : LinearOrder V), |
| 1463 | letI := ord; adm G r ≤ 1 + 6 * r * d ^ 3 := by |
| 1464 | exact exists_order_adm_le_of_subsetAdmBound G r |
| 1465 | (exists_bounded_subsetAdm_vertex G r d hd) |
| 1466 | |
| 1467 | end |
| 1468 | |
| 1469 | end Catalog.Sparsity.AdmBoundByTopGrad |
| 1470 |