← All papers
First page of Block Sensitivity can exceed Spectral Sensitivity Squared

Block Sensitivity can exceed Spectral Sensitivity Squared

Alexander Meiburg

cs.CC Aug 1, 2026 · v1 math.CO
The main theorem constructing a Boolean function with block sensitivity exceeding spectral sensitivity squared is formally verified in Lean on Mathlib.
The spectral sensitivity $λ(f)$ of a Boolean function is the largest eigenvalue of the adjacency matrix of its sensitivity graph. It lower-bounds every standard measure of query complexity, and Aaronson, Ben-David, Kothari, Rao and Tal, who introduced it, asked whether block sensitivity is at most quadratic in it: is $bs(f)=O(λ(f)^{2})$? We show that it is not. We construct a total Boolean function on $2017584$ variables with $bs(f)\ge 14011$ and $λ(f)\le 89.0162$, so that $bs(f)\geλ(f)^{2.127}$, and hence by composition a family with $λ(f_n)\to\infty$ and $bs(f_n)=Ω(λ(f_n)^{2.127})$. The function is the indicator of a union of $k$ subcubes indexed by the vertices of a doubly regular tournament, and the freedom left in the construction is fixed by the Lovász local lemma. The main result has been formally verified in Lean. We also give numerical evidence that a member of the same family on $1255$ variables reaches an exponent near $2.20$, and exhibit a member on $30$ variables whose exponent already exceeds $2$ and whose spectral sensitivity can be computed exactly.

Aaronson, Ben-David, Kothari, Rao and Tal asked whether block sensitivity of a Boolean function is at most quadratic in its spectral sensitivity, i.e. bs(f)=O(λ(f)^2). The answer was open.

A total Boolean function is built as the indicator of a union of subcubes indexed by the vertices of a doubly regular tournament. Gate variables are chosen via the Lovász local lemma to control local certificate incidences, bounding spectral sensitivity. A spectral lemma reduces λ(f)^2 to two local counts, and parameters (k,r) are optimized. The main quantitative bound is formally verified in Lean on top of Mathlib.

A function on 2017584 variables achieves bs(f)≥14011 and λ(f)≤89.0162, giving bs(f)≥λ(f)^2.127, disproving the quadratic conjecture; iterated composition yields an infinite family with the same exponent.