Ordering red attachments along a degree-two region #
A finite set of red attachments to a connected degree-two region can be ordered along a spanning path. Thus Monien and Preis's thin-walk witness applies directly to a vertex set and its attachments, without supplying a walk or ordered positions. Repeated attachment positions are allowed.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_positive_of_thin_region
{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)
(many : 3 ≤ edges.card)
(thin : P.card ≤ M * 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)
:
theorem
Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.thin_region_bounds
{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)
(thin : P.card ≤ M * 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)
(noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X)
: