CubicPathwidth.PwSeq.BootDeletion

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

import CubicPathwidth.PwSeq.BootSeq

/-!
# The deletion process for base degree `k` (Proposition 9.10, `prop:deletion`)

Generalized copy of `T4/DeletionXArith.lean` (`deletion_core_ineq`), the `BootProps`
part of `T4/DeletionXKey.lean` (`comp_sum_ge`, `claim_J`, `key_step`) and
`T4/DeletionX.lean` (`deletion_x`), for a sequence with `BootPropsK k b`. The
`k`-independent torso machinery (`DelX.tcomp_preserve`, `DelX.td_maxred`,
`DelX.tdeg_delete`, `DelX.psi_delete`, `DelX.choose_center`, ...) is reused.

Route note. The `k = 5` proof assumes `Δ ≥ 6` for the maximum torso degree `Δ` of a
non-basic component. Here a non-basic component has `Δ ≥ k + 1 ≥ 4`, which is all that
the arithmetic `deletion_core_ineq` uses (it needs `Δ - 1 ≥ 3`, and `Δ ≥ 2` for a second
neighbour of the centre); the identity `1 - b_Δ = (Δ-1) H_Δ + H_{Δ-1}` is
`BootPropsK.identity` at `Δ ≥ k + 1`.
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq
namespace Boot

open T2 T4 DelX SectionDecomposition

variable {n : ℕ}

theorem deletion_core_ineq {α : Type*} [DecidableEq α] {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b)
    (C N : Finset α) (w : α) (d d' : α → ℕ) (Δ δ : ℕ) (J : ℝ)
    (hΔ : 4 ≤ Δ)
    (hCd : ∀ v ∈ C, 3 ≤ d v ∧ d v ≤ Δ)
    (hwd : d w = Δ)
    (hNC : N ⊆ C.erase w) (hNcard : N.card = Δ)
    (hd'N : ∀ v ∈ N, d' v + 1 = d v)
    (hd'o : ∀ v ∈ C.erase w, v ∉ N → d' v = d v)
    (hδ : ∀ v ∈ C, δ ≤ d v) (hδ' : ∃ v ∈ C, d v = δ)
    (hreg : (∀ v ∈ C, d v = Δ) ∨ ∃ x ∈ N, d x < Δ)
    (hJ : ∀ u ∈ C.erase w, 3 ≤ d' u → T4.runMin b (d' u) ≤ J)
    (hstar : ∃ u ∈ C.erase w, 3 ≤ d' u) :
    ((Δ : ℝ) - 1) * T4.runMin b Δ + T4.runMin b (Δ - 1) + T4.runMin b δ ≤
      ∑ v ∈ N, T4.incr b (d v) + J := by
  have hH0 := hb.runMin_nonneg
  have hNne : N.Nonempty := by
    rw [← Finset.card_pos, hNcard]; omega
  obtain ⟨v₁, hv₁N, hv₁min⟩ := Finset.exists_min_image N d hNne
  have hv₁C : v₁ ∈ C := Finset.mem_of_mem_erase (hNC hv₁N)
  have hv₁w : v₁ ≠ w := Finset.ne_of_mem_erase (hNC hv₁N)
  have hdN : ∀ v ∈ N, 3 ≤ d v ∧ d v ≤ Δ := fun v hv =>
    hCd v (Finset.mem_of_mem_erase (hNC hv))
  have hterm : ∀ v ∈ N.erase v₁, 0 ≤ T4.incr b (d v) - T4.runMin b Δ := by
    intro v hv
    have h1 := hdN v (Finset.mem_of_mem_erase hv)
    have h2 := runMin_anti b h1.2
    have h3 := runMin_le_incr b h1.1
    linarith
  set R := ∑ v ∈ N.erase v₁, (T4.incr b (d v) - T4.runMin b Δ) with hR
  have hRnn : 0 ≤ R := Finset.sum_nonneg hterm
  have hsum : ∑ v ∈ N, T4.incr b (d v) =
      T4.incr b (d v₁) + R + ((Δ : ℝ) - 1) * T4.runMin b Δ := by
    rw [← Finset.add_sum_erase N _ hv₁N]
    rw [hR, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_erase_of_mem hv₁N, hNcard,
      nsmul_eq_mul]
    have : ((Δ - 1 : ℕ) : ℝ) = (Δ : ℝ) - 1 := by
      rw [Nat.cast_sub (by omega)]; simp
    rw [this]
    ring
  rw [hsum]
  suffices key : T4.runMin b (Δ - 1) + T4.runMin b δ ≤ T4.incr b (d v₁) + R + J by linarith
  have hd₁ := hdN v₁ hv₁N
  have hd₁h : T4.runMin b (d v₁) ≤ T4.incr b (d v₁) := runMin_le_incr b hd₁.1
  rcases hreg with hall | ⟨x, hxN, hxlt⟩
  · -- Case 1: regular
    have hδΔ : δ = Δ := by
      obtain ⟨v, hv, hvd⟩ := hδ'
      rw [← hvd]; exact hall v hv
    have hd1 : d v₁ = Δ := hall v₁ hv₁C
    have hd'1 : d' v₁ = Δ - 1 := by
      have := hd'N v₁ hv₁N; omega
    have hJ1 := hJ v₁ (hNC hv₁N) (by omega)
    rw [hd'1] at hJ1
    rw [hδΔ]
    rw [hd1] at hd₁h ⊢
    linarith
  · -- Case 2: not regular
    have hxC : x ∈ C := Finset.mem_of_mem_erase (hNC hxN)
    have hd1lt : d v₁ < Δ := lt_of_le_of_lt (hv₁min x hxN) hxlt
    have hJ1 : T4.runMin b (Δ - 1) ≤ T4.incr b (d v₁) :=
      (runMin_anti b (by omega : d v₁ ≤ Δ - 1)).trans hd₁h
    by_cases h2a : ∃ u ∈ C.erase w, 3 ≤ d' u ∧ d' u ≤ δ
    · obtain ⟨u, hu, hu3, huδ⟩ := h2a
      have := (runMin_anti b huδ).trans (hJ u hu hu3)
      linarith
    · push Not at h2a
      obtain ⟨u₀, hu₀C, hu₀d⟩ := hδ'
      have hδlt : δ < Δ := lt_of_le_of_lt (hδ x hxC) hxlt
      have hu₀w : u₀ ≠ w := by
        intro h; rw [h, hwd] at hu₀d; omega
      have hu₀E : u₀ ∈ C.erase w := Finset.mem_erase.mpr ⟨hu₀w, hu₀C⟩
      have hδ3 : 3 ≤ δ := hu₀d ▸ (hCd u₀ hu₀C).1
      have hδeq : δ = 3 := by
        by_contra hne
        have h4 : 4 ≤ δ := by omega
        by_cases hn : u₀ ∈ N
        · have := hd'N u₀ hn
          have := h2a u₀ hu₀E (by omega)
          omega
        · have := hd'o u₀ hu₀E hn
          have := h2a u₀ hu₀E (by omega)
          omega
      have hu₀N : u₀ ∈ N := by
        by_contra hn
        have := hd'o u₀ hu₀E hn
        have := h2a u₀ hu₀E (by omega)
        omega
      have hd1eq : d v₁ = 3 := by
        have := hv₁min u₀ hu₀N
        have := hd₁.1
        omega
      have hHδ : T4.runMin b δ = T4.incr b (d v₁) := by
        rw [hδeq, hd1eq, runMin_three]
      suffices key2 : T4.runMin b (Δ - 1) ≤ R + J by linarith
      by_cases hx4 : ∃ x ∈ N, 4 ≤ d x
      · obtain ⟨x, hxN, hx4⟩ := hx4
        have h1 := hd'N x hxN
        have h2 := hdN x hxN
        have := hJ x (hNC hxN) (by omega)
        have h3 := runMin_anti b (by omega : d' x ≤ Δ - 1)
        linarith
      · push Not at hx4
        have hall3 : ∀ x ∈ N, d x = 3 := fun x hx => by
          have := hx4 x hx
          have := (hdN x hx).1
          omega
        have hcard : 0 < (N.erase v₁).card := by
          rw [Finset.card_erase_of_mem hv₁N, hNcard]; omega
        obtain ⟨v₂, hv₂⟩ := Finset.card_pos.mp hcard
        have hv₂N : v₂ ∈ N := Finset.mem_of_mem_erase hv₂
        have hRge : T4.incr b (d v₂) - T4.runMin b Δ ≤ R :=
          Finset.single_le_sum hterm hv₂
        rw [hall3 v₂ hv₂N] at hRge
        obtain ⟨u, hu, hu3⟩ := hstar
        have hun : u ∉ N := by
          intro hn
          have := hd'N u hn
          have := hall3 u hn
          omega
        have hdu := hd'o u hu hun
        have hCu := hCd u (Finset.mem_of_mem_erase hu)
        have hJu := hJ u hu hu3
        rw [hdu] at hJu
        have h5 := runMin_anti b hCu.2
        have h6 := runMin_anti b (by omega : 3 ≤ Δ - 1)
        rw [runMin_three] at h6
        linarith

/-- The `H`-terms: components other than `C` survive, and a surviving vertex `u` of `C`
contributes a new component inside `C`. -/
theorem comp_sum_ge (hdyn : TorsoDynamics) {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b)
    {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (hg : Good G F B)
    (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) {C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    {w : Fin n} (hwC : w ∈ C) {B' : Finset (Fin n)}
    (hR : Reach G (F, B) (F.erase w, B')) :
    (∑ D ∈ (tcomps G F B).erase C, T4.runMin b (cmin G F B D) ≤
      ∑ D ∈ tcomps G (F.erase w) B', T4.runMin b (cmin G (F.erase w) B' D)) ∧
    (∀ u ∈ C, u ∈ B' →
      T4.runMin b (tdeg G (F.erase w) B' u) +
        ∑ D ∈ (tcomps G F B).erase C, T4.runMin b (cmin G F B D) ≤
      ∑ D ∈ tcomps G (F.erase w) B', T4.runMin b (cmin G (F.erase w) B' D)) := by
  classical
  have hFB : B ⊆ F := hg.subset
  have hpres : ∀ C' ∈ (tcomps G F B).erase C,
      C' ∈ tcomps G (F.erase w) B' ∧ cmin G (F.erase w) B' C' = cmin G F B C' := by
    intro C' hC'
    obtain ⟨hne, hC'm⟩ := Finset.mem_erase.mp hC'
    have hdisj := components_disjoint (tgraph G F B) hC'm hC (hne)
    have hwC' : w ∉ C' := fun h => Finset.disjoint_left.mp hdisj h hwC
    have hC'B := (mem_components (tgraph G F B) hC'm).1
    exact tcomp_preserve hdyn hg hmin hR hC'm (fun x hx =>
      Finset.mem_erase.mpr ⟨fun h => hwC' (h ▸ hx), hFB (hC'B hx)⟩)
  have hsub : (tcomps G F B).erase C ⊆ tcomps G (F.erase w) B' := fun C' hC' =>
    (hpres C' hC').1
  have heqsum : ∑ D ∈ (tcomps G F B).erase C, T4.runMin b (cmin G (F.erase w) B' D) =
      ∑ D ∈ (tcomps G F B).erase C, T4.runMin b (cmin G F B D) :=
    Finset.sum_congr rfl fun D hD => by rw [(hpres D hD).2]
  refine ⟨?_, ?_⟩
  · rw [← heqsum]
    exact Finset.sum_le_sum_of_subset_of_nonneg hsub (fun D _ _ => hb.runMin_nonneg _)
  · intro u huC huB'
    have hDu : component (tgraph G (F.erase w) B') B' u ∈ tcomps G (F.erase w) B' :=
      component_mem_tcomps huB'
    have hDuC := reach_component_subset hdyn hg hR hC huC huB'
    have huDu : u ∈ component (tgraph G (F.erase w) B') B' u := mem_component_self _ huB'
    have hnot : component (tgraph G (F.erase w) B') B' u ∉ (tcomps G F B).erase C := by
      intro hmem
      obtain ⟨hne, hm⟩ := Finset.mem_erase.mp hmem
      have hdisj := components_disjoint (tgraph G F B) hm hC hne
      exact Finset.disjoint_left.mp hdisj huDu huC
    have hsub2 : insert (component (tgraph G (F.erase w) B') B' u) ((tcomps G F B).erase C) ⊆
        tcomps G (F.erase w) B' := by
      intro D hD
      rcases Finset.mem_insert.mp hD with rfl | hD
      · exact hDu
      · exact hsub hD
    have h1 := Finset.sum_le_sum_of_subset_of_nonneg
      (f := fun D => T4.runMin b (cmin G (F.erase w) B' D)) hsub2
      (fun D _ _ => hb.runMin_nonneg _)
    rw [Finset.sum_insert hnot, heqsum] at h1
    have hle : cmin G (F.erase w) B' (component (tgraph G (F.erase w) B') B' u) ≤
        tdeg G (F.erase w) B' u := by
      unfold cmin
      have hne : (component (tgraph G (F.erase w) B') B' u).Nonempty := ⟨u, huDu⟩
      simp only [hne, dite_true]
      exact Finset.inf'_le _ huDu
    have h2 := runMin_anti b hle
    linarith

/-- The Claim of the manuscript: if `u ∈ C - w` has degree `j ≥ 3` after the deletion
of `w`, then `J₄ ≥ H_j`. -/
theorem claim_J (hdyn : TorsoDynamics) {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b)
    {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (hg : Good G F B)
    (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) {C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    {w : Fin n} (hwC : w ∈ C) {B' : Finset (Fin n)} (hB'sub : B' ⊆ B.erase w)
    (hR : Reach G (F, B) (F.erase w, B'))
    (hdeg' : ∀ v ∈ B', tdeg G (F.erase w) B' v ≤ tdeg G (F.erase w) (B.erase w) v) :
    ∀ u ∈ C.erase w, 3 ≤ tdeg G (F.erase w) (B.erase w) u →
      T4.runMin b (tdeg G (F.erase w) (B.erase w) u) ≤ Jval b G F B C w B' := by
  classical
  intro u hu hu3
  have huC := Finset.mem_of_mem_erase hu
  obtain ⟨hs1, hs2⟩ := Boot.comp_sum_ge hdyn hb hg hmin hC hwC hR
  have hpsi : psi b G (F.erase w) B' ≤ psi b G (F.erase w) (B.erase w) :=
    Boot.psi_le_psi hb hB'sub hdeg'
  unfold Jval
  by_cases huB' : u ∈ B'
  · have h1 := hs2 u huC huB'
    have h2 := runMin_anti b (hdeg' u huB')
    linarith
  · have huBw : u ∈ B.erase w := Finset.mem_erase.mpr ⟨Finset.ne_of_mem_erase hu, 
      (mem_components (tgraph G F B) (show C ∈ components (tgraph G F B) B from hC)).1 huC⟩
    have hsd := Finset.sum_sdiff (f := fun v => b (tdeg G (F.erase w) (B.erase w) v)) hB'sub
    have hmono : ∑ v ∈ B', b (tdeg G (F.erase w) B' v) ≤
        ∑ v ∈ B', b (tdeg G (F.erase w) (B.erase w) v) :=
      Finset.sum_le_sum fun v hv => Boot.monotone hb (hdeg' v hv)
    have hsingle : b (tdeg G (F.erase w) (B.erase w) u) ≤
        ∑ v ∈ (B.erase w) \ B', b (tdeg G (F.erase w) (B.erase w) v) :=
      Finset.single_le_sum (f := fun v => b (tdeg G (F.erase w) (B.erase w) v))
        (fun v _ => Boot.nonneg hb _) (Finset.mem_sdiff.mpr ⟨huBw, huB'⟩)
    have h3 := Boot.runMin_le_b hb hu3
    unfold psi at *
    linarith

/-- One round of the process on a non-basic torso component. -/
theorem key_step (hdyn : TorsoDynamics) {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b)
    {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (hg : Good G F B)
    (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) {C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    (hnb : ¬ BasicK k G F B C) :
    ∃ w ∈ B, ∃ B' ⊆ B.erase w, Reach G (F, B) (F.erase w, B') ∧
      (∀ v ∈ B', 3 ≤ tdeg G (F.erase w) B' v) ∧
      1 + psiMinus b G (F.erase w) B' ≤ psiMinus b G F B := by
  classical
  obtain ⟨hCB, hcl, hconn⟩ := mem_components (tgraph G F B) hC
  have hCne : C.Nonempty := hconn.1
  -- non-basic: unpack
  have hbig : ∃ v ∈ C, k < tdeg G F B v := by
    by_contra h
    apply hnb
    left
    intro v hv
    by_contra h'
    exact h ⟨v, hv, by omega⟩
  have hnodel : ∀ v ∈ C, ∀ B'' : Finset (Fin n), Reach G (F, B) (F.erase v, B'') →
      ¬ Disjoint B'' C := fun v hv B'' hr hd => hnb (Or.inr ⟨v, hv, B'', hr, hd⟩)
  -- the maximum degree
  obtain ⟨w₀, hw₀C, hw₀max⟩ := Finset.exists_max_image C (tdeg G F B) hCne
  set Δ := tdeg G F B w₀ with hΔdef
  have hΔ : k + 1 ≤ Δ := by
    obtain ⟨v, hv, h5⟩ := hbig
    have := hw₀max v hv
    omega
  obtain ⟨w, hwC, hwd, hreg0⟩ := choose_center hconn (tdeg G F B) hw₀max ⟨w₀, hw₀C, rfl⟩
  have hwB : w ∈ B := hCB hwC
  -- the deletion and the maximal reduction
  have hstep : Step G (F, B) (F.erase w, B.erase w) := Step.delete hwB
  have hg1 : Good G (F.erase w) (B.erase w) := hg.reach (Reach.single hstep)
  obtain ⟨B', hB'sub, hRed, hmin', hdeg'⟩ := td_maxred hdyn hg1
  have hR : Reach G (F, B) (F.erase w, B') := (Reach.single hstep).trans hRed
  -- some vertex of C survives
  obtain ⟨u₁, hu₁B', hu₁C⟩ := Finset.not_disjoint_iff.mp (hnodel w hwC B' hR)
  -- the data for the arithmetic lemma
  have hCd : ∀ v ∈ C, 3 ≤ tdeg G F B v ∧ tdeg G F B v ≤ Δ :=
    fun v hv => ⟨hmin v (hCB hv), hw₀max v hv⟩
  have hNC : nbrs G F B w ⊆ C.erase w := by
    intro u hu
    have h := mem_nbrs.mp hu
    refine Finset.mem_erase.mpr ⟨h.1.symm, ?_⟩
    exact hcl w hwC u h.2.2.1 h
  have hNcard : (nbrs G F B w).card = Δ := by
    rw [← tdeg_eq_card_nbrs]; exact hwd
  have hd'N : ∀ v ∈ nbrs G F B w,
      tdeg G (F.erase w) (B.erase w) v + 1 = tdeg G F B v := by
    intro v hv
    have hvw : v ≠ w := Finset.ne_of_mem_erase (nbrs_subset_erase hv)
    have := tdeg_delete hdyn hg hwB hvw
    simpa [hv] using this
  have hd'o : ∀ v ∈ C.erase w, v ∉ nbrs G F B w →
      tdeg G (F.erase w) (B.erase w) v = tdeg G F B v := by
    intro v hv hvn
    have hvw : v ≠ w := Finset.ne_of_mem_erase hv
    have := tdeg_delete hdyn hg hwB hvw
    simpa [hvn] using this
  have hδ : ∀ v ∈ C, cmin G F B C ≤ tdeg G F B v := by
    intro v hv
    unfold cmin
    simp only [hCne, dite_true]
    exact Finset.inf'_le _ hv
  have hδ' : ∃ v ∈ C, tdeg G F B v = cmin G F B C := by
    unfold cmin
    simp only [hCne, dite_true]
    obtain ⟨v, hv, h⟩ := Finset.exists_mem_eq_inf' hCne (tdeg G F B)
    exact ⟨v, hv, h.symm⟩
  have hreg : (∀ v ∈ C, tdeg G F B v = Δ) ∨ ∃ x ∈ nbrs G F B w, tdeg G F B x < Δ := by
    rcases hreg0 with h | ⟨x, hx, hxlt⟩
    · exact Or.inl h
    · exact Or.inr ⟨x, mem_nbrs.mpr hx, hxlt⟩
  have hJ := Boot.claim_J hdyn hb hg hmin hC hwC hB'sub hR hdeg'
  have hstar : ∃ u ∈ C.erase w, 3 ≤ tdeg G (F.erase w) (B.erase w) u := by
    have hu₁w : u₁ ≠ w := Finset.ne_of_mem_erase (hB'sub hu₁B')
    exact ⟨u₁, Finset.mem_erase.mpr ⟨hu₁w, hu₁C⟩,
      (hmin' u₁ hu₁B').trans (hdeg' u₁ hu₁B')⟩
  have hcore := Boot.deletion_core_ineq hb C (nbrs G F B w) w (tdeg G F B)
    (tdeg G (F.erase w) (B.erase w)) Δ (cmin G F B C)
    (Jval b G F B C w B') (by have := hb.three_le; omega) hCd hwd hNC hNcard hd'N hd'o hδ hδ' hreg hJ hstar
  -- assemble
  refine ⟨w, hwB, B', hB'sub, hR, hmin', ?_⟩
  have hid := hb.identity Δ hΔ
  have hpd := psi_delete hdyn b hg hwB
  rw [hwd] at hpd
  have hcsum : ∑ D ∈ tcomps G F B, T4.runMin b (cmin G F B D) =
      T4.runMin b (cmin G F B C) + ∑ D ∈ (tcomps G F B).erase C, T4.runMin b (cmin G F B D) :=
    (Finset.add_sum_erase _ _ hC).symm
  unfold psiMinus
  rw [hcsum]
  unfold Jval at hcore
  have hincr : ∀ v, b (tdeg G F B v) - b (tdeg G F B v - 1) = T4.incr b (tdeg G F B v) :=
    fun v => rfl
  simp only [hincr] at hpd
  linarith

/-- Proposition 9.10 (`prop:deletion`) with base degree `k` (generalizes `T4.deletion_x`): from a good state
with torso minimum degree at least `3`, deletions and reductions reach a state with
torso minimum degree at least `3` all of whose torso components are basic (`BasicK k`),
and the deleted set `X` satisfies `|X| + ψ⁻' ≤ ψ⁻`. -/
theorem deletion (hdyn : TorsoDynamics) {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k 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', BasicK k G F' B' C) ∧
        ((F \ F').card : ℝ) + psiMinus b G F' B' ≤ psiMinus b G F B := by
  classical
  suffices h : ∀ m : ℕ, ∀ F B : Finset (Fin n), B.card = m → 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', BasicK k G F' B' C) ∧
        ((F \ F').card : ℝ) + psiMinus b G F' B' ≤ psiMinus b G F B by
    intro F B hg hmin
    exact h B.card F B rfl hg hmin
  intro m
  induction m using Nat.strong_induction_on with
  | _ m ih =>
    intro F B hcard hg hmin
    by_cases hall : ∀ C ∈ tcomps G F B, BasicK k G F B C
    · exact ⟨F, B, Reach.refl G _, hmin, hall, by simp⟩
    · have hex : ∃ C ∈ tcomps G F B, ¬ BasicK k G F B C := by
        by_contra h
        exact hall fun C hC => by_contra fun hn => h ⟨C, hC, hn⟩
      obtain ⟨C, hC, hnb⟩ := hex
      obtain ⟨w, hwB, B', hB'sub, hR, hmin', hpot⟩ :=
        Boot.key_step hdyn hb hg hmin hC hnb
      have hlt : B'.card < m := by
        have h1 : B'.card ≤ (B.erase w).card := Finset.card_le_card hB'sub
        have h2 : (B.erase w).card < B.card := Finset.card_erase_lt_of_mem hwB
        omega
      obtain ⟨F', B'', hR', hmin'', hbasic, hpot'⟩ :=
        ih B'.card hlt (F.erase w) B' rfl (hg.reach hR) hmin'
      refine ⟨F', B'', hR.trans hR', hmin'', hbasic, ?_⟩
      have hwF : w ∈ F := hg.subset hwB
      have hF'sub : F' ⊆ F.erase w := (Reach.subset hR').1
      have hset : F \ F' = insert w ((F.erase w) \ F') := by
        ext x
        simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert]
        constructor
        · rintro ⟨hxF, hxF'⟩
          by_cases hxw : x = w
          · exact Or.inl hxw
          · exact Or.inr ⟨⟨hxw, hxF⟩, hxF'⟩
        · rintro (rfl | ⟨⟨hxw, hxF⟩, hxF'⟩)
          · exact ⟨hwF, fun h => by have := hF'sub h; simp at this⟩
          · exact ⟨hxF, hxF'⟩
      have hnot : w ∉ (F.erase w) \ F' := by simp
      have hcardF : (F \ F').card = ((F.erase w) \ F').card + 1 := by
        rw [hset, Finset.card_insert_of_notMem hnot]
      rw [hcardF]
      push_cast
      linarith

end Boot
end PwSeq
end CubicPathwidth