CubicPathwidth.PwSeq.Assembly

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

import CubicPathwidth.PwSeq.Defs
import CubicPathwidth.T2.TargetA
import CubicPathwidth.T3.Targets
import CubicPathwidth.C3.All

/-!
# Parent assembly for Lemma 2 and Theorem 1

Conditional on `TargetBootSeq`, `ExtensionClaim`, `BootstrapKClaim`, `TargetMono` and
`TargetSeedHyps`; uses `C3.c3MainClaim`, `T2.target2a` and `T3.target3P/R/S` for the
bases. In the paper: proofs of Lemma 9.3 (`lem:bootstrap-seq`) and Theorem 9.2 (`thm:pw-seq`), subsection Appendix A.4.1 (`sec:proof-pw-seq`).
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq

open T2 T3 T4

/-- On graphs with all degrees in `[3, k]`, the cost of the seed and of its bootstrap
agree vertex by vertex. -/
theorem degreeWeight_seqCost_eq_boot (hBS : TargetBootSeq) {k : ℕ} {a : ℕ → ℝ}
    (hk : 3 ≤ k) {n : ℕ} (G : SimpleGraph (Fin n)) (hmin : HasMinDegreeAtLeast 3 G)
    (hmax : MaxDegreeAtMost k G) :
    degreeWeight G (seqCost k a) = degreeWeight G (bootstrapSeq k a) := by
  classical
  unfold degreeWeight
  unfold HasMinDegreeAtLeast at hmin
  unfold MaxDegreeAtMost at hmax
  refine Finset.sum_congr rfl fun v _ => ?_
  have h3 : 3 ≤ G.degree v := by convert hmin v
  have hkv : G.degree v ≤ k := by convert hmax v
  rw [(hBS k a hk).2.1 _ h3 hkv]
  have hkv' : ((G.degree v : ℕ) : ℕ∞) ≤ (k : ℕ∞) := by exact_mod_cast hkv
  simp only [seqCost, show ¬ G.degree v ≤ 2 by omega, hkv', ↓reduceIte]

/-- With `k = ∞`, the cost is the sequence itself once it vanishes at degrees `≤ 2`. -/
theorem seqCost_top_eq {b : ℕ → ℝ} (h0 : b 0 = 0 ∧ b 1 = 0 ∧ b 2 = 0) (d : ℕ) :
    seqCost ⊤ b d = b d := by
  unfold seqCost
  by_cases hd : d ≤ 2
  · simp only [hd, ↓reduceIte]
    interval_cases d
    · exact h0.1.symm
    · exact h0.2.1.symm
    · exact h0.2.2.symm
  · simp only [hd, le_top, ↓reduceIte]

theorem degreeWeight_seqCost_top {b : ℕ → ℝ} (h0 : b 0 = 0 ∧ b 1 = 0 ∧ b 2 = 0) {n : ℕ}
    (G : SimpleGraph (Fin n)) : degreeWeight G (seqCost ⊤ b) = degreeWeight G b := by
  classical
  unfold degreeWeight
  exact Finset.sum_congr rfl fun v _ => seqCost_top_eq h0 _

/-- (A4) from the children. -/
theorem bootstrapLemma_of (hBS : TargetBootSeq) (hext : ExtensionClaim)
    (hboot : BootstrapKClaim) : TargetBootstrapLemma := by
  intro k a hseed hbase
  have hk : 3 ≤ k := hseed.1
  have hP := hext k a hseed
  have hb := hboot k (bootstrapSeq k a) hP (by
    intro ε hε
    obtain ⟨N, hN⟩ := hbase ε hε
    refine ⟨N, fun n hn G hmin hmax => ?_⟩
    rw [← degreeWeight_seqCost_eq_boot hBS hk G hmin hmax]
    exact hN n hn G hmin hmax)
  refine ⟨le_top, fun ε hε => ?_⟩
  obtain ⟨N, hN⟩ := hb ε hε
  refine ⟨N, fun n hn G => ?_⟩
  rw [degreeWeight_seqCost_top hP.zero G]
  exact hN n hn G

theorem monotone_of_bootPropsK {k : ℕ} {b : ℕ → ℝ} (hP : BootPropsK k b) : Monotone b := by
  refine monotone_nat_of_le_succ fun d => ?_
  by_cases hd : 2 ≤ d
  · simpa using hP.mono (d + 1) (by omega)
  · obtain ⟨h0, h1, h2⟩ := hP.zero
    interval_cases d
    · rw [h0, h1]
    · rw [h1, h2]

/-- (A5) Lemma 2 from the children. -/
theorem lemma2_of (hBS : TargetBootSeq) (hext : ExtensionClaim) (hboot : BootstrapKClaim) :
    TargetLemma2 := by
  intro k a hseed hpw
  have hP := hext k a hseed
  refine ⟨bootstrapLemma_of hBS hext hboot k a hseed (fun ε hε => ?_),
    monotone_of_bootPropsK hP, hP.le_one⟩
  obtain ⟨N, hN⟩ := hpw.2 ε hε
  exact ⟨N, fun n hn G _ _ => hN n hn G⟩

/-- A seed with a base bound on graphs of minimum degree `3` is a pathwidth sequence:
the bootstrap is one, and it is entrywise at most the seed's cost. -/
theorem pathwidthSequence_of_base (hBS : TargetBootSeq) (hext : ExtensionClaim)
    (hboot : BootstrapKClaim) (hmono : TargetMono) {k : ℕ} {a : ℕ → ℝ} (hseed : SeedHyp k a)
    (hbase : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasMinDegreeAtLeast 3 G → MaxDegreeAtMost k G →
        HasPathwidthAtMost G (degreeWeight G (seqCost k a) + ε * (n : ℝ))) :
    PathwidthSequence (k : ℕ∞) a := by
  have hk : 3 ≤ k := hseed.1
  have h := bootstrapLemma_of hBS hext hboot k a hseed hbase
  have hP := hext k a hseed
  have hk' : (3 : ℕ∞) ≤ (k : ℕ∞) := by exact_mod_cast hk
  refine hmono ⊤ k (bootstrapSeq k a) a hk' (fun d hd => ?_) h
  rw [seqCost_top_eq hP.zero d]
  unfold seqCost
  simp only [show ¬ d ≤ 2 by omega, ↓reduceIte]
  by_cases hdk : d ≤ k
  · have hdk' : ((d : ℕ) : ℕ∞) ≤ (k : ℕ∞) := by exact_mod_cast hdk
    simp only [hdk', ↓reduceIte, (hBS k a hk).2.1 d hd hdk, le_refl]
  · have hdk' : ¬ ((d : ℕ) : ℕ∞) ≤ (k : ℕ∞) := by exact_mod_cast hdk
    simp only [hdk', ↓reduceIte]
    exact hP.le_one d

/-! ## The bases -/

/-- A degree-weight with constant cost `c` on all vertices. -/
theorem degreeWeight_const_of_range {k : ℕ} {a : ℕ → ℝ} {c : ℝ} {n : ℕ}
    (G : SimpleGraph (Fin n)) (hmin : HasMinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost k G)
    (hc : ∀ d : ℕ, 3 ≤ d → d ≤ k → seqCost k a d = c) :
    degreeWeight G (seqCost k a) = c * (n : ℝ) := by
  classical
  unfold degreeWeight
  unfold HasMinDegreeAtLeast at hmin
  unfold MaxDegreeAtMost at hmax
  rw [Finset.sum_congr rfl fun v _ => hc _ (by convert hmin v) (by convert hmax v)]
  simp [mul_comm]

theorem seqCost_const {k : ℕ} {c : ℝ} (d : ℕ) (h3 : 3 ≤ d) (hk : d ≤ k) :
    seqCost k (fun _ => c) d = c := by
  have hk' : ((d : ℕ) : ℕ∞) ≤ (k : ℕ∞) := by exact_mod_cast hk
  simp only [seqCost, show ¬ d ≤ 2 by omega, hk', ↓reduceIte]

theorem baseC (ε : ℝ) (hε : 0 < ε) : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
    HasMinDegreeAtLeast 3 G → MaxDegreeAtMost 3 G →
      HasPathwidthAtMost G (degreeWeight G (seqCost 3 seqC) + ε * (n : ℝ)) := by
  obtain ⟨N, hN⟩ := C3.c3MainClaim.2 ε hε
  refine ⟨N, fun n hn G hmin hmax => ?_⟩
  have hsub : IsSubcubic G := by
    classical
    unfold IsSubcubic
    unfold MaxDegreeAtMost at hmax
    intro v
    convert hmax v
  have hw := degreeWeight_const_of_range (k := 3) (a := seqC) (c := C3.c3) G hmin hmax
    (fun d h3 hk => seqCost_const d h3 hk)
  simp only [Nat.cast_ofNat] at hw
  rw [hw]
  have := hN n hn G hsub
  rwa [add_mul] at this

theorem baseF (h1 : SimplexFourClaim) (ε : ℝ) (hε : 0 < ε) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasMinDegreeAtLeast 3 G → MaxDegreeAtMost 4 G →
        HasPathwidthAtMost G (degreeWeight G (seqCost 4 seqF) + ε * (n : ℝ)) := by
  obtain ⟨N, hN⟩ := T2.target2a h1 ε hε
  refine ⟨N, fun n hn G hmin hmax => ?_⟩
  have hw := degreeWeight_const_of_range (k := 4) (a := seqF) (c := F4) G hmin hmax
    (fun d h3 hk => seqCost_const d h3 hk)
  simp only [Nat.cast_ofNat] at hw
  rw [hw]
  have := hN n hn G hmax
  rwa [add_mul] at this

/-- For maximum degree 5, the cost of a triple is the degree-count sum. -/
theorem degreeWeight_coeff_of_maxDeg5 (a₃ a₄ a₅ : ℝ) {n : ℕ} (G : SimpleGraph (Fin n))
    (h5 : MaxDegreeAtMost 5 G) :
    degreeWeight G (seqCost 5 (coeff a₃ a₄ a₅)) =
      a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
        a₅ * (degreeCount G 5 : ℝ) := by
  classical
  unfold degreeWeight degreeCount
  unfold MaxDegreeAtMost at h5
  have key : ∀ v : Fin n, seqCost 5 (coeff a₃ a₄ a₅) (G.degree v) =
      a₃ * (if G.degree v = 3 then 1 else 0) + a₄ * (if G.degree v = 4 then 1 else 0)
        + a₅ * (if G.degree v = 5 then 1 else 0) := by
    intro v
    have hv : G.degree v ≤ 5 := by convert h5 v
    interval_cases h : G.degree v <;> simp [seqCost, coeff] <;> norm_num
  rw [Finset.sum_congr rfl fun v _ => key v]
  simp only [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_boole]

theorem baseTriple {a₃ a₄ a₅ : ℝ} (h : UniformDegreeCountBound5 a₃ a₄ a₅) (ε : ℝ)
    (hε : 0 < ε) : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasMinDegreeAtLeast 3 G → MaxDegreeAtMost 5 G →
        HasPathwidthAtMost G (degreeWeight G (seqCost 5 (coeff a₃ a₄ a₅)) + ε * (n : ℝ)) := by
  obtain ⟨N, hN⟩ := h ε hε
  refine ⟨N, fun n hn G _ hmax => ?_⟩
  rw [degreeWeight_coeff_of_maxDeg5 a₃ a₄ a₅ G hmax]
  exact hN n hn G hmax

/-! ## Theorem 1 from the children -/

section
variable (hBS : TargetBootSeq) (hext : ExtensionClaim) (hboot : BootstrapKClaim)
  (hmono : TargetMono) (hseeds : TargetSeedHyps)
include hBS hext hboot hmono hseeds

theorem thm1C_of : TargetThm1C :=
  pathwidthSequence_of_base hBS hext hboot hmono hseeds.1 baseC

theorem thm1F_of : TargetThm1F := fun h1 =>
  pathwidthSequence_of_base hBS hext hboot hmono hseeds.2.1 (baseF h1)

theorem thm1P_of : TargetThm1P := fun h =>
  pathwidthSequence_of_base hBS hext hboot hmono hseeds.2.2.1 (baseTriple (target3P h))

theorem thm1R_of : TargetThm1R := fun h =>
  pathwidthSequence_of_base hBS hext hboot hmono hseeds.2.2.2.1 (baseTriple (target3R h))

theorem thm1S_of : TargetThm1S := fun h =>
  pathwidthSequence_of_base hBS hext hboot hmono hseeds.2.2.2.2 (baseTriple (target3S h))

end

end PwSeq
end CubicPathwidth

#print axioms CubicPathwidth.PwSeq.lemma2_of
#print axioms CubicPathwidth.PwSeq.thm1C_of
#print axioms CubicPathwidth.PwSeq.thm1P_of