Dependencies

\(A_0(n,d,w)\) is the maximum size of an \((n,d,w)\)-admissible code.

For a finite field \(\mathbb {F}_q\) and \(n \in \mathbb {N}\), the symplectic space is the vector space \(V = \mathbb {F}_q^n \times \mathbb {F}_q^n\), equipped with the symplectic form

A subspace \(S \le V\) is isotropic if \(\omega (u,v)=0\) for all \(u,v\in S\).

Classical codes \(C_Z, C_X \le \mathbb {F}_q^n\) satisfy the CSS condition if

Given \(C_Z \perp C_X\), the CSS stabilizer is the subspace of \(V\) generated by the \(X\)-type vectors \((x,0)\) for \(x \in C_Z\) and \(Z\)-type vectors \((0,z)\) for \(z \in C_X\).

The CSS stabilizer is isotropic if and only if the CSS condition holds.

If \(C_Z \perp C_X\), then \(\dim (\mathrm{cssStabilizer}) = \dim (C_Z) + \dim (C_X)\).

The CSS code \(Q(C_Z, C_X)\) encodes \(k = n - \dim (C_Z) - \dim (C_X)\) logical qudits, and has distance \(d = \min (d_Z, d_X)\) where \(d_Z\) (resp. \(d_X\)) is the minimum weight of a vector in \(C_Z^\perp \setminus C_X\) (resp. \(C_X^\perp \setminus C_Z\)).

If every \((n,d,w)\)-admissible code \(C\) has \(\left\lvert C\right\rvert \le K\), then \(A_0(n,d,w) \le K\).

The set of plain \(\mathrm{AC}^0\) gate operations on the alphabet \(\mathrm{Fin}\, 2\): the identity gate, the NOT gate \(x \mapsto 1 - x_0\), and, for every arity \(n\), the unbounded fan-in AND gate \(x \mapsto \prod _{i} x_i\).

The \(\mathrm{AC}^0[p]\) gate set: the \(\mathrm{AC}^0\) gates (identity, NOT, unbounded AND) together with the unbounded \(\mathrm{MOD}_p\) gate of every arity.

Every gate operation in \(\texttt{ACP.ACp\_ GateOps}\) is one of the following: the identity gate on a single input, the NOT gate \(x \mapsto 1 - x_0\), an unbounded AND gate \(x \mapsto \prod _i x_i\) of some arity \(n\), or a \(\texttt{ACP.modGateOp}\) of some arity \(n\).

The degree-one polynomial \(1 + \omega ^{-1} - \omega ^{-1} X_i\), which on \(\{ 1,\omega \} \) with \(\omega \neq 0\) computes \(x \mapsto x^{-1}\).

For any \(x : \mathrm{Fin}\, n \to K\), the polynomial \(\mathrm{affineInvPoly}\, \omega \, i\) evaluates to \(1 + \omega ^{-1} - \omega ^{-1} x_i\).

The total degree of \(\mathrm{affineInvPoly}\, \omega \, i\) is at most \(1\).

For \(s \subseteq \mathrm{Fin}\, n\), the product \(\prod _{i \in s}(1 + \omega ^{-1} - \omega ^{-1}X_i)\), i.e. the squarefree monomial after the affine inverse substitution.

For any \(x : \mathrm{Fin}\, n \to K\), the affine squarefree monomial indexed by \(s\) evaluates to \(\prod _{i \in s} (1 + \omega ^{-1} - \omega ^{-1} x_i)\).

The total degree of \(\mathrm{affineSquarefreeMonomial}\, \omega \, s\) is at most \(\left\lvert s\right\rvert \).

The De Morgan dual of the OR approximator: \(1 - \texttt{ACP.approxOr}\, (1 - P, S)\), where the approximator is applied to the negated inputs \(i \mapsto 1 - P_i\).

Fix an evaluation point \(y\). The number of seeds \(S\) for which \(\texttt{ACP.approxAnd}\, (P,S)\) evaluated at \(y\) differs from \(\prod _k \bigl(1 - (1 - P_k(y))^{p-1}\bigr)\), multiplied by \(2^\ell \), is at most \(2^{\mathrm{width}\cdot \ell }\).

The total degree of \(\texttt{ACP.approxAnd}\, (P,S)\) is at most \((p-1)\, \ell \cdot \sup _i \deg (P_i)\), the same bound as for the OR approximator.

The list of all polynomials \(\texttt{ACP.approxAnd}\, (P,S)\), one entry per random seed \(S\).

The list \(\texttt{ACP.approxAndPolyList}\) has length \(2^{\mathrm{width}\cdot \ell }\).

Given polynomials \(P_1,\dots ,P_{\mathrm{width}}\) over \(\mathbb {Z}/p\) and a random seed consisting of \(\ell \) subsets \(S_1,\dots ,S_\ell \) of the input positions, the approximator is

Evaluating \(\texttt{ACP.approxOr}\, (P, S)\) at a point \(y\) gives the same result as applying the value-level approximator \(\texttt{ACP.approxOr\_ val}\) to the evaluated inputs \(i \mapsto P_i(y)\) with the same seed \(S\).

For \(v : \mathrm{Fin}\, \mathrm{width} \to \mathbb {Z}/p\) and a seed \(S\), the value-level approximator differs from the OR detector if and only if \(v \ne 0\) and every seed subset has vanishing sum, i.e. \(\sum _{i \in S_k} v_i = 0\) for all \(k\).

Fix an evaluation point \(y\). The number of seeds \(S\) for which \(\texttt{ACP.approxOr}\, (P,S)\) evaluated at \(y\) differs from \(1 - \prod _k \bigl(1 - P_k(y)^{p-1}\bigr)\), multiplied by \(2^\ell \), is at most \(2^{\mathrm{width}\cdot \ell }\); that is, at most a \(2^{-\ell }\) fraction of seeds fail at \(y\).

The total degree of \(\texttt{ACP.approxOr}\) applied to \(P_1,\dots ,P_{\mathrm{width}}\) and a seed \(S\) is at most \((p-1)\, \ell \cdot \sup _i \deg (P_i)\).

The value-level analogue of the randomized OR approximator: for \(v : \mathrm{Fin}\, \mathrm{width} \to \mathbb {Z}/p\) and subsets \(S_1,\dots ,S_\ell \),

The list of all polynomials \(\texttt{ACP.approxOr}\, (P,S)\), one entry per random seed \(S\). It is a list rather than a set, so a polynomial arising from several seeds appears with the corresponding multiplicity.

The list \(\texttt{ACP.approxOrPolyList}\) has length \(2^{\mathrm{width}\cdot \ell }\).

The type of seeds \(\mathrm{Fin}\, \ell \to \mathrm{Finset}(\mathrm{Fin}\, \mathrm{width})\), i.e. \(\ell \) independent subset choices, has cardinality \(2^{\mathrm{width}\cdot \ell }\).

For a target \(f : \{ 0,1\} ^n \to \mathbb {Z}/p\) and a polynomial \(P \in (\mathbb {Z}/p)[X_1,\dots ,X_n]\), the number of Boolean inputs \(x\) with \(P(\mathrm{boolInput}(x)) \neq f(x)\).

If \(a \in \{ 0,1\} \subseteq \mathbb {Z}/p\), then \(1 - (1-a)^{p-1}\) equals the cast of \(\texttt{ACP.bitify}\, (a)\) into \(\mathbb {Z}/p\).

The map \(\mathbb {Z}/p \to \mathrm{Fin}\, 2\) sending \(a\) to \(1\) if \(a = 1\) and to \(0\) otherwise. It is intended to be applied only to values lying in \(\{ 0,1\} \).

Applying \(\mathrm{bitify}_p\) to \(\mathrm{boolVal}_p(b)\) returns the original bit \(b\), for every \(b : \mathrm{Fin}\, 2\).

For a Boolean input \(x : \mathrm{Fin}\, n \to \mathrm{Fin}\, 2\), the map \(\mathrm{boolInput}_p(x)\) sends each coordinate \(i\) to the image of the natural number \(x_i\) in \(\mathbb {Z}/p\).

The value in \(\mathbb {Z}/p\) represented by a bit \(b : \mathrm{Fin}\, 2\), namely the image of the natural number \(b\) under the canonical map \(\mathbb {N}\to \mathbb {Z}/p\).

For every bit \(b : \mathrm{Fin}\, 2\) the element \(\mathrm{boolVal}_p(b)\) lies in the subset \(\{ 0,1\} \) of \(\mathbb {Z}/p\).

For a circuit using only \(\mathrm{AC}^0[p]\) gates, the LayerPolyFamily at any layer \(d \le F.\mathrm{depth}\), obtained by starting from the input layer family and iterating the layer step \(d\) times.

If \(a \in \{ 0,1\} \subseteq \mathbb {Z}/p\), then casting \(\texttt{ACP.bitify}\, (a)\) back into \(\mathbb {Z}/p\) through \(\mathbb {N}\) recovers \(a\).

The embedding uses one extra layer for the inputs: \(C.\texttt{toFeedForward}.\texttt{depth} = C.\texttt{depth} + 1\).

For every circuit \(C\) on \(n\) inputs and every input \(x\), \(C.\texttt{toFeedForward}.\texttt{eval}_1\ x = C.\texttt{eval}\ x\).

For every input \(x\), every layer index \(m\) with \(0 \lt m\) and every node \(v\) of layer \(m\) of \(C.\texttt{toFeedForward}\), the value of \(v\) is \(C.\texttt{toFeedForward}.\texttt{evalNode}\ v\ x = C.\texttt{eval}\ x\).

For every circuit \(C\) on \(n\) inputs, \(C.\texttt{toFeedForward}.\texttt{size} \le C.\texttt{size} \cdot (C.\texttt{depth} + 1)\).

The degree budget for the approximating polynomials after \(d\) layers, defined as

For a nonzero \(v\), the number of seeds \(S : \mathrm{Fin}\, \ell \to \mathrm{Finset} (\mathrm{Fin}\, \mathrm{width})\) on which the value-level approximator disagrees with the OR detector, multiplied by \(2^\ell \), is at most the total number of seeds.

Without any nonvanishing hypothesis on \(v\): the number of seeds on which the value-level approximator disagrees with the OR detector, multiplied by \(2^\ell \), is at most the total number of seeds.

For a feed-forward circuit \(F\), a layer index \(d\), a node \(u\) at layer \(d+1\) and an input \(x\), the value of \(u\) is obtained by applying the gate operation attached to \(u\) to the values of its input nodes at layer \(d\).

If all values \(\mathrm{inputs}_i\) lie in \(\{ 0,1\} \subseteq \mathbb {Z}/p\), then \(\prod _i \bigl(1 - (1 - \mathrm{inputs}_i)^{p-1}\bigr)\) equals the cast into \(\mathbb {Z}/p\) of \(\prod _i \texttt{ACP.bitify}\, (\mathrm{inputs}_i)\), the Boolean AND of the booleanized inputs.

The polynomial \(1 - \bigl(\sum _i P_i\bigr)^{p-1}\) over \(\mathbb {Z}/p\), which computes the \(\mathrm{MOD}_p\) predicate exactly on Boolean values.

If all values \(\mathrm{inputs}_i\) lie in \(\{ 0,1\} \subseteq \mathbb {Z}/p\), then \(1 - \bigl(\sum _i \mathrm{inputs}_i\bigr)^{p-1}\) equals the cast into \(\mathbb {Z}/p\) of the output of the \(\mathrm{MOD}_p\) gate applied to the booleanized inputs \(i \mapsto \texttt{ACP.bitify}\, (\mathrm{inputs}_i)\).

The total degree of \(\texttt{ACP.exactMod}\) applied to \(P_1,\dots ,P_{\mathrm{width}}\) is at most \((p-1)\cdot \sup _i \deg (P_i)\).

For every \(n\), every error parameter \(\ell \), and every gate operation \(\mathrm{op}\) belonging to the \(\mathrm{AC}^0[p]\) gate set, there exists a GatePolyFamily \(p\, n\, \ell \, \mathrm{op}\).

There is a list \(Ps\) of polynomials, namely \(\texttt{ACP.approxAndPolyList}\, (P)\), of length \(2^{\mathrm{width}\cdot \ell }\), every entry of which has total degree at most \((p-1)\ell \cdot \sup _i \deg (P_i)\), and such that for every evaluation point \(y\) the number of seeds failing to compute the AND value at \(y\), times \(2^\ell \), is at most the length of \(Ps\).

There is a list \(Ps\) of polynomials, namely \(\texttt{ACP.approxOrPolyList}\, (P)\), of length \(2^{\mathrm{width}\cdot \ell }\), every entry of which has total degree at most \((p-1)\ell \cdot \sup _i \deg (P_i)\), and such that for every evaluation point \(y\) the number of seeds failing to compute the OR value at \(y\), times \(2^\ell \), is at most the length of \(Ps\).

Let \(\alpha ,\beta \) be finite types with \(\beta \) nonempty and let \(\mathrm{Fail} : \alpha \to \beta \to \mathrm{Prop}\) be decidable. If for every \(a\) the number of \(b\) with \(\mathrm{Fail}\, a\, b\) satisfies \(\left\lvert \{ b : \mathrm{Fail}\, a\, b\} \right\rvert \cdot C \le B\cdot \left\lvert \beta \right\rvert \), then there is a single \(b\) with \(\left\lvert \{ a : \mathrm{Fail}\, a\, b\} \right\rvert \cdot C \le B\cdot \left\lvert \alpha \right\rvert \).

Every function \(f : \{ 1,\omega \} ^n \to K\) agrees on the cube with the evaluation of some polynomial \(P \in K[X_1,\dots ,X_n]\), i.e. \(P(x) = f(x)\) for all \(x\) in the cube.

If \(p \neq q\) are primes, then there is \(\omega \in \mathbb {F}_{p^{q-1}}\) with \(\omega ^{q} = 1\) and \(\omega \neq 1\).

The same statement for a circuit with a unique output node: there is a nonempty finite seed type and polynomials \(P(s)\) of total degree at most \(\mathrm{circuitDegreeBound}(p,\ell ,F.\mathrm{depth})\) such that for every Boolean input \(x\),

Same statement for a circuit with a unique output node: there exist a finite nonempty seed type \(\mathrm{Seed}\) and polynomials \(P : \mathrm{Seed} \to \mathbb {Z}/p[X_1,\dots ,X_n]\), each of total degree at most \(\mathrm{circuitDegreeBound}\, p\, \ell \, F.\mathrm{depth}\), such that for every Boolean input \(x\) the number of seeds \(s\) with \(P_s(\mathrm{boolInput}_p(x)) \ne F.\mathrm{eval}_1(x)\) obeys

Let \(F\) be a feed-forward circuit over \(\mathrm{Fin}\, 2\) with finite node sets, finite output type \(\mathrm{out}\), using only \(\mathrm{AC}^0[p]\) gates, and let \(\ell \) be an error parameter. Then there is a nonempty finite seed type and a family \(P\) of polynomials \(P(s,o)\) over \(\mathbb {Z}/p\) such that every \(P(s,o)\) has total degree at most \(\mathrm{circuitDegreeBound}(p,\ell ,F.\mathrm{depth})\) and, for each Boolean input \(x\),

Let \(p\) be prime and let \(F\) be a feed-forward circuit with finite node layers and a finite output type, all of whose gates lie in the \(\mathrm{AC}^0[p]\) gate set. For every \(\ell \) there exist a finite nonempty seed type \(\mathrm{Seed}\) and polynomials \(P : \mathrm{Seed} \to \mathrm{out} \to \mathbb {Z}/p[X_1,\dots ,X_n]\) such that every \(P_{s,o}\) has total degree at most \(\mathrm{circuitDegreeBound}\, p\, \ell \, F.\mathrm{depth}\), and for every Boolean input \(x\) the seeds on which some output node is computed incorrectly, i.e. \(P_{s,o}(\mathrm{boolInput}_p(x)) \ne F.\mathrm{eval}(x)(o)\) for some \(o\), satisfy

Let \(\mathrm{op}\) be a gate in \(\texttt{ACP.ACp\_ GateOps}\) and let \(P_i\) be polynomials over \(\mathbb {Z}/p\) computing its inputs. Then there exist a nonempty finite seed type \(\mathrm{Seed}\) with decidable equality and a family \(P : \mathrm{Seed} \to \mathrm{MvPolynomial}(\mathrm{Fin}\, n, \mathbb {Z}/p)\) such that every \(P(s)\) has total degree at most \((p-1)\ell \cdot \sup _i \deg (P_i)\), and for every Boolean input \(x\), writing \(y_j = x_j\) cast into \(\mathbb {Z}/p\) and \(\mathrm{inputs}_i = P_i(y)\), if all \(\mathrm{inputs}_i\) lie in \(\{ 0,1\} \) then the number of seeds \(s\) with \(P(s)(y)\) different from the gate value \(\mathrm{op}.\mathrm{func}(i \mapsto \texttt{ACP.bitify}(\mathrm{inputs}_i))\), multiplied by \(2^\ell \), is at most \(\left\lvert \mathrm{Seed}\right\rvert \).

The single-output theorem restated with the seed distribution presented as a nonempty list \(Ps\) of polynomials with multiplicity, one entry per seed: every \(P \in Ps\) has total degree at most \(\mathrm{circuitDegreeBound}(p,\ell ,F.\mathrm{depth})\), and for every Boolean input \(x\) the number of entries of \(Ps\) disagreeing with \(F.\mathrm{eval}_1\, x\), multiplied by \(2^{\ell }\), is at most \(\mathrm{gateCountBefore}\, F\, F.\mathrm{depth} \cdot \left\lvert Ps\right\rvert \).

The list formulation of the previous theorem: for a circuit \(F\) with a unique output node whose gates all lie in the \(\mathrm{AC}^0[p]\) gate set, there is a nonempty list \(Ps\) of polynomials in \(\mathbb {Z}/p[X_1,\dots ,X_n]\), each of total degree at most \(\mathrm{circuitDegreeBound}\, p\, \ell \, F.\mathrm{depth}\), such that for every Boolean input \(x\) the sublist of \(P \in Ps\) with \(P(\mathrm{boolInput}_p(x)) \ne F.\mathrm{eval}_1(x)\) satisfies

Let \(F\) be a feed-forward circuit with a unique output that only uses \(\mathrm{AC}^0[p]\) gate operations. Then there exists a polynomial \(P\) over \(\mathbb {Z}/p\) with \(\deg P \le \mathrm{circuitDegreeBound}\, p\, \ell \, (\mathrm{depth}\, F)\) whose bad-input count against the function computed by \(F\) satisfies \(\mathrm{badInputCount}\cdot 2^{\ell } \le \left\lvert F\right\rvert \cdot 2^{n}\), where \(\left\lvert F\right\rvert \) is the circuit size.

Let \(P\) be a family of polynomials over \(\mathbb {Z}/p\) indexed by a nonempty finite seed type. If for every Boolean input \(x\) the number of seeds \(s\) with \((P_s)(\mathrm{boolInput}(x)) \neq f(x)\), times \(2^{\ell }\), is at most \(B\cdot \left\lvert \mathrm{Seed}\right\rvert \), then some seed \(s\) satisfies \(\mathrm{badInputCount}(f, P_s)\cdot 2^{\ell } \le B\cdot 2^{n}\).

Every function \(f : \{ 1,\omega \} ^n \to K\) on the root cube is represented by a squarefree (multilinear) polynomial: there are coefficients \(c\) indexed by finsets of \(\mathrm{Fin}\, n\) such that \((\texttt{ACP.squarefreePolynomial}\ c)(x) = f(x)\) for all \(x\) in the root cube.

If \(p \neq q\) are primes, then the unit group of \(\mathbb {F}_{p^{q-1}}\) contains an element \(u\) with \(\mathrm{ord}(u) = q\).

A feedforward circuit from inp to out over \(\alpha \) consists of a depth \(d \in \mathbb {N}\), a family of node types indexed by the layers \(\mathrm{Fin}\, (d+1)\), and, for every layer \(i \lt d\), a gate for each node of layer \(i+1\) whose inputs are wired to nodes of layer \(i\). Layer \(0\) is required to be the input type inp and the last layer the output type out.

The function \(\texttt{out} \to \alpha \) sending each output node to its value in the last layer under the input assignment \(xs\).

For an input assignment \(xs : \texttt{inp} \to \alpha \), the value of a node at layer \(d\) is defined by recursion on \(d\): a layer-\(0\) node is read off directly from \(xs\), and a node at layer \(n+1\) evaluates its gate on the values of the layer-\(n\) nodes.

When the output type is a Unique type, the single value \(F.\texttt{eval}\, xs\, \texttt{default} \in \alpha \) computed by the circuit.

The proposition that the node type of every layer \(i\) is finite.

Given a gate \(g\) and an assignment \(xs\) of values to the nodes of its input domain, the value of \(g\) is \(g.\texttt{op}.\texttt{func}\, (xs \circ g.\texttt{inputs})\), i.e. the gate operation applied to the values read along the input wires.

The gate operation of arity \(\mathrm{PUnit}\) that returns its single input unchanged.

Given a Boolean feedforward circuit \(F\), a flag \(\texttt{isAnd}\) on each non-input node and a finiteness witness \(\texttt{gfin}\) for each gate’s arity, \(F.\texttt{IsAndOrGate}\) asserts that every gate operation is the conjunction of its inputs when the flag is true and their disjunction when it is false, the inputs being enumerated by \(\texttt{gfin}\). This is the gate restriction under which \(F\) can be converted into a BoolCircuit.Circuit.

For a set \(S\) of gate operations, \(\texttt{onlyUsesGates}\ S\) asserts that the operation of every gate of the circuit belongs to \(S\).

The size of \(F\) is the cardinality \(\mathrm{Nat.card}\) of the sigma type of all non-input nodes, i.e. the total number of nodes lying in layers \(1,\dots ,\texttt{depth}\).

For an AND/OR feedforward circuit \(F\) and a chosen output node \(o : \texttt{out}\), the tree-shaped \(\texttt{Circuit}\ n\) obtained by tree-unrolling \(o\) from the last layer down to the inputs.

If every gate of \(F\) is an AND or OR gate, then for every output node \(o\) and every input \(x\),

If every gate of \(F\) has at most \(k\) input wires, then for every output node \(o\) the tree-unrolled circuit satisfies \((F.\texttt{toCircuit}\ \texttt{isAnd}\ \texttt{gfin}\ o).\texttt{size} \le (k+1)^{F.\texttt{depth}}\).

Let \(\alpha , \beta , \mathrm{Cand}\) be finite and let \(\mathrm{center} : \mathrm{Cand} \to (\alpha \to \beta )\). If every ball \(\{ f : \left\lvert \{ a : \mathrm{center}\, c\, a \neq f(a)\} \right\rvert \le e\} \) has at most \(B\) elements, and every \(f : \alpha \to \beta \) lies in one of these balls, then \(\left\lvert \alpha \to \beta \right\rvert \le \left\lvert \mathrm{Cand}\right\rvert \cdot B\).

For a finset \(s\) and a decidable predicate \(q\), the length of the filtered list \(s.\mathrm{toList}\) by \(q\) equals the cardinality of the filtered finset \(s\) by \(q\).

For finite types \(\alpha , \beta \), a center function \(\mathrm{center} : \alpha \to \beta \) and a radius \(e\), the number of functions \(f : \alpha \to \beta \) that differ from the center on at most \(e\) coordinates is bounded by

This is a slightly coarser form of the usual bound, which carries \((\left\lvert \beta \right\rvert -1)^t\) in place of \(\left\lvert \beta \right\rvert ^t\).

A gate over alphabet \(\alpha \) with input domain domain consists of a gate operation op (an arity type \(\iota \) together with a function \((\iota \to \alpha ) \to \alpha \)) and a wiring map \(\iota \to \texttt{domain}\) that assigns to each input slot the node it reads from.

For a circuit \(F\) with finite node sets, \(\mathrm{gateCountBefore}\, F\, d\) counts the non-input gates in layers \(1,\dots ,d\): it is \(0\) for \(d = 0\) and, recursively, the count for \(d\) plus the number of nodes at layer \(d+1\).

For a feed-forward circuit \(F\) with all node layers finite, taking \(d = F.\mathrm{depth}\) gives

Let \(F\) be a feed-forward circuit with all node layers finite. Then for every \(d\) with \(d \le F.\mathrm{depth}\),

that is, the number of non-input gates in the first \(d\) layers is the sum of the cardinalities of those layers.

\(\mathrm{gateCountBefore}\, F\, (d+1)\) equals \(\mathrm{gateCountBefore}\, F\, d\) plus the cardinality of the node set at layer \(d+1\).

\(\mathrm{gateCountBefore}\, F\, 0 = 0\): the input layer contributes no gates.

For a feed-forward circuit \(F\), a bound \(d \le F.\mathrm{depth}\) and an index \(j : \mathrm{Fin}\, d\), the layer index \(\mathrm{gateLayerIdx}\, F\, h_d\, j \in \mathrm{Fin}(F.\mathrm{depth}+1)\) is \(j+1\), i.e. the \((j+1)\)-st node layer of \(F\). It packages the non-input layers \(1, \dots , d\) as indices into \(F.\mathrm{nodes}\) so that they can be summed over.

A GatePolyFamily for a gate operation \(\mathrm{op}\) packages a nonempty finite seed type together with, for each tuple of incoming polynomials and each seed, an approximating polynomial in \(n\) variables over \(\mathbb {Z}/p\) subject to two guarantees: its total degree is at most \((p-1)\ell \cdot \sup _i \deg (\text{polys}_i)\), and for every Boolean input \(x\) at which all incoming polynomials evaluate into \(\{ 0,1\} \), the number of seeds on which the approximator disagrees with the true gate value, multiplied by \(2^{\ell }\), is at most the number of seeds. Crucially the seed type depends only on the gate, not on the incoming polynomials.

A choice of GatePolyFamily for each \(\mathrm{AC}^0[p]\) gate operation, obtained from the preceding existence statement.

The LayerPolyFamily at layer \(0\): a single seed, with each input node represented exactly by the corresponding variable \(X_i\), so that no seed is ever bad.

A LayerPolyFamily for a circuit \(F\) at layer \(d\) consists of a nonempty finite seed type and, for each seed, a polynomial for every node of layer \(d\), such that each polynomial has total degree at most \(\mathrm{circuitDegreeBound}(p,\ell ,d)\) and, for every Boolean input \(x\), the number of seeds for which some layer-\(d\) node is mispredicted, multiplied by \(2^{\ell }\), is at most \(\mathrm{gateCountBefore}\, F\, d\) times the number of seeds.

For a list \(l\), a map \(f\) and a decidable predicate \(P\), the length of the filter of \(l.\mathrm{map}\, f\) by \(P\) equals the length of the filter of \(l\) by the pulled-back predicate \(a \mapsto P(f(a))\).

Assume \(\omega \ne 1\). Every polynomial \(Q\) with \(\deg Q \le D\) agrees on the root cube \(\{ 1,\omega \} ^n\) with a low-degree squarefree polynomial: there are coefficients \(c\) on \(\texttt{ACP.LowDegreeSupport}\ n\ D\) such that \((\texttt{ACP.lowDegreeSquarefreePolynomial}\ c)(x) = Q(x)\) for all \(x\) in the cube.

The predicate asserting that every polynomial \(P\) of total degree at most \(d\) has \(E \le \mathrm{badInputCount}(f, P)\), i.e. \(f\) cannot be computed by a degree-\(d\) polynomial on more than \(2^n - E\) points of the Boolean cube.

For a finite type \(K_0\), the number of coefficient functions on low-degree supports is

Given coefficients \(c\) indexed by \(\texttt{ACP.LowDegreeSupport}\ n\ D\), the multivariate polynomial

i.e. the sum of the squarefree monomials \(\texttt{ACP.squarefreeMonomial}\ s\) weighted by \(c\), with the terms of support size \(\gt D\) set to \(0\).

The constructor \(\texttt{ACP.lowDegreeSquarefreePolynomial}\) is additive in its coefficient argument: the polynomial attached to \(c_1 + c_2\) is the sum of the polynomials attached to \(c_1\) and to \(c_2\).

For a finite index set \(S\) and coefficient functions \(c_i\), the polynomial attached to the pointwise sum \(\sum _{i \in S} c_i\) equals \(\sum _{i \in S}\) of the polynomials attached to the individual \(c_i\).

For any coefficient function \(c\) on \(\texttt{ACP.LowDegreeSupport}\ n\ D\), the polynomial \(\texttt{ACP.lowDegreeSquarefreePolynomial}\ c\) has total degree at most \(D\).

The constructor \(\texttt{ACP.lowDegreeSquarefreePolynomial}\) sends the identically zero coefficient function to the zero polynomial.

For \(n, D \in \mathbb {N}\), the type of supports of squarefree monomials of degree at most \(D\): the subtype of finsets \(s \subseteq \mathrm{Fin}\, n\) with \(\left\lvert s\right\rvert \le D\). In the displays below this type is written \(\mathcal{S}_{n,D}\).

The number of low-degree squarefree supports satisfies

The map sending a low-degree support \(s\) to the pair consisting of its exact cardinality \(\left\lvert s\right\rvert \in \mathrm{Fin}(D+1)\) together with \(s\) itself, viewed as an element of \(\{ t : \mathrm{Finset}(\mathrm{Fin}\, n) \mid \left\lvert t\right\rvert = \left\lvert s\right\rvert \} \). It is used as an injection for the binomial-sum bound rather than as a full equivalence.

The gate operation of arity width on Boolean inputs that outputs \(1\) when the sum of its inputs, cast into \(\mathbb {Z}/p\), is \(0\), and outputs \(0\) otherwise.

The Galois field \(\mathbb {F}_{p^{q-1}}\), the standard field choice for the \(\mathrm{MOD}_q\) lower bound.

For a prime \(q\), the Boolean function \(\mathrm{MOD}_q\) on \(n\) inputs viewed as a function \(\{ 0,1\} ^n \to \mathbb {Z}/p\): the output bit of the gate operation \(\mathrm{modGateOp}\ q\ n\) is cast into \(\mathbb {Z}/p\).

Assume \(\omega \ne 1\). If a monomial \(a\, X^m\) has total exponent sum \(\sum _i m_i \le D\), then it agrees on the root cube \(\{ 1,\omega \} ^n\) with a squarefree polynomial built only from supports of size at most \(D\): there exist coefficients \(c\) on \(\texttt{ACP.LowDegreeSupport}\ n\ D\) with \((\texttt{ACP.lowDegreeSquarefreePolynomial}\ c)(x) = (a\, X^m)(x)\) for every \(x\) in the cube.

For primes \(p\) and \(q\), the field \(\mathrm{ModqField}\, q\) has exactly \(p^{q-1}\) elements.

Assume \(\omega \neq 0\), that every function on \(\{ 1,\omega \} ^n\) has a squarefree representative, and the counting hypothesis that not every function on the cube admits a degree-\(\le n/2 + d\) approximant with at most \(e\) bad points. Then no polynomial of total degree at most \(d\) approximates the top monomial \(x \mapsto \prod _i x_i\) within \(e\) bad points.

Let \(K\) be finite, \(\omega \ne 0\), \(\omega \ne 1\). Suppose \(\sum _{t=0}^{e} \binom {2^n}{t}\, \left\lvert K\right\rvert ^{\, t} \le B\) and

Then no polynomial \(P\) with \(\deg P \le d\) approximates the product \(x \mapsto \prod _i x_i\) on the root cube with at most \(e\) errors, i.e. there is no such \(P\) with \(\texttt{ACP.rootCubeBadCount}\ (\prod _i x_i)\ P \le e\).

The same conclusion as the previous theorem, with the abstract counting hypothesis replaced by explicit data: a finite candidate family representing all degree-\(\le n/2 + d\) polynomials on the cube, a bound \(B\) on the size of each Hamming ball of radius \(e\), and the strict inequality \(\left\lvert \{ 1,\omega \} ^n \to K\right\rvert \gt \left\lvert \mathrm{Cand}\right\rvert \cdot B\).

Recursively expands a node \(v\) of layer \(m\) of a Boolean feedforward circuit into a tree-shaped \(\texttt{Circuit}\ n\): a layer-\(0\) node becomes the positive literal of the corresponding input variable, and a node at a higher layer becomes an AND/OR node whose children are the unrollings of the nodes on its input wires. Nodes feeding several downstream gates are duplicated.

If every gate of \(F\) is an AND or OR gate as recorded by \(\texttt{isAnd}\) and \(\texttt{gfin}\), then for every node \(v\) at layer \(m\) and every input \(x : \mathrm{Fin}\, n \to \{ 0,1\} \),

If every gate of \(F\) has at most \(k\) input wires, i.e. \(\mathrm{card}\, (F.\texttt{gates}\ d\ v).\texttt{op}.\iota \le k\) for all \(d\) and \(v\), then the unrolling of any node at layer \(m\) has size at most \((k+1)^m\).

For every \(a \in \mathbb {Z}/p\) with \(p\) prime,

For \(v : \mathrm{Fin}\, \mathrm{width} \to \mathbb {Z}/p\), the quantity \(1 - \prod _{k}\bigl(1 - v_k^{\, p-1}\bigr)\), which detects whether some coordinate of \(v\) is nonzero.

Fix a coordinate \(i\) and a decidable predicate \(\mathrm{Bad}\) on \(\beta _i\), and suppose \(\left\lvert \{ b : \mathrm{Bad}(b)\} \right\rvert \cdot C \le \left\lvert \beta _i\right\rvert \). Then the number of dependent functions \(f\) with \(\mathrm{Bad}(f_i)\) satisfies

Given for each coordinate \(i\) a decidable predicate \(\mathrm{Bad}_i\) on \(\beta _i\) with \(\left\lvert \{ b : \mathrm{Bad}_i(b)\} \right\rvert \cdot C \le \left\lvert \beta _i\right\rvert \), the number of dependent functions bad at some coordinate obeys

For an index \(i\) with decidable equality on the index type, the equivalence

sending a dependent function to its value at \(i\) together with its restriction to the remaining coordinates.

Let \(\mathrm{Bad}\) be a finite set of elements of \(\alpha \), let \(\mathrm{Fail} : \alpha \to \beta \to \mathrm{Prop}\) be decidable with \(\beta \) finite and nonempty, and let \(C\) be a natural number. If for every \(a \in \mathrm{Bad}\) we have \(\left\lvert \{ b : \mathrm{Fail}(a,b)\} \right\rvert \cdot C \le \left\lvert \beta \right\rvert \), then there exists a single \(b \in \beta \) with \(\left\lvert \{ a \in \mathrm{Bad} : \mathrm{Fail}(a,b)\} \right\rvert \cdot C \le \left\lvert \mathrm{Bad}\right\rvert \).

Let \(P\) be a predicate on \(\alpha \), \(Q\) a predicate on \(\alpha \times \beta \), and \(C, B\) natural numbers such that for every \(a\) with \(P(a)\) the fiber count satisfies \(\left\lvert \{ b : Q(a,b)\} \right\rvert \cdot C \le B\). Then

For finite types \(\alpha ,\beta \) and a decidable predicate \(P\) on \(\alpha \), the number of pairs \(z \in \alpha \times \beta \) with \(P(z_1)\) equals \(\left\lvert \{ a : P(a)\} \right\rvert \cdot \left\lvert \beta \right\rvert \).

For a prime \(q\) we have \(q - 1 \neq 0\); this is the side condition needed to compute the cardinality of \(\mathbb {F}_{p^{q-1}}\).

The subtype of vectors \(x : \mathrm{Fin}\, n \to K\) such that each coordinate satisfies \(x_i = 1\) or \(x_i = \omega \).

If \(\omega \neq 0\) and \(x\) lies in \(\{ 1,\omega \} ^n\), then for every coordinate \(i\),

If \(\omega \ne 1\) and \(K\) is finite, then the root cube has exactly \(2^n\) points: \(\left\lvert \{ 1,\omega \} ^n\right\rvert = 2^n\).

If \(\omega \neq 0\) and \(x \in \{ 1,\omega \} ^n\), then \(x_i \neq 0\) for every \(i\).

Suppose a finite family \((\mathrm{poly}\, c)_{c \in \mathrm{Cand}}\) represents, on the cube, every polynomial of total degree at most \(D\); suppose each Hamming ball of radius \(e\) around such a candidate has at most \(B\) elements; and suppose \(\left\lvert \{ 1,\omega \} ^n \to K\right\rvert \gt \left\lvert \mathrm{Cand}\right\rvert \cdot B\). Then it is not the case that every function on the cube has a degree-\(\le D\) approximant with at most \(e\) bad points.

Let \(K\) be finite and \(\omega \ne 1\). Suppose the ball bound \(\sum _{t=0}^{e} \binom {2^n}{t}\, \left\lvert K\right\rvert ^{\, t} \le B\) holds and the counting is strict,

Then it is not the case that every function \(f : \{ 1,\omega \} ^n \to K\) admits a polynomial \(Q\) with \(\deg Q \le D\) and \(\texttt{ACP.rootCubeBadCount}\ f\ Q \le e\).

If \(\omega \ne 1\) and \(K\) is finite, the number of functions \(\{ 1,\omega \} ^n \to K\) is \(\left\lvert K\right\rvert ^{2^n}\).

For \(\omega \neq 0\), \(x \in \{ 1,\omega \} ^n\) and \(s \subseteq \mathrm{Fin}\, n\),

The number of points \(x \in \{ 1,\omega \} ^n\) on which \(P(x) \neq f(x)\).

The finite set of functions \(f : \{ 1,\omega \} ^n \to K\) that differ from a given center function on at most \(e\) points of the cube.

For any center function on the root cube and any radius \(e\), the Hamming ball \(\texttt{ACP.rootCubeBall}\) of radius \(e\) around it satisfies

If \(\omega \ne 1\), the explicit equivalence \(\{ 1,\omega \} ^n \simeq (\mathrm{Fin}\, n \to \mathrm{Fin}\, 2)\) that records, for each coordinate, whether its value is \(1\) or \(\omega \).

The number of points \(x \in \{ 1,\omega \} ^n\) on which two functions \(f, g : \{ 1,\omega \} ^n \to K\) differ.

Assume \(\omega \neq 0\) and that every function on \(\{ 1,\omega \} ^n\) is represented on the cube by a squarefree polynomial. If \(P\) has total degree at most \(d\) and approximates the top monomial \(x \mapsto \prod _i x_i\) with at most \(e\) bad points, then every function \(f\) on the cube has a polynomial \(Q\) with \(\deg Q \le n/2 + d\) and at most \(e\) bad points.

For a feed-forward circuit \(F\) with all node layers finite,

so the total number of non-input gates equals the sum of the cardinalities of all non-input layers.

If a feed-forward circuit \(F\) over the \(\mathrm{AC}^0[p]\) gate set computes \(\mathrm{MOD}_q\) on all Boolean inputs, and if \(\mathrm{MOD}_q\) (viewed in \(\mathbb {Z}/p\)) admits the lower bound \(\mathrm{LowDegreeBadCountLB}\) with parameters \((\mathrm{circuitDegreeBound}\, p\, \ell \, (\mathrm{depth}\, F), E)\), then \(E \cdot 2^{\ell } \le \left\lvert F\right\rvert \cdot 2^{n}\).

Same hypotheses as the previous theorem, but with the bad-count bound taken in the relative form \(E = \delta \cdot 2^{n}\); the conclusion is then the clean size bound \(\delta \cdot 2^{\ell } \le \left\lvert F\right\rvert \).

Let \(\omega \neq 0\) and let \(c\) be a coefficient family. Then there are polynomials \(P_1, P_2\) of total degree at most \(n/2\) such that for every \(x \in \{ 1,\omega \} ^n\),

Let \(\omega \neq 0\) and let \(c\) be a coefficient family. Then there are polynomials \(P_1, R\) of total degree at most \(n/2\) such that for every \(x \in \{ 1,\omega \} ^n\),

so that the second factor is already evaluated at \(x\) itself rather than at the affine substitution.

For \(s \subseteq \mathrm{Fin}\, n\), the monomial \(\prod _{i \in s} X_i\).

For any \(x : \mathrm{Fin}\, n \to K\), the monomial indexed by \(s\) evaluates to \(\prod _{i \in s} x_i\).

The total degree of \(\prod _{i \in s} X_i\) is at most \(\left\lvert s\right\rvert \).

Given coefficients \(c_S\) indexed by subsets \(S \subseteq \mathrm{Fin}\, n\), the polynomial

Given a circuit \(F\) using only \(\mathrm{AC}^0[p]\) gates and a LayerPolyFamily at layer \(d\), this produces a LayerPolyFamily at layer \(d+1\). Its seed type is the product of the previous seed type with one gate seed per node of layer \(d+1\), and each node polynomial is the gate approximator applied to the layer-\(d\) polynomials of its inputs.

For a nonzero vector \(v : \mathrm{Fin}\, n \to \mathbb {Z}/p\), the number of subsets \(s \subseteq \mathrm{Fin}\, n\) with \(\sum _{i \in s} v_i = 0\) is at most half of all \(2^n\) subsets; formally, twice that count is at most the total number of subsets.

For a finite index type \(\iota \), a finite type \(\beta \) and a decidable predicate \(P\) on \(\beta \), the number of functions \(f : \iota \to \beta \) with \(P(f(i))\) for all \(i\) equals \(\left\lvert \{ b : P(b)\} \right\rvert ^{\left\lvert \iota \right\rvert }\).

An \(\texttt{AdaptiveAdversary}\ N\) is an online strategy for the adversary: it provides a loss-selection function \(\mathrm{loss} : (t : \mathbb {N}) \to \texttt{LossHistory}\ N\ t \to (\mathrm{Fin}\, N \to \mathbb {R}) \to \mathrm{Fin}\, N \to \mathbb {R}\) that maps the current round index, the past loss history, and the learner’s current mixed strategy to a loss vector, subject to the validity condition that every coordinate of the chosen loss vector lies in \([0, 1]\).

The \((i,j)\) entry of \(A\) counts arcs, i.e. walks of length one; matrix multiplication sums over an intermediate vertex, and every walk of length \(k\) decomposes uniquely as a shorter walk plus a final arc. This is the directed counterpart of exercise 1.6.2, and it is what makes §10.7’s ranking work: the \(i\)-th level score vector is \(A^{i}J\), counting directed walks of length \(i\) out of each player. Theorem 10.7 consumes it directly.

! Restated for a \(0/1\) matrix, Digraph having no arc multiplicities; for the strict digraphs of §10.7 this is no loss. The right-hand side is Nat.card of a subtype of Quiver.Path, which is finite because the length is pinned — but that finiteness may need to be supplied for Nat.card to behave.

For any finite zero-sum game \(G\) with \(M \ge 2\) rows and any \(\varepsilon \gt 0\), there exist mixed strategies \(p\) (row) and \(q\) (column) forming an \(\varepsilon \)-approximate saddle point: for all pure \(i \in \mathrm{Fin}\, M\) and \(j \in \mathrm{Fin}\, N\),

A social welfare function \(f\) is acyclic if no profile of transitive voter orderings produces a Condorcet cycle in society’s preferences. A cycle occurs when \(f(\mathrm{abVotes}(p)) = f(\mathrm{bcVotes}(p)) = f(\mathrm{caVotes}(p)) = 1\) (the cycle \(a\gt b\gt c\gt a\)) or all equal \(-1\) (the reverse cycle).

