[chris-ai1]

Second slice of M2 of #474 (worker-crei-dc679113-474m2, Claude Code). It proves RL ⊆ RP, BPL ⊆ BPP and BPL ⊆ PSPACE, in a new module Classes/LogSpace/Randomized/BPP.lean. The PR is independent of #1665 (the configuration matrix) and does not use it.

Statements

theorem Cslib.Complexity.RL_subset_RP : RL enc ⊆ RP enc
theorem Cslib.Complexity.BPL_subset_BPP : BPL enc ⊆ BPP enc
theorem Cslib.Complexity.BPL_subset_PSPACE : BPL enc ⊆ PSPACE enc

Proof

1. An RL or BPL machine halts on every branch, so it halts within the derived polynomial clock 2 * (2 * (n + 1)) ^ d (exists_polyClock_of_mem_RL / exists_polyClock_of_mem_BPL, from M1b).
2. Its closed run for that clock is literally a Cslib.Probability.IsPPTOn witness, with the same machine and clock (2 * 2 ^ d) * (n + 1) ^ d.
3. Mapping the output through (· == [true]) keeps it PPT, by IsPPTOn.map with the plain ComputableInPolyTime.beq.
4. Its acceptance probability is acceptCoins input t / 2 ^ t (acceptCoins_eq_mul_eval, from M1c).
5. The PPT characterizations mem_PromiseRP_iff_exists_isPPTOn and mem_PromiseBPP_iff_exists_isPPTOn turn this into RL ⊆ RP and BPL ⊆ BPP.
6. BPL ⊆ PSPACE is BPP_subset_IP followed by IP_subset_PSPACE.

No tidy declaration is used and the tidy-surface baseline is unchanged.

Source → Lean mapping

These inclusions are original formal corollaries of the library's derived-clock and PPT bridges. Arora–Barak, Computational Complexity: A Modern Approach (2009), §7.7, Definition 7.18, printed p.139 supplies the class-definition background:

“The classes BPL and RL are the two-sided error and one-sided error probabilistic analogs of the class L defined in Chapter 4.”

The quotation was checked in the published book. It is not presented as an explicit source statement of these Lean inclusions.

Our RL/BPL use the #474 model: one-way coins, work space as for NL, acceptance by counting coin strings, and halting on every branch without a clock in the definition. M1b derives a polynomial clock with one exponent fixed before the input. The same machine and encoding then witness IsPPTOn; the [true] output test preserves PPT, and the acceptance count gives the verifier-class RP/BPP thresholds. No extra halting or time hypothesis is added.

BPL ⊆ PSPACE composes BPP_subset_IP with IP_subset_PSPACE, both already in the library. This is the IP ⊆ PSPACE direction; Shamir's direction is the reverse PSPACE ⊆ IP. The configuration matrix is not used here.

Tests

ComplexityTests/RandomizedLogSpace.lean:

• USTCON ∈ RP / BPP / PSPACE, via L ⊆ RL ⊆ BPL;
• Set.univ ∈ RP through the concrete coinFlip machine.

Validation

At 29b1fd32911d5276219e6a0f7ded361e0e037d0f:

• scripts/check.sh: all six gates ok;
• check_hygiene.py --check-simp, check_changed_files.py --base origin/main and check_tidy_surface.py: all passed.

Remaining in M2

BPL ⊆ P, by exact evaluation of the configuration matrix of #1665. It needs a polynomial-time certificate:

• breadth-first search for the reachable views;
• T rounds of binary vector updates.

That certificate would reuse the tidy NL ⊆ P machinery in Reachability.lean. That machinery must first be restated in plain form (#862), so this is a follow-up.

Curated abstract assessment: no selected statement, model, definition or scope changes; no new headline or PDF rendering is proposed.

Review

Independent source/API review covers this source. Integration follows #1653 and requires supported-rc2 refresh and an integration delta check. Codex corrected this description's source evidence and attribution using the checked book and library interfaces.

AI disclosure: written with Claude Code (Claude Opus 5.5): the Lean development, tests and this description.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval). Verdict: FINAL, advisory (same session as the authoring workers). Head 29b1fd32911d5276219e6a0f7ded361e0e037d0f, one commit on 96fd02a85 (current main).

Is the PPT witness honest?

• IsPPTOn (Probabilistic/PPT.lean:71) asks for a finite-state MultiTapePTM and c d such that (eval (program a)).map output = eval (machine.runClosed (c * (|a| + 1) ^ d) (enc a)).
• The witness gives exactly that with c = 2 * 2 ^ d, using 2 * (2 * (n + 1)) ^ d = (2 * 2 ^ d) * (n + 1) ^ d and output encBits = identity. So it really is the RL/BPL machine itself, run for the derived clock from exists_polyClock_of_mem_RL/_BPL (M1b).
• The (· == [true]) post-test goes through IsPPTOn.map with the plain ComputableInPolyTime.beq.

Do the acceptance conventions match?

• probability_runClosed_accepts turns Pr[output = [true]] into acceptCoins / 2 ^ t. It relies on acceptCoins_eq_mul_eval, which needs RunsInTime at that clock; (hM a).2.1 supplies it.
• RP: members are accepted with probability ≥ 1/2, from the RL count bound. For non-members, [true] is outside the support, because acceptCoins = 0 makes the evaluation 0. That matches the one-sided mem_PromiseRP_iff_exists_isPPTOn.
• BPP: members get ≥ 2/3. For non-members the rejection probability Pr[¬ accept] ≥ 2/3 comes from acceptance ≤ 1/3, via ProbComp.probability_not.
• ofSet_mem_Promise* converts back to the set classes.
• BPL_subset_PSPACE is IP_subset_PSPACE ∘ BPP_subset_IP, both on main.

Duplicates and tidy: there is no existing RL_subset_RP, BPL_subset_BPP, BPP_subset_PSPACE or BPL_subset_PSPACE on main, so these are new. No tidy declaration is used, and all imports are plain.

Tests: USTCON ∈ RP/BPP/PSPACE via L ⊆ RL/BPL, and Set.univ ∈ RP through the concrete coinFlip machine with its RL membership built inline. The RP test exercises the support (one-sided) branch nontrivially: there are no non-members, but the member branch uses the real count.

Citation: Arora–Barak Section 7.7 is "Randomized space-bounded computation", so the locator fits.

Limits: I did not build locally and am relying on the body's validation and on hosted CI.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732, with independent non-authoring review by /root/review_bpl_containments_1666 — APPROVE this revision. Agent review, not human approval.

The fixed machine and encoding, uniformly chosen polynomial exponent, strong all-branch halting clock and [true] output test give the stated strict-PPT witnesses and exact RP/BPP error thresholds. Other output words are rejection. The IP composition reaches ordinary deterministic PSPACE without an extra assumption. Concrete USTCON and fair-coin clients are checked; the earlier independent #1525 review covers the unchanged clock construction.

I corrected the description to present these as original formal corollaries, with the checked Arora–Barak class-definition quotation/locator as background, and corrected the Shamir direction. Existing curated abstracts and scope are unchanged; BPL ⊆ P remains open.

No local elaboration/build. Exact-head CI40959300862 passed; author reports all six local gates. Supported-rc2 refresh, checks and an integration delta after #1653 remain required.

[SamuelSchlesinger]

Complete — non-author integration coordinator review_logsq_savitch_1671: unchanged reviewed head 29b1fd32911d5276219e6a0f7ded361e0e037d0f landed at 2d1638ce2d1e192e8faa79436edf726df82bfeb0, reusing the independent source/API review. The actual candidate matched the clean preflight on the live #1668 prefix.

Required current-pin queue CI and landed-main CI passed all six gates and applicable source checks. Main restored the exact queue build and published the public cache mapping: GET 200, 4,004 entries, and HEAD 200 for all three newly referenced artifacts. No local Lean build or artifact-body download was used. The fixed machine/encoding, uniformly derived polynomial exponent, strong all-branch halting and rejection of other output words retain their reviewed scope. The broader #474 objective and the remaining BPL-to-P certificate/derandomization work remain open. This is agent integration stewardship, not a new mathematical or human approval.