Suppressing path vertices in forests

Suppressing an independent family of vertices preserves reachability between all surviving vertices. If the original graph is a forest and every removed vertex has degree at most two, the result is again a forest. Thus a tree remains a tree whenever at least one vertex survives. Isolated vertices and leaves are allowed among the removed vertices. If the surviving vertices are independent as well, the removed degree-two vertices correspond bijectively to the surviving edges.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.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

Suppressing independent vertices preserves exactly the reachability between survivors.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.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

A connected graph remains connected when an independent set is suppressed and at least one vertex survives.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.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

Suppressing vertices of degree at most two in a forest cannot create a cycle.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.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

Suppressing independent vertices of degree at most two in a tree leaves a tree, provided at least one vertex survives.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.exists_connection_equiv {V : Type} (B : SimpleGraph V) (S : Finset V) [Fintype V] (forest : B.IsAcyclic) (independent : ∀ u ∈ S, ∀ v ∈ S, ¬B.Adj u v) (coreIndependent : ∀ u ∉ S, ∀ v ∉ S, ¬B.Adj u v) (degree : ∀ v ∈ S, B.degree v ≤ 2) : ∃ (f : ↥({v ∈ S | B.degree v = 2}) ≃ ↑(graph B S).edgeSet), ∀ (x : ↥({v ∈ S | B.degree v = 2})), ∃ (u : { v : V // v ∉ S }) (v : { v : V // v ∉ S }), ↑(f x) = s(u, v) ∧ B.Adj ↑u ↑x ∧ B.Adj ↑x ↑v

In a bipartite forest, suppressing one side of degree at most two gives one distinct edge for each removed degree-two vertex, with its original neighbors.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.edge_ncard_eq_degree_two {V : Type} (B : SimpleGraph V) (S : Finset V) [Fintype V] (forest : B.IsAcyclic) (independent : ∀ u ∈ S, ∀ v ∈ S, ¬B.Adj u v) (coreIndependent : ∀ u ∉ S, ∀ v ∉ S, ¬B.Adj u v) (degree : ∀ v ∈ S, B.degree v ≤ 2) : (graph B S).edgeSet.ncard = {v ∈ S | B.degree v = 2}.card

The suppressed graph has exactly as many edges as there are removed degree-two vertices, when both sides of the original forest are independent.