Repository navigation
feat(WordRAM): Karger–Stein recursive global minimum cut (FastCut) on the randomized word RAM - #1366
Conversation
There was a problem hiding this comment.
Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.
An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.
|
|
|
Fixed in f4d7fd2 (terminal |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1366 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at f4d7fd29f327018df646f7ee0af4674508ea11e6
Thanks for this, Renfei. Recursive contraction with an explicit frame stack inside one while loop is a nice construction, and the proof is cleanly organised around LoopSegment. The PR stacks on #1345, so this review covers only the Milestone 2 commits 202c5b6d, c5a8c657 and f4d7fd29 (git diff 005c99ed4 f4d7fd29; the upstream/main merges after 7945af94 touch no Karger files). Milestone 1 is reviewed in #1345.
What is proved. fastCutProgram_spec and the abstract's kargerSteinFastCut give one fixed 24-register Basis.standard program (lifted to the exact basis in the bridge) for inputs with 2 ≤ n, 4 * (Nat.log 2 n + 1) ≤ w, totalDoubledWeight W < 2 ^ w and a symmetric zero-diagonal W. It halts within 2500 n² (⌊log₂ n⌋ + 2) steps and makes at most fastCutNodeQueries n ≤ 6n² unit-cost rand calls. On every path it outputs cutWeight W C for a non-trivial C, and it changes memory only in [2 + n², 2 + 27n²). When 0 < minCut W, it outputs minCut W with probability at least 1/(⌊log₂ n⌋ + 15). fastCutHighProbProgram_spec and kargerSteinHighProb run (⌊log₂ n⌋ + 15)(⌊log₂ n⌋ + 2) independent trees in 2600 n² (L + 15)(L + 2)² steps and miss minCut W with probability at most 1/(2n).
The probability argument fixes one minimum cut B and pulls it back through the contraction. It uses three facts: survival to t = fastCutThreshold k has probability at least 1/2, a leaf 2 ≤ k ≤ 6 succeeds with probability at least 2/30, and two_branch_hit_prob_ge turns child success 2/s into node success 2/(s+1). Together these give 2/(depth + 30), and fastCutDepth n ≤ 2 log₂ n is proved through the integer potential (k - 4)². The arithmetic avoids Real.log throughout.
Checked instance. At n = 8, the threshold is t = 6: 8·7 = 56 ≤ 2·6·5 = 60 but 56 > 2·5·4 = 40. So the depth is 1 and fastCutNodeQueries 8 = 2·(8−6) + 2·(6−2) = 12, which matches fastCutProgram_barbell8. Since 8 ≥ 7, the barbell test exercises the recursive branch, and its probability bound 1/18 = 1/(3 + 15) is the instantiated headline. The disconnected and zero-weight tests cover minCut W = 0 and S = 0. In the abstract, kargerSteinFastCut and kargerSteinHighProb match the library statements: the same constants, the same 6 * (n * n) and R * (6 * (n * n)) call budgets, and the same frame. #check_abstract stays under #guard_msgs. The abstract remains uncatalogued per #1142.
ci-checks is green on this head, and the earlier hygiene failure is fixed.
Blocking
-
Source locators and mapping for Milestone 2 (AGENTS.md, "New statements and definitions"). The Milestone 2 modules, the abstract and the PR description cite
[KargerStein1996]without a locator. #1345 already received this request for Milestone 1. Please give the exact locators (quoted, or labelled as paraphrase) for: the recursive algorithm (threshold⌈1 + n/√2⌉, two independent branches, base case); theO(n² log n)time bound; theΩ(1/log n)success bound; and theO(n² log³ n)high-probability corollary. Then map each to the Lean statements. Please label these deviations from the source as your own choices:- The integer threshold can be smaller than the source's: at
k = 8it is 6, not 7. - The leaf runs a random contraction to 2 vertices instead of (as I understand the source) exact brute force at
n ≤ 6. This is where the+ 15comes from. - The constants
2500,2600and15, the trial count(L + 15)(L + 2)and the1/(2n)target are yours. - The
(k - 4)²potential argument is original.
I could not check any locator against the pinned paper, because none is given.
- The integer threshold can be smaller than the source's: at
-
Restack onto #1345's current head (
958a487a). The branch still carries #1345 at7945af94, the revision that received CHANGES REQUESTED. Merged as it is, it would land the superseded Milestone 1 code. A trial merge of958a487awith this head conflicts inKargerMinCutAbstract.lean. Also,958a487amakestwo_mul_pred_pow_le_powprivate inGraph.lean, andFastCut.leanstill calls it (inline comment). After the restack, please carry #1345's resolutions over to the Milestone 2 code where they apply (hr24, the0 < minCut Wdocstring note).
Non-blocking
The inline comments raise one more substantive point. Cslib.WordRAM.LoopSegment and execRand_seq_det are general structured word-RAM tools. They currently sit in an Algorithms/WordRAM/Karger file under the namespace Cslib.WordRAM, so the namespace does not match the path. A small module next to Computability/WordRAM/Randomized/Structured.lean would fit them better. Please also add a line to the description saying which existing notions you considered before adding the new public definition LoopSegment. A recorded follow-up is fine if you'd rather not move them in this PR. The other inline comments are nits. Please also link the hosted CI run for the final head in the description.
Limits of this review. I read every public statement in FastCut.lean and the endpoint statements in KargerStein.lean, the abstract and the bridge, and both test files. I sampled the threshold, depth, time and query recurrences, the ℝ≥0∞ probability lemmas, the LoopSegment calculus and the inductive skeleton of fastCutNode_spec. I did not read the roughly 2,500 lines of frame-machine invariant proofs in KargerStein.lean or the bridge's toExact lifting in detail, and I did not build locally.
| else | ||
| t | ||
|
|
||
| /-- Pure-integer Karger–Stein contraction threshold: for `k ≥ 7`, the smallest `t ≥ 2` such that |
There was a problem hiding this comment.
Source mapping (blocking item 1): the source contracts to ⌈1 + k/√2⌉, and this threshold is the least t with C(t,2) ≥ C(k,2)/2. That is never larger than ⌈1 + k/√2⌉ and is sometimes smaller (at k = 8 it is 6, against 7). The survival bound only needs ≥ 1/2, so this is a sound variant. Please label it as a deviation, with the locator of the source's threshold, instead of calling it a pure-integer "replacement".
|
|
||
| 1. **Single-tree recursive contraction (`fastCutProgram`, `r = 24`):** contracts recursively from | ||
| `k ≥ 7` down to the pure-integer threshold `t = fastCutThreshold k` (smallest `t ≥ 2` with | ||
| `k * (k - 1) ≤ 2 * t * (t - 1)`) along two independent branches, switches at `k ≤ 6` to a |
There was a problem hiding this comment.
Source mapping (blocking item 1): as I understand [KargerStein1996], the base case n ≤ 6 computes a minimum cut exactly (brute force). Here a leaf runs one more random contraction down to 2 vertices, which succeeds with probability only ≥ 2/30, and that is where the + 15 in 1/(Nat.log 2 n + 15) comes from. That is a reasonable choice, since it keeps the leaf O(1) without a cut-enumeration routine, but please say so here and in the abstract, with the source locator of the base case it replaces.
|
|
||
| /-- Number of independent `FastCut` trees `(Nat.log 2 n + 15) * (Nat.log 2 n + 2)` (`O(log ^ 2 n)`) | ||
| used by `fastCutHighProbProgram` to achieve failure probability `≤ 1 / (2 * n)`. -/ | ||
| def fastCutTrials (n : ℕ) : ℕ := |
There was a problem hiding this comment.
Please label fastCutTrials and the 1/(2n) target as your own parameter choice, as #1345 now does for highProbTrials. The source states the high-probability bound only asymptotically (O(log² n) repetitions).
| rw [ENNReal.div_le_iff_le_mul (Or.inl hM_pow0) (Or.inl hM_powt)] | ||
| rw [← ENNReal.mul_div_right_comm] | ||
| rw [ENNReal.le_div_iff_mul_le (Or.inl h20) (Or.inl h2t), one_mul, mul_comm] | ||
| exact_mod_cast two_mul_pred_pow_le_pow hM1 |
There was a problem hiding this comment.
Restack blocker (item 2): #1345's head 958a487a makes two_mul_pred_pow_le_pow private in Karger/Graph.lean, so this call stops compiling once the branch is restacked. Either keep that lemma public in #1345 (preferably under a descriptive name, or replaced by Mathlib's one_add_mul_le_pow), or inline the bound here.
| Enables structural induction on explicit call-stack depth inside a single outer `while sp > 0` | ||
| loop, where popping a recursive frame lowers `sp` from `b + 1` to `b` without exiting the loop when | ||
| `b > 0`. -/ | ||
| inductive LoopSegment {B : Basis} {r : ℕ} (w : ℕ) (cond : Cond r) (body : Code B r) : |
There was a problem hiding this comment.
Placement: LoopSegment and its API (single, trans, trans_exists, stepDet, finish, regs_eq, bounded), and also execRand_seq_det in KargerStein.lean, are general facts about structured randomized word-RAM loops and do not depend on Karger. They live in namespace Cslib.WordRAM in a file under Algorithms/WordRAM/Karger/, so the namespace does not match the path (file rule 1). A small module such as Complexity/Computability/WordRAM/Randomized/LoopSegment.lean, imported by FastCut.lean, would make them findable for the next iterative or explicit-stack algorithm. two_branch_hit_prob_ge is similarly generic over ProbComp. Non-blocking: please either move them, or record a follow-up in ROADMAP.md next to #1345's extraction item. Please also state in the description which existing notions you considered before adding LoopSegment (for example ExecRand.loop_iter).
| /-! ### Word-size sufficiency (`logWidth 4 n ≤ w`) and input layout -/ | ||
|
|
||
| /-- `16 ≤ 24`, used to embed `computeDegreesAndTotal` and `contractDownTo` into `Data 24`. -/ | ||
| theorem hr24 : 16 ≤ 24 := by decide |
There was a problem hiding this comment.
nit (same as hr22 in #1345): please make this private, or pass (by decide) at the use sites.
| · simp only [hlt, ↓reduceIte] | ||
| exact ⟨le_rfl, ht, Nat.le_of_not_lt hlt, fun _ hge hlt' => absurd hlt' (not_lt_of_ge hge)⟩ | ||
|
|
||
| theorem fastCutThreshold_ge_two {k : ℕ} (hk : 4 ≤ k) : |
There was a problem hiding this comment.
nit: several public lemmas in this file have no docstring (fastCutThreshold_ge_two … fastCutThreshold_min, the _of_lt_seven/_of_ge_seven unfolding lemmas, fastCutNodeTime_le_pot, fastCutTrials_pos, fastCutHighProb_failure_le_inv_n). Please add one-line docstrings, or make private the ones only used internally (fastCutThresholdAux_spec, fastCutThreshold_eq_of_bounds).
|
|
||
| * [D. R. Karger, *Global Min-cuts in RNC, and Other Ramifications of a Simple Min-Cut | ||
| Algorithm*][Karger1993] | ||
| * [D. R. Karger and C. Stein, *A New Approach to the Minimum Cut Problem*][KargerStein1996] |
There was a problem hiding this comment.
Blocking item 1, abstract side: once you have the Milestone 2 locators, please add them here (or in the kargerSteinFastCut / kargerSteinHighProb docstrings), together with the two deviations: the integer threshold and the randomized k ≤ 6 leaf. A reader of the abstract should be able to see that 1/(log n + 15) is a statement about this variant.
|
Addressed the Round 1 review findings in
AI assistance: Gemini agents (under Renfei Zhou's direction) verified the primary sources and implemented and reviewed this revision. |
orbitingflea
left a comment
orbitingflea
left a comment
There was a problem hiding this comment.
coordinator-claude-d0322fdd, with reviewer reviewer-claude-d0322fdd-1366 (agent review under the shared orbitingflea account, not human approval): CHANGES REQUESTED at 125b61cd482d971e408f9169a0854ce7a142a6a7
Thanks, Renfei. The restack is clean: the Milestone 1 files are identical to #1345's head 6b1d72153, LoopSegment and execRand_seq_det moved verbatim to Complexity/Computability/WordRAM/Randomized/LoopSegment.lean, and the Round 1 nits are done. kargerSteinFastCut and kargerSteinHighProb match fastCutProgram_spec and fastCutHighProbProgram_spec, #check_abstract runs with no allowlist, and the tests instantiate both at n = 8, w = 16. Two small items remain. The first comes from a misreading of the source in the earlier review at f4d7fd29, not from your work.
What is proved. One fixed 24-register program handles every input with 2 ≤ n, symmetric zero-diagonal W, 4 * (Nat.log 2 n + 1) ≤ w and totalDoubledWeight W < 2 ^ w. On every path it halts within 2500 n² (⌊log₂ n⌋ + 2) steps and 6n² rand calls, outputs a non-trivial cut weight, and changes memory only in [2 + n², 2 + 27n²). When 0 < minCut W, it outputs minCut W with probability at least 1 / (⌊log₂ n⌋ + 15). The high-probability program runs (L + 15)(L + 2) trees (L = ⌊log₂ n⌋) within 2600 n² (L + 15)(L + 2)² steps and misses minCut W with probability at most 1 / (2n). The probability proof puts the source's recurrence in the closed form 2 / (d + 30) (fastCutNode_spec); the depth bound ≤ 2⌊log₂ n⌋ comes from the (k − 4)² potential. Checked at n = 8: the threshold is 6 (2·5·4 = 40 < 56 ≤ 60 = 2·6·5; Figure 6 gives ⌈8/√2 + 1⌉ = 7), the depth is 1, there are 12 rand calls, and the hit probability is at least 1/18.
Blocking
- The
k ≤ 6leaf is the source's own base case, not a deviation. In the August 1996 author preprint of [KargerStein1996], Figure 6's base case isG′ ← Contract(G, 2), and equation (2) gives the bound1/15forn < 7. The proof of Lemma 4.3 then setsz₀ = 59and showsz_k < 59 + 2kfork ≥ 1, sop_k = 4/(z_k + 1) ≥ 2/(30 + k). At depth≤ 2⌊log₂ n⌋that is exactly your1/(⌊log₂ n⌋ + 15). The remark after that proof mentions a deterministic algorithm on problems of size 7 only as an alternative; the source never describes brute-force enumeration. Please drop the "instead of brute-force cut enumeration" framing, and stop listing the15as an own choice, inFastCut.lean,KargerStein.lean, the abstract and the PR description. The one real boundary choice is that the cutoffk ≤ 6follows equation (2) and that remark, while Figure 6 itself tests "fewer than 6 vertices". Suggested wording is in the inline comments. - Re-proof of a private fact (CONTRIBUTING.md, "Reuse before re-proving").
FastCut.lean:710–736copiesbernoulli_pow_natandtwo_mul_pred_pow_le_powverbatim from the private versions inKarger/Graph.lean:1218–1244. Please maketwo_mul_pred_pow_le_powpublic there (with a docstring, optionally under a more descriptive name) and delete the copies;FastCut.leanalready importsGraph.lean.hdiv_pow(FastCut.lean:745) likewise repeats Graph's privateennreal_div_pow. Optionally, Mathlib'spow_add_mul_le_add_pow(witha := d,b := 1,n := d + 1) can replacebernoulli_pow_nat.
Non-blocking
- Theorem 4.4 finds all minimum cuts in
O(m log(n²/m))space.kargerSteinHighProbproves that the returned value isminCut Wexcept with probability at most1/(2n), within theO(n²)matrix workspace. Nothing overclaims, but the mapping should say "the minimum-cut-value part of Theorem 4.4". TheO(log² n)repetitions are in its proof, not its statement. probComp_seq_hit_ge(KargerStein.lean:1958) re-derives the publictoOuterMeasure_bind_ge_mul_ennrealfromGraph.lean.pmf_toOuterMeasure_map_ks(:162) restatesPMF.toOuterMeasure_map_apply, the same wrapper #1345 removed.- Nits: the private
fastCutThreshold_eq_of_boundsis unused.FastCut.leanimportsLoopSegmentwithout using it (the client isKargerStein.lean). The potential also replaces the depth claim in the proof of Lemma 4.3, so "Lemmas 4.1–4.3". The integer threshold is smaller than⌈k/√2 + 1⌉for mostk, so "e.g.k = 8".
Restack. #1345 now carries a coordinator citation fix (17867647d) in the abstract's Milestone 1 paragraph and in Karger/Graph.lean. Once #1345 lands on main, please restack this branch onto main and keep #1345's final Milestone 1 wording.
Limits of this review. This covers the Milestone 2 delta since f4d7fd29 plus a fresh read of every public statement in FastCut.lean and LoopSegment.lean, the endpoint statements of KargerStein.lean, the abstract, the bridge endpoints and both test files. Every Section 4 locator was checked against the August 1996 author preprint, not the typeset JACM pages. I did not read the frame-machine invariant proofs or the bridge's exact-basis lifting line by line, and did not build locally. The hosted runs on this head are green: Lean Action CI, Formal abstract PDFs.
| 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 `k = 8` (`t = 6` vs `7`). | ||
| 2. **Contraction base case at `k ≤ 6`:** at `2 ≤ k ≤ 6`, each leaf runs one random contraction down |
There was a problem hiding this comment.
Blocking (source mapping). This leaf is the source's base case. In the August 1996 author preprint, Figure 6 reads "if G has fewer than 6 vertices then G′ ← Contract(G, 2)"; equation (2) gives 1/15 for n < 7; and the proof of Lemma 4.3 gives p_k = 4/(z_k + 1) ≥ 2/(30 + k) from z₀ = 59 and z_k < 59 + 2k (k ≥ 1). The remark after that proof mentions a deterministic algorithm only as an alternative, and the source never describes brute-force enumeration (the earlier review's request came from a misreading). Suggested item 2:
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)`.
| with survival probability `≥ 2 / (k * (k - 1)) ≥ 2 / 30 = 1 / 15`) rather than the deterministic | ||
| base case noted in Lemma 4.3's remark, avoiding a separate brute-force cut-enumeration routine | ||
| and producing the `+ 15` denominator offset in `1 / (Nat.log 2 n + 15)`. | ||
| 3. **Concrete Word-RAM constants and trial schedule (`fastCutTrials`):** `[KargerStein1996]`, |
There was a problem hiding this comment.
With item 2 reworded, please drop 1 / (Nat.log 2 n + 15) from the own-choices list, and note that the O(log² n) repetitions are in the proof of Theorem 4.4:
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.
| unfold fastCutTrials | ||
| nlinarith | ||
|
|
||
| private theorem bernoulli_pow_nat (d j : ℕ) : |
There was a problem hiding this comment.
Blocking (CONTRIBUTING.md, "Reuse before re-proving"). This lemma and two_mul_pred_pow_le_pow below are verbatim copies of the private ones in Karger/Graph.lean:1218–1244. Please make two_mul_pred_pow_le_pow public there (with a docstring, optionally a more descriptive name) and delete these copies; this file already imports Graph.lean. hdiv_pow (line 745) likewise repeats Graph's private ennreal_div_pow. Optional: Mathlib's pow_add_mul_le_add_pow (a := d, b := 1, n := d + 1) can replace bernoulli_pow_nat. The same inequality is also private in Complexity/Computability/MCSP/FormulaMagnification.lean (two_mul_pow_le_succ_pow); merging all three can be a follow-up.
| pure-integer threshold `t = fastCutThreshold k` (smallest `t ≥ 2` with `k * (k - 1) ≤ 2 * t * | ||
| (t - 1)`, an integer deviation from Figure 6's `⌈k / √2 + 1⌉` that is never larger and is | ||
| strictly smaller at `k = 8`, where `t = 6` vs `7`) along two independent branches, switches at | ||
| `k ≤ 6` to a single contraction down to `2` supervertices (matching Figure 6 and Lemma 4.3, |
There was a problem hiding this comment.
Blocking (same as FastCut.lean:29). Suggested parenthetical: "(the source's base case: Figure 6's Contract(G, 2) with the size-7 cutoff of equation (2); a leaf keeps a fixed minimum cut with probability ≥ 2 / (k * (k - 1)) ≥ 1 / 15, equation (2)'s base-case bound, which is where the 15 comes from)". In item 2, after "Theorem 4.4; paraphrase)", consider adding "(the value part only: the source finds all minimum cuts in O(m log(n ^ 2 / m)) space; we prove the returned value is minCut W except with probability ≤ 1 / (2 * n))".
| convenience (deterministic `S = 0` contraction still halts without faulting and outputs a valid cut | ||
| weight). | ||
|
|
||
| The recursive `FastCut` theorems (`kargerSteinFastCut` and `kargerSteinHighProb`) formalize |
There was a problem hiding this comment.
Blocking (same as FastCut.lean:29), plus the scope of Theorem 4.4. Suggested paragraph:
The recursive `FastCut` theorems (`kargerSteinFastCut` and `kargerSteinHighProb`) formalize
`[KargerStein1996]`, Section 4 ("The Recursive Contraction Algorithm"): Figure 6
(`Recursive-Contract`), Lemma 4.1 (`O(n ^ 2 log n)` running time), Lemma 4.2 (`O(n ^ 2)` space in
the matrix representation), Lemma 4.3 (`Omega(1 / log n)` single-tree success probability via
equation (2)), and the minimum-cut-value part of Theorem 4.4 (paraphrase). Theorem 4.4 finds all
minimum cuts with high probability in `O(n ^ 2 log ^ 3 n)` time and `O(m log(n ^ 2 / m))` space;
`kargerSteinHighProb` proves that the returned value is `minCut W` except with probability at
most `1 / (2 * n)`, within the `O(n ^ 2)` matrix workspace. As in Figure 6, a leaf
(`2 <= k <= 6`) runs one randomized contraction down to `2` vertices; the cutoff follows
equation (2) and the remark at the end of the proof of Lemma 4.3 (recurse for `n >= 7`), whereas
Figure 6 itself tests "fewer than 6 vertices". The `15` in `1 / (Nat.log 2 n + 15)` is the
source's constant: equation (2)'s base-case probability `1 / 15` gives
`p_k = 4 / (z_k + 1) >= 2 / (30 + k)` (from `z_0 = 59` and `z_k < 59 + 2 k` for `k >= 1` in the
proof of Lemma 4.3), evaluated at recursion depth at most `2 * Nat.log 2 n`. This formalization
makes three design choices of its own: (1) instead of `ceil(1 + k / sqrt 2)` (Figure 6), each
internal node (`k >= 7`) contracts to the least integer `t >= 2` with
`k * (k - 1) <= 2 * t * (t - 1)` (never larger than `ceil(1 + k / sqrt 2)`, and strictly smaller
at e.g. `k = 8`, where `t = 6` versus `7`, while keeping survival probability `>= 1 / 2`); (2) the
step constants `2500` and `2600`, the trial count `R = (Nat.log 2 n + 15) * (Nat.log 2 n + 2)`,
and the `1 / (2 * n)` failure target are our own (the proof of Theorem 4.4 uses `O(log ^ 2 n)`
repetitions); and (3) the integer quadratic potential `(k - 4) ^ 2` bounding recursion depth, leaf
count, and internal work without `Real.sqrt` or `Real.log` is original to this formalization.
| `6 * (n * n)` `rand` calls, preserving the input matrix and all memory outside | ||
| `[2 + n * n, 2 + 27 * (n * n))`. Internal nodes (`k >= 7`) contract to the least `t >= 2` with | ||
| `k * (k - 1) <= 2 * t * (t - 1)` (an integer variant of Figure 6's `ceil(1 + k / sqrt 2)`), and | ||
| leaves (`k <= 6`) run one randomized contraction down to `2` vertices (producing the `+ 15` term). |
There was a problem hiding this comment.
Suggest: "… and leaves (k <= 6) run one randomized contraction down to 2 vertices, as in Figure 6 (equation (2)'s base-case probability 1 / 15 gives the + 15 term)."
| refine ⟨W₁, part₁, B₁, hC₁, fun i j => (hm_sub i j).trans (hws₁.1 i j), | ||
| isNonTrivialCut_of_pullbackCut part₁ (hpb₁ ▸ hC_nt), hpb₁ ▸ hB_min⟩ | ||
|
|
||
| private theorem probComp_seq_hit_ge {r : ℕ} (m₁ : ProbComp (Data r × ℕ)) |
There was a problem hiding this comment.
Non-blocking: after heval, this is toOuterMeasure_bind_ge_mul_ennreal from Graph.lean (used the same way in KargerMinCut.lean), with PMF.toOuterMeasure_map_apply and ProbComp.support_eval for the step hypothesis. pmf_toOuterMeasure_map_ks (line 162) restates PMF.toOuterMeasure_map_apply, the wrapper #1345 removed.
| 2 * m * (m - 1) < k * (k - 1) := | ||
| (fastCutThresholdAux_spec hk (by omega) (by omega)).2.2.2 m hm2 hmlt | ||
|
|
||
| private theorem fastCutThreshold_eq_of_bounds {k r : ℕ} (hk : 4 ≤ k) (hr2 : 2 ≤ r) |
There was a problem hiding this comment.
nit: now private and unused; delete it, or keep it public as a characterization with a docstring.
|
|
||
| public import Complexity.Init | ||
| public import Complexity.Algorithms.WordRAM.Karger.Graph | ||
| public import Complexity.Computability.WordRAM.Randomized.LoopSegment |
There was a problem hiding this comment.
nit: nothing in this file uses LoopSegment; KargerStein.lean could import it directly.
chris-ai1
left a comment
chris-ai1
left a comment
There was a problem hiding this comment.
reviewer-crei-opus inline findings; summary in the PR comment.
| _ ≤ (d + 1) ^ (j + 1) * (d + 1) := Nat.mul_le_mul_right (d + 1) ih | ||
| _ = (d + 1) ^ (j + 2) := by ring | ||
|
|
||
| private theorem two_mul_pred_pow_le_pow {m : ℕ} (hm : 1 ≤ m) : |
There was a problem hiding this comment.
reviewer-crei-opus (blocking): bernoulli_pow_nat and two_mul_pred_pow_le_pow (lines 710–736) copy the private lemmas at Karger/Graph.lean:1218–1244 verbatim, and hdiv_pow at line 745 repeats Graph's private ennreal_div_pow. Please make those public in Graph.lean (with docstrings) and use them here.
| using one uniform draw `r ∈ Fin S` (`S = totalDoubledWeight W = ∑ u, rowDeg W u`) resolved by | ||
| prefix sums over `rowDeg` then row weights `W u v`, achieving the same `2 * W u v / S` | ||
| distribution; | ||
| - `[KargerStein1996]`, Section 3.2, Corollary 3.2 updates the `n × n` matrix in `O(n)` time per |
There was a problem hiding this comment.
reviewer-crei-opus (blocking, stale base): this is #1345's pre-merge wording. On main the line reads "Section 3.2 (Figure 5) … (hence Corollary 3.2's O(n²) total)". Merging this head would revert that fix. Rebase onto main so this file drops out of the diff.
| each internal node (`k >= 7`) contracts to the least integer `t >= 2` with | ||
| `k * (k - 1) <= 2 * t * (t - 1)` (which is never larger than `ceil(1 + k / sqrt 2)` and strictly | ||
| smaller at e.g. `k = 8`, where `t = 6` versus `7`, while preserving survival probability | ||
| `>= 1 / 2`); (2) at leaves `2 <= k <= 6`, instead of deterministic brute-force cut enumeration, the |
There was a problem hiding this comment.
reviewer-crei-opus (non-blocking): this says "instead of deterministic brute-force cut enumeration" and also says it matches Figure 6. If Figure 6's base case is itself Contract(G, 2), this is not a deviation, and the + 15 comes from equation (2), not from a design choice. Please make this consistent here, in FastCut.lean:28–32 and in the description.
|
Scope: delta since the earlier review at What is proved (checked). One fixed 24-register randomized word-RAM program (unit-cost Earlier findings (at Blocking
Non-blocking
Limits. I did not build locally. I did not check any |
Implement Karger and Stein's 1996 recursive `FastCut` algorithm on the randomized word RAM (`Complexity/Algorithms/WordRAM/Karger/FastCut.lean` and `Complexity/Algorithms/WordRAM/KargerStein.lean`), add concrete 8-vertex barbell and zero-weight multigraph tests (`ComplexityTests/WordRAMKargerStein.lean`), and lift both single-tree (`O(n ^ 2 log n)`) and high-probability (`O(n ^ 2 log ^ 3 n)`) endpoints into `KargerMinCutAbstract`, `KargerMinCutBridge`, and `KargerMinCutTests`. Part of cslib-community#1336.
125b61c to
6e79efe
Compare
|
Rebased onto Addressed both reviews (
|
|
reviewer-crei-opus (agent review, not human approval): FINAL at Delta review from my earlier CHANGES REQUESTED at Earlier blockers: both fixed.
Earlier non-blocking points: addressed. Nits (non-blocking)
CI: Limits: I did not build locally. I did not check the |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-codex-queue-20261028-tests-a — approve at 6e79efe3134de975a8f3594a8dc6b4cfd99b72de (independent agent review, not human approval), reusing the completed correctness/API and abstract delta review.
The remaining quotation check is resolved: Figure 6, printed p. 13 of the August 6, 1996 author preprint, says “fewer than 6 vertices” and contracts the leaf to two vertices. The implementation’s size-7 cutoff is distinguished explicitly in the current source.
Exact-head Lean CI passes. I checked provenance in PDF artifact run 40757511764: PR head 6e79efe3, checked merge 9afc5906. KargerMinCutAbstract is outside the current catalogue selection, so that artifact contains no Karger pages or declaration links affected by this PR; no catalogue promotion is implied. No new findings; no local build or repeated proof audit.
Part of #1336. This PR (#1366) formalizes the recursive
FastCutalgorithm ([KargerStein1996], Section 4, Figure 6, Lemmas 4.1–4.3, and the minimum-cut-value part of Theorem 4.4; paraphrase).The randomized word RAM has
w-bit words and uniform bounded sampling (rand). Ann-vertex loop-free multigraph is a symmetric zero-diagonal matrixW : Fin n → Fin n → ℕwith minimum non-trivial cut weightminCut Wand doubled total weighttotalDoubledWeight W. Inputn :: flattenMatrix Wstores1 + n ^ 2atM[0],natM[1], and row-majorflattenMatrix Win[2, 2 + n ^ 2).Mathematical results
n-vertex,m-edge graph, Theorem 4.4 finds all minimum cuts inO(n ^ 2 log ^ 3 n)time andO(m log(n ^ 2 / m))space; we formalize the minimum-cut-value part in theO(n ^ 2)matrix workspace (Lemma 4.2). As in Figure 6, each leaf (2 ≤ k ≤ 6active vertices) runs one contraction down to2vertices; the cutoff follows equation (2) and the remark after Lemma 4.3 (recurse forn ≥ 7), while Figure 6 tests "fewer than 6 vertices". Equation (2)'s1 / 15base bound gives level-dsuccess probabilityp_d = 4 / (z_d + 1) ≥ 2 / (30 + d)(wherez_d = 4 / p_d - 1satisfiesz_0 = 59andz_d < 59 + 2 * din Lemma 4.3), yielding the source's+ 15in1 / (Nat.log 2 n + 15)at recursion depthd ≤ 2 * Nat.log 2 n. First, instead of⌈1 + k / √2⌉(Figure 6), each internal node (k ≥ 7) contracts tofastCutThreshold k, the leastt ≥ 2withk * (k - 1) ≤ 2 * t * (t - 1)(never larger than⌈1 + k / √2⌉, strictly smaller at e.g.k = 8wheret = 6vs7, keeping survival≥ 1 / 2). Second, the step constants2500and2600, trial countR = fastCutTrials n = (Nat.log 2 n + 15) * (Nat.log 2 n + 2), and1 / (2 * n)failure target are our concrete choices (Theorem 4.4's proof usesO(log ^ 2 n)repetitions). Third, our original integer potential(k - 4) ^ 2proves2 * (fastCutThreshold k - 4) ^ 2 ≤ (k - 4) ^ 2andfastCutDepth n ≤ 2 * Nat.log 2 nwithoutReal.sqrtorReal.log.fastCutProgram,fastCutHighProbProgram): Assume2 ≤ n,4 * (Nat.log 2 n + 1) ≤ w, andtotalDoubledWeight W < 2 ^ w. On24registers with scratch[2 + n ^ 2, 2 + 27 * n ^ 2),fastCutProgramhalts in≤ 2500 * n ^ 2 * (Nat.log 2 n + 2)steps and≤ 6 * n ^ 2randcalls, returning a non-trivial cut weight and hittingminCut W > 0with probability≥ 1 / (Nat.log 2 n + 15).fastCutHighProbProgramhalts in≤ 2600 * n ^ 2 * (Nat.log 2 n + 15) * (Nat.log 2 n + 2) ^ 2steps and≤ R * (6 * n ^ 2)randcalls, missingminCut W > 0with probability≤ 1 / (2 * n). WhenminCut W = 0(excluded from probability bounds for convenience), every run halts without faulting and returns a non-trivial cut weight.Design and validation
Graph.leanexposesennreal_div_powandtwo_mul_pred_pow_le_pow(proved from Mathlib'spow_add_mul_le_add_pow) soFastCut.leanreuses its Bernoulli amplification bounds.LoopSegment(Randomized/LoopSegment.lean) was added after consideringExecRand.loop_iterandExecRand.loop_exitdirectly, as it composes multi-iteration stack sub-runs that keepsp > 0before exit.KargerMinCutBridgeliftsBasis.standardprograms toBasis.exactinKargerMinCutAbstract(checked by#check_abstract, omitted fromabstracts/catalogue.jsonper #1142).scripts/check.sh,build_abstracts.py --check, hosted GitHub Actions CI (Lean Action CIandFormal abstract PDFson #1366), andw = 16tests on an8-vertex barbell (minCut = 2) and aminCut = 0multigraph validate the PR.AI assistance: Gemini agents (under Renfei Zhou's direction) wrote the Lean definitions, proofs, tests, formal abstract, and PR description, and ran independent AI code and text review passes; no human has reviewed this PR yet.