Weighted multigraph cuts, supervertex contractions, and Karger's survival bounds

Combinatorial and probabilistic core for Karger's randomized contraction algorithm [Karger1993] and the Karger–Stein recursive algorithm [KargerStein1996] on n-vertex weighted undirected multigraphs represented as symmetric zero-diagonal adjacency matrices W : Fin n → Fin n → ℕ.

Source statements and notation mapping

• Cut-survival bounds (paraphrase):
  • [Karger1993], Section 2, Theorem 2.1 and Corollary 2.1 (paraphrase): contracting randomly chosen edges in an n-vertex multigraph down to 2 meta-vertices preserves any fixed global minimum cut with probability at least C(n, 2)⁻¹ = 2 / (n * (n - 1)), and repeating O(n ^ 2 log n) independent trials finds a minimum cut with high probability.
  • [KargerStein1996], Section 2, Lemma 2.1, Theorem 2.2, and Corollary 2.3, and Section 2.1, Corollary 2.4 (paraphrase): a fixed cut survives contraction if and only if no contracted edge crosses it; at k active supervertices every singleton cut has weight at least minCut W, so total doubled weight S is at least k * minCut W, a single edge-weight-proportional step crosses a fixed minimum cut with probability at most 2 / k, and contracting from n down to t supervertices preserves the cut with probability at least C(t, 2) / C(n, 2) = t * (t - 1) / (n * (n - 1)).
  • [MitzenmacherUpfal2017], Section 1.5, Theorem 1.8 (paraphrase): multiplying the conditional single-step survival bounds 1 - 2 / i = (i - 2) / i for i = n, …, 3 telescopes to 2 / (n * (n - 1)).
