Assembly across a graph cut #
The two side decompositions meet the decomposition on their vertex boundaries. Their three bag sequences concatenate without enlarging bags. This is the assembly step in Fomin and Høie's Theorem 5.
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_between_cutBoundaries
{W : Type}
[Fintype W]
(H : SimpleGraph W)
(S : Finset W)
:
let T := {w : W | w ∈ cutBoundary H S ∨ w ∈ cutBoundary H Sᶜ};
∃ (D : PathDecomposition (SimpleGraph.induce T H)),
D.StartsAt (Finset.subtype (fun (x : W) => x ∈ T) (cutBoundary H S)) ∧ D.EndsAt (Finset.subtype (fun (x : W) => x ∈ T) (cutBoundary H Sᶜ)) ∧ ∀ (i : Fin D.length), (D.bag i).card ≤ (H.cutFinset S).card + 1
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_assemble_cut
{W : Type}
[Fintype W]
(H : SimpleGraph W)
(S : Finset W)
(DL : PathDecomposition (SimpleGraph.induce {w : W | w ∈ S} H))
(DM : PathDecomposition (SimpleGraph.induce {w : W | w ∈ cutBoundary H S ∨ w ∈ cutBoundary H Sᶜ} H))
(DR : PathDecomposition (SimpleGraph.induce {w : W | w ∉ S} H))
(leftEnd : DL.EndsAt (Finset.subtype (fun (x : W) => x ∈ S) (cutBoundary H S)))
(middleStart :
DM.StartsAt (Finset.subtype (fun (w : W) => w ∈ cutBoundary H S ∨ w ∈ cutBoundary H Sᶜ) (cutBoundary H S)))
(middleEnd : DM.EndsAt (Finset.subtype (fun (w : W) => w ∈ cutBoundary H S ∨ w ∈ cutBoundary H Sᶜ) (cutBoundary H Sᶜ)))
(rightStart : DR.StartsAt (Finset.subtype (fun (x : W) => x ∉ S) (cutBoundary H Sᶜ)))
{b : ℕ}
(leftBound : ∀ (i : Fin DL.length), (DL.bag i).card ≤ b)
(middleBound : ∀ (i : Fin DM.length), (DM.bag i).card ≤ b)
(rightBound : ∀ (i : Fin DR.length), (DR.bag i).card ≤ b)
: