# Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Exact derandomization of logarithmic space: L = RL = BPL](../../preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/paper.pdf)

## Scope

The formalization proves $\mathsf L=\mathsf{RL}=\mathsf{BPL}$ for binary languages in an explicit Turing-machine model with logarithmic workspace. The randomized classes use polynomial time: $\mathsf{RL}$ never accepts a no-instance and accepts a yes-instance with probability at least $1/2$, while $\mathsf{BPL}$ has acceptance probability at least $2/3$ on yes-instances and at most $1/3$ on no-instances. Thus bounded-error randomness does not enlarge deterministic logarithmic space in this model.

The selected theorem asserts equality of the language classes. The paper's explicit compiler and numerical running-time bounds are not separately stated in this Comparator target.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Exact equality of deterministic and randomized logarithmic space | [LogspaceEquality.lean](../ComparatorChallenges/LogspaceEquality.lean) |