CubicPathwidth.PwSeqSpec

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

import CubicPathwidth.T4Spec
import CubicPathwidth.C3Spec

/-!
# Specification: pathwidth sequences (`def:pw-seq`, Theorem 9.2 (`thm:pw-seq`), Lemma 9.3 (`lem:bootstrap-seq`))

STATUS: approved by the author on 2026-10-16. Every `def ... : Prop` below is a proposition that we DEFINE. Nothing here
is proved, and nothing is assumed as an axiom. This file only checks that the
definitions elaborate against the pinned project library (Lean 4.34.0, mathlib
5ed2965256430c3649e86755f9576b54eca72435).
The proofs are in `PwSeq/Basic.lean` and `PwSeq/Targets.lean`.


It imports the approved specifications `T4Spec.lean` (and through it `T3Spec.lean`,
`T2Spec.lean`) and `C3Spec.lean` unchanged, and reuses `HasPathwidthAtMost`,
`MaxDegreeAtMost`, `degreeWeight`, `c3`, `F4`, `Fcubic`, `SimplexFourClaim`, `coeff`
and `AdmissibleTriple`.

Statements (the paper):
* Definition 9.1 (`def:pw-seq`): `(a₃,…,a_k)`, `k ∈ {3,4,…} ∪ {∞}`, is a pathwidth
  sequence if some `ρ(n) = o(n)` gives, for EVERY graph,
  `pw(G) ≤ ∑_{d=3}^{k} a_d n_d + ∑_{d>k} n_d + ρ(n)`;
* Theorem 9.2 (`thm:pw-seq`): `C = (c₃)`, `F = (F₄, F₄)`, `P = (F₃, 0.2575, 0.3667)`,
  `R = (0.1455, 0.2530, 0.3600)`, `S = (5/32, 1/4, 11/32)` are pathwidth sequences;
* Lemma 9.3 (`lem:bootstrap-seq`): the bootstrap of a pathwidth sequence with
  `0 ≤ a₃ ≤ … ≤ a_k` and `a_k + H_k ≤ 1` is a pathwidth sequence, nondecreasing, `≤ 1`.
Corollary 9.5 (`cor:table`) is not formalized (decision of Serge Gaspers, 2026-10-16).

This file is the APPROVAL SURFACE.
-/

noncomputable section

open Filter Topology

namespace CubicPathwidth
namespace PwSeq

open T2 T3 T4

/-! ## 1. Pathwidth sequences (Definition 9.1, `def:pw-seq`) -/

/-- The cost of a vertex of degree `d` under the sequence `(a₃, …, a_k)`:
`0` for `d ≤ 2`, `a d` for `3 ≤ d ≤ k`, and `1` for `d > k`.
`k : ℕ∞` is a natural number or `⊤` (= `∞`); for `k = ⊤` every `d ≥ 3` costs `a d`.
The values `a 0, a 1, a 2` and `a d` for `d > k` are never used. -/
def seqCost (k : ℕ∞) (a : ℕ → ℝ) (d : ℕ) : ℝ :=
  if d ≤ 2 then 0 else if (d : ℕ∞) ≤ k then a d else 1

/-- Definition 9.1 (`def:pw-seq`), in the project's uniform `ε`–`N` form: `(a₃, …, a_k)` with `k ≥ 3`
is a pathwidth sequence if for every `ε > 0` ONE threshold `N` works for every `n ≥ N`
and EVERY simple graph on `Fin n` (no degree restriction):
`pw(G) ≤ ∑_v seqCost k a (d(v)) + ε n`. -/
def PathwidthSequence (k : ℕ∞) (a : ℕ → ℝ) : Prop :=
  3 ≤ k ∧
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasPathwidthAtMost G (degreeWeight G (seqCost k a) + ε * (n : ℝ))

/-- Definition 9.1 (`def:pw-seq`) literally: one remainder function `ρ` with `ρ(n)/n → 0`, valid for
every `n` and every graph on `Fin n`. -/
def PathwidthSequenceRho (k : ℕ∞) (a : ℕ → ℝ) : Prop :=
  3 ≤ k ∧
    ∃ ρ : ℕ → ℝ, Tendsto (fun n : ℕ => ρ n / (n : ℝ)) atTop (𝓝 0) ∧
      ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
        HasPathwidthAtMost G (degreeWeight G (seqCost k a) + ρ n)

/-! ## 2. The bootstrap (Equation (9.1), `eq:bootstrap-rec`) -/

/-- The seed read as a sequence from degree `0`: `0` at degrees `0, 1, 2`. -/
def seedSeq (a : ℕ → ℝ) (d : ℕ) : ℝ := if d ≤ 2 then 0 else a d

/-- 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` (and `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))

/-- The right side of Equation (9.1) (`eq:bootstrap-rec`) at degree `d`, from `b_{d-1}` and `H_{d-1}`:
`max ((1 + (d-1) b_{d-1} - H_{d-1}) / d) (1 - d H_{d-1})`. -/
def bootStep (d : ℕ) (bPrev HPrev : ℝ) : ℝ :=
  max ((1 + ((d : ℝ) - 1) * bPrev - HPrev) / (d : ℝ)) (1 - (d : ℝ) * HPrev)

/-- `bootPair k a d = (b_d, H_d)`: the bootstrap of `(a₃, …, a_k)` computed together
with the running minimum of its increments. `b_d = 0` for `d ≤ 2`, `b_3 = H_3 = a 3`,
`b_d = a d` for `4 ≤ d ≤ k`, `b_d = bootStep d b_{d-1} H_{d-1}` for `d > k`, and
`H_d = min H_{d-1} (b_d - b_{d-1})` for `d ≥ 4`. (The second entry at `d ≤ 2` is unused.) -/
def bootPair (k : ℕ) (a : ℕ → ℝ) : ℕ → ℝ × ℝ
  | 0 => (0, 0)
  | 1 => (0, 0)
  | 2 => (0, 0)
  | 3 => (a 3, a 3)
  | (d + 4) =>
      let p := bootPair k a (d + 3)
      let b := if d + 4 ≤ k then a (d + 4) else bootStep (d + 4) p.1 p.2
      (b, min p.2 (b - p.1))

/-- The bootstrap of `(a₃, …, a_k)`: an infinite sequence `b`, with `b_d = 0` for `d ≤ 2`. -/
def bootstrapSeq (k : ℕ) (a : ℕ → ℝ) (d : ℕ) : ℝ := (bootPair k a d).1

/-- The hypotheses of Lemma 9.3 (`lem:bootstrap-seq`) on the seed: `k ≥ 3`, `0 ≤ a₃ ≤ a₄ ≤ … ≤ a_k`, and
`a_k + H_k ≤ 1` (with `a₂ = 0`, so `h₃ = a₃`). -/
def SeedHyp (k : ℕ) (a : ℕ → ℝ) : Prop :=
  3 ≤ k ∧ 0 ≤ a 3 ∧ (∀ d : ℕ, 3 ≤ d → d < k → a d ≤ a (d + 1)) ∧
    a k + runMin (seedSeq a) k ≤ 1

/-- Every vertex has at least `k` neighbors. -/
def HasMinDegreeAtLeast {n : ℕ} (k : ℕ) (G : SimpleGraph (Fin n)) : Prop := by
  classical
  exact ∀ v : Fin n, k ≤ G.degree v

/-! ## 3. The general statements (approval surface) -/

/-- (A1) The `ε`–`N` form is Definition 9.1 (`def:pw-seq`). -/
def TargetRhoForm : Prop :=
  ∀ (k : ℕ∞) (a : ℕ → ℝ), PathwidthSequence k a ↔ PathwidthSequenceRho k a

/-- (A2) Remark after Definition 9.1 (`def:pw-seq`): a sequence whose costs are entrywise at least
those of a pathwidth sequence (entries beyond the length read as `1`) is one. -/
def TargetMono : Prop :=
  ∀ (k k' : ℕ∞) (a a' : ℕ → ℝ), 3 ≤ k' →
    (∀ d : ℕ, 3 ≤ d → seqCost k a d ≤ seqCost k' a' d) →
    PathwidthSequence k a → PathwidthSequence k' a'

/-- (A3) `bootstrapSeq` is the sequence defined by Equation (9.1) (`eq:bootstrap-rec`). -/
def TargetBootSeq : Prop :=
  ∀ (k : ℕ) (a : ℕ → ℝ), 3 ≤ k →
    (∀ d : ℕ, d ≤ 2 → bootstrapSeq k a d = 0) ∧
    (∀ d : ℕ, 3 ≤ d → d ≤ k → bootstrapSeq k a d = a d) ∧
    (∀ d : ℕ, k < d →
      bootstrapSeq k a d =
        bootStep d (bootstrapSeq k a (d - 1)) (runMin (bootstrapSeq k a) (d - 1)))

/-- (A4) Lemma 9.3 (`lem:bootstrap`) (the manuscript's internal form): a uniform bound on graphs
with minimum degree at least `3` and maximum degree at most `k` extends to all graphs
through the bootstrap. -/
def TargetBootstrapLemma : Prop :=
  ∀ (k : ℕ) (a : ℕ → ℝ), SeedHyp k a →
    (∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ G : SimpleGraph (Fin n),
      HasMinDegreeAtLeast 3 G → MaxDegreeAtMost k G →
        HasPathwidthAtMost G (degreeWeight G (seqCost k a) + ε * (n : ℝ))) →
    PathwidthSequence ⊤ (bootstrapSeq k a)

/-- (A5) Lemma 9.3 (`lem:bootstrap-seq`). -/
def TargetLemma2 : Prop :=
  ∀ (k : ℕ) (a : ℕ → ℝ), SeedHyp k a → PathwidthSequence (k : ℕ∞) a →
    PathwidthSequence ⊤ (bootstrapSeq k a) ∧ Monotone (bootstrapSeq k a) ∧
      ∀ d : ℕ, bootstrapSeq k a d ≤ 1

/-! ## 4. The five seeds and Theorem 9.2 (`thm:pw-seq`) -/

def seqC : ℕ → ℝ := fun _ => C3.c3

def seqF : ℕ → ℝ := fun _ => F4

/-- `P = (F₃, 0.2575, 0.3667)`, with `F₃ = Fcubic` exact. -/
def seqP : ℕ → ℝ := coeff Fcubic (103 / 400) (3667 / 10000)

/-- `R = (0.1455, 0.2530, 0.3600)`. -/
def seqR : ℕ → ℝ := coeff (291 / 2000) (253 / 1000) (9 / 25)

def seqS : ℕ → ℝ := coeff (5 / 32) (1 / 4) (11 / 32)

/-- (A6) All five seeds satisfy the hypotheses of Lemma 9.3 (`lem:bootstrap-seq`). -/
def TargetSeedHyps : Prop :=
  SeedHyp 3 seqC ∧ SeedHyp 4 seqF ∧ SeedHyp 5 seqP ∧ SeedHyp 5 seqR ∧ SeedHyp 5 seqS

/-- (T1) Theorem 9.2 (`thm:pw-seq`). `C` is unconditional (`thm:cubic`, `C3.c3MainClaim`); `F` uses H1
(as `T2.Target2a`); `P`, `R`, `S` use H3 at their own triple (as `T3.Target3P/R/S`). -/
def TargetThm1C : Prop := PathwidthSequence 3 seqC

def TargetThm1F : Prop := SimplexFourClaim → PathwidthSequence 4 seqF

def TargetThm1P : Prop :=
  AdmissibleTriple Fcubic (103 / 400) (3667 / 10000) → PathwidthSequence 5 seqP

def TargetThm1R : Prop :=
  AdmissibleTriple (291 / 2000) (253 / 1000) (9 / 25) → PathwidthSequence 5 seqR

def TargetThm1S : Prop :=
  AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) → PathwidthSequence 5 seqS

end PwSeq
end CubicPathwidth

/-! ## 5. Elaboration checks (not proofs of the claims) -/
#print CubicPathwidth.PwSeq.PathwidthSequence
#print CubicPathwidth.PwSeq.seqCost
#print CubicPathwidth.PwSeq.bootPair
#check CubicPathwidth.PwSeq.TargetRhoForm
#check CubicPathwidth.PwSeq.TargetMono
#check CubicPathwidth.PwSeq.TargetBootSeq
#check CubicPathwidth.PwSeq.TargetBootstrapLemma
#check CubicPathwidth.PwSeq.TargetLemma2
#check CubicPathwidth.PwSeq.TargetSeedHyps
#check CubicPathwidth.PwSeq.TargetThm1C
#check CubicPathwidth.PwSeq.TargetThm1F
#check CubicPathwidth.PwSeq.TargetThm1P
#check CubicPathwidth.PwSeq.TargetThm1R
#check CubicPathwidth.PwSeq.TargetThm1S