CubicPathwidth.T3.DegreeLabels5

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

import CubicPathwidth.T3.Defs
import CubicPathwidth.T2.DegreeLabelsCut

/-!
# Degree-sensitive labels for `3 ≤ δ`, `Δ ≤ 5` (C1)

`degreeLabels5 : DegreeLabels5Claim`.

This adapts `T2/DegreeLabels*.lean` (maximum degree 4) to maximum degree 5. The
definitions of walk amplitudes (`T2.DL.amp`), scales (`T2.DL.sc`), labels
(`T2.DL.lab`), the boundary mass `bdMass`, the tree parent `par`, the step function
`stepM` and the integral identity `integral_stepM` do not depend on the degree bound
and are reused. What changes:

* weights `c x = 1 / (d_x - 1) ∈ [1/4, 1/2]` (`Hyp5`), arc lengths in
  `[ℓ_min, ℓ_max] = [½ ln 2, ½ ln 4 = ln 2]` (`lmax5`, `Jw_len5`);
* the outer shell is `{θ ≤ ν < 4θ} = {R - ℓ_max < D ≤ R}` (`shell_iff5`), and the
  shell step is the paper's moving-cut argument (Steps 1-4 of
  the paper, "Mixed labels") with
  `ε_R = 2 ℓ_max² / (ℓ_min (R - 2 ℓ_max))` (`shell_cut5`, `epsR5`);
* one identity gives the floors for all pairs of degrees `i, j ≥ 2`
  (`rFloor_ok`): `r_{ij}² (1 + s_i s_j)² = 4 s_i s_j` with `s_d = (d-1)^{-1/2}`;
* locality radius `2 J + 2 = R_J / ℓ_min` with `R_J = (J+1) ln 2` (unchanged).
-/

noncomputable section
open scoped BigOperators RealInnerProductSpace
open Classical MeasureTheory Set
open CubicPathwidth.T2 CubicPathwidth.T2.DL

namespace CubicPathwidth
namespace T3
namespace DL5

/-! ## Boundary mass with weights in `[1/4, 1/2]` -/

section Shell

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

/-- Hypotheses on the abstract data, weights `c x ∈ [1/4, 1/2]`. -/
structure Hyp5 (G : SimpleGraph (Fin n)) (ν c : Fin n → ℝ) (u : Fin n) : Prop where
  nonneg : ∀ w, 0 ≤ ν w
  root : ν u = 1
  c_lo : ∀ x, 1 / 4 ≤ c x
  c_hi : ∀ x, c x ≤ 1 / 2
  deg : ∀ x, ((G.degree x : ℝ) - 1) * c x ≤ 1
  parent : ∀ w, w ≠ u → ∃ x, G.Adj x w ∧ ν w = c x * ν x

