CubicPathwidth.T2.TargetBC

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

Statements of the paper formalised here: Theorem 7.1.

import CubicPathwidth.T2.AssemblyB
import CubicPathwidth.T2.LayoutS
import CubicPathwidth.T2.GoodLabelsCount
import CubicPathwidth.T2.HetStar
import CubicPathwidth.T2.StarBoundCont
import CubicPathwidth.T2.Charging
import CubicPathwidth.T2.PhiTail
import CubicPathwidth.T2.FcubicBounds
import CubicPathwidth.T2.DegreeLabelsCut
import CubicPathwidth.T2.Reduction

/-!
# Theorem 2(b) and 2(c), conditional on the labels and reduction claims

Every other child is supplied by a proved theorem.
-/

namespace CubicPathwidth
namespace T2

theorem target2b_of (hL : DegreeLabelsClaim) (hred : ReductionClaim) : Target2b := fun hadm =>
  countBound_of_children plainLayout_s hred (by linarith [Fcubic_ge]) Fcubic_le
    (goodLabelsCount_of hL hetStar starBoundCont charging hadm
      (four_Phi_neg_three_le.trans Fcubic_ge) Fcubic_le)

theorem target2c_of (hL : DegreeLabelsClaim) (hred : ReductionClaim) : Target2c := fun hadm =>
  countBound_of_children plainLayout_s hred (by norm_num) (by norm_num)
    (goodLabelsCount_of hL hetStar starBoundCont charging hadm
      (four_Phi_neg_three_le.trans (by norm_num)) (by norm_num))

/-- **Theorem 2(b)**, the approved target `Target2b`. -/
theorem target2b : Target2b := target2b_of degreeLabels_cut reduction

/-- **Theorem 2(c)**, the approved target `Target2c`. -/
theorem target2c : Target2c := target2c_of degreeLabels_cut reduction

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.target2b_of
#print axioms CubicPathwidth.T2.target2c_of
#print axioms CubicPathwidth.T2.target2b
#print axioms CubicPathwidth.T2.target2c