CubicPathwidth.T4.BasicGlue

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

import CubicPathwidth.T4.ProcessDefs

/-!
# Torso components as sections, and gluing them (`lem:basic`, first case)

Helper facts for `CubicPathwidth/T4/Basic.lean`.

* `coreTorso_eq_induced`: for `U ⊆ B`, the torso of `(F \ (B \ U), U)` is the induced
  torso `inducedOnFin (tgraph G F B) U`. In particular a torso component `C` gives
  the relabelled graph of `ComponentClaim`, and the whole core gives `coreTorso G F B`.
* Degree and weight bounds: a vertex of the relabelled component has torso degree at
  most its torso degree in `(F, B)`, so `degreeWeight` is at most `∑_{v ∈ U} b (tdeg v)`.
* `section_union`, `glueSections`: sections on disjoint pieces with no edges between
  them glue into a section on their union, at the maximum width.
* `unliftSection`: a section on `U` is a path decomposition of `inducedOnFin G U`.
-/

noncomputable section

namespace CubicPathwidth
namespace T4
namespace BasicAux

open T2 SectionDecomposition

variable {n : ℕ}

/-! ## Adjacency of the torso and its relabelled component -/

theorem tgraph_adj_iff (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (u v : Fin n) :
    (tgraph G F B).Adj u v ↔ u ≠ v ∧ u ∈ B ∧ v ∈ B ∧ (G.Adj u v ∨
      ∃ T ∈ components G (F \ B), u ∈ attachment G B T ∧ v ∈ attachment G B T) :=
  Iff.rfl

theorem diff_diff_eq_of_subset {F B U : Finset (Fin n)} (hU : U ⊆ B) :
    (F \ (B \ U)) \ U = F \ B := by
  ext x
  have hx : x ∈ U → x ∈ B := fun h => hU h
  simp only [Finset.mem_sdiff]
  tauto

theorem mem_attachment_inner (G : SimpleGraph (Fin n)) {B U : Finset (Fin n)}
    (hU : U ⊆ B) {x : Fin n} (hx : x ∈ U) (T : Finset (Fin n)) :
    x ∈ attachment G U T ↔ x ∈ attachment G B T := by
  rw [mem_attachment G, mem_attachment G]
  exact ⟨fun h => ⟨hU hx, h.2⟩, fun h => ⟨hx, h.2⟩⟩

theorem coreTorso_adj_induced (G : SimpleGraph (Fin n)) (F B U : Finset (Fin n))
    (hU : U ⊆ B) (i j : Fin U.card) :
    (coreTorso G (F \ (B \ U)) U).Adj i j ↔
      (tgraph G F B).Adj (enumerate U i) (enumerate U j) := by
  have hi : enumerate U i ∈ U := (mem_iff_enumerate U _).mpr ⟨i, rfl⟩
  have hj : enumerate U j ∈ U := (mem_iff_enumerate U _).mpr ⟨j, rfl⟩
  have hne : i ≠ j ↔ enumerate U i ≠ enumerate U j := (enumerate U).injective.ne_iff.symm
  rw [tgraph_adj_iff]
  show (i ≠ j ∧ (G.Adj (enumerate U i) (enumerate U j) ∨
      ∃ T ∈ components G ((F \ (B \ U)) \ U),
        enumerate U i ∈ attachment G U T ∧ enumerate U j ∈ attachment G U T)) ↔ _
  rw [diff_diff_eq_of_subset hU, hne]
  simp only [mem_attachment_inner G hU hi, mem_attachment_inner G hU hj]
  constructor
  · rintro ⟨hne', h⟩
    exact ⟨hne', hU hi, hU hj, h⟩
  · rintro ⟨hne', -, -, h⟩
    exact ⟨hne', h⟩

/-- The torso of a component `U ⊆ B`, relabelled onto `Fin U.card`, is the induced
torso of the state `(F, B)`. -/
theorem coreTorso_eq_induced (G : SimpleGraph (Fin n)) (F B U : Finset (Fin n))
    (hU : U ⊆ B) :
    coreTorso G (F \ (B \ U)) U = inducedOnFin (tgraph G F B) U := by
  ext i j
  exact coreTorso_adj_induced G F B U hU i j

/-! ## Degrees and weights -/

theorem sum_enumerate (U : Finset (Fin n)) (f : Fin n → ℝ) :
    ∑ i : Fin U.card, f (enumerate U i) = ∑ v ∈ U, f v := by
  rw [← Finset.sum_coe_sort U f]
  exact Equiv.sum_comp U.equivFin.symm (fun x : U => f x.val)

open scoped Classical in

theorem degree_inducedOnFin_le (G' : SimpleGraph (Fin n)) (U : Finset (Fin n))
    (i : Fin U.card) :
    (inducedOnFin G' U).degree i ≤ G'.degree (enumerate U i) := by
  classical
  have hsub : ((inducedOnFin G' U).neighborFinset i).image (enumerate U) ⊆
      G'.neighborFinset (enumerate U i) := by
    intro u hu
    obtain ⟨w, hw, rfl⟩ := Finset.mem_image.mp hu
    exact (G'.mem_neighborFinset _ _).mpr (((inducedOnFin G' U).mem_neighborFinset i w).mp hw)
  calc (inducedOnFin G' U).degree i = ((inducedOnFin G' U).neighborFinset i).card := rfl
    _ = (((inducedOnFin G' U).neighborFinset i).image (enumerate U)).card :=
        (Finset.card_image_of_injective _ (enumerate U).injective).symm
    _ ≤ (G'.neighborFinset (enumerate U i)).card := Finset.card_le_card hsub
    _ = G'.degree (enumerate U i) := rfl

open scoped Classical in

theorem tdeg_eq_degree (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (v : Fin n) :
    tdeg G F B v = (tgraph G F B).degree v := rfl

open scoped Classical in

/-- A vertex of the relabelled component has degree at most its torso degree. -/
theorem degree_coreTorso_le (G : SimpleGraph (Fin n)) (F B U : Finset (Fin n))
    (hU : U ⊆ B) (i : Fin U.card) :
    (coreTorso G (F \ (B \ U)) U).degree i ≤ tdeg G F B (enumerate U i) := by
  rw [tdeg_eq_degree, coreTorso_eq_induced G F B U hU]
  exact degree_inducedOnFin_le _ _ _

open scoped Classical in

theorem maxDegreeAtMost_coreTorso (G : SimpleGraph (Fin n)) (F B U : Finset (Fin n))
    (hU : U ⊆ B) {k : ℕ} (hk : ∀ v ∈ U, tdeg G F B v ≤ k) :
    MaxDegreeAtMost k (coreTorso G (F \ (B \ U)) U) := by
  unfold MaxDegreeAtMost
  intro i
  exact (degree_coreTorso_le G F B U hU i).trans
    (hk _ ((mem_iff_enumerate U _).mpr ⟨i, rfl⟩))

open scoped Classical in

/-- The weight of the relabelled component is at most `∑_{v ∈ U} b (tdeg v)`. -/
theorem degreeWeight_coreTorso_le {b : ℕ → ℝ} (hb : BootProps b) (G : SimpleGraph (Fin n))
    (F B U : Finset (Fin n)) (hU : U ⊆ B) :
    degreeWeight (coreTorso G (F \ (B \ U)) U) b ≤ ∑ v ∈ U, b (tdeg G F B v) := by
  rw [← sum_enumerate U (fun v => b (tdeg G F B v))]
  unfold degreeWeight
  apply Finset.sum_le_sum
  intro i _
  exact hb.monotone (degree_coreTorso_le G F B U hU i)

/-! ## Sections on components and their union -/

/-- The empty section. -/
def emptySection (G : SimpleGraph (Fin n)) : SectionDecomposition G ∅ where
  lastIndex := 0
  bag := fun _ => ∅
  interval := by
    intro i j k _ _ _ v hv
    simp at hv
  bag_subset := by
    intro i _ v hv
    simp at hv
  vertex_covered := by
    intro v hv
    simp at hv
  edge_covered := by
    intro u hu
    simp at hu

theorem emptySection_width (G : SimpleGraph (Fin n)) {w : ℝ} (hw : -1 ≤ w) :
    (emptySection G).toBagPath.WidthAtMost w := by
  intro i _
  change ((∅ : Finset (Fin n)).card : ℝ) ≤ w + 1
  simp only [Finset.card_empty, Nat.cast_zero]
  linarith

/-- Two sections on disjoint sets with no edges between them give a section on the
union, whose width is the maximum of the two widths. -/
theorem section_union (G : SimpleGraph (Fin n)) {C U : Finset (Fin n)}
    (P : SectionDecomposition G C) (Q : SectionDecomposition G U)
    (hdisj : Disjoint C U) (hno : ∀ x ∈ C, ∀ y ∈ U, ¬ G.Adj x y) {a b : ℝ}
    (ha : P.toBagPath.WidthAtMost a) (hb : Q.toBagPath.WidthAtMost b) :
    ∃ R : SectionDecomposition G (C ∪ U), R.toBagPath.WidthAtMost (max a b) := by
  have compat : BagPath.Compatible P.toBagPath Q.toBagPath := by
    intro v i j hi hj hvi hvj
    exact (Finset.disjoint_left.mp hdisj (P.bag_subset i hi hvi)
      (Q.bag_subset j hj hvj)).elim
  refine ⟨{ toBagPath := P.toBagPath.concat Q.toBagPath compat
            bag_subset := ?_
            vertex_covered := ?_
            edge_covered := ?_ }, BagPath.concat_width compat ha hb⟩
  · intro i hi v hv
    by_cases h : i ≤ P.lastIndex
    · rw [BagPath.concat_bag_left _ _ _ i h] at hv
      exact Finset.mem_union_left _ (P.bag_subset i h hv)
    · obtain ⟨j, rfl⟩ : ∃ j, i = P.lastIndex + 1 + j := ⟨i - (P.lastIndex + 1), by omega⟩
      rw [BagPath.concat_bag_right _ _ _ j] at hv
      have hj : j ≤ Q.lastIndex := by
        have : P.lastIndex + 1 + j ≤ P.lastIndex + Q.lastIndex + 1 := hi
        omega
      exact Finset.mem_union_right _ (Q.bag_subset j hj hv)
  · intro v hv
    rcases Finset.mem_union.mp hv with h | h
    · obtain ⟨i, hi, hvi⟩ := P.vertex_covered v h
      refine ⟨i, ?_, ?_⟩
      · change i ≤ P.lastIndex + Q.lastIndex + 1
        omega
      · rw [BagPath.concat_bag_left _ _ _ i hi]
        exact hvi
    · obtain ⟨j, hj, hvj⟩ := Q.vertex_covered v h
      refine ⟨P.lastIndex + 1 + j, ?_, ?_⟩
      · change P.lastIndex + 1 + j ≤ P.lastIndex + Q.lastIndex + 1
        omega
      · rw [BagPath.concat_bag_right _ _ _ j]
        exact hvj
  · intro u hu v hv huv
    rcases Finset.mem_union.mp hu with hu' | hu' <;>
      rcases Finset.mem_union.mp hv with hv' | hv'
    · obtain ⟨i, hi, hui, hvi⟩ := P.edge_covered u hu' v hv' huv
      refine ⟨i, ?_, ?_, ?_⟩
      · change i ≤ P.lastIndex + Q.lastIndex + 1
        omega
      · rw [BagPath.concat_bag_left _ _ _ i hi]
        exact hui
      · rw [BagPath.concat_bag_left _ _ _ i hi]
        exact hvi
    · exact (hno u hu' v hv' huv).elim
    · exact (hno v hv' u hu' huv.symm).elim
    · obtain ⟨j, hj, huj, hvj⟩ := Q.edge_covered u hu' v hv' huv
      refine ⟨P.lastIndex + 1 + j, ?_, ?_, ?_⟩
      · change P.lastIndex + 1 + j ≤ P.lastIndex + Q.lastIndex + 1
        omega
      · rw [BagPath.concat_bag_right _ _ _ j]
        exact huj
      · rw [BagPath.concat_bag_right _ _ _ j]
        exact hvj

/-- Glue sections over a finite family of pairwise disjoint pieces. Each piece is
closed under the adjacency of `G`, so there are no edges between different pieces. -/
theorem glueSections (G : SimpleGraph (Fin n)) {w : ℝ} (hw : -1 ≤ w)
    (𝒞 : Finset (Finset (Fin n))) :
    ∀ U : Finset (Fin n), 𝒞.biUnion id = U →
      (∀ C ∈ 𝒞, ∀ u ∈ C, ∀ v, G.Adj u v → v ∈ C) →
      (∀ C ∈ 𝒞, ∀ D ∈ 𝒞, C ≠ D → Disjoint C D) →
      (∀ C ∈ 𝒞, ∃ P : SectionDecomposition G C, P.toBagPath.WidthAtMost w) →
      ∃ P : SectionDecomposition G U, P.toBagPath.WidthAtMost w := by
  classical
  induction 𝒞 using Finset.induction_on with
  | empty =>
    intro U hU _ _ _
    subst hU
    rw [Finset.biUnion_empty]
    exact ⟨emptySection G, emptySection_width G hw⟩
  | @insert C 𝒞' hC ih =>
    intro U hU hcl hdis hP
    subst hU
    have hcl' : ∀ D ∈ 𝒞', ∀ u ∈ D, ∀ v, G.Adj u v → v ∈ D :=
      fun D hD => hcl D (Finset.mem_insert_of_mem hD)
    have hdis' : ∀ D ∈ 𝒞', ∀ E ∈ 𝒞', D ≠ E → Disjoint D E :=
      fun D hD E hE hne =>
        hdis D (Finset.mem_insert_of_mem hD) E (Finset.mem_insert_of_mem hE) hne
    have hP' : ∀ D ∈ 𝒞', ∃ P : SectionDecomposition G D, P.toBagPath.WidthAtMost w :=
      fun D hD => hP D (Finset.mem_insert_of_mem hD)
    obtain ⟨Q, hQ⟩ := ih (𝒞'.biUnion id) rfl hcl' hdis' hP'
    obtain ⟨P, hPw⟩ := hP C (Finset.mem_insert_self _ _)
    have hdisj : Disjoint C (𝒞'.biUnion id) := by
      rw [Finset.disjoint_biUnion_right]
      intro D hD
      exact hdis C (Finset.mem_insert_self _ _) D (Finset.mem_insert_of_mem hD)
        (fun h => hC (by rw [h]; exact hD))
    have hno : ∀ x ∈ C, ∀ y ∈ 𝒞'.biUnion id, ¬ G.Adj x y := by
      intro x hx y hy hxy
      have hyC := hcl C (Finset.mem_insert_self _ _) x hx y hxy
      exact Finset.disjoint_left.mp hdisj hyC hy
    obtain ⟨R, hR⟩ := section_union G P Q hdisj hno hPw hQ
    rw [Finset.biUnion_insert]
    exact ⟨R, hR.mono (max_le le_rfl le_rfl)⟩

/-! ## Sections as path decompositions of induced graphs -/

theorem mem_boundaryPreimage_iff (U X : Finset (Fin n)) (v : Fin U.card) :
    v ∈ boundaryPreimage U X ↔ enumerate U v ∈ X := by
  simp [boundaryPreimage]

/-- A section on `U` is a path decomposition of the induced graph `G[U]`. -/
def unliftSection {G : SimpleGraph (Fin n)} {U : Finset (Fin n)}
    (P : SectionDecomposition G U) : PathDecomposition (inducedOnFin G U) where
  lastIndex := P.lastIndex
  bag := fun i => boundaryPreimage U (P.bag i.val)
  vertex_covered := by
    intro v
    have hv : enumerate U v ∈ U := (mem_iff_enumerate U _).mpr ⟨v, rfl⟩
    obtain ⟨i, hi, hvi⟩ := P.vertex_covered _ hv
    exact ⟨⟨i, by omega⟩, (mem_boundaryPreimage_iff U _ v).mpr hvi⟩
  edge_covered := by
    intro u v huv
    have hu : enumerate U u ∈ U := (mem_iff_enumerate U _).mpr ⟨u, rfl⟩
    have hv : enumerate U v ∈ U := (mem_iff_enumerate U _).mpr ⟨v, rfl⟩
    have huv' : G.Adj (enumerate U u) (enumerate U v) := huv
    obtain ⟨i, hi, hui, hvi⟩ := P.edge_covered _ hu _ hv huv'
    exact ⟨⟨i, by omega⟩, (mem_boundaryPreimage_iff U _ u).mpr hui,
      (mem_boundaryPreimage_iff U _ v).mpr hvi⟩
  interval := by
    intro i j k hij hjk v hv
    have hv' : enumerate U v ∈ P.bag i.val ∧ enumerate U v ∈ P.bag k.val :=
      ⟨(mem_boundaryPreimage_iff U _ v).mp hv.1, (mem_boundaryPreimage_iff U _ v).mp hv.2⟩
    exact (mem_boundaryPreimage_iff U _ v).mpr
      (P.interval i.val j.val k.val (Fin.le_def.mp hij) (Fin.le_def.mp hjk)
        (Nat.le_of_lt_succ k.isLt) _ hv')

theorem unliftSection_width {G : SimpleGraph (Fin n)} {U : Finset (Fin n)}
    (P : SectionDecomposition G U) {w : ℝ} (hP : P.toBagPath.WidthAtMost w) :
    (unliftSection P).WidthAtMost w := by
  intro i
  have hi : i.val ≤ P.lastIndex := Nat.le_of_lt_succ i.isLt
  change ((boundaryPreimage U (P.bag i.val)).card : ℝ) ≤ w + 1
  rw [boundaryPreimage_card U _ (P.bag_subset i.val hi)]
  exact hP i.val hi

theorem hasPathwidthAtMost_of_section {G : SimpleGraph (Fin n)} {U : Finset (Fin n)}
    {w : ℝ} (P : SectionDecomposition G U) (hP : P.toBagPath.WidthAtMost w) :
    HasPathwidthAtMost (inducedOnFin G U) w :=
  ⟨unliftSection P, unliftSection_width P hP⟩

theorem section_of_hasPathwidth {G : SimpleGraph (Fin n)} {U : Finset (Fin n)}
    {w W : ℝ} (h : HasPathwidthAtMost (inducedOnFin G U) w) (hw : w ≤ W) :
    ∃ P : SectionDecomposition G U, P.toBagPath.WidthAtMost W := by
  obtain ⟨D, hD⟩ := h
  exact ⟨lift G U D, (lift_width G U D hD).mono hw⟩

end BasicAux
end T4
end CubicPathwidth