CubicPathwidth.Alg.Proofs2.CommitBound

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

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T4.SeqH

/-!
# D2b: one commit of `algo_T4` pays for itself (`CommitBound`, Lemma A.34 (`lem:alg-deletion`))

Proves `commitBound_of` from `KeyStepAt`, `TorsoSim`, `TorsoLocal`, `TorsoPotentialBridge`,
`ReduceRecordMaximal`, `ComponentsConnected`, `OpsRecordCongr` (the last one is not
needed by this route and is kept to match the frozen signature).
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace D2b

/-! ## Graph-level helpers -/

theorem toSimple_adj (G : Graph) (hG : G.WF) (n : ℕ) (u v : Fin n) :
    (G.toSimpleGraph n).Adj u v ↔ u ≠ v ∧ G.Adj u.val v.val := by
  unfold Graph.toSimpleGraph
  rw [SimpleGraph.fromRel_adj]
  constructor
  · rintro ⟨h1, h2 | h2⟩
    · exact ⟨h1, h2⟩
    · exact ⟨h1, hG.symm _ _ h2⟩
  · rintro ⟨h1, h2⟩
    exact ⟨h1, Or.inl h2⟩

theorem deletedSet_of_red (ops : List Op) (h : ∀ o ∈ ops, ∃ v nb, o = Op.red v nb) :
    deletedSet ops = [] := by
  induction ops with
  | nil => rfl
  | cons o os ih =>
    obtain ⟨v, nb, rfl⟩ := h _ (List.mem_cons_self)
    simp only [deletedSet, List.filterMap_cons]
    exact ih fun o' ho' => h o' (List.mem_cons_of_mem _ ho')

theorem comp_mem {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.mem_iff.mpr hx)
  exact ⟨c, hc, hxc⟩

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.mem_iff.mp (List.mem_flatten.mpr ⟨c, hc, hx⟩)

theorem comps_disjoint {G : Graph} (hG : G.WF) : G.components.Pairwise List.Disjoint := 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).2

theorem mem_induced_iff {G : Graph} (hG : G.WF) (c : List Nat) (x : Nat) :
    x ∈ (G.induced c.contains).nodes ↔ x ∈ G.nodes ∧ x ∈ c := by
  rw [(inducedSpec G c.contains hG).2.1]
  simp

theorem rtg_induced {G : Graph} (hG : G.WF) (c : List Nat)
    (hc : ∀ x ∈ c, ∀ y, G.Adj x y → y ∈ c) (x : Nat) (hx : x ∈ c) (y : Nat)
    (h : Relation.ReflTransGen G.Adj x y) :
    y ∈ c ∧ Relation.ReflTransGen (G.induced c.contains).Adj x y := by
  induction h with
  | refl => exact ⟨hx, Relation.ReflTransGen.refl⟩
  | @tail b d _ hab ih =>
    obtain ⟨hb, hr⟩ := ih
    have hd : d ∈ c := hc b hb d hab
    refine ⟨hd, Relation.ReflTransGen.tail hr ?_⟩
    have := ((inducedSpec G c.contains hG).2.2 b d).mpr ⟨hab, by simpa using hb, by simpa using hd⟩
    exact this

theorem componentGraphs_pairwise {G : Graph} (hG : G.WF) :
    (componentGraphs G).Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes) := by
  unfold componentGraphs
  rw [List.pairwise_map]
  refine List.Pairwise.imp (fun {c1 c2} hd x hx1 hx2 => ?_) (comps_disjoint hG)
  rw [mem_induced_iff hG] at hx1 hx2
  exact List.disjoint_left.mp hd hx1.2 hx2.2

