Constructing and isolating the thin-path system #
Given eligible vertices of black degree at most two, take their induced
connected components. Each has a spanning simple path; different regions
have disjoint vertices and disjoint boundary cuts. Count their actual red
attachments to black components of size at most M to define thin regions.
Unless a positive set of size at most 8 M + 1 already exists, a thin region
has one or two attachments, at most 2 M vertices, and a nonempty boundary.
If eligible vertices lie in black components larger than M, choosing one
small attachment per thin region constructs a restoration family with
region-plus-attachment size at most 3 M. Cycle selection then isolates at
most the original cycle rank many regions and leaves no cycle through any
thin region. The existing family restoration theorem applies with L = 3 M.
This constructs the thin-path system in Monien and Preis's red/black proof.
Full-cut deletion preserves reachability between vertices outside the
isolated regions. Contracting the pieces between all remaining region
boundaries produces a forest. exists_core_forest additionally suppresses
the thin-region vertices, retaining the restoration and cycle-rank bounds
and exact original reachability on the remaining core pieces. With eligible
vertices of degree exactly two, exists_counted_core_forest also proves
that the number of core edges plus the number of shaded paths is exactly
the original number of thin paths. All three constructions retain the
stronger budget reserving cycle rank for small cyclic components. The marks
on small attachments total exactly two per shaded path, so doubly marked
components fit within the same budget. Endpoint marks total two per shaded
path as well, lie outside the eligible set, and record the exact degree
loss there. Restoration charges only marks on the witness. The weighted-tree
reorganization and the final density contradiction of this route are not
formalized; RedBlack.Clusters proves the red/black lemma by another route.
Membership in a region is membership in the corresponding induced component.
Every vertex of a region is eligible.
Every induced region is nonempty and connected in the ambient graph.
The regions cover exactly the eligible vertices.
Distinct regions have no common vertices.
A black edge between eligible regions forces them to coincide.
Distinct regions have disjoint black boundaries.
Nonclosed eligible regions admit distinct choices of boundary edges.
A connected vertex set of ambient degree at most two has a spanning simple path.
Eligible degree-two regions come with spanning paths in the original graph.
Each eligible region has at most two boundary edges.
With ambient degree exactly two, a region is closed or has exactly two boundary edges.
A nonclosed eligible region is a tree, so its spanning path has no extra cycle edges.
The thin-path witness from a connected region and an unordered finite set of at least three red attachments. A spanning path and attachment order are constructed.
The cardinality test defining thin components.
Excluding bounded positive sets bounds every thin region and its number of attachments, and forces its black boundary to be nonempty.
With ambient degree exactly two and no bounded positive witness, every thin region has exactly two boundary edges.
Construct the thin-path restoration family and select regions to isolate.
At most the original cycle rank many regions are selected. Their designated
single-edge deletions preserve reachability; deleting their full cuts leaves
no cycle meeting any thin region and preserves reachability among outside
vertices. The region-boundary quotient is a forest. Each region and its
chosen attachment together have at most 3 M vertices. Small cyclic
components reserve additional units of the original cycle rank.
Construct the forest on the core pieces by isolating selected thin paths, identifying all thin regions in the boundary quotient, and suppressing those vertices. Core reachability agrees with the original black graph, and the restoration size and cycle-rank bounds, including the reserve for small cyclic components, are retained. Core edges count the regions whose remaining boundary has size two.
With eligible vertices of degree exactly two, every unshaded thin path contributes one core edge. Thus the number of core edges plus the number of shaded paths is exactly the original number of thin paths.