Contracting two supervertices

Contraction of a weighted multigraph W : Fin (m + 1) → Fin (m + 1) → ℕ (Cslib.WeightedCut.IsMultigraph) along a pair of distinct supervertices u ≠ v, keeping the supervertices as Fin m. Merging v into u (mergePair) redirects the edges at v to u and drops the edges between them. Swap-compaction (embedCompact, compactIdx) then moves the last supervertex Fin.last m into the freed slot v, so that a contraction step on m + 1 active supervertices only touches rows and columns 0, …, m, as in the O(n)-time matrix update of Karger and Stein, Section 3.2. The contracted matrix is contractMatrix W u v, the updated map from the original vertices to supervertices is contractPart part u v huv, and a cut of Fin (m + 1) that does not separate u and v becomes the cut contractCut v B of Fin m.

Contraction preserves Cslib.WeightedCut.IsContractionOf (isContractionOf_contract), so pulled back cuts keep their weight, and a cut that does not separate u and v keeps its weight (cutWeight_contractCut). The randomized algorithms of Karger and Karger–Stein (CslibFrontier.Algorithms.Karger.Graph) and the deterministic Stoer–Wagner algorithm (CslibFrontier.Algorithms.Lean.StoerWagner.Basic) are built on this API.

Main definitions

• Cslib.WeightedCut.mergePair: the weight matrix after merging v into u.
• Cslib.WeightedCut.embedCompact, Cslib.WeightedCut.compactIdx: swap-compaction of the slots other than v, and its inverse.
• Cslib.WeightedCut.contractMatrix, Cslib.WeightedCut.contractPart, Cslib.WeightedCut.contractCut: the contracted matrix, supervertex map and cut.

Main results

• Cslib.WeightedCut.isMultigraph_contractMatrix: the contracted matrix is a multigraph.
• Cslib.WeightedCut.rowDeg_contractMatrix, Cslib.WeightedCut.totalDoubledWeight_contractMatrix: degrees after contraction; the total doubled weight drops by 2 * W u v.
• Cslib.WeightedCut.isContractionOf_contract: contracting a distinct pair (u, v) and swap-compacting the last active slot preserves Cslib.WeightedCut.IsContractionOf.
• Cslib.WeightedCut.pullbackCut_contractCut, Cslib.WeightedCut.cutWeight_contractCut: a cut that does not separate u and v pulls back to the same set, with the same weight.
• Cslib.WeightedCut.pullbackCut_id: pulling a cut back along the identity gives the same cut.

References

• D. R. Karger and C. Stein, A New Approach to the Minimum Cut Problem

Merging (mergePair) and swap-compaction (embedCompact / contractMatrix)

def Cslib.WeightedCut.mergePair {k : ℕ} (W : Fin k → Fin k → ℕ) (u v i j : Fin k) : ℕ

Matrix update when merging active supervertex v into u (u ≠ v): edges incident to v are redirected to u, self-loops at u are cleared, and row/column v become isolated.

theorem Cslib.WeightedCut.isMultigraph_mergePair {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) (u v : Fin k) : IsMultigraph (mergePair W u v)

theorem Cslib.WeightedCut.mergePair_isolated_left {k : ℕ} (W : Fin k → Fin k → ℕ) (u v j : Fin k) : mergePair W u v v j = 0

theorem Cslib.WeightedCut.mergePair_isolated_right {k : ℕ} (W : Fin k → Fin k → ℕ) (u v i : Fin k) : mergePair W u v i v = 0

theorem Cslib.WeightedCut.rowDeg_mergePair_other {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) {u v x : Fin k} (huv : u ≠ v) (hxu : x ≠ u) (hxv : x ≠ v) : rowDeg (mergePair W u v) x = rowDeg W x

theorem Cslib.WeightedCut.rowDeg_mergePair_u {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) {u v : Fin k} (huv : u ≠ v) : rowDeg (mergePair W u v) u = rowDeg W u - W u v + (rowDeg W v - W v u)

theorem Cslib.WeightedCut.rowDeg_mergePair_v {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : rowDeg (mergePair W u v) v = 0

def Cslib.WeightedCut.embedCompact {m : ℕ} (v : Fin (m + 1)) (i : Fin m) : Fin (m + 1)

Embedding Fin m → Fin (m + 1) corresponding to replacing removed slot v with Fin.last m and keeping all other slots < m in place.

theorem Cslib.WeightedCut.embedCompact_ne {m : ℕ} (v : Fin (m + 1)) (i : Fin m) : embedCompact v i ≠ v

theorem Cslib.WeightedCut.embedCompact_injective {m : ℕ} (v : Fin (m + 1)) : Function.Injective (embedCompact v)

def Cslib.WeightedCut.compactIdx {m : ℕ} (v a : Fin (m + 1)) (ha : a ≠ v) : Fin m

Inverse of embedCompact v on {a : Fin (m + 1) // a ≠ v}.

@[simp]

theorem Cslib.WeightedCut.embedCompact_compactIdx {m : ℕ} (v a : Fin (m + 1)) (ha : a ≠ v) : embedCompact v (compactIdx v a ha) = a

@[simp]

theorem Cslib.WeightedCut.compactIdx_embedCompact {m : ℕ} (v : Fin (m + 1)) (i : Fin m) : compactIdx v (embedCompact v i) ⋯ = i

def Cslib.WeightedCut.contractMatrix {m : ℕ} (W : Fin (m + 1) → Fin (m + 1) → ℕ) (u v : Fin (m + 1)) (i j : Fin m) : ℕ

Swap-compacted m × m adjacency matrix after merging v into u (u ≠ v) and moving active supervertex Fin.last m into slot v (when v ≠ Fin.last m).

theorem Cslib.WeightedCut.isMultigraph_contractMatrix {m : ℕ} {W : Fin (m + 1) → Fin (m + 1) → ℕ} (hW : IsMultigraph W) (u v : Fin (m + 1)) : IsMultigraph (contractMatrix W u v)

theorem Cslib.WeightedCut.sum_embedCompact_eq_sum_erase {m : ℕ} (v : Fin (m + 1)) (f : Fin (m + 1) → ℕ) : ∑ i : Fin m, f (embedCompact v i) = ∑ a ∈ Finset.univ.erase v, f a

theorem Cslib.WeightedCut.rowDeg_contractMatrix {m : ℕ} (W : Fin (m + 1) → Fin (m + 1) → ℕ) (u v : Fin (m + 1)) (i : Fin m) : rowDeg (contractMatrix W u v) i = rowDeg (mergePair W u v) (embedCompact v i)

theorem Cslib.WeightedCut.totalDoubledWeight_contractMatrix {m : ℕ} {W : Fin (m + 1) → Fin (m + 1) → ℕ} (hW : IsMultigraph W) {u v : Fin (m + 1)} (huv : u ≠ v) : totalDoubledWeight (contractMatrix W u v) + 2 * W u v = totalDoubledWeight W

def Cslib.WeightedCut.contractPart {n m : ℕ} (part : Fin n → Fin (m + 1)) (u v : Fin (m + 1)) (huv : u ≠ v) (x : Fin n) : Fin m

Updated supervertex partition Fin n → Fin m after merging v into u (u ≠ v) and swap-compacting slot v.

@[simp]

theorem Cslib.WeightedCut.embedCompact_contractPart {n m : ℕ} (part : Fin n → Fin (m + 1)) (u v : Fin (m + 1)) (huv : u ≠ v) (x : Fin n) : embedCompact v (contractPart part u v huv x) = if part x = v then u else part x

theorem Cslib.WeightedCut.filter_contractPart_eq {n m : ℕ} (part : Fin n → Fin (m + 1)) (u v : Fin (m + 1)) (huv : u ≠ v) (i : Fin m) : {x : Fin n | contractPart part u v huv x = i} = if embedCompact v i = u then {x : Fin n | part x = u} ∪ {x : Fin n | part x = v} else {x : Fin n | part x = embedCompact v i}

theorem Cslib.WeightedCut.isContractionOf_contract {n m : ℕ} {W₀ : Fin n → Fin n → ℕ} {part : Fin n → Fin (m + 1)} {W : Fin (m + 1) → Fin (m + 1) → ℕ} (hC : IsContractionOf W₀ part W) {u v : Fin (m + 1)} (huv : u ≠ v) : IsContractionOf W₀ (contractPart part u v huv) (contractMatrix W u v)

def Cslib.WeightedCut.contractCut {m : ℕ} (v : Fin (m + 1)) (B : Finset (Fin (m + 1))) : Finset (Fin m)

Active cut induced on Fin m after contracting a non-crossing pair (u, v).

theorem Cslib.WeightedCut.pullbackCut_contractCut {n m : ℕ} (part : Fin n → Fin (m + 1)) {u v : Fin (m + 1)} (huv : u ≠ v) {B : Finset (Fin (m + 1))} (hsame : u ∈ B ↔ v ∈ B) : pullbackCut (contractPart part u v huv) (contractCut v B) = pullbackCut part B

theorem Cslib.WeightedCut.pullbackCut_id {V : Type u_1} [Fintype V] [DecidableEq V] (C : Finset V) : pullbackCut id C = C

Pulling a cut back along the identity gives the same cut.

theorem Cslib.WeightedCut.cutWeight_contractCut {k : ℕ} {W : Fin (k + 1) → Fin (k + 1) → ℕ} (hW : IsMultigraph W) {s t : Fin (k + 1)} (hst : s ≠ t) {C : Finset (Fin (k + 1))} (hC : s ∈ C ↔ t ∈ C) : cutWeight (contractMatrix W s t) (contractCut t C) = cutWeight W C

Merging t into s preserves the weight of the cuts that do not separate s and t.