CubicPathwidth.T4.ProcessDefs

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

import CubicPathwidth.T4.Defs
import CubicPathwidth.T2.Reduction

/-!
# Interfaces for the proof of the bootstrap lemma (`lem:bootstrap`, `k = 5`)

In the paper: subsection
"The deletion process and the proof of the bootstrap lemma", and Lemma 4.5 (`lem:reduction`).

## States

We never relabel the input graph `G : SimpleGraph (Fin n)` during the process. A
*state* is a pair `(F, B)` of vertex sets: `F` is the set of vertices not deleted so
far and `B ⊆ F` is the current core. The current reduced graph of the manuscript is
the torso of `G[F]` over `B`: the `G`-edges inside `B`, plus an edge between any two
attachment vertices of a component of `G[F \ B]`. We use it in two forms:

* `tgraph G F B : SimpleGraph (Fin n)`, on the full vertex type, with every vertex
  outside `B` isolated. Torso degrees `tdeg`, the potentials and the torso
  components `tcomps` (subsets of `B`) are defined from it.
* `coreTorso G F B : SimpleGraph (Fin B.card)` (`CoreTorso.lean`), the same graph
  relabelled onto `Fin B.card` by `enumerate B`. Pathwidth statements use this form.

One `Step` is either a *reduction* (remove from `B` a vertex of torso degree at most
two; `F` unchanged: this is one of (R1)–(R4) of Definition 4.2 (`def:reductions`) applied to the torso)
or a *deletion* (remove a core vertex `w` from both `F` and `B`). `Reach` is the
reflexive–transitive closure, and `Good G F B` means that `(F, B)` is reachable from
the initial state `(univ, univ)`, whose torso is `G` itself (`tgraph_univ`). Along a
`Reach` from `(F, B)` to `(F', B')` the set of deleted vertices is `F \ F'`.

## The potential

For a coefficient sequence `b`, `psi b G F B = ∑_{v ∈ B} b (tdeg v)` is `ψ` of the
torso, and `psiMinus b G F B = psi - ∑_{C ∈ tcomps} runMin b (cmin C)` is the
potential `ψ⁻` of the manuscript (`H_d` is `runMin b d`, and `cmin C` is the minimum
torso degree on `C`, i.e. `δ` of that torso component).

## The three children

* `StateClaim` (E2): the torso semantics of the two kinds of steps, maximal reductions,
  Lemma 4.5 (`lem:reduction`) (lifting, paid once) and the second case of Lemma 9.11 (`lem:basic`).
* `BasicClaim` (E3): facts about `ψ⁻` and the first case of Lemma 9.11 (`lem:basic`), assembled
  over the torso components.
* `DeletionClaim` (E4): Proposition 9.10 (`prop:deletion`).

`bootstrap_of_children` in `CubicPathwidth/T4/Process.lean` proves `BootstrapClaim`
from them.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2 SectionDecomposition

variable {n : ℕ}

/-! ## Vocabulary -/

/-- The torso of the state `(F, B)` on the full vertex type: `u ~ v` iff `u ≠ v`, both
lie in `B`, and they are adjacent in `G` or are both attachment vertices of one
component of `G[F \ B]`. Vertices outside `B` are isolated. -/
def tgraph (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) : SimpleGraph (Fin n) where
  Adj u v := u ≠ v ∧ u ∈ B ∧ v ∈ B ∧ (G.Adj u v ∨
    ∃ T ∈ components G (F \ B), u ∈ attachment G B T ∧ v ∈ attachment G B T)
  symm := ⟨by
    intro u v h
    obtain ⟨h1, h2, h3, h4⟩ := h
    refine ⟨h1.symm, h3, h2, ?_⟩
    rcases h4 with h | ⟨T, hT, hu, hv⟩
    · exact Or.inl h.symm
    · exact Or.inr ⟨T, hT, hv, hu⟩⟩
  loopless := ⟨fun u h => h.1 rfl⟩

/-- Torso degree of `v` in the state `(F, B)` (zero for `v ∉ B`). -/
def tdeg (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (v : Fin n) : ℕ := by
  classical
  exact (tgraph G F B).degree v

/-- One step of the process. `reduce`: a core vertex of torso degree at most two is
removed from the core (reduction operations (R1)–(R4) of Definition 4.2 (`def:reductions`), applied to
the torso). `delete`: a core vertex is deleted from the graph. -/
inductive Step (G : SimpleGraph (Fin n)) :
    Finset (Fin n) × Finset (Fin n) → Finset (Fin n) × Finset (Fin n) → Prop
  | reduce {F B : Finset (Fin n)} {v : Fin n} :
      v ∈ B → tdeg G F B v ≤ 2 → Step G (F, B) (F, B.erase v)
  | delete {F B : Finset (Fin n)} {w : Fin n} :
      w ∈ B → Step G (F, B) (F.erase w, B.erase w)

/-- Finite sequences of steps. Along `Reach G (F, B) (F', B')` the deleted set is
`F \ F'`. -/
def Reach (G : SimpleGraph (Fin n)) :
    Finset (Fin n) × Finset (Fin n) → Finset (Fin n) × Finset (Fin n) → Prop :=
  Relation.ReflTransGen (Step G)

/-- A state reachable from the initial state `(univ, univ)`. -/
def Good (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) : Prop :=
  Reach G (Finset.univ, Finset.univ) (F, B)

/-- `ψ_b` of the torso: `∑_{v ∈ B} b (tdeg v)`. -/
def psi (b : ℕ → ℝ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) : ℝ :=
  ∑ v ∈ B, b (tdeg G F B v)

/-- The torso components, as subsets of `B` (connected components of the torso). -/
def tcomps (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) : Finset (Finset (Fin n)) :=
  components (tgraph G F B) B

/-- Minimum torso degree on `C` (`0` for empty `C`). -/
def cmin (G : SimpleGraph (Fin n)) (F B C : Finset (Fin n)) : ℕ :=
  if h : C.Nonempty then C.inf' h (tdeg G F B) else 0

/-- The potential `ψ⁻ = ψ - ∑_{torso components C} H_{δ(C)}` of the manuscript, with
`H_d = runMin b d`. -/
def psiMinus (b : ℕ → ℝ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) : ℝ :=
  psi b G F B - ∑ C ∈ tcomps G F B, runMin b (cmin G F B C)

/-- Definition 9.8 (`def:basic`) with `k = 5`, for a torso component `C` of the state `(F, B)`: either
the maximum torso degree on `C` is at most `5`, or there is `v ∈ C` such that deleting
`v` and then reducing removes all of `C` from the core.

Deviation (harmless): the second alternative is stated on the whole state, as "some
sequence of steps whose only deletion is `v` reaches a core disjoint from `C`"; the
manuscript applies a maximal sequence of reductions to `J - v` for the component `J`.
The manuscript's condition implies this one (reductions inside one torso component are
reductions of the whole torso, (F2)), and `KindTwoClaim` shows that this one still
gives the bound of Lemma 9.11 (`lem:basic`). -/
def Basic (G : SimpleGraph (Fin n)) (F B C : Finset (Fin n)) : Prop :=
  (∀ v ∈ C, tdeg G F B v ≤ 5) ∨
    ∃ v ∈ C, ∃ B'' : Finset (Fin n), Reach G (F, B) (F.erase v, B'') ∧ Disjoint B'' C

/-! ## (E2) `StateClaim`: torso semantics and Lemma 4.5 (`lem:reduction`) -/

/-- (E2a) Torso semantics of the steps, at every good state `(F, B)`:

1. deleting a core vertex `w` deletes `w` from the torso and changes nothing else;
2. removing a core vertex `v` of torso degree at most two from the core is the
   reduction (R1)–(R4) at `v`: `v` disappears and its two torso neighbours (if it
   has two) become adjacent;
3. (F3) of the manuscript: a maximal sequence of reductions exists; its final core
   has minimum torso degree at least `3` (or is empty), and no torso degree increased
   ((F1)).

