refactor(Algorithms/WordRAM/Karger): derive Karger–Stein bounds from client laws

Complexity.lean

@@ -22,6 +22,7 @@ public import Complexity.Algorithms.Lean.Huffman.TwoQueue
 public import Complexity.Algorithms.Lean.KMP.Basic
 public import Complexity.Algorithms.Lean.KMP.Search
 public import Complexity.Algorithms.Lean.Karger.Contraction
+public import Complexity.Algorithms.Lean.Karger.FastCut
 public import Complexity.Algorithms.Lean.Kruskal.Basic
 public import Complexity.Algorithms.Lean.Kruskal.SimpleGraph
 public import Complexity.Algorithms.Lean.Matroid.Greedy
@@ -262,6 +263,7 @@ public import Complexity.Algorithms.WordRAM.Histogram
 public import Complexity.Algorithms.WordRAM.Karger.Contract
 public import Complexity.Algorithms.WordRAM.Karger.FastCut
 public import Complexity.Algorithms.WordRAM.Karger.Graph
+public import Complexity.Algorithms.WordRAM.Karger.OutputLaw
 public import Complexity.Algorithms.WordRAM.KargerMinCut
 public import Complexity.Algorithms.WordRAM.KargerStein
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.CyclicConvolution.Coefficient
@@ -2636,6 +2638,7 @@ public import Complexity.Computability.WordRAM.Randomized.Defs
 public import Complexity.Computability.WordRAM.Randomized.Expected
 public import Complexity.Computability.WordRAM.Randomized.Law
 public import Complexity.Computability.WordRAM.Randomized.LoopSegment
+public import Complexity.Computability.WordRAM.Randomized.LoopSegmentLaw
 public import Complexity.Computability.WordRAM.Randomized.Structured
 public import Complexity.Computability.WordRAM.Randomized.UniformLoopExit
 public import Complexity.Computability.WordRAM.Realization.Absorb
@@ -3641,7 +3644,6 @@ public import Complexity.Languages.Probabilistic.BitString
 public import Complexity.Languages.Probabilistic.BoundedUniform
 public import Complexity.Languages.Probabilistic.CenteredBinomial
 public import Complexity.Languages.Probabilistic.Concentration
-public import Complexity.Languages.Probabilistic.Event
 public import Complexity.Languages.Probabilistic.Expect
 public import Complexity.Languages.Probabilistic.Forking
 public import Complexity.Languages.Probabilistic.Iteration
@@ -3919,6 +3921,7 @@ public import Complexity.Probability.PMF.Bind
 public import Complexity.Probability.PMF.Event
 public import Complexity.Probability.PMF.Expect
 public import Complexity.Probability.PMF.Map
+public import Complexity.Probability.PMF.TwoBranch
 public import Complexity.Probability.PMF.Uniform
 public import Complexity.Probability.PMF.UniformBound
 public import Complexity.Probability.PMF.UniformSubset

Complexity/Algorithms/WordRAM/Karger/OutputLaw.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2026 Renfei Zhou, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Renfei Zhou, Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.Karger.Graph
+public import Complexity.Computability.WordRAM.Heap
+public import Complexity.Computability.WordRAM.Randomized.Law
+public import Complexity.Computability.WordRAM.Time
+
+/-!
+# 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.
+
+## Main results
+
+* `Cslib.Algorithms.WordRAM.Karger.program_of_law`: compiled halt, call, cut and probability
+  contracts from the existing `ExecRandLaw`.
+
+## References
+
+Extracted unchanged from the Karger word-RAM endpoint proof; the algorithm-specific mathematics
+belongs to its specification law.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.Karger
+
+open Cslib.WeightedCut Cslib.WordRAM
+
+/-- 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 the probability
+that `μ` gives it. -/
+theorem program_of_law {r R T T' n w : ℕ} {c : Code .standard r} {out : Fin r}
+    {input : List ℕ} {F : Finset ℕ} {W : Fin n → Fin n → ℕ} {μ : PMF ℕ}
+    (h : ExecRandLaw w c (.init input) (fun y => Modifies F (Data.init (r := r) input).mem y.mem)
+      T R (fun y => y.regs out) μ) (hT : T + 1 ≤ T') (hfit : InputFits w input)
+    (hμ : ∀ v ∈ μ.support, ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ v = cutWeight W C) :
+    RandHaltsWithin w (c.program out) (.init input) T' ∧
+    RandCallsBounded w (c.program out) (.init input) T' R ∧
+    (∀ cfg ∈ (runRand w (c.program out) T' (.running (.init input))).support,
+      ∃ (y : Data r) (C : Finset (Fin n)),
+        cfg = .halted (cutWeight W C) y ∧ y.Bounded w ∧ IsNonTrivialCut C ∧
+        minCut W ≤ cutWeight W C ∧ Modifies F (Data.init (r := r) input).mem y.mem) ∧
+    μ.toOuterMeasure {v | v = minCut W} ≤
+      (evalRand w (c.program out) T' (.init input)).toOuterMeasure
+        {cfg | ∃ y, cfg = .halted (minCut W) y} ∧
+    (evalRand w (c.program out) T' (.init input)).toOuterMeasure
+        {cfg | ∀ y, cfg ≠ .halted (minCut W) y} ≤ μ.toOuterMeasure {v | v ≠ minCut W} := by
+  let output : RandCfg r → ℕ := fun | .halted v _ => v | _ => 0
+  obtain ⟨hhalt, hcalls, hpost, hlaw⟩ := h.program out hT output fun _ _ => rfl
+  have hhalted : ∀ cfg ∈ (evalRand w (c.program out) T' (.init input)).support,
+      ∃ y : Data r, cfg = .halted (y.regs out) y := fun cfg hcfg => by
+    obtain ⟨y, rfl, -⟩ := hpost cfg (by rwa [support_evalRand] at hcfg)
+    exact ⟨y, rfl⟩
+  refine ⟨hhalt, hcalls, fun cfg hcfg => ?_, ?_, ?_⟩
+  · obtain ⟨y, rfl, hmod⟩ := hpost cfg hcfg
+    obtain ⟨C, hC, hv⟩ := hμ (y.regs out) (by
+      rw [← hlaw, PMF.mem_support_map_iff]
+      exact ⟨_, by rwa [support_evalRand], rfl⟩)
+    exact ⟨y, C, by rw [hv], (runRand_bounded_init hfit hcfg).2, hC, minCut_le_cutWeight W hC,
+      hmod⟩
+  · rw [← hlaw, PMF.toOuterMeasure_map_apply]
+    refine PMF.toOuterMeasure_mono _ ?_
+    rintro cfg ⟨hv, hcfg⟩
+    obtain ⟨y, rfl⟩ := hhalted cfg hcfg
+    change y.regs out = minCut W at hv
+    exact ⟨y, by rw [hv]⟩
+  · rw [← hlaw, PMF.toOuterMeasure_map_apply]
+    refine PMF.toOuterMeasure_mono _ ?_
+    rintro cfg ⟨hne, hcfg⟩ hv
+    obtain ⟨y, rfl⟩ := hhalted cfg hcfg
+    change y.regs out = minCut W at hv
+    exact hne y (by rw [hv])
+
+end Cslib.Algorithms.WordRAM.Karger

Complexity/Algorithms/WordRAM/KargerMinCut.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Complexity.Algorithms.WordRAM.Karger.Graph
 public import Complexity.Algorithms.WordRAM.Karger.Contract
+public import Complexity.Algorithms.WordRAM.Karger.OutputLaw
 public import Complexity.Computability.WordRAM.Copy
 public import Complexity.Computability.WordRAM.Time
 
@@ -222,53 +223,6 @@ theorem holdsMatrix_init_amplified {r R n : ℕ} (W : Fin n → Fin n → ℕ) :
     HoldsMatrix (Data.init (r := r) (R :: n :: flattenMatrix W)).mem 3 n W :=
   holdsMatrix_init_append [R, n] W
 
-/-! ### Compiled programs from the law of their output -/
-
-/-- 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 the probability
-that `μ` gives it. -/
-private theorem program_of_law {r R T T' n w : ℕ} {c : Code .standard r} {out : Fin r}
-    {input : List ℕ} {F : Finset ℕ} {W : Fin n → Fin n → ℕ} {μ : PMF ℕ}
-    (h : ExecRandLaw w c (.init input) (fun y => Modifies F (Data.init (r := r) input).mem y.mem)
-      T R (fun y => y.regs out) μ) (hT : T + 1 ≤ T') (hfit : InputFits w input)
-    (hμ : ∀ v ∈ μ.support, ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ v = cutWeight W C) :
-    RandHaltsWithin w (c.program out) (.init input) T' ∧
-    RandCallsBounded w (c.program out) (.init input) T' R ∧
-    (∀ cfg ∈ (runRand w (c.program out) T' (.running (.init input))).support,
-      ∃ (y : Data r) (C : Finset (Fin n)),
-        cfg = .halted (cutWeight W C) y ∧ y.Bounded w ∧ IsNonTrivialCut C ∧
-        minCut W ≤ cutWeight W C ∧ Modifies F (Data.init (r := r) input).mem y.mem) ∧
-    μ.toOuterMeasure {v | v = minCut W} ≤
-      (evalRand w (c.program out) T' (.init input)).toOuterMeasure
-        {cfg | ∃ y, cfg = .halted (minCut W) y} ∧
-    (evalRand w (c.program out) T' (.init input)).toOuterMeasure
-        {cfg | ∀ y, cfg ≠ .halted (minCut W) y} ≤ μ.toOuterMeasure {v | v ≠ minCut W} := by
-  let output : RandCfg r → ℕ := fun | .halted v _ => v | _ => 0
-  obtain ⟨hhalt, hcalls, hpost, hlaw⟩ := h.program out hT output fun _ _ => rfl
-  have hhalted : ∀ cfg ∈ (evalRand w (c.program out) T' (.init input)).support,
-      ∃ y : Data r, cfg = .halted (y.regs out) y := fun cfg hcfg => by
-    obtain ⟨y, rfl, -⟩ := hpost cfg (by rwa [support_evalRand] at hcfg)
-    exact ⟨y, rfl⟩
-  refine ⟨hhalt, hcalls, fun cfg hcfg => ?_, ?_, ?_⟩
-  · obtain ⟨y, rfl, hmod⟩ := hpost cfg hcfg
-    obtain ⟨C, hC, hv⟩ := hμ (y.regs out) (by
-      rw [← hlaw, PMF.mem_support_map_iff]
-      exact ⟨_, by rwa [support_evalRand], rfl⟩)
-    exact ⟨y, C, by rw [hv], (runRand_bounded_init hfit hcfg).2, hC, minCut_le_cutWeight W hC,
-      hmod⟩
-  · rw [← hlaw, PMF.toOuterMeasure_map_apply]
-    refine PMF.toOuterMeasure_mono _ ?_
-    rintro cfg ⟨hv, hcfg⟩
-    obtain ⟨y, rfl⟩ := hhalted cfg hcfg
-    change y.regs out = minCut W at hv
-    exact ⟨y, by rw [hv]⟩
-  · rw [← hlaw, PMF.toOuterMeasure_map_apply]
-    refine PMF.toOuterMeasure_mono _ ?_
-    rintro cfg ⟨hne, hcfg⟩ hv
-    obtain ⟨y, rfl⟩ := hhalted cfg hcfg
-    change y.regs out = minCut W at hv
-    exact hne y (by rw [hv])
-
 /-! ### Endpoint 1: Single-trial Basic Karger (`r = 16`) -/
 
 section SingleTrial