CubicPathwidth.Bootstrap

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

import CubicPathwidth.SectionAssembly
import CubicPathwidth.UniformStep

/-!
# A starting bound from bisection alone

Recursively bisect and hold each cut boundary throughout its side. This pays
c n + c n/2 + ... and gives coefficient 2c. Its purpose is only to enter the
range b < 1/3 where the sharper boundary/core transfer applies. Thus the final
proof need not assume the prior Fomin–Høie bound as an external theorem.
-/

noncomputable section
namespace CubicPathwidth
open SectionDecomposition CutConnector

theorem pathwidth_of_cut_unanchored {n : ℕ} (G : SimpleGraph (Fin n))
    (A : Finset (Fin n)) {a b : ℝ}
    (hA : HasPathwidthAtMost (inducedOnFin G A) a)
    (hB : HasPathwidthAtMost (inducedOnFin G (Finset.univ \ A)) b) :
    HasPathwidthAtMost G
      (max (max (a + ((edges G A).image Prod.fst).card)
        (b + ((edges G A).image Prod.snd).card)) (crossingEdges G A : ℝ)) := by
  classical
  obtain ⟨D, hD⟩ := hA
  obtain ⟨E, hE⟩ := hB
  have hx := ending_hold (lift G A D) ((edges G A).image Prod.fst) (lift_width G A D hD)
  have hy := ending_hold (lift G (Finset.univ \ A) E) ((edges G A).image Prod.snd)
    (lift_width G (Finset.univ \ A) E hE)
  have hX : A ∪ (edges G A).image Prod.fst = A := Finset.union_eq_left.mpr (left_subset G A)
  have hY : (Finset.univ \ A) ∪ (edges G A).image Prod.snd = Finset.univ \ A := by
    apply Finset.union_eq_left.mpr
    intro v hv
    exact Finset.mem_sdiff.mpr ⟨Finset.mem_univ _, right_not_mem G A hv⟩
  rw [hX] at hx
  rw [hY] at hy
  obtain ⟨P, hPend, hP⟩ := hx
  obtain ⟨Q, hQend, hQ⟩ := hy
  exact pathwidth_of_cut_sections G A P Q hPend hQend hP hQ

/-- A coarse but unconditional bootstrap. All thresholds are uniform over G. -/
theorem uniformPathwidthBound_twice_of_bisection {c : ℝ} (hc : 0 ≤ c)
    (hbis : UniformBisectionBound c) : UniformPathwidthBound (2 * c) := by
  classical
  intro ε hε
  let r : ℝ := 2 * c + ε / 2
  have hr : 0 ≤ r := by dsimp [r]; linarith
  obtain ⟨Nc, hNc⟩ := hbis (ε / 8) (by linarith)
  obtain ⟨M, hM⟩ := exists_nat_ge (4 * r / ε)
  let N := max Nc (max 2 M)
  have haff : ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), IsSubcubic G →
      HasPathwidthAtMost G (r * (n : ℝ) + (N : ℝ)) := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro G hG
      by_cases hn : N ≤ n
      · have hnC : Nc ≤ n := (le_max_left _ _).trans hn
        have hn2 : 2 ≤ n := (le_trans (le_max_left _ _) (le_max_right _ _)).trans hn
        have hnM : M ≤ n := (le_trans (le_max_right _ _) (le_max_right _ _)).trans hn
        have hlarge : 4 * r ≤ ε * (n : ℝ) := by
          have hmn : (M : ℝ) ≤ n := by exact_mod_cast hnM
          have ht := (div_le_iff₀ hε).mp (hM.trans hmn)
          nlinarith
        obtain ⟨A, hbal, hcut⟩ := hNc n hnC G hG
        let B := Finset.univ \ A
        have hBcard : B.card = n - A.card := by
          simpa [B] using Finset.card_sdiff_of_subset (Finset.subset_univ A)
        have hsum : A.card + B.card = n := by
          simpa [B, Nat.add_comm] using Finset.card_sdiff_add_card_eq_card (Finset.subset_univ A)
        have hbalanced : A.card ≤ B.card + 1 ∧ B.card ≤ A.card + 1 := by
          simpa only [IsBisection, ← hBcard] using hbal
        have hAhalf : (2 : ℝ) * A.card ≤ (n : ℝ) + 1 := by
          exact_mod_cast (show 2 * A.card ≤ n + 1 by omega)
        have hBhalf : (2 : ℝ) * B.card ≤ (n : ℝ) + 1 := by
          exact_mod_cast (show 2 * B.card ≤ n + 1 by omega)
        have hAsmall : A.card < n := by omega
        have hBsmall : B.card < n := by omega
        have hA := ih A.card hAsmall (inducedOnFin G A) (inducedOnFin_subcubic hG A)
        have hB := ih B.card hBsmall (inducedOnFin G B) (inducedOnFin_subcubic hG B)
        have hw := pathwidth_of_cut_unanchored G A hA hB
        have hX : (((edges G A).image Prod.fst).card : ℝ) ≤ crossingEdges G A := by
          exact_mod_cast (Finset.card_image_le.trans_eq (edges_card G A) :
            ((edges G A).image Prod.fst).card ≤ crossingEdges G A)
        have hY : (((edges G A).image Prod.snd).card : ℝ) ≤ crossingEdges G A := by
          exact_mod_cast (Finset.card_image_le.trans_eq (edges_card G A) :
            ((edges G A).image Prod.snd).card ≤ crossingEdges G A)
        apply hw.mono
        apply max_le
        · apply max_le
          · have hm := mul_le_mul_of_nonneg_left hAhalf hr
            dsimp [r] at *
            nlinarith
          · have hm := mul_le_mul_of_nonneg_left hBhalf hr
            dsimp [r] at *
            nlinarith
        · have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
          have hN0 : (0 : ℝ) ≤ N := Nat.cast_nonneg N
          dsimp [r]
          nlinarith
      · apply (trivial_pathwidth_bound G).mono
        have hnn : (n : ℝ) ≤ N := by exact_mod_cast (show n ≤ N by omega)
        nlinarith [mul_nonneg hr (Nat.cast_nonneg n : (0 : ℝ) ≤ n)]
  obtain ⟨L, hL⟩ := exists_nat_ge (2 * (N : ℝ) / ε)
  refine ⟨L, ?_⟩
  intro n hn G hG
  have hln : (L : ℝ) ≤ n := by exact_mod_cast hn
  have hconst := (div_le_iff₀ hε).mp (hL.trans hln)
  apply (haff n G hG).mono
  dsimp [r]
  nlinarith

end CubicPathwidth
Back to top