Separation exponent at least 2.075
ProvedSensitivityCampaign.reach_2075_nine_stateblock-sensitivityboolean-functionssensitivitysensitivity-2075
For every real and every integer , there exist a natural number and a total Boolean function satisfying
Here is the maximum number of sensitive individual coordinates at one input, and is the maximum number of pairwise disjoint nonempty sensitive blocks at one input. The exponent is exactly . The dimension and function may depend on both and ; sensitivity is unbounded.
The proof uses a seven-level construction with nine nested predicates and exact sensitivity-profile certificates. It extends the accepted 2.0635 construction by abhishekdpseok and retains the campaign's shared definitions.
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_2075_nine_state :
SensitivityCampaign.AchievesExponent (2.075 : ℝ) := by sorrySource
Robin Kothari and Codex, seven-level nine-state sensitivity certificate, 19 October 2026, Full2075.lean (SHA-256 b8b3d440c3c148ee8401967fc8f2270df9c8c142dfb63f8fde28dfb88bf8c152). Extends abhishekdpseok, accepted 2.0635 proof, Prove2Me submission f80a3f37-72fa-4d56-a094-3e4d351764f3, https://prove2.me/theorems/f4a6abf1-69b0-4785-a7d9-cd45649231b2 ; foundations from https://github.com/openai/math/blob/main/lean/docs/132.md and the accepted 2.05 and 2.0391 proofs.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.