CubicPathwidth.T2.DegreeLabels

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

import CubicPathwidth.T2.DegreeLabelsAmp
import CubicPathwidth.T2.DegreeLabelsShell

/-!
# Degree-sensitive Gaussian labels (B1)

`degreeLabels : DegreeLabelsClaim`.

Construction. Put
`sc x = (d_x - 1)^{-1/2}` and let `amp u w` be the largest product of the
scales along a walk from `w` back to `u` (`DegreeLabelsAmp`); thus
`amp u w = e^{-D(u,w)}` for the arc lengths `ℓ(x → y) = ½ ln (d_x - 1)`.
For `J ≥ 1` put `θ = 4^{-(J+1)}`, keep the coefficients with
`amp u w ^ 2 ≥ θ`, and normalize. Then

* common support: for an edge `uv` the coefficient ratios satisfy
  `sc u · amp v ≤ amp u` and `sc v · amp u ≤ amp v`, which gives the factor
  `edgeFloor (d_u) (d_v)` (`common_support_general`, `floor_ok`);
* outer shell: the lost mass lies in `{θ ≤ amp u ^ 2 < 3θ}`, of relative
  mass at most `3/J` (`DegreeLabelsShell`);
* locality: `amp u w ^ 2 ≤ 2^{-dist(u,w)}`, so the support lies in the ball of
  radius `2J + 2`;
* distinctness: `amp u w < 1` for `w ≠ u`.
-/

noncomputable section
open scoped BigOperators RealInnerProductSpace
open Classical

namespace CubicPathwidth
namespace T2
namespace DL

/-! ## Finite estimates with a general floor -/

/-- Coefficient ratios `p b ≤ a`, `q a ≤ b` on the common support give the
factor `ρ` whenever `ρ² (1 + pq)² ≤ 4pq`, i.e. `ρ ≤ 2√(pq)/(1 + pq)`. -/
theorem common_support_general {ι : Type*} (s : Finset ι) (a b : ι → ℝ) {p q ρ : ℝ}
    (hp : 0 ≤ p) (hq : 0 ≤ q) (hρ : 0 ≤ ρ)
    (hρ2 : ρ ^ 2 * (1 + p * q) ^ 2 ≤ 4 * (p * q))
    (h1 : ∀ i ∈ s, p * b i ≤ a i) (h2 : ∀ i ∈ s, q * a i ≤ b i) :
    ρ * Real.sqrt ((∑ i ∈ s, a i ^ 2) * (∑ i ∈ s, b i ^ 2)) ≤ ∑ i ∈ s, a i * b i := by
  have hpoint : ∀ i ∈ s, q * a i ^ 2 + p * b i ^ 2 ≤ (1 + p * q) * (a i * b i) := by
    intro i hi
    have := mul_nonneg (sub_nonneg.mpr (h1 i hi)) (sub_nonneg.mpr (h2 i hi))
    nlinarith
  have hsum := Finset.sum_le_sum hpoint
  rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum, ← Finset.mul_sum] at hsum
  set A := ∑ i ∈ s, a i ^ 2
  set B := ∑ i ∈ s, b i ^ 2
  set S := ∑ i ∈ s, a i * b i
  have hA : 0 ≤ A := Finset.sum_nonneg fun i _ => sq_nonneg _
  have hB : 0 ≤ B := Finset.sum_nonneg fun i _ => sq_nonneg _
  have hpq : 0 < 1 + p * q := by positivity
  have hqp : 0 ≤ q * A + p * B := by positivity
  have hS : 0 ≤ S := by
    by_contra h
    have := mul_neg_of_pos_of_neg hpq (lt_of_not_ge h)
    linarith
  have hAB : 4 * (p * q) * (A * B) ≤ (q * A + p * B) ^ 2 := by
    nlinarith [sq_nonneg (q * A - p * B)]
  have hsq : (q * A + p * B) ^ 2 ≤ ((1 + p * q) * S) ^ 2 := pow_le_pow_left₀ hqp hsum 2
  have key : ρ ^ 2 * (A * B) ≤ S ^ 2 := by
    have h3 : ρ ^ 2 * (1 + p * q) ^ 2 * (A * B) ≤ 4 * (p * q) * (A * B) :=
      mul_le_mul_of_nonneg_right hρ2 (mul_nonneg hA hB)
    have h4 : (1 + p * q) ^ 2 * (ρ ^ 2 * (A * B)) ≤ (1 + p * q) ^ 2 * S ^ 2 := by
      nlinarith
    exact le_of_mul_le_mul_left h4 (by positivity)
  have hx : 0 ≤ ρ * Real.sqrt (A * B) := mul_nonneg hρ (Real.sqrt_nonneg _)
  have hx2 : (ρ * Real.sqrt (A * B)) ^ 2 = ρ ^ 2 * (A * B) := by
    rw [mul_pow, Real.sq_sqrt (mul_nonneg hA hB)]
  exact (pow_le_pow_iff_left₀ hx hS two_ne_zero).mp (hx2 ▸ key)

