Mathematical recurrences and quadratic potential for Karger–Stein (FastCut)

Combinatorial, arithmetic, and probabilistic foundations for the Karger–Stein recursive global minimum cut algorithm ([KargerStein1996], Section 4, Figure 6, Lemmas 4.1–4.3, and the minimum-cut-value part of Theorem 4.4; paraphrase) on the randomized word RAM.

Design notes and deviations from [KargerStein1996]

1. Integer contraction threshold (fastCutThreshold): [KargerStein1996], Section 4, Figure 6 contracts each branch to ⌈k / √2 + 1⌉ vertices so that (t * (t - 1)) / (k * (k - 1)) ≥ 1 / 2 (Section 4, Lemma 4.3). We instead define fastCutThreshold k as the smallest integer t ≥ 2 satisfying k * (k - 1) ≤ 2 * t * (t - 1). This integer deviation directly enforces Lemma 4.3's ≥ 1 / 2 per-branch survival inequality without square roots or divisions; it is never larger than ⌈k / √2 + 1⌉ and is strictly smaller at e.g. k = 8 (t = 6 vs 7).
2. Base case at k ≤ 6, as in the source: each leaf runs one random contraction down to 2 vertices, the base case G' ← Contract(G, 2) of [KargerStein1996], Section 4, Figure 6. The cutoff follows equation (2) and the remark at the end of the proof of Lemma 4.3 (recurse for n ≥ 7); Figure 6 itself tests "fewer than 6 vertices". A leaf keeps a fixed minimum cut with probability ≥ 2 / (k * (k - 1)) ≥ 2 / 30, equation (2)'s base-case bound 1 / 15. The 15 in 1 / (Nat.log 2 n + 15) is the source's constant: the proof of Lemma 4.3 sets z₀ = 59 and shows z_k < 59 + 2 * k for k ≥ 1, so p_k = 4 / (z_k + 1) ≥ 2 / (30 + k); at depth at most 2 * Nat.log 2 n this is 1 / (Nat.log 2 n + 15).
3. Concrete Word-RAM constants and trial schedule (fastCutTrials): [KargerStein1996], Section 4, Lemmas 4.1–4.3 state asymptotic O(n ^ 2 log n) time, O(n ^ 2) space and Ω(1 / log n) single-tree success probability, and the proof of Theorem 4.4 repeats the algorithm O(log ^ 2 n) times; the explicit coefficients in fastCutNodeTime and fastCutScratch, the trial schedule fastCutTrials n = (Nat.log 2 n + 15) * (Nat.log 2 n + 2) and the 1 / (2 * n) failure target are concrete parameter choices of this formalization.
4. Elementary quadratic potential Φ(k) = (k - 4) ^ 2: two_mul_pot_threshold_le proves 2 * (fastCutThreshold k - 4) ^ 2 ≤ (k - 4) ^ 2 for all k ≥ 7 via integer arithmetic (49 * 2 = 98 < 100 = 10 ^ 2), replacing real-valued recurrence unrolling in [KargerStein1996], Section 4, Lemmas 4.1–4.3.

Main definitions

• Cslib.Algorithms.WordRAM.Karger.fastCutThreshold: smallest integer t ≥ 2 satisfying k * (k - 1) ≤ 2 * t * (t - 1).
• Cslib.Algorithms.WordRAM.Karger.fastCutDepth, Cslib.Algorithms.WordRAM.Karger.frameSize, Cslib.Algorithms.WordRAM.Karger.fastCutScratch: recursion depth, per-frame memory footprint, and root-to-leaf active stack scratch bound.
• Cslib.Algorithms.WordRAM.Karger.fastCutNodeTime, Cslib.Algorithms.WordRAM.Karger.fastCutNodeQueries, Cslib.Algorithms.WordRAM.Karger.fastCutTrials: explicit time, rand-call, and high-probability amplification budgets.

Main results

