CubicPathwidth.T4.BasicComp

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

import CubicPathwidth.T4.BasicPsi
import CubicPathwidth.T4.BasicGlue

/-!
# The first case of Lemma 9.11 (`lem:basic`), assembled over the torso components (E3b)

Helper for `CubicPathwidth/T4/Basic.lean`: `componentClaim : ComponentClaim`.

Proof. Let `N` be the threshold of the base hypothesis at `ε`, and `N₀ := N`.
Put `W := max (ψ⁻ + b₃ + ε n + N) q`. For each torso component `C`:

* if all torso degrees on `C` are at most `5` and `|C| ≥ N`, the base bound applied to
  the relabelled component `coreTorso G (F \ (B \ C)) C` gives pathwidth at most
  `∑_{v ∈ C} b (tdeg v) + ε |C|`; and `∑_{v ∈ C} b (tdeg v) ≤ ψ⁻ + H_{δ(C)} ≤ ψ⁻ + b₃`
  (`term_le_psiMinus`, `runMin_le_incr_three`);
* if all torso degrees on `C` are at most `5` and `|C| < N`, the trivial bound
  `|C| - 1 < N ≤ W` applies;
* otherwise `C` has pathwidth at most `q` by hypothesis.

The sections on the components are glued (`glueSections`, the torso has no edges between
components), and the result is converted back to `coreTorso G F B`
(`coreTorso_eq_induced` with `U = B`).
-/

noncomputable section

namespace CubicPathwidth
namespace T4
namespace BasicAux

open T2 SectionDecomposition

variable {n : ℕ}

/-- A torso edge from a vertex of a torso component stays in that component. -/
theorem tcomp_closed {G : SimpleGraph (Fin n)} {F B C : Finset (Fin n)}
    (hC : C ∈ tcomps G F B) :
    ∀ u ∈ C, ∀ v, (tgraph G F B).Adj u v → v ∈ C := by
  intro u hu v hadj
  exact (mem_components (tgraph G F B) hC).2.1 u hu v
    ((tgraph_adj_iff G F B u v).1 hadj).2.2.1 hadj

/-- (E3b) The first case of Lemma 9.11 (`lem:basic`), assembled over the torso components. -/
theorem componentClaim : ComponentClaim := by
  intro b hb hbase ε hε
  obtain ⟨N, hN⟩ := hbase ε hε
  refine ⟨N, ?_⟩
  intro n G F B _hgood hmin q hcomp
  have hpsi0 : 0 ≤ psiMinus b G F B := (psiClaim b hb n G F B hmin).1
  have hb3 : 0 ≤ b 3 := hb.nonneg 3
  have hεn : 0 ≤ ε * (n : ℝ) := mul_nonneg hε.le (Nat.cast_nonneg n)
  have hN0 : (0 : ℝ) ≤ (N : ℝ) := Nat.cast_nonneg N
  have hbig : psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ) ≤
      max (psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ)) q := le_max_left _ _
  set W : ℝ := max (psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ)) q with hW
  have hW1 : -1 ≤ W := by linarith
  have hWN : (N : ℝ) ≤ W := by linarith
  have hsec : ∀ C ∈ tcomps G F B, ∃ P : SectionDecomposition (tgraph G F B) C,
      P.toBagPath.WidthAtMost W := by
    intro C hC
    obtain ⟨hCB, _⟩ := tcomp_props hC
    have hgraph := coreTorso_eq_induced G F B C hCB
    rcases hcomp C hC with hdeg | hq
    · by_cases hsize : N ≤ C.card
      · have hK := maxDegreeAtMost_coreTorso G F B C hCB hdeg
        have hpw := hN C.card hsize _ hK
        have hle : degreeWeight (coreTorso G (F \ (B \ C)) C) b + ε * (C.card : ℝ) ≤ W := by
          have h1 := degreeWeight_coreTorso_le hb G F B C hCB
          have h2 := term_le_psiMinus hb hC hmin
          have h3 := runMin_le_incr_three b (cmin G F B C)
          rw [incr_three hb] at h3
          have h4' : C.card ≤ n := by simpa using Finset.card_le_univ C
          have h4 : (C.card : ℝ) ≤ (n : ℝ) := by exact_mod_cast h4'
          have h5 : ε * (C.card : ℝ) ≤ ε * (n : ℝ) := mul_le_mul_of_nonneg_left h4 hε.le
          have h6 : psiMinus b G F B + b 3 + ε * (n : ℝ) + (N : ℝ) ≤ W := hbig
          linarith
        have hpw' : HasPathwidthAtMost (inducedOnFin (tgraph G F B) C)
            (degreeWeight (coreTorso G (F \ (B \ C)) C) b + ε * (C.card : ℝ)) := by
          rw [← hgraph]
          exact hpw
        exact section_of_hasPathwidth hpw' hle
      · have hlt : (C.card : ℝ) < (N : ℝ) := by
          have : C.card < N := by omega
          exact_mod_cast this
        have hpw := trivial_pathwidth_bound (coreTorso G (F \ (B \ C)) C)
        have hpw' : HasPathwidthAtMost (inducedOnFin (tgraph G F B) C)
            ((C.card : ℝ) - 1) := by
          rw [← hgraph]
          exact hpw
        exact section_of_hasPathwidth hpw' (by linarith)
    · have hq' : HasPathwidthAtMost (inducedOnFin (tgraph G F B) C) q := by
        rw [← hgraph]
        exact hq
      exact section_of_hasPathwidth hq' (le_max_right _ _)
  have hcl : ∀ C ∈ tcomps G F B, ∀ u ∈ C, ∀ v, (tgraph G F B).Adj u v → v ∈ C :=
    fun C hC => tcomp_closed hC
  have hdis : ∀ C ∈ tcomps G F B, ∀ D ∈ tcomps G F B, C ≠ D → Disjoint C D :=
    fun C hC D hD hne => components_disjoint (tgraph G F B) hC hD hne
  have hcov : (tcomps G F B).biUnion id = B := components_cover (tgraph G F B) B
  obtain ⟨P, hPw⟩ := glueSections (tgraph G F B) hW1 (tcomps G F B) B hcov hcl hdis hsec
  have heq : coreTorso G F B = inducedOnFin (tgraph G F B) B := by
    have h := coreTorso_eq_induced G F B B (subset_refl B)
    rwa [Finset.sdiff_self, Finset.sdiff_empty] at h
  rw [heq]
  exact hasPathwidthAtMost_of_section P hPw

end BasicAux
end T4
end CubicPathwidth
Back to top