Marks and the cycle budget of shaded thin paths

Each shaded path contributes exactly two marks to its small attachments. Consequently at most one component with two marks can be charged to each shaded path. Because shading occurs in large original components, it leaves small cyclic components untouched. They retain a separate unit of cycle rank each: doubly marked components and small cyclic components together number at most the original cycle rank.

Each shaded degree-two path also gives two endpoint marks, all outside the eligible set. These marks record exactly the lost outside degrees. In particular, a degree-three vertex made degree two receives a mark, keeping it out of future unmarked paths. Simultaneous restoration charges at most 3 M added vertices per endpoint mark on the witness for the constructed thin-path family.

The constructed isolation and core-forest theorems retain the stronger cycle budget. These statements count the initial shading step. Preservation through the later color swaps and leaf reorganization is not formalized; RedBlack.Clusters proves the red/black lemma by another route.

Source: Burkhard Monien and Robert Preis, Upper bounds on the bisection width of 3- and 4-regular graphs, Journal of Discrete Algorithms 4 (2006), 475–498, https://doi.org/10.1016/j.jda.2005.12.009, steps 3–4.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.attachmentMarks_apply {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (C : B.ConnectedComponent) : (attachmentMarks B R U M shaded) C = ∑ i ∈ shaded, ∑ e ∈ attachmentEdges B R (region B U ↑i) M, if attachmentComponent B R (region B U ↑i) M e = C then 3 - (attachmentEdges B R (region B U ↑i) M).card else 0

The mark count records every red attachment, including repeated target components.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.attachmentMarks_eq_zero_of_large {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (C : B.ConnectedComponent) (large : M < Fintype.card ↥C) : (attachmentMarks B R U M shaded) C = 0

Only original black components of size at most M receive attachment marks.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.degree_attachmentMarks {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (degree : ∀ v ∈ U, B.degree v ≤ 2) (noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X) : Finsupp.degree (attachmentMarks B R U M shaded) = 2 * shaded.card

Each shaded thin path contributes exactly two attachment marks.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.card_doublyMarked_le {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (degree : ∀ v ∈ U, B.degree v ≤ 2) (noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X) (components : Finset B.ConnectedComponent) (marked : ∀ C ∈ components, 2 ≤ (attachmentMarks B R U M shaded) C) : components.card ≤ shaded.card

At most one doubly marked component can be charged to each shaded path.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.smallCycleBudget {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (large : ∀ v ∈ U, M < Fintype.card ↥(B.connectedComponentMk v)) (chosen : ↥(thinComponents B R U M) → Sym2 V) (injective : Function.Injective chosen) (boundary : ∀ (i : ↥(thinComponents B R U M)), chosen i ∈ B.cutFinset (region B U ↑i)) (reachable : (B.deleteEdges ↑(Finset.image chosen shaded)).Reachable = B.Reachable) : SmallCycleBudget B M shaded.card

Shading paths in large components reserves one unit of cycle rank for each untouched small cyclic component, in addition to the cost of shading.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.smallCycleBudget_of_doublyMarked {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (degree : ∀ v ∈ U, B.degree v ≤ 2) (noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X) (budget : SmallCycleBudget B M shaded.card) (marked : Finset B.ConnectedComponent) (twoMarks : ∀ C ∈ marked, 2 ≤ (attachmentMarks B R U M shaded) C) : SmallCycleBudget B M marked.card

Doubly marked components and small cyclic components fit together within the original cycle rank.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.degree_endpointMarks {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (F : RestorationFamily B R ↥(thinComponents B R U M)) (regions : ∀ (C : ↥(thinComponents B R U M)), F.region C = region B U ↑C) (degree : ∀ v ∈ U, B.degree v = 2) (noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X) : Finsupp.degree (F.restrict shaded).endpointMarks = 2 * shaded.card

Each shaded thin path gives exactly two endpoint marks, counting multiplicities.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.endpointMarks_eq_zero_of_mem {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (F : RestorationFamily B R ↥(thinComponents B R U M)) (regions : ∀ (C : ↥(thinComponents B R U M)), F.region C = region B U ↑C) {v : V} (eligible : v ∈ U) : (F.restrict shaded).endpointMarks v = 0

Endpoint marks lie outside the entire eligible set, including unshaded regions.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.degree_isolated_add_endpointMarks {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (F : RestorationFamily B R ↥(thinComponents B R U M)) (regions : ∀ (C : ↥(thinComponents B R U M)), F.region C = region B U ↑C) {v : V} (outside : v ∉ U) : (F.restrict shaded).deletedGraph.degree v + (F.restrict shaded).endpointMarks v = B.degree v

The degree lost at an ineligible vertex is exactly its endpoint mark count.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.newly_degree_two_marked {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (shaded : Finset ↥(thinComponents B R U M)) (F : RestorationFamily B R ↥(thinComponents B R U M)) (regions : ∀ (C : ↥(thinComponents B R U M)), F.region C = region B U ↑C) (degree : ∀ v ∈ U, B.degree v ≤ 2) {v : V} (original : B.degree v = 3) (remaining : (F.restrict shaded).deletedGraph.degree v = 2) : (F.restrict shaded).endpointMarks v = 1

A degree-three vertex made degree two by isolation receives a mark, so it does not enter the next family of unmarked degree-two paths.