Marks on the small components attached to shaded paths

Monien and Preis assign two marks for each shaded thin path. If the path has one red attachment, its small component gets both marks; if it has two, each attachment contributes one mark. The weight 3 - α on each attachment implements these two cases once 1 ≤ α ≤ 2 is proved.

The finite map keeps multiplicities, including parallel red attachments and marks from different paths on the same black component. Its degree is the total number of marks. Values outside the thin-path hypotheses are defined as well but need not have total two per path.

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.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)) : B.ConnectedComponent →₀ ℕ

Marks assigned to small black components by the selected shaded thin paths.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.SmallCycleBudget {V : Type} [Fintype V] (B : SimpleGraph V) (M k : ℕ) : Prop

The count k and the small cyclic components fit together within the original cycle rank. Cyclic components are counted once, regardless of their rank.

Equations

• One or more equations did not get rendered due to their size.