Nisan--Szegedy: a Boolean-valued degree- $k$ function is a $k2^{k-1}$ -junta

Proved

AaronsonAmbainis.nisan_szegedy_relevant_card_le_of_boolean_valued

by Goku · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

boolean_cube_combinatoricsboolean_function_complexity

Call a coordinate $i$ relevant for $p$ when $\operatorname{Inf}_i[p]>0$ , that is, when flipping the $i$ -th bit changes the value of $p$ somewhere on the cube. The Nisan--Szegedy theorem bounds the number of relevant coordinates of a Boolean-valued function by a quantity depending on its degree alone, with no reference to the number of variables $N$ :

\#\{\,i:\operatorname{Inf}_i[p]>0\,\}\;\le\;k\,2^{\,k-1}

for every $p$ of degree at most $k$ taking only the values $0$ and $1$ on $\{0,1\}^N$ . Equivalently, such a $p$ depends on at most $k2^{k-1}$ of its variables -- it is a $k2^{k-1}$ -junta.

This is the result that settles the Aaronson--Ambainis conjecture for Boolean-valued functions: a function with boundedly many relevant coordinates must have a coordinate carrying a constant fraction of its variance. The conjecture's difficulty is that the junta conclusion fails once the range is relaxed from $\{0,1\}$ to the interval $[0,1]$ , where a low-degree function may depend on all $N$ variables.

The bound $k2^{k-1}$ cannot be improved substantially; the source records a matching example.

Formalization Note The source works with $\pm1$ -valued functions on $\{-1,1\}^n$ , whereas the hypothesis here is that $p$ takes only the values $0$ and $1$ at cube points. The two are related by $g=1-2p$ , which is $\pm1$ -valued, has the same degree as $p$ , and satisfies $\operatorname{Inf}_i[g]=4\operatorname{Inf}_i[p]$ in the normalisation used here. O'Donnell's total influence $I[g]=\sum_i\mathbb{E}[(D_ig)^2]$ is one quarter of $\sum_i\operatorname{Inf}_i[g]$ , hence equal to $\sum_i\operatorname{Inf}_i[p]$ ; and $\operatorname{Inf}_i[g]>0$ exactly when $\operatorname{Inf}_i[p]>0$ , so the set of relevant coordinates is the same for both. The degree hypothesis is on totalDegree, the syntactic degree of the representative, which bounds the multilinear degree from above -- the safe direction here.

Preamble

import Definitions.Def_AaronsonAmbainis

Formal statement

namespace AaronsonAmbainis

theorem nisan_szegedy_relevant_card_le_of_boolean_valued
    (N k : ℕ) (p : MvPolynomial (Fin N) ℝ)
    (hdeg : p.totalDegree ≤ k)
    (hbool : ∀ x : Fin N → Bool, cubeEval p x = 0 ∨ cubeEval p x = 1) :
    (Finset.univ.filter (fun i : Fin N => 0 < cubeInfl p i)).card ≤ k * 2 ^ (k - 1) := by sorry

end AaronsonAmbainis

Source

O'Donnell, Analysis of Boolean Functions, Cambridge Univ. Press 2014; corrected version arXiv:2105.10386, Theorem 3.4 (p. 70): "Suppose f : {-1,1}^n -> {-1,1} has deg(f) <= k. Then f is a k*2^(k-1)-junta", with the relevant-coordinate count given in its proof discussion (p. 71). Attributed there (Chapter 3 notes, p. 91) to N. Nisan and M. Szegedy, On the degree of Boolean functions as real polynomials, Computational Complexity 4(4):301-313, 1994.

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back — AaronsonAmbainis.nisan_szegedy_relevant_card_le_of_boolean_valued

Setting and notation. Fix natural numbers $N$ and $k$ (both universally quantified, with no positivity or nondegeneracy constraints whatsoever), and let $p$ be a polynomial in $N$ commuting indeterminates $X_0,\dots,X_{N-1}$ with real coefficients.

Boolean points are functions $x : \{0,\dots,N-1\} \to \{\text{false},\text{true}\}$ , of which there are $2^N$ . Each such $x$ is turned into a real point by the coordinatewise map $\widehat{x}(i) = 1$ if $x(i)=\text{true}$ and $0$ otherwise, and evaluation is $E_p(x) := p(\widehat{x})$ . So the cube used is $\{0,1\}^N \subset \mathbb{R}^N$ (the $0/1$ cube, not the $\pm 1$ cube).

