Dependencies

If \(f\) has degree at most \(k\), then \(\lVert f \rVert _4 \le \sqrt{3}^{\, k}\, \lVert f \rVert _2\).

\(\lVert T_{1/\sqrt{3}} f \rVert _2 \le \lVert f \rVert _{4/3}\) for every \(f\).

For each fixed \(d\), every unbounded fan-in circuit of depth \(d\) computing the parity of \(n\) bits has size \(2^{\Omega (n^{1/d})}\). Håstad’s bound (Theorem 337) improves the exponent to \(n^{1/(d-1)}\).

There are oracles \(A\) and \(B\) with \(\mathsf{P}^A = \mathsf{NP}^A\) and \(\mathsf{P}^B \neq \mathsf{NP}^B\).

If for some \(\varepsilon {\gt} 0\) there is a pseudorandom function family in \(\mathsf{P/poly}\) against which no distinguisher of size \(2^{n^{\varepsilon }}\) has advantage \(2^{-n^{\varepsilon }}\) or more, then no \(\mathsf{P/poly}\)-constructive property of density at least \(2^{-O(n)}\) is useful against \(\mathsf{P/poly}\). The pseudorandomness hypothesis is an explicit assumption, not a proved fact.

\(\mathsf{BPP} \subseteq \mathsf{PAdvice}\).

Some language is not in \(\mathsf{P/poly}\).

\(\mathsf{PAdvice} = \mathsf{P/poly}\).

\(\mathsf{NP} \subseteq \mathsf{IP}\).

\(\mathsf{AC}^0 \subsetneq \mathsf{TC}^0\).

Let \(C\) be a circuit whose dependency graph has longest paths of at most \(2^k\) vertices, and let \(r \le k\). There is a set \(F\) of dependency edges with \(k\, |F| \le r \cdot \mathrm{totalFanIn}(C)\) whose removal leaves a graph whose longest paths have at most \(2^{k-r}\) vertices.

For the concrete universal machine \(\mathtt{utmTM}\): every string has finite plain complexity, and there are constants \(c, a, k\) with \(C^t_{\mathtt{utmTM}}(x) \le |x| + c\) whenever \(t \ge a(2|x|+3)^k\).

The complement of \(\mathrm{SAT}\) (as a set of bit strings, so including all malformed strings) is \(\mathsf{coNP}\)-complete. \(\mathrm{SAT} \in \mathsf{P} \iff \mathsf{P} = \mathsf{NP}\), and \(\mathrm{SAT} \in \mathsf{coNP} \iff \mathsf{NP} = \mathsf{coNP}\).

Let \(C\) be a fan-in-two circuit with \(s + a\) inputs, \(a \ge 1\), and \(M \ge 1\) outputs, whose first \(s\) inputs are a random seed, and let a decidable predicate say which outputs are correct for which inputs \(u \in \{ 0,1\} ^a\). If for every \(u\) the seeds \(\sigma \) on which \(C(\sigma u)\) is incorrect for \(u\) have probability at most \(2^{-(a+1)}\), then one seed is correct for every \(u\), and hardwiring it gives a circuit on \(a\) inputs with the same internal gate count and the same size that is correct for every \(u\).

Now fix \(q \ge 1\), \(t\), and sets \(S_u \subseteq \{ 0,1\} ^n\) for \(u \in \{ 0,1\} ^a\), and say \(C\) implements the relative estimator if, for every seed \(\sigma \) and every \(u\), the output of \(C(\sigma u)\) read as a little-endian unsigned integer equals the output of the estimator of Theorem 188 on \(S_u\) with seed \(\sigma \). Then \(C\) fails to output a relative-error-\(1/q\) approximation of \(|S_u|\) exactly on the estimator’s failure seeds, hence with probability at most \(2^{-t}\) for every \(u\); for \(t = a + 1\), hardwiring a seed gives a circuit of the same size that is accurate on every \(u\). The same holds for a fixed-round adaptive oracle program of fan-in-two circuits (AdaptiveOracleProgram): inlining circuits that answer every query of the right width as the oracle does preserves implementing the estimator, and if the program implements it with \(t = a + 1\) relative to every oracle deciding a language \(A \in \mathsf{P/poly}\), then for some polynomial-size circuit family deciding \(A\), inlining that family and hardwiring a seed gives an ordinary circuit, of the same size as the inlined program, that is accurate on every \(u\).

\(\mathsf{BPP} \subseteq \mathsf{PH}\).

\(\mathsf{BPP} \subseteq \mathsf{PSPACE}\).

Every \(F : \{ 0,1\} ^n \to \{ 0,1\} \) on bit strings determines the Boolean-valued function \(x \mapsto \chi (F(x))\) on the cube. This must be a public bridge. The PCP development has only a related map, Complexity.signOf in an internal module, which sends an \(\mathbb {F}_2\)-valued function on the cube to its \(\pm 1\) encoding. It does not act on bit strings.

The convolution is \((f * g)(x) = \mathbb {E}_y[f(y)\, g(x + y)]\). A density is a nonnegative \(\varphi \) with \(\mathbb {E}[\varphi ] = 1\). The density of a nonempty set \(A\) is \(\varphi _A = 1_A / \mathbb {E}[1_A]\). For \(A = \emptyset \) the Lean definition divides by zero and returns the zero function, so theorems about \(\varphi _A\) assume \(A\) is nonempty.

\(\mathrm{BooleanFunction}(n)\) is the real vector space of functions \(f : \mathbb {F}_2^n \to \mathbb {R}\). Its inner product space structure comes from the uniform-measure inner product \(\langle f, g \rangle = 2^{-n} \sum _x f(x) g(x)\). The uniform expectation \(\mathbb {E}[f]\) is the average of \(f\) over the cube, so \(\mathbb {E}[f] = 2^{-n} \sum _x f(x)\) and \(\langle f, g \rangle = \mathbb {E}_x[f(x) g(x)]\). The type is a def rather than an abbrev, so the \(L^2\) norm does not clash with Mathlib’s sup norm on function types.

The degree-\(k\) part of \(f\) is \(f^{=k} = \sum _{|S| = k} \widehat{f}(S) \chi _S\), and \(f^{\le k} = \sum _{|S| \le k} \widehat{f}(S) \chi _S\). The weight above degree \(k\) is \(W^{{\gt}k}[f] = \sum _{|S| {\gt} k} \widehat{f}(S)^2\). The degree of \(f\) is \(\max \{ |S| : \widehat{f}(S) \neq 0\} \), valued in \(\mathbb {N} \cup \{ \bot \} \) with \(\bot \) for \(f = 0\). For Boolean-valued \(f\), the spectral sample is the probability distribution \(S \mapsto \widehat{f}(S)^2\) on subsets of \([n]\).

\(x^{\oplus i}\) flips coordinate \(i\) of \(x\). This is an involutive equivalence of the cube. The derivative is defined spectrally: \(D_i f = \sum _{S \ni i} \widehat{f}(S)\, \chi _{S \setminus \{ i\} }\). The sensitivity operator is \(L_i f(x) = (f(x) - f(x^{\oplus i}))/2\). These are different operators: by Theorem 530, \(D_i\) removes \(i\) from each frequency, while \(L_i\) keeps only the frequencies that contain \(i\).

The Fourier coefficient of \(f\) on \(S\) is \(\widehat{f}(S) = \langle f, \chi _S \rangle \), and its Fourier weight is \(\widehat{f}(S)^2\). The weight at degree \(k\) is \(W^k[f] = \sum _{|S| = k} \widehat{f}(S)^2\).

Spectrally, \(\mathrm{Inf}_i[f] = \sum _{S \ni i} \widehat{f}(S)^2\) and \(\mathbf{I}[f] = \sum _S |S|\, \widehat{f}(S)^2\).

\(f\) is linear if \(f = \chi _S\) for some \(S\). It is multiplicative if \(f(x + y) = f(x) f(y)\) for all \(x, y\). It is \(\varepsilon \)-close to \(g\) if \(\mathrm{dist}(f, g) \le \varepsilon \), and \(\varepsilon \)-close to a property \(P\) if it is \(\varepsilon \)-close to some \(g\) satisfying \(P\). The BLR acceptance probability is \(\Pr _{x,y}[f(x) f(y) = f(x + y)]\) for independent uniform \(x\) and \(y\).

For real \(p \ge 1\), \(\lVert f \rVert _p = \mathbb {E}[|f|^p]^{1/p}\) under the uniform measure. It should agree with the existing \(L^2\) norm at \(p = 2\) and satisfy Hölder’s inequality.

\(\mathrm{Var}[f] = \mathbb {E}[f^2] - \mathbb {E}[f]^2\) and \(\mathrm{Cov}[f,g] = \mathbb {E}[fg] - \mathbb {E}[f]\mathbb {E}[g]\). The uniform probability of a predicate \(P\) is \(\Pr [P] = \mathbb {E}[1_P]\), where \(1_P\) is the \(0\)–\(1\) indicator of \(P\), and the relative Hamming distance is \(\mathrm{dist}(f,g) = \Pr _x[f(x) \neq g(x)]\).

Order the cube coordinatewise by the values \(\chi (x_i) \in \{ -1, 1\} \). So \(x \le y\) iff \(y\) is obtained from \(x\) by changing some coordinates from \(1\) to \(0\). A function \(f\) is monotone if \(x \le y\) implies \(f(x) \le f(y)\). This is O’Donnell’s order on \(\{ -1,1\} ^n\). It is the reverse of the bitwise order on \(\mathbb {F}_2^n\), and the Lean definition must record the choice explicitly. The circuit library’s IsMonotoneBoolFun is a different notion: monotonicity of \(\{ 0,1\} \)-valued functions on bit strings in the bitwise order.

All four are defined spectrally, for \(\rho \in \mathbb {R}\):

• \(\mathrm{Stab}_\rho [f] = \sum _S \rho ^{|S|} \widehat{f}(S)^2\);

• \(\mathrm{Stab}_\rho [f,g] = \sum _S \rho ^{|S|} \widehat{f}(S)\widehat{g}(S)\);

• the noise (Bonami–Beckner) operator \(T_\rho f = \sum _S \rho ^{|S|} \widehat{f}(S) \chi _S\);

• \(\mathrm{NS}_\rho [f] = (\langle f, f \rangle - \mathrm{Stab}_\rho [f])/2\).

\(\chi : \mathbb {F}_2 \to \mathbb {R}\) sends \(b \mapsto (-1)^b\). For \(S \subseteq [n]\), the parity function is \(\chi _S(x) = \prod _{i \in S} \chi (x_i)\), so \(\chi _\emptyset = 1\). A function is Boolean-valued if every value is \(1\) or \(-1\).

Hirahara’s 2018 distribution \(D^u\): at parameter \(m {\gt} 0\), choose \(n \in \{ 0, \dots , m-1\} \) uniformly and \(x \in \{ 0,1\} ^n\) uniformly, and output \(\mathrm{pair}(x, 1^{m-n})\). The library realizes this with the seed space \(\{ 0, \dots , m-1\} \times \{ 0,1\} ^m\), keeping the first \(n\) bits of the \(m\)-bit string as \(x\), so the slice has \(m \cdot 2^m\) equiprobable seeds. The parameter \(m\) is the sum \(|x| + (m-n)\) of the component lengths, not the length of the encoded pair. The slice \(m = 0\) is totalized as the point \(\mathrm{pair}(\epsilon , \epsilon )\) (a single seed), a library convention.

A heuristic is a deterministic map from strings to the three answers accept, reject and fail; it is errorless for \(L\) if it never accepts outside \(L\) and never rejects inside \(L\). It runs in polynomial time when its answer, encoded as \([\mathrm{true}]\), \([\mathrm{false}]\) or the empty string respectively, is a function in \(\mathsf{FP}\). A distributional problem is a language with a finite ensemble of input strings. For \(\delta \colon \mathbb {N} \to \mathbb {Q}\), \(\mathsf{AvgP}_\delta \) consists of the distributional problems having a polynomial-time errorless heuristic whose failure probability on slice \(n\) is at most \(\delta (n)\) for every \(n\). \(\mathsf{AvgP} = \bigcap _{c \in \mathbb {N}} \mathsf{AvgP}_{\delta _c}\) with \(\delta _c(n) = 1/\max (1,n)^c\), which is \(n^{-c}\) for \(n \ge 1\) and \(1\) at \(n = 0\): for each \(c\) there is a possibly different polynomial-time errorless heuristic meeting \(\delta _c\). This is not the single-scheme formulation in which the heuristic receives \(1/\delta \) as an input; relating the two is part of Definition 471.

A generator is any map \(G \colon \{ 0,1\} ^d \to \{ 0,1\} ^m\) (no efficiency is built in). A test \(T \subseteq \{ 0,1\} ^m\) has distinguishing advantage \(|\Pr _s[G(s) \in T] - \Pr _y[y \in T]|\). Relative to a machine \(M\), clock \(t\) and threshold \(r\): \(T\) is a random test if every \(y \in T\) has \(C^t_M(y) \ge r\); \(T\) is \(\delta \)-dense if \(\Pr _y[y \in T] \ge \delta \); and \(G\) has low complexity if every output satisfies \(C^t_M(G(s)) {\lt} r\).

For an oracle machine \(N\) and Boolean oracle \(A\), \(C^{t,A}_N(x)\) is the minimum length of a program on which \(N^A\) produces \(x\) within \(t\) steps (\(\infty \) if there is none). The random-access oracle of a string \(y\) answers canonical tagged queries “bit \(i\) of \(y\)” and “is \(i {\lt} |y|\)” (malformed and out-of-range queries answer false), so it determines both the contents and the length of \(y\). Conditional complexity is \(C^t_N(x \mid y) = C^{t, \mathrm{oracle}(y)}_N(x)\). Other conditioning conventions (sequential input, paper-specific evaluators) are not identified with this one.

\(\mathrm{cd}^{s,t}_M(x) = C^s_M(x) - C^t_M(x)\) and \(\mathrm{cd}^{s}_M(x) = C^s_M(x) - C_M(x)\), where the difference is \(\infty \) if either term is \(\infty \) and truncated natural subtraction otherwise. Both are defined for all clocks; the second subtraction is always exact, and the first is exact when \(s \le t\) (then \(C^t_M(x) \le C^s_M(x)\)), the case in which its laws are stated.

An ensemble is polynomial-time samplable when a single machine computes its sample map from a polynomially long seed in time polynomial in \(n\), with closure under polynomial-time maps, pairing, padding, products and efficiently chosen mixtures. \(\mathsf{DistNP}\) consists of pairs \((L, D)\) with \(L \in \mathsf{NP}\) and \(D\) polynomial-time samplable. Levin-style domination is kept as a separate notion if needed.

A finite ensemble assigns to each parameter \(n\) a nonempty finite seed space \(S_n\) (with decidable equality) and a sample map \(S_n \to \alpha \); the distribution at \(n\) is the pushforward of the uniform distribution on \(S_n\), with multiplicity. A dyadic ensemble is the special case \(S_n = \{ 0,1\} ^{\ell (n)}\), and its embedding into finite ensembles preserves every event probability. No sample map is called efficient until a machine realizes it (Definition 470). Samples need not have length \(n\).

Hirahara 2022, Definitions 6.1 and 6.5. Fix an ordinary machine \(M\) and a conditional oracle machine \(N\). For a widening trivariate clock \(\tau (|x|, |y|, t) \ge t\), the promise \(\mathsf{GapMINcKT}\) on canonical \((x, y, 1^t, 1^s)\) has yes side \(C^t_N(x \mid y) + \mathrm{cd}^{t,\tau }_M(y) \le s\) and no side \(C^{\tau }_N(x \mid y) {\gt} s + \lfloor \log _2 \tau \rfloor \). The multiplicative version with factor \(\phi \colon \mathbb {N} \to \mathbb {N}\), \(\phi \ge 1\), has the same yes side and no side \(C^{\tau }_N(x \mid y) {\gt} \phi (|x|) \cdot s + \lfloor \log _2 \tau \rfloor \). A conditional estimator \(B\) satisfies Proposition 6.2’s sandwich if \(B(x, y, 1^t) \le C^t_N(x \mid y) + \mathrm{cd}^{t,\tau }_M(y)\) and \(C^{\tau }_N(x \mid y) \le B(x, y, 1^t) + \lfloor \log _2 \tau \rfloor \) on every instance.

Hirahara 2022, Definition 3.3: for a widening clock \(\tau (n, t) \ge t\), the promise on canonical \((x, 1^t, 1^s)\) with yes side \(C^t_U(x) \le s\) and no side \(C^{\tau }_U(x) {\gt} s + \lfloor \log _2 \tau \rfloor \), where \(\tau = \tau (|x|, t)\). An estimator \(B\) satisfies Fact 3.4’s sandwich if \(B(x, 1^t) \le C^t_U(x)\) and \(C^{\tau }_U(x) \le B(x, 1^t) + \lfloor \log _2 \tau \rfloor \) on every instance \((x, 1^t)\); it satisfies it on a set \(E\) of instances if these hold for every instance in \(E\).

Heuristics that may answer incorrectly on a set of bounded probability, \(\mathsf{Heur}_\delta \mathsf{P}\) and \(\mathsf{HeurP}\), the single-scheme versions of \(\mathsf{AvgP}\) and \(\mathsf{HeurP}\), randomized variants, and the standard amplification and inclusion lemmas.

An NW design is an ordered family \(S_1, \dots , S_m\) of \(\ell \)-element subsets of \([d]\), each enumerated injectively. It has overlap budget \(b\) if for every \(i\), \(\sum _{j{\lt}i} 2^{|S_i \cap S_j|} + (m - i) \le b\) (Hirahara’s weak-design cost). For \(f \colon \{ 0,1\} ^\ell \to \{ 0,1\} \) the generator is \(\mathrm{NW}^f(s) = (f(s|_{S_1}), \dots , f(s|_{S_m}))\).

Distributional Kolmogorov complexity, approximation-preserving padding, and the Meta-Complexity Padding Conjecture of Hirahara 2023 stated as an explicit hypothesis, together with its conditional characterization of one-way functions. It is never used as an unconditional theorem.

For an ordinary machine \(M\), a conditional oracle machine \(N\), a clock transformation \(\kappa \) and a loss \(\lambda \), \(\mathrm{SoI}(M, N, \kappa , \lambda )\) asserts, for all \(x, y, t\) with \(|x| + |y| \le t\),

The polynomial package asks for some \(\kappa \) with \(\kappa (t) \ge t\) and \(\kappa (t) \le a(t+1)^k\) for all \(t\), and \(\lambda (t) = \lfloor \log _2 \kappa (t) \rfloor + c\) for a constant \(c\). The inequality holds trivially wherever \(C^t_M(\mathrm{pair}(x,y)) = \infty \), in particular whenever \(t\) is too small for \(M\) to print \(\mathrm{pair}(x,y)\), and everywhere for a machine \(M\) that describes nothing; so SoI has content only for machines constrained by other hypotheses. (An earlier version also required \(C^t_M(\mathrm{pair}(x,y)) {\lt} \infty \) whenever \(|x| + |y| \le t\). That is impossible, since a run of \(t\) steps writes at most \(t\) output bits while \(|\mathrm{pair}(x,y)| = 2|x| + 2 + |y| {\gt} t\) at \(t = |x| + |y|\), and the requirement was removed.) SoI is a hypothesis; nothing in the library asserts it.

An enumeration \(i \mapsto (M_i, p_i)\) of oracle TMs paired with polynomial clocks such that every polynomial-time oracle language, relative to every oracle, is decided by some clocked \(M_i\), and the clocked machines are simulated uniformly in the oracle.

For a set \(P\) of Boolean functions on \(n\) bits (necessarily finite), its density is the exact rational \(|P| / 2^{2^n}\), the fraction of all Boolean functions on \(n\) bits that lie in \(P\).

A family of properties \(P_n\) of \(n\)-bit Boolean functions is large with density \(\delta (n)\) if \(\mathrm{density}(P_n) \ge \delta (n)\); constructive if membership of a truth table of length \(N = 2^n\) is decidable in time polynomial in \(N\) (or by circuits of size polynomial in \(N\)); and useful against \(\mathsf{SIZE}(s)\) if, for all sufficiently large \(n\), no function in \(P_n\) has circuits of size \(s(n)\). The quantifier over lengths and the scale of constructivity are part of the definition.

\(f : \mathbb {N} \to \mathbb {R}\) is negligible if for every \(c \in \mathbb {N}\) there is \(N {\gt} 0\) with \(|f(n)| {\lt} 1 / n^c\) for all \(n \ge N\).

Fix an oracle \(O\) and an oracle TM \(M\); all runs are relative to \(O\), and every step, local or lookup, counts toward a budget. \(M\) accepts \(x\) (within \(t\) steps) if the run on \(x\) reaches the halt state (after at most \(t\) steps) with output cell \(1\) equal to \(1\). \(M\) decides \(L\) in time \(T : \mathbb {N} \to \mathbb {N}\) if on every input \(x\) it reaches the halt state within \(T(|x|)\) steps, with output cell \(1\) equal to \(1\) if \(x \in L\) and equal to \(0\) if \(x \notin L\). \(M\) halts on a program \(p\) within \(t\) steps if the run on \(p\) reaches the halt state after at most \(t\) steps, and produces \(y\) on \(p\) within \(t\) steps if moreover the halted output tape has output \(y\). \(M\) halts on \(p\) (produces \(y\) on \(p\)) if it does so within some finite budget. These have the same shape as the corresponding definitions for ordinary machines.

An oracle NTM has two local transition functions selected by a choice bit and the same query mechanism and cost as an oracle TM, with execution along a fixed choice sequence and existential acceptance within a time bound.

A Boolean oracle is a function \(O : \{ 0,1\} ^* \to \{ 0,1\} \); it decides a language \(A\) if \(O(w) = 1 \iff w \in A\) for every \(w\). An oracle TM with \(k\) work tapes has a finite state type with decidable equality, a start state and a halt state; the input, \(k\) work and output tapes of an ordinary TM plus a dedicated read-write query tape; a partial map sending each query state to a pair (yes-successor, no-successor); and a local transition that reads the symbols under all heads (the query head included), writes symbols of \(\Gamma _w\) on the query, work and output tapes, and moves every head, moving right every head that reads \(\triangleright \). The initial configuration on \(x\) is in the start state with \(x\) on the input tape and every other tape empty. One step relative to \(O\) is defined as follows. The halt state has no successor. In a non-halted query state the machine reads the query word, formed by the cells strictly between the left marker and the query head in left-to-right order (a cell reads \(1\) only if it holds \(1\); \(0\), blank and \(\triangleright \) read as \(0\)), and enters the yes-successor if \(O\) answers \(1\) on it and the no-successor otherwise. The lookup costs exactly one step and changes nothing but the state; in particular the query tape is not erased, and writing the query costs ordinary local steps. Every other non-halted state applies the local transition. The relation \(c \to _O^t c'\) holds when \(c'\) is reached from \(c\) in exactly \(t\) steps relative to \(O\).

An oracle machine \(U\) simulates an oracle machine \(M\) under a compiler \(c : \{ 0,1\} ^* \to \{ 0,1\} ^*\) if for every oracle \(O\) and program \(p\): \(U\) halts on \(c(p)\) relative to \(O\) if and only if \(M\) halts on \(p\) relative to \(O\), and for every \(y\), \(U\) produces \(y\) on \(c(p)\) relative to \(O\) if and only if \(M\) produces \(y\) on \(p\) relative to \(O\). \(U\) simulates \(M\) under \(c\) in time \(\tau : \{ 0,1\} ^* \times \mathbb {N} \to \mathbb {N}\) if for every oracle \(O\), whenever \(M\) produces \(y\) on \(p\) within \(t\) steps relative to \(O\), \(U\) produces \(y\) on \(c(p)\) within \(\tau (p, t)\) steps relative to \(O\); unlike the ordinary timed simulation, bounded halting alone is not required to transfer. \(U\) is universal if for every \(k\) and every oracle machine \(M\) with \(k\) work tapes there is a compiler \(c\), computable by an ordinary deterministic machine, such that \(U\) simulates \(M\) under \(c\). For a policy of admissible clocks, \(U\) is efficiently universal for the policy if moreover \(c\) has additive overhead (\(|c(p)| \le |p| + C\)) and \(U\) simulates \(M\) under \(c\) in some admissible clock \(\tau \); it is efficiently universal if this holds for the polynomial policy, which admits \(\tau \) when \(\tau (p, t) \le a (|p| + t + 1)^e\) for some constants \(a, e\). In every case the compiler, constant and clock depend on \(M\) but are chosen once for all oracles.

A keyed family \(f_k : \{ 0,1\} ^n \to \{ 0,1\} \) computable in polynomial time, and its security game against a nonuniform class of distinguishers with oracle access (or with the full truth table): the advantage in telling \(f_k\) for a random key from a uniformly random function, required to be negligible, or bounded by an explicit function of the distinguisher’s size.

For a language \(A\), \(\mathsf{P}^A\) is the class of languages decided in polynomial time by an oracle TM relative to an oracle deciding \(A\), and \(\mathsf{NP}^A\) is the nondeterministic analogue. Query length is charged through the time needed to write the query.

Every TM with \(k\) work tapes is an oracle TM with \(k\) work tapes, the same states, start and halt state, and no query states. Its local transition applies the source transition to the input, work and output tapes and keeps the query tape inert: it writes only blanks there, and moves the query head right when it reads \(\triangleright \) and leaves it in place otherwise. Erasing the query tape maps an oracle configuration to the ordinary configuration with the same state and input, work and output tapes.

A bit string of length \(n\) is a function \(\{ 0, \dots , n-1\} \to \{ 0,1\} \). Circuits consume bit strings of a fixed length; machines consume lists.

\(\mathsf{BPTIME}(T)\) is the set of languages \(L\) for which there are a machine \(N\) (with any number of work tapes) and \(f = O(T)\) such that every path halts within \(f(|x|)\) steps, \(\mathrm{acceptProb}_N(x, f(|x|)) \ge 2/3\) for \(x \in L\), and \(\mathrm{acceptProb}_N(x, f(|x|)) \le 1/3\) for \(x \notin L\). \(\mathsf{BPP} = \bigcup _k \mathsf{BPTIME}(n^k)\).

A basis is a type of operations, each with an arity constraint (any fan-in, fan-in exactly \(k\), or fan-in at most \(k\)) and an evaluation map on bit strings of admissible length. A circuit over a basis \(B\) with \(N \ge 1\) inputs, \(M \ge 1\) outputs and \(G\) internal gates consists of \(G\) internal gates and \(M\) output gates. A gate applies an operation of \(B\) to a list of wires whose length the operation admits, and each gate input carries its own negation flag. The wires are the \(N\) inputs followed by the \(G\) internal gates. Internal gate \(i\) may read only wires \(0, \dots , N + i - 1\), so the circuit is acyclic by construction, and an output gate may read any wire. Evaluation \(C : \{ 0,1\} ^N \to \{ 0,1\} ^M\) gives each input wire its input bit and each gate the value of its operation on its input wires, each negated when its flag is set. The size of \(C\) is \(G + M\). The depth of an input wire is \(0\), the depth of a gate is one more than the largest depth of a wire it reads (\(1\) for a gate with no inputs), and the depth of \(C\) is the largest depth of an output gate.

The bases whose operations are AND and OR with fan-in exactly \(2\), with fan-in at most \(k\), and with any fan-in. In the last two a gate may have no inputs, and then computes the empty conjunction \(1\) or the empty disjunction \(0\). Negation is available only through the free per-input flags. Unless stated otherwise, a circuit is a circuit over the fan-in-two basis.

A width-\(w\) permutation branching program is a list of instructions \((i, \pi _0, \pi _1)\) with \(i \in \mathbb {N}\) and \(\pi _0, \pi _1 \in S_w\); the instruction reads variable \(i\). Under an assignment \(\alpha \), an instruction selects \(\pi _{\alpha (i)}\), and the program evaluates to the product \(\pi ^{(1)} \pi ^{(2)} \cdots \pi ^{(k)}\) of the selected permutations in \(S_w\), where \((\pi \tau )(y) = \pi (\tau (y))\). A program computes \(f\) through \(\sigma \) if, under every assignment \(\alpha \), it evaluates to \(\sigma \) when \(f(\alpha ) = 1\) and to the identity otherwise.

A fan-in-two single-output circuit is serialized as its gate count in terminated unary followed by its gates in index order, the output gate last. A gate is written as an operation bit, two negation flags, and two absolute wire references in terminated unary. The partial evaluator \(\mathrm{evalCode}(N, c, x)\) decodes \(c\), rejects inputs of the wrong length and codes that are malformed, have trailing bits, are empty, or reference a wire that is not yet computed, and evaluates the gates in order with a memo array. The code of a family at length \(0\) is the bit \(0\) followed by the stored answer; at length \(n \ge 1\) it is the bit \(1\) followed by the code of \(C_n\). The family evaluator runs a code \(c\) on a string \(x\) as follows: if \(x\) is empty, \(c\) must be \(0\, b\) for a bit \(b\), and the answer is \(b\); if \(x\) is nonempty, \(c\) must be \(1\, c'\), and the answer is \(\mathrm{evalCode}(|x|, c', x)\); every other case is rejected. The evaluation language is the set of strings \(\langle c, x \rangle \) (the library’s self-delimiting pairing) on which the family evaluator returns \(1\).

A circuit family over \(B\) consists of a single-output circuit \(C_n\) over \(B\) on \(n\) inputs, with any number of internal gates, for every \(n \ge 1\), together with an output bit for the empty input. It computes the Boolean function family given by \(C_n\) at length \(n \ge 1\) and by the stored bit at length \(0\), and it decides the language of strings on which it outputs \(1\). Its size at \(n \ge 1\) is the size of \(C_n\), and its size at \(0\) is \(0\). It has polynomial size if a single polynomial \(p \in \mathbb {N}[X]\) satisfies \(\mathrm{size}(n) \le p(n)\) for every \(n\).

A Boolean formula is a tree built from variables \(x_i\) (\(i \in \mathbb {N}\)), the two constants, negation, and binary conjunction and disjunction. It is evaluated under a total assignment \(\mathbb {N} \to \{ 0,1\} \). Its size is its number of nodes, its depth is the length of a longest root-to-leaf path, with each negation counted as one level, and its variables are the indices \(i\) of the variables \(x_i\) occurring in it.

\(\mathsf{FormulaNC1}\) is the class of Boolean function families computed by a family of formulas \((\varphi _n)\) in which \(\varphi _n\) reads only variables below \(n\), is evaluated on \(x \in \{ 0,1\} ^n\) under the assignment sending \(i {\lt} n\) to \(x_i\) (and every other index to \(0\)), and has depth at most \(c \lfloor \log _2 n \rfloor + c\) for a constant \(c\). \(\mathsf{Width5BP}\) is the class of Boolean function families decided by a family of width-\(5\) programs \(P_n\) for \(n \ge 1\), each reading only variables below \(n\) and with a designated point \(x_n\), together with an explicit answer at \(n = 0\); on \(x \in \{ 0,1\} ^n\) the output is \(1\) exactly when the value of \(P_n\) under the same assignment moves \(x_n\), and the length of \(P_n\) is at most \(C (n + 1)^k\) for constants \(C, k\).

A basis is complete if, for all \(N, M \ge 1\), every function \(\{ 0,1\} ^N \to \{ 0,1\} ^M\) is computed by some circuit over it; the fan-in-two AND/OR basis is complete. For \(N \ge 1\), \(f : \{ 0,1\} ^N \to \{ 0,1\} \) and a basis \(B\), \(\mathrm{size}_B(f)\) is the least size of a single-output circuit over \(B\) computing \(f\). The general version takes values in \(\mathbb {N} \cup \{ \infty \} \) and equals \(\infty \) exactly when no circuit over \(B\) computes \(f\). For a complete basis a natural-number-valued version is provided, and it agrees with the general one.

A threshold gate with cutoff \(t\) outputs \(1\) when at least \(t\) of its inputs are \(1\); the threshold basis has unweighted threshold gates of any fan-in, with the free negation flags on their inputs. \(\mathsf{TC}^i\) is defined like \(\mathsf{AC}^i\) over this basis.

A function \(f : \{ 0,1\} ^* \to \{ 0,1\} ^*\) is computable if some deterministic machine, with any number of work tapes, computes \(f\).

\(\mathsf{coNL}\) is the class of languages whose complements are in \(\mathsf{NL}\).

\(\mathsf{coNP} = \{ L : \overline{L} \in \mathsf{NP}\} \), where \(\overline{L}\) is the complement of \(L\) in the set of all bit strings. The library forms every complement class with the same constructor (Complexity.complClass).

A computable parser \(\mathrm{dec} : \{ 0,1\} ^* \to V\text{-structures} \cup \{ \bot \} \). It reads the unary size and then the fixed-length relation and constant blocks, and returns \(\bot \) on malformed input, including a size below \(2\) and a constant block that is not one-hot.

A dimension-\(k\) interpretation defines the target universe as a definable subset of \(\mathrm{dom}^k\). Each target relation of arity \(a\) is defined by a formula with \(a k\) free variables. This requires a codec \(\mathrm{Fin}(n^k) \simeq (\mathrm{Fin}(k) \to \mathrm{Fin}(n))\) and a way to assemble environments for the \(a k\) variables.

A decidable structure of size \(n\) is encoded, computably, as the concatenation of three blocks:

• the size in unary, \(1^n 0\);

• for each relation symbol in index order, its truth table, listed over a computable enumeration of all tuples of its arity;

• for each constant symbol in index order, a one-hot block of length \(n\) whose bit \(i\) is \(1\) exactly when the constant is \(i\).

The encoding depends on the canonical order of \(\mathrm{Fin}(n)\).

A formula is an FO matrix if it has no second-order quantifiers, though it may apply relation variables and use first-order quantifiers. It is in \(\exists \mathsf{SO}\) form if it is a possibly empty block of second-order existential quantifiers followed by an FO matrix.

\(Q\) is first-order definable if some sentence \(\varphi \) satisfies \(Q(\mathcal{A}) \iff \mathcal{A} \models \varphi \) for every \(\mathcal{A}\).

For queries \(Q_1\) over \(V\) and \(Q_2\) over \(W\), \(Q_1 \le _{\mathsf{FO}} Q_2\) if some dimension-1 interpretation \(I : V \to W\) has \(Q_1(\mathcal{A}) \iff Q_2(I(\mathcal{A}))\) for all \(V\)-structures \(\mathcal{A}\). An interpretation is quantifier-free if every defining formula has quantifier rank \(0\). \(Q_1\) first-order projection reduces to \(Q_2\) if such an \(I\) can be chosen quantifier-free. This condition is coarser than Immerman’s projective form, in which each target bit depends on a single source bit.

An environment for \(k\) free variables is a map \(\mathrm{Fin}(k) \to \mathrm{Fin}(|\mathcal{A}|)\). Extending it by an element puts that element at index \(0\) and shifts the others. Satisfaction \(\mathcal{A}, \sigma \models \varphi \) is Tarskian, and quantifiers range over \(\mathrm{Fin}(|\mathcal{A}|)\). \(\mathcal{A} \models \varphi \) means satisfaction of a sentence under the empty environment.

Terms with \(k\) free variables are de Bruijn variables \(x_i\) (\(i {\lt} k\)) or constant symbols. Formulas are built from relation atoms, equality, \(\neg \), \(\wedge \), \(\vee \), \(\exists \), and \(\forall \). A quantifier binds variable \(0\) and shifts the others. Sentences are formulas with no free variables. Quantifier rank (the quantifier nesting depth) and size (the number of nodes) are defined by structural recursion.

A dimension-1 interpretation \(I : V \to W\) consists of a \(V\)-formula with \(\mathrm{ar}(R)\) free variables for each relation symbol \(R\) of \(W\), and a source constant for each constant of \(W\). Applying \(I\) to a \(V\)-structure gives a \(W\)-structure on the same universe, in which \(R\) holds exactly where its defining formula does. Formulas translate backwards along \(I\), from \(W\) to \(V\): a target atom becomes its defining formula with the translated argument terms substituted, and a target constant becomes its source constant. Interpretations \(U \to V\) and \(V \to W\) compose to one \(U \to W\) by translating the outer defining formulas. The identity interpretation defines each relation by its own atom and sends each constant to itself.

An isomorphism \(\mathcal{A} \cong \mathcal{B}\) is a pair of mutually inverse maps between the universes whose forward map preserves and reflects every relation and preserves constants. Isomorphisms have identities, inverses, and composites. An embedding is an injective map that preserves and reflects every relation and preserves constants, as in model theory; its image is a substructure of \(\mathcal{B}\) isomorphic to \(\mathcal{A}\). Embeddings have identities and composites, and every isomorphism is one. An injective homomorphism only preserves relations, so \(\mathcal{B}\) may relate images of unrelated elements; every embedding is one. All three notions carry their maps as data.

\(\mathsf{FO}(\mathrm{LFP})\) extends first-order logic with \([\mathrm{lfp}_{R,\bar x}\, \varphi ](\bar t)\) for \(\varphi \) positive in \(R\). It is interpreted as the least fixed point of the monotone operator that \(\varphi \) induces on relations of the arity of \(R\). That fixed point is reached after at most \(n^{\mathrm{ar}(R)}\) iterations.

A computable \(\mathrm{Bool}\)-valued evaluator for first-order formulas on decidable structures. Atoms look up the \(\mathrm{Bool}\)-valued relations, and quantifiers become any and all over the list of universe elements. The sentence form runs it under the empty environment.

First-order logic extended with atoms for the canonical order \(\le \), successor, minimum, and maximum of \(\mathrm{Fin}(n)\). These atoms are interpreted by the existing meta-level helpers. The existing unordered syntax and its unrestricted invariance theorem stay unchanged. Ordered sentences are preserved only by maps that respect the canonical order, and they need not define order-independent queries.

A Boolean query over \(V\) is a property of finite \(V\)-structures. It is order-independent if isomorphic structures agree on it, that is, if it is invariant under isomorphism. Complement, intersection, and union are defined pointwise.

The language of \(Q\) is \(\{ \mathrm{enc}(\mathcal{A}) : \mathcal{A} \text{ decidable}, Q(\mathcal{A})\} \), where \(Q\) is applied to the structure that \(\mathcal{A}\) coerces to. By definition every string in it is an encoding, and the encoding of a decidable structure satisfying \(Q\) lies in it. This is the bridge from queries to the machine-model languages.

\(Q\) is second-order definable if some second-order sentence \(\varphi \) satisfies \(Q(\mathcal{A}) \iff \mathcal{A} \models \varphi \) for every \(\mathcal{A}\).

A relation environment assigns to each relation variable in the context a \(\mathrm{Prop}\)-valued relation of its arity on the universe. Extending it puts the new relation at index \(0\). Satisfaction is defined under an element environment and a relation environment, and second-order quantifiers range over all \(\mathrm{Prop}\)-valued relations of the quantified arity on the universe. \(\mathcal{A} \models \varphi \) for a second-order sentence means satisfaction under the empty environments.

Second-order formulas extend first-order formulas with two constructs: applications of relation variables, and second-order quantifiers \(\exists R\), \(\forall R\) over a fresh relation of a given arity. Relation variables are de Bruijn-indexed by a context listing their arities, innermost first. A second-order sentence has an empty relation context and no free element variables. First-order formulas embed into second-order formulas over any relation context. Size counts nodes.

A finite structure \(\mathcal{A}\) over \(V\) consists of:

• a size \(n \ge 2\) and the universe \(\mathrm{Fin}(n)\);

• for each relation symbol of arity \(k\), a \(\mathrm{Prop}\)-valued relation on \(k\)-tuples, that is, on maps \(\mathrm{Fin}(k) \to \mathrm{Fin}(n)\);

• for each constant symbol, an element.

A decidable structure has the same data, with \(\mathrm{Bool}\)-valued relations, and coerces to a structure in which a relation holds where its value is \(\mathrm{true}\). The canonical order \(\le \), the successor relation (\(b = a + 1\)), the minimum \(0\), and the maximum \(n - 1\) of \(\mathrm{Fin}(n)\) are defined for every structure as meta-level helpers. They are not part of the structure, and no formula can mention them.

Simultaneous substitution \(\varphi [\rho ]\) takes a formula with \(m\) free variables and terms \(\rho (0), \dots , \rho (m-1)\) with \(n\) free variables, and replaces each \(x_k\) by \(\rho (k)\), giving a formula with \(n\) free variables. Under a binder, the substitution is lifted: variable \(0\) stays, and every other image is shifted up one de Bruijn index.

A vocabulary has \(r\) relation symbols, indexed by \(\mathrm{Fin}(r)\), each with an arity in \(\mathbb {N}\), and \(c\) constant symbols, indexed by \(\mathrm{Fin}(c)\). It is relational if \(c = 0\). The graph vocabulary has one binary relation symbol and no constants.

\(\mathsf{DSPACE}(S)\) is the class of languages decided by some DTM, with any number of work tapes, in space \(f\) for some \(f = O(S)\).

For \(T \colon \mathbb {N} \to \mathbb {N}\), \(\mathsf{DTIME}(T)\) is the set of languages \(L\) for which there are a deterministic machine with some number \(k\) of work tapes and a function \(f\) with \(f = O(T)\) such that the machine decides \(L\) within time \(f\): on every input \(x\) it halts within \(f(|x|)\) steps with \(1\) in output cell \(1\) (the first cell after \(\triangleright \)) if \(x \in L\) and \(0\) there otherwise. Here \(f = O(T)\) means that \(f(n) \le C \cdot T(n)\) for some real constant \(C\) and all sufficiently large \(n\).

An \(n \times n\) Boolean matrix (the adjacency matrix of a directed graph on \(n\) vertices) corresponds bijectively to a bit string in \(\{ 0,1\} ^{n \cdot n}\) by row-major serialization, entry \((i, j)\) at position \(n i + j\). In particular there are exactly \(2^{n \cdot n}\) such matrices. No module of the library uses this codec yet.

\(\mathrm{bin}(v)\) is the minimal binary expansion of \(v \in \mathbb {N}\), least significant bit first, with \(\mathrm{bin}(0)\) empty. The decoder accepts a string only if it is the minimal expansion of its value, so representations with trailing high zeros are rejected. The code is not prefix-free; an enclosing framing layer fixes the field boundary.

\(\mathrm{toList}(x) = [x_0, \dots , x_{n-1}]\) serializes in increasing index order; \(\mathrm{ofList}\) reads a list whose length is proved to be \(n\); and \(\mathrm{toTotal}(x) : \mathbb {N} \to \{ 0,1\} \) extends \(x\) by \(0\) outside its range. The variable-length correspondence \(\{ 0,1\} ^* \simeq \Sigma _n \{ 0,1\} ^n\) is Mathlib’s.

\(\{ 0,1\} ^{a+b} \simeq \{ 0,1\} ^a \times \{ 0,1\} ^b\) splits a string into its length-\(a\) prefix and length-\(b\) suffix, with concatenation as the inverse, and \(\{ 0,1\} ^{kT} \simeq (\{ 0,1\} ^T)^k\) splits it into \(k\) blocks in row-major order: block \(i\) is positions \(iT, \dots , iT + T - 1\). For an event \(E \subseteq \{ 0,1\} ^T\) and \(w \in \{ 0,1\} ^{kT}\), \(\# _E(w)\) is the number of blocks of \(w\) lying in \(E\).

A raw circuit is a list of gates, each an AND or OR of two absolute wire indices with a negation flag on each input. At arity \(N\), wires \(0, \dots , N-1\) are the inputs and gate \(i\) produces wire \(N + i\); the raw circuit is well formed if it is nonempty and gate \(i\) reads only wires below \(N + i\). A raw circuit is encoded as its gate count in terminated unary (\(m\) ones, then a zero) followed by its gates, each gate as an operation bit (\(1\) for AND), two negation bits, and its two input wire indices in terminated unary. The code \(\mathrm{code}(C)\) of a single-output circuit \(C\) over the fan-in-two AND/OR basis is the encoding of the raw circuit formed by its internal gates in order followed by its output gate. The raw evaluator computes the wires in order in a memo array and returns the last gate’s value, failing on an empty gate list or on a reference to a wire not yet computed. \(\mathrm{evalCode}(N, w, x)\) fails unless \(|x| = N\); otherwise it decodes \(w\) exactly (rejecting malformed codes and trailing bits) and runs the raw evaluator on \(x\).

A binary codec for a type \(\alpha \) with a size measure \(\| \cdot \| \) consists of an encoder \(e : \alpha \to \{ 0,1\} ^*\), a partial decoder \(d : \{ 0,1\} ^* \to \alpha \cup \{ \bot \} \), the round trip \(d(e(a)) = a\), canonicity (\(d(w) = a\) implies \(w = e(a)\)), and an explicit size bound \(|e(a)| \le s(\| a\| )\). The existing rose-tree encodings (Definition 60) give injectivity only, with no decoder at the level of \(\alpha \) and no size bound.

From codecs for \(\alpha \) and \(\beta \), the product codec encodes \((a, b)\) as \(\langle e_\alpha (a), e_\beta (b) \rangle \), with \(|e(a, b)| = 2|e_\alpha (a)| + 2 + |e_\beta (b)|\), and the tagged-sum codec prefixes one tag bit. Both satisfy the codec laws.

A rose tree is a finite list of rose trees; the size of a node with children \(d_1, \dots , d_m\) is \(2 + \sum _i \mathrm{size}(d_i)\). A tree is serialized as balanced brackets: \(0\) opens a node, its children follow in order, and \(1\) closes it. A stack-based parser \(\mathrm{fromBits}\) returns a tree or fails. A type with an injective map into rose trees (instances exist for rose trees themselves, Booleans, natural numbers, lists, options, and products) gets a bit-string encoding by composing with this serialization. This layer supports the rose-tree machine model.

The block of \(x = x_1 \cdots x_n\) is \(\mathrm{delimit}(x) = x_1 x_1\, x_2 x_2 \cdots x_n x_n\, 0 1\): every bit is doubled and the separator \(01\) ends the block. The parser \(\mathrm{unpair?}\) reads one block off the front of a string and returns the payload and the remaining suffix, or fails on malformed input; \(\mathrm{undelimitBlocks}\) parses a string that consists entirely of blocks into the list of their payloads, or fails. The total helpers used by machines are: \(\mathrm{undelimitBlock}\), the payload of the leading block (empty on malformed input); \(\mathrm{takeFirstBlock}\), the leading block itself, framing included (empty on malformed input); \(\mathrm{hasBlock}\), whether the string begins with a well-formed block; and \(\mathrm{tagBlock}(z)\), which is \(1z\) if \(\mathrm{hasBlock}(z)\) and the empty string otherwise.

For a finite event \(E \subseteq \{ 0,1\} ^T\), \(\Pr [E] = |E| / 2^T \in \mathbb {Q}\).

From a codec for \(\alpha \), a codec for lists over \(\alpha \) that frames each element as a block, with \(|e([a_1, \dots , a_m])| = \sum _i (2|e(a_i)| + 2)\).

Canonical codecs, with explicit length bounds, for finite functions (truth tables), machine states, configurations of time-bounded runs, and bounded interaction transcripts. (Internal fixed-width layouts of machine states and of bounded configuration windows, Complexity.qCodec and Complexity.codeCodec, have exact widths but total, non-canonical decoders.)

For \(f \in \{ 0,1\} ^k\), \(\mathrm{maj}(f) = 1\) if and only if more than \(k/2\) positions of \(f\) are \(1\) (strict majority). For \(w \in \{ 0,1\} ^{kT}\), \(\mathrm{maj}_E(w) = 1\) if and only if \(2\, \# _E(w) {\gt} k\).

\(\pi _1\) reads doubled bits until the separator (returning the bits read so far on malformed input), and \(\pi _2\) returns the suffix after the first block, or the empty string if there is no valid block. Both are total.

For a machine \(N\) with \(n\) work tapes, \(\mathrm{rep}(N, k, T)\) has \(k(n+1)\) work tapes and performs \(k\) sequential runs of \(N\) for exactly \(T\) steps each, each run on a fresh bank of \(n + 1\) work tapes (the last simulating the output tape). Two setup transitions precede the first run. After each run it rewinds the input tape and the run’s bank in exactly \(T + 1\) transitions and records the run’s verdict in one more; after the last run it writes the strict majority of the \(k\) verdicts to its output tape (so for \(k = 0\) it writes \(0\)). Every run occupies exactly \(2T + 2\) transitions whether or not \(N\) halts early, so the total time is \(2 + k(2T + 2)\), and simulated step \(t\) of run \(j\) uses the choice bit at the fixed position \(2 + j(2T + 2) + t\). The compact seed of a choice sequence is the \(kT\) bits at those positions, and the accepting event of \(N\) on \(x\) is the set of \(r \in \{ 0,1\} ^T\) along which \(N\) on \(x\) halts with output cell \(1\) equal to \(1\).

\(\mathsf{ZPP}_{\mathrm{LV}}\) is the class of languages \(L\) with a probabilistic machine \(N\) and a polynomial \(T\) such that every trace on every input \(x\) halts within \(T(|x|)\) steps with output either the correct verdict \([x \in L]\) or a designated “don’t know” answer, and the probability of “don’t know” is at most \(1/2\). (The textbook expected-polynomial-time formulation needs an expected-time machine semantics, which the library does not have.)

\(\mathsf{EXP} = \bigcup _{k} \mathsf{DTIME}(2^{n^k})\) and \(\mathsf{NEXP} = \bigcup _{k} \mathsf{NTIME}(2^{n^k})\).

\(\mathsf{FL}\) is the class of functions \(\{ 0,1\} ^* \to \{ 0,1\} ^*\) computed by a DTM in space \(S\) for some \(S = O(\log n)\). The output is unbounded in length and one-way. \(\mathsf{FNL}\) is the class of polynomially balanced relations whose pair language is in \(\mathsf{L}\), and \(\mathsf{TFNL}\) consists of the relations in \(\mathsf{FNL}\) that are total: every \(x\) has some \(y\) with \(R(x, y)\).

\(\mathsf{FNP}\) is the set of polynomially balanced relations \(R\) with \(\mathrm{pairLang}(R) \in \mathsf{P}\). \(\mathsf{TFNP}\) is the set of \(R \in \mathsf{FNP}\) such that every \(x\) has some \(y\) with \(R(x, y)\).

\(\mathsf{FP}\) is the set of functions \(f \colon \{ 0,1\} ^* \to \{ 0,1\} ^*\) for which some deterministic machine computes \(f\) within time \(T\) with \(T = O(n^d)\) for some \(d\): on every input \(x\) it halts within \(T(|x|)\) steps with \(f(x)\) written on the output tape, that is, output cells \(1, \ldots , |f(x)|\) hold the bits of \(f(x)\) and cell \(|f(x)| + 1\) is blank.

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.

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.

\(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.

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))}\).

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.

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.

Map a QBF to an expression over \(\mathbb {F}\): \(\neg a \mapsto 1 - a\), \(a \wedge b \mapsto ab\), \(\forall x\, \varphi \mapsto \varphi |_{x=0} \cdot \varphi |_{x=1}\), \(\exists x\, \varphi \mapsto 1 - (1 - \varphi |_{x=0})(1 - \varphi |_{x=1})\), interleaved with linearization operators \(L_{x}\, p = (1 - x)\, p|_{x=0} + x\, p|_{x=1}\) that keep every intermediate polynomial of individual degree at most \(2\).

A constraint graph over an alphabet \(\Sigma \) has vertices \(\{ 0, \dots , V - 1\} \) and finitely many indexed directed edges (parallel edges and self-loops allowed), each carrying a Boolean-valued binary constraint on the labels of its tail and head. It is satisfiable if some labelling of the vertices satisfies every edge. For finite nonempty \(\Sigma \), its unsatisfiability value is the least, over all labellings, of the fraction of edges left unsatisfied (taken to be \(0\) for an edgeless graph); it is \(0\) exactly when the graph is satisfiable.

A function \(r\) is constructible if \(x \mapsto 1^{r(|x|)}\) is in \(\mathsf{FP}\).

For \(0 \le s {\lt} c \le 1\) and fixed arity and alphabet, \(\mathrm{Gap}_{c,s}\)-CSP is the promise problem whose yes-instances are encoded constraint systems with value at least \(c\) and whose no-instances have value less than \(s\). \(\mathrm{Gap}\)-MAX-3SAT\(_{1,s}\) separates satisfiable 3CNFs from those in which every assignment satisfies fewer than an \(s\) fraction of the clauses.

\(\mathsf{IP}(c, s)\), \(\mathsf{MA}(c, s)\) and \(\mathsf{AM}(c, s)\): the classes with completeness \(c\) and soundness \(s\) as parameters, together with monotonicity in both thresholds and the identification of the hard-wired classes with \(c = 2/3\), \(s = 1/3\).

A label-cover instance is a bipartite constraint graph with label sets \(\Sigma _A\), \(\Sigma _B\) whose constraints are projections \(\pi _e : \Sigma _A \to \Sigma _B\); its value is the largest fraction of edges satisfied by a labelling.

For \(f : \{ 0,1\} ^m \to \mathbb {F}\), the multilinear extension \(\widetilde{f}(x) = \sum _{b \in \{ 0,1\} ^m} f(b) \prod _i (b_i x_i + (1 - b_i)(1 - x_i))\), with the facts that it agrees with \(f\) on the cube and is the unique multilinear polynomial doing so.

A PCP verifier is non-adaptive: it has a list of proof positions (natural numbers) for each input \(x\) and coin string \(r\), together with an \(\mathsf{FP}\) function mapping \(\mathrm{pair}(x, r)\) to the rose-tree serialization of that list, and a verdict language in \(\mathsf{P}\) that decides \(\mathrm{pair}(\mathrm{pair}(x, r), a)\), where \(a\) lists the bits of the proof (a finite bit string) found at those positions. A position past the end of the proof reads as \(0\). The verifier is query-bounded by \(q\) if it reads at most \(q(|x|)\) positions for every \(x\) and every coin string \(r\).

A transcript is a list of messages (bit strings); the verifier speaks at even positions and the prover at odd ones. A prover strategy is an arbitrary function from the visible transcript to the next message; it never sees the verifier’s coins, and it is bounded by \(m\) if the message it returns on every transcript has length at most \(m\). A protocol consists of a round count, a coin count \(c\) and a message-length bound (functions of the input length), a next-message function in \(\mathsf{FP}\) applied to the encoded view \(\mathrm{pair}(\mathrm{pair}(x, r), \langle \tau \rangle )\) of the input \(x\), the private coins \(r\) and the transcript \(\tau \) (where \(\langle \tau \rangle \) is the rose-tree serialization of \(\tau \)), a proof that for every \(x\), \(r\) and \(\tau \) the verifier’s message has length at most the message bound at \(|x|\), and a verdict language in \(\mathsf{P}\). Each round appends the verifier’s message, computed from the current view, and then the prover’s reply to the transcript extended by that message. The verifier accepts if the view of the transcript after the round count at \(|x|\) many rounds lies in the verdict language, and the accept event is the set of coin strings \(r \in \{ 0,1\} ^{c(|x|)}\) on which it accepts.

For a polynomial \(g\) in \(m\) variables over \(\mathbb {F}\) with individual degree at most \(d\), given by an evaluation oracle, and a claimed value \(v\) of \(\sum _{b \in \{ 0,1\} ^m} g(b)\): in round \(i\) the prover sends a univariate polynomial \(h_i\) of degree at most \(d\), the verifier checks \(h_i(0) + h_i(1)\) against the current claim, and replaces the claim by \(h_i(r_i)\) for a random \(r_i \in \mathbb {F}\); at the end it checks \(g(r_1, \dots , r_m)\) against the last claim.

\(L \in \mathsf{IP}\) if some protocol whose round count, coin count \(c\) and message bound \(m\) are given by polynomials with natural-number coefficients satisfies: for \(x \in L\) some strategy bounded by \(m(|x|)\) is accepted with probability at least \(2/3\), and for \(x \notin L\) every strategy bounded by \(m(|x|)\) is accepted with probability at most \(1/3\), the probability being over uniform \(r \in \{ 0,1\} ^{c(|x|)}\). The counts are required to be polynomials, not merely polynomially bounded, so that the verifier can compute them.

For a deterministic machine \(U\) (with any number of work tapes), a string \(x\) and a clock \(t\),

with values in \(\mathbb {N} \cup \{ \infty \} \) and value \(\infty \) when no program exists. Here “produces” means halting with exact output \(x\) (Definition 11), and “within \(t\) steps” means halting after at most \(t\) transitions. No universality is assumed. A prefix-free variant \(K_U\) is defined only for machines bundled with a proof that their halting domain is prefix-free (TM.PrefixFreeMachine); it is the plain minimum \(C_U\) of the certified machine.

\(\mathsf{L}\) is the class of languages decided by a deterministic transducer, with any number of work tapes, in space \(f\) for some \(f = O(\log n)\).

A language is a set of finite binary strings, \(L \subseteq \{ 0,1\} ^*\).

A negation-normal unbounded formula over \(N\) variables is a tree built from constants, literals, and AND and OR gates of any fan-in; an empty AND is true and an empty OR is false. Its size counts all nodes (constants, literal occurrences, and gates), and its depth counts gates on a longest root-to-leaf path.

Fix a signature and an interpretation of it. The conditional complexity of a target \(f\), possibly with several outputs, given supplied functions \(g_1, \ldots , g_k\) of the same input is the minimum number of gates, every gate counted, of a circuit \(h\) with \(h(x, g(x)) = f(x)\) for every \(x\): the original inputs and the supplied values are free extra inputs, and nothing is required of \(h(x, y)\) when \(y \ne g(x)\). It is \(\infty \) when no circuit computes \(f\) this way.

Let \(D(f)\) and \(L(f)\) be the minimum depth and the minimum number of leaves, constant leaves included, of a De Morgan formula of Theorem 301 computing \(f\); they are defined for every number of inputs, \(0\) included. For \(f\) on \(m\) bits and \(g\) on \(n\) bits, the block composition \(f \diamond g\) applies \(f\) to the values of \(g\) on \(m\) disjoint blocks of \(n\) bits. Substituting formulas gives \(D(f \diamond g) \le D(f) + D(g)\) and \(L(f \diamond g) \le L(f)\, L(g)\) for all \(f\) and \(g\); both bounds are proved.

The Karchmer–Raz–Wigderson conjecture says these bounds are nearly tight. It is formalized in its strong form, with a constant slack. The depth form says that there is a constant \(c\) such that \(D(f) + D(g) \le D(f \diamond g) + c\) for all \(m\), \(n\) and all non-constant \(f\) and \(g\). The size form says that there is a constant \(c\) such that \(L(f)\, L(g) \le c \cdot L(f \diamond g)\) for all such \(f\) and \(g\). The constant does not depend on \(m\), \(n\), \(f\) or \(g\); forms whose slack grows with \(m\) or \(n\) are not formalized. The conjecture is open; it is formalized as a statement only.

Both non-constancy hypotheses are needed. If \(f\) or \(g\) is constant, so is \(f \diamond g\), and it is proved that dropping either hypothesis makes the depth form and the size form false for every \(c\).

A decision tree queries a variable at each internal node and outputs a bit at each leaf. The finite-arity version queries only variables below \(N\). Its depth is the length of a longest root-to-leaf path.

Input \(i\) is essential for \(f : \{ 0,1\} ^N \to \{ 0,1\} ^M\) if flipping bit \(i\) changes \(f(x)\) for some \(x\).

A protocol is a tree indexed by a rectangle \(X \times Y\) of sets of inputs in \(\{ 0,1\} ^N\), \(X\) on the one side and \(Y\) on the zero side. At an internal node, Alice splits \(X\) or Bob splits \(Y\) by an arbitrary predicate, and the two children are indexed by the two parts. A leaf names a coordinate \(i\) with \(x_i = 1\) for all \(x \in X\) and \(y_i = 0\) for all \(y \in Y\). A protocol for the monotone Karchmer–Wigderson game of \(f : \{ 0,1\} ^N \to \{ 0,1\} \) is one indexed by the root rectangle \(f^{-1}(1) \times f^{-1}(0)\), so every node’s rectangle lies in it. The depth is the height of the tree.

A monotone circuit is an AND/OR circuit all of whose negation flags are false. Every monotone circuit computes a monotone function.

A monotone formula over \(N\) variables is a tree built from variables \(x_0, \dots , x_{N-1}\) and binary conjunction and disjunction, without constants or negation. Its leaves are its variable occurrences, and its depth is the length of a longest root-to-leaf path, variables having depth zero. A function \(f\) is monotone if \(x \le y\) pointwise and \(f(x) = 1\) imply \(f(y) = 1\).

A CNF (resp. DNF) over \(N\) variables is a list of clauses (resp. terms), each a list of literals. Its width is the largest number of literals in a clause (term), and its complexity is the number of clauses (terms). These finite-arity normal forms are distinct from the CNF formulas used for satisfiability and resolution.

The parity family \(\oplus \) maps \(x \in \{ 0,1\} ^N\) to \(x_0 \oplus \cdots \oplus x_{N-1}\), with value \(0\) on the empty string.

A propositional proof system for unsatisfiable CNFs is a polynomial-time decidable relation \(V(\varphi , \pi )\) that is sound (\(V(\varphi , \pi )\) implies that \(\varphi \) is unsatisfiable) and complete (every unsatisfiable \(\varphi \) has some \(\pi \) with \(V(\varphi , \pi )\)). It is polynomially bounded if every unsatisfiable \(\varphi \) has such a \(\pi \) with \(|\pi | \le p(|\varphi |)\) for a fixed polynomial \(p\).

For \(q \in \mathbb {N}\), a seed assigns to each of \(N\) coordinates one of \(2q + 1\) symbols: one free symbol and \(q\) labelled copies of each fixed bit, so there are exactly \((2q + 1)^N\) seeds. A seed decodes to a finite-arity restriction, so a uniform seed leaves each coordinate free with probability \(1/(2q+1)\) and fixes it to each bit with probability \(q/(2q+1)\), independently. Events are measured by exact counts of seeds rather than by probabilities.

Clauses are lists of literals over variables in \(\mathbb {N}\), and a CNF is a list of clauses; an assignment is a finite list of bits, variables beyond its end reading \(0\). The resolvent of clauses \(C_1\) and \(C_2\) on a variable \(v\) deletes every occurrence of \(x_v\) from \(C_1\) and of \(\neg x_v\) from \(C_2\) and concatenates the rest. A clause is derivable from \(\varphi \) if it is a clause of \(\varphi \) or a resolvent of two derivable clauses. There is no weakening rule, and the pivot need not occur in the parents.

A resolution refutation of \(\varphi \) is a sequence of clauses ending in the empty clause, each a clause of \(\varphi \) or a resolvent of two earlier ones. Its size is its length and its width is the largest number of literals in one of its clauses. A clause is derivable exactly when it ends such a sequence.

A restriction assigns each variable \(x_i\), \(i \in \mathbb {N}\), either a fixed bit or “free”; the finite-arity version does this for exactly \(N\) variables. The composition \(\rho _1 \circ \rho _2\) fixes a variable to \(\rho _1\)’s value when \(\rho _1\) fixes it and to \(\rho _2\)’s value otherwise. A restriction acts on a total assignment by overwriting the fixed variables, and on a Boolean formula by replacing each fixed variable with the corresponding constant.

\(L \in \mathsf{MA}\) if there are a polynomial \(p\) with natural-number coefficients and \(V \in \mathsf{P}\) such that for \(x \in L\) some proof \(w\) with \(|w| \le p(|x|)\) makes \(\mathrm{pair}(\mathrm{pair}(x, w), r) \in V\) for at least \(2/3\) of the \(r \in \{ 0,1\} ^{p(|x|)}\), and for \(x \notin L\) every such proof does so for at most \(1/3\) of them. \(L \in \mathsf{AM}\) if the coins \(r\) come first and are public: the fraction of \(r \in \{ 0,1\} ^{p(|x|)}\) admitting some reply \(w\) with \(|w| \le p(|x|)\) and \(\mathrm{pair}(\mathrm{pair}(x, r), w) \in V\) is at least \(2/3\) for members and at most \(1/3\) for non-members.

For \(f \colon \{ 0,1\} ^n \to \{ 0,1\} \) with \(n {\gt} 0\) and a threshold \(s\), a finite list \(L \subseteq \{ 0,1\} ^n\) is an anti-checker for \((f, s)\) if every fan-in-two \(\{ \wedge ,\vee \} \) circuit with at most \(s\) gates disagrees with \(f\) on some input of \(L\).

Three promise formulations, all with yes side “minimum size at most the yes threshold” and no side “minimum size strictly above the no threshold”, and all placing malformed strings outside the promise: (a) canonical instances \((n, T, s)\) with yes threshold \(s\) and no threshold \(\rho (n, s)\) for a widening relaxation \(\rho (n, s) \ge s\); (b) slices \(\mathsf{GapMCSP}[s_{\mathrm{yes}}, s_{\mathrm{no}}]\) with arity-indexed thresholds \(s_{\mathrm{yes}}(n) \le s_{\mathrm{no}}(n)\) on canonical codes whose encoded threshold equals \(s_{\mathrm{yes}}(n)\); (c) the raw slice on bare truth tables of length exactly \(N = 2^n\), as in the magnification literature. Adding and erasing the canonical metadata are proved to be side-preserving maps between (b) and (c) in both directions (GapMCSP.rawSliceProblem_mapReducesVia_rawToCanonical, GapMCSP.sliceProblem_mapReducesVia_canonicalToRaw); that these maps are in \(\mathsf{FP}\) is not yet proved.

Parameters are a description loss \(\sigma (n, s)\) and a clock blow-up \(\tau (n, t)\); the promise problem takes a proof that they are widening (\(\sigma (n,s) \ge s\) and \(\tau (n,t) \ge t\) for all arguments), which makes its two sides disjoint. On canonical instances \((x, 1^t, 1^s)\), encoded as \(\mathrm{pair}(\mathrm{pair}(x, 1^t), 1^s)\), the promise \(\mathsf{GapMINKT}(U, \sigma , \tau )\) has yes side \(C^t_U(x) \le s\) and no side \(C^{\tau (|x|,t)}_U(x) {\gt} \sigma (|x|, s)\); malformed strings lie outside the promise. The exact logarithmic variant of Hirahara 2022 is Definition 493.

Hamming distance, balls \(B(r)\) and their binomial volume on \(\{ 0,1\} ^n\); a set of words is \(d\)-separated when distinct words are at distance at least \(d\). A block code is an injective encoding \(\{ 0,1\} ^k \to \{ 0,1\} ^m\), with rate \(k/m\), a \(\mathrm{GF}(2)\)-linearity predicate (preserving zero and XOR), and the minimum-distance contract “distinct messages have codewords at distance at least \(d\)”. The repetition code with \(c \ge 1\) copies is a concrete \(\mathrm{GF}(2)\)-linear instance: it multiplies Hamming distance by exactly \(c\), so it has minimum distance at least \(c\), and for \(k \ge 1\) its rate is exactly \(1/c\).

Levin’s \(\mathrm{Kt}_U(x) = \min \{ |p| + \lceil \log _2 t \rceil : U \text{ produces } x \text{ on } p \text{ within } t \text{ steps}\} \), and the random-access measure \(\mathrm{KT}_U(x) = \min \{ |d| + t\} \) over descriptions \(d\) from which an indexed-bit evaluator answers every query “what is bit \(i\) of \(x\)?” (including a fixed end-marker convention) within \(t\) steps. This requires an explicit random-access evaluator model and an efficient universal evaluator for it. The associated problems are \(\mathsf{MKtP}\) and \(\mathsf{MKTP}\) with a threshold, their search versions, and gap promise problems.

A list code with messages in \(\{ 0,1\} ^k\) encodes each message as a Boolean function on a finite coordinate set and decodes each received word to an indexed list of \(L\) candidate messages; it is list-decodable up to relative distance \(\rho \) if every message whose codeword disagrees with the received word on at most a \(\rho \) fraction of coordinates appears in the list. A family of list codes is indexed by message length \(k\) and inverse accuracy \(q\), with codeword coordinates in \(\{ 0,1\} ^{\ell (k,q)}\). It is list-decodable if each code is list-decodable up to relative distance \(1/2 - 1/q\) for \(q \ge 2\); it has polynomial parameters if \(2^{\ell (k,q)} \le a(k + q + 1)^e\) and the list size is at most \(b(q+1)^f\) for constants \(a, e, b, f\); and a uniform realization is one encoder machine, printing the full truth table of the codeword, and one decoder machine, reading the full truth table of any received word and printing all \(L\) candidates, that work for all \(k, q\) on canonically framed inputs within a common time bound \(a'(k + q + 1)^{e'}\).

Rational parameters are positive fractions \(a/b\) with \(a, b \ge 1\), and all roundings are explicit. For a positive rational \(\beta \) and an integer \(c \ge 1\), the raw problem at \((\beta , c)\) is the raw \(\mathsf{GapMCSP}\) slice with yes threshold \(\lfloor 2^{\lfloor \beta n \rfloor }/(cn) \rfloor \) and no threshold \(2^{\lfloor \beta n \rfloor }\) at arity \(n\). For a positive rational \(\varepsilon \), the size bound at input length \(N\) is \(2^{n + \lceil \varepsilon n \rceil }\) with \(n = \lfloor \log _2 N \rfloor \), which is the rounded \(N^{1+\varepsilon }\) at \(N = 2^n\). The hypothesis \(\mathrm{LB}(c)\) asserts: there is a positive rational \(\varepsilon \) such that for every sufficiently small positive rational \(\beta \) (that is, for all \(\beta \) at most some positive \(\beta _0\)), the raw problem at \((\beta , c)\) is not in \(\mathsf{PromiseEventuallySIZE}(N^{1+\varepsilon })\). The quantifier over small \(\beta \) is a filter at zero from above, kept separate from the eventual quantifier over input lengths.

An instance consists of an arity \(n\), a truth table \(T \in \{ 0,1\} ^{2^n}\) (entry \(k\) is the value on the input whose bit \(j\) is bit \(j\) of \(k\), a little-endian order) and a threshold \(s\), encoded canonically as \(\mathrm{pair}(\mathrm{bin}(n), \mathrm{pair}(\mathrm{bin}(s), T))\) with minimal binary naturals; strings that are not canonical codes (including tables of the wrong length) are no-instances. For \(n {\gt} 0\) the instance is a yes-instance iff some circuit of fan-in-two \(\{ \wedge ,\vee \} \) gates with free negation flags on gate inputs and at most \(s\) gates (input vertices free, the output gate counted) computes the function with truth table \(T\). Arity-zero instances are accepted at every threshold (the size-zero convention of circuit families).

Search-\(\mathsf{MCSP}\); linear-overhead transport of minimum size to other gate conventions; partial-function \(\mathsf{MCSP}\) (truth tables with don’t-care entries); formula, branching-program and oracle-circuit size versions; and implicit variants whose truth table is given by a circuit. Each keeps its qualifiers in its name, and results about a variant are never surfaced as statements about total \(\mathsf{MCSP}\), whose \(\mathsf{NP}\)-hardness is open.

Fix a machine \(U\) and a threshold \(r \colon \mathbb {N} \to \mathbb {N}\). An instance \((x, 1^t)\), with \(t \ge 0\) (the empty clock is \(t = 0\)), is encoded as \(\mathrm{pair}(x, 1^t)\), and \(\mathsf{MINKT}(U, r)\) is the language of canonical codes with the strict inequality \(C^t_U(x) {\lt} r(|x|)\). Malformed strings (a failed pairing or a clock containing a \(0\)) are no-instances.

A map \(f\) is side-preserving from \(\Pi \) to \(\Pi '\) when it sends \(\Pi _{\mathrm{yes}}\) into \(\Pi '_{\mathrm{yes}}\) and \(\Pi _{\mathrm{no}}\) into \(\Pi '_{\mathrm{no}}\); a polynomial-time promise reduction is a side-preserving map \(f \in \mathsf{FP}\). For a language class \(\mathcal{C}\), a promise problem is \(\mathcal{C}\)-hard when the total embedding of every language of \(\mathcal{C}\) reduces to it in this sense, and \(\mathcal{C}\)-complete when in addition it lies in \(\mathrm{Promise}\, \mathcal{C}\). Promise-\(\mathsf{NP}\)-hardness and promise-\(\mathsf{NP}\)-completeness are the case \(\mathcal{C} = \mathsf{NP}\).

\(\mathsf{PromiseSIZE}(s)\) and \(\mathsf{PromisePPoly}\) are the completion lifts of \(\mathsf{SIZE}(s)\) (fan-in-two \(\{ \wedge ,\vee \} \) gates with free negation flags on gate inputs) and \(\mathsf{P/poly}\). A circuit family has one circuit at each positive input length and a stored answer, of size \(0\), on the empty input. \(\mathsf{PromiseSIZE}(s)\) is equivalently the class of promise problems solved on both sides by one circuit family of pointwise size at most \(s\) (mem_PromiseSIZE_iff). \(\mathsf{PromiseEventuallySIZE}(s)\) asks for a family solving both sides whose size is at most \(s(n)\) for all sufficiently large \(n\). The library proves that an eventual polynomial bound already gives \(\mathsf{PromisePPoly}\) (PromiseEventuallySIZE_polynomial_subset_PromisePPoly).

An instance is an arity \(n\), a finite list of samples \((z_i, b_i) \in \{ 0,1\} ^n \times \{ 0,1\} \) (repetitions and contradictions allowed) and a threshold \(s\), with a canonical total codec. A canonical code is a yes-instance iff some fan-in-two \(\{ \wedge ,\vee \} \) circuit with at most \(s\) gates satisfies \(C(z_i) = b_i\) for every sample (for \(n = 0\): some constant is consistent with every sample, at every threshold). Malformed strings are no-instances.

For a machine \(N\), input \(x\), and clock \(T\), the acceptance probability is the rational number

and the probability of output \(y\) is defined the same way with the output condition in place of acceptance. Both are meaningful when every trace has halted by time \(T\).

A configuration of a machine with state set \(Q\) and \(k\) work tapes consists of a state, an input tape, \(k\) work tapes, and an output tape, each a named field. The initial configuration on input \(x\) is in the start state, with \(x\) written from cell \(1\) of the input tape, every other tape empty, and every head at cell \(0\).

\(g\) is clock-constructible if there are an eight-work-tape machine \(M\) and a constant \(C\) such that, for every input \(x\) and every starting layout in which the input tape holds \(x\) with its head at cell \(1\), every work head is at a cell \(\ge 1\) not reading \(\triangleright \), work tapes \(5\) and \(6\) are blank with their heads at cell \(1\), and the output head is at cell \(1\) with \(\triangleright \) at cell \(0\) and nowhere else, \(M\) started in its start state halts within \(C (g(|x|) + |x| + 1)\) steps with: work tape \(6\) holding the unary clock of length \(g(|x|)\) (cells \(1, \dots , g(|x|)\) equal to \(1\), the rest blank, head at cell \(1\)); every other work tape exactly as it started (so the scratch tape \(5\) is again blank); the input head back at cell \(1\); and the output head at cell \(1\) with \(\triangleright \) still at cell \(0\) and nowhere else. The layout is pinned to the diagonalizer that consumes it.

On machines with the same \(k\) work tapes: \(\mathrm{seq}(M_1, M_2)\) runs \(M_1\) to completion and then \(M_2\) on the same tapes; \(\mathrm{if}(M_t, M_1, M_0)\) runs the test \(M_t\), rewinds the output head, and runs \(M_1\) if output cell \(1\) holds \(1\) and \(M_0\) otherwise; \(\mathrm{loop}(M_b, M_t)\) alternates the body and the test, rewinding the output head after each test, and halts once the test leaves \(1\) in output cell \(1\); \(\mathrm{complement}(M)\) runs \(M\), rewinds the output head, and exchanges \(0\) and \(1\) in output cell \(1\) (a blank stays blank). In \(\mathrm{seq}\) (from \(M_1\) to \(M_2\)), in \(\mathrm{loop}\) (from the body to the test), and in \(\mathrm{if}\) (from the branch to the final halt state), the handover is a single step in which every head reading \(\triangleright \) moves one cell right, the other heads stay, and no tape cell changes except that a \(\triangleright \) outside cell \(0\) would be overwritten by a blank. After the test in \(\mathrm{if}\) and \(\mathrm{loop}\) the handover takes several steps: one such step; then steps that move the output head left one cell at a time until it reads \(\triangleright \), and then one cell right; and a last step that reads the output cell under the head (cell \(1\) when \(\triangleright \) appears on the output tape only at cell \(0\)) and enters the chosen branch, the body, or the halt state. In each of these steps every input or work head reading \(\triangleright \) moves one cell right and the others stay, and cells change only as in the single-step handover. The machine \(\mathrm{union}(M_1, M_2)\), with \(M_i\) on \(k_i\) work tapes, has \(k_1 + 1 + k_2\) work tapes: it runs \(M_1\) with its output redirected to work tape \(k_1\), halts with \(1\) in output cell \(1\) if cell \(1\) of that work tape holds \(1\), and otherwise rewinds the input and runs \(M_2\) on the last \(k_2\) work tapes and the real output tape.

For predicates \(\mathit{pre}, \mathit{post}\) on (input tape, work tapes, output tape) and a bound \(b \in \mathbb {N}\), the triple \(\{ \mathit{pre}\} \, M\, \{ \mathit{post}\} _b\) holds if \(M\), started in its start state on any tapes satisfying \(\mathit{pre}\), halts within \(b\) steps on tapes satisfying \(\mathit{post}\). The unbounded triple drops the step bound.

A program is a list of instructions over registers \(R_0, R_1, \dots \) holding natural numbers: immediate load, \(\mathrm{add}\), truncated \(\mathrm{sub}\), \(\mathrm{mul}\), indirect \(\mathrm{load}\) (\(R_d := R_{R_a}\)) and \(\mathrm{store}\) (\(R_{R_a} := R_s\)), conditional and unconditional jumps, and \(\mathrm{halt}\); a program counter past the end halts. On input \(x\), \(R_0 = |x|\), \(R_{i+1} = x_i\), and all other registers are \(0\). Each instruction costs \(1\) plus bit lengths of the values it touches: the constant of an immediate load; both operands and the result for \(\mathrm{add}\) and \(\mathrm{mul}\); both operands for \(\mathrm{sub}\) (whose result is no longer than its first operand); the runtime address and the value moved for indirect \(\mathrm{load}\) and \(\mathrm{store}\); the tested register for a conditional jump; nothing more for \(\mathrm{jmp}\) and \(\mathrm{halt}\). Register indices and jump targets written in the program are not charged. The logarithmic time of a run is the total cost of its non-halted steps, and its unit time is the number of those steps. Space is the peak, over the configurations visited, of the total bit length of the addresses and contents of the nonzero registers.

A program decides \(L\) in time \(T\) if on every input \(x\) it halts after logarithmic cost at most \(T(|x|)\) with \(R_0 = 1\) if \(x \in L\) and \(R_0 = 0\) otherwise; deciding in space \(S\) bounds peak space instead. Then \(\mathsf{DTIME}_{\mathrm{RAM}}(T)\) and \(\mathsf{DSPACE}_{\mathrm{RAM}}(S)\) are the languages decided in time \(O(T)\) and space \(O(S)\), and \(\mathsf{P}_{\mathrm{RAM}} = \bigcup _k \mathsf{DTIME}_{\mathrm{RAM}}(n^k)\).

\(U\) simulates \(M\) under \(c\) in time \(\tau : \{ 0,1\} ^* \times \mathbb {N} \to \mathbb {N}\) if whenever \(M\) halts on \(p\) (resp. produces \(y\) on \(p\)) within \(t\) steps, \(U\) halts on \(c(p)\) (resp. produces \(y\) on \(c(p)\)) within \(\tau (p, t)\) steps. The compiler has additive overhead \(C\) if \(|c(p)| \le |p| + C\) for all \(p\). The clock \(\tau \) is polynomial if \(\tau (p, t) \le a (|p| + t + 1)^e\) for some constants \(a, e\).

The read alphabet is \(\Gamma = \{ 0, 1, \sqcup , \triangleright \} \) and the write alphabet is \(\Gamma _w = \{ 0, 1, \sqcup \} \), so no transition can write the start symbol \(\triangleright \). A head moves left, right, or stays. A tape is a head position \(h \in \mathbb {N}\) together with contents \(\mathbb {N} \to \Gamma \); the type allows any symbol in any cell. Initial tapes have \(\triangleright \) in cell \(0\) and nowhere else, writing at cell \(0\) is a no-op, and moving left at cell \(0\) stays there, so every tape reachable from an initial configuration keeps this marker invariant (statements about arbitrary tapes assume it explicitly). A tape has output \(y \in \{ 0,1\} ^*\) when cells \(1, \dots , |y|\) hold the bits of \(y\) and cell \(|y| + 1\) is blank.

\(T : \mathbb {N} \to \mathbb {N}\) is time-constructible if \(T(n) \ge n\) for all \(n\) and some deterministic machine computes \(x \mapsto \mathrm{bin}(T(|x|))\) (least significant bit first) in time \(O(T(n))\) (Arora–Barak Definition 1.12). The formalized hierarchy theorem does not use this notion.

The universal machine \(\mathcal{U}\) has six work tapes and is \(\mathrm{seq}(\mathrm{init}, \mathrm{seq}(\mathrm{loop}(\mathrm{body}, \mathrm{haltTest}), \mathrm{extract}))\). On input \(\langle \alpha , x \rangle \) it parses the description \(\alpha \) of a one-work-tape machine, simulates one step per loop iteration, tests for the halt state, and finally copies the simulated output tape to its own output tape.

These are classes of Boolean function families, one function \(\{ 0,1\} ^n \to \{ 0,1\} \) for each \(n\) (including \(n = 0\)), not of languages. The depth of a circuit family at length \(n \ge 1\) is the depth of \(C_n\), and at length \(0\) it is \(0\). For \(d : \mathbb {N} \to \mathbb {N}\), \(\mathsf{DEPTH}(d)\) consists of the families computed by a fan-in-two AND/OR circuit family of depth at most \(d(n)\) at every length \(n\), with no size bound; the same definition is available over any basis. A family is in \(\mathsf{NC}^i\) if a fan-in-two AND/OR circuit family of polynomial size and depth at most \(c\, (\lfloor \log _2 n \rfloor + 1)^i\) at every length \(n\), for some constant \(c \in \mathbb {N}\) (with \(\lfloor \log _2 0 \rfloor = 0\)), computes it. \(\mathsf{AC}^i\) is defined the same way with unbounded fan-in. \(\mathsf{NC}^0\), \(\mathsf{NC}^1\) and \(\mathsf{AC}^0\) are the special cases. These classes are nonuniform.

\(\mathsf{NL}\) is the class of languages decided by a nondeterministic transducer, with any number of work tapes, in space \(f\) for some \(f = O(\log n)\).

\(\mathsf{NP} = \bigcup _{k} \mathsf{NTIME}(n^k)\). This is the machine definition; the certificate form is Theorem 126 (one direction, formalized) and Theorem 127 (the other, planned).

\(L\) is \(\mathsf{NP}\)-hard if \(L' \le _p L\) for every \(L' \in \mathsf{NP}\), and \(\mathsf{NP}\)-complete if moreover \(L \in \mathsf{NP}\).

\(\mathsf{NPSPACE} = \bigcup _{k} \mathsf{NSPACE}(n^k)\).

\(\mathsf{NSPACE}(S)\) is the class of languages decided by some NTM, with any number of work tapes, in space \(f\) for some \(f = O(S)\).

\(\mathsf{NTIME}(T)\) is the set of languages \(L\) for which some nondeterministic machine (two transition functions selected by a choice bit) and some \(f = O(T)\) satisfy: every computation path on input \(x\) halts within \(f(|x|)\) steps, and \(x \in L\) if and only if some choice sequence of length \(f(|x|)\) ends in the halting state with \(1\) in output cell \(1\). Rejecting paths are not required to write \(0\).

A nondeterministic Turing machine has the same data as a deterministic one except that it has two transition functions \(\delta _0, \delta _1\), each subject to the same rule at \(\triangleright \). Its execution is defined only through the trace: given a choice sequence \(r \in \{ 0,1\} ^T\), run \(T\) steps, using \(\delta _{r_i}\) at step \(i\), and stay put once the halt state is reached. The same structure serves as a probabilistic machine, with \(r\) read as random bits. A deterministic machine embeds by taking \(\delta _0 = \delta _1 = \delta \).

A nondeterministic machine \(N\) accepts \(x\) in time \(T\) if some choice sequence of length \(T\) leads to the halt state with output cell \(1\) equal to \(1\). It decides \(L\) in time \(T\) if every trace on every input \(x\) has halted after \(T(|x|)\) steps, and \(x \in L\) exactly when \(N\) accepts \(x\) in time \(T(|x|)\) (Arora–Barak Definition 2.1). Rejection is the absence of an accepting path; it does not require output \(0\).

\(\mathsf{P} = \bigcup _{k} \mathsf{DTIME}(n^k)\).

An advice function \(a : \mathbb {N} \to \{ 0,1\} ^*\) has polynomial length if \(|a(n)| \le p(n)\) for every \(n\) and a polynomial \(p \in \mathbb {N}[X]\). A deterministic machine \(M\) decides \(L\) with advice \(a\) in time \(T\) if on input \(\langle a(|x|), x \rangle \) (the library’s self-delimiting pairing) it halts within \(T(|x|)\) steps with \(1\) in the first output cell when \(x \in L\) and \(0\) otherwise. The time bound is measured in \(|x|\), not in the length of the paired input. \(\mathsf{PAdvice}\) is the class of languages decided, by a machine with any number of work tapes, with polynomial-length advice in time \(O(n^d)\) for some \(d\).

\(\langle x, y \rangle = \mathrm{delimit}(x)\, y\): the first component is framed as a block and the second is appended verbatim.

For a relation \(R \subseteq \{ 0,1\} ^* \times \{ 0,1\} ^*\), \(\mathrm{pairLang}(R) = \{ \langle x, y \rangle : R(x, y)\} \) using the library’s pairing codec. \(R\) is polynomially balanced if there is a polynomial \(p\) with \(R(x, y) \Rightarrow |y| \le p(|x|)\).

For arbitrary functions \(r, q : \mathbb {N} \to \mathbb {N}\), \(L \in \mathsf{PCP}(r, q)\) if some verifier query-bounded by \(q\), using exactly \(r(|x|)\) uniformly random coins, accepts some proof of each \(x \in L\) with probability \(1\), and accepts every proof of each \(x \notin L\) with probability at most \(1/2\).

For a polynomial \(p \in \mathbb {N}[X]\) and a language \(L'\), let \(\exists ^p L' = \{ x : \exists w\ (|w| \le p(|x|) \wedge \langle x, w \rangle \in L')\} \) and \(\forall ^p L' = \{ x : \forall w\ (|w| \le p(|x|) \Rightarrow \langle x, w \rangle \in L')\} \), where \(\langle \cdot , \cdot \rangle \) is the library’s pairing. For a class \(\mathcal{C}\), let \(\exists \mathcal{C}\) be the set of languages \(\exists ^p L'\) with \(p\) a polynomial and \(L' \in \mathcal{C}\), and similarly \(\forall \mathcal{C}\). Then \(\Sigma ^p_0 = \mathsf{P}\), \(\Pi ^p_k = \{ L : \overline{L} \in \Sigma ^p_k\} \), \(\Sigma ^p_{k+1} = \exists \Pi ^p_k\), and \(\mathsf{PH} = \bigcup _k \Sigma ^p_k\).

\(3\mathrm{SAT}\) is the set of encodings, in the \(\mathrm{SAT}\) codec, of satisfiable CNF formulas in which every clause has exactly three literals.

Bit strings are read least-significant bit first. Cobham’s algebra is the smallest class of functions \((\{ 0,1\} ^*)^n \to \{ 0,1\} ^*\), over all arities \(n\), that contains the projections, the empty-string constant, the bit successors \(x \mapsto b\, x\) (prepend \(b\)), and \(\mathrm{smash}(x, y) = 1^{|x| \cdot |y|}\), and is closed under composition and limited recursion on notation: if \(g, h_0, h_1, j\) are in the class and the function \(f\) defined by \(f(\varepsilon , v) = g(v)\) and \(f(b\, x, v) = h_b(x, f(x, v), v)\) satisfies \(|f(x, v)| \le |j(x, v)|\) for all \(x, v\), then \(f\) is in the class. The unary fragment is \(\mathsf{CobhamFP}\).

\(L\) is \(\mathsf{coNP}\)-hard if \(L' \le _p L\) for every \(L' \in \mathsf{coNP}\), and \(\mathsf{coNP}\)-complete if moreover \(L \in \mathsf{coNP}\).

Fix a codec for pairs \(\langle G, k \rangle \) of a finite simple graph (vertex count in unary and a row-major adjacency matrix) and a threshold \(k\) in unary, with malformed strings as no-instances. \(\mathrm{INDSET}\), \(\mathrm{CLIQUE}\), and \(\mathrm{VC}\) are the sets of \(\langle G, k \rangle \) such that \(G\) has an independent set of size at least \(k\), a clique of size at least \(k\), and a vertex cover of size at most \(k\), respectively.

A CNF formula is a list of clauses, a clause a list of literals, and a literal a sign with a variable index in \(\mathbb {N}\); an assignment is a bit string, with out-of-range variables read as false. Formulas are encoded as bit strings as follows: a literal is its sign bit followed by its variable index in unary, with every bit doubled; each literal is followed by the undoubled pair \(01\) and each clause by the undoubled pair \(10\). \(\mathrm{SAT}\) is the set of encodings of satisfiable formulas (so strings that encode no formula are excluded). The witness relation holds of \((z, \alpha )\) when \(z\) encodes some \(\varphi \), \(|\alpha | \le |z| + 1\), and \(\alpha \) satisfies \(\varphi \).

A function \(f\) from strings to natural numbers is polynomial-time if \(z \mapsto 1^{f(z)}\) is in \(\mathsf{FP}\), that is, if its value can be written in unary in polynomial time. A predicate \(p\) on strings is polynomial-time if there is a Boolean-valued \(g\) with \(z \mapsto [g(z)]\) in \(\mathsf{FP}\) and \(p(z) \iff g(z) = 1\) for all \(z\).

\(\mathsf{PPTIME}(T)\) is the set of languages \(L\) for which there are a machine \(N\) and \(f = O(T)\) such that every path halts within \(f(|x|)\) steps and \(x \in L \iff \mathrm{acceptProb}_N(x, f(|x|)) {\gt} 1/2\). \(\mathsf{PP} = \bigcup _k \mathsf{PPTIME}(n^k)\).

\(\mathsf{P/poly} = \bigcup _{p \in \mathbb {N}[X]} \mathsf{SIZE}(n \mapsto p(n))\).

A deterministic machine \(M\) halts on a program \(p\) (within time \(t\)) if the run from the initial configuration on \(p\) reaches the halt state (within \(t\) steps). It produces \(y\) on \(p\) (within time \(t\)) if moreover the output tape of the halted configuration has output \(y\). The bounded evaluator \(\mathrm{run}(c, t)\) is the configuration after \(t\) steps, standing still once halted.

A promise problem \(\Pi = (\Pi _{\mathrm{yes}}, \Pi _{\mathrm{no}})\) is a pair of disjoint languages; inputs outside \(\Pi _{\mathrm{yes}} \cup \Pi _{\mathrm{no}}\) are unconstrained. For a language class \(\mathcal{C}\), \(\Pi \) lies in the lifted class \(\mathrm{Promise}\, \mathcal{C}\) when some completion \(L \in \mathcal{C}\) satisfies \(\Pi _{\mathrm{yes}} \subseteq L\) and \(L \cap \Pi _{\mathrm{no}} = \emptyset \). \(\mathsf{PromiseP}\) and \(\mathsf{PromiseNP}\) (and \(\mathsf{PromiseCoNP}\)) are the lifts of \(\mathsf{P}\) and \(\mathsf{NP}\) (and \(\mathsf{coNP}\)). An ordinary language \(L\) embeds as the total promise problem \((L, \overline{L})\).

\(\mathsf{PSPACE} = \bigcup _{k} \mathsf{DSPACE}(n^k)\).

For naturals \(a\) and \(e\): \(e\) approximates \(a\) within factor \(F\) if \(e \le Fa\) and \(a \le Fe\); and \(e\) approximates \(a\) with relative error \(1/q\) if \(q {\gt} 0\) and \((q - 1)a \le qe \le (q + 1)a\), that is, \((1 - 1/q)a \le e \le (1 + 1/q)a\).

\(\mathsf{GapP}\) is the set of \(h \colon \{ 0,1\} ^* \to \mathbb {Z}\) of the form \(h = f - g\) with \(f, g \in \# \mathsf{P}\).

A pairwise-independent family from \(n\)-bit to \(m\)-bit strings with \(s\)-bit seeds is a map \(h \colon \{ 0,1\} ^s \times \{ 0,1\} ^n \to \{ 0,1\} ^m\) such that, over a uniform seed, \(\Pr [h(x) = y] = 2^{-m}\) for all \(x, y\), and \(\Pr [h(x) = y \wedge h(x') = y'] = 2^{-2m}\) for all \(x \neq x'\) and all \(y, y'\). The affine family \(x \mapsto Ax + b\) over \(\mathrm{GF}(2)\), whose seed lists the \(m\) rows \((a_i, b_i)\) of \(n + 1\) bits each, so \(s = m(n+1)\), is one. For \(S \subseteq \{ 0,1\} ^n\), a target \(y \in \{ 0,1\} ^m\) and a seed \(\sigma \), the cell is \(C_\sigma = \{ x \in S : h_\sigma (x) = y\} \); \(\mu \) and \(\mathrm{Var}\) denote the average and the variance of \(|C_\sigma |\) over all \(2^s\) seeds.

Let \(N\) be a machine, \(L\) a language, \(T \colon \mathbb {N} \to \mathbb {N}\) a clock, and \(c\) a rational. \(N\) accepts \(L\) with probability at least \(c\) at clock \(T\) if \(\mathrm{acceptProb}_N(x, T(|x|)) \ge c\) for every \(x \in L\), and \(N\) accepts non-members with probability at most \(c\) at clock \(T\) if \(\mathrm{acceptProb}_N(x, T(|x|)) \le c\) for every \(x \notin L\). \(N\) is probabilistic polynomial-time if there are \(f\) and \(d\) with \(f = O(n^d)\) such that every trace of \(N\) on every input \(x\) has halted after \(f(|x|)\) steps.

\(L \le _p L'\) if there is \(f \in \mathsf{FP}\) with \(x \in L \iff f(x) \in L'\) for all \(x\).

\(\mathsf{RTIME}(T)\) is defined like \(\mathsf{BPTIME}(T)\) with acceptance probability at least \(1/2\) on \(x \in L\) and at most \(0\), that is equal to \(0\), on \(x \notin L\). \(\mathsf{RP} = \bigcup _k \mathsf{RTIME}(n^k)\) and \(\mathsf{coRP} = \{ L : \overline{L} \in \mathsf{RP}\} \).

\(\mathrm{acceptLeafCount}_N(x, T)\) is the number of accepting leaves of the computation tree of \(N\) on \(x\) truncated at depth \(T\): a halted configuration contributes \(1\) if its output cell \(1\) equals \(1\) and \(0\) otherwise, a configuration that has not halted at depth \(T\) contributes \(0\), and any other configuration contributes the sum over its two successors. So a path that halts at depth \(t {\lt} T\) is one leaf, unlike in \(\mathrm{acceptCount}\). \(\# \mathsf{P}\) is the set of \(f \colon \{ 0,1\} ^* \to \mathbb {N}\) for which some machine \(N\), some \(k\), and some \(T = O(n^k)\) satisfy: every path halts within \(T(|x|)\) steps and \(f(x) = \mathrm{acceptLeafCount}_N(x, T(|x|))\) for every \(x\).

A deterministic machine \(U\) simulates \(M\) under a compiler \(c : \{ 0,1\} ^* \to \{ 0,1\} ^*\) if for every program \(p\): \(U\) halts on \(c(p)\) if and only if \(M\) halts on \(p\), and for every \(y\), \(U\) produces \(y\) on \(c(p)\) if and only if \(M\) produces \(y\) on \(p\).

For \(s : \mathbb {N} \to \mathbb {N}\), \(\mathsf{SIZE}(s)\) is the class of languages decided by a fan-in-two AND/OR circuit family whose size at every length \(n\) is at most \(s(n)\). The same definition is available over any basis.

An alternating TM partitions its non-halting states into existential and universal states; acceptance is the least fixed point of the induced \(\vee \)/\(\wedge \) labelling of the configuration graph, or equivalently a bounded game between two players. \(\mathsf{AP}\) is the class of languages decided by an alternating machine all of whose paths halt in polynomial time.

Fix an input \(x\) of length \(n\) and a space bound \(s\), and consider configurations with state set \(Q\) and \(k\) work tapes. A configuration is windowed if its input tape holds the initial input contents, every work cell beyond position \(s\) is blank, and every output cell beyond position \(s + 1\) is blank; the initial configuration is windowed. The code of a configuration records its state, its input head clamped to at most \(n + s + 1\), each work head clamped to at most \(s\) together with work cells \(0, \dots , s\), and its output head clamped to at most \(s + 1\) together with output cells \(0, \dots , s + 1\). Two windowed configurations within decision space \(s\) with the same code are equal. There are exactly \(|Q|\, (n + s + 2)\, \bigl((s + 1)\, 4^{s + 1}\bigr)^k\, (s + 2)\, 4^{s + 2}\) codes, which is at most \(2^{|Q| + (n + s + 2) + 3k(s + 1) + 3(s + 2)}\). A DTM step, or an NTM step under either choice bit, from a windowed configuration within decision space \(s\) gives a windowed configuration. Hence, if every configuration reachable in the configuration graph from a windowed configuration is within decision space \(s\), then all of them are windowed. These declarations live in proof-internal modules and are shared by \(\mathsf{PSPACE} \subseteq \mathsf{EXP}\), \(\mathsf{NL} \subseteq \mathsf{P}\), Savitch’s theorem and the inductive-counting certificate. The sharper count for transducers under auxiliary space, in Theorem 208, is separate.

The configuration graph of an NTM has an edge from each non-halted configuration to each of its two successors, one per choice bit. \(\mathrm{ReachesCfg}\) is the reflexive-transitive closure of this relation, \(\mathrm{ReachesCfgIn}(t)\) and \(\mathrm{ReachesCfgLe}(t)\) are reachability in exactly and in at most \(t\) steps, and \(\mathrm{reachSet}(c_0, t)\) is the set of configurations reached from \(c_0\) within \(t\) rounds of successor closure, that is, the state of breadth-first search after \(t\) rounds.

\(S\) is space-constructible if some DTM maps \(1^n\) to the binary representation of \(S(n)\) in space \(O(S(n))\). This is distinct from the library’s time-constructibility and from the randomness-bound condition used in the PCP theorem.

A configuration on an input of length \(n\) is within auxiliary space \(s\) when every work head is at position at most \(s\) and the input head is at position at most \(n + s + 1\): the input and its first trailing blank are free, and travel farther into the blank tail is charged. The output head is not constrained. A configuration is within decision space \(s\) when in addition its output head is at position at most \(s + 1\); only the verdict cell \(1\) is free.

A DTM decides \(L\) in space \(S\) if every configuration reachable from its initial configuration on \(x\) is within decision space \(S(|x|)\) and, for every \(x\), some reachable configuration is halted with verdict \(1\) if \(x \in L\) and \(0\) if \(x \notin L\). An NTM decides \(L\) in space \(S\) if there is a time bound \(T\) such that every choice sequence halts within \(T(|x|)\) steps, \(x \in L\) exactly when some choice sequence of length \(T(|x|)\) ends halted with verdict \(1\), and every configuration along every path, up to time \(T(|x|)\), is within decision space \(S(|x|)\). A machine is a transducer if its transition function never moves the output head left (for an NTM, under either choice bit); the two deciding predicates do not require this. A DTM computes \(f\) in space \(S\) if it is a transducer, every reachable configuration is within auxiliary space \(S(|x|)\), and on every input \(x\) it halts with output \(f(x)\); the output length is not charged.

A DTM decides \(L\) in time \(T\) and space \(S\) if every reachable configuration on \(x\) is within decision space \(S(|x|)\) and on every input it halts within \(T(|x|)\) steps with the correct verdict. \(\mathsf{DTISP}(T, S)\) is the class of languages decided by a single DTM in time \(t\) and space \(s\) for some \(t = O(T)\) and \(s = O(S)\). Steve’s class is \(\mathsf{SC} = \bigcup _{k, j} \mathsf{DTISP}(n^k, (\log n)^j)\).

For a DTM \(M\), a precondition \(\mathit{pre}\) on (input tape, work tapes, output tape), an input length \(n\) and a space bound \(s\), the space contract holds if, whenever \(M\) starts in its start state on tapes satisfying \(\mathit{pre}\), every configuration it reaches is within auxiliary space \(s\) for input length \(n\). The time-and-space contract with bounds \(b\), \(n\) and \(s\) is the conjunction of the time-bounded triple \(\{ \mathit{pre}\} \, M\, \{ \mathit{post}\} _b\) with this space contract.

A program has a fixed finite set of registers, each holding a natural number of at most \(c \log n\) bits for a program constant \(c\). Instructions are read-only access to the input bit at a register-held index, the input length, successor, comparison and addition on registers, conditionals, bounded loops whose bounds are register values, sequencing, and appending a bit to a write-only output stream.

A QBF is built from variables \(x_i\) (\(i \in \mathbb {N}\)), the constants \(\top \) and \(\bot \), negation, conjunction, disjunction, and the quantifiers \(\exists x_i\) and \(\forall x_i\). It is evaluated under an assignment \(\alpha : \mathbb {N} \to \{ 0,1\} \); a quantifier over \(x_i\) evaluates its body under both updates of \(\alpha \) at \(i\) and takes the disjunction (\(\exists \)) or conjunction (\(\forall \)) of the two values. A formula is closed when it has no free variables, and true when it evaluates to \(1\) under the all-false assignment. The quantifier depth is the largest number of quantifiers on a root-to-leaf path; it bounds, but does not count, alternations, and a formula is quantifier-free when its depth is \(0\).

A bit-string codec for QBF with polynomial-time decoding and a polynomial size bound, and the language \(\mathsf{TQBF}\) of codes of closed true formulas.

A deterministic Turing machine with \(k\) work tapes consists of a finite state type \(Q\) with decidable equality, a start state and a halt state, and a transition function

that must move right every head reading \(\triangleright \). One step applies \(\delta \) to the current state and the symbols under the input head, the \(k\) work heads, and the output head, writes on the work and output tapes, and moves all heads; the halt state has no successor. The relation \(c \to ^t c'\) holds when \(c'\) is reached from \(c\) in exactly \(t\) steps, and \(c \to ^* c'\) is its reflexive–transitive closure.

A deterministic machine \(M\) computes \(f : \{ 0,1\} ^* \to \{ 0,1\} ^*\) in time \(T\) if on every input \(x\) it halts within \(T(|x|)\) steps and its output tape has output \(f(x)\). It computes \(f\) if it does so for some \(T\).

A deterministic machine \(M\) decides \(L\) in time \(T : \mathbb {N} \to \mathbb {N}\) if on every input \(x\) it reaches the halt state within \(T(|x|)\) steps, with output cell \(1\) equal to \(1\) if \(x \in L\) and equal to \(0\) if \(x \notin L\) (Arora–Barak Definition 1.2).

A fan-in-two circuit family is logspace-uniform if some function in \(\mathsf{FL}\) maps \(1^n\) to the family code at length \(n\), for every \(n\), as in Arora–Barak, Section 6.2. The generator reads \(n\) in unary, and its output at \(n = 0\) carries the stored empty-input answer. The class \(\mathsf{UniformPPoly}\) consists of the languages decided by a logspace-uniform circuit family of polynomial size. P-uniformity is not used.

A deterministic machine \(U\) is universal if for every \(k\) and every machine \(M\) with \(k\) work tapes there is a computable compiler \(c\) such that \(U\) simulates \(M\) under \(c\). It is efficiently universal for an admissibility predicate on clocks if for every such \(M\) there are a computable compiler \(c\), a constant \(C\), and a clock \(\tau \) such that \(U\) simulates \(M\) under \(c\), \(c\) has additive overhead \(C\), \(U\) simulates \(M\) under \(c\) in time \(\tau \), and \(\tau \) is admissible; it is efficiently universal when the predicate is polynomiality. Computability of \(c\) is essential: without it a machine that copies its input after a leading \(0\) and diverges after a leading \(1\) would be universal, with a compiler that consults the source machine’s halting behavior and output.

\(\mathsf{ZPP} = \mathsf{RP} \cap \mathsf{coRP}\). The Las Vegas characterization is a separate planned node (Theorem 160); the library has only fixed-clock probabilistic semantics.

For all real \(a, b\), \(\frac{1}{2}\bigl((a + b/\sqrt{3})^4 + (a - b/\sqrt{3})^4\bigr) \le (a^2 + b^2)^2\). Read on one bit, this says \(\lVert T_{1/\sqrt{3}} f \rVert _4^4 \le \lVert f \rVert _2^4\) for \(f(x) = a + bx\). The Lean statement is only the real inequality; the library has no \(L^4\) norm or one-bit noise operator.

For \(0 {\lt} m\) and \(|x| = n {\lt} m\), \(D^u_m\) gives \(\mathrm{pair}(x, 1^{m-n})\) mass \(1/(m \cdot 2^n)\). For every machine \(U\) and threshold \(r\),

For every machine \(U\) and every function \(p \colon \mathbb {N} \to \mathbb {N}\), take the ordinary parameters of the iterated plan, whose transformed clock is \(\tau (n, t) = p(t)\) regardless of output length. No estimator satisfies Fact 3.4’s sandwich for \(U\) and \(\tau \) on every instance: at source time \(0\), no machine prints a string of length \(p(0) + 1\) within \(p(0)\) steps. The estimator hypotheses below are therefore restricted to the plan’s own queries.

Fix an oracle machine \(N\) and an oracle \(A\). (a) If \(t \le t'\) then \(C^{t',A}_N(x) \le C^{t,A}_N(x)\). (b) For an ordinary machine \(M\) viewed as an oracle machine that never queries, \(C^{t,A}_M(x) = C^t_M(x)\) for every oracle \(A\). (c) Suppose \(N\) simulates an oracle machine \(N'\) in time \(\tau \) under a compiler \(c\) (bounded productions transfer for every oracle; bounded halting is not required), with \(|c(p)| \le |p| + C\) and \(\tau (p, t) \le a (|p| + t + 1)^e\) for all \(p, t\). Then there are \(a', e'\), chosen once for all oracles, such that for every oracle \(A\), string \(x\), clock \(t\) and bound \(b\), \(C^{t,A}_{N'}(x) \le b\) implies \(C^{a'(b + t + 1)^{e'},A}_N(x) \le b + C\).

If an event has probability \(p\) under the uniform distribution on a nonempty finite sample space, the probability that at least one of \(k\) independent uniform draws hits it is exactly \(1 - (1-p)^k\), and it is at least \(kp/(1+kp)\); in particular it is at least \(1/2\) whenever \(kp' \ge 1\) for some lower bound \(p' \le p\).

For every \(m\), \(\ell \) and \(\rho {\gt} 1\) there is a polynomial-time computable NW design with \(\sum _{j{\lt}i} 2^{|S_i \cap S_j|} \le \rho (m-1)\) for every \(i\) and seed length \(d = \lceil \ell /\ln \rho \rceil \cdot \ell \) (Raz–Reingold–Vadhan weak designs); its overlap budget is at most \(\rho (m-1) + m\).

(a) A \(\delta \)-dense random test has advantage at least \(\delta \) against every low-complexity generator. (b) If \(m {\gt} 0\) and the advantage is at least \(\delta \), then for \(T\) or its complement there is \(i {\lt} m\) such that the Yao hybrid whose first \(i+1\) coordinates come from \(G\) (the rest uniform) is accepted with probability at least \(\delta /m\) more than the hybrid whose first \(i\) coordinates do. (c) Over any nonempty finite background space, the predictor that outputs a uniform candidate bit when the test accepts and its complement otherwise succeeds with probability exactly \(1/2\) plus the acceptance gain from substituting the true bit for the candidate.

There are exactly \(2^{2^n}\) Boolean functions on \(n\) bits, that is, \(2^{2^n}\) truth tables of length \(2^n\).

For all sets \(P, Q\) of Boolean functions on \(n\) bits: \(|P| \le 2^{2^n}\), \(0 \le \mathrm{density}(P) \le 1\), \(\mathrm{density}(P^c) = 1 - \mathrm{density}(P)\) with \(P^c\) the complement among all Boolean functions on \(n\) bits, and \(\mathrm{density}(P \cup Q) \le \mathrm{density}(P) + \mathrm{density}(Q)\).

Sums of negligible functions and products of a negligible function with a polynomial are negligible; a function bounded in absolute value by a negligible function is negligible.

For every oracle, halting and producing \(y\) within \(t\) steps imply the same within any \(t' \ge t\) steps, and imply eventual halting and eventual production of \(y\), respectively.

Fix an oracle. A step is undefined exactly at the halt state; each configuration has at most one successor and each exact-time run has a unique final configuration. In a non-halted query state, a true answer is one step to the yes-successor and a false answer is one step to the no-successor, with all tapes unchanged. The query word of a tape whose head is at cell \(h\) has exactly \(h - 1\) bits (none when \(h = 0\)). A map from oracle configurations to configurations of an ordinary machine that sends every oracle step to an ordinary step sends every exact-time oracle run to an ordinary run with the same number of steps.

Every oracle machine simulates itself under the identity compiler, in time \((p, t) \mapsto t\). If \(U_1\) simulates \(U_2\) under \(c_1\) and \(U_2\) simulates \(M\) under \(c_2\), then \(U_1\) simulates \(M\) under \(c_1 \circ c_2\), and likewise for timed simulations with clock \((p, t) \mapsto \tau _1(c_2(p), \tau _2(p, t))\). Efficient oracle universality for any clock policy, in particular the polynomial one, implies oracle universality, and enlarging the policy preserves efficient universality.

If \(A\) is PSPACE-complete under polynomial-time many-one reductions then \(\mathsf{P}^A = \mathsf{NP}^A = \mathsf{PSPACE}\).

Let \(P\) be a set of Boolean functions on \(n\) bits with density at least \(\delta \), and let a family \(\{ f_k\} \) have no member in \(P\). Then the test “the truth table lies in \(P\)” accepts a uniformly random function with probability at least \(\delta \) and accepts \(f_k\) with probability \(0\), so its distinguishing advantage is at least \(\delta \). No circuit assumption is used.

For every \(B\), the language \(U_B = \{ 1^n : B \text{ contains a string of length } n\} \) is in \(\mathsf{NP}^B\).

There are injective codes for formulas (a unary token count followed by the postfix token stream) and for width-\(5\) programs (a unary instruction count followed by the instructions, each a unary variable index and two seven-bit permutation ranks), and a total function \(g\) on bit strings, sending every string that does not decode to a formula to the empty string, such that for every formula \(\varphi \) of depth \(d\), \(g(\mathrm{code}(\varphi ))\) is the code of, and decodes to, the program compiled from \(\varphi \) at \(\sigma _0\) in Theorem 282, and \(|g(\mathrm{code}(\varphi ))| \le 4^d + 1 + 4^d (|\mathrm{code}(\varphi )| + 15)\).

A deterministic transducer computes \(g(\mathrm{code}(\varphi ))\) from \(\mathrm{code}(\varphi )\) using \(O(\mathrm{depth}(\varphi ) + \log |\mathrm{code}(\varphi )|)\) work-tape cells.

For a width-\(w\) program \(P\) of length \(\ell \) and a point \(x\), there is a formula that, under every assignment, is true exactly when the value of \(P\) moves \(x\), and that has depth at most \((w + 1) \lceil \log _2 \ell \rceil + 2\), where \(\lceil \log _2 \ell \rceil \) is read as \(0\) for \(\ell \le 1\). If every instruction of \(P\) reads a variable below \(n\), then every variable of the formula is below \(n\).

For a fan-in-two single-output circuit \(C\) with \(N \ge 1\) inputs and size \(s\), \(\mathrm{evalCode}(N, \mathrm{code}(C), x) = C(x)\) for every \(x \in \{ 0,1\} ^N\), and \(|\mathrm{code}(C)| \le 1 + s\, (2(N + s) + 6)\).

The wiring digraph of a circuit has its \(N + G + M\) input, internal and output vertices, numbered in that order, and an edge from each wire to every gate that reads it. Every edge goes from a smaller index to a larger one, so the digraph is acyclic, and its number of edges is at most the total fan-in of the circuit (the number of gate-input occurrences, output gates included). The bound can be strict, since a gate that reads one wire twice contributes one edge.

Write \(\mathrm{size}\) for the fan-in-two AND/OR size complexity. Let \(m \ge 1\), let \(f : \{ 0,1\} ^{k + m} \to \{ 0,1\} \), and let \(g : \{ 0,1\} ^m \to \{ 0,1\} \) output \(1\) on \(y\) exactly when \(f(x\, y) = 1\) for some \(x \in \{ 0,1\} ^k\). Then \(\mathrm{size}(g) \le 2^k (\mathrm{size}(f) + 1)\).

Some two \(5\)-cycles in \(S_5\) have a \(5\)-cycle as their commutator, and every \(5\)-cycle in \(S_5\) is the commutator \([a, b] = a b a^{-1} b^{-1}\) of two \(5\)-cycles \(a\) and \(b\).

Let \(C\) be a fan-in-two circuit on \(k + m\) inputs with \(m \ge 1\), \(M \ge 1\) outputs and \(G\) internal gates, and let \(s \in \{ 0,1\} ^k\). There is a fan-in-two circuit \(C_s\) on \(m\) inputs, again with \(M\) outputs and \(G\) internal gates and hence of the same size as \(C\), such that \(C_s(y) = C(s\, y)\) for every \(y \in \{ 0,1\} ^m\), where \(s\, y\) is the concatenation.

Unfolding one output of a fan-in-two circuit \(C\) with \(N \ge 1\) inputs gives a formula whose variables are all below \(N\), which under every assignment \(\alpha \) computes that output of \(C\) on \((\alpha (0), \dots , \alpha (N - 1))\), and whose depth is at most twice the depth of that output gate. No size bound is claimed, since shared subcircuits are duplicated.

Let \(M\) be a deterministic machine and \(h : \mathbb {N} \to \mathbb {N}\). The direct unrolling of \(M\) at horizon \(h\) has at length \(n \ge 1\) the acceptance circuit of Theorem 261 at horizon \(h(n)\) on \(n\) inputs, the data on the inputs in order and every choice position on input \(0\). The padded direct unrolling \(P_{M,h}\) appends to this gate list constant-\(0\) gates up to \(\kappa _M (h(n) + 2)^3\) gates and then a gate copying the original output, so its gate count is a closed-form cubic in \(h(n)\); at length \(0\) it stores the output bit of the \(h(0)\)-step run on the empty input. Let \(D_{M,h}(n)\) be the family code of \(P_{M,h}\) at length \(n\). If \(M\) decides \(L\) in time \(h\), then \(P_{M,h}\) decides \(L\), and if \(h = O(n^d)\), then \(P_{M,h}\) has size \(O(n^{3d})\). For every polynomial \(q \in \mathbb {N}[X]\) and \(h(n) = q(n) + n + 1\), the map \(x \mapsto D_{M,h}(|x|)\) is in \(\mathsf{FL}\).

Let \(M\) be a probabilistic machine and \(f : \mathbb {N} \to \mathbb {N}\) such that, for every \(x\), the fraction of choice strings \(c \in \{ 0,1\} ^{f(|x|)}\) on which the \(f(|x|)\)-step trace of \(M\) on \(x\) under \(c\) is halted with output \(1\) is at least \(2/3\) if \(x \in L\) and at most \(1/3\) if \(x \notin L\); no halting assumption is made. For every \(n\) there is a single string of \(r(n) f(n)\) random bits, where \(r(n) = 12(n + 1) + 1\), on which the strict majority vote of these \(f(n)\)-step runs of \(M\), one on each of the \(r(n)\) consecutive blocks of \(f(n)\) bits, is correct for every \(x \in \{ 0,1\} ^n\).

The acceptance probability of \(N\) on \(x\) with clock \(T\) is the event probability of the set of accepting choice sequences in \(\{ 0,1\} ^T\), and the probability of output \(y\) is the event probability of the set of choice sequences along which \(N\) halts with output \(y\). Clocks can be extended: if every trace of length \(T\) from a configuration \(c\) ends halted and \(T \le T'\), then every decidable event on the final configuration has the same probability over traces of length \(T'\) from \(c\) as over traces of length \(T\). In particular, if every trace of \(N\) on \(x\) halts within \(T\) steps and \(T \le T'\), the acceptance probability and every output probability of \(N\) on \(x\) agree at clocks \(T\) and \(T'\); and if, on every input \(x\), every trace of \(N\) halts within \(T(|x|)\) steps and \(T \le T'\) pointwise, then for every \(x\) they agree at clocks \(T'(|x|)\) and \(T(|x|)\).

\(\mathrm{decode}(\mathrm{bin}(v)) = v\), and more precisely \(\mathrm{decode}(w) = v\) if and only if \(w = \mathrm{bin}(v)\); \(|\mathrm{bin}(v)|\) is the bit length of \(v\) (Mathlib’s Nat.size); and \(\mathrm{bin}\) is injective.

For every \(r \in \mathbb {N}\) and every rational \(p\) with \(2/3 \le p \le 1\), \(\sum _{j=0}^{r} \binom {2r+1}{j} p^j (1-p)^{2r+1-j} \le \frac13 (8/9)^r\).

\(|\mathrm{toList}(x)| = n\) and the \(i\)-th entry of \(\mathrm{toList}(x)\) is \(x_i\); \(\mathrm{toList}(\mathrm{ofList}(\ell )) = \ell \) and \(\mathrm{ofList}(\mathrm{toList}(x)) = x\); \(\mathrm{toList}\) is injective; and \(\mathrm{toList}\) sends concatenation of bit strings to list append.

The number of \(w \in \{ 0,1\} ^{a+b}\) whose prefix satisfies \(P\) and whose suffix satisfies \(Q\) is \(|P| \cdot |Q|\). Exactly \(\binom {k}{r}\) vectors in \(\{ 0,1\} ^k\) have \(r\) ones. More generally, for a finite set \(\alpha \) and \(E \subseteq \alpha \), exactly \(\binom {k}{j} |E|^j (|\alpha | - |E|)^{k-j}\) tuples in \(\alpha ^k\) have exactly \(j\) entries in \(E\); for a finite set \(J\) of counts, the vectors (respectively tuples) whose number of ones (respectively entries in \(E\)) lies in \(J\) number the corresponding sum over \(j \in J\). In particular the number of \(w \in \{ 0,1\} ^{kT}\) with \(\# _E(w) = j\) is \(\binom {k}{j} |E|^j (2^T - |E|)^{k-j}\).

\(|\{ 0,1\} ^T| = 2^T\), and \(|\{ 0,1\} ^{a+b}| = 2^a \cdot 2^b\).

Let \(\pi : \{ 0,1\} ^m \to \{ 0,1\} ^c\) be a map each of whose fibers has exactly \(2^g\) elements, and let \(A \subseteq \{ 0,1\} ^m\) and \(G \subseteq \{ 0,1\} ^c\) satisfy \(w \in A \iff \pi (w) \in G\). Then \(|A| = |G| \cdot 2^g\), and if \(m = c + g\) then \(\Pr [A] = \Pr [G]\).

\(\mathrm{fromBits}(\mathrm{toBits}(d)) = d\) for every rose tree \(d\); the serialization of \(d\) has length \(\mathrm{size}(d)\); the serialization is injective; and the derived bit-string encoding of any encodable type is injective.

\(|\mathrm{delimit}(x)| = 2|x| + 2\). For all \(x, y\), \(\mathrm{unpair?}(\mathrm{delimit}(x)\, y) = (x, y)\), and conversely if \(\mathrm{unpair?}(z) = (x, y)\) then \(z = \mathrm{delimit}(x)\, y\). For every list of strings \(b_1, \dots , b_m\), \(\mathrm{undelimitBlocks}(\mathrm{delimit}(b_1) \cdots \mathrm{delimit}(b_m)) = [b_1, \dots , b_m]\). Finally \(\mathrm{undelimitBlock}(\mathrm{delimit}(x)\, y) = x\), \(\mathrm{takeFirstBlock}(\mathrm{delimit}(x)\, y) = \mathrm{delimit}(x)\), and \(\mathrm{hasBlock}(z)\) holds exactly when \(\mathrm{unpair?}(z)\) succeeds.

\(|E| \le 2^T\) and \(0 \le \Pr [E] \le 1\); \(E \subseteq F\) implies \(\Pr [E] \le \Pr [F]\); \(\Pr [E^c] = 1 - \Pr [E]\), and for every \(f : \{ 0,1\} ^T \to \{ 0,1\} \), \(\Pr [f = 1] = 1 - \Pr [f = 0]\); \(\Pr [\emptyset ] = 0\) and \(\Pr [\{ 0,1\} ^T] = 1\); and \(\Pr [\sigma (E)] = \Pr [E]\) for every bijection \(\sigma \) of \(\{ 0,1\} ^T\).

\(\Pr _{w \in \{ 0,1\} ^{a+b}}[P(\text{prefix}) \wedge Q(\text{suffix})] = \Pr [P] \cdot \Pr [Q]\).

\(\Pr [E]\) equals Mathlib’s density Finset.dens of \(E\) in \(\{ 0,1\} ^T\), and the uniform average in Lemma 79 is Mathlib’s Finset.expect, so the laws above follow from Mathlib’s general finite-probability API.

For every \(n \ge 1\) there is a codec for \(\{ 0, \dots , n-1\} \) all of whose codewords have length \(\lceil \log _2 n \rceil \), whose decoder rejects values \(\ge n\). (An internal fixed-width layout, Complexity.finCodec, already has width \(\lceil \log _2 n \rceil \) and a round trip, but its decoder is total, reducing modulo \(n\), so it is neither partial nor canonical.)

If \(\sum _{i \in I} \Pr [B_i] {\lt} 1\) for bad events \(B_i \subseteq \{ 0,1\} ^S\) indexed by a finite set \(I\), some seed lies in no \(B_i\). In particular, if \(\Pr [B_x] \le 2^{-(n+1)}\) for every \(x \in \{ 0,1\} ^n\), one seed avoids every \(B_x\).

\(|\{ f : \mathrm{maj}(f) = 1\} | = \sum _{r = \lfloor k/2 \rfloor + 1}^{k} \binom {k}{r}\) and \(|\{ f : \mathrm{maj}(f) = 0\} | = \sum _{r=0}^{\lfloor k/2 \rfloor } \binom {k}{r}\). For \(2r + 1\) blocks, \(|\{ w : \mathrm{maj}_E(w) = 0\} | = \sum _{j=0}^{r} \binom {2r+1}{j} |E|^j (2^T - |E|)^{2r+1-j}\). Moreover \(\# _E(w) + \# _{E^c}(w) = k\), and when \(k\) is odd, \(\mathrm{maj}_{E^c}(w) = 1 - \mathrm{maj}_E(w)\) and negating every bit of \(f\) flips \(\mathrm{maj}(f)\).

With \(p = \Pr [E]\), the probability over \(w \in \{ 0,1\} ^{(2r+1)T}\) that \(\mathrm{maj}_E(w) = 0\) is \(\sum _{j=0}^{r} \binom {2r+1}{j} p^j (1-p)^{2r+1-j}\).

Let \(w : \{ 0,1\} ^T \to \mathbb {Q}_{\ge 0}\) and \(\theta {\gt} 0\). If \(w(r) \ge \theta \) for every \(r \in E\), then \(\Pr [E] \le \mathbb {E}_r[w(r)] / \theta \), where \(\mathbb {E}_r[w(r)] = 2^{-T} \sum _r w(r)\) is the uniform average.

If \(\langle x_1, y_1 \rangle = \langle x_2, y_2 \rangle \) then \(x_1 = x_2\) and \(y_1 = y_2\). Moreover \(\mathrm{unpair?}(z) = (x, y)\) if and only if \(z = \langle x, y \rangle \).

\(|\langle x, y \rangle | = 2|x| + 2 + |y|\). Indexing from \(0\), with \(x = x_0 \cdots x_{|x|-1}\) and \(y = y_0 \cdots y_{|y|-1}\): bits \(2i\) and \(2i + 1\) of \(\langle x, y \rangle \) are \(x_i\) for \(i {\lt} |x|\), bits \(2|x|\) and \(2|x| + 1\) are \(0\) and \(1\), and bit \(2|x| + 2 + j\) is \(y_j\) for \(j {\lt} |y|\).

\(\pi _1 \langle x, y \rangle = x\), \(\pi _2 \langle x, y \rangle = y\), and \(|\pi _2(z)| \le |z|\) for every \(z\).

Let \(\ell = 2 + k(2T + 2)\). Entry \(iT + t\) of the compact seed of \(r \in \{ 0,1\} ^\ell \) (\(i {\lt} k\), \(t {\lt} T\)) is \(r_{2 + i(2T+2) + t}\). Every \(s \in \{ 0,1\} ^{kT}\) is the compact seed of exactly \(2^{2 + k(T+2)}\) sequences in \(\{ 0,1\} ^\ell \), so for every predicate \(P\) on \(\{ 0,1\} ^{kT}\) the number of \(r \in \{ 0,1\} ^\ell \) whose compact seed satisfies \(P\) is \(|P| \cdot 2^{2 + k(T+2)}\), and its probability is \(\Pr [P]\). Consequently, if a machine \(M\) on input \(x\) halts with output cell \(1\) equal to \(1\) along \(r \in \{ 0,1\} ^\ell \) exactly when the compact seed of \(r\) satisfies \(P\), then the acceptance probability of \(M\) on \(x\) with clock \(\ell \) is \(\Pr _{s \in \{ 0,1\} ^{kT}}[P(s)]\).

\(\Pr [E \cup F] \le \Pr [E] + \Pr [F]\), and \(\Pr [\bigcup _{i \in s} E_i] \le \sum _{i \in s} \Pr [E_i]\) for every finite family, with equality when the family is pairwise disjoint. If a map \(f\) sends every point of \(E\) into a finite set \(s\), then \(\Pr [E] = \sum _{i \in s} \Pr [E \cap f^{-1}(i)]\).

The number of points satisfying some \(p_i\), \(i \in s\), is at most \(\sum _{i \in s} |p_i|\). Consequently, if bad sets \(B_i \subseteq S\), indexed by a finite set \(I\), satisfy \(\sum _{i \in I} |B_i| {\lt} |S|\), some \(s \in S\) lies in no \(B_i\).

On Boolean points the arithmetized expression takes the value \(1\) exactly on true formulas and \(0\) otherwise, linearization does not change values on Boolean points, and with linearization every polynomial the protocol handles has individual degree at most \(2\) and total size polynomial in the formula.

Fix a protocol, an input \(x\), a coin count \(t\) and a message bound \(m\). A coin string \(r \in \{ 0,1\} ^t\) is consistent with a transcript \(\tau \) if every verifier message recorded in \(\tau \) is the one the verifier sends on coins \(r\). Define \(\mathrm{gval}\) at a transcript \(\tau \) by recursion on the number of remaining rounds: with none left it counts the coin strings consistent with \(\tau \) on which the verdict accepts the view of \(\tau \), and otherwise it sums, over the verifier messages that the consistent coin strings produce next, the maximum over replies of length at most \(m\) of the value one round down. Let \(\mathrm{gval}(x)\) be its value at the root: coin count \(c(|x|)\), message bound and round count at \(|x|\), and the empty transcript. Then every strategy bounded by the message bound at \(|x|\) has at most \(\mathrm{gval}(x)\) accepting coin strings, and a bounded strategy chosen for \(x\) (a maximizing reply at every node) has exactly \(\mathrm{gval}(x)\).

For \(f : \{ 0,1\} \to R\) with \(R\) a commutative ring, let \(\widetilde{f} : R \to R\) be \(\widetilde{f}(x) = f(0)(1 - x) + f(1)\, x\). Then \(\widetilde{f}(0) = f(0)\) and \(\widetilde{f}(1) = f(1)\), so \(\widetilde{f}\) agrees with \(f\) at both Boolean points.

For a rational \(s\), let \(\mathsf{PCP}_s(r, q)\) be the class with soundness error \(s\) in place of \(1/2\), so \(\mathsf{PCP}_{1/2}(r, q) = \mathsf{PCP}(r, q)\). If \(r\) is constructible and \(0 \le s\), then \(\mathsf{PCP}_s(r, q) \subseteq \mathsf{PCP}_{s^2}(2r, 2q)\). Consequently, if \(r\) is constructible and \(0 \le s {\lt} 1\), every language in \(\mathsf{PCP}_s(r, q)\) is in \(\mathsf{PCP}(2^j r, 2^j q)\) for some \(j \in \mathbb {N}\).

If \(p\) is a nonzero polynomial over a finite field \(\mathbb {F}\) of total degree at most \(d\) in \(m\) variables, a uniformly random point of \(\mathbb {F}^m\) is a root with probability at most \(d / |\mathbb {F}|\); in particular a nonzero univariate polynomial of degree \(d\) has at most \(d\) roots. Mathlib provides the counting statement for MvPolynomial (MvPolynomial.schwartz_zippel_totalDegree, over an integral domain with points drawn from \(S^m\) for a finite set \(S\)); nothing in this node is formalized in the library yet, and what remains is the bridge to the library’s finite probability over encoded coin strings.

The transcript after \(n\) rounds has length exactly \(2n\). If two strategies agree on all transcripts of length at most \(2n\), then for every input and every coin string the transcripts after \(n\) rounds coincide. Hence acceptance and the accept event on input \(x\) depend on the strategy only through its values on transcripts of length at most twice the round count at \(|x|\).

Let \(C(f)\) be the minimum number of gates of a single-output circuit over the imported library’s De Morgan signature computing \(f : \{ 0,1\} ^n \to \{ 0,1\} \), every gate counted, constants and identities included. Then \(\lvert C(f) - C(g) \rvert \le 2n \cdot d_H(f, g)\), where \(d_H\) is the number of truth-table entries on which \(f\) and \(g\) differ. Consequently, if \(t \ge 1\) and \(t {\lt} C(h)\) for some \(h\), then some \(f\) has \(t {\lt} C(f) \le t + 2n\).

A decision tree of depth \(s\) is computed by a DNF of width at most \(s\) and by a CNF of width at most \(s\).

Every monotone formula computes a monotone function, and a monotone formula computing \(f\) has at least as many leaves as \(f\) has essential inputs.

For a finite-arity restriction \(\rho \) and a CNF or DNF \(\varphi \) over \(N\) variables, the simplified restriction \(\varphi |_\rho \) satisfies \(\varphi |_\rho (x) = \varphi (\rho \text{ applied to } x)\) for every \(x \in \{ 0,1\} ^N\), and its width is at most the width of \(\varphi \).

The parity family is in \(\mathsf{TC}^0\).

Every assignment satisfying \(C_1\) and \(C_2\) satisfies their resolvent on any variable, and the resolvent has at most \(|C_1| + |C_2|\) literals.

Evaluating \(\varphi |_\rho \) at \(\alpha \) equals evaluating \(\varphi \) at \(\rho \) applied to \(\alpha \). Restricting by \(\rho _1\) and then by \(\rho _2\) equals restricting by \(\rho _1 \circ \rho _2\), and restriction preserves formula size and depth exactly.

Let \(p \ge 2\). Every finite family of more than \(\ell !\, (p-1)^\ell \) finite sets, each of size exactly \(\ell \), contains \(p\) distinct sets whose pairwise intersections are all equal (to their common intersection). The same holds for more than \((\ell + 1)\, \ell !\, (p-1)^\ell \) sets, each of size at most \(\ell \). This is proved in the imported algebraic-circuits library.

Let the parameters be widening with \(\sigma (n, \cdot )\) monotone. If a search map \(A\) returns, on every \((x, 1^t)\) with \(C^t_U(x) {\lt} \infty \), a program of length at most \(\sigma (|x|, C^t_U(x))\) that produces \(x\) within \(\tau (|x|, t)\) steps, then the decision rule “accept the canonical code of \((x,1^t,1^s)\) iff \(A(x,1^t)\) has length at most \(\sigma (|x|,s)\) and produces \(x\) within \(\tau (|x|,t)\) steps, and reject malformed strings” solves \(\mathsf{GapMINKT}(U, \sigma , \tau )\) (it answers correctly on both promised sides). No hypothesis is placed on \(A\) where \(C^t_U(x) = \infty \).

For every machine \(U\), string \(x\), clocks \(t \le t'\) and bound \(s \in \mathbb {N}\): (a) \(C^t_U(x) \le s\) iff some program of length at most \(s\) produces \(x\) within \(t\) steps, and \(C_U(x) \le s\) iff some program of length at most \(s\) produces \(x\); (b) \(C^{t'}_U(x) \le C^t_U(x)\); (c) \(C_U(x) \le C^t_U(x)\); (d) if \(C^t_U(x) {\lt} \infty \) then \(C^t_U(x) \le t\).

The function \(n \mapsto n + 1\) is clock-constructible, and if \(g\) is clock-constructible then so is \(n \mapsto g(n)(n+1)\). Hence for every \(k \ge 1\) the function \(n \mapsto (n+1)^k\) is clock-constructible.

1. If \(M\) decides \(L\) in time \(T\), then \(\mathrm{complement}(M)\) decides \(\{ 0,1\} ^* \setminus L\) in time \(2T(n) + 4\).

2. If \(M_1\) decides \(L_1\) in time \(T_1\) and \(M_2\) decides \(L_2\) in time \(T_2\), then \(\mathrm{union}(M_1, M_2)\) decides \(L_1 \cup L_2\) in time \(10\, T_1(n) + T_2(n)\).

3. If \(\{ \mathit{pre}\} \, M\, \{ \mathit{post}\} _b\), where \(\mathit{post}\) guarantees that the output tape holds \(\triangleright \) at cell \(0\) and nowhere else, that the output head is at a cell at most \(p\), and that output cell \(1\) holds a symbol satisfying \(\varphi \), then \(\{ \mathit{pre}\} \, \mathrm{complement}(M)\, \{ \mathit{post}'\} _{b + p + 4}\), where \(\mathit{post}'\) says that output cell \(1\) holds the flip of some symbol satisfying \(\varphi \) (\(0\) and \(1\) exchanged, anything else made blank).

\(M\) computes \(f\) in time \(T\) if and only if \(M\) produces \(f(x)\) on \(x\) within time \(T(|x|)\) for every \(x\). \(M\) computes \(f\) if and only if \(M\) produces \(f(x)\) on every \(x\).

Let \(M\) be a deterministic machine.

1. \(M\) produces \(y\) on \(p\) within time \(t\) if and only if \(\mathrm{run}(\mathrm{init}(p), t)\) is halted with output \(y\); in particular bounded production is decidable.

2. Bounded production is monotone in \(t\), and \(M\) produces \(y\) on \(p\) exactly when it does so within some finite time.

3. If \(M\) produces \(y\) on \(p\) within time \(t\), it produces \(y\) on the first \(t\) bits of \(p\) within time \(t\).

4. If \(M\) produces both \(y\) and \(y'\) on \(p\), then \(y = y'\); this holds also for bounded production under two different clocks.

Every machine simulates itself under the identity. If \(U_1\) simulates \(U_2\) under \(c_1\) and \(U_2\) simulates \(M\) under \(c_2\), then \(U_1\) simulates \(M\) under \(c_1 \circ c_2\), and likewise for timed simulations with clock \((p, t) \mapsto \tau _1(c_2(p), \tau _2(p, t))\). Additive overheads add; polynomial clocks compose through a compiler with additive overhead; and computable functions are closed under composition.

If a deterministic machine decides \(L\) in time \(T\), its nondeterministic embedding decides \(L\) in time \(T\). Without a time bound, a deterministic machine and its embedding accept the same strings, where acceptance means reaching the halt state (after some number of steps, along some choice sequence) with output cell \(1\) equal to \(1\).

A machine that simulates a universal machine under a computable compiler is universal. Every machine that is efficiently universal for some admissibility predicate, in particular every efficiently universal machine, is universal.

Let \(w, n, c\) be polynomial-time numbers in the sense of Definition 119, let \(s \in \mathsf{FP}\), and for a string \(x\) let \(v(x)\) be its value as a binary numeral, least significant bit first.

1. The low \(w(z)\) bits of \(n(z)\), least significant first, and the minimal binary expansion \(\mathrm{bin}(n(z))\) are in \(\mathsf{FP}\) as functions of \(z\).

2. \(\min (v(s(z)), c(z))\) is a polynomial-time number; so is \(v(s(z))\) itself when \(v(s(z)) \le c(z)\) for all \(z\).

3. The serialization of \(s(z)\) as a list of bits, and the serialization of the number \(n(z)\), are in \(\mathsf{FP}\) as functions of \(z\).

\(\overline{L} \in \mathsf{coNP}\) if and only if \(L \in \mathsf{NP}\). If \(L_1\) is \(\mathsf{coNP}\)-hard and \(L_1 \le _p L_2\), then \(L_2\) is \(\mathsf{coNP}\)-hard, and \(\mathsf{coNP}\)-complete if moreover \(L_2 \in \mathsf{coNP}\). The complement of an \(\mathsf{NP}\)-hard (respectively \(\mathsf{NP}\)-complete) language is \(\mathsf{coNP}\)-hard (respectively \(\mathsf{coNP}\)-complete), and the complement of a \(\mathsf{coNP}\)-hard (respectively \(\mathsf{coNP}\)-complete) language is \(\mathsf{NP}\)-hard (respectively \(\mathsf{NP}\)-complete).

The language of strings containing a \(1\) is in \(\mathsf{P}\). If \(f \in \mathsf{FP}\) and, for all \(x\), \(x \in L\) exactly when \(f(x)\) contains a \(1\), then \(L \in \mathsf{P}\). In particular, if \(g\) is Boolean-valued, the function \(x \mapsto [g(x)]\) (the one-bit string) is in \(\mathsf{FP}\), and \(x \in L \iff g(x) = 1\), then \(L \in \mathsf{P}\). Conversely, every \(L \in \mathsf{P}\) has such a Boolean-valued \(g\); so \(L \in \mathsf{P}\) if and only if some Boolean-valued \(g\) with \(x \mapsto [g(x)]\) in \(\mathsf{FP}\) satisfies \(x \in L \iff g(x) = 1\) for all \(x\). Finally, if \(k \in \mathsf{FP}\) and \(|k(x)| \le L\) for all \(x\), then \(\{ x : Q(k(x))\} \in \mathsf{P}\) for every predicate \(Q\).

Every constant function is in \(\mathsf{FP}\), and so is \(x \mapsto 1^{|x|}\). For every function \(g\) and every finite set \(S\) of strings, the function equal to \(g\) on \(S\) and to the empty string off \(S\) is in \(\mathsf{FP}\). Hence if \(k \in \mathsf{FP}\) and \(|k(x)| \le L\) for all \(x\), then \(x \mapsto g(k(x))\) is in \(\mathsf{FP}\) for every function \(g\).

Let \(f \in \mathsf{FP}\), write \(1^i\) for the string of \(i\) ones, and write \(f_i(z) = f(\langle z, 1^i \rangle )\).

1. Concatenation over a range: the map \(\langle u, z \rangle \mapsto f_0(z) \, f_1(z) \cdots f_{|u| - 1}(z)\) is in \(\mathsf{FP}\). Hence for every \(m \in \mathsf{FP}\) the map \(z \mapsto f_0(z) \, f_1(z) \cdots f_{|m(z)| - 1}(z)\) is in \(\mathsf{FP}\).

2. List encoding: the same concatenation between a leading \(0\) and a trailing \(1\) is in \(\mathsf{FP}\). If \(f_i(z)\) is the serialization of the \(i\)-th entry of a list \(\ell \) with \(|\ell | = |u|\), it is the serialization of \(\ell \).

3. Counting: the map sending \(\langle 1^n, z \rangle \) to \(1^s\), where \(s = \sum _{i {\lt} n} |f_i(z)|\), is in \(\mathsf{FP}\).

4. Search: the map sending \(\langle 1^n, z \rangle \) to \(1^c\) is in \(\mathsf{FP}\), where, whenever some \(f_i(z)\) with \(i {\lt} n\) is nonempty, \(c\) is the least such \(i\).

5. Maximum: the map sending \(\langle 1^n, z \rangle \) to \(1^M\), where \(M = \max _{i {\lt} n} |f_i(z)|\) (and \(M = 0\) when \(n = 0\)), is in \(\mathsf{FP}\).

6. Bitwise description: if \(x \mapsto 1^{\ell (x)}\) is in \(\mathsf{FP}\) and \(f_i(x)\) is the single bit \(b(x, i)\) for all \(x\) and \(i\), then \(x \mapsto b(x, 0) \, b(x, 1) \cdots b(x, \ell (x) - 1)\) is in \(\mathsf{FP}\).

The identity function is in \(\mathsf{FP}\), and if \(f, g \in \mathsf{FP}\) then \(g \circ f \in \mathsf{FP}\).

For a finite state set \(Q\), a transition \(\delta \colon Q \times \{ 0,1\} \to Q\), an initial state, and an output map \(o \colon Q \times \{ 0,1\} \to \{ 0,1\} ^*\), the transducer that scans \(z\) from left to right and emits \(o(q_i, z_i)\) at each position is in \(\mathsf{FP}\). More generally, the state may be a polynomially bounded string updated by an \(\mathsf{FP}\) step.

Let \(p\) be a polynomial and \(L_0 \in \mathsf{P}\) with \(\langle x, y \rangle \in L_0 \Rightarrow |y| \le p(|x|)\) for all \(x, y\). If, for all \(x\), \(x \in L \iff \exists y\, \langle x, y \rangle \in L_0\), then \(L \in \mathsf{NP}\). For linearly bounded witnesses no balance hypothesis on \(L_0\) is needed: if \(L_0 \in \mathsf{P}\) and, for all \(x\), \(x \in L \iff \exists y\, (|y| \le |x| + 1 \wedge \langle x, y \rangle \in L_0)\), then \(L \in \mathsf{NP}\). In relational form, if \(\mathrm{pairLang}(R) \in \mathsf{P}\), \(R(x, y) \Rightarrow |y| \le |x| + 1\), and \(x \in L \iff \exists y\, R(x, y)\) for all \(x\), then \(L \in \mathsf{NP}\).

Let \(F, \mathit{init}, \mathit{ruler}, \mathit{width} \in \mathsf{FP}\), and suppose \(|F^m(\mathit{init}(z))| \le |\mathit{width}(z)|\) for every \(z\) and every \(m \le |\mathit{ruler}(z)|\). Then \(z \mapsto F^{|\mathit{ruler}(z)|}(\mathit{init}(z))\) is in \(\mathsf{FP}\). The same holds when the width is replaced by a polynomial bound \(|F^m(\mathit{init}(z))| \le B(|z|)\), or by a constant \(c\) with \(|F^{m+1}(\mathit{init}(z))| \le |F^m(\mathit{init}(z))| + c\) for every \(m {\lt} |\mathit{ruler}(z)|\).

\(L \in \mathsf{P}\) if and only if some deterministic machine decides \(L\) within time \(n \mapsto p(n)\) for a polynomial \(p\) with natural-number coefficients. Likewise \(f \in \mathsf{FP}\) if and only if some deterministic machine computes \(f\) within time \(n \mapsto p(n)\) for such a polynomial \(p\).

If \(L_1\) is \(\mathsf{NP}\)-hard and \(L_1 \le _p L_2\), then \(L_2\) is \(\mathsf{NP}\)-hard; if moreover \(L_2 \in \mathsf{NP}\), then \(L_2\) is \(\mathsf{NP}\)-complete. (The variant NPComplete.transfer assumes \(L_1\) \(\mathsf{NP}\)-complete.)

\(L \le _p L\), and \(L_1 \le _p L_2 \le _p L_3\) implies \(L_1 \le _p L_3\).

If \(L_1 \le _p L_2\) then \(\overline{L_1} \le _p \overline{L_2}\), and for each \(\mathcal{C} \in \{ \mathsf{P}, \mathsf{NP}, \mathsf{coNP}\} \), \(L_2 \in \mathcal{C}\) implies \(L_1 \in \mathcal{C}\).

There is a total function in \(\mathsf{FP}\) witnessing \(\mathrm{SAT} \le _p 3\mathrm{SAT}\). On the encoding \(z\) of a formula it outputs the encoding of an exact-3 formula that is satisfiable exactly when the source is: short nonempty clauses are padded by repeating literals, the empty clause becomes a contradictory pair of clauses on a fresh variable, and long clauses are split by a chain of fresh variables, all numbered from \(|z| + 1\) upward (the splitting is exact-3 from any starting counter and equisatisfiable from any counter above every source variable). On a malformed string it outputs a fixed unsatisfiable exact-3 formula. A deterministic machine computes the function within \(6n + 16384(n + 2)^4 + 49\) steps.

In the sense of Definition 119, the following are polynomial-time, for polynomial-time numbers \(f, g, n, b, k, c\) and predicates \(p, q\).

1. The length \(|h(z)|\) of any \(h \in \mathsf{FP}\), every constant, and \(f(z) + g(z)\), \(f(z) \cdot g(z)\), \(f(z) \mathbin {\dot-} g(z)\), \(\min (f(z), g(z))\) and \(\max (f(z), g(z))\).

2. The predicates \(f(z) \le g(z)\), \(f(z) {\lt} g(z)\), \(f(z) = g(z)\), \(p \wedge q\), \(p \vee q\) and \(\neg p\), and the case distinction \(z \mapsto \) (\(f(z)\) if \(p(z)\), else \(g(z)\)). The same case distinction between two functions in \(\mathsf{FP}\) is in \(\mathsf{FP}\).

3. Loops over the indices below \(n(z)\), whose body reads \(\langle z, 1^i \rangle \): the sum of \(f(\langle z, 1^i \rangle )\), the number of \(i\) with \(p(\langle z, 1^i \rangle )\), the least such \(i\) (or \(n(z)\) if there is none), and the largest \(f(\langle z, 1^i \rangle )\). Also \(k(z)\) rounds of an update \(x \mapsto s(z, x)\) from \(a(z)\), when \(\langle z, 1^x \rangle \mapsto s(z, x)\) is polynomial-time and every value along the way is at most a polynomial-time number. Also the bounded quantifiers: \(p(\langle z, 1^i \rangle )\) for every \(i {\lt} n(z)\), and for some \(i {\lt} n(z)\).

4. \(f(z) / g(z)\) and \(f(z) \bmod g(z)\) (with \(f / 0 = 0\)), the capped power \(\min (b(z)^{k(z)}, c(z))\), the binary length of \(f(z)\), and the floor and ceiling logarithms of \(f(z)\) to the base \(b(z)\).

Every predicate \(z \mapsto Q(k(z))\) of a key \(k \in \mathsf{FP}\) of bounded length is polynomial-time. A language whose membership predicate is polynomial-time is in \(\mathsf{P}\).

Let \(N \ge 1\), and let index maps select, among \(N\) primary input wires, the \(m(n + 1)\) coefficients of \(m\) affine forms \(x \mapsto \langle a_i, x \rangle \oplus b_i\) over \(\mathrm{GF}(2)\) and the \(n\) coordinates of \(x\). There is a raw fan-in-two circuit (a gate list whose last gate is the output) with exactly \(m(4n + 4) + 2m + 4\) gates that is well formed over \(N\) inputs and, on every \(N\)-bit input, evaluates to \(1\) exactly when all \(m\) selected forms vanish on the selected \(x\). When the coefficients are the rows of an affine-hash seed \(\sigma \), this is the test \(h_\sigma (x) = 0^m\).

For \(E \subseteq \{ 0,1\} ^m\), say shifts \(u_1, \dots , u_t \in \{ 0,1\} ^m\) cover \(E\) if every \(r \in \{ 0,1\} ^m\) has some \(i\) with \(r \oplus u_i \in E\). If \(\Pr [\overline{E}] \le 2^{-k}\) and \(m {\lt} kt\), some \(t\) shifts cover \(E\). If \(\Pr [E] \le 2^{-k}\) and \(t {\lt} 2^k\), no \(t\) shifts cover \(E\).

For every pairwise-independent family, \(S \subseteq \{ 0,1\} ^n\) and target \(y\): \(\mu = |S|/2^m\); the average number of ordered pairs of distinct members of \(C_\sigma \), which is \(|C_\sigma |(|C_\sigma | - 1)\), is \((|S|^2 - |S|)/2^{2m}\); the average of \(|C_\sigma |^2\) is the sum of these two; and \(\mathrm{Var} = (|S|/2^m)(1 - 2^{-m})\), so \(0 \le \mathrm{Var} \le \mu \). For every \(r {\gt} 0\), \(\Pr [\, \bigl||C_\sigma | - \mu \bigr| \ge r\, ] \le \mathrm{Var}/r^2 \le \mu /r^2\), and if \(\varepsilon {\gt} 0\) and \(\mu {\gt} 0\) then \(\Pr [\, \bigl||C_\sigma | - \mu \bigr| \ge \varepsilon \mu \, ] \le 1/(\varepsilon ^2\mu )\). For occupancy, \(\Pr [C_\sigma \neq \emptyset ] \le \mu \), and if \(\mu {\gt} 0\) then \(\Pr [C_\sigma = \emptyset ] \le 1/\mu \), so \(\Pr [C_\sigma \neq \emptyset ] \ge 1 - 1/\mu \); in particular \(\Pr [C_\sigma \neq \emptyset ] \le 1/8\) when \(\mu \le 1/8\) and \(\Pr [C_\sigma \neq \emptyset ] \ge 7/8\) when \(\mu \ge 8\). Finally, let the amplified occupancy test on \((12k + 1)s\) seed bits return the strict majority of the answers “\(C_\sigma \neq \emptyset \)” for its \(12k + 1\) blocks \(\sigma \). If \(\mu \ge 8\) it returns \(1\) with probability at least \(1 - 2^{-k}\) (so \(0\) with probability at most \(2^{-k}\)), and if \(\mu \le 1/8\) it returns \(1\) with probability at most \(2^{-k}\).

Let \(N\) accept every \(x \in L\) with probability at least \(2/3\) and every \(x \notin L\) with probability at most \(1/3\) at a clock \(f\) (no halting assumption is needed here). For \(n = |x|\) let \(R = 12(f(n) + 11) + 1\) be the number of trials, \(\ell = R f(n)\) the amplified seed length, and \(E_x \subseteq \{ 0,1\} ^{\ell }\) the set of seeds on which a strict majority of the \(R\) runs of \(N\) on \(x\), each for \(f(n)\) steps along its own block of \(f(n)\) bits, accepts. Then \(x \in L\) if and only if some \(\ell + 1\) shifts cover \(E_x\), and \(x \notin L\) if and only if some \(\ell + 1\) shifts cover \(\overline{E_x}\).

For a polarity \(b \in \{ 0,1\} \), the matrix language \(M_b\) is the set of \(z\) such that, with \(x\), \(w\), \(r\) the components that the pair decoders read from \(z\) (exactly \(x\), \(w\), \(r\) when \(z = \langle \langle x, w \rangle , r \rangle \)) and \(\ell \) computed from \(|x|\): if \(|r| = \ell \), then for some \(i \le \ell \) the majority verdict of the \(R\) runs along \(r \oplus u_i\) equals \(b\), where \(u_0, \dots , u_{\ell } \in \{ 0,1\} ^{\ell }\) are the consecutive blocks of \(w\) (bits beyond \(|w|\) read as \(0\)). If \(p\) and \(q\) are polynomials with \((\ell + 1)\ell \le p(n)\) and \(\ell \le q(n)\) for all \(n\), then \(L = \exists ^p \forall ^q M_1\) and \(\overline{L} = \exists ^p \forall ^q M_0\).

Finally, if every path of \(N\) halts within \(T(|x|)\) steps, then \(\mathrm{acceptProb}_N(x, T') = \mathrm{acceptProb}_N(x, T(|x|))\) for every \(T' \ge T(|x|)\), so both bounded-error conditions transfer from the clock \(T\) to any pointwise larger clock.

For every machine \(N\), input \(x\), and \(T \in \mathbb {N}\), \(\mathrm{acceptLeafCount}_N(x, T) \le 2^T\) (more generally, the tree rooted at any configuration and truncated at depth \(T\) has at most \(2^T\) accepting leaves), and likewise \(\mathrm{acceptCount}_N(x, T) \le 2^T\). If every length-\(T\) choice sequence leaves \(N\) on \(x\) in a halted configuration after \(T\) steps and \(T \le T'\), then \(\mathrm{acceptLeafCount}_N(x, T') = \mathrm{acceptLeafCount}_N(x, T)\); in particular, if every path halts within \(T(|x|)\) steps for every \(x\) and \(T \le T'\) pointwise, the accepting-leaf counts at \(T'(|x|)\) and \(T(|x|)\) agree for every \(x\), so a \(\# \mathsf{P}\) value does not depend on the choice of a sufficient clock. (No such invariance is claimed for \(\mathrm{acceptCount}\), which counts length-\(T\) choice strings, so a path that halts early is counted once for each unused suffix.) For every \(f \in \# \mathsf{P}\) there are \(k\) and \(T = O(n^k)\) such that \(f(x) \le 2^{T(|x|)}\) for every \(x\).

The \(c\)-fold Cartesian power \(S^c \subseteq \{ 0,1\} ^{cn}\) of \(S \subseteq \{ 0,1\} ^n\), encoded row-major, consists of the strings all of whose \(n\)-bit blocks lie in \(S\), and \(|S^c| = |S|^c\). If \(c \ge 1\), \(q \ge 1\), \(F^2 q^c \le (q + 1)^c\), and \(e\) approximates \(a^c\) within factor \(F\), then \(\lfloor (Fe)^{1/c} \rfloor \) approximates \(a\) with relative error \(1/q\). For \(F = 16\) and \(c = 8q\) the separation condition holds for every \(q \ge 1\), so a factor-\(16\) estimate \(e\) of \(|S^{8q}|\) yields the relative estimate \(\lfloor (16e)^{1/(8q)} \rfloor \) of \(|S|\).

For every machine \(N\), input \(x\) and clock \(T\), \(\mathrm{acceptProb}_N(x, T) {\gt} 1/2 \iff 2^T {\lt} 2 \cdot \mathrm{acceptCount}_N(x, T)\). Hence for every \(L \in \mathsf{PP}\) there are a machine \(N\), some \(m\), and a clock \(f = O(n^m)\) such that every path halts within \(f(|x|)\) steps and \(x \in L \iff 2^{f(|x|)} {\lt} 2 \cdot \mathrm{acceptCount}_N(x, f(|x|))\).

For every machine \(N\), polynomial \(p \in \mathbb {N}[X]\), and polarity \(b\), take the clock \(f = p\) in Lemma 166. The verdict function \(z \mapsto [z \in M_b]\), with one output bit, is in \(\mathsf{FP}\); consequently \(M_b \in \mathsf{P}\).

Given answers \(\rho _0, \dots , \rho _{n+3} \in \{ 0,1\} \), one per hash width \(j\), the estimate is \(0\) if \(\rho _0 = 0\) and otherwise \(2^{j^*}\), where \(j^*\) is the largest \(j\) with \(\rho _j = 1\); it is always below \(2^{n+4}\). Call the answers accurate for \(a\) if \(\rho _0 = [a {\gt} 0]\), \(\rho _j = 1\) whenever \(8 \cdot 2^j \le a\), and \(\rho _j = 0\) whenever \(8a \le 2^j\). If \(a \le 2^n\) and the answers are accurate for \(a\), the estimate approximates \(a\) within factor \(16\). The hashing estimator for \(S \subseteq \{ 0,1\} ^n\) with amplification \(k\) sets \(\rho _0 = [S \neq \emptyset ]\) and, for \(j \ge 1\), takes \(\rho _j\) to be the amplified occupancy test of Lemma 183 for the affine family to \(j\) bits and target \(0^j\), each width on its own block of the seed. The probability that some answer is not accurate for \(|S|\) is at most \((n + 4)2^{-k}\), so the estimator approximates \(|S|\) within factor \(16\) with probability at least \(1 - (n + 4)2^{-k}\), and at least \(3/4\) when \(k = n + 4\).

If the constant function \(1\) is \(O(S)\), then \(\mathsf{DSPACE}(S)\) is closed under complement. In particular \(\mathsf{PSPACE}\) is closed under complement.

If a DTM decides \(L\) in space \(S\), then so does its embedding as an NTM whose two transition functions coincide, and the embedding of a transducer is a transducer. Hence for every \(S\), \(\mathsf{DSPACE}(S) \subseteq \mathsf{NSPACE}(S)\). If \(S_1 = O(S_2)\) then \(\mathsf{DSPACE}(S_1) \subseteq \mathsf{DSPACE}(S_2)\) and \(\mathsf{NSPACE}(S_1) \subseteq \mathsf{NSPACE}(S_2)\). Consequently \(\mathsf{L} \subseteq \mathsf{NL}\) and \(\mathsf{PSPACE} \subseteq \mathsf{NPSPACE}\).

(1) A configuration predicate that holds at every start satisfying \(\mathit{pre}\), is preserved by every step, and implies auxiliary space \(s\) gives the space contract. (2) If \(\{ \mathit{pre}\} \, M\, \{ \mathit{post}\} _b\) holds and every start configuration satisfying \(\mathit{pre}\) is within auxiliary space \(s_0\), then the time-and-space contract holds with space \(s_0 + b\). (3) A time-and-space contract survives strengthening the precondition, weakening the postcondition, and enlarging the time bound, the input length and the space bound. (4) The sequential composition of two transducers is a transducer. If \(M_1\) satisfies the time-and-space contract from \(\mathit{pre}\) to \(\mathit{mid}\) with bounds \(b_1, n, s_1\), the phase-boundary normalization maps tapes satisfying \(\mathit{mid}\) to tapes satisfying \(\mathit{mid}'\), and \(M_2\) satisfies the contract from \(\mathit{mid}'\) to \(\mathit{post}\) with bounds \(b_2, n, s_2\), then \(\mathrm{seq}(M_1, M_2)\) satisfies the contract from \(\mathit{pre}\) to \(\mathit{post}\) with bounds \(b_1 + 1 + b_2\), \(n\) and \(\max (s_1, s_2)\). (5) If a transducer satisfies, for every input \(x\), the time-and-space contract from the initial tapes on \(x\) to “the output tape holds \(f(x)\)” with bounds \(T(|x|)\), \(|x|\) and \(S(|x|)\), then it computes \(f\) in space \(S\).

(1) If \(T \subseteq \mathrm{reachSet}(c_0, i)\) and \(|\mathrm{reachSet}(c_0, i)| \le |T|\) then \(T = \mathrm{reachSet}(c_0, i)\). The coded search starts from one configuration code and in each round adds the codes of the successors of the configurations the current codes decode to. (2) A code lies in round \(i\) of the coded search from \(a_0\) if and only if some sequence of \(i\) steps from \(a_0\), each staying put or moving to such a successor code, reaches it. (3) If a list of distinct members of round \(i\) is at least as long as the round, every code missing from the list is outside the round. (4) For every \(L \in \mathsf{NL}\) there are an NTM and constants \(C, D, A, B\) such that \(x \notin L\) if and only if round \(A(|x| + 1)^B\) of the coded search from the code of \(\mathrm{init}(x)\), in the window \(C \log |x| + D\), can be listed in this sense with no member decoding to a halted configuration with verdict \(1\).

Let \(G \in \mathsf{FP}\), let \(r, w\) be polynomials with natural-number coefficients, and let \(N : \{ 0,1\} ^* \to \mathbb {N}\) satisfy \(1 \le N(x) \le 2^{w(|x|)}\). Write \(y_i = G^i(\mathrm{pair}(\varepsilon , x))\). Suppose \(|y_i| \le r(|x|)\) for \(i \le N(x) + 1\), \(y_i\) does not begin with \(1\) (it is empty or begins with \(0\)) for \(0 {\lt} i {\lt} N(x)\), \(y_{N(x)}\) begins with \(1\) (the done flag), and \(y_{N(x)+1}\) is nonempty. If \(x \in L\) exactly when \(y_{N(x)+1}\) begins with \(1\), then \(L \in \mathsf{PSPACE}\).

If an NTM \(M\) decides \(L\) in some space bound, then \(x \in L\) if and only if some configuration reachable from \(\mathrm{init}(x)\) in the configuration graph of \(M\) is halted with verdict \(1\). For every \(L \in \mathsf{NL}\) there are an NTM \(M\) and constants \(A, B\) such that for every \(x\): \(x \in L\) if and only if some configuration in \(\mathrm{reachSet}(\mathrm{init}(x), A(|x| + 1)^B)\) is halted with verdict \(1\). Equivalently, \(x \notin L\) if and only if no configuration of that set is halted with verdict \(1\).

\(L \in \mathsf{PSPACE}\) if and only if there are a DTM \(M\) and a polynomial \(q\) with natural-number coefficients such that every configuration \(M\) reaches on \(x\) is within decision space \(q(|x|)\) and \(M\) halts on every input with the correct verdict.

\(\exists x_i\, \varphi \) is true under \(\alpha \) if and only if \(\varphi \) is true under \(\alpha [i \mapsto b]\) for some \(b\), and dually for \(\forall \). Evaluation depends only on the free variables, so a closed formula has an assignment-independent value, and updating or quantifying a variable that is not free changes nothing. Under every assignment, \(\neg \exists x_i\, \varphi \) has the value of \(\forall x_i\, \neg \varphi \), and \(\neg \forall x_i\, \varphi \) that of \(\exists x_i\, \neg \varphi \). Truth commutes with negation, conjunction and disjunction, and if \(\forall x_i\, \varphi \) is true then so is \(\exists x_i\, \varphi \). A conjunction is quantifier-free exactly when both conjuncts are.

(1) For an NTM, \(c\) reaches \(c'\) within \(2^{i+1}\) steps if and only if some midpoint is reachable from \(c\) within \(2^i\) steps and reaches \(c'\) within \(2^i\) steps. (2) If a map into a finite type of cardinality at most \(N\) separates the configurations reachable from \(c_0\), then \(c\) is reachable from \(c_0\) if and only if it is reachable within \(N\) steps. (3) For every \(L \in \mathsf{NPSPACE}\) there are an NTM and a polynomial \(q\) with natural-number coefficients such that \(x \in L\) if and only if some halted configuration with verdict \(1\) is reachable from \(\mathrm{init}(x)\) within \(2^{q(|x|)}\) steps.

For Boolean-valued \(f\), the BLR test accepts with probability \(\frac{1}{2} + \frac{1}{2} \sum _S \widehat{f}(S)^3\). A linear \(f\) is accepted with probability \(1\).

\(\mathbf{I}[f] = \sum _i \mathrm{Inf}_i[f] = \sum _{k=0}^n k\, W^k[f]\). Each influence satisfies \(0 \le \mathrm{Inf}_i[f] \le \mathbf{I}[f]\) and \(\mathrm{Inf}_i[f] \le \langle f, f \rangle \), which is \(1\) for Boolean-valued \(f\). Also \(\mathbf{I}[f] \le n \langle f, f \rangle \), which is \(n\) for Boolean-valued \(f\). If every coefficient on sets of size greater than \(d\) vanishes, then \(\mathbf{I}[f] \le d \langle f, f\rangle \), hence \(\mathbf{I}[f] \le d\) for Boolean-valued \(f\). For parities, \(\mathbf{I}[\chi _S] = |S|\) and \(\mathrm{Inf}_i[\chi _S] = [i \in S]\).

\(\widehat{f}(\{ i\} )^2 \le \mathrm{Inf}_i[f]\) and \(\sum _i \widehat{f}(\{ i\} )^2 = W^1[f] \le \mathbf{I}[f]\). These are not the hypercontractive level-1 inequality of Theorem 543.

If a real-valued \(f\) on \(\{ 0,1\} ^n\) is \(\varepsilon \)-close to \(\chi _S\) (it differs from \(\chi _S\) on at most an \(\varepsilon \) fraction of inputs), then for every \(x\), \(\Pr _y[f(y) f(x + y) = \chi _S(x)] \ge 1 - 2\varepsilon \). No Boolean-valuedness is needed.

\(\mathbb {E}[f] = \widehat{f}(\emptyset )\), \(\mathrm{Var}[f] = \sum _{S \neq \emptyset } \widehat{f}(S)^2\), and \(\mathrm{Cov}[f,g] = \sum _{S \neq \emptyset } \widehat{f}(S)\widehat{g}(S)\). For Boolean-valued \(f\) and \(g\), \(\mathrm{Var}[f] = 1 - \mathbb {E}[f]^2\) and \(\langle f, g \rangle = 1 - 2\, \mathrm{dist}(f,g)\).

Let \(y \sim N_\rho (x)\) mean that each \(\chi (y_i)\) independently equals \(\chi (x_i)\) with probability \(\frac{1+\rho }{2}\) and is flipped otherwise, for \(\rho \in [-1,1]\). Then \(T_\rho f(x) = \mathbb {E}_{y \sim N_\rho (x)}[f(y)]\) and \(\mathrm{Stab}_\rho [f] = \mathbb {E}_{x,\, y \sim N_\rho (x)}[f(x) f(y)]\). In particular, for Boolean-valued \(f\) and \(\delta \in [0,1]\), \(\mathrm{NS}_{1-2\delta }[f] = \Pr [f(x) \neq f(y)]\) when each bit is flipped independently with probability \(\delta \).

For \(\rho \in [0,1]\), \(\langle f, f \rangle - \mathrm{Stab}_\rho [f] \le (1 - \rho )\, \mathbf{I}[f]\). Equivalently, \(\mathrm{NS}_\rho [f] \le \frac{1-\rho }{2}\, \mathbf{I}[f]\).

\(\mathrm{Stab}_\rho [f] = \sum _{k=0}^n \rho ^k W^k[f]\). Moreover \(\mathrm{Stab}_1[f] = \langle f, f \rangle \), \(\mathrm{Stab}_0[f] = \mathbb {E}[f]^2\), and \(\mathrm{NS}_1[f] = 0\). For \(\rho \ge 0\), \(0 \le \mathbb {E}[f]^2 \le \mathrm{Stab}_\rho [f]\). On \(0 \le \rho _1 \le \rho _2\), \(\mathrm{Stab}_{\rho _1}[f] \le \mathrm{Stab}_{\rho _2}[f]\) and \(\mathrm{NS}_{\rho _2}[f] \le \mathrm{NS}_{\rho _1}[f]\). For \(\rho \in [0,1]\), \(\mathrm{Stab}_\rho [f] \le \langle f, f \rangle \) (so \(\mathrm{Stab}_\rho [f] \le 1\) for Boolean-valued \(f\)) and \(\mathrm{NS}_\rho [f] \ge 0\). Always, \(\mathrm{Stab}_\rho [f] + 2\, \mathrm{NS}_\rho [f] = \langle f, f \rangle \).

Every \(f\) has \(\mathrm{Var}[f] \ge 0\). If \(f\) is Boolean-valued, then \(\mathrm{Var}[f] = 4 \Pr [f = 1] \Pr [f = -1]\) and \(0 \le \mathrm{Var}[f] \le 1\). Moreover, with \(\varepsilon = \min (\mathrm{dist}(f, 1), \mathrm{dist}(f, -1))\), the distance to the nearer constant function, \(2\varepsilon \le \mathrm{Var}[f] \le 4\varepsilon \).

(a) If a Boolean function \(d\) satisfies \(d(x) = \mathrm{true}\) exactly when \(x\) lies in the language of a distributional problem, and the one-bit function \(x \mapsto [d(x)]\) is in \(\mathsf{FP}\), then the problem lies in \(\mathsf{AvgP}_\delta \) for every nonnegative \(\delta \) and in \(\mathsf{AvgP}\), whatever its ensemble. (b) An errorless heuristic for \(L\) (efficient or not) rejects with probability at least \(1 - \Pr [L] - \Pr [\mathrm{fail}]\) on every slice of every finite ensemble.

For every \(A\): \(\mathsf{P} \subseteq \mathsf{P}^A \subseteq \mathsf{NP}^A\) and \(\mathsf{NP} \subseteq \mathsf{NP}^A\); if \(A \in \mathsf{P}\) then \(\mathsf{P}^A = \mathsf{P}\).

For \(i \le j\), \(\mathsf{NC}^i \subseteq \mathsf{NC}^j\), \(\mathsf{AC}^i \subseteq \mathsf{AC}^j\) and \(\mathsf{TC}^i \subseteq \mathsf{TC}^j\); in particular \(\mathsf{NC}^0 \subseteq \mathsf{NC}^1\). For every \(i\), \(\mathsf{AC}^i \subseteq \mathsf{TC}^i\); in particular \(\mathsf{AC}^0 \subseteq \mathsf{TC}^0\).

For every \(i\), \(\mathsf{NC}^i \subseteq \mathsf{AC}^i \subseteq \mathsf{NC}^{i+1}\).

\(L \in \mathsf{P/poly}\) if and only if some fan-in-two circuit family decides \(L\) and has size \(O(n^k)\) for some \(k\), that is, size at most \(C n^k\) at every sufficiently large length \(n\), for some constant \(C\).

\(\mathsf{UniformPPoly} \subseteq \mathsf{P/poly}\).

The enumeration of \(k\)-tuples has length \(n^k\) and contains every \(k\)-tuple, so a truth table of arity \(k\) has length \(n^k\). A one-hot block has length \(n\). The encoding has length \(n + 1 + \sum _R n^{\mathrm{ar}(R)} + c \cdot n\), where \(c\) is the number of constants, and for a relational vocabulary it is the unary block followed by the truth tables alone. The size \(n\) is recoverable as the length of the leading block of ones, and a one-hot constant block determines its element.

Order-independent queries are closed under complement, intersection, and union.

For every set \(A \subseteq \mathbb {N}\), computable or not, the language \(\{ x : |x| \in A\} \) lies in \(\bigcup \mathsf{PCP}(r, q)\) over all \(r = O(\log n)\) and \(q = O(1)\), with no constructibility requirement on \(r\).

If \(\mathsf{PSPACE} \subseteq \mathsf{IP}\), then \(\mathsf{IP} = \mathsf{PSPACE}\). The hypothesis is also recorded, unproved, as the proposition PSPACESubsetIP, and the conclusion is stated from either form.

\(\mathsf{MA} \subseteq \mathsf{IP}\).

\(\mathsf{NP} \subseteq \mathsf{MA}\).

\(\mathsf{P} \subseteq \mathsf{MA}\) and \(\mathsf{P} \subseteq \mathsf{AM}\).

\(\mathsf{P} \subseteq \mathsf{PCP}(r, q)\) for all \(r\) and \(q\), and \(\mathsf{PCP}(r, q) \subseteq \mathsf{PCP}(r, q')\) whenever \(q \le q'\) pointwise.

Checking a resolution refutation, encoded as a clause sequence, is a Cook–Reckhow proof system.

\(\mathsf{P}\) is closed under complement, union, intersection, set difference, and symmetric difference. In particular \(\{ L : \overline{L} \in \mathsf{P}\} = \mathsf{P}\). At the level of time bounds, \(L_1 \in \mathsf{DTIME}(T_1)\) and \(L_2 \in \mathsf{DTIME}(T_2)\) imply \(L_1 \cup L_2 \in \mathsf{DTIME}(T_1 + T_2)\).

If \(h \in \mathsf{GapP}\) then \(-h \in \mathsf{GapP}\).

Complementation exchanges the quantifiers: \(\overline{\exists ^p L'} = \forall ^p \overline{L'}\) and \(\overline{\forall ^p L'} = \exists ^p \overline{L'}\), and at the level of classes the complement class of \(\exists \mathcal{C}\) is \(\forall \{ L : \overline{L} \in \mathcal{C}\} \) and dually. Since \(\mathsf{P}\) is closed under complement, \(\Pi ^p_0 = \mathsf{P}\); and \(\Sigma ^p_{k+1} = \exists \Pi ^p_k\), \(\Pi ^p_{k+1} = \forall \Sigma ^p_k\), \(\Sigma ^p_1 = \exists \mathsf{P}\), and \(\Pi ^p_1 = \forall \mathsf{P}\). Moreover \(\mathsf{P} \subseteq \exists \mathsf{P}\) and \(\mathsf{P} \subseteq \forall \mathsf{P}\), and for every \(k\), \(\Sigma ^p_k \subseteq \Sigma ^p_{k+1}\), \(\Pi ^p_k \subseteq \Pi ^p_{k+1}\), and \(\Sigma ^p_k \subseteq \mathsf{PH}\); in particular \(\mathsf{P} \subseteq \mathsf{PH}\).

For every \(T\), \(\mathsf{DTIME}(T) \subseteq \mathsf{DSPACE}(T)\) and \(\mathsf{DTIME}(T) \subseteq \mathsf{NSPACE}(T)\). Hence \(\mathsf{P} \subseteq \mathsf{PSPACE}\) and \(\mathsf{P} \subseteq \mathsf{NPSPACE}\).

Write \(A \le _{\log } B\) when some \(f \in \mathsf{FL}\) satisfies \(x \in A \iff f(x) \in B\). Then \(\le _{\log }\) is reflexive and transitive, \(A \le _{\log } B\) implies \(A \le _p B\), and \(\mathsf{L}\) and \(\mathsf{NL}\) are closed downward under \(\le _{\log }\).

\(\mathsf{NL} \subseteq \mathsf{coNL}\) if and only if \(\mathsf{coNL} \subseteq \mathsf{NL}\). In particular, if \(\mathsf{NL} \subseteq \mathsf{coNL}\) then \(\mathsf{NL} = \mathsf{coNL}\).

Suppose that for every NTM \(M\) deciding some language in space \(S\) with \(S = O(\log n)\), and all constants \(A, B\), there are constants \(C, D\) and a nondeterministic transducer deciding, in space \(C \log n + D\), the set of inputs \(x\) such that no configuration in \(\mathrm{reachSet}(\mathrm{init}(x), A(|x| + 1)^B)\) of \(M\) is halted with verdict \(1\). Then \(\mathsf{NL} \subseteq \mathsf{coNL}\).

If a Boolean-valued \(f\) passes the BLR test with probability at least \(1 - \varepsilon \), then \(f\) is \(\varepsilon \)-close to linear.

\(\widehat{f * g}(S) = \widehat{f}(S)\, \widehat{g}(S)\). The convolution of two densities is a density. For nonempty \(A\), \(\varphi _A\) is a density and \(\widehat{\varphi _A}(S) = |A|^{-1} \sum _{x \in A} \chi _S(x)\). In particular, \(\varphi _{\{ 0\} } = \sum _S \chi _S\), and every Fourier coefficient of \(\varphi _{\{ 0\} }\) is \(1\).

If \(F\) is computed by a decision tree of depth \(t\), then the real-valued view of \(F\) has degree at most \(t\).

\(f = \sum _{k=0}^{n} f^{=k}\) and \(\widehat{f^{=k}}(T) = [|T| = k]\, \widehat{f}(T)\). For \(j \neq k\) the parts \(f^{=j}\) and \(g^{=k}\) are orthogonal. Also \(\lVert f^{=k} \rVert _2^2 = W^k[f]\), \(\sum _{k=0}^n W^k[f] = \langle f, f \rangle \) (which is \(1\) for Boolean-valued \(f\)), \(f^{\le k} = \sum _{j \le k} f^{=j}\), and \(\langle f^{\le k}, f^{\le k} \rangle = \sum _{j \le k} W^j[f]\). Finally, \(f^{=0}\) is the constant \(\mathbb {E}[f]\), \(\mathrm{Var}[f] = \sum _{k=1}^n W^k[f]\), and \(\deg f \le n\).

If \(f\) is Boolean-valued and \(W^1[f] \ge 1 - \delta \), then \(f\) is \(O(\delta )\)-close to \(\chi _{\{ i\} }\) or to \(-\chi _{\{ i\} }\) for some \(i\).

Every \(f : \mathbb {F}_2^n \to \mathbb {R}\) satisfies \(f(x) = \sum _S \widehat{f}(S) \chi _S(x)\), so the parities span. The coefficients are unique: if \(f = \sum _S c_S \chi _S\) pointwise, then \(c_S = \widehat{f}(S)\) for all \(S\). In particular, two functions are equal iff all their Fourier coefficients agree, and \(f = 0\) iff every coefficient vanishes.

Call \(g\) a \(k\)-junta if it depends on at most \(k\) coordinates. For every Boolean-valued \(f\) and \(0 {\lt} \varepsilon \le 1\), \(f\) is \(\varepsilon \)-close to a Boolean-valued \(2^{O(\mathbf{I}[f]/\varepsilon )}\)-junta.