import CubicPathwidth.CoreTorso
import CubicPathwidth.SectionInsertion

/-! Lift a torso path by inserting its disjoint attached components. -/

noncomputable section
namespace CubicPathwidth
open SectionDecomposition
variable {n : ℕ} (G : SimpleGraph (Fin n))

/-- Insert all components at preserved original bags. The overhead is paid
once, since each insertion returns to the same original bag before proceeding. -/
theorem insert_components {F B : Finset (Fin n)} (hB : B ⊆ F)
    (P : SectionDecomposition G B) {p b : ℝ} (hP : P.toBagPath.WidthAtMost p)
    (hb : 0 ≤ b)
    (hpieces : ∀ T ∈ components G (F \ B),
      ∃ Q : SectionDecomposition G T, Q.toBagPath.WidthAtMost b)
    (hanchor : ∀ T ∈ components G (F \ B),
      ∃ i, i ≤ P.lastIndex ∧ attachment G B T ⊆ P.bag i) :
    ∃ R : SectionDecomposition G F, R.toBagPath.WidthAtMost (p + b + 1) := by
  classical
  have hall : ∀ S : Finset (Finset (Fin n)), S ⊆ components G (F \ B) →
      ∃ R : SectionDecomposition G (B ∪ S.biUnion id),
        R.toBagPath.WidthAtMost (p + b + 1) ∧
        ∀ k, k ≤ P.lastIndex → ∃ j, j ≤ R.lastIndex ∧ R.bag j = P.bag k := by
    intro S
    induction S using Finset.induction with
    | empty =>
      intro _
      rw [Finset.biUnion_empty, Finset.union_empty]
      exact ⟨P, hP.mono (by linarith), fun k hk => ⟨k, hk, rfl⟩⟩
    | @insert T S hnot ih =>
      intro hS
      have hT := hS (Finset.mem_insert_self T S)
      have hS' : S ⊆ components G (F \ B) := fun _ h => hS (Finset.mem_insert_of_mem h)
      obtain ⟨R, hR, hkeep⟩ := ih hS'
      obtain ⟨Q, hQ⟩ := hpieces T hT
      obtain ⟨i, hi, hai⟩ := hanchor T hT
      obtain ⟨j, hj, heq⟩ := hkeep i hi
      have hdis : Disjoint (B ∪ S.biUnion id) T := by
        apply Finset.disjoint_left.mpr
        intro v hv hvT
        rcases Finset.mem_union.mp hv with hvB | hvS
        · exact (Finset.mem_sdiff.mp ((mem_components G hT).1 hvT)).2 hvB
        · obtain ⟨U, hU, hvU⟩ := Finset.mem_biUnion.mp hvS
          exact Finset.disjoint_left.mp (components_disjoint G (hS' hU) hT
            (by intro he; subst U; exact hnot hU)) hvU hvT
      have hsep : ∀ v ∈ T, ∀ u ∈ B ∪ S.biUnion id, G.Adj v u → u ∈ R.bag j := by
        intro v hv u hu hadj
        rw [heq]
        rcases Finset.mem_union.mp hu with huB | huS
        · exact hai ((mem_attachment G).mpr ⟨huB, v, hv, hadj.symm⟩)
        · obtain ⟨U, hU, huU⟩ := Finset.mem_biUnion.mp huS
          have huT := (mem_components G hT).2.1 v hv u ((mem_components G (hS' hU)).1 huU) hadj
          exact False.elim (Finset.disjoint_left.mp (components_disjoint G (hS' hU) hT
            (by intro he; subst U; exact hnot hU)) huU huT)
      obtain ⟨R', hR', hkeep'⟩ := insert_at_bag R Q hdis j hj hsep hR hQ
      have hw : R'.toBagPath.WidthAtMost (p + b + 1) := by
        apply hR'.mono
        apply max_le le_rfl
        rw [heq]
        have := hP i hi
        linarith
      have hk : ∀ k, k ≤ P.lastIndex → ∃ j, j ≤ R'.lastIndex ∧ R'.bag j = P.bag k := by
        intro k hk
        obtain ⟨l, hl, hle⟩ := hkeep k hk
        obtain ⟨m, hm, hme⟩ := hkeep' l hl
        exact ⟨m, hm, hme.trans hle⟩
      have he : (B ∪ S.biUnion id) ∪ T = B ∪ (insert T S).biUnion id := by
        rw [Finset.biUnion_insert]
        ext v
        simp only [Finset.mem_union, id_eq]
        tauto
      have hout : ∃ R : SectionDecomposition G ((B ∪ S.biUnion id) ∪ T),
          R.toBagPath.WidthAtMost (p + b + 1) ∧
          ∀ k, k ≤ P.lastIndex → ∃ j, j ≤ R.lastIndex ∧ R.bag j = P.bag k := ⟨R', hw, hk⟩
      rw [he] at hout
      exact hout
  obtain ⟨R, hR, _⟩ := hall (components G (F \ B)) Finset.Subset.rfl
  have he : B ∪ (components G (F \ B)).biUnion id = F := by
    rw [components_cover, Finset.union_sdiff_of_subset hB]
  have hout : ∃ R : SectionDecomposition G (B ∪ (components G (F \ B)).biUnion id),
      R.toBagPath.WidthAtMost (p + b + 1) := ⟨R, hR⟩
  rw [he] at hout
  exact hout

/-- The previously explicit core-lifting obligation, now discharged by
actual subcubic torso and interval-preserving path constructions. -/
theorem coreLiftingBound : CoreLiftingBound coreOverhead := by
  classical
  intro n G hG F C hp hmin
  let B := branchVertices G C
  have hBC : B ⊆ C := Finset.filter_subset _ _
  have hB : B ⊆ F := hBC.trans (LeafPrunes.subset G hp)
  have hattach : ∀ T ∈ components G (F \ B), (attachment G B T).card ≤ 2 :=
    fun T hT => (core_piece_bounds G hG hp hmin hT).2.1
  refine ⟨coreTorso G F B, coreTorso_subcubic G hG F B hattach, ?_⟩
  intro p hpath
  obtain ⟨D, hD⟩ := hpath
  let P := liftTorso G F B D
  have hP := liftTorso_width G F B D hD
  let b : ℝ := 4 * Real.sqrt (F.card : ℝ) + 1
  have hpieces : ∀ T ∈ components G (F \ B),
      ∃ Q : SectionDecomposition G T, Q.toBagPath.WidthAtMost b := by
    intro T hT
    obtain ⟨Q, hQ⟩ := pseudotree_section_decomposition G hG T
      (mem_components G hT).2.2 (core_piece_bounds G hG hp hmin hT).1
    have hc : (T.card : ℝ) ≤ F.card := by
      exact_mod_cast Finset.card_le_card ((mem_components G hT).1.trans Finset.sdiff_subset)
    exact ⟨Q, hQ.mono (by dsimp [b]; linarith [Real.sqrt_le_sqrt hc])⟩
  obtain ⟨R, hR⟩ := insert_components G hB P hP (show 0 ≤ b by dsimp [b]; positivity)
    hpieces (fun T hT => torso_attachment_bag G F B D hT (hattach T hT))
  exact ⟨R, hR.mono (by dsimp [b, coreOverhead]; nlinarith [Real.sqrt_nonneg (F.card : ℝ)])⟩

/-- The original boundary transfer claim, without additional graph inputs. -/
theorem boundaryTransfer : BoundaryTransferClaim :=
  boundaryTransfer_of_tree_and_core forestComponentBound coreLiftingBound

end CubicPathwidth