Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Separation exponent at least 2.1192.1192.119 from a periodic profile invariant

Proved
SensitivityCampaign.reach_2119_periodic

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

block-sensitivityboolean-functionsperiodic-profilesensitivitysensitivity-2119

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

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

Here sensitivity s(f)s(f)s(f) and block sensitivity bs(f)bs(f)bs(f) are maximized over all inputs, and sensitive blocks must be nonempty and pairwise disjoint. The dimension and function may depend on ε\varepsilonε and SSS. The exact exponent is 2119/10002119/10002119/1000. This establishes an exponent bound strictly above 2.12.12.1, 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_2119_periodic :
    SensitivityCampaign.AchievesExponent (2.119 : ℝ) := by sorry
Source
Original exact periodic two-stage invariant certificate developed for yousofy with Codex (2026-10-20), with K=44759, R=24501, and C=83673433898775. It uses the generic nested-predicate tournament construction 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. The complete proof preserves the upstream attribution. Previous checkpoint: accepted 2.085 certificate, submission c6096517-61e7-4f51-bc68-c1521d61eb65, https://prove2.me/theorems/7e54a28e-196b-40a3-a2c0-957e75db9e4f.
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me