OAI.CriticalSK.fixedBulkDeficit_bounds_s2: intermediate lemma from OpenAI, Critical mixing in the Sherrington-Kirkpatrick model (result family 227)

Proved

OAI.CriticalSK.fixedBulkDeficit_bounds_s2

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.CriticalSK.critical_mixing_bounds, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, Critical mixing in the Sherrington-Kirkpatrick model (result family 227), OpenAI Math Release, September 25, 2026, result family 227, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.CriticalSK.fixedBulkDeficit_bounds of lean/OAI/MathematicalPhysics/CriticalSK/PartitionBounds.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.CriticalSK, with open scoped BigOperators Topology NNReal ENNReal, open scoped BigOperators ENNReal NNReal Real Topology, open MeasureTheory ProbabilityTheory Filter, open scoped ENNReal NNReal, open scoped BigOperators NNReal, open scoped BigOperators, open scoped BigOperators InnerProductSpace, open Module, open Matrix Polynomial, open scoped BigOperators Topology, open Filter, open scoped BigOperators NNReal ENNReal Topology Pointwise Matrix.Norms.Elementwise, open Set Metric MeasureTheory MeasureTheory.Measure, open scoped ENNReal NNReal BigOperators, open MeasureTheory ProbabilityTheory, open scoped ENNReal NNReal Topology, open MeasureTheory MeasureTheory.Measure Set Metric, open scoped NNReal ENNReal BigOperators, open scoped NNReal ENNReal, open ProbabilityTheory, open Metric Set MeasureTheory, open scoped ENNReal Pointwise, open MeasureTheory Filter Set Real):

lemma fixedBulkDeficit_bounds_s2 {n : ℕ} {lam : Fin (n+2) → ℝ} {h s : ℝ}
    (hh : 0 ≤ h) (hs : 0 < s) (hs1 : s ≤ 1)
    (hcost : traceCost (n+1) h s ≤ 1/100) (hlam : lam ∈ spectralGood (n+1) h s)
    (hspace : 32768 ≤ (n+2:ℝ)*s*Real.sqrt s) :
    0 < fixedBulkDeficit lam s ∧ fixedBulkDeficit lam s/(1/(2*s)) ≤ 6*((n+2:ℝ)*s*Real.sqrt s) ∧
    128*(∑ i : Fin n, (fixedEdgeVariance lam s i.succ.succ:ℝ)^2) ≤ (fixedBulkDeficit lam s)^2

Definitions. The statement is written with OAI.CriticalSK.fixedBulkDeficit, OAI.CriticalSK.fixedEdgeVariance, OAI.CriticalSK.spectralGood and OAI.CriticalSK.traceCost (definitions bundle OAIQ074C000 of this split).

Used by. The proofs of OAI.CriticalSK.spectralGood_natural_sphere_bounds_s2, OAI.CriticalSK.spectralGood_orientation_variance_s2 and OAI.CriticalSK.spectralGood_sphere_moment_s2 of this split import it.

Preamble

import Mathlib
import Definitions.Def_OAIQ074C000

Formal statement

section

attribute [-instance] _root_.OAI.SKGap.ComplexMatrix.frobeniusInnerProduct
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section

open scoped BigOperators Topology NNReal ENNReal

open scoped BigOperators ENNReal NNReal Real Topology

open MeasureTheory ProbabilityTheory Filter

open scoped ENNReal NNReal

open scoped BigOperators NNReal

open scoped BigOperators

open scoped BigOperators InnerProductSpace

open Module

open Matrix Polynomial

open scoped BigOperators Topology

open Filter

open scoped BigOperators NNReal ENNReal Topology Pointwise Matrix.Norms.Elementwise

open Set Metric MeasureTheory MeasureTheory.Measure

open scoped ENNReal NNReal BigOperators

open MeasureTheory ProbabilityTheory

open scoped ENNReal NNReal Topology

open MeasureTheory MeasureTheory.Measure Set Metric

open scoped NNReal ENNReal BigOperators

open scoped NNReal ENNReal

open ProbabilityTheory

open Metric Set MeasureTheory

open scoped ENNReal Pointwise

open MeasureTheory Filter Set Real

namespace CriticalSK

lemma fixedBulkDeficit_bounds_s2 {n : ℕ} {lam : Fin (n+2) → ℝ} {h s : ℝ}
    (hh : 0 ≤ h) (hs : 0 < s) (hs1 : s ≤ 1)
    (hcost : traceCost (n+1) h s ≤ 1/100) (hlam : lam ∈ spectralGood (n+1) h s)
    (hspace : 32768 ≤ (n+2:ℝ)*s*Real.sqrt s) :
    0 < fixedBulkDeficit lam s ∧ fixedBulkDeficit lam s/(1/(2*s)) ≤ 6*((n+2:ℝ)*s*Real.sqrt s) ∧
    128*(∑ i : Fin n, (fixedEdgeVariance lam s i.succ.succ:ℝ)^2) ≤ (fixedBulkDeficit lam s)^2 := by
  sorry

end CriticalSK

end

end OAI
end

Source

OpenAI, Critical mixing in the Sherrington-Kirkpatrick model (result family 227), OpenAI Math Release, September 25, 2026, https://github.com/openai/math (result family 227; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-mixing-in-the-Sherrington-Kirkpatrick-model-September-25-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/MathematicalPhysics/CriticalSK/PartitionBounds.lean (declaration OAI.CriticalSK.fixedBulkDeficit_bounds)

View graph