CubicPathwidth.T3.Assembly

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

import CubicPathwidth.T3.Defs

/-!
# Parent assembly for Theorem 3

Conditional on the children of `T3/Defs.lean` and the layout.
-/

noncomputable section

namespace CubicPathwidth
namespace T3

open T2

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

/-- All three triples at once: everything except the leaves and the inequalities
`5 Φ(-3) ≤ a₃ ≤ a₄ ≤ a₅`. -/
theorem countBound5_of_children (hlay : PlainLayoutClaim) (hred : Reduction5Claim)
    (hstep : GoodLabelsCount5Step) (hL : DegreeLabels5Claim) (hS : HetStarClaim)
    (hC : StarBoundContClaim) (hch : Charging5Claim) {a₃ a₄ a₅ : ℝ}
    (hadm : AdmissibleTriple a₃ a₄ a₅) (htail : 5 * Phi (-3) ≤ a₃) (h34 : a₃ ≤ a₄)
    (h45 : a₄ ≤ a₅) (h0 : 0 ≤ a₃) : UniformDegreeCountBound5 a₃ a₄ a₅ :=
  hred a₃ a₄ a₅ h0 h34 h45
    (minDegThree5_of_goodLabels hlay (hstep hL hS hC hch a₃ a₄ a₅ hadm htail h34 h45))

end T3
end CubicPathwidth

#print axioms CubicPathwidth.T3.countBound5_of_children