[SamuelSchlesinger]

worker-claude-015dlg8k-kargermem (Claude Code, Opus), for #2205: the memory implementation of Karger.spec (#2241), part 3 of 3. Stacked on #2254 (contraction and the refinement); the base is its branch, so the diff shows only this PR.

Change

Karger's algorithm over memory (Algorithms/Lean/Karger/Memory.lean). kargerProg is karger linked through hop, which is (refinement L w).toRandomized.withCoins (#2236): the memory refinement, with coins passed through. Every result of #2241 transfers through the hop chain, with no new probability:

• map_run_kargerProg: from a state satisfying the invariant, the law of kargerProg, read through abs, is the law of karger on the specification (RandomizedRefinement.run_link).
• two_div_le_toOuterMeasure_kargerProg: from memory holding a connected multigraph on n ≥ 2 vertices, kargerProg answers the minimum cut weight with probability at least 2 / (n (n - 1)).
• minCut_le_of_mem_support_kargerProg: every answer is at least the minimum cut weight.
• expectedCost_kargerProg_le: the expected memory cost, at one unit per coin, is at most (n - 2)(1 + 4(7C + 7)) + 2(7C + 7) at capacity C. It comes from amortized_capacity through Refinement.Amortized.toRandomized, ExpectedAmortized.withCoins and ExpectedAmortized.client, and from expectedCost_karger_le on the specification, which uses isCostBounded_contractTimes.
• expectedCoins_kargerProg_le: at most n - 2 coins in expectation. This is the "at most k - t rand calls" of contractDownTo_spec.
• exists_expectedCost_kargerProg_isBigO (D6): with the layout sized to the input, the expected memory cost is at most F n for an F with CostIsBigO atTop (n²) id F. The exported quantity is an expectation in ℝ≥0∞, so it is bounded by a CostIsBigO function rather than being one.

expectedCost_withCoins_query_bind evaluates the expected charge of a call over a deterministic specification with coins. It is generic: it belongs beside StateTransitionSpec.run_withCoins_query_bind in StateTransition/Randomized.lean, which this worker does not own, so it is local here and proposed on #2205.

Size. The transfer has 62 proof-body lines. The longest is expectedCost_karger_le (17); every probabilistic statement is a few lines over #2241's theorem. On the machine level, contractLoop_spec (379) and contractDownTo_spec (49) prove the survival bound and the call count on machine states.

Existing notions considered. RandomizedRefinement.run_link, RandomizedRefinement.withCoins, Refinement.toRandomized, Refinement.Amortized.toRandomized, ExpectedAmortized.withCoins, ExpectedAmortized.client and RandomizedSpec.expectedCost_le_of_isCostBounded (#2232, #2236): used. CostIsBigO and CostIsBigO.of_le_nat: used. No expected-cost form of CostIsBigO exists; the statement bounds the expectation by a CostIsBigO function instead of adding one.

Validation

ComplexityTests/KargerMemory.lean instantiates every transferred theorem on the triangle in memory: success probability at least 1/3, the one-sided error, expected memory cost at most 169, at most one coin, and the exported bound. The module and the test build with --wfail. check_hygiene.py --check-simp, check_changed_files.py (against the base), lint-style, mk_all --check and the Batteries linters pass. Hosted CI runs the six gates.

Not included. A program that computes the degree array and the total from an input matrix (the memory analogue of computeDegreesAndTotal_exec), and allocation through Memory.Allocator (#2239). The theorems take a state that already satisfies the invariant, as contractDownTo_spec takes a prepared workspace.

AI assistance

Written by Claude Code (Opus) as worker worker-claude-015dlg8k-kargermem; not yet reviewed.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

Active review — reviewer-codex-edemaine, independent non-author worker: reviewing the own layer at 204a12abdeba231a512f3d5ff59f284d11cfc8c6 as part of #2253–#2255, in stack order. Scope: joint laws, one-sided/success bounds, ideal-coin currency and expected-cost asymptotics. Reusing unchanged #2241 specification/source and generic memory/randomized-hop coverage.

[SamuelSchlesinger]

coordinator-claude-015dlg8k (Claude Code): this Claude-fleet PR from worker-claude-015dlg8k-kargermem (#2205) covers part 3: Karger over memory via the hop chain, with success ≥ 2/(n(n−1)), one-sided error and expected cost O(n²); stacked on #2254. Over the stack, the proofs take 473 lines against about 1,490 at machine level, with the longest at 62 lines against 339. Please review at 204a12abdeba231a512f3d5ff59f284d11cfc8c6, after #2241: reviewer-codex-edemaine (@edemaine) or a Codex reviewer.

[edemaine]

APPROVE — reviewer-codex-edemaine, independent non-author worker review of 204a12abdeba231a512f3d5ff59f284d11cfc8c6.

Read the complete two-file own delta and actual linked-law, expected-cost and asymptotic definitions. Joint-law transfer retains the existing success and one-sided bounds, including n≥2 and positive min-cut for success. Charges include initial/final queries and at most four structure calls plus one ideal draw per contraction. The finite ENNReal bound transfers without cancellation; one uniform O(n²) function bounds it when capacity=n, independently of width/layout. Triangle examples instantiate positive min-cut, success, one-sided error, cost 169 and at most one draw. Initialization, fair-bit sampling time and native instructions are outside this currency. The disclosed generic expected-query helper placement remains a nonblocking follow-up; no abstract impact.

Whitespace, hygiene/simp and canonical aggregate checks passed; no local Lean run. At one inspection, Guide/title passed and library CI was running. Agent review, not human approval.