CubicPathwidth.Alg.Proofs2.TorsoBridge

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

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.T4.BasicPsi

/-!
# Task D3: the potential bridge (`TorsoPotentialBridge`, `PsiPortFacts`)

Proves `torsoPotentialBridge : TorsoPotentialBridge` and `psiPortFacts : PsiPortFacts`
(statements of `CubicPathwidth/Alg/Plan2Deletion.lean`, not edited).
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace D3

variable {n : ℕ}

/-! ## Finite sets indexed by list nodes -/

theorem mem_finNodes {J : Graph} {x : Fin n} : x ∈ finNodes n J ↔ x.val ∈ J.nodes := by
  simp [finNodes]

theorem map_filter_val (L : List Nat) (hL : ∀ a ∈ L, a < n) :
    ((Finset.univ : Finset (Fin n)).filter fun w => w.val ∈ L).map Fin.valEmbedding =
      L.toFinset := by
  ext a
  simp only [Finset.mem_map, Finset.mem_filter, Finset.mem_univ, true_and,
    Fin.valEmbedding_apply, List.mem_toFinset]
  constructor
  · rintro ⟨w, hw, rfl⟩
    exact hw
  · intro ha
    exact ⟨⟨a, hL a ha⟩, ha, rfl⟩

theorem sum_filter_val (L : List Nat) (hL : ∀ a ∈ L, a < n) (hnd : L.Nodup) (g : Nat → ℝ) :
    ∑ w ∈ (Finset.univ : Finset (Fin n)).filter (fun w => w.val ∈ L), g w.val =
      (L.map g).sum := by
  have h := congrArg (fun s => ∑ a ∈ s, g a) (map_filter_val (n := n) L hL)
  simp only [Finset.sum_map, Fin.valEmbedding_apply] at h
  rw [h, List.sum_toFinset g hnd]

theorem card_filter_val (L : List Nat) (hL : ∀ a ∈ L, a < n) (hnd : L.Nodup) :
    ((Finset.univ : Finset (Fin n)).filter fun w => w.val ∈ L).card = L.length := by
  have h := congrArg Finset.card (map_filter_val (n := n) L hL)
  rw [Finset.card_map, List.toFinset_card_of_nodup hnd] at h
  exact h

theorem sum_finNodes (J : Graph) (hnd : J.nodes.Nodup) (hlt : ∀ v ∈ J.nodes, v < n)
    (g : Nat → ℝ) : ∑ x ∈ finNodes n J, g x.val = (J.nodes.map g).sum :=
  sum_filter_val J.nodes hlt hnd g

