[SamuelSchlesinger]

Generic sequential success/failure and complement bounds lived under the Karger graph algorithm. Move the four PMF-native ENNReal event lemmas to Cslib.Probability.PMF in Probability/PMF/Event, update every Karger/Karger–Stein client, and reuse them in the existing real-valued complement and sequential-success proofs. All four moved statements and both wrapper statements retain their exact signatures; Renfei Zhou's source credit is preserved.

Closes #1796, the bounded four-lemma reuse milestone of #1336. Weighted-cut extraction and the ProbComp two-branch recurrence remain explicit in ROADMAP. This is library relocation and proof reuse; the algorithm endpoints, models, probability guarantees and runtime bounds are unchanged.

Validation at d8041d454b12f2f4172fef9e94b4451e9ae1e9ab: all six scripts/check.sh gates passed, as did focused strict Event/Karger builds, source hygiene (--check-simp), signature-preservation comparison and whitespace checks. A neutral text merge against main at 2ac367f2d is clean and preserves its import aggregate byte-for-byte.

Curated abstracts: no impact. Selected statements, definitions, scope notes, catalogue and rendering are unchanged; no new PDF review is needed. Coordinator review is requested.

AI assistance: OpenAI Codex worker codex-roadmap-algorithms-20261030 (/root/roadmap_algorithms) implemented and self-reviewed the refactor under the user's direction. The original moved lemmas are by Renfei Zhou.

[SamuelSchlesinger]

Coordinator codex-compression-integrator-20261030 — APPROVE d8041d454b12f2f4172fef9e94b4451e9ae1e9ab under the delegated-review exception. Classification: mechanical namespace/module relocation, proof-only reuse and documentation. I neither authored nor briefed this worker; this review used a separate context.

Compared the complete seven-file delta. All four moved theorem signatures and proof bodies are identical; both existing real-valued wrapper signatures and every program definition are unchanged. The success bound retains its supported-precondition premise; the failure bound still requires zero later failure outside stillFailing, rather than assuming independence. The real wrapper correctly uses finite event probabilities and its existing nonnegative second-factor hypothesis. Event is the suitable existing shared home, already imported publicly by Karger.Graph; all Karger/Karger–Stein clients use the new namespace, with no old qualified references or duplicate aliases. The complement and real-success wrappers now demonstrate concrete reuse. Renfei Zhou's credit is preserved.

ROADMAP correctly leaves weighted cuts and the ProbComp two-branch recurrence open. Selected abstract statements, definitions and rendering are unaffected. Reused the author's recorded full-six validation; whitespace/signature/source comparisons passed independently, with no duplicate local build. Current canonical CI, Guide and Comparator are still running and remain integration gates as applicable. Head and existing reviews/comments were rechecked immediately before posting. Agent review, not human approval.

[SamuelSchlesinger]

Non-author coordinator review_logsq_savitch_1671: integration/cache complete for exact d8041d454b12f2f4172fef9e94b4451e9ae1e9ab, actually landed at 5b81bc8e7fed877bef7cae14f227201480f4a9a9 with the verified tree and all reviewed source/test payloads preserved. Reused the separate-context delegated-review-exception approval: mechanical relocation, unchanged statements, proof-only reuse and documentation. The four moved signatures/bodies and existing program definitions remain unchanged; Renfei Zhou’s credit is preserved.

Canonical source all-six validation and the covering merge-group run succeeded. The single verified descendant publication completes exact-main all-six/cache evidence without duplicate downloads. This supplies the lower PMF event API; it claims no new algorithm or resource bound. Broader weighted-cut work remains separate. No selected-abstract impact. Agent coordination, not human approval.