CubicPathwidth.T4Spec

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

import CubicPathwidth.T3Spec

/-!
# APPROVED specification: Theorem 1.3 (`thm:main`) (all graphs) and Corollary 1.4 (`cor:edges`) (edges)

STATUS: approved by the author on 2026-10-09. 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 `target4`, `target5` in `T4/Targets.lean`.


It imports the approved specifications `T3Spec.lean` and (through it) `T2Spec.lean`
unchanged, and reuses `HasPathwidthAtMost`, `AdmissibleTriple`.

Statements:
* Theorem 1.3 (`thm:main`): for every graph `G`,
  `pw(G) ≤ ∑_{d=3}^{6} (3d-4)/32 · n_d + ∑_{d=7}^{10} (1 - 111/(28(d+1))) · n_d
          + ∑_{d≥11} (1 - 4/(d+1)) · n_d + o(n)`;
  this implies the weaker form with `1 - 111/(28(d+1))` for all `d ≥ 7`, because
  `4 ≥ 111/28`;
* Corollary 1.4 (`cor:edges`): for every graph `G`, `pw(G) ≤ (7/48) m + o(m)`.

This file is the APPROVAL SURFACE.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T3

/-! ## 1. Coefficients and the vertex-weighted sum -/

/-- The coefficient `a_d` of degree `d` in Theorem 1.3 (`thm:main`):
`0` for `d ≤ 2`, `(3d-4)/32` for `3 ≤ d ≤ 6`, `1 - 111/(28(d+1))` for `7 ≤ d ≤ 10`, and
`1 - 4/(d+1)` for `d ≥ 11`. -/
def thm4Coeff (d : ℕ) : ℝ :=
  if d ≤ 2 then 0
  else if d ≤ 6 then (3 * (d : ℝ) - 4) / 32
  else if d ≤ 10 then 1 - 111 / (28 * ((d : ℝ) + 1))
  else 1 - 4 / ((d : ℝ) + 1)

/-- `∑_v a(d(v)) = ∑_d a_d n_d`. -/
def degreeWeight {n : ℕ} (G : SimpleGraph (Fin n)) (a : ℕ → ℝ) : ℝ := by
  classical
  exact ∑ v : Fin n, a (G.degree v)

/-- `m = |E(G)|`. -/
def edgeCount {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ := by
  classical
  exact G.edgeFinset.card

/-! ## 2. The headline claims (approval surface) -/

/-- Theorem 1.3 (`thm:main`), uniformly over ALL finite simple graphs: for every `ε > 0` there is
`N` such that every graph on `n ≥ N` vertices has pathwidth at most
`∑_v thm4Coeff (d(v)) + ε n`. No degree restriction. -/
def Theorem4 : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ G : SimpleGraph (Fin n),
      HasPathwidthAtMost G (degreeWeight G thm4Coeff + ε * (n : ℝ))

/-- Corollary 1.4 (`cor:edges`), uniformly in the number of edges: for every `ε > 0` there is `M`
such that every graph with at least `M` edges, on any number of vertices, has
pathwidth at most `(7/48 + ε) m`. -/
def Corollary5 : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), M ≤ edgeCount G →
    HasPathwidthAtMost G ((7 / 48 + ε) * (edgeCount G : ℝ))

/-- PROOF TARGETS: both from the admissibility of the triple
`S = (5/32, 1/4, 11/32)` (hypothesis H3 of `T3Spec.lean` at `S`). -/
def Target4 : Prop := AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) → Theorem4

def Target5 : Prop := AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) → Corollary5

end T4
end CubicPathwidth

/-! ## 3. Elaboration checks (not proofs of the claims) -/
#check CubicPathwidth.T4.Target4
#check CubicPathwidth.T4.Target5
#print CubicPathwidth.T4.Theorem4
#print CubicPathwidth.T4.Corollary5
#print CubicPathwidth.T4.thm4Coeff
Back to top