Repository navigation
refactor(probability): share Karger event-composition bounds #1796
Description
The generic ℝ≥0∞ sequential success/failure and complement bounds currently live in Algorithms/WordRAM/Karger/Graph.lean. Move them to Probability/PMF/Event.lean, so probability clients can use them without importing a graph algorithm. This is the event-bound milestone of the remaining reuse work in #1336; weighted-cut extraction stays open there.
Acceptance criteria:
- Move
toOuterMeasure_bind_ge_mul_ennreal,toOuterMeasure_bind_le_mul_ennreal,toOuterMeasure_add_compl_ennreal, andtoOuterMeasure_compl_le_one_subto the sharedCslib.Probability.PMFnamespace without changing their mathematical statements. Update every repository client; no deprecated aliases are needed under the current compatibility policy. - Reuse the common
ENNRealcomplement identity intoOuterMeasure_toReal_add_compland assess reuse of the sequential lower bound by the real-valued wrapper. Preserve Renfei Zhou's source credit. - Check representative shared-API clients and existing Karger/Karger–Stein clients, update the bounded ROADMAP entry, assess curated abstracts, and run the full validation sequence before opening the PR.
Worker/session: codex-roadmap-algorithms-20261030 (/root/roadmap_algorithms), branch worker/pmf-event-bounds-20261030, private Extra-drive lane algorithms (provisioning). This is a relocation/reuse milestone, with no new algorithm or runtime claim. Existing Word-RAM resource bounds retain their current models and scope.
AI assistance: OpenAI Codex prepared this milestone under the user's parallel-roadmap instruction.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
active— workercodex-roadmap-algorithms-20261030(/root/roadmap_algorithms) claims this bounded milestone onworker/pmf-event-bounds-20261030. The private Extra-drivealgorithmscheckout is being provisioned; implementation starts only after its readiness notice. Scope and acceptance criteria are above. I checked #1336's explicit release and searched existing issues/PRs for overlapping event-bound work. Next: migrate the four lemmas, simplify their existing real-valued client, and validate the algorithm clients and full tree.SamuelSchlesinger commentedon Oct 30, 2026
Scope clarification from the clean source at
7e32b150: #1336's ROADMAP entry also includestwo_branch_hit_prob_ge. #1796 covers exactly the four PMF-native lemmas listed in this issue. The two-branch recurrence remains open alongside weighted-cut extraction: its present statement is overProbComp, with evaluation/support dependencies and an arithmetic recurrence, so moving it unchanged into the shared PMF event layer would invert that dependency. The implementation will keep these remaining gaps explicit in ROADMAP.SamuelSchlesinger commentedon Oct 30, 2026
awaiting review— workercodex-roadmap-algorithms-20261030(/root/roadmap_algorithms) submitted #1808 atd8041d454. The four-lemma relocation and real-valued proof reuse are complete, all six local validation gates pass, and coordinator review is requested. The PR owns the final change, validation and no-impact abstract assessment; #1336 retains weighted-cut extraction and theProbComptwo-branch recurrence.refactor(probability): share Karger event-composition bounds (cslib-c…
refactor(probabilistic): share the sequential two-branch success rule (…