From 92ebefd054284b1cb0879c58fef87fa63f8c9a79 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:48:50 -0400 Subject: [PATCH] doc(abstracts): list every catalogue entry in the READMEs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The top-level README's "Selected results" listed 17 of the 22 catalogue entries. It omitted Gentry–GSW FHE, Chor–Goldreich, the ETH refutation, Limaye–Srinivasan–Tavenas and Braverman. Its Partial MCSP line also lacked the false-premise note that the catalogue and abstracts/README.md carry. abstracts/README.md said "twenty" groups and its table had no rows for Braverman (#1614) or Limaye–Srinivasan–Tavenas (#1569). Add the missing entries in catalogue order and the Partial MCSP note. Replace the hard-coded count so the next selection cannot make it stale. New lines reuse the catalogue titles and summaries or scopes. Where a summary is long, the line uses a shorter paraphrase of the abstract's statement. Found by auditor-claude-e6cf7b0d-11 (misformalization audit, round 11). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- README.md | 7 ++++++- abstracts/README.md | 8 +++++--- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 17745c7f6..7bbf3fe9d 100644 --- a/README.md +++ b/README.md @@ -62,12 +62,17 @@ the selection is not an exhaustive API reference. * [Toda: a counting oracle decides the polynomial hierarchy](abstracts/ComplexityAbstracts/TodaAbstract.lean): Every problem in the polynomial hierarchy is decidable in polynomial time with an exact counting oracle. * [Barrington: five states capture NC¹](abstracts/ComplexityAbstracts/BarringtonAbstract.lean): Polynomial-length permutation programs on five states capture logarithmic-depth polynomial-size Boolean circuits. * [Håstad and Razborov–Smolensky: parity resists shallow circuits](abstracts/ComplexityAbstracts/ConstantDepthAbstract.lean): At fixed depth, parity requires more than polynomially many gates, including over an odd-prime modular basis. +* [Braverman: polylogarithmic independence fools AC⁰](abstracts/ComplexityAbstracts/BravermanAbstract.lean): k-wise independence with k = (log(m/ε))^O(d²) fools every depth-d circuit of NOT and unbounded fan-in AND/OR gates with size and fan-in at most m, to within error ε. * [Formula lower bounds: parity and Andreev](abstracts/ComplexityAbstracts/FormulaBoundsAbstract.lean): Tree-shaped computation pays for repeated work: parity requires quadratic leaf size, and Andreev gives a stronger explicit bound. +* [Limaye–Srinivasan–Tavenas over any field (after Forbes): constant-depth algebraic circuits for IMM need superpolynomial size](abstracts/ComplexityAbstracts/ConstantDepthArithmeticAbstract.lean): Over every field, constant product-depth simple algebraic circuits computing iterated matrix multiplication of ⌊log₂ ⌊log₂ n⌋⌋ generic n × n matrices need more than n^c gates for every c and all large n. * [One-way functions yield pseudorandom generators and adaptive functions](abstracts/ComplexityAbstracts/CryptographyAbstract.lean): One-wayness yields pseudorandomness, from an extra output bit to functions secure against adaptive oracle queries. +* [Gentry and GSW: fully homomorphic encryption from LWE](abstracts/ComplexityAbstracts/GSWFHEAbstract.lean): Bootstrapping the GSW scheme gives leveled fully homomorphic encryption from decision LWE, and fully homomorphic encryption under an additional circular-security assumption. * [Haken: pigeonhole formulas require long resolution proofs](abstracts/ComplexityAbstracts/ResolutionAbstract.lean): The pigeonhole principle has short CNF statements but requires exponentially many resolution lines. * [Communication: disjointness and inner product resist randomness](abstracts/ComplexityAbstracts/CommunicationAbstract.lean): Both problems require linearly many communicated bits even with shared randomness and bounded error. * [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](abstracts/ComplexityAbstracts/SipserLautemannAbstract.lean): Bounded-error polynomial time admits both existential–universal and universal–existential polynomial descriptions. -* [Ilango: Partial MCSP is hard under the Exponential Time Hypothesis](abstracts/ComplexityAbstracts/PartialMCSPAbstract.lean): Under ETH, deciding circuit size for partial Boolean functions cannot be done in time 2^o(m log m) = N^o(log log N). +* [Chor–Goldreich: the inner product extracts from two weak sources](abstracts/ComplexityAbstracts/ChorGoldreichAbstract.lean): Two independent weak random sources whose min-entropies add up to more than the string length give a nearly fair bit through the inner product modulo two. +* [OpenAI: the Exponential Time Hypothesis is false](abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean): For each fixed clause width, one deterministic machine exactly counts satisfying assignments in subexponential time and polynomial space; every fixed-width SAT exponent is zero, and ETH and SETH are false. +* [Ilango: Partial MCSP is hard under the Exponential Time Hypothesis](abstracts/ComplexityAbstracts/PartialMCSPAbstract.lean): Under ETH, deciding circuit size for partial Boolean functions cannot be done in time 2^o(m log m) = N^o(log log N). *Note (October 2026):* the native formalization now [proves ETH false](abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean). This conditional entry is retained and its theorem remains valid, but its premise is false. * [McKay–Murray–Williams: barely superlinear circuit lower bounds for MCSP separate P from NP](abstracts/ComplexityAbstracts/MagnificationAbstract.lean): If NP has polynomial-size circuits, then MCSP on 2^n-bit truth tables has circuits of size 2^n poly(n + s(n)); hence barely superlinear MCSP lower bounds separate NP from P/poly and P from NP. ## Build and use diff --git a/abstracts/README.md b/abstracts/README.md index b2e7015dd..d49e1a9c5 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -1,8 +1,8 @@ # Selected formal abstracts -The catalogue promotes twenty major result groups. Each has a checked Lean abstract with the -definitions needed to understand its statement, a bridge to the library proof, and an audited -dependency boundary. Some abstracts also allowlist a few library modules for foundational models +The catalogue promotes a small set of major result groups, listed in the table below. Each has a +checked Lean abstract with the definitions needed to understand its statement, a bridge to the +library proof, and an audited dependency boundary. Some abstracts also allowlist a few library modules for foundational models (for example circuit signatures or oracle runs); each such abstract names them in its docstring, and a reader must inspect them as well. The generated PDFs present the mathematical definitions and selected statements first, followed by exact representation details and any shared foundations in @@ -42,7 +42,9 @@ former paper/TeX index is retired; Git history retains its sources. | [Toda: a counting oracle decides the polynomial hierarchy](ComplexityAbstracts/TodaAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/toda.pdf) | Witness counts and oracle bit answers are explicit; correctness holds for every extension of valid oracle answers. | | [Barrington: five states capture NC¹](ComplexityAbstracts/BarringtonAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/barrington.pdf) | Nonuniform circuits and permutation programs; no uniform generator or compiler runtime is asserted. | | [Håstad and Razborov–Smolensky: parity resists shallow circuits](ComplexityAbstracts/ConstantDepthAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/constant-depth.pdf) | Explicit finite bounds, gate semantics and depth conventions; nonuniform lower bounds. | +| [Braverman: polylogarithmic independence fools AC⁰](ComplexityAbstracts/BravermanAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/braverman.pdf) | Arbitrary distributions with uniform marginals on every set of at most k positions; explicit bound with our own constants and exponent, weaker than Braverman's; size and depth count NOT gates and constants; one parameter q bounds the size, the fan-in and log₂ of the inverse error; nonuniform and information-theoretic. | | [Formula lower bounds: parity and Andreev](ComplexityAbstracts/FormulaBoundsAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/formula-bounds.pdf) | De Morgan formulas, literal leaves, explicit block indexing and finite quantitative bounds; no general-circuit lower bound. | +| [Limaye–Srinivasan–Tavenas over any field (after Forbes): constant-depth algebraic circuits for IMM need superpolynomial size](ComplexityAbstracts/ConstantDepthArithmeticAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/constant-depth-arithmetic.pdf) | Any field, formal polynomials, unbounded fan-in sum and product gates, product gates reading distinct wires, size counting all gates; explicit non-asymptotic bound with exponent d^(1/(4^Δ-1)); constant product-depth Δ and the single value d = ⌊log₂ ⌊log₂ n⌋⌋; nonuniform. | | [One-way functions yield pseudorandom generators and adaptive functions](ComplexityAbstracts/CryptographyAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/cryptography.pdf) | Uniform probabilistic polynomial time with explicit native evaluators, negligible advantage and full stateful oracle semantics; asymptotic security, not a concrete implementation audit. | | [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | Explicit GSW algorithms at an LWE family with quasi-polynomial modulus, the GSW key law for the leveled scheme's fresh ciphertexts and Gentry's self-loop key; an existential evaluator, remaining key chain and decryption circuits with correctness, fixed widths, uniformly generated polynomial-size decryption circuits, native algorithms and IND-CPA; circular security as a separate hypothesis. | | [Haken: pigeonhole formulas require long resolution proofs](ComplexityAbstracts/ResolutionAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/resolution.pdf) | The non-onto pigeonhole formula and a line-based resolution rule, with bound 2^(floor(n/24)); proof size is not solver runtime. |