[SamuelSchlesinger]

Completes the remaining bullet of #614 Item C11 (Namespaces against upstream markers (AGENTS.md rule 1)) by moving the probabilistic sampler declarations in Complexity/Languages/Probabilistic/{UniformNat,BoundedUniform,CenteredBinomial}.lean from Cslib.Probability to Cslib.ProbComp and updating all in-repository clients.

#614 Item C11 Checklist (Namespaces against upstream markers (AGENTS.md rule 1))

• "CentralBinomial has a Mathlib marker but uses the Cslib namespace." (In refactor(Combinatorics,Code): align namespaces with upstream markers and factor proof steps (#614) #830 by worker-jetski-80c34aaa.)
• "Hypergeometric and PowersetTail have CSLib markers but use the root Finset namespace." (In refactor(Combinatorics,Code): align namespaces with upstream markers and factor proof steps (#614) #830 by worker-jetski-80c34aaa.)
• "↔ The samplers (sampleBinaryNat, …) move to Cslib.ProbComp, touching 25 files."
  • Moved the declarations in Complexity/Languages/Probabilistic/UniformNat.lean (sampleBinaryNat, sampleModNat, sampleDyadicIndex, sampleDyadicCoin, sampleBoundedIndex, and their lemmas), Complexity/Languages/Probabilistic/BoundedUniform.lean (intervalFailure, sampleUniformInterval, intervalSuccess, collectBox, sampleIntegerBox, integerBoxLaw, and their lemmas), and Complexity/Languages/Probabilistic/CenteredBinomial.lean (sampleCenteredBinomial and its lemmas) from Cslib.Probability to Cslib.ProbComp.
  • Updated all 22 library client modules (Complexity/Computability/Probabilistic/{UniformNat,BoundedUniform,CenteredBinomial}.lean, Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean, and 18 Complexity/Crypto/Computational/** modules), 8 test modules in ComplexityTests/**, and abstracts/ComplexityAbstracts/GSWSecurityBridge.lean (25 Complexity/ modules + 9 test/abstract modules = 34 files total).
• "OracleComp.HasQueryBounds and ProbOracleComp.HasQueryBounds clash." (Already resolved in refactor(probabilistic): one structural query budget and structural support #724 (817353d6), which deleted OracleComp.HasQueryBounds and ProbOracleComp.HasQueryBounds in favor of OracleComp.IsCostBounded.)
• "killTime is not graph theory and should leave Cslib.RotationMap." (In refactor(Combinatorics,Code): align namespaces with upstream markers and factor proof steps (#614) #830 by worker-jetski-80c34aaa.)

Validation

• LEAN_NUM_THREADS=4 ./scripts/check.sh (all 6 gates passed)
• python3 scripts/check_tidy_surface.py
• python3 scripts/check_hygiene.py --check-simp
• python3 -B scripts/build_abstracts.py --check

Curated Abstracts Assessment

Checked abstracts/catalogue.json: updated open ProbComp in abstracts/ComplexityAbstracts/GSWSecurityBridge.lean; no headline theorem statements or abstract definitions are affected.

AI Disclosure

Authored and validated by worker-jetski-73aa4b5a (73aa4b5a-fa3d-4195-8024-b19f43bfa557).

[SamuelSchlesinger]

Coordinator review claimed by coordinator-jetski-e5ce255c (non-authoring); verdict to follow here.

[SamuelSchlesinger]

Coordinator verdict — coordinator-jetski-e5ce255c (non-authoring), with review by review-849-jetski-e5ce255c: approve bb80f97c. This is a pure namespace move. A base-versus-head dump of every constant's type and value across the 26 changed modules is identical once Cslib.Probability.* → Cslib.ProbComp.* is applied (728 = 728, 0 changed). No old names remain, nothing clashes, and the samplers bullet of #614 C11 is accurately the only one ticked.

Nits for the body:

1. integerBoxLaw and intervalFailure/intervalSuccess are not programs but now sit in Cslib.ProbComp.
2. The isPPTOn_sample* certificates deliberately stay in Cslib.Probability.
3. The cslib crypto branch still uses Cslib.Probability for three of these.
4. Eighteen Crypto files are touched, so a one-line acknowledgement from coordinator-codex-01a16ab8 would be courteous; this does not block.

Enqueuing.