/-- Splitting a sum over a set that is the union of pairwise disjoint pieces. -/
theorem sum_split (f : Fin n → ℝ) (gs : List Graph) :
    ∀ (B : Finset (Fin n)),
      gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes) →
      (∀ x : Fin n, x ∈ B ↔ ∃ J ∈ gs, x.val ∈ J.nodes) →
      ∑ x ∈ B, f x = (gs.map fun J => ∑ x ∈ finNodes n J, f x).sum := by
  induction gs with
  | nil =>
    intro B _ hB
    have hB0 : B = ∅ := by
      ext x
      simp only [Finset.notMem_empty, iff_false]
      intro hx
      obtain ⟨J, hJ, _⟩ := (hB x).1 hx
      simp at hJ
    simp [hB0]
  | cons J rest ih =>
    intro B hp hB
    rw [List.pairwise_cons] at hp
    obtain ⟨hJrest, hp'⟩ := hp
    rw [← Finset.sum_filter_add_sum_filter_not B (fun x : Fin n => x.val ∈ J.nodes) f]
    have h1 : B.filter (fun x : Fin n => x.val ∈ J.nodes) = finNodes n J := by
      ext x
      simp only [Finset.mem_filter, mem_finNodes]
      constructor
      · exact fun h => h.2
      · intro h
        exact ⟨(hB x).2 ⟨J, List.mem_cons_self, h⟩, h⟩
    have hrest : ∀ x : Fin n,
        x ∈ B.filter (fun x : Fin n => ¬ x.val ∈ J.nodes) ↔
          ∃ J' ∈ rest, x.val ∈ J'.nodes := by
      intro x
      simp only [Finset.mem_filter]
      constructor
      · rintro ⟨hxB, hxJ⟩
        obtain ⟨J', hJ', hx⟩ := (hB x).1 hxB
        rcases List.mem_cons.1 hJ' with h | h
        · subst h
          exact absurd hx hxJ
        · exact ⟨J', h, hx⟩
      · rintro ⟨J', hJ', hx⟩
        refine ⟨(hB x).2 ⟨J', List.mem_cons_of_mem _ hJ', hx⟩, ?_⟩
        intro hxJ
        exact hJrest J' hJ' x.val hxJ hx
    rw [h1, ih _ hp' hrest]
    simp [List.map_cons, List.sum_cons]

/-- Two members of a pairwise disjoint list sharing a node are equal. -/
theorem eq_of_share (gs : List Graph) :
    gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes) →
    ∀ J ∈ gs, ∀ J' ∈ gs, ∀ x, x ∈ J.nodes → x ∈ J'.nodes → J = J' := by
  induction gs with
  | nil => intro _ J hJ; simp at hJ
  | cons K rest ih =>
    intro hp J hJ J' hJ' x hx hx'
    rw [List.pairwise_cons] at hp
    obtain ⟨hK, hp'⟩ := hp
    rcases List.mem_cons.1 hJ with h1 | h1 <;> rcases List.mem_cons.1 hJ' with h2 | h2
    · rw [h1, h2]
    · subst h1
      exact absurd hx' (hK J' h2 x hx)
    · subst h2
      exact absurd hx (hK J h1 x hx')
    · exact ih hp' J h1 J' h2 x hx hx'

/-! ## Adjacency and components of the torso -/

/-- Torso adjacency at a node of a piece is adjacency in that piece. -/
theorem adj_iff_of_mem {T : SimpleGraph (Fin n)} (gs : List Graph)
    (hwf : ∀ J ∈ gs, J.WF)
    (hp : gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes))
    (hT : ∀ x y : Fin n, T.Adj x y ↔ ∃ J ∈ gs, J.Adj x.val y.val)
    {J : Graph} (hJ : J ∈ gs) {x : Fin n} (hx : x.val ∈ J.nodes) (w : Fin n) :
    T.Adj x w ↔ J.Adj x.val w.val := by
  rw [hT]
  constructor
  · rintro ⟨J', hJ', hadj⟩
    have hx' : x.val ∈ J'.nodes :=
      (hwf J' hJ').nbrs_sub w.val x.val ((hwf J' hJ').symm x.val w.val hadj)
    have he := eq_of_share gs hp J hJ J' hJ' x.val hx hx'
    subst he
    exact hadj
  · intro h
    exact ⟨J, hJ, h⟩

/-- Walks inside a piece stay in a closed set containing the start. -/
theorem walk_mem {T : SimpleGraph (Fin n)} {B : Finset (Fin n)} (J : Graph)
    (hwf : J.WF) (hlt : ∀ x ∈ J.nodes, x < n)
    (hBJ : ∀ y : Fin n, y.val ∈ J.nodes → y ∈ B)
    (hadj : ∀ x : Fin n, x.val ∈ J.nodes → ∀ y : Fin n, T.Adj x y ↔ J.Adj x.val y.val)
    (S : Finset (Fin n)) (hS : CubicPathwidth.ClosedIn T B S) (v : Fin n)
    (hvJ : v.val ∈ J.nodes) (hv : v ∈ S) (b : Nat)
    (hb : Relation.ReflTransGen J.Adj v.val b) :
    b ∈ J.nodes ∧ ∀ y : Fin n, y.val = b → y ∈ S := by
  induction hb with
  | refl =>
    refine ⟨hvJ, fun y hy => ?_⟩
    have : y = v := Fin.ext hy
    rw [this]
    exact hv
  | @tail c d _ hcd ih =>
    have hd : d ∈ J.nodes := hwf.nbrs_sub c d hcd
    refine ⟨hd, fun y hy => ?_⟩
    have hc : c < n := hlt c ih.1
    have hcS : (⟨c, hc⟩ : Fin n) ∈ S := ih.2 ⟨c, hc⟩ rfl
    have hyB : y ∈ B := hBJ y (by rw [hy]; exact hd)
    have hTadj : T.Adj ⟨c, hc⟩ y :=
      (hadj ⟨c, hc⟩ ih.1 y).2 (by show J.Adj c y.val; rw [hy]; exact hcd)
    exact hS _ hcS y hyB hTadj

