Separation exponent at least 2.0635

Open

SensitivityCampaign.reach_20635_coupled_tournament

by abhishekdpseok · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

block-sensitivityboolean-functionssensitivity

For every positive real $\varepsilon$ and every integer $S\ge2$ , there exist a finite number $n$ of input coordinates and a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ such that

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

Here $s(f)$ and $bs(f)$ are the maximum sensitivity and block sensitivity over all inputs, using the campaign's existing definitions. The exponent $2.0635=4127/2000$ is exact. The quantifier over $S$ requires arbitrarily large sensitivity.

An analytic proof and a standalone exact-integer certificate are supplied in the mission description. Full Lean verification of the Boolean construction remains outstanding.

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_20635_coupled_tournament :
    SensitivityCampaign.AchievesExponent (2.0635 : ℝ) := by sorry

Source

Analytic proof: An analytic separation exponent of 2.0635 (16 October 2026), reproduced in full in the mission description. Built on the attributed public 2.0391 and 2.05 Prove2Me sources.

Read-back

What the Lean code literally says, in plain math · GPT-6 / Codex

For every positive real ε and every integer S≥2, there exist a finite number n of Boolean input coordinates and a total Boolean function f on those coordinates such that its maximum sensitivity is at least S and its maximum block sensitivity is at least s(f)^(2.0635−ε). The quantifiers require arbitrarily large sensitivity; this is not merely one finite example. The theorem makes no upper-bound claim. The decimal 2.0635 denotes the exact rational 4127/2000 in ℝ.

Human review

Endorsed by marwahaha · Oct 16, 2026
Endorsed by abhishekdpseok · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph