For every \(N \ge 6\) there is a function \(f : \{ 0,1\} ^N \to \{ 0,1\} \) that no fan-in-two AND/OR circuit of size at most \(\lfloor 2^N / (5N) \rfloor \) computes, where the size \(G + 1\) of a single-output circuit counts its output gate. Consequently \(\mathrm{size}(f) {\gt} \lfloor 2^N / (5N) \rfloor \).

For every \(N \ge 16\), every \(f : \{ 0,1\} ^N \to \{ 0,1\} \) satisfies \(\mathrm{size}(f) \le \lfloor 18 \cdot 2^N / N \rfloor \) over the fan-in-two AND/OR basis.

For every \(\varepsilon {\gt} 0\) and all sufficiently large \(N\), every \(f : \{ 0,1\} ^N \to \{ 0,1\} \) satisfies \(\mathrm{size}(f) \le (1 + \varepsilon )\, 2^N / N\).

For all sufficiently large \(N\), some \(f : \{ 0,1\} ^N \to \{ 0,1\} \) satisfies \(2^N / N {\lt} N + 2\, \mathrm{size}(f)\), that is, \(\mathrm{size}(f) {\gt} (2^N / N - N) / 2\), with \(2^N / N\) a real quotient.

Let the slice complexity of a language \(L\) at length \(n \ge 1\) be the size complexity of its length-\(n\) slice, and \(0\) at \(n = 0\), where a circuit family answers with a stored bit. Then \(L \in \mathsf{SIZE}(s)\) exactly when the slice complexity is at most \(s(n)\) at every \(n\). If \(L \in \mathsf{SIZE}(s)\), then every length-\(n\) slice, \(n = 0\) included, is decided by a CSLib De Morgan circuit with at most \(n + 2s(n) + 1\) gates; conversely, CSLib circuits with at most \(s(n)\) gates at every length \(n \ge 1\) put \(L\) in \(\mathsf{SIZE}(s + 1)\).

For every \(\varepsilon {\gt} 0\) there is one threshold \(N_0\) such that every language has slice complexity at most \((1 + \varepsilon ) 2^n / n\) at every length \(n \ge N_0\). Hence every language is in \(\mathsf{SIZE}(s)\) for some \(s\) with \(s(n) \le (1 + \varepsilon ) 2^n / n\) for all large \(n\), and for some \(s = O(\lfloor 2^n / n \rfloor )\). Conversely, a single language lies outside \(\mathsf{SIZE}(s)\) for every \(s\) with \(n + 2s(n) \le 2^n / n\) for all large \(n\), in particular for every \(s = o(\lfloor 2^n / n \rfloor )\).

For every \(n\), every circuit over the imported library’s De Morgan signature computing \(n\)-input parity has at least \(3(n - 1)\) AND and OR gates; constant, identity, and negation gates are free.

No nonuniform family of unbounded fan-in AND/OR circuits with negations at the inputs, with polynomially many AND and OR gates (negations free) and constant AND/OR depth (negations add no depth), computes parity at every input length. The same holds when negation gates may occur anywhere in the circuits. This is stated for the imported library’s own \(\mathsf{AC}^0\) model; deriving Theorem 336 for \(\mathsf{AC}^0\) as defined here from it is part of the consolidation plan.

Consider circuits of the imported library’s \(\mathsf{AC}^0\) model: unbounded fan-in AND and OR gates and negation gates anywhere, where \(S\) counts the AND and OR gates and the depth counts AND and OR levels only. Let \(d \ge 2\) and \(t \ge 1\). Every such circuit with \(n \ge (20(t + 1))^{d - 1}\) inputs and depth at most \(d\) that computes \(n\)-input parity satisfies \(2^{t + 1} \le 20\, t\, S\). In particular, if \(n \ge 40^{d - 1}\) and \(q = \lfloor \lfloor n^{1/(d-1)} \rfloor / 20 \rfloor \), with \(\lfloor n^{1/(d-1)} \rfloor \) the integer root, then \(S \ge \lfloor 2^q / (20(q - 1)) \rfloor \). This bound is of order \(2^{\Omega (n^{1/(d-1)})}\), but no asymptotic form is stated. It is not transferred to the circuits of this library; see Theorem 337.

Let \(t \ge 4\) and \(N = 2^{20t}\). Every circuit over the imported library’s binary AND/OR signature (fan-in-two AND and OR gates, no constants and no negations, every gate counted) whose inputs are the \(\binom {N}{2}\) edge variables of an \(N\)-vertex graph and which computes \(2^{4t}\)-CLIQUE has more than \(2^{t \cdot 2^t}\) gates.