• Cslib.Algorithms.WordRAM.Karger.two_mul_pot_threshold_le: quadratic potential halving 2 * (fastCutThreshold k - 4) ^ 2 ≤ (k - 4) ^ 2 for every k ≥ 7, proved via integer arithmetic without real square roots.
• Cslib.Algorithms.WordRAM.Karger.fastCutDepth_le_two_mul_log: recursion depth bound fastCutDepth k ≤ 2 * Nat.log 2 k.
• Cslib.Algorithms.WordRAM.Karger.fastCutScratch_le: total root-to-leaf stack workspace bound fastCutScratch n ≤ 26 * (n * n) for n ≥ 2 ([KargerStein1996], Section 4, Lemma 4.2; paraphrase).
• Cslib.Algorithms.WordRAM.Karger.two_branch_hit_prob_ge, Cslib.Algorithms.WordRAM.Karger.root_hit_prob_eq, Cslib.Algorithms.WordRAM.Karger.fastCutHighProb_failure_le: elementary ENNReal probability recurrence 1 - (1 - 1 / s) ^ 2 ≥ 2 / (s + 1) giving ≥ 1 / (Nat.log 2 n + 15) single-tree success ([KargerStein1996], Section 4, Lemma 4.3; paraphrase) and ≤ 1 / (2 * n) amplified failure (the minimum-cut-value part of [KargerStein1996], Section 4, Theorem 4.4; paraphrase) without Real.log or Real.exp.

References

• D. R. Karger and C. Stein, A New Approach to the Minimum Cut Problem
• M. Mitzenmacher and E. Upfal, Probability and Computing

Pure-integer threshold fastCutThreshold and quadratic potential Φ(k) = (k - 4) ^ 2

def Cslib.Algorithms.WordRAM.Karger.fastCutThresholdAux (k : ℕ) : ℕ → ℕ → ℕ

Bounded upward search for the smallest t satisfying k * (k - 1) ≤ 2 * t * (t - 1).

def Cslib.Algorithms.WordRAM.Karger.fastCutThreshold (k : ℕ) : ℕ

Pure-integer Karger–Stein contraction threshold: for k ≥ 7, the smallest t ≥ 2 such that k * (k - 1) ≤ 2 * t * (t - 1), ensuring ((t * (t - 1)) / (k * (k - 1)) : ℝ≥0∞) ≥ 1 / 2 ([KargerStein1996], Section 4, Lemma 4.3; paraphrase). This integer deviation from Figure 6's ⌈k / √2 + 1⌉ is never larger and is strictly smaller at e.g. k = 8 (t = 6 vs 7).

theorem Cslib.Algorithms.WordRAM.Karger.fastCutThreshold_ge_two {k : ℕ} (hk : 4 ≤ k) : 2 ≤ fastCutThreshold k

Lower bound 2 ≤ fastCutThreshold k for k ≥ 4.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutThreshold_le_pred {k : ℕ} (hk : 4 ≤ k) : fastCutThreshold k ≤ k - 1

Upper bound fastCutThreshold k ≤ k - 1 for k ≥ 4.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutThreshold_lt {k : ℕ} (hk : 4 ≤ k) : fastCutThreshold k < k

Strict decrease fastCutThreshold k < k for k ≥ 4.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutThreshold_spec {k : ℕ} (hk : 4 ≤ k) : k * (k - 1) ≤ 2 * fastCutThreshold k * (fastCutThreshold k - 1)

Defining threshold inequality k * (k - 1) ≤ 2 * fastCutThreshold k * (fastCutThreshold k - 1).

theorem Cslib.Algorithms.WordRAM.Karger.fastCutThreshold_lt_of_lt {k m : ℕ} (hk : 4 ≤ k) (hm2 : 2 ≤ m) (hmlt : m < fastCutThreshold k) : 2 * m * (m - 1) < k * (k - 1)

Minimality of fastCutThreshold k: every 2 ≤ m < fastCutThreshold k satisfies 2 * m * (m - 1) < k * (k - 1).

theorem Cslib.Algorithms.WordRAM.Karger.fastCutThreshold_ge_six {k : ℕ} (hk : 7 ≤ k) : 6 ≤ fastCutThreshold k

For k ≥ 7, the contraction threshold satisfies 6 ≤ fastCutThreshold k.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutThreshold_min {k : ℕ} (hk : 7 ≤ k) : 2 * (fastCutThreshold k - 1) * (fastCutThreshold k - 2) < k * (k - 1)

Predecessor minimality inequality 2 * (fastCutThreshold k - 1) * (fastCutThreshold k - 2) < k * (k - 1) for k ≥ 7.

theorem Cslib.Algorithms.WordRAM.Karger.two_mul_pot_threshold_le {k : ℕ} (hk : 7 ≤ k) : 2 * (fastCutThreshold k - 4) ^ 2 ≤ (k - 4) ^ 2

Quadratic potential halving (Φ(k) = (k - 4) ^ 2): for every k ≥ 7, 2 * (fastCutThreshold k - 4) ^ 2 ≤ (k - 4) ^ 2. Uses 49 * 2 = 98 < 100 = 10 ^ 2: if b ^ 2 < 2 * a ^ 2 (a = t - 4 ≥ 2, b = k - 4 ≥ 3), then (7 * b) ^ 2 < 100 * a ^ 2 = (10 * a) ^ 2, so 7 * b < 10 * a and b ^ 2 + 7 * b < 2 * a ^ 2 + 10 * a, contradicting 2 * (t - 1) * (t - 2) < k * (k - 1).

theorem Cslib.Algorithms.WordRAM.Karger.sq_le_six_mul_pot {k : ℕ} (hk : 7 ≤ k) : k ^ 2 ≤ 6 * (k - 4) ^ 2

For every k ≥ 7, k ^ 2 ≤ 6 * (k - 4) ^ 2.

theorem Cslib.Algorithms.WordRAM.Karger.two_mul_add_two_le_three_mul_threshold {k : ℕ} (hk : 7 ≤ k) : 2 * k + 2 ≤ 3 * fastCutThreshold k

For every k ≥ 7, 2 * k + 2 ≤ 3 * fastCutThreshold k, ensuring that linear per-node costs sum geometrically to O((k - 4) ^ 2) across the binary recursion tree.

Recursion depth, stack workspace, query count, and time recurrences

@[irreducible]

def Cslib.Algorithms.WordRAM.Karger.fastCutDepth (k : ℕ) : ℕ

Recursion depth of FastCut down to the base case k ≤ 6.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutDepth_of_lt_seven {k : ℕ} (hk : k < 7) : fastCutDepth k = 0

Base-case unfolding of fastCutDepth for k < 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutDepth_of_ge_seven {k : ℕ} (hk : 7 ≤ k) : fastCutDepth k = fastCutDepth (fastCutThreshold k) + 1

Recursive unfolding of fastCutDepth for k ≥ 7.

theorem Cslib.Algorithms.WordRAM.Karger.two_mul_pow_fastCutDepth_le_pot {k : ℕ} (hk : 7 ≤ k) : 2 * 2 ^ fastCutDepth k ≤ (k - 4) ^ 2

For every k ≥ 7, 2 * 2 ^ fastCutDepth k ≤ (k - 4) ^ 2.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutDepth_le_two_mul_log (k : ℕ) : fastCutDepth k ≤ 2 * Nat.log 2 k

The recursion depth of FastCut on k vertices is at most 2 * Nat.log 2 k.

def Cslib.Algorithms.WordRAM.Karger.frameSize (k : ℕ) : ℕ

Word count of one explicit stack frame at active vertex count k: 4 header words (parentFp, k, stage, savedVal1), immutable k × k frame matrix, working k × k contraction matrix, and k-word degree buffer.

@[irreducible]

def Cslib.Algorithms.WordRAM.Karger.fastCutScratch (k : ℕ) : ℕ

Total stack scratch words along any root-to-leaf active path starting at k vertices.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutScratch_of_lt_seven {k : ℕ} (hk : k < 7) : fastCutScratch k = frameSize k

Base-case unfolding of fastCutScratch for k < 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutScratch_of_ge_seven {k : ℕ} (hk : 7 ≤ k) : fastCutScratch k = frameSize k + fastCutScratch (fastCutThreshold k)

Recursive unfolding of fastCutScratch for k ≥ 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutScratch_le_pot {k : ℕ} (hk : 7 ≤ k) : fastCutScratch k ≤ 26 * (k - 4) ^ 2

Potential-based upper bound fastCutScratch k ≤ 26 * (k - 4) ^ 2 for k ≥ 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutScratch_le {n : ℕ} (hn : 2 ≤ n) : fastCutScratch n ≤ 26 * (n * n)

Total stack workspace for FastCut on n ≥ 2 vertices is at most 26 * (n * n) words.

@[irreducible]

def Cslib.Algorithms.WordRAM.Karger.fastCutNodeQueries (k : ℕ) : ℕ

Worst-case rand-call budget for executing one FastCut subtree of size k.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutNodeQueries_of_lt_seven {k : ℕ} (hk : k < 7) : fastCutNodeQueries k = k - 2

Base-case unfolding of fastCutNodeQueries for k < 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutNodeQueries_of_ge_seven {k : ℕ} (hk : 7 ≤ k) : fastCutNodeQueries k = 2 * (k - fastCutThreshold k) + 2 * fastCutNodeQueries (fastCutThreshold k)

Recursive unfolding of fastCutNodeQueries for k ≥ 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutNodeQueries_le {k : ℕ} (hk : 2 ≤ k) : fastCutNodeQueries k ≤ 6 * (k * k)

One FastCut tree on k ≥ 2 vertices makes at most 6 * (k * k) rand calls.

@[irreducible]

def Cslib.Algorithms.WordRAM.Karger.fastCutNodeTime (k : ℕ) : ℕ

Worst-case instruction budget for executing a FastCut subtree of size k inside fastCutLoop (200 * k ^ 2 internal frame overhead across the 3 stages, 2400 at a base leaf k ≤ 6).

theorem Cslib.Algorithms.WordRAM.Karger.fastCutNodeTime_of_lt_seven {k : ℕ} (hk : k < 7) : fastCutNodeTime k = 2400

Base-case unfolding of fastCutNodeTime for k < 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutNodeTime_of_ge_seven {k : ℕ} (hk : 7 ≤ k) : fastCutNodeTime k = 200 * (k * k) + 2 * fastCutNodeTime (fastCutThreshold k)

Recursive unfolding of fastCutNodeTime for k ≥ 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutNodeTime_le_pot {k : ℕ} (hk : 7 ≤ k) : fastCutNodeTime k ≤ (1200 * fastCutDepth k + 2700) * (k - 4) ^ 2

Potential-based upper bound fastCutNodeTime k ≤ (1200 * fastCutDepth k + 2700) * (k - 4) ^ 2 for k ≥ 7.

theorem Cslib.Algorithms.WordRAM.Karger.fastCutNodeTime_le {n : ℕ} (hn : 2 ≤ n) : fastCutNodeTime n ≤ 2400 * n ^ 2 * (Nat.log 2 n + 2)

Closed-form O(n ^ 2 log n) bound on fastCutNodeTime n for every n ≥ 2.

Elementary ENNReal probability bounds for Karger–Stein

theorem Cslib.Algorithms.WordRAM.Karger.half_le_threshold_survival {k : ℕ} (hk : 7 ≤ k) : 1 / 2 ≤ ↑(fastCutThreshold k * (fastCutThreshold k - 1)) / ↑(k * (k - 1))

At k ≥ 7, contracting down to t = fastCutThreshold k preserves a fixed minimum cut with probability t * (t - 1) / (k * (k - 1)) ≥ 1 / 2.

theorem Cslib.Algorithms.WordRAM.Karger.base_survival_ge {k : ℕ} (hk2 : 2 ≤ k) (hk6 : k ≤ 6) : 2 / 30 ≤ 2 / ↑(k * (k - 1))

At a base leaf 2 ≤ k ≤ 6, a single contraction down to 2 vertices hits a fixed minimum cut with probability 2 / (k * (k - 1)) ≥ 2 / 30.

