OAI.SK.main
ProvedThe theorem states that, for every real inverse temperature β>1, the bad mass of the Sherrington-Kirkpatrick heat-bath dynamics tends to 1 as the system size n tends to infinity, both for the continuous-time dynamics and for the discrete-time dynamics. The model has spin configurations x in {±1}^n and disorder J consisting of independent standard Gaussian couplings J_{ij} for pairs i<j; the Hamiltonian is H(x)=(1/√n)·Σ_{i<j} J_{ij} x_i x_j, the Gibbs measure gives x weight exp(βH(x)) divided by the partition function, and the heat-bath kernel picks a uniformly random site i and resamples its spin from the conditional law exp(β y_i h_i)/(2cosh(βh_i)), where h_i is the local field (1/√n)·Σ_j J_{ij} x_j. The discrete kernel is the k-step power of this one-step kernel, and the continuous kernel at time t is the Poisson mixture Σ_k e^{-nt}(nt)^k/k! of the discrete kernels. The distance from a start x is the total variation distance between the kernel at that time and the Gibbs measure. With time scale exp(n^κ), κ=1/10000, the continuous bad mass is the Gaussian-disorder expectation of the total Gibbs mass of starting configurations x whose total variation distance at time exp(n^κ) exceeds 1/4, and the discrete bad mass is the same with k=⌊exp(n^κ)⌋ steps.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/SKBarriers.lean; bytes 2798..2954 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_SKBarriers namespace OAI noncomputable section open scoped BigOperators Topology open MeasureTheory ProbabilityTheory Filter namespace SK
theorem main (β : ℝ) (hβ : 1 < β) :
Tendsto (continuousBadMass β) atTop (𝓝 1) ∧
Tendsto (discreteBadMass β) atTop (𝓝 1) := by
sorry
end SK
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.