import CubicPathwidth.PwSeq.BootSeq
import CubicPathwidth.T4.BasicComp

/-!
# The first case of `lem:basic` for base degree `k`, over the torso components

Generalized copy of `T4/BasicComp.lean` (`componentClaim`). The base hypothesis now
covers only graphs of minimum degree at least `3` and maximum degree at most `k`; it is
applied to the relabelled torso component `coreTorso G (F \ (B \ C)) C` of a torso
component `C` all of whose torso degrees are at most `k`. Route note: besides the
maximum-degree bound (`maxDegreeAtMost_coreTorso`), this needs that the relabelled
component has minimum degree at least `3` (`Boot.minDegree_coreTorso`: its degrees are
the torso degrees on `C`, because `C` is closed under torso edges, and these are at
least `3` by the hypothesis on the state).
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq
namespace Boot

open T2 T4 BasicAux SectionDecomposition

/-- The first case of `lem:basic` with base degree `k`, assembled over the torso
components: for every good state with torso minimum degree at least `3`, if each torso
component has maximum torso degree at most `k` or pathwidth at most `q`, then
`pw(torso) ≤ max (ψ⁻ + b₃ + ε n + N₀) q`. -/
theorem componentClaim {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b)
    (hbase : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasMinDegreeAtLeast 3 G → MaxDegreeAtMost k G →
        HasPathwidthAtMost G (degreeWeight G b + ε * n))
    (ε : ℝ) (hε : 0 < ε) : ∃ N₀ : ℕ,
      ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)),
        Good G F B → (∀ v ∈ B, 3 ≤ tdeg G F B v) → ∀ q : ℝ,
        (∀ C ∈ tcomps G F B, (∀ v ∈ C, tdeg G F B v ≤ k) ∨
          HasPathwidthAtMost (coreTorso G (F \ (B \ C)) C) q) →
        HasPathwidthAtMost (coreTorso G F B)
          (max (psiMinus b G F B + b 3 + ε * n + N₀) q) := by
  obtain ⟨N, hN⟩ := hbase ε hε
  refine ⟨N, ?_⟩
  intro n G F B _hgood hmin q hcomp
  have hpsi0 : 0 ≤ psiMinus b G F B := (Boot.psi_bounds hb G F B hmin).1
  have hb3 : 0 ≤ b 3 := Boot.nonneg hb 3
  have hεn : 0 ≤ ε * (n : ℝ) := mul_nonneg hε.le (Nat.cast_nonneg n)
  have hN0 : (0 : ℝ) ≤ (N : ℝ) := Nat.cast_nonneg N
  have hbig : psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ) ≤
      max (psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ)) q := le_max_left _ _
  set W : ℝ := max (psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ)) q with hW
  have hW1 : -1 ≤ W := by linarith
  have hWN : (N : ℝ) ≤ W := by linarith
  have hsec : ∀ C ∈ tcomps G F B, ∃ P : SectionDecomposition (tgraph G F B) C,
      P.toBagPath.WidthAtMost W := by
    intro C hC
    obtain ⟨hCB, _⟩ := tcomp_props hC
    have hgraph := coreTorso_eq_induced G F B C hCB
    rcases hcomp C hC with hdeg | hq
    · by_cases hsize : N ≤ C.card
      · have hK := maxDegreeAtMost_coreTorso G F B C hCB hdeg
        have hpw := hN C.card hsize _ (Boot.minDegree_coreTorso hC hmin) hK
        have hle : degreeWeight (coreTorso G (F \ (B \ C)) C) b + ε * (C.card : ℝ) ≤ W := by
          have h1 := Boot.degreeWeight_coreTorso_le hb G F B C hCB
          have h2 := Boot.term_le_psiMinus hb hC hmin
          have h3 := BasicAux.runMin_le_incr_three b (cmin G F B C)
          rw [Boot.incr_three hb] at h3
          have h4' : C.card ≤ n := by simpa using Finset.card_le_univ C
          have h4 : (C.card : ℝ) ≤ (n : ℝ) := by exact_mod_cast h4'
          have h5 : ε * (C.card : ℝ) ≤ ε * (n : ℝ) := mul_le_mul_of_nonneg_left h4 hε.le
          have h6 : psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ) ≤ W := hbig
          linarith
        have hpw' : HasPathwidthAtMost (inducedOnFin (tgraph G F B) C)
            (degreeWeight (coreTorso G (F \ (B \ C)) C) b + ε * (C.card : ℝ)) := by
          rw [← hgraph]
          exact hpw
        exact section_of_hasPathwidth hpw' hle
      · have hlt : (C.card : ℝ) < (N : ℝ) := by
          have : C.card < N := by omega
          exact_mod_cast this
        have hpw := trivial_pathwidth_bound (coreTorso G (F \ (B \ C)) C)
        have hpw' : HasPathwidthAtMost (inducedOnFin (tgraph G F B) C)
            ((C.card : ℝ) - 1) := by
          rw [← hgraph]
          exact hpw
        exact section_of_hasPathwidth hpw' (by linarith)
    · have hq' : HasPathwidthAtMost (inducedOnFin (tgraph G F B) C) q := by
        rw [← hgraph]
        exact hq
      exact section_of_hasPathwidth hq' (le_max_right _ _)
  have hcl : ∀ C ∈ tcomps G F B, ∀ u ∈ C, ∀ v, (tgraph G F B).Adj u v → v ∈ C :=
    fun C hC => BasicAux.tcomp_closed hC
  have hdis : ∀ C ∈ tcomps G F B, ∀ D ∈ tcomps G F B, C ≠ D → Disjoint C D :=
    fun C hC D hD hne => components_disjoint (tgraph G F B) hC hD hne
  have hcov : (tcomps G F B).biUnion id = B := components_cover (tgraph G F B) B
  obtain ⟨P, hPw⟩ := glueSections (tgraph G F B) hW1 (tcomps G F B) B hcov hcl hdis hsec
  have heq : coreTorso G F B = inducedOnFin (tgraph G F B) B := by
    have h := coreTorso_eq_induced G F B B (subset_refl B)
    rwa [Finset.sdiff_self, Finset.sdiff_empty] at h
  rw [heq]
  exact hasPathwidthAtMost_of_section P hPw

end Boot
end PwSeq
end CubicPathwidth