# Average sensitivity of polynomial threshold functions

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Average sensitivity of polynomial threshold functions](../../preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/main.pdf)

## Scope

The formalized result proves the average-sensitivity bound $8d\sqrt n$ for every Boolean threshold function defined by a real multilinear polynomial of degree at most $d$ on the $n$-dimensional cube. The sign convention assigns value $1$ at zero. This establishes the stated asymptotic bound, rather than the separate conjecture identifying exact extremizers.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Average sensitivity of polynomial threshold functions | [GotsmanLinial.lean](../ComparatorChallenges/GotsmanLinial.lean) |