Certified exponent 2.006470828 for the depth-20 seed

Open

SensitivityCampaign.depth_twenty_arithmetic

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

block-sensitivityboolean-functionssensitivity

With $M=9^{21}$ , $A=2(20+2)M^{21}$ , and $B=M^2(2M^2+1)^{20}$ , prove the exact real inequality $A^{2.006470828}\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.depth_twenty_arithmetic :
    let M : ℕ := 9 ^ 21
    ((2 * (20 + 2) * M ^ 21 : ℕ) : ℝ) ^ (2.006470828 : ℝ) ≤
      ((M ^ 2 * (2 * M ^ 2 + 1) ^ 20 : ℕ) : ℝ) := 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^{21}$ , the real-number inequality $[2(20+2)M^{21}]^{2.006470828}≤M^2(2M^2+1)^{20}$ 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.006470828$ , 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