A Paley tournament bound for the sensitivity exponent:
ProvedSensitivityCampaign.paley11987_four_phaseblock-sensitivityboolean-functionscombinatoricssensitivity
For every real and every integer , there are an integer and a total Boolean function such that
Here is the maximum, over all inputs, of the number of individual input bits whose flip changes the output. The block sensitivity is the maximum, over all inputs, of the size of a family of pairwise disjoint nonempty sets of input bits, each of whose simultaneous flip changes the output. The number denotes the exact rational .
The statement uses the campaign's shared definitions of sensitivity, block sensitivity, and SensitivityCampaign.AchievesExponent.
Preamble
import Definitions.Def_SensitivitySeparation import Definitions.Def_SensitivityCampaign import Mathlib.Analysis.SpecialFunctions.Log.Basic
Formal statement
theorem SensitivityCampaign.paley11987_four_phase : SensitivityCampaign.AchievesExponent (2131121719190 / 1000000000000 : ℝ) := by sorry
Source
Original Paley-11987 four-phase Boolean construction and its exact formal certificate. Campaign context: https://prove2.me/campaigns/block-sensitivity-vs-sensitivity. The complete proof source accompanying this submission is the source of the new bound; no external paper is claimed to establish this new exponent.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.