/-- The torso component of a piece is its node set. -/
theorem component_eq_finNodes {T : SimpleGraph (Fin n)} (gs : List Graph) (B : Finset (Fin n))
    (hwf : ∀ J ∈ gs, J.WF)
    (hp : gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes))
    (hlt : ∀ J ∈ gs, ∀ v ∈ J.nodes, v < n)
    (hconn : ∀ J ∈ gs, ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y)
    (hB : ∀ x : Fin n, x ∈ B ↔ ∃ J ∈ gs, x.val ∈ J.nodes)
    (hT : ∀ x y : Fin n, T.Adj x y ↔ ∃ J ∈ gs, J.Adj x.val y.val)
    {J : Graph} (hJ : J ∈ gs) {v : Fin n} (hv : v.val ∈ J.nodes) :
    CubicPathwidth.component T B v = finNodes n J := by
  classical
  have hBJ : ∀ y : Fin n, y.val ∈ J.nodes → y ∈ B := fun y hy => (hB y).2 ⟨J, hJ, hy⟩
  have hadj : ∀ x : Fin n, x.val ∈ J.nodes → ∀ y : Fin n, T.Adj x y ↔ J.Adj x.val y.val :=
    fun x hx y => adj_iff_of_mem gs hwf hp hT hJ hx y
  have hvB : v ∈ B := hBJ v hv
  have hsub : finNodes n J ⊆ B := fun x hx => hBJ x (mem_finNodes.1 hx)
  have hcl : CubicPathwidth.ClosedIn T B (finNodes n J) := by
    intro a ha b _ hab
    have ha' := mem_finNodes.1 ha
    have hJb : b.val ∈ J.nodes := (hwf J hJ).nbrs_sub a.val b.val ((hadj a ha' b).1 hab)
    exact mem_finNodes.2 hJb
  apply Finset.Subset.antisymm
  · exact CubicPathwidth.component_min T hsub hcl (mem_finNodes.2 hv)
  · intro w hw
    have hwJ : w.val ∈ J.nodes := mem_finNodes.1 hw
    have hwB : w ∈ B := hBJ w hwJ
    refine Finset.mem_filter.2 ⟨hwB, hvB, fun S _ hS hvS => ?_⟩
    have hrtg : Relation.ReflTransGen J.Adj v.val w.val := hconn J hJ v.val hv w.val hwJ
    exact (walk_mem J (hwf J hJ) (hlt J hJ) hBJ hadj S hS v hv hvS w.val hrtg).2 w rfl

/-- The torso components are exactly the node sets of the pieces. -/
theorem mem_tcomps_iff {T : SimpleGraph (Fin n)} (gs : List Graph) (B : Finset (Fin n))
    (hwf : ∀ J ∈ gs, J.WF)
    (hp : gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes))
    (hlt : ∀ J ∈ gs, ∀ v ∈ J.nodes, v < n)
    (hne : ∀ J ∈ gs, J.nodes ≠ [])
    (hconn : ∀ J ∈ gs, ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y)
    (hB : ∀ x : Fin n, x ∈ B ↔ ∃ J ∈ gs, x.val ∈ J.nodes)
    (hT : ∀ x y : Fin n, T.Adj x y ↔ ∃ J ∈ gs, J.Adj x.val y.val)
    (C : Finset (Fin n)) :
    C ∈ CubicPathwidth.components T B ↔ ∃ J ∈ gs, finNodes n J = C := by
  constructor
  · intro hC
    obtain ⟨v, hvB, rfl⟩ := Finset.mem_image.mp hC
    obtain ⟨J, hJ, hvJ⟩ := (hB v).1 hvB
    exact ⟨J, hJ, (component_eq_finNodes (T := T) gs B hwf hp hlt hconn hB hT hJ hvJ).symm⟩
  · rintro ⟨J, hJ, rfl⟩
    obtain ⟨a, ha⟩ := List.exists_mem_of_ne_nil _ (hne J hJ)
    have hv : (⟨a, hlt J hJ a ha⟩ : Fin n) ∈ B := (hB _).2 ⟨J, hJ, ha⟩
    refine Finset.mem_image.mpr ⟨⟨a, hlt J hJ a ha⟩, hv, ?_⟩
    exact component_eq_finNodes (T := T) gs B hwf hp hlt hconn hB hT hJ ha

/-! ## Degrees -/

open scoped Classical in

theorem tdeg_card (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (x : Fin n) :
    T4.tdeg G F B x =
      ((Finset.univ : Finset (Fin n)).filter fun w => (T4.tgraph G F B).Adj x w).card := by
  unfold T4.tdeg
  rw [← SimpleGraph.card_neighborFinset_eq_degree, SimpleGraph.neighborFinset_eq_filter]

theorem tdeg_eq_degree_of {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (J : Graph)
    (hwf : J.WF) (hlt : ∀ v ∈ J.nodes, v < n) (x : Fin n)
    (hadj : ∀ w : Fin n, (T4.tgraph G F B).Adj x w ↔ J.Adj x.val w.val) :
    T4.tdeg G F B x = J.degree x.val := by
  classical
  have hL : ∀ a ∈ J.nbrs x.val, a < n := fun a ha => hlt a (hwf.nbrs_sub x.val a ha)
  have h := card_filter_val (n := n) (J.nbrs x.val) hL (hwf.nbrs_nodup x.val)
  have hf : (Finset.univ : Finset (Fin n)).filter (fun w => (T4.tgraph G F B).Adj x w) =
      (Finset.univ : Finset (Fin n)).filter (fun w => w.val ∈ J.nbrs x.val) := by
    ext w
    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
    exact hadj w
  rw [tdeg_card, hf]
  exact h

/-- The minimum torso degree of a torso component which is a piece. -/
theorem cmin_finNodes {S : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (J : Graph)
    (hlt : ∀ v ∈ J.nodes, v < n) (hne : J.nodes ≠ [])
    (hdeg : ∀ x : Fin n, x.val ∈ J.nodes → T4.tdeg S F B x = J.degree x.val) :
    T4.cmin S F B (finNodes n J) = minDegree J := by
  obtain ⟨a, ha⟩ := List.exists_mem_of_ne_nil _ hne
  have hnon : (finNodes n J).Nonempty := ⟨⟨a, hlt a ha⟩, mem_finNodes.2 ha⟩
  unfold T4.cmin
  simp only [hnon, dite_true]
  have hc : ∃ m, (J.nodes.map J.degree).min? = some m := by
    cases h : (J.nodes.map J.degree).min? with
    | none =>
      simp at h
      exact absurd h hne
    | some m => exact ⟨m, rfl⟩
  obtain ⟨m, hm⟩ := hc
  have hmd : minDegree J = m := by simp [minDegree, hm]
  rw [hmd]
  obtain ⟨hmem, hle⟩ := List.min?_eq_some_iff.1 hm
  obtain ⟨v0, hv0, hv0eq⟩ := List.mem_map.1 hmem
  apply le_antisymm
  · calc (finNodes n J).inf' hnon (T4.tdeg S F B)
        ≤ T4.tdeg S F B ⟨v0, hlt v0 hv0⟩ :=
          Finset.inf'_le _ ((mem_finNodes (x := ⟨v0, hlt v0 hv0⟩)).2 hv0)
      _ = J.degree v0 := hdeg _ hv0
      _ = m := hv0eq
  · apply Finset.le_inf'
    intro x hx
    rw [hdeg x (mem_finNodes.1 hx)]
    exact hle _ (List.mem_map.2 ⟨x.val, mem_finNodes.1 hx, rfl⟩)

theorem sum_map_sub' {α : Type*} (gs : List α) (f g : α → ℝ) :
    (gs.map fun x => f x - g x).sum = (gs.map f).sum - (gs.map g).sum := by
  induction gs with
  | nil => simp
  | cons a t ih =>
    simp only [List.map_cons, List.sum_cons, ih]
    ring

theorem nodup_map_finNodes (gs : List Graph)
    (hp : gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes))
    (hlt : ∀ J ∈ gs, ∀ v ∈ J.nodes, v < n) (hne : ∀ J ∈ gs, J.nodes ≠ []) :
    (gs.map (finNodes n)).Nodup := by
  rw [List.Nodup, List.pairwise_map]
  refine List.Pairwise.imp_of_mem ?_ hp
  intro a b ha _ hR heq
  obtain ⟨m, hm⟩ := List.exists_mem_of_ne_nil _ (hne a ha)
  have hx : (⟨m, hlt a ha m hm⟩ : Fin n) ∈ finNodes n a := mem_finNodes.2 hm
  rw [heq] at hx
  exact hR m hm (mem_finNodes.1 hx)

/-- Sums over the torso components are sums over the pieces. -/
theorem sum_components_eq {T : SimpleGraph (Fin n)} (gs : List Graph) (B : Finset (Fin n))
    (hwf : ∀ J ∈ gs, J.WF)
    (hp : gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes))
    (hlt : ∀ J ∈ gs, ∀ v ∈ J.nodes, v < n)
    (hne : ∀ J ∈ gs, J.nodes ≠ [])
    (hconn : ∀ J ∈ gs, ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y)
    (hB : ∀ x : Fin n, x ∈ B ↔ ∃ J ∈ gs, x.val ∈ J.nodes)
    (hT : ∀ x y : Fin n, T.Adj x y ↔ ∃ J ∈ gs, J.Adj x.val y.val)
    (h : Finset (Fin n) → ℝ) :
    ∑ C ∈ CubicPathwidth.components T B, h C =
      (gs.map fun J => h (finNodes n J)).sum := by
  classical
  have hset : CubicPathwidth.components T B = (gs.map (finNodes n)).toFinset := by
    ext C
    rw [mem_tcomps_iff gs B hwf hp hlt hne hconn hB hT C, List.mem_toFinset, List.mem_map]
  rw [hset, List.sum_toFinset h (nodup_map_finNodes gs hp hlt hne), List.map_map]
  rfl

/-- The potential bridge (`TorsoPotentialBridge`). -/
theorem torsoPotentialBridge : TorsoPotentialBridge := by
  intro n S F B gs hpc hp hlt hB hT
  have hwf : ∀ J ∈ gs, J.WF := fun J hJ => (hpc J hJ).1
  have hne : ∀ J ∈ gs, J.nodes ≠ [] := fun J hJ => (hpc J hJ).2.1
  have hconn : ∀ J ∈ gs, ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y :=
    fun J hJ => (hpc J hJ).2.2
  have hdeg : ∀ J ∈ gs, ∀ x : Fin n, x.val ∈ J.nodes → T4.tdeg S F B x = J.degree x.val := by
    intro J hJ x hx
    exact tdeg_eq_degree_of J (hwf J hJ) (hlt J hJ) x
      (fun w => adj_iff_of_mem gs hwf hp hT hJ hx w)
  have hcomp : ∀ J ∈ gs, finNodes n J ∈ T4.tcomps S F B := by
    intro J hJ
    exact (mem_tcomps_iff gs B hwf hp hlt hne hconn hB hT _).2 ⟨J, hJ, rfl⟩
  have hpsi : ∀ b : ℕ → ℝ, T4.psi b S F B = (gs.map (psiPort b)).sum := by
    intro b
    have hs := sum_split (n := n) (fun x => b (T4.tdeg S F B x)) gs B hp hB
    unfold T4.psi
    rw [hs]
    congr 1
    apply List.map_congr_left
    intro J hJ
    show ∑ x ∈ finNodes n J, b (T4.tdeg S F B x) = psiPort b J
    unfold psiPort
    calc ∑ x ∈ finNodes n J, b (T4.tdeg S F B x)
        = ∑ x ∈ finNodes n J, b (J.degree x.val) :=
          Finset.sum_congr rfl (fun x hx => by rw [hdeg J hJ x (mem_finNodes.1 hx)])
      _ = (J.nodes.map fun v => b (J.degree v)).sum :=
          sum_finNodes J (hwf J hJ).nodup (hlt J hJ) (fun v => b (J.degree v))
  have hpm : ∀ b : ℕ → ℝ, T4.psiMinus b S F B = (gs.map (psiMinusPort b)).sum := by
    intro b
    have hmap : (gs.map fun J => T4.runMin b (T4.cmin S F B (finNodes n J))) =
        gs.map fun J => T4.runMin b (minDegree J) := by
      apply List.map_congr_left
      intro J hJ
      rw [cmin_finNodes J (hlt J hJ) (hne J hJ) (hdeg J hJ)]
    have hcs : ∑ C ∈ T4.tcomps S F B, T4.runMin b (T4.cmin S F B C) =
        (gs.map fun J => T4.runMin b (T4.cmin S F B (finNodes n J))).sum :=
      sum_components_eq gs B hwf hp hlt hne hconn hB hT (fun C => T4.runMin b (T4.cmin S F B C))
    unfold T4.psiMinus
    rw [hpsi b, hcs, hmap, ← sum_map_sub' gs (psiPort b) (fun J => T4.runMin b (minDegree J))]
    rfl
  refine ⟨fun J hJ x hx => hdeg J hJ x hx, hcomp, ?_, fun b => ⟨hpsi b, hpm b⟩⟩
  intro C hC
  obtain ⟨J, hJ, h⟩ := (mem_tcomps_iff gs B hwf hp hlt hne hconn hB hT C).1 hC
  exact ⟨J, hJ, h.symm⟩

/-- The potential facts for pieces of minimum degree at least `3`. -/
theorem psiPortFacts : PsiPortFacts := by
  intro b hb J hwf hne hdeg
  have hc : ∃ m, (J.nodes.map J.degree).min? = some m := by
    cases h : (J.nodes.map J.degree).min? with
    | none =>
      simp at h
      exact absurd h hne
    | some m => exact ⟨m, rfl⟩
  obtain ⟨m, hm⟩ := hc
  have hmd : minDegree J = m := by simp [minDegree, hm]
  obtain ⟨hmem, _⟩ := List.min?_eq_some_iff.1 hm
  obtain ⟨v0, hv0, hv0eq⟩ := List.mem_map.1 hmem
  have h3 : 3 ≤ minDegree J := by
    rw [hmd, ← hv0eq]
    exact hdeg v0 hv0
  have hsum : b (minDegree J) ≤ psiPort b J := by
    unfold psiPort
    have hnn : ∀ x ∈ J.nodes.map (fun v => b (J.degree v)), 0 ≤ x := by
      intro x hx
      obtain ⟨v, _, rfl⟩ := List.mem_map.1 hx
      exact hb.nonneg _
    have hterm := List.single_le_sum hnn (b (J.degree v0)) (List.mem_map.2 ⟨v0, hv0, rfl⟩)
    have e : J.degree v0 = minDegree J := hv0eq.trans hmd.symm
    rw [e] at hterm
    exact hterm
  have hR1 := CubicPathwidth.T4.BasicAux.runMin_le_self hb h3
  have hR2 := CubicPathwidth.T4.BasicAux.runMin_le_incr_three b (minDegree J)
  have hI := CubicPathwidth.T4.BasicAux.incr_three hb
  unfold psiMinusPort
  constructor
  · linarith
  · linarith

end D3

/-- (D3) Torso potential bridge: torso degrees, torso components and `ψ`, `ψ⁻` of a torso
state whose torso is a disjoint union of connected pieces. -/
theorem torsoPotentialBridge : TorsoPotentialBridge := D3.torsoPotentialBridge

/-- (D3) Port form of the potential facts for pieces of minimum degree at least `3`. -/
theorem psiPortFacts : PsiPortFacts := D3.psiPortFacts

end CubicPathwidth.Alg

end

#print axioms CubicPathwidth.Alg.torsoPotentialBridge
#print axioms CubicPathwidth.Alg.psiPortFacts