Markov Chain

Motivation

A directed polymer in a random environment is a random walk whose paths are weighted by the disorder they encounter. The walk favors paths with large accumulated weight, and its endpoint distribution can concentrate on a small number of sites even though the number of possible paths grows exponentially. Understanding how much probability remains spread across many small endpoint masses is a basic question about localization. The distinction matters especially beyond exactly solvable polymer models, where explicit formulas for the endpoint law are rarely available. Bates and Chatterjee study this question for independent disorder in every spatial dimension $d\geq1$ under a finite exponential-moment condition Bates and Chatterjee, 2021.

The paper separates two temperature regimes using the limiting free energy. Earlier localization statements detected persistent large atoms. The target here asks whether those atoms account for all endpoint probability in a time-averaged sense. It also specifies the complementary high-temperature behavior, where a suitable vanishing mass threshold captures asymptotically none of the probability. The result is Theorem 1.1 of the preprint, restated as Theorem 6.3 Bates and Chatterjee, 2021, pp. 16, 43.

Setting

Fix $d\geq1$. A path starts at the origin in $\mathbb Z^d$ and makes one of its $2d$ nearest-neighbor moves at each integer time. The environment $(X_{i,x})$ consists of independent, identically distributed real random variables with common law $\mathfrak L$. The disorder law is nondegenerate: it is not concentrated at one number. An inverse temperature $\beta\geq0$ determines the weight of a path $\gamma$ of length $n$:

$$w_\beta(\gamma)=\exp\!\left(\beta\sum_{i=1}^{n}X_{i,\gamma(i)}\right),\qquad Z_n=(2d)^{-n}\sum_{\gamma}w_\beta(\gamma).$$

The endpoint mass function $f_n(x)$ is the sum of weights of paths ending at $x$, divided by the sum of all path weights. Thus $f_n$ is a probability mass function on $\mathbb Z^d$. For $\varepsilon>0$, the $\varepsilon$-atoms are the sites $\mathcal A_n^\varepsilon=\{x:f_n(x)>\varepsilon\}$, and $\rho_n(\omega_n\in\mathcal A_n^\varepsilon)$ is their total mass. The strict inequality matters at a threshold equal to an atom mass.

Write $F_n=\log Z_n/n$ for $n\geq1$, with $F_0=0$, and $\lambda(\alpha)=\log\mathbb E_{\mathfrak L}e^{\alpha X}$. The standing condition is that this exponential moment is finite for every $\alpha\in[-2\beta,2\beta]$. The paper's Theorem A characterizes the high-temperature phase by $\lim_n\mathbb E F_n=\lambda(\beta)$ and the low-temperature phase by $\lim_n\mathbb E F_n<\lambda(\beta)$ Bates and Chatterjee, 2021, pp. 4–5.

Formalization targets

Asymptotic pure atomicity

The goal is both clauses of Theorem 1.1. For every positive deterministic sequence $\varepsilon_i\to0$, low temperature gives

$$\frac1n\sum_{i=0}^{n-1}\rho_i(\omega_i\in\mathcal A_i^{\varepsilon_i})\longrightarrow1 \quad\text{almost surely}.$$

At high temperature there exists a positive deterministic sequence $\varepsilon_i\to0$ for which the same average converges almost surely to $0$. The sequence in this second clause is selected independently of the realized environment. Together the clauses characterize the paper's stronger, almost-sure form of asymptotic pure atomicity Bates and Chatterjee, 2021, Theorems 1.1 and 6.3.

The milestones are fifteen statements of the paper, in the order the proof of the goal uses them:

• the triangle inequality for the distance $d$ on partitioned subprobability measures (Lemma 2.3) and sequential compactness of $(\mathcal S,d)$ (Theorem 2.8);
• continuity of the update law $f\mapsto\mathcal Tf$ into $(\mathcal P(\mathcal S),\mathcal W)$ and of the log moments $f\mapsto\mathbb E\log^q\widetilde F$ (Proposition 3.2);
• convergence of the empirical endpoint measures $\mu_n=\frac1n\sum_{i<n}\delta_{f_i}$ to the fixed-point set $\mathcal K$ (Corollary 4.3); invariant laws charge only states of mass $0$ or $1$ (Proposition 4.4);
• the variational formula for the free energy: $|F_n-\mathcal R(\mu_n)|\to0$ (Proposition 4.5), the lower bound (Proposition 4.6), the key inequality $\sum_{i<n}\mathcal R(\mathcal T^i\delta_{f_0})\ge\mathbb E\log Z_n$ (Lemma 4.8), and $\lim F_n=\inf_{\nu\in\mathcal K}\mathcal R(\nu)$ (Theorem 4.7);
• convergence of $\mu_n$ to the minimizing set $\mathcal M$ (Theorem 4.9), the extrema of $R$ (Lemma 5.1) and the fixed-point characterization of the two phases (Theorem 5.2);
• semicontinuity of the atom functionals (Lemma 6.1), a fixed-threshold criterion for pure atomicity (Lemma 6.2), and a Dini theorem for semicontinuous functions (Lemma 6.4).

Significance

The low-temperature conclusion rules out a residual diffuse component in the time-averaged endpoint law. A vanishing threshold may still be used to collect almost all of the polymer's probability. The high-temperature clause shows that this property distinguishes the phases under the stated moment assumption. The result strengthens a statement that only asks for a positive amount of mass on large atoms, and gives an almost-sure conclusion for the Cesàro averages Bates and Chatterjee, 2021, §§1.2.3, 6.

A formal development would supply a reusable compactification of endpoint probability measures and a checked route from its invariant laws to localization observables. The milestones expose the pieces that need separate verification, and the compactification and variational formula are reusable for the companion mission on geometric localization. The paper proves the mathematical theorem; this mission asks for its Lean proof and the supporting definitions. A compiled statement with sorry is a proof obligation, not a completed machine-checked result.

Difficulty

The endpoint distribution may move through space as time grows, so ordinary pointwise convergence of mass functions does not capture concentration. The compact state space used by the paper permits separated clusters to live on different copies of $\mathbb Z^d$. Its distance identifies translated representatives and loses information about remote mass. A direct application of weak convergence to the event $f(x)>\varepsilon$ also fails at a threshold, because the mass-above-threshold functional is not continuous. The proof must handle its one-sided semicontinuity and the limiting behavior of the update law Bates and Chatterjee, 2021, §§2–3, 6.

Formalization scope

Lean represents sites as Fin d → ℤ and paths as finite step sequences, so the starting point, the $2d$ choices per step, and the normalization of $Z_n$ are explicit. An environment is a measurable independent family on a probability space with common law $\mathfrak L$. The unused time-zero row comes from indexing cells by $\mathbb N$; only rows with index at least one enter the polymer. The moment condition includes the full interval $[-2\beta,2\beta]$, and the disorder law must be nondegenerate. Both phase predicates refer to the canonical product environment, making the classification depend on $\mathfrak L$, $d$, and $\beta$ rather than on an arbitrary realization.

Partitioned subprobability measures are structures of nonnegative summable functions with mass at most one. Their topology is generated by the paper's distance balls. The Borel representation identifies states at distance zero, corresponding to the paper's separation quotient $\mathcal S$. Finite partial isometries carry the degree penalty $2^{-\deg\varphi}$ through an infimum over admissible degrees. The update uses an extended nonnegative sum before conversion to a real denominator. The intended probability law requires the almost-sure finiteness of that denominator and measurability of the update. The real-valued energy integrals require the stated moment condition; a default value for a nonintegrable integral cannot serve as the paper's expectation, and a non-measurable update would make the pushforward $\mathcal Tf$ the zero measure, which is not the paper's object either. The infimum $\inf_{\nu\in\mathcal K}\mathcal R(\nu)$ is taken over the set $\mathcal K$ itself, never as a real infimum whose empty inner range defaults to $0$. The intermediate results in §§3–4 and Lemma 5.1 use the standing $\beta>0$ range. Theorems 1.1 and 5.2 explicitly include $\beta=0$. Wasserstein cost imports the published RWPI.SqrtLasso.transportCost definition.

Solvers can contribute proofs of the compactness, continuity, variational-formula, invariant-law, and atom-functional milestones, or of reusable supporting results such as Lemma 2.11 (measurability of the update) and Corollary 2.5 (when $d(f,g)=0$). The strict positivity of thresholds, nondegenerate disorder, genuine probability laws, and full phase hypotheses are essential: removing any of them could make a formally easy statement unrelated to Theorem 1.1.

Selected references

• Erik Bates and Sourav Chatterjee, The endpoint distribution of directed polymers, Annals of Probability 48 (2020); preprint arXiv:1612.03443v5 (2021). Preprint.

Motivation

Quantum walks give quadratic speed-ups for a class of search problems that classical algorithms solve by running a Markov chain until it hits a marked state. Ambainis's element-distinctness algorithm (Ambainis 2007) and Szegedy's quantization of reversible Markov chains (Szegedy 2004) are the two starting points. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026v4, SIAM J. Comput. 2011) combined them into one search algorithm whose cost is governed by the eigenvalue gap of a reversible chain $P$.

For a non-reversible chain the relevant spectral quantity is not the eigenvalue gap of $P$. It is the singular value gap of a related matrix, the discriminant $D(P)$. In §5 the paper observes that its search algorithm and the proof of its main theorem carry over to non-reversible chains once the eigenvalue gap of $P$ is replaced by the singular value gap of $D(P)$. Positivity of that gap therefore decides whether the algorithm can be used at all. The paper also notes that irreducibility, and even ergodicity, does not guarantee a positive gap. Its Proposition 3 (p. 17, proved in the appendix on pp. 20–21) gives a simple sufficient condition: every state has a positive probability of staying where it is. This mission formalizes that proposition.

Setting

Let $X$ be a finite set of states. A Markov chain on $X$ is a real matrix $P=(p_{xy})_{x,y\in X}$ with nonnegative entries whose rows sum to one; $p_{xy}$ is the probability of moving from $x$ to $y$. The graph underlying $P$ has an edge $x\to y$ whenever $p_{xy}>0$. The chain is irreducible if this graph is strongly connected, so that every state can be reached from every other state.

A stationary distribution of $P$ is a vector $\pi=(\pi_x)_{x\in X}$ with

$$\pi_x>0,\qquad \sum_x \pi_x=1,\qquad \sum_x \pi_x p_{xy}=\pi_y\quad(y\in X).$$

Every irreducible chain has exactly one.

The discriminant of $P$ is the matrix

$$D(P)=\operatorname{diag}(\pi)^{1/2}\cdot P\cdot \operatorname{diag}(\pi)^{-1/2},\qquad D(P)_{xy}=\frac{\sqrt{\pi_x}\,p_{xy}}{\sqrt{\pi_y}},$$

viewed as an operator on $\mathbb C^X$ with the inner product $\langle u,w\rangle=\sum_x\overline{u_x}w_x$. Its singular values $\sigma_0\ge\sigma_1\ge\dots\ge\sigma_{|X|-1}\ge 0$ are the square roots of the eigenvalues of $D(P)^\dagger D(P)$, repeated according to multiplicity. The vector $v=(\sqrt{\pi_x})_{x\in X}$ satisfies $D(P)v=v$ and $v^{\mathsf T}D(P)=v^{\mathsf T}$, so $1$ is always a singular value of $D(P)$. When $P$ is reversible, $D(P)$ is symmetric and its singular values are the absolute values of the eigenvalues of $P$. In general the two can differ.

Formalization targets

Goal: Proposition 3

If $P$ is an irreducible Markov chain on a finite state space $X$ with $p_{xx}>0$ for every $x$, then $D(P)$ has exactly one singular value equal to $1$:

$$\#\{\,i<|X|:\ \sigma_i(D(P))=1\,\}=1 .$$

Together with the bound below, this says that $1=\sigma_0>\sigma_1$, i.e. the singular value gap $1-\sigma_1$ is positive. The goal asserts no explicit lower bound on the gap, so it does not depend on any quantitative estimate.

Milestones, in the order the proof uses them

1. Eq. (9). For unit vectors $u,v\in\mathbb C^X$,

$$|u^\dagger D(P)v|\le\Bigl(\sum_{x,y}|u_x|^2p_{xy}\Bigr)^{1/2}\Bigl(\sum_{x,y}|v_y|^2\tfrac{\pi_x}{\pi_y}p_{xy}\Bigr)^{1/2}\le 1 .$$

2. Lemma 3. Every singular value of $D(P)$ lies in $[0,1]$.
3. §5, p. 17. $v=(\sqrt{\pi_x})$ is a left and right eigenvector of $D(P)$ with eigenvalue $1$.
4. Equality case. If $u,w$ are unit vectors with $u^\dagger D(P)w=1$, then $u_x=w_y\sqrt{\pi_x/\pi_y}$ whenever $p_{xy}>0$.
5. Path chaining. If $u_y=u_x\sqrt{\pi_y/\pi_x}$ along every edge $x\to y$ and $P$ is irreducible, then $u_y=u_{x_1}\sqrt{\pi_y/\pi_{x_1}}$ for all $x_1,y$.

Significance

The result. Proposition 3 is what makes the search algorithm of the paper usable with non-reversible chains. Theorem 8 of the paper bounds the cost of finding a marked element in terms of the singular value gap of $D(P)$, and it needs that gap to be positive. The hypothesis $p_{xx}>0$ costs little: replacing $P$ by $\alpha I+(1-\alpha)P$ for any $\alpha\in(0,1)$ makes every self-loop positive and keeps the stationary distribution. The proposition also connects to the classical study of non-reversible chains: the squared singular values of $D(P)$ are the eigenvalues of the multiplicative reversiblization $PP^*$, which Fill (1991) used to bound convergence to stationarity.

Formalizing it. The proposition and its proof are in the paper and are not in dispute. To our knowledge neither is machine-checked anywhere. The work is a formal proof of the known argument. It exercises Mathlib's recently added singular values of linear maps between finite-dimensional inner product spaces and its theory of irreducible nonnegative matrices, in a setting where the matrix is neither symmetric nor normal.

Difficulty

The obvious route goes through eigenvalues. Irreducibility plus self-loops make $P$ aperiodic, so by Perron–Frobenius the eigenvalue $1$ of $P$ is simple and every other eigenvalue has modulus less than $1$. This does not settle the question. The singular values of a non-normal matrix are not the moduli of its eigenvalues, and the paper points out ergodic chains whose discriminant has zero singular value gap even though their eigenvalue gap is positive. Simplicity of the eigenvalue $1$ of $P$ therefore says nothing about the multiplicity of the singular value $1$ of $D(P)$.

The real content is the equality case of a Cauchy–Schwarz inequality in $\mathbb C^{X\times X}$. It has to be translated into an edge-by-edge relation between the coordinates of the left and right singular vectors, then propagated along directed paths of the chain's graph. The self-loops are what identify the left and right singular vectors with each other. Bookkeeping that is routine on paper costs effort here: passing between the eigenvalue sequence of $D(P)^\dagger D(P)$ and the dimension of its $1$-eigenspace, and between paths in Mathlib's quiver of positive entries and chains of equalities.

Formalization scope

• States and chain. The state space is a Fintype with decidable equality. $P$ is a real matrix in Matrix.rowStochastic ℝ X, and irreducibility is Mathlib's Matrix.IsIrreducible (nonnegative entries and a strongly connected quiver with an edge $x\to y$ iff $p_{xy}>0$). For a row-stochastic matrix this agrees with "every state is reachable from every other state".
• Stationary distribution. It enters as data $\pi$ with the three properties above. Positivity is explicit because $\operatorname{diag}(\pi)^{-1/2}$ needs it. Existence and uniqueness (Perron–Frobenius) are neither needed nor stated.
• Discriminant. $D(P)$ is the complex matrix with entries $\sqrt{\pi_x}p_{xy}/\sqrt{\pi_y}$, acting on EuclideanSpace ℂ X. Its singular values are Mathlib's LinearMap.singularValues, a sequence indexed by $\mathbb N$ that is $0$ beyond $|X|$. The goal counts the indices $i<|X|$ with $\sigma_i=1$. The inner product $u^\dagger D(P)w$ is Mathlib's inner ℂ u (D(P) w). Since the equality-case milestone assumes this equals $1$ exactly, no phase ambiguity remains.
• What is not assumed. Reversibility of $P$ is not assumed. Neither is aperiodicity, primitivity, or a "lazy" bound $p_{xx}\ge 1/2$: the hypothesis is exactly $p_{xx}>0$ for every $x$.
• Ruled-out trivializations. "$1$ is a singular value of $D(P)$" holds for every chain and is not the goal. The goal is that this singular value has multiplicity one. A conclusion such as "some singular value is $<1$" would also be too weak.
• Cost. The paper's search algorithm and its cost bounds (Theorem 8) are out of scope. This mission is purely linear-algebraic.
• Welcome contributions. Proofs of the milestones. The path-chaining milestone is a reusable fact about functions that are multiplicative along the edges of a strongly connected quiver. A general lemma relating the multiplicity of a singular value to the dimension of an eigenspace of $T^\dagger T$ would be useful well beyond this mission.

Selected references

• F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1):142–164, 2011; arXiv:quant-ph/0608026v4. https://arxiv.org/abs/quant-ph/0608026 (DOI 10.1137/090745854)
• M. Szegedy, Quantum speed-up of Markov chain based algorithms, Proc. 45th IEEE FOCS, 32–41, 2004. https://doi.org/10.1109/FOCS.2004.53
• A. Ambainis, Quantum walk algorithm for element distinctness, SIAM J. Comput. 37(1):210–239, 2007; arXiv:quant-ph/0311001. https://arxiv.org/abs/quant-ph/0311001
• J. A. Fill, Eigenvalue bounds on convergence to stationarity for nonreversible Markov chains, with an application to the exclusion process, Ann. Appl. Probab. 1(1):62–87, 1991. https://doi.org/10.1214/aoap/1177005981

Motivation

Open networks of single-server queues with general (non-exponential) interarrival and service times, generalized Jackson networks (GJNs), model manufacturing lines, communication networks and service systems. Their stationary distributions are almost never available in closed form. The standard engineering approximation replaces the scaled queue-length vector by the stationary distribution of a reflected Brownian motion (RBM) in the orthant, which is the diffusion limit of the network in heavy traffic, when every station is close to full utilisation.

The diffusion limit itself (Reiman, 1984) is a statement about the process on finite time intervals. Using the RBM's stationary law as an approximation of the network's stationary law requires interchanging two limits: time to infinity (steady state) and traffic intensity to one (heavy traffic). For a long time this interchange was assumed rather than proved.

Timeline.

• 1984. Reiman proved the process-level heavy-traffic limit for open queueing networks started empty (doi:10.1287/moor.9.3.441).
• 1987. Harrison and Williams characterised when an orthant RBM has a stationary distribution and showed it is unique (doi:10.1080/17442508708833469).
• 1995. Dai related fluid-model stability to positive Harris recurrence of multiclass networks (doi:10.1214/aoap/1177004828).
• 2006. Gamarnik and Zeevi proved the interchange of limits for GJNs whose primitives have exponential moments (arXiv:math/0410066). This mission formalizes that result.

Setting

There are $J$ stations. Station $j$ receives external arrivals with i.i.d. interarrival times of law $F_{A,j}$ (rate $\alpha_j$, or no arrivals at all) and serves jobs first-in-first-out with i.i.d. service times of law $F_{S,j}$ (mean $m_j$, rate $\mu_j = 1/m_j$). A job finishing at $j$ moves to $k$ with probability $p_{jk}$ or leaves. The routing matrix $P$ is substochastic with spectral radius below one. Interarrival and service times have uniformly bounded conditional exponential moments of their residual lives (conditions (1)–(2)). The traffic equation $\lambda = \alpha + P'\lambda$ gives the effective rates $\lambda = [I-P']^{-1}\alpha$ and the traffic intensities $\rho_j = \lambda_j m_j$.

The queue lengths $Q(t)$ are not Markov. The state $\bar Q(t) = (Q(t),\hat a(t),\hat v(t))$, which adds the elapsed interarrival and service times, is a Markov process on $\mathcal X = \mathbb Z_+^J\times\mathbb R_+^{2J}$. A law $\pi$ on $\mathcal X$ is stationary if $\bar Q(0)\sim\pi$ implies $\bar Q(t)\sim\pi$ for all $t\ge0$.

Heavy traffic. Fix a critically loaded network $\Xi$ ($\rho_j=1$ for all $j$) and a vector $\kappa^0>0$. The network $\Xi^n$ slows the arrivals of $\Xi$ at station $j$ by the factor $1-\kappa^0_j/\sqrt n$, so that $\rho^n_j = 1-\kappa_j/\sqrt n<1$ for an explicit $\kappa>0$ (display (17)). Let $\pi^n$ be any stationary distribution of $\Xi^n$, and let $\hat\pi^n$ be the law of $Q^n(0)/\sqrt n$ under $\pi^n$.

The RBM. For a Brownian motion $W$ with drift $\beta$ and covariance $\Gamma$, the RBM $Z$ with parameters $(\beta,\Gamma,I-P')$ solves the Skorohod problem $Z = W + [I-P']Y\ge0$, with $Y$ nondecreasing and increasing only when $Z$ is on the boundary. Here $\beta = -(I-P')M^{-1}\kappa$ and $\Gamma$ is the explicit covariance matrix of Reiman's theorem, built from $\mu$, $\alpha$, $P$ and the squared coefficients of variation $c^2_{a,j}$, $c^2_{s,j}$ of $\Xi$.

Formalization targets

Goal: Theorem 8 (p. 18)

$$\hat\pi^n\ \Rightarrow\ \pi_{\mathrm{RBM}}\qquad(n\to\infty),$$

where $\pi_{\mathrm{RBM}}$ is the unique stationary distribution of the $(\beta,\Gamma,I-P')$-RBM. The formal goal asserts three things: a stationary distribution of the RBM exists, it is the only one, and $\hat\pi^n$ converges weakly to it, for every choice of stationary distributions $\pi^n$.

Milestones

1. Theorems 5 and 6 (pp. 15–16). For a general Markov process, a geometric Lyapunov function $\Phi$ gives $\mathbb E_\pi\Phi\le\phi(t_0)K/(1-\gamma)$. A Lyapunov function with control of $L_2$ gives an exponential tail $\mathbb P_\pi(\Phi>s)\lesssim e^{-\theta s}$.
2. Proposition 1 (p. 11). The fluid model drains in time at most $w'z/\min_j\mu_j(1-\rho_j)$, where $w=e'[I-P']^{-1}$.
3. Lemma A.1 and Propositions 2–3 (pp. 17, 25). The net input deviates from its fluid path by $O(\sqrt n)$ uniformly over initial states. As a result, $\Phi(z,a,v)=w'z$ is a Lyapunov function for $\Xi^n$ with drift $-\sqrt n$ over time $nt_0$.
4. Theorem 7 and Corollary 1 (pp. 17–18). $\mathbb P_{\pi^n}(n^{-1/2}w'Q^n(0)>s)\le C_1e^{-c_1s}$ uniformly in $n$. Hence $\{\hat\pi^n\}$ is tight.
5. Theorems 4, 3 and 2 (cited). Reiman's process limit from a general initial law; Harrison and Williams's existence and uniqueness theorem for the RBM's stationary distribution; existence of $\pi^n$.

Significance

The result. Theorem 8 justifies the use of the RBM's stationary distribution, which is computable or at least numerically tractable, as an approximation of steady-state queue lengths of a heavily loaded network. Theorem 7 also shows that each stationary queue is of order $(1-\rho^{*n})^{-1}$ uniformly in $n$. Together with Theorem 8 this gives convergence of all moments (Corollary 2 of the paper) and, through Theorems 9–12, steady-state approximations of sojourn times and product-form limits.

Formalizing it. No part of this argument is machine-checked. The formalization would add reusable infrastructure for queueing theory in Lean: a Markov-state model of a generalized Jackson network with residual times, Lyapunov bounds on stationary distributions of general Markov processes (Theorems 5–6), and the link between tightness and identification of limit points for stationary laws. Reiman's theorem (Theorem 4) and the Harrison–Williams theorem (Theorem 3) are cited by the paper and are themselves open formalization targets.

Difficulty

Tightness and Reiman's theorem do not combine on their own. Reiman's theorem describes the network on finite time intervals, started empty, while a stationary distribution describes it as time goes to infinity; nothing in the finite-horizon limit forces a limit point of $\hat\pi^n$ to be stationary for the RBM, or forces different subsequences to have the same limit. The interchange therefore needs the process limit from an arbitrary initial law and the uniqueness of the RBM's stationary law, besides tightness.

The tightness step is the technical core. Moment bounds must be uniform in $n$ and in the initial residual times. A Lyapunov argument on the workload $w'Q$ over a time horizon of order $n$ requires deviation bounds of order $\sqrt n$ for renewal processes started at arbitrary ages. This is why the residual-life conditions (1)–(2) appear, and why the strong approximation of Lemma A.2 is used. A naive drift argument over a fixed time horizon fails: in heavy traffic the drift of $w'Q$ per unit time is only of order $n^{-1/2}$.

Formalization scope

• Stations are Fin J, vectors Fin J → ℝ, $P'$ is Pᵀ, and the norm $\|\cdot\|$ is the $\ell^1$ norm, written as an explicit sum. The spectral-radius condition is $P^m\to0$.
• A network is its data $(\mathcal J, F_A, F_S, P)$ plus the predicate IsGJN (positive times, conditions (1)–(2), substochastic $P$). $A_j$ and $S_j$ count renewal epochs in $[0,t]$. The initial times $a_j(0)$, $v_j(0)$ are residual lives given the elapsed ages $\hat a_j(0)$, $\hat v_j(0)$. States carry their elapsed times as reals; the predicate InStateSpace cuts out $\mathcal X=\mathbb Z_+^J\times\mathbb R_+^{2J}$, and the uniform bounds over initial states (Lemma A.1, Propositions 2–3) and the initial laws of Theorem 4 range over $\mathcal X$ only.
• A realization from an initial law is a probability space carrying the primitives with their joint law and processes $Q, B$ satisfying the dynamics (4)–(5) almost surely. $\mathbb E[\cdot\mid\bar Q(0)=x]$ is the expectation under a realization from $\delta_x$. Stationarity of $\pi$ means: a realization from $\pi$ exists, and every realization from $\pi$ has $\bar Q(t)\sim\pi$ for all $t\ge0$.
• The heavy-traffic scaling is read as $a^n_j = a_j/(1-\kappa^0_j/\sqrt n)$. The printed $a_j(1-\kappa^0_j/\sqrt n)$ would overload every $\Xi^n$, so no $\pi^n$ would exist. $\kappa$ is defined so that (17) holds exactly, and every statement about $\Xi^n$ is for all large $n$.
• The RBM is built on the published Reiman84.QueueLength.Paths (Brownian motion with drift and covariance, and the reflection pair). An RBM stationary law must be a probability measure carried by $\mathbb R^J_+$. Weak convergence of laws on $\mathbb R^J$ uses Mathlib's topology on ProbabilityMeasure. Theorem 4's process convergence is in coupling form with the uniform topology on $[0,T]$.
• Quantities $\limsup_n(\cdot)<\infty$ are rendered as one finite bound valid for all large $n$. Expectations of nonnegative quantities are lower Lebesgue integrals in $[0,\infty]$. Constants "depending only on $\Xi$" are quantified before $n$ and before the stationary distributions.
• Disclosed departures from the page:
  • $\phi(t_0)<\infty$ is assumed in Theorem 5.
  • $\{\Phi>K\}\neq\emptyset$ is assumed in Theorem 6. Its tail constant (29) is stated as $(\gamma\theta/2)^{-1}$, which is what the paper's proof yields, instead of the printed $(1-\gamma\theta/2)^{-1}$.
  • $\Gamma$ is positive definite in Theorem 3, the hypothesis of Harrison and Williams.
  • The derivative bound $w'\dot q(t)\le-\min_j\mu_j(1-\rho_j)$ of Proposition 1 is stated for $\rho_j\le1$ at every station; the page states it unconditionally, and it fails when two stations are overloaded.
  • Theorems 5 and 6 are stated for the time-$t_0$ transition kernel of the Markov process.
• A trivializing formalization is ruled out explicitly. The goal keeps the existence and uniqueness of $\pi_{\mathrm{RBM}}$ as conjuncts, stationarity requires a realization to exist, and the RBM's stationary law must live on the orthant. Hence neither an impossible network nor an empty RBM notion makes the goal vacuous.
• Contributions are welcome on any milestone. The cited Theorems 2–4 are substantial on their own, and Theorems 5–6 are independent of queueing.

Selected references

• D. Gamarnik and A. Zeevi, Validity of heavy traffic steady-state approximations in generalized Jackson networks, Ann. Appl. Probab. 16(1), 2006, 56–90. arXiv:math/0410066, doi:10.1214/105051605000000638
• M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9(3), 1984, 441–458. doi:10.1287/moor.9.3.441
• J. M. Harrison and R. J. Williams, Brownian models of open queueing networks with homogeneous customer populations, Stochastics 22, 1987, 77–115. doi:10.1080/17442508708833469
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5(1), 1995, 49–77. doi:10.1214/aoap/1177004828
• H. Chen and D. D. Yao, Fundamentals of Queueing Networks: Performance, Asymptotics, and Optimization, Springer, 2001 (reference [11] of the paper; Chapter 7).

Motivation

Random coordinate frames allow comparison between different sequences of matching directions in a shuffle. The source uses partially observed card lists to obtain estimates for the full permutation law. The source is OpenAI's September 2026 manuscript.

The companion Conditional information under deterministic coordinate sweeps develops the conditional-information side of the same published eight-clause goal. Both manuscripts are represented by this one draft because they point to the identical formal statement, OAI.ThorpResults.remaining_main.

Setting

A Thorp shuffle acts on $2^d$ binary-labelled positions by independent pair switches followed by a cyclic coordinate rotation. A sweep consists of $d$ physical shuffles. Partial observations record an injective ordered list of card positions.

Formalization targets

$$\sup_\sigma\|q_d^{*32800d}\sigma-U\|_{\mathrm{TV}}\to0,\qquad t_{\mathrm{mix}}(d)=\Theta(\log 2^d).$$

Eight asymptotic results about the Thorp shuffle of 2^d cards, whose positions are the d-bit strings, hold simultaneously. One Thorp step on d≥1 bits uses one fair coin for each (d−1)-bit suffix: the first bit of a position is flipped according to the coin of its remaining bits, and then the bits are cyclically rotated; the d=0 step is the identity. A shuffle of t steps composes t independent such steps, and 'distance' is total variation (half the L¹ distance) from the uniform law on permutations. (1) FrameMain: for every ε>0, for all large d and every starting permutation, the law after 32800·d steps is within total variation ε of uniform. (2) InformationMain has three parts. For large d, any k with 8k≤7·2^d, any start and any list of k distinct labelled positions, the law of the images of the labels after 256·d steps is within ε of uniform on injective k-lists. For large d and 16k≤15·2^d, the same list distance after 1024·d steps is at most (2^d)^(−3/2). Finally, distance(d, 2048·d) tends to 0, and for every d the distance from any start equals distance(d, 2048·d). (3) SpectrumMain: there is p>0 such that for all d≥1 the regularTrace at exponent 2p is at most 17/16 (a sum over Young-diagram shapes of size 2^d of dimension times the trace of |Q|^{2p}, where Q is the averaged Specht-module operator of d-step shuffles) and, for every integer M≥p and every σ, the sweep distance after M·d steps (total variation of the shifted law from uniform) is at most 1/8. (4) SignedMain: for all real η,κ with η>0 there is r≥1 such that, for all d≥1, every shape μ of size 2^d and all Young diagrams α,β,γ with |α|+|β|+|γ|=2^d, the logarithm of the weighted moment dim·Re tr((QQ)^r) is at most a(η,d)·signedEntropy(α,β)+remainderBudget(κ,d,|γ|), where a(η,d)=η(1−1/(2√d)), signedEntropy sums log((|α|+|β|)/rowlength) over cells of α and β, and the remainder is 0 if |γ|=0 and otherwise max(0, a(κ,d)·|γ|·log 2^d−|γ|·log(2^d/|γ|)). (5) DegreeSavingMain: there are an even r≥2 and η>0 such that for all d and shapes μ, dim·Re tr((QQ)^r) ≤ dim^(1−η). (6) FullDensityMain: there is v≥1 such that, for every ε>0 and large d, every shifted law after v·d steps has normalized squared L² density distance (2^d)!·Σ_g(law−1/(2^d)!)² below ε. (7) ForwardMixingMain: there is v≥1 such that for large d every shifted law after v·d steps has total variation below ε. (8) OptimalOrderMain: the mixing time, the least t with distance at most 1/4, is Θ(log 2^d).

The goal is OAI.ThorpResults.remaining_main.

Significance

The selected published goal packages eight results, including fixed-list estimates, spectral moments, signed moments, degree savings, full-density convergence, and optimal-order mixing. The detailed clauses below specify the complete bundle. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Changing coordinates must preserve the joint path law, including what has already been revealed. Marginal uniformity of individual cards does not control the full permutation.

Formalization scope

The goal is the shared remaining_main bundle used by several companion manuscripts. It retains all eight formal clauses rather than claiming a new manuscript-specific statement. The displayed bounds are two of those clauses; the full conjunction remains the proof obligation.

The shared definitions are supplied by ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Random coordinate frames and partial permutation laws, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.
• OpenAI, Conditional information under deterministic coordinate sweeps, preprint, September 2026. Companion manuscript.

Motivation

Cutoff means that a Markov chain’s transition from far from equilibrium to near equilibrium occurs in a negligible fraction of its mixing time. The source studies heat-bath dynamics for a disordered mean-field Ising model. The source is OpenAI's September 2026 manuscript.

Setting

The Sherrington–Kirkpatrick model has independent centered Gaussian pair couplings with variance $\beta^2/n$ and zero external field. One discrete update picks a site uniformly and resamples its spin from its conditional Gibbs law. Mixing time uses worst-case total variation distance.

Formalization targets

$$\mathbb P_g\!\left(\frac{t_{\mathrm{mix}}(g,\varepsilon)}{t_{\mathrm{mix}}(g,1-\varepsilon)}>1+\eta\right)\to0\qquad(0\le\beta<1/2,\ 0<\varepsilon<1/2,\ \eta>0).$$

For real parameters β with 0 ≤ β < 1/2, ε with 0 < ε < 1/2, and η > 0, two things hold for the Sherrington–Kirkpatrick model with n spins, where a disorder g is a real coupling for each pair i < j of sites and the Gibbs measure at zero external field has weight proportional to exp((1/2) Σᵢ Σⱼ σᵢ gᵢⱼ σⱼ) on spin configurations σ ∈ {±1}ⁿ (couplings symmetrized, diagonal zero). The dynamics is a heat-bath single-site chain: choose a site uniformly at random, then keep or flip its spin with probabilities proportional to the Gibbs masses of the two configurations (for n = 0 the transition matrix is the identity). The distance after k steps is the maximum over starting configurations of the total variation distance (half the ℓ¹ distance) between the k-step distribution and the Gibbs measure, and mixingTime(g, δ) is the least k whose distance is at most δ (the infimum of the set, so 0 if that set is empty). The disorder law makes the couplings independent centered Gaussians with variance β²/n. First, the probability under this law that the ratio mixingTime(g, ε) / mixingTime(g, 1 − ε) exceeds 1 + η tends to 0 as n → ∞. Second, for all sufficiently large n, every disorder g satisfies mixingTime(g, 1 − ε) > 0.

The goal is OAI.SKRatio.ratio_cutoff.

Significance

The available target gives ratio cutoff in probability over the disorder and eventual positivity of the denominator for every disorder. It isolates a precise mixing-time comparison. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Fast relaxation estimates alone do not prove that all fixed total-variation thresholds become asymptotically equivalent. The worst starting configuration and the random couplings both enter the comparison.

Formalization scope

The attached range is $0\le\beta<1/2$, narrower than the full high-temperature range discussed in the manuscript. The target does not specify the cutoff location. Dynamics is discrete single-site updating; the exceptional $n=0$ transition is the identity.

The shared definitions are supplied by SKRatio. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Sampling a graph with a prescribed degree vector requires moving among realizations without changing degrees. The switch chain performs local edge replacements and asks whether these suffice for rapid global mixing. The source manuscript presents the surrounding research claim.

Setting

States are simple undirected labeled graphs realizing a graphical vector d on n≥4 vertices. The lazy switch chain stays put with probability one half and otherwise proposes one ordered replacement between distinct perfect matchings on four vertices, rejecting invalid proposals.

Formalization target

Prove

$$\tau_{TV}(1/4)\le2n^8,$$

with mixing time zero for a singleton state space. When more than one state exists, prove the spectral-gap lower bound 1/(24n²·binom(n,4)).

The selected formal target is OAI.Problem315.switch_chain_main.

Significance and status

The goal covers every graphical degree sequence under the stated degree bound, without regularity or density restrictions. Connectivity and explicit exponential total-variation decay are available supporting targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Connectivity gives eventual communication but no polynomial rate. The estimate must be uniform across degree vectors and initial graphs.

Formalization scope

The kernel is defined by exact counts of four-vertex proposals, and total variation is the finite half-ℓ₁ distance from uniform measure. The main theorem contains the singleton case explicitly. The manuscript’s exact sampler is not an additional published target here.

Selected references

• OpenAI, Polynomial mixing of the switch chain for every graphical degree sequence, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation: a dimension saving for the binary coordinate sweep

The Thorp shuffle cuts a deck in half, pairs cards in corresponding positions, and lets an independent fair coin order each pair before the pairs are interleaved. On $N=2^d$ cards, removing the deterministic rotation of coordinates turns $d$ physical shuffles into one binary coordinate sweep: in each coordinate direction, in order, every pair of positions differing in that coordinate is independently swapped with probability $1/2$. After one sweep each card is uniform, but the joint permutation retains dependence because cards share switches.

By finite-group Fourier analysis (Diaconis–Shahshahani 1981), fast mixing of the whole deck follows from a power saving $\|K_\lambda\|_{\rm op}\le D_\lambda^{-g}$ for the sweep in every irreducible representation $\lambda$ of $S_N$. The source obtains this saving by first controlling a perturbed sweep, in which each line permutation is mostly uniform, conditionally on prescribed trajectories of some cards, and then transferring the estimate analytically to the binary sweep.

Timeline

• 1973 — Thorp introduces the shuffle in a study of nonrandom shuffling in Faro (Thorp, JASA 1973).
• 1981 — Diaconis and Shahshahani introduce the Fourier upper-bound method for random walks on $S_n$ (Z. Wahrsch. 1981).
• 2005/2008 — Morris proves $O(d^{44})$ physical shuffles for $N=2^d$ with a chameleon process that conditions on the trajectory of an occupied set (SIAM J. Comput. 2008); Montenegro and Tetali sharpen it to $O(d^{29})$ (2006).
• 2009 — Morris proves $O((\log N)^4)$ for every even $N$ (Ann. Probab. 2009); Morris, Rogaway and Stegers analyze selected-card Thorp marginals for small-domain encryption (CRYPTO 2009).
• 2012 — Hoang, Morris and Rogaway use a conditional squared-discrepancy calculation for the swap-or-not shuffle (CRYPTO 2012).
• 2013 — Morris proves $O(d^3)$ for $N=2^d$, exposing complete labeled trajectories successively (CPC 2013).
• 2014–2015 — Czumaj and Vöcking: nearly uniform joint positions of a $(1-\varepsilon)$ fraction of the cards after $O(d^2)$ shuffles (ICALP 2014); Czumaj, switching networks (STOC 2015).
• 2026 — The OpenAI preprint Conditional coordinate sweeps and analytic transfer (OpenAI Math Release, September 26, 2026) proves the binary sweep contraction below, giving $t_{\rm mix}(d)=\Theta(d)$ physical shuffles. The preprint has not been peer reviewed and its results are not formally verified.

Setting

Positions are binary strings $\{0,1\}^d$, $N=2^d$ (Lean: Slot d := Fin d → Bool). For a coordinate $j$, a layer flips bit $j$ of a position $x$ according to a fair coin attached to the edge $\{x,x+e_j\}$; the binary sweep applies the layers for $j=1,\dots,d$ in order, with all coins independent (Lean: binarySweep, binaryLaw d its law on $S_N$). For an irreducible unitary representation $\rho_\lambda$ of $S_N$ of dimension $D_\lambda$, the sweep operator is

$$K_\lambda=\mathbb E_{g\sim B_N}\rho_\lambda(g).$$

Write $B_N^{*w}$ for the law of $w$ independent sweeps and $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.

For the conditional estimate, an ordered product grid is $\Omega=\Omega_1\times\dots\times\Omega_b$ with each $|\Omega_j|=m_j$ a power of two in $[R,R^2]$; a sweep permutes the lines parallel to coordinate $1$, then coordinate $2$, and so on, each line independently with law $L_m(z)=(1-z)U_m+zB_m$. A family $\mathcal H$ of $h$ prescribed trajectories (disjoint at every layer) is conditioned on; the remaining random bijection of the $s-h$ free slots has average $K^{\mathcal H}_\lambda$ in each irreducible $\lambda\vdash s-h$, with line cost $C(\mathcal H)=\sum_{L}\log\bigl(|L|^{h_L}/(|L|)_{h_L}\bigr)$.

Formalization targets

Milestone: conditional sweep moment estimate (Theorem 3.1)

There are a power of two $R\ge2$, an integer $q\ge1$ and $z_*>0$ such that for every grid, every feasible family $\mathcal H$, every $z\in[0,z_*]$ and every irreducible $\lambda\vdash s-h$,

$$\log\|K^{\mathcal H}_\lambda\|_{2q}^{2q}\le -c(s)\log D_\lambda+e(s)\,h\log s-C(\mathcal H),$$

with $c(s)=c_0+1/\sqrt{\log s}$, $e(s)=e_0-1/\sqrt{\log s}$, $c_0=e_0=10^{-4}$, and $\log 0=-\infty$.

Goal: binary sweep contraction (Theorem 1.1)

There are absolute constants $g>0$ and $d_0$ such that for all $d\ge d_0$ and every irreducible unitary representation of $S_{2^d}$ of dimension $D$,

$$\|K_\lambda\|_{\rm op}\le D^{-g};$$

the sign representation is annihilated, $\sum_g B_N(g)\,\mathrm{sgn}(g)=0$; and there is an absolute integer $w$ such that

$$\sup_{\tau\in S_N}\bigl\|B_N^{*w}(\cdot\,\tau^{-1})-U_N\bigr\|_{\rm TV}\xrightarrow[d\to\infty]{}0 .$$

The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Since one binary sweep is exactly $d$ physical shuffles, the goal gives $O(d)$ physical shuffles for mixing from every starting deck, and the support obstruction (Proposition 1.2: $t$ shuffles reach at most $2^{tN/2}$ permutations) gives the matching lower bound $2d-O(1)$; thus $t_{\rm mix}(d)=\Theta(d)$, improving Morris 2013. The power saving in every irreducible representation is a stronger, reusable statement: it controls any number of further sweeps and any function of the permutation through Fourier analysis.

Formalizing it. The goal is stated for explicit finite objects (coins, sweeps, Fourier operators on $\mathbb C^D$), with existential constants only. A formal proof would certify optimal-order mixing for the Thorp sweep. The conditional estimate (Theorem 3.1) is formalized separately and is the natural intermediate milestone.

Difficulty

The obvious induction—split the coordinates and multiply child bounds—breaks because revealing card paths changes the conditional law of the line permutations, and the induction must be stable when more paths are revealed. The source handles this with the line cost $C(\mathcal H)$, which records the exact cost of prescribing positions without replacement. A second obstacle is that the conditional estimate is only available for mostly-uniform lines ($z$ small), while the Thorp sweep is the binary case $z=1$; for a fixed grid the sweep operator is a matrix polynomial in $z$ whose behavior at $z=1$ is not controlled by real-segment bounds alone. Representations of very small "level" (first appearing on few tracked cards) need a separate sparse estimate.

Formalization scope

• Goal (binary_sweep_contraction_and_mixing): three conjuncts. BinaryContractionTarget: $\exists g>0\ \exists d_0\ \forall d\ge d_0\ \forall D$ and every irreducible representation $\rho$ of Equiv.Perm (Slot d) on EuclideanSpace ℂ (Fin D) preserving norms, the operator norm of $\sum_g \mathrm{binaryLaw}(g)\rho(g)$ is at most $D^{-g}$ (real power). Sign: for every $d>0$, $\sum_g \mathrm{binaryLaw}(g)\,\mathrm{sgn}(g)=0$. UniformSweepMixingTarget: $\exists w\ \forall\varepsilon>0\ \exists d_0\ \forall d\ge d_0\ \forall\tau$, total variation of the $w$-fold convolution power translated by $\tau$ from uniform is at most $\varepsilon$. Physical shuffles are not modelled; the statement is about sweeps.
• Milestone (conditional_main): grids are Grid with $b\ge1$ coordinates of $r\le\text{bits}_j\le2r$ ($R=2^r$); trajectories are Holes with disjointness at every layer and coordinate-respecting steps; feasibility means some line choices realize them; the residual bijection is identified with the stabilizer of the input holes via a fixed reference completion; representations are UnitaryIrrep of that stabilizer; the Schatten moment is $\mathrm{Re}\operatorname{Tr}((K^*K)^q)$; $z_*\le1/2$.
• The mapped item all_grid_moment is a parameter-explicit form of the same induction under numerical largeness hypotheses and a small-perturbation hypothesis, kept as a plain item.
• Infrastructure: Specht-module dimension estimates, branching and Pieri rules, signed Schur–Weyl decompositions, Schatten norms, and the subharmonic maximum principle; the analytic-transfer step is reusable for other families of averaging operators polynomial in a parameter.

Selected references

• E. O. Thorp, Nonrandom shuffling with applications to the game of Faro, J. Amer. Statist. Assoc. 68 (1973), 842–847. https://doi.org/10.1080/01621459.1973.10481434
• P. Diaconis and M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981), 159–179. https://doi.org/10.1007/BF00535487
• B. Morris, The mixing time of the Thorp shuffle, SIAM J. Comput. 38 (2008), 484–504. https://doi.org/10.1137/050636231
• R. Montenegro and P. Tetali, Mathematical aspects of mixing times in Markov chains, Found. Trends Theor. Comput. Sci. 1 (2006), 237–354. https://doi.org/10.1561/0400000003
• B. Morris, Improved mixing time bounds for the Thorp shuffle and L-reversal chain, Ann. Probab. 37 (2009), 453–477. https://doi.org/10.1214/08-AOP409
• B. Morris, Improved mixing time bounds for the Thorp shuffle, Combin. Probab. Comput. 22 (2013), 118–132. https://doi.org/10.1017/S0963548312000478
• B. Morris, P. Rogaway and T. Stegers, How to encipher messages on a small domain, CRYPTO 2009, LNCS 5677, 286–302. https://doi.org/10.1007/978-3-642-03356-8_17
• V. T. Hoang, B. Morris and P. Rogaway, An enciphering scheme based on a card shuffle, CRYPTO 2012, LNCS 7417, 1–13. https://doi.org/10.1007/978-3-642-32009-5_1
• A. Czumaj and B. Vöcking, Thorp shuffling, butterflies, and non-Markovian couplings, ICALP 2014, LNCS 8572, 344–355. https://doi.org/10.1007/978-3-662-43948-7_29
• A. Czumaj, Random permutations using switching networks, STOC 2015, 703–712. https://doi.org/10.1145/2746539.2746629
• A. Berele and A. Regev, Hook Young diagrams, combinatorics and representations of Lie superalgebras, Bull. Amer. Math. Soc. (N.S.) 8 (1983), 337–339. https://doi.org/10.1090/S0273-0979-1983-15110-8
• OpenAI, Conditional coordinate sweeps and analytic transfer, OpenAI Math Release preprint, September 26, 2026 (source; Theorem 1.1, p. 2; Theorem 3.1, p. 7). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Conditional-coordinate-sweeps-and-analytic-transfer-September-26-2026/main.pdf

Motivation: optimal-order mixing for the Thorp shuffle

The Thorp shuffle is a simple card-shuffling rule: cut a deck of $n$ cards into two equal halves, pair cards in corresponding positions, and let an independent fair coin decide the order within each pair when the pairs are interleaved. It is a standard test case for mixing-time methods and a building block in small-domain enciphering schemes. For $n=2^d$ every individual card is uniform after $d$ shuffles, but the joint order of all $n$ cards is much harder to control. Determining whether $O(d)=O(\log n)$ shuffles suffice to make the full permutation close to uniform was a long-standing question.

Timeline

• 1973 — Thorp introduces the model in a study of nonrandom shuffling in Faro (Thorp, JASA 1973).
• 2005/2008 — Morris proves the first polynomial-in-$d$ bound, $O(d^{44})$ shuffles for $n=2^d$, using evolving sets and a chameleon process (Morris, SIAM J. Comput. 2008).
• 2006 — Montenegro and Tetali sharpen this to $O(d^{29})$ by spectral-profile and evolving-set estimates (Montenegro–Tetali 2006, §6.4).
• 2009 — Morris introduces an entropy method based on card interactions and obtains $O(\log^4 n)$ for every even deck size (Morris, Ann. Probab. 2009).
• 2013 — Morris obtains $O(d^3)$ for dyadic decks (Morris, CPC 2013).
• 2026 — The OpenAI preprint Random-subspace tests and trace smoothing for coordinate sweeps (OpenAI Math Release, September 26, 2026) claims a uniform bound on a fixed Schatten moment of one coordinate sweep in the full regular representation, which yields total-variation mixing after an absolute number of sweeps, i.e. $O(d)$ physical shuffles. The preprint has not been peer reviewed and its result is not formally verified.

Setting

Index the $n=2^d$ positions by binary strings $x\in\mathbb F_2^d$ (in Lean, Card d := Fin d → Bool). One physical shuffle sends

$$(x_1,x_2,\dots,x_d)\longmapsto(x_2,\dots,x_d,\;x_1+\xi_{x_2,\dots,x_d})$$

with independent fair bits $\xi$ (Lean: step d ξ = rotate * pairSwitch ξ). After $d$ physical shuffles the rotations cancel, and the result is a coordinate sweep: one random matching switch in each coordinate direction. Write $\mu_t$ for the law on $S_n$ of $t$ physical shuffles (Lean: law d t, the fraction of coin sequences producing a given permutation).

For a partition $\lambda\vdash n$ let $V_\lambda$ be the Specht module (the irreducible representation of $S_n$ indexed by $\lambda$), of dimension $D_\lambda$, and let $Q_n(\lambda)=\sum_g \mu_d(g)\,\lambda(g)$ be the average of the sweep in $V_\lambda$. For an operator $Y$, $|Y|=(Y^*Y)^{1/2}$ and traces are unnormalized. The regular trace of the $P$-th power is

$$\operatorname{Tr}_{\rm reg}|Q_n|^P=\sum_{\lambda\vdash n}D_\lambda\operatorname{Tr}_{V_\lambda}|Q_n(\lambda)|^P ,$$

in which the trivial representation contributes exactly $1$. Total variation is $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.

Formalization targets

Goal: regular-trace smoothing (Theorem 1.1)

There is an absolute real $P\ge2$ such that for every $d\ge1$ (so $n=2^d\ge2$)

$$\operatorname{Tr}_{\rm reg}|Q_n|^P\le 1+n^{-10},$$

and for every integer $v$ with $2v\ge P$ and every initial deck $\sigma$,

$$\tfrac12\sum_{g\in S_n}\Bigl|\mu_{vd}(g\sigma^{-1})-\tfrac1{n!}\Bigr|\le\tfrac12\,n^{-5}.$$

The constant $P$ is not specified; only its existence and uniformity in $d$ are asserted. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Since one sweep is $d$ physical shuffles, the second clause shows that $O(d)=O(\log n)$ Thorp shuffles bring the full permutation within $\tfrac12 n^{-5}$ of uniform from every starting deck. A counting argument on coin strings (Proposition 5.1 of the source) shows that at least $2d-O(1)$ physical shuffles are needed, so this order is optimal, improving the $O(d^3)$ bound of Morris 2013. The regular-trace bound is stronger than an operator-norm bound for each irreducible: it controls all singular values with their multiplicities, which is what yields polynomially small total-variation distance.

Formalizing it. The statement is fully finite and explicit: an existential over one real constant followed by inequalities for each $d$. A formal proof would certify an optimal-order mixing bound for a widely studied shuffle. Specht modules, Schatten-type traces via continuous functional calculus, and the shuffle law are all defined in the mission's definition file and can be reused for related shuffling problems.

Difficulty

Single-card and few-card statistics mix after one sweep, but the full permutation involves all $\sim n\log n$ bits of information, and the coin choices of a sweep interact across coordinates. The natural route—bounding the operator norm of $Q_n(\lambda)$ separately in each irreducible representation—does not suffice, because the regular trace weights each representation by its dimension $D_\lambda$, and the number of partitions grows like $e^{c\sqrt n}$. A uniform power must work simultaneously for representations of tiny dimension (very long first row), intermediate dimension, and dimension close to $\sqrt{n!}$, and splitting the coordinates into row and column groups produces two symmetry decompositions that do not commute.

Formalization scope

• Positions are Fin d → Bool; permutations are Equiv.Perm (Card d); partitions of $2^d$ are Young diagrams of cardinality $2^d$ (Shapes (2^d)).
• The Specht module is built concretely as the span of the orbit of the standard polytabloid in the space of functions on tabloids, transported to a Euclidean (Hilbert) space; cards are relabelled to cells by a fixed bijection. Q d μ is the average over all coin sequences of length $d$ of the representation of run d d.
• absoluteTrace A P is the real part of the trace of CFC.rpow (CFC.sqrt (A⋆A)) P, i.e. $\operatorname{Tr}|A|^P$; regularTrace multiplies by finrank.
• sweepDistance d v σ is total variation of the law of $v\cdot d$ physical shuffles, right-translated by $\sigma$, from the uniform weight $1/(2^d)!$. The integer $v$ is converted with Int.toNat; since $P\ge2$ and $2v\ge P$, $v\ge1$ and no truncation occurs.
• The support lower bound (Proposition 5.1) is not part of the goal.
• Infrastructure needed: Specht-module dimensions and branching, Schatten-norm inequalities (Hölder, Araki–Lieb–Thirring), Schur–Weyl duality, and the partial-deck density bound from the companion preprint on routing densities. Contributions formalizing any of these pieces are welcome.

Selected references

• E. O. Thorp, Nonrandom shuffling with applications to the game of Faro, J. Amer. Statist. Assoc. 68 (1973), 842–847. https://doi.org/10.1080/01621459.1973.10481434
• B. Morris, The mixing time of the Thorp shuffle, SIAM J. Comput. 38 (2008), 484–504. https://doi.org/10.1137/050636231
• R. Montenegro and P. Tetali, Mathematical aspects of mixing times in Markov chains, Found. Trends Theor. Comput. Sci. 1 (2006), 237–354. https://doi.org/10.1561/0400000003
• B. Morris, Improved mixing time bounds for the Thorp shuffle and L-reversal chain, Ann. Probab. 37 (2009), 453–477. https://doi.org/10.1214/08-AOP409
• B. Morris, Improved mixing time bounds for the Thorp shuffle, Combin. Probab. Comput. 22 (2013), 118–132. https://doi.org/10.1017/S0963548312000478
• H. Araki, On an inequality of Lieb and Thirring, Lett. Math. Phys. 19 (1990), 167–170. https://doi.org/10.1007/BF01045887
• A. Berele and A. Regev, Hook Young diagrams with applications to combinatorics and to representations of Lie superalgebras, Adv. Math. 64 (1987), 118–175. https://doi.org/10.1016/0001-8708(87)90007-7
• B. E. Sagan, The Symmetric Group, 2nd ed., GTM 203, Springer, 2001. https://doi.org/10.1007/978-1-4757-6804-6
• OpenAI, Random-subspace tests and trace smoothing for coordinate sweeps, OpenAI Math Release preprint, September 26, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Random-subspace-tests-and-trace-smoothing-for-coordinate-sweeps-September-26-2026/paper.pdf

Motivation

In the low-temperature phase $\beta>1$ of the Sherrington–Kirkpatrick (SK) spin glass, the Gibbs measure is believed to split into many nearly separated pieces, and local dynamics such as heat-bath (Glauber) updates should take a very long time to move between them. Worst-case slow mixing (some bad starting state) is a weak statement: it says nothing about what happens when the chain is started from a typical equilibrium sample, which is how such chains are used in practice. This mission asks for a much stronger obstruction: for most equilibrium configurations held fixed as starting points, the dynamics is still far from equilibrium after a stretched-exponential time.

Timeline

• 1975. Sherrington and Kirkpatrick introduce the model (doi:10.1103/PhysRevLett.35.1792).
• 1980. Parisi proposes his variational description of the free energy (doi:10.1088/0305-4470/13/4/009).
• 2003, 2006. Guerra's interpolation bound and Talagrand's matching lower bound establish the Parisi formula (doi:10.1007/s00220-002-0773-5, doi:10.4007/annals.2006.163.221).
• 2009–2010. Monthus–Garel and Billoire report numerical evidence for an $n^{1/3}$ scale of logarithmic relaxation times (doi:10.1088/1742-5468/2009/12/P12017, doi:10.1088/1742-5468/2010/11/P11034).
• 2018. Ben Arous and Jagannath turn overlap free-energy barriers into exponentially small spectral gaps for mean-field spin glasses under landscape hypotheses that exclude pure SK (doi:10.1007/s00220-018-3152-6).
• 2022. El Alaoui, Montanari and Sellke prove an obstruction to stable sampling algorithms at $\beta>1$ (arXiv:2203.05093).
• 2025. Sellke proves exponentially slow worst-case Glauber mixing for SK at sufficiently large $\beta$ (arXiv:2511.22621).
• 2026. Bandeira, El Alaoui and Rödder prove polynomial mixing at every $\beta$ under a large uniform external field (arXiv:2607.06813).

The source of this mission is an OpenAI preprint dated September 24, 2026. It covers the entire range $\beta>1$, at zero field, for typical rather than worst-case starts.

Setting

For $n\ge2$ and independent standard Gaussians $(J_{ij})_{i<j}$, put

$$H^J(x)=\frac1{\sqrt n}\sum_{i<j}J_{ij}x_ix_j,\qquad \pi^J(x)=\frac{e^{\beta H^J(x)}}{Z^J},\qquad x\in\{-1,1\}^n .$$

In continuous-time heat-bath dynamics each site has a rate-one clock; when site $i$ rings, its spin becomes $s\in\{\pm1\}$ with probability $e^{\beta sh_i}/(2\cosh\beta h_i)$, where $h_i=n^{-1/2}\sum_{j\ne i}J_{ij}x_j$. Let $P^J_t$ be its kernel and $K^J$ the discrete kernel that resamples one uniformly chosen site. For a fixed start $x$,

$$d^J(x,t)=\|P^J_t(x,\cdot)-\pi^J\|_{\rm TV},\qquad d^J_{\rm disc}(x,k)=\|(K^J)^k(x,\cdot)-\pi^J\|_{\rm TV}.$$

Formalization targets

Goal: Theorem 1.1

Let $\kappa=1/10000$. For every fixed $\beta>1$,

$$\mathbb P_{J,\ x_0\sim\pi^J}\Bigl\{d^J\bigl(x_0,e^{n^\kappa}\bigr)>\tfrac14\Bigr\}\to1,\qquad \mathbb P_{J,\ x_0\sim\pi^J}\Bigl\{d^J_{\rm disc}\bigl(x_0,\lfloor e^{n^\kappa}\rfloor\bigr)>\tfrac14\Bigr\}\to1 .$$

The order matters: $x_0$ is drawn from $\pi^J$ and then held fixed as the starting state. Lean: OAI.SK.main, open on the platform; it writes the joint probability as the disorder average of the Gibbs mass of slow starts.

Significance

The theorem shows that throughout the low-temperature phase, a Gibbs-sampled start carries information that local updates cannot erase in time $e^{n^{1/10000}}$; in particular (Corollary 1.2) every polynomial time scale is too short from a typical start. This separates the zero-field low-temperature SK model from the high-temperature and large-field regimes, where polynomial mixing holds. The exponent $1/10000$ is not claimed to be optimal; numerical studies suggest $n^{1/3}$.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Integrating the transition kernel over the starting state recovers $\pi^J$ at every time, so averaging arguments are useless; the obstruction must be established start by start, for a set of starts of Gibbs mass tending to one. Free-energy barrier criteria in the style of Ben Arous–Jagannath do not apply to the pure quadratic SK covariance. The proof needs quantitative Parisi-type comparisons for constrained replica overlaps, and a mechanism ("locking") that forces small overlaps with a third replica to stay put when two replicas overlap substantially.

Formalization scope

• hamiltonian J x = (∑_{i<j} J_{ij} x_i x_j)/√n; disorderLaw n is the product of standard Gaussians over pairs $i<j$.
• heatBath β J x y is the one-step kernel: average over sites $i$ of the conditional resampling probability, nonzero only when $y$ agrees with $x$ off $i$ (so holding is included).
• discreteKernel iterates it; continuousKernel β J t = ∑_k e^{-nt}(nt)^k/k! · K^k, the uniformized rate-$n$ chain, equivalent to rate-one clocks per site.
• continuousBadMass β n and discreteBadMass β n are $\mathbb E_J$ of the Gibbs mass of starts with distance $>1/4$ at time timeScale n = exp(n^κ) (resp. its floor).
• The goal asserts both bad masses tend to $1$ for each fixed $\beta>1$.

Infrastructure: finite Markov chains, Gaussian interpolation (Guerra–Talagrand bounds for constrained overlaps), Parisi functional regularity, and Gaussian concentration. The paper's Theorem 2.4 (quantitative free-energy comparison), Proposition 4.4 (absolute-overlap locking) and Proposition 6.1 (stretched-exponential coverage) are natural intermediate targets.

Selected references

• OpenAI, Stretched-exponential barriers for typical SK initial states, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Stretched-exponential-barriers-for-typical-SK-initial-states-September-24-2026/paper.pdf
• D. Sherrington, S. Kirkpatrick, Solvable model of a spin-glass, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.1792
• G. Parisi, A sequence of approximated solutions to the S-K model for spin glasses, J. Phys. A, 1980. https://doi.org/10.1088/0305-4470/13/4/009
• F. Guerra, Broken replica symmetry bounds in the mean field spin glass model, Comm. Math. Phys., 2003. https://doi.org/10.1007/s00220-002-0773-5
• M. Talagrand, The Parisi formula, Ann. of Math., 2006. https://doi.org/10.4007/annals.2006.163.221
• G. Ben Arous, A. Jagannath, Spectral gap estimates in mean field spin glasses, Comm. Math. Phys., 2018. https://doi.org/10.1007/s00220-018-3152-6
• M. Sellke, Exponentially slow mixing of the low temperature SK model, preprint, 2025. https://arxiv.org/abs/2511.22621
• A. S. Bandeira, A. El Alaoui, A. Rödder, Mixing of Glauber dynamics on high overlap Gibbs measures, preprint, 2026. https://arxiv.org/abs/2607.06813
• A. El Alaoui, A. Montanari, M. Sellke, Sampling from the Sherrington–Kirkpatrick Gibbs measure via algorithmic stochastic localization, FOCS 2022. https://arxiv.org/abs/2203.05093
• D. Panchenko, Free energy in the mixed p-spin models with vector spins, Ann. Probab., 2018. https://doi.org/10.1214/17-AOP1194

Motivation

The Sherrington–Kirkpatrick (SK) model is the mean-field spin glass, and $\beta=1$ is its equilibrium critical point. Physicists expect critical slowing down: at a phase transition, local dynamics needs time growing polynomially in the system size to relax. For the SK model this was studied through linearized mean-field theory, dynamical equations for correlation and response, and simulations of equilibrium autocorrelations on an $n^{2/3}$ time scale. Rigorous results on Glauber dynamics had concentrated on high temperature, where mixing is fast. This mission asks for a rigorous total-variation obstruction at $\beta=1$: most equilibrium configurations, used as starting states, are still far from equilibrium after $o(n^{2/3})$ time.

Timeline

• 1975, 1978. Sherrington and Kirkpatrick introduce the model and study Glauber autocorrelations above the critical temperature (doi:10.1103/PhysRevLett.35.1792, doi:10.1103/PhysRevB.17.4384).
• 1976. Kosterlitz, Thouless and Jones analyze the spherical spin glass, with its transition at the spectral edge (doi:10.1103/PhysRevLett.36.1217).
• 1981–1982. Sompolinsky and Zippelius develop dynamical equations for correlation and response (doi:10.1103/PhysRevLett.47.359, doi:10.1103/PhysRevB.25.6860).
• 1996. Comets relates the Ising and spherical partition functions via a Haar-averaging identity (doi:10.24033/ast.331).
• 2011. Billoire and Campbell numerically examine critical autocorrelations on the $n^{2/3}$ scale (doi:10.1103/PhysRevB.84.054442).
• 2016, 2022. Baik and Lee, and Landon, prove free-energy fluctuation limits for the spherical model, including criticality (doi:10.1007/s10955-016-1610-0, doi:10.1063/5.0054298).
• 2019, 2022. Bauerschmidt–Bodineau and Eldan–Koehler–Zeitouni prove functional inequalities at high temperature (doi:10.1016/j.jfa.2019.01.007, doi:10.1007/s00440-021-01085-x).
• 2026. Du and Huang prove critical free-energy and overlap results (arXiv:2607.02172, arXiv:2608.08752); Wang and Boban–Li–Oveis Gharan prove fast mixing for $\beta<1/2$ and $\beta<1/2+\varepsilon_0$ (arXiv:2608.22159, arXiv:2609.13138).

The source of this mission is an OpenAI preprint dated September 24, 2026.

Setting

At $\beta=1$ and zero field, let $W_{ij}\sim N(0,1/n)$ be independent for $i<j$ and

$$\mu_W(x)\propto\exp\Bigl(\sum_{i<j}W_{ij}x_ix_j\Bigr),\qquad x\in\{-1,1\}^n .$$

A heat-bath update at site $i$ resamples $x_i$ from its conditional law given the other spins. In continuous time every site has an independent rate-one clock (generator $\sum_i(K_i-I)$); in discrete time each step updates a uniformly chosen site (kernel $n^{-1}\sum_iK_i$). For a fixed start $x$, $d^{\rm ct}_t(W,x)$ and $d^{\rm dt}_k(W,x)$ are the total-variation distances to $\mu_W$.

Formalization targets

Goal: Theorem 1.1 (realized equilibrium initial states)

For every deterministic $t_n\ge0$ with $t_n=o(n^{2/3})$ and every deterministic integer $k_n=o(n^{5/3})$,

$$\mu_W\{x:\ d^{\rm ct}_{t_n}(W,x)>1/4\}\ \xrightarrow{\ \mathbb P\ }\ 1,\qquad \mu_W\{x:\ d^{\rm dt}_{k_n}(W,x)>1/4\}\ \xrightarrow{\ \mathbb P\ }\ 1 .$$

Lean: OAI.CriticalSK.realized_equilibrium_initial_states, open on the platform.

Milestone: Theorem 1.2 (covariance and linear tests)

With $\Sigma=\operatorname{Cov}_{\mu_W}(x)$, $\mathcal D(f)=\sum_i\mu_W[\operatorname{Var}(f\mid x_{-i})]$ and $R_{\rm lin}=\sup_{a\ne0}\operatorname{Var}(a^{\mathsf T}x)/\mathcal D(a^{\mathsf T}x)$: for every $M_n\to\infty$, with probability tending to one,

$$\|\Sigma\|,\ R_{\rm lin}\ \in\ \bigl[n^{2/3}/M_n,\ M_nn^{2/3}\bigr].$$

Milestones: Theorem 1.3 (critical mixing bounds)

For every fixed $\epsilon>0$,

$$\mathbb P\{n^{2/3-\epsilon}\le t_{\rm mix}\le e^{\epsilon n}\}\to1,\qquad \mathbb P\{n^{5/3-\epsilon}\le k_{\rm mix}\le e^{\epsilon n}\}\to1,$$

with a separate Lean target for the lower bounds alone.

Significance

The theorem shows that at criticality the slow direction is visible from typical equilibrium starts, not only from adversarial ones, and pins the time scale $n^{2/3}$ to the spectral edge of the coupling matrix. Theorem 1.2 identifies the covariance scale $n^{2/3}$, contrasting with bounded covariance at every $\beta<1$. A companion OpenAI preprint uses Theorems 1.1 and 1.2 as inputs for matching upper bounds $n^{2/3+o(1)}$.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.

Difficulty

Averaging over the starting state gives back the stationary law, so the obstruction must be proved start by start. The slow observable is the projection $v^{\mathsf T}x$ on the top eigenvector of the coupling matrix; the difficulty is the static estimate that this projection is rarely small on the $n^{1/3}$ scale under the Ising Gibbs law. This requires edge-of-spectrum random matrix estimates, a precise comparison between the Ising law and a tilted spherical law, and control of the conditioning on the sphere.

Formalization scope

• hamiltonian W x = ∑_{i<j} W_{ij} x_i x_j; disorderLaw n is the product of gaussianReal 0 (1/n) over pairs $i<j$.
• siteKernel W i is the heat-bath kernel on configurations agreeing off $i$; discreteKernel = n^{-1}∑_i siteKernel; continuousKernel W t = exp(t ∑_i (siteKernel W i - 1)).
• continuousGoodMass/discreteGoodMass are the Gibbs masses of starts with distance $>1/4$; convergence in probability is written as $\mathbb P(|\text{mass}-1|\ge\delta)\to0$ for all $\delta>0$.
• covarianceNorm is the Euclidean operator norm; linearRayleigh is a real sSup over nonzero $a$ (the quotient is bounded and the set nonempty).
• Mixing times are sInf over times at which all starts are within $1/4$.

Infrastructure: finite continuous-time Markov chains (matrix exponentials), GOE edge estimates, tridiagonal models, spherical integrals. The intermediate results Proposition 3.1, Theorem 5.3 and Proposition 5.4 are natural further milestones.

Selected references

• OpenAI, Critical slowing down in the Sherrington–Kirkpatrick model, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-slowing-down-in-the-Sherrington-Kirkpatrick-model-September-24-2026/paper.pdf
• D. Sherrington, S. Kirkpatrick, Solvable model of a spin-glass, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.1792
• H. Sompolinsky, A. Zippelius, Dynamic theory of the spin-glass phase, Phys. Rev. Lett., 1981. https://doi.org/10.1103/PhysRevLett.47.359
• F. Comets, A spherical bound for the Sherrington–Kirkpatrick model, Astérisque, 1996. https://doi.org/10.24033/ast.331
• H. Du, B. Huang, Fluctuations of the Sherrington–Kirkpatrick free energy at critical temperature, preprint, 2026. https://arxiv.org/abs/2607.02172
• H. Du, B. Huang, Overlap distribution of the critical Sherrington–Kirkpatrick model, preprint, 2026. https://arxiv.org/abs/2608.08752
• J. Baik, J. O. Lee, Fluctuations of the free energy of the spherical Sherrington–Kirkpatrick model, J. Stat. Phys., 2016. https://doi.org/10.1007/s10955-016-1610-0
• B. Landon, Free energy fluctuations of the two-spin spherical SK model at critical temperature, J. Math. Phys., 2022. https://doi.org/10.1063/5.0054298
• A. Billoire, I. A. Campbell, Dynamics in the Sherrington–Kirkpatrick Ising spin glass at and above $T_g$, Phys. Rev. B, 2011. https://doi.org/10.1103/PhysRevB.84.054442