Majority and Torus Polynomials: Bounded-Lift Lower Bounds and Explicit Constructions
Saint Wesonga
cs.CC
Oct 13, 2026 · v1
TL;DR
Lower bounds and explicit torus polynomial constructions for Majority are formalized in Lean 4 with Mathlib, including Paturi's approximate-degree characterization, with a public repository.
Abstract
Bhrushundi et al. (2019) introduced torus polynomial approximation as an approach to separating Majority from $ACC^0$. In this model, approximation is measured modulo integers. Krishan and Vishwanathan (2026) developed a duality framework for lower bounds and posed five open problems. We resolve two of these, concerning integer lifts and explicit polynomial approximations. An integer lift records the integer shifts that turn a torus approximation into an ordinary real approximation. We show that a degree-d torus polynomial approximating Majority with error at most 1/8 and lift contained in an interval of width $B$ must satisfy $d(B + 1) = Ω(n)$. This rules out low-degree approximating polynomials with lifts in {-1, 0, 1}, answering their Open Problem 2. We also answer Open Problem 5 by giving, for every Boolean function on $n \geq 1$ variables, an explicit torus polynomial approximation of degree at most $n - 1$. Its error is optimal: zero when the accepting set has even cardinality and $2^{-n-1}$ otherwise. The results presented were discovered and formalized in Lean using GPT-6 Astra.
Problem
Torus polynomial approximation has been proposed as a route to separating Majority from ACC^0. Krishan and Vishwanathan posed open problems on integer lifts and on explicit low-degree torus approximations. This work resolves two of them, Open Problems 2 and 5.
Approach
A torus approximation whose integer lift lies in an interval of width B is converted into a real approximation using a Taylor-polynomial decoder of degree O(B+1). Paturi's approximate-degree lower bound for Majority is then applied. For the explicit construction, the full-cube coefficient of the multilinear extension is cancelled, with a parity-character correction when needed. All results, including Paturi's characterization, are formalized in Lean 4 with Mathlib. The formalization builds on an existing Lean circuit-complexity framework and was produced with the help of an AI model.
Results
A degree-d torus approximation of Majority with error at most 1/8 and lift width B must satisfy d(B+1)=Ω(n), with explicit constant c=1/160000 in Lean. This rules out low-degree approximations with lifts in {-1,0,1}. Every Boolean function on n variables has an explicit torus approximation of degree at most n-1 with optimal error: 0 if the accepting set has even size and 2^{-n-1} otherwise.
