refactor(probabilistic): share the sequential two-branch success rule

Complexity.lean

@@ -2805,6 +2805,7 @@ public import Complexity.Languages.Probabilistic.BitString
 public import Complexity.Languages.Probabilistic.BoundedUniform
 public import Complexity.Languages.Probabilistic.CenteredBinomial
 public import Complexity.Languages.Probabilistic.Concentration
+public import Complexity.Languages.Probabilistic.Event
 public import Complexity.Languages.Probabilistic.Expect
 public import Complexity.Languages.Probabilistic.Forking
 public import Complexity.Languages.Probabilistic.Iteration

Complexity/Algorithms/WordRAM/Karger/FastCut.lean

@@ -69,13 +69,11 @@ minimum-cut-value part of Theorem 4.4; paraphrase) on the randomized word RAM.
 * `Cslib.Algorithms.WordRAM.Karger.fastCutScratch_le`: total root-to-leaf stack workspace bound
   `fastCutScratch n ≤ 26 * (n * n)` for `n ≥ 2` (`[KargerStein1996]`, Section 4, Lemma 4.2;
   paraphrase).
-* `Cslib.Algorithms.WordRAM.Karger.two_branch_hit_prob_ge`,
-  `Cslib.Algorithms.WordRAM.Karger.root_hit_prob_eq`,
-  `Cslib.Algorithms.WordRAM.Karger.fastCutHighProb_failure_le`: elementary `ENNReal` probability
-  recurrence `1 - (1 - 1 / s) ^ 2 ≥ 2 / (s + 1)` giving `≥ 1 / (Nat.log 2 n + 15)` single-tree
-  success (`[KargerStein1996]`, Section 4, Lemma 4.3; paraphrase) and `≤ 1 / (2 * n)` amplified
-  failure (the minimum-cut-value part of `[KargerStein1996]`, Section 4, Theorem 4.4; paraphrase)
-  without `Real.log` or `Real.exp`.
+* `Cslib.Algorithms.WordRAM.Karger.root_hit_prob_eq`: normalize the root-depth success bound to
+  `1 / (Nat.log 2 n + 15)` (`[KargerStein1996]`, Section 4, Lemma 4.3; paraphrase).
+* `Cslib.Algorithms.WordRAM.Karger.fastCutHighProb_failure_le`: amplified failure bound
+  `≤ 1 / (2 * n)` (the minimum-cut-value part of `[KargerStein1996]`, Section 4, Theorem 4.4;
+  paraphrase), without `Real.log` or `Real.exp`.
 
 ## References
 
@@ -589,92 +587,6 @@ private theorem one_sub_inv_nat {s : ℕ} (hs : 1 ≤ s) :
     exact_mod_cast Nat.sub_add_cancel hs
   rw [hsub, ← div_eq_mul_inv, ENNReal.div_self hs0 hst]
 
