CubicPathwidth.ForestDecomposition

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

import CubicPathwidth.ForestStructure
import CubicPathwidth.SectionAssembly
import CubicPathwidth.BoundaryAssembly

/-! Actual narrow path decompositions of finite forests. -/

noncomputable section
namespace CubicPathwidth
open SectionDecomposition

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

theorem section_of_components (U : Finset (Fin n)) {w : ℝ} (hw : -1 ≤ w)
    (hparts : ∀ T ∈ components G U,
      ∃ P : SectionDecomposition G T, P.toBagPath.WidthAtMost w) :
    ∃ P : SectionDecomposition G U, P.toBagPath.WidthAtMost w := by
  have go : ∀ A : Finset (Finset (Fin n)), A ⊆ components G U →
      ∃ P : SectionDecomposition G (A.biUnion id), P.toBagPath.WidthAtMost w := by
    intro A
    induction A using Finset.induction_on with
    | empty =>
      intro _
      let P : SectionDecomposition G ∅ := {
        toBagPath := BagPath.single ∅
        bag_subset := by intro i hi; exact Finset.Subset.refl _
        vertex_covered := by simp
        edge_covered := by simp }
      refine ⟨P, ?_⟩
      intro i hi
      simpa [P, BagPath.single] using (show (0 : ℝ) ≤ w + 1 by linarith)
    | @insert T A hnot ih =>
      intro hA
      have hT := hA (Finset.mem_insert_self _ _)
      have hA' : A ⊆ components G U := (Finset.subset_insert _ _).trans hA
      obtain ⟨P, hP⟩ := ih hA'
      obtain ⟨Q, hQ⟩ := hparts T hT
      have hdis : Disjoint (A.biUnion id) T := by
        apply Finset.disjoint_left.mpr
        intro v hv hvT
        obtain ⟨S, hS, hvS⟩ := Finset.mem_biUnion.mp hv
        exact Finset.disjoint_left.mp (components_disjoint G (hA' hS) hT
          (by intro he; subst S; exact hnot hS)) hvS hvT
      have hsep : ∀ v ∈ T, ∀ u ∈ A.biUnion id, G.Adj v u → u ∈ (∅ : Finset (Fin n)) := by
        intro v hv u hu hadj
        obtain ⟨S, hS, huS⟩ := Finset.mem_biUnion.mp hu
        have huU := (mem_components G (hA' hS)).1 huS
        have huT := (mem_components G hT).2.1 v hv u huU hadj
        exact False.elim (Finset.disjoint_left.mp hdis
          (Finset.mem_biUnion.mpr ⟨S, hS, huS⟩) huT)
      let P' := P.endAtSubset ∅ (Finset.empty_subset _)
      have hP' : P'.toBagPath.WidthAtMost w := endAtSubset_width _ _ _ hP
      obtain ⟨R, _, hR⟩ := append_component P' Q ∅ (Finset.empty_subset _) hdis
        (endAtSubset_last _ _ _) hsep hP' hQ
      have heq : (insert T A).biUnion id = (A.biUnion id) ∪ T := by
        simp [Finset.union_comm]
      rw [heq]
      exact ⟨R, by simpa using hR⟩
  have h := go (components G U) (Finset.Subset.refl _)
  rw [components_cover G U] at h
  exact h

theorem sqrt_half_bound {a b : ℕ} (h : 2 * a ≤ b) :
    4 * Real.sqrt (a : ℝ) ≤ 3 * Real.sqrt (b : ℝ) := by
  have ha := Real.sqrt_nonneg (a : ℝ)
  have hb := Real.sqrt_nonneg (b : ℝ)
  have ha2 := Real.sq_sqrt (Nat.cast_nonneg a : (0 : ℝ) ≤ a)
  have hb2 := Real.sq_sqrt (Nat.cast_nonneg b : (0 : ℝ) ≤ b)
  have hcast : 2 * (a : ℝ) ≤ b := by exact_mod_cast h
  nlinarith [sq_nonneg (4 * Real.sqrt (a : ℝ) - 3 * Real.sqrt (b : ℝ))]

/-- A generous square-root bound keeps the original asymptotic theorem
unchanged while avoiding a separate formal logarithmic-error calculation. -/
theorem forest_section_decomposition (U : Finset (Fin n)) (hU : ForestSection G U) :
    ∃ P : SectionDecomposition G U, P.toBagPath.WidthAtMost (4 * Real.sqrt (U.card : ℝ)) := by
  have go : ∀ m : ℕ, ∀ U : Finset (Fin n), U.card = m → ForestSection G U →
      ∃ P : SectionDecomposition G U, P.toBagPath.WidthAtMost (4 * Real.sqrt (U.card : ℝ)) := by
    intro m
    induction m using Nat.strong_induction_on with
    | h m ih =>
      intro U hm hforest
      let _ : Decidable (SectionConnected G U) := Classical.propDecidable _
      by_cases hconn : SectionConnected G U
      · obtain ⟨v, hv, hcentroid⟩ := forest_centroid G hforest hconn
        have hnpos := Finset.card_pos.mpr hconn.1
        have hroot : (1 : ℝ) ≤ Real.sqrt (U.card : ℝ) := by
          have hn : (1 : ℝ) ≤ U.card := by exact_mod_cast hnpos
          simpa using Real.sqrt_le_sqrt hn
        obtain ⟨P, hP⟩ := section_of_components G (U.erase v)
          (show -1 ≤ 3 * Real.sqrt (U.card : ℝ) by nlinarith [Real.sqrt_nonneg (U.card : ℝ)])
          (by
            intro T hT
            have ht := mem_components G hT
            have hc := hcentroid T hT
            have hlt : T.card < m := by omega
            obtain ⟨Q, hQ⟩ := ih _ hlt T rfl
              (ForestSection.mono G hforest (ht.1.trans (Finset.erase_subset _ _)))
            exact ⟨Q, hQ.mono (sqrt_half_bound hc)⟩)
        have heq : (U.erase v) ∪ {v} = U := by
          rw [Finset.union_comm, Finset.singleton_union, Finset.insert_erase hv]
        have hwidth := (hold_width P {v} hP).mono
          (show 3 * Real.sqrt (U.card : ℝ) + (({v} : Finset (Fin n)).card : ℝ) ≤
              4 * Real.sqrt (U.card : ℝ) by simp only [Finset.card_singleton, Nat.cast_one]; linarith)
        have h : ∃ Q : SectionDecomposition G ((U.erase v) ∪ {v}),
            Q.toBagPath.WidthAtMost (4 * Real.sqrt (U.card : ℝ)) := ⟨P.hold {v}, hwidth⟩
        rw [heq] at h
        exact h
      · apply section_of_components G U (by nlinarith [Real.sqrt_nonneg (U.card : ℝ)])
        intro T hT
        have ht := mem_components G hT
        have hne : T ≠ U := by intro he; exact hconn (he ▸ ht.2.2)
        have hlt : T.card < m := by
          rw [← hm]
          exact Finset.card_lt_card (Finset.ssubset_iff_subset_ne.mpr ⟨ht.1, hne⟩)
        obtain ⟨P, hP⟩ := ih _ hlt T rfl (ForestSection.mono G hforest ht.1)
        have hc : (T.card : ℝ) ≤ U.card := by exact_mod_cast Finset.card_le_card ht.1
        exact ⟨P, hP.mono (mul_le_mul_of_nonneg_left (Real.sqrt_le_sqrt hc) (by norm_num))⟩
  exact go _ U rfl hU

theorem degreeExcess_eq_sum (U : Finset (Fin n)) :
    degreeExcess G U = ∑ v ∈ U, (((sectionNeighbors G U v).card : ℤ) - 2) := by
  simp [degreeExcess, incidence, Finset.sum_sub_distrib, mul_comm]

theorem sum_component_excess (U : Finset (Fin n)) :
    ∑ T ∈ components G U, degreeExcess G T = degreeExcess G U := by
  classical
  simp_rw [degreeExcess_eq_sum]
  have he : ∀ T ∈ components G U, ∀ v ∈ T, sectionNeighbors G T v = sectionNeighbors G U v := by
    intro T hT v hv
    have ht := mem_components G hT
    ext w
    simp only [mem_sectionNeighbors]
    exact ⟨fun h => ⟨ht.1 h.1, h.2⟩, fun h => ⟨ht.2.1 v hv w h.1 h.2, h.2⟩⟩
  calc
    _ = ∑ T ∈ components G U, ∑ v ∈ T, (((sectionNeighbors G U v).card : ℤ) - 2) := by
      apply Finset.sum_congr rfl
      intro T hT
      apply Finset.sum_congr rfl
      intro v hv
      rw [he T hT v hv]
    _ = ∑ v ∈ (components G U).biUnion id, (((sectionNeighbors G U v).card : ℤ) - 2) := by
      symm
      apply Finset.sum_biUnion
      intro S hS T hT hne
      exact components_disjoint G hS hT hne
    _ = _ := by rw [components_cover]

/-- The formerly missing tree-component construction is now supplied. -/
theorem forestComponentBound : ForestComponentBound coreOverhead := by
  classical
  intro n G hG F hbad
  obtain ⟨S, hSF, hclosed, hneg⟩ : ∃ S, S ⊆ F ∧ ClosedIn G F S ∧ degreeExcess G S < 0 := by
    simpa only [NonnegativeComponentExcess, not_forall, not_le, exists_prop] using hbad
  have hsome : ∃ T ∈ components G S, degreeExcess G T < 0 := by
    by_contra hn
    have hnonneg : ∀ T ∈ components G S, 0 ≤ degreeExcess G T := by
      intro T hT
      by_contra h
      exact hn ⟨T, hT, by omega⟩
    have hs := Finset.sum_nonneg hnonneg
    rw [sum_component_excess] at hs
    omega
  obtain ⟨T, hT, hTneg⟩ := hsome
  have ht := mem_components G hT
  obtain ⟨P, hP⟩ := forest_section_decomposition G T (forest_of_connected_negative G ht.2.2 hTneg)
  refine ⟨T, ht.2.2.1, ht.1.trans hSF, closed_trans G hclosed ht.2.1 ht.1, P, ?_⟩
  apply hP.mono
  have hc : (T.card : ℝ) ≤ F.card := by exact_mod_cast Finset.card_le_card (ht.1.trans hSF)
  have hs := Real.sqrt_le_sqrt hc
  have hp := Real.sqrt_nonneg (F.card : ℝ)
  unfold coreOverhead
  linarith

end CubicPathwidth