Exact growth-rate separation from shared local-lemma labelings

Proved

SensitivityCampaign.reach_gamma_growth_rate

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

block-sensitivityboolean-functionscoupled-profileexact-growth-ratelovasz-local-lemmasensitivity

Set

\alpha=\frac{\log(25260794820729601)}{\log(50063687)}\approx2.1303199395913162612.

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

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

The logarithmic quotient is the exact lower-bound exponent supplied by this construction; the decimal is only an approximation. Sensitivity and block sensitivity are maximized over all inputs; sensitive blocks are nonempty and pairwise disjoint. Consequently every fixed exponent $c<\alpha$ occurs as a literal power separation for arbitrarily large sensitivity.

Preamble

import Mathlib
import Definitions.Def_SensitivityCampaign

Formal statement

theorem SensitivityCampaign.reach_gamma_growth_rate :
    SensitivityCampaign.AchievesExponent
      (Real.log (25260794820729601 : ℝ) / Real.log (50063687 : ℝ)) := 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