The cubic bisection bound

This records the conclusion of Monien and Preis's bisection theorem. Bisection.Helpful proves the sharp theorem for every positive slack.

def Algebraic.Cutwidth.BisectionBound (ξ : ℝ) (N₀ : ℕ) : Prop

The cubic bisection bound with slack ξ and threshold N₀: each simple 3-regular graph on n > N₀ vertices has a cut into sides differing in size by at most one, with at most (1/6 + ξ) n crossing edges.

Equations

• One or more equations did not get rendered due to their size.