-/-- Elementary recurrence `2 / (s + 1) ≤ 1 - (1 - 1 / s) ^ 2` in `ℝ≥0∞` for `1 ≤ s`, derived from
-`(2 * s - 1) * (s + 1) = 2 * s ^ 2 + s - 1 ≥ 2 * s ^ 2`. -/
-theorem one_sub_sq_one_sub_inv_ge {s : ℕ} (hs : 1 ≤ s) :
-    (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤ 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by
-  rw [one_sub_inv_nat hs]
-  have hs0 : (s : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : s ≠ 0)
-  have hst : (s : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top s
-  have hs20 : ((s * s : ℕ) : ℝ≥0∞) ≠ 0 := by exact_mod_cast (Nat.mul_pos hs hs).ne'
-  have hs2t : ((s * s : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _
-  have hsp10 : ((s + 1 : ℕ) : ℝ≥0∞) ≠ 0 := by positivity
-  have hsp1t : ((s + 1 : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _
-  have hsq_eq : (((s - 1 : ℕ) : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 =
-      (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by
-    simp only [sq, div_eq_mul_inv, Nat.cast_mul, ENNReal.mul_inv (Or.inl hs0) (Or.inl hst)]
-    ring
-  rw [hsq_eq]
-  have hsub_eq : (1 : ℝ≥0∞) - (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) =
-      ((2 * s - 1 : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by
-    refine ENNReal.sub_eq_of_eq_add
-      (ENNReal.div_ne_top (ENNReal.natCast_ne_top _) hs20) ?_
-    rw [div_eq_mul_inv, div_eq_mul_inv, ← add_mul]
-    have hsum : (2 * s - 1) + (s - 1) * (s - 1) = s * s := by
-      obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩
-      have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega
-      have h2 : d + 1 - 1 = d := by omega
-      rw [h1, h2]
-      ring
-    have hcast : ((2 * s - 1 : ℕ) : ℝ≥0∞) + (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) =
-        ((s * s : ℕ) : ℝ≥0∞) := by exact_mod_cast hsum
-    rw [hcast, ← div_eq_mul_inv, ENNReal.div_self hs20 hs2t]
-  rw [hsub_eq]
-  rw [ENNReal.div_le_iff_le_mul (Or.inl hsp10) (Or.inl hsp1t)]
-  rw [← ENNReal.mul_div_right_comm]
-  rw [ENNReal.le_div_iff_mul_le (Or.inl hs20) (Or.inl hs2t)]
-  have hnat : 2 * (s * s) ≤ (2 * s - 1) * (s + 1) := by
-    obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩
-    have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega
-    rw [h1]
-    nlinarith
-  exact_mod_cast hnat
-
-/-- Sequential two-branch success probability recurrence on `ProbComp`: if Branch 1 hits `hit₁`
-with probability `≥ 1 / s`, any outcome in `hit₁` guarantees `f a b ∈ hit` on every supported `b`,
-and conditioned on any outcome outside `hit₁` Branch 2 achieves `f a b ∈ hit` with probability
-`≥ 1 / s`, then the combined computation hits `hit` with probability `≥ 2 / (s + 1)`. -/
-theorem two_branch_hit_prob_ge {α β γ : Type} (m₁ : ProbComp α) (m₂ : α → ProbComp β)
-    (f : α → β → γ) (hit₁ : Set α) (hit : Set γ) {s : ℕ} (hs : 1 ≤ s)
-    (hb₁ : (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ m₁.eval.toOuterMeasure hit₁)
-    (hprop₁ : ∀ a ∈ m₁.support, a ∈ hit₁ → ∀ b ∈ (m₂ a).support, f a b ∈ hit)
-    (hb₂ : ∀ a ∈ m₁.support, a ∉ hit₁ →
-      (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ ((m₂ a).eval.map (f a)).toOuterMeasure hit) :
-    (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤
-      (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval.toOuterMeasure hit := by
-  let p := (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval
-  have hp_eq : p = m₁.eval.bind (fun a => (m₂ a).eval.map (f a)) := by
-    dsimp only [p]
-    rw [ProbComp.eval_bind]
-    refine congrArg (m₁.eval.bind ·) (funext fun a => ?_)
-    rw [bind_pure_comp, ProbComp.eval_map]
-  have hcompl_le : p.toOuterMeasure hitᶜ ≤ (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by
-    rw [hp_eq, sq]
-    refine toOuterMeasure_bind_le_mul_ennreal m₁.eval (fun a => (m₂ a).eval.map (f a))
-      hit₁ᶜ hitᶜ (toOuterMeasure_compl_le_one_sub m₁.eval hit₁ hb₁) ?_ ?_
-    · intro a ha_eval ha_miss
-      have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval
-      exact toOuterMeasure_compl_le_one_sub _ hit (hb₂ a ha ha_miss)
-    · intro a ha_eval ha_not_miss
-      have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval
-      have ha_hit : a ∈ hit₁ := not_not.mp ha_not_miss
-      rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply]
-      refine tsum_eq_zero_iff.mpr fun b => ?_
-      by_cases hb_eval : b ∈ (m₂ a).eval.support
-      · have hb : b ∈ (m₂ a).support := (ProbComp.support_eval (m₂ a)) ▸ hb_eval
-        have hmem : f a b ∈ hit := hprop₁ a ha ha_hit b hb
-        have hnot : b ∉ (f a ⁻¹' hitᶜ) := fun hc => hc hmem
-        exact Set.indicator_of_notMem hnot _
-      · have hp0 : (m₂ a).eval b = 0 := by simpa only [PMF.mem_support_iff, not_not] using hb_eval
-        simp [hp0]
-  have hsum := toOuterMeasure_add_compl_ennreal p hit
-  have hhit_ge : 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 ≤ p.toOuterMeasure hit := by
-    refine tsub_le_iff_right.mpr ?_
-    calc
-      (1 : ℝ≥0∞) = p.toOuterMeasure hit + p.toOuterMeasure hitᶜ := hsum.symm
-      _ ≤ p.toOuterMeasure hit + (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by gcongr
-  exact (one_sub_sq_one_sub_inv_ge hs).trans hhit_ge
-
 /-- At the root depth budget `d = 2 * Nat.log 2 n`, `2 / (d + 30) = 1 / (Nat.log 2 n + 15)`. -/
 theorem root_hit_prob_eq (n : ℕ) :
     (2 : ℝ≥0∞) / ((2 * Nat.log 2 n + 30 : ℕ) : ℝ≥0∞) =

Complexity/Algorithms/WordRAM/KargerStein.lean

@@ -14,6 +14,7 @@ public import Complexity.Algorithms.WordRAM.Karger.FastCut
 public import Complexity.Computability.WordRAM.Copy
 public import Complexity.Computability.WordRAM.Randomized.LoopSegment
 public import Complexity.Computability.WordRAM.Time
+import Complexity.Languages.Probabilistic.Event
 
 /-!
 # Karger–Stein's recursive `FastCut` algorithm on the word RAM
@@ -2725,7 +2726,7 @@ theorem fastCutNode_spec {n w : ℕ} {W₀ : Fin n → Fin n → ℕ}
         dsimp only [t] at ht₁ ht₂
         omega
       · intro B hmin_pos hB_nt hB_min
-        have hrec := two_branch_hit_prob_ge m_b1 (fun z₁ => m₂_fn z₁.1)
+        have hrec := ProbComp.two_branch_hit_prob_ge m_b1 (fun z₁ => m₂_fn z₁.1)
           (fun z₁ z₂ => (z₂.1, z₁.2 + z₂.2))
           {z₁ | z₁.1.regs retVal = minCut W₀}
           {z | z.1.regs retVal = minCut W₀}

Complexity/Languages/Probabilistic/Event.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2026 Renfei Zhou, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Renfei Zhou, Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Languages.Probabilistic.Semantics
+import Complexity.Probability.PMF.Event
+
+/-!
+# Sequential success bounds for probabilistic programs
+
+A first program can establish success, and a second program can recover when the first fails.
+If each branch succeeds with probability at least `1 / s` on the inputs that need it, and later
+execution retains every first-branch success, the sequence succeeds with probability at least
+`2 / (s + 1)`. The second program may depend on the first result. Hypotheses apply only to
+possible outcomes, and no independence or finite output-type hypothesis is needed.
+
+These are bounds on the distributions denoted by terminating `ProbComp` programs. Runtime and
+oracle-query costs require separate certificates.
+
+## Main results
+
+* `Cslib.ProbComp.two_branch_hit_prob_ge`: retained first-branch success and conditional recovery
+  give the two-branch success bound.
+
+## References
+
+The generic success rule is from Renfei Zhou's Karger–Stein development.
+-/
+
+@[expose] public section
+
+namespace Cslib.ProbComp
+
+open scoped ENNReal
+open Cslib.Probability.PMF
+
+/-- Elementary recurrence `2 / (s + 1) ≤ 1 - (1 - 1 / s) ^ 2` in `ℝ≥0∞` for `1 ≤ s`, derived from
+`(2 * s - 1) * (s + 1) = 2 * s ^ 2 + s - 1 ≥ 2 * s ^ 2`. -/
+private theorem one_sub_sq_one_sub_inv_ge {s : ℕ} (hs : 1 ≤ s) :
+    (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤ 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by
+  have hs0 : (s : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : s ≠ 0)
+  have hst : (s : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top s
+  have hsub : (1 : ℝ≥0∞) - 1 / (s : ℝ≥0∞) =
+      ((s - 1 : ℕ) : ℝ≥0∞) / (s : ℝ≥0∞) := by
+    rw [ENNReal.natCast_sub, Nat.cast_one, ENNReal.sub_div (fun _ _ => hs0),
+      ENNReal.div_self hs0 hst]
+  rw [hsub]
+  have hs20 : ((s * s : ℕ) : ℝ≥0∞) ≠ 0 := by exact_mod_cast (Nat.mul_pos hs hs).ne'
+  have hs2t : ((s * s : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _
+  have hsp10 : ((s + 1 : ℕ) : ℝ≥0∞) ≠ 0 := by positivity
+  have hsp1t : ((s + 1 : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _
+  have hsq_eq : (((s - 1 : ℕ) : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 =
+      (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by
+    simp only [sq, div_eq_mul_inv, Nat.cast_mul, ENNReal.mul_inv (Or.inl hs0) (Or.inl hst)]
+    ring
+  rw [hsq_eq]
+  have hsub_eq : (1 : ℝ≥0∞) - (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) =
+      ((2 * s - 1 : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by
+    refine ENNReal.sub_eq_of_eq_add
+      (ENNReal.div_ne_top (ENNReal.natCast_ne_top _) hs20) ?_
+    rw [div_eq_mul_inv, div_eq_mul_inv, ← add_mul]
+    have hsum : (2 * s - 1) + (s - 1) * (s - 1) = s * s := by
+      obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩
+      have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega
+      have h2 : d + 1 - 1 = d := by omega
+      rw [h1, h2]
+      ring
+    have hcast : ((2 * s - 1 : ℕ) : ℝ≥0∞) + (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) =
+        ((s * s : ℕ) : ℝ≥0∞) := by exact_mod_cast hsum
+    rw [hcast, ← div_eq_mul_inv, ENNReal.div_self hs20 hs2t]
+  rw [hsub_eq]
+  rw [ENNReal.div_le_iff_le_mul (Or.inl hsp10) (Or.inl hsp1t)]
+  rw [← ENNReal.mul_div_right_comm]
+  rw [ENNReal.le_div_iff_mul_le (Or.inl hs20) (Or.inl hs2t)]
+  have hnat : 2 * (s * s) ≤ (2 * s - 1) * (s + 1) := by
+    obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩
+    have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega
+    rw [h1]
+    nlinarith
+  exact_mod_cast hnat
+
+/-- Sequential two-branch success probability recurrence on `ProbComp`: if Branch 1 hits `hit₁`
+with probability `≥ 1 / s`, any outcome in `hit₁` guarantees `f a b ∈ hit` on every supported `b`,
+and conditioned on any outcome outside `hit₁` Branch 2 achieves `f a b ∈ hit` with probability
+`≥ 1 / s`, then the combined computation hits `hit` with probability `≥ 2 / (s + 1)`. -/
+theorem two_branch_hit_prob_ge {α β γ : Type} (m₁ : ProbComp α) (m₂ : α → ProbComp β)
+    (f : α → β → γ) (hit₁ : Set α) (hit : Set γ) {s : ℕ} (hs : 1 ≤ s)
+    (hb₁ : (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ m₁.eval.toOuterMeasure hit₁)
+    (hprop₁ : ∀ a ∈ m₁.support, a ∈ hit₁ → ∀ b ∈ (m₂ a).support, f a b ∈ hit)
+    (hb₂ : ∀ a ∈ m₁.support, a ∉ hit₁ →
+      (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ ((m₂ a).eval.map (f a)).toOuterMeasure hit) :
+    (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤
+      (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval.toOuterMeasure hit := by
+  let p := (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval
+  have hp_eq : p = m₁.eval.bind (fun a => (m₂ a).eval.map (f a)) := by
+    dsimp only [p]
+    rw [ProbComp.eval_bind]
+    refine congrArg (m₁.eval.bind ·) (funext fun a => ?_)
+    rw [bind_pure_comp, ProbComp.eval_map]
+  have hcompl_le : p.toOuterMeasure hitᶜ ≤ (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by
+    rw [hp_eq, sq]
+    refine toOuterMeasure_bind_le_mul_ennreal m₁.eval (fun a => (m₂ a).eval.map (f a))
+      hit₁ᶜ hitᶜ (toOuterMeasure_compl_le_one_sub m₁.eval hit₁ hb₁) ?_ ?_
+    · intro a ha_eval ha_miss
+      have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval
+      exact toOuterMeasure_compl_le_one_sub _ hit (hb₂ a ha ha_miss)
+    · intro a ha_eval ha_not_miss
+      have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval
+      have ha_hit : a ∈ hit₁ := not_not.mp ha_not_miss
+      rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply]
+      refine tsum_eq_zero_iff.mpr fun b => ?_
+      by_cases hb_eval : b ∈ (m₂ a).eval.support
+      · have hb : b ∈ (m₂ a).support := (ProbComp.support_eval (m₂ a)) ▸ hb_eval
+        have hmem : f a b ∈ hit := hprop₁ a ha ha_hit b hb
+        have hnot : b ∉ (f a ⁻¹' hitᶜ) := fun hc => hc hmem
+        exact Set.indicator_of_notMem hnot _
+      · have hp0 : (m₂ a).eval b = 0 := by simpa only [PMF.mem_support_iff, not_not] using hb_eval
+        simp [hp0]
+  have hsum := toOuterMeasure_add_compl_ennreal p hit
+  have hhit_ge : 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 ≤ p.toOuterMeasure hit := by
+    refine tsub_le_iff_right.mpr ?_
+    calc
+      (1 : ℝ≥0∞) = p.toOuterMeasure hit + p.toOuterMeasure hitᶜ := hsum.symm
+      _ ≤ p.toOuterMeasure hit + (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by gcongr
+  exact (one_sub_sq_one_sub_inv_ge hs).trans hhit_ge
+
+end Cslib.ProbComp

ComplexityTests/ProbCompEvent.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Languages.Probabilistic.Event
+
+/-! Shared probabilistic-program success bounds, without a graph-algorithm import. -/
+
+namespace ComplexityTests.ProbCompEvent
+
+open Cslib
+open scoped ENNReal
+
+private theorem coin_hit :
+    (1 : ℝ≥0∞) / 2 ≤ (ProbComp.uniform Bool).eval.toOuterMeasure {true} := by
+  rw [ProbComp.eval_uniform, PMF.toOuterMeasure_apply_singleton,
+    Probability.PMF.uniformOfFintype_apply]
+  norm_num
+
+-- The first success skips the second draw; a fresh coin recovers after failure. The
+-- continuation depends on the first result, and the shared bound gives at least `2 / 3`.
+example : (2 : ℝ≥0∞) / 3 ≤ (do
+    let a ← ProbComp.uniform Bool
+    let b ← (if a then pure false else ProbComp.uniform Bool)
+    pure (a || b)).eval.toOuterMeasure {true} := by
+  refine ProbComp.two_branch_hit_prob_ge (ProbComp.uniform Bool)
+    (fun a => if a then pure false else ProbComp.uniform Bool) (fun a b => a || b)
+    {true} {true}
+    (s := 2) (by decide) coin_hit ?_ ?_
+  · intro a _ ha b _
+    change a = true at ha
+    subst a
+    simp
+  · intro a _ ha
+    have hfalse : a = false := by cases a <;> simp_all
+    subst a
+    change (1 : ℝ≥0∞) / 2 ≤ ((ProbComp.uniform Bool).eval.map id).toOuterMeasure {true}
+    rw [PMF.map_id]
+    exact coin_hit
+
+-- At `s = 1`, a certain first success is retained through any later program. The later
+-- program need not succeed when given the unsupported first result `false`.
+example (later : Bool → ProbComp Bool) :
+    (1 : ℝ≥0∞) ≤ (do
+      let a ← (pure true : ProbComp Bool)
+      let b ← later a
+      pure (a || b)).eval.toOuterMeasure {true} := by
+  have h := ProbComp.two_branch_hit_prob_ge (pure true) later (fun a b => a || b)
+    {true} {true} (s := 1) (by decide) (by simp) (by
+      intro a _ ha b _
+      change a = true at ha
+      subst a
+      simp) (by
+      intro a ha hmiss
+      have ha' : a = true := OracleComp.eq_of_mem_supportWith_pure ha
+      exact False.elim (hmiss ha'))
+  have htwo : (2 : ℝ≥0∞) / 2 = 1 := ENNReal.div_self (by norm_num) (by norm_num)
+  simpa only [show ((1 + 1 : ℕ) : ℝ≥0∞) = 2 by norm_num, htwo] using h
+
+end ComplexityTests.ProbCompEvent

ROADMAP.md

@@ -757,15 +757,13 @@ reuse is demonstrated.
 
 - **One sensitivity API.** Define the sensitivity measures over any `Fintype` in CSLib and drop
   the separate measures of the sensitivity-separation development.
-- **Weighted multigraph cuts and two-branch probability recurrence** ([#1336]): extract
+- **Weighted multigraph cuts** ([#1336]): extract
   `IsMultigraph` (renamed e.g. `IsSymmLoopless` or phrased via `Matrix.IsSymm` with zero diagonal),
   `IsNonTrivialCut`,
   `cutWeight`, `minCut`, `rowDeg`, `totalDoubledWeight`, `flattenMatrix`, and `IsContractionOf` from
   `Complexity/Algorithms/WordRAM/Karger/Graph.lean` (shared by `KargerMinCut` and `KargerStein`) into
   `Complexity/Foundations/Combinatorics/WeightedCut.lean` with a bridge lemma relating `cutWeight W C`
-  to `(Cslib.Multigraph.edgeCut ends C).card`. Extract `two_branch_hit_prob_ge` from
-  `Karger/FastCut.lean` into a shared probabilistic-program module; its `ProbComp` evaluation and
-  support dependencies should stay above the `PMF` event layer.
+  to `(Cslib.Multigraph.edgeCut ends C).card`.
 - **CNF evaluation certificates:** `fun_prop` certificates for evaluating literals, clauses and
   formulas under a polynomial-time assignment, so clients stop passing `CNF.eval`,
   `Clause.eval` and `Literal.eval` to `fun_prop` as unfolding hints.