Locating a tree component for the endpoint induction

Fomin and Høie's Lemma 4, Case 3.A, uses the elementary fact that a finite graph with fewer edges than vertices has a connected component that is a tree. The component includes isolated vertices as one-vertex trees. If every vertex of a prescribed boundary has at least two neighbors outside it and the boundary has more than one third of the vertices, degree counting produces the required edge deficit in its complement.

The quantitative version also bounds the size of a tree component in terms of the edge deficit. It supports the small-component analysis in Monien and Preis's red/black graph argument.

theorem Algebraic.Cutwidth.exists_small_tree_component_of_edge_deficit {W : Type} [Fintype W] (H : SimpleGraph W) (M : ℕ) (deficit : (M + 1) * H.edgeFinset.card < M * Fintype.card W) : ∃ (C : H.ConnectedComponent), C.toSimpleGraph.IsTree ∧ Fintype.card ↥C ≤ M

A linear edge deficit forces a small tree component. No degree bound is required.

theorem Algebraic.Cutwidth.exists_tree_component_of_card_edgeFinset_lt {W : Type} [Fintype W] (H : SimpleGraph W) (hcard : H.edgeFinset.card < Fintype.card W) : ∃ (C : H.ConnectedComponent), C.toSimpleGraph.IsTree

A graph with fewer edges than vertices has a tree component.

theorem Algebraic.Cutwidth.complement_card_edges_lt {W : Type} [Fintype W] (H : SimpleGraph W) (X : Finset W) (degree : ∀ (v : W), H.degree v ≤ 3) (large : Fintype.card W < 3 * X.card) (outside : ∀ v ∈ X, 2 ≤ (H.neighborFinset v \ X).card) : (SimpleGraph.induce {w : W | w ∉ X} H).edgeFinset.card < Fintype.card { w : W // w ∉ X }

In a subcubic graph, a boundary larger than one third of the graph with at least two outside neighbors per boundary vertex leaves fewer edges than vertices in its complement.

theorem Algebraic.Cutwidth.exists_tree_component_complement {W : Type} [Fintype W] (H : SimpleGraph W) (X : Finset W) (degree : ∀ (v : W), H.degree v ≤ 3) (large : Fintype.card W < 3 * X.card) (outside : ∀ v ∈ X, 2 ≤ (H.neighborFinset v \ X).card) : ∃ (C : (SimpleGraph.induce {w : W | w ∉ X} H).ConnectedComponent), C.toSimpleGraph.IsTree

The tree component required by Case 3.A of Fomin and Høie's endpoint decomposition lemma exists under its degree and boundary-size conditions.

theorem Algebraic.Cutwidth.boundary_reduction {W : Type} [Fintype W] (H : SimpleGraph W) (X : Finset W) (degree : ∀ (v : W), H.degree v ≤ 3) (large : Fintype.card W < 3 * X.card) : (∃ v ∈ X, (H.neighborFinset v \ X).card ≤ 1) ∨ ∃ (C : (SimpleGraph.induce {w : W | w ∉ X} H).ConnectedComponent), C.toSimpleGraph.IsTree

The structural alternatives in the endpoint induction: a large boundary contains a vertex with at most one outside neighbor, or its complement has a tree component. Either alternative permits deleting a nonempty set of vertices.