Compiled minimum-cut programs from an output law

The basic Karger and recursive Karger–Stein programs share the same final step: compile a structured code whose observed word has a law supported on non-trivial cut weights. This module transports that law to halted configurations, retaining supported-path halt and random-call bounds, bounded data and the exact memory frame. Their amplification loops also share the update of the best cut weight after each trial.

Main results

• Cslib.Algorithms.WordRAM.Karger.program_of_law: compiled halt, call, cut and probability contracts from the existing ExecRandLaw.
• Cslib.Algorithms.WordRAM.Karger.program_failure_le_inv_n: unconditional 1 / n failure probability bound for compiled amplified minimum-cut programs.
• Cslib.Algorithms.WordRAM.Karger.minUpdate_exec: the running-minimum update on any registers, with its register frame.

References

Extracted unchanged from the Karger word-RAM endpoint proof; the algorithm-specific mathematics belongs to its specification law.

theorem Cslib.Algorithms.WordRAM.Karger.program_of_law {r R T T' n w : ℕ} {c : WordRAM.Code WordRAM.Basis.standard r} {out : Fin r} {input : List ℕ} {F : Finset ℕ} {W : Fin n → Fin n → ℕ} {μ : PMF ℕ} (h : WordRAM.ExecRandLaw w c (WordRAM.Data.init input) (fun (y : WordRAM.Data r) => WordRAM.Modifies F (WordRAM.Data.init input).mem y.mem) T R (fun (y : WordRAM.Data r) => y.regs out) μ) (hT : T + 1 ≤ T') (hfit : WordRAM.InputFits w input) (hμ : ∀ v ∈ μ.support, ∃ (C : Finset (Fin n)), WeightedCut.IsNonTrivialCut C ∧ v = WeightedCut.cutWeight W C) : WordRAM.RandHaltsWithin w (c.program out) (WordRAM.State.init input) T' ∧ WordRAM.RandCallsBounded w (c.program out) (WordRAM.State.init input) T' R ∧ (∀ cfg ∈ OracleComp.support (WordRAM.runRand w (c.program out) T' (WordRAM.RandCfg.running (WordRAM.State.init input))), ∃ (y : WordRAM.Data r) (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 F (WordRAM.Data.init input).mem y.mem) ∧ μ.toOuterMeasure {v : ℕ | v = WeightedCut.minCut W} ≤ (WordRAM.evalRand w (c.program out) T' (WordRAM.State.init input)).toOuterMeasure {cfg : WordRAM.RandCfg r | ∃ (y : WordRAM.Data r), cfg = WordRAM.RandCfg.halted (WeightedCut.minCut W) y} ∧ (WordRAM.evalRand w (c.program out) T' (WordRAM.State.init input)).toOuterMeasure {cfg : WordRAM.RandCfg r | ∀ (y : WordRAM.Data r), cfg ≠ WordRAM.RandCfg.halted (WeightedCut.minCut W) y} ≤ μ.toOuterMeasure {v : ℕ | v ≠ WeightedCut.minCut W}

A compiled program whose output word has the law μ, supported on the weights of non-trivial cuts of W, halts on every path with such a weight, and outputs minCut W with at least the probability that μ gives it; it fails to do so with at most the probability that μ gives the other values.

theorem Cslib.Algorithms.WordRAM.Karger.program_failure_le_inv_n {r T' n w : ℕ} {c : WordRAM.Code WordRAM.Basis.standard r} {out : Fin r} {input : List ℕ} {W : Fin n → Fin n → ℕ} (hlaw : 2 ≤ n → ∃ (R : ℕ) (T : ℕ) (P : WordRAM.Data r → Prop) (μ : PMF ℕ), WordRAM.ExecRandLaw w c (WordRAM.Data.init input) P T R (fun (y : WordRAM.Data r) => y.regs out) μ ∧ T + 1 ≤ T' ∧ (0 < WeightedCut.minCut W → μ.toOuterMeasure {v : ℕ | v ≠ WeightedCut.minCut W} ≤ 1 / ↑(2 * n)) ∧ (WeightedCut.minCut W = 0 → ∀ v ∈ μ.support, v = 0)) : (WordRAM.evalRand w (c.program out) T' (WordRAM.State.init input)).toOuterMeasure {cfg : WordRAM.RandCfg r | ∀ (y : WordRAM.Data r), cfg ≠ WordRAM.RandCfg.halted (WeightedCut.minCut W) y} ≤ 1 / ↑n

Unconditional 1 / n failure-probability bound for a compiled minimum-cut program c.program out: for n < 2 the right-hand side 1 / n is at least 1; for 2 ≤ n, the program's miss probability is bounded by μ.toOuterMeasure {v | v ≠ minCut W}, which is 0 when minCut W = 0 and μ is supported on {0}, and at most 1 / (2 * n) ≤ 1 / n when 0 < minCut W.

theorem Cslib.Algorithms.WordRAM.Karger.minUpdate_exec {r w : ℕ} {trial zero val best : Fin r} (hbz : best ≠ zero) {x : WordRAM.Data r} (hz : x.regs zero = 0) : ∃ (y : WordRAM.Data r), WordRAM.ExecWithin w (WordRAM.Code.branch (WordRAM.Cond.eq trial zero) (WordRAM.Code.op (WordRAM.Op.copy best val)) (WordRAM.Code.branch (WordRAM.Cond.lt val best) (WordRAM.Code.op (WordRAM.Op.copy best val)) (WordRAM.Code.op (WordRAM.Op.const zero 0)))) x y 5 ∧ y.mem = x.mem ∧ (y.regs best = if x.regs trial = 0 then x.regs val else min (x.regs val) (x.regs best)) ∧ ∀ (i : Fin r), i ≠ best → y.regs i = x.regs i

The running-minimum update shared by the amplification loops, on any registers: on the first trial (trial equal to the zero register) it records val in best, and afterwards the smaller of val and best. It runs within five instructions and changes no other register or memory.