theorem Cslib.Algorithms.WordRAM.Karger.half_mul_two_div_eq {s : ℕ} (hs : 1 ≤ s) : 1 / 2 * (2 / ↑s) = 1 / ↑s

(1 / 2) * (2 / s) = 1 / s in ℝ≥0∞ for 1 ≤ s.

theorem Cslib.Algorithms.WordRAM.Karger.one_sub_sq_one_sub_inv_ge {s : ℕ} (hs : 1 ≤ s) : 2 / ↑(s + 1) ≤ 1 - (1 - 1 / ↑s) ^ 2

Elementary recurrence 2 / (s + 1) ≤ 1 - (1 - 1 / s) ^ 2 in ℝ≥0∞ for 1 ≤ s, derived from (2 * s - 1) * (s + 1) = 2 * s ^ 2 + s - 1 ≥ 2 * s ^ 2.

theorem Cslib.Algorithms.WordRAM.Karger.two_branch_hit_prob_ge {α β γ : Type} (m₁ : ProbComp α) (m₂ : α → ProbComp β) (f : α → β → γ) (hit₁ : Set α) (hit : Set γ) {s : ℕ} (hs : 1 ≤ s) (hb₁ : 1 / ↑s ≤ m₁.eval.toOuterMeasure hit₁) (hprop₁ : ∀ a ∈ OracleComp.support m₁, a ∈ hit₁ → ∀ b ∈ OracleComp.support (m₂ a), f a b ∈ hit) (hb₂ : ∀ a ∈ OracleComp.support m₁, a ∉ hit₁ → 1 / ↑s ≤ (PMF.map (f a) (m₂ a).eval).toOuterMeasure hit) : 2 / ↑(s + 1) ≤ (do let a ← m₁ let b ← m₂ a pure (f a b)).eval.toOuterMeasure hit

Sequential two-branch success probability recurrence on ProbComp: if Branch 1 hits hit₁ with probability ≥ 1 / s, any outcome in hit₁ guarantees f a b ∈ hit on every supported b, and conditioned on any outcome outside hit₁ Branch 2 achieves f a b ∈ hit with probability ≥ 1 / s, then the combined computation hits hit with probability ≥ 2 / (s + 1).

theorem Cslib.Algorithms.WordRAM.Karger.root_hit_prob_eq (n : ℕ) : 2 / ↑(2 * Nat.log 2 n + 30) = 1 / ↑(Nat.log 2 n + 15)

At the root depth budget d = 2 * Nat.log 2 n, 2 / (d + 30) = 1 / (Nat.log 2 n + 15).

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

Concrete O(log ^ 2 n) trial schedule (Nat.log 2 n + 15) * (Nat.log 2 n + 2) used by fastCutHighProbProgram to achieve failure probability ≤ 1 / (2 * n) (instantiating the asymptotic O(log ^ 2 n) repetition count in the proof of [KargerStein1996], Section 4, Theorem 4.4; paraphrase).

theorem Cslib.Algorithms.WordRAM.Karger.fastCutTrials_pos (n : ℕ) : 1 ≤ fastCutTrials n

For every n, fastCutTrials n executes at least one FastCut tree (1 ≤ fastCutTrials n).

theorem Cslib.Algorithms.WordRAM.Karger.fastCutHighProb_failure_le (n : ℕ) : (1 - 1 / ↑(Nat.log 2 n + 15)) ^ fastCutTrials n ≤ 1 / ↑(2 * n)

Elementary failure probability bound for fastCutTrials n independent FastCut trees: (1 - 1 / (Nat.log 2 n + 15)) ^ fastCutTrials n ≤ 1 / (2 * n).

theorem Cslib.Algorithms.WordRAM.Karger.fastCutHighProb_failure_le_inv_n (n : ℕ) : (1 - 1 / ↑(Nat.log 2 n + 15)) ^ fastCutTrials n ≤ 1 / ↑n

Weakened failure probability bound (1 - 1 / (Nat.log 2 n + 15)) ^ fastCutTrials n ≤ 1 / n.