Finite Boolean families from shared local-lemma labelings and a four-stage cycle

Proved

SensitivityCampaign.coupled_gamma_periodic_seeds

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

block-sensitivityboolean-functionscoupled-profilefinite-familylovasz-local-lemmasensitivity

For each integer $m\ge0$ , there exist a dimension $n$ and a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ such that

s(f)\le C\,R^m,\qquad bs(f,0)\ge G^m,

where

C=3418946681687790375032,\quad R=50063687,\quad G=25260794820729601=12607^4.

Here $s(f)$ is the maximum sensitivity over all inputs, and $bs(f,0)$ is block sensitivity at the all-zero input, witnessed by nonempty pairwise disjoint sensitive blocks. The dimension and function may depend on $m$ . The construction uses one shared edge labeling with five simultaneous defect bounds and four repeated tournament stages. This finite-family theorem supplies the exact lower-bound exponent $\log(G)/\log(R)\approx2.13031993959$ , in the campaign's arbitrary positive exponent-loss sense.

Preamble

import Mathlib
import Definitions.Def_SensitivityCampaign
open OAI.Paper320

Formal statement

theorem SensitivityCampaign.coupled_gamma_periodic_seeds (m : ℕ) :
    ∃ (n : ℕ) (f : (Fin n → Bool) → Bool),
      sensitivity f ≤ 3418946681687790375032 * 50063687 ^ m ∧
      25260794820729601 ^ m ≤ blockSensitivityAt f (fun _ => false) := 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