From 8ea02ff44538da5f3aa6741c6d56f11f0df46610 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 01:38:37 -0400 Subject: [PATCH] =?UTF-8?q?doc(LogSpace):=20point=20the=20BPL=20=E2=8A=86?= =?UTF-8?q?=20P=20remarks=20at=20BPL=5Fsubset=5FP?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two module docstrings predate #1672 and still say that BPL ⊆ P by exact evaluation of the configuration matrix is not proved or formalized. It is `Cslib.Complexity.BPL_subset_P` in `LogSpace/Randomized/PolyTime`. Found by `auditor-claude-e6cf7b0d-14`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/LogSpace/Randomized/BPP.lean | 5 +++-- .../Classes/LogSpace/Randomized/ConfigurationMatrix.lean | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/BPP.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/BPP.lean index 29370b067a..2ccc91b1cb 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/BPP.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/BPP.lean @@ -31,8 +31,9 @@ programs (`Cslib.Complexity.mem_PromiseRP_iff_exists_isPPTOn`, (`Cslib.Complexity.BPP_subset_IP`, `Cslib.Complexity.IP_subset_PSPACE`) this gives `BPL ⊆ PSPACE`. -The stronger inclusion `BPL ⊆ P`, by exact evaluation of the configuration matrix, is not -proved here. +The stronger inclusion `BPL ⊆ P`, by exact evaluation of the configuration matrix, is +`Cslib.Complexity.BPL_subset_P` in +`Complexity.Computability.Complexity.Classes.LogSpace.Randomized.PolyTime`. ## Main results diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean index a81a7f8a1d..7f4b270010 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean @@ -43,8 +43,9 @@ machine on its configurations [Gill][Gill1977]. Borodin, Cook and Pippenger comp and inverse in parallel [Borodin, Cook and Pippenger][BorodinCookPippenger1983], which gives `BPSPACE(S) ⊆ DSPACE(S²)` [Hoza, Section 4.3][Hoza2022]; the inverse of `1 - W` as the sum `W⁰ + W¹ + …` of transition-matrix powers is the picture of [Hoza, Section 3.2][Hoza2022]. -Exact evaluation of the polynomial-size matrix also gives `BPL ⊆ P`. None of these algorithms is -formalized here. +Exact evaluation of the polynomial-size matrix also gives `BPL ⊆ P`. The parallel algorithms are +not formalized; a sequential exact evaluation, which gives `Cslib.Complexity.BPL_subset_P`, is in +`Complexity.Computability.Complexity.Classes.LogSpace.Randomized.PolyTime`. The matrices are indexed by an arbitrary closed set of views rather than a set of configurations of bounded size, and have no time layers: the model of `Cslib.Complexity.BPL`