Prove2Me

Separation exponent at least 2.13012.1301 from coupled target and guard profiles

Proved
SensitivityCampaign.reach_21301_coupled

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

block-sensitivityboolean-functionscoupled-profilemultiple-defect-labelingsensitivitysensitivity-21301

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

s(f)≥S,bs(f)≥s(f)2.1301−ε.s(f)\ge S,\qquad bs(f)\ge s(f)^{2.1301-\varepsilon}.

Sensitivity and block sensitivity are maximized over all inputs, and the sensitive blocks are nonempty and pairwise disjoint. The dimension and function may depend on ε\varepsilon and SS. The exact exponent is 21301/1000021301/10000. In particular, setting ε=0.0001\varepsilon=0.0001 gives the fixed exponent c=2.13c=2.13 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_21301_coupled :
    SensitivityCampaign.AchievesExponent (2.1301 : ℝ) := by sorry
Source
Original multiple-defect labeling and coupled target/guard periodic construction developed for yousofy with Codex (2026-10-20), with fifteen nested predicates, K=14207, R=7922, G=201838849 and C=32057676379612508934192581. The proof includes every new combinatorial lemma and actual Boolean-family assembly. It retains the generic nested-predicate tournament foundation and attribution 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. Accepted preceding checkpoints: https://prove2.me/theorems/cf005af0-93b2-44c1-991f-ddab41d85874 and https://prove2.me/theorems/e9d89148-5d69-4758-8795-53a8de4c8bfc.
Human review

  • Endorsed by Shuze Chen · Oct 20, 2026

    Confirmed by the moderator at approval.

  • Endorsed by yousofy · Oct 20, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph