CubicPathwidth.PwSeq.Targets

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

Statements of the paper formalised here: Theorem 9.2, Lemma 9.3.

import CubicPathwidth.PwSeq.Assembly
import CubicPathwidth.PwSeq.Basic
import CubicPathwidth.PwSeq.Extension
import CubicPathwidth.PwSeq.Seeds
import CubicPathwidth.PwSeq.Bootstrap

/-!
# Pathwidth sequences: the approved targets

Definition 1.1 (`targetRhoForm`, `targetMono`), the bootstrap (`targetBootSeq`,
`targetBootstrapLemma`, `targetLemma2`), the seeds (`targetSeedHyps`) and Theorem 1
for `C`, `F`, `P`, `R`, `S`.
-/

namespace CubicPathwidth
namespace PwSeq

/-- (A4) Lemma 9.3 (`lem:bootstrap`) for general base degree `k`. -/
theorem targetBootstrapLemma : TargetBootstrapLemma :=
  bootstrapLemma_of targetBootSeq extension bootstrapK

/-- (A5) **Lemma 2.** -/
theorem targetLemma2 : TargetLemma2 := lemma2_of targetBootSeq extension bootstrapK

/-- (T1) **Theorem 1**, seed `C = (c₃)`. -/
theorem targetThm1C : TargetThm1C :=
  thm1C_of targetBootSeq extension bootstrapK targetMono targetSeedHyps

/-- (T1) **Theorem 1**, seed `F = (F₄, F₄)`. -/
theorem targetThm1F : TargetThm1F :=
  thm1F_of targetBootSeq extension bootstrapK targetMono targetSeedHyps

/-- (T1) **Theorem 1**, seed `P = (F₃, 0.2575, 0.3667)`. -/
theorem targetThm1P : TargetThm1P :=
  thm1P_of targetBootSeq extension bootstrapK targetMono targetSeedHyps

/-- (T1) **Theorem 1**, seed `R = (0.1455, 0.2530, 0.3600)`. -/
theorem targetThm1R : TargetThm1R :=
  thm1R_of targetBootSeq extension bootstrapK targetMono targetSeedHyps

/-- (T1) **Theorem 1**, seed `S = (5/32, 1/4, 11/32)`. -/
theorem targetThm1S : TargetThm1S :=
  thm1S_of targetBootSeq extension bootstrapK targetMono targetSeedHyps

end PwSeq
end CubicPathwidth

#check (CubicPathwidth.PwSeq.targetRhoForm : CubicPathwidth.PwSeq.TargetRhoForm)
#check (CubicPathwidth.PwSeq.targetMono : CubicPathwidth.PwSeq.TargetMono)
#check (CubicPathwidth.PwSeq.targetBootSeq : CubicPathwidth.PwSeq.TargetBootSeq)
#check (CubicPathwidth.PwSeq.targetBootstrapLemma : CubicPathwidth.PwSeq.TargetBootstrapLemma)
#check (CubicPathwidth.PwSeq.targetLemma2 : CubicPathwidth.PwSeq.TargetLemma2)
#check (CubicPathwidth.PwSeq.targetSeedHyps : CubicPathwidth.PwSeq.TargetSeedHyps)
#check (CubicPathwidth.PwSeq.targetThm1C : CubicPathwidth.PwSeq.TargetThm1C)
#check (CubicPathwidth.PwSeq.targetThm1F : CubicPathwidth.PwSeq.TargetThm1F)
#check (CubicPathwidth.PwSeq.targetThm1P : CubicPathwidth.PwSeq.TargetThm1P)
#check (CubicPathwidth.PwSeq.targetThm1R : CubicPathwidth.PwSeq.TargetThm1R)
#check (CubicPathwidth.PwSeq.targetThm1S : CubicPathwidth.PwSeq.TargetThm1S)
#print axioms CubicPathwidth.PwSeq.targetRhoForm
#print axioms CubicPathwidth.PwSeq.targetMono
#print axioms CubicPathwidth.PwSeq.targetBootSeq
#print axioms CubicPathwidth.PwSeq.targetBootstrapLemma
#print axioms CubicPathwidth.PwSeq.targetLemma2
#print axioms CubicPathwidth.PwSeq.targetSeedHyps
#print axioms CubicPathwidth.PwSeq.targetThm1C
#print axioms CubicPathwidth.PwSeq.targetThm1F
#print axioms CubicPathwidth.PwSeq.targetThm1P
#print axioms CubicPathwidth.PwSeq.targetThm1R
#print axioms CubicPathwidth.PwSeq.targetThm1S
Back to top