Joining the two boundaries of a graph cut

The boundary transition in Fomin and Høie's Pathwidth of cubic graphs and exact algorithms (2006), Theorem 5, has width at most the number of crossing edges. This finite lemma does not require a degree bound. It is one part of the pathwidth proof, completed in Bisection from the still unproved sharp cubic bisection theorem.

theorem Algebraic.Cutwidth.PathDecomposition.exists_between_of_crossing {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (left : ∀ u ∈ S, ∃ v ∉ S, H.Adj u v) (right : ∀ v ∉ S, ∃ u ∈ S, H.Adj u v) : ∃ (D : PathDecomposition H) (first : Fin D.length) (last : Fin D.length), (∀ (i : Fin D.length), first ≤ i ∧ i ≤ last) ∧ D.bag first = S ∧ D.bag last = Sᶜ ∧ ∀ (i : Fin D.length), (D.bag i).card ≤ (H.cutFinset S).card + 1

If every vertex has a neighbor across a cut, there is a path decomposition starting with one side and ending with the other, of width at most the cut size. Edges within either side are covered by its endpoint bag.