CubicPathwidth.Sw4.Targets

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

Statements of the paper formalised here: Theorem 8.2, Theorem 9.2.

import CubicPathwidth.Sw4.Assembly
import CubicPathwidth.Sw4.Layout4
import CubicPathwidth.Sw4.PsiLower
import CubicPathwidth.Sw4.ZeroVertex
import CubicPathwidth.Sw4.FrontierVertex
import CubicPathwidth.Sw4.GoodLabels

/-!
# Theorem 8.2 (`thm:switched4`) and the seed `M`: the approved targets

`TargetThm62` and `TargetThm1M` of `Sw4Spec.lean`, under H6 (`SwitchMixedClaim`) and
H7 (`SwitchedChargingClaim`).
-/

namespace CubicPathwidth
namespace Sw4

/-- The base: `δ ≥ 3`, `Δ ≤ 4`, under H6 and H7. -/
theorem base_of (h6 : SwitchMixedClaim) (h7 : SwitchedChargingClaim) :
    T2.MinDegThreeBound C3.c3 aM :=
  minDegThree_of switchedLayout4
    (goodLabelsSw_of (zeroVertex_of psiLower h6) (frontierVertex_of h7))

/-- **Theorem 8.2 (`thm:switched4`).** -/
theorem targetThm62 : TargetThm62 := fun h6 h7 => theorem62_of (base_of h6 h7)

/-- **Theorem 1**, seed `M = (c₃, 0.2627)`. -/
theorem targetThm1M : TargetThm1M := fun h6 h7 => thm1M_of (base_of h6 h7)

end Sw4
end CubicPathwidth

#check (CubicPathwidth.Sw4.targetThm62 : CubicPathwidth.Sw4.TargetThm62)
#check (CubicPathwidth.Sw4.targetThm1M : CubicPathwidth.Sw4.TargetThm1M)
#print axioms CubicPathwidth.Sw4.targetThm62
#print axioms CubicPathwidth.Sw4.targetThm1M