CubicPathwidth.T2.ReductionPieces

Source file CubicPathwidth/T2/ReductionPieces.lean of the Lean project (how it is built).

import CubicPathwidth.CoreLifting

/-!
# Pieces removed by degree-at-most-two reductions have small pathwidth

`Piece G T A` records how a vertex set `T` was removed by reductions while
attached to the vertex set `A`. It is a rooted tree decomposition with bags of
at most three vertices: a `node` bag is `insert v A`, and its subtree `T`
hangs from that bag. From this structure we extract, for every subset `S` of
the piece, a balanced separator of at most three vertices. Recursive balanced
separators give a section decomposition of width at most `12 * √|T|`.
-/

noncomputable section
namespace CubicPathwidth
namespace T2
open SectionDecomposition

variable {n : ℕ} (G : SimpleGraph (Fin n))

/-- A rooted tree decomposition of width at most two, hanging from `A`. -/
inductive Piece : Finset (Fin n) → Finset (Fin n) → Prop
  | empty (A : Finset (Fin n)) : Piece ∅ A
  | union {T₁ T₂ A : Finset (Fin n)} : Piece T₁ A → Piece T₂ A → Piece (T₁ ∪ T₂) A
  | node {v : Fin n} {T A : Finset (Fin n)} : (insert v A).card ≤ 3 →
      (∀ u, G.Adj v u → u ∈ T ∨ u ∈ A) → Piece T (insert v A) → Piece (insert v T) A
  | mono {T A A' : Finset (Fin n)} : Piece T A → A ⊆ A' → Piece T A'

variable {G}

/-- Every edge leaving a piece ends in its attachment set. -/
theorem Piece.edges {T A : Finset (Fin n)} (h : Piece G T A) :
    ∀ u ∈ T, ∀ w, G.Adj u w → w ∈ T ∨ w ∈ A := by
  induction h with
  | empty A => intro u hu; simp at hu
  | union _ _ ih₁ ih₂ =>
    intro u hu w hw
    rcases Finset.mem_union.mp hu with hu | hu
    · rcases ih₁ u hu w hw with h | h
      · exact Or.inl (Finset.mem_union_left _ h)
      · exact Or.inr h
    · rcases ih₂ u hu w hw with h | h
      · exact Or.inl (Finset.mem_union_right _ h)
      · exact Or.inr h
  | @node v T A _ hv _ ih =>
    intro u hu w hw
    rcases Finset.mem_insert.mp hu with rfl | hu
    · rcases hv w hw with h | h
      · exact Or.inl (Finset.mem_insert_of_mem h)
      · exact Or.inr h
    · rcases ih u hu w hw with h | h
      · exact Or.inl (Finset.mem_insert_of_mem h)
      · rcases Finset.mem_insert.mp h with rfl | h
        · exact Or.inl (Finset.mem_insert_self _ _)
        · exact Or.inr h
  | mono _ hAA' ih =>
    intro u hu w hw
    rcases ih u hu w hw with h | h
    · exact Or.inl h
    · exact Or.inr (hAA' h)

variable (G) in

/-- A finite union of pieces with a common attachment set is a piece. -/
theorem Piece.biUnion (A : Finset (Fin n)) (𝒯 : Finset (Finset (Fin n)))
    (h : ∀ T ∈ 𝒯, Piece G T A) : Piece G (𝒯.biUnion id) A := by
  classical
  induction 𝒯 using Finset.induction_on with
  | empty => simpa using Piece.empty (G := G) A
  | @insert T 𝒯 _ ih =>
    rw [Finset.biUnion_insert]
    exact Piece.union (h T (Finset.mem_insert_self _ _))
      (ih fun S hS => h S (Finset.mem_insert_of_mem hS))

variable (G) in

/-- A connected component of `S \ X` cannot leave a region whose outgoing
edges all end in `Y`, when `Y ∩ S ⊆ X`. -/
theorem component_region {S X R Y C : Finset (Fin n)}
    (hR : ∀ u ∈ R, ∀ w, G.Adj u w → w ∈ R ∨ w ∈ Y)
    (hY : ∀ w ∈ Y, w ∈ S → w ∈ X) (hC : C ∈ components G (S \ X)) :
    C ⊆ R ∨ Disjoint C R := by
  classical
  obtain ⟨hCU, _, hconn⟩ := mem_components G hC
  have hclosed : ClosedIn G (S \ X) (R ∩ (S \ X)) := by
    intro u hu w hw hadj
    obtain ⟨huR, _⟩ := Finset.mem_inter.mp hu
    refine Finset.mem_inter.mpr ⟨?_, hw⟩
    rcases hR u huR w hadj with h | h
    · exact h
    · exact False.elim ((Finset.mem_sdiff.mp hw).2 (hY w h (Finset.mem_sdiff.mp hw).1))
  rcases connected_subset_or_disjoint G hCU hconn hclosed with h | h
  · exact Or.inl (h.trans Finset.inter_subset_left)
  · right
    apply Finset.disjoint_left.mpr
    intro u huC huR
    exact Finset.disjoint_left.mp h huC (Finset.mem_inter.mpr ⟨huR, hCU huC⟩)

theorem card_inter_of_sdiff {S T : Finset (Fin n)} (h : S.card < 2 * (S \ T).card) :
    2 * (S ∩ T).card < S.card := by
  have := Finset.card_sdiff_add_card_inter S T
  omega

/-- Balanced separators of at most three vertices inside a piece. -/
theorem Piece.separator {T A : Finset (Fin n)} (h : Piece G T A) (hA : A.card ≤ 3) :
    ∀ S : Finset (Fin n), 2 * (S \ T).card ≤ S.card →
      ∃ X ⊆ S, X.card ≤ 3 ∧ ∀ C ∈ components G (S \ X), 2 * C.card ≤ S.card := by
  classical
  induction h with
  | empty A =>
    intro S hS
    refine ⟨∅, Finset.empty_subset _, by simp, ?_⟩
    intro C hC
    have hCS : C ⊆ S := (mem_components G hC).1.trans Finset.sdiff_subset
    have h1 := Finset.card_le_card hCS
    simp only [Finset.sdiff_empty] at hS
    omega
  | @union T₁ T₂ A h₁ h₂ ih₁ ih₂ =>
    intro S hS
    by_cases hS₁ : 2 * (S \ T₁).card ≤ S.card
    · exact ih₁ hA S hS₁
    by_cases hS₂ : 2 * (S \ T₂).card ≤ S.card
    · exact ih₂ hA S hS₂
    have hi₁ := card_inter_of_sdiff (by omega : S.card < 2 * (S \ T₁).card)
    have hi₂ := card_inter_of_sdiff (by omega : S.card < 2 * (S \ T₂).card)
    refine ⟨A ∩ S, Finset.inter_subset_right,
      (Finset.card_le_card Finset.inter_subset_left).trans hA, ?_⟩
    intro C hC
    have hY : ∀ w ∈ A, w ∈ S → w ∈ A ∩ S := fun w hw hwS => Finset.mem_inter.mpr ⟨hw, hwS⟩
    have hCS : C ⊆ S := (mem_components G hC).1.trans Finset.sdiff_subset
    rcases component_region G h₁.edges hY hC with hc₁ | hd₁
    · have := Finset.card_le_card (Finset.subset_inter hCS hc₁)
      omega
    rcases component_region G h₂.edges hY hC with hc₂ | hd₂
    · have := Finset.card_le_card (Finset.subset_inter hCS hc₂)
      omega
    have hsub : C ⊆ S \ (T₁ ∪ T₂) := by
      intro u hu
      refine Finset.mem_sdiff.mpr ⟨hCS hu, ?_⟩
      rw [Finset.mem_union, not_or]
      exact ⟨Finset.disjoint_left.mp hd₁ hu, Finset.disjoint_left.mp hd₂ hu⟩
    have := Finset.card_le_card hsub
    omega
  | @node v T A hcard hv hT ih =>
    intro S hS
    by_cases hS' : 2 * (S \ T).card ≤ S.card
    · exact ih hcard S hS'
    have hi := card_inter_of_sdiff (by omega : S.card < 2 * (S \ T).card)
    refine ⟨insert v A ∩ S, Finset.inter_subset_right,
      (Finset.card_le_card Finset.inter_subset_left).trans hcard, ?_⟩
    intro C hC
    have hY : ∀ w ∈ insert v A, w ∈ S → w ∈ insert v A ∩ S :=
      fun w hw hwS => Finset.mem_inter.mpr ⟨hw, hwS⟩
    have hCU := (mem_components G hC).1
    have hCS : C ⊆ S := hCU.trans Finset.sdiff_subset
    rcases component_region G hT.edges hY hC with hc | hd
    · have := Finset.card_le_card (Finset.subset_inter hCS hc)
      omega
    have hsub : C ⊆ S \ insert v T := by
      intro u hu
      refine Finset.mem_sdiff.mpr ⟨hCS hu, ?_⟩
      intro hmem
      rcases Finset.mem_insert.mp hmem with rfl | hmem
      · exact (Finset.mem_sdiff.mp (hCU hu)).2
          (Finset.mem_inter.mpr ⟨Finset.mem_insert_self _ _, hCS hu⟩)
      · exact Finset.disjoint_left.mp hd hu hmem
    have := Finset.card_le_card hsub
    omega
  | @mono T A A' _ hAA' ih =>
    intro S hS
    exact ih ((Finset.card_le_card hAA').trans hA) S hS

variable (G) in

/-- Recursive balanced separators of at most three vertices give width
`O(√|U|)`. -/
theorem separator_section_decomposition (U : Finset (Fin n))
    (hsep : ∀ S ⊆ U, ∃ X ⊆ S, X.card ≤ 3 ∧
      ∀ C ∈ components G (S \ X), 2 * C.card ≤ S.card) :
    ∃ P : SectionDecomposition G U,
      P.toBagPath.WidthAtMost (12 * Real.sqrt (U.card : ℝ)) := by
  have go : ∀ m : ℕ, ∀ S : Finset (Fin n), S.card = m → S ⊆ U →
      ∃ P : SectionDecomposition G S,
        P.toBagPath.WidthAtMost (12 * Real.sqrt (S.card : ℝ)) := by
    intro m
    induction m using Nat.strong_induction_on with
    | h m ih =>
      intro S hm hSU
      obtain ⟨X, hXS, hX, hbal⟩ := hsep S hSU
      have hroot := Real.sqrt_nonneg (S.card : ℝ)
      obtain ⟨P, hP⟩ := section_of_components G (S \ X)
        (show -1 ≤ 9 * Real.sqrt (S.card : ℝ) by linarith) (by
          intro C hC
          have hc := hbal C hC
          have hne := Finset.card_pos.mpr (mem_components G hC).2.2.1
          have hlt : C.card < m := by omega
          have hCS : C ⊆ U := (mem_components G hC).1.trans (Finset.sdiff_subset.trans hSU)
          obtain ⟨Q, hQ⟩ := ih _ hlt C rfl hCS
          refine ⟨Q, hQ.mono ?_⟩
          have := sqrt_half_bound hc
          linarith)
      have hwidth := (hold_width P X hP).mono
        (show 9 * Real.sqrt (S.card : ℝ) + (X.card : ℝ) ≤ 12 * Real.sqrt (S.card : ℝ) by
          by_cases hS : S.Nonempty
          · have h1 : (1 : ℝ) ≤ Real.sqrt (S.card : ℝ) := by
              have : (1 : ℝ) ≤ S.card := by exact_mod_cast Finset.card_pos.mpr hS
              simpa using Real.sqrt_le_sqrt this
            have : (X.card : ℝ) ≤ 3 := by exact_mod_cast hX
            linarith
          · have hS0 : S = ∅ := Finset.not_nonempty_iff_eq_empty.mp hS
            subst hS0
            have hX0 : X = ∅ := Finset.subset_empty.mp hXS
            subst hX0
            simp)
      have heq : (S \ X) ∪ X = S := Finset.sdiff_union_of_subset hXS
      have h : ∃ Q : SectionDecomposition G ((S \ X) ∪ X),
          Q.toBagPath.WidthAtMost (12 * Real.sqrt (S.card : ℝ)) := ⟨P.hold X, hwidth⟩
      rw [heq] at h
      exact h
  exact go _ U rfl Finset.Subset.rfl

/-- Every piece hanging from at most three vertices has width `O(√|T|)`. -/
theorem Piece.section_decomposition {T A : Finset (Fin n)} (h : Piece G T A)
    (hA : A.card ≤ 3) :
    ∃ P : SectionDecomposition G T,
      P.toBagPath.WidthAtMost (12 * Real.sqrt (T.card : ℝ)) := by
  apply separator_section_decomposition G T
  intro S hS
  apply h.separator hA S
  rw [Finset.sdiff_eq_empty_iff_subset.mpr hS]
  simp

end T2
end CubicPathwidth