CubicPathwidth.Alg.Proofs2.R7Balanced

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets

/-!
# R7: balanced elimination bag (`cl:alg-elim` and Claim A.30 (`cl:alg-balanced`), port form)

Route (no tree decompositions). Let `E_t` be the set of the first `t` eliminated vertices
of `reduce_record` (`ops.take t`). Let `k` be least such that `H[E_k]` has a component `K`
with more than `N/2` vertices, `v = v_k`, `X = {v} ∪ nb_k`. Every component `C` of `H - X`
has at most `N/2` vertices:
* if `C` misses `K`, then `|C| ≤ N - |K| < N/2`;
* otherwise `C` lies in a component `S` of `H[E_{k-1}]` (all of them have at most `N/2`
  vertices by minimality), and the attachment of `S` lies in `X`: a neighbour `y` of `S`
  outside `E_{k-1}` is adjacent in the record graph `G_{k-1}` to `v` (walk `v → S → y`
  through `E_{k-1}`, invariant `St`), hence `y ∈ nb_k`.
Edges of the record graph are described by `W` (walks with interior in `E_t`).
-/

namespace CubicPathwidth.Alg.R7

open Graph

/-! ## Generic lemmas -/

theorem rtg_closed {α : Type} (r : α → α → Prop) (P : α → Prop)
    (hP : ∀ p q, P p → r p q → P q) {p q : α} (h : Relation.ReflTransGen r p q)
    (hp : P p) : P q := by
  induction h with
  | refl => exact hp
  | tail _ hbc ih => exact hP _ _ ih hbc

theorem rtg_mono {α : Type} {r p : α → α → Prop} (h : ∀ a b, r a b → p a b) {a b : α}
    (hab : Relation.ReflTransGen r a b) : Relation.ReflTransGen p a b := by
  induction hab with
  | refl => exact Relation.ReflTransGen.refl
  | tail _ hbc ih => exact Relation.ReflTransGen.tail ih (h _ _ hbc)

/-! ## Walks with interior in a set -/

/-- `W H E a b`: a walk from `a` to `b` in `H` whose interior vertices all satisfy `E`. -/
inductive W (H : Graph) (E : Nat → Prop) : Nat → Nat → Prop
  | adj {a b : Nat} : H.Adj a b → W H E a b
  | step {a x b : Nat} : H.Adj a x → E x → W H E x b → W H E a b

theorem W.split {H : Graph} {E E' : Nat → Prop} {v : Nat}
    (hE : ∀ x, E' x → E x ∨ x = v) :
    ∀ {a b : Nat}, W H E' a b → W H E a b ∨ (W H E a v ∧ W H E v b) := by
  intro a b h
  induction h with
  | adj hab => exact Or.inl (W.adj hab)
  | @step a x b hax hx _ ih =>
    rcases hE x hx with hEx | hxv
    · rcases ih with h1 | ⟨h1, h2⟩
      · exact Or.inl (W.step hax hEx h1)
      · exact Or.inr ⟨W.step hax hEx h1, h2⟩
    · subst hxv
      rcases ih with h1 | ⟨h1, h2⟩
      · exact Or.inr ⟨W.adj hax, h1⟩
      · exact Or.inr ⟨W.adj hax, h2⟩

theorem W.snoc {H : Graph} {E : Nat → Prop} {a b c : Nat} (h : W H E a b) :
    E b → H.Adj b c → W H E a c := by
  induction h with
  | adj hab => intro hb hbc; exact W.step hab hb (W.adj hbc)
  | step hax hx _ ih => intro hb hbc; exact W.step hax hx (ih hb hbc)

theorem W.of_rtg {H : Graph} {E : Nat → Prop} (x0 x : Nat)
    (h : Relation.ReflTransGen (fun p q => H.Adj p q ∧ E p ∧ E q) x0 x) :
    ∀ y, H.Adj x y → E x → W H E x0 y := by
  induction h with
  | refl => intro y hy _; exact W.adj hy
  | @tail c d _ hcd ih =>
    intro y hdy hEd
    exact W.snoc (ih d hcd.1 hcd.2.1) hcd.2.2 hdy

/-! ## One reduction step -/

theorem redStep_wf {G : Graph} (hG : G.WF) (v : Nat) : (redStep G v).WF := by
  have hR := removeNodeSpec G v hG
  unfold redStep
  split
  next a b hab =>
    have hnd := hG.nbrs_nodup v
    rw [hab] at hnd
    have hne : a ≠ b := by simpa using hnd
    exact (addEdgeSpec _ a b hR.1 hne).1
  next => exact hR.1

theorem redStep_nodes {G : Graph} (hG : G.WF) (v x : Nat) (hx : x ∈ (redStep G v).nodes) :
    x ∈ G.nodes ∧ x ≠ v := by
  have hR := removeNodeSpec G v hG
  unfold redStep at hx
  split at hx
  next a b hab =>
    have ha : a ∈ G.nbrs v := by rw [hab]; simp
    have hb : b ∈ G.nbrs v := by rw [hab]; simp
    have hne : a ≠ b := by
      have hnd := hG.nbrs_nodup v
      rw [hab] at hnd
      simpa using hnd
    have hav : a ≠ v := fun h => hG.loopless v (by rw [h] at ha; exact ha)
    have hbv : b ≠ v := fun h => hG.loopless v (by rw [h] at hb; exact hb)
    rw [(addEdgeSpec _ a b hR.1 hne).2.1 x, hR.2.1 x] at hx
    rcases hx with ⟨h1, h2⟩ | h1 | h1
    · exact ⟨h1, h2⟩
    · subst h1; exact ⟨hG.nbrs_sub v _ ha, hav⟩
    · subst h1; exact ⟨hG.nbrs_sub v _ hb, hbv⟩
  next =>
    exact (hR.2.1 x).1 hx

theorem redStep_adj_of {G : Graph} (hG : G.WF) {v x y : Nat} (hxv : x ≠ v) (hyv : y ≠ v)
    (h : G.Adj x y) : (redStep G v).Adj x y := by
  have hR := removeNodeSpec G v hG
  unfold redStep
  split
  next a b hab =>
    have hnd := hG.nbrs_nodup v
    rw [hab] at hnd
    have hne : a ≠ b := by simpa using hnd
    rw [(addEdgeSpec _ a b hR.1 hne).2.2 x y]
    exact Or.inl ((hR.2.2 x y).2 ⟨h, hxv, hyv⟩)
  next => exact (hR.2.2 x y).2 ⟨h, hxv, hyv⟩

theorem redStep_adj_pair {G : Graph} (hG : G.WF) (v a b : Nat)
    (ha : a ∈ G.nbrs v) (hb : b ∈ G.nbrs v) (hab : a ≠ b) (hlen : (G.nbrs v).length ≤ 2) :
    (redStep G v).Adj a b := by
  have hR := removeNodeSpec G v hG
  have hnd := hG.nbrs_nodup v
  obtain ⟨p, q, hpq⟩ : ∃ p q, G.nbrs v = [p, q] := by
    rcases hL : G.nbrs v with _ | ⟨p, _ | ⟨q, _ | ⟨r, l⟩⟩⟩
    · rw [hL] at ha; simp at ha
    · rw [hL] at ha hb
      simp only [List.mem_cons, List.not_mem_nil, or_false] at ha hb
      exact absurd (ha.trans hb.symm) hab
    · exact ⟨p, q, rfl⟩
    · rw [hL] at hlen
      simp only [List.length_cons] at hlen
      omega
  have hpq' : p ≠ q := by
    rw [hpq] at hnd
    simpa using hnd
  simp only [redStep, hpq]
  rw [(addEdgeSpec _ p q hR.1 hpq').2.2 a b]
  rw [hpq] at ha hb
  simp only [List.mem_cons, List.not_mem_nil, or_false] at ha hb
  rcases ha with h1 | h1 <;> rcases hb with h2 | h2
  · exact absurd (h1.trans h2.symm) hab
  · exact Or.inr (Or.inl ⟨h1, h2⟩)
  · exact Or.inr (Or.inr ⟨h1, h2⟩)
  · exact absurd (h1.trans h2.symm) hab

theorem nbrs_len_le {G : Graph} (hG : G.WF) {v : Nat} {nb : List Nat}
    (hlen : nb.length ≤ 2) (hadj : ∀ x, x ∈ nb ↔ G.Adj v x) : (G.nbrs v).length ≤ 2 := by
  have hsub : G.nbrs v ⊆ nb := by
    intro x hx
    exact (hadj x).2 hx
  exact le_trans (((hG.nbrs_nodup v).subperm hsub).length_le) hlen

/-! ## Elimination sets along the record -/

/-- Membership of `x` in the set of vertices eliminated by the first `t` operations. -/
def elimKeep (ops : List Op) (t : Nat) (x : Nat) : Bool :=
  (redVertices (ops.take t)).contains x

/-- Propositional form of `elimKeep`. -/
def elimSet (ops : List Op) (t : Nat) (x : Nat) : Prop := elimKeep ops t x = true

theorem elimSet_succ {ops : List Op} {t v : Nat} {nb : List Nat}
    (hop : ops[t]? = some (Op.red v nb)) (x : Nat) :
    elimSet ops (t + 1) x ↔ elimSet ops t x ∨ x = v := by
  unfold elimSet elimKeep
  rw [List.take_add_one, hop]
  simp [redVertices]

theorem elimKeep_of_le (ops : List Op) {t : Nat} (h : ops.length ≤ t) :
    elimKeep ops t = elimKeep ops ops.length := by
  unfold elimKeep
  rw [List.take_of_length_le h, List.take_length]

theorem elimSet_zero (ops : List Op) (x : Nat) : ¬ elimSet ops 0 x := by
  unfold elimSet elimKeep
  simp [redVertices]

/-! ## Invariant of the record -/

/-- The record graph after the first `t` operations: a well-formed graph `G` with
`OpsRecord G (ops.drop t) R`, no vertex eliminated so far, and whose adjacency among
the vertices not eliminated so far is given by walks in `H` through eliminated vertices. -/
structure St (H : Graph) (ops : List Op) (R : Graph) (t : Nat) (G : Graph) : Prop where
  wf : G.WF
  recd : OpsRecord G (ops.drop t) R
  elim : ∀ x, elimSet ops t x → x ∉ G.nodes
  walk : ∀ a b, ¬ elimSet ops t a → ¬ elimSet ops t b → a ≠ b →
    W H (elimSet ops t) a b → G.Adj a b

theorem exists_St (H : Graph) (ops : List Op) (R G0 : Graph)
    (hG0 : G0.WF) (hG0adj : ∀ a b, G0.Adj a b ↔ H.Adj a b)
    (hrec : OpsRecord G0 ops R) (hred : ∀ o ∈ ops, ∃ v nb, o = Op.red v nb) :
    ∀ t, t ≤ ops.length → ∃ G, St H ops R t G := by
  intro t
  induction t with
  | zero =>
    intro _
    refine ⟨G0, ⟨hG0, by simpa using hrec, fun x hx => absurd hx (elimSet_zero ops x), ?_⟩⟩
    intro a b _ _ _ hw
    cases hw with
    | adj h => exact (hG0adj a b).2 h
    | step _ hx _ => exact absurd hx (elimSet_zero ops _)
  | succ t ih =>
    intro ht
    obtain ⟨G, hG⟩ := ih (Nat.le_of_succ_le ht)
    have hlt : t < ops.length := Nat.lt_of_succ_le ht
    have hmem : ops[t] ∈ ops := List.getElem_mem hlt
    obtain ⟨v, nb, hop⟩ := hred _ hmem
    have hop' : ops[t]? = some (Op.red v nb) := by
      rw [List.getElem?_eq_getElem hlt, hop]
    have hdrop : ops.drop t = Op.red v nb :: ops.drop (t + 1) := by
      rw [List.drop_eq_getElem_cons hlt, hop]
    have hrt := hG.recd
    rw [hdrop] at hrt
    obtain ⟨hv, hnd, hlen, hadj, hrest⟩ := hrt
    have hsucc := elimSet_succ hop'
    refine ⟨redStep G v, redStep_wf hG.wf v, hrest, ?_, ?_⟩
    · intro x hx hmem'
      rcases (hsucc x).1 hx with h | h
      · exact hG.elim x h (redStep_nodes hG.wf v x hmem').1
      · exact (redStep_nodes hG.wf v x hmem').2 h
    · intro a b ha hb hab hw
      have ha' : ¬ elimSet ops t a ∧ a ≠ v := by
        refine ⟨fun h => ha ((hsucc a).2 (Or.inl h)), fun h => ha ((hsucc a).2 (Or.inr h))⟩
      have hb' : ¬ elimSet ops t b ∧ b ≠ v := by
        refine ⟨fun h => hb ((hsucc b).2 (Or.inl h)), fun h => hb ((hsucc b).2 (Or.inr h))⟩
      have hvE : ¬ elimSet ops t v := fun h => hG.elim v h hv
      rcases W.split (E := elimSet ops t) (E' := elimSet ops (t + 1)) (v := v)
          (fun x hx => (hsucc x).1 hx) hw with h | ⟨h1, h2⟩
      · exact redStep_adj_of hG.wf ha'.2 hb'.2 (hG.walk a b ha'.1 hb'.1 hab h)
      · have hav : G.Adj a v := hG.walk a v ha'.1 hvE ha'.2 h1
        have hvb : G.Adj v b := hG.walk v b hvE hb'.1 (Ne.symm hb'.2) h2
        have hav' : a ∈ G.nbrs v := hG.wf.symm a v hav
        have hlen2 := nbrs_len_le hG.wf hlen hadj
        exact redStep_adj_pair hG.wf v a b hav' hvb hab hlen2

/-! ## Component facts -/

theorem comp_nodup {G : Graph} (hG : G.WF) {c : List Nat} (hc : c ∈ G.components) :
    c.Nodup := by
  have hp := (componentsSpec G hG).1
  have hnd : G.components.flatten.Nodup := hp.nodup_iff.mpr hG.nodup
  exact (List.nodup_flatten.mp hnd).1 c hc

theorem comp_mem_nodes {G : Graph} (hG : G.WF) {c : List Nat} (hc : c ∈ G.components)
    {x : Nat} (hx : x ∈ c) : x ∈ G.nodes := by
  have hp := (componentsSpec G hG).1
  exact hp.subset (List.mem_flatten.mpr ⟨c, hc, hx⟩)

theorem comp_exists_mem {G : Graph} (hG : G.WF) {c : List Nat} (hc : c ∈ G.components) :
    ∃ x, x ∈ c :=
  List.exists_mem_of_ne_nil c ((componentsSpec G hG).2.1 c hc)

theorem comp_closed {G : Graph} (hG : G.WF) {c : List Nat} (hc : c ∈ G.components)
    {x : Nat} (hx : x ∈ c) {y : Nat} (hxy : G.Adj x y) : y ∈ c :=
  (componentsSpec G hG).2.2 c hc x hx y hxy

theorem comp_exists {G : Graph} (hG : G.WF) {x : Nat} (hx : x ∈ G.nodes) :
    ∃ c ∈ G.components, x ∈ c := by
  have hp := (componentsSpec G hG).1
  obtain ⟨c, hc, hxc⟩ := List.mem_flatten.mp (hp.symm.subset hx)
  exact ⟨c, hc, hxc⟩

/-- Members of a component of an induced graph are nodes with the right keep value. -/
theorem comp_keep {H : Graph} (hH : H.WF) {keep : Nat → Bool} {c : List Nat}
    (hc : c ∈ (H.induced keep).components) {x : Nat} (hx : x ∈ c) :
    x ∈ H.nodes ∧ keep x = true :=
  (inducedSpec H keep hH).2.1 x |>.1 (comp_mem_nodes (inducedSpec H keep hH).1 hc hx)

theorem rtg_ind {H : Graph} (hH : H.WF) {keep : Nat → Bool} {x y : Nat}
    (h : Relation.ReflTransGen (H.induced keep).Adj x y) :
    Relation.ReflTransGen (fun p q => H.Adj p q ∧ keep p = true ∧ keep q = true) x y :=
  rtg_mono (fun p q hpq => (inducedSpec H keep hH).2.2 p q |>.1 hpq) h

/-- Absorption: a component `C` of `H[kZ]` that meets a set `S` closed under `H`-edges
into `kZ` lies in `S`. -/
theorem comp_absorb {H : Graph} (hH : H.WF) (hConn : ComponentsConnected)
    {kZ : Nat → Bool} {S C : List Nat} {u : Nat}
    (hC : C ∈ (H.induced kZ).components) (huS : u ∈ S) (huC : u ∈ C)
    (hcl : ∀ p q, p ∈ S → H.Adj p q → kZ q = true → q ∈ S) :
    ∀ w ∈ C, w ∈ S := by
  intro w hw
  have hR := rtg_ind hH (hConn (H.induced kZ) (inducedSpec H kZ hH).1 C hC u huC w hw)
  exact rtg_closed (fun p q => H.Adj p q ∧ kZ p = true ∧ kZ q = true) (fun x => x ∈ S)
    (fun p q hp hpq => hcl p q hp hpq.1 hpq.2.2) hR huS

theorem len_le_of_sub {A B : List Nat} (hA : A.Nodup) (_hB : B.Nodup)
    (hsub : ∀ w ∈ A, w ∈ B) : A.length ≤ B.length :=
  (hA.subperm hsub).length_le

theorem len_add_le {H : Graph} {A B : List Nat} (hA : A.Nodup) (hB : B.Nodup)
    (hd : ∀ a ∈ A, a ∉ B) (hsub : ∀ a ∈ A ++ B, a ∈ H.nodes) :
    A.length + B.length ≤ H.numNodes := by
  have hnd : (A ++ B).Nodup :=
    List.nodup_append.2 ⟨hA, hB, fun a ha b hb hab => hd a ha (hab ▸ hb)⟩
  have := (hnd.subperm hsub).length_le
  simp only [List.length_append] at this
  exact this

/-! ## The balanced bag -/

theorem keep_notin {X : List Nat} {u : Nat} (h : (fun y => !X.contains y) u = true) :
    u ∉ X := by
  intro hu
  simp [hu] at h

/-- `H[E_t]` has a component with more than `N/2` vertices. -/
def Big (H : Graph) (ops : List Op) (t : Nat) : Prop :=
  ∃ c ∈ (H.induced (elimKeep ops t)).components, H.numNodes < 2 * c.length

theorem not_big_zero (H : Graph) (hH : H.WF) (ops : List Op) : ¬ Big H ops 0 := by
  rintro ⟨c, hc, _⟩
  obtain ⟨x, hx⟩ := comp_exists_mem (inducedSpec H _ hH).1 hc
  have := (comp_keep hH hc hx).2
  exact elimSet_zero ops x this

theorem balanced_core (H : Graph) (hH : H.WF) (ops : List Op) (R : Graph)
    (hred : ∀ o ∈ ops, ∃ v nb, o = Op.red v nb)
    (hall : ∀ x ∈ H.nodes, elimSet ops ops.length x)
    (hSt : ∀ t, t ≤ ops.length → ∃ G, St H ops R t G)
    (hConn : ComponentsConnected) (hN : 1 ≤ H.numNodes) :
    ∃ X ∈ elimBags ops, ∀ c ∈ (H.induced fun v => !X.contains v).components,
      2 * c.length ≤ H.numNodes := by
  classical
  by_cases hA : ∃ t, Big H ops t
  · obtain ⟨k, hk, hmin⟩ : ∃ k, Big H ops k ∧ ∀ j < k, ¬ Big H ops j :=
      ⟨Nat.find hA, Nat.find_spec hA, fun j hj => Nat.find_min hA hj⟩
    have hk0 : k ≠ 0 := fun h => not_big_zero H hH ops (h ▸ hk)
    have hkM : k ≤ ops.length := by
      by_contra hcon
      apply hmin ops.length (by omega)
      unfold Big at hk ⊢
      rw [elimKeep_of_le ops (by omega)] at hk
      exact hk
    obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩
    have hjlt : j < ops.length := by omega
    have hmemj : ops[j] ∈ ops := List.getElem_mem hjlt
    obtain ⟨v, nb, hop⟩ := hred _ hmemj
    have hop' : ops[j]? = some (Op.red v nb) := by
      rw [List.getElem?_eq_getElem hjlt, hop]
    have hmem : Op.red v nb ∈ ops := by rw [← hop]; exact hmemj
    obtain ⟨G, hG⟩ := hSt j (by omega)
    have hdrop : ops.drop j = Op.red v nb :: ops.drop (j + 1) := by
      rw [List.drop_eq_getElem_cons hjlt, hop]
    have hrt := hG.recd
    rw [hdrop] at hrt
    obtain ⟨hv, hnd, hlen, hadj, hrest⟩ := hrt
    have hXmem : v :: nb ∈ elimBags ops :=
      List.mem_filterMap.2 ⟨Op.red v nb, hmem, rfl⟩
    refine ⟨v :: nb, hXmem, ?_⟩
    intro C hC
    have hCnd : C.Nodup := comp_nodup (inducedSpec H (fun y => !(v :: nb).contains y) hH).1 hC
    obtain ⟨K, hKmem, hKbig⟩ := hk
    have hKnd : K.Nodup := comp_nodup (inducedSpec H (elimKeep ops (j + 1)) hH).1 hKmem
    have hmin' : ¬ Big H ops j := hmin j (Nat.lt_succ_self j)
    by_cases hCK : ∃ u ∈ C, u ∈ K
    · obtain ⟨u, huC, huK⟩ := hCK
      have huZ := comp_keep hH hC huC
      have huX : u ≠ v ∧ u ∉ nb := by
        have hnotin : u ∉ v :: nb := keep_notin huZ.2
        exact ⟨fun h => hnotin (h ▸ List.mem_cons_self), fun h => hnotin (List.mem_cons_of_mem _ h)⟩
      have huE : elimSet ops j u := by
        have h1 : elimSet ops (j + 1) u := (comp_keep hH hKmem huK).2
        rcases (elimSet_succ hop' u).1 h1 with h | h
        · exact h
        · exact absurd h huX.1
      obtain ⟨S0, hS0mem, huS0⟩ := comp_exists (inducedSpec H (elimKeep ops j) hH).1
        ((inducedSpec H (elimKeep ops j) hH).2.1 u |>.2 ⟨huZ.1, huE⟩)
      have hS0nd : S0.Nodup := comp_nodup (inducedSpec H (elimKeep ops j) hH).1 hS0mem
      have hS0size : 2 * S0.length ≤ H.numNodes := by
        by_contra hc
        exact hmin' ⟨S0, hS0mem, by omega⟩
      -- (i) the component `S0` of `H[E_j]` containing `u` is attached to `v`
      have hx0 : ∃ x0 ∈ S0, H.Adj x0 v := by
        by_contra hno
        push Not at hno
        have hcl0 : ∀ p q, p ∈ S0 → H.Adj p q → elimKeep ops (j + 1) q = true → q ∈ S0 := by
          intro p q hp hpq hq
          rcases (elimSet_succ hop' q).1 hq with h | h
          · exact comp_closed (inducedSpec H (elimKeep ops j) hH).1 hS0mem hp
              (((inducedSpec H (elimKeep ops j) hH).2.2 p q).2
                ⟨hpq, (comp_keep hH hS0mem hp).2, h⟩)
          · subst h
            exact absurd hpq (hno p hp)
        have hKS := comp_absorb hH hConn hKmem huS0 huK hcl0
        have := len_le_of_sub hKnd hS0nd hKS
        omega
      -- (ii) attachment: every outside neighbour of `S0` lies in `X`
      have hatt : ∀ x ∈ S0, ∀ y, H.Adj x y → ¬ elimSet ops j y → y ∈ v :: nb := by
        intro x hx y hxy hyE
        by_cases hyv : y = v
        · exact List.mem_cons.2 (Or.inl hyv)
        · obtain ⟨x0, hx0, hx0v⟩ := hx0
          have hvx0 : H.Adj v x0 := hH.symm x0 v hx0v
          have hrtg := rtg_ind hH
            (hConn (H.induced (elimKeep ops j)) (inducedSpec H (elimKeep ops j) hH).1 S0 hS0mem
              x0 hx0 x hx)
          have hWx : W H (elimSet ops j) x0 y :=
            W.of_rtg (E := elimSet ops j) x0 x hrtg y hxy (comp_keep hH hS0mem hx).2
          have hWv : W H (elimSet ops j) v y :=
            W.step hvx0 (comp_keep hH hS0mem hx0).2 hWx
          have hvE : ¬ elimSet ops j v := fun h => hG.elim v h hv
          have hGadj : G.Adj v y := hG.walk v y hvE hyE (Ne.symm hyv) hWv
          exact List.mem_cons_of_mem _ ((hadj y).2 hGadj)
      -- (iii) `S0` is closed outside `X`; `C` lies in `S0`
      have hcl : ∀ p q, p ∈ S0 → H.Adj p q →
          (fun y => !(v :: nb).contains y) q = true → q ∈ S0 := by
        intro p q hp hpq hq
        have hqX : q ∉ v :: nb := keep_notin hq
        by_cases hE : elimSet ops j q
        · exact comp_closed (inducedSpec H (elimKeep ops j) hH).1 hS0mem hp
            (((inducedSpec H (elimKeep ops j) hH).2.2 p q).2 ⟨hpq, (comp_keep hH hS0mem hp).2, hE⟩)
        · exact absurd (hatt p hp q hpq hE) hqX
      have hCS0 := comp_absorb hH hConn hC huS0 huC hcl
      have := len_le_of_sub hCnd hS0nd hCS0
      omega
    · push Not at hCK
      have hCH : ∀ w ∈ C, w ∈ H.nodes := fun w hw => (comp_keep hH hC hw).1
      have hKH : ∀ w ∈ K, w ∈ H.nodes := fun w hw => (comp_keep hH hKmem hw).1
      have hsum := len_add_le (H := H) hCnd hKnd (fun a ha hb => hCK a ha hb)
        (fun a ha => (List.mem_append.1 ha).elim (hCH a) (hKH a))
      omega
  · -- no component of `H[E_t]` is big: in particular `H` itself
    have hBM : ¬ Big H ops ops.length := fun h => hA ⟨_, h⟩
    obtain ⟨x, hx⟩ : ∃ x, x ∈ H.nodes := by
      cases hn : H.nodes with
      | nil => simp [Graph.numNodes, hn] at hN
      | cons x _ => exact ⟨x, by simp⟩
    have hxE := hall x hx
    obtain ⟨nb, hnb⟩ : ∃ nb, Op.red x nb ∈ ops := by
      unfold elimSet elimKeep at hxE
      rw [List.take_length] at hxE
      have hmem := (List.contains_iff_mem).1 hxE
      unfold redVertices at hmem
      obtain ⟨a, ha, hfa⟩ := List.mem_filterMap.1 hmem
      cases a with
      | red w nb' =>
        simp only [Option.some.injEq] at hfa
        subst hfa
        exact ⟨nb', ha⟩
      | del w => simp at hfa
    refine ⟨x :: nb, List.mem_filterMap.2 ⟨Op.red x nb, hnb, rfl⟩, ?_⟩
    intro C hC
    have hCnd : C.Nodup := comp_nodup (inducedSpec H (fun y => !(x :: nb).contains y) hH).1 hC
    obtain ⟨u, huC⟩ := comp_exists_mem (inducedSpec H (fun y => !(x :: nb).contains y) hH).1 hC
    have huZ := comp_keep hH hC huC
    obtain ⟨S0, hS0mem, huS0⟩ := comp_exists (inducedSpec H (elimKeep ops ops.length) hH).1
      ((inducedSpec H (elimKeep ops ops.length) hH).2.1 u |>.2 ⟨huZ.1, hall u huZ.1⟩)
    have hS0size : 2 * S0.length ≤ H.numNodes := by
      by_contra hc
      exact hBM ⟨S0, hS0mem, by omega⟩
    have hcl : ∀ p q, p ∈ S0 → H.Adj p q →
        (fun y => !(x :: nb).contains y) q = true → q ∈ S0 := by
      intro p q hp hpq _hq
      have hqH : q ∈ H.nodes := hH.nbrs_sub p q hpq
      exact comp_closed (inducedSpec H (elimKeep ops ops.length) hH).1 hS0mem hp
        (((inducedSpec H (elimKeep ops ops.length) hH).2.2 p q).2
          ⟨hpq, (comp_keep hH hS0mem hp).2, hall q hqH⟩)
    have hCS0 := comp_absorb hH hConn hC huS0 huC hcl
    have := len_le_of_sub hCnd (comp_nodup (inducedSpec H _ hH).1 hS0mem) hCS0
    omega

theorem reduceLoop_red (fuel : Nat) : ∀ (G : Graph) (stack : List Nat) (opsRev : List Op),
    (∀ o ∈ opsRev, ∃ v nb, o = Op.red v nb) →
    ∀ o ∈ (reduceLoop fuel G stack opsRev).2.1, ∃ v nb, o = Op.red v nb := by
  induction fuel with
  | zero =>
    intro G stack opsRev h o ho
    cases stack with
    | nil => simp only [reduceLoop] at ho; exact h o (List.mem_reverse.1 ho)
    | cons _ _ => simp only [reduceLoop] at ho; exact h o (List.mem_reverse.1 ho)
  | succ f ih =>
    intro G stack opsRev h o ho
    cases stack with
    | nil => simp only [reduceLoop] at ho; exact h o (List.mem_reverse.1 ho)
    | cons v rest =>
      simp only [reduceLoop] at ho
      split at ho
      · exact ih _ _ _ h o ho
      · refine ih _ _ _ ?_ o ho
        intro o' ho'
        rcases List.mem_cons.1 ho' with rfl | ho''
        · exact ⟨v, _, rfl⟩
        · exact h o' ho''

theorem reduceRecord_red (G : Graph) : ∀ o ∈ (reduceRecord G).2, ∃ v nb, o = Op.red v nb := by
  intro o ho
  simp only [reduceRecord, reduceRecordF] at ho
  exact reduceLoop_red _ _ _ [] (by simp) o ho

/-! ## Main theorem -/

theorem balancedElimBag_aux (hMax : ReduceRecordMaximal)
    (hConn : ComponentsConnected) : BalancedElimBag := by
  unfold BalancedElimBag
  intro H hH hN hEmpty
  have hI := inducedSpec H (fun _ => true) hH
  have hG0 : H.copy.WF := hI.1
  have hG0adj : ∀ a b, H.copy.Adj a b ↔ H.Adj a b := by
    intro a b
    show (H.induced fun _ => true).Adj a b ↔ H.Adj a b
    rw [hI.2.2 a b]
    simp
  have hrec : OpsRecord H.copy (reduceRecord H.copy).2 (reduceRecord H.copy).1 :=
    (hMax H.copy hG0).1
  have hred := reduceRecord_red H.copy
  have hspec := reduceRecordSpec H.copy hG0
  have hnil : (reduceRecord H.copy).1.nodes = [] := by
    have h0 : (reduceRecord H.copy).1.nodes.length = 0 := hEmpty
    exact List.length_eq_zero_iff.1 h0
  have hall : ∀ x ∈ H.nodes, elimSet (reduceRecord H.copy).2 (reduceRecord H.copy).2.length x := by
    intro x hx
    have hxc : x ∈ H.copy.nodes := (hI.2.1 x).2 ⟨hx, rfl⟩
    rcases hspec.2.2.2.2 x hxc with h | h
    · rw [hnil] at h
      exact absurd h List.not_mem_nil
    · unfold elimSet elimKeep
      rw [List.take_length]
      simp [h]
  exact balanced_core H hH _ _ hred hall
    (fun t ht => exists_St H _ _ H.copy hG0 hG0adj hrec hred t ht) hConn hN

end CubicPathwidth.Alg.R7

namespace CubicPathwidth.Alg

set_option linter.unusedVariables false in

/-- `R7` (`cl:alg-elim` and Claim A.30 (`cl:alg-balanced`)): some elimination bag of `reduce_record`
is a balanced separator. Route without tree decompositions (see the module docstring of
`CubicPathwidth.Alg.R7`). The hypotheses `hSim`, `hCongr`, `hApp` are part of the planned
signature and are not needed by this proof (the attachment facts come from the record
itself, see `R7.balanced_core`); they are kept unused. -/
theorem balancedElimBag_of (hSim : TorsoSim) (hMax : ReduceRecordMaximal)
    (hConn : ComponentsConnected) (hCongr : OpsRecordCongr) (hApp : OpsRecordAppend) :
    BalancedElimBag :=
  R7.balancedElimBag_aux hMax hConn

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.balancedElimBag_of