diff --git a/Complexity.lean b/Complexity.lean
index aa5d494bc..7f094c5a0 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1708,6 +1708,7 @@ public import Complexity.Languages.Probabilistic.Basic
 public import Complexity.Languages.Probabilistic.BitString
 public import Complexity.Languages.Probabilistic.CenteredBinomial
 public import Complexity.Languages.Probabilistic.Concentration
+public import Complexity.Languages.Probabilistic.Forking
 public import Complexity.Languages.Probabilistic.Iteration
 public import Complexity.Languages.Probabilistic.LinearHash
 public import Complexity.Languages.Probabilistic.Memoize
@@ -1849,6 +1850,7 @@ public import Complexity.Probability.Divergence
 public import Complexity.Probability.Entropy
 public import Complexity.Probability.EntropyConcentration
 public import Complexity.Probability.EntropyExtraction
+public import Complexity.Probability.Forking
 public import Complexity.Probability.Guessing
 public import Complexity.Probability.HashIsolation
 public import Complexity.Probability.IID
diff --git a/Complexity/Languages/Probabilistic/Forking.lean b/Complexity/Languages/Probabilistic/Forking.lean
new file mode 100644
index 000000000..bab38b63c
--- /dev/null
+++ b/Complexity/Languages/Probabilistic/Forking.lean
@@ -0,0 +1,351 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Languages.Probabilistic.Oracle.Transcript
+public import Complexity.Probability.Forking
+import Complexity.Languages.Probabilistic.Presample
+import Complexity.Languages.Probabilistic.Repeat
+import Complexity.Probability.PMF
+import Complexity.Probability.Product
+
+/-!
+# Forking oracle programs
+
+An oracle program `P s : OracleComp (fun _ : Query => H) (Option ℕ × β)`, with explicit coins
+`s`, asks queries whose answers lie in a finite set `H` and finally names one of its queries by
+its position, or none. A name counts only if the program actually asked a query at that position
+(`validIndex`). Forking runs the program with uniform answers and, if it validly names position
+`j`, runs it again on the same coins with the same answers before `j` and fresh answers from `j`
+on; it succeeds when the rerun validly names `j` too and the answers at `j` differ. Both runs then
+ask the same first `j + 1` queries, so the named query exists in both and is the same, while its
+two answers differ (`mem_support_fork`).
+
+`runWithAnswers` runs a program on a list of answers, deterministically, recording its queries.
+Answering queries from `q` presampled uniform answers has the law of answering them uniformly as
+they come, when the program asks at most `q` queries: this is the presampling theorem
+`ProbOracleComp.HasQueryBounds.eval_presample` (`interpret_uniform_eq`, and
+`run_interpret_countingUniform_eq` when the queries are also counted). Hence the general forking
+lemma (`Probability.Forking.le_add_sqrt_fork`) bounds the probability that the program, with
+uniform answers, validly names a query by `q / |H| + √(q · frk)` (`le_add_sqrt_fork`).
+
+The coins are explicit: the second run replays them. A program with private randomness is put in
+this form by drawing its coins in advance. The statements are exact; no efficiency is involved.
+
+## Main definitions
+
+* `Cslib.OracleComp.runWithAnswers`: run on a list of answers, recording the queries.
+* `Cslib.OracleComp.validIndex`: the named position, if it is below `q` and was queried.
+* `Cslib.OracleComp.countingUniform`: uniform answers as queries come, counting them.
+* `Cslib.OracleComp.forkingAlgorithm`: a program on coins and an answer vector, for forking.
+
+## Main results
+
+* `Cslib.OracleComp.interpret_uniform_eq`, `Cslib.OracleComp.run_interpret_countingUniform_eq`:
+  uniform answers as they come, or presampled.
+* `Cslib.OracleComp.le_add_sqrt_fork`: the forking lemma for oracle programs.
+* `Cslib.OracleComp.mem_support_fork`: both runs of a successful fork ask the same queries up to
+  the named one, and answer it differently.
+* `Cslib.OracleComp.take_runWithAnswers`: a program's first `n + 1` queries depend only on its
+  first `n` answers.
+
+## References
+
+* [M. Bellare, G. Neven, *Multi-Signatures in the Plain Public-Key Model and a General Forking
+  Lemma*][BellareNeven2006], Lemma 1.
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Lemma 19.8.
+-/
+
+@[expose] public section
+
+namespace Cslib.OracleComp
+
+open Probability
+
+variable {Query H α : Type}
+
+/-- Run a program on a list of answers, in order, answering `default` once the list is exhausted;
+return its result and its queries, in order. -/
+def runWithAnswers (default : H) : OracleComp (fun _ : Query => H) α → List H → α × List Query
+  | .pure a, _ => (a, [])
+  | .liftBind q cont, answers =>
+    ((runWithAnswers default (cont (answers.headD default)) answers.tail).1,
+      q :: (runWithAnswers default (cont (answers.headD default)) answers.tail).2)
+
+/-- Returning a value asks no query. -/
+@[simp] theorem runWithAnswers_pure (default : H) (a : α) (answers : List H) :
+    runWithAnswers default (pure a : OracleComp (fun _ : Query => H) α) answers = (a, []) := rfl
+
+/-- A query is answered by the head of the list, and the rest goes to the continuation. -/
+@[simp] theorem runWithAnswers_query_bind (default : H) (q : Query)
+    (cont : H → OracleComp (fun _ : Query => H) α) (answers : List H) :
+    runWithAnswers default (OracleComp.query (spec := fun _ : Query => H) q >>= cont) answers =
+      ((runWithAnswers default (cont (answers.headD default)) answers.tail).1,
+        q :: (runWithAnswers default (cont (answers.headD default)) answers.tail).2) := rfl
+
+/-- A mapped query is answered by the head of the list. -/
+@[simp] theorem runWithAnswers_map_query (default : H) (f : H → α) (q : Query)
+    (answers : List H) :
+    runWithAnswers default (f <$> OracleComp.query (spec := fun _ : Query => H) q) answers =
+      (f (answers.headD default), [q]) := rfl
+
+/-- A program's first `n + 1` queries depend only on the first `n` answers. -/
+theorem take_runWithAnswers (default : H) (program : OracleComp (fun _ : Query => H) α) :
+    ∀ {answers answers' : List H} {n : ℕ}, answers.take n = answers'.take n →
+      (runWithAnswers default program answers).2.take (n + 1) =
+        (runWithAnswers default program answers').2.take (n + 1) := by
+  induction program with
+  | pure a => intros; rfl
+  | liftBind q cont ih =>
+    intro answers answers' n h
+    cases n with
+    | zero => rfl
+    | succ n =>
+      have hsplit : answers.headD default = answers'.headD default ∧
+          answers.tail.take n = answers'.tail.take n := by
+        cases answers <;> cases answers' <;> simp_all
+      simp only [runWithAnswers, List.take_succ_cons, hsplit.1, ih _ hsplit.2]
+
+/-! ### Presampled answers -/
+
+/-- Answering the lifted program from a saved list is running it on that list. -/
+private theorem eval_run_withSampleList (default : H)
+    (program : OracleComp (fun _ : Query => H) α) (answers : List H) :
+    ProbComp.eval ((fun (result, next, _) => (result, next)) <$>
+      (interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n))
+        (withSampleList default fun v _ s => (pure (v, s) : ProbComp (H × Unit))))
+          (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q)
+            program)).run ((), answers)) =
+      PMF.pure ((runWithAnswers default program answers).1, ()) := by
+  induction program generalizing answers with
+  | pure a => rfl
+  | liftBind q cont ih =>
+    change _ = PMF.pure ((runWithAnswers default (cont (answers.headD default)) answers.tail).1, ())
+    rw [← ih (answers.headD default) answers.tail]
+    rfl
+
+/-- Answering lifted queries uniformly as they come is answering them uniformly. -/
+private theorem eval_run_uniform [Fintype H] [Nonempty H]
+    (program : OracleComp (fun _ : Query => H) α) :
+    ProbComp.eval ((interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n))
+        (fun _ s => do
+          let value ← ProbComp.uniform H
+          (pure (value, s) : ProbComp (H × Unit))))
+          (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q)
+            program)).run ()) =
+      (interpret (fun _ => PMF.uniformOfFintype H) program).map (·, ()) := by
+  have hstate : (fun (_ : Query) (s : Unit) => do
+      let value ← ProbComp.uniform H
+      (pure (value, s) : ProbComp (H × Unit))) =
+      fun _ s => (fun a => (a, s)) <$> ProbComp.uniform H := by
+    funext _ s
+    rw [map_eq_bind_pure_comp]
+    rfl
+  have heval : ProbComp.eval (interpret (fun _ => ProbComp.uniform H) program) =
+      interpret (fun _ => PMF.uniformOfFintype H) program := by
+    change interpret ProbComp.unifOracle (interpret _ program) = _
+    rw [interpret_interpret]
+    congr 1
+    funext q
+    exact ProbComp.eval_uniform H
+  rw [interpret_interpret]
+  simp only [ProbOracleComp.interpret_query]
+  rw [hstate, run_interpret_stateless, ProbComp.eval_map, heval]
+
+/-- `q` uniform samples, collected in a list, are the entries of a uniform vector. -/
+private theorem eval_replicate_uniform [Fintype H] [Nonempty H] (q : ℕ) :
+    ProbComp.eval (replicate q (ProbComp.uniform H)) =
+      (PMF.uniformOfFintype (Fin q → H)).map List.ofFn := by
+  induction q with
+  | zero =>
+    have hconst : (List.ofFn : (Fin 0 → H) → List H) = Function.const _ [] :=
+      funext fun _ => List.ofFn_zero
+    rw [replicate_zero, ProbComp.eval_pure, hconst, PMF.map_const]
+  | succ q ih =>
+    rw [replicate_succ, ← Probability.PMF.pi_uniformOfFintype, Probability.PMF.pi_fin_succ,
+      Probability.PMF.pi_uniformOfFintype]
+    simp only [ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_uniform, ih, PMF.map_bind,
+      PMF.map_comp, Function.comp_def, List.ofFn_succ, Fin.cons_zero, Fin.cons_succ]
+
+/-- The lazy law of uniform answers is the law of `q` presampled uniform answers, for a program
+asking at most `q` queries: an instance of the presampling theorem
+`ProbOracleComp.HasQueryBounds.eval_presample`. -/
+theorem interpret_uniform_eq [Fintype H] [Nonempty H] (default : H)
+    (program : OracleComp (fun _ : Query => H) α) {size : Query → ℕ} {q maxSize : ℕ}
+    (hq : (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q)
+      program).HasQueryBounds size q maxSize) :
+    interpret (fun _ => PMF.uniformOfFintype H) program =
+      (PMF.uniformOfFintype (Fin q → H)).map fun h =>
+        (runWithAnswers default program (List.ofFn h)).1 := by
+  have hp := hq.eval_presample (ProbComp.uniform H) default
+    (fun v _ s => (pure (v, s) : ProbComp (H × Unit))) ()
+  rw [eval_run_uniform, ProbComp.eval_bind, eval_replicate_uniform] at hp
+  simp only [eval_run_withSampleList, PMF.bind_map, Function.comp_def] at hp
+  have hfst := congrArg (PMF.map Prod.fst) hp
+  simp only [PMF.map_comp, Function.comp_def] at hfst
+  rw [show PMF.map (fun x => x) (interpret (fun _ => PMF.uniformOfFintype H) program) =
+    interpret (fun _ => PMF.uniformOfFintype H) program from PMF.map_id _] at hfst
+  rw [← hfst, PMF.map_bind]
+  simp only [PMF.pure_map]
+  rfl
+
+/-- Answer queries uniformly as they come, counting them in the state. -/
+noncomputable def countingUniform [Fintype H] [Nonempty H] (_ : Query) : StateT ℕ PMF H :=
+  fun count => (PMF.uniformOfFintype H).map (·, count + 1)
+
+/-- Answering the lifted program from a saved list, counting the calls, is running it on that
+list. -/
+private theorem eval_run_withSampleList_count (default : H)
+    (program : OracleComp (fun _ : Query => H) α) (count : ℕ) (answers : List H) :
+    ProbComp.eval ((fun (result, next, _) => (result, next)) <$>
+      (interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n))
+        (withSampleList default fun v _ n => (pure (v, n + 1) : ProbComp (H × ℕ))))
+          (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q)
+            program)).run (count, answers)) =
+      PMF.pure ((runWithAnswers default program answers).1,
+        count + (runWithAnswers default program answers).2.length) := by
+  induction program generalizing count answers with
+  | pure a => simp only [runWithAnswers, List.length_nil, add_zero]; rfl
+  | liftBind q cont ih =>
+    change _ = PMF.pure ((runWithAnswers default (cont (answers.headD default)) answers.tail).1,
+      count + ((runWithAnswers default (cont (answers.headD default)) answers.tail).2.length + 1))
+    rw [show count + ((runWithAnswers default (cont (answers.headD default)) answers.tail).2.length
+      + 1) = (count + 1) +
+        (runWithAnswers default (cont (answers.headD default)) answers.tail).2.length by omega,
+      ← ih (answers.headD default) (count + 1) answers.tail]
+    rfl
+
+/-- Answering lifted queries uniformly as they come, counting them, is `countingUniform`. -/
+private theorem eval_run_counting [Fintype H] [Nonempty H]
+    (program : OracleComp (fun _ : Query => H) α) (count : ℕ) :
+    ProbComp.eval ((interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n))
+        (fun _ n => do
+          let value ← ProbComp.uniform H
+          (pure (value, n + 1) : ProbComp (H × ℕ))))
+          (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q)
+            program)).run count) =
+      (interpret countingUniform program).run count := by
+  rw [ProbOracleComp.eval_run_interpret, interpret_interpret]
+  congr 1
+  congr 1
+  funext q n
+  simp only [ProbOracleComp.interpret_query, ProbComp.eval_bind, ProbComp.eval_uniform,
+    ProbComp.eval_pure]
+  rfl
+
+/-- Counting variant of `interpret_uniform_eq`: answering uniformly as queries come, and counting
+them, has the law of running on `q` presampled uniform answers and counting the queries made. -/
+theorem run_interpret_countingUniform_eq [Fintype H] [Nonempty H] (default : H)
+    (program : OracleComp (fun _ : Query => H) α) {size : Query → ℕ} {q maxSize : ℕ}
+    (hq : (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q)
+      program).HasQueryBounds size q maxSize) (count : ℕ) :
+    (interpret countingUniform program).run count =
+      (PMF.uniformOfFintype (Fin q → H)).map fun h =>
+        ((runWithAnswers default program (List.ofFn h)).1,
+          count + (runWithAnswers default program (List.ofFn h)).2.length) := by
+  have hp := hq.eval_presample (ProbComp.uniform H) default
+    (fun v _ n => (pure (v, n + 1) : ProbComp (H × ℕ))) count
+  rw [eval_run_counting, ProbComp.eval_bind, eval_replicate_uniform] at hp
+  simp only [eval_run_withSampleList_count, PMF.bind_map, Function.comp_def] at hp
+  rw [← hp]
+  rfl
+
+/-! ### Forking -/
+
+/-- The named position, if it is below `q` and names one of the `count` queries made. A program
+naming a position it never queried does not count as naming one. -/
+def validIndex (q count : ℕ) (position : Option ℕ) : Option (Fin q) :=
+  position.bind fun j => if h : j < q ∧ j < count then some ⟨j, h.1⟩ else none
+
+/-- A valid index is a named position below `q` and below the number of queries made. -/
+theorem validIndex_eq_some {q count : ℕ} {position : Option ℕ} {j : Fin q}
+    (h : validIndex q count position = some j) : position = some j.val ∧ j.val < count := by
+  cases position with
+  | none => simp [validIndex] at h
+  | some p =>
+    simp only [validIndex, Option.bind_some] at h
+    split_ifs at h with hp
+    simp only [Option.some.injEq] at h
+    subst h
+    exact ⟨rfl, hp.2⟩
+
+/-- A program with explicit coins as an algorithm on coins and `q` answers, for the general
+forking lemma: the validly named position, and the result with the queries. -/
+def forkingAlgorithm {S β : Type} (default : H) (q : ℕ)
+    (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (s : S) (h : Fin q → H) :
+    Option (Fin q) × ((Option ℕ × β) × List Query) :=
+  (validIndex q (runWithAnswers default (program s) (List.ofFn h)).2.length
+      (runWithAnswers default (program s) (List.ofFn h)).1.1,
+    runWithAnswers default (program s) (List.ofFn h))
+
+variable {S β : Type} [Fintype H] [Nonempty H] [DecidableEq H]
+
+/-- **The forking lemma for oracle programs** ([BellareNeven2006], Lemma 1): if a program with
+explicit coins asks at most `q` queries, and with probability `acc` names one of the queries it
+made when they are answered uniformly as they come, then forking it succeeds with probability
+`frk` such that `acc ≤ q / |H| + √(q · frk)`. -/
+theorem le_add_sqrt_fork (first : PMF S)
+    (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (default : H)
+    {size : Query → ℕ} {q maxSize : ℕ}
+    (hq : ∀ s, (interpret (fun q => ProbOracleComp.query (spec := fun _ : Query => H) q)
+      (program s)).HasQueryBounds size q maxSize) :
+    ((do
+      let s ← first
+      let run ← (interpret countingUniform (program s)).run 0
+      return (validIndex q run.2 run.1.1).isSome : PMF Bool) true).toReal ≤
+      q / Fintype.card H + √(q * ((Forking.fork first (forkingAlgorithm default q program)).map
+        Option.isSome true).toReal) := by
+  have hacc : (do
+      let s ← first
+      let run ← (interpret countingUniform (program s)).run 0
+      return (validIndex q run.2 run.1.1).isSome : PMF Bool) =
+      Forking.accept first (forkingAlgorithm default q program) := by
+    simp only [Forking.accept, forkingAlgorithm, Probability.PMF.monad_bind_eq_bind,
+      Probability.PMF.monad_pure_eq_pure]
+    refine congrArg _ (funext fun s => ?_)
+    rw [run_interpret_countingUniform_eq default (program s) (hq s), PMF.bind_map]
+    simp only [zero_add]
+    rfl
+  rw [hacc]
+  exact Forking.le_add_sqrt_fork first _
+
+/-- A successful fork of a program reruns it on the same coins with answers that agree before the
+named position `j` and differ at it. Both runs name `j`, ask the same first `j + 1` queries, and
+have actually asked a query at position `j`, the same one. -/
+theorem mem_support_fork {first : PMF S}
+    {program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)} {default : H} {q : ℕ}
+    {j : Fin q} {out out' : (Option ℕ × β) × List Query}
+    (hfork : some (j, out, out') ∈
+      (Forking.fork first (forkingAlgorithm default q program)).support) :
+    ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧
+      out = runWithAnswers default (program s) (List.ofFn h) ∧
+      out' = runWithAnswers default (program s) (List.ofFn h') ∧
+      out.1.1 = some j.val ∧ out'.1.1 = some j.val ∧
+      out.2.take (j + 1) = out'.2.take (j + 1) ∧
+      ∃ query, out.2[j.val]? = some query ∧ out'.2[j.val]? = some query := by
+  obtain ⟨s, hs, h, h', hagree, hne, hrun, hrun'⟩ := Forking.mem_support_fork hfork
+  simp only [forkingAlgorithm, Prod.mk.injEq] at hrun hrun'
+  obtain ⟨hidx, rfl⟩ := hrun
+  obtain ⟨hidx', rfl⟩ := hrun'
+  obtain ⟨hpos, hlt⟩ := validIndex_eq_some hidx
+  obtain ⟨hpos', hlt'⟩ := validIndex_eq_some hidx'
+  have htake : (runWithAnswers default (program s) (List.ofFn h)).2.take (j + 1) =
+      (runWithAnswers default (program s) (List.ofFn h')).2.take (j + 1) := by
+    refine take_runWithAnswers default (program s) ?_
+    refine List.ext_getElem (by simp) fun i hi _ => ?_
+    simp only [List.length_take, List.length_ofFn] at hi
+    simp only [List.getElem_take, List.getElem_ofFn]
+    exact hagree ⟨i, by omega⟩ (Fin.mk_lt_of_lt_val (by omega))
+  refine ⟨s, hs, h, h', hagree, hne, rfl, rfl, hpos, hpos', htake,
+    (runWithAnswers default (program s) (List.ofFn h)).2[j.val], List.getElem?_eq_getElem hlt, ?_⟩
+  have hget := congrArg (fun l : List Query => l[j.val]?) htake
+  simp only [List.getElem?_take, Nat.lt_succ_self, ite_true] at hget
+  rw [← hget, List.getElem?_eq_getElem hlt]
+
+end Cslib.OracleComp
diff --git a/Complexity/Probability/Forking.lean b/Complexity/Probability/Forking.lean
new file mode 100644
index 000000000..f962f08f9
--- /dev/null
+++ b/Complexity/Probability/Forking.lean
@@ -0,0 +1,343 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Probability.Rewinding
+import Complexity.Probability.PMF
+import Mathlib.Algebra.Order.Chebyshev
+
+/-!
+# The general forking lemma
+
+An algorithm `A` gets coins `s`, drawn from a distribution, and `q` answers `h : Fin q → H`, drawn
+independently and uniformly from a finite set `H`, and outputs an optional index `j : Fin q`
+together with a result. The *forking algorithm* runs `A` once; if it outputs an index `j`, it
+runs `A` again on the same coins and the same answers before `j`, with fresh answers from `j` on
+(`splice`). It succeeds when the second run outputs the same index `j` and the two answers at `j`
+differ, and it returns both results.
+
+The general forking lemma of Bellare and Neven ([BellareNeven2006], Lemma 1) bounds the success
+probability `frk` of forking by the acceptance probability `acc` of one run:
+`acc ^ 2 / q - acc / |H| ≤ frk` (`sq_div_sub_le_fork`), and consequently
+`acc ≤ q / |H| + √(q · frk)` (`le_add_sqrt_fork`). For each index `j` this is the rewinding lemma
+(`Rewinding.sq_sub_le_twice`), with the coins and the answers before `j` as the first stage, the
+answer at `j` as the challenge and the answers after `j` as fresh randomness of the second stage;
+summing over `j` loses the factor `q` by the Cauchy–Schwarz inequality. Boneh and Shoup prove the
+same bound for `r`-impersonation adversaries ([BonehShoup2023], Lemma 19.8).
+
+The algorithm is deterministic given its coins and answers, which is the form forking needs: the
+second run reuses the coins. The statements are exact; no efficiency is involved.
+
+## Main definitions
+
+* `Cslib.Probability.Forking.splice`: answers from one vector before an index, another from it on.
+* `Cslib.Probability.Forking.accept`: run once and accept when an index is output.
+* `Cslib.Probability.Forking.fork`: the forking algorithm.
+
+## Main results
+
+* `Cslib.Probability.Forking.sq_div_sub_le_fork`: `acc ^ 2 / q - acc / |H| ≤ frk`.
+* `Cslib.Probability.Forking.le_add_sqrt_fork`: `acc ≤ q / |H| + √(q · frk)`.
+* `Cslib.Probability.Forking.mem_support_fork`: what a successful fork returns.
+
+## References
+
+* [M. Bellare, G. Neven, *Multi-Signatures in the Plain Public-Key Model and a General Forking
+  Lemma*][BellareNeven2006], Lemma 1.
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Lemma 19.8.
+-/
+
+@[expose] public section
+
+namespace Cslib.Probability.Forking
+
+variable {S H β : Type} {q : ℕ}
+
+/-- The answers of `h` before the index `j` and those of `h'` from `j` on. -/
+def splice (j : Fin q) (h h' : Fin q → H) : Fin q → H := fun i => if i < j then h i else h' i
+
+variable [Fintype H] [Nonempty H]
+
+/-- One run: draw coins and uniform answers, and accept when `A` outputs an index. -/
+noncomputable def accept (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) :
+    PMF Bool := do
+  let s ← first
+  let h ← PMF.uniformOfFintype (Fin q → H)
+  return (A s h).1.isSome
+
+/-- The forking algorithm ([BellareNeven2006]): run `A` on coins `s` and answers `h`; if it
+outputs an index `j`, rerun it on `s` and on `splice j h h'` for fresh answers `h'`, and succeed
+with both results when the rerun outputs `j` too and `h j ≠ h' j`. -/
+noncomputable def fork [DecidableEq H] (first : PMF S)
+    (A : S → (Fin q → H) → Option (Fin q) × β) : PMF (Option (Fin q × β × β)) := do
+  let s ← first
+  let h ← PMF.uniformOfFintype (Fin q → H)
+  let h' ← PMF.uniformOfFintype (Fin q → H)
+  return match (A s h).1 with
+    | none => none
+    | some j => if (A s (splice j h h')).1 = some j ∧ h j ≠ h' j then
+        some (j, (A s h).2, (A s (splice j h h')).2) else none
+
+/-! ### Splitting the answers at an index -/
+
+/-- Answers from `b` before `j`, the answer `t` at `j`, and answers from `r` after `j`. -/
+private def glue (j : Fin q) (b : Fin q → H) (t : H) (r : Fin q → H) : Fin q → H :=
+  fun i => if i < j then b i else if i = j then t else r i
+
+/-- Gluing is the first component of an equivalence, whose other components are the unused
+parts of `b` and `r`. -/
+private def glueEquiv (j : Fin q) :
+    (Fin q → H) × H × (Fin q → H) ≃ (Fin q → H) × (Fin q → H) × H where
+  toFun x := (glue j x.1 x.2.1 x.2.2, fun i => if i < j then x.2.2 i else x.1 i, x.2.2 j)
+  invFun y := (fun i => if i < j then y.1 i else y.2.1 i, y.1 j,
+    fun i => if i < j then y.2.1 i else if i = j then y.2.2 else y.1 i)
+  left_inv x := by
+    obtain ⟨b, t, r⟩ := x
+    simp only [glue, lt_self_iff_false, ite_false, ite_true, Prod.mk.injEq]
+    refine ⟨funext fun i => ?_, trivial, funext fun i => ?_⟩
+    · split_ifs <;> rfl
+    · by_cases h₁ : i < j <;> by_cases h₂ : i = j <;> simp [h₁, h₂]
+  right_inv y := by
+    obtain ⟨x, z, u⟩ := y
+    simp only [lt_self_iff_false, ite_false, ite_true, Prod.mk.injEq]
+    refine ⟨funext fun i => ?_, funext fun i => ?_, trivial⟩
+    · by_cases h₁ : i < j <;> by_cases h₂ : i = j <;> simp [glue, h₁, h₂]
+    · split_ifs <;> rfl
+
+/-- Gluing independent uniform parts gives uniform answers. -/
+private theorem bind_glue {γ : Type} (j : Fin q) (k : (Fin q → H) → PMF γ) :
+    ((PMF.uniformOfFintype (Fin q → H)).bind fun b => (PMF.uniformOfFintype H).bind fun t =>
+      (PMF.uniformOfFintype (Fin q → H)).bind fun r => k (glue j b t r)) =
+      (PMF.uniformOfFintype (Fin q → H)).bind k := by
+  have hprod : ((PMF.uniformOfFintype (Fin q → H)).bind fun b =>
+      (PMF.uniformOfFintype H).bind fun t => (PMF.uniformOfFintype (Fin q → H)).bind fun r =>
+        PMF.pure (b, t, r)) = PMF.uniformOfFintype ((Fin q → H) × H × (Fin q → H)) := by
+    rw [← Probability.PMF.uniformOfFintype_prod, ← Probability.PMF.uniformOfFintype_prod]
+    simp only [PMF.map, PMF.bind_bind, Function.comp_def, PMF.pure_bind]
+  have hfst : (PMF.uniformOfFintype ((Fin q → H) × H × (Fin q → H))).map
+      (fun x => glue j x.1 x.2.1 x.2.2) = PMF.uniformOfFintype (Fin q → H) := by
+    have := Probability.PMF.uniformOfFintype_prod_map_fst (α := Fin q → H)
+      (β := (Fin q → H) × H)
+    rw [← Probability.PMF.uniformOfFintype_map_equiv (glueEquiv j), PMF.map_comp] at this
+    exact this
+  calc _ = ((PMF.uniformOfFintype ((Fin q → H) × H × (Fin q → H))).map
+        (fun x => glue j x.1 x.2.1 x.2.2)).bind k := by
+        rw [← hprod]
+        simp only [PMF.bind_map, PMF.bind_bind, PMF.pure_bind, Function.comp_def]
+    _ = _ := by rw [hfst]
+
+omit [Fintype H] [Nonempty H] in
+private theorem glue_self (j : Fin q) (b : Fin q → H) (t : H) (r : Fin q → H) :
+    glue j b t r j = t := by
+  simp [glue]
+
+omit [Fintype H] [Nonempty H] in
+private theorem splice_glue (j : Fin q) (b b' : Fin q → H) (t t' : H) (r r' : Fin q → H) :
+    splice j (glue j b t r) (glue j b' t' r') = glue j b t' r' := by
+  funext i
+  by_cases h₁ : i < j <;> simp [splice, glue, h₁]
+
+/-! ### One index -/
+
+/-- The first stage at an index: coins, and answers to use before the index. -/
+private noncomputable def firstAt (first : PMF S) : PMF (S × (Fin q → H)) := do
+  let s ← first
+  let b ← PMF.uniformOfFintype (Fin q → H)
+  return (s, b)
+
+/-- Accepting with the index `j` is one run of a rewinding experiment. -/
+private theorem acceptAt_eq_once (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β)
+    (j : Fin q) :
+    (do
+      let s ← first
+      let h ← PMF.uniformOfFintype (Fin q → H)
+      return decide ((A s h).1 = some j) : PMF Bool) =
+      Rewinding.once (firstAt first) (fun _ _ => PMF.uniformOfFintype (Fin q → H))
+        (fun x t r => decide ((A x.1 (glue j x.2 t r)).1 = some j)) := by
+  simp only [Rewinding.once, firstAt, Probability.PMF.monad_bind_eq_bind,
+    Probability.PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind]
+  congr 1
+  funext s
+  exact (bind_glue j fun h => PMF.pure (decide ((A s h).1 = some j))).symm
+
+variable [DecidableEq H]
+
+/-- Forking with the index `j` is two runs of the rewinding experiment. -/
+private theorem forkAt_eq_twice (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β)
+    (j : Fin q) :
+    (do
+      let s ← first
+      let h ← PMF.uniformOfFintype (Fin q → H)
+      let h' ← PMF.uniformOfFintype (Fin q → H)
+      return decide ((A s h).1 = some j ∧ (A s (splice j h h')).1 = some j ∧ h j ≠ h' j) :
+      PMF Bool) =
+      Rewinding.twice (firstAt first) (fun _ _ => PMF.uniformOfFintype (Fin q → H))
+        (fun x t r => decide ((A x.1 (glue j x.2 t r)).1 = some j)) := by
+  simp only [Rewinding.twice, firstAt, Probability.PMF.monad_bind_eq_bind,
+    Probability.PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind]
+  congr 1
+  funext s
+  rw [← bind_glue j]
+  congr 1
+  funext b
+  congr 1
+  funext t
+  conv_lhs => enter [2, r]; rw [← bind_glue j]
+  simp only [splice_glue, glue_self, PMF.bind_const]
+  rw [PMF.bind_comm]
+  congr 1
+  funext t'
+  congr 1
+  funext r
+  congr 1
+  funext r'
+  congr 1
+  simp only [Bool.decide_and, ne_eq, decide_not, Bool.and_assoc]
+  rfl
+
+/-! ### Summing over the indices -/
+
+omit [DecidableEq H] [Fintype H] [Nonempty H] in
+/-- An event that names one index is the disjoint union of its events at each index. -/
+private theorem bind_match_apply {X : Type} (μ : PMF X) (index : X → Option (Fin q))
+    (event : Fin q → X → Prop) [∀ j x, Decidable (event j x)] :
+    (μ.bind fun x => PMF.pure (match index x with
+      | none => false
+      | some j => decide (event j x))) true =
+      ∑ j, (μ.bind fun x => PMF.pure (decide (index x = some j ∧ event j x))) true := by
+  simp only [PMF.bind_apply, PMF.pure_apply]
+  rw [← Summable.tsum_finsetSum fun _ _ => ENNReal.summable]
+  refine tsum_congr fun x => ?_
+  rw [← Finset.mul_sum]
+  congr 1
+  cases hx : index x with
+  | none => simp
+  | some j =>
+    rw [Finset.sum_eq_single j (fun j' _ hj' => by simp [Ne.symm hj']) (by simp)]
+    simp
+
+omit [DecidableEq H] in
+/-- The acceptance probability, as a real number. -/
+private theorem toReal_accept (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) :
+    (accept first A true).toReal = ∑ j, ((do
+      let s ← first
+      let h ← PMF.uniformOfFintype (Fin q → H)
+      return decide ((A s h).1 = some j) : PMF Bool) true).toReal := by
+  have h := bind_match_apply ((first.bind fun s => (PMF.uniformOfFintype (Fin q → H)).bind
+    fun h => PMF.pure (s, h))) (fun x => (A x.1 x.2).1) (fun _ _ => True)
+  simp only [PMF.bind_bind, PMF.pure_bind, and_true] at h
+  rw [← ENNReal.toReal_sum fun _ _ => PMF.apply_ne_top _ _]
+  refine congrArg ENNReal.toReal (Eq.trans ?_ h)
+  simp only [accept, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure]
+  refine congrArg (fun p : PMF Bool => p true)
+    (congrArg _ (funext fun s => congrArg _ (funext fun h => ?_)))
+  cases (A s h).1 <;> rfl
+
+/-- The success probability of forking, as a real number. -/
+private theorem toReal_fork (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) :
+    ((fork first A).map Option.isSome true).toReal = ∑ j, ((do
+      let s ← first
+      let h ← PMF.uniformOfFintype (Fin q → H)
+      let h' ← PMF.uniformOfFintype (Fin q → H)
+      return decide ((A s h).1 = some j ∧ (A s (splice j h h')).1 = some j ∧ h j ≠ h' j) :
+        PMF Bool) true).toReal := by
+  have h := bind_match_apply ((first.bind fun s => (PMF.uniformOfFintype (Fin q → H)).bind
+    fun h => (PMF.uniformOfFintype (Fin q → H)).bind fun h' => PMF.pure (s, h, h')))
+    (fun x => (A x.1 x.2.1).1)
+    (fun j x => (A x.1 (splice j x.2.1 x.2.2)).1 = some j ∧ x.2.1 j ≠ x.2.2 j)
+  simp only [PMF.bind_bind, PMF.pure_bind] at h
+  rw [← ENNReal.toReal_sum fun _ _ => PMF.apply_ne_top _ _]
+  refine congrArg ENNReal.toReal (Eq.trans ?_ h)
+  simp only [fork, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure,
+    PMF.map_bind, PMF.pure_map]
+  refine congrArg (fun p : PMF Bool => p true) (congrArg _ (funext fun s =>
+    congrArg _ (funext fun h => congrArg _ (funext fun h' => ?_))))
+  cases (A s h).1 with
+  | none => rfl
+  | some j => by_cases hc : (A s (splice j h h')).1 = some j ∧ h j ≠ h' j <;> simp [hc]
+
+/-! ### The forking lemma -/
+
+/-- **The general forking lemma** ([BellareNeven2006], Lemma 1): forking succeeds with
+probability at least `acc ^ 2 / q - acc / |H|`, where `acc` is the probability that one run
+outputs an index. -/
+theorem sq_div_sub_le_fork (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) :
+    (accept first A true).toReal ^ 2 / q - (accept first A true).toReal / Fintype.card H ≤
+      ((fork first A).map Option.isSome true).toReal := by
+  set N : ℝ := (Fintype.card H : ℝ)
+  set a : Fin q → ℝ := fun j => ((do
+    let s ← first
+    let h ← PMF.uniformOfFintype (Fin q → H)
+    return decide ((A s h).1 = some j) : PMF Bool) true).toReal
+  have hj (j : Fin q) : a j ^ 2 - a j / N ≤ ((do
+      let s ← first
+      let h ← PMF.uniformOfFintype (Fin q → H)
+      let h' ← PMF.uniformOfFintype (Fin q → H)
+      return decide ((A s h).1 = some j ∧ (A s (splice j h h')).1 = some j ∧ h j ≠ h' j) :
+        PMF Bool) true).toReal := by
+    simp only [a, acceptAt_eq_once, forkAt_eq_twice]
+    exact Rewinding.sq_sub_le_twice _ _ _
+  rw [toReal_fork, toReal_accept]
+  have hcs : (∑ j, a j) ^ 2 / q ≤ ∑ j, a j ^ 2 := by
+    rcases Nat.eq_zero_or_pos q with rfl | hq
+    · simp
+    · rw [div_le_iff₀ (by exact_mod_cast hq), mul_comm]
+      simpa using sq_sum_le_card_mul_sum_sq (s := Finset.univ) (f := a)
+  calc (∑ j, a j) ^ 2 / q - (∑ j, a j) / N ≤ ∑ j, a j ^ 2 - ∑ j, a j / N := by
+        rw [Finset.sum_div]
+        linarith
+    _ = ∑ j, (a j ^ 2 - a j / N) := by rw [Finset.sum_sub_distrib]
+    _ ≤ _ := Finset.sum_le_sum fun j _ => hj j
+
+/-- The forking lemma solved for the acceptance probability: `acc ≤ q / |H| + √(q · frk)`. -/
+theorem le_add_sqrt_fork (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) :
+    (accept first A true).toReal ≤
+      q / Fintype.card H + √(q * ((fork first A).map Option.isSome true).toReal) := by
+  set ε := (accept first A true).toReal with hεdef
+  set N : ℝ := (Fintype.card H : ℝ)
+  have hN : 0 < N := Nat.cast_pos.mpr Fintype.card_pos
+  have hfork := sq_div_sub_le_fork first A
+  by_cases hε : ε ≤ q / N
+  · exact hε.trans (le_add_of_nonneg_right (Real.sqrt_nonneg _))
+  · have hq : (0 : ℝ) < q := by
+      rcases Nat.eq_zero_or_pos q with hq0 | hq0
+      · subst hq0
+        exact absurd (by simp [hεdef, toReal_accept]) hε
+      · exact_mod_cast hq0
+    have hsq : (ε - q / N) ^ 2 ≤ q * ((fork first A).map Option.isSome true).toReal := by
+      have hmul := mul_le_mul_of_nonneg_left hfork hq.le
+      refine le_trans ?_ hmul
+      have hexpand : q * (ε ^ 2 / q - ε / N) = (ε - q / N) ^ 2 + (ε - q / N) * (q / N) := by
+        field_simp
+        ring
+      rw [hexpand]
+      exact le_add_of_nonneg_right (mul_nonneg (by linarith) (by positivity))
+    have := Real.abs_le_sqrt hsq
+    linarith [le_abs_self (ε - q / N)]
+
+/-- A successful fork comes from one coin sample and two answer vectors that agree before the
+returned index `j` and differ at it, on both of which `A` outputs `j`. -/
+theorem mem_support_fork {first : PMF S} {A : S → (Fin q → H) → Option (Fin q) × β}
+    {j : Fin q} {out out' : β} (hfork : some (j, out, out') ∈ (fork first A).support) :
+    ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧
+      A s h = (some j, out) ∧ A s h' = (some j, out') := by
+  simp only [fork, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure,
+    PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at hfork
+  obtain ⟨s, hs, h, -, h', -, hres⟩ := hfork
+  refine ⟨s, hs, h, splice j h h', fun i hi => by simp [splice, hi], ?_⟩
+  cases hA : (A s h).1 with
+  | none => simp [hA] at hres
+  | some j' =>
+    simp only [hA] at hres
+    split_ifs at hres with hc
+    · simp only [Option.some.injEq, Prod.mk.injEq] at hres
+      obtain ⟨rfl, rfl, rfl⟩ := hres
+      refine ⟨by simpa [splice] using hc.2, Prod.ext hA rfl, Prod.ext hc.1 rfl⟩
+
+end Cslib.Probability.Forking
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index c588ffe5d..d31de221c 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -86,6 +86,7 @@ import ComplexityTests.CountingVerifier
 import ComplexityTests.Crypto.Bootstrapping
 import ComplexityTests.Crypto.Encryption
 import ComplexityTests.Crypto.FixedKeySecurity
+import ComplexityTests.Crypto.Forking
 import ComplexityTests.Crypto.GMWPointwise
 import ComplexityTests.Crypto.GSW
 import ComplexityTests.Crypto.GSWDecryption
diff --git a/ComplexityTests/Crypto/Forking.lean b/ComplexityTests/Crypto/Forking.lean
new file mode 100644
index 000000000..218fdc7f4
--- /dev/null
+++ b/ComplexityTests/Crypto/Forking.lean
@@ -0,0 +1,115 @@
+/-
+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.Forking
+import Complexity.Probability.Forking
+import Complexity.Probability.PMF
+
+/-!
+# Tests for the forking lemma
+
+An algorithm that always names its only answer is accepted with probability `1`, so forking it
+succeeds with probability at least `1 - 1 / 2`; it succeeds exactly when two independent bits
+differ, so the bound is attained. The oracle program that asks one query and names it satisfies
+the hypotheses of the oracle forking lemma, which gives a positive forking probability; a
+successful fork gives two runs that ask the same query. A program that names a position without
+asking any query never forks successfully.
+-/
+
+namespace ComplexityTests.Crypto.Forking
+
+open Cslib Cslib.Probability
+
+/-- Always name the only answer. -/
+def always (_ : Unit) (_ : Fin 1 → Bool) : Option (Fin 1) × Unit := (some 0, ())
+
+example : (Forking.accept (PMF.pure ()) always true) = 1 := by
+  simp [Forking.accept, always]
+
+/-- The general forking lemma for `always`: `1 - 1 / 2 ≤ frk`. -/
+example : (1 : ℝ) / 2 ≤ ((Forking.fork (PMF.pure ()) always).map Option.isSome true).toReal := by
+  have h := Forking.sq_div_sub_le_fork (PMF.pure ()) always
+  have hacc : (Forking.accept (PMF.pure ()) always true).toReal = 1 := by
+    simp [Forking.accept, always]
+  rw [hacc] at h
+  simp only [Fintype.card_bool, Nat.cast_ofNat, Nat.cast_one, one_pow, div_one] at h
+  linarith
+
+/-! ### Oracle programs -/
+
+/-- Ask one query and name it. -/
+def askOnce (_ : Unit) : OracleComp (fun _ : Unit => Bool) (Option ℕ × Bool) := do
+  let a ← OracleComp.query (spec := fun _ : Unit => Bool) ()
+  return (some 0, a)
+
+/-- `askOnce` asks one query. -/
+theorem askOnce_queries (s : Unit) :
+    (OracleComp.interpret (fun q => ProbOracleComp.query (spec := fun _ : Unit => Bool) q)
+      (askOnce s)).HasQueryBounds (fun _ => 0) 1 0 := by
+  have h := (ProbOracleComp.HasQueryBounds.query (Response := fun _ : Unit => Bool) ()
+    (fun _ => 0) le_rfl).bind fun a =>
+      ProbOracleComp.HasQueryBounds.pure (Response := fun _ : Unit => Bool) (some 0, a)
+        (fun _ => 0) 0
+  simpa [askOnce] using h
+
+/-- Forking `askOnce`, which always names its query, succeeds with probability at least
+`1 / 4`. -/
+example : (1 : ℝ) / 4 ≤ ((Forking.fork (PMF.pure ())
+    (OracleComp.forkingAlgorithm false 1 askOnce)).map Option.isSome true).toReal := by
+  have h := OracleComp.le_add_sqrt_fork (PMF.pure ()) askOnce false askOnce_queries
+  have hacc : ((do
+      let s ← PMF.pure ()
+      let run ← (OracleComp.interpret OracleComp.countingUniform (askOnce s)).run 0
+      return (OracleComp.validIndex 1 run.2 run.1.1).isSome : PMF Bool) true).toReal = 1 := by
+    rw [Probability.PMF.monad_bind_eq_bind, PMF.pure_bind, Probability.PMF.monad_bind_eq_bind,
+      OracleComp.run_interpret_countingUniform_eq false (askOnce ()) (askOnce_queries ()),
+      PMF.bind_map]
+    simp [Function.comp_def, askOnce, OracleComp.validIndex]
+  rw [hacc] at h
+  simp only [Fintype.card_bool, Nat.cast_ofNat, Nat.cast_one, one_mul] at h
+  have hsqrt : (1 : ℝ) / 2 ≤ √(((Forking.fork (PMF.pure ())
+      (OracleComp.forkingAlgorithm false 1 askOnce)).map Option.isSome true).toReal) := by
+    linarith
+  nlinarith [Real.sq_sqrt (ENNReal.toReal_nonneg (a := ((Forking.fork (PMF.pure ())
+    (OracleComp.forkingAlgorithm false 1 askOnce)).map Option.isSome true))), Real.sqrt_nonneg
+    (((Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1 askOnce)).map
+      Option.isSome true).toReal)]
+
+/-- Both runs of a successful fork of `askOnce` ask the same query. -/
+example {j : Fin 1} {out out' : (Option ℕ × Bool) × List Unit}
+    (hfork : some (j, out, out') ∈
+      (Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1 askOnce)).support) :
+    out.2.take (j + 1) = out'.2.take (j + 1) := by
+  obtain ⟨-, -, -, -, -, -, -, -, -, -, htake, -⟩ := OracleComp.mem_support_fork hfork
+  exact htake
+
+/-- Name position `0` without asking any query. -/
+def nameWithoutAsking (_ : Unit) : OracleComp (fun _ : Unit => Bool) (Option ℕ × Unit) :=
+  pure (some 0, ())
+
+/-- A program that names position `0` without asking any query does not validly name it, so its
+fork never succeeds. -/
+example : (Forking.fork (PMF.pure ()) (OracleComp.forkingAlgorithm false 1
+    nameWithoutAsking)).map Option.isSome true = 0 := by
+  simp [Forking.fork, OracleComp.forkingAlgorithm, OracleComp.validIndex, nameWithoutAsking]
+
+/-! ### Axioms -/
+
+/--
+info: 'Cslib.Probability.Forking.sq_div_sub_le_fork' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Forking.sq_div_sub_le_fork
+
+/--
+info: 'Cslib.OracleComp.le_add_sqrt_fork' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms OracleComp.le_add_sqrt_fork
+
+end ComplexityTests.Crypto.Forking
diff --git a/ROADMAP.md b/ROADMAP.md
index 295511540..45b3092c9 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -1156,10 +1156,13 @@ Jukna coverage below is an additional target beyond the V1 port:
   a family of prime-order groups with plain polynomial-time operations, instantiated by
   [Schnorr groups](Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean), and
   [Schnorr identification](Complexity/Crypto/Computational/SchnorrIdentification.lean) is secure
-  against direct attacks by uniform strict PPT impersonators under it. Open: security against
-  eavesdropping in the strict-PPT model, where simulating transcripts needs approximately uniform
-  `ZMod q` samples and hence an explicit statistical-distance term, and Fiat–Shamir/Schnorr
-  signatures in the random-oracle model with the forking bound of Theorem 19.16.
+  against direct attacks by uniform strict PPT impersonators under it. The general
+  [forking lemma](Complexity/Probability/Forking.lean) (Bellare–Neven) is proved, also for
+  [oracle programs](Complexity/Languages/Probabilistic/Forking.lean) with explicit coins and
+  presampled answers. Open (see #640): Fiat–Shamir/Schnorr signatures in the random-oracle model
+  with the bound of Theorem 19.16, and security against eavesdropping in the strict-PPT model,
+  where simulating transcripts needs approximately uniform `ZMod q` samples and hence an explicit
+  statistical-distance term.
 
 The current V1 port excludes the circuitized anti-checker, hardness-magnification argument and
 MINKT/MINCKT developments. The long-term canon above includes metacomplexity; those results should
diff --git a/references.bib b/references.bib
index 25cffc233..8d9a6be8c 100644
--- a/references.bib
+++ b/references.bib
@@ -390,6 +390,16 @@ @inproceedings{BonehHaleviHamburgOstrovsky2008
   url          = {https://crypto.stanford.edu/~dabo/papers/circular.pdf}
 }
 
+@inproceedings{BellareNeven2006,
+  author       = {Mihir Bellare and Gregory Neven},
+  title        = {Multi-Signatures in the Plain Public-Key Model and a General Forking Lemma},
+  booktitle    = {Proceedings of the 13th ACM Conference on Computer and Communications Security},
+  pages        = {390--399},
+  publisher    = {ACM},
+  year         = {2006},
+  doi          = {10.1145/1180405.1180453}
+}
+
 @misc{BonehShoup2023,
   author       = {Dan Boneh and Victor Shoup},
   title        = {A Graduate Course in Applied Cryptography},