Separation exponent at least $2.1303$ from shared local-lemma labelings

Proved

SensitivityCampaign.reach_21303_gamma

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

block-sensitivityboolean-functionscoupled-profilelovasz-local-lemmasensitivitysensitivity-21303

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.1303-\varepsilon}.

Sensitivity and block sensitivity are maximized over all inputs; the sensitive blocks are nonempty and pairwise disjoint. The dimension and function may depend on $\varepsilon$ and $S$ . The target exponent is exactly $21303/10000$ . In particular, taking $\varepsilon=0.0001$ gives the fixed exponent $c=2.1302$ with arbitrarily large sensitivity.

Preamble

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

Formal statement

theorem SensitivityCampaign.reach_21303_gamma :
    SensitivityCampaign.AchievesExponent (2.1303 : ℝ) := by sorry

Source

New four-stage coupled target/guard construction and a self-contained formal proof of the classical finite asymmetric Lovász local lemma, developed for yousofy with Codex (2026-10-20). Constants: K=12607, joint defect thresholds [23,33,45,57,71], gamma=254/253, fifteen nested predicates, R=50063687, G=12607^4=25260794820729601, C=3418946681687790375032. The standalone proof includes the finite asymmetric local lemma, joint independence, dependency counts, exact integer activity certificate, and actual Boolean/block assembly. Classical asymmetric local lemma: Moser and Tardos, A constructive proof of the general Lovász Local Lemma, arXiv:0903.0544v3, Theorem1.1; only its existential conclusion is used and proved directly here. Retains the generic nested-predicate tournament foundation and attribution from Robin Kothari and Codex, accepted 2.075 proof, Prove2Me submission819ad4c6-aa25-48ca-82e9-c8df39c182c0, https://prove2.me/theorems/49fdd176-c319-4f1e-b15f-b1fd5130f0bc. Earlier coupled-family checkpoint: https://prove2.me/theorems/ddfe4bf3-88be-4876-a196-33c20c0319ff.

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

Separation exponent at least 2.13032.13032.1303 from shared local-lemma labelings

Separation exponent at least $2.1303$ from shared local-lemma labelings