Separation exponent at least $2.123$ from sharper one-defect profiles

Proved

SensitivityCampaign.reach_2123_near

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

block-sensitivityboolean-functionsperiodic-profilesensitivitysensitivity-2123

For every real $\varepsilon>0$ and every integer $S\ge2$ , there exist a natural number $n$ and a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ satisfying

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

Here sensitivity $s(f)$ and block sensitivity $bs(f)$ are maximized over all inputs, and sensitive blocks must be nonempty and pairwise disjoint. The dimension and function may depend on $\varepsilon$ and $S$ . The exact exponent is $2123/1000$ . This establishes an exponent bound strictly above $2.1$ , with arbitrarily large sensitivity.

Preamble

import Mathlib
import Definitions.Def_SensitivityCampaign
import Theorems.Thm_SensitivityCampaign_finite_certificate
import Theorems.Thm_SensitivityCampaign_finite_certificate_log
open OAI.Paper320

Formal statement

theorem SensitivityCampaign.reach_2123_near :
    SensitivityCampaign.AchievesExponent (2.123 : ℝ) := by sorry

Source

Original sharper one-defect labeling and profile-transfer certificate developed for yousofy with Codex (2026-10-20), K=30541, R=16743, C=338799730753167. The proof uses the generic nested-predicate tournament foundation from Robin Kothari and Codex, accepted 2.075 proof, Prove2Me submission 819ad4c6-aa25-48ca-82e9-c8df39c182c0, https://prove2.me/theorems/49fdd176-c319-4f1e-b15f-b1fd5130f0bc, preserving its earlier OpenAI and community attribution. Previous periodic checkpoint: accepted 2.119 theorem https://prove2.me/theorems/cf005af0-93b2-44c1-991f-ddab41d85874. The new proof includes the one-defect labeling and sharper zero-profile lemmas completely.

View graph

Separation exponent at least 2.1232.1232.123 from sharper one-defect profiles

Separation exponent at least $2.123$ from sharper one-defect profiles