plan(logspace): BPL ⊆ L via the OpenAI preprint route (M7 of #474) #1444

Split out of #474 (milestone M7), on @crei's decision of 2026-10-28.

Status: the source is an unrefereed preprint, so this issue follows an unrefereed result. The machine model is fixed in #474 (#474), and Phase 0 / M1 is #459. Phases 1–7 below are the M7 plan from #474's body, unchanged. The provenance table of ideas stays in #474.

Goal

Prove BPL ⊆ L, hence L = RL = BPL, natively in complexitylib. The proof transfers the proof ideas of the OpenAI preprint into our own definitions and infrastructure. It does not vendor or translate their Lean code, theorems or lemmas.

Source (from #474)

Source and status

The claim. OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL, preprint dated 2026-09-23, in https://github.com/openai/math, preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/paper.pdf. It is a 106-page paper. It has not been peer reviewed, and as far as I know it has not yet been reviewed by the community.

Their Lean proof. lean/OAI/Computability/Logspace at 1581d4cb is 39 modules, about 43k lines, depending only on Mathlib. Its statement is fixed by lean/ComparatorChallenges/LogspaceEquality.lean.

• I built it independently, in an isolated scratch project, on their pin (Lean v4.34.1 with their Mathlib) and also unmodified on complexitylib's pin (v4.36.0-rc1, Mathlib 625d8914).
• Both builds succeed with no errors.
• #print axioms on the main theorem reports only propext, Classical.choice and Quot.sound.
• The challenge definitions describe the standard polynomial-time RL and BPL with one-way coins. They are character-identical in the solution.

Why not vendor their code.

• It has about 18.7k warnings under our linter settings and uses autoImplicit true.
• Its names are opaque (Umbra, Rock, Helix.Moon).
• About 60% of it is a bespoke compiler for space-bounded programs, which duplicates what our read-machine pipeline already provides.

It cannot meet the rule that every module must be upstreamable.

The Lean route is simpler than the paper's, and this plan follows the Lean route:

• No property (T): an elementary Fourier spectral gap instead.
• 4th moments instead of 8th.
• No fingerprinting: an exact catalytic identifier comparison instead.
• No median: average over all environments and compare with a threshold.
• Fixed precision only.

Phases

Each phase is its own module group and its own implementation issue. Statements and names are ours; the OpenAI preprint is cited for the ideas.

Phase 0: classes (#459 M1). RL and BPL for MultiTapePTM, with the basic inclusions.

Phase 1: configuration graph (idea 1).

• For a space-bounded MultiTapePTM: a time-layered, box-truncated configuration matrix S, with acceptance probability = ((I − S)⁻¹ e)(start).
• Entries and paired ports are locally computable from encoded configurations.
• Builds on cslib ConfigBound and our encodings.
• Also yields BPL ⊆ PSPACE and BPL ⊆ P for plan(logspace): randomized logspace — RL and BPL, inclusions, USTCON ∈ RL, Nisan's generator #459.

Phase 2: correction-and-copy hierarchy (ideas 2–4). Pure linear algebra on finite, strictly forward, substochastic matrices, with no machines:

• the factorization identity;
• factorial truncation;
• detectors and copies;
• the stage bound 0 ≤ p(x) − W_k(x̄_k) ≤ |V|·2^{−c k}.

This is the most reusable and readable piece.

Phase 3: sampling environment (ideas 5, 7′, 8, 9).

• Retention channels by polynomial hashing over 𝔽_P.
• The uniform Fourier ping-pong gap for shear and translation moves, stated through our Expander API (spectral expansion, the Lazy graph, Mixing, AffinePlane).
• Contraction in L⁴.
• Conditional averaging on retention slices.

Phase 4: the estimator as mathematics (ideas 6, 10–12).

• A recursive function of the environment, with stochastic atoms, slack-scaled telescoping differences, source release and compression.
• Error bound in the L⁴ norm, by strong induction on the budget.
• No space accounting yet.

Phase 5: catalytic comparison (idea 14). A general lemma: reversible register updates that restore borrowed memory and test equality exactly. It belongs next to the Cook–Mertz registers (TreeEval/CookMertz).

Phase 6: space realization (ideas 15–17).

• An iterative frame stack, as in TreeEval/Iterative, whose frames satisfy the telescoping allowance.
• A Turing.ReadMachine, certified step by step into a tidy multi-tape machine, as in TreeEval/Reader/* and USTCON/Reader/*.
• Digit-stream arithmetic, and a prime search reusing the one in the TreeEval reader.
• Our read-machine pipeline replaces the 28k-line program compiler of the OAI Lean development.

Checkpoint. Before the full O(log n) bound, a first realization could store complete identifiers in each of the O(log n) frames, with no catalytic comparison and no allowance accounting. I expect this to give BPL ⊆ DSPACE(log² n), a classical result (Borodin–Cook–Pippenger; Nisan), as a fully verified intermediate theorem. The upgrade to O(log n) then isolates exactly ideas 14 and 17.

Phase 7: decision (ideas 18–19).

• Average over all environments and compare with 1/2, giving BPL ⊆ L.
• Then L = RL = BPL.
• Abstract and catalogue entry, ROADMAP, theorem index.

Dependencies

• Phases 2, 3 and 5 are independent and can start in parallel, alongside Phase 0.
• Phase 1 needs Phase 0.
• Phase 4 needs Phases 2 and 3.
• Phase 6 needs Phases 1, 4 and 5.
• Phase 7 needs everything.

Phase 6 is by far the largest part and carries most of the engineering risk.

Decisions for review

1. Wording. Until the preprint has been reviewed, ROADMAP and the catalogue should present the result as "formalized following a recent preprint", with the provenance above.
2. Route. Follow the Lean route: elementary gap, no fingerprints, average instead of median, fixed precision. Do not formalize the paper's general-precision and compiler extensions (Theorem 1.2 with arbitrary precision, §13).
3. Phase split and checkpoint. Should the log² n checkpoint be a required milestone?
4. Bibliography. Add the preprint and the pre-existing sources above (Ben-Or–Cleve 1992, Gabber–Galil 1981, Burger 1991, Giles 2008, Heinrich 2001, Chor–Goldreich 1989, Gillman 1998, Cook–McKenzie 1987, Avizienis 1963, Shalom 1999) to references.bib as phases land.

Relation to the classical track in #474

• The classical milestones are M1–M6: definitions, the configuration matrix, RL ⊆ L², BPL ⊆ L², Nisan's generator and Saks–Zhou. They stay in plan(logspace): formalize BPL ⊆ L natively, transferring the proof ideas of the OpenAI preprint #474.
• This issue shares M1 (plan(logspace): randomized logspace — RL and BPL, inclusions, USTCON ∈ RL, Nisan's generator #459) and M2, the configuration matrix (= Phase 1 here).

Status: available for design review. Not ready to implement until each phase has its own issue.