CubicPathwidth.T4.Defs

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

import CubicPathwidth.T4Spec

/-!
# Plan interfaces for Theorem 4 and Corollary 5 (not the approval surface)

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

* `sigma`: the bootstrap sequence of the triple `S` (`eq:bootstrap-rec` with `k = 5`),
  written through its closed recurrence `d σ_d = (d-2) σ_{d-1} + σ_{d-2} + 1` for
  `d ≥ 7` (Lemma 9.7, `lem:concave`); `SeqClaim` (E1) states the facts the proof needs.
* `BootProps b`: the properties of a coefficient sequence used by the bootstrap
  lemma with base degree `5` (`lem:extension`, identity Equation (9.2) (`eq:bootstrap-identity`)).
* `BootstrapClaim` (E2–E5): Lemma 9.3 (`lem:bootstrap`) with `k = 5`.
* `Cor5Claim` (E6): Corollary 5 from Theorem 4.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2 T3

/-! ## The sequence -/

/-- The bootstrap sequence of `S = (5/32, 1/4, 11/32)`. -/
def sigma : ℕ → ℝ
  | 0 => 0
  | 1 => 0
  | 2 => 0
  | 3 => 5 / 32
  | 4 => 1 / 4
  | 5 => 11 / 32
  | 6 => 7 / 16
  | (d + 7) => (((d : ℝ) + 5) * sigma (d + 6) + sigma (d + 5) + 1) / ((d : ℝ) + 7)

/-- Increment `h_d = b_d - b_{d-1}`. -/
def incr (b : ℕ → ℝ) (d : ℕ) : ℝ := b d - b (d - 1)

/-- Running minimum `H_d = min_{3 ≤ i ≤ d} h_i` (`H_d = h_3` for `d ≤ 3`). -/
def runMin (b : ℕ → ℝ) : ℕ → ℝ
  | 0 => incr b 3
  | 1 => incr b 3
  | 2 => incr b 3
  | 3 => incr b 3
  | (d + 4) => min (runMin b (d + 3)) (incr b (d + 4))

/-- Properties of a coefficient sequence used by the bootstrap lemma, base degree 5. -/
structure BootProps (b : ℕ → ℝ) : Prop where
  zero : b 0 = 0 ∧ b 1 = 0 ∧ b 2 = 0
  mono : ∀ d : ℕ, 3 ≤ d → b (d - 1) ≤ b d
  identity : ∀ d : ℕ, 6 ≤ d → 1 - b d = ((d : ℝ) - 1) * runMin b d + runMin b (d - 1)
  le_one : ∀ d : ℕ, b d ≤ 1

/-- (E1) The facts about `sigma` that the proof uses. -/
def SeqClaim : Prop :=
  BootProps sigma ∧ ∀ d : ℕ, sigma d ≤ thm4Coeff d

/-! ## The bootstrap lemma with base degree 5 -/

/-- (E2–E5) Lemma 9.3 (`lem:bootstrap`) with `k = 5`: a uniform bound for maximum degree 5
extends to all graphs. -/
def BootstrapClaim : Prop :=
  ∀ b : ℕ → ℝ, BootProps b →
    (∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      MaxDegreeAtMost 5 G → HasPathwidthAtMost G (degreeWeight G b + ε * n)) →
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasPathwidthAtMost G (degreeWeight G b + ε * n)

/-! ## Corollary 5 -/

/-- (E6) Corollary 5 from Theorem 4. -/
def Cor5Claim : Prop := Theorem4 → Corollary5

end T4
end CubicPathwidth
Back to top