CubicPathwidth.T2.DegreeLabelsCut

Source file CubicPathwidth/T2/DegreeLabelsCut.lean of the Lean project (how it is built).

import CubicPathwidth.T2.DegreeLabels

/-!
# Mixed labels with the paper's cut argument

`degreeLabels_cut : DegreeLabelsClaim`, a second proof of `degreeLabels` whose shell
estimate follows the proof of the mixed correlation lemma in
the paper (Steps 1-4), instead of packing disjoint cuts
(`DegreeLabelsShell.shell_le`, `pack`).

Dictionary. `ν = amp² = e^{-2D}`, so `D(w) = Dd ν w = -½ ln ν w`; the arc lengths are
`ℓ(x → y) = -½ ln c x ∈ [ℓ_min, ℓ_max] = [½ ln 2, ½ ln 3]` (`lmin`, `lmax`,
`Jw_len`); the ball is `B(u) = ballD ν R = {w : D(w) ≤ R}`, i.e. `ν w ≥ e^{-2R}`
(`le_nu_iff`); we take `R = Rad J = (J+1) ln 2`, so `e^{-2R} = θ J = 4^{-(J+1)}`.

* Step 1: `shell_iff` (`θ ≤ ν < 3θ` is `R - ℓ_max < D ≤ R`, as `e^{2 ℓ_max} = 3`);
  that the lost set lies in this shell is the `hsub` part of `retained_cut`.
* Step 2: the tree parent `par` (a tight parent of largest mass, so that `D(p(w))`
  is smallest); children carry at most the parent's mass is `bdMass_insert`
  (`DegreeLabelsShell`).
* Step 3: `m(t) = mcut t = cutMass (e^{-2t})` is nonincreasing (`mcut_anti`, from
  `cutMass_mono`); the cut `A_t` is `{w ≠ u : D(p w) < t ≤ D w}` (`mem_bd_iff`,
  `mem_cut_iff_Jw`), so `m` is the step function `stepM t = ∑_w ν w 1[t ∈ J_w]`
  (`mcut_eq_stepM`), `J_w = (D(p w), D w]` (`Jw`).
* Step 4: the integral identity `∫_a^b m = ∑_w ν w |J_w ∩ (a,b]|` (`integral_stepM`);
  the two bullets and the conclusion `shell mass ≤ ε_R · ball mass` with
  `ε_R = 2 ℓ_max² / (ℓ_min (R - 2 ℓ_max))` (`shell_cut`); transfer to the labels
  (`lost_le`, `retained_cut`, `lab_corr_cut`).
* The theorem `degreeLabels_cut` chooses `J` with `ε_R ≤ min η 1`.
-/

noncomputable section
open scoped BigOperators RealInnerProductSpace
open Classical MeasureTheory Set

namespace CubicPathwidth
namespace T2
namespace DL

section Cut

variable {n : ℕ} {G : SimpleGraph (Fin n)} {ν c : Fin n → ℝ} {u : Fin n}

/-- Shortest arc length `ℓ_min = ½ ln 2`. -/
def lmin : ℝ := Real.log 2 / 2

/-- Longest arc length `ℓ_max = ½ ln 3`. -/
def lmax : ℝ := Real.log 3 / 2

/-- The directed distance `D(w) = -½ ln ν(w)` (`ν = e^{-2D}`). -/
def Dd (ν : Fin n → ℝ) (w : Fin n) : ℝ := -(Real.log (ν w) / 2)

/-- Tight parents of `w`. -/
def tight (G : SimpleGraph (Fin n)) (ν c : Fin n → ℝ) (w : Fin n) : Finset (Fin n) :=
  Finset.univ.filter fun x => G.Adj x w ∧ ν w = c x * ν x

/-- The tree parent `p(w)`: a tight parent of largest mass (`D` smallest). -/
def par (G : SimpleGraph (Fin n)) (ν c : Fin n → ℝ) (w : Fin n) : Fin n :=
  if h : (tight G ν c w).Nonempty then Classical.choose (Finset.exists_max_image _ ν h) else w

