CubicPathwidth.Sw4.Assembly

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

import CubicPathwidth.Sw4.Defs
import CubicPathwidth.PwSeq.Targets
import CubicPathwidth.T2.Reduction

/-!
# Parent assembly for Theorem 8.2 (`thm:switched4`) and the seed `M` (Q6, Q7)

Conditional on `SwitchedLayout4Claim` and `GoodLabelsSw c₃ 0.2627`. The base on
`δ ≥ 3`, `Δ ≤ 4` comes from the layout and the labels (proof of Theorem 8.2 (`thm:switched4`), first
part); Theorem 8.2 (`thm:switched4`) follows by `T2.reduction`, and Theorem 9.2 (`thm:pw-seq`) for `M` by the general
bootstrap (`PwSeq.pathwidthSequence_of_base` with `k = 4`).
-/

noncomputable section

namespace CubicPathwidth
namespace Sw4

open T2 T3 PwSeq

/-- `c₃ < 3/20`. -/
theorem c3_lt : C3.c3 < 3 / 20 := by
  have hpi : 3 < Real.pi := Real.pi_gt_three
  have hA0 : 0 ≤ Real.arccos (5 / 6) := Real.arccos_nonneg _
  have hA1 : Real.arccos (5 / 6) < 3 / 5 := C3.arccos_five_sixths_lt
  have hq1 : 3 / (4 * Real.pi) < 1 / 4 := by
    rw [div_lt_iff₀ (by positivity)]
    linarith
  have hc : C3.c3 = 3 / (4 * Real.pi) * Real.arccos (5 / 6) := rfl
  rw [hc]
  calc 3 / (4 * Real.pi) * Real.arccos (5 / 6) ≤ 1 / 4 * Real.arccos (5 / 6) :=
        mul_le_mul_of_nonneg_right hq1.le hA0
    _ < 1 / 4 * (3 / 5) := by linarith
    _ = 3 / 20 := by norm_num

theorem c3_le_aM : C3.c3 ≤ aM := by
  have := c3_lt
  unfold aM
  linarith

/-- The seed `M` satisfies the hypotheses of Lemma 2 with `k = 4`. -/
theorem seedHyp_M : SeedHyp 4 seqM := by
  have h0 := c3_bounds.1
  have hle := c3_le_aM
  refine ⟨by norm_num, ?_, fun d hd1 hd2 => ?_, ?_⟩
  · simpa [seqM] using h0
  · interval_cases d
    simpa [seqM] using hle
  · have hmin : runMin (seedSeq seqM) 4 ≤ incr (seedSeq seqM) 4 := runMin_four_le _
    have hinc : incr (seedSeq seqM) 4 = aM - C3.c3 := by
      simp [incr, seedSeq, seqM]
    have h4 : seqM 4 = aM := by simp [seqM]
    rw [hinc] at hmin
    rw [h4]
    have : aM = 2627 / 10000 := rfl
    linarith

/-- For maximum degree 4, the cost of `M` is `c₃ n₃ + 0.2627 n₄`. -/
theorem degreeWeight_seqM {n : ℕ} (G : SimpleGraph (Fin n)) (h4 : MaxDegreeAtMost 4 G) :
    T4.degreeWeight G (seqCost 4 seqM) =
      C3.c3 * (degreeCount G 3 : ℝ) + aM * (degreeCount G 4 : ℝ) := by
  classical
  unfold T4.degreeWeight degreeCount
  unfold MaxDegreeAtMost at h4
  have key : ∀ v : Fin n, seqCost 4 seqM (G.degree v) =
      C3.c3 * (if G.degree v = 3 then 1 else 0) + aM * (if G.degree v = 4 then 1 else 0) := by
    intro v
    have hv : G.degree v ≤ 4 := by convert h4 v
    interval_cases h : G.degree v <;> (simp [seqCost, seqM]; try norm_num)
  rw [Finset.sum_congr rfl fun v _ => key v]
  simp only [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_boole]

/-- (Q6) The layout and good labels give the bound for `δ ≥ 3`, `Δ ≤ 4`. The `+1` of
the connector bound is absorbed into `ε n` for `n ≥ 2/ε`. -/
theorem minDegThree_of (hlay : SwitchedLayout4Claim) {a₃ a₄ : ℝ}
    (hgood : GoodLabelsSw a₃ a₄) : MinDegThreeBound a₃ a₄ := by
  intro ε hε
  obtain ⟨N, hN⟩ := hgood (ε / 2) (half_pos hε)
  refine ⟨max N ⌈2 / ε⌉₊, ?_⟩
  intro n hn G hmin hmax
  have hnN : N ≤ n := le_trans (le_max_left _ _) hn
  have hnε : (2 / ε : ℝ) ≤ n :=
    le_trans (Nat.le_ceil _) (by exact_mod_cast le_trans (le_max_right _ _) hn)
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  have hone : (1 : ℝ) ≤ ε / 2 * n := by
    rw [div_le_iff₀ hε] at hnε
    nlinarith
  obtain ⟨y, hy, hin, hout, hlo, hup⟩ := hN n hnN G hmin hmax
  set β := a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) with hβ
  have hmono : β + ε / 2 * n ≤ β + ε * n := by nlinarith
  apply hlay n G hmax y hy
  · intro t ht
    exact (hin t ht).trans hmono
  · intro t ht
    exact (hout t ht).trans hmono
  · have hmax' : (max (hatL0 G y) (hatL0' G y) : ℝ) ≤ β + ε / 2 * n := by
      rcases le_total (hatL0 G y) (hatL0' G y) with h | h
      · rw [max_eq_right (by exact_mod_cast h)]
        exact hup
      · rw [max_eq_left (by exact_mod_cast h)]
        exact hlo
    nlinarith

/-- (Q7) Theorem 8.2 (`thm:switched4`) from the base. -/
theorem theorem62_of (hbase : MinDegThreeBound C3.c3 aM) : Theorem62 :=
  reduction C3.c3 aM c3_bounds.1 c3_le_aM hbase

/-- (Q7) Theorem 9.2 (`thm:pw-seq`) for `M` from the base. -/
theorem thm1M_of (hbase : MinDegThreeBound C3.c3 aM) : PathwidthSequence 4 seqM := by
  have h := pathwidthSequence_of_base targetBootSeq extension bootstrapK targetMono seedHyp_M
    (k := 4) (a := seqM) ?_
  · simpa using h
  intro ε hε
  obtain ⟨N, hN⟩ := hbase ε hε
  refine ⟨N, fun n hn G hmin hmax => ?_⟩
  simp only [Nat.cast_ofNat]
  rw [degreeWeight_seqM G hmax]
  exact hN n hn G hmin hmax

end Sw4
end CubicPathwidth

#print axioms CubicPathwidth.Sw4.minDegThree_of
#print axioms CubicPathwidth.Sw4.theorem62_of
#print axioms CubicPathwidth.Sw4.thm1M_of
Back to top