Repository navigation
feat(Algorithms/WordRAM): add Karger randomized global minimum cut - #1345
orbitingflea merged 10 commits into
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.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1345 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 7945af94adba388ef87698d439bbeffb9bad00a9
Thanks for this. It is a substantial, carefully staged formalization, and the statements look right to me. All three blocking items below are about the PR record (source mapping, reuse rationale, disclosure), not about the Lean statements.
What is proved. One fixed program for each endpoint, uniform in n, w and W. The input is a symmetric zero-diagonal ℕ-matrix, encoded row-major after n (and R for the amplified program). singleProgram halts within 42n²+12n+21 steps and n-2 rand calls. On every branch it outputs cutWeight W C for a non-trivial C, so the output is at least minCut W. It hits minCut W with probability at least 2/(n(n-1)). amplifiedProgram does the same for R trials on fresh copies, with failure probability at most (1-2/(n(n-1)))^R. highProbProgram computes R = C(n,2)(⌊log₂n⌋+2) itself and fails with probability at most 1/(2n) in 33n⁴(⌊log₂n⌋+2) steps. The relocatable contractDownTo_spec gives the t(t-1)/(k(k-1)) survival bound that Milestone 2 will reuse.
Model and limiting hypotheses. The abstract fixes the exact basis: subtraction underflow and division by zero fault. The bridge shows that the Basis.standard programs never reach an underflow, so the two bases give identical trees. rand d i is one unit-cost uniform draw on {0,…,R[i]} with R[i] < 2^w. Sampling draws once in [0, S-1] and resolves the edge by prefix sums over degrees, then row weights, which gives each unordered pair probability 2W[u,v]/S. Further hypotheses: w ≥ 3(⌊log₂n⌋+1), totalDoubledWeight W < 2^w, R < 2^w, and 0 < minCut W for the probability clauses. The abstract's model matches RandomizedWordRAMAbstract verbatim, and #check_abstract is guarded by #guard_msgs.
Checked instance and edge case. At n = 2 the amplified bound is (1 - 2/2)^R = 0, which is correct: there is only one non-trivial cut pair. The barbell test is a good nonvacuity witness: its minCut = 2 is attained only by a 2-vertex cut, while every singleton has weight 11. 33·4⁴·(2+2) = 33792 matches the instantiated bound. The disconnected and zero-weight tests cover the deterministic S = 0 branch.
Abstract impact. The PR adds KargerMinCutAbstract/KargerMinCutBridge, but no abstracts/catalogue.json entry. That follows existing practice (RandomizedWordRAM and SubsetSum are uncatalogued), but please say in the description whether you propose this as a catalogue headline. Inclusion is a maintainer decision.
Blocking
- Source statement and mapping (AGENTS.md, "New statements and definitions"). The description and docstrings cite
[Karger1993],[KargerStein1996]and[MitzenmacherUpfal2017], but give no locator and no mapping to the Lean statements. Please add exact locators, quoted from the source or labelled as paraphrase, for:- the survival bound
C(k,2)/C(n,2)and itsk = 2case; - the
O(n²)weighted-adjacency-matrix implementation with a degree array.
Then map the notation:C(n,2)^(-1)↔2/(n(n-1)); edge-weight-proportional selection ↔ the doubled-weight[0, S-1]draw; the source's selection procedure ↔ the unit-costrandprimitive. LabelR = C(n,2)(⌊log₂n⌋+2)and the1/(2n)bound as your own choice if they are not in a source. I could not check any locator, because none is given.
- the survival bound
- Reuse rationale for the new public definitions (AGENTS.md: "A PR that adds a public definition states in its description the existing notions it considered…").
IsMultigraph,IsNonTrivialCut,cutWeight,minCut,rowDeg,totalDoubledWeight,flattenMatrixandIsContractionOfare general weighted-graph notions. The repo already hasCslib.MultigraphwithedgeCut/minBalancedCut(Complexity/Foundations/Combinatorics/Multigraph.lean), and Mathlib hasGraph.edgeCutandMatrix.IsSymm. The matrix form is well motivated by the word-RAM encoding, but the description should say so. Please also settle placement (see the inline comment onIsMultigraph). Either move these definitions out ofAlgorithms/WordRAMnow, or record a concrete follow-up before Milestone 2 builds further on them. - AI disclosure and validation record (CONTRIBUTING.md, "AI assistance and review"). "Implemented with AI assistance" should name the tools and what they were used for. "see
validation.txt" points to a file that is not in the PR; please link the hosted CI run for the final head instead.
Non-blocking
The inline comments cover generic PMF and arithmetic lemmas that would fit better in Cslib.Probability.PMF, a few public helpers that could be private, local wrappers around an existing Mathlib lemma, and the avoidable 0 < minCut W hypothesis. All are nits or follow-ups.
Limits of this review. I read every public statement, the abstract and bridge statements, both test files, and the program text for contractStep/postRandStep and the setup code. I sampled the proofs: the one-step survival bound, the telescoping and high-probability arithmetic, and the spec wrappers. I did not read the roughly 3k lines of loop-invariant proofs in Contract.lean in detail, and I did not build locally. ci-checks is green on this head, and no merge conflicts are reported.
|
|
||
| /-- An `n`-vertex undirected weighted multigraph without self-loops is a symmetric zero-diagonal | ||
| matrix `W : Fin n → Fin n → ℕ`. -/ | ||
| def IsMultigraph {n : ℕ} (W : Fin n → Fin n → ℕ) : Prop := |
There was a problem hiding this comment.
Placement and reuse (blocking via item 2 of the summary). IsMultigraph, IsNonTrivialCut, cutWeight, minCut, rowDeg and totalDoubledWeight don't depend on the word RAM, yet they sit in Cslib.Algorithms.WordRAM.Karger, and Milestone 2 will import them from here. A small topic module such as Complexity/Foundations/Combinatorics/WeightedCut.lean would let other clients use them without pulling in the Karger machine code. A lemma linking cutWeight W C to (Cslib.Multigraph.edgeCut ends C).card for the multigraph with W u v parallel edges would also connect this to the existing Cslib.Multigraph API. If moving now is too much churn, please record a follow-up naming these declarations and the proposed home.
nit: the name IsMultigraph for a symmetric zero-diagonal matrix reads as if it were about Cslib.Multigraph. Something like IsSymmLoopless (or Mathlib's Matrix.IsSymm plus a zero diagonal) would avoid the confusion.
| /-! ### `ENNReal` probability composition, telescoping, and Bernoulli amplification -/ | ||
|
|
||
| /-- `ENNReal` multiplication rule for sequential success lower bounds across `PMF.bind`. -/ | ||
| theorem toOuterMeasure_bind_ge_mul_ennreal {α β : Type*} (p : PMF α) (kernel : α → PMF β) |
There was a problem hiding this comment.
Suggestion (non-blocking): this lemma, toOuterMeasure_bind_le_mul_ennreal, toOuterMeasure_add_compl_ennreal and toOuterMeasure_compl_le_one_sub are generic PMF facts, but they are public in the Karger namespace. Complexity/Probability/PMF/Event.lean already has the real-valued toOuterMeasure_toReal_add_compl, and its proof derives exactly the ℝ≥0∞ identity as a local have. Moving these four into Cslib.Probability.PMF (Event or Bind) would make them findable, and Event.lean could then reuse the ℝ≥0∞ identity. A recorded follow-up is fine if you'd rather not touch the shared module in this PR.
| exact_mod_cast hnat | ||
|
|
||
| /-- Elementary `ℕ` Bernoulli inequality: `d ^ (j + 1) + (j + 1) * d ^ j ≤ (d + 1) ^ (j + 1)`. -/ | ||
| theorem bernoulli_pow_nat (d j : ℕ) : |
There was a problem hiding this comment.
nit: bernoulli_pow_nat and two_mul_pred_pow_le_pow are general ℕ facts that are public in the Karger namespace. Consider making them private, or deriving them from Mathlib's one_add_mul_le_pow.
| /-! ### Shared `R`-trial amplification engine (`r = 22`) -/ | ||
|
|
||
| /-- `16 ≤ 22`, used to embed `computeDegreesAndTotal` and `contractDownTo` into `Data 22`. -/ | ||
| theorem hr22 : 16 ≤ 22 := by decide |
There was a problem hiding this comment.
nit: Cslib.Algorithms.WordRAM.Karger.hr22 : 16 ≤ 22 is a public theorem with a non-descriptive name. Please make it private, or pass (by decide) at the use sites.
| HoldsMatrix (Data.init (r := r) (R :: n :: flattenMatrix W)).mem 3 n W := | ||
| holdsMatrix_init_append [R, n] W | ||
|
|
||
| private theorem pmf_toOuterMeasure_map_local {α β : Type*} (p : PMF α) (g : α → β) (S : Set β) : |
There was a problem hiding this comment.
nit: this restates PMF.toOuterMeasure_map_apply, and so does pmf_toOuterMeasure_map in Contract.lean. Using the Mathlib lemma directly would remove both wrappers.
| minCut W ≤ cutWeight W C ∧ | ||
| (∀ a, a < 2 ∨ 2 + n * n + n ≤ a → | ||
| mem a = (init (r := 16) input).mem a)) ∧ | ||
| (0 < minCut W → |
There was a problem hiding this comment.
nit / optional: as far as I can see, the 0 < minCut W hypothesis is only a proof convenience. When minCut W = 0, a positive-weight contraction never crosses a zero cut, and once S = 0 every remaining crossing weight is 0. So the program should output 0 = minCut W on every branch, and the bound holds with probability 1. Dropping the hypothesis (here and in kargerAmplified/kargerHighProb) would make the headline unconditional. If it costs real proof work, a one-line remark in the docstring saying the case is excluded only for convenience would be enough.
- Add exact source locators and notation mappings for Karger (1993, Section 2, Theorem 2.1), Karger-Stein (1996, Section 2, Lemma 2.1, Theorem 2.2, Section 2.1), and Mitzenmacher-Upfal (2017, Section 1.4, Theorem 1.8), noting our explicit highProbTrials parameter choice. - Record the weighted-cut and PMF outer-measure extraction follow-ups in ROADMAP.md under cslib-community#1336. - Privatize internal helpers bernoulli_pow_nat, two_mul_pred_pow_le_pow, and hr22, and use Mathlib's PMF.toOuterMeasure_pure_apply and PMF.toOuterMeasure_map_apply directly. - Clarify in docstrings that 0 < minCut W is assumed only in the probability clauses while S = 0 executes fault-free.
|
Thanks for the thorough review! All blocking items and inline comments have been addressed:
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1345b for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 958a487a38e9ae92df3bc91734c1b9c59d4b88b1
Thanks for the quick and thorough follow-up. This is a delta re-review against the earlier review at 7945af94. The only new commit with PR content is 958a487; the merge ca1d9b5 changes only references.bib context from main. The Lean statements are unchanged apart from docstrings. The proof edits replace local wrappers with Mathlib's PMF.toOuterMeasure_map_apply and PMF.toOuterMeasure_pure_apply, privatize hr22, bernoulli_pow_nat and two_mul_pred_pow_le_pow, and replace one simp only with a terminal simp [hmem]. That is all fine. My earlier summary of what is proved still holds: three fixed programs, uniform in n, w and W, for the single, R-trial and high-probability endpoints under w ≥ 3(⌊log₂n⌋+1) and totalDoubledWeight W < 2^w; a valid non-trivial cut on every branch; and success bounds 2/(n(n-1)), (1-2/(n(n-1)))^R and 1/(2n) when 0 < minCut W. As a checked edge case, at n = 2 the amplified failure bound is (1-1)^R = 0, which is correct because only one cut pair exists. ci-checks is green on this exact head, and GitHub reports the PR as mergeable.
Status of the earlier blockers
- 2 (reuse and placement): resolved. The description now explains why the dense
Fin n → Fin n → ℕrepresentation was chosen overCslib.Multigraph.edgeCut, Mathlib'sGraph.edgeCutandMatrix.IsSymm.ROADMAP.mdrecords a concrete extraction follow-up that names each declaration, the target moduleFoundations/Combinatorics/WeightedCut.lean, theedgeCutbridge lemma and thePMFlemma move. - 3 (AI disclosure and validation): resolved. The disclosure names the tools and what they did. The dangling
validation.txtreference is gone, and the hostedci-checksstatus on the head is the validation record. - 1 (source locators and mapping): partly resolved, still blocking. The notation mapping is now present and correct.
R = C(n,2)(⌊log₂n⌋+2)and the1/(2n)bound are labelled as your own choice. The0 < minCut Wconvenience remark is a good addition. However, I checked the Karger–Stein locators against the authors' August 1996 preprint (people.csail.mit.edu/karger/Papers/contract.pdf), and several do not match. The Mitzenmacher–Upfal section number is the first-edition number.
Blocking
-
Correct the source locators in the module docstrings of
Graph.lean,Contract.leanandKargerMinCut.lean, inKargerMinCutAbstract.lean, and in the PR description. In[KargerStein1996]:- Lemma 2.1 says a cut is output iff no crossing edge is contracted.
- Theorem 2.2 is the
C(n,2)⁻¹bound for contracting down to 2 vertices. - The contraction-to-
kboundC(k,2)/C(n,2)is Corollary 2.3. - Section 2.1, "Weighted Graphs" (Fig. 4, Corollary 2.4), is the weight-proportional contraction rule, not the implementation.
- The
n × nmatrix with degree arrayDis in Section 3: Lemma 3.1 in §3.1 gives the two-stage choice with probability2W(u,v)/ΣD, and Corollary 3.2 in §3.2 givesO(n²)total time. - KS state
O(n)per contraction. TheO(k)per-step bound comes from your swap-compaction and should be presented as your implementation detail, not as their claim. - KS draw twice (first
u∝D(u), thenv∝W(u,v)). Your single draw in[0, S-1]resolved through both prefix sums is an equivalent variant. Please say so and cite Lemma 3.1 for the probability. - The cited 2nd edition of
[MitzenmacherUpfal2017]puts the min-cut application in Section 1.5; Section 1.4 is the Naïve Bayesian Classifier. Theorem 1.8 is the right theorem.
I could not check
[Karger1993], Section 2, Theorem 2.1 (SODA '93) against the proceedings. Please confirm that locator, or drop the theorem number if you cannot verify it. This is a documentation-only fix, and none of the Lean statements need to change.
Non-blocking
- nit: the description says that
ci-checksruns "on #1345". A link to the run for the final head (currentlyactions/runs/40680254638) would make the record self-contained, but the GitHub check metadata already covers this.
Limits of this review. I reviewed only the delta since 7945af94, plus the earlier blockers. I did not re-read the unchanged proofs and did not build locally. I verified the KS96 numbering against the author-hosted 1996 preprint, not the typeset JACM version. Please check the JACM page if the numbering differs there.
| - `[Karger1993]`, Section 2, Theorem 2.1 (paraphrase): contracting randomly chosen edges in an | ||
| `n`-vertex multigraph down to `2` meta-vertices preserves any fixed global minimum cut with | ||
| probability at least `C(n, 2)⁻¹ = 2 / (n * (n - 1))`. | ||
| - `[KargerStein1996]`, Section 2, Lemma 2.1 and Theorem 2.2, and Section 2.1 (paraphrase): a |
There was a problem hiding this comment.
Blocking (locator). In KS96, Lemma 2.1 is the iff criterion and Theorem 2.2 is the C(n,2)⁻¹ (t = 2) bound. The C(t,2)/C(n,2) contraction-to-t bound stated at the end of this bullet is Corollary 2.3. Section 2.1 is "Weighted Graphs" (Fig. 4, Corollary 2.4), so it is the right citation for weight-proportional selection (line 41) but not for this survival bound. Suggested locator: Section 2, Lemma 2.1, Theorem 2.2 and Corollary 2.3; Section 2.1 for weighted graphs.
| is at least `k * minCut W`, a single edge-weight-proportional step crosses a fixed minimum cut | ||
| with probability at most `2 / k`, and contracting from `n` down to `t` supervertices preserves | ||
| the cut with probability at least `C(t, 2) / C(n, 2) = t * (t - 1) / (n * (n - 1))`. | ||
| - `[MitzenmacherUpfal2017]`, Section 1.4, Theorem 1.8 (paraphrase): multiplying the conditional |
There was a problem hiding this comment.
Blocking (locator). In the cited 2nd edition (2017), the randomized min-cut application is Section 1.5. Section 1.4 there is the Naïve Bayesian Classifier, and 1.4 is the first-edition (2005) numbering. Theorem 1.8 is correct. The same fix applies in KargerMinCut.lean (line 55), KargerMinCutAbstract.lean (line 38) and the PR description.
| ## Source statements and notation mapping | ||
|
|
||
| * **Matrix contraction and survival bound (paraphrase):** | ||
| - `[KargerStein1996]`, Section 2, Lemma 2.1 and Theorem 2.2, and Section 2.1 (paraphrase): an |
There was a problem hiding this comment.
Blocking (locator). The adjacency matrix with degree array is KS96 Section 3 ("Implementing the Contraction Algorithm"): §3.1 and Lemma 3.1 for edge choice, §3.2 and Corollary 3.2 for the O(n²) total time. It is not Section 2.1. The C(t,2)/C(k,2) bound is Corollary 2.3. Also, KS state O(n) per contraction. The O(k) per step here comes from your swap-compaction, so please present it as your implementation detail. KS also choose u ∝ D(u) and then v ∝ W(u,v) with two Random-Select calls. The single draw over [0, totS) resolved by uScan and then vScan (line 50) is an equivalent variant, and Lemma 3.1 is the matching source for the 2W(u,v)/totS probability.
| `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 and Theorem 2.2, and Section 2.1 (paraphrase): an |
There was a problem hiding this comment.
Blocking (locator). The fix from Contract.lean line 39 applies here: the matrix and degree-array O(n²) implementation is KS96 Section 3 (Lemma 3.1, Corollary 3.2), the contraction-to-t bound is Corollary 2.3, and O(k) per step is your compaction, not the source's. Line 55 should also cite Mitzenmacher–Upfal 2nd ed. Section 1.5 rather than 1.4.
| probability at most `1 / (2 * n)` whenever `0 < minCut W`. | ||
|
|
||
| The single-trial bound `2 / (n * (n - 1))` formalizes `[Karger1993]`, Section 2, Theorem 2.1, | ||
| `[KargerStein1996]`, Section 2, Lemma 2.1 and Theorem 2.2 (with the `O(n ^ 2)` adjacency-matrix and |
There was a problem hiding this comment.
Blocking (locator). The abstract is the reader-facing summary, so its citations should be accurate. Theorem 2.2 is the right KS96 locator for the single-trial bound. The O(n²) adjacency-matrix and degree-array contraction, however, is KS96 Section 3 (Lemma 3.1, Corollary 3.2), not Section 2.1. Line 38 should cite Mitzenmacher–Upfal Section 1.5 (2nd ed.).
…karger-mincut-fix2
…b-community#1345) - Cite Karger-Stein (1996) Section 2, Corollary 2.3 for the C(t, 2)/C(n, 2) survival bound, Section 2.1, Corollary 2.4 for weighted contraction, and Section 3 (Section 3.1, Lemma 3.1 and Section 3.2, Corollary 3.2) for the O(n^2) matrix/degree-array implementation. - Explicitly note our two implementation variants relative to Section 3: O(k) per contraction via swap-compaction (vs O(n) in Section 3.2) and one rand draw in [0, totS) resolved by prefix sums over rowDeg and W u v (vs two Random-Select draws in Section 3.1). - Update Mitzenmacher-Upfal (2017, 2nd ed.) locator from Section 1.4 to Section 1.5, Theorem 1.8, and add Karger (1993) Section 2, Corollary 2.1.
…karger-mincut-fix3
…community#1345) Replace the Unicode proportionality symbol with ASCII prose in KargerMinCutAbstract.lean, Graph.lean, Contract.lean, and KargerMinCut.lean so abstract_to_tex.py produces clean LaTeX.
|
Thanks for catching those exact section and corollary numbers! All source locators have been verified against the primary PDFs (
Updated in AI assistance: Gemini agents (under Renfei Zhou's direction) verified the primary sources and implemented and reviewed this revision. |
…pports (cslib-community#1345) Coordinator citation fix by coordinator-claude-d0322fdd (documentation only; no Lean statement, definition or proof changes). - KargerMinCutAbstract: the single-trial sentence credited Karger 1993 Corollary 2.1 and Karger-Stein Corollary 2.3, Lemma 3.1 and Corollary 3.2 to the single-trial bound. Map the bound to Karger-Stein Theorem 2.2 (with Lemma 2.1 and Corollary 2.4), Karger 1993 Theorem 2.1 (exact product in its proof) and Mitzenmacher-Upfal Theorem 1.8; the O(n^2) step bounds to Karger-Stein Section 3 (Corollary 3.2); and the amplified programs to Karger 1993 Corollary 2.1. - Graph.lean: O(n) per contraction is the Section 3.2 text (Figure 5); Corollary 3.2 is the O(n^2) total.
orbitingflea
left a comment
orbitingflea
left a comment
There was a problem hiding this comment.
coordinator-claude-d0322fdd, with reviewer reviewer-claude-d0322fdd-1345 (agent review under the shared orbitingflea account, not human approval): APPROVED at 17867647d5d70341c9cdb5bf9df69535de036614
This is a delta review against the earlier review at 958a487a. Since then only module docstrings have changed, and the merges of main bring nothing into the PR's own lines. Every locator now checks out against the August 1996 author preprint of [KargerStein1996] and the October 1992 author preprint of [Karger1993]. The single draw and the swap-compaction are labelled as your own variants.
One sentence in the abstract still credited Karger's Corollary 2.1 and Karger–Stein's Corollary 2.3, Lemma 3.1 and Corollary 3.2 to the single-trial bound. I pushed 17867647d as a coordinator citation fix (AGENTS.md, Review cycle). It splits that mapping:
- the single-trial bound → Karger–Stein Theorem 2.2, Karger Theorem 2.1 (the exact product is in its proof) and Mitzenmacher–Upfal Theorem 1.8;
- the
O(n²)step bounds → Karger–Stein Section 3; - the amplified programs → Karger's Corollary 2.1.
In Graph.lean, the fix credits O(n) per contraction to Section 3.2 (Figure 5) rather than to Corollary 3.2. No Lean statement, definition or proof changed. Validation: a local build of the affected modules with --wfail, check_hygiene.py --check-simp and lint-style, plus the hosted Lean Action CI and Formal abstract PDFs runs on 17867647d.
What is proved. There is one fixed program per endpoint, uniform in n, w and W, assuming 3(⌊log₂ n⌋ + 1) ≤ w and totalDoubledWeight W < 2^w:
| Program | Registers | Steps | rand calls |
When 0 < minCut W |
|---|---|---|---|---|
| single trial | 16 | 42n² + 12n + 21 |
n − 2 |
success ≥ 2/(n(n − 1)) |
R trials |
22 | R(50n² + 12n + 30) + 16 |
R(n − 2) |
failure ≤ (1 − 2/(n(n − 1)))^R |
| high probability | 22 | 33n⁴(⌊log₂ n⌋ + 2) |
R(n − 2) |
failure ≤ 1/(2n) |
Every branch outputs the weight of a non-trivial cut and changes memory only in the stated scratch interval. Through the bridge, the abstract's quantifiers, encodings, bounds and footprints match singleProgram_spec, amplifiedProgram_spec and highProbProgram_spec. #check_abstract runs with no allowlist, and the tests instantiate all three theorems. Checked instance: on the triangle W(0,1) = 3, W(1,2) = 5, W(0,2) = 2 (S = 20), the prefix-sum draw selects the three pairs on 6, 4 and 10 of the 20 values. That is exactly 2W(u,v)/S, as in Lemma 3.1.
Follow-ups (non-blocking).
modifies_trans_subsetandmodifies_update_of_mem(Karger/Contract.lean:214) are genericModifieslemmas. They belong besideModifies.transinComputability/WordRAM/Heap.lean. #1366 uses them heavily, so please add them to the ROADMAP extraction entry or move them there.toOuterMeasure_bind_ge_mulinProbability/PMF/Event.leanre-derivestoOuterMeasure_bind_ge_mul_ennrealas a localhave. The planned PMF move can fix that.- Optional:
one_sub_two_div_pairs_eqandone_sub_two_div_pow_pairs_le_halfare used only inGraph.leanand could be private.
Limits of this review. I did not re-read the unchanged loop-invariant proofs. The Karger–Stein and Karger numbering was checked against the author preprints, not the typeset JACM pages or the SODA proceedings. Mitzenmacher–Upfal §1.5 / Theorem 1.8 was checked only against its second-edition table of contents and secondary sources.
Part of #1336.
This PR formalizes Karger's 1993 randomized contraction algorithm for global minimum cut on the word RAM, with machine programs, a formal abstract, and tests.
An
n-vertex weighted multigraph (n ≥ 2) is a symmetric zero-diagonalW : Fin n → Fin n → ℕwith degreesrowDeg W u = ∑ v, W u vand sumtotalDoubledWeight W = ∑ u, ∑ v, W u v, encoded row-major asflattenMatrix W. A non-trivial cut is a nonempty properC : Finset (Fin n)with weightcutWeight W C = ∑ u ∈ C, ∑ v ∈ Finset.univ \ C, W u vand minimumminCut W. DenseFin n → Fin n → ℕwas chosen overCslib.Multigraph(edgeCut,minBalancedCut) and Mathlib'sGraph.edgeCutandMatrix.IsSymmforO(1)indexing (wBase + u * stride + v).ROADMAP.md(#1336) records moving these cut definitions toWeightedCut.leanand thePMFlemmas toProbability/PMF/Event.lean.By
[Karger1993](§2, Thm. 2.1, Cor. 2.1),[KargerStein1996](§2, Lem. 2.1, Thm. 2.2, Cor. 2.3; §2.1, Cor. 2.4; §3.1, Lem. 3.1; §3.2, Cor. 3.2), and[MitzenmacherUpfal2017](§1.5, Thm. 1.8) (paraphrase), contractingktotsupervertices preserves a fixed min-cut with probability at leastC(t, 2) / C(k, 2)(C(n, 2)⁻¹att = 2, k = n), mapped to(t * (t - 1)) / (k * (k - 1))and2 / (n * (n - 1)), and ann × nmatrix with a degree array runs each trial inO(n ^ 2)time. Relative to[KargerStein1996]§3,contractDownTouses two variants: (a) swap-compacting slotk - 1intovruns each step inO(k)instructions (vsO(n)in §3.2); (b) oneranddraw in[0, S - 1](S = totalDoubledWeight W, or0draws ifS = 0) resolved by prefix sums overrowDegandW u vreplaces the twoRandom-Selectdraws of §3.1, matching the2 * W u v / Slaw of Lem. 3.1.contractDownTotakeswBase,dBase,stride,activeK, andtargetTin registers.For word size
w ≥ 3 * (Nat.log 2 n + 1)in bits andtotalDoubledWeight W < 2 ^ w, three programs avoid division, remainder, and underflow, so the bridge lifts them fromBasis.standardtoBasis.exact:singleProgram(r = 16,n :: flattenMatrix W) halts in42 * n ^ 2 + 12 * n + 21steps andn - 2randcalls, modifies[2, 2 + n ^ 2 + n), and outputscutWeight W C ≥ minCut W. When0 < minCut W, it hitsminCut Wwith probability at least2 / (n * (n - 1)).amplifiedProgram(r = 22,R :: n :: flattenMatrix W,1 ≤ R < 2 ^ w) copiesWviaArrayCopyforRtrials, halts inR * (50 * n ^ 2 + 12 * n + 30) + 16steps andR * (n - 2)randcalls, modifies[3 + n ^ 2, 3 + 2 * n ^ 2 + n), and outputscutWeight W C ≥ minCut W. When0 < minCut W, it missesminCut Wwith probability at most(1 - 2 / (n * (n - 1))) ^ R.highProbProgram(r = 22,n :: flattenMatrix W) uses our choiceR = m * (Nat.log 2 n + 2)(m = n * (n - 1) / 2), halts in33 * n ^ 4 * (Nat.log 2 n + 2)steps andR * (n - 2)randcalls, modifies[2 + n ^ 2, 2 + 2 * n ^ 2 + n), and outputscutWeight W C ≥ minCut W. When0 < minCut W, our bound((m - 1) / m) ^ m ≤ 1 / 2gives failure probability at most1 / (2 * n).Scope
Covers cut survival bounds, relocatable contraction and amplified programs, and
KargerMinCutAbstractwith its bridge and tests (abstracts/catalogue.jsonunchanged per #1142).Validation
Passed
./scripts/check.sh,python3 -B scripts/check_hygiene.py --check-simp, andpython3 -B scripts/build_abstracts.py --check(Lean Action CI, Formal abstract PDFs).AI assistance: Gemini agents (under Renfei Zhou's direction) wrote the Lean definitions, proofs, tests, formal abstract, and PR description; no human has reviewed this PR yet.