Separation exponent at least
ProvedSensitivityCampaign.reach_source_q5_best_3738277295413674block-sensitivityboolean-functionssensitivity
Set
For every real and every natural number , there exist a natural number and a total Boolean function with
Here is the maximum number of sensitive singleton coordinates over all inputs, and is the maximum number of pairwise disjoint nonempty sensitive blocks over all inputs. This is the campaign's unchanged AchievesExponent predicate at the exact logarithmic value. The decimal is an approximation. The already accepted primitive theorem proves the same quantified assertion and a strict comparison with the preceding five-tolerance bound.
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_source_q5_best_3738277295413674 :
SensitivityCampaign.AchievesExponent (Real.log (1522813785050025472152230187890625 : ℝ) / Real.log (3738277295413674 : ℝ)) := by sorrySource
Exact campaign-template form of https://prove2.me/theorems/01bb63ef-ced2-4ae9-8b81-b5ed295526c6, accepted submission a9d25c46-43bd-4fb1-826b-0ed075b8cf0a. Shared definitions and template from https://prove2.me/campaigns/block-sensitivity-vs-sensitivity. Earlier OpenAI and Robin Kothari/Codex attribution is retained in the accepted source. New construction: yousofy with Codex.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.