Karger's randomized global minimum cut algorithm on the word RAM

Implements Karger's randomized contraction algorithm [Karger1993] on n-vertex weighted undirected multigraphs (n ≥ 2, IsMultigraph W) over Cslib.WordRAM.Basis.standard, providing three complete machine-level endpoints built on the workspace-relocatable subroutine contractDownTo:

1. Single-trial contraction (singleProgram, r = 16): runs on n :: flattenMatrix W, computes row degrees at 2 + n ^ 2, contracts in place down to 2 supervertices in at most 42 * n ^ 2 + 12 * n + 21 steps and n - 2 rand calls, outputs a genuine non-trivial cut weight cutWeight W C ≥ minCut W on every supported branch, and achieves minCut W with probability at least 2 / (n * (n - 1)) whenever 0 < minCut W.
2. Repeated-trial amplification (amplifiedProgram, r = 22): runs on R :: n :: flattenMatrix W (1 ≤ R), copies the immutable input matrix from [3, 3 + n ^ 2) into [3 + n ^ 2, 3 + 2 * n ^ 2) via Cslib.WordRAM.ArrayCopy before each of R independent contractions, halts within R * (50 * n ^ 2 + 12 * n + 30) + 16 steps and R * (n - 2) rand calls with a genuine non-trivial cut weight ≥ minCut W, and misses minCut W with probability at most (1 - 2 / (n * (n - 1))) ^ R whenever 0 < minCut W.
3. Explicit O(n ^ 4 log n) high-probability global minimum cut (highProbProgram, r = 22): runs on n :: flattenMatrix W, computes highProbTrials n = (n * (n - 1) / 2) * (⌊log₂ n⌋ + 2) in registers using shifts and multiplication (without .div or .mod), halts within 33 * n ^ 4 * (Nat.log 2 n + 2) steps with a genuine non-trivial cut weight ≥ minCut W, and misses minCut W with probability at most 1 / (2 * n) (hence at most 1 / n) whenever 0 < minCut W, via an elementary Bernoulli power bound without Real.exp.

Source statements and notation mapping

• Source locators (paraphrase):
  • [Karger1993], Section 2, Theorem 2.1 and Corollary 2.1 (paraphrase): contracting uniformly chosen edges in an n-vertex multigraph down to 2 meta-vertices returns 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 amplifies the success probability to 1 - 1 / poly(n).
  • [KargerStein1996], Section 2, Lemma 2.1, Theorem 2.2, and Corollary 2.3, Section 2.1, Corollary 2.4, and Section 3 ("Implementing the Contraction Algorithm", Section 3.1, Lemma 3.1 and Section 3.2, Corollary 3.2) (paraphrase): contracting an n-vertex weighted multigraph from k down to t supervertices via edge-weight-proportional selection preserves any fixed minimum cut with probability at least C(t, 2) / C(k, 2) = t * (t - 1) / (k * (k - 1)) (2 / (n * (n - 1)) at t = 2, k = n), and an n × n weighted adjacency matrix with a maintained row-degree array executes each trial in O(n ^ 2) total time (O(n) per step in Section 3.2).
  • [MitzenmacherUpfal2017], Section 1.5, Theorem 1.8 (paraphrase): multiplying single-step survival bounds 1 - 2 / i from i = n down to 3 yields 2 / (n * (n - 1)).
• Notation mapping, implementation variants, and parameter choices:
  • C(n, 2)⁻¹ ↔ 2 / (n * (n - 1)) (singleProgram_spec, amplifiedProgram_spec);
  • whereas [KargerStein1996], Section 3.1 draws twice (u proportional to D[u] then v proportional to W[u, v] via two Random-Select calls), contractDownTo uses an equivalent single-draw variant: one unit-cost rand draw in {0, …, S - 1} (S = totalDoubledWeight W) resolved through linear prefix-sum scans uScan (rowDeg) and vScan (W[u, v]), achieving the same 2 * W[u, v] / S distribution of Lemma 3.1; and whereas Section 3.2 states O(n) per contraction step, our swap-compaction of active slot k - 1 into v gives O(k) instructions on k active supervertices;
  • the concrete trial count highProbTrials n = (n * (n - 1) / 2) * (Nat.log 2 n + 2) and the 1 / (2 * n) failure bound in highProbProgram_spec are our own parameter choice instantiating the O(n ^ 2 log n) amplification of [Karger1993], Section 2, Corollary 2.1;
  • the hypothesis 0 < minCut W in the probability clauses is included only for proof convenience (when minCut W = 0, deterministic S = 0 contraction still halts without faulting and outputs a valid non-trivial cut weight).

Main definitions

• Cslib.Algorithms.WordRAM.Karger.singleCode, Cslib.Algorithms.WordRAM.Karger.singleProgram, Cslib.Algorithms.WordRAM.Karger.singleTime: single-trial Basic Karger (r = 16).
• Cslib.Algorithms.WordRAM.Karger.ampCore, Cslib.Algorithms.WordRAM.Karger.amplifiedCode, Cslib.Algorithms.WordRAM.Karger.amplifiedProgram, Cslib.Algorithms.WordRAM.Karger.amplifiedTime: R-trial amplified Karger (r = 22).
• Cslib.Algorithms.WordRAM.Karger.highProbCode, Cslib.Algorithms.WordRAM.Karger.highProbProgram, Cslib.Algorithms.WordRAM.Karger.highProbTime: O(n ^ 4 log n) high-probability global min-cut (r = 22).

Main results

• Cslib.Algorithms.WordRAM.Karger.singleProgram_spec: worst-case O(n ^ 2) step bound, n - 2 rand-call bound, pathwise non-trivial cut realization, Modifies frame, and 2 / (n * (n - 1)) success probability lower bound for singleProgram.
• Cslib.Algorithms.WordRAM.Karger.amplifiedProgram_spec: worst-case O(R * n ^ 2) step bound, R * (n - 2) rand-call bound, pathwise non-trivial cut realization, Modifies frame, and (1 - 2 / (n * (n - 1))) ^ R failure probability upper bound for amplifiedProgram.
• Cslib.Algorithms.WordRAM.Karger.highProbProgram_spec, Cslib.Algorithms.WordRAM.Karger.highProbProgram_failure_le_inv_n: worst-case 33 * n ^ 4 * (Nat.log 2 n + 2) step bound, pathwise non-trivial cut realization, Modifies frame, and 1 / (2 * n) (1 / n) failure probability upper bound for highProbProgram.

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

Word-size sufficiency and Data.init matrix layout

theorem Cslib.Algorithms.WordRAM.Karger.fits_workspace_of_logWidth_three {n w : ℕ} (hn : 2 ≤ n) (hw : WordRAM.logWidth 3 n ≤ w) : WordRAM.Fits w (3 + 2 * (n * n) + n)

Under 2 ≤ n and logWidth 3 n ≤ w, workspace end-addresses up to 3 + 2 * (n * n) + n fit in w-bit words.

theorem Cslib.Algorithms.WordRAM.Karger.fits_highProbTrials_of_logWidth_three {n w : ℕ} (hn : 2 ≤ n) (hw : WordRAM.logWidth 3 n ≤ w) : WordRAM.Fits w (highProbTrials n)

Under 2 ≤ n and logWidth 3 n ≤ w, highProbTrials n and intermediate n * (n - 1) and Nat.log 2 n + 2 values fit in w-bit words.

theorem Cslib.Algorithms.WordRAM.Karger.inputFits_single {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (totalDoubledWeight W)) : WordRAM.InputFits w (n :: flattenMatrix W)

logWidth 3 n ≤ w and Fits w (totalDoubledWeight W) suffice for InputFits w (n :: flattenMatrix W).

theorem Cslib.Algorithms.WordRAM.Karger.inputFits_amplified {R n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hw : WordRAM.logWidth 3 n ≤ w) (hR : WordRAM.Fits w R) (htot : WordRAM.Fits w (totalDoubledWeight W)) : WordRAM.InputFits w (R :: n :: flattenMatrix W)

logWidth 3 n ≤ w, Fits w R, and Fits w (totalDoubledWeight W) suffice for InputFits w (R :: n :: flattenMatrix W).

theorem Cslib.Algorithms.WordRAM.Karger.holdsMatrix_init_append {r n : ℕ} (pfx : List ℕ) (W : Fin n → Fin n → ℕ) : HoldsMatrix (WordRAM.Data.init (pfx ++ flattenMatrix W)).mem (1 + pfx.length) n W

In Data.init (pfx ++ flattenMatrix W), the flattened matrix occupies memory starting at 1 + pfx.length with stride n.

theorem Cslib.Algorithms.WordRAM.Karger.holdsMatrix_init_single {r n : ℕ} (W : Fin n → Fin n → ℕ) : HoldsMatrix (WordRAM.Data.init (n :: flattenMatrix W)).mem 2 n W

In Data.init (n :: flattenMatrix W), memory holds W at base 2 with stride n.

theorem Cslib.Algorithms.WordRAM.Karger.holdsMatrix_init_amplified {r R n : ℕ} (W : Fin n → Fin n → ℕ) : HoldsMatrix (WordRAM.Data.init (R :: n :: flattenMatrix W)).mem 3 n W

In Data.init (R :: n :: flattenMatrix W), memory holds W at base 3 with stride n.

Endpoint 1: Single-trial Basic Karger (r = 16)

