import CubicPathwidth.Relabelling

/-!
# Reducing the prescribed-end-bag theorem to stable boundaries

The induction below removes a boundary vertex with zero or one neighbour
outside the boundary. A stable boundary has at least two outside neighbours
at every vertex. The width budget is monotone in both sizes; recursive
budgets are compared, never added. The stable structural case remains an
explicit input to the reduction.
-/

noncomputable section
namespace CubicPathwidth
open SectionDecomposition

/-- An endpoint witness on an induced section, using the original labels. -/
def HasEndingSection {n : ℕ} (G : SimpleGraph (Fin n))
    (U X : Finset (Fin n)) (w : ℝ) : Prop :=
  ∃ P : SectionDecomposition G U,
    P.bag P.lastIndex = X ∧ P.toBagPath.WidthAtMost w

theorem HasEndingSection.mono {n : ℕ} {G : SimpleGraph (Fin n)}
    {U X : Finset (Fin n)} {a b : ℝ}
    (h : HasEndingSection G U X a) (hab : a ≤ b) : HasEndingSection G U X b := by
  obtain ⟨P, hP, hw⟩ := h
  exact ⟨P, hP, hw.mono hab⟩

/-- Neighbours lying in a specified induced vertex set. -/
def sectionNeighbors {n : ℕ} (G : SimpleGraph (Fin n))
    (U : Finset (Fin n)) (v : Fin n) : Finset (Fin n) := by
  classical
  exact U.filter (G.Adj v)

@[simp] theorem mem_sectionNeighbors {n : ℕ} {G : SimpleGraph (Fin n)}
    {U : Finset (Fin n)} {u v : Fin n} :
    u ∈ sectionNeighbors G U v ↔ u ∈ U ∧ G.Adj v u := by
  classical
  simp [sectionNeighbors]

/-- No endpoint deletion move is available. -/
def StableBoundary {n : ℕ} (G : SimpleGraph (Fin n))
    (U X : Finset (Fin n)) : Prop :=
  ∀ v ∈ X, 2 ≤ (sectionNeighbors G (U \ X) v).card

/-- The two local endpoint moves reduce a general boundary to the stable
case. The only structural input is explicitly displayed as `hstable`. -/
theorem endingSection_induction {n : ℕ} (G : SimpleGraph (Fin n))
    (W : ℕ → ℕ → ℝ)
    (hmono : ∀ m m' x x', m ≤ m' → x ≤ x' → W m x ≤ W m' x')
    (hsize : ∀ m x : ℕ, x ≤ m → (x : ℝ) ≤ W m x)
    (hstable : ∀ U X : Finset (Fin n), X ⊆ U → StableBoundary G U X →
      (∀ V Y : Finset (Fin n), V.card < U.card → Y ⊆ V →
        HasEndingSection G V Y (W V.card Y.card)) →
      HasEndingSection G U X (W U.card X.card)) :
    ∀ U X : Finset (Fin n), X ⊆ U → HasEndingSection G U X (W U.card X.card) := by
  classical
  have go : ∀ m : ℕ, ∀ U : Finset (Fin n), U.card = m →
      ∀ X : Finset (Fin n), X ⊆ U → HasEndingSection G U X (W U.card X.card) := by
    intro m
    induction m using Nat.strong_induction_on with
    | h m ih =>
      intro U hU X hX
      by_cases hs : StableBoundary G U X
      · apply hstable U X hX hs
        intro V Y hV hY
        exact ih V.card (by omega) V rfl Y hY
      · obtain ⟨v, hvX, hvsmall⟩ : ∃ v ∈ X,
            (sectionNeighbors G (U \ X) v).card < 2 := by
          simpa only [StableBoundary, not_forall, not_le, exists_prop] using hs
        have hvU : v ∈ U := hX hvX
        have hlt : (U.erase v).card < m := by
          rw [← hU]
          exact Finset.card_erase_lt_of_mem hvU
        have hinsert : insert v (U.erase v) = U := Finset.insert_erase hvU
        have hbudget := hsize U.card X.card (Finset.card_le_card hX)
        have herase : (U.erase v).card ≤ U.card := Finset.card_le_card (Finset.erase_subset _ _)
        by_cases hz : sectionNeighbors G (U \ X) v = ∅
        · have hxsub : X.erase v ⊆ U.erase v := Finset.erase_subset_erase v hX
          obtain ⟨P, hend, hw⟩ := ih _ hlt (U.erase v) rfl (X.erase v) hxsub
          have hn : ∀ u ∈ U.erase v, G.Adj v u → u ∈ X := by
            intro u hu hadj
            by_contra huX
            have hmem : u ∈ sectionNeighbors G (U \ X) v :=
              mem_sectionNeighbors.mpr ⟨Finset.mem_sdiff.mpr
                ⟨Finset.mem_of_mem_erase hu, huX⟩, hadj⟩
            rw [hz] at hmem
            exact Finset.notMem_empty u hmem
          have hw' := hw.mono (hmono _ _ _ _ herase
            (Finset.card_le_card (Finset.erase_subset _ _)))
          obtain ⟨Q, hQ, hQw⟩ := restore_zero_outside P v (Finset.notMem_erase _ _)
            X hvX (by simpa only [hinsert] using hX) hend hn hw'
          have hQw' := hQw.mono (max_le le_rfl (by linarith))
          have hresult : HasEndingSection G (insert v (U.erase v)) X (W U.card X.card) :=
            ⟨Q, hQ, hQw'⟩
          simpa only [hinsert] using hresult
        · have hc : (sectionNeighbors G (U \ X) v).card = 1 := by
            have hp := Finset.card_pos.mpr (Finset.nonempty_iff_ne_empty.mpr hz)
            omega
          obtain ⟨u, hu⟩ := Finset.card_eq_one.mp hc
          have huN : u ∈ sectionNeighbors G (U \ X) v := by rw [hu]; simp
          obtain ⟨huUX, hvu⟩ := mem_sectionNeighbors.mp huN
          obtain ⟨huU, huX⟩ := Finset.mem_sdiff.mp huUX
          have huv : u ≠ v := by intro h; subst u; exact huX hvX
          have huErase : u ∈ U.erase v := Finset.mem_erase.mpr ⟨huv, huU⟩
          have hxsub : insert u (X.erase v) ⊆ U.erase v :=
            Finset.insert_subset huErase (Finset.erase_subset_erase v hX)
          have hxc : (insert u (X.erase v)).card ≤ X.card := by
            have he := Finset.card_erase_add_one hvX
            have hi := Finset.card_insert_le u (X.erase v)
            omega
          obtain ⟨P, hend, hw⟩ := ih _ hlt (U.erase v) rfl (insert u (X.erase v)) hxsub
          have hn : ∀ z ∈ U.erase v, G.Adj v z → z ∈ X ∨ z = u := by
            intro z hzU hvz
            by_cases hzX : z ∈ X
            · exact Or.inl hzX
            · right
              have hzN : z ∈ sectionNeighbors G (U \ X) v :=
                mem_sectionNeighbors.mpr ⟨Finset.mem_sdiff.mpr
                  ⟨Finset.mem_of_mem_erase hzU, hzX⟩, hvz⟩
              rw [hu] at hzN
              exact Finset.mem_singleton.mp hzN
          have hw' := hw.mono (hmono _ _ _ _ herase hxc)
          obtain ⟨Q, hQ, hQw⟩ := restore_one_outside P v u (Finset.notMem_erase _ _)
            huErase X hvX (by simpa only [hinsert] using hX) hend hn hw'
          have hQw' := hQw.mono (max_le le_rfl hbudget)
          have hresult : HasEndingSection G (insert v (U.erase v)) X (W U.card X.card) :=
            ⟨Q, hQ, hQw'⟩
          simpa only [hinsert] using hresult
  intro U X hX
  exact go U.card U rfl X hX