/-- Passing from common-support norms to full variances keeps the fraction `t`. -/
theorem corr_of_retained (A B U V C t ρ : ℝ) (hρ : 0 ≤ ρ)
    (ht : 0 ≤ t) (hU : 0 < U) (hV : 0 < V)
    (hA : t * U ≤ A) (hB : t * V ≤ B)
    (hC : ρ * Real.sqrt (A * B) ≤ C) :
    ρ * t ≤ C / Real.sqrt (U * V) := by
  have hUV : 0 < U * V := mul_pos hU hV
  have hA0 : 0 ≤ A := (mul_nonneg ht hU.le).trans hA
  have hprod : (t * U) * (t * V) ≤ A * B :=
    mul_le_mul hA hB (mul_nonneg ht hV.le) hA0
  have hsUV := Real.sq_sqrt hUV.le
  have hsquare : (t * Real.sqrt (U * V)) ^ 2 ≤ A * B := by
    calc
      (t * Real.sqrt (U * V)) ^ 2 = t ^ 2 * (U * V) := by rw [mul_pow, hsUV]
      _ = (t * U) * (t * V) := by ring
      _ ≤ A * B := hprod
  have hroot := Real.le_sqrt_of_sq_le hsquare
  have hm := (mul_le_mul_of_nonneg_left hroot hρ).trans hC
  apply (le_div_iff₀ (Real.sqrt_pos.mpr hUV)).mpr
  nlinarith

/-! ## The three floors -/

theorem sqrt6_eq : Real.sqrt 6 = Real.exp (Real.log 6 / 4) ^ 2 := by
  rw [← Real.exp_nat_mul, Real.sqrt_eq_rpow, Real.rpow_def_of_pos (by norm_num)]
  congr 1
  push_cast
  ring

theorem floor34 : r34 ^ 2 * (1 + (Real.sqrt 2)⁻¹ * (Real.sqrt 3)⁻¹) ^ 2 ≤
    4 * ((Real.sqrt 2)⁻¹ * (Real.sqrt 3)⁻¹) := by
  have h6 : Real.sqrt 2 * Real.sqrt 3 = Real.sqrt 6 := by
    rw [← Real.sqrt_mul (by norm_num)]; norm_num
  rw [← mul_inv, h6, sqrt6_eq, r34, Real.cosh_eq, Real.exp_neg]
  set e := Real.exp (Real.log 6 / 4)
  have he : 0 < e := Real.exp_pos _
  apply le_of_eq
  field_simp
  ring

theorem floor33 : r33 ^ 2 * (1 + (Real.sqrt 2)⁻¹ * (Real.sqrt 2)⁻¹) ^ 2 ≤
    4 * ((Real.sqrt 2)⁻¹ * (Real.sqrt 2)⁻¹) := by
  have h2 : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (by norm_num)
  have hp : (Real.sqrt 2)⁻¹ * (Real.sqrt 2)⁻¹ = 1 / 2 := by
    rw [← mul_inv, ← pow_two, h2]; norm_num
  rw [hp, r33, div_pow, mul_pow, h2]
  norm_num

theorem floor44 : r44 ^ 2 * (1 + (Real.sqrt 3)⁻¹ * (Real.sqrt 3)⁻¹) ^ 2 ≤
    4 * ((Real.sqrt 3)⁻¹ * (Real.sqrt 3)⁻¹) := by
  have h2 : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num)
  have hp : (Real.sqrt 3)⁻¹ * (Real.sqrt 3)⁻¹ = 1 / 3 := by
    rw [← mul_inv, ← pow_two, h2]; norm_num
  rw [hp, r44, div_pow, h2]
  norm_num

/-- Scale attached to a degree. -/
def scD (d : ℕ) : ℝ := (Real.sqrt ((d : ℝ) - 1))⁻¹

theorem floor_ok {i j : ℕ} (hi : i = 3 ∨ i = 4) (hj : j = 3 ∨ j = 4) :
    0 ≤ edgeFloor i j ∧ edgeFloor i j ^ 2 * (1 + scD i * scD j) ^ 2 ≤ 4 * (scD i * scD j) := by
  have p33 : 0 ≤ r33 := by unfold r33; positivity
  have p44 : 0 ≤ r44 := by unfold r44; positivity
  have p34 : 0 ≤ r34 := by unfold r34; exact (one_div_pos.mpr (Real.cosh_pos _)).le
  rcases hi with rfl | rfl <;> rcases hj with rfl | rfl <;> norm_num [edgeFloor, scD]
  · exact ⟨p33, floor33⟩
  · exact ⟨p34, floor34⟩
  · refine ⟨p34, ?_⟩
    rw [mul_comm (Real.sqrt 3)⁻¹]
    exact floor34
  · exact ⟨p44, floor44⟩

/-! ## Scales of a graph with `3 ≤ δ`, `Δ ≤ 4` -/

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

def sc (x : Fin n) : ℝ := scD (G.degree x)

/-- Squared scale `1 / (d_x - 1)`. -/
def cw (x : Fin n) : ℝ := sc G x ^ 2

theorem sc_nonneg {G : SimpleGraph (Fin n)} (x : Fin n) : 0 ≤ sc G x :=
  inv_nonneg.mpr (Real.sqrt_nonneg _)

theorem inv_sqrt2_lt_one : (Real.sqrt 2)⁻¹ < 1 := by
  have h : 1 < Real.sqrt 2 := by
    rw [show (1 : ℝ) = Real.sqrt 1 by simp]
    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  exact inv_lt_one_of_one_lt₀ h

section Deg

