CubicPathwidth.PseudotreeDecomposition

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

import CubicPathwidth.ForestDecomposition

/-! Decomposing a connected subcubic section with at most as many edges as vertices. -/

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

theorem sectionNeighbors_mono {U V : Finset (Fin n)} (h : U ⊆ V) (v : Fin n) :
    sectionNeighbors G U v ⊆ sectionNeighbors G V v := by
  intro w hw
  exact mem_sectionNeighbors.mpr ⟨h (mem_sectionNeighbors.mp hw).1, (mem_sectionNeighbors.mp hw).2⟩

theorem forest_restore_leaf {U : Finset (Fin n)} {v : Fin n} (_hv : v ∈ U)
    (hforest : ForestSection G (U.erase v)) (hdeg : (sectionNeighbors G U v).card ≤ 1) :
    ForestSection G U := by
  classical
  intro S hS hne
  by_cases hvS : v ∈ S
  · by_cases he : (S.erase v).Nonempty
    · have hs := hforest (S.erase v) (Finset.erase_subset_erase v hS) he
      have hd := (Finset.card_le_card (sectionNeighbors_mono G
        ((Finset.erase_subset v S).trans hS) v)).trans hdeg
      have hi := degreeExcess_insert G (Finset.notMem_erase v S)
      rw [Finset.insert_erase hvS] at hi
      omega
    · have hz := Finset.not_nonempty_iff_eq_empty.mp he
      have hsingle : S = {v} := by
        rw [← Finset.insert_erase hvS, hz]
        rfl
      simp [hsingle, degreeExcess, incidence_singleton]
  · apply hforest S _ hne
    intro w hw
    exact Finset.mem_erase.mpr ⟨by intro he; subst w; exact hvS hw, hS hw⟩

theorem connected_erase_leaf {U : Finset (Fin n)} {v : Fin n}
    (hconn : SectionConnected G U) (hv : v ∈ U)
    (hdeg : (sectionNeighbors G U v).card = 1) : SectionConnected G (U.erase v) := by
  classical
  obtain ⟨u, hu⟩ := Finset.card_eq_one.mp hdeg
  have hn : u ∈ sectionNeighbors G U v := by rw [hu]; simp
  obtain ⟨huU, hvu⟩ := mem_sectionNeighbors.mp hn
  have unique : ∀ w ∈ U, G.Adj v w → w = u := by
    intro w hw hadj
    have hmem := mem_sectionNeighbors.mpr ⟨hw, hadj⟩
    rw [hu] at hmem
    exact Finset.mem_singleton.mp hmem
  refine ⟨⟨u, Finset.mem_erase.mpr ⟨hvu.ne.symm, huU⟩⟩, ?_⟩
  intro S hS hc hne
  have hvS : v ∉ S := fun h => Finset.notMem_erase v U (hS h)
  have hSU := hS.trans (Finset.erase_subset v U)
  by_cases huS : u ∈ S
  · have hclosed : ClosedIn G U (insert v S) := by
      intro a ha w hw hadj
      by_cases hwv : w = v
      · subst w
        exact Finset.mem_insert_self _ _
      · rcases Finset.mem_insert.mp ha with rfl | haS
        · rw [unique w hw hadj]
          exact Finset.mem_insert_of_mem huS
        · exact Finset.mem_insert_of_mem (hc a haS w (Finset.mem_erase.mpr ⟨hwv, hw⟩) hadj)
    have he := hconn.2 (insert v S) (Finset.insert_subset hv hSU) hclosed
      (Finset.insert_nonempty _ _)
    have he' := congrArg (fun A : Finset (Fin n) => A.erase v) he
    simpa [Finset.erase_insert hvS] using he'
  · have hclosed : ClosedIn G U S := by
      intro a ha w hw hadj
      have hwv : w ≠ v := by
        intro he
        subst w
        exact huS ((unique a (hSU ha) hadj.symm) ▸ ha)
      exact hc a ha w (Finset.mem_erase.mpr ⟨hwv, hw⟩) hadj
    have he := hconn.2 S hSU hclosed hne
    exact False.elim (hvS (he.symm ▸ hv))

theorem LeafPrunes.connected {U C : Finset (Fin n)} (h : LeafPrunes G U C)
    (hconn : SectionConnected G U) : SectionConnected G C := by
  induction h with
  | refl U => exact hconn
  | step v hv hdeg rest ih => exact ih (connected_erase_leaf G hconn hv hdeg)

theorem LeafPrunes.forest_erase {U C : Finset (Fin n)} (h : LeafPrunes G U C)
    {z : Fin n} (hz : z ∈ C) (hforest : ForestSection G (C.erase z)) :
    ForestSection G (U.erase z) := by
  classical
  induction h with
  | refl U => exact hforest
  | @step V C v hv hdeg rest ih =>
    have hzV := LeafPrunes.subset G rest hz
    have hvz : v ≠ z := by intro he; subst v; exact Finset.notMem_erase z V hzV
    apply forest_restore_leaf G (Finset.mem_erase.mpr ⟨hvz, hv⟩)
    · simpa only [Finset.erase_right_comm] using ih hz hforest
    · exact (Finset.card_le_card (sectionNeighbors_mono G (Finset.erase_subset _ _) _)).trans hdeg.le