/-- The nonrecursive stable case is a useful specialization. -/
theorem endingSection_of_stable {n : ℕ} (G : SimpleGraph (Fin n))
    (W : ℕ → ℕ → ℝ)
    (hmono : ∀ m m' x x', m ≤ m' → x ≤ x' → W m x ≤ W m' x')
    (hsize : ∀ m x : ℕ, x ≤ m → (x : ℝ) ≤ W m x)
    (hstable : ∀ U X : Finset (Fin n), X ⊆ U → StableBoundary G U X →
      HasEndingSection G U X (W U.card X.card)) :
    ∀ U X : Finset (Fin n), X ⊆ U → HasEndingSection G U X (W U.card X.card) :=
  endingSection_induction G W hmono hsize (fun U X hX hs _ => hstable U X hX hs)

/-- The finite boundary budget uses a single overhead at the original size. -/
def endpointBudget (b C : ℝ) (L : ℕ → ℝ) (m x : ℕ) : ℝ :=
  max ((x : ℝ) + 1) (b * (m : ℝ) + (1 - 3 * b) * (x : ℝ) + C) + L m

theorem endpointBudget_mono {b C : ℝ} (hb : 0 ≤ b) (hb' : b ≤ 1 / 3)
    {L : ℕ → ℝ} (hL : Monotone L) {m m' x x' : ℕ}
    (hm : m ≤ m') (hx : x ≤ x') :
    endpointBudget b C L m x ≤ endpointBudget b C L m' x' := by
  have hm' : (m : ℝ) ≤ m' := by exact_mod_cast hm
  have hx' : (x : ℝ) ≤ x' := by exact_mod_cast hx
  have hbmul := mul_le_mul_of_nonneg_left hm' hb
  have hxmul := mul_le_mul_of_nonneg_left hx' (show 0 ≤ 1 - 3 * b by linarith)
  apply add_le_add _ (hL hm)
  exact max_le_max (by linarith) (by linarith)

theorem endpointBudget_ge_size (b C : ℝ) {L : ℕ → ℝ}
    (hL : ∀ m, 0 ≤ L m) (m x : ℕ) : (x : ℝ) ≤ endpointBudget b C L m x := by
  unfold endpointBudget
  linarith [le_max_left ((x : ℝ) + 1) (b * m + (1 - 3 * b) * x + C), hL m]

end CubicPathwidth