CubicPathwidth.CorePieces

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

import CubicPathwidth.PseudotreeDecomposition

/-! Components outside the core's branch vertices have at most two attachments. -/

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

def branchVertices (C : Finset (Fin n)) : Finset (Fin n) :=
  C.filter (fun v => (sectionNeighbors G C v).card = 3)

def attachment (B T : Finset (Fin n)) : Finset (Fin n) :=
  T.biUnion (sectionNeighbors G B)

theorem mem_attachment {B T : Finset (Fin n)} {v : Fin n} :
    v ∈ attachment G B T ↔ v ∈ B ∧ ∃ u ∈ T, G.Adj v u := by
  simp only [attachment, Finset.mem_biUnion, mem_sectionNeighbors]
  constructor
  · rintro ⟨u, hu, hv, huv⟩
    exact ⟨hv, u, hu, huv.symm⟩
  · rintro ⟨hv, u, hu, hvu⟩
    exact ⟨u, hu, hv, hvu.symm⟩

theorem attachment_subset (B T : Finset (Fin n)) : attachment G B T ⊆ B :=
  fun _ h => (mem_attachment G).mp h |>.1

theorem attachment_card_le (B T : Finset (Fin n)) :
    (attachment G B T).card ≤ incidence G T B := Finset.card_biUnion_le

theorem incidence_mono_right (U : Finset (Fin n)) {V W : Finset (Fin n)} (h : V ⊆ W) :
    incidence G U V ≤ incidence G U W :=
  Finset.sum_le_sum (fun v _ => Finset.card_le_card (sectionNeighbors_mono G h v))

theorem incidence_insert_left {U V : Finset (Fin n)} {v : Fin n} (hv : v ∉ U) :
    incidence G (insert v U) V = incidence G U V + (sectionNeighbors G V v).card := by
  simp [incidence, Finset.sum_insert hv, Nat.add_comm]

theorem incidence_insert_right {U V : Finset (Fin n)} {v : Fin n} (hv : v ∉ V) :
    incidence G U (insert v V) = incidence G U V + (sectionNeighbors G U v).card := by
  rw [incidence_symm G U, incidence_insert_left G hv, incidence_symm G V U]

/-- Leaf restoration preserves the degree budget on every closed subset
outside a retained set B. The closure condition is essential. -/
theorem LeafPrunes.closed_incidence_le_two {F C B : Finset (Fin n)}
    (hp : LeafPrunes G F C) (hBC : B ⊆ C)
    (hC : ∀ v ∈ C \ B, (sectionNeighbors G C v).card ≤ 2) :
    ∀ S : Finset (Fin n), S ⊆ F \ B → ClosedIn G (F \ B) S →
      incidence G S F ≤ 2 * S.card := by
  classical
  induction hp with
  | refl C =>
    intro S hS _
    calc
      incidence G S C ≤ ∑ _v ∈ S, 2 := Finset.sum_le_sum (fun v hv => hC v (hS hv))
      _ = _ := by simp [Nat.mul_comm]
  | @step U C v hv hdeg rest ih =>
    intro S hS hclosed
    have hBU : B ⊆ U.erase v := hBC.trans (LeafPrunes.subset G rest)
    have hvB : v ∉ B := fun h => Finset.notMem_erase v U (hBU h)
    have hinsert : insert v (U.erase v) = U := Finset.insert_erase hv
    by_cases hvS : v ∈ S
    · have hsub : S.erase v ⊆ (U.erase v) \ B := by
        intro u hu
        obtain ⟨huv, huS⟩ := Finset.mem_erase.mp hu
        obtain ⟨huU, huB⟩ := Finset.mem_sdiff.mp (hS huS)
        exact Finset.mem_sdiff.mpr ⟨Finset.mem_erase.mpr ⟨huv, huU⟩, huB⟩
      have hc : ClosedIn G ((U.erase v) \ B) (S.erase v) := by
        intro u hu w hw hadj
        have hwU := Finset.mem_sdiff.mp hw
        exact Finset.mem_erase.mpr ⟨(Finset.mem_erase.mp hwU.1).1,
          hclosed u (Finset.mem_of_mem_erase hu) w
            (Finset.mem_sdiff.mpr ⟨Finset.mem_of_mem_erase hwU.1, hwU.2⟩) hadj⟩
      have hrec := ih hBC hC (S.erase v) hsub hc
      have hin := incidence_insert_left G (V := U) (Finset.notMem_erase v S)
      rw [Finset.insert_erase hvS, hdeg] at hin
      have hin' := incidence_insert_right G (U := S.erase v) (Finset.notMem_erase v U)
      rw [hinsert] at hin'
      have hd : (sectionNeighbors G (S.erase v) v).card ≤ 1 :=
        (Finset.card_le_card (sectionNeighbors_mono G
          ((Finset.erase_subset v S).trans (hS.trans Finset.sdiff_subset)) v)).trans hdeg.le
      have hcard := Finset.card_erase_add_one hvS
      omega
    · have hsub : S ⊆ (U.erase v) \ B := by
        intro u hu
        obtain ⟨huU, huB⟩ := Finset.mem_sdiff.mp (hS hu)
        exact Finset.mem_sdiff.mpr ⟨Finset.mem_erase.mpr
          ⟨by intro he; subst u; exact hvS hu, huU⟩, huB⟩
      have hc : ClosedIn G ((U.erase v) \ B) S := by
        intro u hu w hw hadj
        obtain ⟨hwU, hwB⟩ := Finset.mem_sdiff.mp hw
        exact hclosed u hu w (Finset.mem_sdiff.mpr ⟨Finset.mem_of_mem_erase hwU, hwB⟩) hadj
      have hrec := ih hBC hC S hsub hc
      have hn : sectionNeighbors G S v = ∅ := by
        apply Finset.eq_empty_iff_forall_notMem.mpr
        intro u hu
        obtain ⟨huS, hvu⟩ := mem_sectionNeighbors.mp hu
        exact hvS (hclosed u huS v (Finset.mem_sdiff.mpr ⟨hv, hvB⟩) hvu.symm)
      have hi := incidence_insert_right G (U := S) (Finset.notMem_erase v U)
      rw [hinsert, hn] at hi
      simpa only [hi, Finset.card_empty, Nat.add_zero] using hrec