If \(f\) is \(\pm 1\)-valued and acyclic, then \(\mathrm{corr}(f) = -1/3\).

Proof sketch:

1. For any \(\pm 1\) triple \((a,b,c)\) avoiding the two all-equal cycles, \(ab + bc + ac = -1\).

2. Summing over all \(6^n\) profiles: \(\sum _p (f_{\! ab}\cdot f_{\! bc} + f_{\! bc}\cdot f_{\! ca} + f_{\! ab}\cdot f_{\! ca}) = -6^n\).

3. Each pairwise expected product equals \(\mathrm{corr}(f)\), so \(3\cdot \mathrm{corr}(f) = -1\), giving \(\mathrm{corr}(f) = -1/3\).

Let \(f:\{ 0,1\} ^n\to \mathbb {R}\) be a social welfare function that is odd (antisymmetric), \(\pm 1\)-valued, unanimous, and acyclic. Then \(f\) is a dictatorship: there exists a voter \(i_0\) such that \(f = \mathrm{dict}_{i_0}\).

Proof:

1. Acyclicity \(\Rightarrow \) \(\mathrm{corr}(f) = -1/3\) (Lemma ArrowTheorem.acyclic_implies_corrFunc).

2. \(\mathrm{corr}(f) = -1/3\) \(\Rightarrow \) \(\hat f(S) = 0\) for \(|S|\ne 1\) (Lemma ArrowTheorem.corrFunc_eq_neg_third_of_weight_one).

3. Degree-1 + unanimous + \(\pm 1\)-valued \(\Rightarrow \) dictator (Lemma ArrowTheorem.degree_one_implies_dictator).

\(\mathrm{abPref}(k)\), \(\mathrm{bcPref}(k)\), \(\mathrm{caPref}(k)\) give the Boolean preference of ordering \(k\in \{ 0,\dots ,5\} \) in the \(a\)-vs-\(b\), \(b\)-vs-\(c\), and \(c\)-vs-\(a\) comparisons, respectively.

Given a profile \(p\), the vote vectors \(\mathrm{abVotes}(p)\), \(\mathrm{bcVotes}(p)\), \(\mathrm{caVotes}(p) \in \{ 0,1\} ^n\) record each voter’s pairwise preference.

The Fourier correlation function of \(f\) is

For odd \(f\), only odd-level terms contribute.

If \(\mathrm{corr}(f) = -1/3\), then \(\hat f(S) = 0\) for all \(S\) with \(|S| \ne 1\). Combined with oddness (\(\hat f(\varnothing ) = 0\)), all Fourier weight lies on level 1: \(W_1[f] = 1\).

For any odd \(\pm 1\)-valued function,

Proof sketch: For odd \(|S|\ge 1\) we have \((-1/3)^{|S|}\ge -1/3\). Even-level coefficients vanish by oddness. Hence \(\mathrm{corr}(f) \ge (-1/3)\sum _S \hat f(S)^2 = -1/3\).

Suppose \(f\) is \(\pm 1\)-valued, unanimous, and \(\hat f(S) = 0\) for all \(|S|\ne 1\). Then \(f\) is a dictator.

Proof sketch: Write \(f = \sum _i a_i\chi _{\{ i\} }\) where \(a_i = \hat f(\{ i\} )\).

1. Parseval: \(\sum _i a_i^2 = 1\).

2. Unanimity: \(f(\mathbf{0}) = \sum _i a_i = 1\).

3. For each \(j\), the value \(f(e_j) = 1 - 2a_j \in \{ -1,1\} \) forces \(a_j\in \{ 0,1\} \).

4. From \(a_j\in \{ 0,1\} \) and \(\sum a_j^2 = \sum a_j = 1\): exactly one \(a_{j_0} = 1\) and the rest are \(0\).

5. Hence \(f = \chi _{\{ j_0\} } = \mathrm{dict}_{j_0}\).

For any \(f:\{ 0,1\} ^n\to \mathbb {R}\), \(\bigl(\tfrac 16\bigr)^n\sum _p f(\mathrm{abVotes}(p))\, f(\mathrm{caVotes}(p)) = \mathrm{corr}(f)\).

For any \(f:\{ 0,1\} ^n\to \mathbb {R}\), \(\bigl(\tfrac 16\bigr)^n\sum _p f(\mathrm{bcVotes}(p))\, f(\mathrm{caVotes}(p)) = \mathrm{corr}(f)\).

For voters with i.i.d. uniform orderings,

The same identity holds for the \(bc\)–\(ca\) and \(ab\)–\(ca\) pairs.

Let \(f:\{ 0,1\} ^n\to \mathbb {R}\) and let \(\mathrm{votes}_1,\mathrm{votes}_2\) map each profile to a Boolean cube point. If the pair satisfies the kernel identity \(\bigl(\tfrac 16\bigr)^n\sum _p \chi _S(\mathrm{votes}_1(p))\, \chi _T(\mathrm{votes}_2(p)) = [S = T]\, (-1/3)^{|S|}\) for all \(S,T\), then

\(f\) is a dictatorship if there exists a voter \(i\) such that \(f = \mathrm{dict}_i\), i.e. society’s preference always equals voter \(i\)’s.

For \(A\subseteq \mathrm{Fin}\, n\) and \(g:\mathrm{Fin}\, n\to \mathbb {R}\),

rewriting a product over a finset as a product over all of \(\mathrm{Fin}\, n\) with an indicator.

A profile assigns each of the \(n\) voters one of the 6 orderings: \(p : \mathrm{Fin}\, n \to \mathrm{Fin}\, 6\).

Specialization of the general kernel to the \(ab\)–\(bc\) vote pair: for all \(S,T\subseteq [n]\),

Specialization of the general kernel to the \(ab\)–\(ca\) vote pair: for all \(S,T\subseteq [n]\),

Specialization of the general kernel to the \(bc\)–\(ca\) vote pair: for all \(S,T\subseteq [n]\),

Let \(\mathrm{xPref},\mathrm{yPref}:\mathrm{Fin}\, 6\to \mathrm{Bool}\) be two preference assignments with balanced marginals \(\sum _k s(\mathrm{xPref}(k)) = \sum _k s(\mathrm{yPref}(k)) = 0\) and cross-sum \(\sum _k s(\mathrm{xPref}(k))\, s(\mathrm{yPref}(k)) = -2\). Then for all \(S,T\subseteq [n]\),

Summing pairwise sign products over all 6 orderings:

Hence \(\mathbb {E}[s_{ab}\cdot s_{bc}] = -2/6 = -1/3\).

Summing the signed \(a\)-vs-\(b\) preference over all six orderings gives \(\sum _{k=0}^{5} s_{ab}(k) = 0\); the \(ab\) marginal is balanced.

Summing the signed \(b\)-vs-\(c\) preference over all six orderings gives \(\sum _{k=0}^{5} s_{bc}(k) = 0\); the \(bc\) marginal is balanced.

Summing the signed \(c\)-vs-\(a\) preference over all six orderings gives \(\sum _{k=0}^{5} s_{ca}(k) = 0\); the \(ca\) marginal is balanced.

A social welfare function \(f:\{ 0,1\} ^n\to \mathbb {R}\) is unanimous if \(f(\texttt{false},\dots ,\texttt{false}) = 1\): when all voters prefer alternative \(a\) over \(b\), so does society.

For an assignment \(x : \mathrm{Fin}\, n \to \mathbb {Z}\) and a set \(C \subseteq \mathrm{Fin}\, n\), the product

*\(D(G)\) is \(k\)-arc-connected if and only if \(G\) is \(k\)-edge-connected.*

The associated digraph faithfully preserves connectivity, so the directed notion generalises the undirected one. Contrast §10.6, where the question is which orientations — not the doubling — preserve it; there the answer is much more delicate (Robbins, Nash-Williams).

"\(G\) is \(k\)-edge-connected" is spelled k \(\le \) edgeConnectivity G, per §3.1. Step 2 needs that a minimal edge cut is \([S, S^{c}]\) for a component \(S\), which is the same fact the local IsEdgeCut docstring notes when reconciling the book’s shape-based definition with the deletion-based one used here.

+ Statement repaired — [Nontrivial V] added. The \(\leftrightarrow \) was false on a one-vertex carrier. Take card V = 1, so \(G = \bot \), and \(k = 1\). Left side: there is no nonempty proper S : Finset V, so IsKArcConnected 1 holds vacuously. *Right side:* \(\bot \) on one vertex is Connected, so nothing disconnects it, \(G\) has no edge cut at all, and edgeConnectivity G = 0; the claim \(1 \le 0\) fails.

[Nontrivial V] excludes exactly that carrier and is the hypothesis the book’s "nontrivial digraph" convention supplies implicitly (compare diconnected_iff_isKArcConnected_one above, which already carries it). ! Both Menger statements in Networks.lean consume this lemma, so their hypotheses must be checked against the added Nontrivial when they are proved.

Given \(T\) distributions \(p_0, \dots , p_{T-1}\) over \(\mathrm{Fin}\, n\) (each presented as non-negative weights summing to \(1\)) and \(T \gt 0\), the average strategy is the mixed strategy with weights

For any \(f : \mathrm{Fin}\, T \to \mathrm{Fin}\, N \to \mathbb {R}\) and \(T \gt 0\),

Given a \(k \times d\) matrix \(A\) and a finite set \(V \subseteq \mathbb {R}^d\), BadPair \(\varepsilon \; V\; A\) holds when there exists some ordered pair \((u, v) \in V \times V\) whose images under \(A\) fail the distortion predicate, i.e. the projection distorts that pair by more than a factor of \(\varepsilon \).

For a parameter \(\varepsilon \in \mathbb {R}\), a matrix \(A\), and a vector \(x\in \mathbb {R}^d\), the predicate \(\texttt{BadSingle}\, \varepsilon \, A\, x\) holds when the squared-norm distortion is strictly too large:

This is the “bad event” whose probability must be controlled by the JL concentration argument.

For \(L \in [0,1]\) and any \(\eta \in \mathbb {R}\),

The bound is established by showing that the function \(\varphi (\eta ) = -L\eta + \eta ^2/8 - \ln (1-L+Le^{-\eta })\) is convex with \(\varphi (0) = 0\) and \(\varphi '(0) = 0\).

For \(0 \le p \le 1\) and any event, the Bernoulli\((p)\) restriction probability decomposes according to the number of free variables:

because conditioning \(R_p\) on having exactly \(k\) free variables yields exactly the model \(R_k\).

Let \(0 \lt p \le 1\), \(w, s \gt 0\), and \(\varepsilon \gt 0\). Then there exists \(N\) such that for every \(n \ge N\) with \(n \gt 0\) and every event satisfying \(\mathrm{fixedSizeRestrProb}\, (\mathrm{event})\, k \le (5kw/n)^s\) for all \(k \le n\), one has \(\Pr _{R_p}[\mathrm{event}] \le (10pw)^s + \varepsilon \). Asymptotically the exponential tail vanishes, leaving only the leading bound \((10pw)^s\).

Let \(n \gt 0\), \(0 \lt p \le 1\), and \(w, s \gt 0\). If the event satisfies \(\mathrm{fixedSizeRestrProb}\, (\mathrm{event})\, k \le (5kw/n)^s\) for every \(k \le n\), then under the Bernoulli model,

The binomial probability mass function, \(\Pr [\mathrm{Bin}(n,p) = k] = \binom {n}{k}\, p^k\, (1-p)^{n-k}\).

If \(0 \le p \le 1\), then \(0 \le \mathrm{binomialPMF}\, n\, p\, k\) for every \(k\).

If \(0 \le p \le 1\), then the binomial PMF sums to \(1\) over \(k\) ranging in \(\{ 0, \dots , n\} \), i.e. \(\sum _{k=0}^{n} \mathrm{binomialPMF}\, n\, p\, k = 1\). This is the binomial theorem applied to \((p + (1-p))^n = 1\).

For \(0 \lt p \le 1\), the upper tail of the binomial distribution beyond \(2np\) is exponentially small: summing \(\mathrm{binomialPMF}\, n\, p\, k\) over those \(k \in \{ 0, \dots , n\} \) with \(k \gt 2np\) is at most \(e^{-np/3}\).

For any \(p \gt 0\) and any \(\varepsilon \gt 0\), there exists \(N\) such that for all \(m \ge N\) one has \(e^{-mp/3} \lt \varepsilon \); that is, the tail term decays to \(0\).

The probability of an event under the fixed-size restriction model \(R_k\), which is uniform over restrictions with exactly \(k\) free variables. It is defined as the fraction of restrictions with exactly \(k\) free variables that satisfy the event.

For any event, the fixed-size restriction probability satisfies \(\mathrm{fixedSizeRestrProb}\, (\mathrm{event})\, k \le 1\).

For any event, the fixed-size restriction probability satisfies \(0 \le \mathrm{fixedSizeRestrProb}\, (\mathrm{event})\, k\).

For natural numbers \(n\) and \(k\), this is the finite set of restrictions on \(n\) variables whose set of free variables has cardinality exactly \(k\).

Given a game \(G\) and a mixed row strategy \(p\), bestColumn is the pure column \(j^* \in \mathrm{Fin}\, N\) that minimises \(\mathrm{payoffVsPure}(G, p, \cdot )\), chosen via the classical axiom of choice from the finite minimiser.

For any game \(G\), mixed row strategy \(p\), and pure column \(j\),

That is, the chosen column is indeed a minimiser.

The best expert loss in hindsight is the minimum cumulative loss achieved by any single expert:

Given a game \(G\) and a mixed column strategy \(q\), bestRow is the pure row \(i^* \in \mathrm{Fin}\, M\) that maximises \(\mathrm{pureVsPayoff}(G, \cdot , q)\), chosen classically from the finite maximiser.

For any game \(G\), mixed column strategy \(q\), and pure row \(i\),

If \(n \gt 0\), \(1 \le d\), \(2d \le n\), and \(w \le J_2(n,d)\), then

The binary entropy function

using the base-\(2\) logarithm, with the convention \(0\log _2 0 = 0\) inherited from \(\log _2 0 = 0\).

\(H(1/2) = 1\).

\(H(0) = 0\).

Fact 4.2 (lower half). Under the same hypotheses \(n \gt 0\), \(q \gt 0\), \(q \le \ell \), \(2\ell \le n\) and \(2q \le n\),

with the binomial coefficients again read in \(\mathbb {R}\) via \(\texttt{chooseR}\).

Fact 4.2 (upper half). Let \(n, \ell , q\) be naturals with \(n \gt 0\), \(q \gt 0\), \(q \le \ell \), \(2\ell \le n\) and \(2q \le n\). Then

where both binomial coefficients are taken in \(\mathbb {R}\) via \(\texttt{chooseR}\).

For \(0 \le \tau \le 1/2\),

The average \(\mathrm{avgLast}\, f\) of \(f\) over its last coordinate is the function on \(n\) variables given by \(\tfrac 12\bigl(\mathrm{restrictLast}\, f\, \mathrm{false} + \mathrm{restrictLast}\, f\, \mathrm{true}\bigr)\).

If \(X\) is \(B\)-reasonable and not equivalent to \(0\), then for every \(t \in [0,1]\),

If \(X\) is \(B\)-reasonable and not equivalent to \(0\) (its second moment is positive), then for every \(t \gt 0\),

The key algebraic inequality driving the inductive step of the Bonami lemma: for \(a, b, A, B, C \ge 0\) (with \(a, b, B, C\) nonnegative) satisfying \(A \le 9^{m+1} a^2\), \(B \le 9^m b^2\), and \(C^2 \le A\cdot B\), one has

The main Bonami inequality stated through the expectation operator: if a Boolean function \(f\) has degree at most \(k\), then

A Boolean function \(f\) of degree at most \(k\) is \(9^{k}\)-reasonable under the uniform measure on the hypercube.

If \(f\) has degree at most \(k\), then its average over the last coordinate \(\mathrm{avgLast}\, f\) also has degree at most \(k\).

If \(f\) has degree at most \(k\), then its half-difference over the last coordinate \(\mathrm{diffLast}\, f\) has degree at most \(k-1\).

A Boolean function \(f\) of degree at most \(0\) is constant: \(f(x) = f(\mathrm{default})\) for all \(x\).

For a Boolean function \(f\) of degree at most \(0\) (hence constant), \(\mathbb {E}[f^4] = \bigl(\mathbb {E}[f^2]\bigr)^2\).

The half-difference \(\mathrm{diffLast}\, f\) of \(f\) over its last coordinate is the function on \(n\) variables given by \(\tfrac 12\bigl(\mathrm{restrictLast}\, f\, \mathrm{false} - \mathrm{restrictLast}\, f\, \mathrm{true}\bigr)\).

For Boolean functions \(g, h\) on the cube, \(\bigl(\mathbb {E}[g^2 h^2]\bigr)^2 \le \mathbb {E}[g^4]\cdot \mathbb {E}[h^4]\).

For every Boolean function \(f\), \(0 \le \mathbb {E}[f^4]\).

For every Boolean function \(f\), \(0 \le \mathbb {E}[f^2]\).

For Boolean functions \(g, h\), \(0 \le \mathbb {E}[g^2 h^2]\).

The expectation of \(\varphi \) on the cube of dimension \(n+1\) is the average of the expectations of its two restrictions:

For each \(S \subseteq \mathrm{Fin}\, n\), the Fourier coefficient of \(\mathrm{avgLast}\, f\) at \(S\) equals the Fourier coefficient of \(f\) at the image of \(S\) under castSucc: \(\widehat{\mathrm{avgLast}\, f}(S) = \widehat{f}(\mathrm{castSucc}(S))\).

For each \(S \subseteq \mathrm{Fin}\, n\), the Fourier coefficient of \(\mathrm{diffLast}\, f\) at \(S\) equals the Fourier coefficient of \(f\) at the image of \(S\) under castSucc together with the last index: \(\widehat{\mathrm{diffLast}\, f}(S) = \widehat{f}\bigl(\mathrm{castSucc}(S) \cup \{ \mathrm{last}\, n\} \bigr)\).

Writing \(g = \mathrm{avgLast}\, f\) and \(h = \mathrm{diffLast}\, f\), the fourth moment of \(f\) decomposes as

For all real \(a, b\), \((a+b)^4 + (a-b)^4 = 2\, (a^4 + 6\, a^2 b^2 + b^4)\).

A real random variable \(X\) on a measurable space \(\Omega \) with measure \(P\) is \(B\)-reasonable when its fourth moment is controlled by its second moment, namely

Let \(X\) be a discrete random variable on a finite space whose law is a PMF \(\pi \). If \(\mu \gt 0\) is a lower bound on every atom probability \(\pi (\omega )\), then \(X\) is \((1/\mu )\)-reasonable.

If \(P\) is a probability measure on the cube assigning each point the uniform weight, then the \(p\)-th moment of \(f\) under \(P\) coincides with the expectation \(\mathbb {E}[f^p]\).

Let \(Z \ge 0\) be a nonnegative random variable with finite first and second moments and positive mean. For every \(\theta \) with \(0 \le \theta \le 1\),

Given a Boolean function \(f\) on \(n+1\) variables and a bit \(b\), the restriction \(\mathrm{restrictLast}\, f\, b\) is the function on \(n\) variables obtained by fixing the last coordinate to \(b\), i.e. \(x \mapsto f(x, b)\).

For every \(x\), the restriction of \(f\) fixing the last coordinate to false equals the sum of the average and the half-difference: \(\mathrm{restrictLast}\, f\, \mathrm{false}\, x = \mathrm{avgLast}\, f\, x + \mathrm{diffLast}\, f\, x\).

For every \(x\), the restriction of \(f\) fixing the last coordinate to true equals the difference of the average and the half-difference: \(\mathrm{restrictLast}\, f\, \mathrm{true}\, x = \mathrm{avgLast}\, f\, x - \mathrm{diffLast}\, f\, x\).

Writing \(g = \mathrm{avgLast}\, f\) and \(h = \mathrm{diffLast}\, f\), the second moment of \(f\) decomposes as \(\mathbb {E}[f^2] = \mathbb {E}[g^2] + \mathbb {E}[h^2]\).

For all real \(a, b\), \((a+b)^2 + (a-b)^2 = 2\, (a^2 + b^2)\).

For any \(\varphi \) on the cube of dimension \(n+1\), the total sum decomposes according to the value of the last coordinate:

The canonical uniform probability measure on the Boolean hypercube \(\{ 0,1\} ^n\).

The uniform measure assigns each point \(x\) of the cube the combinatorial uniform weight: \((\mathrm{uniformMeasure}\, n)(\{ x\} ) = \mathrm{uniformWeight}\, n\).

The uniform point weight satisfies \(\mathrm{uniformWeight}(n+1) = \mathrm{uniformWeight}(n)/2\).

The BLR acceptance probability of \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is

where \(x, y\) are drawn uniformly from \(\{ 0,1\} ^n\).

For any \(f : \{ 0,1\} ^n \to \{ 0,1\} \),

Write \(g = \texttt{BoolBLR.lift\_ pm1}\, f\). For all \(x, y \in \{ 0,1\} ^n\),

If \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is linear, then \(\texttt{BoolBLR.BLR\_ accept\_ prob}\, f = 1\); that is, the BLR test accepts every linear function with probability \(1\).

Let \(f : \{ 0,1\} ^n \to \{ 0,1\} \) satisfy \(f(x \oplus y) = f(x) \oplus f(y)\) for all \(x, y\), and write \(g = \texttt{BoolBLR.lift\_ pm1}\, f\). Then \(g\) is multiplicative on XOR:

If \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is linear, then \(f(x \oplus y) = f(x) \oplus f(y)\) for all \(x, y \in \{ 0,1\} ^n\).

If \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is \(\varepsilon \)-far from linear, then

That is, a function that is \(\varepsilon \)-far from every linear function causes the BLR test to reject with probability at least \(\varepsilon \).

If \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is \(\varepsilon \)-far from linear, then the sum of cubed Fourier coefficients of \(\texttt{BoolBLR.lift\_ pm1}\, f\) satisfies

This follows by combining the per-coefficient bound \(\hat{f}(S) \le 1-2\varepsilon \) with the Parseval identity \(\sum _S \hat{f}(S)^2 = 1\).

Let \(f : \{ 0,1\} ^n \to \{ 0,1\} \) be \(\varepsilon \)-far from linear and write \(g = \texttt{BoolBLR.lift\_ pm1}\, f\). Then for every \(S \subseteq [n]\),

For every \(f : \{ 0,1\} ^n \to \{ 0,1\} \), the \(\pm 1\) lift \(g = \texttt{BoolBLR.lift\_ pm1}\, f\) has unit Fourier mass:

The distance between two Boolean functions \(f, g : \{ 0,1\} ^n \to \{ 0,1\} \) is

computed as the uniform expectation of the indicator \(\mathbf{1}[f(x) \ne g(x)]\).

A function \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is \(\varepsilon \)-far from linear if \(0 \le \varepsilon \le 1\) and for every linear function \(g : \{ 0,1\} ^n \to \{ 0,1\} \) we have \(\operatorname{dist}(f, g) \ge \varepsilon \).

Let \(f, g : \{ 0,1\} ^n \to \{ 0,1\} \), let \(S \subseteq [n]\), and suppose \(\texttt{BoolBLR.lift\_ pm1}\, g = \chi _S\) and \(\operatorname{dist}(f, g) \ge \varepsilon \). Then the Fourier coefficient of \(\texttt{BoolBLR.lift\_ pm1}\, f\) at \(S\) satisfies \(\widehat{\texttt{BoolBLR.lift\_ pm1}\, f}(S) \le 1 - 2\varepsilon \).

For all \(f, g : \{ 0,1\} ^n \to \{ 0,1\} \) and every \(x \in \{ 0,1\} ^n\),

If \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is \(\varepsilon \)-far from linear, then for every \(S \subseteq [n]\),

A function \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is linear if for all \(x, y \in \{ 0,1\} ^n\) we have

where \(\oplus \) denotes bitwise XOR (i.e. Bool.xor).

Given \(f : \{ 0,1\} ^n \to \{ 0,1\} \), its \(\pm 1\) lift \(\texttt{BoolBLR.lift\_ pm1}\, f : \{ 0,1\} ^n \to \mathbb {R}\) is defined by \(x \mapsto (-1)^{f(x)}\), converting each Boolean output to a real sign via BoolToPM1.

A Boolean function \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is linear if and only if there exists a set \(S \subseteq [n]\) such that the \(\pm 1\) lift \(\texttt{BoolBLR.lift\_ pm1}\, f\) equals the Fourier character \(\chi _S\).

For every \(S \subseteq [n]\) and all \(x, y \in \{ 0,1\} ^n\),

Let \(f : \{ 0,1\} ^n \to \{ 0,1\} \) satisfy \(\texttt{BoolBLR.lift\_ pm1}\, f = \chi _S\) for some \(S \subseteq [n]\), and let \(x, y \in \{ 0,1\} ^n\). Assuming the multiplicativity identity \(\chi _S(x \oplus y) = \chi _S(x)\chi _S(y)\), one has

If \(\texttt{BoolBLR.lift\_ pm1}\, f = \chi _S\) for some \(S \subseteq [n]\), then for all \(x, y \in \{ 0,1\} ^n\),

This is the previous lemma with the multiplicativity hypothesis discharged.

Restatement of the support formula in the exact form used inside the proof of the character criterion: for linear \(f\) and any \(x \in \{ 0,1\} ^n\), \(f(x)\) is the parity of the number of coordinates \(i\) with \(x_i = \texttt{true}\) and \(f(e_i) = \texttt{true}\).

Let \(f : \{ 0,1\} ^n \to \{ 0,1\} \) be linear. Then for every \(s \subseteq [n]\), writing \(\mathbf{1}_s\) for the indicator vector of \(s\) and \(e_i\) for the \(i\)-th basis vector, the value \(f(\mathbf{1}_s)\) is false when

and true otherwise; that is, \(f(\mathbf{1}_s)\) is the parity of the number of \(i \in s\) with \(f(e_i) = \texttt{true}\).

Specialization of the previous lemma to the support of an arbitrary point: if \(f : \{ 0,1\} ^n \to \{ 0,1\} \) is linear, then for every \(x \in \{ 0,1\} ^n\) the value \(f(x)\) is the parity of the number of coordinates \(i\) with \(x_i = \texttt{true}\) and \(f(e_i) = \texttt{true}\).

For any \(f : \{ 0,1\} ^n \to \mathbb {R}\),

For any \(f : \{ 0,1\} ^n \to \{ 0,1\} \), letting \(\hat{g}(S)\) denote the Fourier coefficient of \(g = \texttt{BoolBLR.lift\_ pm1}\, f\),

Write \(g = \texttt{BoolBLR.lift\_ pm1}\, f\). For every \(x \in \{ 0,1\} ^n\),

i.e. the self-convolution of \(g\) has Fourier coefficients \(\hat{g}(S)^2\).

Write \(g = \texttt{BoolBLR.lift\_ pm1}\, f\) and assume \((g * g)(x) = \sum _S \hat{g}(S)^2 \chi _S(x)\) for all \(x\). Then

A Boolean circuit on \(n\) variables is a tree whose leaves are literals (lit \(l\)) and whose internal nodes (node \(isAnd\) \(children\)) are AND gates when \(isAnd = \mathrm{true}\) and OR gates when \(isAnd = \mathrm{false}\), applied to a list of child circuits. No alternation or deduplication constraint is imposed.

The depth of a circuit (longest root-to-leaf path): a literal has depth \(0\) and a node has depth \(1\) plus the maximum depth among its children.

Evaluates a circuit under an assignment \(x\): a literal evaluates via \(\mathrm{Lit.eval}\), an AND node is the conjunction (foldr with &&, unit true) of its children’s values, and an OR node is the disjunction (foldr with ||, unit false).

An induction principle for Circuit stating that to prove a predicate \(\mathrm{motive}\) holds for every circuit it suffices to prove it for every literal and, in the node case, to prove \(\mathrm{motive}(\texttt{node}\, isAnd\, cs)\) assuming \(\mathrm{motive}\, c\) for every child \(c \in cs\). This works around the lack of native support for nested inductives.

The number of literal occurrences in a circuit: a literal contributes \(1\) and a node contributes the sum of the literal counts of its children.

The maximum depth over a list \(cs\) of circuits (with \(0\) for the empty list), used to compute the depth at a node.

The maximum fanin of a circuit: a literal has fanin \(0\), and a node’s value is the maximum of the number of its children and the maximal fanin occurring recursively among its children.

For every Boolean circuit \(C\) on \(n\) inputs, \(1 \le C.\texttt{size}\).

Given a circuit \(c\) on \(m\) variables and a function \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\), the re-indexed circuit \(\mathrm{reidx}(c, f)\) on \(m'\) variables is obtained by replacing each literal index \(i\) by \(f(i)\) (keeping its sign) and recursing structurally through the \(\mathrm{And}/\mathrm{Or}\) nodes.

For every circuit \(c\) on \(m\) variables and every \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\), the re-indexed circuit has the same depth as \(c\), i.e. \(\mathrm{depth}(\mathrm{reidx}(c, f)) = \mathrm{depth}(c)\).