/-- The interval `J_w = (D(p(w)), D(w)]`. -/
def Jw (G : SimpleGraph (Fin n)) (ν c : Fin n → ℝ) (w : Fin n) : Set ℝ :=
  Ioc (Dd ν (par G ν c w)) (Dd ν w)

/-- The cut mass `m(t)` as a step function of the real level: `∑_w ν(w) 1[t ∈ J_w]`. -/
def stepM (G : SimpleGraph (Fin n)) (ν c : Fin n → ℝ) (t : ℝ) : ℝ :=
  ∑ w, ν w * (Jw G ν c w).indicator (fun _ => (1 : ℝ)) t

/-- The cut mass of the level `e^{-2t}` in the sense of `DegreeLabelsShell`. -/
def mcut (G : SimpleGraph (Fin n)) (ν c : Fin n → ℝ) (t : ℝ) : ℝ :=
  cutMass G ν c (Real.exp (-2 * t))

theorem par_spec (H : Hyp G ν c u) {w : Fin n} (hw : w ≠ u) :
    par G ν c w ∈ tight G ν c w ∧ ∀ x ∈ tight G ν c w, ν x ≤ ν (par G ν c w) := by
  have hne : (tight G ν c w).Nonempty := by
    obtain ⟨x, hx, hwx⟩ := H.parent w hw
    exact ⟨x, by simp [tight, hx, hwx]⟩
  unfold par
  split_ifs
  exact Classical.choose_spec (Finset.exists_max_image _ ν hne)

theorem par_adj (H : Hyp G ν c u) {w : Fin n} (hw : w ≠ u) :
    G.Adj (par G ν c w) w ∧ ν w = c (par G ν c w) * ν (par G ν c w) := by
  have := (par_spec H hw).1
  simpa [tight] using this

/-- Steps 2–3, interface: `w` lies in the cut at level `s < 1` iff `ν w ≤ s < ν (p w)`. -/
theorem mem_bd_iff (H : Hyp G ν c u) {s : ℝ} (hs : s < 1) {w : Fin n} :
    w ∈ bd G ν c (lvl ν s) ↔ w ≠ u ∧ ν w ≤ s ∧ s < ν (par G ν c w) := by
  rw [mem_bd_lvl]
  constructor
  · rintro ⟨h1, x, hx, hadj, hwx⟩
    have hwu : w ≠ u := by
      rintro rfl
      rw [H.root] at h1
      linarith
    refine ⟨hwu, h1, hx.trans_le ((par_spec H hwu).2 x ?_)⟩
    simp [tight, hadj, hwx]
  · rintro ⟨hwu, h1, h2⟩
    exact ⟨h1, par G ν c w, h2, (par_adj H hwu).1, (par_adj H hwu).2⟩

theorem Dd_root (H : Hyp G ν c u) : Dd ν u = 0 := by simp [Dd, H.root]

theorem nu_par_pos (H : Hyp G ν c u) {w : Fin n} (hw : w ≠ u) (hpos : 0 < ν w) :
    0 < ν (par G ν c w) := by
  obtain ⟨-, h⟩ := par_adj H hw
  have h1 := H.c_lo (par G ν c w)
  have h2 := H.nonneg (par G ν c w)
  by_contra hcon
  have : ν (par G ν c w) = 0 := le_antisymm (not_lt.mp hcon) h2
  rw [this] at h
  linarith

/-- Membership in `J_w` at a level `t > 0`: the pointwise form of Step 3. -/
theorem mem_cut_iff_Jw (H : Hyp G ν c u) {t : ℝ} (ht : 0 < t) {w : Fin n} (hpos : 0 < ν w) :
    w ∈ bd G ν c (lvl ν (Real.exp (-2 * t))) ↔ t ∈ Jw G ν c w := by
  have hs : Real.exp (-2 * t) < 1 := by
    rw [Real.exp_lt_one_iff]; linarith
  rw [mem_bd_iff H hs]
  by_cases hwu : w = u
  · subst hwu
    simp only [Jw, Dd_root H, mem_Ioc]
    constructor
    · rintro ⟨h, -⟩; exact absurd rfl h
    · rintro ⟨-, h⟩; linarith
  · have hp := nu_par_pos H hwu hpos
    simp only [Jw, Dd, mem_Ioc, hwu, ne_eq, not_false_eq_true, true_and]
    rw [← Real.log_le_iff_le_exp hpos, ← Real.lt_log_iff_exp_lt hp]
    constructor <;> rintro ⟨h1, h2⟩
    · exact ⟨by linarith, by linarith⟩
    · exact ⟨by linarith, by linarith⟩

theorem mcut_eq_stepM (H : Hyp G ν c u) {t : ℝ} (ht : 0 < t) : mcut G ν c t = stepM G ν c t := by
  unfold mcut cutMass bdMass stepM
  rw [← Finset.univ_inter (bd G ν c (lvl ν (Real.exp (-2 * t)))), ← Finset.sum_ite_mem]
  refine Finset.sum_congr rfl fun w _ => ?_
  rcases (H.nonneg w).eq_or_lt with h0 | hpos
  · rw [← h0]; simp
  · by_cases hm : w ∈ bd G ν c (lvl ν (Real.exp (-2 * t)))
    · have := (mem_cut_iff_Jw H ht hpos).mp hm
      simp only [hm, ite_true, indicator_of_mem this, mul_one]
    · have : t ∉ Jw G ν c w := fun h => hm ((mem_cut_iff_Jw H ht hpos).mpr h)
      simp only [hm, ite_false, indicator_of_notMem this, mul_zero]

/-- Step 3: the cut mass is nonincreasing on `(0,∞)`. -/
theorem mcut_anti (H : Hyp G ν c u) {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    mcut G ν c t ≤ mcut G ν c s := by
  unfold mcut
  apply cutMass_mono H (Real.exp_pos _).le
  · exact Real.exp_le_exp.mpr (by linarith)
  · rw [Real.exp_lt_one_iff]; linarith

theorem stepM_anti (H : Hyp G ν c u) {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    stepM G ν c t ≤ stepM G ν c s := by
  rw [← mcut_eq_stepM H hs, ← mcut_eq_stepM H (hs.trans_le hst)]
  exact mcut_anti H hs hst

theorem measurable_Jw (w : Fin n) : MeasurableSet (Jw G ν c w) := measurableSet_Ioc

theorem integrable_Jw (w : Fin n) :
    Integrable ((Jw G ν c w).indicator fun _ => (1 : ℝ)) := by
  refine (integrable_indicator_iff (measurable_Jw w)).mpr (integrableOn_const ?_)
  simp [Jw]

theorem integrableOn_stepM (a b : ℝ) :
    IntegrableOn (stepM G ν c) (Ioc a b) := by
  unfold stepM
  refine integrable_finsetSum _ fun w _ => ?_
  exact (integrable_Jw w).const_mul _ |>.integrableOn

/-- Step 4: the integral identity `∫_a^b m = ∑_w ν(w) |J_w ∩ (a,b]|`. -/
theorem integral_stepM (a b : ℝ) :
    ∫ t in Ioc a b, stepM G ν c t =
      ∑ w, ν w * volume.real (Jw G ν c w ∩ Ioc a b) := by
  unfold stepM
  rw [integral_finsetSum]
  · refine Finset.sum_congr rfl fun w _ => ?_
    rw [integral_const_mul, setIntegral_indicator (measurable_Jw w), setIntegral_const,
      Set.inter_comm]
    simp
  · intro w _
    exact ((integrable_Jw w).const_mul _).integrableOn

/-! ### Step 4: the arc lengths and the two bullet estimates -/

theorem lmin_pos : 0 < lmin := by unfold lmin; have := Real.log_pos (by norm_num : (1:ℝ) < 2); linarith

theorem lmin_le_lmax : lmin ≤ lmax := by
  unfold lmin lmax
  have := Real.log_le_log (by norm_num : (0:ℝ) < 2) (by norm_num : (2:ℝ) ≤ 3)
  linarith

theorem lmax_pos : 0 < lmax := lmin_pos.trans_le lmin_le_lmax

/-- The interval `J_w` has length in `[ℓ_min, ℓ_max]`. -/
theorem Jw_len (H : Hyp G ν c u) {w : Fin n} (hw : w ≠ u) (hpos : 0 < ν w) :
    lmin ≤ Dd ν w - Dd ν (par G ν c w) ∧ Dd ν w - Dd ν (par G ν c w) ≤ lmax := by
  obtain ⟨-, h⟩ := par_adj H hw
  have hp := nu_par_pos H hw hpos
  set p := par G ν c w
  have hc0 : 0 < c p := by linarith [H.c_lo p]
  have hlog : Real.log (ν w) = Real.log (c p) + Real.log (ν p) := by
    rw [h, Real.log_mul hc0.ne' hp.ne']
  have e : Dd ν w - Dd ν p = -(Real.log (c p)) / 2 := by
    unfold Dd; rw [hlog]; ring
  have h1 : Real.log (c p) ≤ -Real.log 2 := by
    have := Real.log_le_log hc0 (H.c_hi p)
    rwa [one_div, Real.log_inv] at this
  have h2 : -Real.log 3 ≤ Real.log (c p) := by
    have := Real.log_le_log (by norm_num : (0:ℝ) < 1/3) (H.c_lo p)
    rwa [one_div, Real.log_inv] at this
  rw [e]; unfold lmin lmax
  constructor <;> linarith

theorem vol_inter_le (l h a b : ℝ) : volume.real (Ioc l h ∩ Ioc a b) ≤ max (h - l) 0 := by
  rw [← Real.volume_real_Ioc]
  exact measureReal_mono inter_subset_left measure_Ioc_lt_top.ne

theorem vol_inter_eq_zero {l h a b : ℝ} (hlb : b ≤ l ∨ h ≤ a) :
    volume.real (Ioc l h ∩ Ioc a b) = 0 := by
  have : Ioc l h ∩ Ioc a b = ∅ := by
    rw [Set.eq_empty_iff_forall_notMem]
    rintro t ⟨⟨h1, h2⟩, h3, h4⟩
    rcases hlb with h | h <;> linarith
  rw [this]; simp

/-- The ball `B(u) = {w : D(w) ≤ R}` (on the component of `u`). -/
def ballD (ν : Fin n → ℝ) (R : ℝ) : Finset (Fin n) :=
  Finset.univ.filter fun w => 0 < ν w ∧ Dd ν w ≤ R

/-- The outer shell `{R - ℓ_max < D(w) ≤ R}`. -/
def shellD (ν : Fin n → ℝ) (R : ℝ) : Finset (Fin n) :=
  Finset.univ.filter fun w => 0 < ν w ∧ R - lmax < Dd ν w ∧ Dd ν w ≤ R

/-- The constant `ε_R = 2 ℓ_max² / (ℓ_min (R - 2 ℓ_max))`. -/
def epsR (R : ℝ) : ℝ := 2 * lmax ^ 2 / (lmin * (R - 2 * lmax))

/-- The shell estimate of the paper (Step 4). -/
theorem shell_cut (H : Hyp G ν c u) {R : ℝ} (hR : 2 * lmax < R) :
    ∑ w ∈ shellD ν R, ν w ≤ epsR R * ∑ w ∈ ballD ν R, ν w := by
  have hlmin := lmin_pos
  have hlmax := lmax_pos
  set T := R - 2 * lmax with hT
  have hTpos : 0 < T := by linarith
  set σ := ∑ w ∈ ballD ν R, ν w with hσ
  have hRT : R - T = 2 * lmax := by rw [hT]; ring
  -- first bullet: `T m(T) ≤ ℓ_max σ`
  have b1 : T * stepM G ν c T ≤ lmax * σ := by
    have h1 : T * stepM G ν c T ≤ ∫ t in Ioc 0 T, stepM G ν c t := by
      have := setIntegral_mono_on (μ := volume) (f := fun _ => stepM G ν c T)
        (integrableOn_const (by simp)) (integrableOn_stepM 0 T) measurableSet_Ioc
        (fun t ht => stepM_anti H ht.1 ht.2)
      rw [setIntegral_const, Real.volume_real_Ioc_of_le hTpos.le] at this
      simpa using this
    rw [integral_stepM] at h1
    refine h1.trans ?_
    calc ∑ w, ν w * volume.real (Jw G ν c w ∩ Ioc 0 T)
        ≤ ∑ w, (if w ∈ ballD ν R then lmax * ν w else 0) := by
          refine Finset.sum_le_sum fun w _ => ?_
          rcases (H.nonneg w).eq_or_lt with h0 | hpos
          · rw [← h0]; simp
          · by_cases hwu : w = u
            · subst hwu
              have : volume.real (Jw G ν c w ∩ Ioc 0 T) = 0 := by
                apply vol_inter_eq_zero; right; simp [Dd_root H]
              rw [this, mul_zero]; split_ifs
              · exact mul_nonneg lmax_pos.le (H.nonneg _)
              · exact le_rfl
            · obtain ⟨hl1, hl2⟩ := Jw_len H hwu hpos
              by_cases hb : w ∈ ballD ν R
              · simp only [hb, ite_true]
                have h3 := vol_inter_le (Dd ν (par G ν c w)) (Dd ν w) 0 T
                rw [max_eq_left (by linarith)] at h3
                have h4 : volume.real (Jw G ν c w ∩ Ioc 0 T) ≤ lmax := by
                  unfold Jw; linarith
                nlinarith [mul_le_mul_of_nonneg_left h4 (H.nonneg w)]
              · simp only [hb, ite_false]
                have hD : R < Dd ν w := by
                  by_contra hcon
                  exact hb (by simp [ballD, hpos, not_lt.mp hcon])
                have : volume.real (Jw G ν c w ∩ Ioc 0 T) = 0 := by
                  apply vol_inter_eq_zero; left; linarith
                rw [this]; simp
      _ = lmax * σ := by
          rw [Finset.sum_ite_mem, Finset.univ_inter, ← Finset.mul_sum]
  -- second bullet: `ℓ_min (shell mass) ≤ 2 ℓ_max m(T)`
  have b2 : lmin * ∑ w ∈ shellD ν R, ν w ≤ 2 * lmax * stepM G ν c T := by
    have h1 : ∫ t in Ioc T R, stepM G ν c t ≤ 2 * lmax * stepM G ν c T := by
      have := setIntegral_mono_on (μ := volume) (g := fun _ => stepM G ν c T)
        (integrableOn_stepM T R) (integrableOn_const (by simp)) measurableSet_Ioc
        (fun t ht => stepM_anti H hTpos ht.1.le)
      rw [setIntegral_const, Real.volume_real_Ioc_of_le (by linarith), hRT] at this
      simpa using this
    refine le_trans ?_ h1
    rw [integral_stepM, Finset.mul_sum]
    refine le_trans ?_ (Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ (shellD ν R))
      (fun w _ _ => mul_nonneg (H.nonneg w) measureReal_nonneg))
    refine Finset.sum_le_sum fun w hw => ?_
    simp only [shellD, Finset.mem_filter, Finset.mem_univ, true_and] at hw
    obtain ⟨hpos, hD1, hD2⟩ := hw
    have hwu : w ≠ u := by
      rintro rfl; rw [Dd_root H] at hD1; linarith
    obtain ⟨hl1, hl2⟩ := Jw_len H hwu hpos
    have hsub : Jw G ν c w ⊆ Ioc T R := by
      intro t ht
      exact ⟨by linarith [ht.1], by linarith [ht.2]⟩
    rw [Set.inter_eq_left.mpr hsub, Jw, Real.volume_real_Ioc_of_le (by linarith)]
    rw [mul_comm lmin]
    exact mul_le_mul_of_nonneg_left hl1 (H.nonneg w)
  unfold epsR
  rw [div_mul_eq_mul_div, le_div_iff₀ (mul_pos hlmin hTpos)]
  have hS : 0 ≤ ∑ w ∈ shellD ν R, ν w := Finset.sum_nonneg fun w _ => H.nonneg w
  nlinarith [mul_le_mul_of_nonneg_right b2 hTpos.le,
    mul_le_mul_of_nonneg_left b1 (by positivity : 0 ≤ 2 * lmax)]

end Cut

/-! ## Application to the labels: radius `R_J = (J+1) ln 2`, threshold `θ J = e^{-2 R_J}` -/

/-- The truncation radius `R_J = (J+1) ln 2` (so that `e^{-2 R_J} = θ J = 4^{-(J+1)}`). -/
def Rad (J : ℕ) : ℝ := ((J : ℝ) + 1) * Real.log 2

theorem log_θ (J : ℕ) : Real.log (θ J) = -2 * Rad J := by
  unfold θ Rad
  rw [Real.log_pow, one_div, Real.log_inv, show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
  push_cast
  ring

theorem exp_Rad (J : ℕ) : Real.exp (-2 * Rad J) = θ J := by
  rw [← log_θ, Real.exp_log (θ_pos J)]

/-- Membership in the retained set is the radius condition `D(u,w) ≤ R`. -/
theorem le_nu_iff {ν : Fin n → ℝ} {J : ℕ} {w : Fin n} :
    θ J ≤ ν w ↔ 0 < ν w ∧ Dd ν w ≤ Rad J := by
  constructor
  · intro h
    have hp : 0 < ν w := (θ_pos J).trans_le h
    refine ⟨hp, ?_⟩
    have := Real.log_le_log (θ_pos J) h
    rw [log_θ] at this
    unfold Dd; linarith
  · rintro ⟨hp, h⟩
    rw [← Real.log_le_log_iff (θ_pos J) hp, log_θ]
    unfold Dd at h; linarith

/-- Shell points: `θ ≤ ν < 3 θ` means `R - ℓ_max < D ≤ R`. -/
theorem shell_iff {ν : Fin n → ℝ} {J : ℕ} {w : Fin n} :
    (θ J ≤ ν w ∧ ν w < 3 * θ J) ↔ (0 < ν w ∧ Rad J - lmax < Dd ν w ∧ Dd ν w ≤ Rad J) := by
  constructor
  · rintro ⟨h1, h2⟩
    obtain ⟨hp, hD⟩ := le_nu_iff.mp h1
    refine ⟨hp, ?_, hD⟩
    have := Real.log_lt_log hp h2
    rw [Real.log_mul (by norm_num) (θ_pos J).ne', log_θ] at this
    unfold Dd lmax; linarith
  · rintro ⟨hp, h1, h2⟩
    refine ⟨le_nu_iff.mpr ⟨hp, h2⟩, ?_⟩
    rw [← Real.log_lt_log_iff hp (by have := θ_pos J; positivity),
      Real.log_mul (by norm_num) (θ_pos J).ne', log_θ]
    unfold Dd lmax at h1; linarith

theorem epsR_nonneg {R : ℝ} (hR : 2 * lmax < R) : 0 ≤ epsR R := by
  unfold epsR
  have := lmin_pos
  have : 0 < R - 2 * lmax := by linarith
  positivity

/-- The lost mass of the paper: the outer shell has mass at most `ε_R` times the ball mass. -/
theorem lost_le (H : Hyp G ν c u) {J : ℕ} (hR : 2 * lmax < Rad J) :
    ∑ w ∈ Finset.univ.filter (fun w => θ J ≤ ν w ∧ ν w < 3 * θ J), ν w ≤
      epsR (Rad J) * ∑ w ∈ Finset.univ.filter (fun w => θ J ≤ ν w), ν w := by
  have h := shell_cut H hR
  have h1 : ∑ w ∈ Finset.univ.filter (fun w => θ J ≤ ν w ∧ ν w < 3 * θ J), ν w ≤
      ∑ w ∈ shellD ν (Rad J), ν w := by
    refine Finset.sum_le_sum_of_subset_of_nonneg ?_ (fun w _ _ => H.nonneg w)
    intro w hw
    simp only [shellD, Finset.mem_filter, Finset.mem_univ, true_and] at hw ⊢
    exact shell_iff.mp hw
  have h2 : ∑ w ∈ ballD ν (Rad J), ν w ≤
      ∑ w ∈ Finset.univ.filter (fun w => θ J ≤ ν w), ν w := by
    refine Finset.sum_le_sum_of_subset_of_nonneg ?_ (fun w _ _ => H.nonneg w)
    intro w hw
    simp only [ballD, Finset.mem_filter, Finset.mem_univ, true_and] at hw ⊢
    exact le_nu_iff.mpr hw
  exact h1.trans (h.trans (mul_le_mul_of_nonneg_left h2 (epsR_nonneg hR)))

section Main'

variable {n : ℕ} {G : SimpleGraph (Fin n)} (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
include hmin hmax

/-- Retained mass, with the shell bounded by the paper's cut argument. -/
theorem retained_cut {J : ℕ} (hR : 2 * lmax < Rad J) {u v : Fin n} (huv : G.Adj u v) :
    (1 - epsR (Rad J)) * mass G J u ≤ ∑ w ∈ supp G J u ∩ supp G J v, nu G u w := by
  have H := hyp hmin hmax u
  have hsplit := Finset.sum_sdiff (s₁ := supp G J u ∩ supp G J v) (s₂ := supp G J u)
    (f := nu G u) Finset.inter_subset_left
  have hsub : supp G J u \ (supp G J u ∩ supp G J v) ⊆
      Finset.univ.filter (fun w => θ J ≤ nu G u w ∧ nu G u w < 3 * θ J) := by
    intro w hw
    simp only [supp, Finset.mem_sdiff, Finset.mem_inter, Finset.mem_filter, Finset.mem_univ,
      true_and, not_and] at hw ⊢
    obtain ⟨h1, h2⟩ := hw
    refine ⟨h1, ?_⟩
    have hv : nu G v w < θ J := lt_of_not_ge (h2 h1)
    have hc := amp_concat (sc_nonneg (G := G)) (sc_le_one hmin hmax) huv w
    have hsq := pow_le_pow_left₀ (mul_nonneg (sc_nonneg (G := G) v)
      (amp_nonneg (sc_nonneg (G := G)) u w)) hc 2
    rw [mul_pow] at hsq
    have hlo := cw_lo hmin hmax v
    unfold cw at hlo
    unfold nu at hv ⊢
    nlinarith [sq_nonneg (amp G (sc G) u w)]
  have hlost := Finset.sum_le_sum_of_subset_of_nonneg hsub (fun w _ _ => H.nonneg w)
  have hshell := lost_le H hR
  have hmass : mass G J u = ∑ w ∈ supp G J u, nu G u w := rfl
  have hsupp : supp G J u = Finset.univ.filter (fun w => θ J ≤ nu G u w) := rfl
  rw [← hsupp] at hshell
  rw [sub_mul, one_mul, hmass]
  linarith

theorem lab_corr_cut {J : ℕ} (hR : 2 * lmax < Rad J) (hε : epsR (Rad J) ≤ 1) {u v : Fin n}
    (huv : G.Adj u v) :
    edgeFloor (G.degree u) (G.degree v) * (1 - epsR (Rad J)) ≤ ⟪lab G J u, lab G J v⟫ := by
  have h0 := sc_nonneg (G := G)
  have h1 := sc_le_one hmin hmax
  obtain ⟨hρ, hρ2⟩ := floor_ok (deg_cases hmin hmax u) (deg_cases hmin hmax v)
  rw [lab_inner hmin hmax, coef_inner_sum]
  have ht : 0 ≤ 1 - epsR (Rad J) := by linarith
  apply corr_of_retained _ _ _ _ _ _ _ hρ ht (mass_pos hmin hmax J u) (mass_pos hmin hmax J v)
    (retained_cut hmin hmax hR huv)
  · simpa only [Finset.inter_comm] using retained_cut hmin hmax hR huv.symm
  · exact common_support_general _ _ _ (h0 u) (h0 v) hρ hρ2
      (fun w _ => amp_concat h0 h1 huv.symm w) (fun w _ => amp_concat h0 h1 huv w)

end Main'

end DL

/-- (B1) Degree-sensitive labels, with the shell estimated by the cut argument. -/
theorem degreeLabels_cut : DegreeLabelsClaim := by
  intro η hη
  set η' := min η 1 with hη'
  have hη'0 : 0 < η' := lt_min hη one_pos
  have hη'1 : η' ≤ 1 := min_le_right _ _
  have hη'η : η' ≤ η := min_le_left _ _
  have hlmin := DL.lmin_pos
  have hlmax := DL.lmax_pos
  have hlog2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
  set K : ℝ := 2 * DL.lmax ^ 2 / (DL.lmin * η') + 2 * DL.lmax with hK
  have hKpos : 0 < K := by positivity
  set J := ⌈K / Real.log 2⌉₊ with hJdef
  have hJK : K ≤ DL.Rad J := by
    have hc := Nat.le_ceil (K / Real.log 2)
    rw [div_le_iff₀ hlog2] at hc
    unfold DL.Rad
    nlinarith
  have hR : 2 * DL.lmax < DL.Rad J := by
    have : 0 < 2 * DL.lmax ^ 2 / (DL.lmin * η') := by positivity
    linarith
  have hε : DL.epsR (DL.Rad J) ≤ η' := by
    unfold DL.epsR
    have hpos : 0 < DL.lmin * (DL.Rad J - 2 * DL.lmax) := mul_pos hlmin (by linarith)
    rw [div_le_iff₀ hpos]
    have h1 : 2 * DL.lmax ^ 2 / (DL.lmin * η') ≤ DL.Rad J - 2 * DL.lmax := by
      have : K - 2 * DL.lmax ≤ DL.Rad J - 2 * DL.lmax := by linarith
      simpa [hK] using this
    rw [div_le_iff₀ (mul_pos hlmin hη'0)] at h1
    nlinarith
  refine ⟨2 * J + 2, ?_⟩
  intro n G hmin hmax
  refine ⟨DL.lab G J, DL.norm_lab hmin hmax J, ?_, DL.lab_local hmin hmax J,
    fun u v huv => DL.lab_injective hmin hmax J huv⟩
  intro u v huv
  have h := DL.lab_corr_cut hmin hmax hR (hε.trans hη'1) huv
  obtain ⟨hρ, -⟩ := DL.floor_ok (DL.deg_cases hmin hmax u) (DL.deg_cases hmin hmax v)
  have : (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤
      edgeFloor (G.degree u) (G.degree v) * (1 - DL.epsR (DL.Rad J)) := by
    rw [mul_comm]
    exact mul_le_mul_of_nonneg_left (by linarith) hρ
  exact this.trans h

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.degreeLabels_cut