Constructing and counting the suppressed red graph #
The two-neighbor lemma constructs each red edge. Incidence bijections identify its degree and internal-edge counts with the boundary counts in the helpfulness lift.
theorem
Algebraic.Cutwidth.Bisection.Internal.exists_boundarySuppression
{W : Type}
[Fintype W]
(H : SimpleGraph W)
{S : Finset W}
(regular : H.IsRegularOfDegree 3)
(outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1)
(independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d)
:
Nonempty (BoundarySuppression H S)
theorem
Algebraic.Cutwidth.Bisection.Internal.BoundarySuppression.red_degree
{W : Type}
[Fintype W]
(H : SimpleGraph W)
{S : Finset W}
(Q : BoundarySuppression H S)
(v : ↥(S \ cutBoundary H S))
:
theorem
Algebraic.Cutwidth.Bisection.Internal.boundaryInterior_degree
{W : Type}
[Fintype W]
(H : SimpleGraph W)
{S : Finset W}
(v : ↥(S \ cutBoundary H S))
:
(SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H).degree v = (H.neighborFinset ↑v ∩ (S \ cutBoundary H S)).card
theorem
Algebraic.Cutwidth.Bisection.Internal.BoundarySuppression.degree_sum
{W : Type}
[Fintype W]
(H : SimpleGraph W)
{S : Finset W}
(Q : BoundarySuppression H S)
(regular : H.IsRegularOfDegree 3)
(v : ↥(S \ cutBoundary H S))
:
theorem
Algebraic.Cutwidth.Bisection.Internal.BoundarySuppression.internalEdges_card
{W : Type}
[Fintype W]
(H : SimpleGraph W)
{S : Finset W}
(Q : BoundarySuppression H S)
(X : Finset ↥(S \ cutBoundary H S))
:
(RedBlack.internalEdges Q.red X).card = (sharedBoundary H S (Finset.map (Function.Embedding.subtype fun (v : W) => v ∈ S \ cutBoundary H S) X)).card
theorem
Algebraic.Cutwidth.Bisection.Internal.boundaryInterior_cut_card
{W : Type}
[Fintype W]
(H : SimpleGraph W)
{S : Finset W}
(X : Finset ↥(S \ cutBoundary H S))
:
((SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H).cutFinset X).card = (H.cutFinset (Finset.map (Function.Embedding.subtype fun (v : W) => v ∈ S \ cutBoundary H S) X) \ H.cutFinset (cutBoundary H S)).card
theorem
Algebraic.Cutwidth.Bisection.Internal.BoundarySuppression.exists_helpful_set_of_positive
{W : Type}
[Fintype W]
(H : SimpleGraph W)
{S : Finset W}
(Q : BoundarySuppression H S)
(regular : H.IsRegularOfDegree 3)
(outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1)
(independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d)
{X : Finset ↥(S \ cutBoundary H S)}
(positive : RedBlack.Positive (SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H) Q.red X)
: