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) whenever 0 < minCut W (and unconditionally at most 1 / n in highProbProgram_failure_le_inv_n), via an elementary Bernoulli power bound without Real.exp.

No probability is proved on machine states. Each program simulates a client of Cslib.Algorithms.Lean.Karger: the word it outputs has the law of the answer of Cslib.Algorithms.Lean.Karger.karger (singleCode_law), or of the amplification client Cslib.Algorithms.Lean.Karger.minRuns run against independent runs of karger (amplifiedCode_law, highProbCode_law). Each trial contracts as the client does (contractDownTo_law) and reads half the total weight of the two supervertices left (ContractState.mem_add_one), and the loop of trials keeps the least answer as minRuns does (ampTrialBody_law, ampLoop_law). The success and failure bounds and the cut realization are the specification's (Cslib.Algorithms.Lean.Karger.two_div_le_toOuterMeasure_karger, Cslib.Algorithms.Lean.Karger.minRuns_ne_minCut_le, Cslib.Algorithms.Lean.Karger.exists_cut_of_mem_support_answerLaw, Cslib.Algorithms.Lean.Karger.mem_support_minRuns), carried through those laws.

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 spec probability clauses (singleProgram_spec, amplifiedProgram_spec, highProbProgram_spec) is retained there for the per-trial survival ratio, whereas highProbProgram_failure_le_inv_n holds unconditionally without 2 ≤ n or 0 < minCut W (when minCut W = 0 and 2 ≤ n, contraction preserves zero minimum cut so every run outputs 0).

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.singleCode_law, Cslib.Algorithms.WordRAM.Karger.amplifiedCode_law, Cslib.Algorithms.WordRAM.Karger.highProbCode_law: each program's output has the law of the output of karger or of amplified karger, within its instruction and rand-call bounds.
• Cslib.Algorithms.WordRAM.Karger.ampTrialBody_law, Cslib.Algorithms.WordRAM.Karger.ampLoop_law, Cslib.Algorithms.WordRAM.Karger.ampCore_law: one trial, the loop of trials and the amplification core.
• 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) (unconditional 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 (Karger.highProbTrials n)

Under 2 ≤ n and logWidth 3 n ≤ w, highProbTrials n fits 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 (WeightedCut.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 (WeightedCut.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_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_law {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : WeightedCut.IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (WeightedCut.totalDoubledWeight W)) : WordRAM.ExecRandLaw w singleCode (WordRAM.Data.init (n :: flattenMatrix W)) (fun (y : WordRAM.Data 16) => WordRAM.Modifies (Finset.Ico 2 (2 + n * n + n)) (WordRAM.Data.init (n :: flattenMatrix W)).mem y.mem) (42 * n ^ 2 + 12 * n + 20) (n - 2) (fun (y : WordRAM.Data 16) => y.regs Reg.val1) (Lean.Karger.answerLaw { size := n, weight := W })

A single trial runs karger. At word size w ≥ logWidth 3 n with totalDoubledWeight W < 2 ^ w, singleCode on n :: flattenMatrix W runs within singleTime n - 1 instructions and n - 2 rand calls and writes only [2, 2 + n * n + n). The weight it leaves in val1 has the law of the answer of Lean.Karger.karger on ⟨n, W⟩: contractDownTo contracts as the client does (contractDownTo_law), and singlePost reads the weight between the last two supervertices, half their total weight.

theorem Cslib.Algorithms.WordRAM.Karger.singleProgram_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : WeightedCut.IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (WeightedCut.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 (WeightedCut.cutWeight W C) y ∧ WordRAM.Data.Bounded w y ∧ WeightedCut.IsNonTrivialCut C ∧ WeightedCut.minCut W ≤ WeightedCut.cutWeight W C ∧ WordRAM.Modifies (Finset.Ico 2 (2 + n * n + n)) (WordRAM.Data.init input).mem y.mem) ∧ (0 < WeightedCut.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 (WeightedCut.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

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_law {w sb n R i : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} {x : WordRAM.Data 22} (hn : 2 ≤ n) (hW : WeightedCut.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 (WeightedCut.totalDoubledWeight W)) (hinv : AmpInv w sb n R i W mem₀ x) : WordRAM.ExecRandLaw w ampTrialBody x (AmpInv w sb n R (i + 1) W mem₀) (49 * n ^ 2 + 12 * n + 27) (n - 2) (fun (y : WordRAM.Data 22) => y.regs AmpReg.bestVal) (PMF.map (fun (v : ℕ) => if i = 0 then v else min v (x.regs AmpReg.bestVal)) (Lean.Karger.answerLaw { size := n, weight := W }))

One trial runs karger. From AmpInv at trial i < R, ampTrialBody runs within 49 n² + 12 n + 27 instructions and n - 2 rand calls and keeps the invariant at trial i + 1. Its new bestVal has the law of the answer v of Lean.Karger.karger on ⟨n, W⟩, taken as is on the first trial and as min v bestVal after: contractDownToAt contracts the fresh copy of W as the client does (contractDownToAt_law), and ampTrialPost reads the weight between the last two supervertices, half their total weight.

theorem Cslib.Algorithms.WordRAM.Karger.ampLoop_law {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : WeightedCut.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 (WeightedCut.totalDoubledWeight W)) (rem i : ℕ) (x : WordRAM.Data 22) : i + rem = R → AmpInv w sb n R i W mem₀ x → WordRAM.ExecRandLaw w ampLoop x (AmpInv w sb n R R W mem₀) (rem * (50 * n ^ 2 + 12 * n + 30) + 2) (rem * (n - 2)) (fun (y : WordRAM.Data 22) => y.regs AmpReg.bestVal) (OracleComp.evalWith (fun (x : Unit) => Lean.Karger.answerLaw { size := n, weight := W }) (if i = 0 then Lean.Karger.minRuns rem else OracleComp.iterate rem Lean.Karger.minStep (x.regs AmpReg.bestVal)))

The loop of trials runs amplified Karger. From AmpInv at trial i, with rem = R - i trials left, ampLoop runs within rem (50 n² + 12 n + 30) + 2 instructions and rem (n - 2) rand calls and ends at trial R. Its bestVal has the law of the amplification client run against independent runs of Lean.Karger.karger on ⟨n, W⟩: of Lean.Karger.minRuns rem on the first trial, and of rem more Lean.Karger.minSteps from bestVal after.

theorem Cslib.Algorithms.WordRAM.Karger.ampCore_law {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {x : WordRAM.Data 22} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : WeightedCut.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 (WeightedCut.totalDoubledWeight W)) (hsrc_mat : HoldsMatrix x.mem sb n W) : WordRAM.ExecRandLaw w ampCore x (fun (y : WordRAM.Data 22) => WordRAM.Modifies (Finset.Ico (sb + n * n) (sb + 2 * (n * n) + n)) x.mem y.mem) (R * (50 * n ^ 2 + 12 * n + 30) + 8) (R * (n - 2)) (fun (y : WordRAM.Data 22) => y.regs AmpReg.bestVal) (OracleComp.evalWith (fun (x : Unit) => Lean.Karger.answerLaw { size := n, weight := W }) (Lean.Karger.minRuns R))

The amplification core runs amplified Karger. For 1 ≤ R trials, from a state with srcBase = sb, nOrig = n, numTrials = R and HoldsMatrix x.mem sb n W, ampCore runs within R (50 n² + 12 n + 30) + 8 instructions and R (n - 2) rand calls and writes only the workspace. Its bestVal has the law of Lean.Karger.minRuns R against independent runs of Lean.Karger.karger on ⟨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_law {R n w : ℕ} {W : Fin n → Fin n → ℕ} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : WeightedCut.IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (hR_fit : WordRAM.Fits w R) (htot : WordRAM.Fits w (WeightedCut.totalDoubledWeight W)) : WordRAM.ExecRandLaw w amplifiedCode (WordRAM.Data.init (R :: n :: flattenMatrix W)) (fun (y : WordRAM.Data 22) => WordRAM.Modifies (Finset.Ico (3 + n * n) (3 + 2 * (n * n) + n)) (WordRAM.Data.init (R :: n :: flattenMatrix W)).mem y.mem) (R * (50 * n ^ 2 + 12 * n + 30) + 15) (R * (n - 2)) (fun (y : WordRAM.Data 22) => y.regs AmpReg.bestVal) (OracleComp.evalWith (fun (x : Unit) => Lean.Karger.answerLaw { size := n, weight := W }) (Lean.Karger.minRuns R))

amplifiedCode runs amplified Karger. At word size w ≥ logWidth 3 n with 1 ≤ R, R < 2 ^ w and totalDoubledWeight W < 2 ^ w, amplifiedCode on R :: n :: flattenMatrix W runs within amplifiedTime R n - 1 instructions and R (n - 2) rand calls and writes only [3 + n * n, 3 + 2 * (n * n) + n). Its bestVal has the law of Lean.Karger.minRuns R against independent runs of Lean.Karger.karger on ⟨n, W⟩.

theorem Cslib.Algorithms.WordRAM.Karger.amplifiedProgram_spec {R n w : ℕ} {W : Fin n → Fin n → ℕ} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : WeightedCut.IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (hR_fit : WordRAM.Fits w R) (htot : WordRAM.Fits w (WeightedCut.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 (WeightedCut.cutWeight W C) y ∧ WordRAM.Data.Bounded w y ∧ WeightedCut.IsNonTrivialCut C ∧ WeightedCut.minCut W ≤ WeightedCut.cutWeight W C ∧ WordRAM.Modifies (Finset.Ico (3 + n * n) (3 + 2 * (n * n) + n)) (WordRAM.Data.init input).mem y.mem) ∧ (0 < WeightedCut.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 (WeightedCut.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 = Karger.highProbTrials n

theorem Cslib.Algorithms.WordRAM.Karger.highProbTime_bound {n : ℕ} (hn : 2 ≤ n) : 4 * Nat.log 2 n + Karger.highProbTrials n * (50 * n ^ 2 + 12 * n + 30) + 22 ≤ highProbTime n

The setup's 4 log₂ n + 13 instructions, the highProbTrials n trials' highProbTrials n (50 n² + 12 n + 30) + 8 and the final halt fit in highProbTime n.

theorem Cslib.Algorithms.WordRAM.Karger.highProbCode_law {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : WeightedCut.IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (WeightedCut.totalDoubledWeight W)) : WordRAM.ExecRandLaw w highProbCode (WordRAM.Data.init (n :: flattenMatrix W)) (fun (y : WordRAM.Data 22) => WordRAM.Modifies (Finset.Ico (2 + n * n) (2 + 2 * (n * n) + n)) (WordRAM.Data.init (n :: flattenMatrix W)).mem y.mem) (4 * Nat.log 2 n + Karger.highProbTrials n * (50 * n ^ 2 + 12 * n + 30) + 21) (Karger.highProbTrials n * (n - 2)) (fun (y : WordRAM.Data 22) => y.regs AmpReg.bestVal) (OracleComp.evalWith (fun (x : Unit) => Lean.Karger.answerLaw { size := n, weight := W }) (Lean.Karger.minRuns (Karger.highProbTrials n)))

highProbCode runs amplified Karger. At word size w ≥ logWidth 3 n with totalDoubledWeight W < 2 ^ w, highProbCode on n :: flattenMatrix W runs within 4 log₂ n + highProbTrials n (50 n² + 12 n + 30) + 21 instructions and highProbTrials n (n - 2) rand calls and writes only [2 + n * n, 2 + 2 * (n * n) + n). Its bestVal has the law of Lean.Karger.minRuns (highProbTrials n) against independent runs of Lean.Karger.karger on ⟨n, W⟩.

theorem Cslib.Algorithms.WordRAM.Karger.highProbProgram_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : WeightedCut.IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (WeightedCut.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) (Karger.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 (WeightedCut.cutWeight W C) y ∧ WordRAM.Data.Bounded w y ∧ WeightedCut.IsNonTrivialCut C ∧ WeightedCut.minCut W ≤ WeightedCut.cutWeight W C ∧ WordRAM.Modifies (Finset.Ico (2 + n * n) (2 + 2 * (n * n) + n)) (WordRAM.Data.init input).mem y.mem) ∧ (0 < WeightedCut.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 (WeightedCut.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 → ℕ} (hW : WeightedCut.IsMultigraph W) (hw : WordRAM.logWidth 3 n ≤ w) (htot : WordRAM.Fits w (WeightedCut.totalDoubledWeight 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 (WeightedCut.minCut W) y} ≤ 1 / ↑n

highProbProgram misses minCut W with probability at most 1 / n, unconditionally without 2 ≤ n or 0 < minCut W: for n < 2 the bound 1 / n is at least 1, and for 2 ≤ n with minCut W = 0 every contraction trial outputs 0.