• Notation mapping and implementation variants:
  • C(t, 2) / C(n, 2) and C(n, 2)⁻¹ ↔ ((t * (t - 1) : ℕ) : ℝ≥0∞) / (n * (n - 1)) and 2 / (n * (n - 1)) (step_survival_prob_ge, telescope_survival_step);
  • [KargerStein1996], Section 3.1, Lemma 3.1 selects (u, v) with probability 2 * W u v / S via two Random-Select draws (u proportional to D(u) then v proportional to W(u, v)); our edgeOffset / IsSampledPair formalizes an equivalent single-draw variant using one uniform draw r ∈ Fin S (S = totalDoubledWeight W = ∑ u, rowDeg W u) resolved by prefix sums over rowDeg then row weights W u v, achieving the same 2 * W u v / S distribution;
  • [KargerStein1996], Section 3.2 (Figure 5) updates the n × n matrix in O(n) time per contraction (hence Corollary 3.2's O(n ^ 2) total); our embedCompact / contractMatrix swap-compacts active slot k - 1 into the removed slot v so each contraction on k active supervertices scans only 0..k - 1 (O(k) time);
  • highProbTrials n = (n * (n - 1) / 2) * (Nat.log 2 n + 2) and the elementary Real.exp-free Bernoulli bound highProb_failure_le (≤ 1 / (2 * n)) are our own concrete parameter choices instantiating the O(n ^ 2 log n) repeated-trial amplification of [Karger1993], Section 2, Corollary 2.1.

Main definitions

• Cslib.Algorithms.WordRAM.Karger.IsMultigraph: symmetric zero-diagonal weight matrix.
• Cslib.Algorithms.WordRAM.Karger.IsNonTrivialCut, Cslib.Algorithms.WordRAM.Karger.cutWeight, Cslib.Algorithms.WordRAM.Karger.minCut: non-trivial vertex cuts, cut weights, and global minimum cut weight.
• Cslib.Algorithms.WordRAM.Karger.rowDeg, Cslib.Algorithms.WordRAM.Karger.totalDoubledWeight, Cslib.Algorithms.WordRAM.Karger.flattenMatrix: supervertex degrees, doubled total edge weight, and row-major n ^ 2-element flattening.
• Cslib.Algorithms.WordRAM.Karger.IsContractionOf, Cslib.Algorithms.WordRAM.Karger.mergePair, Cslib.Algorithms.WordRAM.Karger.embedCompact, Cslib.Algorithms.WordRAM.Karger.contractMatrix, Cslib.Algorithms.WordRAM.Karger.contractPart: supervertex partition contractions and swap-compacted adjacency updates from m + 1 down to m active supervertices.
• Cslib.Algorithms.WordRAM.Karger.edgeOffset, Cslib.Algorithms.WordRAM.Karger.IsSampledPair: prefix-sum interval characterization of edge-weight-proportional sampling from Fin S.

Main results

• Cslib.Algorithms.WordRAM.Karger.cutWeight_pullbackCut: pulling back any active cut along a supervertex contraction preserves its cut weight exactly.
• Cslib.Algorithms.WordRAM.Karger.isContractionOf_contract: contracting a distinct pair (u, v) and swap-compacting the last active slot preserves IsContractionOf.
• Cslib.Algorithms.WordRAM.Karger.surviving_card_eq, Cslib.Algorithms.WordRAM.Karger.step_survival_prob_ge: a fixed minimum cut survives one edge-proportional contraction on k supervertices with probability at least (k - 2) / k.
• Cslib.Algorithms.WordRAM.Karger.telescope_survival_step: telescoping multiplication identity ((m - 1) / (m + 1)) * (t * (t - 1) / (m * (m - 1))) = t * (t - 1) / ((m + 1) * m) in ℝ≥0∞.
• Cslib.Algorithms.WordRAM.Karger.highProb_failure_le: elementary Bernoulli amplification bound (1 - 2 / (n * (n - 1))) ^ ((n * (n - 1) / 2) * (Nat.log 2 n + 2)) ≤ 1 / (2 * n).

References

• D. R. Karger, Global Min-cuts in RNC, and Other Ramifications of a Simple Min-Cut Algorithm
• D. R. Karger and C. Stein, A New Approach to the Minimum Cut Problem
• M. Mitzenmacher and E. Upfal, Probability and Computing

Weighted multigraphs and global minimum cuts

def Cslib.Algorithms.WordRAM.Karger.IsMultigraph {n : ℕ} (W : Fin n → Fin n → ℕ) : Prop

An n-vertex undirected weighted multigraph without self-loops is a symmetric zero-diagonal matrix W : Fin n → Fin n → ℕ.

def Cslib.Algorithms.WordRAM.Karger.IsNonTrivialCut {n : ℕ} (C : Finset (Fin n)) : Prop

A vertex subset C ⊆ Fin n defines a non-trivial cut when both C and its complement are nonempty.

theorem Cslib.Algorithms.WordRAM.Karger.isNonTrivialCut_iff_card {n : ℕ} (C : Finset (Fin n)) : IsNonTrivialCut C ↔ 0 < C.card ∧ C.card < n

theorem Cslib.Algorithms.WordRAM.Karger.isNonTrivialCut_compl {n : ℕ} {C : Finset (Fin n)} (hC : IsNonTrivialCut C) : IsNonTrivialCut (Finset.univ \ C)

theorem Cslib.Algorithms.WordRAM.Karger.isNonTrivialCut_singleton {n : ℕ} (hn : 2 ≤ n) (a : Fin n) : IsNonTrivialCut {a}

theorem Cslib.Algorithms.WordRAM.Karger.exists_isNonTrivialCut {n : ℕ} (hn : 2 ≤ n) : ∃ (C : Finset (Fin n)), IsNonTrivialCut C

def Cslib.Algorithms.WordRAM.Karger.cutWeight {n : ℕ} (W : Fin n → Fin n → ℕ) (C : Finset (Fin n)) : ℕ

Total weight of edges crossing (C, Finset.univ \ C).

def Cslib.Algorithms.WordRAM.Karger.rowDeg {n : ℕ} (W : Fin n → Fin n → ℕ) (u : Fin n) : ℕ

Weighted degree of vertex u in W.

def Cslib.Algorithms.WordRAM.Karger.totalDoubledWeight {n : ℕ} (W : Fin n → Fin n → ℕ) : ℕ

Sum of all row degrees ∑ u, ∑ v, W u v, equal to twice the total edge weight of W.

theorem Cslib.Algorithms.WordRAM.Karger.entry_le_rowDeg {n : ℕ} (W : Fin n → Fin n → ℕ) (u v : Fin n) : W u v ≤ rowDeg W u

theorem Cslib.Algorithms.WordRAM.Karger.rowDeg_le_totalDoubledWeight {n : ℕ} (W : Fin n → Fin n → ℕ) (u : Fin n) : rowDeg W u ≤ totalDoubledWeight W

theorem Cslib.Algorithms.WordRAM.Karger.entry_le_totalDoubledWeight {n : ℕ} (W : Fin n → Fin n → ℕ) (u v : Fin n) : W u v ≤ totalDoubledWeight W

theorem Cslib.Algorithms.WordRAM.Karger.cutWeight_compl {n : ℕ} {W : Fin n → Fin n → ℕ} (hW : IsMultigraph W) (C : Finset (Fin n)) : cutWeight W (Finset.univ \ C) = cutWeight W C

theorem Cslib.Algorithms.WordRAM.Karger.cutWeight_le_sum_rowDeg {n : ℕ} (W : Fin n → Fin n → ℕ) (C : Finset (Fin n)) : cutWeight W C ≤ ∑ u ∈ C, rowDeg W u

theorem Cslib.Algorithms.WordRAM.Karger.two_mul_cutWeight_le_totalDoubledWeight {n : ℕ} {W : Fin n → Fin n → ℕ} (hW : IsMultigraph W) (C : Finset (Fin n)) : 2 * cutWeight W C ≤ totalDoubledWeight W

theorem Cslib.Algorithms.WordRAM.Karger.cutWeight_singleton {n : ℕ} {W : Fin n → Fin n → ℕ} (hW : IsMultigraph W) (a : Fin n) : cutWeight W {a} = rowDeg W a

theorem Cslib.Algorithms.WordRAM.Karger.cutWeight_two_singleton_zero {W : Fin 2 → Fin 2 → ℕ} (hW : IsMultigraph W) : cutWeight W {0} = W 0 1

noncomputable def Cslib.Algorithms.WordRAM.Karger.minCut {n : ℕ} (W : Fin n → Fin n → ℕ) : ℕ

Global minimum cut weight of an n-vertex multigraph W, defined as the greatest lower bound of cutWeight W C over all non-trivial cuts C.

theorem Cslib.Algorithms.WordRAM.Karger.minCut_le_cutWeight {n : ℕ} (W : Fin n → Fin n → ℕ) {C : Finset (Fin n)} (hC : IsNonTrivialCut C) : minCut W ≤ cutWeight W C

theorem Cslib.Algorithms.WordRAM.Karger.exists_minCut_achiever {n : ℕ} (hn : 2 ≤ n) (W : Fin n → Fin n → ℕ) : ∃ (C : Finset (Fin n)), IsNonTrivialCut C ∧ cutWeight W C = minCut W

theorem Cslib.Algorithms.WordRAM.Karger.le_minCut_iff {n : ℕ} (hn : 2 ≤ n) (W : Fin n → Fin n → ℕ) (m : ℕ) : m ≤ minCut W ↔ ∀ (C : Finset (Fin n)), IsNonTrivialCut C → m ≤ cutWeight W C

theorem Cslib.Algorithms.WordRAM.Karger.minCut_pos_iff {n : ℕ} (hn : 2 ≤ n) (W : Fin n → Fin n → ℕ) : 0 < minCut W ↔ ∀ (C : Finset (Fin n)), IsNonTrivialCut C → 0 < cutWeight W C

theorem Cslib.Algorithms.WordRAM.Karger.minCut_le_rowDeg {n : ℕ} (hn : 2 ≤ n) {W : Fin n → Fin n → ℕ} (hW : IsMultigraph W) (a : Fin n) : minCut W ≤ rowDeg W a

theorem Cslib.Algorithms.WordRAM.Karger.mul_minCut_le_totalDoubledWeight {n : ℕ} (hn : 2 ≤ n) {W : Fin n → Fin n → ℕ} (hW : IsMultigraph W) : n * minCut W ≤ totalDoubledWeight W

theorem Cslib.Algorithms.WordRAM.Karger.totalDoubledWeight_pos_of_minCut_pos {n : ℕ} (hn : 2 ≤ n) {W : Fin n → Fin n → ℕ} (hW : IsMultigraph W) (hpos : 0 < minCut W) : 0 < totalDoubledWeight W

Row-major matrix flattening

def Cslib.Algorithms.WordRAM.Karger.flattenMatrix {n : ℕ} (W : Fin n → Fin n → ℕ) : List ℕ

Row-major n * n-element list encoding of W : Fin n → Fin n → ℕ.

@[simp]

theorem Cslib.Algorithms.WordRAM.Karger.length_flattenMatrix {n : ℕ} (W : Fin n → Fin n → ℕ) : (flattenMatrix W).length = n * n

theorem Cslib.Algorithms.WordRAM.Karger.getElem_flattenMatrix {n : ℕ} (W : Fin n → Fin n → ℕ) (u v : Fin n) : (flattenMatrix W)[↑u * n + ↑v] = W u v

theorem Cslib.Algorithms.WordRAM.Karger.mem_flattenMatrix_le_totalDoubledWeight {n : ℕ} (W : Fin n → Fin n → ℕ) {x : ℕ} (hx : x ∈ flattenMatrix W) : x ≤ totalDoubledWeight W

Supervertex partitions and contraction algebra

def Cslib.Algorithms.WordRAM.Karger.pullbackCut {n k : ℕ} (part : Fin n → Fin k) (B : Finset (Fin k)) : Finset (Fin n)

Pull back an active cut B ⊆ Fin k along a supervertex map part : Fin n → Fin k.

theorem Cslib.Algorithms.WordRAM.Karger.mem_pullbackCut {n k : ℕ} (part : Fin n → Fin k) (B : Finset (Fin k)) (x : Fin n) : x ∈ pullbackCut part B ↔ part x ∈ B

theorem Cslib.Algorithms.WordRAM.Karger.pullbackCut_empty {n k : ℕ} (part : Fin n → Fin k) : pullbackCut part ∅ = ∅

theorem Cslib.Algorithms.WordRAM.Karger.pullbackCut_univ {n k : ℕ} (part : Fin n → Fin k) : pullbackCut part Finset.univ = Finset.univ

theorem Cslib.Algorithms.WordRAM.Karger.pullbackCut_compl {n k : ℕ} (part : Fin n → Fin k) (B : Finset (Fin k)) : pullbackCut part (Finset.univ \ B) = Finset.univ \ pullbackCut part B

theorem Cslib.Algorithms.WordRAM.Karger.isNonTrivialCut_pullbackCut {n k : ℕ} {part : Fin n → Fin k} (hsurj : Function.Surjective part) {B : Finset (Fin k)} (hB : IsNonTrivialCut B) : IsNonTrivialCut (pullbackCut part B)

theorem Cslib.Algorithms.WordRAM.Karger.isNonTrivialCut_of_pullbackCut {n k : ℕ} (part : Fin n → Fin k) {B : Finset (Fin k)} (h : IsNonTrivialCut (pullbackCut part B)) : IsNonTrivialCut B

structure Cslib.Algorithms.WordRAM.Karger.IsContractionOf {n k : ℕ} (W₀ : Fin n → Fin n → ℕ) (part : Fin n → Fin k) (W : Fin k → Fin k → ℕ) : Prop

W : Fin k → Fin k → ℕ is the contracted multigraph of W₀ : Fin n → Fin n → ℕ along surjective supervertex assignment part : Fin n → Fin k.

• surj : Function.Surjective part
• multigraph : IsMultigraph W
• offDiag (a b : Fin k) : a ≠ b → W a b = ∑ x : Fin n with part x = a, ∑ y : Fin n with part y = b, W₀ x y

theorem Cslib.Algorithms.WordRAM.Karger.isContractionOf_id {n : ℕ} {W₀ : Fin n → Fin n → ℕ} (hW₀ : IsMultigraph W₀) : IsContractionOf W₀ id W₀

theorem Cslib.Algorithms.WordRAM.Karger.cutWeight_pullbackCut {n k : ℕ} {W₀ : Fin n → Fin n → ℕ} {part : Fin n → Fin k} {W : Fin k → Fin k → ℕ} (hC : IsContractionOf W₀ part W) (B : Finset (Fin k)) : cutWeight W₀ (pullbackCut part B) = cutWeight W B

theorem Cslib.Algorithms.WordRAM.Karger.minCut_le_of_isContractionOf {n k : ℕ} (hk : 2 ≤ k) {W₀ : Fin n → Fin n → ℕ} {part : Fin n → Fin k} {W : Fin k → Fin k → ℕ} (hC : IsContractionOf W₀ part W) : minCut W₀ ≤ minCut W

theorem Cslib.Algorithms.WordRAM.Karger.two_vertex_contraction_output {n : ℕ} {W₀ : Fin n → Fin n → ℕ} {part : Fin n → Fin 2} {W : Fin 2 → Fin 2 → ℕ} (hC : IsContractionOf W₀ part W) : IsNonTrivialCut (pullbackCut part {0}) ∧ W 0 1 = cutWeight W₀ (pullbackCut part {0}) ∧ minCut W₀ ≤ W 0 1

Phase A (mergePair) and Phase B (embedCompact / contractMatrix)

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

Phase A 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.Algorithms.WordRAM.Karger.isMultigraph_mergePair {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) (u v : Fin k) : IsMultigraph (mergePair W u v)

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

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

theorem Cslib.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.rowDeg_mergePair_v {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : rowDeg (mergePair W u v) v = 0

def Cslib.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.embedCompact_ne {m : ℕ} (v : Fin (m + 1)) (i : Fin m) : embedCompact v i ≠ v

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

def Cslib.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.embedCompact_compactIdx {m : ℕ} (v a : Fin (m + 1)) (ha : a ≠ v) : embedCompact v (compactIdx v a ha) = a

@[simp]

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

def Cslib.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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.Algorithms.WordRAM.Karger.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

Prefix-sum edge-proportional sampling on Fin S

def Cslib.Algorithms.WordRAM.Karger.degBefore {k : ℕ} (W : Fin k → Fin k → ℕ) (u : Fin k) : ℕ

Sum of rowDeg W a over all a < u.

def Cslib.Algorithms.WordRAM.Karger.weightBefore {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : ℕ

Sum of W u b over all b < v.

def Cslib.Algorithms.WordRAM.Karger.edgeOffset {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : ℕ

Flattened prefix-sum start offset of directed edge slot (u, v) inside [0, S).

theorem Cslib.Algorithms.WordRAM.Karger.weightBefore_add_le_rowDeg {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : weightBefore W u v + W u v ≤ rowDeg W u

theorem Cslib.Algorithms.WordRAM.Karger.weightBefore_le_of_lt {k : ℕ} (W : Fin k → Fin k → ℕ) (u : Fin k) {v₁ v₂ : Fin k} (hlt : v₁ < v₂) : weightBefore W u v₁ + W u v₁ ≤ weightBefore W u v₂

theorem Cslib.Algorithms.WordRAM.Karger.degBefore_add_le_totalDoubledWeight {k : ℕ} (W : Fin k → Fin k → ℕ) (u : Fin k) : degBefore W u + rowDeg W u ≤ totalDoubledWeight W

theorem Cslib.Algorithms.WordRAM.Karger.degBefore_le_of_lt {k : ℕ} (W : Fin k → Fin k → ℕ) {u₁ u₂ : Fin k} (hlt : u₁ < u₂) : degBefore W u₁ + rowDeg W u₁ ≤ degBefore W u₂

theorem Cslib.Algorithms.WordRAM.Karger.edgeOffset_add_le_totalDoubledWeight {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : edgeOffset W u v + W u v ≤ totalDoubledWeight W

def Cslib.Algorithms.WordRAM.Karger.IsSampledPair {k : ℕ} (W : Fin k → Fin k → ℕ) (r : ℕ) (u v : Fin k) : Prop

IsSampledPair W r u v holds when sample r falls inside the half-open interval [edgeOffset W u v, edgeOffset W u v + W u v).

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.Karger.instDecidableIsSampledPair {k : ℕ} (W : Fin k → Fin k → ℕ) (r : ℕ) (u v : Fin k) : Decidable (IsSampledPair W r u v)

theorem Cslib.Algorithms.WordRAM.Karger.isSampledPair_ne {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) {r : ℕ} {u v : Fin k} (h : IsSampledPair W r u v) : u ≠ v

theorem Cslib.Algorithms.WordRAM.Karger.isSampledPair_unique {k : ℕ} (W : Fin k → Fin k → ℕ) {r : ℕ} {u₁ v₁ u₂ v₂ : Fin k} (h₁ : IsSampledPair W r u₁ v₁) (h₂ : IsSampledPair W r u₂ v₂) : u₁ = u₂ ∧ v₁ = v₂

theorem Cslib.Algorithms.WordRAM.Karger.exists_isSampledPair {k : ℕ} (W : Fin k → Fin k → ℕ) {r : ℕ} (hr : r < totalDoubledWeight W) : ∃ (u : Fin k) (v : Fin k), IsSampledPair W r u v

theorem Cslib.Algorithms.WordRAM.Karger.card_sampledPair_fiber {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : {r : Fin (totalDoubledWeight W) | IsSampledPair W (↑r) u v}.card = W u v

def Cslib.Algorithms.WordRAM.Karger.SampleSurvives {k : ℕ} (W : Fin k → Fin k → ℕ) (B : Finset (Fin k)) (r : Fin (totalDoubledWeight W)) : Prop

Event on Fin (totalDoubledWeight W) where the edge sampled at r keeps both endpoints on the same side of B.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.Karger.instDecidableSampleSurvives {k : ℕ} (W : Fin k → Fin k → ℕ) (B : Finset (Fin k)) (r : Fin (totalDoubledWeight W)) : Decidable (SampleSurvives W B r)

theorem Cslib.Algorithms.WordRAM.Karger.not_sampleSurvives_iff_crosses {k : ℕ} (W : Fin k → Fin k → ℕ) (B : Finset (Fin k)) (r : Fin (totalDoubledWeight W)) : ¬SampleSurvives W B r ↔ ∃ (u : Fin k) (v : Fin k), IsSampledPair W (↑r) u v ∧ ¬(u ∈ B ↔ v ∈ B)

theorem Cslib.Algorithms.WordRAM.Karger.crossing_card_eq {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) (B : Finset (Fin k)) : {r : Fin (totalDoubledWeight W) | ¬SampleSurvives W B r}.card = 2 * cutWeight W B

theorem Cslib.Algorithms.WordRAM.Karger.surviving_card_eq {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) (B : Finset (Fin k)) : {r : Fin (totalDoubledWeight W) | SampleSurvives W B r}.card = totalDoubledWeight W - 2 * cutWeight W B

theorem Cslib.Algorithms.WordRAM.Karger.step_survival_prob_ge {k : ℕ} (hk : 2 ≤ k) {W : Fin k → Fin k → ℕ} (hW : IsMultigraph W) {B : Finset (Fin k)} (hS : 0 < totalDoubledWeight W) (hdeg : k * cutWeight W B ≤ totalDoubledWeight W) : ↑(k - 2) / ↑k ≤ (Probability.PMF.uniformOfFintype (Fin (totalDoubledWeight W))).toOuterMeasure {r : Fin (totalDoubledWeight W) | SampleSurvives W B r}

One-step survival probability lower bound: if k ≥ 2, 0 < totalDoubledWeight W, and k * cutWeight W B ≤ totalDoubledWeight W, then a uniform sample r : Fin (totalDoubledWeight W) satisfies SampleSurvives W B r with probability at least (k - 2) / k.

ENNReal probability composition, telescoping, and Bernoulli amplification

theorem Cslib.Algorithms.WordRAM.Karger.toOuterMeasure_bind_ge_mul_ennreal {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (pre : Set α) (event : Set β) {s₁ s₂ : ENNReal} (hp : s₁ ≤ p.toOuterMeasure pre) (hstep : ∀ a ∈ p.support, a ∈ pre → s₂ ≤ (kernel a).toOuterMeasure event) : s₁ * s₂ ≤ (p.bind kernel).toOuterMeasure event

ENNReal multiplication rule for sequential success lower bounds across PMF.bind.

theorem Cslib.Algorithms.WordRAM.Karger.toOuterMeasure_bind_le_mul_ennreal {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (stillFailing : Set α) (failure : Set β) {q₁ q₂ : ENNReal} (hp : p.toOuterMeasure stillFailing ≤ q₁) (hfail : ∀ a ∈ p.support, a ∈ stillFailing → (kernel a).toOuterMeasure failure ≤ q₂) (hsucc : ∀ a ∈ p.support, a ∉ stillFailing → (kernel a).toOuterMeasure failure = 0) : (p.bind kernel).toOuterMeasure failure ≤ q₁ * q₂

ENNReal multiplication rule for independent-trial failure upper bounds: if p stays in stillFailing with probability at most q₁, every supported a ∈ stillFailing fails under kernel a with probability at most q₂, and every supported a ∉ stillFailing has zero failure probability under kernel a, then p.bind kernel fails with probability at most q₁ * q₂.

theorem Cslib.Algorithms.WordRAM.Karger.toOuterMeasure_add_compl_ennreal {α : Type u_1} (p : PMF α) (s : Set α) : p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1

Exact complementation law p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1 for discrete PMFs, valid on arbitrary types without measurability hypotheses.

theorem Cslib.Algorithms.WordRAM.Karger.toOuterMeasure_compl_le_one_sub {α : Type u_1} (p : PMF α) (s : Set α) {q : ENNReal} (hq : q ≤ p.toOuterMeasure s) : p.toOuterMeasure sᶜ ≤ 1 - q

theorem Cslib.Algorithms.WordRAM.Karger.ennreal_div_pow (a b : ENNReal) (m : ℕ) : (a / b) ^ m = a ^ m / b ^ m

Power of a quotient in ℝ≥0∞: (a / b) ^ m = a ^ m / b ^ m.

theorem Cslib.Algorithms.WordRAM.Karger.telescope_survival_step {t m : ℕ} (ht : 2 ≤ t) (htm : t ≤ m) : ↑(m - 1) / ↑(m + 1) * (↑(t * (t - 1)) / ↑(m * (m - 1))) = ↑(t * (t - 1)) / ↑((m + 1) * m)

Telescoping cancellation step for contractDownTo survival probability from m + 1 down to t (2 ≤ t ≤ m): ((m - 1) / (m + 1)) * (t * (t - 1) / (m * (m - 1))) = t * (t - 1) / ((m + 1) * m).

theorem Cslib.Algorithms.WordRAM.Karger.two_mul_pred_pow_le_pow {m : ℕ} (hm : 1 ≤ m) : 2 * (m - 1) ^ m ≤ m ^ m

Elementary Bernoulli power bound 2 * (m - 1) ^ m ≤ m ^ m for 1 ≤ m.

theorem Cslib.Algorithms.WordRAM.Karger.one_sub_two_div_pairs_eq {n : ℕ} (hn : 2 ≤ n) : 1 - 2 / ↑(n * (n - 1)) = ↑(n * (n - 1) / 2 - 1) / ↑(n * (n - 1) / 2)

theorem Cslib.Algorithms.WordRAM.Karger.one_sub_two_div_pow_pairs_le_half {n : ℕ} (hn : 2 ≤ n) : (1 - 2 / ↑(n * (n - 1))) ^ (n * (n - 1) / 2) ≤ 1 / 2

def Cslib.Algorithms.WordRAM.Karger.highProbTrials (n : ℕ) : ℕ

Elementary high-probability trial count (n * (n - 1) / 2) * (Nat.log 2 n + 2) for Basic Karger amplification.

theorem Cslib.Algorithms.WordRAM.Karger.highProbTrials_pos {n : ℕ} (hn : 2 ≤ n) : 1 ≤ highProbTrials n

theorem Cslib.Algorithms.WordRAM.Karger.highProb_failure_le {n : ℕ} (hn : 2 ≤ n) : (1 - 2 / ↑(n * (n - 1))) ^ highProbTrials n ≤ 1 / ↑(2 * n)

Elementary failure probability bound for highProbTrials n independent contractions: (1 - 2 / (n * (n - 1))) ^ ((n * (n - 1) / 2) * (Nat.log 2 n + 2)) ≤ 1 / (2 * n).

theorem Cslib.Algorithms.WordRAM.Karger.highProb_failure_le_inv_n {n : ℕ} (hn : 2 ≤ n) : (1 - 2 / ↑(n * (n - 1))) ^ highProbTrials n ≤ 1 / ↑n