For every circuit \(c\) on \(m\) variables, every \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\), and every assignment \(g : \mathrm{Fin}\, m' \to \mathrm{Bool}\), evaluating the re-indexed circuit under \(g\) equals evaluating \(c\) under the pulled-back assignment \(g \circ f\), i.e. \(\mathrm{eval}(\mathrm{reidx}(c, f), g) = \mathrm{eval}(c, g \circ f)\).

The total number of nodes of a circuit (internal gates plus literal leaves): a literal has size \(1\) and a node has size \(1\) plus the sum of the sizes of its children.

The sum of the sizes over a list \(cs\) of circuits, used to compute the size at a node.

Turns a circuit \(C\) on \(n\) inputs into a feedforward circuit \(\texttt{FeedForward}\ \texttt{Bool}\ (\mathrm{Fin}\, n)\ \mathrm{Unit}\) of depth \(C.\texttt{depth} + 1\): layer \(0\) carries the \(n\) input variables and every higher layer carries a single wire. The gate from layer \(0\) to layer \(1\) computes \(C.\texttt{eval}\) from all inputs at once, and all later gates are identity wires that pass the single Boolean value upward.

Converts a general circuit into a normal-form AND circuit: a literal becomes a singleton clause; an AND node maps its children through \(\mathrm{toNOr}\); and an OR node is wrapped as a single OR node built from the children’s \(\mathrm{toNAnd}\) images, enforcing alternation.

Converts a general circuit into a normal-form OR circuit: a literal becomes a singleton clause; an OR node maps its children through \(\mathrm{toNAnd}\); and an AND node is wrapped as a single AND node built from the children’s \(\mathrm{toNOr}\) images, enforcing alternation.

A technical lemma: if \(g(h\, c) = f\, c\) for all \(c \in cs\), then the additive foldr of \(g\) over \(cs.\mathrm{map}\; h\) equals the additive foldr of \(f\) over \(cs\).

A technical lemma: if \(g(h\, c) \le k \cdot f\, c\) for all \(c \in cs\), then the additive foldr of \(g\) over \(cs.\mathrm{map}\; h\) is at most \(k\) times the additive foldr of \(f\) over \(cs\).

For any list of literals \(lits\) and input \(x\), the right fold of \(\& \& \) over the literal evaluations (starting from \(\mathrm{true}\)) equals the term evaluation \(\texttt{Term.eval}\, (lits.\mathrm{map}\, \texttt{Lit.toLiteral})\, x\).

A technical lemma: if \(g(h\, c) = f\, c\) for all \(c \in cs\), then the conjunctive foldr of \(g\) over \(cs.\mathrm{map}\; h\) equals the conjunctive foldr of \(f\) over \(cs\).

For any list of literals \(lits\) and input \(x\), the right fold of \(||\) over the literal evaluations (starting from \(\mathrm{false}\)) equals the CNF clause evaluation \(\texttt{CNF.evalClause}\, (lits.\mathrm{map}\, \texttt{Lit.toLiteral})\, x\).

A technical lemma: if \(g(h\, c) = f\, c\) for all \(c \in cs\), then the disjunctive foldr of \(g\) over \(cs.\mathrm{map}\; h\) equals the disjunctive foldr of \(f\) over \(cs\).

A literal for Boolean circuits: a variable index \(\mathtt{idx} : \mathrm{Fin}\, n\) together with a polarity \(\mathtt{sign} : \mathrm{Bool}\) (true = positive occurrence).

In a clause whose variable indices are pairwise distinct, any two literals \(l_1, l_2 \in lits\) that share the same index (\(l_1.\mathrm{idx} = l_2.\mathrm{idx}\)) are in fact equal, \(l_1 = l_2\).

For a literal \(l\) on \(n\) variables and an assignment \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\), the value \(l.\mathrm{eval}\, x\) is \(x_{l.\mathrm{idx}}\) when \(l\) is positive (\(l.\mathrm{sign} = \mathrm{true}\)) and \(\lnot x_{l.\mathrm{idx}}\) when \(l\) is negated.

For every literal \(l\) and input \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), the circuit evaluation \(l.\mathrm{eval}\, x\) equals the evaluation of its converted literal \(l.\mathrm{toLiteral}.\mathrm{eval}\, x\).

Maps a Boolean-circuit literal \(l : \texttt{BoolCircuit.Lit}\, n\) to the corresponding switching-lemma \(\texttt{Literal}\, n\), recording the same variable index and polarity.

A normal-form AND circuit on \(n\) variables: either a base clause given by a list of literals whose variable indices are pairwise distinct (a Nodup proof on \(lits.\mathrm{map}\; \mathrm{Lit.idx}\)), or a node that ANDs together a list of normal-form OR circuits. Together with \(\mathrm{NOrCircuit}\) this forms a strictly alternating AND/OR normal form.

If a normal-form AND circuit \(c\) equals a clause built from literals \(lits\) with a duplication-free proof \(h\), then the variable indices \(lits.\mathrm{map}\; \mathrm{Lit.idx}\) are pairwise distinct.

Sends an AND-clause \(\texttt{NAndCircuit}.\mathrm{clause}\, lits\) to the \(\texttt{Term}\) (a conjunction of literals) obtained by mapping each circuit literal through Lit.toLiteral.

