CubicPathwidth.CutSweep.All

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

Statements of the paper formalised here: Theorem 3.1.

import CubicPathwidth.CutSweep.Assembly
import CubicPathwidth.CutSweep.Deterministic
import CubicPathwidth.CutSweep.Crossing
import CubicPathwidth.CutSweep.Sweep

/-!
# The cut sweep (Theorem 3.1, `thm:cut-sweep`)

Checked (standard axioms only): N1 `constantClaim`, L1 `layoutClaim`,
L2 `orderingClaim`, G2 `crossingClaim`, C1–C2 `sweepClaim_of_crossing`, and the
parent `cutSweepClaim_of_children`. Together they give `cutSweep : CutSweepClaim`,
the approved statement of `CutSweepSpec.lean`.
-/

namespace CubicPathwidth.CutSweep

/-- Theorem 3.1 (`thm:cut-sweep`): `pw ≤ cw ≤ c_* n + o(n)` for maximum degree three, with
`c_* = (3/(2π)) arcsin(1/3) < 1/6`. -/
theorem cutSweep : CutSweepClaim :=
  cutSweepClaim_of_children constantClaim layoutClaim orderingClaim
    (sweepClaim_of_crossing crossingClaim)

end CubicPathwidth.CutSweep

#print axioms CubicPathwidth.CutSweep.cutSweep