Constructing positive red/black sets

The first two constructions in Monien and Preis's core lemma join black components by red edges, or attach three black components to a short black path. Adding a set with no black boundary cannot increase the black cut. Three internal red edges therefore suffice when the connecting set has at most two external black edges.

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.mem_internalEdges {V E : Type} [Fintype E] (R : Multigraph V E) {X : Finset V} {e : E} : e ∈ internalEdges R X ↔ R.fst e ∈ X ∧ R.snd e ∈ X

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.internalEdges_mono {V E : Type} [Fintype E] (R : Multigraph V E) {X Y : Finset V} (h : X ⊆ Y) : internalEdges R X ⊆ internalEdges R Y

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.cut_union_subset_of_empty {V : Type} [Fintype V] (B : SimpleGraph V) (X : Finset V) {Y : Finset V} (closed : B.cutFinset Y = ∅) : B.cutFinset (X ∪ Y) ⊆ B.cutFinset X

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.cut_biUnion_eq_empty {V : Type} [Fintype V] (B : SimpleGraph V) {ι : Type} (I : Finset ι) (A : ι → Finset V) (closed : ∀ i ∈ I, B.cutFinset (A i) = ∅) : B.cutFinset (I.biUnion A) = ∅

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.cut_component_eq_empty {V : Type} [Fintype V] (B : SimpleGraph V) (C : B.ConnectedComponent) : B.cutFinset C.supp.toFinset = ∅

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.positive_of_closed_edge {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {X : Finset V} (closed : B.cutFinset X = ∅) {e : E} (hfst : R.fst e ∈ X) (hsnd : R.snd e ∈ X) : Positive B R X

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_component_edge {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (C D : B.ConnectedComponent) (M : ℕ) (smallC : Fintype.card ↥C ≤ M) (smallD : Fintype.card ↥D ≤ M) {e : E} (hfst : R.fst e ∈ C.supp) (hsnd : R.snd e ∈ D.supp) : ∃ (X : Finset V), X.card ≤ 2 * M ∧ Positive B R X

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_attachments {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (P : Finset V) (edges : Finset E) (A : E → Finset V) (M : ℕ) (cut : (B.cutFinset P).card < edges.card) (closed : ∀ e ∈ edges, B.cutFinset (A e) = ∅) (small : ∀ e ∈ edges, (A e).card ≤ M) (attached : ∀ e ∈ edges, R.fst e ∈ P ∧ R.snd e ∈ A e ∨ R.snd e ∈ P ∧ R.fst e ∈ A e) : ∃ (X : Finset V), X.card ≤ P.card + edges.card * M ∧ Positive B R X

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.card_cut_le_two_of_connected {V : Type} [Fintype V] (B : SimpleGraph V) {P : Finset V} (connected : (SimpleGraph.induce {v : V | v ∈ P} B).Connected) (degree : ∀ v ∈ P, B.degree v ≤ 2) : (B.cutFinset P).card ≤ 2

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_three_attachments {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (P : Finset V) (edges : Finset E) (A : E → Finset V) (M : ℕ) (connected : (SimpleGraph.induce {v : V | v ∈ P} B).Connected) (degree : ∀ v ∈ P, B.degree v ≤ 2) (three : edges.card = 3) (closed : ∀ e ∈ edges, B.cutFinset (A e) = ∅) (small : ∀ e ∈ edges, (A e).card ≤ M) (attached : ∀ e ∈ edges, R.fst e ∈ P ∧ R.snd e ∈ A e ∨ R.snd e ∈ P ∧ R.fst e ∈ A e) : ∃ (X : Finset V), X.card ≤ P.card + 3 * M ∧ Positive B R X

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_walk_attachments {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {u v : V} (p : B.Walk u v) (edges : Finset E) (A : E → Finset V) (M : ℕ) (degree : ∀ w ∈ p.support, B.degree w ≤ 2) (three : edges.card = 3) (closed : ∀ e ∈ edges, B.cutFinset (A e) = ∅) (small : ∀ e ∈ edges, (A e).card ≤ M) (attached : ∀ e ∈ edges, R.fst e ∈ p.support ∧ R.snd e ∈ A e ∨ R.snd e ∈ p.support ∧ R.fst e ∈ A e) : ∃ (X : Finset V), X.card ≤ p.length + 1 + 3 * M ∧ Positive B R X

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_adjacent_pair_le_three_average {n : ℕ} (w : Fin (n + 2) → ℕ) : ∃ (i : Fin (n + 1)), (n + 2) * (w i.castSucc + w i.succ) ≤ 3 * ∑ j : Fin (n + 2), w j

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_three_close_positions {n : ℕ} (pos : Fin (n + 3) → ℕ) (ordered : Monotone pos) : ∃ (i : Fin (n + 1)), (n + 2) * (pos i.succ.succ - pos i.castSucc.castSucc) ≤ 3 * (pos (Fin.last (n + 2)) - pos 0)

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_thin_walk {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {u v : V} (p : B.Walk u v) {n : ℕ} (edge : Fin (n + 3) ↪ E) (pos : Fin (n + 3) → ℕ) (A : E → Finset V) (M : ℕ) (ordered : Monotone pos) (within : ∀ (i : Fin (n + 3)), pos i ≤ p.length) (degree : ∀ w ∈ p.support, B.degree w ≤ 2) (thin : p.length ≤ M * (n + 3)) (closed : ∀ (i : Fin (n + 3)), B.cutFinset (A (edge i)) = ∅) (small : ∀ (i : Fin (n + 3)), (A (edge i)).card ≤ M) (attached : ∀ (i : Fin (n + 3)), R.fst (edge i) = p.getVert (pos i) ∧ R.snd (edge i) ∈ A (edge i) ∨ R.snd (edge i) = p.getVert (pos i) ∧ R.fst (edge i) ∈ A (edge i)) : ∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X