Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/EvenStepReduction/Full.lean
1import Catalog.Sparsity.ShallowMinor.Full
2import Catalog.Sparsity.UniformQuasiWideness.Full
3
4namespace Catalog.Sparsity.EvenStepReduction
5
6open Catalog.Sparsity.ShallowMinor Catalog.Sparsity.UniformQuasiWideness
7
8-- ── Helpers ─────────────────────────────────────────────────────────────
9
10private def jBall {V : Type} (G : SimpleGraph V) (j : ℕ) (v : V) : Set V :=
11 {u : V | ∃ p : G.Walk v u, p.length ≤ j}
12
13private lemma mem_jBall_self {V : Type} (G : SimpleGraph V) (j : ℕ) (v : V) :
14 v ∈ jBall G j v :=
15 ⟨.nil, Nat.zero_le _⟩
16
17private lemma jBall_disjoint {V : Type} {G : SimpleGraph V} [DecidableEq V] {j : ℕ}
18 {A : Set V} (hA : DistIndependent G (2 * j) A) {a b : V} (ha : a ∈ A) (hb : b ∈ A)
19 (hab : a ≠ b) : Disjoint (jBall G j a) (jBall G j b) :=
20 Set.disjoint_left.mpr fun u ⟨pa, hpa⟩ ⟨pb, hpb⟩ =>
21 absurd (show (pa.append pb.reverse).length ≤ 2 * j by
22 rw [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_reverse]; omega)
23 (Nat.not_le.mpr (hA ha hb hab _))
24
25private lemma walk_crossing_edge {V : Type} {G : SimpleGraph V} [DecidableEq V]
26 {u v : V} (p : G.Walk u v) (j : ℕ) (hj : j + 1 ≤ p.length) :
27 ∃ c d : V, G.Adj c d ∧
28 (∃ q₁ : G.Walk u c, q₁.length ≤ j) ∧
29 (∃ q₂ : G.Walk d v, q₂.length + j + 1 ≤ p.length) := by
30 induction p generalizing j with
31 | nil => simp [SimpleGraph.Walk.length_nil] at hj
32 | cons h p' ih =>
33 match j with
34 | 0 =>
35 exact ⟨_, _, h, ⟨.nil, le_refl 0⟩,
36 ⟨p', by simp [SimpleGraph.Walk.length_cons]⟩⟩
37 | j + 1 =>
38 have hj' : j + 1 ≤ p'.length := by
39 simp [SimpleGraph.Walk.length_cons] at hj; omega
40 obtain ⟨c, d, hadj, ⟨q₁, hq₁⟩, ⟨q₂, hq₂⟩⟩ := ih j hj'
41 exact ⟨c, d, hadj,
42 ⟨.cons h q₁, by simp [SimpleGraph.Walk.length_cons]; omega⟩,
43 ⟨q₂, by simp [SimpleGraph.Walk.length_cons]; omega⟩⟩
44
45/-- Map a walk in `deleteVerts G S` to a walk in `G` of the same length. -/
46private def toGWalk {V : Type} {G : SimpleGraph V} {S : Set V}
47 {u v : V} (p : (deleteVerts G S).Walk u v) : G.Walk u v :=
48 p.map { toFun := id, map_rel' := fun {_ _} h => And.left h }
49
50@[simp] private lemma toGWalk_length {V : Type} {G : SimpleGraph V} {S : Set V}
51 {u v : V} (p : (deleteVerts G S).Walk u v) : (toGWalk p).length = p.length :=
52 SimpleGraph.Walk.length_map _ _
53
54-- ── Main theorem ────────────────────────────────────────────────────────
55
56theorem evenStepReduction {V : Type} [DecidableEq V] [Fintype V]
57 (G : SimpleGraph V) (j : ℕ) (A : Finset V)
58 (hA : DistIndependent G (2 * j + 1) ↑A) :
59 ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (H : SimpleGraph W)
60 (AW : Finset W),
61 IsShallowMinor H G j ∧
62 A.card ≤ AW.card ∧
63 (↑AW : Set W).Pairwise (fun u v => ¬H.Adj u v) ∧
64 (∀ (S : Finset W) (m : ℕ),
65 Disjoint S AW →
66 (∃ B : Finset W, B ⊆ AW ∧ m ≤ B.card ∧
67 DistIndependent (deleteVerts H ↑S) 2 ↑B) →
68 ∃ (S' : Finset V) (B' : Finset V),
69 S'.card ≤ S.card ∧ ↑B' ⊆ ↑A ∧ Disjoint B' S' ∧ m ≤ B'.card ∧
70 DistIndependent (deleteVerts G ↑S') (2 * (j + 1)) ↑B') := by
71 classical
72 have hA2j : DistIndependent G (2 * j) ↑A :=
73 fun a ha b hb hab p => Nat.lt_of_le_of_lt (by omega) (hA ha hb hab p)
74 set W := {v : V // v ∈ A ∨ ∀ a ∈ A, v ∉ jBall G j a} with hW_def
75 let branchOf : W → Set V := fun w =>
76 if w.val ∈ A then jBall G j w.val else {w.val}
77 let H : SimpleGraph W :=
78 { Adj := fun w₁ w₂ => w₁ ≠ w₂ ∧
79 ∃ x ∈ branchOf w₁, ∃ y ∈ branchOf w₂, G.Adj x y
80 symm := fun _ _ ⟨hne, x, hx, y, hy, hadj⟩ =>
81 ⟨hne.symm, y, hy, x, hx, hadj.symm⟩
82 loopless := ⟨fun w h => h.1 rfl⟩ }
83 let aEmb : {v // v ∈ A} ↪ W :=
84 { toFun := fun ⟨v, hv⟩ => ⟨v, Or.inl hv⟩
85 inj' := fun a b h => Subtype.ext (congrArg (fun w : W => w.val) h) }
86 set AW := Finset.univ.map aEmb with hAW_def
87 have hAW_mem : ∀ w ∈ AW, w.val ∈ A := by
88 intro w hw; obtain ⟨⟨v, hv⟩, _, rfl⟩ := Finset.mem_map.mp hw; exact hv
89 have hA_to_AW : ∀ (a : V) (ha : a ∈ A), (⟨a, Or.inl ha⟩ : W) ∈ AW := by
90 intro a ha; exact Finset.mem_map.mpr ⟨⟨a, ha⟩, Finset.mem_univ _, rfl⟩
91 have hOut : ∀ w : W, w.val ∉ A → ∀ a ∈ A, w.val ∉ jBall G j a := by
92 intro w hw; rcases w.prop with h | h; exact absurd h hw; exact h
93 have hBrA : ∀ w : W, w.val ∈ A → branchOf w = jBall G j w.val :=
94 fun _ h => if_pos h
95 have hBrOut : ∀ w : W, w.val ∉ A → branchOf w = {w.val} :=
96 fun _ h => if_neg h
97 refine ⟨W, inferInstance, inferInstance, H, AW, ?_, ?_, ?_, ?_⟩
98 -- ── (1) IsShallowMinor H G j ──
99 · refine ⟨⟨branchOf, fun w => w.val, fun w => ?_, fun u v huv => ?_,
100 fun w x hx => ?_, fun u v hadj => hadj.2⟩⟩
101 · -- center_mem
102 by_cases hw : w.val ∈ A
103 · rw [hBrA w hw]; exact mem_jBall_self G j w.val
104 · simp only [hBrOut w hw, Set.mem_singleton_iff]
105 · -- branchDisjoint
106 by_cases hu : u.val ∈ A <;> by_cases hv : v.val ∈ A
107 · rw [hBrA u hu, hBrA v hv]
108 exact jBall_disjoint hA2j hu hv (Subtype.val_injective.ne huv)
109 · rw [hBrA u hu, hBrOut v hv]
110 exact Set.disjoint_left.mpr fun x hx (hxv : x = v.val) =>
111 hOut v hv u.val hu (hxv ▸ hx)
112 · rw [hBrOut u hu, hBrA v hv]
113 exact Set.disjoint_left.mpr fun x (hx : x = u.val) hxv =>
114 hOut u hu v.val hv (hx ▸ hxv)
115 · rw [hBrOut u hu, hBrOut v hv]
116 exact Set.disjoint_left.mpr fun x (hx : x = u.val) (hxv : x = v.val) =>
117 huv (Subtype.ext (hx.symm.trans hxv))
118 · -- branchRadius
119 by_cases hw : w.val ∈ A
120 · rw [hBrA w hw] at hx ⊢
121 obtain ⟨q, hq⟩ := hx
122 exact ⟨q.bypass, q.bypass_isPath, q.length_bypass_le.trans hq,
123 fun z hz => ⟨q.takeUntil z (q.support_bypass_subset hz),
124 (q.length_takeUntil_le (q.support_bypass_subset hz)).trans hq⟩⟩
125 · rw [hBrOut w hw] at hx ⊢
126 subst hx
127 exact ⟨.nil, SimpleGraph.Walk.IsPath.nil, Nat.zero_le _,
128 fun z hz => by
129 simp [SimpleGraph.Walk.support_nil] at hz; exact hz⟩
130 -- ── (2) A.card ≤ AW.card ──
131 · rw [hAW_def, Finset.card_map, Finset.card_univ, Fintype.card_coe]
132 -- ── (3) AW is independent in H ──
133 · intro wa hwa wb hwb hwne hadj
134 obtain ⟨_, x, hx, y, hy, hxy⟩ := hadj
135 have hwa_A := hAW_mem wa hwa; have hwb_A := hAW_mem wb hwb
136 rw [hBrA wa hwa_A] at hx; rw [hBrA wb hwb_A] at hy
137 obtain ⟨px, hpx⟩ := hx; obtain ⟨py, hpy⟩ := hy
138 exact absurd (show (px.append (.cons hxy py.reverse)).length ≤ 2 * j + 1 by
139 rw [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons,
140 SimpleGraph.Walk.length_reverse]; omega)
141 (Nat.not_le.mpr (hA hwa_A hwb_A (Subtype.val_injective.ne hwne) _))
142 -- ── (4) Lifting property ──
143 · intro S m hDisj ⟨B, hBsub, hmB, hBind⟩
144 let valEmb : W ↪ V := ⟨Subtype.val, Subtype.val_injective⟩
145 refine ⟨S.map valEmb, B.map valEmb, ?_, ?_, ?_, ?_, ?_⟩
146 · rw [Finset.card_map]
147 · intro v hv
148 obtain ⟨w, hw, rfl⟩ := Finset.mem_map.mp hv
149 exact hAW_mem w (hBsub hw)
150 · rw [Finset.disjoint_left]; intro v hv hv'
151 obtain ⟨w, hw, rfl⟩ := Finset.mem_map.mp hv
152 obtain ⟨w', hw', heq⟩ := Finset.mem_map.mp hv'
153 have := Subtype.val_injective heq; subst this
154 exact Finset.disjoint_right.mp hDisj (hBsub hw) hw'
155 · rw [Finset.card_map]; exact hmB
156 · intro a ha b hb hab
157 simp only [Finset.coe_map, Set.mem_image] at ha hb
158 obtain ⟨wa, hwa_mem, rfl⟩ := ha
159 obtain ⟨wb, hwb_mem, rfl⟩ := hb
160 have hwne : wa ≠ wb := fun h => hab (congrArg Subtype.val h)
161 have hwa_A := hAW_mem wa (hBsub hwa_mem)
162 have hwb_A := hAW_mem wb (hBsub hwb_mem)
163 have hwa_nS : wa ∉ (S : Set W) :=
164 fun h => Finset.disjoint_right.mp hDisj (hBsub hwa_mem) h
165 have hwb_nS : wb ∉ (S : Set W) :=
166 fun h => Finset.disjoint_right.mp hDisj (hBsub hwb_mem) h
167 set S' := S.map valEmb
168 intro p
169 by_contra hle; push_neg at hle
170 -- Lower bound from hA
171 have hp_lb : 2 * j + 2 ≤ p.length := by
172 have := hA hwa_A hwb_A (Subtype.val_injective.ne hwne) (toGWalk p)
173 simp at this; omega
174 -- Apply walk_crossing_edge to p (deleteVerts walk) at depth j
175 obtain ⟨c, d, hadj_del, ⟨q₁, hq₁⟩, ⟨q₂, hq₂⟩⟩ :=
176 walk_crossing_edge p j (by omega : j + 1 ≤ p.length)
177 have hadj_cd : G.Adj c d := hadj_del.1
178 have hd_nS' : d ∉ (↑S' : Set V) := hadj_del.2.2
179 have hc_ball : c ∈ jBall G j wa.val :=
180 ⟨toGWalk q₁, by simp; exact hq₁⟩
181 have hq₂_le : q₂.length ≤ j + 1 := by omega
182 by_cases hq₂j : q₂.length ≤ j
183 · -- Case 1: d ∈ jBall(wb, j) → length-1 H-walk → contradiction
184 have hd_ball : d ∈ jBall G j wb.val :=
185 ⟨(toGWalk q₂).reverse, by simp; exact hq₂j⟩
186 have hH_adj : H.Adj wa wb :=
187 ⟨hwne,
188 c, show c ∈ branchOf wa by rw [hBrA wa hwa_A]; exact hc_ball,
189 d, show d ∈ branchOf wb by rw [hBrA wb hwb_A]; exact hd_ball,
190 hadj_cd⟩
191 exact absurd (hBind (Finset.mem_coe.mpr hwa_mem) (Finset.mem_coe.mpr hwb_mem)
192 hwne (.cons (show (deleteVerts H ↑S).Adj wa wb from ⟨hH_adj, hwa_nS, hwb_nS⟩) .nil))
193 (by simp [SimpleGraph.Walk.length_cons, SimpleGraph.Walk.length_nil])
194 · -- Case 2: q₂.length = j+1 → d outside all jBalls → H-path wa-wd-wb
195 push_neg at hq₂j
196 have hq₂_eq : q₂.length = j + 1 := by omega
197 have hd_outside : ∀ a' ∈ A, d ∉ jBall G j a' := by
198 intro a' ha' ⟨pd, hpd⟩
199 by_cases haa : wa.val = a'
200 · -- d ∈ jBall(wa.val, j). Walk wa.val→d (pd), d→wb.val (q₂). Total ≤ 2j+1.
201 subst haa
202 have := hA hwa_A hwb_A (Subtype.val_injective.ne hwne)
203 (pd.append (toGWalk q₂))
204 simp [SimpleGraph.Walk.length_append] at this; omega
205 · -- Walk wa.val→c (q₁), edge c→d, walk d→a' (pd.reverse). Total ≤ 2j+1.
206 have := hA hwa_A ha' haa
207 ((toGWalk q₁).append (.cons hadj_cd pd.reverse))
208 simp [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons,
209 SimpleGraph.Walk.length_reverse] at this; omega
210 have hd_notA : d ∉ A := fun hd => hd_outside d hd (mem_jBall_self G j d)
211 let wd : W := ⟨d, Or.inr hd_outside⟩
212 have hwd_nS : wd ∉ (S : Set W) := by
213 intro hs
214 exact hd_nS' (Finset.mem_coe.mpr
215 (Finset.mem_map.mpr ⟨wd, Finset.mem_coe.mp hs, rfl⟩))
216 have hH_wa_wd : H.Adj wa wd := by
217 refine ⟨fun h => ?_, c, ?_, d, ?_, hadj_cd⟩
218 · subst h; exact hd_notA hwa_A
219 · rw [hBrA wa hwa_A]; exact hc_ball
220 · simp only [hBrOut wd hd_notA, Set.mem_singleton_iff]; rfl
221 have hH_wd_wb : H.Adj wd wb := by
222 refine ⟨fun h => ?_, d, ?_, ?_⟩
223 · subst h; exact hd_notA hwb_A
224 · simp only [hBrOut wd hd_notA, Set.mem_singleton_iff]; rfl
225 · -- q₂ has length j+1 ≥ 1, extract first step
226 match q₂, hq₂_eq with
227 | .cons hedge q₂', hlen =>
228 refine ⟨_, ?_, hedge.left⟩
229 rw [hBrA wb hwb_A]
230 exact ⟨(toGWalk q₂').reverse, by
231 simp [SimpleGraph.Walk.length_cons] at hlen; simp; omega⟩
232 -- length-2 walk wa → wd → wb in deleteVerts H ↑S → contradiction
233 exact absurd (hBind (Finset.mem_coe.mpr hwa_mem) (Finset.mem_coe.mpr hwb_mem)
234 hwne (.cons ⟨hH_wa_wd, hwa_nS, hwd_nS⟩ (.cons ⟨hH_wd_wb, hwd_nS, hwb_nS⟩ .nil)))
235 (by simp [SimpleGraph.Walk.length_cons])
236
237end Catalog.Sparsity.EvenStepReduction
238