theorem incidence_closed_split {F B T : Finset (Fin n)}
    (hB : B ⊆ F) (hT : T ⊆ F \ B) (hc : ClosedIn G (F \ B) T) :
    incidence G T F = incidence G T T + incidence G T B := by
  have heq : incidence G T F = incidence G T (T ∪ B) := by
    apply Finset.sum_congr rfl
    intro v hv
    congr 1
    ext w
    simp only [mem_sectionNeighbors, Finset.mem_union]
    constructor
    · intro h
      by_cases hwB : w ∈ B
      · exact ⟨Or.inr hwB, h.2⟩
      · exact ⟨Or.inl (hc v hv w (Finset.mem_sdiff.mpr ⟨h.1, hwB⟩) h.2), h.2⟩
    · rintro ⟨hw | hw, hadj⟩
      · exact ⟨(Finset.mem_sdiff.mp (hT hw)).1, hadj⟩
      · exact ⟨hB hw, hadj⟩
  rw [heq, incidence_union_right]
  exact Finset.disjoint_left.mpr (fun v hv hvB => (Finset.mem_sdiff.mp (hT hv)).2 hvB)

theorem core_piece_bounds (hG : IsSubcubic G) {F C : Finset (Fin n)}
    (hp : LeafPrunes G F C) (_hmin : ∀ v ∈ C, 2 ≤ (sectionNeighbors G C v).card)
    {T : Finset (Fin n)} (hT : T ∈ components G (F \ branchVertices G C)) :
    degreeExcess G T ≤ 0 ∧ (attachment G (branchVertices G C) T).card ≤ 2 ∧
      incidence G T (branchVertices G C) ≤ 2 := by
  classical
  have ht := mem_components G hT
  have hBC : branchVertices G C ⊆ C := Finset.filter_subset _ _
  have hB := hBC.trans (LeafPrunes.subset G hp)
  have hdeg : ∀ v ∈ C \ branchVertices G C, (sectionNeighbors G C v).card ≤ 2 := by
    intro v hv
    obtain ⟨hvC, hvB⟩ := Finset.mem_sdiff.mp hv
    have hupper : (sectionNeighbors G C v).card ≤ 3 := by
      apply le_trans (Finset.card_le_card (show sectionNeighbors G C v ⊆ G.neighborFinset v from ?_)) (hG v)
      intro u hu
      exact (G.mem_neighborFinset _ _).mpr (mem_sectionNeighbors.mp hu).2
    have hn : (sectionNeighbors G C v).card ≠ 3 := by
      intro he
      exact hvB (Finset.mem_filter.mpr ⟨hvC, he⟩)
    omega
  have hbudget := LeafPrunes.closed_incidence_le_two G hp hBC hdeg T ht.1 ht.2.1
  have hsplit := incidence_closed_split G hB ht.1 ht.2.1
  have hlow := connected_excess_lower G ht.2.2
  have hcard := attachment_card_le G (branchVertices G C) T
  unfold degreeExcess at *
  omega

end CubicPathwidth