Suppose that, for all large \(n\), the length-\(n\) member of a family of Boolean functions is \(K(n)\)-rectangle-free (under every split of its inputs, every rectangle of accepted inputs has a side with fewer than \(K(n)\) elements), with \(K(n) \le n^c\) for a natural number \(c\), and has at least \(2^{n - 2}\) accepting inputs. Then for all large \(n\) every formula over the full binary basis (all sixteen binary gates, constant leaves allowed) computing the length-\(n\) member satisfies \(n^2 \le 64(c + 3)\log _2 n \cdot L\), where \(L\) counts variable leaves and constants are free; that is, it has at least \(n^2 / (64(c + 3)\log _2 n)\) variable leaves. This is a conditional statement about any such family: no explicit rectangle-free family is formalized.

Consider the imported library’s De Morgan formulas, trees of literal leaves \(x_i\) and \(\neg x_i\), constant leaves, and binary AND and OR gates, with depth the length of a longest root-to-leaf path and size the number of leaves, constants included. In the Karchmer–Wigderson game of \(f\), Alice holds \(x\) with \(f(x) = 1\), Bob holds \(y\) with \(f(y) = 0\), and a deterministic protocol must output a coordinate where \(x\) and \(y\) differ. For every \(f\) on \(n \ge 1\) inputs, the minimum depth of a formula computing \(f\) equals the minimum depth of a protocol for this game, and the minimum size of a formula equals the minimum number of leaves of a protocol. The hypothesis \(n \ge 1\) is used because a protocol leaf names an input position; the fact that no protocol exists at \(n = 0\) is a remark, not a formalized statement.

For real exponents \(1 \le a {\lt} b\), the class of Boolean function families, one function for each input length, whose De Morgan circuit complexity in the imported library’s signature (every gate counted, constants and identities included) is at most \(C \lfloor n^a \rfloor \) for some constant \(C\) and all large \(n\) is strictly contained in the corresponding class for \(\lfloor n^b \rfloor \). The families are nonuniform and no explicit separating family is given.

Over any signature and interpretation, conditional complexity obeys the triangle inequality: computing \(h\) given \(f\) costs at most computing \(h\) given \(g\) plus computing \(g\) given \(f\). Over \(\mathbb {F}_2\), take any signature whose operations have arity at most two, interpreted over \(\mathbb {F}_2\), in which some one-gate circuit computes \(x_0 + x_1\). Then the conditional complexity of a nonzero linear form \(t \cdot x\) given linear helpers \(s_1 \cdot x, \ldots , s_k \cdot x\) is exactly

where \(\lvert \cdot \rvert \) is Hamming weight: the fewest helpers and inputs whose sum is the target, minus one. Every gate is counted, constant gates included. The signature may contain other operations as well, nonlinear ones included; the single-gate addition is a hypothesis of the theorem.

Every arithmetic circuit over a field, with addition, multiplication, and constant gates, whose output equals \(p\) as a formal polynomial has at least \(\lceil \operatorname {rank} H_p(a) / 2 \rceil \) multiplication gates, where \(H_p(a)\) is the Hessian of \(p\) at any point \(a\). Additions and constants are free, but every multiplication gate is counted, including multiplication by a constant. This is weaker than the classical form of the bound, which counts only nonscalar multiplications.

Over a field of characteristic zero, any expression of \(x_1 x_2 \cdots x_{2n}\) as a polynomial identity \(\sum _{i \in I} a_i \ell _i^{2n}\), with scalars \(a_i\) and linear forms \(\ell _i\) without constant term, has \(\lvert I \rvert \ge \binom {2n}{n}\). This bounds the number of terms of this restricted representation, not arithmetic circuit size.

Circuits are over the imported library’s De Morgan signature with its standard cost: negation, AND, and OR gates cost one, constants and identities are free. For \(f\) on \(n\) inputs and \(t \ge 1\), the mass complexity of \(f\) at \(t\) copies is the minimum cost of one circuit that evaluates \(f\) independently on \(t\) disjoint blocks of \(n\) inputs.

For every real \(0 \le \gamma {\lt} 1\) and \(\varepsilon {\gt} 0\) there is a threshold such that for every \(n\) above it, every \(f\) on \(n\) inputs, and every \(1 \le t \le 2^{\gamma n}\), the mass complexity of \(f\) at \(t\) copies is at most \((1/(1 - \gamma ) + \varepsilon )\, 2^n / n\). In a coarser discrete form, for all natural numbers \(a {\lt} b\) there is a constant \(C\) such that at every length \(n \ge 1\), every \(f\) on \(n\) inputs, and every \(1 \le t \le 2^{\lfloor a n / b \rfloor }\), the mass complexity is at most \(C \lfloor 2^n / n \rfloor \).

With mass complexity as in Theorem 308, let \(D : \mathbb {N} \to \mathbb {N}\) satisfy \(D(n) = o(n / \log n)\) in the discrete form: for every natural number \(M \ge 1\), eventually \(M \cdot D(n) \cdot \lfloor \log _2 n \rfloor \le n\). Then for every natural number \(P \ge 1\), for all large \(n\), every \(f\) on \(n\) inputs, and every \(1 \le t \le 2^{D(n)}\), the mass complexity of \(f\) at \(t\) copies is at most \((1 + 1/P)\, 2^n / n\), stated without division as \(P\, n \cdot \mathrm{mass}(f, t) \le (P + 1)\, 2^n\).

Assume that for every \(\xi {\gt} 0\) all sufficiently large simple 3-regular graphs on \(h\) vertices have pathwidth at most \((1/6 + \xi )h\), that is, a path decomposition whose bags have at most \((1/6 + \xi )h + 1\) vertices. Then every rectangle-free Boolean function family with polynomial rectangle threshold and at least \(2^{n-2}\) accepting inputs, as in Theorem 300, needs circuits of more than \((4 - \varepsilon )n\) gates over the full binary basis (all sixteen binary gates, every gate counted), for every \(\varepsilon {\gt} 0\) and all large \(n\). The pathwidth bound is an explicit hypothesis of the theorem. It is the published theorem of Fomin and Høie on the pathwidth of cubic graphs, which is not formalized here. As for Theorem 300, no explicit rectangle-free family is formalized, so this is a conditional statement about any such family.

Over any basis, the number of essential inputs of the function \(\{ 0,1\} ^N \to \{ 0,1\} ^M\) computed by a circuit is at most the circuit’s total fan-in, the number of gate-input occurrences with output gates included. For circuits over the AND/OR basis of fan-in at most \(k\), it is at most \(k\) times the size \(G + M\).

Every fan-in-two AND/OR circuit computing \(N\)-bit parity or its complement, \(N \ge 1\), has size at least \(2N - 1\), that is, at least \(2(N - 1)\) internal gates. Hence \(\mathrm{size}(\oplus _N) \ge 2N - 1\).

Let \(G\) be a finite acyclic digraph with \(S\) edges whose longest simple path has at most \(2^k\) vertices, and let \(r \le k\). There is a set \(F\) of edges of \(G\) with \(k\, |F| \le r S\) whose removal leaves a digraph whose longest simple path has at most \(2^k / 2^r\) vertices.

Every Boolean formula \(\varphi \) of size \(s\) has an equivalent formula of depth at most \(15 + 12 \lceil \log _2 s \rceil \) and size at most \(80 s^8 - 4\).

Every monotone formula computing \(f : \{ 0,1\} ^N \to \{ 0,1\} \) yields a protocol for the monotone Karchmer–Wigderson game of \(f\) of the same depth, and every such protocol yields a monotone formula of the same depth computing \(f\). Hence, for every \(d \in \mathbb {N}\), the game has a protocol of depth at most \(d\) if and only if some monotone formula of depth at most \(d\) computes \(f\). There is no monotonicity hypothesis on \(f\); by Lemma 320, both sides fail when \(f\) is not monotone.

For \(N \ge 1\), every DNF and every CNF computing \(N\)-bit parity has at least \(2^{N-1}\) terms, respectively clauses.

Let \(\varphi \) be a DNF of width \(w\) over \(N\) variables, no term of which contains a complementary pair of literals, and let \(q, s \in \mathbb {N}\). Call a restriction bad if the complete-block switching decision tree of the restricted formula has depth at least \(s\). This tree, rather than the canonical tree that queries one variable at a time, is the one used here: at the first surviving term it queries all of that term’s free variables before accepting or continuing. Then

Every DNF agrees with its sub-DNF of consistent terms, whose width is no larger, and the bound holds for that sub-DNF with \(w\) the original width. The same bounds hold for CNFs, where the condition is that no clause contains a complementary pair, and the switching tree and bad event are defined through the De Morgan dual DNF. Reading the counts as probabilities, which is not a separate formal statement: a uniform seed is bad with probability at most \((4(w+1)/q)^s\) when \(q \ge 1\).

Let \(C\) be an unbounded-fan-in AND/OR circuit, with negations only through the free per-input flags, with \(N\) inputs and \(G\) internal gates, and let output \(j\) have depth \(D\), counting the output gate. Some negation-normal unbounded formula computes output \(j\), has depth at most \(D\), and has size at most \((2(N + G) + 1)^{D+1}\).

Let \(\varphi \) be a negation-normal unbounded formula over \(N\) variables with depth at most \(d\), and let \(s \ge 2\) and \(q \in \mathbb {N}\). For any sequence of \(d\) restrictions, one per level, a staged compiler turns \(\varphi \) into a decision tree that computes \(\varphi \) under their composition, earlier restrictions taking precedence. For \(d\) independent sparse seeds, the number of \(d\)-tuples of seeds for which this decision tree has depth at least \(s\), multiplied by \(q^s\), is at most \(\mathrm{size}(\varphi )\, ((2q+1)^N)^d\, (4(s + 1))^s\). Consequently, if \(q {\gt} 0\) and

then some tuple of seeds leaves at least \(s\) variables free and reduces \(\varphi \) to a decision tree of depth less than \(s\).

Let \(\varphi \) be a negation-normal unbounded formula over \(N\) variables that computes parity, and let \(d \ge \mathrm{depth}(\varphi )\), \(s \ge 2\) and \(q \ge 1\). Then

The parity family is not in \(\mathsf{AC}^0\). The analogous statement for the imported library’s \(\mathsf{AC}^0\) model is Theorem 297; this one, for \(\mathsf{AC}^0\) as defined in this library, is not yet formalized.

For every \(d \ge 2\) there is \(\varepsilon _d {\gt} 0\) such that, for all sufficiently large \(N\), every unbounded-fan-in AND/OR circuit of depth \(d\) computing \(N\)-bit parity has size at least \(2^{\varepsilon _d N^{1/(d-1)}}\). Theorem 298 proves an explicit non-asymptotic form of this bound for the imported library’s \(\mathsf{AC}^0\) model; the statement here, for the circuits of this library, is not yet formalized.

The bound of Theorem 331 holds, up to an additive error \(\varepsilon \), when the free/fixed pattern and the fixed values are drawn from a distribution that \(\varepsilon \)-fools CNFs of size polynomial in \(N\) instead of the uniform product distribution (Trevisan–Xue). With an explicit generator fooling CNFs, such restrictions can be sampled from \(\mathrm{polylog}(N / \varepsilon )\) random bits.

Every monotone fan-in-two circuit computing the product of two \(n \times n\) Boolean matrices has at least \(n^3\) AND gates.

There is \(\varepsilon {\gt} 0\) such that for all \(k \le n^{1/4}\), every monotone circuit deciding whether an \(n\)-vertex graph, given by its adjacency bits, contains a \(k\)-clique has size at least \(2^{\varepsilon \sqrt{k}}\) (Razborov; Alon–Boppana; Arora–Barak Theorem 14.7). Only a weaker bound at special parameters, in the imported library’s model, is formalized: Theorem 299 gives more than \(2^{t \cdot 2^t}\) gates for \(k = 2^{4t}\) and \(n = 2^{20t}\), \(t \ge 4\), which for large \(t\) is below \(2^{\varepsilon \sqrt{k}} = 2^{\varepsilon 4^t}\).

Every clause derivable from \(\varphi \) is satisfied by every assignment satisfying \(\varphi \). In particular, if the empty clause is derivable from \(\varphi \), then \(\varphi \) is unsatisfiable.

If \(\varphi \) is unsatisfiable, then the empty clause is derivable from \(\varphi \).

If an unsatisfiable CNF over \(n\) variables whose clauses have at most \(k\) literals has a resolution refutation of size \(S\), then it has one of width at most \(k + O(\sqrt{n \log S})\).

Let \(\mathrm{PHP}^{n+1}_n\) be the CNF over variables \(p_{ij}\) (\(i \le n + 1\), \(j \le n\)) stating that every pigeon \(i\) sits in some hole and no hole holds two pigeons. Every resolution refutation of \(\mathrm{PHP}^{n+1}_n\) has size \(2^{\Omega (n)}\).

A polynomially bounded propositional proof system exists if and only if \(\mathsf{NP} = \mathsf{coNP}\).