Part 1 holds for every state with `w ∈ B`; part 2 uses that in a good state every
component of `G[F \ B]` has at most two attachment vertices. -/
def TorsoDynamics : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)), Good G F B →
    (∀ w ∈ B, ∀ x y : Fin n,
        (tgraph G (F.erase w) (B.erase w)).Adj x y ↔
          (tgraph G F B).Adj x y ∧ x ≠ w ∧ y ≠ w) ∧
    (∀ v ∈ B, tdeg G F B v ≤ 2 → ∀ x y : Fin n,
        (tgraph G F (B.erase v)).Adj x y ↔
          x ≠ v ∧ y ≠ v ∧ ((tgraph G F B).Adj x y ∨
            (x ≠ y ∧ (tgraph G F B).Adj x v ∧ (tgraph G F B).Adj y v))) ∧
    (∃ B' ⊆ B, Reach G (F, B) (F, B') ∧ (∀ v ∈ B', 3 ≤ tdeg G F B' v) ∧
        ∀ v ∈ B', tdeg G F B' v ≤ tdeg G F B v)

/-- (E2b) Lemma 4.5 (`lem:reduction`) ("reductions are paid once") in state form: if a good state
`(F, B)` reaches `(F', B')`, then
`pw(torso(F, B)) ≤ |F \ F'| + pw(torso(F', B')) + 12 √n + 1`.

Deviation: the remainder is `12 √n + 1` (balanced separators of the reduction pieces,
`T2.Piece.section_decomposition`, and `insert_components`) instead of
`3 log₂ n + 4`; any `o(n)` remainder suffices for Lemma 9.3 (`lem:bootstrap`). With
`(F, B) = (univ, univ)` the left side is `pw(G)` (`hasPathwidth_of_coreTorso_univ`). -/
def LiftClaim : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B F' B' : Finset (Fin n)) (p : ℝ),
    Good G F B → Reach G (F, B) (F', B') →
    HasPathwidthAtMost (coreTorso G F' B') p →
    HasPathwidthAtMost (coreTorso G F B)
      (((F \ F').card : ℝ) + p + 12 * Real.sqrt (n : ℝ) + 1)

/-- (E2c) Second case of Lemma 9.11 (`lem:basic`): if `C` is a torso component of a good state and
some sequence of steps whose only deletion is `v ∈ C` removes all of `C` from the core,
then the torso component `C` has pathwidth at most `1 + (-1) + 12 √n + 1`.

The torso component is written `coreTorso G (F \ (B \ C)) C`: the torso of the state
obtained by deleting the other core vertices `B \ C`. Its edges are exactly the torso
edges of `(F, B)` inside `C`, relabelled by `enumerate C`.

Proof route in the manuscript: Lemma 4.5 (`lem:reduction`) applied to `J = torso[C]` with
`D = {v}` and empty final graph. Reductions outside `C` do not affect `C` ((F2)). -/
def KindTwoClaim : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B C B'' : Finset (Fin n)) (v : Fin n),
    Good G F B → C ∈ tcomps G F B → v ∈ C →
    Reach G (F, B) (F.erase v, B'') → Disjoint B'' C →
    HasPathwidthAtMost (coreTorso G (F \ (B \ C)) C) (12 * Real.sqrt (n : ℝ) + 1)

/-- (E2) The state machinery: torso semantics, Lemma 4.5 (`lem:reduction`), second case of
Lemma 9.11 (`lem:basic`). -/
def StateClaim : Prop := TorsoDynamics ∧ LiftClaim ∧ KindTwoClaim

/-! ## (E3) `BasicClaim`: the potential and the first case of Lemma 9.11 (`lem:basic`) -/

/-- (E3a) The facts about `ψ⁻` used in the proof of Lemma 9.3 (`lem:bootstrap`) (paragraph
"The potential"): `ψ⁻ ≥ 0` when the torso has minimum degree at least `3`, and
`ψ⁻ ≤ ψ` because `H ≥ 0`. -/
def PsiClaim : Prop :=
  ∀ b : ℕ → ℝ, BootProps b →
    ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)),
      (∀ v ∈ B, 3 ≤ tdeg G F B v) →
      0 ≤ psiMinus b G F B ∧ psiMinus b G F B ≤ psi b G F B

/-- (E3b) First case of Lemma 9.11 (`lem:basic`), assembled over the torso components (the bullet
"The final graph" in the proof of Lemma 9.3 (`lem:bootstrap`)). Let the base bound for maximum
degree `5` hold (the hypothesis of `BootstrapClaim`). For every `ε > 0` there is `N₀`
such that: for every good state with torso minimum degree at least `3` and every
`q`, if each torso component either has maximum torso degree at most `5` or has
pathwidth at most `q`, then
`pw(torso) ≤ max (ψ⁻ + b₃ + ε n + N₀) q`.

The first alternative is handled by the base bound applied to the relabelled torso
component `coreTorso G (F \ (B \ C)) C` (whose degrees are the torso degrees on `C`),
using `ψ(C) = ψ⁻(C) + H_{δ(C)} ≤ ψ⁻(C) + b₃` and `ψ⁻(C) ≤ ψ⁻` (the other components
have `ψ⁻ ≥ 0`); components with fewer than `N₀` vertices use the trivial bound. The
pathwidth of the torso is the maximum over its components.

Deviation: the remainder `ρ(n)` of the manuscript is replaced by `ε n + N₀`, the form
in which `BootstrapClaim` supplies the base bound. The hypothesis `Good` is not needed
for the truth of the statement and is included only for convenience. -/
def ComponentClaim : Prop :=
  ∀ b : ℕ → ℝ, BootProps b →
    (∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      MaxDegreeAtMost 5 G → HasPathwidthAtMost G (degreeWeight G b + ε * n)) →
    ∀ ε : ℝ, 0 < ε → ∃ N₀ : ℕ,
      ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)),
        Good G F B → (∀ v ∈ B, 3 ≤ tdeg G F B v) → ∀ q : ℝ,
        (∀ C ∈ tcomps G F B, (∀ v ∈ C, tdeg G F B v ≤ 5) ∨
          HasPathwidthAtMost (coreTorso G (F \ (B \ C)) C) q) →
        HasPathwidthAtMost (coreTorso G F B)
          (max (psiMinus b G F B + b 3 + ε * n + N₀) q)

/-- (E3) Lemma 9.11 (`lem:basic`) (first case) and the facts about `ψ⁻`. -/
def BasicClaim : Prop := PsiClaim ∧ ComponentClaim

/-! ## (E4) `DeletionClaim`: the deletion process -/

/-- (E4) Proposition 9.10 (`prop:deletion`) with `k = 5`: from a good state whose torso has minimum
degree at least `3` (or is empty), some finite sequence of deletions and reductions
reaches a state whose torso has minimum degree at least `3` (or is empty) and all of
whose torso components are basic, and the deleted set `X = F \ F'` satisfies
`|X| + ψ⁻(F', B') ≤ ψ⁻(F, B)`.

