Dependencies

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 uniform probability measure on \(\{ 0,1\} ^n\) assigns weight \(2^{-n}\) to each point.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 Walsh characters form an orthonormal system:

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

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

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

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

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

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

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

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

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 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 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 majority function on \(\{ 0,1\} ^{2k+1}\) outputs \(1\) if more than half the inputs are \(\texttt{false}\), and \(-1\) otherwise.

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

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

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

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

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

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

The Fourier weight at level \(k\) is

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.

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

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

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

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.

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

Summing pairwise sign products over all 6 orderings:

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

The Fourier correlation function of \(f\) is

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

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

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

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

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

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

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

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

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

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

A codeword of length \(n\) over alphabet \(\alpha \) is a function \(c : \mathrm{Fin}\, n \to \alpha \).

Pointwise addition, subtraction, and the all-zero codeword.

A (block) code of length \(n\) over \(\alpha \) is a finite set () of codewords.

A code \(C\) is linear with generator matrix \(G\) (shape \(n\times m\)) if every message \(c':\mathrm{Fin}\, m\to \alpha \) maps to a codeword \(Gc'\in C\), and every codeword in \(C\) arises this way.

Existential version: there exists some \(m\) and generator matrix \(G\) witnessing linearity.

Hamming distance between two codewords, wrapping Mathlib’s .

holds when \(d\) is the minimum Hamming distance of \(C\): there exist distinct codewords at distance exactly \(d\), and no two distinct codewords are closer than \(d\).

The Hamming weight of \(c\) is \(d(c, \mathbf{0})\).

asserts existence of a code of size \(A\) and minimum distance \(d\) that is maximal among all such codes.

The Hamming ball of radius \(l\) around \(c\):

implemented as a .

If a code \(C\) has minimum distance \(d\), then \(d \le n\).

Assuming \(\alpha \) is nontrivial, a code \(C\subseteq \alpha ^n\) with minimum distance \(d\) satisfies

For any center \(c\) and radius \(l\),

If \(C\) has minimum distance \(d\gt 0\), then for distinct \(c_1,c_2\in C\),

Reformulation of the previous lemma as .

Let \(q=|\alpha |\gt 1\). If \(C\subseteq \alpha ^n\) has minimum distance \(d\gt 0\), then

For \(0\lt p\le 1-1/q\) and \(q=|\alpha |\),

For \(q\ge 2\) and \(0\lt p\lt 1\),

Variant using a different exponentiation operator.

For \(x\ge 0\),

For \(0\lt p\lt 1\) and \(q\ge 2\), eventually

For \(q=|\alpha |\) and \(0\lt p\le 1-1/q\),

If \(C\) is linear (witnessed by some generator matrix) and has minimum distance \(d\), then:

• every nonzero codeword in \(C\) has weight at least \(d\);

• some codeword in \(C\) has weight exactly \(d\).

The uniform probability mass function on \(\alpha ^n\), encoded as a function \(\alpha ^n\to \mathbb {R}\) assigning \(1/|\alpha |^n\) to each vector.

For fixed \(x\in \alpha ^k\) and \(v\in \alpha ^n\), the set \(\{ G : Gx=v\} \) is finite.

\(\mu _x(v)\) is the fraction of \(n\times k\) matrices \(G\) satisfying \(Gx=v\).

Utility returning the \(i\)-th row of a matrix as a \(1\times k\) matrix.

If \(x\neq 0\) and \(k\ge 1\), then for a uniformly random \(n\times k\) matrix \(G\) over \(\alpha \), the product \(Gx\) is uniformly distributed over \(\alpha ^n\):

For any nonzero \(x\in \alpha ^k\),

The number of \(n\times k\) matrices that send some nonzero message to a codeword of weight \(\lt d\) is at most

If \(k \le n - \lceil \log _q|B_{d-1}(\mathbf{0})|\rceil - 1\), then there exists a generator matrix \(G\) such that every nonzero message is mapped to a codeword of Hamming weight at least \(d\).

A code \(C\) is \((\rho ,L)\)-list-decodable if every Hamming ball of radius \(\lfloor \rho n\rfloor \) contains at most \(L\) codewords of \(C\).

If the ball volume \(V\) and code size \(M\) satisfy the counting inequality

then there exists a code \(C\) of size \(M\) that is \((p,L)\)-list-decodable.

For \(k\le M\le N\),

For the choice \(r = 1-H_q(\rho )-1/L\), \(M=\lfloor q^{rn}\rfloor \), and \(V=\lfloor q^{H_q(\rho )n}\rfloor \), whenever \(L\lt M\le q^n\),

For any \(q=|\alpha |\), \(0\lt \rho \le 1-1/q\), and \(L\ge 1\), there exist codes of rate \(r = 1-H_q(\rho )-1/L\) that are \((\rho ,L)\)-list-decodable.

A binary codeword of length \(n\) is a function \(\mathrm{Fin}\, n \to \mathrm{Bool}\).

The Hamming weight \(\mathrm{wt}(x) = |\{ i : x_i = 1\} |\); the Hamming distance \(\mathrm{hdist}(x,y) = \mathrm{wt}(x \oplus y)\).

A code \(C \subseteq \{ 0,1\} ^n\) is \((n,d,w)\)-admissible if every pair of distinct codewords has Hamming distance \(\ge d\) and every codeword has weight \(\le w\).

Map \(x \in \{ 0,1\} ^n\) to the vector \(\hat{x}^\alpha _i = (-1)^{x_i} - \alpha \) (with \(\alpha \ge 0\)), viewed in \(\mathbb {R}^n\).

\(\langle \hat{x},\hat{y}\rangle = n - 2\, \mathrm{hdist}(x,y)\).

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

If \(n \gt 0\), \(1 \le d\), \(2d \le n\), and \(w \le J_2(n,d)\), then \((n - 2d) + \alpha ^2 n + 2\alpha (2w - n) \le 0\) for the choice \(\alpha = \alpha (n,d)\).

In a finite inner-product space, if a set \(S\) of unit vectors has pairwise non-positive inner products, then one can project away one vector and reduce to a smaller set in the orthogonal complement with the same property.

A set of unit vectors in an \(n\)-dimensional real inner product space with pairwise non-positive inner products has size at most \(2n\).

A finite set of unit vectors in \(\mathbb {R}^n\) with pairwise non-positive inner products has cardinality at most \(2n\).

Let \(C \subseteq \{ 0,1\} ^n\) be a code with minimum distance \(\ge d\) and all weights \(\le w\). For any \(\alpha \ge 0\) with \((n-2d) + \alpha ^2 n + 2\alpha (2w-n) \le 0\),

If \(n \gt 0\), \(1 \le d\), \(2d \le n\), and all codewords of \(C\) have weight \(\le w \le J_2(n,d)\) and minimum distance \(\ge d\), then \(|C| \le 2n\).

Every \((n,d,w)\)-admissible code \(C\) with \(w \le J_2(n,d)\) satisfies \(|C| \le 2n\).

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

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

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

The four Pauli basis elements \(\{ I,X,Y,Z\} \), represented as an inductive type.

A Pauli string of length \(n\) is a function \(p : \mathrm{Fin}\, n \to \mathrm{PauliBasis}\).

The support \(\mathrm{supp}(p) \subseteq \mathrm{Fin}\, n\) consists of coordinates where \(p(i) \neq I\); the weight is \(\mathrm{wt}(p) = |\mathrm{supp}(p)|\).

The set of all Pauli strings of weight at most \(t\):

The \(n\)-qubit Hilbert space \(\mathcal{H}_n = \ell ^2\! \bigl(\{ 0,1\} ^n,\mathbb {C}\bigr)\), implemented as .

\(\dim _{\mathbb {C}}(\mathcal{H}_n) = 2^n\).

For \(p \in \mathrm{PauliString}\, n\), the associated Pauli operator \(\hat{p} : \mathcal{H}_n \to \mathcal{H}_n\).

A subspace \(C \le \mathcal{H}_n\) satisfies the Knill–Laflamme condition for \(t\)-error correction if for all Pauli strings \(E,F\) with \(\mathrm{wt}(E),\mathrm{wt}(F) \le t\) there exists \(\lambda _{EF}\in \mathbb {C}\) such that \(P_C\, E^\dagger F\, P_C = \lambda _{EF}\, P_C\), where \(P_C\) is the orthogonal projection onto \(C\).

A code is non-degenerate if it satisfies the Knill–Laflamme condition and additionally \(P_C E^\dagger F P_C = 0\) whenever \(E \neq F\).

The error sphere \(\mathrm{ES}(C,t)\) is the subspace \(\bigvee _{\mathrm{wt}(p)\le t} \hat{p}(C)\), i.e. the supremum of the Pauli images of \(C\) over all \(t\)-errors.

If \(C\) is non-degenerate and \(E \neq F\) both have weight \(\le t\), then \(\hat{E}(C) \perp \hat{F}(C)\).

If \(C\) is non-degenerate,

If \(C \le \mathcal{H}_n\) is non-degenerate, then

For \(u = (x,z), v = (x',z') \in V = \mathbb {F}_p^n \times \mathbb {F}_p^n\),

\(\omega \) is bilinear: additive and scalar-homogeneous in each argument.

\(\omega (u,v) = -\omega (v,u)\).

If \(\omega (u,v) = 0\) for all \(v\), then \(u = 0\).

\(\omega \) packaged as a .

The support \(\mathrm{supp}(v) \subseteq \mathrm{Fin}\, n\) consists of coordinates where either component of \(v\) is nonzero; the weight is \(\mathrm{wt}(v) = |\mathrm{supp}(v)|\).

\(\mathrm{wt}(v) \le n\) for all \(v \in V\).

For \(C \subseteq \mathrm{Fin}\, n\), the support submodule \(V_C = \{ v \in V \mid \mathrm{supp}(v) \subseteq C\} \).

\(\dim _{\mathbb {F}_p}(V_C) = 2|C|\).

For a submodule \(S \le V\), \(S^{\perp _\omega } = \{ v \in V \mid \forall s \in S,\; \omega (v,s) = 0\} \).

\(\dim (S^{\perp _\omega }) = 2n - \dim (S)\).

\(S\) is isotropic if \(S \le S^{\perp _\omega }\), i.e. \(\omega (u,v) = 0\) for all \(u,v \in S\).

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

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

An erasure set \(E \subseteq \mathrm{Fin}\, n\) is correctable for \(S\) if every \(v \in V_E \cap S^{\perp _\omega }\) is already in \(S\).

If \(|E| \lt d(S)\), then \(E\) is correctable.

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

Let \(S\) be isotropic. If \(A,B \subseteq \mathrm{Fin}\, n\) are disjoint and both correctable, then

For any isotropic submodule \(S \le V\),