SamuelSchlesinger · Oct 24, 2026 · Oct 24, 2026
diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean
@@ -73,7 +73,7 @@ All are polynomial-time in their unary or binary inputs.
 
 namespace Cslib.Complexity.QBFProtocol
 
-open Cslib.Logic.PL Polynomial Turing.MultiTapeTM Cslib.Probability
+open Cslib.Logic.PL Polynomial Turing.MultiTapeTM Cslib.Probability Cslib.ProbComp
 open scoped ENNReal
 
 /-! ### Arithmetic modulo `p` -/

diff --git a/Complexity/Computability/Probabilistic/BoundedUniform.lean b/Complexity/Computability/Probabilistic/BoundedUniform.lean
@@ -36,7 +36,7 @@ Failure remains in the certified program's output.
 
 namespace Cslib.Probability
 
-open Turing.MultiTapeTM
+open ProbComp Turing.MultiTapeTM
 
 /-- Unary bounds and attempt counts give a uniform strict PPT sampler, including its failure
 result and every stored attempt. -/

diff --git a/Complexity/Computability/Probabilistic/CenteredBinomial.lean b/Complexity/Computability/Probabilistic/CenteredBinomial.lean
@@ -37,7 +37,7 @@ charges both blocks of independent trials, their counts, and signed subtraction.
 
 namespace Cslib.Probability
 
-open Turing.MultiTapeTM
+open ProbComp Turing.MultiTapeTM
 
 /-- The centered-binomial program is uniformly strict PPT, with a unary parameter and binary
 signed output. No fixed finite output type or finite-rank encoding is used. -/
@@ -69,5 +69,5 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleCenteredBinomial {α
     {input : α ↪ List Bool} {parameter : α → ℕ}
     (hparameter : ComputableTidilyInPolyTime parameter input encUnary) :
     Cslib.Probability.IsPPTOn input encIntBin
-      (fun a => Cslib.Probability.sampleCenteredBinomial (parameter a)) :=
+      (fun a => Cslib.ProbComp.sampleCenteredBinomial (parameter a)) :=
   Cslib.Probability.isPPTOn_sampleCenteredBinomial.preprocess hparameter
diff --git a/Complexity/Computability/Probabilistic/UniformNat.lean b/Complexity/Computability/Probabilistic/UniformNat.lean
@@ -66,7 +66,7 @@ theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_dyadicSize :
 
 namespace Cslib.Probability
 
-open Turing.MultiTapeTM
+open ProbComp Turing.MultiTapeTM
 
 /-- A unary bit width gives a uniformly strict PPT sampler with binary natural output. -/
 theorem isPPTOn_sampleBinaryNat : IsPPTOn encUnary encNat sampleBinaryNat :=
@@ -106,12 +106,12 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleBinaryNat {α : Type
     {input : α ↪ List Bool} {width : α → ℕ}
     (hwidth : ComputableTidilyInPolyTime width input encUnary) :
     Cslib.Probability.IsPPTOn input encNat
-      (fun a => Cslib.Probability.sampleBinaryNat (width a)) :=
+      (fun a => Cslib.ProbComp.sampleBinaryNat (width a)) :=
   Cslib.Probability.isPPTOn_sampleBinaryNat.preprocess hwidth
 
 namespace Cslib.Probability
 
-open Turing.MultiTapeTM
+open ProbComp Turing.MultiTapeTM
 
 /-- Approximately uniform residues: reducing a computed number of fair bits modulo a computed
 modulus is uniformly strict PPT, with binary output. -/

diff --git a/Complexity/Crypto/Computational/GGM/Reduction.lean b/Complexity/Crypto/Computational/GGM/Reduction.lean
@@ -157,7 +157,7 @@ theorem levelTest_gap (generator : List Bool → List Bool) (adversary : OracleD
 dyadic ranges, and unused indices reject. The query budget is a fixed function of the parameter. -/
 noncomputable def reduction (generator : List Bool → List Bool) (adversary : OracleDistinguisher)
     (count : ℕ → ℕ) : Distinguisher := fun n challenge => do
-  let depth ← sampleDyadicIndex n
+  let depth ← ProbComp.sampleDyadicIndex n
   if depth < n then levelTest generator adversary n depth (count n) challenge else pure false
 
 /-- Efficient generation and an efficient query budget give one uniform PPT reduction. -/
@@ -194,7 +194,7 @@ theorem reduction_gap (generator : List Bool → List Bool) (adversary : OracleD
     (lt_dyadicSize n).le (dyadicSize (count n))
     (fun depth hdepth =>
       levelTest_gap generator adversary n depth (count n) hdepth hqueries)
-  simpa only [eval_bind_sampleDyadicIndex_guard, PMF.monad_bind_eq_bind,
+  simpa only [ProbComp.eval_bind_sampleDyadicIndex_guard, PMF.monad_bind_eq_bind,
     hybridGame_zero, hybridGame_self] using h
 
 /-- The real/ideal PRF advantage is the reduction's generator advantage times the two sampling

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean
@@ -37,7 +37,7 @@ the equality below exposes only the public marginal, as required by the security
 
 namespace Cslib.Crypto.Homomorphic.GSW
 
-open Probability
+open ProbComp Probability
 
 /-- Reduce the difference of two independent `η`-bit counts modulo the actual modulus. -/
 noncomputable def noiseLaw (w η : ℕ) : PMF (ZMod (2 ^ w)) :=

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling.lean
@@ -49,7 +49,7 @@ encryption security, complete native algorithm certificate or bootstrappability
 
 namespace Cslib.Crypto.Homomorphic.GSW
 
-open Probability
+open ProbComp Probability
 
 /-- Sample one residue from `w` independent fair bits. -/
 noncomputable def sampleResidue (w : ℕ) : ProbComp (ZMod (2 ^ w)) :=

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Randomness.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Randomness.lean
@@ -37,7 +37,7 @@ is proved separately; matrix computation and cryptographic security remain separ
 
 namespace Cslib.Crypto.Homomorphic.GSW
 
-open Probability
+open ProbComp Probability
 
 /-- A residue uses a uniform word of exactly its binary width. -/
 theorem exists_uniform_seed_sampleResidue (w : ℕ) :

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean
@@ -51,7 +51,7 @@ arithmetic, the complete GSW key-generation or encryption algorithms, or computa
 
 namespace Cslib.Crypto.Homomorphic.GSW
 
-open Probability Turing.MultiTapeTM
+open ProbComp Probability Turing.MultiTapeTM
 
 /-- Secret entries, public-matrix rows and signed errors, without dependent dimensions. -/
 abbrev SerializedKeyInputs := List ℕ × (List (List ℕ) × List ℤ)

diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction.lean
@@ -48,7 +48,7 @@ its beginning. Dyadic padding coordinates reject, and decoding is total on every
 
 namespace Cslib.Crypto.Homomorphic.Scheme
 
-open Probability Turing.MultiTapeTM
+open ProbComp Probability Turing.MultiTapeTM
 
 /-- Active flag, earlier keys, predecessor, challenge public key, later keys, and unary bit index.
 Every saved secret belongs to a key generated by the reduction itself. -/

diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/Game.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/Game.lean
@@ -39,7 +39,7 @@ outgoing link has been erased.
 
 namespace Cslib.Crypto.Homomorphic.Scheme
 
-open Probability
+open ProbComp Probability
 open scoped NNReal
 
 variable (E : Scheme)

diff --git a/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean b/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean
@@ -50,7 +50,7 @@ Adapted from the cslib `crypto` branch at
 
 namespace Cslib.Crypto.SavedPrediction
 
-open Probability BitString Turing.MultiTapeTM
+open ProbComp Probability BitString Turing.MultiTapeTM
 
 /-- Finite data needed to reuse one coordinate predictor on arbitrary observations. -/
 structure Description where

diff --git a/Complexity/Crypto/Computational/Hybrid/Sequence.lean b/Complexity/Crypto/Computational/Hybrid/Sequence.lean
@@ -48,7 +48,7 @@ Adapted from Crypto/Computational/Hybrid/Sequence.lean on the cslib `crypto` bra
 
 namespace Cslib.Crypto
 
-open Probability Turing.MultiTapeTM
+open ProbComp Probability Turing.MultiTapeTM
 open scoped NNReal
 
 variable {α : Type}

diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean
@@ -86,7 +86,7 @@ one-way hash functions and GMR/Merkle authentication trees.
 
 namespace Cslib.Crypto
 
-open Filter Probability Turing.MultiTapeTM
+open Filter ProbComp Probability Turing.MultiTapeTM
 open scoped NNReal ENNReal
 
 @[fun_prop]

diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Clipped.lean b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Clipped.lean
@@ -49,7 +49,7 @@ Adapted from the cslib `crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203c
 
 namespace Cslib.Crypto.Pseudoentropy.Boosting
 
-open Probability BitString Turing.MultiTapeTM
+open ProbComp Probability BitString Turing.MultiTapeTM
 
 /-- The clipped affine probability associated with a signed margin. -/
 noncomputable def clippedProbability (slope margin : ℝ) : ℝ :=

diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean
@@ -50,7 +50,7 @@ Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean on the cslib `crypto`
 
 namespace Cslib.Crypto.Pseudoentropy.Boosting
 
-open Probability BitString Turing.MultiTapeTM
+open ProbComp Probability BitString Turing.MultiTapeTM
 
 /-- The numerator of a clipped linear weight, computed entirely with natural numbers.
 The excess of correct over incorrect votes is `2 * votes.count truth - votes.length` in

diff --git a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean
@@ -49,7 +49,7 @@ Adapted from the cslib `crypto` branch at
 
 namespace Cslib.Crypto.Pseudoentropy.SamplablePair
 
-open Probability Probability.PMF BitString Boosting Filter Turing.MultiTapeTM
+open ProbComp Probability Probability.PMF BitString Boosting Filter Turing.MultiTapeTM
 
 /-- All tests in a uniformly efficient polynomial-size family eventually admit dense soft masks
 with small distinguishing gap whenever their density is valid. The common eventual threshold

diff --git a/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean b/Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean
@@ -55,7 +55,7 @@ Adapted from Crypto/Computational/Pseudoentropy/HashPair.lean on the cslib `cryp
 
 namespace Cslib.Crypto.Pseudoentropy.HashPair
 
-open Cslib.Probability Cslib.Probability.PMF BitString Turing.MultiTapeTM
+open Cslib.ProbComp Cslib.Probability Cslib.Probability.PMF BitString Turing.MultiTapeTM
 
 /-- The number of possible hash lengths. Six extra lengths leave room for the truncation
 threshold in the inversion proof; rounding up makes sampling exact with fair bits. -/

diff --git a/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean
@@ -43,7 +43,7 @@ Adapted from the cslib `crypto` branch at
 
 namespace Cslib.Crypto.Pseudoentropy
 
-open Probability Probability.PMF BitString
+open ProbComp Probability Probability.PMF BitString
 
 open scoped NNReal
 

diff --git a/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean b/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean
@@ -53,7 +53,7 @@ at `5ff69ca93402e7c947208dc56396d6d86203ccd8`, using typed saved seeds and the t
 
 namespace Cslib.Crypto.Pseudoentropy.HashPair
 
-open Probability BitString GoldreichLevin Turing.MultiTapeTM
+open ProbComp Probability BitString GoldreichLevin Turing.MultiTapeTM
 
 /-- One polynomial tape budget covers all digest lengths and parity queries for an image. -/
 def coinBudget (c d n imageLength : ℕ) : ℕ :=

diff --git a/Complexity/Crypto/Computational/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean
@@ -59,7 +59,7 @@ Adapted from Crypto/Computational/Stretch.lean on the cslib `crypto` branch at
 
 namespace Cslib.Crypto.PRGStretch
 
-open Probability BitString Turing.MultiTapeTM
+open ProbComp Probability BitString Turing.MultiTapeTM
 
 /-- Hybrid `i` has `i` genuinely random suffix bits and `total - i` seed expansions left. -/
 noncomputable def hybrid (generator : List Bool → List Bool) (n total i : ℕ) : PMF (List Bool) :=
@@ -372,7 +372,7 @@ end Cslib.Crypto.PRGStretch
 
 namespace Cslib.Crypto
 
-open Probability BitString Turing.MultiTapeTM
+open ProbComp Probability BitString Turing.MultiTapeTM
 
 /-- Amplify a one-bit PRG to any efficiently computed, strictly larger output length. -/
 theorem PseudorandomGenerator.amplify {generator : List Bool → List Bool}

diff --git a/Complexity/Crypto/Computational/UniformChoice.lean b/Complexity/Crypto/Computational/UniformChoice.lean
@@ -52,7 +52,7 @@ nonnegative game API.
 
 namespace Cslib.Crypto
 
-open Probability Turing.MultiTapeTM
+open ProbComp Probability Turing.MultiTapeTM
 open scoped NNReal
 
 namespace UniformChoice

diff --git a/Complexity/Languages/Probabilistic/BoundedUniform.lean b/Complexity/Languages/Probabilistic/BoundedUniform.lean
@@ -36,29 +36,30 @@ transcript/error and an extractor's implementation require separate proofs.
 
 ## Main definitions
 
-* `Cslib.Probability.sampleUniformInterval`: bounded retry with an explicit failure result.
-* `Cslib.Probability.intervalFailure`, `Cslib.Probability.intervalSuccess`: exact event masses.
-* `Cslib.Probability.sampleIntegerBox`: coordinatewise finite-attempt integer-box sampling.
-* `Cslib.Probability.integerBoxLaw`: the exact mathematical uniform reference law.
+* `Cslib.ProbComp.sampleUniformInterval`: bounded retry with an explicit failure result.
+* `Cslib.ProbComp.intervalFailure`, `Cslib.ProbComp.intervalSuccess`: exact event masses.
+* `Cslib.ProbComp.sampleIntegerBox`: coordinatewise finite-attempt integer-box sampling.
+* `Cslib.ProbComp.integerBoxLaw`: the exact mathematical uniform reference law.
 
 ## Main results
 
-* `Cslib.Probability.eval_sampleUniformInterval_none`,
-  `Cslib.Probability.eval_sampleUniformInterval_some_toReal`: the full interval law.
-* `Cslib.Probability.sampleUniformInterval_conditional`: conditional uniformity at observable
+* `Cslib.ProbComp.eval_sampleUniformInterval_none`,
+  `Cslib.ProbComp.eval_sampleUniformInterval_some_toReal`: the full interval law.
+* `Cslib.ProbComp.sampleUniformInterval_conditional`: conditional uniformity at observable
   success events.
-* `Cslib.Probability.sampleUniformInterval_test_error_le`: unconditional interval error,
+* `Cslib.ProbComp.sampleUniformInterval_test_error_le`: unconditional interval error,
   including the binary-bound implementation.
-* `Cslib.Probability.eval_sampleIntegerBox_some`, `Cslib.Probability.eval_sampleIntegerBox_none`:
+* `Cslib.ProbComp.eval_sampleIntegerBox_some`, `Cslib.ProbComp.eval_sampleIntegerBox_none`:
   the full joint success/failure law.
-* `Cslib.Probability.sampleIntegerBox_test_error_le`: explicit unconditional statistical error.
-* `Cslib.Probability.sampleIntegerBox_support`: exact output dimension and integer bounds.
+* `Cslib.ProbComp.sampleIntegerBox_test_error_le`: explicit unconditional statistical error.
+* `Cslib.ProbComp.sampleIntegerBox_support`: exact output dimension and integer bounds.
 -/
 
 @[expose] public section
 
-namespace Cslib.Probability
+namespace Cslib.ProbComp
 
+open Probability
 open scoped ENNReal NNReal
 
 /-- The probability that one capped draw is rejected. At bound zero every draw is rejected. -/
@@ -740,4 +741,4 @@ theorem integerBoxLaw_apply_index (radius dimension : ℕ)
   simp_rw [hcoord]
   simp
 
-end Cslib.Probability
+end Cslib.ProbComp
diff --git a/Complexity/Languages/Probabilistic/CenteredBinomial.lean b/Complexity/Languages/Probabilistic/CenteredBinomial.lean
@@ -24,14 +24,15 @@ or encryption-security property is asserted. Native runtime is certified separat
 
 ## Main definitions
 
-* `sampleCenteredBinomial`: subtract two independently sampled Boolean counts.
+* `Cslib.ProbComp.sampleCenteredBinomial`: subtract two independently sampled Boolean counts.
 
 ## Main results
 
-* `eval_sampleCenteredBinomial`: the exact two-word distribution.
-* `eval_sampleCenteredBinomial_eq_map`: the same law from one word of `2 * η` bits.
-* `mem_support_sampleCenteredBinomial_iff`: support is exactly the closed integer interval.
-* `map_neg_eval_sampleCenteredBinomial`: negation preserves the distribution.
+* `Cslib.ProbComp.eval_sampleCenteredBinomial`: the exact two-word distribution.
+* `Cslib.ProbComp.eval_sampleCenteredBinomial_eq_map`: the same law from one word of `2 * η` bits.
+* `Cslib.ProbComp.mem_support_sampleCenteredBinomial_iff`: support is exactly the closed integer
+  interval.
+* `Cslib.ProbComp.map_neg_eval_sampleCenteredBinomial`: negation preserves the distribution.
 
 ## References
 
@@ -41,7 +42,9 @@ or encryption-security property is asserted. Native runtime is certified separat
 
 @[expose] public section
 
-namespace Cslib.Probability
+namespace Cslib.ProbComp
+
+open Probability
 
 /-- Subtract the true counts of two independent blocks of `η` fair bits. -/
 noncomputable def sampleCenteredBinomial (η : ℕ) : ProbComp ℤ := do
@@ -110,4 +113,4 @@ theorem map_neg_eval_sampleCenteredBinomial (η : ℕ) :
     PMF.pure_map, neg_sub]
   rw [PMF.bind_comm]
 
-end Cslib.Probability
+end Cslib.ProbComp
diff --git a/Complexity/Languages/Probabilistic/UniformNat.lean b/Complexity/Languages/Probabilistic/UniformNat.lean
@@ -31,19 +31,21 @@ range is at most `2 * (bound + 1)`. `sampleDyadicCoin bound numerator` compares
 
 ## Main definitions
 
-* `sampleBinaryNat`: exact uniform sampling from a specified bit width.
-* `sampleModNat`: approximately uniform sampling of residues modulo a given modulus.
-* `sampleDyadicIndex`: exact uniform sampling in the power-of-two range.
-* `sampleBoundedIndex`: a capped uniform index with a rejection sentinel.
-* `sampleDyadicCoin`: an exact capped dyadic acceptance probability.
+* `Cslib.ProbComp.sampleBinaryNat`: exact uniform sampling from a specified bit width.
+* `Cslib.ProbComp.sampleModNat`: approximately uniform sampling of residues modulo a given modulus.
+* `Cslib.ProbComp.sampleDyadicIndex`: exact uniform sampling in the power-of-two range.
+* `Cslib.ProbComp.sampleBoundedIndex`: a capped uniform index with a rejection sentinel.
+* `Cslib.ProbComp.sampleDyadicCoin`: an exact capped dyadic acceptance probability.
 
 ## Main results
 
-* `eval_sampleBinaryNat`, `mem_support_sampleBinaryNat_iff`: the exact law and support.
-* `eval_sampleModNat`, `dist_map_natCast_eval_sampleModNat_le`: the law of the residue sampler
-  and its distance from uniform on `ZMod q`.
-* `eval_sampleDyadicIndex`, `eval_sampleBoundedIndex`: exact distribution laws.
-* `eval_sampleDyadicCoin_true`: exact acceptance mass, including zero and one.
+* `Cslib.ProbComp.eval_sampleBinaryNat`, `Cslib.ProbComp.mem_support_sampleBinaryNat_iff`:
+  the exact law and support.
+* `Cslib.ProbComp.eval_sampleModNat`, `Cslib.ProbComp.dist_map_natCast_eval_sampleModNat_le`:
+  the law of the residue sampler and its distance from uniform on `ZMod q`.
+* `Cslib.ProbComp.eval_sampleDyadicIndex`, `Cslib.ProbComp.eval_sampleBoundedIndex`:
+  exact distribution laws.
+* `Cslib.ProbComp.eval_sampleDyadicCoin_true`: exact acceptance mass, including zero and one.
 
 ## References
 
@@ -53,9 +55,9 @@ Adapted from Languages/Probabilistic/UniformNat.lean on the cslib `crypto` branc
 
 @[expose] public section
 
-namespace Cslib.Probability
+namespace Cslib.ProbComp
 
-open BitString
+open BitString Probability
 
 /-- Interpret exactly `width` independent fair bits as a binary natural number. -/
 noncomputable def sampleBinaryNat (width : ℕ) : ProbComp ℕ :=
@@ -183,4 +185,4 @@ theorem eval_sampleBoundedIndex (bound : ℕ) :
   simp [sampleBoundedIndex, ProbComp.eval_map, BitString.eval_sampleList,
     uniformList_boundedBinaryValue]
 
-end Cslib.Probability
+end Cslib.ProbComp
diff --git a/ComplexityTests/Axioms.lean b/ComplexityTests/Axioms.lean
@@ -4979,11 +4979,11 @@ info: 'Cslib.BitString.uniformList_binaryValue' depends on axioms:
 #print axioms Cslib.BitString.uniformList_binaryValue
 
 /--
-info: 'Cslib.Probability.eval_sampleBoundedIndex' depends on axioms:
+info: 'Cslib.ProbComp.eval_sampleBoundedIndex' depends on axioms:
 [propext, Classical.choice, Quot.sound]
 -/
 #guard_msgs in
-#print axioms Cslib.Probability.eval_sampleBoundedIndex
+#print axioms Cslib.ProbComp.eval_sampleBoundedIndex
 
 /--
 info: 'Cslib.Probability.isPPTOn_sampleBoundedIndex' depends on axioms: