Reserving cycle rank for untouched cyclic components

Each cyclic connected component needs at least one edge beyond a spanning tree. Reachability-preserving deletions and untouched cyclic components therefore use disjoint portions of the original cycle rank. In the thin-path argument, paths are shaded only inside large components, leaving every small cyclic component available for this reservation.

theorem Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.card_vertices_add_cyclic_le {V : Type} [Fintype V] (B : SimpleGraph V) (cyclic : Finset B.ConnectedComponent) (cycles : ∀ C ∈ cyclic, ¬C.toSimpleGraph.IsAcyclic) : Fintype.card V + cyclic.card ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent

theorem Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.card_removed_add_untouched_cyclic_le {V : Type} [Fintype V] (B : SimpleGraph V) (removed : Finset (Sym2 V)) (edges : removed ⊆ B.edgeFinset) (reachable : (B.deleteEdges ↑removed).Reachable = B.Reachable) (cyclic : Finset B.ConnectedComponent) (cycles : ∀ C ∈ cyclic, ¬C.toSimpleGraph.IsAcyclic) (kept : ∀ C ∈ cyclic, ∀ {u v : V}, u ∈ C.supp → v ∈ C.supp → B.Adj u v → s(u, v) ∉ removed) : removed.card + cyclic.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent