OAI.SKGapCutoff.Recipe.buffered_root_direction_weak: intermediate lemma from OpenAI, A spectral gap throughout the high-temperature Sherrington-Kirkpatrick phase (result family 227)

Proved

OAI.SKGapCutoff.Recipe.buffered_root_direction_weak

by dbenbenn · Oct 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.SKGap.sk_main, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, A spectral gap throughout the high-temperature Sherrington-Kirkpatrick phase (result family 227), OpenAI Math Release, September 24, 2026, result family 227, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.SKGapCutoff.Recipe.buffered_root_direction_weak of lean/OAI/Probability/SKGap/Localization/LocalExtraction.lean at commit 1581d4c, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.SKGapCutoff.Recipe, with open scoped BigOperators Matrix.Norms.Frobenius, open SKGap.Stein Primary Static):

theorem buffered_root_direction_weak {j K B Aroot ε c r₀ R ρ : ℝ}
    (hj : 0≤j) (hK : 0≤K) (hB : 0≤B) (hA : 1≤Aroot) (hc : 0 < c)
    (hr₀ : 0 < r₀) (hρ : 0<ρ) (hε : 0≤ε) (hAR : Real.exp (R/2)≤Aroot)
    (hbuffer : (K+4*j)*(2*ρ) < r₀)
    (hR : (1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ)≤R)
    (hsmall : (3*Real.exp (R/2)+2)*((1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ))≤ε)
    (himplicit : (1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ)≤
      c/(2*(|j| *Real.exp (R/2)*(3*Real.exp (R/2)+16)+1)))
    (habsorb : (|j| *|literalSizeBudget j c R K
        (KernelExpr.dr (KernelExpr.atom 0 0 false))|)*
      ((1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ))≤(1:ℝ)/2)
    (k : ℕ) :
    ∃A≥1,∀W C : ℝ,0≤W→0≤C→∀(Ω : Type u) (n : Ω→ℕ)
      (J : ∀b,Interaction (n b)) (h e : ∀b,Fin (n b)→ℝ) (P : ∀b,Observables (n b)),
      (∀b,0<n b)→(∀b,(J b).IsSymm)→(∀b,vectorNorm (e b)≤1)→
      (∀b,StartedMatrixEvent j K (Real.exp (R/2)) A (c/2) B W C (k+3) (2+2*(k+1)) (J b))→
      (∀b,¬SKGap.rootBad j Aroot ε c r₀ (J b) (h b))→
      (∀b,4*(residualDerivativeBudget j K B k+residualDerivativeBudget j K B (k+1))≤ρ*Real.sqrt (n b:ℝ))→
      (∀b x,0≤P b x)→(∀b,∑x,P b x=1)→
      (∀b x i,conditionalMean (P b) x i=mag j (J b) (h b) 1 x i)→
      ∃r : ∀b,Fin (n b)→ℝ,(∀b,SKGap.tapField j (J b) (h b) (r b)=0 ∧
          ∀v,SKGap.tapField j (J b) (h b) v=0→v=r b) ∧
      ∃D≥0,∀b (G : Observables (n b)),
        |∑x,P b x*(residualCutoff ρ j (J b) (h b) k x*G x)*
          (∑i,(Real.tanh (fld j (J b) (h b) (k+1) x i)-Real.tanh (r b i))*e b i)|≤D*starNorm (P b) G

Definitions. The statement is written with OAI.SKGap.Field, OAI.SKGap.rootBad, OAI.SKGap.tapField, OAI.SKGapCutoff.Interaction, OAI.SKGapCutoff.Observables, OAI.SKGapCutoff.Spin, OAI.SKGapCutoff.Primary.fld, OAI.SKGapCutoff.Primary.mag, OAI.SKGapCutoff.Recipe.vectorNorm, OAI.SKGapCutoff.Static.conditionalMean, OAI.SKGap.Stein.KernelExpr and OAI.SKGap.Stein.KernelExpr.dr (definitions bundle OAIQ072A000 of this split); OAI.SKGapCutoff.Recipe.StartedMatrixEvent, OAI.SKGapCutoff.Recipe.literalSizeBudget, OAI.SKGapCutoff.Recipe.residualCutoff, OAI.SKGapCutoff.Recipe.residualDerivativeBudget and OAI.SKGapCutoff.Static.starNorm (definitions bundle OAIQ072A002 of this split).

Used by. The proof of OAI.SKGapCutoff.Recipe.buffered_posterior_covariance of this split imports it.

Preamble

import Mathlib
import Definitions.Def_OAIQ072A002

Formal statement

section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section

noncomputable section
open scoped BigOperators Matrix.Norms.Frobenius
namespace SKGapCutoff.Recipe
open SKGap.Stein Primary Static
universe u

theorem buffered_root_direction_weak {j K B Aroot ε c r₀ R ρ : ℝ}
    (hj : 0≤j) (hK : 0≤K) (hB : 0≤B) (hA : 1≤Aroot) (hc : 0 < c)
    (hr₀ : 0 < r₀) (hρ : 0<ρ) (hε : 0≤ε) (hAR : Real.exp (R/2)≤Aroot)
    (hbuffer : (K+4*j)*(2*ρ) < r₀)
    (hR : (1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ)≤R)
    (hsmall : (3*Real.exp (R/2)+2)*((1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ))≤ε)
    (himplicit : (1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ)≤
      c/(2*(|j| *Real.exp (R/2)*(3*Real.exp (R/2)+16)+1)))
    (habsorb : (|j| *|literalSizeBudget j c R K
        (KernelExpr.dr (KernelExpr.atom 0 0 false))|)*
      ((1+2*j)*(1+(1+(K+3*j)/c)*(K+4*j))*(2*ρ))≤(1:ℝ)/2)
    (k : ℕ) :
    ∃A≥1,∀W C : ℝ,0≤W→0≤C→∀(Ω : Type u) (n : Ω→ℕ)
      (J : ∀b,Interaction (n b)) (h e : ∀b,Fin (n b)→ℝ) (P : ∀b,Observables (n b)),
      (∀b,0<n b)→(∀b,(J b).IsSymm)→(∀b,vectorNorm (e b)≤1)→
      (∀b,StartedMatrixEvent j K (Real.exp (R/2)) A (c/2) B W C (k+3) (2+2*(k+1)) (J b))→
      (∀b,¬SKGap.rootBad j Aroot ε c r₀ (J b) (h b))→
      (∀b,4*(residualDerivativeBudget j K B k+residualDerivativeBudget j K B (k+1))≤ρ*Real.sqrt (n b:ℝ))→
      (∀b x,0≤P b x)→(∀b,∑x,P b x=1)→
      (∀b x i,conditionalMean (P b) x i=mag j (J b) (h b) 1 x i)→
      ∃r : ∀b,Fin (n b)→ℝ,(∀b,SKGap.tapField j (J b) (h b) (r b)=0 ∧
          ∀v,SKGap.tapField j (J b) (h b) v=0→v=r b) ∧
      ∃D≥0,∀b (G : Observables (n b)),
        |∑x,P b x*(residualCutoff ρ j (J b) (h b) k x*G x)*
          (∑i,(Real.tanh (fld j (J b) (h b) (k+1) x i)-Real.tanh (r b i))*e b i)|≤D*starNorm (P b) G := by
  sorry

end SKGapCutoff.Recipe

end
end

end OAI
end

Source

OpenAI, A spectral gap throughout the high-temperature Sherrington-Kirkpatrick phase (result family 227), OpenAI Math Release, September 24, 2026, https://github.com/openai/math (result family 227; paper: https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-spectral-gap-throughout-the-high-temperature-Sherrington-Kirkpatrick-phase-September-24-2026/main.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/OAI/Probability/SKGap/Localization/LocalExtraction.lean (declaration OAI.SKGapCutoff.Recipe.buffered_root_direction_weak)

View graph