From 2e06b65873f07c132dfa8cf8849977bf9790416a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 22:36:52 -0400 Subject: [PATCH 1/3] doc(roadmap): rewrite as a short plan of open directions Rewrite ROADMAP.md as a forward-looking plan of directions only, grouped by area, with links to the tracking issues (#897 and its tracks, #862, #798, issues, PRs, module docstrings and the README hold them. Every open direction is kept, and open items without an issue stay as direction lines. Four open directions recovered from the closed area checklists are added. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ROADMAP.md | 2149 ++++++++++------------------------------------------ 1 file changed, 409 insertions(+), 1740 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 107acf6a40..304bd97b4e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1,1747 +1,416 @@ -# Development roadmap +# Roadmap -Outstanding work and the rationale needed to guide it. See the [README](README.md) for -completed reference developments. +The directions Complexitylib aims to cover, grouped by area. This file lists directions only: +status, progress and completion notes live on the linked issues and pull requests, module +docstrings describe what is proved, and the [README](README.md) and the curated formal abstracts +present completed results. A PR edits this file when it opens or closes a direction. -## Deferred issue scopes +A direction is complete only when its machine, resource and quantitative conclusions are proved +for the actual algorithms, with explicit models, encodings and assumptions. An abstract algorithm, +a class definition or an assumed reconstruction theorem does not complete it. Search Mathlib, +CSLib and this library before starting, and check upstream work. -The following broad projects remain mathematical coverage targets, but are deferred from the -active implementation queue. Their issues were closed as not planned, not as proved results; -existing developments, source credit and saved branches remain available for a future bounded task. +## Programs -* [Valiant permanent completeness (#321)](https://github.com/cslib-community/complexitylib/issues/321): - the full VNP-completeness reduction remains open. -* [General auxiliary-input zero knowledge (#324)](https://github.com/cslib-community/complexitylib/issues/324): - the uniform polynomial-time-family milestone is proved; the stronger endpoint below remains open. -* [Williams's square-root-space simulation (#361)](https://github.com/cslib-community/complexitylib/issues/361) - and [implicit Tree Evaluation (#367)](https://github.com/cslib-community/complexitylib/issues/367): - existing algebraic and query-machine results remain proved, while the implicit evaluator and - full simulation are deferred. -* [Vollmer's generalized-quantifier survey (#399)](https://github.com/cslib-community/complexitylib/issues/399): - source and dependency mapping is available, but the paper has not been formalized as a whole. - Faithful treatment requires ordered leaf words, explicit uniformity and input-access models, - finite-monoid classification and generalized logical quantifiers. - -## Highest priorities - -1. **Goldreich–Micali–Wigderson zero knowledge.** If one-way functions exist, every language in NP - has an interactive computational zero-knowledge proof system, secure against probabilistic - polynomial-time verifiers with auxiliary input. - - *Partial:* [Commitment](Complexity/Crypto/Computational/Commitment.lean) proves Naor's - two-message bit commitment scheme (`naorCommit`, `naorBitCommitment`, - `OneWay.exists_bitCommitmentScheme`) with statistical binding and computational hiding against - randomized stateful PPT receivers (`CommitmentReceiver`, `commitmentHidingGame`, - `StatefulHiding`, `PseudorandomGenerator.naorStatefulHiding`, with - `StatefulHiding.computational_hiding` bridging to deterministic polynomial-time receiver-string - and bit families), and - [ZeroKnowledge](Complexity/Crypto/Computational/ZeroKnowledge.lean) - ([GMW/Protocol](Complexity/Crypto/Computational/GMW/Protocol.lean), - [GMW/Soundness](Complexity/Crypto/Computational/GMW/Soundness.lean), - [GMW/PolyTime](Complexity/Crypto/Computational/GMW/PolyTime.lean), - [GMW/Simulator](Complexity/Crypto/Computational/GMW/Simulator.lean)) proves a two-round - 3-copy masked-3SAT truth-table commitment zero-knowledge proof system for `ThreeSAT` and every - `A ∈ NP` (`ZeroKnowledgeProof`, `zeroKnowledgeProofThreeSAT`, - `OneWay.exists_zeroKnowledgeProof_of_mem_NP`) from any uniform one-way function via HILL and - Cook–Levin, with uniform zero knowledge (`GenerableZeroKnowledge`, - `ZeroKnowledgeProof.generableZeroKnowledge`) over deterministic polynomial-time-generable - instance/witness/auxiliary-input families `(x n, w n, z n)` (and fixed-instance security via - `zero_knowledge_const`) at soundness error `1 / 3` (the proof bounds it by `1 / 8 + 2^{-(n+8)}`). Because the - auxiliary input is a deterministic polynomial-time function of `1^n`, this does not reach the - general auxiliary-input statement above. - - *Pointwise reduction and auxiliary-input interface milestones (#427, #698):* - `GMW.gmwView_advantage_le` bounds every valid instance/witness/auxiliary tuple by - `(7/8)^(n+1)` plus `dyadicSize(n+1) * dyadicSize(totalLen(f a))` times one concrete - PRG-challenge advantage at seed size `n+7`. The final test receives `(n,a,z,view)`; - `isPPTOn_gmwViewReduction` charges the complete encoded tuple and challenge, including - adaptive queries and retained verifier randomness/state. `AuxiliaryInputZeroKnowledge` - (`ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`) states the general auxiliary-input notion - for arbitrary polynomially bounded valid families against full-input uniform strict PPT - distinguishers, with the stronger-to-restricted bridge - `AuxiliaryInputZeroKnowledge.generableZeroKnowledge`. Under the explicit advice-PRG premise - `GMW.AdvicePRG` (`gmwView_negligible_of_advice_prg`), the GMW proof systems satisfy - `ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge` - (`PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction`, - `PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP`). - No implication from current uniform one-wayness/HILL to `GMW.AdvicePRG` is proved. The direct - pad-replacement proof does not require the separate Naor commitment-hiding theorem. - - *Open (this priority):* zero knowledge in Goldreich's sense (Def. 4.3.10), for every - `x ∈ L` with arbitrary auxiliary input `z` against probabilistic polynomial-time verifiers; - witness-level Levin reductions; and sequential soundness amplification to negligible error. - The full auxiliary-input convention still needs a formal security-premise/clock bridge: - polynomial time in total encoded input, used in #427, differs from a clock independent - of an unbounded auxiliary word. The pointwise milestone does not complete this objective. -2. **Rompel’s signature theorem.** One-way functions exist if and only if digital signature schemes - exist that are existentially unforgeable under adaptive chosen-message attacks by probabilistic - polynomial-time adversaries. - - *Partial:* [Signature](Complexity/Crypto/Computational/Signature.lean) defines uniform strict - PPT signature schemes for exactly `n`-bit messages at security parameter `n`, adaptive EUF-CMA - and one-time EUF-CMA, and proves full security implies one-time security. - [OneWayToSignature](Complexity/Crypto/Computational/OneWayToSignature.lean) proves secure - signatures imply one-way functions and constructs Lamport one-time signatures from any - one-way function, giving `exists_oneWay_iff_exists_oneTimeSignature`. - - *Open:* the many-time sufficiency direction from arbitrary one-way functions, including - universal one-way hash functions and authentication trees. The one-time equivalence does not - establish Rompel's full theorem or security for arbitrary polynomial-length messages. -3. **Gentry’s bootstrapping theorem.** A semantically secure, bootstrappable encryption scheme - yields compact leveled fully homomorphic encryption for every polynomially bounded circuit - depth. Here bootstrappability requires homomorphic evaluation of suitably augmented decryption - circuits. With an appropriate additional circular-security assumption, the construction yields a - fixed-key fully homomorphic scheme without a predetermined depth bound. - *Recovery milestones:* [refresh](Complexity/Crypto/Computational/Homomorphic/Refresh.lean) - constructs identity and NAND refresh from actual decryption circuits and proves correctness - for arbitrary well-sized old ciphertexts, including prior evaluation outputs, with fixed - output width. [Efficiency](Complexity/Crypto/Computational/Homomorphic/Efficiency.lean) - derives strict PPT refresh from base encryption/evaluation certificates and a uniform - decryption-circuit generator; construction of the NAND augmentation is also certified. - [KeyChain](Complexity/Crypto/Computational/Homomorphic/KeyChain.lean) constructs the actual - sampler with `L + 1` independent key pairs and `L` adjacent encrypted links, with exact support - and native PPT certificates. The [layered evaluator](Complexity/Crypto/Computational/Homomorphic/Layered.lean) - uses only public keys and encrypted links. Its - [correctness theorem](Complexity/Crypto/Computational/Homomorphic/Layered/Correctness.lean) - covers every well-formed consecutive-layer program and every supported key chain and output, - preserving exact wire counts and ciphertext widths through one key transition per layer. - Its [PPT certificate](Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean) - charges the complete public encoding, including binary wire indices, and bounds execution - even on malformed keys, links and references. - The [circuit compiler](Complexity/Computability/Circuit/Boolean/Layered/Compile.lean) - turns a shared De Morgan circuit with `s` gates, `n` inputs and designated-output depth `d` - into exactly `2d` layers, each of width `n + 3s`, followed by ordered output wiring. - [Correctness](Complexity/Computability/Circuit/Boolean/Layered/Compile/Correctness.lean) - preserves its semantics, including unused gates, repeated outputs and depth-zero wiring; - [size bounds](Complexity/Computability/Circuit/Boolean/Layered/Compile/Size.lean) charge - every binary reference and encoding delimiter. Its - [native certificate](Complexity/Computability/Circuit/Boolean/Layered/Compile/PolyTime.lean) - computes the depth table and schedule uniformly across arities, including malformed raw codes. - [Ordinary encrypted evaluation](Complexity/Crypto/Computational/Homomorphic/Evaluation.lean) - composes the compiler and layered evaluator along a generated chain of `2d + 1` keys, retaining - exact ciphertext width. Its - [PPT certificate](Complexity/Crypto/Computational/Homomorphic/Evaluation/PolyTime.lean) - covers the complete public input without correctness or validity assumptions. - The [depth-budgeted scheme](Complexity/Crypto/Computational/Homomorphic/Leveled/Basic.lean) - generates `2B + 1` base keys for budget `B`. It uses - [identity-layer padding](Complexity/Computability/Circuit/Boolean/Layered/Padding.lean) so every - circuit of designated-output depth at most `B` finishes under the same final key. Its public - artifact contains public keys and adjacent encrypted links; its private artifact retains the - initial and final secrets. A tag distinguishes fresh from evaluated ciphertexts, adapting the - two endpoints to the existing `Scheme.Correct` interface. There is no circular encrypted link. - [Correctness](Complexity/Crypto/Computational/Homomorphic/Leveled/Correctness.lean) proves this - interface for the actual algorithms on fresh inputs. Exact secret-key and ciphertext lengths - are `3 * secretWidth n + 1` and `ciphertextWidth n + 1`, independent of `B`. This does not - promise that evaluated wrapper ciphertexts can be reused as fresh inputs to another call. - [Native certificates](Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean) - cover serialization, total decoding, compilation, padding and tagged decryption on all inputs, - uniformly in unary `(n, B)`. They yield efficient schemes for efficiently computed unary budget - families. The decryption-circuit generator also supplies polynomial bounds on both derived - widths; decryption itself has no budget parameter. - [Compactness](Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean) gives one - polynomial-size circuit family and common polynomial time and space bounds in the security - parameter for the complete tagged decryption algorithm, including endpoint decoding and tag - selection. The circuit family and resource bounds are independent of every budget and requested - depth family and cover all inputs of the prescribed widths, including malformed secrets. The - circuit result proves nonuniform existence; it does not provide a generator for these wrapper - circuits. - [Refresh tests](ComplexityTests/Crypto/HomomorphicRefresh.lean), - [layered tests](ComplexityTests/Crypto/HomomorphicLayered.lean), and - [ordinary-circuit tests](ComplexityTests/Crypto/HomomorphicEvaluation.lean) instantiate the - construction and runtime hypotheses in an explicitly insecure scheme whose base evaluator - rejects evaluated inputs. They exercise key switching, repeated refresh, shared wires, constants, - empty layers and zero depth. [Compiler tests](ComplexityTests/CircuitLayering.lean) also cover - dead gates, empty outputs, shared OR gates, skipped depths, and malformed binary references. - [Leveled tests](ComplexityTests/Crypto/HomomorphicLeveled.lean) check budgets zero, one and two, - distinct initial/final secrets at positive budgets, and circuits of different actual depths - under the same endpoint, malformed inputs and nonconstant efficient budget families. - The [IND-CPA reduction](Complexity/Crypto/Computational/Homomorphic/Leveled/Security.lean) - proves security of the actual serialized leveled scheme against uniform native two-stage - adversaries. It assumes base IND-CPA security, native key generation and encryption, fixed - supported secret length, and an efficient unary budget. The adversary chooses its messages - after seeing the entire public artifact and retains its exact saved state. The - [key-chain reduction](Complexity/Crypto/Computational/Homomorphic/KeyChain/Security.lean) - erases links in reverse order with uniform link/bit sampling and an executable polynomial - cap derived from native key generation; no circular-security or efficient-width premise is - used. The [combined theorems](Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean) - give correctness, exact polynomial widths independent of the budget, and IND-CPA for the - same constructed scheme. `Leveled.exists_scheme_of_polynomiallyBounded` covers every - `PolynomiallyBounded` requested depth family by selecting a computable unary budget - `c * (n + 1)^d` that dominates it at every parameter, including its finite prefix. The requested - family need not be computable: the algorithms execute the majorant. The theorem supplies native - certificates for all four algorithms and permits every circuit within the requested depth. - [Endpoint tests](ComplexityTests/Crypto/Bootstrapping.lean) cover arbitrary predicate-dependent - depth families, large finite-prefix spikes, and the full tagged decoder's compactness, while - retaining the security assumptions explicitly. - [Key-chain tests](ComplexityTests/Crypto/KeyChainSecurity.lean) and - [leveled security tests](ComplexityTests/Crypto/LeveledSecurity.lean) exercise repeated random - keys, retained encryption randomness, adaptive saved state, empty secrets, zero links and padding. - This is a qualitative single-challenge security transfer, not Gentry's exact - concrete-security bound. - The [fixed-key construction](Complexity/Crypto/Computational/Homomorphic/FixedKey/Basic.lean) - samples one base key and encrypts its secret bits under that same public key. Key generation - has no circuit or depth parameter; the public artifact is reused at every compiled layer. - [Correctness](Complexity/Crypto/Computational/Homomorphic/FixedKey/Correctness.lean) covers - all finite Boolean circuits and arbitrary well-sized decrypting inputs, including prior - evaluation outputs. Secret and ciphertext widths are exactly the original base widths. - [Native certificates](Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean) - cover all four actual algorithms and the complete encoded circuit and input data, including - malformed artifacts. The uniform decryption-circuit generator bounds both widths and the - unchanged decryption-circuit size polynomially in the security parameter. - [Security](Complexity/Crypto/Computational/Homomorphic/FixedKey/Security.lean) assumes base - IND-CPA and the explicit [one-key circular experiment](Complexity/Crypto/Computational/Encryption/Circular.lean): - the public key and complete vector of secret-bit encryptions must be jointly indistinguishable - from the corresponding zero encryptions. This fixed-query assumption does not assert general - adaptive KDM security. The [combined theorem](Complexity/Crypto/Computational/Homomorphic/FixedKey/Bootstrapping.lean) - proves correctness, compactness, native efficiency and IND-CPA for the same fixed-key scheme. - [Construction tests](ComplexityTests/Crypto/HomomorphicFixedKey.lean) check repeated evaluation - under one key, even though the explicitly insecure base fixture rejects evaluated inputs. - [Security tests](ComplexityTests/Crypto/FixedKeySecurity.lean) reject joint leakage hidden by - identical ciphertext marginals and keep a security-only fixture's failed correctness explicit. - Together these establish the generic qualitative conditional bootstrapping theorem tracked in - [#322](https://github.com/cslib-community/complexitylib/issues/322). A concrete LWE-based - cryptosystem satisfying its correctness, security, bootstrappability and native efficiency - hypotheses remains open in [#486](https://github.com/cslib-community/complexitylib/issues/486). - The insecure construction fixtures and security-only fixtures do not supply that joint - instantiation. The reductions do not claim Gentry's exact concrete-security loss. - The [deterministic GSW core](Complexity/Crypto/Computational/Homomorphic/GSW/Basic.lean) - constructs the public matrix, encryption with explicit binary coins, NAND and decryption for - modulus `q = 2^w` and Boolean ciphertext matrices of dimension `N = (n + 1) * w`. - It proves the exact integer error equations and correctness under the strict margin - `4 * |error| < q`. The [noise bounds](Complexity/Crypto/Computational/Homomorphic/GSW/Noise.lean) - are `m * β` for fresh encryption and `B₁ + N * B₂` for NAND. - [Tests](ComplexityTests/Crypto/GSW.lean) exercise both messages and all NAND inputs with nonzero - noise, including negative wraparound and decoder boundaries. This is the power-of-two - specialization of Gentry--Sahai--Waters (2013), omitting its redundant top digit. - The [finite samplers](Complexity/Crypto/Computational/Homomorphic/GSW/Sampling.lean) - instantiate actual key generation and encryption with uniform power-of-two residues, - independent binary coins and errors given by the difference of two independent `η`-bit counts. - Every supported error lies in `[-η, η]`. Fresh encryption and NAND of two fresh ciphertexts - are correct under the respective strict margins - `4*m*η < 2^w` and `4*(1+N)*m*η < 2^w`, respectively, with `w > 0`. - A [flat-tape identity](Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Randomness.lean) - preserves the full joint public-key, secret-key and ciphertext law using - `n*w + m*n*w + 2*m*η + N*m` fair bits. - [Serialized random-input samplers](Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean) - have uniform native PPT certificates and exact typed-distribution bridges, with unary - dimensions, binary residues and signed binary errors. - [Sampling tests](ComplexityTests/Crypto/GSWSampling.lean) include nonzero signed errors, - actual generated keys, both messages, NAND, empty dimensions and growing native inputs. - These results do not identify the finite noise with a Gaussian or assert its hardness. - The [complete serialized algorithms](Complexity/Crypto/Computational/Homomorphic/GSW/Serialized.lean) - compute actual public keys and ciphertexts using binary modular arithmetic and explicit unary - dimensions. Their [native certificates](Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/PolyTime.lean) - establish strict PPT for key generation and encryption on arbitrary encoded inputs. - [Exact bridges](Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean) - preserve the typed joint key law and encryption law, with public/secret word lengths - `m*(n+1)*w` and `n*w`, and all `N^2` ciphertext bits. - [Runtime tests](ComplexityTests/Crypto/GSWNative.lean) cover signed wraparound, ragged and - truncated inputs, zero dimensions, bit order and growing-parameter clients. - [Serialized decryption and NAND](Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean) - agree with the typed operations on every raw word, padding missing bits with zero and ignoring - excess bits. NAND retains modular integer counts and produces exactly `N^2` bits. Their - [native certificates](Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation/PolyTime.lean) - charge the full inputs and output with uniformly varying unary dimensions and binary arithmetic. - Correctness transports the existing strict noise margins, including every supported actual - key and encryption draw. [Regressions](ComplexityTests/Crypto/GSWEvaluation.lean) check small - widths, negative wraparound, asymmetric NAND products, positive noise and a native client - composing key generation, encryption, NAND and decryption. - The [statistical hiding theorem](Complexity/Crypto/Computational/Homomorphic/GSW/Hiding.lean) - proves the uniform-public-matrix step of their security argument. For `d = n + 1` and - `N = d * w`, the actual ciphertext gives any randomized two-stage adversary acceptance - probabilities differing by at most `N * sqrt(2^(w*d) / 2^m)`. The adversary sees the public - matrix before choosing its messages and retains arbitrary state. The underlying - [shared-matrix bound](Complexity/Probability/BitString/SubsetSum/Matrix.lean) works for every - positive modulus, with loss linear in the number of independently sampled binary rows; - it neither assumes whole-matrix two-universality nor gives a bound for every fixed matrix. - [Regressions](ComplexityTests/Crypto/GSWHiding.lean) include a composite-modulus counterexample - to whole-matrix universality and an adaptive game with exact nonzero advantage. - The [generated-key security theorem](Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean) - proves single-challenge IND-CPA for the actual serialized key generator and encryption program - against uniform classical strict PPT adversaries. Its - [decision-LWE assumption](Complexity/Crypto/Computational/LWE/Basic.lean) compares the public - word `[B*t+e | B]` with a uniform matrix of the same shape; the - [distribution bridge](Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean) supplies exactly - the sampled centered-binomial error law, without exposing the secret or errors. - One uniform hidden-bit reduction preserves the adversary's full saved state and bounds its - chosen-message advantage by twice its decision-LWE advantage plus the statistical term above. - The [positive-noise parameter family](Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean) - takes `n = η = λ+1`, `w = 16+8*ceil(log₂(λ+1))` and `m = (n+1)*w+2λ`. - It proves the entropy surplus, uniform native parameter routines and strict fresh/one-NAND - correctness margins simultaneously; the security theorem leaves only the specified LWE - hypothesis. [Regression clients](ComplexityTests/Crypto/GSWSecurity.lean) check saved-state - preservation, the attained factor-two loss, adaptive message choice and actual algorithm - certificates. A [checked formal abstract](abstracts/ComplexityAbstracts/GSWSecurityAbstract.lean) - spells out both algorithms, their native efficiency and this precise conditional security - result. It remains outside the curated headline catalogue while the full FHE recovery is open. - Hardness for the specified noise family is assumed; no worst-case lattice reduction is supplied. - A separate [depth-margin family](Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean) - takes `t = 1+ceil(log₂(λ+2))`, `n = η = λ+1`, `w = 16384*t²`, `N = (n+1)*w`, - `m = N+2λ` and `L = 512*t`. It proves `4*m*η*(N+1)^L < 2^w` for every parameter, - including zero, together with the entropy surplus, polynomial bounds and uniform native - unary parameter routines. Only the modulus is returned in binary. - Its [security corollary](Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters/Security.lean) - assumes decision LWE for this exact new family; the earlier family's hardness premise is - insufficient. The [actual selected-row decryptor](Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit.lean) - computes total serialized decryption on every well-sized raw secret/ciphertext pair, including - widths zero and one. Its depth is at most `28 + 18*clog₂(w+1) + 12*clog₂(n)` and its gate - count at most `131*(n+1)*(w+1)²`. The [native generator](Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/PolyTime.lean) - charges all arithmetic, indexing, wiring and complete layered NAND augmentation. - The [parameter fit](Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/Parameters.lean) - proves that the actual augmented circuit, with two NAND microlevels per De Morgan level, - fits `L` at every security parameter. [Checked clients](ComplexityTests/Crypto/GSWDecryptionCircuit.lean) - include both decoder ties, negative wraparound, boundary widths and a uniform family generator. - These circuit results do not establish bootstrappability or transfer a hardness premise. - Full native circuit evaluation, bootstrappability with compatible parameters and the concrete - FHE instantiation remain open in #486. The earlier parameter family - proves fresh and one-NAND correctness; it does not yet supply the augmented-decryption circuit - or the separate joint circular-security assumption needed for the fixed-key endpoint. - The [code-composition API](Complexity/Computability/Circuit/Boolean/CodeComposition.lean) - provides a native polynomial-time constructor for shared-input blocks with different gate - counts, checked against the existing carry-save circuit without padding. This supports the - complete shallow-decryption generator in #528. - [Native carry-save generators](Complexity/Computability/Circuit/Boolean/CarrySave/PolyTime.lean) - construct the exact existing three-to-two and four-to-two reducers from unary width, - including all binary references and the unequal carry-bit blocks. - The [balanced-code generator](Complexity/Computability/Circuit/Boolean/BalancedCode.lean) - constructs the exact existing half-split tree from the complete native leaf-code list, - binary input arity and native operator/fallback codes. Its polynomial certificate charges - all interval-table rows and wire encodings, including dead gates and malformed raw data. - This completes the balanced-construction prerequisite #543 used by the complete #528 decryptor. -4. **Completeness of oblivious transfer.** In the ideal oblivious-transfer hybrid model, every - polynomial-time multiparty functionality admits a protocol secure against static malicious - corruptions, with security defined by real/ideal simulation and allowing abort, under the - standard communication assumptions. This does not guarantee fairness or delivery of outputs. -5. **Håstad’s optimal MAX-E3SAT hardness.** For every fixed ε with 0 < ε < 1/8, it is NP-hard to - distinguish satisfiable E3-CNF formulas from E3-CNF formulas for which every assignment - satisfies at most a 7/8 + ε fraction of clauses. *Partial:* - [Hastad](Complexity/Computability/PCP/Approximation/Hastad.lean) proves the analytic core: - completeness and soundness of Håstad's noisy 3-bit linear test on folded Long Code tables - against `GapLabelCover` with a uniform threshold `0 < η < 1` - (`Cslib.PCP.Hastad.gapLabelCover_dichotomy_lt_one`), exercised on genuine parallel-edge - no-instances in [the tests](ComplexityTests/Hastad.lean), and - [MaxExactThreeSAT](Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean) proves the - easy `7 / 8` random-assignment bound. The reduction to MAX-E3LIN/MAX-E3SAT and NP-hardness of - Label Cover (PCP theorem with parallel repetition) remain open. For parallel repetition (#886), - [CorrelatedSampling](Complexity/Probability/CorrelatedSampling.lean) proves Holenstein's - correlated sampling step (agreement `≥ (1 - δ) / (1 + δ)`) and - [Embedding](Complexity/Probability/CorrelatedSampling/Embedding.lean) his local embedding lemma - (Lemma 8), and [ProductConditioning](Complexity/Probability/ProductConditioning.lean) proves - Raz's conditioning lemma (Holenstein's Lemma 5). - [TwoProverGame](Complexity/Computability/PCP/TwoProverGame.lean) defines two-prover games, - their value and parallel repetition (with `value G ^ n ≤ value (G.pow n)`); the remaining - embedding steps and the repetition theorem itself are not yet formalized. -6. **Williams’s ACC lower bound.** NEXP ⊄ ACC⁰: some language in nondeterministic exponential time - has no polynomial-size, constant-depth nonuniform circuit family over unbounded-fan-in AND, OR, - NOT and modular-counting gates with fixed moduli. -7. **Valiant’s algebraic completeness theorem.** Over every field of characteristic different from - two, the permanent polynomial family is VNP-complete under polynomially bounded projections: - every VNP family is obtained from a polynomially larger permanent by substituting variables and - field constants. -8. **Kabanets–Impagliazzo derandomization-to-lower-bounds theorem.** If polynomial identity testing - for arithmetic circuits over the integers has a deterministic polynomial-time algorithm, then - either NEXP ⊄ P/poly or the permanent family has no polynomial-size arithmetic circuits over the - integers. -9. **Babai–Fortnow–Lund multiprover theorem.** MIP = NEXP: a language has a classical multiprover - interactive proof with a probabilistic polynomial-time verifier and constant - completeness–soundness gap if and only if it belongs to nondeterministic exponential time. The - provers cannot communicate during the protocol. *Partial:* - [MIP](Complexity/Computability/Complexity/Classes/MIP.lean) defines classical multiprover - proofs with a constant number of provers per language and a strict polynomial-time fair-coin - verifier. It proves `IP ⊆ MIP₂ ⊆ MIP`, closure under Karp reductions, deterministic prover - optimality, and the unconditional upper bound `MIP ⊆ NEXP`. The reverse direction - `NEXP ⊆ MIP₂`, requiring the BFL multilinearity test and arithmetization of exponential-time - tableaux, is deferred; the full characterization is not claimed. -10. **Regev’s worst-case-to-average-case reduction.** For suitable modulus q and Gaussian noise - rate α satisfying αq > 2√n, an efficient algorithm for search-LWE in dimension n yields a - quantum polynomial-time algorithm for worst-case GapSVP and SIVP with approximation factor - Õ(n/α). The noise distribution, modulus restrictions and quantum reduction are part of the - theorem. - -## Modern FHE methods and deployment priorities - -The planning update is tracked in -[#513](https://github.com/cslib-community/complexitylib/issues/513). The targets below remain -unimplemented; the generic Gentry theorem and current GSW development do not establish them. -First complete [#486](https://github.com/cslib-community/complexitylib/issues/486): actual GSW -algorithms, the exact chosen-noise decision-LWE reduction, admissible parameters, and shallow -augmented decryption connected to the leveled/fixed-key endpoints. The current native -key-generation/encryption and security milestones are -[#500](https://github.com/cslib-community/complexitylib/issues/500) and -[#501](https://github.com/cslib-community/complexitylib/issues/501); completing them still leaves -decryption/evaluation runtime and bootstrappability obligations. - -**Industrial context, checked 2026-10-23.** Current FHE libraries serve distinct workloads: - -| Workload | Methods and current implementation evidence | +| Program | Issues | | --- | --- | -| Exact modular arithmetic and packed integer computations | BFV/BGV are supported by [Microsoft SEAL](https://github.com/microsoft/SEAL) and [OpenFHE](https://github.com/openfheorg/openfhe-development). | -| Approximate vector arithmetic, including numerical inference | CKKS is supported by SEAL and OpenFHE; its numerical approximation is part of the result contract. | -| Boolean/integer operations, comparisons and lookup tables | [TFHE-rs](https://docs.zama.org/tfhe-rs/get-started) implements TFHE with programmable bootstrapping; OpenFHE also implements FHEW/TFHE-family methods. | - -There is commercial use beyond library availability: [Duality states that its secure data -collaboration platform is built with OpenFHE](https://dualitytech.com/platform/open-source/), and -[Zama documents TFHE-rs execution in its confidential-blockchain coprocessors](https://docs.zama.org/protocol/protocol/overview/coprocessor). -These are vendor descriptions, not market-share measurements or independent deployment audits. -Bounded-depth arithmetic can use leveled evaluation without bootstrapping; a bootstrap is a -separate algorithmic capability, not something every workload invokes. - -Develop the following in reviewable milestones, reusing existing finite sampling, gadget algebra, -native certificates and game reductions where their hypotheses match: - -1. **Shared ring arithmetic and precise RLWE experiments.** Construct the actual polynomial-ring - operations, starting with `R_q = (Z/qZ)[X]/(X^d + 1)` for power-of-two `d`. Prove residue-number - (RNS/CRT) conversions, rounding and modulus-switching error bounds; prove that forward/inverse - negacyclic NTTs implement ring multiplication under explicit modulus/root conditions. Give - native certificates for the serialized algorithms, including malformed inputs. The - [Intel HEXL kernels](https://github.com/IntelLabs/hexl) provide a concrete implementation target. - Define the exact RLWE secret/error distributions and distinguishing experiment separately: - an ordinary-LWE reduction for #486 does not establish this RLWE claim. -2. **FHEW/TFHE programmable bootstrapping.** Follow - [Ducas–Micciancio](https://eprint.iacr.org/2014/816) and - [Chillotti–Gama–Georgieva–Izabachène](https://eprint.iacr.org/2016/870), a close next use of the - GSW gadget work. Construct ring-GSW external products, blind rotation, sample extraction and - key switching. For an explicit plaintext domain and admissible lookup table `f`, prove that - the actual bootstrap decrypts to `f(m)`, with its noise and failure bounds, output width and - total runtime. Account for negacyclic lookup restrictions and finite torus representations; - floating-point FFT implementations need their own rounding-error proof. Then assess - [smaller-key methods of Lee et al.](https://eprint.iacr.org/2022/198) and batched variants, +| Frontier program: ambitious theorems toward the research frontier | [#897]; its tracks are linked below | +| Metacomplexity: time-bounded Kolmogorov complexity, partial MCSP, hardness magnification | [#798], audit [#884] | +| Plain computability: delete the tidy calculus, keeping a machine-level kernel | [#862], from [#456] | +| Consolidation: duplicates, accurate statements and docs, less churn | [#949], [#939] | +| A concrete LWE-based fully homomorphic scheme | [#486] | +| Immerman–Szelepcsényi follow-ups | [#885] | +| Boneh–Shoup cryptography tracks; zero-knowledge architecture | [#640], [#643] | +| A Verso guide with a chapter per area | [#585] | + +## Cryptography + +### Landmark theorems + +1. **Goldreich–Micali–Wigderson zero knowledge in full.** If one-way functions exist, every + language in NP has a computational zero-knowledge proof in Goldreich's sense (Def. 4.3.10): + for every `x ∈ L` and arbitrary auxiliary input `z`, against probabilistic polynomial-time + verifiers. This needs a bridge between the security premise and a clock independent of an + unbounded auxiliary word, witness-level Levin reductions, and sequential soundness + amplification to negligible error. Derive the advice-PRG premise of the auxiliary-input + theorem from uniform one-wayness, or replace it. +2. **Rompel's signature theorem.** One-way functions imply digital signatures that are + existentially unforgeable under adaptive chosen-message attacks, for arbitrary + polynomial-length messages: universal one-way hash functions and authentication trees. +3. **Gentry's bootstrapping, instantiated** ([#486]). A concrete LWE-based scheme satisfying the + correctness, security, bootstrappability and native-efficiency hypotheses of the generic + theorem: full native evaluation of the augmented GSW decryption circuit, bootstrappability + with compatible parameters, and the joint circular-security assumption needed for the + fixed-key endpoint. Gentry's exact concrete-security loss is a separate target. +4. **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time + multiparty functionality admits a protocol secure against static malicious corruptions, with + real/ideal simulation and abort, under the standard communication assumptions. +5. **Regev's worst-case to average-case reduction.** For suitable `q` and Gaussian noise rate + `α` with `αq > 2√n`, an efficient search-LWE algorithm yields a quantum polynomial-time + algorithm for worst-case GapSVP and SIVP within `Õ(n/α)`. The noise distribution, modulus + restrictions and quantum reduction are part of the theorem. + +### Modern fully homomorphic encryption + +After [#486], develop these in reviewable milestones, reusing the finite sampling, gadget +algebra, native certificates and game reductions where their hypotheses match. [#513] maps the +schemes to current libraries and workloads. + +1. **Ring arithmetic and RLWE.** Polynomial-ring operations over `(Z/qZ)[X]/(X^d + 1)`, RNS/CRT + conversions, rounding and modulus-switching error bounds, and negacyclic NTTs implementing + ring multiplication, with native certificates. Define the RLWE secret and error laws and + experiment separately; an ordinary-LWE reduction does not give them. +2. **FHEW/TFHE programmable bootstrapping** (Ducas–Micciancio; Chillotti–Gama–Georgieva– + Izabachène). Ring-GSW external products, blind rotation, sample extraction and key switching; + prove the bootstrap decrypts to `f(m)` with its noise, failure, width and runtime bounds, + including negacyclic lookup restrictions and torus representations; floating-point FFT + implementations need their own rounding-error proof. Then smaller-key and batched variants, preserving their exact secret distributions and joint error bounds. -3. **Exact packed BFV/BGV.** Formalize the constructions of - [Brakerski–Gentry–Vaikuntanathan](https://eprint.iacr.org/2011/277) and - [Fan–Vercauteren](https://eprint.iacr.org/2012/144), including slot encoding, multiplication, - relinearization, rotations and level/modulus management. For permitted arithmetic circuits, - prove decryption equals evaluation in the stated plaintext ring, with explicit depth, noise, - modulus and packing conditions. Distinguish equality modulo the plaintext modulus from - ordinary integer equality; the latter needs a range bound. Establish leveled evaluation - before adding a separately proved refresh algorithm. -4. **Approximate packed CKKS and its bootstrap.** Follow - [Cheon–Kim–Kim–Song](https://eprint.iacr.org/2016/421). Define finite message encodings and the - complex-slot interpretation, then prove an explicit norm bound on decoded evaluation error - for bounded inputs and specified scales, levels and circuits. Include rescaling, rounding, - key switching and rotations in that bound. A bootstrap must prove its precision after modulus - raising, coefficient/slot transforms and approximate modular reduction; use the - [OpenFHE bootstrap description](https://github.com/openfheorg/openfhe-development/blob/main/src/pke/examples/CKKS_BOOTSTRAPPING.md) - as a concrete implementation reference. Approximate arithmetic requires an explicit - approximate-correctness interface, not the current exact Boolean equality contract. -5. **Scheme switching and multiparty extensions.** OpenFHE's CKKS/FHEW switching, vectorized - functional bootstrapping and threshold variants motivate later targets. Prove each conversion - preserves the intended value within its range/precision contract and state the joint - evaluation-key security assumption. For threshold key generation/decryption, fix corruption - thresholds, interaction, robustness and decryption-query access explicitly; distinguish - honest-but-curious security from malicious security. These are protocol theorems beyond - single-key IND-CPA. - -For every scheme, specify whether encryption is public-key or symmetric and prove the matching -chosen-plaintext security reduction for the actual algorithms and public evaluation keys. Keep -ordinary LWE/RLWE assumptions, circular/KDM assumptions and concrete attack-cost estimates distinct. -If correctness permits a nonzero decryption-failure probability, introduce that game explicitly -and relate it to the current perfect-support interface. Require nonvacuous parameter families, -composed error bounds, full-input native runtime and independent source/statement review before -claiming an endpoint. Hardware acceleration benchmarks do not replace any of these proofs. - -## Long-term coverage and reuse - -The long-term bar is to support formalizing every paper appearing in the -[Electronic Colloquium on Computational Complexity](https://eccc.weizmann.ac.il/colloquium/call_for_papers/). -Across successive papers, the additional work should increasingly be their new mathematics: -standard models, representation changes, reductions, resource certificates and proof techniques -should come from the library. This is an amortized goal. A new method may require substantial -infrastructure once; later developments should reuse it instead of rebuilding it. Count that -infrastructure's implementation and maintenance cost when assessing the improvement. - -The reusable-API placement audit [#404](https://github.com/cslib-community/complexitylib/issues/404) -follows the space/constructibility extraction in #402. It tracks generic time-class, encoding, -bit-string and NP helpers still located in specialized theorem modules; each proposed extraction -needs an import-boundary review and preserves existing public interfaces and resource conventions. - -### Catalogue the classes and theorems - -Build an auditable coverage index spanning the complete -[Complexity Zoo](https://complexityzoo.net/Complexity_Zoo), including its hierarchies, nonuniform -and communication classes, and extend it with the canonical problems and theorems needed by ECCC -papers. The Zoo supplies a catalogue and references; verify definitions and results against their -primary sources. This is a coverage target, not a claim that the catalogue is already formalized. - -Each entry should record its source and aliases, precise model and conventions, existing Lean -declarations, missing prerequisites, and status: unassessed, definition only, partial development, -or verified theorem. Track containments, separations, closure properties, complete problems and -reductions separately. A defined class or a combinatorial lemma does not establish its advertised -machine characterization, completeness theorem or efficient construction. - -Cover decision, function, search, counting, promise, distributional and parameterized problems. -Keep uniformity, advice, oracle access, error gaps, resource measures and reduction types explicit. -Share class operators and their closure theorems where they derive families of variants. Keep -canonical definitions in their mathematical modules; the index should link to them rather than -maintain a second set of definitions. Existing module docstrings, source markers and the detailed -milestones below remain the authority for their respective facts. - -### Next steps after basic class closure - -The verifier-based `UP` and `CeqP` developments, basic Boolean closures, exact-count -polynomial-time precomposition, and generic DP/SAT–UNSAT completeness are implemented. -The forward machine-to-verifier direction is proved for `#P` and `GapP`: accepting and -rejecting terminal counts of fixed finite-control list-choice machines under polynomial clocks -have actual certified binary verifiers. The actual reverse guess-and-verify construction and -[#P machine characterization](Complexity/Computability/Complexity/Classes/SharpP/Characterization.lean) -are now proved. The [signed GapP construction and characterization](Complexity/Computability/Complexity/Classes/SharpP/GapMachine.lean) -are also proved, using balanced verdict routing and an actual selector between independent witness -families. The [UP](Complexity/Computability/Complexity/Classes/UP/Machine.lean) and -[FewP](Complexity/Computability/Complexity/Classes/FewP/Machine.lean) native characterizations -are also proved: the exact #P bridge preserves the bound of one or a polynomial on accepting -occurrence traces, independently of the all-branches clock. SPP, FewP, fixed-modulus ModP, coUP and coC=P -now have verifier-based definitions and basic closure/containment developments. FewP ⊆ SPP and -PH ⊆ P^#P = P^PP are proved, with uniform simulations under the function-bit oracle convention. -Exact #P/GapP counts now have certified binary-output polynomial-space evaluators, yielding -PP ⊆ PSPACE and P^PP = P^#P ⊆ PSPACE, including arbitrary injective oracle encodings via -total clocked counting-machine extensions -([counting space](Complexity/Computability/Complexity/Classes/Counting/OracleSpace.lean)). -Extend these with counting reductions and further oracle results, preserving exact -multiplicities when required. The current modular Boolean closures require a prime modulus. The complementary modular class is -implemented, with equality to ModP for prime moduli. Fixed positive moduli admit GapP -zero/nonzero-residue characterizations; SPP (hence FewP) is in both modular classes for every -modulus at least two, including composite moduli. Both modular classes lie in PSPACE for every -fixed natural modulus. US, coDP, the finite Boolean -hierarchy (`BH` and `coBH`, base-class Boolean operations on `BH`, and the finite-hierarchy -level-collapse equivalences `BH_{k+1} = BH_k ↔ BH_k = coBH_k ⇒ BH = BH_k`), WPP and LWPP now have -definitions and elementary containments/closures. Full Boolean-hierarchy Boolean closure is -proved with explicit finite-level upper bounds, as is BH ⊆ Σ₂ ∩ Π₂ using same-level union and -intersection closure of every Σₖ and Πₖ -([hierarchy connection](Complexity/Computability/Complexity/Classes/BooleanHierarchy/PH.lean)), -and Kadin's polynomial-hierarchy collapse (`coBH k ⊆ BH k → PH = Σ₃ᴾ`, `BH (k + 1) = BH k → PH = Σ₃ᴾ`, -`DP = coDP → PH = Σ₃ᴾ`, and `SATUNSAT ∈ coDP → PH = Σ₃ᴾ`) is proved in -[BooleanHierarchy.Kadin](Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean). -Further proved results include LWPP many-one -reduction closure, unary-indexed target normalization, and full one-sided polynomial-family -multiple-target robustness: Poly-WPP = WPP and Poly-LWPP = LWPP, and the full two-sided -(Poly,Poly)-WPP/WPP and (Poly,Poly)-LWPP/LWPP characterizations with disjoint uniformly computed -accepting/rejecting binary target lists. Original targets may be zero; neither index must be -computable ([WPP.TwoSided](Complexity/Computability/Complexity/Classes/WPP/TwoSided.lean)). -Uniform bounded conjunction and disjunction also preserve both classes for a single jointly -uniform language on instances and unary indices, with any polynomial-time unary input-dependent -bound. The LWPP proof normalizes all possible prefix targets at each length -([WPP.Bounded](Complexity/Computability/Complexity/Classes/WPP/Bounded.lean)); it does not -establish adaptive oracle closure. Polynomial-time truth-table reductions now preserve both -WPP and LWPP, using an arbitrary polynomial-time Boolean combiner on a uniform batch of -queries ([WPP.TruthTable](Complexity/Computability/Complexity/Classes/WPP/TruthTable.lean)). -Query lengths and unary query counts may vary at fixed input length; LWPP normalizes both. -Adaptive WPP closure and UP-oracle containment are not claimed by this result. -Oracle lowness of SPP (`GapPWithOracle_eq_GapP_of_mem_SPP`, hence lowness for `SPP`, `C=P`, `PP`, -and the unrelativized-`FP`-target classes `LWPPWithFixedTarget` and `WPPWithFixedTarget`), LWPP -(`exists_mul_mem_GapP_of_mem_LWPP`, hence lowness for `C=P`, `PP`, and the unrelativized-`FP`-target -classes `LWPPWithFixedTarget` and `WPPWithFixedTarget`), and WPP (`PPWithOracle_eq_PP_of_mem_WPP`) -is proved in [WPP.Lowness](Complexity/Computability/Complexity/Classes/WPP/Lowness.lean), and -[SharpP.Lowness](Complexity/Computability/Complexity/Classes/SharpP/Lowness.lean) proves -precomposition of `#P` and `GapP` with `FP^(UP ∩ coUP)` functions, the exact lowness -characterizations `Low(#P) = UP ∩ coUP` (`SharpPWithOracle_eq_SharpP_iff`), `Low(UP ∩ coUP) = UP ∩ coUP` -(`UPWithOracle_inter_coUPWithOracle_eq_iff`), `Low(GapP) = SPP` (`GapPWithOracle_eq_GapP_iff`), -and `Low(SPP) = SPP` (`SPPWithOracle_eq_SPP_iff`), `UP ∩ coUP` lowness for `UP`, `coUP`, `FewP`, -`US`, and `SBPWithFixedTarget`, and `SPP`/`FewP`/`UP ∩ coUP` lowness for relativized modular -counting classes (`ModPWithOracle_eq_ModP_of_mem_SPP`, `coModPWithOracle_eq_coModP_of_mem_SPP`, -`ParityPWithOracle_eq_ParityP_of_mem_SPP`); -target-relativized `LWPP^A` / `WPP^A` / `SBP^A` definitions and lowness with `FP^A` targets are not claimed. -[Oracle lowness of `NP ∩ coNP` and `UP ∩ coUP`](Complexity/Computability/Complexity/Classes/Oracle/Lowness.lean) -proves `P^(NP ∩ coNP) = NP ∩ coNP`, `P^(UP ∩ coUP) = UP ∩ coUP`, `NP^(NP ∩ coNP) = NP`, the -characterization `NP^A = NP ↔ A ∈ NP ∩ coNP` (`NPWithOracle_eq_NP_iff`), and -`NP = coNP ↔ ∀ A ∈ NP, NP^A = NP` (`NP_eq_coNP_iff_forall_NPWithOracle_eq_NP`). -PP is closed under polynomial-time truth-table reductions (Fortnow–Reingold), hence under -intersection, union, difference, symmetric difference (Beigel–Reingold–Spielman) and -polynomial-time bounded quantifiers ([PP.TruthTable](Complexity/Computability/Complexity/Classes/PP/TruthTable.lean)). -The proof uses Newman's sign-approximating polynomial on GapP. P is closed under the same -reductions. Closure of PP under adaptive polynomial-time Turing reductions (`P^PP = PP`) would -give `PH ⊆ PP` by Toda's theorem; it is open and not claimed. -The binary-output FP-to-#P/GapP bridge is available. Parsimonious Cook–Levin gives #P-completeness of #SAT and SAT-based complete problems for ⊕P, US, ModₖP/coModₖP, PP (both threshold #SAT and MAJSAT) and C=P/coC=P ([CountingSAT](Complexity/Computability/Complexity/Problems/CountingSAT.lean)). Remaining extensions include -permanent completeness and target-relativized WPP/LWPP oracle classes with `FP^A` targets. -SBP and AWPP now have verifier-based definitions, the elementary NP/BPP/SPP-to-PP -containments, many-one reduction closure, SBP union closure and AWPP Boolean closure. -WPP ⊆ AWPP is proved, including signed binary-output targets. Uniform AWPP -amplification achieves error at most `2^(-r(x))` for every requested exponent polynomially -bounded in encoded input length, using one GapP numerator and a length-polynomial -dyadic denominator. The requested rate need not be computable: the construction -uses a fixed dominating polynomial. The explicit construction uses `12q(n)` majority -trials and denominator exponent `12q(n)p(n)`; see -[AWPP amplification](Complexity/Computability/Complexity/Classes/AWPP/Amplification.lean). -[Uniform SBP amplification](Complexity/Computability/Complexity/Classes/SBP/Amplification.lean) -achieves multiplicative gap `2^r(x)` for every polynomially bounded requested exponent, -with a #P count and positive binary-output polynomial-time threshold. Intersecting an SBP -language with a BPP language stays in SBP. MA ⊆ SBP is proved with the Arthur–Merlin classes. -The [set lower bound protocol](Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean) -already proves SBP ⊆ AM. [Uniform indexed #P/GapP products](Complexity/Computability/Complexity/Classes/SharpP/Products.lean) -provide a counting-algebra foundation for future oracle simulations. -[Relativized counting and majority verifiers](Complexity/Computability/Complexity/Classes/PP/Oracle.lean) -provide the positive-GapP characterization and elimination of P-decidable oracles. -[AWPP PP-lowness](Complexity/Computability/Complexity/Classes/AWPP/Lowness.lean) is proved for -the strict adaptive oracle-verifier model: every AWPP word oracle satisfies -`PPWithOracle A enc = PP enc`, with arbitrary injective input encodings and exact ties rejecting. -These definitions retain the verifier-model boundary stated above. - -### Extend the mathematical canon - -This map adds long-term directions to the concrete developments below. It follows the breadth of -[ECCC's scope](https://eccc.weizmann.ac.il/colloquium/call_for_papers/) and the Zoo, rather than the -contents of the original port. Entries are targets for coverage audits and substantial theorem -developments, not assertions that every prerequisite is missing or assignments to current workers. - -| Area | Coverage to establish or extend | +3. **Exact packed BFV/BGV** (Brakerski–Gentry–Vaikuntanathan; Fan–Vercauteren). Slot encoding, + multiplication, relinearization, rotations and level management, with leveled evaluation + before a separately proved refresh. Equality modulo the plaintext modulus differs from + ordinary integer equality, which needs a range bound. +4. **Approximate packed CKKS and its bootstrap** (Cheon–Kim–Kim–Song), with an explicit + approximate-correctness interface and a norm bound on decoded error covering rescaling, + rounding, key switching and rotations. +5. **Scheme switching and threshold variants**, with explicit range/precision contracts, + evaluation-key assumptions, corruption thresholds, interaction, robustness and + decryption-query access, distinguishing honest-but-curious from malicious security. + +For each scheme, prove chosen-plaintext security for the actual algorithms and public evaluation +keys; keep LWE/RLWE, circular/KDM assumptions and attack-cost estimates distinct; introduce a +decryption-failure game when correctness is not perfect; and require nonvacuous parameter +families and full-input native runtime. + +### Public-key, lattice and symmetric constructions ([#640]) + +- **Sigma protocols and Fiat–Shamir** ([#581]): computational Schnorr signatures under discrete + log against strict PPT forgers; eavesdropping security in the strict-PPT model, with the + statistical-distance term from sampling `ZMod q`. +- **Diffie–Hellman and ElGamal:** group-element messages, efficient key generation and + encryption, the efficient DDH random self-reduction (Boneh–Shoup Ex. 10.10), hashed ElGamal, + Cramer–Shoup CCA security, and Pedersen commitments. +- **Lattices** ([#645]): Fiat–Shamir with aborts and signatures from SIS (Lyubashevsky 2009, + 2012); strict-PPT samplers for integer boxes; identification security under SIS; efficiency + certificates for the simulator and extractor; full interactive-view simulation; SIS for + general moduli; module SIS and module LWE toward Dilithium-style schemes, as theory. +- **Symmetric:** `IsOraclePPT` admissibility of the PRF-pad reduction, uniform word-level + forger and hash families, the asymptotic `PseudorandomFunction` corollary and fresh-nonce + multi-query Carter–Wegman security ([#736]); the 4-round strong Feistel bound ([#748]); the + Naor–Reingold PRF from DDH. +- **General:** reusable adaptive reductions, public-key encryption, universal-instance zero + knowledge, hard-core predicates and hardness amplification, and connections to learning and + average-case hardness. + +### Zero-knowledge proof systems toward libzk ([#643]) + +In order: +- the `PublicCoin → IP` bridge, with a uniform word verifier and adversarial decoding; +- parallel and AND/OR composition, and round-by-round knowledge soundness; +- oracle statements, so a later phase can query an earlier phase's oracle message (virtual + output oracles, as in ArkLib), with knowledge soundness and zero knowledge in oracle worlds; +- efficiency-certified simulators and extractors, and auxiliary-input zero knowledge on the core; +- polynomial commitment and evaluation-query reductions, and the Ligero IOP; +- the BCS transform to non-interactive arguments in the random-oracle model; +- VOLE as an ideal functionality, and VOLE-in-the-head; +- libzk's compositional structure as a composition of these components, without ciphersuites. + +## Complexity classes and reductions + +### Coverage catalogue + +Build an auditable coverage index spanning the [Complexity Zoo](https://complexityzoo.net/Complexity_Zoo) +and the canonical problems and theorems that ECCC papers need, verified against primary sources. +Each entry records its source and aliases, precise model and conventions, Lean declarations, +missing prerequisites and level (definition, partial development, verified theorem). Track +containments, separations, closure properties, complete problems and reductions separately, and +cover decision, function, search, counting, promise, distributional and parameterized problems, +with uniformity, advice, oracle access, error gaps, resources and reduction types explicit. The +index links to canonical definitions rather than keeping a second set. + +### Structure, time and space + +- **PRIMES ∈ P** ([#893]): the hard direction of the AKS criterion, the small-`r` bound and the + polynomial-time algorithm on binary inputs. +- Time, space and exponential hierarchies; oracle, advice, unambiguous and promise classes; + completeness, padding, self-reducibility, relativization and oracle separations, preserving + each reduction's resource bound. +- A tight time hierarchy, which needs a linear-overhead tape-indexed simulation, and the + `f log f` hierarchy with its simulation bound. The space hierarchy for `log n ≤ g n`, which + needs a universal simulation that does not hold its input. +- **Space** ([#885]): 2SAT NL-complete, `NSPACE(s) = coNSPACE(s)`, and Savitch bounds for general + space-constructible functions. +- **Randomized logspace** ([#459], [#474]): RL and BPL, `USTCON ∈ RL`, Nisan's generator, + `BPL ⊆ L²` and Saks–Zhou. +- **Reingold:** a symmetric-machine model of SL, and the edge-list encoding of USTCON by a + logspace reduction. +- **Williams's `TIME[t] ⊆ SPACE[√(t log t)]`** ([#888]): implicit Tree Evaluation with the + fan-in-`d` space bound, subroutine calls for implicit gates and leaves, and padding of + non-perfect trees. For Cook–Mertz itself: malformed-input handling and the refined + `O(ℓ + H log(ℓ + 2))` parameter bound. +- Alternating time and space classes and bounded-alternation characterizations of PH; sharp + bounds for sublinear space, distinct from polynomial-space simulation. + +### Counting and modular classes + +- Counting reductions and further oracle results preserving exact multiplicities; permanent + #P-completeness; modular and counting hierarchies; the oracle-algorithm form of Stockmeyer's + approximate counting. +- Boolean closures of the modular classes for composite moduli. +- Target-relativized `LWPP^A`, `WPP^A` and `SBP^A` with `FP^A` targets; adaptive WPP closure and + UP-oracle containment. +- Native oracle counting machines: efficient encoded oracle checking, response-access costs and + oracle-machine characterizations, with resource bounds uniform over admissible oracles. + +### Interactive proofs + +- **MIP = NEXP** ([#892]): `NEXP ⊆ MIP₂` through the BFL multilinearity test and arithmetization + of exponential-time tableaux; GKR delegation. +- Private-to-public-coin transformations, `AM[k] = AM`, interactive-machine characterizations + of Arthur–Merlin classes, and statistical and perfect zero knowledge. + +### Descriptive complexity and first-order reductions + +Ordered first-order complexity follows Immerman: structures on `{0, …, n-1}` with `n ≥ 2`, FO +means FO(≤, BIT), and `≤_fo`, `≤_fop` and `≤_qfp` keep their standard meanings; the order-free +`FO.Reduces` and `FO.QFReduces` stay as a general layer. In dependency order: + +- **Ordered completeness.** SAT, 3SAT, 3COL, independent set, clique and vertex cover + NP-complete under first-order or quantifier-free projections; REACH NL-complete under + first-order reductions. +- **Projections:** projection reducibility on finite structure classes and the standard ordered + machine-encoding bridge. The classical qfp convention excludes BIT (Immerman–Landau, + Definition 3.6), and arbitrary quantifier-free combinations of input relations are not + projections. +- **Circuit Value P-complete under first-order reductions**, via `REACHa → MCVP → CVP` (Immerman, + Theorem 3.26 and Exercise 3.28), with the alternating-logspace simulation of polynomial-time + machines and the translation to `encCircuitValue`. +- Numeric certificates for further restricted-domain families; canonical BIT on a restricted + domain need not be first-order definable. +- The ordered ESO-to-NP direction of Fagin's theorem. +- Order-free: SAT-to-3SAT, graph-property hardness, and bridges to the separately encoded + problems. +- Logical characterizations of further resource classes, fixed-point and order-invariant + queries, and uniform translations between syntax, structures and algorithms. +- A witness-carrying reduction structure once a client needs one, for example size bounds for + Cook–Levin. + +### Uniform circuit families + +Define logspace and DLOGTIME uniformity with explicit gate-address, direct-connection and input +encodings; certify circuit generation, evaluation and the machine-to-circuit simulations, +preserving size, depth and construction resources; and prove FO with order and BIT equals +DLOGTIME-uniform AC⁰ under explicit conventions. + +### Search, parameterized and fine-grained complexity + +- **TFNP:** CLS, further local search, fixed-point and equilibrium problems. +- **Parameterized:** strongly uniform variants (computable `f`), further explicit polynomial + kernels, the W and A hierarchies, and parameterized lower bounds. +- **Exponential-time SAT** ([#894]): amplify Schöning's random walk, with a time bound, then + PPSZ. Further fine-grained reductions and consequences of ETH, SETH and other named hypotheses. + +### Approximation and PCP + +- **Håstad's optimal MAX-E3SAT hardness** ([#886]): for `0 < ε < 1/8`, NP-hardness of + distinguishing satisfiable E3-CNF formulas from those where every assignment satisfies at most + `7/8 + ε` of the clauses. This needs the reduction to MAX-E3LIN and, through the 4-clause XOR + gadget, to MAX-E3SAT; Raz–Holenstein parallel repetition for small-soundness Label Cover; and + the perfect-completeness reduction. +- The FGLSS clique-hardness reduction and its amplification, retaining the exact gap and + reduction runtime. +- Gap and approximation-preserving reductions, APX/PTAS/FPTAS, inapproximability consequences of + PCP, CSP classifications and relaxation gaps, with assumptions such as the Unique Games + Conjecture stated explicitly. The 2-to-2 games theorem waits for [#886]. +- **A practical PCP construction:** a reasonably runnable construction and its cost on complete + reductions; rotation certificates polynomial in the bit length of a vertex name; machine-level + error reduction and extractors from expander walks, with certified seed and evaluation costs. + +### Proof complexity + +Proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares, and +certified DPLL solver runtimes. + +## Circuits and algebraic complexity + +- **Williams's NEXP ⊄ ACC⁰ and Murray–Williams's NQP ⊄ ACC⁰** ([#889]): no polynomial-size, + constant-depth circuits over AND, OR, NOT and fixed-modulus counting gates for some language in + NEXP. +- Uniform and nonuniform NC, AC and TC, circuit-to-machine bridges, algorithm-to-lower-bound + arguments, and barriers such as natural proofs and algebrization. NC simulation of unrestricted + `TCⁱ` needs Muroga's threshold weight-bounding theorem. +- Formula lower bounds beyond Andreev's, following Jukna; Raz–Wigderson's monotone depth bound for + matching on general graphs. +- **An explicit frontier extractor:** port v1's sumset-extractor construction with an explicit + family in `Complexity.P encBits` that discharges the frontier lower bounds' hypotheses. It would + exceed the library's unconditional `3.5 N - o(N)` bound in P, so it needs an independent + correctness review of the frontier core. +- **Weighted threshold representations:** v1's explicit source-reduction family, universal scalar + circuit synthesis, entropy and asymptotic activity bounds, and geometric cutting. +- **Construction runtimes**, certified separately from gate counts: the mass-production + constructors, with constructive choices of information sets and line menus; the + iterated-function preprocessing; and the bit complexity of formula evaluation on the rational + hitting-list matrices. +- **Algebraic complexity** ([#891]): Limaye–Srinivasan–Tavenas constant-depth lower bounds; the + Kabanets–Impagliazzo theorem (a deterministic PIT algorithm implies NEXP ⊄ P/poly or the + permanent has no polynomial-size arithmetic circuits); Valiant's VNP-completeness of the + permanent over fields of characteristic other than two; formula and branching-program models, + identity testing, hitting sets, and tensor and rank methods, with uniform construction costs + certified separately from gate counts. +- **Real-algebraic decision procedures:** port the Sturm–Tarski query evaluator, recursive + evaluator, implicit arithmetic, native space certificates and the ETR upper bound from + [lean-canny](https://github.com/SamuelSchlesinger/lean-canny). + +### Jukna coverage + +Formalize the established results, constructions and worthwhile exercises of +[Jukna's *Boolean Function Complexity* (2012)](https://web.vu.lt/mif/s.jukna/boolean/index.html), +with the author's [errata](https://web.vu.lt/mif/s.jukna/boolean/misprints-BFC.html), auditing +each statement against the numbered result. Organize modules by subject, not chapter. + +| Chapters | Next coverage work | | --- | --- | -| Structural complexity | Time/space and exponential hierarchies; oracle and advice classes; unambiguous and promise classes; completeness, padding, self-reducibility, Ladner's theorem, relativization and oracle separations. `PRIMES ∈ P` (AKS, #893): the [AKS identity](Complexity/Foundations/NumberTheory/AKS/Criterion.lean) and [correctness of the AKS tests](Complexity/Foundations/NumberTheory/AKS/Correctness.lean) (Theorem 4.1, for any `r` with `ord_r(n) > log₂² n`) are proved; the small-`r` bound (Lemma 4.3) and the polynomial-time algorithm on binary inputs remain. Preserve each reduction's resource bound. | -| Space and alternation | Build on native `NPSPACE = PSPACE`, TQBF completeness, `NL ⊆ P`, [PH ⊆ PSPACE](Complexity/Computability/Complexity/Classes/Inclusions.lean) and [AP = PSPACE](Complexity/Computability/Complexity/Classes/Alternation/Savitch.lean). Extend the [machine-class milestones](#machine-class-milestones), alternating time/space classes and bounded-alternation characterizations of PH. Distinguish polynomial-space simulation from sharp bounds for sublinear space. | -| Counting and modular classes | Build on `#P`, `GapP`, `PP`, [parity-P](Complexity/Computability/Complexity/Classes/ParityP.lean) and [Toda's PH ⊆ P^#P theorem](Complexity/Computability/Complexity/Classes/Toda.lean), with a fixed polynomial-time program correct against every oracle answering the counting function's bits. Extend counting reductions and machine characterizations, permanent completeness, modular/counting hierarchies and the oracle-algorithm form of Stockmeyer approximate counting. | -| Interactive and probabilistic proofs | [IP ⊆ PSPACE](Complexity/Computability/Complexity/Classes/IP/PSPACE.lean) is proved for the strict polynomial-time, private-coin verifier model. [IP = PSPACE](Complexity/Computability/Complexity/Classes/IP/Shamir.lean) is proved, with a machine-certified Shamir–Shen-style verifier for TQBF, and [computational zero-knowledge proofs for NP](Complexity/Crypto/Computational/ZeroKnowledge.lean) (via a 3-copy masked-3SAT truth-table commitment protocol following Goldreich–Micali–Wigderson) are proved from one-way functions for uniform polynomial-time-generable instance/witness/auxiliary-input families at soundness error `1 / 3`. [Arthur–Merlin classes](Complexity/Computability/Complexity/Classes/ArthurMerlin.lean) are defined, with amplification, `AM ⊆ Π₂`, the set lower bound protocol and graph non-isomorphism in AM; develop public/private-coin transformations, the deferred BFL reverse inclusion, universal-instance and arbitrary-auxiliary-input zero knowledge, witness-level Levin reductions, statistical/perfect zero knowledge and sequential soundness amplification. [Classical MIP](Complexity/Computability/Complexity/Classes/MIP.lean) with a constant number of provers satisfies `IP ⊆ MIP₂ ⊆ MIP ⊆ NEXP`, with deterministic prover optimality and Karp-reduction closure. Reuse the existing PCP and probabilistic foundations. | -| Boolean circuits and parallel computation | Build on the `3.5n - o(n)` general-circuit lower bound for affine dispersers of dimension `o(n)` ([AffineDisperser](Complexity/Computability/Circuit/Boolean/AffineDisperser.lean)) and the De Morgan cover-complexity transfer ([Fusion/DeMorgan](Complexity/Computability/Circuit/Fusion/DeMorgan.lean)). Complete the [Jukna coverage](#jukna-coverage), uniform/nonuniform NC/AC/TC and related classes, circuit-to-machine bridges, algorithm-to-lower-bound arguments and barriers such as natural proofs and algebrization. | -| Algebraic and arithmetic complexity | Build on [VP and p-projections](Complexity/Computability/Circuit/Arithmetic/VP.lean), [VNP and VP ⊆ VNP](Complexity/Computability/Circuit/Arithmetic/VNP.lean), [determinant ∈ VP](Complexity/Computability/Circuit/Arithmetic/Determinant.lean) over commutative rings, and [Laplace expansion of the permanent](Complexity/Foundations/Data/Matrix/Permanent.lean). Prove permanent VNP-completeness with its characteristic assumptions, prove the Kabanets–Impagliazzo theorem, extend formula/branching-program models, identity testing, hitting sets, tensor and rank methods, and certify uniform construction costs separately from gate counts. | -| Approximation and constraint satisfaction | [Random assignment](Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean) proves the `7 / 8` random-assignment bound for exact 3-CNF with three distinct variables per clause (`CNF.IsExactThreeDistinct`), and [Håstad's 3-bit test](Complexity/Computability/PCP/Approximation/Hastad.lean) proves completeness and soundness of Håstad's 3-bit linear test against `GapLabelCover` (`1 - δ` vs `1 / 2 + 4 * ε`). Build the reduction to MAX-E3LIN and, via the 4-clause XOR gadget, to MAX-E3SAT on clauses with three distinct variables, Raz's parallel repetition theorem, and the perfect-completeness `(1, 7 / 8 + ε)` reduction; develop further gap and approximation-preserving reductions, APX/PTAS/FPTAS, canonical inapproximability consequences of PCP, CSP classifications and relaxation gaps. State assumptions such as the Unique Games Conjecture explicitly. | -| Pseudorandomness and coding | Build on [conditional `P = BPP` from exponential worst-case hardness in `E` (Impagliazzo–Wigderson)](Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean) via Nisan–Wigderson and Sudan–Trevisan–Vadhan, [Sudan's Reed–Solomon list decoding](Complexity/Foundations/Data/Code/Sudan.lean) (decoder correctness only: the decoder is noncomputable and no running time is claimed), and [expander-walk hitting bounds](Complexity/Foundations/Combinatorics/Expander/Hitting.lean). Extend space-bounded generators, extractors/condensers (seeded extractors from the leftover hash lemma and the [Chor–Goldreich two-source extractor](Complexity/Probability/Extractor/TwoSource.lean) are in `Probability/Extractor`; track #895 continues toward Chattopadhyay–Zuckerman), limited independence, explicit expanders, and Guruswami–Sudan / local decoding. Separate finite combinatorial guarantees from uniform construction and decoding costs. | -| Complexity-theoretic cryptography | One-way functions imply SAT ∉ P and SAT ∉ BPP, and MCSP ∈ BPP rules them out (Kabanets–Cai; [OneWay/MCSP](Complexity/Crypto/Computational/OneWay/MCSP.lean)). [Naor bit commitments](Complexity/Crypto/Computational/Commitment.lean) (with hiding against randomized stateful PPT receivers and deterministic polynomial-time receiver-string/bit families), [Goldreich–Micali–Wigderson zero knowledge for NP](Complexity/Crypto/Computational/ZeroKnowledge.lean) (uniform zero knowledge over deterministic polynomial-time instance/witness/auxiliary-input families via a 3-copy masked-3SAT truth-table commitment protocol), [uniform symmetric MACs and PRF-based MACs](Complexity/Crypto/Computational/MAC.lean) (`SUFCMA`, `EUFCMA`, `OneTimeEUFCMA`, quantitative `EUF-CMA ≤ SUF-CMA`, unique-tag equivalence, and the Boneh–Shoup Theorem 6.2 PRF-to-SUF-CMA/EUF-CMA reduction), and [keyed collision-resistant hash families and the Merkle–Damgård transform](Complexity/Crypto/Computational/CollisionResistant.lean) are proved. Uniform one-way functions are also equivalent to one-time secure digital signatures for `n`-bit messages, via [Lamport's construction](Complexity/Crypto/Computational/OneWayToSignature.lean); full EUF-CMA security implies one-way functions. [Carter–Wegman MACs](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) formalize unconditional one-time and adaptive multi-query issued-counter EUF-CMA/SUF-CMA security (`≤ ε`) from `ε`-almost-Δ-universal hash families together with the arbitrary-pad hybrid bound, the exact single-query fixed-nonce reduction to `prfRealGame`/`prfIdealGame` (`prfOneTimeGame_le`, `prfOneTimeGame_ofProbComp_le`), and `xpolyHash`/Boolean-matrix/subset-sum instantiations (`IsOraclePPT` admissibility of the PRF-pad reduction, uniform word-level forger/hash families, the asymptotic `PseudorandomFunction` corollary, and fresh-counter nonces remain open). Extend the existing OWF/PRG/PRF/MAC/CRHF/commitment/ZK results with reusable adaptive reductions, many-time digital signatures, encryption, universal-instance zero knowledge, hard-core and hardness-amplification methods, and connections to learning and average-case hardness. | -| Communication, queries and data structures | Build on the `Ω(n)` bounded-error randomized disjointness lower bound ([Disjointness](Complexity/Computability/Communication/Disjointness.lean)), Karchmer–Wigderson ([Boolean](Complexity/Computability/Circuit/Boolean/KarchmerWigderson.lean), [monotone](Complexity/Computability/Circuit/Monotone/KarchmerWigderson.lean)), and Raz–Wigderson's monotone depth bound for bipartite matching ([BipartiteMatching](Complexity/Computability/Circuit/Monotone/BipartiteMatching.lean)). Deterministic query-to-communication lifting for the index gadget is proved ([Lifting](Complexity/Computability/Communication/Lifting/Simulation.lean), #890) with gadget size about `n⁴`; the `n^{1+ε}` gadget (spread lemma), randomized lifting and applications remain. Extend multiparty protocols, discrepancy and information complexity, direct-sum/product results, and reductions to streaming, sketching and cell-probe lower bounds. Reuse upstream query models. | -| Proof complexity | Build on [Cook–Reckhow systems and simulations](Complexity/Computability/Complexity/ProofSystem.lean), including the polynomially bounded-system characterization of NP = coNP, the [resolution size–width tradeoff](Complexity/Logics/Propositional/Resolution/SizeWidth.lean), [tree-like resolution/DPLL search-tree certificates](Complexity/Logics/Propositional/Resolution/TreeLike.lean), [Tseitin formulas on expanders](Complexity/Logics/Propositional/Resolution/TseitinExpander.lean) and [Haken's pigeonhole lower bound](Complexity/Logics/Propositional/Resolution/Pigeonhole.lean). Extend proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares. The certificate correspondence does not certify a DPLL solver's runtime. | -| Average-case complexity and learning | Uniform-distribution learning on CSLib's PAC API, the LMN low-degree algorithm and Kushilevitz–Mansour with membership queries are [proved](Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean); running times are not machine-certified. Distributional problems and reductions, samplability, average-to-worst-case connections, PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. Existing cryptographic learners are starting points, not coverage of learning theory. | -| Property and distribution testing | Distance and access models, one/two-sided and tolerant testing, query/sample bounds, canonical graph/algebraic/distribution testers and lower bounds. | -| Fine-grained and parameterized complexity | Under ETH, 3-coloring, independent set, vertex cover and Hamiltonian cycle and path have no 2^{o(\|V\|+\|E\|)} algorithms and clique none in 2^{o(\|V\|)} ([GraphProblems](Complexity/Computability/Complexity/FineGrained/GraphProblems.lean)); the Hamiltonian bounds (directed and undirected) use linear-size diamond reductions. [FPT and XP](Complexity/Computability/Complexity/Parameterized.lean) are defined with arbitrary (not necessarily computable) `f`; `P ⊆ FPT ⊆ XP`, Boolean closure of FPT (complement for XP), closure under fpt-reductions and `FPT = XP = P` for bounded parameters are proved, and SAT is in FPT for the number of variables. [Kernelization](Complexity/Computability/Complexity/Parameterized/Kernelization.lean) (`IsKernelization`, `HasKernel`, `HasPolyKernel`) and the Cai–Chen–Downey–Fellows equivalence (`A ∈ FPT enc κ ↔ HasKernel enc κ A` for `A ∈ DTIME enc t` over a nonempty instance type) are proved, and [VertexCover](Complexity/Computability/Complexity/Parameterized/VertexCover.lean) is in FPT parameterized by target size `k` in time `O(2^k (|x|+1)^e)` by a bounded search tree and has [Buss's polynomial kernel](Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean) with at most `k(k+2)` vertices and encoded length at most `40(k+1)^6` (`VertexCover_hasPolyKernel`). On the algorithmic side, one trial of [Schöning's random walk](Complexity/Computability/Complexity/FineGrained/Schoening.lean) finds a satisfying assignment of a satisfiable k-CNF with probability at least `((k-1)/k)^(k-3) (k/(2(k-1)))^n / (3n + 1)`, which is `(3/4)^n / (3n + 1)` for 3-SAT; amplification, a time bound and PPSZ remain (#894). Further fine-grained reductions and consequences conditional on ETH/SETH and other named hypotheses; strongly uniform (computable `f`) variants, further explicit polynomial kernels, W/A hierarchies and parameterized lower bounds. | -| Total search and computational games | Build on [FNP, FP and TFNP with search reductions](Complexity/Computability/Complexity/Classes/TFNP.lean), including `FP = FNP` exactly when `P = NP` ([search to decision](Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean)), `TFNP ⊆ FP → NP ∩ coNP ⊆ P`, and the canonical subclasses [PLS, PPP, PPAD and PPA](Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean) with their combinatorial totality principles ([Principles](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Principles.lean)), inclusions `PLS, PPP, PPAD, PPA ⊆ TFNP`, `PPAD ⊆ PPP`, and `PPAD ⊆ PPA`, and De Morgan circuit problems (`LocalOpt ∈ PLS`, `Pigeon ∈ PPP`, `EndOfLine ∈ PPAD`, `Leaf ∈ PPA`). Their [completeness](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Completeness.lean) now follows from polynomial-time construction of function-family circuit codes, preserving binary local-search costs. Develop CLS, further local search, fixed-point and equilibrium problems. | -| Logic and descriptive complexity | Building on [Fagin's theorem](Complexity/Computability/Complexity/Fagin/Converse.lean): logical characterizations of additional resource classes, fixed-point and order-invariant queries, and uniform translations between syntax, structures and algorithms. | -| Kolmogorov complexity and metacomplexity | Build on [plain Kolmogorov uncomputability](Complexity/Computability/Kolmogorov/Uncomputability.lean), [single-tape and Post–Turing (`TM0`/`TM1`) description methods and simulations](Complexity/Computability/Kolmogorov/SingleTape.lean), and [multi-tape description methods and `Partrec` optimality](Complexity/Computability/Kolmogorov/MultiTape.lean) (#318): `ofTM0` and `ofTM1` are defined through the `SingleTapeTM` embeddings of Mathlib's `TM0`/`TM1`; `ofSingleTapeTM` (and `ofTM0`) are simulated by `ofMultiTapeTM` with zero program overhead and linear time overhead (single-tape → multi-tape only; the reverse simulation is not formalized); and each of `ofSingleTapeTM`, `ofTM0`, `ofTM1` and `ofMultiTapeTM`, pushed forward along a computable decoder, is simulated by the universal partial-recursive description method `universal` with additive overhead. Extend prefix-free complexity, resource-bounded MCSP variants and connections to learning, cryptography and lower bounds. | -| Quantum complexity | The [quantum query model with phase oracles and the BBBV `Ω(√N)` lower bound for search](Complexity/Computability/QueryComplexity/Quantum/Search.lean) are proved, with [Grover's algorithm](Complexity/Computability/QueryComplexity/Quantum/Grover.lean) meeting it (`⌊π/(4θ)⌋ ≤ π√N/4` queries, success at least `1 - 1/N`) (#896); BQP and `BQP ⊆ PP` remain. Reusable circuit/channel/measurement semantics, uniformity and approximation costs, BQP/QMA and related query, communication and interactive classes, amplification, containments and complete problems. Reuse suitable quantum foundations rather than create incompatible models. | - -### Measure reuse across papers - -Use a growing, source-pinned sample of papers across these areas as demanding clients, including -papers chosen after an API was designed. For each, identify the exact claims and assumptions, -reused declarations, genuinely new mathematics, missing standard dependencies, and representation -or automation friction. Promote recurring obligations into shared APIs only after demonstrating -reuse; a framework is not successful merely because its first client compiles. - -Measure the whole sequence of developments: shared code plus clients, proof and interface size, -elaboration/checking cost, and remaining manual machine or encoding work. The desired trend is -less repeated foundational work per paper while preserving readable proofs and exact quantitative -statements. Novel arguments will still require novel proofs. Keep this catalogue and evidence -linked to declarations and reviewed revisions, rather than adding parallel narrative inventories. - -## Repository identity and home - -This library is **Complexitylib**: computational complexity theory built on CSLib. The temporary -name `complexitylib2` distinguished the CSLib-based rewrite while both implementations were active; -it is not a lasting project identity. The canonical repository is -[`cslib-community/complexitylib`](https://github.com/cslib-community/complexitylib). The original, -pre-CSLib implementation remains available at the renamed historical repository -[`complexitylib-v1`](https://github.com/SamuelSchlesinger/complexitylib-v1), with archival pending -disposition of remaining work there. - -Moving the repository to CSLib Community is an owner and name change for continuing development, -not a handover of Samuel's editorial direction and not acceptance into upstream CSLib. AI -assistance is a development method, and community participation includes mathematical review, API -design, documentation and maintenance as well as proving new theorems. - -The repository consolidation has these maintenance requirements: - -* **Auditable claims.** Check each README result against its public statement, definitions, - assumptions, encodings and resource model. Preserve nonconstructive and conditional boundaries; - passing Lean does not establish that a statement matches its prose or literature source. -* **Reproducible validation and review.** Run all six checks on the migration revision, retain the - full-library axiom audit and representative clients, and record independent review with that - revision in the PR or commit description, following - [CONTRIBUTING.md](CONTRIBUTING.md#ai-assistance-and-review). -* **A usable contribution path.** A new contributor can find a bounded task, the relevant APIs, - source references, validation commands and review expectations without private conversation - history or a maintainer's agent installation. -* **One active project.** Preserve this repository's issues, pull requests, releases and history - through a repository transfer; archive V1 rather than maintaining two active libraries. Verify - redirects, CI, release assets and repository links after the move. - -Completing every V1 port, Jukna chapter, or future resource-bound improvement is not a condition -of the repository move. The work below remains available for subsequent, independently reviewed -batches. - -## Continuing priorities - -1. **First-order reductions and projections, with machine and uniformity bridges.** Complete - these milestones in order of their dependencies. Each requires public Lean results, a - nonvacuous client, a headline-abstract assessment, and independent mathematical, API and - formal-abstract reviews of the completed revision. - - - [ ] **Ordered first-order complexity, in standard terminology.** Decided 2026-10-19: the - library's first-order complexity follows the usual convention of descriptive complexity - [Immerman][Immerman1999]. Structures are ordered, on `{0, …, n-1}` with `n ≥ 2`, and FO - means FO(≤, BIT). The lower bound follows - [Proviso 1.15, p. 16](https://people.cs.umass.edu/~immerman/pub/ch0_1_2.pdf): - the numeric constants 0 and 1 are distinct. This corrects the handoff's `n ≥ 1`. - First-order reductions are first-order queries on lexicographically - ordered k-tuples, and `≤_fo`, `≤_fop` and `≤_qfp` keep their standard meanings. The - order-free `FO.Reduces`, `FO.QFReduces` and `FO.Definable` remain as a general layer of - interpretations without built-in order. The ordered notions get their own names. Restate - the headline results in the ordered setting: SAT, 3SAT, 3COL, IS, clique and VC - NP-complete under first-order or quantifier-free projections; FO(≤, BIT) ⊆ L; first-order - reductions are logspace reductions; REACH NL-complete; Circuit Value P-complete under - first-order reductions. The order-free versions cannot reach several of these: SAT → 3SAT - appears to need an order, and SAT-hardness without order needs an empty-structure - hypothesis. - The ordered query layer allows dependence on the canonical order; it does not impose - invariance under arbitrary permutations of the input relations. Numeric predicates are - computed from the universe size, not supplied as unverified input tables. - **Canonical-structure prerequisite completed (#33):** - [Ordered/Basic](Complexity/Logics/FirstOrder/Ordered/Basic.lean) supplies canonical - `≤`/`BIT` and numeric `0`/`1`/`max` on `Fin n`, `n ≥ 2`, using native Mathlib - terms/formulas and language sums. Input formulas, including constants and quantifiers, - preserve truth. [Ordered/Interpretation](Complexity/Logics/FirstOrder/Ordered/Interpretation.lean) - realizes forgetting the numeric expansion through the existing relational interpretation - API, with an isomorphism to the input. - **Target-constant prerequisite completed (#38):** - [Interpretation/Constants](Complexity/Logics/FirstOrder/Interpretation/Constants.lean) - adds finitely many formula-defined target constants, with explicit existence and uniqueness - inside the interpreted domain, and native formula/sentence truth-preserving pullback. - [Ordered/Constants](Complexity/Logics/FirstOrder/Ordered/Constants.lean) supplies valid - target `0`/`1`/`max` for every canonical structure with `n ≥ 2`. - **Full-domain tuple-order prerequisite completed (#43):** - [Ordered/Tuple](Complexity/Logics/FirstOrder/Ordered/Tuple.lean) gives the arbitrary-base - lexicographic rank bijection and exact first-difference order, reusing the existing - colexicographic index by coordinate reversal. - [Ordered/TupleInterpretation](Complexity/Logics/FirstOrder/Ordered/TupleInterpretation.lean) - defines quantifier-free strict/weak order and the canonical full-domain constants, with - proved unique selection and ranks `0`, `1`, `n^k - 1` for positive dimension. - **Full-domain successor prerequisite completed (#54):** - [Ordered/TupleSuccessor](Complexity/Logics/FirstOrder/Ordered/TupleSuccessor.lean) - proves that the carry formula holds exactly at consecutive arbitrary-base lexicographic - ranks, with explicit zero-dimension and maximum/no-wrap boundaries. Its generic compiler - preserves quantifier-freeness when the supplied source successor is quantifier-free. - The canonical `≤`/BIT instance uses a universal adjacency formula; no unconditional - quantifier-free successor claim is made for this basis. - **Canonical addition prerequisite completed (#64):** - [Ordered/Addition](Complexity/Logics/FirstOrder/Ordered/Addition.lean) defines one native - formula over `≤` and BIT whose semantics on every `Fin n`, `n ≥ 2`, is exact natural-number - addition `x + y = z`. Out-of-range sums have no satisfying result; this is not modular - addition. It formalizes the PLUS part of Immerman's Theorem 1.17(1), using the carry - characterization of Proposition 1.9. - **Canonical Bit Sum prerequisite completed (#91):** - [Ordered/BitSum](Complexity/Logics/FirstOrder/Ordered/BitSum.lean) defines one native - formula whose semantics on every `Fin n`, `n ≥ 2`, is `y = x.bitIndices.length`, with - exactly one output for each input. This proves Immerman's Lemma 1.18, historically due to - Barrington, Immerman and Straubing, using a balanced addition-tree variant of the source's - packed running-sum proof. Eight bounded words encode all node bits; their native decoder - uses exact shifts and fixed PLUS chains, with no assumed semantic certificate or variable - multiplication predicate. A fixed finite disjunction handles small numerals. - **Canonical multiplication completed (#102):** - [Ordered/Multiplication](Complexity/Logics/FirstOrder/Ordered/Multiplication.lean) defines - one native TIMES formula with exact ordinary-product semantics `x * y = z` on every - canonical `Fin n`, `n ≥ 2`. Every candidate is rejected on overflow. This completes the - PLUS/TIMES endpoint of Immerman's Theorem 1.17(1), using the proved native Bit Sum and - a carry-table variant of the source's packed short sums. Eight words store global - boundary carries; sixteen words store each local block. Both block endpoints agree with - the global words, all decoders constrain high bits, and the final carry vanishes from the - input-width bound. The witnesses fit for arbitrary universe sizes; a fixed finite branch - handles small inputs. No multiplication relation or semantic certificate is assumed. - **Full-tuple BIT lifting completed (#112):** - [Ordered/TupleBit](Complexity/Logics/FirstOrder/Ordered/TupleBit.lean) supplies an actual - native formula for every fixed dimension `k`, with exact `lexRank x`/`lexRank y` BIT - semantics on every canonical `Fin n`, `n ≥ 2`. It handles arbitrary bases, indices larger - than the source universe, high-index rejection and explicitly false dimension zero. - Native affine word arithmetic, multiplication and radix conversion represent the source - cardinality in seven digits and each tuple rank in `7k` digits. The formula witnesses a - positive binary radix with its cube below `n`; no out-of-domain scalar or supplied numeric - certificate is assumed. A fixed finite disjunction covers sizes two through eight. - This proves the full-domain BIT endpoint of Immerman's Exercise 1.33(3), with no - formula-size efficiency claim. - **Numeric-preserving full-tuple composition completed (#121):** - [Ordered/FullTuple](Complexity/Logics/FirstOrder/Ordered/FullTuple.lean) constructs the - actual canonical numeric interpretation from the proved native order, BIT and constant - formulas; clients supply only the target input-relation definitions. For `n ≥ 2` and - positive dimension `k`, ranking is an isomorphism of the entire ordered language to - `Fin (n^k)`, including genuine numeric constants, and native pullback preserves every - formula and sentence. Source input vocabularies may have functions; target input - vocabularies are relational. - [Ordered/FullTuple/Composition](Complexity/Logics/FirstOrder/Ordered/FullTuple/Composition.lean) - composes positive dimensions `k` and `l` with coordinate `(j,i)` mapped to `j*k+i`. - The proved rank identity compares the flattened base-`n` tuple with the outer base-`n^k` - tuple of inner ranks. The composite is isomorphic to the successive canonical targets, - and all formula/sentence pullbacks agree. No full-tuple numeric certificate is assumed. - This is the full-domain case of Immerman's Proposition 1.28 for relational intermediate - and output input vocabularies, with Remark 1.32's canonical numerics. It does not identify - base-`n` digits with binary strings. - **Native ordered model checking completed (#128):** - [FirstOrder/Ordered](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Ordered.lean) - proves that every fixed sentence over a finite relational input vocabulary expanded by - canonical `0`, `1`, `max`, order and BIT has its actual encoded query language in L. - Numeric atoms, including quantified ones, use proved native expressions; the input retains - unary cardinality and the existing framed input tables in `tupleIndex` order. Invalid table - shapes and sizes zero/one reject. Work space is logarithmic in the full encoded input length, - with no combined-complexity or arbitrary-raw-word claim. This is the relational-input case - of Immerman's Theorem 3.1. The original order-free empty-universe behavior is preserved. - **Canonical full-tuple interpretation transducer completed (#137):** - [Ordered/FullTuple/Encoding](Complexity/Logics/FirstOrder/Ordered/FullTuple/Encoding.lean) - and - [FirstOrder/Ordered/Reduction](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Ordered/Reduction.lean) - prove that every fixed canonical full-tuple interpretation between finite relational - input vocabularies computes its encoded target structure in logarithmic space. Admissible - sources of size `n ≥ 2` map to the canonical rank universe `Fin (n^k)` numbered by - `lexRank`, serializing only the target input relations in `tupleIndex` order; invalid - shapes and sizes zero and one map to a fixed malformed target outside every target query - language. For positive dimension `k > 0`, the decoded target with its own canonical - numerics is isomorphic to the interpreted full ordered structure preserving every - natural rank, and `encodedMap` is a logspace many-one reduction from the pulled-back - ordered query language to the target ordered query language. This is the full-domain - canonical transducer of Immerman's Proposition 3.5; restricted domains and class-level - closure are now covered by the #309 entry below. Projections and NL/P completeness remain - open. - **Ordered NP-to-ESO converse recovered (#173):** - [Fagin/Ordered](Complexity/Computability/Complexity/Fagin/Ordered.lean) defines every - arbitrary ordered query whose source-only encoding language is in NP by one ESO sentence - over the current canonical language. It retains the fixed `Fin n` order, requires `n ≥ 2`, - rejects malformed source tables, and imposes no permutation-invariance hypothesis. - The existing strict-verifier/tableau construction is reused through a shared power-sentence - lemma; the order-free characterization is unchanged. The ordered ESO-to-NP direction - remains open. - **Next milestones:** projections and NL/P completeness. These remain open. - The full-domain hypothesis matters: the paragraph after Exercise 1.33 warns that canonical - BIT on an arbitrary definable restricted domain need not be first-order definable. - Restricted-domain numeric preservation therefore requires its own explicit definitions - and certificate. - **Ordered `≤_fo` with domain formulas (#309, semantic layer):** - [Ordered/DomainInterpretation](Complexity/Logics/FirstOrder/Ordered/DomainInterpretation.lean) - maps a source to the tuples satisfying a domain formula, renumbered by lexicographic rank - (admissible when every source has at least two such tuples, the library's convention after - Proviso 1.15); its - [Encoding](Complexity/Logics/FirstOrder/Ordered/DomainInterpretation/Encoding.lean) gives - `encodedMap`, partial decoding `decode?` and the commutation lemma consumed by - `ManyOneReducibleBy.lift`. A numeric - [Certificate](Complexity/Logics/FirstOrder/Ordered/DomainInterpretation/Certificate.lean) - defines the target order, BIT and constants on domain tuples (Immerman's Remark 1.32 - requirement), yielding sentence pullback; - [Composition](Complexity/Logics/FirstOrder/Ordered/DomainInterpretation/Composition.lean) - pulls outer certificates back through inner ones, and - [Ordered/Reduction](Complexity/Logics/FirstOrder/Ordered/Reduction.lean) defines - `Ordered.Reduces` with `refl`, `trans`, `compl` and `Definable.of_reduces`. - [FullTuple/DomainInterpretation](Complexity/Logics/FirstOrder/Ordered/FullTuple/DomainInterpretation.lean) - embeds full-tuple interpretations with their native certificate and proves the encoded maps - agree. **First-order reductions are logspace reductions (#309):** one domain-counting - [transducer](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean), - parametrized by the formula compiler, computes order-free interpretations and - [ordered interpretations with a domain formula](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Ordered/Reduction.lean) - in logarithmic space; the full-tuple transducer is its `domain = ⊤` instance. - `DomainInterpretation.logSpaceReducible` needs no certificate, and - `Ordered.Reduces.logSpaceReducible` gives `≤_fo ⇒ ≤_log` with L/P closure (Immerman's - Proposition 3.10). Open: certificates for further restricted-domain families. - **Many-one core (#309, #314):** `PolyTimeReducible`, `LogSpaceReducible`, - `Ordered.Reduces`, `MappingReducible` and `FPTReducible` are instances of - [ManyOneReducibleBy](Complexity/Computability/Complexity/Reduction/ManyOne.lean), and - polynomial-time, logspace, `#P` (`SharpPHard`/`SharpPComplete`), search - (`SearchHard`/`SearchComplete`) and promise (`PromiseProblem.NPHard`) hardness/completeness - are instances of polymorphic `HardUnder` and `CompleteUnder`; only structurally distinct - reductions (`FO.Reduces`/`QFReduces`/`ReducesNontrivial`, two-condition promise - `PolyTimeReducible`, and `ParsimoniousReducible` on `α → ℕ`) remain outside - `ManyOneReducibleBy`. A witness-carrying reduction structure is deferred until a client - needs one (e.g. size bounds for Cook–Levin). - - - [x] **Order-free SAT reductions.** [SAT completeness](Complexity/Computability/Complexity/Fagin/SAT.lean) - is proved for isomorphism-closed classes in NP containing every empty structure, with a - nonempty-input variant. Order-free 3SAT and 3COL are interreducible; SAT reduces to - independent set on universes of at least two elements, and independent set, clique and - vertex cover are ESO-definable. The singleton obstruction to unrestricted SAT-to-independent-set - reducibility is proved. SAT-to-3SAT, graph-property hardness in this framework, and bridges - to the separately encoded problems remain outstanding. These are order-free variants; - the standard ordered completeness statements above remain open. - - - [ ] **FO reductions and projections.** The vocabulary-parametric, relativized core is - implemented in [ProjectionFormula](Complexity/Logics/FirstOrder/ProjectionFormula.lean) and - [Projection](Complexity/Logics/FirstOrder/Projection.lean): selection of one literal before - quantifying over input structures, mutually exclusive numeric cases, truth-preserving - substitution, identity/composition isomorphisms, and quantifier-free composition. The - [graph-complement client](Complexity/Logics/FirstOrder/Projection/Graph.lean) and tests cover - nonvacuity, empty universes, nullary relations and the failure of two-bit conjunction to be - a projection. Quantifier-free reducibility - ([QFReduces](Complexity/Logics/FirstOrder/Reduction/QuantifierFree.lean)), full-domain tuple - interpretations ([Interpretation/Tuple](Complexity/Logics/FirstOrder/Interpretation/Tuple.lean)) - and the tactics `fo_qf`, `fo_iso_closed`, `fo_simp` and `fo_reduction` - ([Tactic/FirstOrder](Complexity/Tactic/FirstOrder.lean)) are implemented, simplifying - composite and higher-dimensional interpretations and composite projections, with independent - set, clique and vertex cover as quantifier-free reducible - [structure classes](Complexity/Logics/FirstOrder/Problems/SizedGraph.lean). - **Still outstanding:** the classical positive-dimensional full-universe - specialization and canonical numeric preservation, projection reducibility on finite - structure classes, and the standard ordered machine encoding bridge. Reuse - [FO.Interpretation](Complexity/Logics/FirstOrder/Interpretation.lean) and - [FO.Reduces](Complexity/Logics/FirstOrder/Reduction.lean) for the semantic interfaces. State - the canonical order/`BIT` convention on `Fin n` explicitly; the classical qfp convention - excludes BIT ([Immerman–Landau, Definition 3.6](https://people.cs.umass.edu/~immerman/pub/mult.pdf)). - Arbitrary quantifier-free Boolean combinations of input relations are not projections. - [First-order model checking in L](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder.lean) - is proved for relational FO without order or BIT, and - [canonical ordered model checking](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Ordered.lean) - now includes genuine numeric constants, order and BIT for source sizes at least two. - - - [x] **Order-free interpretations as logspace reductions.** The - [machine-certified transducer](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Reduction.lean) - streams interpreted relation tables using tuple ranks. Every order-free interpretation - reduction to an isomorphism-closed target induces a logspace many-one reduction of encoded - query languages, with L/P closure. Empty universes and domains, nullary relations, - dimension zero, and invalid parsed table shapes are handled. Canonical full-tuple ordered - interpretations, with or without a domain formula, are instances of the same - [transducer](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean), - and ordered first-order reductions are logspace reductions - ([FirstOrder/Ordered/Reduction](Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Ordered/Reduction.lean), #309). - - - [x] **Circuit Value logspace completeness.** [Circuit Value is P-complete](Complexity/Computability/Complexity/Problems/CircuitValue/Completeness.lean) - under logarithmic-space many-one reductions, via a machine-certified tableau writer. - The theorem covers every injective instance encoding and implies membership in L exactly - when P equals L for every encoding. Work space excludes read-only input and write-only - output, and correctness is required on encoded instances. - - - [x] **Monotone Circuit Value logspace completeness.** - [Monotone Circuit Value is P-complete](Complexity/Computability/Complexity/Problems/MonotoneCircuitValue/Completeness.lean) - under logarithmic-space many-one reductions, using a dual-rail tableau and a shared - streaming writer. General Circuit Value reduces to it. No planarity restriction or - first-order completeness theorem is established by this construction. - - - [ ] **Circuit Value completeness under first-order reductions.** Prove P-hardness under - the standard ordered reduction via `REACHa → MCVP → CVP`, following - [Immerman, Chapter 3, Theorem 3.26 and Exercise 3.28](https://people.cs.umass.edu/~immerman/book/ch3.pdf). - Supply the alternating-logspace simulation of polynomial-time machines and the translation - from relational circuits to `encCircuitValue`. The logspace tableau theorem above does not - supply this stronger reduction or the ordered relational-to-machine encoding bridge. - - - [ ] **Uniform circuit families.** The current - [NC/AC/TC hierarchies](Complexity/Computability/Circuit/Boolean/DepthClasses.lean), - [ACⁱ[q] ⊆ TCⁱ](Complexity/Computability/Circuit/Boolean/ModMajority.lean) and - [carry-save threshold/majority simulation in NC¹ and NCⁱ⁺¹](Complexity/Computability/Circuit/Boolean/ThresholdNC1.lean) - (for polynomially fan-in-bounded threshold and majority circuits; eliminating unbounded - repeated-wire multiplicities in unrestricted `TCⁱ` requires Muroga's threshold - weight-bounding theorem) are - nonuniform, and [FO model checking in AC⁰](Complexity/Computability/Circuit/Boolean/FirstOrder.lean) - constructs nonuniform circuits over relational atomic inputs, without order/`BIT`. - [Polynomial-time function-family compilation](Complexity/Computability/Complexity/Problems/CircuitValue/Compilation.lean) - now certifies construction of circuit codes from encoded instances, with separately - prescribed unary input/output widths. Its proof reuses the uniform tableau writer, - prefix hardwiring and shared-input circuit composition; it establishes no depth bound. - The [carry-lookahead adder](Complexity/Computability/Circuit/Boolean/CarryLookahead.lean) - computes exact unsigned addition with carry-in and carry-out at every width, including zero. - Its depth is at most `7 + 2*ceil(log₂(w+1))`, with polynomial size and every gate charged. - The modular version has depth at most `8 + 2*ceil(log₂(w+1))`; a carry-save finishing client - preserves the existing 4-to-2 reducer's value modulo `2^w` and clears its second word. - The [native generators](Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean) - construct the complete binary gate/output codes from unary width, reusing fixed formula - templates and shared-input code assembly. This establishes polynomial-time uniformity for - these arithmetic circuits. The complete GSW shallow-decryption circuit and native constructor - are described above; stronger logspace and DLOGTIME uniformity remain open. - Define logspace and DLOGTIME uniformity with explicit gate-address, direct-connection and - input encodings. Certify circuit generation and evaluation and the relevant machine-to- - circuit simulations, preserving size, depth and construction-resource bounds. Prove - FO with order and `BIT` equals DLOGTIME-uniform AC⁰ under explicit input-access and encoding - conventions; an unqualified - nonuniform class definition or simulation is insufficient. - - - [ ] **Counting-machine characterizations.** The current - [#P/GapP definitions](Complexity/Computability/Complexity/Classes/SharpP.lean) use verifier - witness counts and differences of such counts. The - [occurrence-labelled terminal branch semantics](Complexity/Computability/Machines/Turing/MultiTape/Counting.lean) - and [canonical index-certificate bijection](Complexity/Computability/Machines/Turing/MultiTape/Counting/Certificate.lean) - now preserve accepting and rejecting counts separately, including equal-effect choices and - early halting. Increasing a sufficient all-branches clock preserves the counts; the time - predicate explicitly excludes stuck states (#93). The - [actual binary checker](Complexity/Computability/Machines/Turing/MultiTape/Counting/Checker.lean) - now has a tidy polynomial-time proof through existing finite storage and the loop calculus. - Its exact binary/index correspondence proves - [both terminal counts in #P and their difference in GapP](Complexity/Computability/Complexity/Classes/SharpP/Machine.lean) - for every polynomial clock (#92). With fixed finite control, a fixed number of tapes and - Boolean alphabet, the certificate length is `b * p(|enc a|)` for a machine-dependent fixed - width `b > 0`; invalid codes contribute to neither verdict. This counts only branches - halted by the clock. `HaltsWithin` additionally supplies full termination without stuck - branches. Runtime is polynomial in the input/certificate pair, with the machine fixed, - not uniform in a supplied machine description. - The [binary-guess scanner](Complexity/Computability/Machines/Turing/MultiTape/Counting/Guess.lean) - supplies one terminal branch per Boolean word of the input length, with an exact `n + 1` - clock and singleton halt. Its shared FreeM/List execution preserves each word's multiplicity. - The [List/native execution bridge](Complexity/Computability/Machines/Turing/MultiTape/Counting/Execution.lean), - [singleton deterministic lift](Complexity/Computability/Machines/Turing/MultiTape/Counting/Deterministic.lean) - and [shared-tape sequencing laws](Complexity/Computability/Machines/Turing/MultiTape/Counting/Sequential.lean) - now preserve exact occurrence multiplicities and add actual all-branches clocks (#110). - The sequencing bound explicitly assumes nonempty transition lists at every local view; - the actual scanner and singleton lift satisfy this condition. This is shared-tape - sequencing, without preparing or resetting a continuation's input. The - [closed buffered compiler](Complexity/Computability/Machines/Turing/MultiTape/Counting/Composition.lean) - now feeds each source output to a consumer with separately reserved blank work tapes, - retaining source scratch and the real input head (#113). Output redirection emits into - the buffer in each source transition; singleton deterministic preparation rewinds and - marks it in `word.length + 4` transitions, including the empty word. Exact full-configuration - and native count laws preserve every List occurrence. From initialized empty output, - nonblocking components with clocks `T₀` and `T₁` have native composite clock - `T₀ + (T₀ + 4 + T₁)`; the consumer bound must hold for every produced word. - The [actual guess-and-verify pipeline](Complexity/Computability/Machines/Turing/MultiTape/Counting/Verifier.lean) - now computes the witness length in unary, generates each witness once, retains the framed - instance, and runs the singleton-lifted tidy verifier (#116). Its fixed finite machine has - a polynomial all-branches clock in the original encoded input length, including framing, - both buffers and workspace restoration. The output List retains one occurrence per witness, - even when Boolean outcomes coincide. The - [#P characterization](Complexity/Computability/Complexity/Classes/SharpP/Characterization.lean) - combines this construction with the forward checker and preserves accepting and rejecting - counts separately. All constructed transition tables are globally nonblocking; the halting - contract is on encoded instances, hence all binary inputs when the encoding is `encBits`. - The [signed construction and GapP characterization](Complexity/Computability/Complexity/Classes/SharpP/GapMachine.lean) - now realize every difference of two #P counts by one native machine (#120, completing the - endpoint of #106). The [one-step verdict router](Complexity/Computability/Machines/Turing/MultiTape/Counting/Verdict.lean) - gives a successful witness one chosen-sign leaf and an unsuccessful witness one accepting - plus one rejecting leaf. A [two-occurrence selector](Complexity/Computability/Machines/Turing/MultiTape/Counting/Alternative.lean) - adds independently prepared families, with disjoint reserved work tapes and their original, - possibly unequal witness lengths. Routing a verifier of clock `T` costs `T + (T + 4 + 1)`; - combining routed clocks `S₊, S₋` costs `S₊ + S₋ + 1`. Extra clock time uses first-halt stability, - not extra choices. Zero, odd and negative gaps are included, with no oracle channels or - input-dependent machine advice. - The [UP](Complexity/Computability/Complexity/Classes/UP/Machine.lean) and - [FewP](Complexity/Computability/Complexity/Classes/FewP/Machine.lean) native iff endpoints - now transport their accepting-count bounds through the actual parsimonious #P bridge (#131). - Fixed finite parameters and a polynomial all-branches clock precede every encoded input; - the ambiguity bound is one for UP and a separate polynomial in encoded input length for - FewP. Rejecting and total branch counts are not bounded by the ambiguity polynomial. - Duplicate accepting occurrences remain distinct, while first-halt clock padding preserves - their multiplicities. - [Native oracle occurrence replay](Complexity/Computability/Machines/Turing/MultiTape/Counting/Oracle/Replay.lean) - now gives exact ordered equality between the shared FreeM run and canonical fixed-clock - index certificates (#136), under an explicit positive uniform local-list length bound. - It retains consumed indices, complete configurations and branch-local private oracle state; - live cutoffs are retained, with terminal filtering and both verdict counts proved separately. - Trace erasure recovers the ordinary shared interpretation, and the Empty-channel cases - recover raw closed List execution and the existing terminal certificate decoder. - This is semantic replay, without a nonblocking or halting hypothesis. A later oracle clock - contract must be nonvacuous and uniform over admissible handlers; the generic total-PMF - predicate cannot be instantiated blindly at an occurrence interface containing `Fin 0`. - Closed counting clocks and characterizations are unaffected. Efficient encoded oracle - checking, response-access costs, and native oracle-machine characterizations remain open; - resource bounds must be uniform over admissible oracles, while correctness may specialize - to one fixed language oracle. - -2. **Complete theorem ports using the existing certificate APIs.** Extend automation when a - concrete port is blocked or several clients repeat the same proof burden. Constructor, projection, - lookup and composition rules should infer encodings for ordinary functional expressions. - Test equivalent spellings and alternative encodings before adding tactic cases. Generalize - reusable list, bounded-table, cache and nested-loop invariants where clients need them; - callers supply the meaningful invariant, and automation handles routine encoding arithmetic. - Use Cook–Levin and GGM as demanding regression clients. General open-program composition - remains separate from the implemented - [closed stateful substitution](Complexity/Computability/Probabilistic/OracleSimulation.lean). - Extend quantitative certificates to retain separate time, workspace and output-size bounds - through composition. Apply cumulative streaming contracts to captured iteration and nested - loops, discharging routine encoding arithmetic automatically. Certify PRG stretching with - seed length, round count and generator cost kept separate. - -3. **Practical PCP and expander constructions.** The - [PCP theorem](Complexity/Computability/PCP/Completeness.lean) includes certified construction - and verification, but the fixed parameters are enormous. Develop a reasonably runnable - construction and measure complete reductions. The - [six-query tester](Complexity/Computability/PCP/SelectedComposition.lean) now feeds the shared - executable composition compiler and the full reduction, with a 128-symbol output alphabet and - a certified amplification gap of `2^-61`. The final binary verifier also encodes labels and - repeats its check, so it does not have a six-query bound. The existing rotation certificate is - polynomial in the number of vertices; polynomial time in the bit length of a vertex name - remains a stronger, separate target. The [expander-walk hitting bound](Complexity/Foundations/Combinatorics/Expander/Hitting.lean) - now gives a finite probability estimate for avoiding sets, including changing sets along the - walk. Derive machine-level error reduction and extractor guarantees with certified seed and - evaluation costs; the hitting estimate alone does not supply those algorithms. - -4. **Reduce repeated proof bookkeeping.** Improve configuration views, tape partitions, handoff - identities and preservation rules when they simplify multiple clients. Keep simplification - narrowly oriented and machine transitions out of global simp. Share mathematical bookkeeping - only with demonstrated reuse, counting helper proofs as part of the total cost. - -5. **Curated formal abstracts and PDFs.** The selection in - [abstracts/catalogue.json](abstracts/catalogue.json) replaces the former paper/TeX index. - Each promoted group has a checked Abstract/Bridge pair, explicit model and scope notes, and - a generated individual PDF. Selection requires a substantial full endpoint rather than broad - coverage of every library theorem. Continue to improve readability and independently compare - changed abstracts with their final source statements. `#check_abstract` inspects elaborated - dependencies; notation, macros and local instances are excluded by the skill's rules rather - than mechanically. Generated PDFs are review and dissemination artifacts, not additional proofs. - -6. **Plain computability in definitions and public results (#456).** Plain - `ComputableInPolyTime` and its tidy bridges are in place, together with plain space, big-O and - FPT notions (#551). `P`, `NP`, `FNP` and the polynomial-time reductions (#546), the - probabilistic, counting and hierarchy classes (#547), the `TFNP` subclasses (#548), FPT - reductions, kernels and proof systems (#549) and the cryptographic primitives (#550, including - deterministic families in commitment hiding and zero-knowledge) use it, and the WPP/LWPP - robustness results expose plain certificates (#562). Remaining: isolating tidy computability - to proofs everywhere, by mechanically mirroring the calculus in plain form (#608), sweeping - the remaining public tidy statements and guarding the result in CI (#456), and switching the - abstract bridges to the shared predicate. - -## Remaining theorem developments - -The port still includes substantial mathematical developments beyond the completed reference -results. Track these by their public theorems, rather than by source-file counts. -Jukna coverage below is an additional target beyond the V1 port: - -* **Real-algebraic decision procedures.** The [sign-query counting identity](Complexity/Foundations/Data/Polynomial/SignQueries.lean) - expresses scaled finite sign-pattern counts through integer product-sign queries, including - distinct real roots. Porting the Sturm–Tarski query evaluator, native space certificates and - ETR upper bound from [lean-canny](https://github.com/SamuelSchlesinger/lean-canny) remains open. -* **Mass-production constructor runtime.** Certify runtime separately from the native gate-cost - bounds in [Uhlig](Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig.lean) and - [fine mass production](Complexity/Computability/Circuit/Boolean/MassProduction/Fine.lean). - The current constructions choose information sets and line menus nonconstructively. -* **Iterated-function circuits.** Port the - [existing Lean development](https://github.com/SamuelSchlesinger/iterating-functions/blob/main/lean/README.md): - input-time and batched iteration, navigation and hitting times, sparse-counter and - affine-controller bounds, and hard-power counting. It already uses CSLib - circuits and some mass-production infrastructure. The - [functional-graph foundations](Complexity/Foundations/Combinatorics/FunctionalGraph.lean) - (transient and cycle structure, checkpoint packing, exact distinct-power counts, - [cycle-spectrum reduction and canonical hitting-time identities](Complexity/Foundations/Combinatorics/FunctionalGraph/Spectrum.lean), - [min-max duality for required paths in in-forests](Complexity/Foundations/Combinatorics/FunctionalGraph/ForestDuality.lean), - [semantic correctness of the six-step distinguished-point procedure](Complexity/Foundations/Combinatorics/FunctionalGraph/DistinguishedPoints.lean), - [checkpoint forests](Complexity/Foundations/Combinatorics/FunctionalGraph/CheckpointForest.lean), - [interval labels](Complexity/Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean), - [compressed segments](Complexity/Foundations/Combinatorics/FunctionalGraph/ForestSegments.lean) - and [compressed-forest navigation](Complexity/Foundations/Combinatorics/FunctionalGraph/ForestNavigation.lean)) and - [native circuit iteration](Complexity/Computability/Circuit/Iteration.lean) with retained - orbits are in place, as are the [fixed-power theorem](Complexity/Computability/Circuit/Boolean/Iteration.lean), - its encoded and burn-in forms, the optimized square-root bounds and permutation inversion; the - [input-time](Complexity/Computability/Circuit/Boolean/Iteration/InputTime.lean) and - [batched iteration](Complexity/Computability/Circuit/Boolean/Iteration/Batch.lean), cycle labels, - transient depths, additive long-time bounds, - [compressed-forest reachability](Complexity/Computability/Circuit/Boolean/Iteration/ForestCircuits.lean), - [hitting-time navigation](Complexity/Computability/Circuit/Boolean/Iteration/NavigationCircuits.lean), - [complete visit-schedule circuits](Complexity/Computability/Circuit/Boolean/Iteration/VisitScheduleCircuits.lean), - [sparse-counter navigation, visit schedules and hitting-time bounds](Complexity/Computability/Circuit/Boolean/Iteration/SparseNavigation.lean), - [autonomous-controller / affine-payload iteration bounds](Complexity/Computability/Circuit/Boolean/Iteration/AffineController.lean), - [universal-map simulation and hardwiring](Complexity/Computability/Circuit/Boolean/Iteration/UniversalMap.lean), - [in-place multi-head machine bounds](Complexity/Computability/Circuit/Boolean/Iteration/InPlace.lean), - [sequential-squaring exponent reduction](Complexity/Computability/Circuit/Boolean/Iteration/SequentialSquaring.lean), - [hard-power counting, modular-counter lower bounds, and prime-cycle permutations](Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter.lean), - and [batched modular-counter upper and lower bounds](Complexity/Computability/Circuit/Boolean/Iteration/CounterBatch.lean) - are also implemented. Nonuniform circuit - existence does not certify the preprocessing algorithm's runtime. -* **Rational hitting-list runtime.** The [rational-matrix hitting lists](Complexity/Computability/Circuit/Rational.lean) - are ported, and the complete polynomial-time generator runtime is proved: - [generator parameter certificates](Complexity/Computability/Circuit/Rational/Runtime/Parameters.lean), - [binary integer arithmetic](Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean), - polynomial-time staged division-free integer determinant `detRows_polytime` - ([Runtime/Determinant](Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean)), - [binary division and remainder](Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryDiv.lean) - (`binary_divMod`, `binary_div`, `binary_mod`), - [Euclidean GCD](Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Gcd.lean) - (`binary_gcd`), - [canonical natural and reduced-rational encoding certificates](Complexity/Computability/Circuit/Rational/Runtime/Encode.lean) - (`encodeNat_polytime`, `encodeDivInt_polytime`), - [integer lift tables](Complexity/Computability/Circuit/Rational/Runtime/Lift.lean) - (`liftRows_polytime`), - [per-point Cramer normalization and tuple encoding](Complexity/Computability/Circuit/Rational/Runtime/Point.lean) - (`pointWord_polytime`), and - [grid enumeration, unary input parsing, and the standalone generator](Complexity/Computability/Circuit/Rational/Runtime.lean) - (`hittingList_polytime`, `hittingGenerator_polytime`, `hittingGenerator_spec`), charging all - arithmetic and storage growth. Polynomial bit complexity of formula evaluation on the emitted - matrices remains separate. -* **Explicit frontier extractor.** Port v1's explicit sumset-extractor construction - (`Complexitylib/Algebraic/LowerBound/Cutwidth/Extractor`) together with its instantiation: - an explicit family in `Complexity.P encBits` that discharges the hypotheses of the worst-case or - average-case [frontier lower bounds](Complexity/Computability/Circuit/Frontier/FanInTwo.lean). - Such a port needs an independent correctness review of the frontier core, since it would exceed - the library's unconditional `3.5 N - o(N)` bound in `P` - (`AffineDisperser.exists_mem_P_eventually_le_size`). The earlier conditional sumset-extractor - layer was withdrawn (#391). -* **Weighted threshold representations.** Complete the remaining results in - [Threshold Circuits as Decision Trees and Finite-State Programs](https://github.com/SamuelSchlesinger/threshold-circuits). - The [separable and bi-monotone comparison tree rectangle bounds](Complexity/Computability/DecisionTree/Separable.lean), - [decision-tree node-count, rank, decision-list, and energy bounds for inner product](Complexity/Computability/DecisionTree/InnerProduct.lean), - exact [inner-product and rectangle-density activity bounds](Complexity/Computability/Circuit/Boolean/WeightedThreshold/InnerProduct.lean) - (including [shifted-baseline activity](Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activity.lean) - and [decision-tree affine leaf scores](Complexity/Computability/DecisionTree/AffineScore.lean)), - [native scalar-capacity bound](Complexity/Computability/Circuit/Boolean/WeightedThreshold/CapacityCircuit.lean) - (including the single-direction, direction-run, and multilevel threshold capacity corollaries), - [mixed-activation capacity bound](Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activation.lean), - [median-cut rectangle and cut bounds](Complexity/Computability/Circuit/Boolean/WeightedThreshold/Cut.lean), - [fan-in-two component and block-excess bounds](Complexity/Computability/Circuit/Boolean/WeightedThreshold/Components.lean), - [direction-menu capacity bounds](Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean) - (including bounded internal fan-in and bounded integer internal-weight corollaries), - [pending-bias state simulation and input-summary / phased-cut lower bounds](Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean), - [scalar query-activity run capacity and Cover enumerative coding bounds](Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean), - and [unambiguous transcript cells and quadratic-potential unique-sink representations](Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean) - are proved. Port v1's explicit source-reduction family. - Further manuscript work includes universal scalar circuit synthesis, - entropy and asymptotic activity bounds, and geometric cutting. - -* **Worst-case hardness and derandomization.** The - [worst-case-hardness implication P = BPP](Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean) - is proved for hardness at all large lengths, by the Sudan–Trevisan–Vadhan encoding and - Nisan–Wigderson. Remaining: the infinitely-often variant and the EXP ⊄ P/poly endpoint of - Babai, Fortnow, Nisan and Wigderson. -* **Further PCP consequences.** Constant-factor NP-hardness of approximating Independent Set, - Clique and Vertex Cover is [proved](Complexity/Computability/PCP/Approximation/IndependentSet.lean) - via Karp's occurrence graph. Build the FGLSS clique-hardness reduction and amplification on the existing - [gap-preserving reductions](Complexity/Computability/Complexity/Classes/Promise/Reduction.lean) and certified PCP - construction; retain the exact gap and reduction runtime. -* **Randomized communication and information.** The `Ω(n)` bounded-error randomized disjointness - lower bound is [proved](Complexity/Computability/Communication/Disjointness.lean); Raz–Wigderson's - monotone depth bound is [proved](Complexity/Computability/Circuit/Monotone/BipartiteMatching.lean) - for bipartite matching (general graphs remain). Develop - information complexity and its reductions to streaming and sketching lower bounds. -* **List decoding.** Extend [Sudan's Reed–Solomon list-decoding theorem](Complexity/Foundations/Data/Code/Sudan.lean) - to Guruswami–Sudan list decoding. Keep interpolation, list-size/agreement guarantees and - uniform decoding runtime as separate obligations. -* **Hypercontractivity and formula lower bounds.** KKL, Talagrand's inequality and Friedgut's junta - theorem are [proved](Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean). Extend the existing - [hypercontractivity results for p ≤ 2 ≤ q](Complexity/Foundations/BooleanAnalysis/Hypercontractivity.lean) - and their Boolean-analysis applications. Continue formula lower bounds beyond the existing - [Khrapchenko bound](Complexity/Computability/Circuit/Boolean/Khrapchenko.lean), - [Subbotovskaya shrinkage](Complexity/Computability/Circuit/Boolean/Formula/Subbotovskaya.lean) and - [Andreev's `n^(5/2 - o(1))` lower bound](Complexity/Computability/Circuit/Boolean/Formula/Andreev.lean), - following the Jukna coverage below. -* **Search and parameterized complexity.** [FNP, FP and TFNP](Complexity/Computability/Complexity/Classes/TFNP.lean) - are defined with polynomial-time search reductions, `FP = FNP` exactly when `P = NP` is - [proved](Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean), and `TFNP ⊆ FP` - implies `NP ∩ coNP ⊆ P`. PLS, PPP, PPAD and PPA and their - [canonical complete circuit problems](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Completeness.lean) - are proved (#151, #168). Develop CLS and further complete search problems. Building on - [FPT, XP and fpt-reductions](Complexity/Computability/Complexity/Parameterized.lean), the - kernelization characterization of FPT, a bounded-search-tree algorithm for vertex cover (#152), - and [Buss's polynomial kernel for vertex cover](Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean) - (#270) are proved; develop strongly uniform variants and the W hierarchy. - The long-term coverage table identifies the broader class families. -* **Universal hashing (#640, track D).** Proved (#663): one definition each of - [`ε`-universal and `ε`-Δ-universal](Complexity/Probability/HashFamily.lean) families; - pairwise independent families are - [universal and Δ-universal](Complexity/Probability/PairwiseIndependentHash/Universal.lean), the - Boolean-matrix and subset-sum families are Δ-universal, the - [Carter–Wegman polynomial](Complexity/Probability/HashFamily/Polynomial.lean) and - [multiply-shift](Complexity/Probability/HashFamily/MultiplyShift.lean) families are proved, and - the [leftover hash lemma](Complexity/Probability/UniversalHash.lean) is proved over - `ε`-universal families (`IsUniversalHash.leftover_hash`) with `IsTwoUniversal` as its - `1 / |Output|` case and the pseudoentropy clients updated. -* **Sigma protocols, Schnorr identification and Fiat–Shamir (#581).** Boneh–Shoup Chapter 19. - The exact algebraic core is proved: - [Sigma protocols](Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean) with explicit - extractors and perfect simulators, the - [linear-preimage protocol](Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean) over prime - order `q` with Schnorr, Okamoto, Chaum–Pedersen and linear systems as instances, and - [AND/OR composition](Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean). The exact - [rewinding lemma](Complexity/Probability/Rewinding.lean), the extraction bound - `ε ≤ 1/N + √ε'` and HVZK ⇒ eavesdropping security are proved for - [identification from Sigma protocols](Complexity/Crypto/Protocols/SigmaProtocol/Identification.lean) - and [Schnorr identification](Complexity/Crypto/Protocols/SigmaProtocol/SchnorrIdentification.lean). - The [discrete-log assumption](Complexity/Crypto/Computational/DiscreteLog.lean) is stated for - a family of prime-order groups with plain polynomial-time operations, instantiated by - [Schnorr groups](Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean), and - [Schnorr identification](Complexity/Crypto/Computational/SchnorrIdentification.lean) is secure - against direct attacks by uniform strict PPT impersonators under it. The general - [forking lemma](Complexity/Probability/Forking.lean) (Bellare–Neven) is proved, also for - [oracle programs](Complexity/Languages/Probabilistic/Forking.lean) with explicit coins and - presampled answers. [Fiat–Shamir signatures](Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean) - in the [random-oracle model](Complexity/Crypto/Protocols/Signature/RandomOracle.lean) are - correct and, exactly, EUF-CMA secure with the bound - `Qs · (Qs + Qro) · δ + (Qro + 1)/N + √((Qro + 1) · ε')` of Theorem 19.16 and Equation 19.21, - by the - [difference lemma](Complexity/Languages/Probabilistic/UntilBad.lean), presampling and forking; - [Schnorr signatures](Complexity/Crypto/Protocols/SigmaProtocol/SchnorrSignature.lean) have - `1/q`-unpredictable commitments and the exact bound with `δ = 1/q`. - Open (see #640): computational Schnorr signatures under discrete log for strict PPT forgers, - and security against eavesdropping in the strict-PPT model, where simulating transcripts needs - approximately uniform `ZMod q` samples and hence an explicit statistical-distance term. -* **Diffie–Hellman assumptions and ElGamal encryption (#640, track C, #873).** Boneh–Shoup - Section 10.5 and Exercise 11.5. Over a `PrimeOrderGroupFamily`, - [Computational and Decisional Diffie–Hellman](Complexity/Crypto/Computational/DiffieHellman.lean) - (`cdhGame`, `CDH`, `ddhRealGame`, `ddhIdealGame`, `DDH`) are formalized with the reductions - `DDH ⇒ CDH ⇒ DiscreteLog` (`CDH.discreteLog`, `DDH.cdh`, `DDH.discreteLog`) and the distributional - DDH rerandomisation lemma (`ddhRerandomizeLaw_real`, `ddhRerandomizeLaw_ideal`, Exercises 10.8–10.9). - [ElGamal public-key encryption](Complexity/Crypto/Computational/ElGamal.lean) (`elGamalEncrypt`, - `elGamalDecrypt`, polynomial-time encoded decryption `decodeElGamal`, and bit encryption - `elGamalCPAGame`) is proved IND-CPA secure for one-bit messages under DDH - (`advantage_elGamalCPAGame_le`, `DDH.elGamalINDCPA`, Boneh–Shoup Exercise 11.5(a)). Open: - group-element messages and efficient honest key generation/encryption, the efficient DDH random - self-reduction (Exercise 10.10), hashed ElGamal, Cramer–Shoup CCA - security, and Pedersen commitments over `PrimeOrderGroupFamily`. -* **Lattice identification and signatures (#640, track B).** The short-integer-solution - hypothesis, exact box rejection sampling and Lyubashevsky identification are in review (#660). - Open: Fiat–Shamir with aborts and signatures from SIS [Lyubashevsky 2009, 2012]; efficiency - certificates for the identification simulator and extractor; SIS for a general (prime) modulus; - module SIS and module LWE over polynomial rings, and Dilithium-style signatures as theory, not a - parameter set or ciphersuite. -* **Zero-knowledge proof systems toward libzk (#643, #640).** The - [interactive-reduction core](Complexity/Computability/Interactive/Basic.lean) has typed - public-coin protocols with oracle access to the prover's messages, worlds for the oracle model, - and named extractors and simulators. It defines completeness, soundness, straight-line knowledge - soundness, round-by-round soundness and HVZK; knowledge soundness and HVZK are stated in the - plain model. In the plain model, - [sequential composition](Complexity/Computability/Interactive/Sequential.lean) is proved for - completeness, soundness, knowledge soundness and round-by-round soundness, and so is per-stage - iteration. [Round-by-round soundness implies soundness](Complexity/Computability/Interactive/Plain.lean). - [Sumcheck with a final evaluation check](Complexity/Computability/Interactive/Sumcheck.lean), - the first client, is perfectly complete and has soundness error `n · d / |F|`; both follow from - the one-round theorems by composition. Open, in order: - - the `PublicCoin → IP` bridge, with a uniform word verifier and adversarial decoding; - - parallel and AND/OR composition, and round-by-round knowledge soundness; - - oracle statements. Today a later phase cannot query an earlier phase's oracle message, - because `Verifier.append` routes the second verifier's queries only to its own messages. - Sumcheck followed by an evaluation query on a committed polynomial needs this, and so do FRI - and Ligero. The design item is virtual output oracles, as in ArkLib's - `OracleOutputSimulation`. Knowledge soundness and zero knowledge in oracle worlds go with it: - extractors that see the prover's queries, and simulators that program the world; - - efficiency-certified simulators and extractors, and auxiliary-input zero knowledge (#704) - on the core; - - polynomial commitment and evaluation-query reductions, and the Ligero IOP; - - the BCS transform from public-coin IOPs to non-interactive arguments in the random-oracle - model; - - VOLE as an ideal functionality and VOLE-in-the-head; - - the compositional structure of libzk (Shelat's IETF draft) as a composition of these - components, stated as theory without concrete ciphersuites. - - The design is on #643, and the TQBF, PCP and GMW bridges are recorded there. -* **GKR delegation (#892).** [Layered](Complexity/Computability/Interactive/GKR/Layered.lean) - defines layered arithmetic circuits and proves the GKR identity expressing the multilinear - extension of a layer through the wiring predicates and the layer below. - [Summand](Complexity/Computability/Interactive/GKR/Summand.lean) gives the polynomial each - layer's sumcheck runs on (its sum, values and degree at most two per variable), and - [Bundle](Complexity/Computability/Interactive/Bundle.lean) runs a family of reductions on - statement-dependent parameters with the same completeness and round-by-round soundness. - [Protocol](Complexity/Computability/Interactive/GKR/Protocol.lean) assembles the GKR protocol - (output step, bundled sumcheck and line step per layer, input step): perfectly complete and - sound with error `(width depth + ∑ 5 · width i) / |F|`, by composition. Open: verifier efficiency - under log-space uniformity (M3), and the route to NEXP ⊆ MIP. -* **Classic symmetric constructions (#640, track D).** Proved: PRF-based MACs (#677), keyed - collision-resistant hash families and Merkle–Damgård (#678), universal hashing (#663), - [Carter–Wegman MACs from Δ-universal hashing](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) - (#736, #746, #842, including one-time, adaptive multi-query issued-counter, arbitrary-pad hybrid, - and exact single-query fixed-nonce `prfRealGame`/`prfIdealGame` reduction bounds), and the - Even–Mansour cipher in the ideal-permutation model (algebraic permutations, one-query secrecy, - one-sided query security, 2-query breaks when omitting either whitening key, the Boneh–Shoup - Theorem 4.10 bad-key transcript intersection bound `2 * Q_e * Q_π / |G|`, exact equivalence of - the two-sided ideal and fixed-key real games with lazy bidirectional random-permutation samplers - in `evenMansourIdealGame_eq_lazy` and `realGameForKey_eq_lazy`, the key-shifted lazy permutation - coupling inequality `run_idealLazyHandler_good_le_realLazyHandler`, and the full two-sided PRP - `Game.advantage` bounds `2 * Q_e * Q_π / |G|` in - `advantage_evenMansourRealGame_evenMansourIdealGame_le` and - `advantage_singleKeyEvenMansourRealGame_evenMansourIdealGame_le`, #761, #834). - [Feistel networks and the Luby–Rackoff theorem](Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean) - (#748, #834, Boneh–Shoup Section 4.4 / Luby–Rackoff 1988), backed by the shared - [lazy bidirectional random-permutation sampler](Complexity/Languages/Probabilistic/RandomPermutation.lean) - (#834), prove the `Q.choose 2 * ε + Q.choose 2 / |G|` - 3-round adaptive CPA bound with Δ-universal Round 1 - (`advantage_feistel3HashIdealGame_randomFunctionGame_le`), the `2 * Q.choose 2 / |G|` - uniform-random-round corollary (`advantage_feistel3RandomRoundsGame_randomFunctionGame_le`), the - 3-round and 4-round PRF-to-Feistel hybrid bounds - (`advantage_feistel3KeyedGame_randomFunctionGame_le`, - `advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le`), the PRP-PRF switching - bound `Q.choose 2 / |G|²` and 3-round PRP bounds against a uniform random permutation - (`advantage_idealPermGame_randomFunctionGame_le`, - `advantage_feistel3RandomRoundsGame_idealPermGame_le`, - `advantage_feistel3KeyedGame_idealPermGame_le`), and the 3-query - chosen-ciphertext attack against 3-round Feistel (`eval_feistel3_feistel3CCAAttack`, with the - equal-input sanity check `advantage_feistel3CCAAttack_self`, the finite positive gap - `(|Equiv.Perm (G × G)|)⁻¹ ≤ advantage` against the true bidirectional random-permutation game - `idealStrongGame` for `|G| ≥ 3` in `le_advantage_feistel3CCAAttack_idealStrongGame`, the - quantitative nonnegligible lower bound `1 - |G|⁻¹ - 4 / |G|² ≤ advantage` against - `idealStrongGame` for any `l₀ ≠ l₁` in `le_advantage_feistel3CCAAttack_idealStrongGame_of_ne`, - and the separate exact `1 - |G|⁻¹` bound against the independent-table benchmark - `independentTableStrongGame` in `advantage_feistel3CCAAttack_independentTable`). - Open: `IsOraclePPT` admissibility of the PRF-pad reduction, uniform word-level forger/hash - families, the asymptotic `PseudorandomFunction` corollary, and fresh-nonce multi-query - Carter–Wegman MAC security (#736); the 4-round strong Feistel information-theoretic collision - bound (#748); and the Naor–Reingold PRF from the decisional Diffie–Hellman assumption. - -* **Lattice Sigma protocols and post-quantum signatures (#640, track B).** Proved (#645): the - [SIS hypothesis](Complexity/Crypto/Computational/SIS/Basic.lean) for power-of-two moduli, exact - [box rejection sampling](Complexity/Probability/RejectionSampling.lean), - [Sigma protocols with aborts](Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean), and - [Lyubashevsky identification](Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky.lean) with - completeness up to aborts and its exact abort probability, special soundness extracting a short - integer solution of `[A | T]`, and exact HVZK for the erased-abort projection. Full interactive-view simulation remains open - (#680/#643). Open: Fiat–Shamir with - aborts and its signatures (after track A's random-oracle Fiat–Shamir), strict-PPT samplers for - integer boxes, identification security under SIS, general moduli, module SIS and module - lattices toward Dilithium-style schemes. - -The current V1 port excludes the circuitized anti-checker, hardness-magnification argument and -MINKT/MINCKT developments. The long-term canon above includes metacomplexity; those results should -return as independently scoped, reviewed developments rather than automatic legacy ports. Retain -existing checked [MCSP definitions](Complexity/Computability/MCSP/Basic.lean), -[succinct variants](Complexity/Computability/MCSP/Succinct.lean), -[Shannon bounds](Complexity/Computability/MCSP/Shannon.lean) and -[anti-checker existence](Complexity/Computability/MCSP/AntiChecker.lean). -These do not include an efficient anti-checker generator or a hardness-magnification theorem. - -## Finishing the recovered developments - -Complete bounded endpoints on ordinary branches, with the six checks and independent API, -correctness and formal-abstract reviews before closing a milestone. Retain the FO-reduction -and machine-characterization priorities above. The native NL complement theorem is proved below. -The Arthur–Merlin and hardness-amplification developments have their own prerequisites and should be split at the -following endpoints, rather than submitted as class definitions or conditional wrappers alone. - -| Development | First independently useful endpoint | Remaining endpoint and dependencies | -| --- | --- | --- | -| Iterated functions M2b | Sparse-counter centralizers and signed fixed powers are in [SparseDisplacement](Complexity/Computability/Circuit/Boolean/Iteration/SparseDisplacement.lean). Interval charts, encoding/decoding, canonical labels and additive variable-time circuits are in [SparseTime](Complexity/Computability/Circuit/Boolean/Iteration/SparseTime.lean), including both charged coordinate conversions. General compressed-forest reachability, first-hitting-time navigation, and complete visit-schedule circuits are in [ForestCircuits](Complexity/Computability/Circuit/Boolean/Iteration/ForestCircuits.lean), [NavigationCircuits](Complexity/Computability/Circuit/Boolean/Iteration/NavigationCircuits.lean), and [VisitScheduleCircuits](Complexity/Computability/Circuit/Boolean/Iteration/VisitScheduleCircuits.lean), with combinatorial checkpoint forests, interval labels, nonmerging segments, and compressed-forest navigation in [CheckpointForest](Complexity/Foundations/Combinatorics/FunctionalGraph/CheckpointForest.lean), [ForestIntervals](Complexity/Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean), [ForestSegments](Complexity/Foundations/Combinatorics/FunctionalGraph/ForestSegments.lean) and [ForestNavigation](Complexity/Foundations/Combinatorics/FunctionalGraph/ForestNavigation.lean), and sparse-counter specializations in [SparseNavigation](Complexity/Computability/Circuit/Boolean/Iteration/SparseNavigation.lean), [ResidueAdd](Complexity/Computability/Circuit/Boolean/Iteration/ResidueAdd.lean) and [HittingTime](Complexity/Foundations/Combinatorics/FunctionalGraph/HittingTime.lean). Autonomous controllers and affine-payload iteration bounds are in [AffineController](Complexity/Computability/Circuit/Boolean/Iteration/AffineController.lean). Universal-map simulation, product/group-action hardwiring, in-place multi-head machine bounds, and sequential-squaring reduction are in [UniversalMap](Complexity/Computability/Circuit/Boolean/Iteration/UniversalMap.lean), [InPlace](Complexity/Computability/Circuit/Boolean/Iteration/InPlace.lean) and [SequentialSquaring](Complexity/Computability/Circuit/Boolean/Iteration/SequentialSquaring.lean). Ordered circuit-description counting, modular-counter $\tilde\Omega(2^{n/2})$ power lower bounds, remainder reductions, subexponential-horizon barriers, hash-class prime-cycle permutations, and batched modular-counter upper and lower bounds are in [CircuitCounting](Complexity/Computability/Circuit/Boolean/Iteration/CircuitCounting.lean), [ModulusCounter](Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter.lean), [PrimeCycles](Complexity/Computability/Circuit/Boolean/Iteration/PrimeCycles.lean) and [CounterBatch](Complexity/Computability/Circuit/Boolean/Iteration/CounterBatch.lean). All ports follow source `c4cfa198`. | Done: all M2b iteration endpoints are proved. Nonuniform circuit existence does not certify preprocessing runtime. | -| NL = coNL | Done: [streaming inductive counting](Complexity/Algorithms/Reachability/InductiveCounting/Bounds.lean), with exact acceptance semantics, logarithmic-size registers and bounded termination on every branch. Certificates are checked without retaining paths or a reachable set. | Done: [native complement decider](Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting.lean) and [`NSPACE(s) = coNSPACE(s)`](Complexity/Computability/Complexity/Classes/Space/Nondeterministic.lean) for every bound with `log₂ n ≤ s n`, constructible or not, with [NL = coNL](Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean) as the case `s = log₂`, for arbitrary injective instance encodings. Compact configuration IDs of a growing radix and read-only input queries are compiled to finite-state native NTMs, with every-prefix workspace `O(s n)` and every-branch halting; the radix grows only after a certified overflow, as in Immerman's remark after his Theorem 1. The source may be a `RecognizesInSpace` recognizer with looping branches; these recognize exactly the native `NSPACE` problems. General space-constructible Savitch bounds remain separate. Follow-ups (#885): [STCON is NL-complete](Complexity/Computability/Complexity/Problems/STCON/Completeness.lean), [2SAT is NL-complete](Complexity/Computability/Complexity/Problems/TwoSAT/Completeness.lean). | -| Arthur–Merlin | Done: verifier-based MA and AM, error reduction, NP ∪ BPP ⊆ MA ⊆ AM ⊆ Π₂ᵖ, MA ⊆ Σ₂ᵖ ∩ Π₂ᵖ and MA ⊆ SBP ([ArthurMerlin](Complexity/Computability/Complexity/Classes/ArthurMerlin.lean)); the [set lower bound protocol and SBP ⊆ AM](Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean), [public-coin GNI in AM](Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean), and [PH = Σ₂ᵖ from coNP ⊆ AM for every encoding](Complexity/Computability/Complexity/Classes/ArthurMerlin/Collapse.lean). | Interactive-machine characterizations, AM[k] = AM and private-to-public-coin transformations remain separate endpoints. | -| Worst-case-hardness derandomization | Done for eventual hardness: [P = BPP from 2^(γn) De Morgan circuit hardness of a language in E](Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean), with the explicit field, the encoding in E and the parameter schedule certified. | The infinitely-often variant; the EXP-not-in-P/poly endpoint of Babai, Fortnow, Nisan and Wigderson. | - -Do not mark these endpoints complete from an abstract algorithm, a class definition, or an -assumed reconstruction theorem: their machine/resource and quantitative conclusions are part of -acceptance. The curated formal abstracts record selected completed statements with their assumptions and scope. - -## Jukna coverage - -Formalize the established theorems, lemmas, constructions and exercise results throughout -[Jukna's *Boolean Function Complexity: Advances and Frontiers* (2012)](https://web.vu.lt/mif/s.jukna/boolean/index.html), -using the author's [errata](https://web.vu.lt/mif/s.jukna/boolean/misprints-BFC.html). -The target is all useful established results and constructions, including supporting lemmas and -worthwhile exercises. Open problems are separate research opportunities, not completion -requirements. Reuse Mathlib and CSLib for the supporting mathematics. - -Complete and review developments individually; book-wide coverage is a long-term program, not -a prerequisite for using the library. Organize modules by mathematical subject rather than book -chapter. - -The [almost-injective binary linear map](Complexity/Probability/BitString/LinearHash/Collisions.lean) -implements Lemma 1.17, including its unordered-pair collision bound and an injective-map -corollary. Its matrix selection is existential; the partial-function circuit upper bounds that -use it remain outstanding. - -This initial map follows the [contents](https://web.vu.lt/mif/s.jukna/boolean/TOC.pdf). -The linked modules are starting points, not evidence of complete chapter coverage. Audit exact -statements and hypotheses against each numbered result, including circuit bases, cost conventions, -uniformity, explicitness and quantitative strength; a citation or related theorem is insufficient. - -| Chapters | Existing entry points | Next coverage work | -| --- | --- | --- | -| 1–2: foundations and Boolean analysis | [Circuit hierarchy](Complexity/Computability/Circuit/Boolean/Hierarchy.lean), [Shannon synthesis](Complexity/Computability/Circuit/Boolean/ShannonSynthesis.lean), [Fourier analysis](Complexity/Foundations/BooleanAnalysis/Fourier.lean) | Audit counting, graph complexity, degree and approximation results. | -| 3–5: communication | [Protocols](Complexity/Computability/Communication/Protocol.lean), [Karchmer–Wigderson](Complexity/Computability/Communication/KarchmerWigderson.lean) | Complete matrix, randomized and multiparty results. | -| 6–10: formulas and circuits | [Spira](Complexity/Computability/Circuit/Boolean/Spira.lean), [Khrapchenko](Complexity/Computability/Circuit/Boolean/Khrapchenko.lean), [Subbotovskaya](Complexity/Computability/Circuit/Boolean/Formula/Subbotovskaya.lean), [Andreev](Complexity/Computability/Circuit/Boolean/Formula/Andreev.lean), [monotone clique](Complexity/Computability/Circuit/Monotone/Clique/LowerBound.lean) | Audit remaining formula and monotone bounds; develop span programs and negation complexity. | -| 11–13: depth restrictions and general gates | [Håstad](Complexity/Computability/Circuit/Boolean/Hastad.lean), [Smolensky](Complexity/Computability/Circuit/Boolean/Smolensky.lean), [symmetric gates](Complexity/Computability/Circuit/Boolean/ShallowSymmetric.lean) | Audit depth-three, threshold, entropy, wire and linear-operator bounds. | -| 14–17: trees and branching programs | [Decision-tree certificates](Complexity/Computability/DecisionTree/Certificate.lean), [Barrington](Complexity/Computability/Circuit/Boolean/BarringtonClass.lean) | Complete bounded-read and bounded-time lower bounds and remaining tree results. | -| 18–19: proof complexity | [Resolution size–width](Complexity/Logics/Propositional/Resolution/SizeWidth.lean), [tree-like resolution](Complexity/Logics/Propositional/Resolution/TreeLike.lean), [Tseitin](Complexity/Logics/Propositional/Resolution/TseitinExpander.lean), [pigeonhole](Complexity/Logics/Propositional/Resolution/Pigeonhole.lean), [Cook–Reckhow systems](Complexity/Computability/Complexity/ProofSystem.lean) | Develop proof-space and cutting-plane lower bounds. | -| 20: barriers and further methods | [Fusion API](Complexity/Computability/Circuit/Fusion/Basic.lean), [Nisan–Wigderson core](Complexity/Computability/Kolmogorov/NisanWigderson.lean) | Match the book's generator, natural-proof, fusion and indirect lower-bound results. | -| Appendix A: mathematical prerequisites | Mathlib and `Complexity/Foundations/` | Reuse existing statements and fill dependencies as clients require them. | - -## Approximation and Fusion milestones - -These milestones extend the existing [semifilter covers](Complexity/Computability/Circuit/Fusion/Semifilter.lean) -and [cyclic characterization](Complexity/Computability/Circuit/Fusion/Cyclic/Compiler.lean) -using [Oliveira's approximation-method notes (2018)](https://www.dcs.warwick.ac.uk/~igorcarb/documents/papers/approximation-method-fusion-note.pdf) -and [Cavalar–Oliveira, ECCC TR25-033 (2025)](https://eccc.weizmann.ac.il/report/2025/033/). -Credit the earlier results of Razborov, Karchmer, Wigderson, and Nakayama–Maruoka where used. -The issues carry ownership and review history. Circuit bounds use the native basis with free -constants and binary unions; the source docstrings record the precise scope of each result. - -| Milestone | Proved result and scope | -| --- | --- | -| [Quadratic completeness #12](https://github.com/cslib-community/complexitylib/issues/12) | **Proved:** [quadratic compiler](Complexity/Computability/Circuit/Fusion/Quadratic.lean) uses exactly `t²` AND gates for a `t`-pair cover and gives the minimum source-cost bound, including arbitrary carriers, empty input families and trivial targets (TR25-033, Theorem 24; PR #19). | -| [Approximation bridge and counting barrier #13](https://github.com/cslib-community/complexitylib/issues/13) | **Proved:** [exact consistency and local observation errors](Complexity/Computability/Circuit/Fusion/Consistency.lean), the [fixed pair sampler, weighted averaging and `8n + 8` certificate barrier](Complexity/Computability/Circuit/Fusion/Sampling.lean) (Oliveira, Lemma 3 and Theorem 6; PRs #20 and #22). This is a local observation bridge, not a formal equivalence of all approximation models. | -| [Graph transfer and inequality #14](https://github.com/cslib-community/complexitylib/issues/14) | **Proved:** [row/column-to-literal transfer](Complexity/Computability/Circuit/Fusion/Graph.lean) for any admissible witness subclass, including semi-ultrafilters, and [exact canonical/full cover and intersection cost `n`](Complexity/Computability/Circuit/Fusion/Graph/Inequality.lean) for inequality on `2^n` vertices per side (TR25-033, Lemmas 39/48 and Proposition 40; PR #21). | -| [Random graph covers #15](https://github.com/cslib-community/complexitylib/issues/15) | **Proved:** [finite inclusion-pattern counting](Complexity/Computability/Circuit/Fusion/Encoding.lean) and [random graph hardness](Complexity/Computability/Circuit/Fusion/Graph/Random.lean): for `N ≥ 16`, probability at least `1 - 2⁻ᴺ` of `⌊N/16⌋ < ρ(G) ≤ N` under the uniform distribution on all labelled bipartite graphs (TR25-033, Theorem 37; PR #23). | -| [Conondeterministic complexity #16](https://github.com/cslib-community/complexitylib/issues/16) | **Proved:** [universal-verifier cover extraction](Complexity/Computability/Circuit/Fusion/Conondeterministic.lean) and the [converse compiler](Complexity/Computability/Circuit/Fusion/Converse.lean) give `ρ_ultra(f) ≤ C_forall,AND(f) ≤ 5ρ_ultra(f)`. The [extended-natural circuit measure](Complexity/Computability/Circuit/Boolean/Conondeterministic.lean) minimizes over all finite auxiliary counts and verifiers; a `t`-pair cover gives exactly `3t` auxiliary bits and `5t` AND gates, including zero and constant cases (TR25-033, Theorem 45, credited there to Karchmer; PRs #25 and #28). The explicit factor five comes from the formalized certificate construction. The graph transfer above specializes to semi-ultrafilters (Lemma 48). | -| [De Morgan circuit size #334](https://github.com/cslib-community/complexitylib/issues/334) | **Proved:** [De Morgan transfer](Complexity/Computability/Circuit/Fusion/DeMorgan.lean) of unrestricted cover complexity `ρ(f)` from literals: `ρ(f) ≤ C_AND(f) ≤ ρ(f)²` for monotone AND complexity from literals, and `ρ(f) ≤ 2C(f)`, `C(f) ≤ 4(ρ(f)+1)²(2n+ρ(f)+1) + n` for De Morgan circuit size `C(f)`, negations anywhere and every gate charged. The lower bound uses the existing [dual-rail translation](Complexity/Computability/Circuit/Monotone/DualRail.lean) and holds for any admissible witness class; the upper bound adds a [total-size bound](Complexity/Computability/Circuit/Fusion/Quadratic.lean) `4(t+1)²(n+t+1)` for the quadratic compiler. The formalized upper bound is cubic in the cover size when it exceeds `n`, not quadratic, because unions are charged; this is a property of the construction. | - -Keep the source models explicit: constants, zero-gate constructions, exact versus one-sided -literal consistency, and AND versus total gate costs. The counting barrier requires a capacity -bound over every pair; it does not apply to a bound restricted to a particular circuit's gate -pairs and is not an upper bound on unrestricted cover complexity. The sampling and reconstruction -lemmas are proved, not assumed. These are -formalizations of established results, not claims of new explicit superlinear circuit lower bounds. - -## Stateful algorithms and data structures prototype - -The [stateful interface calculus](Complexity/Foundations/Semantics/Stateful/Basic.lean) separates -mathematical operations, [semantic modules](Complexity/Foundations/Semantics/Stateful/Composition.lean), -[native realizations](Complexity/Foundations/Semantics/Stateful/Realization.lean), and -[resource certificates](Complexity/Foundations/Semantics/Stateful/Resource.lean). Adaptive client proofs, -semantic Hoare rules, module substitution and hidden-state potentials compose without choosing -a backend. The [two-stack queue](Complexity/Algorithms/Lean/Queue.lean) and -[reset-and-replay timeline editing](Complexity/Algorithms/Lean/Retroactive.lean) are -checked constructions, with explicit primitive-cost assumptions; their pure client controllers -do not yet have total Word-RAM time certificates. - -The shared [ordered-set interface](Complexity/Foundations/Semantics/Stateful/OrderedSet.lean) -and [optional-minimum contract](Complexity/Foundations/Data/OrderedSet.lean) are independent of -representations and costs. The interface admits arbitrary linearly ordered keys and is total; -a bounded-key implementation may restrict insertion admissibility separately. The -[unbalanced binary search tree](Complexity/Algorithms/Lean/SearchTree/Basic.lean) implements -membership, insertion, minimum and strict successor over any linear order, preserving a strict -BST invariant and finite-set semantics. Duplicate insertion preserves the tree; missing successors -and empty queries return `none`. Its [native realization](Complexity/Algorithms/Lean/SearchTree/Stateful.lean) -transfers correctness and additive node-visit bounds to adaptive clients. Each operation visits -at most the initial height, bounded by set cardinality; this is not a logarithmic or RAM-time -claim. [Checked examples](ComplexityTests/SearchTree.lean) contrast height-three and height-seven -representations of the same seven keys and execute an answer-dependent two-minimum query. -[Deletion](Complexity/Algorithms/Lean/SearchTree/Erase.lean) replaces a matching node by its left -subtree when the right one is empty and otherwise splices in the successor from the right subtree, -with finite-set semantics, invariant preservation, unchanged trees for absent keys, -and node visits and resulting height bounded by the initial height -([examples](ComplexityTests/SearchTreeErase.lean)). Adding deletion to the shared stateful -ordered-set interface, balancing, and concrete heap/RAM representations remain open. - -[Static fusion trees #443](https://github.com/cslib-community/complexitylib/issues/443) -have a [finite-set endpoint](Complexity/Algorithms/WordRAM/FusionTree/Static.lean) proving -worst-case inclusive predecessor in `O(1 + log_w n)` actual standard-basis RAM instructions -and `O(n)` words for nonempty sets (`O(n + 1)` including empty sets). -The [query program](Complexity/Algorithms/WordRAM/FusionTree/Query.lean) charges initialization, -node search, checked multiword arithmetic, pointer traversal, and halt. Explicit bounds are -`3100000 * (Nat.log w n + 1)` instructions and `126n + 1042` data/register words, uniformly -for `w ≥ 2`. Presence and value occupy separate registers, so key zero remains distinct from -absence. The entire allocation frontier must fit an address word separately from the keys. -The bounded-size code family contains width-dependent constants; static preprocessing uses -classical witnesses and has no RAM running-time certificate. Uniform preprocessing and dynamic -updates remain open. The checked-overflow -[multiword multiplication dependency #444](https://github.com/cslib-community/complexitylib/issues/444) -provides reusable arithmetic. Shared workspace initialization now accompanies the canonical -`WordRAM/Multiword/Digits` module, letting Transfer, Bitwise and Shift import digit infrastructure -without depending on multiplication. -The shared child-height lemmas in `Algorithms/Lean/FusionTree/Tree` support both -`Model.decode_rep` and `QueryProgram.exec_loop_height` without duplicate proofs. - -[Client resource contracts](Complexity/Foundations/Semantics/Stateful/CostHoare.lean) combine -admissibility, postconditions and initial-state-dependent operation budgets. Their sequencing -rules retain answer-dependent costs; separate method budgets transport contracts through -successive semantic modules and then to additive native execution measures. The `stateful` -tactic uses local contracts and structural rules, with intermediate assertions and implementation -choices supplied explicitly. A two-layer adaptive counter example checks both execution branches -and rejects an insufficient budget. - -[RAM controller certificates](Complexity/Computability/WordRAM/Controller.lean) now connect a -fixed machine fragment to an admissible client, charging its control flow and register preparation. -Sequencing uses one fixed continuation fragment for all represented answers; pure semantic results -require actual execution evidence. Named certificates are reused by `stateful`, while `polytime` -can retrieve the distinct uniform RAM function-time predicate. The -[adaptive stack controller](Complexity/Algorithms/WordRAM/Stack/Controller.lean) starts from the -standard singleton input, installs an empty stack at address two, pushes and pops the input, and -uses the observed answer to replace zero through another pair of stack calls. It returns -`max n 1` in exactly 49 instructions for zero and 29 otherwise, including setup, argument writes, -control flow and halt. All inputs fit its logarithmic numerical-magnitude width threshold. -This does not certify arbitrary Lean continuations or a conversion to Turing-machine time. - -The [fixed-program bridge](Complexity/Computability/WordRAM/Dynamic.lean) has concrete bounded -[stack](Complexity/Algorithms/WordRAM/Stack.lean) and -[prefix-sum](Complexity/Algorithms/WordRAM/PrefixSums/Dynamic.lean) clients. These certify persistent -operation execution, word-fit conditions, instruction costs including halt, and arbitrary -admissible adaptive histories. Finite-footprint assertions and faithful probe transcripts supply -frame rules. Prefix sums use a balanced aggregation tree for a power-of-two number of entries, -not a Fenwick layout. Machine costs exclude initial representation construction and external argument -encoding/delivery and result decoding; the stated storage bounds concern reserved representation regions. - -The [shared-memory RAM queue](Complexity/Algorithms/WordRAM/Queue/Dynamic.lean) now realizes -FIFO enqueue and dequeue with one fixed eleven-register dispatcher. Two reserved arrays hold -at most `capacity` live values in `2 * capacity` reserved word cells. An empty-front dequeue -executes a real rear-to-front transfer loop. Eight credits per rear element give at most -fourteen amortized instructions per queue call, including halt, with initial and final credit -retained. Six actual register instructions initialize the empty representation without clearing -memory. The worked adaptive client reinserts an observed dequeued value and checks FIFO order, -zero-valued observations, full/zero capacity and instruction-budget rejection. This direct -implementation shares the FIFO specification with the abstract two-stack construction above; -it is not a compilation of that construction's free-monad methods. Arbitrary external client -computation and argument delivery remain outside the per-operation bound. - -The [recursive van Emde Boas set](Complexity/Algorithms/Lean/VanEmdeBoas/Basic.lean) -supports bounded insertion, membership and strict successor for the universe -`U(d) = 2^(2^d)`. Its minimum-excluded cluster representation has checked -[invariant preservation and exact insertion semantics](Complexity/Algorithms/Lean/VanEmdeBoas/Insert.lean), -[least-successor and absence theorems](Complexity/Algorithms/Lean/VanEmdeBoas/Successor.lean), -and a [finite-set abstraction](Complexity/Algorithms/Lean/VanEmdeBoas/Elements.lean). -The [contiguous layout arithmetic](Complexity/Algorithms/Lean/VanEmdeBoas/Layout.lean) -has nonoverlapping recursive records and an explicit bound of ten words per universe element. -The [recursive memory refinement](Complexity/Algorithms/WordRAM/VanEmdeBoas/Model.lean) -interprets actual memory, including stale empty extrema and arbitrary surrounding memory. -[Fixed-program native calls](Complexity/Algorithms/WordRAM/VanEmdeBoas/Call.lean) -certify insertion (`39*(d+1)+16`), membership (`28*(d+1)+18`), and strict successor -(`65*(d+1)+22`, using a `4*d`-word scratch stack) on one 213-instruction 32-register dispatcher -independent of depth and word width, charging setup, dispatch, loop control, and halt, with -exact GenericRAM transfers and logarithmic `log₂(log₂ U)` bounds -([Insert](Complexity/Algorithms/WordRAM/VanEmdeBoas/Insert.lean), -[Member](Complexity/Algorithms/WordRAM/VanEmdeBoas/Member.lean), -[Successor](Complexity/Algorithms/WordRAM/VanEmdeBoas/Successor.lean)). -A separate [uniform 32-register initializer](Complexity/Algorithms/WordRAM/VanEmdeBoas/Init.lean) -constructs the empty represented tree and scratch stack pointer from arbitrary bounded memory -in at most `8 * span d + 20 * d + 25 ≤ 80 * U + 20 * d` instructions within a total footprint -of `span d + 4 * (d + 1) ≤ 10 * U + 4 * (d + 1)` words. The operations are packaged as a -`DynamicCertificate` for the finite-set `Stateful.Spec` on `[0, U)`, with combined -initialization-and-adaptive-client execution (`run_initialized`) charging at most -`65*(d+1)+22` instructions per operation while preserving all memory outside -`[base, base + span d + 4 * (d + 1))`. External client computation and argument register writes -between calls are not charged to individual operations; deletion and predecessor remain future -work. The recursive minimum-excluded variant is credited to Demaine's exposition, separately -from the original van Emde Boas--Kaas--Zijlstra stratified representation. - -The [doubling array](Complexity/Algorithms/WordRAM/DynamicArray.lean) implements dynamic append -and indexed read with one fixed twelve-register dispatcher using the bump allocator and array-copy -loop. Fifteen instructions initialize the empty array by allocating and zeroing a one-word block at -address zero. Appending writes in place in seven instructions when spare capacity remains and -doubles capacity in `15 * cap + 19` instructions when full. Potential `15 * (2 * |vs| - cap)` -bounds every append by `49` amortized instructions before dispatch (`52` including dispatch and -halt) and every indexed read by `6` instructions including dispatch and halt, retaining initial -and final credit across arbitrary admissible adaptive clients. Old blocks remain allocated, so the -space bound `frontier < 4 * |vs|` for nonempty arrays limits total words ever allocated rather than -reclaimed live storage; deallocation, shrinking, and compiled client controllers remain open. - -Outstanding: controllers for larger adaptive and iterative clients; -reusable allocation and deallocation, shrinking and live/peak space accounting, -richer ownership and recursive procedures; independent model -realizations for cell probes, caches and randomness; and present/historical queries for the -retroactive interface. Upstream API coordination and coordinator review remain prerequisites -for integration. - -## Machine-class milestones - -Polynomial efficiency is sufficient for many reductions, but does not establish tight time or -space bounds. Further class-level work needs resource certificates for the actual algorithms: - -* Binary-counted space loops: the [native `Nat.fold` certificate](Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Fold.lean) - ports lean-canny's indexed fold and adds a prefix-invariant rule. The child and seed may use - arbitrary polynomial space; every accumulator prefix must have polynomially bounded encoded - length. Extracting lean-canny's recursive evaluator, implicit arithmetic and ETR algorithm - remains separate work; this fold establishes none of their algebraic or class-level results. -* Mathlib TM2 compatibility: the [polynomial-time bridge](Complexity/Computability/Machines/Turing/TM2/PolyTime.lean) - transfers typed computations with finite working alphabets to the tidy multi-tape calculus - under standard binary word encodings. The [polynomial-space bridge](Complexity/Computability/Machines/Turing/TM2/PolySpace.lean) - transfers terminating computations with polynomially bounded stacks without a runtime bound. - The [reverse compiler](Complexity/Computability/Machines/Turing/TM2/Reverse/Bounds.lean) - constructs finite-alphabet stack machines with time - `n + (k + 1) * (t + 1) + o + 3` and total reachable stack length at most `n + s + o`, including - initialization and canonical cleanup. The [transfer API](Complexity/Computability/Machines/Turing/TM2/Reverse/Transfer.lean) - proves polynomial-time computation and PSPACE decision equivalence under the original binary - encodings, without polynomial runtime assumptions for space. Input storage adds linear space; - sublinear work-space comparisons and a linear-space forward simulation remain open; -* Tree Evaluation: the [Cook–Mertz machine](Complexity/Computability/TreeEval/Space.lean) - has a proved parameterized space bound on valid encoded instances and an - `O(log n · log log n)` input-size space corollary on nontrivial instances (`1 ≤ ℓ` and - `1 ≤ H`); malformed-input handling and the refined `O(ℓ + H log(ℓ + 2))` parameter bound - remain outstanding. Toward Williams's `TIME[t] ⊆ SPACE[√(t log t)]` (#361), the - [fan-in-`d` procedure](Complexity/Computability/TreeEval/Ary/CookMertz.lean) is proved correct - over `d + 1` registers when `d · ℓ < |K| - 1` (milestone M1); at `d = 2` it is the binary - procedure step for step, whose correctness is derived from it - ([`Ary.proc_ofBinary`](Complexity/Computability/TreeEval/CookMertz.lean)). Implicit Tree - Evaluation (#367) starts from - [query machines in the space of their states](Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean), - which charge neither the input nor the output; the fan-in-`d` space bound, subroutine calls for - implicit gates and leaves, padding of non-perfect trees, and the remaining milestones are open; -* the space hierarchy below linear space: the - [space hierarchy](Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean) and - `L ⊊ PSPACE` are proved for space-constructible bounds `g` with `n ≤ g n`, and the textbook - form for `log n ≤ g n` needs a universal simulation that does not hold its input; the - [time hierarchy](Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean) and `P ⊊ EXP` - are proved with a polynomial simulation gap, so a tight tape-indexed hierarchy needs a - linear-overhead simulation and an `f log f` time hierarchy the corresponding simulation bound; -* Reingold's theorem: [USTCON ∈ L and SL = L](Complexity/Computability/Complexity/Classes/LogSpace/USTCON.lean) - are proved for the adjacency-matrix encoding (with `SL` defined by logspace many-one reducibility - to `USTCON`, completeness of `USTCON` for `SL` and `L`, and the unary-header injectivity lemma - shared with `TreeEval` in [List/Append.lean](Complexity/Foundations/Data/List/Append.lean)); a - symmetric-Turing-machine model of `SL` and an edge-list variant of `USTCON` by a logspace - reduction remain; -* Native [NL = coNL](Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean) is - proved by streaming inductive counting, including complement deciders for recognizers with - looping branches, and has a - [formal abstract](abstracts/ComplexityAbstracts/ImmermanSzelepcsenyiAbstract.lean). Directed `s`–`t` connectivity on adjacency matrices is - [NL-complete](Complexity/Computability/Complexity/Problems/STCON/Completeness.lean) under - logspace reductions, and so is its complement; so is - [2SAT](Complexity/Computability/Complexity/Problems/TwoSAT/Completeness.lean), through the - implication-graph criterion of Aspvall, Plass and Tarjan. Nondeterministic space is - [closed under complement](Complexity/Computability/Complexity/Classes/Space/Nondeterministic.lean) - for every bound `s` with `log₂ n ≤ s n` (#885). - `PH ⊆ PSPACE` is also proved by evaluating quantified predicates in - [polynomial space](Complexity/Computability/Complexity/Classes/Inclusions.lean); -* alternating time/space classes and bounded-alternation characterizations of `PH`, beyond the - proved [AP = PSPACE](Complexity/Computability/Complexity/Classes/Alternation/Savitch.lean); -* the ordered logarithmic-space FO encoding bridge and first-order Circuit Value completeness in the - [first continuing priority](#continuing-priorities), together with uniform circuit-family and - counting-machine characterizations; -* RAM value domains: the [generic core](Complexity/Computability/GenericRAM/Defs.lean) now permits - arbitrary value, address, configuration and constant-symbol types, partial operations/tests, - and model-specific fault policies. The [WordRAM adapter](Complexity/Computability/WordRAM/Generic.lean) - preserves every step, fault, output and instruction count for every basis and arbitrary state. - Instances cover the [signed bounded integer model](Complexity/Computability/GenericRAM/Signed.lean) - of lean-trominoes and [exact reals and prime fields](Complexity/Computability/GenericRAM/Algebraic.lean) - with separate tagged natural address words. Real semantics is noncomputable; prime fields are - executable. The algebraic variant has checked word arithmetic and rational constants with - nonzero field denominators; no field-to-word conversion is provided. The - [native scalar interface](Complexity/Computability/GenericRAM/Native.lean) separately certifies - checked literals/operations, tests, address extraction and move/control validation with arbitrary - native TM time/space bounds; it is equivalent to native computability when bounds are unrestricted. - Polynomial bounds yield native polynomial time. A - [bounded-natural addition model](Complexity/Computability/GenericRAM/Native/Nat.lean) supplies every - scalar certificate, and [WordRAM native primitives](Complexity/Computability/WordRAM/Native.lean) - supply complete polynomial-time `NativePrimitives` bundles for `Basis.standard`, `Basis.additive`, - `Basis.arithmetic`, and `Basis.exact` (plus restricted sub-bases and homomorphic preimages) across - all unary-encoded widths with binary operands (#489). The native tidy calculus has - [fixed finite tuple rules](Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Pi.lean) - with linear access/gather/update and arbitrary summed construction bounds, - [retained-input option elimination](Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Option.lean) - charging extraction, repeated option computation, input retention, and the selected handler - (#301), [sum injections and projections](Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Sum.lean), - and [native certificate combinators](Complexity/Computability/GenericRAM/Native/Combinators.lean). - The [finite-state step representation](Complexity/Computability/GenericRAM/Simulation/Finite.lean), - [certified native step simulator](Complexity/Computability/GenericRAM/Simulation/Turing.lean), - and [clocked multi-step simulator and whole-run transport](Complexity/Computability/GenericRAM/Simulation/Run.lean) - implement single steps and clocked multi-step runs of any fixed generic-RAM program over sparse - memory and arbitrary `NativePrimitives`, preserving all successor states, halts and faults - (`denote_step`, `denote_run`, `executes_iff_exists_run`), bounding sparse-memory growth by at most - one stored address per step (`length_entries_run_le`), retaining parameterized primitive and - sparse-memory time/space bounds along the run (`le_runTime_of_run_eq_inl`, - `le_runSpace_of_run_eq_inl`), and transporting halting `Executes` certificates to native - multitape Turing machines with both explicit `ComputableTidilyInO` bounds and automatic - `ComputableTidilyInPolyTime` corollaries, including `WordRAM` specializations (#298, #292). - Uniform arbitrary-program dispatch, general width-selection/input-fit theorems, and simulating - individual operations by programs over smaller bases remain open (#293). - Generalizing the structured program calculus and time-class APIs to arbitrary domains, - weighted/bit costs, and simulations between these instances also remain open. No - real-RAM/Turing-machine equivalence is claimed. The redesigned typed core is proposed in - [CSLib #1158](https://github.com/leanprover/cslib/pull/1158); its scope and remaining compatibility - bridges are recorded in [UPSTREAM.md](UPSTREAM.md#coordination-before-submission); -* Sparse RAM memory: [association-list semantics](Complexity/Computability/GenericRAM/SparseMemory/Basic.lean) - and [native multitape TM certificates](Complexity/Computability/GenericRAM/SparseMemory/Turing.lean) - implement default-valued reads and insert/replace writes using Mathlib's `AList` and the existing - encoded equality/search/filter calculus. Parameterized time/space bounds depend on stored-cell - count and encoded address/value lengths; cubic-time and linear-space corollaries use full binary - input length. Overwrites preserve cardinality, and writes retain distinct addresses. The read - default is supplied as input to one uniform machine. Combined with the certified single-step and - clocked whole-run simulators above (#298, #292), this supports transporting fixed-program RAM - executions to native multitape Turing machines; uniform arbitrary-program dispatch and general - width-selection/input-fit reductions remain open (#293). No bridge - for arbitrary exact real arithmetic is claimed; -* RAM models: the [bounded-word RAM](Complexity/Computability/WordRAM/Defs.lean), adapted from the - Lean formalization accompanying the tromino undecidability paper, is parameterized by a - [basis of word operations](Complexity/Computability/WordRAM/Basis.lean) built on circuit - signatures, with the standard, arithmetic (the source's operations on unsigned words) and - additive bases; programs and decision procedures - [transfer along meaning-preserving maps of bases](Complexity/Computability/WordRAM/MapOp.lean) - with identical runs, and `Program .additive r` compiles directly to `Cslib.RAM` via - `ToRAM.compileAdditive` and `Basis.additiveHomStandard` (#315). Simulating an operation by a - program over a smaller basis with an instruction budget (the analogue of circuit - `SimulatesWithCost`) and an AC⁰ basis remain open. The machine has [linear and polynomial - instruction bounds](Complexity/Computability/WordRAM/Time.lean) with width-dependent time and - encodings, arbitrary predicates on input/width pairs, and width-indexed code of uniformly bounded - length. Explicit `Uniform` variants retain one fixed program, which may read the word size; - `LogWord` wrappers express the transdichotomous lower-bound assumption. Alongside these, - asymptotic time with constants shared across widths and Mathlib width-schedule bridges are - available. The machine also has - [structured programs](Complexity/Computability/WordRAM/Structured.lean) compiling with exact - instruction counts, [allocation and arrays](Complexity/Computability/WordRAM/Allocation.lean) and - a [linear-time element-distinctness client](Complexity/Algorithms/WordRAM/ElementDistinctness.lean) - over `.additive` whose promised inputs provably fit at that threshold. The generic classes alone do not supply - this input-fit guarantee. The [additive-memory compiler](Complexity/Computability/WordRAM/RAM.lean) - now forward-simulates successful fitting runs in the existing - [`Cslib.RAM`](Complexity/Computability/RAM/Defs.lean) with logarithmic cost - `8 * (bitLength (r + 5) + 1) * (t + 1) * (w + 1)`, including its two register initializers - and final output copy/jump, from an explicitly supplied padded input. A separate - [input preparer](Complexity/Computability/RAM/Input.lean) now charges the backward relocation and - prefix clearing from five zero scratch cells followed by a length header and the input words. - It reaches the exact padded register state before arbitrary appended code in logarithmic cost - `(24 + R) * (bitLength (R + 5) + 2) * (input.length + 1) * b` for `R ≥ 5`, given bit-length - bound `b` on the header and words; external input installation remains uncharged. The - [composed bridge](Complexity/Computability/WordRAM/RAMInput.lean) now includes that preparation - in `C_r * (t + input.length + 1) * (w + 1)`, for an explicit constant depending only on the - source register count. The same fixed compiler gives a - [bounded-universe element-distinctness decider](Complexity/Algorithms/WordRAM/ElementDistinctnessRAM.lean) - of logarithmic RAM cost `2735 * (n + 1) * (Nat.log 2 (n + 1) + 1)`, including preparation; - the separately supplied padded-input bound is `2448 * (n + 1) * (Nat.log 2 (n + 1) + 1)`. - These statements retain the explicit preloaded length-bearing convention and entry promise. - Wider-fragment and Turing-machine simulations remain open. The unrestricted converse - from prescribed-width to uniform decision is false: width can supply instance-dependent advice. - A useful conversion must specify an input-fit guarantee, a size-based width-selection procedure - with computability and resource bounds, encoding conventions, and simulation overhead. Transfer - of cell-probe lower bounds and the source's Horn-SAT, 2SAT, matching and domino-tiling clients - also remain open; -* Single-tape, Post–Turing (`TM0`/`TM1`), and `Partrec` integration (#318): [tape equivalences](Complexity/Foundations/Data/BiTape.lean) (`StackTape.equivListBlank`, `BiTape.equivTape`), [translations](Complexity/Computability/Machines/Turing/SingleTape/PostTuringMachine.lean) between `SingleTapeTM` and Mathlib's `Turing.TM0` and `Turing.TM1` (step-for-step for `toTM1` and up to one final halting step for `ofTM0`; `toTM0` and `ofTM1` preserve evaluation only), [1-work-tape multi-tape simulation](Complexity/Computability/Machines/Turing/MultiTape/SingleTape.lean) (`MultiTapeTM.ofSingleTapeTM` in time `3 * |x| + 2 * t + 6` and space `3 * |x| + 2 * t + 7`, lifting `SingleTapeTM.TimeComputable` and `PolyTimeComputable`), [`Primrec`/`Partrec`/`Computable` bridges](Complexity/Computability/Machines/Turing/MultiTape/Halting/Partrec.lean) for [single-tape](Complexity/Computability/Machines/Turing/SingleTape/Partrec.lean) and multi-tape machines (`IsComputable.computable`, `IsDecidable.computablePred`, `MappingReducible.manyOneReducible`), and [machine-backed Kolmogorov complexity](Complexity/Computability/Kolmogorov/SingleTape.lean) (`ofSingleTapeTM`, `ofTM0`, `ofTM1`, [multi-tape `IsPartrec` optimality](Complexity/Computability/Kolmogorov/MultiTape.lean)) are proved; reverse multi-tape-to-single-tape simulation and machine-backed Nisan–Wigderson decoding results remain open; -* concrete list-decodable codes for Nisan–Wigderson and order-invariant descriptive-complexity - queries. - -Check upstream work before starting these developments. The existing combinatorial or -machine-relative cores do not by themselves establish the missing uniform resource guarantees. - -## Candidate proof improvements - -These are experiments to validate, not claimed savings: - -* Factor indicator-expectation identities from PCP's second-moment calculation and recurring - cardinality/logarithm conversions only when a second client benefits. - -Judge changes on client readability, total proof burden and elaboration cost. Count proof fields -and helper APIs, and distinguish source-line counts from runtime or proof-term size. -[scripts/proof_lengths.py](scripts/proof_lengths.py) supports comparison against a Git revision. - -Past measurements, reviews and proposals remain in the -[historical roadmap](https://github.com/cslib-community/complexitylib/blob/c88395234575284c2fe1e9e3619ead1c2f6fd7f3/ROADMAP.md). +| 1–2: foundations and Boolean analysis | Counting, graph complexity, degree and approximation results; the partial-function circuit upper bounds that use Lemma 1.17. | +| 3–5: communication | Matrix, randomized and multiparty results. | +| 6–10: formulas and circuits | Remaining formula and monotone bounds; span programs and negation complexity. | +| 11–13: depth restrictions and general gates | Depth-three, threshold, entropy, wire and linear-operator bounds. | +| 14–17: trees and branching programs | Bounded-read and bounded-time lower bounds and the remaining tree results. | +| 18–19: proof complexity | Proof-space and cutting-plane lower bounds. | +| 20: barriers and further methods | The book's generator, natural-proof, fusion and indirect lower-bound results. | + +## Pseudorandomness, coding and Boolean analysis + +- **Derandomization from hardness:** the infinitely-often variant, and the EXP ⊄ P/poly endpoint + of Babai, Fortnow, Nisan and Wigderson. +- **Extractors** ([#895]) up to explicit two-source extractors; condensers, limited independence, + explicit expanders and space-bounded generators, with finite guarantees separate from uniform + construction and decoding costs. +- **Codes:** Guruswami–Sudan list decoding and local decoding, keeping interpolation, + list-size/agreement guarantees and decoding runtime as separate obligations; concrete + list-decodable codes for Nisan–Wigderson. +- **Boolean analysis:** hypercontractivity beyond `p ≤ 2 ≤ q` and its applications. + +## Communication, queries, learning and other models + +- **Lifting** ([#890]): Raz–McKenzie and Göös–Pitassi–Watson query-to-communication lifting. +- Multiparty protocols, discrepancy and information complexity, direct-sum and direct-product + results, and reductions to streaming, sketching and cell-probe lower bounds. +- **Learning:** machine-certified running times for the LMN and Kushilevitz–Mansour learners; + distributional problems and reductions, samplability, average-to-worst-case connections, + PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. +- **Property and distribution testing:** access models, one/two-sided and tolerant testing, + query and sample bounds, canonical testers and lower bounds. +- **Kolmogorov complexity and metacomplexity** ([#798], [#884]): prefix-free complexity, + resource-bounded MCSP variants and connections to learning, cryptography and lower bounds; the + circuitized anti-checker with an efficient generator, hardness magnification and MINKT/MINCKT + as independently scoped developments; the reverse multi-tape-to-single-tape simulation and + machine-backed Nisan–Wigderson decoding. +- **Quantum computation** ([#896]): BQP ⊆ PP and the BBBV and Grover bounds; reusable + circuit, channel and measurement semantics, reusing suitable quantum foundations rather than + incompatible models; BQP, QMA and related query, communication and interactive classes. + +## Machines, RAM and data structures + +- **Plain computability** ([#862]): delete the tidy calculus, keeping only a machine-level + kernel inside the Machines layer, and switch the abstract bridges to the shared predicate. +- **Certificate APIs and automation.** Infer encodings for ordinary functional expressions + through constructor, projection, lookup and composition rules; generalize list, bounded-table, + cache and nested-loop invariants where clients need them; keep separate time, workspace and + output-size bounds through composition; apply cumulative streaming contracts to captured + iteration and nested loops; certify PRG stretching with seed length, rounds and generator cost + kept separate; and develop general open-program composition. Use Cook–Levin and GGM as + regression clients. Improve configuration views, tape partitions and handoff identities only + where several clients benefit, keeping machine transitions out of global simp. +- **Mathlib TM2:** sublinear work-space comparisons and a linear-space forward simulation. +- **Generic RAM:** uniform arbitrary-program dispatch and general width-selection and input-fit + theorems; simulating operations by programs over smaller bases; structured programs and time + classes over arbitrary value domains with weighted or bit costs; simulations between instances; + the typed core proposed in [CSLib #1158](https://github.com/leanprover/cslib/pull/1158). +- **Word RAM:** an AC⁰ basis; wider-fragment and Turing-machine simulations; size-based width + selection with an input-fit guarantee and explicit overhead; transfer of cell-probe lower + bounds; and the Horn-SAT, 2SAT, matching and domino-tiling clients. +- **Stateful algorithms and data structures:** Word-RAM controllers for larger adaptive and + iterative clients, including the two-stack queue and timeline-editing controllers; reusable + allocation and deallocation, shrinking, and live and peak space accounting; ownership and + recursive procedures; model realizations for cell probes, caches and randomness; present and + historical queries for the retroactive interface; deletion in the shared ordered-set interface, + balancing, and heap or RAM representations of search trees; uniform preprocessing and dynamic + updates for fusion trees; deletion and predecessor for van Emde Boas sets; and deallocation, + shrinking and compiled client controllers for the doubling array. +- **A typed-call evaluator** for fixed-program Word-RAM clients, returning the typed observation, + final state and halt-inclusive instruction cost, so the prefix-sum and stack clients no longer + assemble preparation, evaluation and halt accounting by hand. + +## Coverage and reuse + +The long-term bar is to support formalizing every paper in the +[Electronic Colloquium on Computational Complexity](https://eccc.weizmann.ac.il/colloquium/call_for_papers/), +with the additional work per paper increasingly its new mathematics: standard models, +representation changes, reductions, resource certificates and proof techniques come from the +library. Use a growing, source-pinned sample of papers, including some chosen after an API was +designed, as demanding clients, and promote recurring obligations into shared APIs only after +reuse is demonstrated. + +- **One sensitivity API.** Define the sensitivity measures over any `Fintype` in CSLib and drop + the separate measures of the sensitivity-separation development. +- **CNF evaluation automation:** `fun_prop` certificates for evaluating literals, clauses and + formulas under a polynomial-time assignment, and `Literal.eval` simp lemmas, so clients stop + unfolding `CNF.eval`. +- Factor indicator-expectation identities from PCP's second-moment calculation, and recurring + cardinality and logarithm conversions, once a second client benefits. + +## Documentation and repository + +- **The guide** ([#585]): a chapter per area, including Foundations (bit strings, Fourier + analysis, PMF and `ProbComp`, codes), proof complexity, descriptive complexity, and Word RAM + and algorithms, reusing checked examples. +- **Curated formal abstracts:** improve readability, and compare each changed abstract with its + final source statements. +- **Archive `complexitylib-v1`** once its remaining work is dispositioned. + +## Deferred scopes + +These remain coverage targets but are deferred from the active queue; their issues were closed as +not planned, not as proved. + +- The full VNP-completeness reduction for the permanent ([#321]). +- General auxiliary-input zero knowledge ([#324]); see the GMW theorem above. +- Williams's square-root-space simulation ([#361]) and implicit Tree Evaluation ([#367]), now the + frontier track [#888]. +- Vollmer's generalized-quantifier survey ([#399]): ordered leaf words, explicit uniformity and + input-access models, finite-monoid classification and generalized logical quantifiers. + +[#321]: https://github.com/cslib-community/complexitylib/issues/321 +[#324]: https://github.com/cslib-community/complexitylib/issues/324 +[#361]: https://github.com/cslib-community/complexitylib/issues/361 +[#367]: https://github.com/cslib-community/complexitylib/issues/367 +[#399]: https://github.com/cslib-community/complexitylib/issues/399 +[#456]: https://github.com/cslib-community/complexitylib/issues/456 +[#459]: https://github.com/cslib-community/complexitylib/issues/459 +[#474]: https://github.com/cslib-community/complexitylib/issues/474 +[#486]: https://github.com/cslib-community/complexitylib/issues/486 +[#513]: https://github.com/cslib-community/complexitylib/issues/513 +[#581]: https://github.com/cslib-community/complexitylib/issues/581 +[#585]: https://github.com/cslib-community/complexitylib/issues/585 +[#640]: https://github.com/cslib-community/complexitylib/issues/640 +[#643]: https://github.com/cslib-community/complexitylib/issues/643 +[#645]: https://github.com/cslib-community/complexitylib/issues/645 +[#736]: https://github.com/cslib-community/complexitylib/issues/736 +[#748]: https://github.com/cslib-community/complexitylib/issues/748 +[#798]: https://github.com/cslib-community/complexitylib/issues/798 +[#862]: https://github.com/cslib-community/complexitylib/issues/862 +[#884]: https://github.com/cslib-community/complexitylib/issues/884 +[#885]: https://github.com/cslib-community/complexitylib/issues/885 +[#886]: https://github.com/cslib-community/complexitylib/issues/886 +[#888]: https://github.com/cslib-community/complexitylib/issues/888 +[#889]: https://github.com/cslib-community/complexitylib/issues/889 +[#890]: https://github.com/cslib-community/complexitylib/issues/890 +[#891]: https://github.com/cslib-community/complexitylib/issues/891 +[#892]: https://github.com/cslib-community/complexitylib/issues/892 +[#893]: https://github.com/cslib-community/complexitylib/issues/893 +[#894]: https://github.com/cslib-community/complexitylib/issues/894 +[#895]: https://github.com/cslib-community/complexitylib/issues/895 +[#896]: https://github.com/cslib-community/complexitylib/issues/896 +[#897]: https://github.com/cslib-community/complexitylib/issues/897 +[#939]: https://github.com/cslib-community/complexitylib/issues/939 +[#949]: https://github.com/cslib-community/complexitylib/issues/949 From 0317cf2d20fd724f552c7b86fe97f1effe0bcbc5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 22:59:53 -0400 Subject: [PATCH 2/3] doc(roadmap): address review of the directions draft Drop 2SAT NL-completeness (#915). Link the pre-rewrite file as the archive of past detail, including the FHE industrial context, and keep the eprint links on the scheme names. Narrow the composite-moduli direction, restore a ranked index of the landmark theorems, and restore the GSW limitations as targets, the FO numeric-predicate convention, the quantum line's scope and #608. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ROADMAP.md | 130 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 82 insertions(+), 48 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 304bd97b4e..a2a78c226e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -10,6 +10,9 @@ for the actual algorithms, with explicit models, encodings and assumptions. An a a class definition or an assumed reconstruction theorem does not complete it. Search Mathlib, CSLib and this library before starting, and check upstream work. +The [pre-rewrite roadmap][archive] is the archive of past detail and design records, including +the FHE industrial context, the first-order design decisions and the repository's history. + ## Programs | Program | Issues | @@ -23,54 +26,77 @@ CSLib and this library before starting, and check upstream work. | Boneh–Shoup cryptography tracks; zero-knowledge architecture | [#640], [#643] | | A Verso guide with a chapter per area | [#585] | +### Landmark theorems, in priority order + +Priorities live in this list and in the tiers of [#897]. + +1. [Goldreich–Micali–Wigderson zero knowledge in full](#cryptographic-landmarks) +2. [Rompel's signature theorem](#cryptographic-landmarks) +3. [Gentry's bootstrapping, instantiated](#cryptographic-landmarks) ([#486]) +4. [Completeness of oblivious transfer](#cryptographic-landmarks) +5. [Håstad's optimal MAX-E3SAT hardness](#approximation-and-pcp) ([#886]) +6. [Williams's NEXP ⊄ ACC⁰](#circuits-and-algebraic-complexity) ([#889]) +7. [Valiant's VNP-completeness of the permanent](#circuits-and-algebraic-complexity) +8. [The Kabanets–Impagliazzo theorem](#circuits-and-algebraic-complexity) ([#891]) +9. [MIP = NEXP](#interactive-proofs) ([#892]) +10. [Regev's worst-case to average-case reduction](#cryptographic-landmarks) + ## Cryptography -### Landmark theorems - -1. **Goldreich–Micali–Wigderson zero knowledge in full.** If one-way functions exist, every - language in NP has a computational zero-knowledge proof in Goldreich's sense (Def. 4.3.10): - for every `x ∈ L` and arbitrary auxiliary input `z`, against probabilistic polynomial-time - verifiers. This needs a bridge between the security premise and a clock independent of an - unbounded auxiliary word, witness-level Levin reductions, and sequential soundness - amplification to negligible error. Derive the advice-PRG premise of the auxiliary-input - theorem from uniform one-wayness, or replace it. -2. **Rompel's signature theorem.** One-way functions imply digital signatures that are - existentially unforgeable under adaptive chosen-message attacks, for arbitrary - polynomial-length messages: universal one-way hash functions and authentication trees. -3. **Gentry's bootstrapping, instantiated** ([#486]). A concrete LWE-based scheme satisfying the - correctness, security, bootstrappability and native-efficiency hypotheses of the generic - theorem: full native evaluation of the augmented GSW decryption circuit, bootstrappability - with compatible parameters, and the joint circular-security assumption needed for the - fixed-key endpoint. Gentry's exact concrete-security loss is a separate target. -4. **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time - multiparty functionality admits a protocol secure against static malicious corruptions, with - real/ideal simulation and abort, under the standard communication assumptions. -5. **Regev's worst-case to average-case reduction.** For suitable `q` and Gaussian noise rate - `α` with `αq > 2√n`, an efficient search-LWE algorithm yields a quantum polynomial-time - algorithm for worst-case GapSVP and SIVP within `Õ(n/α)`. The noise distribution, modulus - restrictions and quantum reduction are part of the theorem. +### Cryptographic landmarks + +- **Goldreich–Micali–Wigderson zero knowledge in full.** If one-way functions exist, every + language in NP has a computational zero-knowledge proof in Goldreich's sense (Def. 4.3.10): + for every `x ∈ L` and arbitrary auxiliary input `z`, against probabilistic polynomial-time + verifiers. This needs a bridge between the security premise and a clock independent of an + unbounded auxiliary word, witness-level Levin reductions, and sequential soundness + amplification to negligible error. State it under nonuniformly one-way functions, as + Goldreich does (*Foundations of Cryptography*, Vol. 1, Section 4.4), and derive the + nonuniform (advice-secure) PRG premise of the auxiliary-input theorem from that; uniform + one-wayness is not known to give such a generator. +- **Rompel's signature theorem.** One-way functions imply digital signatures that are + existentially unforgeable under adaptive chosen-message attacks, for arbitrary + polynomial-length messages: universal one-way hash functions and authentication trees. +- **Gentry's bootstrapping, instantiated** ([#486]). A concrete LWE-based scheme satisfying the + correctness, security, bootstrappability and native-efficiency hypotheses of the generic + theorem: full native evaluation of the augmented GSW decryption circuit, bootstrappability + with compatible parameters, and the joint circular-security assumption needed for the + fixed-key endpoint. Further targets: a uniform generator for the leveled scheme's wrapper + decryption circuits (uniform compactness), reuse of evaluated ciphertexts as fresh inputs + (multi-hop evaluation), and Gentry's exact concrete-security loss. +- **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time + multiparty functionality admits a protocol secure against static malicious corruptions, with + real/ideal simulation and abort, under the standard communication assumptions. +- **Regev's worst-case to average-case reduction.** For suitable `q` and Gaussian noise rate + `α` with `αq > 2√n`, an efficient search-LWE algorithm yields a quantum polynomial-time + algorithm for worst-case GapSVP and SIVP within `Õ(n/α)`. The noise distribution, modulus + restrictions and quantum reduction are part of the theorem. ### Modern fully homomorphic encryption After [#486], develop these in reviewable milestones, reusing the finite sampling, gadget -algebra, native certificates and game reductions where their hypotheses match. [#513] maps the -schemes to current libraries and workloads. +algebra, native certificates and game reductions where their hypotheses match. The +[pre-rewrite FHE section][archive-fhe] maps the schemes to current libraries and workloads. 1. **Ring arithmetic and RLWE.** Polynomial-ring operations over `(Z/qZ)[X]/(X^d + 1)`, RNS/CRT conversions, rounding and modulus-switching error bounds, and negacyclic NTTs implementing ring multiplication, with native certificates. Define the RLWE secret and error laws and experiment separately; an ordinary-LWE reduction does not give them. -2. **FHEW/TFHE programmable bootstrapping** (Ducas–Micciancio; Chillotti–Gama–Georgieva– - Izabachène). Ring-GSW external products, blind rotation, sample extraction and key switching; - prove the bootstrap decrypts to `f(m)` with its noise, failure, width and runtime bounds, - including negacyclic lookup restrictions and torus representations; floating-point FFT - implementations need their own rounding-error proof. Then smaller-key and batched variants, - preserving their exact secret distributions and joint error bounds. -3. **Exact packed BFV/BGV** (Brakerski–Gentry–Vaikuntanathan; Fan–Vercauteren). Slot encoding, +2. **FHEW/TFHE programmable bootstrapping** + ([Ducas–Micciancio](https://eprint.iacr.org/2014/816); + [Chillotti–Gama–Georgieva–Izabachène](https://eprint.iacr.org/2016/870)). Ring-GSW external + products, blind rotation, sample extraction and key switching; prove the bootstrap decrypts + to `f(m)` with its noise, failure, width and runtime bounds, including negacyclic lookup + restrictions and torus representations; floating-point FFT implementations need their own + rounding-error proof. Then the [smaller-key methods of Lee et al.](https://eprint.iacr.org/2022/198) + and batched variants, preserving their exact secret distributions and joint error bounds. +3. **Exact packed BFV/BGV** ([Brakerski–Gentry–Vaikuntanathan](https://eprint.iacr.org/2011/277); + [Fan–Vercauteren](https://eprint.iacr.org/2012/144)). Slot encoding, multiplication, relinearization, rotations and level management, with leveled evaluation before a separately proved refresh. Equality modulo the plaintext modulus differs from ordinary integer equality, which needs a range bound. -4. **Approximate packed CKKS and its bootstrap** (Cheon–Kim–Kim–Song), with an explicit +4. **Approximate packed CKKS and its bootstrap** + ([Cheon–Kim–Kim–Song](https://eprint.iacr.org/2016/421)), with an explicit approximate-correctness interface and a norm bound on decoded error covering rescaling, rounding, key switching and rotations. 5. **Scheme switching and threshold variants**, with explicit range/precision contracts, @@ -138,7 +164,7 @@ index links to canonical definitions rather than keeping a second set. - A tight time hierarchy, which needs a linear-overhead tape-indexed simulation, and the `f log f` hierarchy with its simulation bound. The space hierarchy for `log n ≤ g n`, which needs a universal simulation that does not hold its input. -- **Space** ([#885]): 2SAT NL-complete, `NSPACE(s) = coNSPACE(s)`, and Savitch bounds for general +- **Space** ([#885]): `NSPACE(s) = coNSPACE(s)`, and Savitch bounds for general space-constructible functions. - **Randomized logspace** ([#459], [#474]): RL and BPL, `USTCON ∈ RL`, Nisan's generator, `BPL ⊆ L²` and Saks–Zhou. @@ -156,7 +182,9 @@ index links to canonical definitions rather than keeping a second set. - Counting reductions and further oracle results preserving exact multiplicities; permanent #P-completeness; modular and counting hierarchies; the oracle-algorithm form of Stockmeyer's approximate counting. -- Boolean closures of the modular classes for composite moduli. +- For composite moduli: the prime-power collapse `Mod_{p^e}P = Mod_pP` and union closure. + Complement closure for moduli that are not prime powers is open, and relativizing proofs + cannot give it (Barrington–Beigel–Rudich), so it is not a library direction. - Target-relativized `LWPP^A`, `WPP^A` and `SBP^A` with `FP^A` targets; adaptive WPP closure and UP-oracle containment. - Native oracle counting machines: efficient encoded oracle checking, response-access costs and @@ -173,7 +201,8 @@ index links to canonical definitions rather than keeping a second set. Ordered first-order complexity follows Immerman: structures on `{0, …, n-1}` with `n ≥ 2`, FO means FO(≤, BIT), and `≤_fo`, `≤_fop` and `≤_qfp` keep their standard meanings; the order-free -`FO.Reduces` and `FO.QFReduces` stay as a general layer. In dependency order: +`FO.Reduces` and `FO.QFReduces` stay as a general layer. Numeric predicates are computed from the +universe size, not supplied as unverified input tables. In dependency order: - **Ordered completeness.** SAT, 3SAT, 3COL, independent set, clique and vertex cover NP-complete under first-order or quantifier-free projections; REACH NL-complete under @@ -302,17 +331,20 @@ each statement against the numbered result. Organize modules by subject, not cha query and sample bounds, canonical testers and lower bounds. - **Kolmogorov complexity and metacomplexity** ([#798], [#884]): prefix-free complexity, resource-bounded MCSP variants and connections to learning, cryptography and lower bounds; the - circuitized anti-checker with an efficient generator, hardness magnification and MINKT/MINCKT - as independently scoped developments; the reverse multi-tape-to-single-tape simulation and - machine-backed Nisan–Wigderson decoding. + circuitized anti-checker with an efficient generator, hardness magnification, MINCKT and + hardness results for MINKT, as independently scoped developments; the reverse + multi-tape-to-single-tape simulation and machine-backed Nisan–Wigderson decoding. - **Quantum computation** ([#896]): BQP ⊆ PP and the BBBV and Grover bounds; reusable - circuit, channel and measurement semantics, reusing suitable quantum foundations rather than - incompatible models; BQP, QMA and related query, communication and interactive classes. + 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 + problems. ## Machines, RAM and data structures -- **Plain computability** ([#862]): delete the tidy calculus, keeping only a machine-level - kernel inside the Machines layer, and switch the abstract bridges to the shared predicate. +- **Plain computability** ([#862]): complete the plain calculus ([#608]), delete the tidy + calculus, keeping only a machine-level kernel inside the Machines layer, and switch the + abstract bridges to the shared predicate. - **Certificate APIs and automation.** Infer encodings for ordinary functional expressions through constructor, projection, lookup and composition rules; generalize list, bounded-table, cache and nested-loop invariants where clients need them; keep separate time, workspace and @@ -353,9 +385,9 @@ reuse is demonstrated. - **One sensitivity API.** Define the sensitivity measures over any `Fintype` in CSLib and drop the separate measures of the sensitivity-separation development. -- **CNF evaluation automation:** `fun_prop` certificates for evaluating literals, clauses and - formulas under a polynomial-time assignment, and `Literal.eval` simp lemmas, so clients stop - unfolding `CNF.eval`. +- **CNF evaluation certificates:** `fun_prop` certificates for evaluating literals, clauses and + formulas under a polynomial-time assignment, so clients stop passing `CNF.eval`, + `Clause.eval` and `Literal.eval` to `fun_prop` as unfolding hints. - Factor indicator-expectation identities from PCP's second-moment calculation, and recurring cardinality and logarithm conversions, once a second client benefits. @@ -380,6 +412,8 @@ not planned, not as proved. - Vollmer's generalized-quantifier survey ([#399]): ordered leaf words, explicit uniformity and input-access models, finite-monoid classification and generalized logical quantifiers. +[archive]: https://github.com/cslib-community/complexitylib/blob/c89dd48c/ROADMAP.md +[archive-fhe]: https://github.com/cslib-community/complexitylib/blob/c89dd48c/ROADMAP.md#modern-fhe-methods-and-deployment-priorities [#321]: https://github.com/cslib-community/complexitylib/issues/321 [#324]: https://github.com/cslib-community/complexitylib/issues/324 [#361]: https://github.com/cslib-community/complexitylib/issues/361 @@ -389,9 +423,9 @@ not planned, not as proved. [#459]: https://github.com/cslib-community/complexitylib/issues/459 [#474]: https://github.com/cslib-community/complexitylib/issues/474 [#486]: https://github.com/cslib-community/complexitylib/issues/486 -[#513]: https://github.com/cslib-community/complexitylib/issues/513 [#581]: https://github.com/cslib-community/complexitylib/issues/581 [#585]: https://github.com/cslib-community/complexitylib/issues/585 +[#608]: https://github.com/cslib-community/complexitylib/issues/608 [#640]: https://github.com/cslib-community/complexitylib/issues/640 [#643]: https://github.com/cslib-community/complexitylib/issues/643 [#645]: https://github.com/cslib-community/complexitylib/issues/645 From f0c9b1df5513e504184b348986d548e843195810 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 04:10:58 -0400 Subject: [PATCH 3/3] doc(roadmap): drop directions completed since the draft MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completed since this draft: NSPACE closure under complement and the #885 follow-ups (issue closed), the AKS criterion and small-r bound, the GKR protocol, Chor–Goldreich, deterministic GPW lifting, BBBV and Grover, and the forward direction of Liu–Pass. Each bullet now names only what remains open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- ROADMAP.md | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index a2a78c226e..6d632b756b 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -22,7 +22,6 @@ the FHE industrial context, the first-order design decisions and the repository' | Plain computability: delete the tidy calculus, keeping a machine-level kernel | [#862], from [#456] | | Consolidation: duplicates, accurate statements and docs, less churn | [#949], [#939] | | A concrete LWE-based fully homomorphic scheme | [#486] | -| Immerman–Szelepcsényi follow-ups | [#885] | | Boneh–Shoup cryptography tracks; zero-knowledge architecture | [#640], [#643] | | A Verso guide with a chapter per area | [#585] | @@ -156,16 +155,15 @@ index links to canonical definitions rather than keeping a second set. ### Structure, time and space -- **PRIMES ∈ P** ([#893]): the hard direction of the AKS criterion, the small-`r` bound and the - polynomial-time algorithm on binary inputs. +- **PRIMES ∈ P** ([#893]): the polynomial-time AKS algorithm on binary inputs, on top of the + proved criterion and small-`r` bound. - Time, space and exponential hierarchies; oracle, advice, unambiguous and promise classes; completeness, padding, self-reducibility, relativization and oracle separations, preserving each reduction's resource bound. - A tight time hierarchy, which needs a linear-overhead tape-indexed simulation, and the `f log f` hierarchy with its simulation bound. The space hierarchy for `log n ≤ g n`, which needs a universal simulation that does not hold its input. -- **Space** ([#885]): `NSPACE(s) = coNSPACE(s)`, and Savitch bounds for general - space-constructible functions. +- **Space:** Savitch bounds for general space-constructible functions. - **Randomized logspace** ([#459], [#474]): RL and BPL, `USTCON ∈ RL`, Nisan's generator, `BPL ⊆ L²` and Saks–Zhou. - **Reingold:** a symmetric-machine model of SL, and the edge-list encoding of USTCON by a @@ -193,7 +191,7 @@ index links to canonical definitions rather than keeping a second set. ### Interactive proofs - **MIP = NEXP** ([#892]): `NEXP ⊆ MIP₂` through the BFL multilinearity test and arithmetization - of exponential-time tableaux; GKR delegation. + of exponential-time tableaux; an efficient GKR verifier under log-space uniformity. - Private-to-public-coin transformations, `AM[k] = AM`, interactive-machine characterizations of Arthur–Merlin classes, and statistical and perfect zero knowledge. @@ -311,9 +309,9 @@ each statement against the numbered result. Organize modules by subject, not cha - **Derandomization from hardness:** the infinitely-often variant, and the EXP ⊄ P/poly endpoint of Babai, Fortnow, Nisan and Wigderson. -- **Extractors** ([#895]) up to explicit two-source extractors; condensers, limited independence, - explicit expanders and space-bounded generators, with finite guarantees separate from uniform - construction and decoding costs. +- **Extractors** ([#895]) beyond Chor–Goldreich: two-source extractors for lower min-entropy; + condensers, limited independence, explicit expanders and space-bounded generators, with finite + guarantees separate from uniform construction and decoding costs. - **Codes:** Guruswami–Sudan list decoding and local decoding, keeping interpolation, list-size/agreement guarantees and decoding runtime as separate obligations; concrete list-decodable codes for Nisan–Wigderson. @@ -321,7 +319,8 @@ each statement against the numbered result. Organize modules by subject, not cha ## Communication, queries, learning and other models -- **Lifting** ([#890]): Raz–McKenzie and Göös–Pitassi–Watson query-to-communication lifting. +- **Lifting** ([#890]): applications of deterministic lifting, such as partition-number + separations, and randomized lifting. - Multiparty protocols, discrepancy and information complexity, direct-sum and direct-product results, and reductions to streaming, sketching and cell-probe lower bounds. - **Learning:** machine-certified running times for the LMN and Kushilevitz–Mansour learners; @@ -329,12 +328,13 @@ each statement against the numbered result. Organize modules by subject, not cha PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. - **Property and distribution testing:** access models, one/two-sided and tolerant testing, query and sample bounds, canonical testers and lower bounds. -- **Kolmogorov complexity and metacomplexity** ([#798], [#884]): prefix-free complexity, +- **Kolmogorov complexity and metacomplexity** ([#798], [#884]): the converse direction of + Liu–Pass (`K^t` mildly hard on average implies one-way functions); prefix-free complexity, resource-bounded MCSP variants and connections to learning, cryptography and lower bounds; the circuitized anti-checker with an efficient generator, hardness magnification, MINCKT and hardness results for MINKT, as independently scoped developments; the reverse multi-tape-to-single-tape simulation and machine-backed Nisan–Wigderson decoding. -- **Quantum computation** ([#896]): BQP ⊆ PP and the BBBV and Grover bounds; reusable +- **Quantum computation** ([#896]): BQP ⊆ PP; 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 @@ -434,7 +434,6 @@ not planned, not as proved. [#798]: https://github.com/cslib-community/complexitylib/issues/798 [#862]: https://github.com/cslib-community/complexitylib/issues/862 [#884]: https://github.com/cslib-community/complexitylib/issues/884 -[#885]: https://github.com/cslib-community/complexitylib/issues/885 [#886]: https://github.com/cslib-community/complexitylib/issues/886 [#888]: https://github.com/cslib-community/complexitylib/issues/888 [#889]: https://github.com/cslib-community/complexitylib/issues/889