CubicPathwidth.Alg.Proofs2.T4LoopStep

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

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets

/-!
# D2a2: one round of `t4Loop` preserves the structural invariant `T4LoopInv`

Proof of `T4LoopInvStep` (`Plan2Deletion.lean`, task D2a2) from the Stage 2 hypotheses
`ReduceRecordMaximal`, `ComponentsConnected`, `OpsRecordCongr`, `OpsRecordAppend` and
`OpsRecordFrame`. Stage 1 results (`T4Inv` bookkeeping, `ThinOK`, the commit step, the
specs of the graph layer) are imported from `Proofs/T3LoopPreserves.lean` and
`Proofs/Targets.lean`.

Four cases of one round: fuel exhaustion (the stack is dumped into `final`), a sweep
finalization, a thin round (`red` empties `J.copy.removeNode w`), and a commit (the
components of `red` replace `J`; the record is extended by the frame rule).
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace T4LoopStep

/-! ## Same graphs and records -/

theorem sameGraph_trans {G H K : Graph} (h : SameGraph G H) (h' : SameGraph H K) :
    SameGraph G K :=
  ⟨fun v => (h.1 v).trans (h'.1 v), fun u v => (h.2 u v).trans (h'.2 u v)⟩

theorem opsRecord_nil_iff (F R : Graph) : OpsRecord F [] R ↔ SameGraph F R := Iff.rfl

theorem opsRecord_del_iff (F : Graph) (w : Nat) (ops : List Op) (R : Graph) :
    OpsRecord F (Op.del w :: ops) R ↔ w ∈ F.nodes ∧ OpsRecord (F.removeNode w) ops R :=
  Iff.rfl

theorem opsRecord_red_iff (F : Graph) (v : Nat) (nb : List Nat) (ops : List Op) (R : Graph) :
    OpsRecord F (Op.red v nb :: ops) R ↔
      (v ∈ F.nodes ∧ nb.Nodup ∧ nb.length ≤ 2 ∧ (∀ x, x ∈ nb ↔ F.Adj v x) ∧
        OpsRecord (redStep F v) ops R) :=
  Iff.rfl

/-- Changing the final graph of a record by a graph with the same nodes and edges. -/
theorem opsRecord_right_congr : ∀ (ops : List Op) (F R R' : Graph),
    SameGraph R R' → OpsRecord F ops R → OpsRecord F ops R'
  | [], F, R, R', h, hF => by
    rw [opsRecord_nil_iff] at hF ⊢
    exact sameGraph_trans hF h
  | Op.red v nb :: ops, F, R, R', h, hF => by
    rw [opsRecord_red_iff] at hF ⊢
    exact ⟨hF.1, hF.2.1, hF.2.2.1, hF.2.2.2.1, opsRecord_right_congr ops _ R R' h hF.2.2.2.2⟩
  | Op.del w :: ops, F, R, R', h, hF => by
    rw [opsRecord_del_iff] at hF ⊢
    exact ⟨hF.1, opsRecord_right_congr ops _ R R' h hF.2⟩

/-- `SameGraph` between the copy-and-remove graph of `J` and the remove of `J`. -/
theorem copy_removeNode_sameGraph (hRem : RemoveNodeSpec) (hInd : InducedSpec)
    (J : Graph) (hJ : J.WF) (w : Nat) : SameGraph (J.copy.removeNode w) (J.removeNode w) := by
  have hc := hInd J (fun _ => true) hJ
  have hcopyN : ∀ x, x ∈ J.copy.nodes ↔ x ∈ J.nodes := fun x => by
    have := hc.2.1 x
    simp only [Graph.copy]
    simpa using this
  have hcopyA : ∀ x y, J.copy.Adj x y ↔ J.Adj x y := fun x y => by
    have := hc.2.2 x y
    simp only [Graph.copy]
    simpa using this
  have h1 := hRem J.copy w hc.1
  have h2 := hRem J w hJ
  refine ⟨fun x => ?_, fun x y => ?_⟩
  · rw [h1.2.1 x, h2.2.1 x, hcopyN x]
  · rw [h1.2.2 x y, h2.2.2 x y, hcopyA x y]

/-- A graph with no nodes is `SameGraph` to `Graph.empty`. -/
theorem sameGraph_empty_of_numNodes (G : Graph) (hG : G.WF) (h : G.numNodes = 0) :
    SameGraph G Graph.empty := by
  have hn : G.nodes = [] := by
    unfold Graph.numNodes at h
    exact List.length_eq_zero_iff.1 h
  refine ⟨fun x => ?_, fun u v => ?_⟩
  · rw [hn]
    simp [Graph.empty]
  · constructor
    · intro hA
      have := hG.nbrs_sub u v hA
      rw [hn] at this
      exact absurd this (List.not_mem_nil)
    · intro hA
      simp [Graph.empty, Graph.Adj, Graph.nbrs] at hA

/-! ## `unionAll` -/

theorem unionAll_nodes_iff {gs : List Graph} (hgs : ∀ J ∈ gs, J.WF) (x : Nat) :
    x ∈ (unionAll gs).nodes ↔ ∃ J ∈ gs, x ∈ J.nodes :=
  (unionAllSpec gs hgs).2.1 x

theorem unionAll_adj_iff {gs : List Graph} (hgs : ∀ J ∈ gs, J.WF) (x y : Nat) :
    (unionAll gs).Adj x y ↔ ∃ J ∈ gs, J.Adj x y :=
  (unionAllSpec gs hgs).2.2 x y

theorem unionAll_wf {gs : List Graph} (hgs : ∀ J ∈ gs, J.WF) : (unionAll gs).WF :=
  (unionAllSpec gs hgs).1

/-- `unionAll` does not see the order of its list (`SameGraph`). -/
theorem unionAll_perm_sameGraph {gs gs' : List Graph} (hp : gs.Perm gs')
    (hgs : ∀ J ∈ gs, J.WF) : SameGraph (unionAll gs) (unionAll gs') := by
  have hgs' : ∀ J ∈ gs', J.WF := fun J hJ => hgs J (hp.symm.subset hJ)
  refine ⟨fun x => ?_, fun x y => ?_⟩
  · rw [unionAll_nodes_iff hgs, unionAll_nodes_iff hgs']
    exact ⟨fun ⟨J, hJ, h⟩ => ⟨J, hp.subset hJ, h⟩, fun ⟨J, hJ, h⟩ => ⟨J, hp.symm.subset hJ, h⟩⟩
  · rw [unionAll_adj_iff hgs, unionAll_adj_iff hgs']
    exact ⟨fun ⟨J, hJ, h⟩ => ⟨J, hp.subset hJ, h⟩, fun ⟨J, hJ, h⟩ => ⟨J, hp.symm.subset hJ, h⟩⟩

theorem unionAll_cons_nodes {J : Graph} {L : List Graph} (hJ : J.WF)
    (hL : ∀ J' ∈ L, J'.WF) (x : Nat) :
    x ∈ (unionAll (J :: L)).nodes ↔ x ∈ J.nodes ∨ x ∈ (unionAll L).nodes := by
  have hgs : ∀ J' ∈ J :: L, J'.WF := by
    intro J' hJ'
    rcases List.mem_cons.1 hJ' with rfl | h
    · exact hJ
    · exact hL J' h
  rw [unionAll_nodes_iff hgs, unionAll_nodes_iff hL]
  constructor
  · rintro ⟨J', hJ', h⟩
    rcases List.mem_cons.1 hJ' with rfl | h'
    · exact Or.inl h
    · exact Or.inr ⟨J', h', h⟩
  · rintro (h | ⟨J', hJ', h⟩)
    · exact ⟨J, List.mem_cons_self, h⟩
    · exact ⟨J', List.mem_cons_of_mem _ hJ', h⟩

theorem unionAll_cons_adj {J : Graph} {L : List Graph} (hJ : J.WF)
    (hL : ∀ J' ∈ L, J'.WF) (x y : Nat) :
    (unionAll (J :: L)).Adj x y ↔ J.Adj x y ∨ (unionAll L).Adj x y := by
  have hgs : ∀ J' ∈ J :: L, J'.WF := by
    intro J' hJ'
    rcases List.mem_cons.1 hJ' with rfl | h
    · exact hJ
    · exact hL J' h
  rw [unionAll_adj_iff hgs, unionAll_adj_iff hL]
  constructor
  · rintro ⟨J', hJ', h⟩
    rcases List.mem_cons.1 hJ' with rfl | h'
    · exact Or.inl h
    · exact Or.inr ⟨J', h', h⟩
  · rintro (h | ⟨J', hJ', h⟩)
    · exact ⟨J, List.mem_cons_self, h⟩
    · exact ⟨J', List.mem_cons_of_mem _ hJ', h⟩

theorem unionAll_append_nodes {gs1 gs2 : List Graph} (h1 : ∀ J ∈ gs1, J.WF)
    (h2 : ∀ J ∈ gs2, J.WF) (x : Nat) :
    x ∈ (unionAll (gs1 ++ gs2)).nodes ↔ x ∈ (unionAll gs1).nodes ∨ x ∈ (unionAll gs2).nodes := by
  have hgs : ∀ J ∈ gs1 ++ gs2, J.WF := fun J hJ =>
    (List.mem_append.1 hJ).elim (h1 J) (h2 J)
  rw [unionAll_nodes_iff hgs, unionAll_nodes_iff h1, unionAll_nodes_iff h2]
  constructor
  · rintro ⟨J', hJ', h⟩
    rcases List.mem_append.1 hJ' with h' | h'
    · exact Or.inl ⟨J', h', h⟩
    · exact Or.inr ⟨J', h', h⟩
  · rintro (⟨J', hJ', h⟩ | ⟨J', hJ', h⟩)
    · exact ⟨J', List.mem_append_left _ hJ', h⟩
    · exact ⟨J', List.mem_append_right _ hJ', h⟩

theorem unionAll_append_adj {gs1 gs2 : List Graph} (h1 : ∀ J ∈ gs1, J.WF)
    (h2 : ∀ J ∈ gs2, J.WF) (x y : Nat) :
    (unionAll (gs1 ++ gs2)).Adj x y ↔ (unionAll gs1).Adj x y ∨ (unionAll gs2).Adj x y := by
  have hgs : ∀ J ∈ gs1 ++ gs2, J.WF := fun J hJ =>
    (List.mem_append.1 hJ).elim (h1 J) (h2 J)
  rw [unionAll_adj_iff hgs, unionAll_adj_iff h1, unionAll_adj_iff h2]
  constructor
  · rintro ⟨J', hJ', h⟩
    rcases List.mem_append.1 hJ' with h' | h'
    · exact Or.inl ⟨J', h', h⟩
    · exact Or.inr ⟨J', h', h⟩
  · rintro (⟨J', hJ', h⟩ | ⟨J', hJ', h⟩)
    · exact ⟨J', List.mem_append_left _ hJ', h⟩
    · exact ⟨J', List.mem_append_right _ hJ', h⟩

/-! ## Components -/

/-- The nodes of the component graphs of `Js` are the nodes of `Js`. -/
theorem componentGraphs_mem_nodes (hInd : InducedSpec) (hComp : ComponentsSpec)
    (Js : Graph) (hJs : Js.WF) (x : Nat) :
    (∃ C ∈ componentGraphs Js, x ∈ C.nodes) ↔ x ∈ Js.nodes := by
  constructor
  · rintro ⟨C, hC, hx⟩
    obtain ⟨c, _, rfl⟩ := CubicPathwidth.Alg.T3.componentGraphs_mem hC
    exact (((hInd Js c.contains hJs).2.1 x).1 hx).1
  · intro hx
    have hx' : x ∈ Js.components.flatten := (hComp Js hJs).1.symm.subset hx
    obtain ⟨c, hc, hxc⟩ := List.mem_flatten.1 hx'
    refine ⟨Js.induced c.contains, CubicPathwidth.Alg.T3.mem_componentGraphs_of hc, ?_⟩
    exact ((hInd Js c.contains hJs).2.1 x).2 ⟨hx, List.contains_iff_mem.2 hxc⟩

/-- Adjacency in the component graphs of `Js` is adjacency in `Js`. -/
theorem componentGraphs_adj_iff (hInd : InducedSpec) (hComp : ComponentsSpec)
    (Js : Graph) (hJs : Js.WF) (x y : Nat) :
    (∃ C ∈ componentGraphs Js, C.Adj x y) ↔ Js.Adj x y := by
  constructor
  · rintro ⟨C, hC, hA⟩
    obtain ⟨c, _, rfl⟩ := CubicPathwidth.Alg.T3.componentGraphs_mem hC
    exact (((hInd Js c.contains hJs).2.2 x y).1 hA).1
  · intro hA
    have hy : y ∈ Js.nodes := hJs.nbrs_sub x y hA
    have hx : x ∈ Js.nodes := hJs.nbrs_sub y x (hJs.symm x y hA)
    have hx' : x ∈ Js.components.flatten := (hComp Js hJs).1.symm.subset hx
    obtain ⟨c, hc, hxc⟩ := List.mem_flatten.1 hx'
    have hyc : y ∈ c := (hComp Js hJs).2.2 c hc x hxc y hA
    refine ⟨Js.induced c.contains, CubicPathwidth.Alg.T3.mem_componentGraphs_of hc, ?_⟩
    exact ((hInd Js c.contains hJs).2.2 x y).2
      ⟨hA, List.contains_iff_mem.2 hxc, List.contains_iff_mem.2 hyc⟩

/-- Reachability inside a neighbour-closed set lifts to its induced graph. -/
theorem rtg_induced_of_closed (G : Graph) (c : List Nat)
    (hcl : ∀ x ∈ c, ∀ y, G.Adj x y → y ∈ c)
    (hA : ∀ x y, (G.induced c.contains).Adj x y ↔
      G.Adj x y ∧ c.contains x = true ∧ c.contains y = true)
    (x y : Nat) (hx : x ∈ c) (h : Relation.ReflTransGen G.Adj x y) :
    Relation.ReflTransGen (G.induced c.contains).Adj x y := by
  have key : ∀ z, Relation.ReflTransGen G.Adj x z →
      z ∈ c ∧ Relation.ReflTransGen (G.induced c.contains).Adj x z := by
    intro z hz
    induction hz with
    | refl => exact ⟨hx, Relation.ReflTransGen.refl⟩
    | tail _ hbc ih =>
      obtain ⟨hb, hrt⟩ := ih
      have hc := hcl _ hb _ hbc
      exact ⟨hc, hrt.tail ((hA _ _).2 ⟨hbc, List.contains_iff_mem.2 hb,
        List.contains_iff_mem.2 hc⟩)⟩
  exact (key y h).2

/-- Degrees of a neighbour-closed component are the degrees in the parent graph. -/
theorem degree_induced_of_closed (G : Graph) (hG : G.WF) (c : List Nat)
    (hI : (G.induced c.contains).WF)
    (hA : ∀ x y, (G.induced c.contains).Adj x y ↔
      G.Adj x y ∧ c.contains x = true ∧ c.contains y = true)
    (hcl : ∀ x ∈ c, ∀ y, G.Adj x y → y ∈ c) (v : Nat) (hv : v ∈ c) :
    (G.induced c.contains).degree v = G.degree v := by
  unfold Graph.degree
  apply List.Perm.length_eq
  rw [List.perm_ext_iff_of_nodup (hI.nbrs_nodup v) (hG.nbrs_nodup v)]
  intro x
  constructor
  · intro hx
    exact ((hA v x).1 hx).1
  · intro hx
    exact (hA v x).2 ⟨hx, List.contains_iff_mem.2 hv, List.contains_iff_mem.2 (hcl v hv x hx)⟩

theorem componentGraphs_wf (hInd : InducedSpec) (Js : Graph) (hJs : Js.WF) :
    ∀ C ∈ componentGraphs Js, C.WF := by
  intro C hC
  obtain ⟨c, _, rfl⟩ := CubicPathwidth.Alg.T3.componentGraphs_mem hC
  exact (hInd Js c.contains hJs).1

/-- The component graphs of a connected graph of minimum degree `≥ 3` are pieces. -/
theorem piece_of_component (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hConn : ComponentsConnected) (Js : Graph) (hJs : Js.WF)
    (hdeg : ∀ v ∈ Js.nodes, 3 ≤ Js.degree v) :
    ∀ C ∈ componentGraphs Js, T4Piece C := by
  intro C hC
  obtain ⟨c, hc, rfl⟩ := CubicPathwidth.Alg.T3.componentGraphs_mem hC
  obtain ⟨hperm, hne, hcl⟩ := hComp Js hJs
  have hI := hInd Js c.contains hJs
  have hA := hI.2.2
  have hcl' : ∀ x ∈ c, ∀ y, Js.Adj x y → y ∈ c := hcl c hc
  refine ⟨hI.1, ?_, ?_, ?_⟩
  · obtain ⟨x, hx⟩ := List.exists_mem_of_ne_nil c (hne c hc)
    intro h
    have hxN : x ∈ (Js.induced c.contains).nodes :=
      ((hI.2.1 x).2 ⟨hperm.subset (List.mem_flatten.2 ⟨c, hc, hx⟩), List.contains_iff_mem.2 hx⟩)
    rw [h] at hxN
    exact List.not_mem_nil hxN
  · intro x hx y hy
    have hx1 := (hI.2.1 x).1 hx
    have hy1 := (hI.2.1 y).1 hy
    exact rtg_induced_of_closed Js c hcl' hA x y (List.contains_iff_mem.1 hx1.2)
      (hConn Js hJs c hc x (List.contains_iff_mem.1 hx1.2) y (List.contains_iff_mem.1 hy1.2))
  · intro v hv
    have hv1 := (hI.2.1 v).1 hv
    rw [degree_induced_of_closed Js hJs c hI.1 hA hcl' v (List.contains_iff_mem.1 hv1.2)]
    exact hdeg v hv1.1

/-! ## The records of one round -/

/-- The commit record: `J` with the deletion of `w` and the reductions of
`J.copy.removeNode w` is a legal record from `J` to the reduced graph. -/
theorem del_record_of (hRem : RemoveNodeSpec) (hInd : InducedSpec) (hMax : ReduceRecordMaximal)
    (hCongr : OpsRecordCongr) (J : Graph) (hJ : J.WF) (w : Nat) (hw : w ∈ J.nodes) :
    OpsRecord J (Op.del w :: (reduceRecordF (J.copy.removeNode w)).2.1)
      (reduceRecordF (J.copy.removeNode w)).1 := by
  have hK := CubicPathwidth.Alg.T3.copy_remove_facts hRem hInd J hJ w
  have hmx : OpsRecord (J.copy.removeNode w) (reduceRecordF (J.copy.removeNode w)).2.1
      (reduceRecordF (J.copy.removeNode w)).1 := (hMax _ hK.1).1
  have hS := copy_removeNode_sameGraph hRem hInd J hJ w
  have hJR : OpsRecord (J.removeNode w) (reduceRecordF (J.copy.removeNode w)).2.1
      (reduceRecordF (J.copy.removeNode w)).1 :=
    hCongr _ _ _ _ hK.1 (hRem J w hJ).1 hS hmx
  rw [opsRecord_del_iff]
  exact ⟨hw, hJR⟩

/-- The thin record: when the reduction of `J.copy.removeNode w` empties the graph, the
record of `J` (deletion of `w`, then the reductions) ends in the empty graph. -/
theorem thin_record_of (hRem : RemoveNodeSpec) (hInd : InducedSpec) (hMax : ReduceRecordMaximal)
    (hCongr : OpsRecordCongr) (hRed : ReduceRecordSpec) (J : Graph) (hJ : J.WF) (w : Nat)
    (hw : w ∈ J.nodes) (hz : (reduceRecordF (J.copy.removeNode w)).1.numNodes = 0) :
    OpsRecord J (Op.del w :: (reduceRecordF (J.copy.removeNode w)).2.1) Graph.empty := by
  have hK := CubicPathwidth.Alg.T3.copy_remove_facts hRem hInd J hJ w
  have hsp := CubicPathwidth.Alg.T3.red_specs hRed _ hK.1
  have hJR := del_record_of hRem hInd hMax hCongr J hJ w hw
  have hsg : SameGraph (reduceRecordF (J.copy.removeNode w)).1 Graph.empty :=
    sameGraph_empty_of_numNodes _ hsp.1 hz
  rw [opsRecord_del_iff] at hJR ⊢
  exact ⟨hw, opsRecord_right_congr _ _ _ _ hsg hJR.2⟩

/-- The record of a commit round: the record of `J` (deletion of `w`, then the reductions
ending in `Js`) is framed by the other graphs of the stack and `final`, and the global
record is extended by it. -/
theorem commit_record_of (hInd : InducedSpec) (hComp : ComponentsSpec) (hFrame : OpsRecordFrame)
    (hApp : OpsRecordAppend) (G0 J : Graph) (rest F : List Graph) (ops red : List Op) (w : Nat)
    (Js : Graph) (hG0 : G0.WF) (hJ : J.WF)
    (hRec : OpsRecord G0 ops (unionAll (J :: (rest ++ F))))
    (hdisj : ∀ B ∈ rest ++ F, ∀ x ∈ J.nodes, x ∉ B.nodes)
    (hF : ∀ B ∈ rest ++ F, B.WF) (hJs : Js.WF) (hDel : OpsRecord J (Op.del w :: red) Js) :
    OpsRecord G0 (ops ++ (Op.del w :: red)) (unionAll ((componentGraphs Js).reverse ++ rest ++ F)) := by
  have hMWF : ∀ X ∈ J :: (rest ++ F), X.WF := by
    intro X hX
    rcases List.mem_cons.1 hX with h | h
    · exact h ▸ hJ
    · exact hF X h
  have hLWF : ∀ X ∈ rest ++ F, X.WF := hF
  have hCsRevWF : ∀ C ∈ (componentGraphs Js).reverse, C.WF := fun C hC =>
    componentGraphs_wf hInd Js hJs C (List.mem_reverse.1 hC)
  have hM : (unionAll (J :: (rest ++ F))).WF := unionAll_wf hMWF
  have hL : (unionAll (rest ++ F)).WF := unionAll_wf hLWF
  have hdisj' : ∀ x, x ∈ J.nodes → x ∉ (unionAll (rest ++ F)).nodes := by
    intro x hx hxL
    obtain ⟨B, hB, hxB⟩ := (unionAll_nodes_iff hLWF x).1 hxL
    exact hdisj B hB x hx hxB
  have hMnodes := unionAll_cons_nodes hJ hLWF
  have hMadj := unionAll_cons_adj hJ hLWF
  have hCsNodes : ∀ x, x ∈ (unionAll (componentGraphs Js).reverse).nodes ↔ x ∈ Js.nodes := by
    intro x
    rw [unionAll_nodes_iff hCsRevWF]
    simp only [List.mem_reverse]
    exact componentGraphs_mem_nodes hInd hComp Js hJs x
  have hCsAdj : ∀ x y, (unionAll (componentGraphs Js).reverse).Adj x y ↔ Js.Adj x y := by
    intro x y
    rw [unionAll_adj_iff hCsRevWF]
    simp only [List.mem_reverse]
    exact componentGraphs_adj_iff hInd hComp Js hJs x y
  have hM'nodes : ∀ v, v ∈ (unionAll ((componentGraphs Js).reverse ++ (rest ++ F))).nodes ↔
      v ∈ Js.nodes ∨ v ∈ (unionAll (rest ++ F)).nodes := by
    intro v
    rw [unionAll_append_nodes hCsRevWF hLWF v, hCsNodes v]
  have hM'adj : ∀ u v, (unionAll ((componentGraphs Js).reverse ++ (rest ++ F))).Adj u v ↔
      Js.Adj u v ∨ (unionAll (rest ++ F)).Adj u v := by
    intro u v
    rw [unionAll_append_adj hCsRevWF hLWF u v, hCsAdj u v]
  have hfr := hFrame J Js (unionAll (rest ++ F)) (unionAll (J :: (rest ++ F)))
    (unionAll ((componentGraphs Js).reverse ++ (rest ++ F))) (Op.del w :: red) hJ hL hM
    hdisj' hMnodes hMadj hM'nodes hM'adj hDel
  have hrec2 := hApp G0 _ _ ops (Op.del w :: red) hG0 hM hRec hfr
  have e : (componentGraphs Js).reverse ++ rest ++ F = (componentGraphs Js).reverse ++ (rest ++ F) :=
    List.append_assoc _ _ _
  rw [e]
  exact hrec2

/-! ## The loop invariant step -/

end T4LoopStep

open T4LoopStep

/-- (D2a2) One round of `t4Loop` preserves the structural invariant `T4LoopInv`. -/
theorem t4LoopInvStep_of (hMax : ReduceRecordMaximal) (hConn : ComponentsConnected)
    (hCongr : OpsRecordCongr) (hApp : OpsRecordAppend) (hFrame : OpsRecordFrame) :
    T4LoopInvStep := by
  have hRem : RemoveNodeSpec := removeNodeSpec
  have hInd : InducedSpec := inducedSpec
  have hComp : ComponentsSpec := componentsSpec
  have hRed : ReduceRecordSpec := reduceRecordSpec
  have hWF : WFBasics := wfBasics
  unfold T4LoopInvStep
  refine ⟨fun G0 stack final ops hG0 hInv => ?_, fun G0 J rest final ops hG0 hInv => ?_⟩
  · -- fuel exhaustion: the stack is dumped into `final`
    obtain ⟨hT, hThin, hRec, hPc, hTh⟩ := hInv
    have hp : (stack ++ final.map (fun e => e.graph)).Perm
        ((final ++ stack.map fun J => FinalEntry.mk J FinalKind.sweep []).map
          (fun e => e.graph)) := by
      rw [CubicPathwidth.Alg.T3.map_graph_append_sweep]
      exact List.perm_append_comm
    have hgs : ∀ X ∈ stack ++ final.map (fun e => e.graph), X.WF := fun X hX => (hPc X hX).1
    unfold T4LoopInv
    refine ⟨?_, ?_, ?_, ?_, ?_⟩
    · rw [List.nil_append]
      exact CubicPathwidth.Alg.T3.T4Inv_perm hT hp
    · exact CubicPathwidth.Alg.T3.thinOK_sweep_list final hThin stack
    · rw [List.nil_append]
      exact opsRecord_right_congr _ _ _ _ (unionAll_perm_sameGraph hp hgs) hRec
    · intro X hX
      rw [List.nil_append] at hX
      exact hPc X (hp.symm.subset hX)
    · intro e he hk
      rcases List.mem_append.1 he with he | he
      · exact hTh e he hk
      · obtain ⟨J, _, rfl⟩ := List.mem_map.1 he
        simp at hk
  · -- one round at the head `J` of the stack
    obtain ⟨hT, hThin, hRec, hPc, hTh⟩ := hInv
    have hJp : T4Piece J := hPc J (by simp)
    have hJ : J.WF := hJp.1
    have hA : ∀ X ∈ J :: (rest ++ final.map (fun e => e.graph)), X.WF := by
      intro X hX
      exact (hPc X hX).1
    refine ⟨fun hmax => ?_, fun hmax => ?_⟩
    · -- finalize a graph of maximum degree at most `5`
      have hp := CubicPathwidth.Alg.T3.perm_entry_snoc rest final J FinalKind.sweep []
      unfold T4LoopInv
      refine ⟨CubicPathwidth.Alg.T3.T4Inv_perm hT hp, CubicPathwidth.Alg.T3.thinOK_sweep final hThin J, ?_, ?_, ?_⟩
      · exact opsRecord_right_congr _ _ _ _ (unionAll_perm_sameGraph hp hA) hRec
      · intro X hX
        exact hPc X (hp.symm.subset hX)
      · intro e he hk
        rcases List.mem_append.1 he with he | he
        · exact hTh e he hk
        · rw [List.mem_singleton] at he
          subst he
          simp at hk
    · -- a round with the chosen vertex `w`
      dsimp only
      have hpos : 0 < J.maxDegree := by omega
      have hw : t4ChooseW J ∈ J.nodes := CubicPathwidth.Alg.T3.t4ChooseW_mem J hpos
      have hK := CubicPathwidth.Alg.T3.copy_remove_facts hRem hInd J hJ (t4ChooseW J)
      have hspec := CubicPathwidth.Alg.T3.red_specs hRed _ hK.1
      have hmx : OpsRecord (J.copy.removeNode (t4ChooseW J))
          (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1
          (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1 ∧
          (∀ v ∈ (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1.nodes,
            3 ≤ (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1.degree v) :=
        ⟨(hMax _ hK.1).1, (hMax _ hK.1).2.1⟩
      refine ⟨fun hz => ?_, fun hz => ?_⟩
      · -- thin round: the graph of `w` is emptied
        have hJR := thin_record_of hRem hInd hMax hCongr hRed J hJ (t4ChooseW J) hw hz
        unfold T4LoopInv
        have hp := CubicPathwidth.Alg.T3.perm_entry_snoc rest final J FinalKind.thin
          (Op.del (t4ChooseW J) :: (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1)
        refine ⟨CubicPathwidth.Alg.T3.T4Inv_perm hT hp, CubicPathwidth.Alg.T3.thinOK_thin final hThin J
          (t4ChooseW J) _ hspec.2.2.2 hw, ?_, ?_, ?_⟩
        · exact opsRecord_right_congr _ _ _ _ (unionAll_perm_sameGraph hp hA) hRec
        · intro X hX
          exact hPc X (hp.symm.subset hX)
        · intro e he hk
          rcases List.mem_append.1 he with he | he
          · exact hTh e he hk
          · rw [List.mem_singleton] at he
            subst he
            refine ⟨hJR, ?_⟩
            rw [CubicPathwidth.Alg.T3.deletedSet_del_cons,
              CubicPathwidth.Alg.T3.deletedSet_nil_of_red _ hspec.2.2.2]
            rfl
      · -- commit round: `J` is replaced by the components of the reduced graph
        have hcommitT := CubicPathwidth.Alg.T3.commit_inv' hWF hInd hComp G0 J
          (J.copy.removeNode (t4ChooseW J)) (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1
          rest (final.map (fun e : FinalEntry => e.graph)) ops
          (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1 (t4ChooseW J) hT hw hK.2.1 hK.2.2
          hspec.1 hspec.2.1 hspec.2.2.1 hspec.2.2.2
        have hPair : (J :: (rest ++ final.map (fun e : FinalEntry => e.graph))).Pairwise
            (fun A B : Graph => ∀ x, x ∈ A.nodes → x ∉ B.nodes) := by
          obtain ⟨_, hP, _, _, _⟩ := hT
          exact hP
        have hdisj : ∀ B ∈ rest ++ final.map (fun e : FinalEntry => e.graph), ∀ x ∈ J.nodes,
            x ∉ B.nodes :=
          fun B hB x hx => (List.pairwise_cons.1 hPair).1 B hB x hx
        have hmemRF : ∀ B ∈ rest ++ final.map (fun e : FinalEntry => e.graph),
            B ∈ (J :: rest) ++ final.map (fun e : FinalEntry => e.graph) := by
          intro B hB
          rcases List.mem_append.1 hB with h | h
          · exact List.mem_append_left _ (List.mem_cons_of_mem J h)
          · exact List.mem_append_right _ h
        have hFWF : ∀ B ∈ rest ++ final.map (fun e : FinalEntry => e.graph), B.WF :=
          fun B hB => (hPc B (hmemRF B hB)).1
        unfold T4LoopInv
        refine ⟨hcommitT, hThin, ?_, ?_, ?_⟩
        · exact commit_record_of hInd hComp hFrame hApp G0 J rest
            (final.map (fun e : FinalEntry => e.graph)) ops
            (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1 (t4ChooseW J)
            (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1 hG0 hJ hRec hdisj hFWF hspec.1
            (del_record_of hRem hInd hMax hCongr J hJ (t4ChooseW J) hw)
        · intro X hX
          rcases List.mem_append.1 hX with h | h
          · rcases List.mem_append.1 h with h' | h'
            · exact piece_of_component hInd hComp hConn _ hspec.1 hmx.2 X (List.mem_reverse.1 h')
            · exact hPc X (hmemRF X (List.mem_append_left _ h'))
          · exact hPc X (hmemRF X (List.mem_append_right _ h))
        · intro e he hk
          exact hTh e he hk

end CubicPathwidth.Alg

end

#print axioms CubicPathwidth.Alg.t4LoopInvStep_of