Repository navigation
refactor(probabilistic): share the sequential two-branch success rule #1812
Description
The generic two_branch_hit_prob_ge theorem currently lives in Algorithms/WordRAM/Karger/FastCut.lean, although its statement concerns arbitrary ProbComp programs. Extract it into a small Languages/Probabilistic/Event.lean module above the program semantics and PMF event layers. This is the remaining two-branch reuse milestone of #1336, depending on the four PMF lemmas in #1808; weighted-cut extraction stays open there.
Acceptance criteria:
- Preserve the exact mathematical statement of
two_branch_hit_prob_geinCslib.ProbComp, retain Renfei Zhou's source credit, migrate the Karger–Stein client, and remove the old declaration without aliases. - Keep the single-use arithmetic recurrence private beside its proof, reuse Mathlib's existing arithmetic API, and avoid a dependency from the PMF layer back to probabilistic programs. Add no algorithm or runtime claim.
- Check a concrete sequential coin experiment and an absorbing-success boundary case using only the shared program event module, update the import aggregate and bounded ROADMAP item, assess selected abstracts, and pass the full validation sequence.
Worker/session: codex-roadmap-algorithms-20261030 (/root/roadmap_algorithms), private Extra-drive algorithms lane, branch worker/probcomp-event-bounds-20261030 stacked on #1808. #1808 remains preserved and receives review fixes first. This is relocation, privatization of proof plumbing, and client reuse; public mathematical meanings remain unchanged.
AI assistance: OpenAI Codex drafted this milestone under the user's roadmap instruction.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
active— workercodex-roadmap-algorithms-20261030(/root/roadmap_algorithms) claims this bounded milestone onworker/probcomp-event-bounds-20261030, in the existing private Extra-drive algorithms lane. Searches found no competing issue/PR beyond #1336/#1796; #1336's owner explicitly released its remaining reuse work. Next: move the existing program-level rule, check concrete shared-API clients, and validate. #1808's published branch and checked source remain preserved; any review findings there take priority.SamuelSchlesinger commentedon Oct 30, 2026
awaiting review— workercodex-roadmap-algorithms-20261030(/root/roadmap_algorithms) submitted #1825 atbfd8bd411, stacked on approved #1808. All six local validation gates pass on the exact source, including the adaptive coin and certain-success regression clients. The PR owns validation, source preservation and the no-impact abstract assessment. Coordinator review is requested; #1336 retains weighted-cut extraction.SamuelSchlesinger commentedon Oct 30, 2026
awaiting integration— workercodex-roadmap-algorithms-20261030hands #1825 to the coordinating review/merge queue. Independent agent approval covers the exact published revision under the delegated-review exception. Canonical integration checks and the #1808 dependency remain with the coordinator; this issue stays open until merge.refactor(probabilistic): share the sequential two-branch success rule (…