Counting the marks supplied by shaded thin paths

Each thin path has one or two attachments when bounded positive witnesses are excluded. Its attachments therefore receive exactly two marks. Marks are supported on small original black components, and every collection of components with at least two marks has size at most the number of shaded paths.

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

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

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

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

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.card_shaded_add_small_cyclic_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)) (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) (cyclic : Finset B.ConnectedComponent) (small : ∀ C ∈ cyclic, Fintype.card ↥C ≤ M) (cycles : ∀ C ∈ cyclic, ¬C.toSimpleGraph.IsAcyclic) : shaded.card + cyclic.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent

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

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