OAI.SKValue.value_consequences

The theorem states three consequences, for a Brownian space W (a probability space carrying a strongly measurable real Brownian motion B indexed by nonnegative reals) and an order parameter γ (a real function that on [0,1) is nonnegative, monotone and right-continuous, and is integrable on (0,1]). Here phi(t,x) is the supremum, over progressive controls α with |α|≤1 adapted to the Brownian increments after time t, of the expected value of |x + B₁ − B_t + ∫₀^{1−t} γ(t+s)α_s ds| − ½∫₀^{1−t} γ(t+s)α_s² ds; gradient and curvature are its first and second x-derivatives (Lean's deriv); parisi(γ) = phi(0,0) − ½∫₀¹ tγ(t)dt; and IsMinimizer means parisi(γ) ≤ parisi(η) for every order parameter η. IsDiffusion for a process X means that X, stopped at time 1, is adapted to the Brownian filtration, and that almost surely X is continuous on [0,1] and satisfies X_t = B_t + ∫₀ᵗ γ(s)·gradient(s, X_s) ds for all t in [0,1]. groundStateSequence(n) is (1/n) times the Gaussian expectation, over i.i.d. standard normal couplings J_{ij} with i<j, of the maximum over spin vectors σ∈{±1}ⁿ of n^{-1/2}Σ_{i<j} J_{ij}σ_iσ_j, and groundStateValue is its limit as n→∞ (taken with Lean's limUnder). First, for every minimizer γ and every diffusion X, ScalarValueConclusion holds: groundStateSequence converges to groundStateValue; and there is a random variable U such that the gradient process, frozen at U from time 1 on, is a martingale; almost surely |U|≤1, U²=1 and gradient(t,X_t) → U as t↑1; the mean-square distance E[(gradient(t,X_t) − U)²] tends to 0 as t↑1; groundStateValue equals E|X₁| − ∫₀¹ tγ(t)dt, equals E[U·B₁], and equals ∫₀¹ E[curvature(t,X_t)]dt, with that integrand interval integrable on [0,1]. Second, for the same hypotheses and any T with 0<T<1, FiniteGaussianConclusion holds: for all large N the normalizers of the Euler-scheme curvature coefficients at mesh steps j<N are positive; a shifted sum of products of Gaussian-projection coefficients, built from a rounded sign of gradient(T, Euler path) + 2Φ(z_N) − 1, converges as N→∞ to ∫₀ᵀ E[curvature(t,X_t)]dt; and ∫₀^S E[curvature(t,X_t)]dt tends to groundStateValue as S↑1. Third, for every W and every minimizer γ, groundStateValue = parisi(γ).