CubicPathwidth.T2.TargetA

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

Statements of the paper formalised here: Theorem 1.1, Theorem 7.1.

import CubicPathwidth.T2.AssemblyA
import CubicPathwidth.T2.LayoutS
import CubicPathwidth.T2.GoodLabels4
import CubicPathwidth.T2.IdealLimit
import CubicPathwidth.T2.StarFour
import CubicPathwidth.T2.Slepian
import CubicPathwidth.T2.Bridge

/-!
# Theorem 2(a), conditional on the bridge lemma

Every child of `theorem2a_of_children` is supplied by a proved theorem, except
`BridgeClaim`, which is taken as an explicit hypothesis here.
-/

namespace CubicPathwidth
namespace T2

theorem target2a_of_bridge (hb : BridgeClaim) : Target2a := fun h1 =>
  theorem2a_of_children plainLayout_s
    (goodLabels4_of_star (starFour_of slepian hb h1)) (idealLimit_of_bridge hb)

/-- **Theorem 2(a)**, the approved target `Target2a`: hypothesis H1 implies
`pw(G) ≤ F₄ n + o(n)` uniformly over graphs of maximum degree at most 4. -/
theorem target2a : Target2a := target2a_of_bridge bridge

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.target2a_of_bridge
#print axioms CubicPathwidth.T2.target2a