Averaging over the cube is $\mathbb{E}[f] = 2^{-N}\sum_{x} f(x)$ , the sum ranging over all $2^N$ Boolean points. For a coordinate $i$ , $x^{\oplus i}$ denotes $x$ with its $i$ -th bit negated. The influence of coordinate $i$ on $p$ is

\mathrm{Infl}_i(p) = 2^{-N}\sum_{x} \bigl(E_p(x) - E_p(x^{\oplus i})\bigr)^2 .

This is the average of a squared difference over all $2^N$ points (so every edge of the cube is counted twice, once from each endpoint), with no extra factor of $\tfrac12$ or $\tfrac14$ .

Hypotheses.

$\deg_{\text{tot}}(p) \le k$ , where $\deg_{\text{tot}}$ is the total degree of the formal polynomial — the maximum, over monomials with nonzero coefficient, of the sum of the exponents. This is a property of the given algebraic representative, not of the induced function on the cube: $X_0^2 - X_0$ is identically $0$ on the cube but has total degree $2$ , so the hypothesis would require $k \ge 2$ for it. By convention the zero polynomial has total degree $0$ .
For every Boolean point $x$ , $E_p(x) = 0$ or $E_p(x) = 1$ . This is a pointwise exact two-valued condition at all $2^N$ cube points — not "bounded in $[0,1]$ ", not "approximately Boolean", not "Boolean on some subset". Equivalently, $p$ restricted to the $0/1$ cube is the indicator function of some subset. The hypothesis is satisfiable (e.g. $p = 0$ , or $p = X_0$ ), so the statement is not vacuous.

Conclusion. Let $S = \{\, i : \mathrm{Infl}_i(p) > 0 \,\}$ be the set of coordinates of strictly positive influence. Because $\mathrm{Infl}_i(p)$ is an average of squares, $\mathrm{Infl}_i(p) > 0$ holds exactly when there is at least one Boolean point $x$ with $E_p(x) \ne E_p(x^{\oplus i})$ . So the filtered cardinality counts the coordinates on which the induced cube function genuinely depends — a count of relevant variables, with no weighting by influence magnitude and no threshold other than "nonzero". The assertion is

|S| \le k \cdot 2^{\,k-1},

an inequality between natural numbers, where $k-1$ is truncated natural-number subtraction.

Points a reader might not expect.

Natural subtraction at $k = 0$ . For $k = 0$ the exponent is $0 - 1 = 0$ rather than $-1$ , so the right-hand side is $0 \cdot 2^{0} = 0$ , not $0 \cdot 2^{-1}$ . The value is $0$ either way because of the leading factor $k$ , so the truncation does not inflate the bound; but the claim at $k=0$ is the sharp assertion that no coordinate has positive influence. For $k = 1$ the bound is $1$ , for $k=2$ it is $4$ , for $k=3$ it is $12$ .
No dependence on $N$ . The right-hand side involves only $k$ ; the conclusion is uniform in the number of variables.
Degenerate parameters silently admitted. $N = 0$ is allowed: then there is exactly one Boolean point, the index set is empty, and the left-hand side is $0$ . $k$ may be arbitrarily large, and $k$ need not be the actual total degree of $p$ — it is only an upper bound, so the conclusion weakens as $k$ grows. There is no requirement that $p$ depend on any of its variables, that $p$ be multilinear, or that both values $0$ and $1$ actually occur.
Cardinality vs. total influence. The bound is on the number of coordinates with nonzero influence, not on $\sum_i \mathrm{Infl}_i(p)$ or on any degree/variance quantity.

Unused definition in the bundle. The imported definitions also provide the cube variance $\mathrm{Var}(p)$ , which does not appear anywhere in this theorem's statement.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by Goku · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Nisan--Szegedy: a Boolean-valued degree-kkk function is a k2k−1k2^{k-1}k2k−1-junta

Nisan--Szegedy: a Boolean-valued degree- $k$ function is a $k2^{k-1}$ -junta