import CubicPathwidth.T3.Defs
import CubicPathwidth.T2.Reduction

/-!
# Reduction for maximum degree five (`Reduction5Claim`)

Adapts `T2.reduction` (maximum degree four, two coefficients) to maximum degree
five and three coefficients. The degree-independent part of the route (good cores,
the minimal core `exists_minimal_core`, torso degrees `torso_degree_le`, the
lifting lemmas and `coreOverhead_sublinear`) is reused unchanged from
`CubicPathwidth.T2`. Only the degree-count transfer and the maximum degree of the
torso are new.

* `degreeCount_three_four_five`, `degreeCount_four_five`, `degreeCount_five`:
  degree counts of a graph of maximum degree at most five as counts of
  `{v | k ≤ deg v}`.
* `card_ge_le`: an injection `e` that does not decrease degrees does not
  decrease the number of vertices of degree at least `k`.
* `degreeCount_transfer5`: `a₃ n₃(R) + a₄ n₄(R) + a₅ n₅(R) ≤ a₃ n₃(G) + a₄ n₄(G) + a₅ n₅(G)`
  for `0 ≤ a₃ ≤ a₄ ≤ a₅`.
* `reduction5 : Reduction5Claim`.
-/

noncomputable section
namespace CubicPathwidth
namespace T3

open T2
open SectionDecomposition

open Classical in
/-- Degree counts of a graph of maximum degree at most five, summed. -/
theorem degreeCount_three_four_five {k : ℕ} (H : SimpleGraph (Fin k))
    (hH : ∀ v, H.degree v ≤ 5) :
    degreeCount H 3 + degreeCount H 4 + degreeCount H 5 =
      (Finset.univ.filter fun v => 3 ≤ H.degree v).card := by
  unfold degreeCount
  simp only [Finset.card_filter]
  rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl
  intro v _
  have := hH v
  split_ifs <;> omega

open Classical in
/-- Degree counts of a graph of maximum degree at most five, summed. -/
theorem degreeCount_four_five {k : ℕ} (H : SimpleGraph (Fin k))
    (hH : ∀ v, H.degree v ≤ 5) :
    degreeCount H 4 + degreeCount H 5 =
      (Finset.univ.filter fun v => 4 ≤ H.degree v).card := by
  unfold degreeCount
  simp only [Finset.card_filter]
  rw [← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl
  intro v _
  have := hH v
  split_ifs <;> omega

open Classical in
/-- Degree count of degree five in a graph of maximum degree at most five. -/
theorem degreeCount_five {k : ℕ} (H : SimpleGraph (Fin k)) (hH : ∀ v, H.degree v ≤ 5) :
    degreeCount H 5 = (Finset.univ.filter fun v => 5 ≤ H.degree v).card := by
  unfold degreeCount
  simp only [Finset.card_filter]
  apply Finset.sum_congr rfl
  intro v _
  have := hH v
  split_ifs <;> omega

open Classical in
/-- An injection that does not decrease degrees does not decrease the number of
vertices of degree at least `k`. -/
theorem card_ge_le {m n : ℕ} (R : SimpleGraph (Fin m)) (G : SimpleGraph (Fin n))
    (e : Fin m ↪ Fin n) (hdeg : ∀ i, R.degree i ≤ G.degree (e i)) (k : ℕ) :
    (Finset.univ.filter fun i => k ≤ R.degree i).card ≤
      (Finset.univ.filter fun v => k ≤ G.degree v).card := by
  apply Finset.card_le_card_of_injOn e
  · intro i hi
    simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢
    exact hi.trans (hdeg i)
  · intro i _ j _ hij
    exact e.injective hij

open Classical in
/-- Degree-count transfer along a degree-dominated injection, maximum degree five. -/
theorem degreeCount_transfer5 {m n : ℕ} (G : SimpleGraph (Fin n)) (R : SimpleGraph (Fin m))
    (e : Fin m ↪ Fin n) (hdeg : ∀ i, R.degree i ≤ G.degree (e i)) (hG : MaxDegreeAtMost 5 G)
    {a₃ a₄ a₅ : ℝ} (h3 : 0 ≤ a₃) (h34 : a₃ ≤ a₄) (h45 : a₄ ≤ a₅) :
    a₃ * (degreeCount R 3 : ℝ) + a₄ * (degreeCount R 4 : ℝ) + a₅ * (degreeCount R 5 : ℝ) ≤
      a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
        a₅ * (degreeCount G 5 : ℝ) := by
  have hG' : ∀ v, G.degree v ≤ 5 := by
    intro v
    have := hG v
    convert this
  have hR : ∀ i, R.degree i ≤ 5 := fun i => (hdeg i).trans (hG' (e i))
  have c5 : degreeCount R 5 ≤ degreeCount G 5 := by
    rw [degreeCount_five R hR, degreeCount_five G hG']
    exact card_ge_le R G e hdeg 5
  have c4 : degreeCount R 4 + degreeCount R 5 ≤ degreeCount G 4 + degreeCount G 5 := by
    rw [degreeCount_four_five R hR, degreeCount_four_five G hG']
    exact card_ge_le R G e hdeg 4
  have c3 : degreeCount R 3 + degreeCount R 4 + degreeCount R 5 ≤
      degreeCount G 3 + degreeCount G 4 + degreeCount G 5 := by
    rw [degreeCount_three_four_five R hR, degreeCount_three_four_five G hG']
    exact card_ge_le R G e hdeg 3
  have c5' : (degreeCount R 5 : ℝ) ≤ degreeCount G 5 := by exact_mod_cast c5
  have c4' : (degreeCount R 4 : ℝ) + degreeCount R 5 ≤ degreeCount G 4 + degreeCount G 5 := by
    exact_mod_cast c4
  have c3' : (degreeCount R 3 : ℝ) + degreeCount R 4 + degreeCount R 5 ≤
      degreeCount G 3 + degreeCount G 4 + degreeCount G 5 := by
    exact_mod_cast c3
  have p1 := mul_le_mul_of_nonneg_left c3' h3
  have p2 := mul_le_mul_of_nonneg_left c4' (sub_nonneg.mpr h34)
  have p3 := mul_le_mul_of_nonneg_left c5' (sub_nonneg.mpr h45)
  nlinarith

/-- (C6) Vertices of degree at most two cost `o(n)` in pathwidth, maximum degree five. -/
theorem reduction5 : Reduction5Claim := by
  intro a₃ a₄ a₅ h3 h34 h45 hbound ε hε
  obtain ⟨N₁, hN₁⟩ := hbound (ε / 2) (by linarith)
  obtain ⟨N₂, hN₂⟩ := coreOverhead_sublinear (ε / 8) (by linarith)
  obtain ⟨M, hM⟩ := exists_nat_ge (4 * ((N₁ : ℝ) + 1) / ε)
  refine ⟨max N₂ M, ?_⟩
  intro n hn G hG
  classical
  obtain ⟨B, hgood, hmin3⟩ := exists_minimal_core G
  have hattach : ∀ T ∈ components G (Finset.univ \ B), (attachment G B T).card ≤ 2 :=
    fun T hT => (hgood T hT).1
  have hdom := torso_degree_le G Finset.univ B hattach
  have hRmin : MinDegreeAtLeast 3 (coreTorso G Finset.univ B) := by
    intro i
    convert hmin3 i
  have hRmax : MaxDegreeAtMost 5 (coreTorso G Finset.univ B) := by
    intro i
    have h1 := hdom i
    have h2 := hG (enumerate B i)
    convert h1.trans (by convert h2)
  have hcount := degreeCount_transfer5 G (coreTorso G Finset.univ B) (enumerate B)
    (by intro i; convert hdom i) hG h3 h34 h45
  have ha4 : 0 ≤ a₄ := h3.trans h34
  have ha5 : 0 ≤ a₅ := ha4.trans h45
  have hS : 0 ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
      a₅ * (degreeCount G 5 : ℝ) := by
    have q3 := mul_nonneg h3 (Nat.cast_nonneg (degreeCount G 3))
    have q4 := mul_nonneg ha4 (Nat.cast_nonneg (degreeCount G 4))
    have q5 := mul_nonneg ha5 (Nat.cast_nonneg (degreeCount G 5))
    linarith
  have hBn : (B.card : ℝ) ≤ n := by
    have := Finset.card_le_univ B
    simp only [Fintype.card_fin] at this
    exact_mod_cast this
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  have hRpw : HasPathwidthAtMost (coreTorso G Finset.univ B)
      (a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
        a₅ * (degreeCount G 5 : ℝ) + ε / 2 * n + N₁) := by
    by_cases hm : N₁ ≤ B.card
    · obtain ⟨D, hD⟩ := hN₁ B.card hm _ hRmin hRmax
      refine ⟨D, fun i => (hD i).trans ?_⟩
      have : ε / 2 * (B.card : ℝ) ≤ ε / 2 * n :=
        mul_le_mul_of_nonneg_left hBn (by linarith)
      have : (0 : ℝ) ≤ N₁ := Nat.cast_nonneg _
      linarith
    · obtain ⟨D, hD⟩ := trivial_pathwidth_bound (coreTorso G Finset.univ B)
      refine ⟨D, fun i => (hD i).trans ?_⟩
      have : (B.card : ℝ) ≤ N₁ := by exact_mod_cast (not_le.mp hm).le
      have : 0 ≤ ε / 2 * (n : ℝ) := by positivity
      linarith
  obtain ⟨D, hD⟩ := hRpw
  have hP := liftTorso_width G Finset.univ B D hD
  have hpieces : ∀ T ∈ components G (Finset.univ \ B),
      ∃ Q : SectionDecomposition G T, Q.toBagPath.WidthAtMost (12 * Real.sqrt (n : ℝ)) := by
    intro T hT
    obtain ⟨Q, hQ⟩ := (hgood T hT).2.section_decomposition (by have := (hgood T hT).1; omega)
    have hc : (T.card : ℝ) ≤ n := by
      have := Finset.card_le_univ T
      simp only [Fintype.card_fin] at this
      exact_mod_cast this
    exact ⟨Q, hQ.mono (by linarith [Real.sqrt_le_sqrt hc])⟩
  obtain ⟨R', hR'⟩ := insert_components G (Finset.subset_univ B) (liftTorso G Finset.univ B D) hP
    (by positivity) hpieces
    (fun T hT => torso_attachment_bag G Finset.univ B D hT (hattach T hT))
  refine ⟨R'.toFull, toFull_width R' (hR'.mono ?_)⟩
  have h1 := hN₂ n ((le_max_left _ _).trans hn)
  unfold coreOverhead at h1
  have hMn : (M : ℝ) ≤ n := by exact_mod_cast (le_max_right _ _).trans hn
  have h2 : 4 * ((N₁ : ℝ) + 1) ≤ ε * n := by
    have := hM.trans hMn
    rw [div_le_iff₀ hε] at this
    linarith
  have : (0 : ℝ) ≤ Real.sqrt n := Real.sqrt_nonneg _
  nlinarith

end T3
end CubicPathwidth

#print axioms CubicPathwidth.T3.reduction5