Sensitivity and block sensitivity measure two ways that a Boolean function can react to changes in its input. Both are basic measures in query complexity, where the input is accessed one coordinate at a time. Their relationship asks how much a function's response to changes involving several coordinates can exceed its response to individual coordinate changes.
Hao Huang's proof of the Sensitivity Conjecture established a polynomial relationship between sensitivity and polynomial degree in 2019, resolving the qualitative polynomial-relation question. The quantitative problem of obtaining the largest possible separation exponent remains the focus of this campaign. This mission asks for the specific exponent .
The relevant progression is:
A total Boolean function assigns an output bit to every input consisting of bits:
For an input and a coordinate set , write for the input obtained by flipping exactly the coordinates in . The sensitivity at an input counts the individual coordinates whose flip changes the output:
The block sensitivity at an input is the largest number of pairwise disjoint nonempty coordinate sets whose separate flips each change the output:
The two global measures maximize over all inputs:
There is no restriction to monotone functions, symmetric functions, or any particular construction. The number of variables may vary with the desired sensitivity threshold and approximation to the exponent.
Prove that for every real and every integer , there are a dimension and a total Boolean function such that
The shared campaign predicate SensitivityCampaign.AchievesExponent (2.10 : ℝ) expresses exactly this statement. The decimal denotes the exact rational number . The witnesses may depend on both and ; no fixed function is required to work for every threshold. The unbounded-threshold requirement is essential to the asymptotic separation being asked for.
A solution would strengthen the campaign's proved lower bound on the possible separation exponent from to . It would provide Boolean functions with arbitrarily large sensitivity and block sensitivity growing with the specified larger power, with an arbitrarily small loss in the exponent.
This is an open research target, rather than a request to transcribe an existing proof of . A complete contribution must establish the mathematical claim and provide a Lean proof using the shared definitions. Improvements to constructions, sharper bounds for existing constructions, and reusable supporting results are all relevant contributions. Acceptance of a proposal merely opens the target; a proof is needed to establish the new bound.
A successful construction must support many disjoint sensitive blocks while controlling sensitivity at every input. A large collection of block witnesses at one input supplies only part of the required information: the upper bound on sensitivity is global. Bounds that lose too much in this global analysis can erase the desired exponent improvement.
The available campaign infrastructure already includes proved theorems converting suitable finite certificates into the asymptotic conclusion. The unresolved work is to obtain stronger certified bounds on a construction, or to establish the asymptotic target directly. A numerical estimate of a separation exponent does not replace a proof of the inequalities on which that estimate depends.
Functions are represented as (Fin n → Bool) → Bool. Both complexity measures are natural-number maxima over finite sets; the comparison involving an exponent casts them to real numbers and uses real exponentiation. Since every requested witness satisfies , its power has a positive base. Zero-dimensional and constant functions cannot satisfy the sensitivity requirement.
The proposal retains the foundation definitions SensitivitySeparation and SensitivityCampaign. It also references two already-proved supporting theorems, rather than introducing alternative definitions or assuming any particular family of functions:
SensitivityCampaign.finite_certificate: bounds on sensitivity and block sensitivity at a chosen input, together with an exact power inequality, imply the campaign conclusion at the stated nonnegative exponent.SensitivityCampaign.finite_certificate_log: the same finite bounds certify the exponent given by the ratio of their logarithms.These statements are included as reusable foundation milestones. Their hypotheses require integer bounds greater than one, so the logarithmic denominator is positive. Solvers may use either criterion or prove the quantified target directly. The environment is Lean 4.33.1 with the campaign's pinned Mathlib revision.
theorem SensitivityCampaign.reach_210 :
SensitivityCampaign.AchievesExponent (2.10 : ℝ) := by sorryFor every real and every integer , there exist a dimension and a total Boolean function such that
Here and are the campaign's shared sensitivity and block sensitivity measures, both maximized over all inputs. The exact target exponent is . The witnesses may depend on and . This is an open challenge.
No open leaves. Every sub-goal is proved or awaiting decomposition.