theorem connected_nonnegativeComponentExcess {U : Finset (Fin n)}
    (hconn : SectionConnected G U) (he : 0 ≤ degreeExcess G U) :
    NonnegativeComponentExcess G U := by
  classical
  intro S hS hc
  by_cases hn : S.Nonempty
  · rw [hconn.2 S hS hc hn]
    exact he
  · have hz := Finset.not_nonempty_iff_eq_empty.mp hn
    simp [hz, degreeExcess, incidence]

theorem incidence_positive {U V : Finset (Fin n)}
    {u v : Fin n} (hu : u ∈ U) (hv : v ∈ V) (huv : G.Adj u v) : 0 < incidence G U V := by
  have hn : 0 < (sectionNeighbors G V u).card :=
    Finset.card_pos.mpr ⟨v, mem_sectionNeighbors.mpr ⟨hv, huv⟩⟩
  exact hn.trans_le (Finset.single_le_sum
    (f := fun w => (sectionNeighbors G V w).card) (fun _ _ => Nat.zero_le _) hu)

theorem degree_two_erase_forest {U : Finset (Fin n)} (hconn : SectionConnected G U)
    (hdeg : ∀ v ∈ U, (sectionNeighbors G U v).card = 2) {z : Fin n} (hz : z ∈ U) :
    ForestSection G (U.erase z) := by
  classical
  intro S hS hne
  have hSU := hS.trans (Finset.erase_subset z U)
  have hproper : S ≠ U := by intro he; exact Finset.notMem_erase z U (hS (he.symm ▸ hz))
  obtain ⟨u, hu, v, hv, huv⟩ := connected_cross_edge G hconn hSU hne hproper
  have hpos := incidence_positive G hu hv huv
  have hsum : incidence G S U = 2 * S.card := by
    unfold incidence
    simp only [Finset.sum_congr rfl (fun v hv => hdeg v (hSU hv))]
    simp [Nat.mul_comm]
  have heq : S ∪ (U \ S) = U := Finset.union_sdiff_of_subset hSU
  have he := incidence_union_right G (U := S) (Finset.sdiff_disjoint.symm : Disjoint S (U \ S))
  rw [heq] at he
  unfold degreeExcess
  omega

theorem pseudotree_section_decomposition (hG : IsSubcubic G) (U : Finset (Fin n))
    (hconn : SectionConnected G U) (hex : degreeExcess G U ≤ 0) :
    ∃ P : SectionDecomposition G U,
      P.toBagPath.WidthAtMost (4 * Real.sqrt (U.card : ℝ) + 1) := by
  classical
  by_cases hneg : degreeExcess G U < 0
  · obtain ⟨P, hP⟩ := forest_section_decomposition G U (forest_of_connected_negative G hconn hneg)
    exact ⟨P, hP.mono (by linarith)⟩
  · have heq : degreeExcess G U = 0 := by omega
    obtain ⟨C, hp, hm⟩ := exists_leafPrunes_minDegree_two G U
      (connected_nonnegativeComponentExcess G hconn (by omega))
    have hCconn := LeafPrunes.connected G hp hconn
    have heC := hp.excess_eq
    have hcount := degreeExcess_eq_branch_card G hG C hm
    have hCdeg : ∀ v ∈ C, (sectionNeighbors G C v).card = 2 := by
      intro v hv
      have hl := hm v hv
      have hu : (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 w hw
        exact (G.mem_neighborFinset _ _).mpr (mem_sectionNeighbors.mp hw).2
      by_contra hn
      have hthree : (sectionNeighbors G C v).card = 3 := by omega
      have hnz : 0 < (C.filter (fun v => (sectionNeighbors G C v).card = 3)).card :=
        Finset.card_pos.mpr ⟨v, Finset.mem_filter.mpr ⟨hv, hthree⟩⟩
      omega
    obtain ⟨z, hz⟩ := hCconn.1
    have hforest := LeafPrunes.forest_erase G hp hz (degree_two_erase_forest G hCconn hCdeg hz)
    obtain ⟨P, hP⟩ := forest_section_decomposition G (U.erase z) hforest
    have hzU := LeafPrunes.subset G hp hz
    have hU : (U.erase z) ∪ {z} = U := by
      rw [Finset.union_comm, Finset.singleton_union, Finset.insert_erase hzU]
    have hc : ((U.erase z).card : ℝ) ≤ U.card := by exact_mod_cast Finset.card_le_card (Finset.erase_subset z U)
    have hwidth := (hold_width P {z} hP).mono
      (show 4 * Real.sqrt ((U.erase z).card : ℝ) + (({z} : Finset (Fin n)).card : ℝ) ≤
          4 * Real.sqrt (U.card : ℝ) + 1 by
        simp only [Finset.card_singleton, Nat.cast_one]
        linarith [Real.sqrt_le_sqrt hc])
    have hout : ∃ Q : SectionDecomposition G ((U.erase z) ∪ {z}),
        Q.toBagPath.WidthAtMost (4 * Real.sqrt (U.card : ℝ) + 1) := ⟨P.hold {z}, hwidth⟩
    rw [hU] at hout
    exact hout

end CubicPathwidth