CubicPathwidth.ForestStructure

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

import CubicPathwidth.FiniteComponents

/-! Forest structure and balanced separators using finite incidence counts. -/

noncomputable section
namespace CubicPathwidth

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

def ForestSection (U : Finset (Fin n)) : Prop :=
  ∀ S : Finset (Fin n), S ⊆ U → S.Nonempty → degreeExcess G S < 0

theorem ForestSection.mono {U V : Finset (Fin n)} (h : ForestSection G U)
    (hV : V ⊆ U) : ForestSection G V := fun S hS => h S (hS.trans hV)

/-- Growing a nonempty set inside a connected section never decreases its
edge-minus-vertex excess: every new vertex has an old neighbour. -/
theorem connected_excess_mono {U S : Finset (Fin n)} (hU : SectionConnected G U)
    (hS : S ⊆ U) (hne : S.Nonempty) : degreeExcess G S ≤ degreeExcess G U := by
  classical
  have go : ∀ k : ℕ, ∀ S : Finset (Fin n), (U \ S).card = k →
      S ⊆ U → S.Nonempty → degreeExcess G S ≤ degreeExcess G U := by
    intro k
    induction k using Nat.strong_induction_on with
    | h k ih =>
      intro S hk hS hne
      by_cases heq : S = U
      · subst S
        exact le_rfl
      · obtain ⟨u, hu, v, hv, huv⟩ := connected_cross_edge G hU hS hne heq
        obtain ⟨hvU, hvS⟩ := Finset.mem_sdiff.mp hv
        have hsub : insert v S ⊆ U := Finset.insert_subset hvU hS
        have hlt : (U \ insert v S).card < k := by
          have hc := Finset.card_sdiff_add_card_eq_card hS
          have hc' := Finset.card_sdiff_add_card_eq_card hsub
          rw [Finset.card_insert_of_notMem hvS] at hc'
          omega
        have hrec := ih _ hlt (insert v S) rfl hsub (Finset.insert_nonempty _ _)
        have hdegree : 1 ≤ (sectionNeighbors G S v).card := Finset.card_pos.mpr
          ⟨u, mem_sectionNeighbors.mpr ⟨hu, huv.symm⟩⟩
        rw [degreeExcess_insert G hvS] at hrec
        omega
  exact go _ S rfl hS hne

theorem connected_excess_lower {U : Finset (Fin n)} (hU : SectionConnected G U) :
    -2 ≤ degreeExcess G U := by
  obtain ⟨v, hv⟩ := hU.1
  have h := connected_excess_mono G hU (Finset.singleton_subset_iff.mpr hv)
    (Finset.singleton_nonempty v)
  simpa [degreeExcess, incidence_singleton] using h

theorem forest_of_connected_negative {U : Finset (Fin n)}
    (hU : SectionConnected G U) (hneg : degreeExcess G U < 0) : ForestSection G U := by
  intro S hS hne
  exact (connected_excess_mono G hU hS hne).trans_lt hneg

/-- A component after deleting a vertex of a forest has at most one neighbour
of that vertex. Two such neighbours would force nonnegative excess. -/
theorem forest_component_neighbors_le_one {U T : Finset (Fin n)} {v : Fin n}
    (hU : ForestSection G U) (hv : v ∈ U) (hT : T ∈ components G (U.erase v)) :
    (sectionNeighbors G T v).card ≤ 1 := by
  have ht := mem_components G hT
  have hvT : v ∉ T := fun h => Finset.notMem_erase v U (ht.1 h)
  have hlow := connected_excess_lower G ht.2.2
  have hneg := hU (insert v T) (Finset.insert_subset hv
    (ht.1.trans (Finset.erase_subset _ _))) (Finset.insert_nonempty _ _)
  rw [degreeExcess_insert G hvT] at hneg
  omega

theorem connected_component_neighbor {U T : Finset (Fin n)} {v : Fin n}
    (hU : SectionConnected G U) (hv : v ∈ U) (hT : T ∈ components G (U.erase v)) :
    ∃ w ∈ T, G.Adj v w := by
  have ht := mem_components G hT
  have hTU := ht.1.trans (Finset.erase_subset v U)
  have hvT : v ∉ T := fun h => Finset.notMem_erase v U (ht.1 h)
  have hne : T ≠ U := by intro he; exact hvT (he.symm ▸ hv)
  obtain ⟨w, hw, z, hz, hwz⟩ := connected_cross_edge G hU hTU ht.2.2.1 hne
  have hzv : z = v := by
    by_contra h
    exact (Finset.mem_sdiff.mp hz).2
      (ht.2.1 w hw z (Finset.mem_erase.mpr ⟨h, (Finset.mem_sdiff.mp hz).1⟩) hwz)
  subst z
  exact ⟨w, hw, hwz.symm⟩

def largestBranch (U : Finset (Fin n)) (v : Fin n) : ℕ :=
  (U.erase v).sup (fun w => (component G (U.erase v) w).card)

/-- A finite tree has a vertex whose deletion leaves components of at most
half its order. The proof moves into a heavy branch until the maximum falls. -/
theorem forest_centroid {U : Finset (Fin n)}
    (hforest : ForestSection G U) (hconn : SectionConnected G U) :
    ∃ v ∈ U, ∀ T ∈ components G (U.erase v), 2 * T.card ≤ U.card := by
  classical
  obtain ⟨v, hv, hmin⟩ := Finset.exists_min_image U (largestBranch G U) hconn.1
  refine ⟨v, hv, ?_⟩
  intro T hT
  have hTmax : T.card ≤ largestBranch G U v := by
    obtain ⟨w, hw, rfl⟩ := Finset.mem_image.mp hT
    exact Finset.le_sup (f := fun z => (component G (U.erase v) z).card) hw
  by_contra hlarge
  have hpositive : 0 < largestBranch G U v := by omega
  have hne : (U.erase v).Nonempty := by
    by_contra hn
    have hz : U.erase v = ∅ := Finset.not_nonempty_iff_eq_empty.mp hn
    simp [largestBranch, hz] at hpositive
  obtain ⟨r, hr, hrmax⟩ := Finset.exists_max_image (U.erase v)
    (fun w => (component G (U.erase v) w).card) hne
  let C := component G (U.erase v) r
  have hCmem : C ∈ components G (U.erase v) := Finset.mem_image.mpr ⟨r, hr, rfl⟩
  have hc := mem_components G hCmem
  have hCmax : C.card = largestBranch G U v := by
    exact le_antisymm (Finset.le_sup (f := fun z => (component G (U.erase v) z).card) hr)
      (Finset.sup_le hrmax)
  have hCbig : U.card < 2 * C.card := by omega
  obtain ⟨w, hwC, hvw⟩ := connected_component_neighbor G hconn hv hCmem
  have hwU : w ∈ U := Finset.mem_of_mem_erase (hc.1 hwC)
  have hnle := forest_component_neighbors_le_one G hforest hv hCmem
  have hsingle : sectionNeighbors G C v = {w} := by
    apply Finset.eq_singleton_iff_unique_mem.mpr
    refine ⟨mem_sectionNeighbors.mpr ⟨hwC, hvw⟩, ?_⟩
    intro z hz
    exact (Finset.card_le_one.mp hnle) z hz w (mem_sectionNeighbors.mpr ⟨hwC, hvw⟩)
  have hdclosed : ClosedIn G (U.erase w) (U \ C) := by
    intro a ha z hz hadj
    refine Finset.mem_sdiff.mpr ⟨Finset.mem_of_mem_erase hz, ?_⟩
    intro hzC
    by_cases hav : a = v
    · subst a
      have hzN : z ∈ sectionNeighbors G C v := mem_sectionNeighbors.mpr ⟨hzC, hadj⟩
      rw [hsingle] at hzN
      exact (Finset.mem_erase.mp hz).1 (Finset.mem_singleton.mp hzN)
    · exact (Finset.mem_sdiff.mp ha).2 (hc.2.1 z hzC a
        (Finset.mem_erase.mpr ⟨hav, (Finset.mem_sdiff.mp ha).1⟩) hadj.symm)
  have hnew : largestBranch G U w ≤ C.card - 1 := by
    apply Finset.sup_le
    intro z hz
    let S := component G (U.erase w) z
    have hs := component_subset G (U.erase w) z
    rcases connected_subset_or_disjoint G hs (component_connected G hz) hdclosed with hd | hd
    · have hb := Finset.card_le_card hd
      have hCU : C ⊆ U := hc.1.trans (Finset.erase_subset _ _)
      have hsum := Finset.card_sdiff_add_card_eq_card hCU
      omega
    · have hsub : S ⊆ C.erase w := by
        intro a ha
        have haU := Finset.mem_of_mem_erase (hs ha)
        have haC : a ∈ C := by
          by_contra hnot
          exact Finset.disjoint_left.mp hd ha (Finset.mem_sdiff.mpr ⟨haU, hnot⟩)
        exact Finset.mem_erase.mpr ⟨(Finset.mem_erase.mp (hs ha)).1, haC⟩
      have hb := Finset.card_le_card hsub
      rw [Finset.card_erase_of_mem hwC] at hb
      exact hb
  have hold := hmin w hwU
  have hcp := Finset.card_pos.mpr hc.2.2.1
  omega

end CubicPathwidth