CubicPathwidth.CutSweep.Assembly

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

import CubicPathwidth.CutSweep.Defs

/-!
# P0: the children imply `CutSweepClaim`

Fix `ε > 0`. Choose the radius `R` with `β_R < c_* + ε/2`
(`exists_radiusCoefficient_lt`), then good labels at radius `R` with error
`ε/2`; ordering by them bounds the cutwidth by `(c_* + ε) n`.
-/

noncomputable section

namespace CubicPathwidth
namespace CutSweep

theorem cutSweepClaim_of_children (hc : ConstantClaim) (hlay : LayoutClaim)
    (hord : OrderingClaim) (hsw : SweepClaim) : CutSweepClaim := by
  refine ⟨hc.1, hc.2, hlay, ?_⟩
  intro ε hε
  obtain ⟨R, hR, hβ⟩ := exists_radiusCoefficient_lt (ε / 2) (by linarith)
  obtain ⟨N, hN⟩ := hsw R hR (ε / 2) (by linarith)
  refine ⟨N, fun n hn G hG => ?_⟩
  obtain ⟨y, hy, hcount⟩ := hN n hn G hG
  refine hord n G y hy _ fun t => (hcount t).trans ?_
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  nlinarith

end CutSweep
end CubicPathwidth