CubicPathwidth.PwSeq.Defs

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

import CubicPathwidth.PwSeqSpec
import CubicPathwidth.T4.Defs

/-!
# Plan interfaces for the pathwidth-sequence targets (not the approval surface)

Every `...Claim` below is a DEFINED proposition. Theorems using one take it as an
explicit hypothesis. No axiom is introduced.

* `BootPropsK k b`: the properties of a coefficient sequence used by the bootstrap
  lemma with base degree `k` (Lemma 9.6, `lem:extension`); for `k = 5` it contains
  `T4.BootProps`.
* `ExtensionClaim` (Q2): Lemma 9.6 (`lem:extension`) for general `k`: the bootstrap of a seed
  satisfying `SeedHyp` has these properties.
* `BootstrapKClaim` (Q3): Lemma 9.3 (`lem:bootstrap`) for general `k`, with the base hypothesis on
  graphs of minimum degree at least `3` and maximum degree at most `k`.
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq

open T2 T4

/-- `PwSeq.runMin` and `T4.runMin` are the same function. -/
theorem runMin_eq_t4 (b : ℕ → ℝ) : PwSeq.runMin b = T4.runMin b := by
  funext d
  induction d using Nat.strong_induction_on with
  | _ d ih =>
    match d, ih with
    | 0, _ => rfl
    | 1, _ => rfl
    | 2, _ => rfl
    | 3, _ => rfl
    | d + 4, ih =>
      simp only [PwSeq.runMin, T4.runMin, PwSeq.incr, T4.incr]
      rw [ih (d + 3) (by omega)]

/-- Properties of a coefficient sequence used by the bootstrap lemma, base degree `k`
(`lem:extension` and the hypotheses of Lemma 9.3 (`lem:bootstrap`)). `H_d` is `T4.runMin b d`. -/
structure BootPropsK (k : ℕ) (b : ℕ → ℝ) : Prop where
  three_le : 3 ≤ k
  zero : b 0 = 0 ∧ b 1 = 0 ∧ b 2 = 0
  mono : ∀ d : ℕ, 3 ≤ d → b (d - 1) ≤ b d
  identity : ∀ d : ℕ, k + 1 ≤ d →
    1 - b d = ((d : ℝ) - 1) * T4.runMin b d + T4.runMin b (d - 1)
  budget : ∀ d : ℕ, k ≤ d → b d + T4.runMin b d ≤ 1
  runMin_nonneg : ∀ d : ℕ, 0 ≤ T4.runMin b d
  le_one : ∀ d : ℕ, b d ≤ 1

/-- (Q2) Lemma 9.6 (`lem:extension`) for general `k`. -/
def ExtensionClaim : Prop :=
  ∀ (k : ℕ) (a : ℕ → ℝ), SeedHyp k a → BootPropsK k (bootstrapSeq k a)

/-- (Q3) Lemma 9.3 (`lem:bootstrap`) for general base degree `k`: a uniform bound on graphs with
minimum degree at least `3` and maximum degree at most `k` extends to all graphs. -/
def BootstrapKClaim : Prop :=
  ∀ (k : ℕ) (b : ℕ → ℝ), BootPropsK k b →
    (∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasMinDegreeAtLeast 3 G → MaxDegreeAtMost k G →
        HasPathwidthAtMost G (degreeWeight G b + ε * n)) →
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasPathwidthAtMost G (degreeWeight G b + ε * n)

end PwSeq
end CubicPathwidth