theorem componentGraphs_props {G : Graph} (hG : G.WF) (hC : ComponentsConnected) :
    ∀ J ∈ componentGraphs G, J.WF ∧ J.nodes ≠ [] ∧
      ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y := by
  intro J hJ
  unfold componentGraphs at hJ
  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hJ
  have hcl := (componentsSpec G hG).2.2 c hc
  have hcne := (componentsSpec G hG).2.1 c hc
  refine ⟨(inducedSpec G c.contains hG).1, ?_, ?_⟩
  · obtain ⟨x, hx⟩ := List.exists_mem_of_ne_nil c hcne
    intro h
    have hxJ : x ∈ (G.induced c.contains).nodes := (mem_induced_iff hG c x).mpr
      ⟨comp_mem_nodes hG hc hx, hx⟩
    rw [h] at hxJ
    simp at hxJ
  · intro x hx y hy
    have hx' := ((mem_induced_iff hG c x).mp hx).2
    have hy' := ((mem_induced_iff hG c y).mp hy).2
    exact (rtg_induced hG c hcl x hx' y (hC G hG c hc x hx' y hy')).2

theorem compGraph_cover {G : Graph} (hG : G.WF) (x : Nat) :
    x ∈ G.nodes ↔ ∃ J ∈ componentGraphs G, x ∈ J.nodes := by
  constructor
  · intro hx
    obtain ⟨c, hc, hxc⟩ := comp_mem hG hx
    exact ⟨G.induced c.contains, List.mem_map_of_mem hc,
      (mem_induced_iff hG c x).mpr ⟨hx, hxc⟩⟩
  · rintro ⟨J, hJ, hxJ⟩
    unfold componentGraphs at hJ
    obtain ⟨c, _, rfl⟩ := List.mem_map.mp hJ
    exact ((mem_induced_iff hG c x).mp hxJ).1

theorem compGraph_adj {G : Graph} (hG : G.WF) (a b : Nat) :
    G.Adj a b ↔ ∃ J ∈ componentGraphs G, J.Adj a b := by
  constructor
  · intro h
    obtain ⟨c, hc, hac⟩ := comp_mem hG (wfBasics G hG a b h).1
    have hb : b ∈ c := (componentsSpec G hG).2.2 c hc a hac b h
    refine ⟨G.induced c.contains, List.mem_map_of_mem hc, ?_⟩
    exact ((inducedSpec G c.contains hG).2.2 a b).mpr ⟨h, by simpa using hac, by simpa using hb⟩
  · rintro ⟨J, hJ, hadj⟩
    unfold componentGraphs at hJ
    obtain ⟨c, _, rfl⟩ := List.mem_map.mp hJ
    exact ((inducedSpec G c.contains hG).2.2 a b).mp hadj |>.1

theorem compGraph_deg {G : Graph} (hG : G.WF) {c : List Nat} (hc : c ∈ G.components)
    {x : Nat} (hx : x ∈ c) : (G.induced c.contains).degree x = G.degree x := by
  unfold Graph.degree
  apply List.Perm.length_eq
  rw [List.perm_ext_iff_of_nodup ((inducedSpec G c.contains hG).1.nbrs_nodup x) (hG.nbrs_nodup x)]
  intro y
  have hcl := (componentsSpec G hG).2.2 c hc
  have hxc : c.contains x = true := by simpa using hx
  constructor
  · intro h
    exact ((inducedSpec G c.contains hG).2.2 x y).mp h |>.1
  · intro h
    have hy : y ∈ c := hcl x hx y h
    exact ((inducedSpec G c.contains hG).2.2 x y).mpr ⟨h, hxc, by simpa using hy⟩

/-! ## Maximum degree and the choice of the centre `t4ChooseW` -/

theorem foldl_max_ge (f : Nat → Nat) (l : List Nat) :
    ∀ acc : Nat, acc ≤ l.foldl (fun m v => max m (f v)) acc := by
  induction l with
  | nil => intro acc; exact le_refl _
  | cons a l ih =>
    intro acc
    simp only [List.foldl_cons]
    exact le_trans (le_max_left acc (f a)) (ih _)

theorem le_foldl_max (f : Nat → Nat) (l : List Nat) :
    ∀ (acc v : Nat), v ∈ l → f v ≤ l.foldl (fun m v => max m (f v)) acc := by
  induction l with
  | nil => intro acc v hv; simp at hv
  | cons a l ih =>
    intro acc v hv
    simp only [List.foldl_cons]
    rcases List.mem_cons.mp hv with rfl | hv
    · exact le_trans (le_max_right acc (f v)) (foldl_max_ge f l _)
    · exact ih _ v hv

theorem foldl_max_eq (f : Nat → Nat) (l : List Nat) : ∀ acc : Nat,
    l.foldl (fun m v => max m (f v)) acc = acc ∨
      ∃ v ∈ l, l.foldl (fun m v => max m (f v)) acc = f v := by
  induction l with
  | nil => intro acc; exact Or.inl rfl
  | cons a l ih =>
    intro acc
    simp only [List.foldl_cons]
    rcases ih (max acc (f a)) with h | ⟨v, hv, h⟩
    · rcases max_choice acc (f a) with h' | h'
      · exact Or.inl (h.trans h')
      · exact Or.inr ⟨a, List.mem_cons_self, h.trans h'⟩
    · exact Or.inr ⟨v, List.mem_cons_of_mem _ hv, h⟩

theorem deg_le_maxDeg (J : Graph) {v : Nat} (hv : v ∈ J.nodes) : J.degree v ≤ J.maxDegree :=
  le_foldl_max J.degree J.nodes 0 v hv

theorem exists_deg_eq_maxDeg (J : Graph) (hpos : 0 < J.maxDegree) :
    ∃ v ∈ J.nodes, J.degree v = J.maxDegree := by
  rcases foldl_max_eq J.degree J.nodes 0 with h | ⟨v, hv, h⟩
  · have h0 : J.maxDegree = 0 := h
    omega
  · exact ⟨v, hv, h.symm⟩

theorem getD_min_mem (l : List Nat) (h : l ≠ []) : (l.min?).getD 0 ∈ l := by
  cases hm : l.min? with
  | none => exact absurd (List.min?_eq_none_iff.mp hm) h
  | some a => simpa [hm] using List.min?_mem hm

theorem t4ChooseW_spec (J : Graph) (hJ : J.WF)
    (hC : ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y)
    (hpos : 0 < J.maxDegree) :
    t4ChooseW J ∈ J.nodes ∧ J.degree (t4ChooseW J) = J.maxDegree ∧
      ((∃ u ∈ J.nbrs (t4ChooseW J), J.degree u < J.maxDegree) ∨
        (∀ v ∈ J.nodes, J.degree v = J.maxDegree)) := by
  obtain ⟨v0, hv0, hd0⟩ := exists_deg_eq_maxDeg J hpos
  unfold t4ChooseW
  simp only []
  set cands := List.filter (fun v => J.degree v == J.maxDegree) J.nodes with hcands
  set good := List.filter (fun v => (J.nbrs v).any fun u => decide (J.degree u < J.maxDegree))
    cands with hgood
  have hmemC : ∀ v, v ∈ cands ↔ v ∈ J.nodes ∧ J.degree v = J.maxDegree := by
    intro v
    simp [hcands]
  have hmemG : ∀ v, v ∈ good ↔ v ∈ cands ∧ ∃ u ∈ J.nbrs v, J.degree u < J.maxDegree := by
    intro v
    simp [hgood]
  have hcne : cands ≠ [] := by
    obtain ⟨v0', h0⟩ : ∃ v, v ∈ cands := ⟨v0, (hmemC v0).mpr ⟨hv0, hd0⟩⟩
    exact fun h => by simp [h] at h0
  split_ifs with hg
  · have hgnil : good = [] := List.isEmpty_iff.mp hg
    have hwX := getD_min_mem cands hcne
    generalize (cands.min?).getD 0 = w at hwX ⊢
    have hw' := (hmemC w).mp hwX
    refine ⟨hw'.1, hw'.2, Or.inr ?_⟩
    have claim : ∀ y, Relation.ReflTransGen J.Adj w y →
        y ∈ J.nodes ∧ J.degree y = J.maxDegree := by
      intro y hy
      induction hy with
      | refl => exact hw'
      | @tail b d _ hab ih =>
        have hd : d ∈ J.nodes := hJ.nbrs_sub b d hab
        have hle : J.degree d ≤ J.maxDegree := deg_le_maxDeg J hd
        refine ⟨hd, le_antisymm hle ?_⟩
        by_contra hlt
        push Not at hlt
        have hbg : b ∈ good := (hmemG b).mpr ⟨(hmemC b).mpr ih, d, hab, hlt⟩
        rw [hgnil] at hbg
        simp at hbg
    intro v hv
    exact (claim v (hC w hw'.1 v hv)).2
  · have hgne : good ≠ [] := fun h => hg (by simp [h])
    have hwX := getD_min_mem good hgne
    generalize (good.min?).getD 0 = w at hwX ⊢
    obtain ⟨hwC, u, hu, hlt⟩ := (hmemG w).mp hwX
    have hw' := (hmemC w).mp hwC
    exact ⟨hw'.1, hw'.2, Or.inl ⟨u, hu, hlt⟩⟩


/-! ## Copies, removal, and the torso of a piece -/

theorem copy_wf {J : Graph} (hJ : J.WF) : J.copy.WF := (inducedSpec J (fun _ => true) hJ).1

theorem copy_nodes {J : Graph} (hJ : J.WF) (x : Nat) : x ∈ J.copy.nodes ↔ x ∈ J.nodes :=
  ⟨fun h => ((inducedSpec J (fun _ => true) hJ).2.1 x).mp h |>.1,
    fun h => ((inducedSpec J (fun _ => true) hJ).2.1 x).mpr ⟨h, rfl⟩⟩

theorem copy_adj {J : Graph} (hJ : J.WF) (x y : Nat) : J.copy.Adj x y ↔ J.Adj x y :=
  ⟨fun h => ((inducedSpec J (fun _ => true) hJ).2.2 x y).mp h |>.1,
    fun h => ((inducedSpec J (fun _ => true) hJ).2.2 x y).mpr ⟨h, rfl, rfl⟩⟩

/-- The graph `J - w` (copy, then remove `w`), as in `reduce_record(J.copy.remove_node w)`. -/
def Hg (J : Graph) (w : Nat) : Graph := J.copy.removeNode w

/-- The reduced graph `R` of `Hg J w`. -/
def Rg (J : Graph) (w : Nat) : Graph := (reduceRecordF (Hg J w)).1

/-- The vertices of `J` as a finset of `Fin n`. -/
def V0of (F : Graph) (n : ℕ) : Finset (Fin n) := Finset.univ.filter fun x => x.val ∈ F.nodes

/-- The vertices of `R` as a finset of `Fin n`. -/
def Bof (R : Graph) (n : ℕ) : Finset (Fin n) := Finset.univ.filter fun x => x.val ∈ R.nodes

theorem mem_V0of {F : Graph} {n : ℕ} (x : Fin n) : x ∈ V0of F n ↔ x.val ∈ F.nodes := by
  simp [V0of]

theorem mem_Bof {R : Graph} {n : ℕ} (x : Fin n) : x ∈ Bof R n ↔ x.val ∈ R.nodes := by
  simp [Bof]

theorem Hg_wf {J : Graph} (hJ : J.WF) (w : Nat) : (Hg J w).WF :=
  (removeNodeSpec _ w (copy_wf hJ)).1

theorem Hg_nodes {J : Graph} (hJ : J.WF) (w x : Nat) :
    x ∈ (Hg J w).nodes ↔ x ∈ J.nodes ∧ x ≠ w := by
  unfold Hg
  rw [(removeNodeSpec _ w (copy_wf hJ)).2.1 x, copy_nodes hJ]

theorem Hg_adj {J : Graph} (hJ : J.WF) (w u v : Nat) :
    (Hg J w).Adj u v ↔ J.Adj u v ∧ u ≠ w ∧ v ≠ w := by
  unfold Hg
  rw [(removeNodeSpec _ w (copy_wf hJ)).2.2 u v, copy_adj hJ]

/-- `OpsRecord J [] J`. -/
theorem opsRecord_nil_self (J : Graph) : OpsRecord J [] J := by
  show SameGraph J J
  exact ⟨fun _ => Iff.rfl, fun _ _ => Iff.rfl⟩

/-- Unpacking `TorsoSim` for a record with no deletions. -/
theorem sim_unpack (hSim : TorsoSim) {n : ℕ} {F R : Graph} {ops : List Op} (hF : F.WF)
    (hn : ∀ v ∈ F.nodes, v < n) (hops : OpsRecord F ops R) (hdel : deletedSet ops = []) :
    T4.Good (F.toSimpleGraph n) (V0of F n) (V0of F n) ∧
    T4.Reach (F.toSimpleGraph n) (V0of F n, V0of F n) (V0of F n, Bof R n) ∧
    ∀ x y : Fin n, (T4.tgraph (F.toSimpleGraph n) (V0of F n) (Bof R n)).Adj x y ↔
      R.Adj x.val y.val := by
  have h := hSim n F R ops hF hn hops
  have hF1 : (V0of F n).filter (fun x : Fin n => x.val ∉ deletedSet ops) = V0of F n :=
    Finset.filter_true_of_mem fun x _ => by simp [hdel]
  refine ⟨h.1, ?_, ?_⟩
  · have h2 := h.2.1
    rw [show (Finset.univ.filter fun x : Fin n => x.val ∈ F.nodes).filter
        (fun x : Fin n => x.val ∉ deletedSet ops) = V0of F n from hF1] at h2
    exact h2
  · have h3 := h.2.2
    rw [show (Finset.univ.filter fun x : Fin n => x.val ∈ F.nodes).filter
        (fun x : Fin n => x.val ∉ deletedSet ops) = V0of F n from hF1] at h3
    exact h3

/-- The torso of a piece `J` (one component, no deletions): the potential bridge applied
to the single graph `[J]`. -/
theorem piece_torso (hSim : TorsoSim) (hBr : TorsoPotentialBridge) {J : Graph} {n : ℕ}
    (hJ : J.WF) (hC : ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y)
    (hJne : J.nodes ≠ []) (hn : ∀ v ∈ J.nodes, v < n) :
    T4.Good (J.toSimpleGraph n) (V0of J n) (V0of J n) ∧
    (∀ x : Fin n, x.val ∈ J.nodes → T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) x =
      J.degree x.val) ∧
    V0of J n ∈ T4.tcomps (J.toSimpleGraph n) (V0of J n) (V0of J n) ∧
    (∀ x y : Fin n, (T4.tgraph (J.toSimpleGraph n) (V0of J n) (V0of J n)).Adj x y ↔
      J.Adj x.val y.val) ∧
    ∀ b : ℕ → ℝ, T4.psiMinus b (J.toSimpleGraph n) (V0of J n) (V0of J n) =
      psiMinusPort b J := by
  obtain ⟨hGood, -, hadj⟩ := sim_unpack hSim hJ hn (opsRecord_nil_self J) rfl
  have hBJ : Bof J n = V0of J n := rfl
  rw [hBJ] at hadj
  have hgs : ∀ J' ∈ [J], J'.WF ∧ J'.nodes ≠ [] ∧
      ∀ x ∈ J'.nodes, ∀ y ∈ J'.nodes, Relation.ReflTransGen J'.Adj x y := by
    intro J' hJ'
    simp only [List.mem_singleton] at hJ'
    subst hJ'
    exact ⟨hJ, hJne, hC⟩
  have hpw : [J].Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes) :=
    List.pairwise_singleton _ _
  have hn' : ∀ J' ∈ [J], ∀ v ∈ J'.nodes, v < n := by
    intro J' hJ' v hv
    simp only [List.mem_singleton] at hJ'
    subst hJ'
    exact hn v hv
  have hmemB : ∀ x : Fin n, x ∈ V0of J n ↔ ∃ J' ∈ [J], x.val ∈ J'.nodes := by
    intro x
    simp [mem_V0of]
  have hadj' : ∀ x y : Fin n, (T4.tgraph (J.toSimpleGraph n) (V0of J n) (V0of J n)).Adj x y ↔
      ∃ J' ∈ [J], J'.Adj x.val y.val := by
    intro x y
    simpa using hadj x y
  obtain ⟨c1, c2, -, c4⟩ := hBr n (J.toSimpleGraph n) (V0of J n) (V0of J n) [J] hgs hpw hn'
    hmemB hadj'
  refine ⟨hGood, ?_, ?_, ?_, ?_⟩
  · intro x hx
    exact c1 J (by simp) x hx
  · exact c2 J (by simp)
  · intro x y
    rw [hadj x y]
  · intro b
    have := (c4 b).2
    simpa using this

theorem compGraph_deg' {G : Graph} (hG : G.WF) {J' : Graph} (hJ' : J' ∈ componentGraphs G)
    {x : Nat} (hx : x ∈ J'.nodes) : J'.degree x = G.degree x := by
  unfold componentGraphs at hJ'
  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hJ'
  exact compGraph_deg hG hc ((mem_induced_iff hG c x).mp hx).2

theorem compGraph_nodes_sub {G : Graph} (hG : G.WF) {J' : Graph} (hJ' : J' ∈ componentGraphs G)
    {x : Nat} (hx : x ∈ J'.nodes) : x ∈ G.nodes := by
  unfold componentGraphs at hJ'
  obtain ⟨c, _, rfl⟩ := List.mem_map.mp hJ'
  exact ((mem_induced_iff hG c x).mp hx).1

/-- The torso of the reduced graph `R = Rg J w` on the state `(F₀, Bof R n)`, obtained from
`TorsoSim` for `Hg J w` and `TorsoLocal`. -/
theorem red_torso (hSim : TorsoSim) (hLoc : TorsoLocal) (hMax : ReduceRecordMaximal)
    {J : Graph} {n : ℕ} (hJ : J.WF) (hn : ∀ v ∈ J.nodes, v < n) {w : Nat}
    (hwn : w < n) :
    (Rg J w).WF ∧ (∀ x ∈ (Rg J w).nodes, x ∈ J.nodes ∧ x ≠ w) ∧
    (∀ v ∈ (Rg J w).nodes, 3 ≤ (Rg J w).degree v) ∧
    Bof (Rg J w) n ⊆ (V0of J n).erase ⟨w, hwn⟩ ∧
    T4.Reach (J.toSimpleGraph n) ((V0of J n).erase ⟨w, hwn⟩, (V0of J n).erase ⟨w, hwn⟩)
      ((V0of J n).erase ⟨w, hwn⟩, Bof (Rg J w) n) ∧
    ∀ x y : Fin n, (T4.tgraph (J.toSimpleGraph n) ((V0of J n).erase ⟨w, hwn⟩)
      (Bof (Rg J w) n)).Adj x y ↔ (Rg J w).Adj x.val y.val := by
  have hHW : (Hg J w).WF := Hg_wf hJ w
  have hHn : ∀ v ∈ (Hg J w).nodes, v < n := fun v hv => hn v ((Hg_nodes hJ w v).mp hv).1
  have hRS := reduceRecordSpec (Hg J w) hHW
  dsimp only at hRS
  obtain ⟨hRS1, hRS2, -, hRS4, -⟩ := hRS
  have hMx := hMax (Hg J w) hHW
  dsimp only at hMx
  have hops : OpsRecord (Hg J w) (reduceRecordF (Hg J w)).2.1 (Rg J w) := hMx.1
  have hdel : deletedSet (reduceRecordF (Hg J w)).2.1 = [] := by
    apply deletedSet_of_red
    intro o ho
    obtain ⟨v, nb, h, -⟩ := hRS4 o ho
    exact ⟨v, nb, h⟩
  obtain ⟨-, hReachH, hAdjH⟩ := sim_unpack hSim hHW hHn hops hdel
  have hVH : V0of (Hg J w) n = (V0of J n).erase ⟨w, hwn⟩ := by
    ext x
    rw [mem_V0of, Finset.mem_erase, mem_V0of, Hg_nodes hJ]
    constructor
    · rintro ⟨h1, h2⟩
      exact ⟨fun h => h2 (congrArg Fin.val h), h1⟩
    · rintro ⟨h1, h2⟩
      exact ⟨h2, fun h => h1 (Fin.ext h)⟩
  have hR2 : ∀ x ∈ (Rg J w).nodes, x ∈ J.nodes ∧ x ≠ w := fun x hx =>
    (Hg_nodes hJ w x).mp (hRS2 x hx)
  have hRsub : Bof (Rg J w) n ⊆ (V0of J n).erase ⟨w, hwn⟩ := by
    intro x hx
    rw [mem_Bof] at hx
    rw [Finset.mem_erase, mem_V0of]
    refine ⟨fun h => ?_, (hR2 _ hx).1⟩
    exact (hR2 _ hx).2 (congrArg Fin.val h)
  have hagree : ∀ u ∈ (V0of J n).erase ⟨w, hwn⟩, ∀ v ∈ (V0of J n).erase ⟨w, hwn⟩,
      (J.toSimpleGraph n).Adj u v ↔ ((Hg J w).toSimpleGraph n).Adj u v := by
    intro u hu v hv
    rw [Finset.mem_erase, mem_V0of] at hu hv
    have huw : u.val ≠ w := fun h => hu.1 (Fin.ext h)
    have hvw : v.val ≠ w := fun h => hv.1 (Fin.ext h)
    rw [toSimple_adj J hJ, toSimple_adj (Hg J w) hHW, Hg_adj hJ]
    exact and_congr_right fun _ => ⟨fun h => ⟨h, huw, hvw⟩, fun h => h.1⟩
  obtain ⟨hTG, hRe⟩ := hLoc n (J.toSimpleGraph n) ((Hg J w).toSimpleGraph n)
    ((V0of J n).erase ⟨w, hwn⟩) hagree
  rw [hVH] at hReachH hAdjH
  have hBsub := hRsub
  refine ⟨hRS1, hR2, hMx.2.1, hRsub, ?_, ?_⟩
  · exact hRe _ _ _ _ subset_rfl subset_rfl hReachH
  · intro x y
    rw [hTG _ _ hRsub subset_rfl]
    exact hAdjH x y

/-- The potential bridge for the components of a reduced graph `R` on a state whose core is
`B = Bof R n` and whose torso is `R`. -/
theorem red_bridge (hBr : TorsoPotentialBridge) (hConn : ComponentsConnected) {n : ℕ}
    {R : Graph} (S : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (hR : R.WF)
    (hRn : ∀ v ∈ R.nodes, v < n)
    (hB : ∀ x : Fin n, x ∈ B ↔ x.val ∈ R.nodes)
    (hadj : ∀ x y : Fin n, (T4.tgraph S F B).Adj x y ↔ R.Adj x.val y.val) :
    (∀ b : ℕ → ℝ, T4.psiMinus b S F B = ((componentGraphs R).map (psiMinusPort b)).sum) ∧
    (∀ x : Fin n, x ∈ B → T4.tdeg S F B x = R.degree x.val) := by
  have hn' : ∀ J ∈ componentGraphs R, ∀ v ∈ J.nodes, v < n := fun J hJ v hv =>
    hRn v (compGraph_nodes_sub hR hJ hv)
  have hmemB : ∀ x : Fin n, x ∈ B ↔ ∃ J ∈ componentGraphs R, x.val ∈ J.nodes := fun x => by
    rw [hB x]
    exact compGraph_cover hR x.val
  have hadj' : ∀ x y : Fin n, (T4.tgraph S F B).Adj x y ↔
      ∃ J ∈ componentGraphs R, J.Adj x.val y.val := fun x y =>
    (hadj x y).trans (compGraph_adj hR x.val y.val)
  obtain ⟨c1, -, -, c4⟩ := hBr n S F B (componentGraphs R) (componentGraphs_props hR hConn)
    (componentGraphs_pairwise hR) hn' hmemB hadj'
  refine ⟨fun b => (c4 b).2, ?_⟩
  intro x hx
  obtain ⟨J', hJ', hxJ'⟩ := (hmemB x).mp hx
  rw [c1 J' hJ' x hxJ']
  exact compGraph_deg' hR hJ' hxJ'

end D2b

open D2b in

theorem commitBound_of (hKey : KeyStepAt) (hSim : TorsoSim) (hLoc : TorsoLocal)
    (hBr : TorsoPotentialBridge) (hMax : ReduceRecordMaximal) (hConn : ComponentsConnected)
    (hCongr : OpsRecordCongr) : CommitBound := by
  intro J hpiece hbig
  obtain ⟨hJ, hJne, hJconn, hJdeg3⟩ := hpiece
  intro red hredne
  have hpos : 0 < J.maxDegree := by omega
  obtain ⟨n, hn⟩ : ∃ n : ℕ, ∀ v ∈ J.nodes, v < n :=
    ⟨J.nodes.sum + 1, fun v hv => by have := List.le_sum_of_mem hv; omega⟩
  obtain ⟨hwJ, hwdeg, hwreg⟩ := t4ChooseW_spec J hJ hJconn hpos
  have hwn : t4ChooseW J < n := hn _ hwJ
  obtain ⟨hRW, hRsub, hRdeg3, hBsub, hReach, hAdjR⟩ := red_torso hSim hLoc hMax hJ hn hwn
  obtain ⟨hGood, hdegJ, hCJ, hadjJ, hpsiJ⟩ := piece_torso hSim hBr hJ hJconn hJne hn
  have hRn : ∀ v ∈ (Rg J (t4ChooseW J)).nodes, v < n := fun v hv => hn v (hRsub v hv).1
  obtain ⟨hpsiR, -⟩ := red_bridge hBr hConn (J.toSimpleGraph n)
    ((V0of J n).erase ⟨t4ChooseW J, hwn⟩) (Bof (Rg J (t4ChooseW J)) n) hRW hRn
    (fun x => mem_Bof x) hAdjR
  have hwdegF : T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) ⟨t4ChooseW J, hwn⟩ =
      J.maxDegree := by
    rw [hdegJ _ hwJ]
    exact hwdeg
  have h2 : ∀ v ∈ V0of J n, 3 ≤ T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) v := by
    intro x hx
    have hxJ := (mem_V0of x).mp hx
    rw [hdegJ x hxJ]
    exact hJdeg3 _ hxJ
  have h4 : (⟨t4ChooseW J, hwn⟩ : Fin n) ∈ V0of J n := (mem_V0of _).mpr hwJ
  have h5 : ∀ v ∈ V0of J n, T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) v ≤
      T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) ⟨t4ChooseW J, hwn⟩ := by
    intro x hx
    have hxJ := (mem_V0of x).mp hx
    rw [hdegJ x hxJ, hwdegF]
    exact deg_le_maxDeg J hxJ
  have h6 : 6 ≤ T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) ⟨t4ChooseW J, hwn⟩ := by
    rw [hwdegF]
    omega
  have h7 : (∀ v ∈ V0of J n, T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) v =
        T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) ⟨t4ChooseW J, hwn⟩) ∨
      ∃ x, (T4.tgraph (J.toSimpleGraph n) (V0of J n) (V0of J n)).Adj ⟨t4ChooseW J, hwn⟩ x ∧
        T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) x <
          T4.tdeg (J.toSimpleGraph n) (V0of J n) (V0of J n) ⟨t4ChooseW J, hwn⟩ := by
    rcases hwreg with ⟨u, hu, hlt⟩ | hall
    · right
      have huJ : u ∈ J.nodes := hJ.nbrs_sub _ _ hu
      refine ⟨⟨u, hn u huJ⟩, (hadjJ _ _).mpr hu, ?_⟩
      rw [hdegJ ⟨u, hn u huJ⟩ huJ, hwdegF]
      show J.degree u < J.maxDegree
      exact hlt
    · left
      intro x hx
      have hxJ := (mem_V0of x).mp hx
      rw [hdegJ x hxJ, hwdegF, hall x.val hxJ]
  have h11 : ∃ u ∈ Bof (Rg J (t4ChooseW J)) n, u ∈ V0of J n := by
    have hne : (Rg J (t4ChooseW J)).nodes ≠ [] := by
      intro h
      apply hredne
      unfold Graph.numNodes
      rw [show red.1.nodes = [] from h]
      rfl
    obtain ⟨u, hu⟩ := List.exists_mem_of_ne_nil _ hne
    exact ⟨⟨u, hn u (hRsub u hu).1⟩, (mem_Bof _).mpr hu, (mem_V0of _).mpr (hRsub u hu).1⟩
  have h10 : ∀ v ∈ Bof (Rg J (t4ChooseW J)) n, 3 ≤ T4.tdeg (J.toSimpleGraph n)
      ((V0of J n).erase ⟨t4ChooseW J, hwn⟩) (Bof (Rg J (t4ChooseW J)) n) v := by
    intro x hx
    rw [(red_bridge hBr hConn (J.toSimpleGraph n) ((V0of J n).erase ⟨t4ChooseW J, hwn⟩)
      (Bof (Rg J (t4ChooseW J)) n) hRW hRn (fun x => mem_Bof x) hAdjR).2 x hx]
    exact hRdeg3 _ ((mem_Bof x).mp hx)
  have hKeyApp := hKey T4.sigma T4.seqClaim_h.1 n (J.toSimpleGraph n) (V0of J n) (V0of J n)
    (V0of J n) (Bof (Rg J (t4ChooseW J)) n) ⟨t4ChooseW J, hwn⟩ hGood h2 hCJ h4 h5 h6 h7
    hBsub hReach h10 h11
  rw [hpsiR T4.sigma, hpsiJ T4.sigma] at hKeyApp
  exact hKeyApp

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.commitBound_of