CubicPathwidth.Alg.Proofs2.X4LabelTransfer

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.C3.Intervals

/-!
# Stage 2 task X4: `LabelTransfer`

Rank labels. For a real injective labeling `y` of `Fin m`, and a relabelling `e` of a
well-formed graph `G` onto `Fin m`, put `Y (e i) := 2·rank y i - (2ℓ - 1)` with
`ℓ = #{j | y j ≤ 0}`. These are odd integers, nonzero, with the same order as `y` and
with `Y < 0 ↔ y ≤ 0`. Every rational level set `{Y ≤ t}` is a level set `{y ≤ s}`
(`thr`), and the sign conditions on `s` follow from the sign conditions on `t`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace X4

open scoped Classical

/-! ## Threshold separation for a downward closed family -/

theorem thr {m : ℕ} (y : Fin m → ℝ) (Pr : Fin m → Prop) [DecidablePred Pr] (t : ℝ)
    (hdown : ∀ i j, y i ≤ y j → Pr j → Pr i)
    (hpos : 0 < t → ∀ i, ¬ Pr i → 0 < y i)
    (hneg : t < 0 → ∀ i, Pr i → y i ≤ 0) :
    ∃ s : ℝ, (∀ i, Pr i ↔ y i ≤ s) ∧ (0 < t → 0 < s) ∧ (t < 0 → s ≤ 0) := by
  have hA : ∃ s0 : ℝ, (∀ i, Pr i → y i ≤ s0) ∧ (∀ j, ¬ Pr j → s0 < y j) := by
    by_cases hQ : ∃ j, ¬ Pr j
    · obtain ⟨j1, hj1⟩ := hQ
      obtain ⟨j2, hj2, hmin⟩ := Finset.exists_min_image
        (Finset.univ.filter fun j => ¬ Pr j) y ⟨j1, by simp [hj1]⟩
      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hj2 hmin
      have hPlow : ∀ i, Pr i → y i < y j2 := by
        intro i hi
        by_contra h
        push_neg at h
        exact hj2 (hdown j2 i h hi)
      by_cases hP : ∃ i, Pr i
      · obtain ⟨i0, hi0⟩ := hP
        obtain ⟨i1, hi1, hmax⟩ := Finset.exists_max_image
          (Finset.univ.filter fun i => Pr i) y ⟨i0, by simp [hi0]⟩
        simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi1 hmax
        refine ⟨(y i1 + y j2) / 2, fun i hi => ?_, fun j hj => ?_⟩
        · have h1 := hmax i hi
          have h2 := hPlow i1 hi1
          linarith
        · have h1 := hmin j hj
          have h2 := hPlow i1 hi1
          linarith
      · push_neg at hP
        refine ⟨y j2 - 1, fun i hi => absurd hi (hP i), fun j hj => ?_⟩
        have := hmin j hj
        linarith
    · push_neg at hQ
      refine ⟨∑ k, |y k|, fun i _ => ?_, fun j hj => absurd (hQ j) hj⟩
      have h1 : |y i| ≤ ∑ k, |y k| :=
        Finset.single_le_sum (f := fun k => |y k|) (fun k _ => abs_nonneg _) (Finset.mem_univ i)
      linarith [le_abs_self (y i)]
  obtain ⟨s0, hA1, hA2⟩ := hA
  have hlev : ∀ s : ℝ, (∀ i, Pr i → y i ≤ s) → (∀ j, ¬ Pr j → s < y j) →
      ∀ i, Pr i ↔ y i ≤ s := by
    intro s h1 h2 i
    constructor
    · exact h1 i
    · intro hi
      by_contra hn
      exact not_le.mpr (h2 i hn) hi
  rcases lt_trichotomy t 0 with ht | ht | ht
  · refine ⟨min s0 0, hlev _ (fun i hi => le_min (hA1 i hi) (hneg ht i hi))
      (fun j hj => lt_of_le_of_lt (min_le_left _ _) (hA2 j hj)), fun h => (lt_asymm ht h).elim,
      fun _ => min_le_right _ _⟩
  · refine ⟨s0, hlev s0 hA1 hA2, fun h => by linarith, fun h => by linarith⟩
  · have hpos' := hpos ht
    by_cases hs0 : 0 < s0
    · exact ⟨s0, hlev s0 hA1 hA2, fun _ => hs0, fun h => (lt_asymm ht h).elim⟩
    · push_neg at hs0
      by_cases hQ : ∃ j, ¬ Pr j
      · obtain ⟨j1, hj1⟩ := hQ
        obtain ⟨j2, hj2, hmin⟩ := Finset.exists_min_image
          (Finset.univ.filter fun j => ¬ Pr j) y ⟨j1, by simp [hj1]⟩
        simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hj2 hmin
        have hc : 0 < y j2 := hpos' j2 hj2
        refine ⟨y j2 / 2, hlev _ (fun i hi => ?_) (fun j hj => ?_), fun _ => by linarith,
          fun h => (lt_asymm ht h).elim⟩
        · linarith [hA1 i hi]
        · linarith [hmin j hj]
      · push_neg at hQ
        refine ⟨1, fun i => ⟨fun _ => ?_, fun _ => hQ i⟩, fun _ => one_pos,
          fun h => (lt_asymm ht h).elim⟩
        linarith [hA1 i (hQ i)]

