CubicPathwidth.SectionAssembly

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

import CubicPathwidth.BoundaryInduction

/-!
# Holding a boundary and appending a separate component

These constructions include vertex/edge coverage, the interval axiom, and
the exact final bag. Appending a component while holding the boundary takes
the maximum of the two section widths, independent of recursion depth.
-/

noncomputable section
namespace CubicPathwidth
namespace SectionDecomposition

variable {n : ℕ} {G : SimpleGraph (Fin n)} {U V : Finset (Fin n)}

/-- Add X to every bag, covering the graph induced by U union X. -/
def hold (P : SectionDecomposition G U) (X : Finset (Fin n)) :
    SectionDecomposition G (U ∪ X) where
  lastIndex := P.lastIndex
  bag := fun i => P.bag i ∪ X
  interval := by
    intro i j k hij hjk hk v hv
    by_cases hx : v ∈ X
    · exact Finset.mem_union_right _ hx
    · have hi := (Finset.mem_union.mp hv.1).resolve_right hx
      have hk' := (Finset.mem_union.mp hv.2).resolve_right hx
      exact Finset.mem_union_left _ (P.interval i j k hij hjk hk v ⟨hi, hk'⟩)
  bag_subset := by
    intro i hi v hv
    rcases Finset.mem_union.mp hv with hv | hv
    · exact Finset.mem_union_left _ (P.bag_subset i hi hv)
    · exact Finset.mem_union_right _ hv
  vertex_covered := by
    intro v hv
    rcases Finset.mem_union.mp hv with hv | hv
    · obtain ⟨i, hi, hvi⟩ := P.vertex_covered v hv
      exact ⟨i, hi, Finset.mem_union_left _ hvi⟩
    · exact ⟨0, Nat.zero_le _, Finset.mem_union_right _ hv⟩
  edge_covered := by
    intro u hu v hv huv
    by_cases huX : u ∈ X
    · by_cases hvX : v ∈ X
      · exact ⟨0, Nat.zero_le _, Finset.mem_union_right _ huX, Finset.mem_union_right _ hvX⟩
      · have hvU := (Finset.mem_union.mp hv).resolve_right hvX
        obtain ⟨i, hi, hvi⟩ := P.vertex_covered v hvU
        exact ⟨i, hi, Finset.mem_union_right _ huX, Finset.mem_union_left _ hvi⟩
    · have huU := (Finset.mem_union.mp hu).resolve_right huX
      by_cases hvX : v ∈ X
      · obtain ⟨i, hi, hui⟩ := P.vertex_covered u huU
        exact ⟨i, hi, Finset.mem_union_left _ hui, Finset.mem_union_right _ hvX⟩
      · have hvU := (Finset.mem_union.mp hv).resolve_right hvX
        obtain ⟨i, hi, hui, hvi⟩ := P.edge_covered u huU v hvU huv
        exact ⟨i, hi, Finset.mem_union_left _ hui, Finset.mem_union_left _ hvi⟩

theorem hold_width (P : SectionDecomposition G U) (X : Finset (Fin n))
    {w : ℝ} (hP : P.toBagPath.WidthAtMost w) :
    (P.hold X).toBagPath.WidthAtMost (w + (X.card : ℝ)) := by
  intro i hi
  have hc : ((P.bag i ∪ X).card : ℝ) ≤ (P.bag i).card + X.card := by
    exact_mod_cast Finset.card_union_le (P.bag i) X
  have hw := hP i hi
  change ((P.bag i ∪ X).card : ℝ) ≤ _
  linarith

theorem hold_bag (P : SectionDecomposition G U) (X : Finset (Fin n)) (i : ℕ) :
    (P.hold X).bag i = P.bag i ∪ X := rfl

/-- Two compatible sections cover their union when every edge of the union
belongs to at least one section. -/
def concat (P : SectionDecomposition G U) (Q : SectionDecomposition G V)
    (hc : BagPath.Compatible P.toBagPath Q.toBagPath)
    (he : ∀ u ∈ U ∪ V, ∀ v ∈ U ∪ V, G.Adj u v →
      (u ∈ U ∧ v ∈ U) ∨ (u ∈ V ∧ v ∈ V)) :
    SectionDecomposition G (U ∪ V) where
  toBagPath := P.toBagPath.concat Q.toBagPath hc
  bag_subset := by
    intro i hi v hv
    change i ≤ P.lastIndex + Q.lastIndex + 1 at hi
    by_cases hip : i ≤ P.lastIndex
    · rw [BagPath.concat_bag_left _ _ _ _ hip] at hv
      exact Finset.mem_union_left _ (P.bag_subset i hip hv)
    · have hiq : i - (P.lastIndex + 1) ≤ Q.lastIndex := by omega
      change v ∈ (if i ≤ P.lastIndex then P.bag i else Q.bag (i - (P.lastIndex + 1))) at hv
      rw [ite_eq_right hip] at hv
      exact Finset.mem_union_right _ (Q.bag_subset _ hiq hv)
  vertex_covered := by
    intro v hv
    rcases Finset.mem_union.mp hv with hv | hv
    · obtain ⟨i, hi, hvi⟩ := P.vertex_covered v hv
      exact ⟨i, by change i ≤ P.lastIndex + Q.lastIndex + 1; omega,
        (BagPath.concat_bag_left _ _ _ _ hi).symm ▸ hvi⟩
    · obtain ⟨i, hi, hvi⟩ := Q.vertex_covered v hv
      exact ⟨P.lastIndex + 1 + i, by change _ ≤ P.lastIndex + Q.lastIndex + 1; omega,
        (BagPath.concat_bag_right _ _ _ _).symm ▸ hvi⟩
  edge_covered := by
    intro u hu v hv huv
    rcases he u hu v hv huv with ⟨huU, hvU⟩ | ⟨huV, hvV⟩
    · obtain ⟨i, hi, hui, hvi⟩ := P.edge_covered u huU v hvU huv
      refine ⟨i, by change i ≤ P.lastIndex + Q.lastIndex + 1; omega, ?_, ?_⟩
      · exact (BagPath.concat_bag_left _ _ _ _ hi).symm ▸ hui
      · exact (BagPath.concat_bag_left _ _ _ _ hi).symm ▸ hvi
    · obtain ⟨i, hi, hui, hvi⟩ := Q.edge_covered u huV v hvV huv
      refine ⟨P.lastIndex + 1 + i, by change _ ≤ P.lastIndex + Q.lastIndex + 1; omega, ?_, ?_⟩
      · exact (BagPath.concat_bag_right _ _ _ _).symm ▸ hui
      · exact (BagPath.concat_bag_right _ _ _ _).symm ▸ hvi

theorem concat_width (P : SectionDecomposition G U) (Q : SectionDecomposition G V)
    (hc) (he) {a b : ℝ} (hP : P.toBagPath.WidthAtMost a) (hQ : Q.toBagPath.WidthAtMost b) :
    (P.concat Q hc he).toBagPath.WidthAtMost (max a b) :=
  BagPath.concat_width hc hP hQ

theorem concat_last (P : SectionDecomposition G U) (Q : SectionDecomposition G V) (hc) (he) :
    (P.concat Q hc he).bag (P.concat Q hc he).lastIndex = Q.bag Q.lastIndex :=
  BagPath.concat_last P.toBagPath Q.toBagPath hc

/-- Add the prescribed boundary to every bag, then end at exactly X. -/
theorem ending_hold (P : SectionDecomposition G U) (X : Finset (Fin n))
    {w : ℝ} (hP : P.toBagPath.WidthAtMost w) :
    HasEndingSection G (U ∪ X) X (w + (X.card : ℝ)) := by
  let Q := P.hold X
  have hx : X ⊆ Q.bag Q.lastIndex := Finset.subset_union_right
  exact ⟨Q.endAtSubset X hx, endAtSubset_last _ _ _,
    endAtSubset_width _ _ _ (hold_width P X hP)⟩

/-- Append a disjoint component whose neighbours in the old section all lie
in its final bag X. This is the exact tree-component assembly step. -/
theorem append_component (P : SectionDecomposition G U) (Q : SectionDecomposition G V)
    (X : Finset (Fin n)) (hX : X ⊆ U) (hdis : Disjoint U V)
    (hend : P.bag P.lastIndex = X)
    (hsep : ∀ v ∈ V, ∀ u ∈ U, G.Adj v u → u ∈ X)
    {a b : ℝ} (hP : P.toBagPath.WidthAtMost a) (hQ : Q.toBagPath.WidthAtMost b) :
    HasEndingSection G (U ∪ V) X (max a (b + (X.card : ℝ))) := by
  classical
  let R := Q.hold X
  have hc : BagPath.Compatible P.toBagPath R.toBagPath := by
    intro v i j hi hj hvi hvj
    have hvU := P.bag_subset i hi hvi
    have hvX : v ∈ X := by
      rcases Finset.mem_union.mp hvj with hvQ | hvX
      · exact False.elim (Finset.disjoint_left.mp hdis hvU (Q.bag_subset j hj hvQ))
      · exact hvX
    exact ⟨hend.symm ▸ hvX, Finset.mem_union_right _ hvX⟩
  have he : ∀ u ∈ U ∪ (V ∪ X), ∀ v ∈ U ∪ (V ∪ X), G.Adj u v →
      (u ∈ U ∧ v ∈ U) ∨ (u ∈ V ∪ X ∧ v ∈ V ∪ X) := by
    intro u hu v hv huv
    by_cases huU : u ∈ U
    · by_cases hvU : v ∈ U
      · exact Or.inl ⟨huU, hvU⟩
      · have hvVX := (Finset.mem_union.mp hv).resolve_left hvU
        have hvV : v ∈ V := (Finset.mem_union.mp hvVX).resolve_right (fun h => hvU (hX h))
        exact Or.inr ⟨Finset.mem_union_right _ (hsep v hvV u huU huv.symm), hvVX⟩
    · have huVX := (Finset.mem_union.mp hu).resolve_left huU
      have huV : u ∈ V := (Finset.mem_union.mp huVX).resolve_right (fun h => huU (hX h))
      by_cases hvU : v ∈ U
      · exact Or.inr ⟨huVX, Finset.mem_union_right _ (hsep u huV v hvU huv)⟩
      · exact Or.inr ⟨huVX, (Finset.mem_union.mp hv).resolve_left hvU⟩
  let S := P.concat R hc he
  have hx : X ⊆ S.bag S.lastIndex := by
    rw [concat_last]
    exact Finset.subset_union_right
  have hs : HasEndingSection G (U ∪ (V ∪ X)) X (max a (b + (X.card : ℝ))) :=
    ⟨S.endAtSubset X hx, endAtSubset_last _ _ _,
      endAtSubset_width _ _ _ (concat_width P R hc he hP (hold_width Q X hQ))⟩
  have hunion : U ∪ (V ∪ X) = U ∪ V := by
    ext v
    simp only [Finset.mem_union]
    constructor
    · rintro (h | h | h)
      · exact Or.inl h
      · exact Or.inr h
      · exact Or.inl (hX h)
    · rintro (h | h)
      · exact Or.inl h
      · exact Or.inr (Or.inl h)
  simpa only [hunion] using hs

end SectionDecomposition
end CubicPathwidth