CubicPathwidth.PwSeq.Bootstrap

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

import CubicPathwidth.T4.TorsoDyn
import CubicPathwidth.T4.Lift
import CubicPathwidth.PwSeq.BootDeletion
import CubicPathwidth.PwSeq.BootComp

/-!
# The bootstrap lemma for base degree `k ≥ 3` (Q3, Lemma 9.3 (`lem:bootstrap`))

`bootstrapK : BootstrapKClaim`. In the paper: subsection Section 9.3 (`sec:bootstrap-proof`).

The proof is the proof of `T4.bootstrap` (`T4/Process.lean`, base degree `5`) with `5`
replaced by `k`. The `k`-independent state machinery is reused unchanged:
`T4.torsoDynamics` (torso semantics and maximal reductions), `T4.liftClaim`
(`lem:reduction`, paid once) and `T4.kindTwo` (the second case of Lemma 9.11 (`lem:basic`)). The
`k`-dependent parts are the generalized copies

* `Boot.deletion` (`BootDeletion.lean`): Proposition 9.10 (`prop:deletion`) for base degree `k`;
* `Boot.componentClaim` (`BootComp.lean`): the first case of Lemma 9.11 (`lem:basic`), which applies
  the base hypothesis (minimum degree at least `3`, maximum degree at most `k`) to the
  relabelled torso components.

Steps: (1) reduce `G` maximally to a state `(univ, B₀)` with torso minimum degree at
least `3` and `ψ(univ, B₀) ≤ ∑_v b(d(v))`; (2) run the deletion process to `(F₁, B₁)`
with all torso components basic and `|univ \ F₁| + ψ⁻(F₁, B₁) ≤ ψ⁻(univ, B₀) ≤ ψ(univ, B₀)`;
(3) bound the final torso by `max (ψ⁻ + b₃ + (ε/2) n + N₀) (12 √n + 1)`; (4) lift once:
`pw(G) ≤ |univ \ F₁| + pw(torso) + 12 √n + 1`; (5) absorb `b₃ + N₀ + 24 √n + 2` into
`(ε/2) n` for large `n`.
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq

open T2 T4 SectionDecomposition

/-- (Q3) Lemma 9.3 (`lem:bootstrap`) for general base degree `k ≥ 3`: a uniform bound on graphs with
minimum degree at least `3` and maximum degree at most `k` extends to all graphs. -/
theorem bootstrapK : BootstrapKClaim := by
  intro k b hb hbase ε hε
  have hdyn := torsoDynamics
  obtain ⟨N₀, hN₀⟩ := Boot.componentClaim hb hbase (ε / 2) (by linarith)
  obtain ⟨N₂, hN₂⟩ := coreOverhead_sublinear (ε / 16) (by linarith)
  obtain ⟨M, hM⟩ := exists_nat_ge (4 * ((N₀ : ℝ) + 3) / ε)
  refine ⟨max N₂ M, ?_⟩
  intro n hn G
  -- Step 1: maximal reduction of `G`.
  have hgood0 := good_univ G
  obtain ⟨-, -, B₀, hB₀sub, hR₀, hB₀min, hB₀deg⟩ :=
    hdyn n G Finset.univ Finset.univ hgood0
  have hgoodB₀ : Good G Finset.univ B₀ := hgood0.reach hR₀
  have hpsi0 : psi b G Finset.univ B₀ ≤ degreeWeight G b := by
    rw [← psi_univ b G]
    exact Boot.psi_le_psi hb hB₀sub hB₀deg
  -- Step 2: the deletion process.
  obtain ⟨F₁, B₁, hR₁, hmin₁, hbasic₁, hpot⟩ :=
    Boot.deletion hdyn hb n G Finset.univ B₀ hgoodB₀ hB₀min
  have hR₀₁ : Reach G (Finset.univ, Finset.univ) (F₁, B₁) := hR₀.trans hR₁
  have hgood₁ : Good G F₁ B₁ := hR₀₁
  have hψ₀ := (Boot.psi_bounds hb G Finset.univ B₀ hB₀min).2
  have hψ₁ := (Boot.psi_bounds hb G F₁ B₁ hmin₁).1
  -- Step 3: the final torso.
  have hq : ∀ C ∈ tcomps G F₁ B₁, (∀ v ∈ C, tdeg G F₁ B₁ v ≤ k) ∨
      HasPathwidthAtMost (coreTorso G (F₁ \ (B₁ \ C)) C) (12 * Real.sqrt (n : ℝ) + 1) := by
    intro C hC
    rcases hbasic₁ C hC with h | ⟨v, hv, B'', hR, hdisj⟩
    · exact Or.inl h
    · exact Or.inr (kindTwo n G F₁ B₁ C B'' v hgood₁ hC hv hR hdisj)
  have htorso := hN₀ n G F₁ B₁ hgood₁ hmin₁ _ hq
  -- Step 4: lift once.
  have hlifted := hasPathwidth_of_coreTorso_univ G
    (liftClaim n G Finset.univ Finset.univ F₁ B₁ _ hgood0 hR₀₁ htorso)
  -- Step 5: arithmetic.
  apply hlifted.mono
  have hsq : 0 ≤ Real.sqrt (n : ℝ) := Real.sqrt_nonneg _
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  have hb3 : 0 ≤ b 3 := Boot.nonneg hb 3
  have hb3' : b 3 ≤ 1 := hb.le_one 3
  have hmax : max (psiMinus b G F₁ B₁ + b 3 + ε / 2 * n + N₀) (12 * Real.sqrt n + 1) ≤
      psiMinus b G F₁ B₁ + b 3 + ε / 2 * n + N₀ + (12 * Real.sqrt n + 1) := by
    apply max_le
    · linarith
    · have : (0 : ℝ) ≤ N₀ := Nat.cast_nonneg _
      have : 0 ≤ ε / 2 * (n : ℝ) := by positivity
      linarith
  have h1 := hN₂ n ((le_max_left _ _).trans hn)
  unfold coreOverhead at h1
  have hMn : (M : ℝ) ≤ n := by exact_mod_cast (le_max_right _ _).trans hn
  have h2' : 4 * ((N₀ : ℝ) + 3) ≤ ε * n := by
    have := hM.trans hMn
    rw [div_le_iff₀ hε] at this
    linarith
  linarith

end PwSeq
end CubicPathwidth

#check (CubicPathwidth.PwSeq.bootstrapK : CubicPathwidth.PwSeq.BootstrapKClaim)
#print axioms CubicPathwidth.PwSeq.bootstrapK
Back to top