theorem bdMass_insert5 {u : Fin n} (H : Hyp5 G ν c u) {S : Finset (Fin n)} {x p : Fin n}
    (hxS : x ∉ S) (hpS : p ∈ S) (hpx : G.Adj p x) (hx : ν x = c p * ν p) :
    bdMass G ν c (insert x S) ≤ bdMass G ν c S := by
  have hxbd : x ∈ bd G ν c S := by
    simp only [bd, Finset.mem_filter, Finset.mem_univ, true_and]
    exact ⟨hxS, p, hpS, hpx, hx⟩
  set K := ((G.neighborFinset x).erase p).filter (fun w => ν w = c x * ν x) with hK
  have hsub : bd G ν c (insert x S) ⊆ (bd G ν c S).erase x ∪ K := by
    intro w hw
    simp only [bd, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert,
      not_or] at hw
    obtain ⟨⟨hwx, hwS⟩, y, hy, hyw, hwy⟩ := hw
    rcases hy with hy | hy
    · subst hy
      apply Finset.mem_union_right
      simp only [hK, Finset.mem_filter, Finset.mem_erase, SimpleGraph.mem_neighborFinset]
      exact ⟨⟨fun h => hwS (h ▸ hpS), hyw⟩, hwy⟩
    · apply Finset.mem_union_left
      simp only [Finset.mem_erase, bd, Finset.mem_filter, Finset.mem_univ, true_and]
      exact ⟨hwx, hwS, y, hy, hyw, hwy⟩
  have h1 := Finset.sum_le_sum_of_subset_of_nonneg hsub (fun w _ _ => H.nonneg w)
  have h2 := sum_union_le_of_nonneg (s := (bd G ν c S).erase x) (t := K) H.nonneg
  have h4 := Finset.sum_erase_eq_sub (f := ν) hxbd
  have h5 : ∑ w ∈ K, ν w = K.card * (c x * ν x) := by
    rw [Finset.sum_congr rfl (fun w hw => (Finset.mem_filter.mp hw).2), Finset.sum_const,
      nsmul_eq_mul]
  have hpN : p ∈ G.neighborFinset x := (G.mem_neighborFinset x p).mpr hpx.symm
  have h6 : (K.card : ℝ) ≤ (G.degree x : ℝ) - 1 := by
    have hc := Finset.card_le_card (Finset.filter_subset (fun w => ν w = c x * ν x)
      ((G.neighborFinset x).erase p))
    rw [Finset.card_erase_of_mem hpN, G.card_neighborFinset_eq_degree] at hc
    have hd : 1 ≤ G.degree x := by
      rw [← G.card_neighborFinset_eq_degree]
      exact Finset.card_pos.mpr ⟨p, hpN⟩
    have hc' : (K.card : ℝ) ≤ ((G.degree x - 1 : ℕ) : ℝ) := by exact_mod_cast hc
    rw [Nat.cast_sub hd] at hc'
    simpa using hc'
  have h7 := H.deg x
  have hcx : 0 ≤ c x := by linarith [H.c_lo x]
  have hνx := H.nonneg x
  have h8 := mul_le_mul_of_nonneg_right h6 (mul_nonneg hcx hνx)
  have h9 := mul_le_mul_of_nonneg_right h7 hνx
  unfold bdMass
  nlinarith

theorem bdMass_anti5 {u : Fin n} (H : Hyp5 G ν c u) : ∀ (N : ℕ) (S T : Finset (Fin n)),
    (T \ S).card = N → u ∈ S → UpClosed ν S → UpClosed ν T → S ⊆ T →
      (∀ z ∈ T, 0 < ν z) → bdMass G ν c T ≤ bdMass G ν c S := by
  intro N
  induction N with
  | zero =>
    intro S T hN _ _ _ hST _
    have hTS : T ⊆ S := by
      intro z hz
      by_contra h
      have hz' : z ∈ T \ S := Finset.mem_sdiff.mpr ⟨hz, h⟩
      rw [Finset.card_eq_zero] at hN
      simp [hN] at hz'
    rw [Finset.Subset.antisymm hST hTS]
  | succ N ih =>
    intro S T hN huS hS hT hST hpos
    have hne : (T \ S).Nonempty := by
      rw [← Finset.card_pos, hN]
      omega
    obtain ⟨x, hx, hmax⟩ := Finset.exists_max_image (T \ S) ν hne
    obtain ⟨hxT, hxS⟩ := Finset.mem_sdiff.mp hx
    have hxu : x ≠ u := fun h => hxS (h ▸ huS)
    obtain ⟨p, hpx, hxp⟩ := H.parent x hxu
    have hνx := hpos x hxT
    have hνp : ν x < ν p := by
      have h1 := H.c_hi p
      have h2 := H.nonneg p
      nlinarith
    have hpT : p ∈ T := hT x hxT p hνp
    have hpS : p ∈ S := by
      by_contra h
      have := hmax p (Finset.mem_sdiff.mpr ⟨hpT, h⟩)
      linarith
    have hS' : UpClosed ν (insert x S) := by
      intro y hy z hyz
      rcases Finset.mem_insert.mp hy with hy | hy
      · rw [hy] at hyz
        have hzT := hT x hxT z hyz
        by_contra hz
        have hzS : z ∉ S := fun h => hz (Finset.mem_insert_of_mem h)
        have := hmax z (Finset.mem_sdiff.mpr ⟨hzT, hzS⟩)
        linarith
      · exact Finset.mem_insert_of_mem (hS y hy z hyz)
    have hcard : (T \ insert x S).card = N := by
      rw [Finset.sdiff_insert, Finset.card_erase_of_mem hx, hN]
      rfl
    have := ih (insert x S) T hcard (Finset.mem_insert_of_mem huS) hS' hT
      (Finset.insert_subset hxT hST) hpos
    exact this.trans (bdMass_insert5 H hxS hpS hpx hxp)

theorem cutMass_mono5 {u : Fin n} (H : Hyp5 G ν c u) {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t)
    (ht : t < 1) : cutMass G ν c s ≤ cutMass G ν c t := by
  refine bdMass_anti5 H _ (lvl ν t) (lvl ν s) rfl ?_ (upClosed_lvl t) (upClosed_lvl s) ?_ ?_
  · simp [lvl, H.root, ht]
  · intro w hw
    simp only [lvl, Finset.mem_filter, Finset.mem_univ, true_and] at hw ⊢
    linarith
  · intro z hz
    simp only [lvl, Finset.mem_filter, Finset.mem_univ, true_and] at hz
    linarith

end Shell

/-! ## The paper's moving-cut argument -/

section Cut

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

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

theorem lmax5_eq : lmax5 = Real.log 2 := by
  unfold lmax5
  rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
  push_cast
  ring

theorem lmin_le_lmax5 : lmin ≤ lmax5 := by
  unfold lmin lmax5
  have := Real.log_le_log (by norm_num : (0:ℝ) < 2) (by norm_num : (2:ℝ) ≤ 4)
  linarith

theorem lmax5_pos : 0 < lmax5 := lmin_pos.trans_le lmin_le_lmax5

theorem par_spec5 (H : Hyp5 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_adj5 (H : Hyp5 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_spec5 H hw).1
  simpa [tight] using this

theorem mem_bd_iff5 (H : Hyp5 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_spec5 H hwu).2 x ?_)⟩
    simp [tight, hadj, hwx]
  · rintro ⟨hwu, h1, h2⟩
    exact ⟨h1, par G ν c w, h2, (par_adj5 H hwu).1, (par_adj5 H hwu).2⟩

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

theorem nu_par_pos5 (H : Hyp5 G ν c u) {w : Fin n} (hw : w ≠ u) (hpos : 0 < ν w) :
    0 < ν (par G ν c w) := by
  obtain ⟨-, h⟩ := par_adj5 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

theorem mem_cut_iff_Jw5 (H : Hyp5 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_iff5 H hs]
  by_cases hwu : w = u
  · subst hwu
    simp only [Jw, Dd_root5 H, mem_Ioc]
    constructor
    · rintro ⟨h, -⟩; exact absurd rfl h
    · rintro ⟨-, h⟩; linarith
  · have hp := nu_par_pos5 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_stepM5 (H : Hyp5 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_Jw5 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_Jw5 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_anti5 (H : Hyp5 G ν c u) {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    mcut G ν c t ≤ mcut G ν c s := by
  unfold mcut
  apply cutMass_mono5 H (Real.exp_pos _).le
  · exact Real.exp_le_exp.mpr (by linarith)
  · rw [Real.exp_lt_one_iff]; linarith

theorem stepM_anti5 (H : Hyp5 G ν c u) {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    stepM G ν c t ≤ stepM G ν c s := by
  rw [← mcut_eq_stepM5 H hs, ← mcut_eq_stepM5 H (hs.trans_le hst)]
  exact mcut_anti5 H hs hst

/-- The interval `J_w` has length in `[ℓ_min, ℓ_max]`. -/
theorem Jw_len5 (H : Hyp5 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) ≤ lmax5 := by
  obtain ⟨-, h⟩ := par_adj5 H hw
  have hp := nu_par_pos5 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 4 ≤ Real.log (c p) := by
    have := Real.log_le_log (by norm_num : (0:ℝ) < 1/4) (H.c_lo p)
    rwa [one_div, Real.log_inv] at this
  rw [e]; unfold lmin lmax5
  constructor <;> linarith

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

/-- The constant `ε_R = 2 ℓ_max² / (ℓ_min (R - 2 ℓ_max))` for `ℓ_max = ln 2`. -/
def epsR5 (R : ℝ) : ℝ := 2 * lmax5 ^ 2 / (lmin * (R - 2 * lmax5))

/-- The shell estimate of the paper (Step 4). -/
theorem shell_cut5 (H : Hyp5 G ν c u) {R : ℝ} (hR : 2 * lmax5 < R) :
    ∑ w ∈ shellD5 ν R, ν w ≤ epsR5 R * ∑ w ∈ ballD ν R, ν w := by
  have hlmin := lmin_pos
  have hlmax := lmax5_pos
  set T := R - 2 * lmax5 with hT
  have hTpos : 0 < T := by linarith
  set σ := ∑ w ∈ ballD ν R, ν w with hσ
  have hRT : R - T = 2 * lmax5 := by rw [hT]; ring
  -- first bullet: `T m(T) ≤ ℓ_max σ`
  have b1 : T * stepM G ν c T ≤ lmax5 * σ := 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_anti5 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 lmax5 * ν 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_root5 H]
              rw [this, mul_zero]; split_ifs
              · exact mul_nonneg lmax5_pos.le (H.nonneg _)
              · exact le_rfl
            · obtain ⟨hl1, hl2⟩ := Jw_len5 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) ≤ lmax5 := 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
      _ = lmax5 * σ := 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 ∈ shellD5 ν R, ν w ≤ 2 * lmax5 * stepM G ν c T := by
    have h1 : ∫ t in Ioc T R, stepM G ν c t ≤ 2 * lmax5 * 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_anti5 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 (shellD5 ν R))
      (fun w _ _ => mul_nonneg (H.nonneg w) measureReal_nonneg))
    refine Finset.sum_le_sum fun w hw => ?_
    simp only [shellD5, Finset.mem_filter, Finset.mem_univ, true_and] at hw
    obtain ⟨hpos, hD1, hD2⟩ := hw
    have hwu : w ≠ u := by
      rintro rfl; rw [Dd_root5 H] at hD1; linarith
    obtain ⟨hl1, hl2⟩ := Jw_len5 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 epsR5
  rw [div_mul_eq_mul_div, le_div_iff₀ (mul_pos hlmin hTpos)]
  have hS : 0 ≤ ∑ w ∈ shellD5 ν 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 * lmax5)]

end Cut

/-! ## Radius `R_J = (J+1) ln 2`, threshold `θ J = e^{-2 R_J}` -/

section Radius

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

/-- Shell points: `θ ≤ ν < 4 θ` means `R - ℓ_max < D ≤ R`, as `e^{2 ℓ_max} = 4`. -/
theorem shell_iff5 {ν : Fin n → ℝ} {J : ℕ} {w : Fin n} :
    (θ J ≤ ν w ∧ ν w < 4 * θ J) ↔ (0 < ν w ∧ Rad J - lmax5 < 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 lmax5; 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 lmax5 at h1; linarith

theorem epsR5_nonneg {R : ℝ} (hR : 2 * lmax5 < R) : 0 ≤ epsR5 R := by
  unfold epsR5
  have := lmin_pos
  have : 0 < R - 2 * lmax5 := by linarith
  positivity

/-- The lost mass: the outer shell has mass at most `ε_R` times the ball mass. -/
theorem lost_le5 (H : Hyp5 G ν c u) {J : ℕ} (hR : 2 * lmax5 < Rad J) :
    ∑ w ∈ Finset.univ.filter (fun w => θ J ≤ ν w ∧ ν w < 4 * θ J), ν w ≤
      epsR5 (Rad J) * ∑ w ∈ Finset.univ.filter (fun w => θ J ≤ ν w), ν w := by
  have h := shell_cut5 H hR
  have h1 : ∑ w ∈ Finset.univ.filter (fun w => θ J ≤ ν w ∧ ν w < 4 * θ J), ν w ≤
      ∑ w ∈ shellD5 ν (Rad J), ν w := by
    refine Finset.sum_le_sum_of_subset_of_nonneg ?_ (fun w _ _ => H.nonneg w)
    intro w hw
    simp only [shellD5, Finset.mem_filter, Finset.mem_univ, true_and] at hw ⊢
    exact shell_iff5.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 (epsR5_nonneg hR)))

end Radius

/-! ## The floors: one identity for all pairs of degrees -/

/-- `scD i * scD j = (√((i-1)(j-1)))⁻¹ = exp(-2 x)` with `x = ¼ ln((i-1)(j-1))`;
hence `r_{ij} = sech x` satisfies `r_{ij}² (1 + s_i s_j)² = 4 s_i s_j` exactly. -/
theorem rFloor_ok {i j : ℕ} (hi : 2 ≤ i) (hj : 2 ≤ j) :
    0 ≤ rFloor i j ∧ rFloor i j ^ 2 * (1 + scD i * scD j) ^ 2 ≤ 4 * (scD i * scD j) := by
  have hi' : (1 : ℝ) < i := by exact_mod_cast hi
  have hj' : (1 : ℝ) < j := by exact_mod_cast hj
  have ha1 : 0 < (i : ℝ) - 1 := by linarith
  have ha2 : 0 < (j : ℝ) - 1 := by linarith
  have ha : 0 < ((i : ℝ) - 1) * ((j : ℝ) - 1) := mul_pos ha1 ha2
  refine ⟨?_, ?_⟩
  · unfold rFloor; exact (one_div_pos.mpr (Real.cosh_pos _)).le
  set a := ((i : ℝ) - 1) * ((j : ℝ) - 1) with ha_def
  set E := Real.exp (Real.log a / 4) with hE
  have hEpos : 0 < E := Real.exp_pos _
  have hsq : Real.sqrt a = E ^ 2 := by
    rw [hE, ← Real.exp_nat_mul, Real.sqrt_eq_rpow, Real.rpow_def_of_pos ha]
    congr 1
    push_cast
    ring
  have hs : scD i * scD j = (E ^ 2)⁻¹ := by
    rw [scD, scD, ← mul_inv, ← Real.sqrt_mul ha1.le, ← hsq]
  have hr : rFloor i j = 1 / ((E + E⁻¹) / 2) := by
    unfold rFloor
    rw [← ha_def, Real.cosh_eq, Real.exp_neg]
  rw [hs, hr]
  apply le_of_eq
  field_simp
  ring

end DL5

/-! ## Labels for `3 ≤ δ`, `Δ ≤ 5` -/

namespace DL5

variable {n : ℕ} {G : SimpleGraph (Fin n)}

section Deg

variable (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 5 G)
include hmin hmax

theorem deg_cases5 (x : Fin n) : G.degree x = 3 ∨ G.degree x = 4 ∨ G.degree x = 5 := by
  have h1 : 3 ≤ G.degree x := hmin x
  have h2 : G.degree x ≤ 5 := hmax x
  omega

theorem deg_real5 (x : Fin n) : (3 : ℝ) ≤ G.degree x ∧ (G.degree x : ℝ) ≤ 5 := by
  have h1 : 3 ≤ G.degree x := hmin x
  have h2 : G.degree x ≤ 5 := hmax x
  exact ⟨by exact_mod_cast h1, by exact_mod_cast h2⟩

theorem cw_eq5 (x : Fin n) : cw G x = ((G.degree x : ℝ) - 1)⁻¹ := by
  have := deg_real5 hmin hmax x
  rw [cw, sc, scD, inv_pow, Real.sq_sqrt (by linarith)]

theorem cw_lo5 (x : Fin n) : 1 / 4 ≤ cw G x := by
  have := deg_real5 hmin hmax x
  rw [cw_eq5 hmin hmax, one_div]
  exact inv_anti₀ (by linarith) (by linarith)

theorem cw_hi5 (x : Fin n) : cw G x ≤ 1 / 2 := by
  have := deg_real5 hmin hmax x
  rw [cw_eq5 hmin hmax, one_div]
  exact inv_anti₀ (by norm_num) (by linarith)

theorem cw_deg5 (x : Fin n) : ((G.degree x : ℝ) - 1) * cw G x ≤ 1 := by
  have := deg_real5 hmin hmax x
  rw [cw_eq5 hmin hmax, mul_inv_cancel₀ (by linarith)]

theorem sc_le5 (x : Fin n) : sc G x ≤ (Real.sqrt 2)⁻¹ := by
  have := deg_real5 hmin hmax x
  exact inv_anti₀ (Real.sqrt_pos.mpr two_pos) (Real.sqrt_le_sqrt (by linarith))

theorem sc_le_one5 (x : Fin n) : sc G x ≤ 1 :=
  (sc_le5 hmin hmax x).trans inv_sqrt2_lt_one.le

omit hmax in

theorem nbr_nonempty5 (w : Fin n) : (G.neighborFinset w).Nonempty := by
  apply Finset.card_pos.mp
  rw [G.card_neighborFinset_eq_degree]
  have : 3 ≤ G.degree w := hmin w
  omega

end Deg

section Main

variable (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 5 G)
include hmin hmax

theorem amp_self5 (u : Fin n) : amp G (sc G) u u = 1 :=
  amp_self (sc_nonneg (G := G)) (sc_le_one5 hmin hmax) u

theorem hyp5 (u : Fin n) : Hyp5 G (nu G u) (cw G) u where
  nonneg := fun w => sq_nonneg _
  root := by simp [nu, amp_self5 hmin hmax u]
  c_lo := cw_lo5 hmin hmax
  c_hi := cw_hi5 hmin hmax
  deg := cw_deg5 hmin hmax
  parent := fun w hwu => by
    obtain ⟨x, hx, heq⟩ := amp_tight (sc_nonneg (G := G)) (sc_le_one5 hmin hmax)
      (nbr_nonempty5 hmin w) hwu
    exact ⟨x, hx.symm, by rw [nu, nu, cw, heq]; ring⟩

theorem mem_supp_self5 (J : ℕ) (u : Fin n) : u ∈ supp G J u := by
  unfold supp
  refine Finset.mem_filter.mpr ⟨Finset.mem_univ _, ?_⟩
  rw [nu, amp_self5 hmin hmax u, one_pow]
  exact θ_le_one J

theorem mass_pos5 (J : ℕ) (u : Fin n) : 0 < mass G J u := by
  have h := Finset.single_le_sum (f := nu G u) (fun w _ => sq_nonneg _)
    (mem_supp_self5 hmin hmax J u)
  have h1 : nu G u u = 1 := by simp [nu, amp_self5 hmin hmax u]
  unfold mass
  linarith

/-- Retained mass, with the shell bounded by the paper's cut argument. -/
theorem retained_cut5 {J : ℕ} (hR : 2 * lmax5 < Rad J) {u v : Fin n} (huv : G.Adj u v) :
    (1 - epsR5 (Rad J)) * mass G J u ≤ ∑ w ∈ supp G J u ∩ supp G J v, nu G u w := by
  have H := hyp5 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 < 4 * θ 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_one5 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_lo5 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_le5 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_inner5 (J : ℕ) (u v : Fin n) :
    ⟪lab G J u, lab G J v⟫ = (∑ w, coef G J u w * coef G J v w) /
      Real.sqrt (mass G J u * mass G J v) := by
  have hu := mass_pos5 hmin hmax J u
  have hv := mass_pos5 hmin hmax J v
  rw [lab, lab, real_inner_smul_left, real_inner_smul_right, Real.sqrt_mul hu.le]
  have : ⟪(WithLp.toLp 2 (coef G J u) : GaussianField.Sample n), WithLp.toLp 2 (coef G J v)⟫ =
      ∑ w, coef G J u w * coef G J v w := by
    simp [PiLp.inner_apply, mul_comm]
  rw [this]
  field_simp

