Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/OddStepReduction/Full.lean
1import Catalog.Sparsity.ShallowMinor.Full
2import Catalog.Sparsity.UniformQuasiWideness.Full
3
4namespace Catalog.Sparsity.OddStepReduction
5
6open Catalog.Sparsity.ShallowMinor Catalog.Sparsity.UniformQuasiWideness
7
8/-- The j-ball of `v` in `G`: vertices reachable by a walk of length ≤ j. -/
9private def jBall {V : Type} (G : SimpleGraph V) (j : ℕ) (v : V) : Set V :=
10 {u : V | ∃ p : G.Walk v u, p.length ≤ j}
11
12private lemma mem_jBall_self {V : Type} (G : SimpleGraph V) (j : ℕ) (v : V) :
13 v ∈ jBall G j v :=
14 ⟨.nil, Nat.zero_le _⟩
15
16private lemma jBall_disjoint {V : Type} {G : SimpleGraph V} [DecidableEq V] {j : ℕ}
17 {A : Set V} (hA : DistIndependent G (2 * j) A) {a b : V} (ha : a ∈ A) (hb : b ∈ A)
18 (hab : a ≠ b) : Disjoint (jBall G j a) (jBall G j b) :=
19 Set.disjoint_left.mpr fun u ⟨pa, hpa⟩ ⟨pb, hpb⟩ =>
20 absurd (show (pa.append pb.reverse).length ≤ 2 * j by
21 rw [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_reverse]; omega)
22 (Nat.not_le.mpr (hA ha hb hab _))
23
24/-- In a walk of length ≥ j+1, there is an edge at depth j: vertices c, d with
25 G.Adj c d, a walk from start to c of length ≤ j, and a walk from d to end
26 of length ≤ p.length − j − 1. -/
27private lemma walk_crossing_edge {V : Type} {G : SimpleGraph V} [DecidableEq V]
28 {u v : V} (p : G.Walk u v) (j : ℕ) (hj : j + 1 ≤ p.length) :
29 ∃ c d : V, G.Adj c d ∧
30 (∃ q₁ : G.Walk u c, q₁.length ≤ j) ∧
31 (∃ q₂ : G.Walk d v, q₂.length + j + 1 ≤ p.length) := by
32 induction p generalizing j with
33 | nil => simp [SimpleGraph.Walk.length_nil] at hj
34 | cons h p' ih =>
35 match j with
36 | 0 =>
37 exact ⟨_, _, h, ⟨.nil, le_refl 0⟩,
38 ⟨p', by simp [SimpleGraph.Walk.length_cons]⟩⟩
39 | j + 1 =>
40 have hj' : j + 1 ≤ p'.length := by
41 simp [SimpleGraph.Walk.length_cons] at hj; omega
42 obtain ⟨c, d, hadj, ⟨q₁, hq₁⟩, ⟨q₂, hq₂⟩⟩ := ih j hj'
43 exact ⟨c, d, hadj,
44 ⟨.cons h q₁, by simp [SimpleGraph.Walk.length_cons]; omega⟩,
45 ⟨q₂, by simp [SimpleGraph.Walk.length_cons]; omega⟩⟩
46
47/-- Lemma 3.5 (consequence form): given a distance-`2j` independent set `A` in
48 `G`, there exists a depth-`j` minor `H` of `G` such that any independent
49 set of size `m` in `H` lifts to a distance-`(2j+1)` independent subset of
50 `A` of the same size.
51
52 The full statement is an iff (distance-`(2j+1)` independence in `G` ↔
53 distance-`1` independence in `H`), but the consequence form suffices for
54 the densification argument. -/
55theorem oddStepReduction {V : Type} [DecidableEq V] [Fintype V]
56 (G : SimpleGraph V) (j : ℕ) (A : Finset V)
57 (hA : DistIndependent G (2 * j) ↑A) :
58 ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (H : SimpleGraph W),
59 IsShallowMinor H G j ∧
60 A.card ≤ Fintype.card W ∧
61 (∀ m : ℕ, (∃ B : Finset W, m ≤ B.card ∧ DistIndependent H 1 ↑B) →
62 ∃ B' : Finset V, ↑B' ⊆ ↑A ∧ m ≤ B'.card ∧
63 DistIndependent G (2 * j + 1) ↑B') := by
64 -- W = subtype of A
65 set W := {v : V // v ∈ A} with hW_def
66 -- Define H: vertices of A are adjacent in H iff their j-balls have a G-edge between them
67 let H : SimpleGraph W :=
68 { Adj := fun w₁ w₂ => w₁ ≠ w₂ ∧
69 ∃ x ∈ jBall G j w₁.val, ∃ y ∈ jBall G j w₂.val, G.Adj x y
70 symm := fun _ _ ⟨hne, x, hx, y, hy, hadj⟩ =>
71 ⟨hne.symm, y, hy, x, hx, hadj.symm⟩
72 loopless := ⟨fun w h => h.1 rfl⟩ }
73 refine ⟨W, inferInstance, inferInstance, H, ?_, ?_, ?_⟩
74 -- (1) IsShallowMinor H G j
75 · exact ⟨{
76 branchSet := fun w => jBall G j w.val
77 center := fun w => w.val
78 center_mem := fun w => mem_jBall_self G j w.val
79 branchDisjoint := fun u v huv =>
80 jBall_disjoint hA u.prop v.prop (Subtype.val_injective.ne huv)
81 branchRadius := fun w x hx => by
82 obtain ⟨q, hq⟩ := hx
83 exact ⟨q.bypass, q.bypass_isPath, q.length_bypass_le.trans hq,
84 fun z hz => ⟨q.takeUntil z (q.support_bypass_subset hz),
85 (q.length_takeUntil_le (q.support_bypass_subset hz)).trans hq⟩⟩
86 branchEdge := fun u v hadj => hadj.2
87 }⟩
88 -- (2) A.card ≤ Fintype.card W
89 · exact le_of_eq (Fintype.card_coe A).symm
90 -- (3) Lifting property
91 · intro m ⟨B, hmB, hBind⟩
92 refine ⟨B.map ⟨Subtype.val, Subtype.val_injective⟩, ?_, ?_, ?_⟩
93 -- B' ⊆ A
94 · intro v hv
95 obtain ⟨w, _, rfl⟩ := Finset.mem_map.mp hv
96 exact w.prop
97 -- m ≤ B'.card
98 · rw [Finset.card_map]; exact hmB
99 -- DistIndependent G (2 * j + 1) B'
100 · intro a ha b hb hab
101 simp only [Finset.coe_map, Set.mem_image, Function.Embedding.coeFn_mk] at ha hb
102 obtain ⟨wa, hwa_mem, rfl⟩ := ha
103 obtain ⟨wb, hwb_mem, rfl⟩ := hb
104 have hwne : wa ≠ wb := fun h => hab (congrArg Subtype.val h)
105 -- wa, wb not adjacent in H (from distance-1 independence of B)
106 have hnadj : ¬H.Adj wa wb := by
107 intro hadj
108 have := hBind (Finset.mem_coe.mpr hwa_mem) (Finset.mem_coe.mpr hwb_mem)
109 hwne (.cons hadj .nil)
110 simp [SimpleGraph.Walk.length_cons, SimpleGraph.Walk.length_nil] at this
111 -- Extract: no G-edge between the j-balls
112 have hno_edge : ∀ x ∈ jBall G j wa.val, ∀ y ∈ jBall G j wb.val, ¬G.Adj x y := by
113 intro x hx y hy hadj_xy
114 exact hnadj ⟨hwne, x, hx, y, hy, hadj_xy⟩
115 -- Show any walk has length > 2j + 1
116 intro p
117 by_contra hle
118 push_neg at hle
119 by_cases hshort : j + 1 ≤ p.length
120 · -- Use crossing edge at depth j
121 obtain ⟨c, d, hadj_cd, ⟨q₁, hq₁⟩, ⟨q₂, hq₂⟩⟩ := walk_crossing_edge p j hshort
122 exact hno_edge c ⟨q₁, hq₁⟩ d
123 ⟨q₂.reverse, by rw [SimpleGraph.Walk.length_reverse]; omega⟩ hadj_cd
124 · -- Walk length ≤ j ≤ 2j, contradicts distance-2j independence
125 push_neg at hshort
126 exact absurd (hA wa.prop wb.prop (Subtype.val_injective.ne hwne) p) (by omega)
127
128end Catalog.Sparsity.OddStepReduction
129