Separation exponent at least from a periodic profile invariant
ProvedSensitivityCampaign.reach_2119_periodicblock-sensitivityboolean-functionsperiodic-profilesensitivitysensitivity-2119
For every real and every integer , there exist a natural number and a total Boolean function satisfying
Here sensitivity and block sensitivity are maximized over all inputs, and sensitive blocks must be nonempty and pairwise disjoint. The dimension and function may depend on and . The exact exponent is . This establishes an exponent bound strictly above , 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 sorrySource
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.