import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets

/-!
# Stage 2, task K4c: `algo_T4` realizes Theorem 4

From the internal bound `AlgoT4InternalBound` (width `≤ ∑ thm4Coeff + ε n₀ + C`, with
`n₀` the number of non-isolated vertices, `n₀ ≤ n`) and the Stage 1 export
`algoT4Exported` (the output is a path decomposition), we get the realization for
`n ≥ N`, with `N` chosen so that `C ≤ ε n / 2`.
-/

noncomputable section

namespace CubicPathwidth.Alg

/-- `n₀ ≤ n`: the non-isolated vertices form a subset of `Fin n`. -/
theorem nonIsolatedCount_le_card {n : ℕ} (S : SimpleGraph (Fin n)) :
    nonIsolatedCount S ≤ n := by
  unfold nonIsolatedCount
  classical
  calc _ ≤ (Finset.univ : Finset (Fin n)).card := Finset.card_filter_le _ _
    _ = n := by simp

/-- (K4c) Theorem 4 realized by `algo_T4`, from the internal bound. -/
theorem algoT4RealizesTheorem4_of (h : AlgoT4InternalBound) : AlgoT4RealizesTheorem4 := by
  intro hAdm ε hε
  obtain ⟨C, hC⟩ := h hAdm (ε / 2) (by positivity)
  refine ⟨⌈2 * |C| / ε⌉₊, ?_⟩
  intro n hN S hD
  obtain ⟨lab, hfb, hw⟩ := hC n S
  refine ⟨lab, hfb, algoT4Exported n S lab, ?_⟩
  have hnN : (⌈2 * |C| / ε⌉₊ : ℝ) ≤ (n : ℝ) := by exact_mod_cast hN
  have h1 : 2 * |C| / ε ≤ (n : ℝ) := (Nat.le_ceil _).trans hnN
  rw [div_le_iff₀ hε] at h1
  have h2 : (nonIsolatedCount S : ℝ) ≤ n := by exact_mod_cast nonIsolatedCount_le_card S
  have h3 : ε / 2 * (nonIsolatedCount S : ℝ) ≤ ε / 2 * n :=
    mul_le_mul_of_nonneg_left h2 (by positivity)
  have h4 : C ≤ ε * n / 2 := by linarith [le_abs_self C]
  linarith

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT4RealizesTheorem4_of