CubicPathwidth.T3.Targets

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

Statements of the paper formalised here: Theorem 7.2.

import CubicPathwidth.T3.Assembly
import CubicPathwidth.T3.Constants
import CubicPathwidth.T3.Charging5
import CubicPathwidth.T3.PhiTail5
import CubicPathwidth.T3.Reduction5
import CubicPathwidth.T3.DegreeLabels5
import CubicPathwidth.T3.GoodLabelsCount5
import CubicPathwidth.T2.LayoutS
import CubicPathwidth.T2.HetStar
import CubicPathwidth.T2.StarBoundCont

/-!
# Theorem 3 (maximum degree 5): the three approved targets

`target3P : Target3P`, `target3R : Target3R`, `target3S : Target3S`.
-/

namespace CubicPathwidth
namespace T3

open T2

theorem countBound5 {a₃ a₄ a₅ : ℝ} (hadm : AdmissibleTriple a₃ a₄ a₅)
    (htail : 5 * Phi (-3) ≤ a₃) (h34 : a₃ ≤ a₄) (h45 : a₄ ≤ a₅) :
    UniformDegreeCountBound5 a₃ a₄ a₅ :=
  countBound5_of_children plainLayout_s reduction5 goodLabelsCount5_step degreeLabels5
    hetStar starBoundCont charging5 hadm htail h34 h45
    (le_trans (mul_nonneg (by norm_num) (by unfold Phi; exact MeasureTheory.measureReal_nonneg)) htail)

/-- **Theorem 3 with the triple `P`**, the approved target `Target3P`. -/
theorem target3P : Target3P := fun hadm =>
  countBound5 hadm tail_P triple_P_mono.1 triple_P_mono.2

/-- **Theorem 3 with the triple `R`**, the approved target `Target3R`. -/
theorem target3R : Target3R := fun hadm =>
  countBound5 hadm tail_R (by norm_num) (by norm_num)

/-- **Theorem 3 with the triple `S`**, the approved target `Target3S`. -/
theorem target3S : Target3S := fun hadm =>
  countBound5 hadm tail_S (by norm_num) (by norm_num)

end T3
end CubicPathwidth

#check (CubicPathwidth.T3.target3P : CubicPathwidth.T3.Target3P)
#check (CubicPathwidth.T3.target3R : CubicPathwidth.T3.Target3R)
#check (CubicPathwidth.T3.target3S : CubicPathwidth.T3.Target3S)
#print axioms CubicPathwidth.T3.target3P
#print axioms CubicPathwidth.T3.target3R
#print axioms CubicPathwidth.T3.target3S