CubicPathwidth.Alg.Proofs2.L5SwitchedWidth

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

import CubicPathwidth.Alg.Spec2
import CubicPathwidth.Alg.Proofs.C4Switched
import CubicPathwidth.Alg.Proofs.C1Perm

/-!
# L5: width of the median-switched layout (`SwitchedLayoutWidth`)

Bag by bag, as sets (paper: Lemma 8.4 (`lem:median-layout`); port: `switchedLayoutF`, with the
block structure of `C4.layoutB`). Inner bag `i`: `{v_i} ∪ innerFr (Y v_{i-1})`; the
bag `C_{-1}` has at most `lowerZeroP` elements; the connector bags `C_j` have at most
`|D| + max(|P|, |W'|) + 2 ≤ max(L₀, L₀') + 2` elements (`lem:connector-linear` gives the count);
outer bag `k`: `{v} ∪ outerFr (Y v)` with `Y v > 0`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace L5

/-! ## 1. Generic list facts -/

theorem len_filter_or_and {α : Type} (p q : α → Bool) (L : List α) :
    (L.filter p).length + (L.filter q).length =
      (L.filter (fun x => p x || q x)).length + (L.filter (fun x => p x && q x)).length := by
  induction L with
  | nil => simp
  | cons a L ih =>
    cases hp : p a <;> cases hq : q a <;> simp [hp, hq] at ih ⊢ <;> omega

theorem len_filter_not_add {α : Type} (s : α → Bool) (L : List α) :
    (L.filter (fun x => !s x)).length + (L.filter s).length = L.length := by
  induction L with
  | nil => simp
  | cons a L ih =>
    cases hs : s a <;> simp [hs] at ih ⊢ <;> omega

theorem len_filter_mono {α : Type} {p q : α → Bool} (L : List α)
    (h : ∀ x, p x = true → q x = true) :
    (L.filter p).length ≤ (L.filter q).length :=
  (List.monotone_filter_right L h).length_le

theorem len_filter_eq_zero {α : Type} {p : α → Bool} (L : List α) (h : ∀ x, p x = false) :
    (L.filter p).length = 0 := by
  have : (L.filter p).length ≤ (L.filter (fun _ => false)).length :=
    len_filter_mono L (fun x hx => by rw [h x] at hx; exact absurd hx (by simp))
  simpa using this

theorem card_le_length (B : List Nat) : B.toFinset.card ≤ B.length :=
  List.toFinset_card_le B

theorem card_cons_le (v : Nat) (F S : List Nat) (h : ∀ x ∈ F, x ∈ S) :
    (v :: F).toFinset.card ≤ S.length + 1 := by
  rw [List.toFinset_cons]
  refine (Finset.card_insert_le _ _).trans ?_
  have h1 : F.toFinset ⊆ S.toFinset := fun x hx => by
    rw [List.mem_toFinset] at hx ⊢
    exact h x hx
  have h2 := Finset.card_le_card h1
  have h3 := List.toFinset_card_le S
  omega

/-- A list of bags of width at most `w` (as sets) has `pdWidth ≤ w`, when `w + 1 ≥ 0`. -/
theorem pdWidth_le_of (bags : List Bag) (w : ℝ) (hw : 0 ≤ w + 1)
    (h : ∀ B ∈ bags, (B.toFinset.card : ℝ) ≤ w + 1) : pdWidth bags ≤ w := by
  have key : ∀ bs : List Bag, (∀ B ∈ bs, (B.toFinset.card : ℝ) ≤ w + 1) →
      ((maxBagCard bs : ℕ) : ℝ) ≤ w + 1 := by
    intro bs
    induction bs with
    | nil =>
      intro _
      simpa [maxBagCard] using hw
    | cons B bs ih =>
      intro hB
      have h1 : (B.toFinset.card : ℝ) ≤ w + 1 := hB B (by simp)
      have h2 := ih (fun B' hB' => hB B' (by simp [hB']))
      have e : maxBagCard (B :: bs) = max B.toFinset.card (maxBagCard bs) := by
        simp [maxBagCard]
      rw [e, Nat.cast_max]
      exact max_le h1 h2
  have := key bags h
  unfold pdWidth
  linarith

/-! ## 2. Order and thresholds -/

theorem switchedOrder_sorted (G : Graph) (Y : Labels) :
    (switchedOrder G Y).Pairwise (fun a b => Y a ≤ Y b) := by
  have trans : ∀ a b c : Nat,
      (decide (Y a < Y b) || (decide (Y a = Y b) && decide (a ≤ b))) = true →
      (decide (Y b < Y c) || (decide (Y b = Y c) && decide (b ≤ c))) = true →
      (decide (Y a < Y c) || (decide (Y a = Y c) && decide (a ≤ c))) = true := by
    intro a b c h1 h2
    simp only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at h1 h2 ⊢
    rcases h1 with h1 | ⟨h1, h1'⟩ <;> rcases h2 with h2 | ⟨h2, h2'⟩
    · exact Or.inl (lt_trans h1 h2)
    · exact Or.inl (by rw [← h2]; exact h1)
    · exact Or.inl (by rw [h1]; exact h2)
    · exact Or.inr ⟨h1.trans h2, by omega⟩
  have total : ∀ a b : Nat,
      ((decide (Y a < Y b) || (decide (Y a = Y b) && decide (a ≤ b))) ||
        (decide (Y b < Y a) || (decide (Y b = Y a) && decide (b ≤ a)))) = true := by
    intro a b
    simp only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq]
    rcases lt_trichotomy (Y a) (Y b) with h | h | h
    · exact Or.inl (Or.inl h)
    · rcases le_total a b with hab | hab
      · exact Or.inl (Or.inr ⟨h, hab⟩)
      · exact Or.inr (Or.inr ⟨h.symm, hab⟩)
    · exact Or.inr (Or.inl h)
  have hs := List.pairwise_mergeSort trans total G.nodes
  unfold switchedOrder
  refine hs.imp ?_
  intro a b hab
  simp only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at hab
  rcases hab with h | ⟨h, _⟩
  · exact h.le
  · exact le_of_eq h

theorem pos_le {Y : Labels} {order : List Nat} (hs : order.Pairwise (fun a b => Y a ≤ Y b))
    {i j : Nat} (hi : i < order.length) (hj : j < order.length) (hij : i ≤ j) :
    Y (order[i]) ≤ Y (order[j]) := by
  rcases Nat.lt_or_ge i j with h | h
  · exact List.pairwise_iff_getElem.1 hs i j hi hj h
  · have : i = j := by omega
    subst this
    exact le_refl _

/-- Threshold lemma: for a node `x` of a sorted injective order, the position of `x` is at
most `m` iff `Y x ≤ Y (order[m])`. -/
theorem thr_iff {G : Graph} {Y : Labels} (hG : G.WF) (hinj : LabelsInjOn G Y)
    {order : List Nat} (hperm : order.Perm G.nodes)
    (hs : order.Pairwise (fun a b => Y a ≤ Y b))
    {m : Nat} (hm : m < order.length) {x : Nat} (hx : x ∈ G.nodes) :
    order.idxOf x ≤ m ↔ Y x ≤ Y (order.getD m 0) := by
  have hnd : order.Nodup := hperm.nodup_iff.2 hG.nodup
  have hxo : x ∈ order := hperm.mem_iff.2 hx
  have hym : order[m] ∈ G.nodes := hperm.mem_iff.1 (List.getElem_mem hm)
  have ha : order.idxOf x < order.length := List.idxOf_lt_length_iff.2 hxo
  have hxa : order[order.idxOf x] = x := List.getElem_idxOf ha
  have hy : order.getD m 0 = order[m] := by
    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hm]
    rfl
  rw [hy]
  rcases lt_trichotomy (order.idxOf x) m with h | h | h
  · refine iff_of_true (by omega) ?_
    have := pos_le hs ha hm h.le
    rwa [hxa] at this
  · subst h
    exact iff_of_true le_rfl (le_of_eq (by rw [hxa]))
  · refine iff_of_false (by omega) ?_
    intro hle
    have h1 := pos_le hs hm ha h.le
    rw [hxa] at h1
    have heq : Y x = Y order[m] := le_antisymm hle h1
    have hxm : x = order[m] := hinj x hx _ hym heq
    have : order.idxOf x = m := by
      rw [hxm]
      exact hnd.idxOf_getElem m hm
    omega


/-! ## 3. Frontiers and bag membership -/

theorem mem_innerFr {G : Graph} {Y : Labels} {t : ℚ} {x : Nat} :
    x ∈ innerFr G Y t ↔ x ∈ G.nodes ∧ Y x ≤ t ∧ ∃ w ∈ G.nbrs x, t < Y w := by
  unfold innerFr
  simp [List.mem_filter, List.any_eq_true]

theorem mem_outerFr {G : Graph} {Y : Labels} {t : ℚ} {x : Nat} :
    x ∈ outerFr G Y t ↔ x ∈ G.nodes ∧ t < Y x ∧ ∃ u ∈ G.nbrs x, Y u ≤ t := by
  unfold outerFr
  simp [List.mem_filter, List.any_eq_true]

theorem bag_cases {G : Graph} {Y : Labels} {order q : List Nat} {B : Bag}
    (hB : B ∈ C4.layoutB G Y order q) :
    (∃ i, i < C4.nLow G Y ∧ B = C4.innerB G order i) ∨ B = C4.cm1B G Y ∨
      (∃ j, j ≤ q.length ∧ B = C4.csB G Y q j) ∨
      (∃ k, k < order.length - C4.nLow G Y ∧ B = C4.outB G Y order k) := by
  unfold C4.layoutB at hB
  simp only [List.mem_append, List.mem_map, List.mem_range, List.mem_singleton] at hB
  rcases hB with ((⟨i, hi, rfl⟩ | rfl) | ⟨j, hj, rfl⟩) | ⟨k, hk, rfl⟩
  · exact Or.inl ⟨i, hi, rfl⟩
  · exact Or.inr (Or.inl rfl)
  · exact Or.inr (Or.inr (Or.inl ⟨j, by omega, rfl⟩))
  · exact Or.inr (Or.inr (Or.inr ⟨k, hk, rfl⟩))

/-! ## 4. Inner bags -/

theorem inner_card {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : C4.OrdOK G Y order q) (hinj : LabelsInjOn G Y)
    (hs : order.Pairwise (fun a b => Y a ≤ Y b)) {i : Nat} (hi : i < C4.nLow G Y)
    {w : ℝ} (hinner : ∀ t : ℚ, t < 0 → ((innerFr G Y t).length : ℝ) ≤ w) (hw0 : 0 ≤ w) :
    ((C4.innerB G order i).toFinset.card : ℝ) ≤ w + 1 := by
  have hnl : C4.nLow G Y ≤ order.length := by
    rw [h.length]
    exact C4.nLow_le
  have hnd : order.Nodup := h.nodup hG.nodup
  rcases i with _ | j
  · have h1 : (C4.innerB G order 0).toFinset.card ≤ 1 := by
      refine (card_le_length _).trans ?_
      simp [C4.innerB]
    have h2 : ((C4.innerB G order 0).toFinset.card : ℝ) ≤ 1 := by exact_mod_cast h1
    linarith
  · have hj : j < order.length := by omega
    have hjn : order.getD j 0 ∈ G.nodes := h.mem.1 (C4.getD_mem_order hj)
    have hlow : isLow Y (order.getD j 0) = true := by
      apply (h.low_iff hjn).2
      rw [C4.idxOf_getD hnd hj]
      omega
    have ht : Y (order.getD j 0) < 0 := by
      unfold isLow at hlow
      simpa using hlow
    have hsub : ∀ x ∈ (order.take (j + 1)).filter
        (fun u => (G.nbrs u).any fun y => !decide (y ∈ order.take (j + 1))),
        x ∈ innerFr G Y (Y (order.getD j 0)) := by
      intro x hx
      obtain ⟨hxT, hany⟩ := List.mem_filter.1 hx
      obtain ⟨y, hy, hyT⟩ := List.any_eq_true.1 hany
      have hxo : x ∈ order := List.mem_of_mem_take hxT
      have hxn : x ∈ G.nodes := h.mem.1 hxo
      have hidx : order.idxOf x < j + 1 := (List.mem_take_iff_idxOf_lt hxo).1 hxT
      rw [mem_innerFr]
      refine ⟨hxn, ?_, ?_⟩
      · exact (thr_iff hG hinj h.perm hs hj hxn).1 (by omega)
      · have hyn : y ∈ G.nodes := hG.nbrs_sub x y hy
        have hyo : y ∈ order := h.mem.2 hyn
        have hyT' : y ∉ order.take (j + 1) := by simpa using hyT
        have hyidx : j + 1 ≤ order.idxOf y := by
          by_contra hc
          exact hyT' ((List.mem_take_iff_idxOf_lt hyo).2 (by omega))
        refine ⟨y, hy, ?_⟩
        by_contra hc
        have hle : Y y ≤ Y (order.getD j 0) := not_lt.1 hc
        have := (thr_iff hG hinj h.perm hs hj hyn).2 hle
        omega
    have hc := card_cons_le (order.getD (j + 1) 0) _ _ hsub
    have hc2 : ((innerFr G Y (Y (order.getD j 0))).length : ℝ) ≤ w := hinner _ ht
    have hc3 : (C4.innerB G order (j + 1)).toFinset.card ≤
        (innerFr G Y (Y (order.getD j 0))).length + 1 := by
      unfold C4.innerB
      exact hc
    have hc4 : ((C4.innerB G order (j + 1)).toFinset.card : ℝ) ≤
        ((innerFr G Y (Y (order.getD j 0))).length : ℝ) + 1 := by
      exact_mod_cast hc3
    linarith

/-! ## 5. Outer bags -/

theorem outer_card {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : C4.OrdOK G Y order q) (hinj : LabelsInjOn G Y)
    (hs : order.Pairwise (fun a b => Y a ≤ Y b)) (hnz : ∀ v ∈ G.nodes, Y v ≠ 0)
    {k : Nat} (hk : k < order.length - C4.nLow G Y)
    {w : ℝ} (houter : ∀ t : ℚ, 0 < t → ((outerFr G Y t).length : ℝ) ≤ w) :
    ((C4.outB G Y order k).toFinset.card : ℝ) ≤ w + 1 := by
  have hnl : C4.nLow G Y + k < order.length := by omega
  have hnodup : order.Nodup := h.nodup hG.nodup
  have hvn : order.getD (C4.nLow G Y + k) 0 ∈ G.nodes :=
    h.mem.1 (C4.getD_mem_order hnl)
  have hvidx : order.idxOf (order.getD (C4.nLow G Y + k) 0) = C4.nLow G Y + k :=
    C4.idxOf_getD hnodup hnl
  have hvhigh : isLow Y (order.getD (C4.nLow G Y + k) 0) = false := by
    cases hl : isLow Y (order.getD (C4.nLow G Y + k) 0)
    · rfl
    · have := (h.low_iff hvn).1 hl
      omega
  have ht : 0 < Y (order.getD (C4.nLow G Y + k) 0) := by
    have h1 : ¬ (Y (order.getD (C4.nLow G Y + k) 0) < 0) := by
      intro hc
      have hl : isLow Y (order.getD (C4.nLow G Y + k) 0) = true := by
        unfold isLow
        simpa using hc
      rw [hvhigh] at hl
      exact absurd hl (by simp)
    exact lt_of_le_of_ne (not_lt.1 h1) (fun e => hnz _ hvn e.symm)
  have hsub : ∀ x ∈ G.nodes.filter (fun x => !decide (x ∈ G.nodes.filter (isLow Y) ++
      (order.drop (C4.nLow G Y)).take (k + 1)) &&
        (G.nbrs x).any fun u => decide (u ∈ G.nodes.filter (isLow Y) ++
          (order.drop (C4.nLow G Y)).take (k + 1))),
      x ∈ outerFr G Y (Y (order.getD (C4.nLow G Y + k) 0)) := by
    intro x hx
    obtain ⟨hxn, hxf⟩ := List.mem_filter.1 hx
    simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
      decide_eq_true_eq, List.any_eq_true] at hxf
    obtain ⟨hxT, u, hu, huT⟩ := hxf
    have hun : u ∈ G.nodes := hG.nbrs_sub x u hu
    have hT1 := h.mem_T (k := k) hxn
    have hT2 := h.mem_T (k := k) hun
    rw [mem_outerFr]
    refine ⟨hxn, ?_, u, hu, ?_⟩
    · by_contra hc
      have hle := not_lt.1 hc
      have hidx := (thr_iff hG hinj h.perm hs hnl hxn).2 hle
      exact hxT (hT1.2 (by omega))
    · exact (thr_iff hG hinj h.perm hs hnl hun).1 (by
        have := hT2.1 huT
        omega)
  have hc : (C4.outB G Y order k).toFinset.card ≤
      (outerFr G Y (Y (order.getD (C4.nLow G Y + k) 0))).length + 1 := by
    unfold C4.outB
    exact card_cons_le _ _ _ hsub
  have hN : ((C4.outB G Y order k).toFinset.card : ℝ) ≤
      ((outerFr G Y (Y (order.getD (C4.nLow G Y + k) 0))).length : ℝ) + 1 := by
    exact_mod_cast hc
  have := houter _ ht
  linarith


/-! ## 6. The bag `C_{-1}` and the level-zero counts -/

theorem U_W_disj (G : Graph) (Y : Labels) (x : Nat) :
    (inU G Y x && (inD G Y x && inW G Y x)) = false := by
  by_contra hc
  simp only [Bool.not_eq_false, Bool.and_eq_true] at hc
  obtain ⟨h1, _, h3⟩ := hc
  have hl := (C4.inU_iff.1 h1).1
  have hh := (C4.inW_iff.1 h3).1
  rw [hl] at hh
  exact absurd hh (by simp)

theorem cm1_card (G : Graph) (Y : Labels) :
    (C4.cm1B G Y).toFinset.card ≤ lowerZeroP G Y := by
  refine (card_le_length _).trans ?_
  have e : (G.nodes.filter (inU G Y)).length + (G.nodes.filter fun v => inD G Y v && inW G Y v).length
      = (G.nodes.filter fun v => inU G Y v || (inD G Y v && inW G Y v)).length +
        (G.nodes.filter fun v => inU G Y v && (inD G Y v && inW G Y v)).length :=
    len_filter_or_and _ _ _
  have z : (G.nodes.filter fun v => inU G Y v && (inD G Y v && inW G Y v)).length = 0 :=
    len_filter_eq_zero _ (U_W_disj G Y)
  unfold C4.cm1B lowerZeroP
  omega

/-! ## 7. Degrees and the connector items -/

theorem items_filter_len (G : Graph) (Y : Labels) (X : List Nat) :
    (((C4.pSet G Y).map (C4.eSet G Y)).filter (fun e => subsetB e X)).length =
      ((C4.pSet G Y).filter (fun u => subsetB (C4.eSet G Y u) X)).length := by
  rw [List.filter_map, List.length_map]
  rfl

theorem eSet_len_le {G : Graph} {Y : Labels} (hdeg : G.MaxDegLE 3) {u : Nat} (hu : u ∈ G.nodes)
    (hU : inU G Y u = true) (hD : inD G Y u = false) : (C4.eSet G Y u).length ≤ 2 := by
  unfold C4.eSet
  have hdu := hdeg u hu
  have hlen : (G.nbrs u).length = G.degree u := rfl
  by_cases h3 : G.degree u = 3
  · have hnot : ∃ x ∈ G.nbrs u, C4.wpF G Y x = false := by
      by_contra hcon
      push Not at hcon
      have hall : (G.nbrs u).all (fun x => isLow Y x != isLow Y u) = true := by
        rw [List.all_eq_true]
        intro x hx
        have hw : C4.wpF G Y x = true := by simpa using hcon x hx
        have hlx : isLow Y x = false := (C4.wpF_iff.1 hw).1.1
        have hlu : isLow Y u = true := (C4.inU_iff.1 hU).1
        simp [hlx, hlu]
      have hDt : inD G Y u = true := by
        unfold inD
        simp [h3, hall]
      rw [hD] at hDt
      exact absurd hDt (by simp)
    obtain ⟨x, hx, hxw⟩ := hnot
    have hlt := (List.length_filter_lt_length_iff_exists (p := C4.wpF G Y)
      (l := G.nbrs u)).2 ⟨x, hx, by simp [hxw]⟩
    omega
  · have := List.length_filter_le (C4.wpF G Y) (G.nbrs u)
    omega

/-- `|D| + |P| ≤ L₀`. -/
theorem sum_D_P (G : Graph) (Y : Labels) :
    (G.nodes.filter (inD G Y)).length + (C4.pSet G Y).length ≤ lowerZeroP G Y := by
  have e1 : (G.nodes.filter (inD G Y)).length ≤
      (G.nodes.filter fun v => inD G Y v && isLow Y v).length +
        (G.nodes.filter fun v => inD G Y v && inW G Y v).length := by
    have a : (G.nodes.filter fun v => inD G Y v && isLow Y v).length +
        (G.nodes.filter fun v => inD G Y v && inW G Y v).length =
        (G.nodes.filter fun v => (inD G Y v && isLow Y v) || (inD G Y v && inW G Y v)).length +
        (G.nodes.filter fun v => (inD G Y v && isLow Y v) && (inD G Y v && inW G Y v)).length :=
      len_filter_or_and _ _ _
    have b : (G.nodes.filter (inD G Y)).length ≤
        (G.nodes.filter fun v => (inD G Y v && isLow Y v) || (inD G Y v && inW G Y v)).length := by
      refine len_filter_mono _ (fun x hx => ?_)
      cases hl : isLow Y x
      · have hw := C4.inW_of_inD_high hx hl
        simp [hx, hw]
      · simp [hx]
    have z : (G.nodes.filter fun v => (inD G Y v && isLow Y v) && (inD G Y v && inW G Y v)).length
        = 0 := by
      refine len_filter_eq_zero _ (fun x => ?_)
      cases hw : inW G Y x with
      | false => simp
      | true =>
        have := (C4.inW_iff.1 hw).1
        simp [this]
    omega
  have e2 : (C4.pSet G Y).length + (G.nodes.filter fun v => inD G Y v && isLow Y v).length ≤
      (G.nodes.filter (inU G Y)).length := by
    have hP : C4.pSet G Y = G.nodes.filter fun u =>
        inU G Y u && !inD G Y u && (G.nbrs u).any (C4.wpF G Y) := rfl
    rw [hP]
    have a : (G.nodes.filter fun u => inU G Y u && !inD G Y u && (G.nbrs u).any (C4.wpF G Y)).length +
        (G.nodes.filter fun v => inD G Y v && isLow Y v).length =
        (G.nodes.filter fun u => (inU G Y u && !inD G Y u && (G.nbrs u).any (C4.wpF G Y)) ||
          (inD G Y u && isLow Y u)).length +
        (G.nodes.filter fun u => (inU G Y u && !inD G Y u && (G.nbrs u).any (C4.wpF G Y)) &&
          (inD G Y u && isLow Y u)).length :=
      len_filter_or_and _ _ _
    have z : (G.nodes.filter fun u => (inU G Y u && !inD G Y u && (G.nbrs u).any (C4.wpF G Y)) &&
          (inD G Y u && isLow Y u)).length = 0 := by
      refine len_filter_eq_zero _ (fun x => ?_)
      cases inD G Y x <;> simp
    have b : (G.nodes.filter fun u => (inU G Y u && !inD G Y u && (G.nbrs u).any (C4.wpF G Y)) ||
          (inD G Y u && isLow Y u)).length ≤ (G.nodes.filter (inU G Y)).length := by
      refine len_filter_mono _ (fun x hx => ?_)
      simp only [Bool.or_eq_true, Bool.and_eq_true] at hx
      rcases hx with hr | hs
      · exact hr.1.1
      · exact C4.inU_of_inD_low hs.1 hs.2
    omega
  unfold lowerZeroP
  omega

/-- `|D| + |W'| ≤ L₀'`, where `W' = W \ D`. -/
theorem sum_D_W (G : Graph) (Y : Labels) :
    (G.nodes.filter (inD G Y)).length + (G.nodes.filter (C4.wpF G Y)).length ≤
      upperZeroP G Y := by
  have hW : G.nodes.filter (C4.wpF G Y) = G.nodes.filter fun v => inW G Y v && !inD G Y v := rfl
  rw [hW]
  have e1 : (G.nodes.filter (inD G Y)).length + (G.nodes.filter fun v => inW G Y v && !inD G Y v).length =
      (G.nodes.filter fun v => inD G Y v || (inW G Y v && !inD G Y v)).length +
        (G.nodes.filter fun v => inD G Y v && (inW G Y v && !inD G Y v)).length :=
    len_filter_or_and _ _ _
  have z1 : (G.nodes.filter fun v => inD G Y v && (inW G Y v && !inD G Y v)).length = 0 := by
    refine len_filter_eq_zero _ (fun x => ?_)
    cases inD G Y x <;> simp
  have e2 : (G.nodes.filter fun v => inD G Y v || (inW G Y v && !inD G Y v)).length ≤
      (G.nodes.filter fun v => inW G Y v || (inD G Y v && isLow Y v)).length := by
    refine len_filter_mono _ (fun x hx => ?_)
    simp only [Bool.or_eq_true, Bool.and_eq_true, Bool.not_eq_true'] at hx ⊢
    rcases hx with hd | ⟨hw, hnd⟩
    · cases hl : isLow Y x
      · exact Or.inl (C4.inW_of_inD_high hd hl)
      · exact Or.inr ⟨hd, rfl⟩
    · exact Or.inl hw
  have e3 : (G.nodes.filter (inW G Y)).length + (G.nodes.filter fun v => inD G Y v && isLow Y v).length =
      (G.nodes.filter fun v => inW G Y v || (inD G Y v && isLow Y v)).length +
        (G.nodes.filter fun v => inW G Y v && (inD G Y v && isLow Y v)).length :=
    len_filter_or_and _ _ _
  have z3 : (G.nodes.filter fun v => inW G Y v && (inD G Y v && isLow Y v)).length = 0 := by
    refine len_filter_eq_zero _ (fun x => ?_)
    cases hw : inW G Y x with
    | false => simp
    | true =>
      have := (C4.inW_iff.1 hw).1
      simp [this]
  unfold upperZeroP
  omega

/-! ## 8. The connector bags `C_j` -/

/-- Size of `C_j`: `|D| + (|P| - c(j-1)) + j`, with `c` the number of items covered by the
first `j - 1` connector elements; Lemma A.33 (`lem:connector-linear`) bounds `c` from below. -/
theorem cs_card {G : Graph} {Y : Labels} {q : List Nat}
    {j : Nat} (hj : j ≤ q.length) (hqlen : q.length = (G.nodes.filter (C4.wpF G Y)).length)
    (hcon : ∀ J, J ≤ (G.nodes.filter (C4.wpF G Y)).length →
      (J : ℤ) - ((C4.pSet G Y).filter (fun u => subsetB (C4.eSet G Y u) (q.take J))).length ≤
        max 0 (((G.nodes.filter (C4.wpF G Y)).length : ℤ) - (C4.pSet G Y).length) + 1) :
    ((C4.csB G Y q j).toFinset.card : ℤ) ≤
      ((G.nodes.filter (inD G Y)).length : ℤ) + (C4.pSet G Y).length +
        max 0 (((G.nodes.filter (C4.wpF G Y)).length : ℤ) - (C4.pSet G Y).length) + 2 := by
  have hl : (C4.csB G Y q j).toFinset.card ≤ (C4.csB G Y q j).length := card_le_length _
  have hl' : ((C4.csB G Y q j).toFinset.card : ℤ) ≤ ((C4.csB G Y q j).length : ℤ) := by
    exact_mod_cast hl
  refine hl'.trans ?_
  unfold C4.csB
  rw [List.length_append, List.length_append, List.length_take]
  have hA : ((C4.pSet G Y).filter (fun u => !subsetB (C4.eSet G Y u) (q.take (j - 1)))).length +
      ((C4.pSet G Y).filter (fun u => subsetB (C4.eSet G Y u) (q.take (j - 1)))).length =
      (C4.pSet G Y).length :=
    len_filter_not_add _ _
  rcases Nat.eq_zero_or_pos j with rfl | hjpos
  · have h0 : (0 : ℤ) ≤ max 0 (((G.nodes.filter (C4.wpF G Y)).length : ℤ) - (C4.pSet G Y).length) :=
      le_max_left _ _
    have hm : min 0 q.length = 0 := Nat.zero_min _
    rw [hm]
    omega
  · have hc := hcon (j - 1) (by omega)
    have htk : min j q.length ≤ j := min_le_left _ _
    omega

/-- The connector bag bound in the form used by the main theorem. -/
theorem cs_bag_le {G : Graph} {Y : Labels} {q : List Nat}
    {j : Nat} (hj : j ≤ q.length) (hqlen : q.length = (G.nodes.filter (C4.wpF G Y)).length)
    (hcon : ∀ J, J ≤ (G.nodes.filter (C4.wpF G Y)).length →
      (J : ℤ) - ((C4.pSet G Y).filter (fun u => subsetB (C4.eSet G Y u) (q.take J))).length ≤
        max 0 (((G.nodes.filter (C4.wpF G Y)).length : ℤ) - (C4.pSet G Y).length) + 1) :
    ((C4.csB G Y q j).toFinset.card : ℤ) ≤ ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℤ) + 2 := by
  have hz := cs_card hj hqlen hcon
  have hDA := sum_D_P G Y
  have hDQ := sum_D_W G Y
  have hKA : ((G.nodes.filter (inD G Y)).length : ℤ) + ((C4.pSet G Y).length : ℤ) ≤
      ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℤ) := by
    have : (G.nodes.filter (inD G Y)).length + (C4.pSet G Y).length ≤
        max (lowerZeroP G Y) (upperZeroP G Y) := hDA.trans (le_max_left _ _)
    exact_mod_cast this
  have hKQ : ((G.nodes.filter (inD G Y)).length : ℤ) +
      ((G.nodes.filter (C4.wpF G Y)).length : ℤ) ≤
      ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℤ) := by
    have : (G.nodes.filter (inD G Y)).length + (G.nodes.filter (C4.wpF G Y)).length ≤
        max (lowerZeroP G Y) (upperZeroP G Y) := hDQ.trans (le_max_right _ _)
    exact_mod_cast this
  rcases le_total ((G.nodes.filter (C4.wpF G Y)).length : ℤ) ((C4.pSet G Y).length : ℤ) with h | h
  · rw [max_eq_left (by omega)] at hz
    omega
  · rw [max_eq_right (by omega)] at hz
    omega


