Prove2Me

SKValue

Definition

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

This block sets up the Parisi variational formula and stochastic-control framework for the ground state of the Sherrington-Kirkpatrick model. standardGaussian is the N(0,1) law on the reals, and gaussianProduct(ι) is the product of standard Gaussians over a finite index type. For N+1 Gaussian coordinates z, coordinate(N,j,z) reads index j mod (N+1). With step h=T/N and mesh times t_j=jh, euler(T,N,γ,u,z) is the Euler scheme starting at 0 with X_{j+1}=X_j+√h·coordinate(N,j,z)+h·γ(t_j)·u(t_j,X_j). An OrderParameter is a function γ on the reals that, on [0,1), is nonnegative, monotone and right-continuous, and is integrable on (0,1]. A BrownianSpace is a probability space carrying a real Brownian motion B indexed by nonnegative reals, with its natural filtration and a shifted filtration generated by increments of B after time t. An admissible control at time t is a progressively measurable process, for the shifted filtration, bounded in absolute value by 1. controlPayoff(t,x,α) is the expectation of |x+B_1−B_t+∫_0^{1−t}γ(t+s)α_s ds| minus (1/2)∫_0^{1−t}γ(t+s)α_s² ds. phi(t,x) is the supremum of this payoff over admissible controls. gradient and curvature are its first and second derivatives in x. parisi(γ) is phi(0,0)−(1/2)∫0^1 tγ(t)dt, and IsMinimizer(γ) means parisi(γ)≤parisi(η) for every order parameter η. IsDiffusion(γ,X) says X, stopped at time 1, is adapted to the Brownian filtration and, almost surely, X is continuous on [0,1] and satisfies X_t=B_t+∫0^tγ(s)·gradient(s,X_s)ds. For the Ising model, spin maps true to 1 and false to −1; hamiltonian(n,J,σ)=n^{−1/2}Σ{i<j}J{ij}σ_iσ_j; groundStateSequence(n) is (1/n) times the Gaussian expectation, over i.i.d. standard Gaussian couplings J, of the maximum of the Hamiltonian over spin configurations; and groundStateValue is its limit at infinity, defined with limUnder. gradientStopped uses gradient(t,X_t) for t<1 and a terminal variable U at t≥1. ScalarValueConclusion(γ,X) is the defined proposition that the ground-state sequence converges to groundStateValue, and some U exists such that the stopped gradient is a martingale, almost surely |U|≤1, U²=1 and gradient(t,X_t)→U as t→1 from below, E[(gradient(t,X_t)−U)²]→0, groundStateValue=E|X_1|−∫0^1 tγ(t)dt, groundStateValue=E[U·B_1], and groundStateValue equals ∫0^1 E[curvature(t,X_t)]dt with that integrand interval integrable on [0,1]. The remaining definitions build a finite Gaussian discretization: eulerPath runs euler with u=gradient; rawCoefficient is curvature at the Euler path and mesh time; normalizer is the inverse root mean square of rawCoefficient; gaussianIncrement is normalizer times rawCoefficient times the coordinate; roundedSign is the sign of gradient(T,X_N)+2·cdf(coordinate N)−1; coefficientA(j) for j≥1 is E[roundedSign·gaussianIncrement(j−1)] and 0 for j=0; coefficientB(i)=E[roundedSign·coordinate(i−1)]; and shiftedCoefficientSum is Σ{j=0}^{N}A_j·B{j+1}. FiniteGaussianConclusion(γ,X,T) is the defined proposition that eventually in N all normalizers with j<N are positive, shiftedCoefficientSum tends to ∫_0^T E[curvature(t,X_t)]dt, and these integrals over [0,S] tend to groundStateValue as S→1 from below. The block contains only definitions and these two conclusion propositions, with no theorem asserting them.

Definition code
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SKValue.lean; bytes 16..7554
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib

namespace OAI

open MeasureTheory ProbabilityTheory Filter Set
open scoped Topology ENNReal NNReal BigOperators

namespace SKValue

noncomputable def standardGaussian : Measure ℝ := gaussianReal 0 1

instance : IsProbabilityMeasure standardGaussian := by unfold standardGaussian; infer_instance

noncomputable def gaussianProduct (ι : Type) [Fintype ι] : Measure (ι → ℝ) :=
  Measure.pi (fun _ : ι ↦ standardGaussian)
instance gaussianProduct_probability (ι : Type) [Fintype ι] :
    IsProbabilityMeasure (gaussianProduct ι) := by
  unfold gaussianProduct
  infer_instance

def coordinate (N : ℕ) (j : ℕ) (z : Fin (N+1) → ℝ) : ℝ :=
  z ⟨j % (N+1), Nat.mod_lt _ (Nat.succ_pos _)⟩

noncomputable def stepSize (T : ℝ) (N : ℕ) : ℝ := T / N
noncomputable def meshTime (T : ℝ) (N j : ℕ) : ℝ := j * stepSize T N

noncomputable def euler (T : ℝ) (N : ℕ) (γ : ℝ → ℝ) (u : ℝ → ℝ → ℝ)
    (z : Fin (N+1) → ℝ) : ℕ → ℝ
  | 0 => 0
  | j+1 => euler T N γ u z j + Real.sqrt (stepSize T N) * coordinate N j z +
      stepSize T N * γ (meshTime T N j) * u (meshTime T N j) (euler T N γ u z j)

structure OrderParameter where
  coeff : ℝ → ℝ
  nonneg : ∀ t ∈ Ico (0 : ℝ) 1, 0 ≤ coeff t
  monotone : MonotoneOn coeff (Ico (0 : ℝ) 1)
  rightContinuous : ∀ t ∈ Ico (0 : ℝ) 1, ContinuousWithinAt coeff (Ici t) t
  integrable : IntegrableOn coeff (Ioc (0 : ℝ) 1)

structure BrownianSpace where
  Ω : Type
  measurableSpace : MeasurableSpace Ω
  μ : @Measure Ω measurableSpace
  probability : @IsProbabilityMeasure Ω measurableSpace μ
  B : ℝ≥0 → Ω → ℝ
  measurable : ∀ t, @StronglyMeasurable Ω ℝ _ measurableSpace (B t)
  brownian : @IsBrownianReal Ω measurableSpace B μ

attribute [instance] BrownianSpace.measurableSpace BrownianSpace.probability

noncomputable def BrownianSpace.filtration (W : BrownianSpace) :
    Filtration ℝ≥0 W.measurableSpace := Filtration.natural W.B W.measurable

noncomputable def shiftedFiltration (W : BrownianSpace) (t : ℝ) :
    Filtration ℝ≥0 W.measurableSpace :=
  Filtration.natural (fun s ω ↦ W.B (Real.toNNReal t + s) ω - W.B (Real.toNNReal t) ω)
    (fun _ ↦ (W.measurable _).sub (W.measurable _))

def Admissible (W : BrownianSpace) (t : ℝ) (α : ℝ≥0 → W.Ω → ℝ) : Prop :=
  IsProgressive (shiftedFiltration W t) α ∧ ∀ s ω, |α s ω| ≤ 1

noncomputable def controlPayoff (W : BrownianSpace) (γ : OrderParameter)
    (t x : ℝ) (α : ℝ≥0 → W.Ω → ℝ) : ℝ :=
  ∫ ω, (|x + W.B 1 ω - W.B (Real.toNNReal t) ω +
    ∫ s in (0 : ℝ)..(1-t), γ.coeff (t+s) * α (Real.toNNReal s) ω| -
    (1/2 : ℝ) * ∫ s in (0 : ℝ)..(1-t), γ.coeff (t+s) * α (Real.toNNReal s) ω ^ 2) ∂W.μ

noncomputable def phi (W : BrownianSpace) (γ : OrderParameter) (t x : ℝ) : ℝ :=
  sSup {r | ∃ α, Admissible W t α ∧ r = controlPayoff W γ t x α}

noncomputable def gradient (W : BrownianSpace) (γ : OrderParameter) (t x : ℝ) : ℝ :=
  deriv (phi W γ t) x

noncomputable def curvature (W : BrownianSpace) (γ : OrderParameter) (t x : ℝ) : ℝ :=
  deriv (gradient W γ t) x

noncomputable def parisi (W : BrownianSpace) (γ : OrderParameter) : ℝ :=
  phi W γ 0 0 - (1/2 : ℝ) * ∫ t in (0 : ℝ)..1, t * γ.coeff t

def IsMinimizer (W : BrownianSpace) (γ : OrderParameter) : Prop :=
  ∀ η : OrderParameter, parisi W γ ≤ parisi W η

def IsDiffusion (W : BrownianSpace) (γ : OrderParameter) (X : ℝ → W.Ω → ℝ) : Prop :=
  Adapted W.filtration (fun t ω ↦ X (min (t : ℝ) 1) ω) ∧
  (∀ᵐ ω ∂W.μ, ContinuousOn (fun t ↦ X t ω) (Icc (0 : ℝ) 1) ∧
    ∀ t ∈ Icc (0 : ℝ) 1,
      X t ω = W.B (Real.toNNReal t) ω +
        ∫ s in (0 : ℝ)..t, γ.coeff s * gradient W γ s (X s ω))

noncomputable def spin (b : Bool) : ℝ := if b then 1 else -1

noncomputable def hamiltonian (n : ℕ) (J : (Fin n × Fin n) → ℝ)
    (σ : Fin n → Bool) : ℝ :=
  (Real.sqrt (n : ℝ))⁻¹ *
    ∑ i : Fin n, ∑ j : Fin n, if i < j then J (i,j) * spin (σ i) * spin (σ j) else 0

noncomputable def groundStateSequence (n : ℕ) : ℝ :=
  (n : ℝ)⁻¹ * ∫ J, sSup (range (hamiltonian n J)) ∂gaussianProduct (Fin n × Fin n)

noncomputable def groundStateValue : ℝ := limUnder atTop groundStateSequence

noncomputable def gradientStopped (W : BrownianSpace) (γ : OrderParameter)
    (X : ℝ → W.Ω → ℝ) (U : W.Ω → ℝ) (t : ℝ≥0) (ω : W.Ω) : ℝ :=
  if (t : ℝ) < 1 then gradient W γ t (X t ω) else U ω

def ScalarValueConclusion (W : BrownianSpace) (γ : OrderParameter)
    (X : ℝ → W.Ω → ℝ) : Prop :=
  Tendsto groundStateSequence atTop (𝓝 groundStateValue) ∧
  ∃ U : W.Ω → ℝ,
    Martingale (gradientStopped W γ X U) W.filtration W.μ ∧
    (∀ᵐ ω ∂W.μ, |U ω| ≤ 1 ∧ (U ω)^2 = 1 ∧
      Tendsto (fun t ↦ gradient W γ t (X t ω)) (𝓝[<] (1 : ℝ)) (𝓝 (U ω))) ∧
    Tendsto (fun t ↦ ∫ ω, (gradient W γ t (X t ω) - U ω)^2 ∂W.μ)
      (𝓝[<] (1 : ℝ)) (𝓝 (0 : ℝ)) ∧
    groundStateValue = (∫ ω, |X 1 ω| ∂W.μ) - ∫ t in (0 : ℝ)..1, t * γ.coeff t ∧
    groundStateValue = ∫ ω, U ω * W.B 1 ω ∂W.μ ∧
    groundStateValue = ∫ t in (0 : ℝ)..1, ∫ ω, curvature W γ t (X t ω) ∂W.μ ∧
    IntervalIntegrable (fun t ↦ ∫ ω, curvature W γ t (X t ω) ∂W.μ) volume 0 1

noncomputable def eulerPath (W : BrownianSpace) (γ : OrderParameter) (T : ℝ) (N : ℕ)
    (z : Fin (N+1) → ℝ) (j : ℕ) : ℝ :=
  euler T N γ.coeff (gradient W γ) z j

noncomputable def rawCoefficient (W : BrownianSpace) (γ : OrderParameter)
    (T : ℝ) (N j : ℕ) (z : Fin (N+1) → ℝ) : ℝ :=
  curvature W γ (meshTime T N j) (eulerPath W γ T N z j)

noncomputable def normalizer (W : BrownianSpace) (γ : OrderParameter)
    (T : ℝ) (N j : ℕ) : ℝ :=
  (Real.sqrt (∫ z, (rawCoefficient W γ T N j z)^2 ∂gaussianProduct (Fin (N+1))))⁻¹

noncomputable def gaussianIncrement (W : BrownianSpace) (γ : OrderParameter)
    (T : ℝ) (N j : ℕ) (z : Fin (N+1) → ℝ) : ℝ :=
  normalizer W γ T N j * rawCoefficient W γ T N j z * coordinate N j z

noncomputable def roundedSign (W : BrownianSpace) (γ : OrderParameter)
    (T : ℝ) (N : ℕ) (z : Fin (N+1) → ℝ) : ℝ :=
  Real.sign (gradient W γ T (eulerPath W γ T N z N) +
    2 * cdf standardGaussian (coordinate N N z) - 1)

noncomputable def coefficientA (W : BrownianSpace) (γ : OrderParameter)
    (T : ℝ) (N j : ℕ) : ℝ :=
  if j = 0 then 0 else
    ∫ z, roundedSign W γ T N z * gaussianIncrement W γ T N (j-1) z
      ∂gaussianProduct (Fin (N+1))

noncomputable def coefficientB (W : BrownianSpace) (γ : OrderParameter)
    (T : ℝ) (N i : ℕ) : ℝ :=
  ∫ z, roundedSign W γ T N z * coordinate N (i-1) z ∂gaussianProduct (Fin (N+1))

noncomputable def shiftedCoefficientSum (W : BrownianSpace) (γ : OrderParameter)
    (T : ℝ) (N : ℕ) : ℝ :=
  ∑ j ∈ Finset.range (N+1), coefficientA W γ T N j * coefficientB W γ T N (j+1)

def FiniteGaussianConclusion (W : BrownianSpace) (γ : OrderParameter)
    (X : ℝ → W.Ω → ℝ) (T : ℝ) : Prop :=
  (∀ᶠ N in atTop, ∀ j < N, 0 < normalizer W γ T N j) ∧
  Tendsto (shiftedCoefficientSum W γ T) atTop
    (𝓝 (∫ t in (0 : ℝ)..T, ∫ ω, curvature W γ t (X t ω) ∂W.μ)) ∧
  Tendsto (fun S ↦ ∫ t in (0 : ℝ)..S, ∫ ω, curvature W γ t (X t ω) ∂W.μ)
    (𝓝[<] (1 : ℝ)) (𝓝 groundStateValue)



end SKValue
end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/SKValue.lean
Human review

  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph