15 Frontiers: directions beyond the current tracks
This chapter records areas the library does not yet cover. For each it names one precise target, what the target would build on, and a first step. Most nodes below are not formalized, and most of those are not yet ready: stating them in Lean needs a definition the library does not have. The exception is the general Karchmer–Wigderson theorem, with its protocol model: the imported algebraic-circuits library proves it (Definition 608 and Theorem 609). Where related infrastructure exists elsewhere, it is named as a starting point, not as progress toward the target.
15.1 Hardness of approximation
The PCP theorem is formalized in the interaction chapter (Theorem 389): \(\mathsf{NP}\) is the union of the classes \(\mathsf{PCP}(r, q)\) over constructible \(r = O(\log n)\) and \(q = O(1)\), with perfect completeness and soundness \(1/2\). Optimal inapproximability is a far target beyond it. The intermediate steps (gap constraint satisfaction, label cover and parallel repetition) appear in the interaction chapter’s section on hardness of approximation.
Write \(\mathsf{PCP}_{c,s}(r, q)\) for the variant of \(\mathsf{PCP}(r,q)\) with completeness \(c\) and soundness \(s\). For every \(\varepsilon {\gt} 0\), \(\mathsf{NP}\) is the union of the classes \(\mathsf{PCP}_{1-\varepsilon ,\, 1/2+\varepsilon }(r, 3)\) over \(r = O(\log n)\), with a verifier that accepts iff the XOR of the three bits it reads equals a bit determined by its coins. Consequently, approximating MAX-3SAT within a factor \(7/8 + \varepsilon \) is \(\mathsf{NP}\)-hard.
Compose the PCP theorem with parallel repetition (Label Cover) and a long-code test. Its soundness analysis is Fourier analysis with noise, extending the BLR argument. First step: define \(\mathsf{PCP}_{c,s}\) with explicit rational \(c\) and \(s\), show it agrees with the existing \(\mathsf{PCP}\) at \(c = 1\), \(s = 1/2\), and define gap-preserving reductions between constraint satisfaction problems.
15.2 Derandomization
The library’s metacomplexity modules, presented in the average-case chapter, already formalize finite pseudorandomness infrastructure:
fixed-length generators Complexity.BitGenerator, arbitrary maps with no efficiency built in, and their distinguishing advantage against a finite test (Definition 477);
Yao’s hybrid step and the next-bit-prediction identity (Lemma 478);
Nisan–Wigderson designs Complexity.NWDesign and the associated generator Complexity.NWDesign.generator (Definition 479);
a finite reconstruction step against tests made of strings of high time-bounded Kolmogorov complexity (Theorem 480).
What is missing is the circuit-based statement of pseudorandomness, the existence of designs with the needed parameters, and the hardness-versus-randomness theorems built on them.
A family \(G_m : \{ 0,1\} ^{\ell (m)} \to \{ 0,1\} ^m\) is a pseudorandom generator with seed length \(\ell \) if two conditions hold:
for every \(m\) and every circuit \(C\) of size at most \(m\) on \(m\) inputs, \(\lvert \Pr _s[C(G_m(s)) = 1] - \Pr _u[C(u) = 1] \rvert {\lt} 1/10\);
\(G_m\) is computable in time \(2^{O(\ell (m))}\).
Suppose there are \(L \in \bigcup _c \mathsf{DTIME}(2^{cn})\) and \(\varepsilon {\gt} 0\) such that, for all sufficiently large \(n\), no circuit of size \(2^{\varepsilon n}\) agrees with \(L\) on more than a \(1/2 + 2^{-\varepsilon n}\) fraction of inputs of length \(n\). Then \(\mathsf{BPP} = \mathsf{P}\).
The NW generator built from \(L\) on a design with logarithmic seed is a pseudorandom generator by the hybrid and reconstruction argument. Enumerate its \(\mathrm{poly}(n)\) seeds. First step: prove that designs with the required parameters exist, then restate the existing finite reconstruction against circuit tests instead of Kolmogorov tests.
Suppose there are \(L \in \bigcup _c \mathsf{DTIME}(2^{cn})\) and \(\varepsilon {\gt} 0\) such that, for all sufficiently large \(n\), no circuit of size \(2^{\varepsilon n}\) decides \(L\) on all inputs of length \(n\). Then \(\mathsf{BPP} = \mathsf{P}\). This almost-everywhere hypothesis is stronger than \(L \notin \mathsf{SIZE}(2^{\varepsilon n})\): the library’s \(\mathsf{SIZE}\) bounds the size at every length (Definition 246), so non-membership only says that some length has no such circuit, and even an eventual size bound would give only infinitely-often hardness.
Amplify worst-case hardness to the average-case hardness required by Nisan–Wigderson, via local list decoding of a concatenated code or the XOR lemma. First step: instantiate the abstract list-decodable code interface Complexity.BooleanListCode, whose decoder reads the whole received word, with a concrete code, and add the local decoding this argument needs. An explicit list-decodable family is itself still planned (Theorem 465).
Every \((\log (s/\varepsilon ))^{O(d^2)}\)-wise independent distribution on \(\{ 0,1\} ^n\) \(\varepsilon \)-fools every unbounded fan-in circuit of size \(s\) and depth \(d\).
Approximate the circuit by a low-degree polynomial in two ways: in \(L^2\) via Linial–Mansour–Nisan, and pointwise off a small error set via Razborov–Smolensky. Then sandwich it. First step: define \(k\)-wise independent distributions and \(\varepsilon \)-fooling for a finite family of tests.
15.3 Space-bounded derandomization
For all \(R\), \(w\), and \(\varepsilon \) there is a generator \(G : \{ 0,1\} ^{O(\log R \cdot \log (Rw/\varepsilon ))} \to \{ 0,1\} ^R\) that \(\varepsilon \)-fools every read-once oblivious branching program of length \(R\) and width \(w\). The generator is computable in space linear in its seed. Consequently, randomized logspace with two-sided error (\(\mathsf{BPL}\)) is contained in \(\mathsf{DSPACE}(\log ^2 n)\).
Recursively apply pairwise-independent hash functions, halving the program at each level. The library’s fixed-width pairwise-independent hash families (Definition 182), built for Stockmeyer-style counting, are a starting point. First step: define read-once branching programs and \(\mathsf{BPL}\) as logspace probabilistic machines that halt in polynomial time. The library’s branching programs are width-\(w\) permutation programs, used at width \(5\) for Barrington’s theorem: each step applies a permutation of the \(w\) states selected by one input bit, so they are not required to be read-once, and their steps are permutations rather than arbitrary maps between layers.
Undirected \(s\)–\(t\) connectivity is in \(\mathsf{L}\).
Make the graph regular, then alternate powering with zig-zag products against a constant-size expander until the graph is an expander of logarithmic diameter. The resulting rotation maps are computable in logspace. The PCP development’s internal modules contain regular graphs presented by rotation maps, the zig-zag product of \(G\) and \(H\) with the spectral bound \(\lambda _G + \lambda _H + \lambda _H^2\) (the simpler Reingold–Vadhan–Wigderson estimate), and a zig-zag tower of expanders grown from one constant-size base graph, all of which may be reusable. They are not stated about space-bounded computation. First step: fix a graph encoding and state the undirected connectivity language.
15.4 Cryptographic foundations
\(f \in \mathsf{FP}\) is one-way (against nonuniform adversaries) if for every family of polynomial-size circuits \((A_n)\), the function \(n \mapsto \Pr _{x \in \{ 0,1\} ^n}[f(A_n(f(x))) = f(x)]\) is negligible.
Let \(f\) be one-way and \(g(x, r) = (f(x), r)\) with \(|r| = |x|\). Then \(\langle x, r \rangle \bmod 2\) is a hard-core predicate for \(g\): every family of polynomial-size circuits predicts it from \(g(x,r)\) with probability at most \(1/2 + \mathrm{negl}(n)\).
A good predictor is a noisy oracle for the Hadamard encoding of \(x\). Local list decoding, which finds every large Fourier coefficient of the predictor, recovers a short list containing \(x\). First step: define hard-core predicates, and prove the finite list-decoding statement for the Hadamard code in Fourier language.
If a length-doubling pseudorandom generator secure against polynomial-size circuits exists, then so does a pseudorandom function family secure against polynomial-size oracle circuits.
Evaluate the tree of generator applications along the input bits. A hybrid argument over tree levels, restricted to the nodes the adversary queries, bounds the advantage. First step: define cryptographic PRGs and a PRF oracle game with negligible advantage, compatible with the planned pseudorandom function families of the natural-proofs barrier (Definition 419). Also prove that one-way permutations yield PRGs via Goldreich–Levin and the existing finite Yao hybrid step (Lemma 478).
15.5 Communication complexity
The library formalizes the monotone Karchmer–Wigderson correspondence (Theorem 322). Its rectangle-indexed protocols (Complexity.KarchmerWigderson.Protocol) translate to and from monotone formulas with exactly equal depth. The imported algebraic-circuits library proves the general Karchmer–Wigderson theorem for De Morgan formulas, for protocols specialized to Karchmer–Wigderson games (Definition 608 and Theorem 609; the same result is Theorem 301). General two-party communication complexity is not formalized: protocols for arbitrary functions and relations, randomized protocols, and lower-bound methods such as rectangle partitions, fooling sets and discrepancy.
A deterministic protocol for \(f : X \times Y \to Z\) is a binary tree. Each internal node is owned by Alice, who branches on a function of \(x\), or by Bob, who branches on a function of \(y\). Each leaf is labelled by an output. The cost is the depth, and \(D(f)\) is the minimum cost of a protocol computing \(f\). Only the protocols of Karchmer–Wigderson games are formalized (Definition 608); their leaves name a coordinate, and they solve a relation rather than compute a function.
For every distribution \(\mu \) on \(X \times Y\) and every error \(\varepsilon {\lt} 1/2\), public-coin randomized protocols satisfy \(R_\varepsilon (f) \ge \log _2\bigl((1 - 2\varepsilon )/\mathrm{disc}_\mu (f)\bigr)\). The inner product \(\mathrm{IP}_n(x,y) = \sum _i x_i y_i \bmod 2\) has uniform discrepancy at most \(2^{-n/2}\). Hence \(R_{1/3}(\mathrm{IP}_n) \ge n/2 - O(1)\).
A \(c\)-bit protocol partitions \(X \times Y\) into at most \(2^c\) rectangles. Lindsey’s lemma bounds each rectangle’s bias using orthogonality of the Hadamard matrix, that is, of the parities. First step: prove the rectangle partition lemma and the fooling-set bound \(D(\mathrm{EQ}_n) \ge n\).
These definitions come from the imported algebraic-circuits library. A De Morgan formula on \(n\) inputs is a binary tree whose leaves are literals \(x_i\) or \(\lnot x_i\) or Boolean constants and whose internal nodes are binary AND or OR gates. A protocol on \(n\) inputs is a binary tree whose leaves each name a coordinate \(i {\lt} n\) and whose internal nodes are each owned by Alice or by Bob and branch by an arbitrary Boolean function of the owner’s whole input in \(\{ 0,1\} ^n\); on inputs \(x\) for Alice and \(y\) for Bob it outputs the coordinate at the leaf it reaches. For both, the depth is the length of a longest root-to-leaf path (a leaf has depth \(0\)) and the size is the number of leaves, constant leaves included. A protocol solves the game on a rectangle \(A \times B\) if its output \(i\) satisfies \(x_i \neq y_i\) for all \(x \in A\) and \(y \in B\); it solves the Karchmer–Wigderson game of \(f : \{ 0,1\} ^n \to \{ 0,1\} \) if it solves the game on \(f^{-1}(1) \times f^{-1}(0)\). The minimum formula depth and size of \(f\) (over formulas computing \(f\) at every input) and the minimum protocol depth and size of its game are infima in \(\mathbb {N} \cup \{ \infty \} \), equal to \(\infty \) when no formula or protocol exists.
In the model of Definition 608, for every \(n \ge 1\) and every \(f : \{ 0,1\} ^n \to \{ 0,1\} \), constant or not, the minimum depth of a De Morgan formula computing \(f\) equals the minimum depth of a protocol for the Karchmer–Wigderson game of \(f\), in which Alice holds \(x \in f^{-1}(1)\), Bob holds \(y \in f^{-1}(0)\), and they must output some \(i\) with \(x_i \neq y_i\). Likewise the minimum number of leaves of a formula computing \(f\) equals the minimum number of leaves of a protocol for the game. The hypothesis \(n \ge 1\) cannot be dropped: for \(n = 0\) no protocol exists, since a leaf must name a coordinate, while a constant formula has depth \(0\). This is the result of Theorem 301.
Both translations preserve depth and leaf count exactly. From a formula: an OR gate becomes an Alice node where she says whether her input satisfies the left disjunct, and play continues in a disjunct her input satisfies; an AND gate becomes a Bob node where he says whether his input satisfies the left conjunct, and play continues in a conjunct his input violates. A literal leaf names its coordinate, and a constant leaf, reachable only on an empty rectangle, names a default coordinate, which exists because \(n \ge 1\). From a protocol: track the rectangle of inputs consistent with the transcript. Alice nodes become OR gates, Bob nodes become AND gates, and a leaf naming \(i\) becomes whichever of \(x_i\) and \(\lnot x_i\) is \(1\) on Alice’s side and \(0\) on Bob’s side, or a constant when one side is empty.
15.6 Algebraic complexity
The imported algebraic-circuits library already has arithmetic circuits: CSLib straight-line circuits over its arithmetic signature (Algebraic.Arithmetic.signature), with binary addition, binary multiplication and constant gates, evaluable in any carrier with addition and multiplication, in particular as formal polynomials in Mathlib’s MvPolynomial. They are used for lower bounds on computing a single polynomial, such as Theorem 306. Polynomial families, degree bounds, projections and the classes below are not formalized.
Fix a field \(\mathbb {F}\). An arithmetic circuit is a DAG with \(+\) and \(\times \) gates over variables and field constants. \(\mathsf{VP}\) is the class of polynomial families \((f_n)\) with \(\mathrm{poly}(n)\) variables and degree, computed by \(\mathrm{poly}(n)\)-size arithmetic circuits. \(\mathsf{VNP}\) is the class of families \(f_n(x) = \sum _{e \in \{ 0,1\} ^{m(n)}} g_n(x, e)\) with \((g_n) \in \mathsf{VP}\) and \(m\) polynomial.
Over any field of characteristic other than \(2\), the permanent family \((\mathrm{perm}_n)\) is \(\mathsf{VNP}\)-complete under polynomial-size projections.
Show the permanent is in \(\mathsf{VNP}\) via Ryser’s formula. For hardness, convert formulas to weighted graphs whose cycle covers compute the polynomial. First step: on top of the imported arithmetic circuits and their MvPolynomial semantics, define polynomial families, their size and degree bounds, and \(p\)-projections. The Boolean counterpart, \(\# \mathsf{P}\)-completeness of the \(0/1\) permanent, would connect to the existing class \(\# \mathsf{P}\) (Definition 170).
15.7 Fine-grained and parameterized complexity
Suppose that for every \(\delta {\gt} 0\) there is \(k\) such that \(k\)-SAT on \(n\) variables has no algorithm running in time \(2^{(1-\delta )n}\, \mathrm{poly}(n)\) (SETH). Then for every \(\delta {\gt} 0\) there is \(c\) such that Orthogonal Vectors on \(N\) vectors of dimension \(c \log N\) has no algorithm running in time \(N^{2-\delta }\).
Split the variables into two halves and enumerate partial assignments. Map each to a vector over the clauses, after sparsification. First step: running times are measured in a parameter (the number of variables \(n\)) rather than input length, so fine-grained reductions need explicit time bounds in named parameters, beyond the existing \(\mathsf{DTIME}\).
A parameterized problem is a language \(L\) with a polynomial-time parameter \(\kappa \). It is in \(\mathsf{FPT}\) if it is decidable in time \(g(\kappa (x)) \cdot |x|^{O(1)}\) for some computable \(g\). An fpt-reduction preserves membership, runs in fpt time, and bounds the target parameter by a function of the source parameter. \(\mathsf{W[1]}\) is the closure of \(k\)-Clique under fpt-reductions. First targets: Vertex Cover is in \(\mathsf{FPT}\) by a \(2^k\)-branching algorithm, and \(k\)-Clique is \(\mathsf{W[1]}\)-complete by definition, with \(k\)-Independent Set equivalent to it.
15.8 Quantum computation
Define \(\mathsf{BQP}\) by polynomial-time uniform families of quantum circuits over the gate set \(\{ \mathrm{Hadamard}, \mathrm{Toffoli}\} \), with error \(1/3\). Then \(\mathsf{BQP} \subseteq \mathsf{PP}\).
With Hadamard and Toffoli gates all amplitudes are real: each amplitude is a signed count of computation paths divided by \(2^{h/2}\), where \(h\) is the number of Hadamard gates. Squaring, the acceptance probability is \((\# \text{positive} - \# \text{negative})/2^h\) over pairs of polynomially checkable paths that end in the same accepting basis state, which a \(\mathsf{PP}\) machine can compare with a threshold. First step: define the path-sum semantics of such circuits and prove it agrees with the matrix semantics on small examples.