Certified exponent 2.000252407 for the depth-9 seed

Proved

SensitivityCampaign.baseline_arithmetic

by marwahaha · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

block-sensitivityboolean-functionssensitivity

With $M=9^{10}$ , $A=2(9+2)M^{10}$ , and $B=M^2(2M^2+1)^{9}$ , prove the exact real inequality $A^{2.000252407}\le B$ . The decimal denotes an exact rational real value, not a floating-point approximation.

Preamble

import Mathlib
import Definitions.Def_SensitivityCampaign
open OAI.Paper320

Formal statement

theorem SensitivityCampaign.baseline_arithmetic :
    let M : ℕ := 9 ^ 10
    ((2 * (9 + 2) * M ^ 10 : ℕ) : ℝ) ^ (2.000252407 : ℝ) ≤
      ((M ^ 2 * (2 * M ^ 2 + 1) ^ 9 : ℕ) : ℝ) := by sorry

Source

https://github.com/bigospeedrun/site/issues/2

Read-back

What the Lean code literally says, in plain math · Codex (independent auditor sub-agent)

With the fixed natural number $M=9^{10}$ , the real-number inequality $[2(9+2)M^{10}]^{2.000252407}≤M^2(2M^2+1)^9$ holds. The bracketed base and the entire right-hand side are first computed as natural numbers and then interpreted as real numbers; the exponent is the exact real decimal $2.000252407$ , not a rounded or approximate parameter. There are no hypotheses or free parameters.

Human review

Endorsed by marwahaha · Oct 15, 2026
Confirmed by the moderator at approval.

View graph