CubicPathwidth.CutSweepSpec

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

import CubicPathwidth

/-!
# APPROVED specification: the cut sweep (`thm:cut-sweep` of the manuscript)

STATUS: approved by the author on 2026-10-29. `CutSweepClaim` below is a proposition that we DEFINE; this file
proves nothing and assumes nothing as an axiom. The proof is
`CubicPathwidth.CutSweep.cutSweep : CutSweepClaim` in `CutSweep/All.lean`,
against the pinned project library (Lean 4.34.0, mathlib
5ed2965256430c3649e86755f9576b54eca72435).


The original specification `CubicPathwidth.lean` is imported unchanged, so
`IsSubcubic`, `PathDecomposition`, `HasPathwidthAtMost` and
`bisectionCoefficient` keep their existing, already-reviewed meaning. This file
adds the cut size of a vertex set, cutwidth and one claim.

This file is the APPROVAL SURFACE. Proof-plan interfaces will live in separate
files; they may change during proof work without renewed approval, provided
this file, its imports and the trust boundary are unchanged.
-/

noncomputable section

namespace CubicPathwidth
namespace CutSweep

/-! ## 1. Cuts and cutwidth (approval surface) -/

/-- `cutSize G A` is the number of edges of `G` with exactly one end in `A`.
Each such edge is counted once, from its end in `A`: the vertex `v ∈ A`
contributes its neighbors outside `A`. The local `classical` command only
provides the decidability used by the finite count. -/
def cutSize {n : ℕ} (G : SimpleGraph (Fin n)) (A : Finset (Fin n)) : ℕ := by
  classical
  exact ∑ v ∈ A, (G.neighborFinset v \ A).card

/-- An ordering of the vertices is a bijection `σ : Fin n ≃ Fin n`; vertex `v`
is at position `σ v`. `prefixSet σ i` is the set of the first `i` vertices,
those at positions `0, …, i-1`. For `i ≥ n` it is the whole vertex set. -/
def prefixSet {n : ℕ} (σ : Fin n ≃ Fin n) (i : ℕ) : Finset (Fin n) :=
  Finset.univ.filter (fun v => ((σ v : ℕ) < i))

/-- Cutwidth at most the REAL number `w`: some ordering has every prefix cut of
size at most `w`. The prefixes with `i = 0` and `i ≥ n` have no leaving edges,
so including them changes nothing for `w ≥ 0`. The prefix `i = 0` also forces
`w ≥ 0`, so even the empty graph has cutwidth at most `w` exactly when
`w ≥ 0`. As for pathwidth, no minimization function is needed. -/
def HasCutwidthAtMost {n : ℕ} (G : SimpleGraph (Fin n)) (w : ℝ) : Prop :=
  ∃ σ : Fin n ≃ Fin n, ∀ i : ℕ, (cutSize G (prefixSet σ i) : ℝ) ≤ w

/-- The epsilon-N meaning of a universal cutwidth bound `a * n + o(n)` for
maximum degree at most three, with the quantifier order of
`UniformPathwidthBound`: `N` depends on `ε` only, never on `n` or `G`. -/
def UniformCutwidthBound (a : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ G : SimpleGraph (Fin n), IsSubcubic G →
        HasCutwidthAtMost G ((a + ε) * (n : ℝ))

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

/-- MAIN TARGET, Theorem 3.1 (`thm:cut-sweep`) of the manuscript.

`bisectionCoefficient` is `c_* = (3/(2π)) · arccos(2√2/3) ≈ 0.1622602`, defined
in the frozen `CubicPathwidth.lean`. The four conjuncts say:

1. `c_* = (3/(2π)) · arcsin(1/3)`, the form used in the manuscript;
2. `c_* < 1/6`;
3. pathwidth is at most cutwidth: for every graph on `Fin n` (any degrees) and
   every real `w`, cutwidth at most `w` implies pathwidth at most `w`;
4. `c_*` is a universal cutwidth coefficient for finite simple graphs of
   maximum degree at most three: for every `ε > 0` there is `N` such that every
   such graph on `n ≥ N` vertices has an ordering whose prefix cuts all have
   at most `(c_* + ε) * n` edges.

Naming this proposition does NOT prove it. -/
def CutSweepClaim : Prop :=
  bisectionCoefficient = (3 / (2 * Real.pi)) * Real.arcsin (1 / 3) ∧
    bisectionCoefficient < (1 : ℝ) / 6 ∧
    (∀ (n : ℕ) (G : SimpleGraph (Fin n)) (w : ℝ),
      HasCutwidthAtMost G w → HasPathwidthAtMost G w) ∧
    UniformCutwidthBound bisectionCoefficient

end CutSweep
end CubicPathwidth

/-! ## 3. Elaboration checks (not proofs of the claim)

`#check` reports a declaration's TYPE; `#print` shows its definition. Neither
proves a proposition. -/
#check CubicPathwidth.CutSweep.cutSize
#check CubicPathwidth.CutSweep.HasCutwidthAtMost
#print CubicPathwidth.CutSweep.CutSweepClaim
#print CubicPathwidth.bisectionCoefficient
#print CubicPathwidth.HasPathwidthAtMost
Back to top