Boundary counts for the bisection assembly

Both vertex boundaries are bounded by the number of crossing edges. Cutting an induced subgraph on the same side cannot increase that edge count.

theorem Algebraic.Cutwidth.cutFinset_compl {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) : H.cutFinset Sᶜ = H.cutFinset S

The two orientations of a cut have the same crossing edges.

theorem Algebraic.Cutwidth.card_cutBoundary_le {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) : (cutBoundary H S).card ≤ (H.cutFinset S).card

Each boundary vertex can be charged to a distinct crossing edge.

theorem Algebraic.Cutwidth.card_cutFinset_induce_le {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (T : Set W) [DecidablePred fun (x : W) => x ∈ T] [Fintype ↑T] : ((SimpleGraph.induce T H).cutFinset (Finset.subtype (fun (x : W) => x ∈ T) S)).card ≤ (H.cutFinset S).card

Inducing a graph cannot increase the number of edges crossing a fixed side.