Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/UQWImpliesND/Full.lean
1import Catalog.Sparsity.Preliminaries.Full
2import Catalog.Sparsity.UniformQuasiWideness.Full
3import Catalog.Sparsity.NowhereDense.Full
4import Catalog.Sparsity.ShallowMinor.Full
5import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
6import Mathlib.Combinatorics.SimpleGraph.Walk.Operations
7import Mathlib.Data.Finset.Image
8import Mathlib.Data.Finset.Card
9
10namespace Catalog.Sparsity.UQWImpliesND
11
12open Catalog.Sparsity.Preliminaries Catalog.Sparsity.NowhereDense Catalog.Sparsity.UniformQuasiWideness
13open Catalog.Sparsity.ShallowMinor
14
15/-- Transfer a G-walk to (deleteVerts G S) when all support vertices avoid S. -/
16private lemma walk_to_deleteVerts {V : Type} {G : SimpleGraph V} {S : Set V}
17 {u v : V} (p : G.Walk u v) (h : ∀ w ∈ p.support, w ∉ S) :
18 ∃ q : (deleteVerts G S).Walk u v, q.length = p.length := by
19 induction p with
20 | nil => exact ⟨.nil, rfl⟩
21 | cons hadj tail ih =>
22 have htail : ∀ w ∈ tail.support, w ∉ S := by
23 intro w hw; apply h; rw [SimpleGraph.Walk.support_cons]
24 exact List.mem_cons_of_mem _ hw
25 have hstart := h _ (SimpleGraph.Walk.start_mem_support _)
26 have hnext := htail _ (SimpleGraph.Walk.start_mem_support _)
27 obtain ⟨q, hq⟩ := ih htail
28 exact ⟨.cons ⟨hadj, hstart, hnext⟩ q, by
29 rw [SimpleGraph.Walk.length_cons, SimpleGraph.Walk.length_cons, hq]⟩
30
31/-- Lemma 3.3: if a class `C` is uniformly quasi-wide, then `C` is nowhere
32 dense. -/
33theorem uqw_implies_nd (C : GraphClass) :
34 UniformlyQuasiWide C → IsNowhereDense C := by
35 classical
36 intro hUQW d
37 obtain ⟨N, s, hN⟩ := hUQW (2 * d + 1)
38 use N (s + 2)
39 intro V _ _ G hG
40 unfold IsShallowMinor; intro ⟨M⟩
41 set n := N (s + 2) + 1
42 -- Centers are injective (from branch disjointness)
43 have hM_inj : Function.Injective M.center := by
44 intro i j hij; by_contra h
45 exact Set.disjoint_left.mp (M.branchDisjoint i j h) (M.center_mem i) (hij ▸ M.center_mem j)
46 -- Build A = image of centers, |A| ≥ N(s+2)
47 set A := Finset.univ.image M.center with hA_def
48 have hA_card : N (s + 2) ≤ A.card := by
49 rw [Finset.card_image_of_injective _ hM_inj]; simp [n]
50 -- Apply UQW
51 obtain ⟨S, B, hS_card, hB_sub, hB_card, hB_indep⟩ := hN (s + 2) G hG A hA_card
52 -- B ⊆ A (from hB_sub : ↑B ⊆ ↑A \ ↑S)
53 have hB_in_A : ∀ b ∈ B, b ∈ A := by
54 intro b hb
55 exact (Finset.mem_sdiff.mp (Finset.mem_coe.mp (hB_sub (Finset.mem_coe.mpr hb)))).1
56 -- B_pre: preimage indices of B under M.center
57 set B_pre := Finset.univ.filter (fun i : Fin n => M.center i ∈ B)
58 -- B_pre.image M.center = B
59 have hB_img : B_pre.image M.center = B := by
60 ext b; constructor
61 · intro hb
62 obtain ⟨i, hi, heq⟩ := Finset.mem_image.mp hb
63 exact heq ▸ (Finset.mem_filter.mp hi).2
64 · intro hb
65 obtain ⟨i, _, heq⟩ := Finset.mem_image.mp (hB_in_A _ hb)
66 exact Finset.mem_image.mpr ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ _, heq ▸ hb⟩, heq⟩
67 -- |B_pre| = |B| ≥ s+2
68 have hB_pre_card : s + 2 ≤ B_pre.card := by
69 calc s + 2 ≤ B.card := hB_card
70 _ = (B_pre.image M.center).card := by rw [hB_img]
71 _ = B_pre.card := Finset.card_image_of_injective _ hM_inj
72 -- dirty: indices in B_pre whose branch set intersects S
73 set dirty := B_pre.filter (fun i => ∃ v ∈ S, v ∈ M.branchSet i)
74 -- |dirty| ≤ |S| ≤ s via injection to S
75 have hdirty_card : dirty.card ≤ s := by
76 suffices dirty.card ≤ S.card from le_trans this hS_card
77 let wit : Fin n → V := fun i =>
78 if h : ∃ v ∈ S, v ∈ M.branchSet i then h.choose else M.center i
79 apply Finset.card_le_card_of_injOn wit
80 · intro i hi
81 have hd := (Finset.mem_filter.mp hi).2
82 simp only [wit, dif_pos hd]; exact hd.choose_spec.1
83 · intro i hi j hj hij
84 have hdi := (Finset.mem_filter.mp (Finset.mem_coe.mp hi)).2
85 have hdj := (Finset.mem_filter.mp (Finset.mem_coe.mp hj)).2
86 simp only [wit, dif_pos hdi, dif_pos hdj] at hij
87 by_contra h
88 exact Set.disjoint_left.mp (M.branchDisjoint i j h)
89 hdi.choose_spec.2 (hij ▸ hdj.choose_spec.2)
90 -- clean = B_pre \ dirty has ≥ 2 elements
91 set clean := B_pre \ dirty
92 have hclean_card : 2 ≤ clean.card := by
93 have h_add : clean.card + dirty.card = B_pre.card :=
94 Finset.card_sdiff_add_card_eq_card (Finset.filter_subset _ _)
95 omega
96 -- Pick two distinct clean indices
97 obtain ⟨i, hi, j, hj, hij⟩ := Finset.one_lt_card.mp (by omega : 1 < clean.card)
98 -- Extract properties of clean indices
99 have hi_bpre := Finset.sdiff_subset hi
100 have hj_bpre := Finset.sdiff_subset hj
101 have hi_B : M.center i ∈ B := (Finset.mem_filter.mp hi_bpre).2
102 have hj_B : M.center j ∈ B := (Finset.mem_filter.mp hj_bpre).2
103 have hi_clean : ∀ v ∈ M.branchSet i, v ∉ (↑S : Set V) := by
104 intro v hv hvS
105 exact (Finset.mem_sdiff.mp hi).2
106 (Finset.mem_filter.mpr ⟨hi_bpre, v, Finset.mem_coe.mp hvS, hv⟩)
107 have hj_clean : ∀ v ∈ M.branchSet j, v ∉ (↑S : Set V) := by
108 intro v hv hvS
109 exact (Finset.mem_sdiff.mp hj).2
110 (Finset.mem_filter.mpr ⟨hj_bpre, v, Finset.mem_coe.mp hvS, hv⟩)
111 -- Walk construction via minor model
112 obtain ⟨x, hxi, y, hyj, hadj⟩ := M.branchEdge i j hij
113 obtain ⟨p1, _, hp1_len, hp1_supp⟩ := M.branchRadius i x hxi
114 obtain ⟨p2, _, hp2_len, hp2_supp⟩ := M.branchRadius j y hyj
115 -- Transfer p1 to deleteVerts (all support in branchSet(i), clean)
116 obtain ⟨p1d, hp1d_len⟩ := walk_to_deleteVerts p1
117 (fun v hv => hi_clean v (hp1_supp v hv))
118 -- Transfer p2.reverse to deleteVerts (all support in branchSet(j), clean)
119 obtain ⟨p2rd, hp2rd_len⟩ := walk_to_deleteVerts p2.reverse (by
120 intro v hv; rw [SimpleGraph.Walk.support_reverse, List.mem_reverse] at hv
121 exact hj_clean v (hp2_supp v hv))
122 -- Single edge x → y in deleteVerts
123 have hadj_del : (deleteVerts G ↑S).Adj x y :=
124 ⟨hadj, hi_clean x hxi, hj_clean y hyj⟩
125 -- Compose: center(i) →[p1d] x →[hadj_del] y →[p2rd] center(j)
126 set walk_del := p1d.append (.cons hadj_del p2rd)
127 have hwalk_del_len : walk_del.length ≤ 2 * d + 1 := by
128 simp only [walk_del, SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons]
129 rw [hp1d_len, hp2rd_len, SimpleGraph.Walk.length_reverse]; omega
130 -- Contradiction: hB_indep requires walk length > 2d+1 for distinct B-members
131 have hci_ne_cj : M.center i ≠ M.center j := fun h => hij (hM_inj h)
132 exact Nat.not_lt.mpr hwalk_del_len
133 (hB_indep (Finset.mem_coe.mpr hi_B) (Finset.mem_coe.mpr hj_B) hci_ne_cj walk_del)
134
135end Catalog.Sparsity.UQWImpliesND
136