theorem norm_lab5 (J : ℕ) (u : Fin n) : ‖lab G J u‖ = 1 := by
  have hu := mass_pos5 hmin hmax J u
  have h := lab_inner5 hmin hmax J u u
  rw [real_inner_self_eq_norm_sq] at h
  simp only [← pow_two, coef_sq_sum] at h
  rw [Real.sqrt_sq hu.le, div_self hu.ne'] at h
  have h0 := norm_nonneg (lab G J u)
  nlinarith

theorem lab_corr_cut5 {J : ℕ} (hR : 2 * lmax5 < Rad J) (hε : epsR5 (Rad J) ≤ 1) {u v : Fin n}
    (huv : G.Adj u v) :
    rFloor (G.degree u) (G.degree v) * (1 - epsR5 (Rad J)) ≤ ⟪lab G J u, lab G J v⟫ := by
  have h0 := sc_nonneg (G := G)
  have h1 := sc_le_one5 hmin hmax
  obtain ⟨hρ, hρ2⟩ := rFloor_ok (i := G.degree u) (j := G.degree v)
    (by have := hmin u; omega) (by have := hmin v; omega)
  rw [lab_inner5 hmin hmax, coef_inner_sum]
  have ht : 0 ≤ 1 - epsR5 (Rad J) := by linarith
  apply corr_of_retained _ _ _ _ _ _ _ hρ ht (mass_pos5 hmin hmax J u) (mass_pos5 hmin hmax J v)
    (retained_cut5 hmin hmax hR huv)
  · simpa only [Finset.inter_comm] using retained_cut5 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)

theorem lab_local5 (J : ℕ) (u w : Fin n) (hw : w ∉ Locality.ball G u (2 * J + 2)) :
    lab G J u w = 0 := by
  rw [lab_apply]
  suffices coef G J u w = 0 by rw [this, mul_zero]
  unfold coef
  split_ifs with h
  · exfalso
    apply hw
    have h0 := sc_nonneg (G := G)
    have hθ := θ_pos J
    have hapos : 0 < amp G (sc G) u w := by
      have := amp_nonneg (G := G) h0 u w
      rcases this.lt_or_eq with h' | h'
      · exact h'
      · unfold nu at h
        rw [← h'] at h
        norm_num at h
        linarith
    have hr := reachable_of_amp_pos hapos
    have hle := amp_le_pow_dist (G := G) h0 (sc_le5 hmin hmax) (inv_sqrt2_lt_one).le u w
    have hsq := pow_le_pow_left₀ hapos.le hle 2
    have h2 : ((Real.sqrt 2)⁻¹ ^ G.dist u w) ^ 2 = (1 / 2 : ℝ) ^ G.dist u w := by
      rw [← pow_mul, mul_comm, pow_mul, inv_pow, Real.sq_sqrt (by norm_num), one_div]
    have hθ2 : θ J = (1 / 2 : ℝ) ^ (2 * J + 2) := by
      rw [θ, show 2 * J + 2 = 2 * (J + 1) by ring, pow_mul]
      norm_num
    have hfin : (1 / 2 : ℝ) ^ (2 * J + 2) ≤ (1 / 2 : ℝ) ^ G.dist u w := by
      rw [← hθ2, ← h2]
      unfold nu at h
      linarith
    rw [pow_le_pow_iff_right_of_lt_one₀ (by norm_num) (by norm_num)] at hfin
    exact (Locality.mem_ball G u w _).mpr ⟨hr, hfin⟩
  · rfl

theorem amp_lt_one5 {u w : Fin n} (hwu : w ≠ u) : amp G (sc G) u w < 1 := by
  have h0 := sc_nonneg (G := G)
  have h1 := sc_le_one5 hmin hmax
  obtain ⟨x, -, hx⟩ := amp_le_parent h0 h1 (nbr_nonempty5 hmin w) hwu
  have := amp_le_one (G := G) h0 h1 u x
  have := sc_le5 hmin hmax x
  have := inv_sqrt2_lt_one
  have := h0 x
  nlinarith

theorem lab_injective5 (J : ℕ) {u v : Fin n} (huv : u ≠ v) : lab G J u ≠ lab G J v := by
  intro h
  have h0 := sc_nonneg (G := G)
  have hu := Real.sqrt_pos.mpr (mass_pos5 hmin hmax J u)
  have hv := Real.sqrt_pos.mpr (mass_pos5 hmin hmax J v)
  have e1 := congrArg (fun x : GaussianField.Sample n => x u) h
  have e2 := congrArg (fun x : GaussianField.Sample n => x v) h
  simp only [lab_apply] at e1 e2
  have cself : ∀ z, coef G J z z = 1 := fun z => by
    simp only [coef, nu, amp_self5 hmin hmax z, one_pow, θ_le_one, ite_true]
  have cbound : ∀ {a b : Fin n}, a ≠ b → 0 ≤ coef G J a b ∧ coef G J a b < 1 := by
    intro a b hab
    unfold coef
    split_ifs
    · exact ⟨amp_nonneg (G := G) h0 a b, amp_lt_one5 hmin hmax (Ne.symm hab)⟩
    · exact ⟨le_rfl, one_pos⟩
  rw [cself] at e1 e2
  obtain ⟨n1, c1⟩ := cbound (Ne.symm huv)
  obtain ⟨n2, c2⟩ := cbound huv
  set a := (Real.sqrt (mass G J u))⁻¹
  set b := (Real.sqrt (mass G J v))⁻¹
  have ha : 0 < a := inv_pos.mpr hu
  have hb : 0 < b := inv_pos.mpr hv
  have : a * 1 * (a * coef G J u v) = b * coef G J v u * (b * 1) := by
    rw [e1, e2]
  nlinarith [mul_pos ha ha, mul_pos hb hb, mul_nonneg n1 n2]

end Main

end DL5

/-- (C1) Degree-sensitive labels for `3 ≤ δ`, `Δ ≤ 5`: for every `η > 0` some locality
radius works. The shell step follows the moving-cut proof of the paper with
`ℓ_min = ½ ln 2`, `ℓ_max = ln 2`. -/
theorem degreeLabels5 : DegreeLabels5Claim := 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 := lmin_pos
  have hlmax := DL5.lmax5_pos
  have hlog2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
  set K : ℝ := 2 * DL5.lmax5 ^ 2 / (lmin * η') + 2 * DL5.lmax5 with hK
  have hKpos : 0 < K := by positivity
  set J := ⌈K / Real.log 2⌉₊ with hJdef
  have hJK : K ≤ Rad J := by
    have hc := Nat.le_ceil (K / Real.log 2)
    rw [div_le_iff₀ hlog2] at hc
    unfold Rad
    nlinarith
  have hR : 2 * DL5.lmax5 < Rad J := by
    have : 0 < 2 * DL5.lmax5 ^ 2 / (lmin * η') := by positivity
    linarith
  have hε : DL5.epsR5 (Rad J) ≤ η' := by
    unfold DL5.epsR5
    have hpos : 0 < lmin * (Rad J - 2 * DL5.lmax5) := mul_pos hlmin (by linarith)
    rw [div_le_iff₀ hpos]
    have h1 : 2 * DL5.lmax5 ^ 2 / (lmin * η') ≤ Rad J - 2 * DL5.lmax5 := by
      have : K - 2 * DL5.lmax5 ≤ Rad J - 2 * DL5.lmax5 := 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 ⟨lab G J, DL5.norm_lab5 hmin hmax J, ?_, DL5.lab_local5 hmin hmax J,
    fun u v huv => DL5.lab_injective5 hmin hmax J huv⟩
  intro u v huv
  have h := DL5.lab_corr_cut5 hmin hmax hR (hε.trans hη'1) huv
  obtain ⟨hρ, -⟩ := DL5.rFloor_ok (i := G.degree u) (j := G.degree v)
    (by have := hmin u; omega) (by have := hmin v; omega)
  have : (1 - η) * rFloor (G.degree u) (G.degree v) ≤
      rFloor (G.degree u) (G.degree v) * (1 - DL5.epsR5 (Rad J)) := by
    rw [mul_comm]
    exact mul_le_mul_of_nonneg_left (by linarith) hρ
  exact this.trans h

end T3
end CubicPathwidth

#print axioms CubicPathwidth.T3.degreeLabels5