Accounting for restored black edges

Isolating a set deletes its black cut. To transfer a positive set back to the original graph, add the isolated set and pay for its remaining external black edges with newly internal red edges. An overlap with the old witness is allowed when that overlap has empty black cut.

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.cut_deleteEdges {V : Type} [Fintype V] (B : SimpleGraph V) (F : Finset (Sym2 V)) (X : Finset V) : (B.deleteEdges ↑F).cutFinset X = B.cutFinset X \ F

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.cut_union_of_closed_inter {V : Type} [Fintype V] (B : SimpleGraph V) {X A : Finset V} (closed : B.cutFinset (X ∩ A) = ∅) : B.cutFinset (X ∪ A) = symmDiff (B.cutFinset X) (B.cutFinset A)

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.card_internalEdges_union_ge {V E : Type} [Fintype E] (R : Multigraph V E) (X A : Finset V) : (internalEdges R X).card + (internalEdges R A \ internalEdges R X).card ≤ (internalEdges R (X ∪ A)).card

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.positive_restore_cut {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {X A : Finset V} (positive : Positive (B.deleteEdges ↑(B.cutFinset A)) R X) (closed : B.cutFinset (X ∩ A) = ∅) (budget : (B.cutFinset A \ B.cutFinset X).card ≤ (internalEdges R A \ internalEdges R X).card) : Positive B R (X ∪ A)

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.positive_restore_two_boundary {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {X A : Finset V} (positive : Positive (B.deleteEdges ↑(B.cutFinset A)) R X) (closed : B.cutFinset (X ∩ A) = ∅) (two : (B.cutFinset A).card ≤ 2) (crossing : (B.cutFinset A ∩ B.cutFinset X).Nonempty) (newRed : (internalEdges R A \ internalEdges R X).Nonempty) : Positive B R (X ∪ A)