Preserving endpoint bags in graph induction

These operations implement the deletion cases of Fomin and Høie's Lemma 4 in Pathwidth of cubic graphs and exact algorithms (2006). A subset can be appended as a new last bag. A deleted vertex can be restored when all its neighbors occur in the last bag. All bounds count bag vertices, so a bound b on nonempty bags corresponds to width at most b - 1. Without a terminal neighbor condition, inserting the vertex into every bag costs at most one.

theorem Algebraic.Cutwidth.PathDecomposition.trivial_endsAt {W : Type} {H : SimpleGraph W} [Fintype W] : (trivial H).EndsAt Finset.univ

The one-bag decomposition ends in the full vertex set.

theorem Algebraic.Cutwidth.PathDecomposition.EndsAt.reverse {W : Type} {H : SimpleGraph W} {D : PathDecomposition H} {X : Finset W} (hend : D.EndsAt X) : D.reverse.StartsAt X

Reversal turns a prescribed last bag into a prescribed first bag.

theorem Algebraic.Cutwidth.PathDecomposition.StartsAt.reverse {W : Type} {H : SimpleGraph W} {D : PathDecomposition H} {X : Finset W} (hstart : D.StartsAt X) : D.reverse.EndsAt X

Reversal turns a prescribed first bag into a prescribed last bag.

theorem Algebraic.Cutwidth.PathDecomposition.StartsAt.exists_endsAt {W : Type} {H : SimpleGraph W} {D : PathDecomposition H} {X : Finset W} (hstart : D.StartsAt X) : ∃ (Y : Finset W), D.EndsAt Y

A decomposition with a first bag also has a last bag.

theorem Algebraic.Cutwidth.PathDecomposition.EndsAt.relabel {W : Type} {H : SimpleGraph W} {V : Type} {G : SimpleGraph V} {D : PathDecomposition G} {X : Finset V} (hend : D.EndsAt X) (e : G ≃g H) : (D.relabel e).EndsAt (Finset.map e.toEmbedding X)

Relabelling preserves the prescribed last bag.

theorem Algebraic.Cutwidth.PathDecomposition.StartsAt.relabel {W : Type} {H : SimpleGraph W} {V : Type} {G : SimpleGraph V} {D : PathDecomposition G} {X : Finset V} (hstart : D.StartsAt X) (e : G ≃g H) : (D.relabel e).StartsAt (Finset.map e.toEmbedding X)

Relabelling preserves the prescribed first bag.

theorem Algebraic.Cutwidth.PathDecomposition.card_relabel_bag {W : Type} {H : SimpleGraph W} {V : Type} {G : SimpleGraph V} (D : PathDecomposition G) (e : G ≃g H) (i : Fin D.length) : ((D.relabel e).bag i).card = (D.bag i).card

A graph isomorphism preserves every bag's cardinality.

theorem Algebraic.Cutwidth.PathDecomposition.EndsAt.exists_subset {W : Type} {H : SimpleGraph W} {D : PathDecomposition H} {X Y : Finset W} (hend : D.EndsAt Y) (hXY : X ⊆ Y) {b : ℕ} (bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b) : ∃ (D' : PathDecomposition H), D'.EndsAt X ∧ ∀ (i : Fin D'.length), (D'.bag i).card ≤ b

Appending a subset of the terminal bag preserves the bag-size bound.

theorem Algebraic.Cutwidth.PathDecomposition.exists_restoreVertex {W : Type} {H : SimpleGraph W} (v : W) (D : PathDecomposition (SimpleGraph.induce {w : W | w ≠ v} H)) {Y : Finset { w : W // w ≠ v }} (hend : D.EndsAt Y) (neighbors : ∀ (w : W), H.Adj v w → w ∈ Finset.map (Function.Embedding.subtype fun (x : W) => x ≠ v) Y) {b : ℕ} (bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b) (hY : Y.card + 1 ≤ b) : ∃ (D' : PathDecomposition H), D'.EndsAt (insert v (Finset.map (Function.Embedding.subtype fun (x : W) => x ≠ v) Y)) ∧ ∀ (i : Fin D'.length), (D'.bag i).card ≤ b

Restore a deleted vertex in a new last bag. The last bag before restoration must contain every neighbor; no other bag grows.

theorem Algebraic.Cutwidth.PathDecomposition.exists_endsAt_of_delete {W : Type} {H : SimpleGraph W} (v : W) {X Y : Finset W} (hv : v ∈ Y) (D : PathDecomposition (SimpleGraph.induce {w : W | w ≠ v} H)) (hend : D.EndsAt (Finset.subtype (fun (x : W) => x ≠ v) Y)) (neighbors : ∀ (w : W), H.Adj v w → w ∈ Y) (hXY : X ⊆ Y) {b : ℕ} (bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b) (hY : Y.card ≤ b) : ∃ (D' : PathDecomposition H), D'.EndsAt X ∧ ∀ (i : Fin D'.length), (D'.bag i).card ≤ b

Delete a boundary vertex, then restore it and shrink the endpoint bag. For the zero-neighbor case use Y = X; for a unique outside neighbor u, use Y = insert u X. Only the new bag Y must fit the size bound.

theorem Algebraic.Cutwidth.PathDecomposition.exists_addVertex {W : Type} {H : SimpleGraph W} (v : W) (D : PathDecomposition (SimpleGraph.induce {w : W | w ≠ v} H)) {b : ℕ} (bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b) : ∃ (D' : PathDecomposition H), D'.EndsAt {v} ∧ ∀ (i : Fin D'.length), (D'.bag i).card ≤ b + 1

Insert a deleted vertex into every bag, then append its singleton. This costs at most one vertex per bag and needs no condition on its neighbors.