variable {G} (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
include hmin hmax

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

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

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

theorem cw_lo (x : Fin n) : 1 / 3 ≤ cw G x := by
  have := deg_real hmin hmax x
  rw [cw_eq hmin hmax, one_div]
  exact inv_anti₀ (by linarith) (by linarith)

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

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

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

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

omit hmax in

theorem nbr_nonempty (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

/-! ## Labels -/

/-- Squared amplitude. -/
def nu (u w : Fin n) : ℝ := amp G (sc G) u w ^ 2

def θ (J : ℕ) : ℝ := (1 / 4 : ℝ) ^ (J + 1)

def supp (J : ℕ) (u : Fin n) : Finset (Fin n) := Finset.univ.filter fun w => θ J ≤ nu G u w

def coef (J : ℕ) (u w : Fin n) : ℝ := if θ J ≤ nu G u w then amp G (sc G) u w else 0

def mass (J : ℕ) (u : Fin n) : ℝ := ∑ w ∈ supp G J u, nu G u w

def lab (J : ℕ) (u : Fin n) : GaussianField.Sample n :=
  (Real.sqrt (mass G J u))⁻¹ • WithLp.toLp 2 (coef G J u)

theorem θ_pos (J : ℕ) : 0 < θ J := by unfold θ; positivity

theorem θ_le_one (J : ℕ) : θ J ≤ 1 := by
  unfold θ
  exact pow_le_one₀ (by norm_num) (by norm_num)

theorem four_θ_lt {J : ℕ} (hJ : 1 ≤ J) : 4 * θ J < 1 := by
  unfold θ
  rw [pow_succ]
  have : (1 / 4 : ℝ) ^ J ≤ (1 / 4) ^ 1 := pow_le_pow_of_le_one (by norm_num) (by norm_num) hJ
  nlinarith

theorem pow_θ_lt (J : ℕ) : (4 : ℝ) ^ J * θ J < 1 := by
  unfold θ
  rw [pow_succ, ← mul_assoc, ← mul_pow]
  norm_num

theorem lab_apply (J : ℕ) (u w : Fin n) :
    lab G J u w = (Real.sqrt (mass G J u))⁻¹ * coef G J u w := by
  simp [lab]

theorem coef_sq_sum (J : ℕ) (u : Fin n) : ∑ w, coef G J u w ^ 2 = mass G J u := by
  rw [mass, supp, Finset.sum_filter]
  apply Finset.sum_congr rfl
  intro w _
  unfold coef nu
  split_ifs <;> simp

theorem coef_inner_sum (J : ℕ) (u v : Fin n) :
    ∑ w, coef G J u w * coef G J v w =
      ∑ w ∈ supp G J u ∩ supp G J v, amp G (sc G) u w * amp G (sc G) v w := by
  rw [supp, supp, ← Finset.filter_and, Finset.sum_filter]
  apply Finset.sum_congr rfl
  intro w _
  unfold coef
  split_ifs <;> simp_all

section Main

variable {G} (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
include hmin hmax

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

theorem hyp (u : Fin n) : Hyp G (nu G u) (cw G) u where
  nonneg := fun w => sq_nonneg _
  root := by simp [nu, amp_self' hmin hmax u]
  c_lo := cw_lo hmin hmax
  c_hi := cw_hi hmin hmax
  deg := cw_deg hmin hmax
  parent := fun w hwu => by
    obtain ⟨x, hx, heq⟩ := amp_tight (sc_nonneg (G := G)) (sc_le_one hmin hmax)
      (nbr_nonempty hmin w) hwu
    exact ⟨x, hx.symm, by rw [nu, nu, cw, heq]; ring⟩

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

theorem mass_pos (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_self hmin hmax J u)
  have h1 : nu G u u = 1 := by simp [nu, amp_self' hmin hmax u]
  unfold mass
  linarith

theorem retained {J : ℕ} (hJ : 1 ≤ J) {u v : Fin n} (huv : G.Adj u v) :
    (1 - 3 / (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 := shell_le H (θ_pos J) (four_θ_lt hJ)
  have hpack := pack H (θ_pos J) J (pow_θ_lt J)
  have hJpos : (0 : ℝ) < J := by exact_mod_cast hJ
  have hcut : cutMass G (nu G u) (cw G) (4 * θ J) ≤ mass G J u / J := by
    rw [le_div_iff₀ hJpos, mul_comm]
    exact hpack
  have hmass : mass G J u = ∑ w ∈ supp G J u, nu G u w := rfl
  have h3 : 3 / (J : ℝ) * mass G J u = 3 * (mass G J u / J) := by ring
  rw [sub_mul, one_mul, h3]
  linarith

theorem lab_inner (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_pos hmin hmax J u
  have hv := mass_pos 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_lab (J : ℕ) (u : Fin n) : ‖lab G J u‖ = 1 := by
  have hu := mass_pos hmin hmax J u
  have h := lab_inner 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 {J : ℕ} (hJ : 3 ≤ J) {u v : Fin n} (huv : G.Adj u v) :
    edgeFloor (G.degree u) (G.degree v) * (1 - 3 / (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 hJ' : (3 : ℝ) ≤ J := by exact_mod_cast hJ
  have ht : 0 ≤ 1 - 3 / (J : ℝ) := by
    rw [sub_nonneg, div_le_one (by linarith)]
    exact hJ'
  apply corr_of_retained _ _ _ _ _ _ _ hρ ht (mass_pos hmin hmax J u) (mass_pos hmin hmax J v)
    (retained hmin hmax (by omega) huv)
  · simpa only [Finset.inter_comm] using retained hmin hmax (by omega) 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_local (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_le 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_one {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_one hmin hmax
  obtain ⟨x, -, hx⟩ := amp_le_parent h0 h1 (nbr_nonempty hmin w) hwu
  have := amp_le_one (G := G) h0 h1 u x
  have := sc_le hmin hmax x
  have := inv_sqrt2_lt_one
  have := h0 x
  nlinarith

theorem lab_injective (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_pos hmin hmax J u)
  have hv := Real.sqrt_pos.mpr (mass_pos 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_self' 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_one 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 DL

/-- (B1) Degree-sensitive labels: for every `η > 0` some locality radius works. -/
theorem degreeLabels : DegreeLabelsClaim := by
  intro η hη
  set J := ⌈3 / η⌉₊ + 3 with hJdef
  refine ⟨2 * J + 2, ?_⟩
  intro n G hmin hmax
  have hJ3 : 3 ≤ J := by omega
  have hJη : 3 / (J : ℝ) ≤ η := by
    have hc := Nat.le_ceil (3 / η)
    have hJ : (⌈3 / η⌉₊ : ℝ) ≤ J := by rw [hJdef]; push_cast; linarith
    have hJpos : (0 : ℝ) < J := by
      have : (3 : ℝ) ≤ J := by exact_mod_cast hJ3
      linarith
    rw [div_le_iff₀ hJpos]
    have := (div_le_iff₀ hη).mp (hc.trans hJ)
    linarith
  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 hmin hmax hJ3 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 - 3 / (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