CubicPathwidth.T2.AssemblyB

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

import CubicPathwidth.T2.DefsB

/-!
# Parent assembly for Theorem 2(b) and 2(c)

Conditional on the layout, good labels and reduction claims.
-/

noncomputable section

namespace CubicPathwidth
namespace T2

theorem minDegThree_of_goodLabels (hlay : PlainLayoutClaim) {a₃ a₄ : ℝ}
    (hgood : GoodLabelsCount a₃ a₄) : MinDegThreeBound a₃ a₄ := by
  intro ε hε
  obtain ⟨N, hN⟩ := hgood ε hε
  refine ⟨N, fun n hn G h3 h4 => ?_⟩
  obtain ⟨y, hy, hfr⟩ := hN n hn G h3 h4
  exact hlay n G y hy _ hfr

theorem countBound_of_children (hlay : PlainLayoutClaim) (hred : ReductionClaim)
    {a₃ a₄ : ℝ} (h0 : 0 ≤ a₃) (h34 : a₃ ≤ a₄) (hgood : GoodLabelsCount a₃ a₄) :
    UniformDegreeCountBound a₃ a₄ :=
  hred a₃ a₄ h0 h34 (minDegThree_of_goodLabels hlay hgood)

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.countBound_of_children