[SamuelSchlesinger]

Part of #3725 (repeated proof machinery). Author: Jetski worker sessions 025a212a (delegating) and 4702ea05 (implementation), branch proofs/wordram-algorithm-twins. This PR is its own task record.

Three Word-RAM algorithm refactors, one commit each:

1. Karger amplification loop. ampLoop_law (KargerMinCut) and fastCutAmpLoop_law (KargerStein) repeated the same 25-line induction over the remaining trials. The new public Karger.minRunsLoop_law in Algorithms/WordRAM/Karger/OutputLaw.lean sits next to minUpdate_exec, whose module docstring already describes the shared best-cut update, and is listed in Main results. It covers any while trial < trials do body with invariant Inv i, given R ≥ 1, T + 2 ≤ S and a body law μ.map (if i = 0 then v else min v best), and concludes the minRuns/minStep law. Both client statements are unchanged, and each proof is now an unfold plus one exact. OutputLaw publicly imports Lean/Karger/Contraction because the statement names minRuns/minStep; both clients already depended on it.
2. Multiword. Arithmetic's private exec_clear_framed re-proved Mul's Schoolbook.exec_clear (same code, same induction), and its only caller used only the memory part. exec_clear is now public with a docstring, and the copy is deleted. exec_row also composes its frames with the existing frame_trans/frame_mono, as Sub.exec_digits already does.
3. ExactTriangle exec_adapt. The three per-square copy calls shared about 14 lines of fact plumbing each. They now use one private exec_copyStep.

No existing public statement or name changes. New public API: minRunsLoop_law, plus exec_clear made public. Net −44 lines (+98/−142). proof_copies.py reports no repeated block in the touched files.

Left as is, with reasons:

• exec_row (multiply-add with carry) vs exec_digits (subtract with borrow): the cell semantics, invariants and value equations differ, so a generic digit loop would abstract all three.
• fastCutStep_stage0/1_law: different branch nesting.
• The ExactTriangle Instances layout preambles: fixing them would mean a representation redesign with named layouts.
• The MatrixReadback p/q branches: these differ in their residue arguments.

This is refactoring only, with no new mathematics.

Validation: lake build --wfail --iofail of OutputLaw, KargerMinCut, KargerStein, Mul, Arithmetic, Bank, BankArithmetic, FusionTree Compress, Adapt, CallableFixedPrime.Exec and the tests WordRAMKargerMinCut, WordRAMKargerStein, WordRAMMultiword. scripts/check.sh --quick passed (73 affected targets, lint, hygiene, ratchets, mk_all). Single-file elaboration (warm lake env lean, min, before → after): OutputLaw 5.3 → 5.2 s, KargerMinCut 10.9 → 8.3 s, KargerStein 40.7 → 32.2 s, Mul 18.3 → 18.0 s, Arithmetic 5.6 → 4.6 s, Adapt 5.4 → 4.6 s. CI does the full run.

Manuals: manual/.../probabilistic-workflows.md cites OutputLaw only for program_of_law, and neither manual describes these proofs, so neither needs an edit.

AI assistance: prepared by AI agents (Jetski). Not reviewed by a human.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head 671b925cd41ef8da51a0fe34218fdaefcc195403. This is agent review, not human review.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) of head 671b925cd41ef8da51a0fe34218fdaefcc195403: APPROVE.

Verified:

• Cslib.Algorithms.WordRAM.Karger.minRunsLoop_law (Algorithms/WordRAM/Karger/OutputLaw.lean) cleanly separates the per-trial body bound T from the charged loop budget S (T + 2 ≤ S), accommodating both exact step accounting in KargerMinCut.ampLoop_law and slack upper bounds in KargerStein.fastCutAmpLoop_law without changing either caller's public theorem statement. Its public import of Lean.Karger.Contraction adds zero transitive fan-out since KargerMinCut and KargerStein are the sole importers and already import it via Karger.Contract.
• Exposing Schoolbook.exec_clear (Multiword/Mul.lean) removes the duplicate 27-line Arithmetic.exec_clear_framed (Multiword/Arithmetic.lean) and aligns Mul.exec_row's frame composition with Sub.exec_digits via frame_trans/frame_mono.
• exec_copyStep (ExactTriangle/CallableFixedPrime/Adapt.lean) soundly discharges all four exec_copy preconditions and register/memory frames across all three edge-list copies (ab, bc, ac).
• All four "left as is" notes in the PR description were checked against source and are genuine structural differences rather than missed extractions. Local check_hygiene.py --check-simp, check_projection_chains.py, check_encoding_readability.py, and check_operator_manual.py all pass.

Non-blocking nit: Schoolbook.exec_clear's docstring says "changing only them and the carry workspace", whereas Workspace.Frame permits both total and carry to vary. Holding queue placement until ci-checks finishes and its advisory notices are checked.

This is agent review, not human review.