Strictly improved sensitivity separation with multiplier 50,063,523

Proved

SensitivityCampaign.reach_50063523_strict

by yousofy · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

block-sensitivityboolean-functionssensitivitystrict-exponent-improvement

Let $s(f)$ and $\operatorname{bs}(f)$ denote the sensitivity and block sensitivity of a finite Boolean function. Put

\alpha=\frac{\log(12607^4)}{\log(50063523)}\approx2.1303203332203657.

For every $\varepsilon>0$ and every integer $S\ge2$ , there exist an integer $n$ and a Boolean function $f:\{0,1\}^n\to\{0,1\}$ such that

s(f)\ge S,\qquad \operatorname{bs}(f)\ge s(f)^{\alpha-\varepsilon}.

This endpoint strictly improves the previously established $\log(12607^4)/\log(50063687)\approx2.1303199395913163$ . It is obtained by refining the finite recipe in the coupled recursive construction while retaining the same shared labeling and block amplification. No assertion of optimality is made.

Preamble

import Mathlib
import Definitions.Def_SensitivityCampaign

Formal statement

theorem SensitivityCampaign.reach_50063523_strict : SensitivityCampaign.AchievesExponent
      (Real.log (25260794820729601 : ℝ) / Real.log (50063523 : ℝ)) ∧
    (Real.log (25260794820729601 : ℝ) / Real.log (50063687 : ℝ) <
      Real.log (25260794820729601 : ℝ) / Real.log (50063523 : ℝ)) := by sorry

Source

Refinement of https://prove2.me/theorems/2bc2b8ee-797d-4500-9dc8-9b23c457e131 and the accepted finite construction https://prove2.me/theorems/13efa201-cabf-4776-8b79-3e67e73e02a0. Historical source attribution to Robin Kothari/Codex and earlier OpenAI development is retained in the proof bundle.

View graph