def Cslib.Algorithms.WordRAM.Karger.singleSetup : WordRAM.Code WordRAM.Basis.standard 16

Setup for singleCode: read n from mem[1] and configure (wBase, dBase, stride, activeK, targetT) = (2, 2 + n * n, n, n, 2).

def Cslib.Algorithms.WordRAM.Karger.singlePost : WordRAM.Code WordRAM.Basis.standard 16

Postprocessing for singleCode: load the contracted superedge weight mem[wBase + 1] into val1.

def Cslib.Algorithms.WordRAM.Karger.singleCode : WordRAM.Code WordRAM.Basis.standard 16

Structured 16-register single-trial Karger contraction program on n :: flattenMatrix W.

def Cslib.Algorithms.WordRAM.Karger.singleProgram : WordRAM.Program WordRAM.Basis.standard 16

Compiled 16-register single-trial Karger contraction program.

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

Worst-case instruction bound 42 * n ^ 2 + 12 * n + 21 for singleProgram.

theorem Cslib.Algorithms.WordRAM.Karger.singleSetup_exec {w n : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hw : WordRAM.logWidth 3 n ≤ w) : ∃ (y : WordRAM.Data 16), WordRAM.Exec w singleSetup (WordRAM.Data.init (n :: flattenMatrix W)) y 7 ∧ y.mem = (WordRAM.Data.init (n :: flattenMatrix W)).mem ∧ y.regs Reg.wBase = 2 ∧ y.regs Reg.dBase = 2 + n * n ∧ y.regs Reg.stride = n ∧ y.regs Reg.activeK = n ∧ y.regs Reg.targetT = 2

theorem Cslib.Algorithms.WordRAM.Karger.singlePost_exec {w wb : ℕ} {x : WordRAM.Data 16} (hwBase : x.regs Reg.wBase = wb) (h1 : WordRAM.Fits w 1) (hwb1 : WordRAM.Fits w (wb + 1)) : ∃ (y : WordRAM.Data 16), WordRAM.Exec w singlePost x y 3 ∧ y.mem = x.mem ∧ y.regs Reg.val1 = x.mem (wb + 1)

theorem Cslib.Algorithms.WordRAM.Karger.singleCode_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (totalDoubledWeight W)) : ∃ (m : ProbComp (WordRAM.Data 16 × ℕ)), WordRAM.ExecRand w singleCode (WordRAM.Data.init (n :: flattenMatrix W)) m ∧ OracleComp.IsQueryBounded m (n - 2) ∧ (∀ z ∈ OracleComp.support m, z.2 + 1 ≤ singleTime n ∧ WordRAM.Modifies (Finset.Ico 2 (2 + n * n + n)) (WordRAM.Data.init (n :: flattenMatrix W)).mem z.1.mem ∧ ∃ (C : Finset (Fin n)), IsNonTrivialCut C ∧ z.1.regs Reg.val1 = cutWeight W C) ∧ (0 < minCut W → 2 / ↑(n * (n - 1)) ≤ m.eval.toOuterMeasure {z : WordRAM.Data 16 × ℕ | z.1.regs Reg.val1 = minCut W})

Structured ProbComp specification of singleCode.

theorem Cslib.Algorithms.WordRAM.Karger.singleProgram_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (totalDoubledWeight W)) : have input := n :: flattenMatrix W; WordRAM.RandHaltsWithin w singleProgram (WordRAM.State.init input) (singleTime n) ∧ WordRAM.RandCallsBounded w singleProgram (WordRAM.State.init input) (singleTime n) (n - 2) ∧ (∀ cfg ∈ OracleComp.support (WordRAM.runRand w singleProgram (singleTime n) (WordRAM.RandCfg.running (WordRAM.State.init input))), ∃ (y : WordRAM.Data 16) (C : Finset (Fin n)), cfg = WordRAM.RandCfg.halted (cutWeight W C) y ∧ WordRAM.Data.Bounded w y ∧ IsNonTrivialCut C ∧ minCut W ≤ cutWeight W C ∧ WordRAM.Modifies (Finset.Ico 2 (2 + n * n + n)) (WordRAM.Data.init input).mem y.mem) ∧ (0 < minCut W → 2 / ↑(n * (n - 1)) ≤ (WordRAM.evalRand w singleProgram (singleTime n) (WordRAM.State.init input)).toOuterMeasure {cfg : WordRAM.RandCfg 16 | ∃ (y : WordRAM.Data 16), cfg = WordRAM.RandCfg.halted (minCut W) y})

Single-trial Basic Karger specification (singleProgram). At word size w ≥ logWidth 3 n when totalDoubledWeight W < 2 ^ w:

1. singleProgram halts within singleTime n = 42 * n ^ 2 + 12 * n + 21 steps;
2. executes at most n - 2 rand calls;
3. on every supported branch, outputs cutWeight W C ≥ minCut W for a genuine non-trivial cut C of W while modifying memory only in [2, 2 + n * n + n);
4. when 0 < minCut W (excluded only for proof convenience; S = 0 contraction still halts fault-free with a valid cut weight), outputs minCut W with probability at least 2 / (n * (n - 1)).

Shared R-trial amplification engine (r = 22)

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.zero : Fin 22

Constant register 0 (Reg.zero embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.one : Fin 22

Constant register 1 (Reg.one embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.wBase : Fin 22

Working matrix base address (Reg.wBase embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.dBase : Fin 22

Working degree-array base address (Reg.dBase embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.stride : Fin 22

Working matrix row stride (Reg.stride embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.activeK : Fin 22

Active supervertex count k (Reg.activeK embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.targetT : Fin 22

Target supervertex count t (Reg.targetT embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.totS : Fin 22

Active doubled edge weight S (Reg.totS embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.idx : Fin 22

Loop index scratch register (Reg.idx embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.rem : Fin 22

Loop counter / remainder scratch register (Reg.rem embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.addr1 : Fin 22

Primary scratch address register (Reg.addr1 embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.val1 : Fin 22

Primary scratch value register (Reg.val1 embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.val2 : Fin 22

Secondary scratch value register (Reg.val2 embedded into Fin 22).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.srcBase : Fin 22

Base address of the immutable input matrix W.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.nOrig : Fin 22

Original vertex count n, preserved across all trials.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.matLen : Fin 22

Word count n * n of the flattened matrix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.numTrials : Fin 22

Total number R of independent trials to execute.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.trialIdx : Fin 22

Number of trials completed so far (0 .. R).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.AmpReg.bestVal : Fin 22

Minimum cut weight seen across completed trials.

def Cslib.Algorithms.WordRAM.Karger.copyRegMap : Fin 7 → Fin 22

Injective register map embedding Cslib.WordRAM.ArrayCopy (r = 7) into Fin 22 with (src, dst, len, idx, addr, value, one) = (srcBase, wBase, matLen, idx, addr1, val1, one).

theorem Cslib.Algorithms.WordRAM.Karger.copyRegMap_injective : Function.Injective copyRegMap

def Cslib.Algorithms.WordRAM.Karger.copyMatrixCode : WordRAM.Code WordRAM.Basis.standard 22

Copy matLen words from srcBase to wBase via Cslib.WordRAM.ArrayCopy.program.

theorem Cslib.Algorithms.WordRAM.Karger.copyMatrixCode_exec {w sb wb n : ℕ} {W : Fin n → Fin n → ℕ} {x : WordRAM.Data 22} (hsb : x.regs AmpReg.srcBase = sb) (hwb : x.regs AmpReg.wBase = wb) (hlen : x.regs AmpReg.matLen = n * n) (hdisj : sb + n * n ≤ wb) (h1 : WordRAM.Fits w 1) (hwEnd : WordRAM.Fits w (wb + n * n)) (hsrc_mat : HoldsMatrix x.mem sb n W) : ∃ (y : WordRAM.Data 22), WordRAM.ExecWithin w copyMatrixCode x y (7 * (n * n) + 4) ∧ HoldsMatrix y.mem wb n W ∧ WordRAM.Modifies (Finset.Ico wb (wb + n * n)) x.mem y.mem ∧ y.regs AmpReg.wBase = wb ∧ y.regs AmpReg.dBase = x.regs AmpReg.dBase ∧ y.regs AmpReg.srcBase = sb ∧ y.regs AmpReg.nOrig = x.regs AmpReg.nOrig ∧ y.regs AmpReg.matLen = n * n ∧ y.regs AmpReg.numTrials = x.regs AmpReg.numTrials ∧ y.regs AmpReg.trialIdx = x.regs AmpReg.trialIdx ∧ y.regs AmpReg.bestVal = x.regs AmpReg.bestVal

def Cslib.Algorithms.WordRAM.Karger.ampTrialPost : WordRAM.Code WordRAM.Basis.standard 22

Postprocessing at the end of each trial: extract mem[wBase + 1], update bestVal (replacing it unconditionally on trial 0 and taking the minimum thereafter), and increment trialIdx.

def Cslib.Algorithms.WordRAM.Karger.ampTrialBody : WordRAM.Code WordRAM.Basis.standard 22

Single amplification trial: copy [srcBase, srcBase + n * n) into wBase, initialize row degrees at dBase, contract down to 2 supervertices, and update bestVal.

def Cslib.Algorithms.WordRAM.Karger.ampLoop : WordRAM.Code WordRAM.Basis.standard 22

Loop running numTrials independent contractions.

def Cslib.Algorithms.WordRAM.Karger.ampCore : WordRAM.Code WordRAM.Basis.standard 22

Shared amplification core assuming srcBase, nOrig, and numTrials are initialized in registers.

structure Cslib.Algorithms.WordRAM.Karger.AmpInv (w sb n R i : ℕ) (W : Fin n → Fin n → ℕ) (mem₀ : ℕ → ℕ) (x : WordRAM.Data 22) : Prop

Loop invariant for ampLoop at trialIdx = i ≤ R.

• regs_srcBase : x.regs AmpReg.srcBase = sb
• regs_wBase : x.regs AmpReg.wBase = sb + n * n
• regs_dBase : x.regs AmpReg.dBase = sb + 2 * (n * n)
• regs_nOrig : x.regs AmpReg.nOrig = n
• regs_matLen : x.regs AmpReg.matLen = n * n
• regs_numTrials : x.regs AmpReg.numTrials = R
• regs_trialIdx : x.regs AmpReg.trialIdx = i
• src_matrix : HoldsMatrix x.mem sb n W
• modifies_ws : WordRAM.Modifies (Finset.Ico (sb + n * n) (sb + 2 * (n * n) + n)) mem₀ x.mem
• best_cut : 0 < i → ∃ (C : Finset (Fin n)), IsNonTrivialCut C ∧ x.regs AmpReg.bestVal = cutWeight W C

theorem Cslib.Algorithms.WordRAM.Karger.ampTrialPost_exec {w wb i R : ℕ} {x : WordRAM.Data 22} (hwb : x.regs AmpReg.wBase = wb) (hti : x.regs AmpReg.trialIdx = i) (hiR : i < R) (h1 : WordRAM.Fits w 1) (hwb1 : WordRAM.Fits w (wb + 1)) (hR_fit : WordRAM.Fits w R) : ∃ (y : WordRAM.Data 22), WordRAM.ExecWithin w ampTrialPost x y 10 ∧ y.mem = x.mem ∧ y.regs AmpReg.srcBase = x.regs AmpReg.srcBase ∧ y.regs AmpReg.wBase = wb ∧ y.regs AmpReg.dBase = x.regs AmpReg.dBase ∧ y.regs AmpReg.nOrig = x.regs AmpReg.nOrig ∧ y.regs AmpReg.matLen = x.regs AmpReg.matLen ∧ y.regs AmpReg.numTrials = x.regs AmpReg.numTrials ∧ y.regs AmpReg.trialIdx = i + 1 ∧ y.regs AmpReg.bestVal = if i = 0 then x.mem (wb + 1) else min (x.mem (wb + 1)) (x.regs AmpReg.bestVal)

theorem Cslib.Algorithms.WordRAM.Karger.ampTrialBody_spec {w sb n R i : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} {x : WordRAM.Data 22} (hn : 2 ≤ n) (hW : IsMultigraph W) (hiR : i < R) (h1 : WordRAM.Fits w 1) (hdEnd : WordRAM.Fits w (sb + 2 * (n * n) + n)) (hR_fit : WordRAM.Fits w R) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hinv : AmpInv w sb n R i W mem₀ x) : ∃ (m : ProbComp (WordRAM.Data 22 × ℕ)), WordRAM.ExecRand w ampTrialBody x m ∧ OracleComp.IsQueryBounded m (n - 2) ∧ (∀ z ∈ OracleComp.support m, z.2 ≤ 49 * n ^ 2 + 12 * n + 27 ∧ AmpInv w sb n R (i + 1) W mem₀ z.1 ∧ (0 < i → x.regs AmpReg.bestVal = minCut W → z.1.regs AmpReg.bestVal = minCut W)) ∧ (0 < minCut W → m.eval.toOuterMeasure {z : WordRAM.Data 22 × ℕ | z.1.regs AmpReg.bestVal ≠ minCut W} ≤ 1 - 2 / ↑(n * (n - 1)))

Specification of a single trial ampTrialBody from AmpInv.

theorem Cslib.Algorithms.WordRAM.Karger.ampLoop_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (h1 : WordRAM.Fits w 1) (hdEnd : WordRAM.Fits w (sb + 2 * (n * n) + n)) (hR_fit : WordRAM.Fits w R) (htot : WordRAM.Fits w (totalDoubledWeight W)) (rem i : ℕ) (x : WordRAM.Data 22) : i + rem = R → AmpInv w sb n R i W mem₀ x → ∃ (m : ProbComp (WordRAM.Data 22 × ℕ)), WordRAM.ExecRand w ampLoop x m ∧ OracleComp.IsQueryBounded m (rem * (n - 2)) ∧ (∀ z ∈ OracleComp.support m, z.2 ≤ rem * (50 * n ^ 2 + 12 * n + 30) + 2 ∧ AmpInv w sb n R R W mem₀ z.1 ∧ (0 < i → x.regs AmpReg.bestVal = minCut W → z.1.regs AmpReg.bestVal = minCut W)) ∧ (0 < minCut W → m.eval.toOuterMeasure {z : WordRAM.Data 22 × ℕ | z.1.regs AmpReg.bestVal ≠ minCut W} ≤ (1 - 2 / ↑(n * (n - 1))) ^ rem)

Specification of ampLoop over rem = R - i remaining trials.

theorem Cslib.Algorithms.WordRAM.Karger.ampCore_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {x : WordRAM.Data 22} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : IsMultigraph W) (hsb : x.regs AmpReg.srcBase = sb) (hnOrig : x.regs AmpReg.nOrig = n) (hnumT : x.regs AmpReg.numTrials = R) (h1 : WordRAM.Fits w 1) (hdEnd : WordRAM.Fits w (sb + 2 * (n * n) + n)) (hR_fit : WordRAM.Fits w R) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hsrc_mat : HoldsMatrix x.mem sb n W) : ∃ (m : ProbComp (WordRAM.Data 22 × ℕ)), WordRAM.ExecRand w ampCore x m ∧ OracleComp.IsQueryBounded m (R * (n - 2)) ∧ (∀ z ∈ OracleComp.support m, z.2 ≤ R * (50 * n ^ 2 + 12 * n + 30) + 8 ∧ WordRAM.Modifies (Finset.Ico (sb + n * n) (sb + 2 * (n * n) + n)) x.mem z.1.mem ∧ ∃ (C : Finset (Fin n)), IsNonTrivialCut C ∧ z.1.regs AmpReg.bestVal = cutWeight W C) ∧ (0 < minCut W → m.eval.toOuterMeasure {z : WordRAM.Data 22 × ℕ | z.1.regs AmpReg.bestVal ≠ minCut W} ≤ (1 - 2 / ↑(n * (n - 1))) ^ R)

Specification of ampCore for 1 ≤ R trials from any state with srcBase = sb, nOrig = n, numTrials = R, and HoldsMatrix x.mem sb n W.

Endpoint 2: Amplified R-trial Karger (r = 22)

def Cslib.Algorithms.WordRAM.Karger.amplifiedSetup : WordRAM.Code WordRAM.Basis.standard 22

Setup for amplifiedCode on R :: n :: flattenMatrix W: load R = mem[1], n = mem[2], and set srcBase = 3.

def Cslib.Algorithms.WordRAM.Karger.amplifiedCode : WordRAM.Code WordRAM.Basis.standard 22

Structured 22-register R-trial Karger program on R :: n :: flattenMatrix W.

def Cslib.Algorithms.WordRAM.Karger.amplifiedProgram : WordRAM.Program WordRAM.Basis.standard 22

Compiled 22-register R-trial Karger program.

def Cslib.Algorithms.WordRAM.Karger.amplifiedTime (R n : ℕ) : ℕ

Worst-case instruction bound R * (50 * n ^ 2 + 12 * n + 30) + 16 for amplifiedProgram.

theorem Cslib.Algorithms.WordRAM.Karger.amplifiedSetup_exec {w R n : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hw : WordRAM.logWidth 3 n ≤ w) : ∃ (y : WordRAM.Data 22), WordRAM.Exec w amplifiedSetup (WordRAM.Data.init (R :: n :: flattenMatrix W)) y 5 ∧ y.mem = (WordRAM.Data.init (R :: n :: flattenMatrix W)).mem ∧ y.regs AmpReg.srcBase = 3 ∧ y.regs AmpReg.nOrig = n ∧ y.regs AmpReg.numTrials = R

theorem Cslib.Algorithms.WordRAM.Karger.amplifiedCode_spec {R n w : ℕ} {W : Fin n → Fin n → ℕ} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (hR_fit : WordRAM.Fits w R) (htot : WordRAM.Fits w (totalDoubledWeight W)) : ∃ (m : ProbComp (WordRAM.Data 22 × ℕ)), WordRAM.ExecRand w amplifiedCode (WordRAM.Data.init (R :: n :: flattenMatrix W)) m ∧ OracleComp.IsQueryBounded m (R * (n - 2)) ∧ (∀ z ∈ OracleComp.support m, z.2 + 1 ≤ amplifiedTime R n ∧ WordRAM.Modifies (Finset.Ico (3 + n * n) (3 + 2 * (n * n) + n)) (WordRAM.Data.init (R :: n :: flattenMatrix W)).mem z.1.mem ∧ ∃ (C : Finset (Fin n)), IsNonTrivialCut C ∧ z.1.regs AmpReg.bestVal = cutWeight W C) ∧ (0 < minCut W → m.eval.toOuterMeasure {z : WordRAM.Data 22 × ℕ | z.1.regs AmpReg.bestVal ≠ minCut W} ≤ (1 - 2 / ↑(n * (n - 1))) ^ R)

Structured ProbComp specification of amplifiedCode.

theorem Cslib.Algorithms.WordRAM.Karger.amplifiedProgram_spec {R n w : ℕ} {W : Fin n → Fin n → ℕ} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (hR_fit : WordRAM.Fits w R) (htot : WordRAM.Fits w (totalDoubledWeight W)) : have input := R :: n :: flattenMatrix W; WordRAM.RandHaltsWithin w amplifiedProgram (WordRAM.State.init input) (amplifiedTime R n) ∧ WordRAM.RandCallsBounded w amplifiedProgram (WordRAM.State.init input) (amplifiedTime R n) (R * (n - 2)) ∧ (∀ cfg ∈ OracleComp.support (WordRAM.runRand w amplifiedProgram (amplifiedTime R n) (WordRAM.RandCfg.running (WordRAM.State.init input))), ∃ (y : WordRAM.Data 22) (C : Finset (Fin n)), cfg = WordRAM.RandCfg.halted (cutWeight W C) y ∧ WordRAM.Data.Bounded w y ∧ IsNonTrivialCut C ∧ minCut W ≤ cutWeight W C ∧ WordRAM.Modifies (Finset.Ico (3 + n * n) (3 + 2 * (n * n) + n)) (WordRAM.Data.init input).mem y.mem) ∧ (0 < minCut W → (WordRAM.evalRand w amplifiedProgram (amplifiedTime R n) (WordRAM.State.init input)).toOuterMeasure {cfg : WordRAM.RandCfg 22 | ∀ (y : WordRAM.Data 22), cfg ≠ WordRAM.RandCfg.halted (minCut W) y} ≤ (1 - 2 / ↑(n * (n - 1))) ^ R)

R-trial amplified Karger specification (amplifiedProgram). At word size w ≥ logWidth 3 n when 1 ≤ R, R < 2 ^ w, and totalDoubledWeight W < 2 ^ w:

1. amplifiedProgram halts within amplifiedTime R n = R * (50 * n ^ 2 + 12 * n + 30) + 16 steps;
2. executes at most R * (n - 2) rand calls;
3. on every supported branch, outputs cutWeight W C ≥ minCut W for a genuine non-trivial cut C of W while modifying memory only in [3 + n * n, 3 + 2 * (n * n) + n);
4. when 0 < minCut W (excluded only for proof convenience; S = 0 contraction still halts fault-free with a valid cut weight), misses minCut W with probability at most (1 - 2 / (n * (n - 1))) ^ R.

Endpoint 3: Explicit O(n ^ 4 log n) high-probability global minimum cut (r = 22)

def Cslib.Algorithms.WordRAM.Karger.logStep : WordRAM.Code WordRAM.Basis.standard 22

Body of logLoop: halve rem via right-shift by 1 and increment idx.

def Cslib.Algorithms.WordRAM.Karger.logLoop : WordRAM.Code WordRAM.Basis.standard 22

Loop computing idx = Nat.log 2 n from rem = n (n ≥ 1), idx = 0, one = 1.

def Cslib.Algorithms.WordRAM.Karger.highProbSetup : WordRAM.Code WordRAM.Basis.standard 22

Setup for highProbCode on n :: flattenMatrix W: load n = mem[1], compute numTrials = highProbTrials n = (n * (n - 1) / 2) * (Nat.log 2 n + 2) using shifts and multiplications, and set srcBase = 2.

def Cslib.Algorithms.WordRAM.Karger.highProbCode : WordRAM.Code WordRAM.Basis.standard 22

Structured 22-register O(n ^ 4 log n) high-probability Karger program on n :: flattenMatrix W.

def Cslib.Algorithms.WordRAM.Karger.highProbProgram : WordRAM.Program WordRAM.Basis.standard 22

Compiled 22-register O(n ^ 4 log n) high-probability Karger program.

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

Worst-case instruction bound 33 * n ^ 4 * (Nat.log 2 n + 2) for highProbProgram.

theorem Cslib.Algorithms.WordRAM.Karger.logLoop_exec {w n : ℕ} {x : WordRAM.Data 22} (hn : 1 ≤ n) (hone : x.regs AmpReg.one = 1) (hrem : x.regs AmpReg.rem = n) (hidx : x.regs AmpReg.idx = 0) (hnOrig : x.regs AmpReg.nOrig = n) (hn_fit : WordRAM.Fits w n) (hlg_fit : WordRAM.Fits w (Nat.log 2 n)) : ∃ (y : WordRAM.Data 22), WordRAM.ExecWithin w logLoop x y (4 * Nat.log 2 n + 2) ∧ y.mem = x.mem ∧ y.regs AmpReg.one = 1 ∧ y.regs AmpReg.nOrig = n ∧ y.regs AmpReg.idx = Nat.log 2 n

theorem Cslib.Algorithms.WordRAM.Karger.highProbSetup_exec {w n : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hw : WordRAM.logWidth 3 n ≤ w) : ∃ (y : WordRAM.Data 22), WordRAM.ExecWithin w highProbSetup (WordRAM.Data.init (n :: flattenMatrix W)) y (4 * Nat.log 2 n + 13) ∧ y.mem = (WordRAM.Data.init (n :: flattenMatrix W)).mem ∧ y.regs AmpReg.srcBase = 2 ∧ y.regs AmpReg.nOrig = n ∧ y.regs AmpReg.numTrials = highProbTrials n

theorem Cslib.Algorithms.WordRAM.Karger.highProbCode_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (totalDoubledWeight W)) : ∃ (m : ProbComp (WordRAM.Data 22 × ℕ)), WordRAM.ExecRand w highProbCode (WordRAM.Data.init (n :: flattenMatrix W)) m ∧ OracleComp.IsQueryBounded m (highProbTrials n * (n - 2)) ∧ (∀ z ∈ OracleComp.support m, z.2 + 1 ≤ highProbTime n ∧ WordRAM.Modifies (Finset.Ico (2 + n * n) (2 + 2 * (n * n) + n)) (WordRAM.Data.init (n :: flattenMatrix W)).mem z.1.mem ∧ ∃ (C : Finset (Fin n)), IsNonTrivialCut C ∧ z.1.regs AmpReg.bestVal = cutWeight W C) ∧ (0 < minCut W → m.eval.toOuterMeasure {z : WordRAM.Data 22 × ℕ | z.1.regs AmpReg.bestVal ≠ minCut W} ≤ 1 / ↑(2 * n))

Structured ProbComp specification of highProbCode.

theorem Cslib.Algorithms.WordRAM.Karger.highProbProgram_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (totalDoubledWeight W)) : have input := n :: flattenMatrix W; WordRAM.RandHaltsWithin w highProbProgram (WordRAM.State.init input) (highProbTime n) ∧ WordRAM.RandCallsBounded w highProbProgram (WordRAM.State.init input) (highProbTime n) (highProbTrials n * (n - 2)) ∧ (∀ cfg ∈ OracleComp.support (WordRAM.runRand w highProbProgram (highProbTime n) (WordRAM.RandCfg.running (WordRAM.State.init input))), ∃ (y : WordRAM.Data 22) (C : Finset (Fin n)), cfg = WordRAM.RandCfg.halted (cutWeight W C) y ∧ WordRAM.Data.Bounded w y ∧ IsNonTrivialCut C ∧ minCut W ≤ cutWeight W C ∧ WordRAM.Modifies (Finset.Ico (2 + n * n) (2 + 2 * (n * n) + n)) (WordRAM.Data.init input).mem y.mem) ∧ (0 < minCut W → (WordRAM.evalRand w highProbProgram (highProbTime n) (WordRAM.State.init input)).toOuterMeasure {cfg : WordRAM.RandCfg 22 | ∀ (y : WordRAM.Data 22), cfg ≠ WordRAM.RandCfg.halted (minCut W) y} ≤ 1 / ↑(2 * n))

Explicit O(n ^ 4 log n) high-probability global minimum cut (highProbProgram). At word size w ≥ logWidth 3 n when 2 ≤ n and totalDoubledWeight W < 2 ^ w:

1. highProbProgram halts within highProbTime n = 33 * n ^ 4 * (Nat.log 2 n + 2) steps;
2. executes at most highProbTrials n * (n - 2) rand calls;
3. on every supported branch, outputs cutWeight W C ≥ minCut W for a genuine non-trivial cut C of W while modifying memory only in [2 + n * n, 2 + 2 * (n * n) + n);
4. when 0 < minCut W (excluded only for proof convenience; S = 0 contraction still halts fault-free with a valid cut weight), misses minCut W with probability at most 1 / (2 * n).

theorem Cslib.Algorithms.WordRAM.Karger.highProbProgram_failure_le_inv_n {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hpos : 0 < minCut W) : (WordRAM.evalRand w highProbProgram (highProbTime n) (WordRAM.State.init (n :: flattenMatrix W))).toOuterMeasure {cfg : WordRAM.RandCfg 22 | ∀ (y : WordRAM.Data 22), cfg ≠ WordRAM.RandCfg.halted (minCut W) y} ≤ 1 / ↑n

Corollary of highProbProgram_spec: when 0 < minCut W, highProbProgram misses minCut W with probability at most 1 / n.