import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T4.Cor5S

/-!
# Stage 2, task K5: `algo_T4` realizes Corollary 5

From the internal bound `AlgoT4InternalBound` (width `≤ ∑ thm4Coeff + ε n₀ + C`) and
the degree facts `n₀ ≤ 2m` and `∑ thm4Coeff(d(v)) ≤ (7/48) m` (`T4.coeff_le`,
`∑ deg = 2m`), we get the realization for `m ≥ M`, with `M` chosen so that `C ≤ ε m / 2`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open scoped Classical in
/-- `∑ deg = 2m`. -/
theorem sum_degree_eq_two_mul_edgeCount {n : ℕ} (S : SimpleGraph (Fin n)) :
    ∑ v, S.degree v = 2 * T4.edgeCount S := by
  classical
  unfold T4.edgeCount
  exact SimpleGraph.sum_degrees_eq_twice_card_edges S

open scoped Classical in
/-- `n₀ ≤ 2m`: every non-isolated vertex has degree at least `1`. -/
theorem nonIsolatedCount_le_two_mul_edgeCount {n : ℕ} (S : SimpleGraph (Fin n)) :
    nonIsolatedCount S ≤ 2 * T4.edgeCount S := by
  rw [← sum_degree_eq_two_mul_edgeCount S]
  unfold nonIsolatedCount
  classical
  calc _ = ∑ v ∈ Finset.univ.filter (fun v : Fin n => S.degree v ≠ 0), 1 := by simp
    _ ≤ ∑ v ∈ Finset.univ.filter (fun v : Fin n => S.degree v ≠ 0), S.degree v :=
        Finset.sum_le_sum (fun v hv => by simp at hv; omega)
    _ ≤ ∑ v, S.degree v :=
        Finset.sum_le_sum_of_subset_of_nonneg (Finset.filter_subset _ _)
          (fun _ _ _ => Nat.zero_le _)

open scoped Classical in
/-- `∑ thm4Coeff(d(v)) ≤ (7/48) m`, from the per-degree bound `a_d ≤ (7/96) d`. -/
theorem degreeWeight_thm4Coeff_le_edgeCount {n : ℕ} (S : SimpleGraph (Fin n)) :
    T4.degreeWeight S T4.thm4Coeff ≤ 7 / 48 * (T4.edgeCount S : ℝ) := by
  unfold T4.degreeWeight
  have hdeg : (∑ v : Fin n, ((S.degree v : ℕ) : ℝ)) = 2 * (T4.edgeCount S : ℝ) := by
    exact_mod_cast sum_degree_eq_two_mul_edgeCount S
  calc _ ≤ ∑ v : Fin n, 7 / 96 * ((S.degree v : ℕ) : ℝ) :=
        Finset.sum_le_sum (fun v _ => CubicPathwidth.T4.coeff_le _)
    _ = 7 / 96 * ∑ v : Fin n, ((S.degree v : ℕ) : ℝ) := by rw [Finset.mul_sum]
    _ = 7 / 48 * (T4.edgeCount S : ℝ) := by rw [hdeg]; ring

/-- (K5) Corollary 5 realized by `algo_T4`, from the internal bound. -/
theorem algoT4RealizesCorollary5_of (h : AlgoT4InternalBound) : AlgoT4RealizesCorollary5 := by
  intro hAdm ε hε
  obtain ⟨C, hC⟩ := h hAdm (ε / 4) (by positivity)
  refine ⟨⌈2 * |C| / ε⌉₊, ?_⟩
  intro n S hD hM
  obtain ⟨lab, hfb, hw⟩ := hC n S
  refine ⟨lab, hfb, algoT4Exported n S lab, ?_⟩
  have hMR : (⌈2 * |C| / ε⌉₊ : ℝ) ≤ (T4.edgeCount S : ℝ) := by exact_mod_cast hM
  have h1 : 2 * |C| / ε ≤ (T4.edgeCount S : ℝ) := (Nat.le_ceil _).trans hMR
  rw [div_le_iff₀ hε] at h1
  have h2 : (nonIsolatedCount S : ℝ) ≤ 2 * (T4.edgeCount S : ℝ) := by
    exact_mod_cast nonIsolatedCount_le_two_mul_edgeCount S
  have h3 : ε / 4 * (nonIsolatedCount S : ℝ) ≤ ε / 4 * (2 * (T4.edgeCount S : ℝ)) :=
    mul_le_mul_of_nonneg_left h2 (by positivity)
  have h4 := degreeWeight_thm4Coeff_le_edgeCount S
  have h5 : C ≤ ε * (T4.edgeCount S : ℝ) / 2 := by linarith [le_abs_self C]
  linarith

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT4RealizesCorollary5_of