Block sensitivity vs. sensitivity: exponent at least 2.000252407
ProvedSensitivityCampaign.baselineFor every and every integer , there is a total Boolean function with and .
import Mathlib import Definitions.Def_SensitivityCampaign open OAI.Paper320
theorem SensitivityCampaign.baseline :
SensitivityCampaign.AchievesExponent (2.000252407 : ℝ) := by sorryRead-back
What the Lean code literally says, in plain math · Codex (independent auditor sub-agent)
For a Boolean function on bits, let be the maximum, over all inputs, of the number of individual coordinates whose flip changes its output, and let be the maximum size of a family of pairwise disjoint nonempty coordinate sets whose separate flips at input each change its output; the empty family is permitted and has size zero. Write for the maximum of over all inputs . Unconditionally, for the exact real number , for every real and every natural number , there exist a natural number and a Boolean function on bits such that and , with the power taken in the reals. The witnesses may depend on both and , and may be negative; zero-dimensional witnesses are ruled out by .
Confirmed by the moderator at approval.