Forest preservation under path suppression

Assign each removed vertex with a surviving neighbor to one such neighbor. Edges whose assigned endpoints coincide are contracted. Components of these edges contain at most one surviving vertex; the degree-two bound makes every suppressed edge an edge of the resulting bridge quotient. This embeds the suppressed graph into a forest. Projection and lifting of walks separately give exact reachability on surviving vertices.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.Internal.reachable_iff {V : Type} (B : SimpleGraph V) (S : Finset V) (independent : ∀ u ∈ S, ∀ v ∈ S, ¬B.Adj u v) {u v : { v : V // v ∉ S }} : (graph B S).Reachable u v ↔ B.Reachable ↑u ↑v

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.Internal.connected {V : Type} (B : SimpleGraph V) (S : Finset V) [Nonempty { v : V // v ∉ S }] (original : B.Connected) (independent : ∀ u ∈ S, ∀ v ∈ S, ¬B.Adj u v) : (graph B S).Connected

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.Internal.isAcyclic {V : Type} (B : SimpleGraph V) (S : Finset V) [Fintype V] (forest : B.IsAcyclic) (degree : ∀ v ∈ S, B.degree v ≤ 2) : (graph B S).IsAcyclic

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.Internal.isTree {V : Type} (B : SimpleGraph V) (S : Finset V) [Fintype V] [Nonempty { v : V // v ∉ S }] (tree : B.IsTree) (independent : ∀ u ∈ S, ∀ v ∈ S, ¬B.Adj u v) (degree : ∀ v ∈ S, B.degree v ≤ 2) : (graph B S).IsTree