CubicPathwidth.T2.Reduction

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

import CubicPathwidth.T2.DefsB
import CubicPathwidth.T2.ReductionPieces

/-!
# Reductions: vertices of degree at most two cost `o(n)` in pathwidth

Plan (written before the proof; route actually used).

The reductions (R1)–(R4) are not simulated step by step. A reduced graph is
encoded by its vertex set `B ⊆ V(G)` and the existing torso `coreTorso G univ B`
(from `CoreTorso.lean`): `G`-edges inside `B`, plus an edge between the two
attachments of each component of `V \ B`. A set `B` is a `GoodCore` when every
component `T` of `V \ B` has at most two attachment vertices and carries a
`Piece` structure (`ReductionPieces.lean`): a rooted tree decomposition with
bags of at most three vertices recording how `T` was removed.

1. `goodCore_univ`: `B = V` is good (no components).
2. `goodCore_erase`: if `B` is good and a torso vertex `v` has torso degree at
   most two, then `B.erase v` is good. The new component through `v` is `v`
   plus the old components attached to `v`; its attachment is contained in the
   torso neighbourhood of `v`. This is one reduction (R1)–(R4).
3. `exists_minimal_core`: a good `B` of minimum size has a torso of minimum
   degree at least three.
4. `torso_degree_le` (as in `coreTorso_subcubic`): torso degrees are at most
   the `G`-degrees. Hence maximum degree at most four, and
   `degreeCount_transfer`: `a₃ n₃(R) + a₄ n₄(R) ≤ a₃ n₃(G) + a₄ n₄(G)` when
   `0 ≤ a₃ ≤ a₄`.
5. `Piece.section_decomposition`: every piece has a section decomposition of
   width at most `12 √|T|` (balanced separators of size three, recursively).
6. Lifting: `liftTorso`, `torso_attachment_bag` and `insert_components`
   (`CoreLifting.lean`, "every old bag survives unchanged") give
   `pw(G) ≤ pw(R) + 12 √n + 1`.
7. Assembly: if `|B| ≥ N₁` use `MinDegThreeBound` at `ε/2`; otherwise use the
   trivial bound `|B| - 1 < N₁`. The overhead `N₁ + 12 √n + 1` is at most
   `(ε/2) n` for large `n` (`coreOverhead_sublinear`).
-/

noncomputable section
namespace CubicPathwidth
namespace T2
open SectionDecomposition

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

/-- A reduced vertex set: the removed components have at most two attachments
and were removed by reductions. -/
def GoodCore (B : Finset (Fin n)) : Prop :=
  ∀ T ∈ components G (Finset.univ \ B),
    (attachment G B T).card ≤ 2 ∧ Piece G T (attachment G B T)

theorem mem_components_of_mem {U : Finset (Fin n)} {u : Fin n} (hu : u ∈ U) :
    component G U u ∈ components G U := by
  classical
  unfold components
  exact Finset.mem_image.mpr ⟨u, hu, rfl⟩

theorem goodCore_univ : GoodCore G Finset.univ := by
  classical
  intro T hT
  have hT' := (mem_components G hT).2.2.1
  obtain ⟨u, hu⟩ := hT'
  have := (mem_components G hT).1 hu
  simp at this

open Classical in

/-- Torso degrees are bounded by the original degrees. -/
theorem torso_degree_le (F B : Finset (Fin n))
    (hattach : ∀ T ∈ components G (F \ B), (attachment G B T).card ≤ 2)
    (i : Fin B.card) : (coreTorso G F B).degree i ≤ G.degree (enumerate B i) := by
  let K := coreTorso G F B
  have hw : ∀ j : K.neighborFinset i, ∃ w : G.neighborFinset (enumerate B i),
      ((w : Fin n) = enumerate B j ∨ ∃ T ∈ components G (F \ B),
        (w : Fin n) ∈ T ∧ enumerate B i ∈ attachment G B T ∧
          enumerate B j ∈ attachment G B T) := by
    intro j
    obtain ⟨w, hadj, hr⟩ := torso_edge_witness G ((K.mem_neighborFinset _ _).mp j.property)
    exact ⟨⟨w, (G.mem_neighborFinset _ _).mpr hadj⟩, hr⟩
  choose f hf using hw
  have hinj : Function.Injective f := by
    intro j k he
    have hwval := congrArg Subtype.val he
    have hij : enumerate B i ≠ enumerate B j :=
      fun h => ((K.mem_neighborFinset _ _).mp j.property).1 ((enumerate B).injective h)
    have hik : enumerate B i ≠ enumerate B k :=
      fun h => ((K.mem_neighborFinset _ _).mp k.property).1 ((enumerate B).injective h)
    apply Subtype.ext
    apply (enumerate B).injective
    rcases hf j with hj | ⟨S, hS, hwS, hiS, hjS⟩ <;>
      rcases hf k with hk | ⟨T, hT, hwT, hiT, hkT⟩
    · exact hj.symm.trans (hwval.trans hk)
    · have hwB : (f k : Fin n) ∈ B := by
        rw [← hwval, hj]
        exact (mem_iff_enumerate B _).mpr ⟨j, rfl⟩
      exact False.elim ((Finset.mem_sdiff.mp ((mem_components G hT).1 hwT)).2 hwB)
    · have hwB : (f j : Fin n) ∈ B := by
        rw [hwval, hk]
        exact (mem_iff_enumerate B _).mpr ⟨k, rfl⟩
      exact False.elim ((Finset.mem_sdiff.mp ((mem_components G hS).1 hwS)).2 hwB)
    · have hST : S = T := by
        by_contra hne
        exact Finset.disjoint_left.mp (components_disjoint G hS hT hne) hwS (hwval.symm ▸ hwT)
      subst T
      exact two_attachment_unique (hattach S hS) hiS hjS hkT hij hik
  have hc := Fintype.card_le_of_injective f hinj
  have hc' : (K.neighborFinset i).card ≤ (G.neighborFinset (enumerate B i)).card := by
    simpa only [Fintype.card_coe] using hc
  exact hc'

open Classical in

/-- One reduction step: a torso vertex of degree at most two can be removed. -/
theorem goodCore_erase {B : Finset (Fin n)} (hB : GoodCore G B) {i : Fin B.card}
    (hdeg : (coreTorso G Finset.univ B).degree i ≤ 2) :
    GoodCore G (B.erase (enumerate B i)) := by
  obtain ⟨v, hv⟩ : ∃ v, enumerate B i = v := ⟨_, rfl⟩
  rw [hv]
  have hvB : v ∈ B := (mem_iff_enumerate B v).mpr ⟨i, hv⟩
  have hmemU : ∀ u, u ∈ Finset.univ \ B ↔ u ∉ B := by simp
  have hmemU' : ∀ u, u ∈ Finset.univ \ B.erase v ↔ u = v ∨ u ∉ B := by
    intro u
    simp only [Finset.mem_sdiff, Finset.mem_univ, true_and, Finset.mem_erase, not_and_or,
      not_not, ne_eq]
  have hUU' : Finset.univ \ B ⊆ Finset.univ \ B.erase v := by
    intro u hu
    exact (hmemU' u).mpr (Or.inr ((hmemU u).mp hu))
  intro T' hT'
  obtain ⟨hT'U', hT'cl, hT'conn⟩ := mem_components G hT'
  have hcomp : ∀ u ∈ T', u ∈ Finset.univ \ B → component G (Finset.univ \ B) u ⊆ T' := by
    intro u huT hu
    rcases connected_subset_or_disjoint G ((component_subset G _ u).trans hUU')
      (component_connected G hu) hT'cl with h | h
    · exact h
    · exact False.elim (Finset.disjoint_left.mp h (mem_component_self G hu) huT)
  by_cases hvT : v ∈ T'
  · have hvA : v ∉ attachment G (B.erase v) T' := by
      intro h
      have := attachment_subset G _ _ h
      simp at this
    have hattv : ∀ T ∈ components G (Finset.univ \ B), T ⊆ T' → v ∈ attachment G B T := by
      intro T hT hTT'
      obtain ⟨hTU, hTcl, hTconn⟩ := mem_components G hT
      have hne : T ≠ T' := by
        intro h
        rw [← h] at hvT
        exact (hmemU v).mp (hTU hvT) hvB
      obtain ⟨x, hx, y, hy, hxy⟩ := connected_cross_edge G hT'conn hTT' hTconn.1 hne
      obtain ⟨hyT', hyT⟩ := Finset.mem_sdiff.mp hy
      have hyv : y = v := by
        by_contra hyv
        have hyU : y ∈ Finset.univ \ B :=
          (hmemU y).mpr (((hmemU' y).mp (hT'U' hyT')).resolve_left hyv)
        exact hyT (hTcl x hx y hyU hxy)
      rw [hyv] at hxy
      exact (mem_attachment G).mpr ⟨hvB, x, hx, hxy.symm⟩
    have hA'card : (attachment G (B.erase v) T').card ≤ 2 := by
      have hsub : attachment G (B.erase v) T' ⊆
          ((coreTorso G Finset.univ B).neighborFinset i).image (enumerate B) := by
        intro a ha
        obtain ⟨haB', u, huT', hau⟩ := (mem_attachment G).mp ha
        obtain ⟨hav, haB⟩ := Finset.mem_erase.mp haB'
        obtain ⟨j, hj⟩ := (mem_iff_enumerate B a).mp haB
        refine Finset.mem_image.mpr ⟨j, ?_, hj⟩
        rw [SimpleGraph.mem_neighborFinset]
        refine ⟨fun hij => hav (by rw [← hj, ← hij, hv]), ?_⟩
        by_cases huv : u = v
        · left
          rw [hv, hj, ← huv]
          exact hau.symm
        · right
          have huU : u ∈ Finset.univ \ B :=
            (hmemU u).mpr (((hmemU' u).mp (hT'U' huT')).resolve_left huv)
          refine ⟨component G (Finset.univ \ B) u, mem_components_of_mem G huU, ?_, ?_⟩
          · rw [hv]
            exact hattv _ (mem_components_of_mem G huU) (hcomp u huT' huU)
          · rw [hj]
            exact (mem_attachment G).mpr ⟨haB, u, mem_component_self G huU, hau⟩
      calc (attachment G (B.erase v) T').card
          ≤ (((coreTorso G Finset.univ B).neighborFinset i).image (enumerate B)).card :=
            Finset.card_le_card hsub
        _ ≤ ((coreTorso G Finset.univ B).neighborFinset i).card := Finset.card_image_le
        _ ≤ 2 := by
            rw [SimpleGraph.card_neighborFinset_eq_degree]
            exact hdeg
    have hsplit : T'.erase v =
        ((components G (Finset.univ \ B)).filter (· ⊆ T')).biUnion id := by
      ext u
      constructor
      · intro hu
        obtain ⟨huv, huT'⟩ := Finset.mem_erase.mp hu
        have huU : u ∈ Finset.univ \ B :=
          (hmemU u).mpr (((hmemU' u).mp (hT'U' huT')).resolve_left huv)
        exact Finset.mem_biUnion.mpr ⟨component G (Finset.univ \ B) u,
          Finset.mem_filter.mpr ⟨mem_components_of_mem G huU, hcomp u huT' huU⟩,
          mem_component_self G huU⟩
      · intro hu
        obtain ⟨T, hT, huT⟩ := Finset.mem_biUnion.mp hu
        obtain ⟨hTc, hTT'⟩ := Finset.mem_filter.mp hT
        refine Finset.mem_erase.mpr ⟨?_, hTT' huT⟩
        intro huv
        rw [huv] at huT
        exact (hmemU v).mp ((mem_components G hTc).1 huT) hvB
    have hchild : Piece G (T'.erase v) (insert v (attachment G (B.erase v) T')) := by
      rw [hsplit]
      apply Piece.biUnion
      intro T hT
      obtain ⟨hTc, hTT'⟩ := Finset.mem_filter.mp hT
      apply Piece.mono (hB T hTc).2
      intro w hw
      obtain ⟨hwB, x, hxT, hwx⟩ := (mem_attachment G).mp hw
      by_cases hwv : w = v
      · rw [hwv]
        exact Finset.mem_insert_self _ _
      · exact Finset.mem_insert_of_mem ((mem_attachment G).mpr
          ⟨Finset.mem_erase.mpr ⟨hwv, hwB⟩, x, hTT' hxT, hwx⟩)
    have hnode := Piece.node (G := G) (v := v) (T := T'.erase v)
      (A := attachment G (B.erase v) T')
      (by rw [Finset.card_insert_of_notMem hvA]; omega)
      (by
        intro u hu
        by_cases huB : u ∈ B
        · right
          exact (mem_attachment G).mpr
            ⟨Finset.mem_erase.mpr ⟨hu.ne.symm, huB⟩, v, hvT, hu.symm⟩
        · left
          have huU' : u ∈ Finset.univ \ B.erase v := (hmemU' u).mpr (Or.inr huB)
          exact Finset.mem_erase.mpr ⟨hu.ne.symm, hT'cl v hvT u huU' hu⟩)
      hchild
    rw [Finset.insert_erase hvT] at hnode
    exact ⟨hA'card, hnode⟩
  · have hT'U : T' ⊆ Finset.univ \ B := by
      intro u hu
      refine (hmemU u).mpr (((hmemU' u).mp (hT'U' hu)).resolve_left ?_)
      intro h
      rw [h] at hu
      exact hvT hu
    have hT'cl' : ClosedIn G (Finset.univ \ B) T' :=
      fun a ha w hw hadj => hT'cl a ha w (hUU' hw) hadj
    have hT'mem : T' ∈ components G (Finset.univ \ B) := by
      obtain ⟨u, hu⟩ := hT'conn.1
      rw [← component_eq_of_connected G hT'U hT'cl' hT'conn hu]
      exact mem_components_of_mem G (hT'U hu)
    have hatt : attachment G (B.erase v) T' = attachment G B T' := by
      ext w
      rw [mem_attachment, mem_attachment]
      constructor
      · rintro ⟨hw, h⟩
        exact ⟨Finset.mem_of_mem_erase hw, h⟩
      · rintro ⟨hw, x, hx, hwx⟩
        refine ⟨Finset.mem_erase.mpr ⟨?_, hw⟩, x, hx, hwx⟩
        intro hwv
        rw [hwv] at hwx
        exact hvT (hT'cl x hx v ((hmemU' v).mpr (Or.inl rfl)) hwx.symm)
    rw [hatt]
    exact hB T' hT'mem

open Classical in

/-- A good core of minimum size has a torso of minimum degree at least three. -/
theorem exists_minimal_core : ∃ B : Finset (Fin n), GoodCore G B ∧
    ∀ i : Fin B.card, 3 ≤ (coreTorso G Finset.univ B).degree i := by
  obtain ⟨B, hB, hmin⟩ := Finset.exists_min_image
    ((Finset.univ : Finset (Finset (Fin n))).filter (GoodCore G)) Finset.card
    ⟨Finset.univ, Finset.mem_filter.mpr ⟨Finset.mem_univ _, goodCore_univ G⟩⟩
  have hgood := (Finset.mem_filter.mp hB).2
  refine ⟨B, hgood, ?_⟩
  intro i
  by_contra h
  have hg := goodCore_erase G hgood (i := i) (by omega)
  have hle := hmin _ (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hg⟩)
  have hvB : enumerate B i ∈ B := (mem_iff_enumerate B _).mpr ⟨i, rfl⟩
  have := Finset.card_erase_lt_of_mem hvB
  omega

open Classical in

/-- Degree-count transfer along a degree-dominated injection. -/
theorem degreeCount_transfer {m : ℕ} (R : SimpleGraph (Fin m)) (e : Fin m ↪ Fin n)
    (hdeg : ∀ i, R.degree i ≤ G.degree (e i)) (hG : MaxDegreeAtMost 4 G)
    {a₃ a₄ : ℝ} (h3 : 0 ≤ a₃) (h34 : a₃ ≤ a₄) :
    a₃ * (degreeCount R 3 : ℝ) + a₄ * (degreeCount R 4 : ℝ) ≤
      a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) := by
  have hG' : ∀ v, G.degree v ≤ 4 := by
    intro v
    have := hG v
    convert this
  have h4 : degreeCount R 4 ≤ degreeCount G 4 := by
    unfold degreeCount
    apply Finset.card_le_card_of_injOn e
    · intro i hi
      have hi' : R.degree i = 4 := by
        have := (Finset.mem_filter.mp hi).2
        convert this
      have h1 := hdeg i
      have h2 := hG' (e i)
      simp only [Finset.coe_filter, Finset.mem_univ, true_and]
      change G.degree (e i) = 4
      omega
    · intro i _ j _ hij
      exact e.injective hij
  have hsum : ∀ {k : ℕ} (H : SimpleGraph (Fin k)),
      degreeCount H 3 + degreeCount H 4 =
        (Finset.univ.filter fun v => H.degree v = 3 ∨ H.degree v = 4).card := by
    intro k H
    unfold degreeCount
    rw [Finset.filter_or, Finset.card_union_of_disjoint]
    exact Finset.disjoint_filter.mpr (fun v _ h3 h4 => by omega)
  have h34c : degreeCount R 3 + degreeCount R 4 ≤ degreeCount G 3 + degreeCount G 4 := by
    rw [hsum R, hsum G]
    apply Finset.card_le_card_of_injOn e
    · intro i hi
      have hi' := (Finset.mem_filter.mp hi).2
      have h1 := hdeg i
      have h2 := hG' (e i)
      simp only [Finset.coe_filter, Finset.mem_univ, true_and]
      change G.degree (e i) = 3 ∨ G.degree (e i) = 4
      omega
    · intro i _ j _ hij
      exact e.injective hij
  have c4 : (degreeCount R 4 : ℝ) ≤ degreeCount G 4 := by exact_mod_cast h4
  have c34 : (degreeCount R 3 : ℝ) + degreeCount R 4 ≤ degreeCount G 3 + degreeCount G 4 := by
    exact_mod_cast h34c
  have := mul_le_mul_of_nonneg_left c34 h3
  have := mul_le_mul_of_nonneg_left c4 (sub_nonneg.mpr h34)
  nlinarith

/-- (B5) Vertices of degree at most two cost `o(n)` in pathwidth. -/
theorem reduction : ReductionClaim := by
  intro a₃ a₄ h3 h34 hbound ε hε
  obtain ⟨N₁, hN₁⟩ := hbound (ε / 2) (by linarith)
  obtain ⟨N₂, hN₂⟩ := coreOverhead_sublinear (ε / 8) (by linarith)
  obtain ⟨M, hM⟩ := exists_nat_ge (4 * ((N₁ : ℝ) + 1) / ε)
  refine ⟨max N₂ M, ?_⟩
  intro n hn G hG
  classical
  obtain ⟨B, hgood, hmin3⟩ := exists_minimal_core G
  have hattach : ∀ T ∈ components G (Finset.univ \ B), (attachment G B T).card ≤ 2 :=
    fun T hT => (hgood T hT).1
  have hdom := torso_degree_le G Finset.univ B hattach
  have hRmin : MinDegreeAtLeast 3 (coreTorso G Finset.univ B) := by
    intro i
    convert hmin3 i
  have hRmax : MaxDegreeAtMost 4 (coreTorso G Finset.univ B) := by
    intro i
    have h1 := hdom i
    have h2 := hG (enumerate B i)
    convert h1.trans (by convert h2)
  have hcount := degreeCount_transfer G (coreTorso G Finset.univ B) (enumerate B)
    (by intro i; convert hdom i) hG h3 h34
  have ha4 : 0 ≤ a₄ := h3.trans h34
  have hS : 0 ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) := by positivity
  have hBn : (B.card : ℝ) ≤ n := by
    have := Finset.card_le_univ B
    simp only [Fintype.card_fin] at this
    exact_mod_cast this
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  have hRpw : HasPathwidthAtMost (coreTorso G Finset.univ B)
      (a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε / 2 * n + N₁) := by
    by_cases hm : N₁ ≤ B.card
    · obtain ⟨D, hD⟩ := hN₁ B.card hm _ hRmin hRmax
      refine ⟨D, fun i => (hD i).trans ?_⟩
      have : ε / 2 * (B.card : ℝ) ≤ ε / 2 * n :=
        mul_le_mul_of_nonneg_left hBn (by linarith)
      have : (0 : ℝ) ≤ N₁ := Nat.cast_nonneg _
      linarith
    · obtain ⟨D, hD⟩ := trivial_pathwidth_bound (coreTorso G Finset.univ B)
      refine ⟨D, fun i => (hD i).trans ?_⟩
      have : (B.card : ℝ) ≤ N₁ := by exact_mod_cast (not_le.mp hm).le
      have : 0 ≤ ε / 2 * (n : ℝ) := by positivity
      linarith
  obtain ⟨D, hD⟩ := hRpw
  have hP := liftTorso_width G Finset.univ B D hD
  have hpieces : ∀ T ∈ components G (Finset.univ \ B),
      ∃ Q : SectionDecomposition G T, Q.toBagPath.WidthAtMost (12 * Real.sqrt (n : ℝ)) := by
    intro T hT
    obtain ⟨Q, hQ⟩ := (hgood T hT).2.section_decomposition (by have := (hgood T hT).1; omega)
    have hc : (T.card : ℝ) ≤ n := by
      have := Finset.card_le_univ T
      simp only [Fintype.card_fin] at this
      exact_mod_cast this
    exact ⟨Q, hQ.mono (by linarith [Real.sqrt_le_sqrt hc])⟩
  obtain ⟨R', hR'⟩ := insert_components G (Finset.subset_univ B) (liftTorso G Finset.univ B D) hP
    (by positivity) hpieces
    (fun T hT => torso_attachment_bag G Finset.univ B D hT (hattach T hT))
  refine ⟨R'.toFull, toFull_width R' (hR'.mono ?_)⟩
  have h1 := hN₂ n ((le_max_left _ _).trans hn)
  unfold coreOverhead at h1
  have hMn : (M : ℝ) ≤ n := by exact_mod_cast (le_max_right _ _).trans hn
  have h2 : 4 * ((N₁ : ℝ) + 1) ≤ ε * n := by
    have := hM.trans hMn
    rw [div_le_iff₀ hε] at this
    linarith
  have : (0 : ℝ) ≤ Real.sqrt n := Real.sqrt_nonneg _
  nlinarith

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.reduction