From c8175d732b6094c04cbbd5c42aa1b833f6f3de8a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 02:26:36 -0400 Subject: [PATCH] =?UTF-8?q?doc(roadmap):=20drop=20landed=20BQP=20=E2=8A=86?= =?UTF-8?q?=20PP=20and=20narrow=20feasible=20interpolation=20to=20what=20r?= =?UTF-8?q?emains?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- ROADMAP.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 5123aac860..abca0af503 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -338,10 +338,10 @@ DLOGTIME-uniform AC⁰ under explicit conventions. - Proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares, and certified DPLL solver runtimes. -- **Feasible interpolation:** from a Resolution refutation of `A(x,y) ∧ B(x,z)`, construct a - circuit separating the `x` assignments extendible to `A` from those extendible to `B`, with - proof-size and extraction-time bounds. Prove the monotone variant under its polarity - hypotheses and transfer circuit and communication lower bounds to proof-size lower bounds. +- **Feasible interpolation** ([#1817]): extraction-time bounds for Resolution interpolants over + an explicit circuit encoding; a sharper monotone separator bound (Alon–Boppana) for a + stronger clique–coloring size lower bound; and the transfer of communication lower bounds to + proof-size lower bounds. - **Proof search:** automatizability and weak automatizability with explicit encodings and runtime dependence on the shortest proof; proof-search reductions built on the Cook–Reckhow and p-simulation APIs; then reflection principles and bounded-arithmetic witnessing theorems. @@ -455,7 +455,7 @@ each statement against the numbered result. Organize modules by subject, not cha `Kolmogorov/Conditional.lean`, and `Kolmogorov/MINcKT.lean`), as independently scoped developments; the reverse multi-tape-to-single-tape simulation and machine-backed Nisan–Wigderson decoding. -- **Quantum computation** ([#896]): BQP ⊆ PP; reusable +- **Quantum computation** ([#896]): reusable circuit, channel and measurement semantics with uniformity and approximation costs, reusing suitable quantum foundations rather than incompatible models; BQP, QMA and related query, communication and interactive classes, with amplification, containments and complete @@ -868,5 +868,6 @@ not planned, not as proved. [#1449]: https://github.com/cslib-community/complexitylib/issues/1449 [#1524]: https://github.com/cslib-community/complexitylib/issues/1524 [#1572]: https://github.com/cslib-community/complexitylib/issues/1572 +[#1817]: https://github.com/cslib-community/complexitylib/issues/1817 [#1819]: https://github.com/cslib-community/complexitylib/issues/1819 [#1824]: https://github.com/cslib-community/complexitylib/issues/1824