The torso semantics `TorsoDynamics` (part of `StateClaim`) is an explicit hypothesis:
with it, the proof is about the evolving graph `tgraph` only (Cases 1, 2a, 2b of the
manuscript, the claim on `J₄`, and the identity `1 - b_Δ = (Δ-1) H_Δ + H_{Δ-1}`,
`BootProps.identity`, for `Δ ≥ 6`). -/
def DeletionClaim : Prop :=
  TorsoDynamics →
    ∀ b : ℕ → ℝ, BootProps b →
      ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)),
        Good G F B → (∀ v ∈ B, 3 ≤ tdeg G F B v) →
        ∃ F' B' : Finset (Fin n), Reach G (F, B) (F', B') ∧
          (∀ v ∈ B', 3 ≤ tdeg G F' B' v) ∧
          (∀ C ∈ tcomps G F' B', Basic G F' B' C) ∧
          ((F \ F').card : ℝ) + psiMinus b G F' B' ≤ psiMinus b G F B

/-! ## Proved helper lemmas (usable by all children) -/

theorem Reach.trans {G : SimpleGraph (Fin n)} {s t u : Finset (Fin n) × Finset (Fin n)}
    (h₁ : Reach G s t) (h₂ : Reach G t u) : Reach G s u :=
  Relation.ReflTransGen.trans h₁ h₂

theorem Reach.refl (G : SimpleGraph (Fin n)) (s : Finset (Fin n) × Finset (Fin n)) :
    Reach G s s :=
  Relation.ReflTransGen.refl

theorem Reach.single {G : SimpleGraph (Fin n)} {s t : Finset (Fin n) × Finset (Fin n)}
    (h : Step G s t) : Reach G s t :=
  Relation.ReflTransGen.single h

theorem Good.reach {G : SimpleGraph (Fin n)} {F B F' B' : Finset (Fin n)}
    (h : Good G F B) (h' : Reach G (F, B) (F', B')) : Good G F' B' :=
  Reach.trans h h'

theorem good_univ (G : SimpleGraph (Fin n)) : Good G Finset.univ Finset.univ :=
  Reach.refl G _

/-- Steps only shrink both sets. -/
theorem Reach.subset {G : SimpleGraph (Fin n)} {s t : Finset (Fin n) × Finset (Fin n)}
    (h : Reach G s t) : t.1 ⊆ s.1 ∧ t.2 ⊆ s.2 := by
  induction h with
  | refl => exact ⟨Finset.Subset.rfl, Finset.Subset.rfl⟩
  | tail _ hs ih =>
    cases hs with
    | reduce _ _ => exact ⟨ih.1, (Finset.erase_subset _ _).trans ih.2⟩
    | delete _ =>
      exact ⟨(Finset.erase_subset _ _).trans ih.1, (Finset.erase_subset _ _).trans ih.2⟩

/-- In a good state the core lies inside the undeleted vertices. -/
theorem Good.subset {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (h : Good G F B) :
    B ⊆ F := by
  have key : ∀ t : Finset (Fin n) × Finset (Fin n),
      Reach G (Finset.univ, Finset.univ) t → t.2 ⊆ t.1 := by
    intro t ht
    induction ht with
    | refl => exact Finset.Subset.rfl
    | tail _ hs ih =>
      cases hs with
      | reduce _ _ => exact (Finset.erase_subset _ _).trans ih
      | delete _ => exact Finset.erase_subset_erase _ ih
  exact key _ h

/-- Deleting a set `S` of core vertices, one at a time. -/
theorem reach_delete_set (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) :
    ∀ S : Finset (Fin n), S ⊆ B → Reach G (F, B) (F \ S, B \ S) := by
  classical
  intro S
  induction S using Finset.induction_on with
  | empty => simpa using Reach.refl G (F, B)
  | @insert a S ha ih =>
    intro hS
    have h1 := ih ((Finset.subset_insert a S).trans hS)
    have haB : a ∈ B \ S := Finset.mem_sdiff.mpr ⟨hS (Finset.mem_insert_self a S), ha⟩
    have h2 := Reach.single (Step.delete (G := G) (F := F \ S) haB)
    have e1 : (F \ S).erase a = F \ insert a S := by
      ext x; simp [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert]; tauto
    have e2 : (B \ S).erase a = B \ insert a S := by
      ext x; simp [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert]; tauto
    rw [e1, e2] at h2
    exact h1.trans h2

/-- The torso of the initial state is `G`. -/
theorem tgraph_univ (G : SimpleGraph (Fin n)) :
    tgraph G Finset.univ Finset.univ = G := by
  classical
  ext u v
  simp only [tgraph, Finset.mem_univ, true_and, Finset.sdiff_self]
  have hc : components G (∅ : Finset (Fin n)) = ∅ := by
    unfold components
    simp
  rw [hc]
  constructor
  · rintro ⟨_, h | ⟨T, hT, _⟩⟩
    · exact h
    · simp at hT
  · intro h
    exact ⟨G.ne_of_adj h, Or.inl h⟩

theorem degree_congr {H H' : SimpleGraph (Fin n)} (h : H = H') (v : Fin n)
    [Fintype (H.neighborSet v)] [Fintype (H'.neighborSet v)] :
    H.degree v = H'.degree v := by
  subst h
  congr 1
  exact Subsingleton.elim _ _

/-- Torso degrees of the initial state are the degrees of `G`. -/
theorem tdeg_univ (G : SimpleGraph (Fin n)) (v : Fin n) [Fintype (G.neighborSet v)] :
    tdeg G Finset.univ Finset.univ v = G.degree v := by
  classical
  unfold tdeg
  exact degree_congr (tgraph_univ G) v

/-- The potential of the initial state is `∑_v b(d(v))`. -/
theorem psi_univ (b : ℕ → ℝ) (G : SimpleGraph (Fin n)) :
    psi b G Finset.univ Finset.univ = degreeWeight G b := by
  classical
  unfold psi degreeWeight
  apply Finset.sum_congr rfl
  intro v _
  rw [tdeg_univ]

/-- `coreTorso` is the relabelled `tgraph`. -/
theorem coreTorso_adj_iff (G : SimpleGraph (Fin n)) (F B : Finset (Fin n))
    (i j : Fin B.card) :
    (coreTorso G F B).Adj i j ↔ (tgraph G F B).Adj (enumerate B i) (enumerate B j) := by
  have hi : enumerate B i ∈ B := (mem_iff_enumerate B _).mpr ⟨i, rfl⟩
  have hj : enumerate B j ∈ B := (mem_iff_enumerate B _).mpr ⟨j, rfl⟩
  constructor
  · rintro ⟨hne, h⟩
    exact ⟨fun he => hne ((enumerate B).injective he), hi, hj, h⟩
  · rintro ⟨hne, _, _, h⟩
    exact ⟨fun he => hne (by rw [he]), h⟩

/-- Pathwidth of `G` from pathwidth of the torso of the initial state. -/
theorem hasPathwidth_of_coreTorso_univ (G : SimpleGraph (Fin n)) {p : ℝ}
    (h : HasPathwidthAtMost (coreTorso G Finset.univ Finset.univ) p) :
    HasPathwidthAtMost G p := by
  obtain ⟨D, hD⟩ := h
  exact ⟨(liftTorso G Finset.univ Finset.univ D).toFull,
    toFull_width _ (liftTorso_width G Finset.univ Finset.univ D hD)⟩

/-- The torso with empty core has pathwidth `-1`. -/
theorem coreTorso_empty_pw (G : SimpleGraph (Fin n)) (F : Finset (Fin n)) :
    HasPathwidthAtMost (coreTorso G F ∅) (-1) := by
  simpa using trivial_pathwidth_bound (coreTorso G F ∅)

/-! ## Sequence facts -/

theorem BootProps.monotone {b : ℕ → ℝ} (hb : BootProps b) : Monotone b := by
  apply monotone_nat_of_le_succ
  intro d
  rcases Nat.lt_or_ge d 2 with h | h
  · interval_cases d
    · rw [hb.zero.1, hb.zero.2.1]
    · rw [hb.zero.2.1, hb.zero.2.2]
  · have := hb.mono (d + 1) (by omega)
    simpa using this

theorem BootProps.nonneg {b : ℕ → ℝ} (hb : BootProps b) (d : ℕ) : 0 ≤ b d := by
  have := hb.monotone (Nat.zero_le d)
  rw [hb.zero.1] at this
  exact this

/-- `ψ` does not increase when the core shrinks and torso degrees do not increase. -/
theorem psi_le_psi {b : ℕ → ℝ} (hb : BootProps b) {G : SimpleGraph (Fin n)}
    {F B F' B' : Finset (Fin n)} (hsub : B' ⊆ B)
    (hdeg : ∀ v ∈ B', tdeg G F' B' v ≤ tdeg G F B v) :
    psi b G F' B' ≤ psi b G F B := by
  unfold psi
  calc ∑ v ∈ B', b (tdeg G F' B' v) ≤ ∑ v ∈ B', b (tdeg G F B v) :=
        Finset.sum_le_sum fun v hv => hb.monotone (hdeg v hv)
    _ ≤ ∑ v ∈ B, b (tdeg G F B v) :=
        Finset.sum_le_sum_of_subset_of_nonneg hsub (fun v _ _ => hb.nonneg _)

end T4
end CubicPathwidth