If the variable indices of an AND-clause’s literals are pairwise distinct, then the converted term \((\texttt{NAndCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm}\) has the Nodup property.

If the literal indices of an AND-clause are distinct, then within the converted term any two literals sharing the same variable are equal.

The width of the term obtained from an AND-clause equals the number of its literals: \(\texttt{Term.width}\, (\texttt{NAndCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm} = lits.\mathrm{length}\).

The constant-true AND circuit, given by the empty clause (an empty conjunction).

The depth of a normal-form AND circuit: a clause has depth \(0\), and a node has depth \(1\) plus the maximum depth among its child OR circuits.

Evaluates a normal-form AND circuit under an assignment \(x\): a clause is the conjunction of its literals’ values (unit true), and a node is the conjunction of its child OR circuits’ values.

The number of literal occurrences in a normal-form AND circuit: a clause contributes the length of its literal list, and a node contributes the sum over its child OR circuits.

If every child \(c\) of an \(\texttt{NAndCircuit}.\mathrm{node}\, cs\) is an OR-clause, then for all \(x\) the circuit evaluation \((\texttt{NAndCircuit}.\mathrm{node}\, cs).\mathrm{eval}\, x\) equals the CNF evaluation \(\texttt{CNF.eval}\, ((\texttt{NAndCircuit}.\mathrm{node}\, cs).\mathrm{toCNF})\, x\).

The normal-form AND circuit consisting of the single positive literal on variable \(i\).

The total node count of a normal-form AND circuit: a clause has size \(1\), and a node has size \(1\) plus the sum of the sizes of its child OR circuits.

The forgetful map turning a normal-form AND circuit into a general circuit: a clause becomes an AND node over its literals, and a node becomes an AND node over the circuit images of its child OR circuits.

Converts a depth-2 \(\texttt{NAndCircuit}\) (an AND of OR-clauses) into a \(\texttt{CNF}\), the list of clauses obtained by converting each OR-clause via NOrCircuit.clauseToTerm; a bare clause maps to the empty CNF.

If every child of an \(\texttt{NAndCircuit}.\mathrm{node}\, cs\) is an OR-clause with distinct literal indices, then every clause in the resulting CNF has the Nodup property.

If every child of an \(\texttt{NAndCircuit}.\mathrm{node}\, cs\) is an OR-clause with distinct literal indices, then in every clause of the resulting CNF any two literals on the same variable are equal.

If every OR-clause child has at most \(w\) literals (with distinct indices), then the CNF \((\texttt{NAndCircuit}.\mathrm{node}\, cs).\mathrm{toCNF}\) has width at most \(w\).

If a normal-form OR circuit \(c\) equals a clause built from literals \(lits\) with a duplication-free proof \(h\), then the variable indices \(lits.\mathrm{map}\; \mathrm{Lit.idx}\) are pairwise distinct.

Sends an OR-clause \(\texttt{NOrCircuit}.\mathrm{clause}\, lits\) to the \(\texttt{Term}\) obtained by mapping each circuit literal through Lit.toLiteral; this term plays the role of one CNF clause (a disjunction of literals).

If the variable indices of an OR-clause’s literals are pairwise distinct, then the converted term \((\texttt{NOrCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm}\) has the Nodup property.

If the literal indices of an OR-clause are distinct, then within the converted term any two literals sharing the same variable are equal.

The width of the term obtained from an OR-clause equals the number of its literals: \(\texttt{Term.width}\, (\texttt{NOrCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm} = lits.\mathrm{length}\).

The constant-false OR circuit, given by the empty clause (an empty disjunction).

The depth of a normal-form OR circuit: a clause has depth \(0\), and a node has depth \(1\) plus the maximum depth among its child AND circuits.

Evaluates a normal-form OR circuit under an assignment \(x\): a clause is the disjunction of its literals’ values (unit false), and a node is the disjunction of its child AND circuits’ values.

The number of literal occurrences in a normal-form OR circuit: a clause contributes the length of its literal list, and a node contributes the sum over its child AND circuits.

If every child \(c\) of an \(\texttt{NOrCircuit}.\mathrm{node}\, cs\) is an AND-clause, then for all \(x\) the circuit evaluation \((\texttt{NOrCircuit}.\mathrm{node}\, cs).\mathrm{eval}\, x\) equals the DNF evaluation \(\texttt{DNF.eval}\, ((\texttt{NOrCircuit}.\mathrm{node}\, cs).\mathrm{toDNF})\, x\).

The normal-form OR circuit consisting of the single positive literal on variable \(i\).

The total node count of a normal-form OR circuit: a clause has size \(1\), and a node has size \(1\) plus the sum of the sizes of its child AND circuits.

The forgetful map turning a normal-form OR circuit into a general circuit: a clause becomes an OR node over its literals, and a node becomes an OR node over the circuit images of its child AND circuits.

Converts a depth-2 \(\texttt{NOrCircuit}\) (an OR of AND-clauses) into a \(\texttt{DNF}\), the list of terms obtained by converting each AND-clause via NAndCircuit.clauseToTerm; a bare clause maps to the empty DNF.

If every child of an \(\texttt{NOrCircuit}.\mathrm{node}\, cs\) is an AND-clause with distinct literal indices, then every term in the resulting DNF has the Nodup property.

If every child of an \(\texttt{NOrCircuit}.\mathrm{node}\, cs\) is an AND-clause with distinct literal indices, then in every term of the resulting DNF any two literals on the same variable are equal.

If every AND-clause child has at most \(w\) literals (with distinct indices), then the DNF \((\texttt{NOrCircuit}.\mathrm{node}\, cs).\mathrm{toDNF}\) has width at most \(w\).

For every circuit \(c\) and assignment \(x\), \((c.\mathrm{toNAnd}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\).

For every circuit \(c\), \((c.\mathrm{toNAnd}).\mathrm{litCount} = c.\mathrm{litCount}\).

For every circuit \(c\), \((c.\mathrm{toNAnd}).\mathrm{size} \le 2\, c.\mathrm{size}\).

For every circuit \(c\) and assignment \(x\), both normalizations agree with the original on values: \((c.\mathrm{toNAnd}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\) and \((c.\mathrm{toNOr}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\).

For every circuit \(c\), both normalizations preserve the literal count: \((c.\mathrm{toNAnd}).\mathrm{litCount} = c.\mathrm{litCount}\) and \((c.\mathrm{toNOr}).\mathrm{litCount} = c.\mathrm{litCount}\).

For every circuit \(c\), both normalizations have size at most twice the original: \((c.\mathrm{toNAnd}).\mathrm{size} \le 2\, c.\mathrm{size}\) and \((c.\mathrm{toNOr}).\mathrm{size} \le 2\, c.\mathrm{size}\).

For every circuit \(c\) and assignment \(x\), \((c.\mathrm{toNOr}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\).

For every circuit \(c\), \((c.\mathrm{toNOr}).\mathrm{litCount} = c.\mathrm{litCount}\).

For every circuit \(c\), \((c.\mathrm{toNOr}).\mathrm{size} \le 2\, c.\mathrm{size}\).

The Boolean hypercube of dimension \(n\) is \(\{ 0,1\} ^n\), represented as the function type \(\mathrm{Fin}\, n \to \mathrm{Bool}\).

A Boolean function of arity \(n\) is a function \(f : \{ 0,1\} ^n \to \mathbb {R}\).

The sign encoding maps \(\mathrm{Bool}\) to \(\{ -1,1\} \subset \mathbb {R}\):

\(\sigma (\texttt{false}) = 1\), \(\sigma (\texttt{true}) = -1\), \(\sigma (b)^2 = 1\), and \(\sigma (\lnot b) = -\sigma (b)\).

There are exactly \(2^n\) Walsh characters, matching the dimension of \(L^2(\{ 0,1\} ^n)\).

The Walsh–Fourier character associated to \(S\subseteq [n]\) is

The family \(\{ \chi _S\} _{S\subseteq [n]}\) forms an orthonormal basis for \(L^2(\{ 0,1\} ^n,\mathrm{uniform})\).

\(\chi _\varnothing \equiv 1\).

Flipping coordinate \(i\) negates \(\chi _S\) when \(i\in S\) and leaves it unchanged otherwise:

\(\chi _S(x)\cdot \chi _T(x) = \chi _{S\mathbin {\triangle } T}(x)\), where \(\triangle \) denotes symmetric difference.

If \(S\) and \(T\) are disjoint then \(\chi _{S\cup T}(x) = \chi _S(x)\cdot \chi _T(x)\).

Flipping all bits multiplies the character by \((-1)^{|S|}\):

\(\chi _{\{ i\} }(x) = \sigma (x_i)\).

\(\chi _S(x)^2 = 1\) for all \(S\) and \(x\).

The discrete derivative of \(f\) in direction \(i\) is the Boolean function

where \(x^{i\mapsto b}\) sets coordinate \(i\) of \(x\) to \(b\).

The discrete derivative respects addition: \(D_i(f + g) = D_i f + D_i g\).

The discrete derivative commutes with scalar multiplication: \(D_i(c\cdot f) = c\cdot D_i f\) for \(c\in \mathbb {R}\).

The discrete derivative \(D_i\) packaged as an \(\mathbb {R}\)-linear map on the space of Boolean functions.

The dictator function for coordinate \(i\) outputs the sign of the \(i\)-th bit: \(\mathrm{dict}_i(x) = (-1)^{x_i}\). Its unique nonzero Fourier coefficient is \(\widehat{\mathrm{dict}_i}(\{ i\} ) = 1\).

\(\mathrm{dict}_i = \chi _{\{ i\} }\).

The expectation of \(f\) under the uniform measure:

The expectation operator respects addition: \(E_i(f + g) = E_i f + E_i g\).

The expectation operator commutes with scalar multiplication: \(E_i(c\cdot f) = c\cdot E_i f\) for \(c\in \mathbb {R}\).

The expectation operator \(E_i\) packaged as an \(\mathbb {R}\)-linear map on the space of Boolean functions.

The expectation operator in direction \(i\) averages \(f\) over the two values of coordinate \(i\):

The point \(x^i\in \{ 0,1\} ^n\) obtained from \(x\) by flipping the \(i\)-th coordinate.

Flipping coordinate \(i\) twice returns the original point: \((x^i)^i = x\).

If \(i\ne j\) then flipping coordinate \(i\) does not change coordinate \(j\): \((x^i)_j = x_j\).

The Walsh characters form an orthonormal system:

The Fourier–Walsh coefficient of \(f\) at frequency \(S\) is

\(\hat f(\varnothing ) = \mathbb {E}[f]\).

If \(f\) is odd and \(|S|\) is even, then \(\hat f(S) = 0\).

A Boolean function \(f\) has degree at most \(k\) if every nonzero Fourier coefficient is supported on a set of size at most \(k\): for all \(S\), if \(\hat f(S)\ne 0\) then \(|S|\le k\).

The influence of coordinate \(i\) on \(f\) measures how often flipping bit \(i\) changes the output:

For \(\pm 1\)-valued \(f\) this equals \(\Pr [f(x)\ne f(x^i)]\).

\(\mathrm{Inf}_i[\chi _S] = [i\in S]\).

For any \(\pm 1\)-valued function and any coordinate \(i\), \(\mathrm{Inf}_i[f] \le 1\).

The \(L^2\) inner product of two Boolean functions with respect to the uniform measure:

\(\langle f + g, h\rangle = \langle f, h\rangle + \langle g, h\rangle \).

\(\langle \chi _S, \chi _S\rangle = 1\).

\(\langle f, g\rangle = \langle g, f\rangle \).

\(\langle f, f\rangle \ge 0\).

If \(f\) is \(\pm 1\)-valued then \(\langle f, f\rangle = 1\).

A Boolean function \(f\) is odd if \(f(\lnot x) = -f(x)\) for all \(x\). This models antisymmetry of pairwise preferences in social choice.

\(f\) is \(\pm 1\)-valued if \(f(x)\in \{ -1,1\} \) for all \(x\).

The \(L^2\) norm of \(f\): \(\| f\| = \sqrt{\langle f,f\rangle }\).

The majority function on \(\{ 0,1\} ^{2k+1}\) outputs \(1\) if more than half the inputs are \(\texttt{false}\), and \(-1\) otherwise.

There exists a coordinate \(i\) with \(\mathrm{Inf}_i[f] \ge I[f]/n\).

The maximum sensitivity of \(f\) over all inputs.

Let \(P\) be a probability measure on \(\{ 0,1\} ^n\) that assigns the uniform weight to each singleton. Then for any Boolean function \(f\) and \(p\in \mathbb {N}\), the \(p\)-th moment of \(f\) under \(P\) equals the uniform expectation of \(f^p\):

The noise operator \(T_\rho \) with parameter \(\rho \in [-1,1]\), defined via the Fourier domain by

Probabilistically, \(T_\rho f(x) = \mathbb {E}_y[f(y)]\) where each bit of \(y\) agrees with \(x_i\) with probability \(\tfrac {1+\rho }{2}\) and is flipped with probability \(\tfrac {1-\rho }{2}\), independently.

The noise operator \(T_\rho \) is self-adjoint with respect to the \(L^2\) inner product:

The parity function \(f(x) = (-1)^{x_1+\cdots +x_n}\) satisfies \(\hat f([n]) = 1\) and \(\hat f(S) = 0\) for \(S\ne [n]\).

\(\mathrm{parity}_n = \chi _{[n]}\).

The squared \(L^2\) norm of \(f\) equals the sum of squared Fourier coefficients:

If \(f\) is \(\pm 1\)-valued then \(\sum _{S\subseteq [n]}\hat f(S)^2 = 1\).

The inner product of two Boolean functions equals the sum of the products of their Fourier coefficients:

The sensitivity of \(f\) at \(x\) is the number of coordinates \(i\) such that flipping bit \(i\) changes \(f(x)\).

Summing the sign encoding over the two Boolean values gives zero: \(\sum _{b\in \mathrm{Bool}} \sigma (b) = 0\).

Summing the character \(\chi _S\) over the whole hypercube yields

For points \(x, y\in \{ 0,1\} ^n\),

This is the completeness kernel underlying Fourier inversion.

For any \(c : \mathrm{Fin}\, n \to \mathbb {R}\),

\(I[f] = \sum _{i=1}^n \mathrm{Inf}_i[f]\).

The uniform probability measure on \(\{ 0,1\} ^n\) assigns weight \(2^{-n}\) to each point.

Every Boolean function \(f:\{ 0,1\} ^n\to \mathbb {R}\) has the unique representation

This is the Fourier inversion formula for the uniform measure on \(\{ 0,1\} ^n\).

The Fourier weight at level \(k\) is

The average of the two values of the \(\pm 1\) embedding is zero:

A Boolean function of arity \(n\) is an element of type \(\{ 0,1\} ^n \to \mathbb {R}\), defined as an abbreviation for BooleanAnalysis.BooleanFunc \(n\).

The map \(\mathrm{BoolToPM1} : \mathrm{Bool} \to \mathbb {R}\) sends \(\mathtt{false}\) to \(1\) and \(\mathtt{true}\) to \(-1\), realising the standard identification \(\{ 0,1\} \cong \{ \pm 1\} \).

For every \(b : \mathrm{Bool}\), \(\mathrm{BoolToPM1}(\lnot b) = -\mathrm{BoolToPM1}(b)\).

For every \(b : \mathrm{Bool}\), \(\mathrm{BoolToPM1}(b)^2 = 1\).

For all \(a, b : \mathrm{Bool}\), \(\mathrm{BoolToPM1}(a \oplus b) = \mathrm{BoolToPM1}(a) \cdot \mathrm{BoolToPM1}(b)\); that is, XOR corresponds to multiplication in \(\{ \pm 1\} \subset \mathbb {R}\).

For every \(n : \mathbb {N}\), the Boolean hypercube satisfies \(|\{ 0,1\} ^n| = 2^n\).

For a set \(S \subseteq [n]\), the Walsh character \(\chi _S : \{ 0,1\} ^n \to \mathbb {R}\) is

defined as an alias for BooleanAnalysis.chiS.

\(\chi _\emptyset = \mathbf{1}\), the constant function equal to \(1\).

For every \(S \subseteq [n]\), \(\chi _S(\mathbf{0}) = 1\).

For every \(S \subseteq [n]\) and \(x \in \{ 0,1\} ^n\), \(\chi _S(x)^2 = 1\).

For every \(S \subseteq [n]\) and every \(x \in \{ 0,1\} ^n\), \(\chi _S(x)^2 = 1\). This is the squaring form (with exponent \(2\) rather than an explicit product) of the fact that Walsh characters take values in \(\{ \pm 1\} \).

For all \(S, T \subseteq [n]\) and \(x \in \{ 0,1\} ^n\),

where \(S \mathbin {\triangle } T\) denotes the symmetric difference.

The convolution of \(f, g : \{ 0,1\} ^n \to \mathbb {R}\) is the function

For \(f : \{ 0,1\} ^n \to \mathbb {R}\), the uniform expectation is

\(\mathbb {E}[\chi _\emptyset ] = 1\).

If \(S \ne \emptyset \), then \(\mathbb {E}[\chi _S] = 0\).

For a non-empty \(S \subseteq [n]\), the uniform expectation of the character \(\chi _S\) factorises over the coordinates of \(S\):

The locally-defined expectation BoolFourier.expectation agrees with BooleanAnalysis.expect: for every \(f\), \(\mathbb {E}[f] = \mathrm{expect}(f)\).

If \(g : \mathrm{Fin}\, n \to \mathrm{Bool} \to \mathbb {R}\) and \(f(x) = \prod _{i} g_i(x_i)\), then

The Fourier coefficient of \(f : \{ 0,1\} ^n \to \mathbb {R}\) at \(S \subseteq [n]\) is

If \(S \ne T\), then \(\widehat{\chi _S}(T) = 0\).

For every \(S \subseteq [n]\), \(\widehat{\chi _S}(S) = 1\).

For all \(f, g : \{ 0,1\} ^n \to \mathbb {R}\) and \(S \subseteq [n]\),

Let \(f, g : \{ 0,1\} ^n \to \mathbb {R}\), let \(S \subseteq [n]\), assume the Fubini interchange for the convolution coefficient, and let \(y \in \{ 0,1\} ^n\). Then translating the argument of \(g\) by \(y\) only multiplies the character-weighted sum by \(\chi _S(y)\):

For all \(f, g : \{ 0,1\} ^n \to \mathbb {R}\) and \(S \subseteq [n]\), the double sum defining the unnormalised convolution coefficient may be reordered:

For all \(x, y \in \{ 0,1\} ^n\) and \(S \subseteq [n]\),

expressing that \(\chi _S\) is a character of the group \((\mathbb {F}_2)^n\). The statement also carries the (unused) Fubini hypothesis of the enclosing proof.

For every \(f\) and \(S\), \(\mathrm{fourier\_ coeff}(f, S) = \mathrm{fourierCoeff}(f, S)\), bridging the local and upstream definitions.

Every Boolean function \(f : \{ 0,1\} ^n \to \mathbb {R}\) expands in the Walsh–Fourier basis:

The Boolean hypercube of dimension \(n\) is the type \(\{ 0,1\} ^n\), defined as an abbreviation for BooleanAnalysis.BoolCube \(n\).

The inner product of \(f, g : \{ 0,1\} ^n \to \mathbb {R}\) is

If \(S \ne T\), then \(\langle \chi _S, \chi _T \rangle = 0\).

For every \(S \subseteq [n]\), \(\langle \chi _S, \chi _S \rangle = 1\).

The squared \(L^2\) norm of \(f : \{ 0,1\} ^n \to \mathbb {R}\) is

For every \(f : \{ 0,1\} ^n \to \mathbb {R}\),

For every \(f : \{ 0,1\} ^n \to \mathbb {R}\), the locally-defined squared \(L^2\) norm agrees with the upstream inner product of \(f\) with itself:

The partial inverse \(\mathrm{PM1ToBool?} : \mathbb {R} \to \mathrm{Option}\, \mathrm{Bool}\) returns \(\mathtt{some}\, \mathtt{true}\) on \(-1\), \(\mathtt{some}\, \mathtt{false}\) on \(1\), and \(\mathtt{none}\) on all other real numbers.

As functions of \(S\), the evaluation of characters at the all-zeros vector is constant:

For every \(x \in \{ 0,1\} ^n\) with \(x \ne \mathbf{0}\),

Let \(x \in \{ 0,1\} ^n\) with \(x \ne \mathbf{0}\) and let \(i\) be a coordinate with \(x_i = \mathtt{true}\). Then the sum of all characters at \(x\) equals the sum of their negations:

For \(x, y \in \{ 0,1\} ^n\), the vector \(\mathrm{xor\_ vec}(x,y)_i = x_i \oplus y_i\) is the componentwise XOR, giving the group operation on \((\mathbb {F}_2)^n\).

\(\mathrm{zero\_ vec}(n) : \{ 0,1\} ^n\) is the constant-\(\mathtt{false}\) function, serving as the additive identity of the group \((\mathbb {F}_2)^n\).

The complete decision tree for a function \(f\) that queries variables \(k, k+1, \dots , n-1\) in order, starting from accumulator assignment \(acc\), and outputs \(f\) applied to the completed assignment at each leaf.

For a function \(f\), an index \(k \le n\), and an accumulator assignment \(acc\), the complete decision tree \(\mathrm{buildFullDTree}\, f\, k\, acc\) that queries variables \(k, k+1, \dots , n-1\) in order has depth at most \(n - k\).

For a function \(f\), an index \(k \le n\), and assignments \(acc, x\) agreeing on all coordinates below \(k\) (i.e. \(acc\, i = x\, i\) whenever \(i.\mathrm{val} \lt k\)), the complete decision tree \(\mathrm{buildFullDTree}\, f\, k\, acc\) evaluates to \(f\, x\) on \(x\).

\(|M| + |M^c| = n\).

If \(p \gt 0\) and \(m \cdot p \le 1\) (as is the case for \(m\) disjoint events each of probability at least \(p\)), then \(m \le p^{-1}\).

An orientation is a choice, independently for each edge, of one of its two directions; with \(\varepsilon \) edges and two choices each the product rule gives \(2^\varepsilon \). These are labelled objects: two orientations differing only by a symmetry of \(G\) still count separately.

Step 1 is the whole exercise and the Sym2 bookkeeping is the only fiddly part — the natural first move is to prove a helper turning IsOrientationOf into "for each edge, exactly one of the two directions".

The number of Pauli strings with support exactly \(S\) is \(3^{|S|}\), since each coordinate in \(S\) is assigned one of the three non-identity Paulis.

For natural numbers \(n, m \gt 0\) and reals \(\mathrm{val}_f, \mathrm{val}_{f_{L,R}}\), if

then

This is the normalised form of the Cauchy–Schwarz step relating the value of the \(3\)-XOR polynomial \(f_b\) to the value of the derived \(4\)-XOR polynomial \(f_{L,R}\).

For \(t + 1 \le n\) and real \(a \ne x\) there is a scalar \(c \gt 0\) with

For \(t \le n\) and real \(a, x\), the truncated reproducing kernel is

Under the same hypotheses (\(t + 1 \le n\) and \(a\) strictly below every real zero of \(K_t^{(n)}\)), there exists a threshold \(\eta \) such that \(\Phi _{n,t}(a,x) \le 0\) for every integer \(x\) with \(\eta \le x \le n\).

Let \((\Omega ,\mu )\) be a probability space, \(k\gt 0\), and let \(Y:\Omega \to \mathbb {R}\) be measurable with \(Y_*\mu = N(0,1/k)\). For every \(t\in \mathbb {R}\) with \(|t|\le k/4\), the map \(\omega \mapsto \exp \bigl(t(Y(\omega )^2-1/k)\bigr)\) is \(\mu \)-integrable and

The proof combines the Gaussian quadratic MGF closed form (integral_exp_mul_sq_gaussianReal_zero) with the Taylor inequality (neg_log_one_sub_two_mul_le_two_sq) applied at \(s := t/k\).

Let \(Y_1,\dots ,Y_k:\Omega \to \mathbb {R}\) be i.i.d. with law \(N(0,1/k)\) under a probability measure \(\mu \), and let \(0\lt \varepsilon \lt 1\). Then

The proof applies the Bernstein tail bound to the i.i.d. sum of centered chi-squared summands, using hasBernsteinMGF_centered_chi_squared and the generic sum and tail-bound lemmas from the Bernstein framework.

For all \(n\) and \(\alpha \), \(\binom {n}{2\alpha } \le n^{2\alpha }\).

For \(n \ge 2\),

as real numbers.

For naturals \(n\) and \(k\), \(\texttt{chooseR}\, n\, k\) is the binomial coefficient \(\binom {n}{k}\) cast into \(\mathbb {R}\).

(Chvátal and Komlós). Let \(D\) be a digraph with \(\chi \gt mn\), and let \(f\) be a real-valued function on \(V\). Then \(D\) has either a directed path \((u_{0}, \dots , u_m)\) with \(f(u_{0}) \le f(u_{1}) \le \dots \le f(u_m)\), or a directed path \((v_{0}, \dots , v_n)\) with \(f(v_{0}) \gt f(v_{1}) \gt \dots \gt f(v_n)\).*

Theorem 10.1 says a high chromatic number forces a long directed path; this refines it by controlling how \(f\) behaves along that path. A large enough chromatic number forces a monotone directed path — weakly increasing of length \(m\), or strictly decreasing of length \(n\). Part (b) reads off Erdős–Szekeres.

Paths are List V with two IsChains — one for adjacency, one for the \(f\)-comparison — plus Nodup, rather than Quiver.Paths, so that the monotonicity condition can be stated alongside. Note the asymmetry \(\le \) versus \(\gt \) is the book’s and is essential: with two weak orders step 3 would fail on an arc where \(f u = f w\).

(Chvátal and Lovász, 1974). *A loopless digraph \(D\) has an independent set \(S\) such that each vertex of \(D\) not in \(S\) is reachable from a vertex in \(S\) by a directed path of length at most two.*

Such a set is called a semi-kernel. The independence requirement is what makes it non-trivial — one wants mutually non-adjacent "dominators" from which everything else is within two steps. Corollary 10.2 is the tournament case, where independence forces \(|S| = 1\).

The \(u = v\) disjunct in the goal covers the reflexive case and is not in the book, which says "each vertex not in \(S\)"; it is harmless and makes the statement easier to instantiate. hloop : Irreflexive D.Adj is B&M’s "loopless". IsIndepSet is taken in toSimpleGraphInclusive, matching "independent set" for the underlying graph.

For isotropic \(S\),

A CNF formula is a conjunction of clauses, each clause a disjunction of literals; it is represented as \(\mathtt{CNF}\, n = \mathtt{List}\, (\mathtt{Term}\, n)\) with dual evaluation semantics.

A CNF formula evaluates to true on input \(x\) iff every clause holds under \(x\).

A single CNF clause evaluates to true on input \(x\) iff some literal in it holds under \(x\) (disjunction semantics).

The width of a CNF formula \(c\), defined as the maximum width over its clauses (and \(0\) for the empty formula).

Converts a CNF \(\psi \) to its De Morgan dual DNF by negating every literal, so each clause (a disjunction) becomes a term (a conjunction) of negated literals: \(\lnot \bigl(\bigwedge _i \bigvee _j l_{ij}\bigr) = \bigvee _i \bigl(\bigwedge _j \lnot l_{ij}\bigr)\).

\((\mathrm{cnfToDualDNF}\, \psi ).\mathrm{eval}\, x = \lnot \, (\psi .\mathrm{eval}\, x)\).

\((\mathrm{cnfToDualDNF}\, \psi ).\mathrm{width} = \psi .\mathrm{width}\).

An \(n\)-qubit quantum code is a subspace of the \(n\)-qubit Hilbert space \(\mathcal{H}_n\).

\(d(S) = \min \{ \mathrm{wt}(v) \mid v \in S^{\perp _\omega } \setminus S,\; \mathrm{wt}(v) \neq 0\} \) (or \(0\) if no such \(v\) exists).

If \(S\) is isotropic and \(k(S) = 0\), then \(d(S) = 0\).

\(d(S) \le n\).

\(k(S) = n - \dim (S)\).

For naturals \(n\) and \(d\), \(A(n,d)\) is the supremum of the cardinalities \(k\) for which there is a finite set \(C\) of binary codewords \(\mathrm{Fin}\, n \to \mathrm{Bool}\) with \(|C| = k\) and such that any two distinct \(x, y \in C\) differ in at least \(d\) coordinates.

The orthogonal projection of \(\mathcal{H}_n\) onto a subspace \(C\), viewed as an endomorphism \(P_C : \mathcal{H}_n \to \mathcal{H}_n\).

For any \(x \in \mathcal{H}_n\), the value \(P_C\, x\) coincides with the orthogonal projection \(\Pi _C(x)\) of \(x\) onto \(C\).

If \(x \in C\), then \(P_C\, x = x\).

The code projection is idempotent: \(P_C(P_C\, x) = P_C\, x\) for all \(x \in \mathcal{H}_n\).

For any \(x \in \mathcal{H}_n\), the projected vector \(P_C\, x\) belongs to the code subspace \(C\).

A finite set \(C\) of binary words of length \(n\) is \((n,d,w)\)-admissible when any two distinct elements of \(C\) are at Hamming distance at least \(d\) and every element of \(C\) has weight at most \(w\).

The real quantity

If \(n \gt 0\), \(d \ge 1\), and \(2d \le n\), then \(\alpha (n,d) \lt 1\).

For all \(n,d\) one has \(0 \le \alpha (n,d)\).

If \(n \gt 0\) and \(2d \le n\) then \(\alpha (n,d)^2 = (n - 2d)/n\).

Assume \(n \gt 0\), \(1 \le d\) and \(2d \le n\). If \(C\) is a finite set of binary words of length \(n\) whose distinct elements are at Hamming distance at least \(d\), whose weights are all at most \(w\), and if \(w \le J_2(n,d)\), then \(\left\lvert C\right\rvert \le 2n\).

Assume \(n \gt 0\), \(1 \le d\) and \(2d \le n\). Every \((n,d,w)\)-admissible code \(C\) with \(w \le J_2(n,d)\) satisfies \(\left\lvert C\right\rvert \le 2n\).

Let \(n \gt 0\) and let \(C\) be a finite set of binary words of length \(n\) with pairwise Hamming distance at least \(d\) and all weights at most \(w\). If \(\alpha \ge 0\) is such that \(\hat{x}^\alpha \neq 0\) for all \(x \in C\) and \((n - 2d) + \alpha ^2 n + 2\alpha (2w - n) \le 0\), then \(\left\lvert C\right\rvert \le 2n\).

The type of binary words of length \(n\), namely functions \(\mathrm{Fin}\, n \to \mathrm{Bool}\).

For a finite subset \(S\) of an additive group and \(u \in S\), \(\left\lvert S\right\rvert \le \left\lvert \{ \, v \in S : v \neq u \text{ and } v \neq -u \, \} \right\rvert + 2\).

For all binary words \(x,y\) and every coordinate \(i\), \(\mathrm{pmOne}(x)_i \cdot \mathrm{pmOne}(y)_i\) equals \(1\) if \(x_i = y_i\) and \(-1\) otherwise.

Abbreviation for the \(n\)-dimensional real Euclidean space \(\mathbb {R}^n\) with the \(\ell ^2\) inner product, i.e. EuclideanSpace \(\mathbb {R}\) \((\mathrm{Fin}\, n)\).

For a unit vector \(u\) in a finite-dimensional real inner product space \(V\), \(\dim _{\mathbb {R}} (\mathrm{span}_{\mathbb {R}}\{ u\} )^{\perp } = \dim _{\mathbb {R}} V - 1\).

For binary words \(x,y\) of length \(n\), the Hamming distance is the number of coordinates on which they differ: \(\mathrm{hdist}(x,y) = \left\lvert \{ \, i : x_i \neq y_i \, \} \right\rvert \).

\(\langle \mathbf{1}, \mathbf{1}\rangle = n\) in \(\mathbb {R}^n\).

For every binary word \(x\) of length \(n\),

For all binary words \(x,y\) of length \(n\),

Let \(V\) be a real inner product space, \(u \in V\) a unit vector, and \(x,y \in V\) with \(\langle x,u\rangle \le 0\), \(\langle y,u\rangle \le 0\) and \(\langle x,y\rangle \le 0\). Then the components of \(x\) and \(y\) orthogonal to \(u\) satisfy \(\langle x - \langle x,u\rangle u,\ y - \langle y,u\rangle u\rangle \le 0\).

For all \(\alpha \in \mathbb {R}\) and binary words \(x,y\),

If \(\alpha \ge 0\), \(\mathrm{hdist}(x,y) \ge d\), and \(\mathrm{wt}(x), \mathrm{wt}(y) \le w\), then

The real quantity

If \(n \gt 0\), \(2d \le n\), and \(w \le J_2(n,d)\), then for \(\alpha = \alpha (n,d)\)

Given a unit vector \(u\), this packages the normalized projection \(\lVert \mathrm{orthProj}(u,v)\rVert ^{-1}\mathrm{orthProj}(u,v)\) together with its membership proof as an element of the subspace \((\mathrm{span}_{\mathbb {R}}\{ u\} )^{\perp }\).

The value in \(V\) underlying \(\mathrm{mkProj}(u,v)\) is \(\lVert \mathrm{orthProj}(u,v)\rVert ^{-1}\, \mathrm{orthProj}(u,v)\).

If \(u,v\) are unit vectors with \(v \neq u\) and \(v \neq -u\), then \(\lVert \ \lVert \mathrm{orthProj}(u,v)\rVert ^{-1}\, \mathrm{orthProj}(u,v)\ \rVert = 1\).

The rescaling \(u \mapsto \lVert u\rVert ^{-1} \cdot u\) of a vector of \(\mathbb {R}^n\).

Let \(u,v,w\) be unit vectors with \(\langle v,u\rangle \le 0\), \(\langle w,u\rangle \le 0\), \(\langle v,w\rangle \le 0\), with \(v,w \notin \{ u,-u\} \) and \(v \neq w\). Then the normalized projections \(\lVert \mathrm{orthProj}(u,v)\rVert ^{-1}\mathrm{orthProj}(u,v)\) and \(\lVert \mathrm{orthProj}(u,w)\rVert ^{-1}\mathrm{orthProj}(u,w)\) cannot be equal (the statement derives a contradiction from their equality).

Under \(\lVert u\rVert = 1\), \(\langle v,w\rangle \le 0\), \(\langle v,u\rangle \le 0\) and \(\langle w,u\rangle \le 0\) (with both projections nonzero), the normalized projections of \(v\) and \(w\) also have non-positive inner product.

The vector in \(\mathbb {R}^n\) all of whose coordinates equal \(1\).

Every coordinate of \(\mathbf{1} \in \mathbb {R}^n\) equals \(1\): for each \(i\), \(\mathbf{1}_i = 1\).

For \(u,v\) in a real inner product space, \(\mathrm{orthProj}(u,v) = v - \langle u,v\rangle u\), the projection of \(v\) onto the orthogonal complement of \(\mathrm{span}\{ u\} \).

Let \(\lVert u\rVert = 1\) and let \(v,w\) satisfy \(\langle v,w\rangle \le 0\), \(\langle v,u\rangle \le 0\) and \(\langle w,u\rangle \le 0\). Then \(\langle \mathrm{orthProj}(u,v), \mathrm{orthProj}(u,w)\rangle \le 0\).

If \(\lVert u\rVert = 1\) then \(\mathrm{orthProj}(u,v) \in (\mathrm{span}_{\mathbb {R}}\{ u\} )^{\perp }\) for every \(v\).

If \(u\) and \(v\) are unit vectors with \(v \neq u\) and \(v \neq -u\), then \(\mathrm{orthProj}(u,v) \neq 0\).

The map sending a binary word \(x\) to the real vector in \(\mathbb {R}^n\) whose \(i\)-th coordinate is \(-1\) if \(x_i = \texttt{true}\) and \(+1\) otherwise.

If \(x_i = \texttt{false}\) then \(\mathrm{pmOne}(x)_i = 1\).

If \(x_i = \texttt{true}\) then \(\mathrm{pmOne}(x)_i = -1\).

Let \(u\) be a unit vector and \(S\) a set of unit vectors each having non-positive inner product with \(u\). Then \(x \mapsto x - \langle x,u\rangle u\) is injective on \(S\).

If \(u\) and \(x\) are unit vectors with \(\langle x,u\rangle \le 0\) and \(x \neq u\), \(x \neq -u\), then \(x - \langle x,u\rangle u \neq 0\).

For a unit vector \(u\) and any \(x\) in a real inner product space, \(\lVert x - \langle x,u\rangle u\rVert ^2 = \lVert x\rVert ^2 - \langle x,u\rangle ^2\).

Let \(V\) be a finite-dimensional real inner product space and \(S \subseteq V\) a finite set of unit vectors whose pairwise inner products are non-positive. Then \(\left\lvert S\right\rvert \le 2 \dim _{\mathbb {R}} V\).

A finite set \(S\) of unit vectors in \(\mathbb {R}^n\) with pairwise non-positive inner products satisfies \(\left\lvert S\right\rvert \le 2n\).

For a real parameter \(\alpha \) and a binary word \(x\), the vector \(\hat{x}^\alpha = \mathrm{pmOne}(x) - \alpha \cdot \mathbf{1} \in \mathbb {R}^n\).

If \(n \gt 0\) and \(0 \le \alpha \lt 1\), then \(\hat{x}^\alpha \neq 0\) for every binary word \(x\) of length \(n\).

For a binary word \(x\) of length \(n\), its weight is the number of coordinates where \(x\) takes the value true: \(\mathrm{wt}(x) = \left\lvert \{ \, i : x_i = \texttt{true} \, \} \right\rvert \).

For a length-\(n\) code over an alphabet of size \(q\), the ball volume at radius \(t\) is

In the binary case \(q = 2\), the ball volume simplifies to