/-! ## Rank labels -/

variable {m : ℕ}

/-- `ℓ = #{j | y j ≤ 0}` (written out in the lemmas that need it). -/
def fl (y : Fin m → ℝ) (i : Fin m) : ℚ :=
  2 * ((C3.rank y i : ℕ) : ℚ) - (2 * (((Finset.univ.filter fun u => y u ≤ 0).card : ℕ) : ℚ) - 1)

/-- The rank labeling, transported along `e`; off the image of `e` it is `0`. -/
def lab (e : Fin m → Nat) (y : Fin m → ℝ) : Labels :=
  fun v => ∑ i, if e i = v then fl y i else 0

theorem lab_e {e : Fin m → Nat} (he : Function.Injective e) (y : Fin m → ℝ) (i : Fin m) :
    lab e y (e i) = fl y i := by
  simp only [lab]
  rw [Finset.sum_eq_single i]
  · simp
  · intro j _ hj
    rw [if_neg (fun h => hj (he h))]
  · intro h
    exact absurd (Finset.mem_univ i) h

theorem fl_neg_iff (y : Fin m → ℝ) (i : Fin m) : fl y i < 0 ↔ y i ≤ 0 := by
  have key : fl y i < 0 ↔
      ((2 * C3.rank y i + 1 : ℕ) : ℚ) < ((2 * (Finset.univ.filter fun u => y u ≤ 0).card : ℕ) : ℚ) := by
    unfold fl
    push_cast
    constructor <;> intro h <;> linarith
  have h2 := C3.rank_lt_lowerCount_iff y i
  rw [key, Nat.cast_lt, ← h2]
  omega

theorem fl_ne_zero (y : Fin m → ℝ) (i : Fin m) : fl y i ≠ 0 := by
  intro h
  have key : ((2 * C3.rank y i + 1 : ℕ) : ℚ) = ((2 * (Finset.univ.filter fun u => y u ≤ 0).card : ℕ) : ℚ) := by
    unfold fl at h
    push_cast
    linarith
  have key2 := Nat.cast_injective key
  omega

theorem fl_mono {y : Fin m → ℝ} (hy : Function.Injective y) {i j : Fin m} (h : y i ≤ y j) :
    fl y i ≤ fl y j := by
  have h1 : C3.rank y i ≤ C3.rank y j := (C3.rank_le_iff hy).mpr h
  have h2 : ((C3.rank y i : ℕ) : ℚ) ≤ ((C3.rank y j : ℕ) : ℚ) := by exact_mod_cast h1
  unfold fl
  linarith

theorem fl_inj {y : Fin m → ℝ} (hy : Function.Injective y) {i j : Fin m}
    (h : fl y i = fl y j) : i = j := by
  have h1 : C3.rank y i = C3.rank y j := by
    unfold fl at h
    have : ((C3.rank y i : ℕ) : ℚ) = ((C3.rank y j : ℕ) : ℚ) := by linarith
    exact_mod_cast this
  exact C3.rank_injective hy h1

/-! ## Transport along a relabelling -/

theorem card_filter_eq {e : Fin m → Nat} (he : Function.Injective e) (L : List Nat)
    (hL : L.Nodup) (hsub : ∀ v ∈ L, ∃ i, e i = v) (p : Nat → Bool) :
    (L.filter p).length =
      (Finset.univ.filter fun i => e i ∈ L ∧ p (e i) = true).card := by
  rw [← List.toFinset_card_of_nodup (hL.filter p), ← Finset.card_image_of_injective _ he]
  congr 1
  ext x
  simp only [List.mem_toFinset, List.mem_filter, Finset.mem_image, Finset.mem_filter,
    Finset.mem_univ, true_and]
  constructor
  · rintro ⟨hx, hp⟩
    obtain ⟨i, rfl⟩ := hsub x hx
    exact ⟨i, ⟨hx, hp⟩, rfl⟩
  · rintro ⟨i, ⟨hx, hp⟩, rfl⟩
    exact ⟨hx, hp⟩

theorem mem_nbrs_iff {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (i : Fin m) (x : Nat) :
    x ∈ G.nbrs (e i) ↔ ∃ j, e j = x ∧ S.Adj i j := by
  constructor
  · intro hx
    obtain ⟨j, hj⟩ := (hrel.2.1 x).mp (hG.nbrs_sub _ _ hx)
    refine ⟨j, hj, (hrel.2.2 i j).mpr ?_⟩
    show e j ∈ G.nbrs (e i)
    rw [hj]
    exact hx
  · rintro ⟨j, rfl, hj⟩
    exact (hrel.2.2 i j).mp hj

theorem nodes_filter_length {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (p : Nat → Bool) :
    (G.nodes.filter p).length = (Finset.univ.filter fun i => p (e i) = true).card := by
  rw [card_filter_eq hrel.1 G.nodes hG.nodup (fun v hv => (hrel.2.1 v).mp hv) p]
  congr 1
  apply Finset.filter_congr
  intro i _
  exact ⟨fun h => h.2, fun h => ⟨(hrel.2.1 (e i)).mpr ⟨i, rfl⟩, h⟩⟩

theorem nbrs_any_iff {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (i : Fin m) (P : Nat → Bool) :
    (G.nbrs (e i)).any P = true ↔ ∃ j, S.Adj i j ∧ P (e j) = true := by
  rw [List.any_eq_true]
  constructor
  · rintro ⟨x, hx, hp⟩
    obtain ⟨j, rfl, hj⟩ := (mem_nbrs_iff hG hrel i x).mp hx
    exact ⟨j, hj, hp⟩
  · rintro ⟨j, hj, hp⟩
    exact ⟨e j, (mem_nbrs_iff hG hrel i (e j)).mpr ⟨j, rfl, hj⟩, hp⟩

theorem nbrs_all_iff {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (i : Fin m) (P : Nat → Bool) :
    (G.nbrs (e i)).all P = true ↔ ∀ j, S.Adj i j → P (e j) = true := by
  rw [List.all_eq_true]
  constructor
  · intro h j hj
    exact h _ ((mem_nbrs_iff hG hrel i (e j)).mpr ⟨j, rfl, hj⟩)
  · intro h x hx
    obtain ⟨j, rfl, hj⟩ := (mem_nbrs_iff hG hrel i x).mp hx
    exact h j hj

theorem nbrs_length {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (i : Fin m) [Fintype (S.neighborSet i)] (hG : G.WF) (hrel : IsRelabel G S e) :
    G.degree (e i) = S.degree i := by
  unfold Graph.degree
  rw [← SimpleGraph.card_neighborFinset_eq_degree]
  have h := card_filter_eq hrel.1 (G.nbrs (e i)) (hG.nbrs_nodup _)
    (fun v hv => (hrel.2.1 v).mp (hG.nbrs_sub _ _ hv)) (fun _ => true)
  simp only [List.filter_true, and_true] at h
  rw [h]
  congr 1
  ext j
  simp only [Finset.mem_filter, Finset.mem_univ, true_and, SimpleGraph.mem_neighborFinset]
  exact (hrel.2.2 i j).symm

/-! ## The labeling: order, signs, nonvanishing -/

theorem lab_inj {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hrel : IsRelabel G S e) (y : Fin m → ℝ) (hy : Function.Injective y) :
    LabelsInjOn G (lab e y) := by
  intro u hu v hv huv
  obtain ⟨i, rfl⟩ := (hrel.2.1 u).mp hu
  obtain ⟨j, rfl⟩ := (hrel.2.1 v).mp hv
  rw [lab_e hrel.1, lab_e hrel.1] at huv
  rw [fl_inj hy huv]

theorem lab_ne {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hrel : IsRelabel G S e) (y : Fin m → ℝ) :
    ∀ v ∈ G.nodes, lab e y v ≠ 0 := by
  intro v hv
  obtain ⟨i, rfl⟩ := (hrel.2.1 v).mp hv
  rw [lab_e hrel.1]
  exact fl_ne_zero y i

/-- Level sets of `lab` at rational thresholds are level sets of `y`, with the sign
conditions of `LabelTransfer`. -/
theorem levels {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hrel : IsRelabel G S e) (y : Fin m → ℝ) (hy : Function.Injective y) (t : ℚ) :
    ∃ s : ℝ, (∀ i, lab e y (e i) ≤ t ↔ y i ≤ s) ∧ (0 < t → 0 < s) ∧ (t < 0 → s ≤ 0) := by
  obtain ⟨s, h1, h2, h3⟩ := thr y (fun i => lab e y (e i) ≤ t) (t : ℝ)
    (fun (i j : Fin m) (hij : y i ≤ y j) (hj : lab e y (e j) ≤ t) => by
      rw [lab_e hrel.1] at hj ⊢
      exact le_trans (fl_mono hy hij) hj)
    (fun (ht : (0 : ℝ) < t) (i : Fin m) (hi : ¬ lab e y (e i) ≤ t) => by
      rw [lab_e hrel.1] at hi
      have ht' : (0 : ℚ) < t := by exact_mod_cast ht
      have h0 : 0 < fl y i := lt_of_lt_of_le ht' (le_of_lt (not_le.mp hi))
      by_contra hcon
      exact absurd ((fl_neg_iff y i).mpr (not_lt.mp hcon)) (not_lt.mpr h0.le))
    (fun (ht : (t : ℝ) < 0) (i : Fin m) (hi : lab e y (e i) ≤ t) => by
      rw [lab_e hrel.1] at hi
      have ht' : t < 0 := by exact_mod_cast ht
      exact (fl_neg_iff y i).mp (lt_of_le_of_lt hi ht'))
  exact ⟨s, h1, fun h => h2 (by exact_mod_cast h), fun h => h3 (by exact_mod_cast h)⟩

theorem lt_iff_of_levels {e : Fin m → Nat} {y : Fin m → ℝ} {t : ℚ} {s : ℝ}
    (h1 : ∀ i, lab e y (e i) ≤ t ↔ y i ≤ s) (i : Fin m) :
    t < lab e y (e i) ↔ s < y i := by
  rw [← not_le, ← not_le]
  exact not_congr (h1 i)

/-! ## Frontiers -/

theorem mem_outerFrontier {S : SimpleGraph (Fin m)} (y : Fin m → ℝ) (s : ℝ) (i : Fin m) :
    i ∈ C3.outerFrontier S y s ↔ s < y i ∧ ∃ u, S.Adj u i ∧ y u ≤ s := by
  unfold C3.outerFrontier
  simp

theorem mem_innerFrontier {S : SimpleGraph (Fin m)} (y : Fin m → ℝ) (s : ℝ) (i : Fin m) :
    i ∈ C3.innerFrontier S y s ↔ y i ≤ s ∧ ∃ w, S.Adj i w ∧ s < y w := by
  unfold C3.innerFrontier
  simp

theorem mem_crossFull {S : SimpleGraph (Fin m)} (y : Fin m → ℝ) (i : Fin m) :
    i ∈ C3.crossFull S y ↔ S.degree i = 3 ∧ ∀ z, S.Adj i z → (y i ≤ 0 ↔ 0 < y z) := by
  unfold C3.crossFull
  simp

theorem outer_pred {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) (t : ℚ) (s : ℝ)
    (h1 : ∀ i, lab e y (e i) ≤ t ↔ y i ≤ s) (i : Fin m) :
    (decide (t < lab e y (e i)) && (G.nbrs (e i)).any fun u => decide (lab e y u ≤ t)) = true ↔
      (s < y i ∧ ∃ j, S.Adj i j ∧ y j ≤ s) := by
  rw [Bool.and_eq_true, decide_eq_true_eq, nbrs_any_iff hG hrel i (fun u => decide (lab e y u ≤ t))]
  simp only [decide_eq_true_eq]
  rw [lt_iff_of_levels h1 i]
  constructor
  · rintro ⟨h2, j, hj, h3⟩
    exact ⟨h2, j, hj, (h1 j).mp h3⟩
  · rintro ⟨h2, j, hj, h3⟩
    exact ⟨h2, j, hj, (h1 j).mpr h3⟩

theorem inner_pred {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) (t : ℚ) (s : ℝ)
    (h1 : ∀ i, lab e y (e i) ≤ t ↔ y i ≤ s) (i : Fin m) :
    (decide (lab e y (e i) ≤ t) && (G.nbrs (e i)).any fun w => decide (t < lab e y w)) = true ↔
      (y i ≤ s ∧ ∃ j, S.Adj i j ∧ s < y j) := by
  rw [Bool.and_eq_true, decide_eq_true_eq, nbrs_any_iff hG hrel i (fun w => decide (t < lab e y w))]
  simp only [decide_eq_true_eq]
  constructor
  · rintro ⟨h2, j, hj, h3⟩
    exact ⟨(h1 i).mp h2, j, hj, (lt_iff_of_levels h1 j).mp h3⟩
  · rintro ⟨h2, j, hj, h3⟩
    exact ⟨(h1 i).mpr h2, j, hj, (lt_iff_of_levels h1 j).mpr h3⟩

theorem outer_card {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) (t : ℚ) (s : ℝ)
    (h1 : ∀ i, lab e y (e i) ≤ t ↔ y i ≤ s) :
    (outerFr G (lab e y) t).length = (C3.outerFrontier S y s).card := by
  unfold outerFr
  rw [nodes_filter_length hG hrel]
  congr 1
  ext i
  rw [mem_outerFrontier, Finset.mem_filter, outer_pred hG hrel y t s h1 i]
  simp only [Finset.mem_univ, true_and]
  constructor
  · rintro ⟨h2, j, hj, h3⟩
    exact ⟨h2, j, hj.symm, h3⟩
  · rintro ⟨h2, j, hj, h3⟩
    exact ⟨h2, j, hj.symm, h3⟩

theorem inner_card {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) (t : ℚ) (s : ℝ)
    (h1 : ∀ i, lab e y (e i) ≤ t ↔ y i ≤ s) :
    (innerFr G (lab e y) t).length = (C3.innerFrontier S y s).card := by
  unfold innerFr
  rw [nodes_filter_length hG hrel]
  congr 1
  ext i
  rw [mem_innerFrontier, Finset.mem_filter, inner_pred hG hrel y t s h1 i]
  simp only [Finset.mem_univ, true_and]

/-! ## Level-zero counts -/

theorem isLow_eq {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat} (hrel : IsRelabel G S e) (y : Fin m → ℝ) (i : Fin m) :
    isLow (lab e y) (e i) = decide (y i ≤ 0) := by
  simp only [isLow, lab_e hrel.1, fl_neg_iff]

theorem inU_iff {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) (i : Fin m) :
    inU G (lab e y) (e i) = true ↔ (y i ≤ 0 ∧ ∃ j, S.Adj i j ∧ 0 < y j) := by
  rw [inU, Bool.and_eq_true, nbrs_any_iff hG hrel i (fun x => !isLow (lab e y) x)]
  simp only [isLow_eq hrel, Bool.not_eq_true', decide_eq_true_eq, decide_eq_false_iff_not, not_le]

theorem inW_iff {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) (i : Fin m) :
    inW G (lab e y) (e i) = true ↔ (0 < y i ∧ ∃ j, S.Adj i j ∧ y j ≤ 0) := by
  rw [inW, Bool.and_eq_true, nbrs_any_iff hG hrel i (fun u => isLow (lab e y) u)]
  simp only [isLow_eq hrel, Bool.not_eq_true', decide_eq_true_eq, decide_eq_false_iff_not, not_le]

theorem inD_iff {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) (i : Fin m) :
    inD G (lab e y) (e i) = true ↔
      (S.degree i = 3 ∧ ∀ z, S.Adj i z → (y i ≤ 0 ↔ 0 < y z)) := by
  rw [inD, Bool.and_eq_true, beq_iff_eq, nbrs_length i hG hrel, nbrs_all_iff hG hrel i]
  apply and_congr Iff.rfl
  apply forall_congr'
  intro j
  apply imp_congr_right
  intro _
  rw [isLow_eq hrel, isLow_eq hrel]
  simp only [← not_le]
  by_cases hj : y j ≤ 0 <;> by_cases hi : y i ≤ 0 <;> simp [hj, hi]

theorem lower_eq {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) :
    lowerZeroP G (lab e y) = C3.lowerZero S y := by
  unfold lowerZeroP C3.lowerZero
  rw [nodes_filter_length hG hrel, nodes_filter_length hG hrel]
  congr 1
  · congr 1
    ext i
    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
    rw [mem_innerFrontier]
    exact inU_iff hG hrel y i
  · congr 1
    ext i
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Bool.and_eq_true]
    rw [inD_iff hG hrel y i, inW_iff hG hrel y i, mem_crossFull]
    constructor
    · rintro ⟨⟨hd, hz⟩, hp, _⟩
      exact ⟨⟨hd, hz⟩, hp⟩
    · rintro ⟨⟨hd, hz⟩, hp⟩
      have hdpos : 0 < S.degree i := by rw [hd]; norm_num
      obtain ⟨j, hj⟩ := (S.degree_pos_iff_exists_adj i).mp hdpos
      have hj0 : y j ≤ 0 := not_lt.mp (fun h => absurd ((hz j hj).mpr h) (not_le.mpr hp))
      exact ⟨⟨hd, hz⟩, hp, j, hj, hj0⟩

theorem upper_eq {G : Graph} {S : SimpleGraph (Fin m)} {e : Fin m → Nat}
    (hG : G.WF) (hrel : IsRelabel G S e) (y : Fin m → ℝ) :
    upperZeroP G (lab e y) = C3.upperZero S y := by
  unfold upperZeroP C3.upperZero
  rw [nodes_filter_length hG hrel, nodes_filter_length hG hrel]
  congr 1
  · congr 1
    ext i
    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
    rw [inW_iff hG hrel y i, mem_outerFrontier]
    constructor
    · rintro ⟨h1, j, hj, h2⟩
      exact ⟨h1, j, hj.symm, h2⟩
    · rintro ⟨h1, j, hj, h2⟩
      exact ⟨h1, j, hj.symm, h2⟩
  · congr 1
    ext i
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Bool.and_eq_true]
    rw [inD_iff hG hrel y i, mem_crossFull, isLow_eq hrel, decide_eq_true_eq]

end X4

theorem labelTransfer : LabelTransfer := by
  intro G m S e hG hrel y hy
  refine ⟨X4.lab e y, X4.lab_inj hrel y hy, X4.lab_ne hrel y, ?_, ?_, ?_⟩
  · intro t
    obtain ⟨s, h1, h2, _⟩ := X4.levels hrel y hy t
    exact ⟨s, h2, X4.outer_card hG hrel y t s h1⟩
  · intro t ht
    obtain ⟨s, h1, _, h3⟩ := X4.levels hrel y hy t
    exact ⟨s, h3 ht, X4.inner_card hG hrel y t s h1⟩
  · exact ⟨X4.lower_eq hG hrel y, X4.upper_eq hG hrel y⟩

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.labelTransfer