Endpoint marks of the constructed thin paths

Every thin region has two boundary edges when eligible vertices have degree exactly two. Shading gives two endpoint marks per region. These marks lie outside the entire eligible set: a boundary edge between two eligible vertices would join their induced components. Outside degrees drop by exactly the mark count, so a degree-three vertex that becomes degree two receives one mark and remains excluded from eligible paths.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.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