CubicPathwidth.T4.Basic

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

import CubicPathwidth.T4.ProcessDefs
import CubicPathwidth.T4.BasicPsi
import CubicPathwidth.T4.BasicGlue
import CubicPathwidth.T4.BasicComp

/-!
# The children `basicClaim` (E3): the potential and the first case of Lemma 9.11 (`lem:basic`)

In the paper: the paragraph
"The potential" and Lemma 9.11 (`lem:basic`), and the bullet "The final graph" in the proof of
Lemma 9.3 (`lem:bootstrap`).

* `psiClaim` (`BasicPsi.lean`): `0 ≤ ψ⁻ ≤ ψ` when every core vertex has torso degree
  at least `3`. Each torso component contributes `ψ(C) - H_{δ(C)} ≥ 0`.
* `componentClaim` (`BasicComp.lean`): the pathwidth of the torso is at most
  `max (ψ⁻ + b₃ + ε n + N₀) q`, obtained by gluing the sections of the components
  (`BasicGlue.lean`).

The proof assumes nothing beyond the definitions in `ProcessDefs.lean`.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

/-- (E3) Lemma 9.11 (`lem:basic`) (first case) and the facts about `ψ⁻`. -/
theorem basicClaim : BasicClaim :=
  ⟨BasicAux.psiClaim, BasicAux.componentClaim⟩

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.basicClaim