end L5

open L5

/-! ## 9. The main theorem -/

/-- `switched_layout` (median-switched layout, Lemma 8.4 (`lem:median-layout`)) has width at most `w`
under the frontier hypotheses of `SwitchedLayoutWidth`, and its connector does not fall
back. Uses Lemma A.33 (`lem:connector-linear`, `ConnectorLemma10`) for the count of connector bags and the connector
no-fallback statement `ConnectorNoFallback` (`Spec.lean` §7). -/
theorem switchedLayoutWidth_of (hL10 : ConnectorLemma10) (hN : ConnectorNoFallback) :
    SwitchedLayoutWidth := by
  intro G hG hdeg Y hinj hnz w hinner houter hw
  have hK0 : (0 : ℝ) ≤ ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℝ) := Nat.cast_nonneg _
  have hw' : ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℝ) + 1 ≤ w := by
    rw [Nat.cast_max]
    exact hw
  have hw0 : (0 : ℝ) ≤ w := by linarith
  have hQsnd : (G.nodes.filter (C4.wpF G Y)).Nodup := hG.nodup.filter _
  have hitems_ok : ∀ e ∈ (C4.pSet G Y).map (C4.eSet G Y),
      e.Nodup ∧ 1 ≤ e.length ∧ e.length ≤ 2 ∧ ∀ z ∈ e, z ∈ G.nodes.filter (C4.wpF G Y) := by
    intro e he
    obtain ⟨u, hu, rfl⟩ := List.mem_map.1 he
    obtain ⟨hun, hU, hD, x, hx, hxw⟩ := C4.mem_pSet.1 hu
    refine ⟨(hG.nbrs_nodup u).filter _, List.length_pos_of_mem (List.mem_filter.2 ⟨hx, hxw⟩),
      eSet_len_le hdeg hun hU hD, ?_⟩
    intro z hz
    obtain ⟨hz1, hz2⟩ := List.mem_filter.1 hz
    exact List.mem_filter.2 ⟨hG.nbrs_sub u z hz1, hz2⟩
  have hflag : (switchedLayoutF G Y).2 = false :=
    hN (G.nodes.filter (C4.wpF G Y)) ((C4.pSet G Y).map (C4.eSet G Y)) hQsnd hitems_ok
  obtain ⟨hperm, hcount⟩ :=
    hL10 (G.nodes.filter (C4.wpF G Y)) ((C4.pSet G Y).map (C4.eSet G Y)) hQsnd hitems_ok
  refine ⟨hflag, ?_⟩
  rw [C4.switchedLayout_eq]
  have hperm_o : (switchedOrder G Y).Perm G.nodes := switchedOrderPerm G Y
  have hsplit : switchedOrder G Y = (switchedOrder G Y).filter (isLow Y) ++
      (switchedOrder G Y).filter (fun x => !isLow Y x) :=
    C4.lows_first (isLow Y) _ (C4.switchedOrder_pairwise G Y)
  have hqmem : ∀ x, x ∈ connectorOrder (G.nodes.filter (C4.wpF G Y))
      ((C4.pSet G Y).map (C4.eSet G Y)) ↔ x ∈ G.nodes.filter (C4.wpF G Y) :=
    fun x => hperm.mem_iff
  have hOK : C4.OrdOK G Y (switchedOrder G Y)
      (connectorOrder (G.nodes.filter (C4.wpF G Y)) ((C4.pSet G Y).map (C4.eSet G Y))) :=
    ⟨hperm_o, hsplit, hqmem⟩
  have hs := switchedOrder_sorted G Y
  have hqlen : (connectorOrder (G.nodes.filter (C4.wpF G Y))
      ((C4.pSet G Y).map (C4.eSet G Y))).length = (G.nodes.filter (C4.wpF G Y)).length :=
    hperm.length_eq
  have hcon : ∀ J, J ≤ (G.nodes.filter (C4.wpF G Y)).length →
      (J : ℤ) - ((C4.pSet G Y).filter (fun u => subsetB (C4.eSet G Y u)
        ((connectorOrder (G.nodes.filter (C4.wpF G Y))
          ((C4.pSet G Y).map (C4.eSet G Y))).take J))).length ≤
        max 0 (((G.nodes.filter (C4.wpF G Y)).length : ℤ) - (C4.pSet G Y).length) + 1 := by
    intro J hJ
    have h1 := hcount J hJ
    rw [items_filter_len, List.length_map] at h1
    exact h1
  apply pdWidth_le_of _ w (by linarith)
  intro B hB
  rcases bag_cases hB with ⟨i, hi, rfl⟩ | rfl | ⟨j, hj, rfl⟩ | ⟨k, hk, rfl⟩
  · exact inner_card hG hOK hinj hs hi hinner hw0
  · have h1 : ((C4.cm1B G Y).toFinset.card : ℝ) ≤ ((lowerZeroP G Y : ℕ) : ℝ) := by
      exact_mod_cast cm1_card G Y
    have h2 : ((lowerZeroP G Y : ℕ) : ℝ) ≤
        ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℝ) := by
      exact_mod_cast le_max_left _ _
    linarith
  · have hz := cs_bag_le hj hqlen hcon
    have hfin : ∀ n : ℕ, (n : ℤ) ≤ ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℤ) + 2 →
        (n : ℝ) ≤ w + 1 := by
      intro n hn
      have h3 : n ≤ max (lowerZeroP G Y) (upperZeroP G Y) + 2 := by omega
      have h4 : (n : ℝ) ≤ ((max (lowerZeroP G Y) (upperZeroP G Y) : ℕ) : ℝ) + 2 := by
        exact_mod_cast h3
      linarith
    exact hfin _ hz
  · exact outer_card hG hOK hinj hs hnz hk houter

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.switchedLayoutWidth_of