All missions

Motivation

Risk-averse optimization replaces the expected cost $\mathbb E[X]$ of a random outcome by a risk function $\rho(X)$ that also penalizes dispersion: mean–deviation, mean–semideviation, conditional value-at-risk (CVaR) and their combinations are the standard examples in stochastic programming and portfolio selection. A decision maker who uses $\rho$ should not prefer an outcome that every risk-averse expected-utility maximizer rejects. For costs, the order that expresses this agreement among risk-averse agents is the increasing convex order: $X_2$ is worse than $X_1$ if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every increasing convex disutility $u$. It is the counterpart, for costs, of second-order stochastic dominance.

Whether a given mean–risk model is consistent with stochastic dominance was settled model by model: Ogryczak and Ruszczyński for mean–semideviation models (Eur. J. Oper. Res. 1999, Math. Program. 2001, SIAM J. Optim. 2002) and Pflug for CVaR (2000). Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) gave a single criterion, Theorem 5.1, which contains these results as special cases: among risk functions that depend only on the distribution of the outcome, consistency with the increasing convex order is equivalent to two structural properties, monotonicity and risk aversion.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $p\in[1,\infty)$. The space of outcomes is $\mathcal X=\mathcal L_p(\Omega,\mathcal F,P)$, the real random variables with $\mathbb E|X|^p<\infty$. An outcome is a cost: smaller is better. A risk function is a map $\rho:\mathcal X\to\mathbb R$.

• The cdf of $X$ is $F_X(t)=P(X\le t)$. $\rho$ is distribution invariant (Definition 5.2) if $F_{X_1}=F_{X_2}$ implies $\rho(X_1)=\rho(X_2)$.
• $\rho$ satisfies (A2) (monotonicity) if $X\le Y$ almost surely implies $\rho(X)\le\rho(Y)$.
• $\rho$ is risk averse (Definition 5.1) if for every $\sigma$-algebra $\mathcal G\subset\mathcal F$ and every $X\in\mathcal X$,

$$\rho(X)\ \ge\ \rho\big(\mathbb E[X\mid\mathcal G]\big),$$

for every version of the conditional expectation.

• For random variables $X_1,X_2$, the usual stochastic order $X_2\succeq_{\mathrm{st}}X_1$ holds if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every nondecreasing $u:\mathbb R\to\mathbb R$ for which both expectations exist; the increasing convex order $X_2\succeq_{\mathrm{icx}}X_1$ is the same with $u$ ranging over the increasing convex functions.
• $\rho$ is consistent with an order $\succeq$ if $X_2\succeq X_1$ implies $\rho(X_2)\ge\rho(X_1)$ for all $X_1,X_2\in\mathcal X$.

The paper places one more standing assumption on §5.2: the space is rich enough to carry a uniform random variable, a measurable $U:\Omega\to\mathbb R$ with $P(U\le t)=t$ for all $t\in[0,1]$.

In Lean these are IsUniformRV, cdfOf, cdfInv, DistInvariant, A2, RiskAverse, StLE, ConsistentSt and ConsistentIcx in the namespace ConvexRiskFn.Order; the increasing convex order is the published StochasticOrders.MonotoneConvex.IcxOrder P P X₁ X₂, read as $X_1\preceq_{\mathrm{icx}}X_2$.

Formalization targets

Goal: Theorem 5.1 (p. 446)

Under the standing assumptions, for every distribution-invariant $\rho:\mathcal X\to\mathbb R$,

$$\rho\ \text{consistent with}\ \succeq_{\mathrm{icx}}\quad\Longleftrightarrow\quad \rho\ \text{satisfies (A2) and is risk averse}.$$

No convexity, translation equivariance or positive homogeneity of $\rho$ is assumed.

Milestones

1. The usual stochastic order and the cdf (§5.2, p. 445): $X_2\succeq_{\mathrm{st}}X_1$ iff $F_{X_2}(t)\le F_{X_1}(t)$ for all $t$.
2. The quantile coupling (proof of Lemma 5.1, p. 446): $F_X^{-1}(U)$ has the law of $X$, and $F_{X_2}\le F_{X_1}$ gives $F_{X_1}^{-1}(U)\le F_{X_2}^{-1}(U)$ almost surely.
3. Lemma 5.1 (p. 445): a distribution-invariant $\rho$ is consistent with $\succeq_{\mathrm{st}}$ iff it satisfies (A2).
4. Conditional expectation is icx-smaller (proof of Theorem 5.1, p. 446): $\mathbb E[X\mid\mathcal G]\in\mathcal X$ and $\mathbb E[X\mid\mathcal G]\preceq_{\mathrm{icx}}X$.
5. Strassen's coupling on $\Omega$ (proof of Theorem 5.1, p. 446): if $X_1\preceq_{\mathrm{icx}}X_2$, there are $\widehat X_1\overset{D}{\sim}X_1$, $\widehat X_2\overset{D}{\sim}X_2$ on the same $\Omega$ with $\widehat X_1\le\mathbb E[\widehat X_2\mid\widehat X_1]$ a.s.

Significance

Theorem 5.1 reduces a property quantified over all pairs of ordered distributions to two properties that can be checked on the risk function directly. Monotonicity is usually immediate, and risk aversion follows for the main examples from the dual representation of the risk function (the paper verifies it for mean–semideviation and for CVaR-based models in §5.1). The theorem then yields at once the consistency of these models with the increasing convex order, which was previously proved case by case. It also explains the failures: a law-invariant risk function that violates (A2), such as mean–deviation for $p>1$ under the paper's condition $(*)$, cannot be consistent with any increasing integral stochastic order.

The result has a complete published proof. What the mission adds is a machine-checked version of it on the paper's own space $\mathcal L_p(\Omega,\mathcal F,P)$, together with reusable pieces of stochastic-order theory: the cdf characterization of the usual stochastic order, the quantile coupling, conditional Jensen in increasing-convex form, and Strassen's martingale coupling realized on a given space carrying a uniform random variable. Mathlib has conditional Jensen for convex functions (ConvexOn.map_condExp_le_univ) but not the stochastic orders, the quantile coupling or Strassen's theorem. Strassen's theorem for laws on $\mathbb R^n$, with a coupling on some probability space, is posed separately on Prove2Me but not proved.

Difficulty

The forward direction is short given milestone 4. The reverse direction is where the work is. Consistency compares $\rho(X_1)$ and $\rho(X_2)$ for random variables that are related only through their laws: $X_1\preceq_{\mathrm{icx}}X_2$ says nothing about $X_1(\omega)$ versus $X_2(\omega)$, so neither (A2) nor risk aversion applies to the pair as given. The argument has to replace the pair by another pair, with the same laws, on the same space $\Omega$, related by a conditional expectation; only then can monotonicity and risk aversion be chained. Producing that pair is Strassen's theorem, a nonconstructive existence result about martingale couplings, and it has to be realized on the given $\Omega$, not on a product space built for the purpose, because $\rho$ is defined only on $\mathcal L_p(\Omega,\mathcal F,P)$. That is the role of the uniform random variable, and transporting the coupling onto $\Omega$ through it is a separate measure-theoretic step. The first-order analogue, Lemma 5.1, needs the same kind of transfer, through quantile functions, whose values at $0$ and $1$ must be handled.

Formalization scope

• $\mathcal L_p$ is encoded by functions $\Omega\to\mathbb R$ satisfying MemLp X p P with 1 ≤ p and p ≠ ⊤, not by almost-everywhere classes. $\rho$ is a function (Ω → ℝ) → ℝ; every definition quantifies only over MemLp arguments, so its values elsewhere play no role. $\rho$ is real valued, as in Definition 5.2.
• The order in (A2) is the almost-sure order, the order of $\mathcal L_p$ (p. 434).
• "For which the expectations exist" is integrability of $u\circ X_1$ and $u\circ X_2$, as in the published increasing convex order.
• Risk aversion quantifies over every sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$ and every $\mathcal G$-measurable version of Mathlib's conditional expectation P[X|m].
• The uniform random variable and $p\in[1,\infty)$ appear as hypotheses of the goal, of Lemma 5.1 and of milestone 5, exactly where the paper's standing assumptions of §5.2 apply. Milestones 1 and 4 do not need them.
• The quantile $F^{-1}(t)=\inf\{s:F(s)\ge t\}$ is a real infimum, which is $0$ where the paper's value is $\pm\infty$ ($t\notin(0,1)$); milestone 2 is therefore stated almost surely.
• The goal mentions neither quantiles, nor $U$ beyond its existence, nor any coupling. A statement that assumed convexity of $\rho$, dropped distribution invariance, restricted to bounded or pointwise-ordered outcomes, or replaced risk aversion by the single $\sigma$-algebra $\{\emptyset,\Omega\}$ would be a different and weaker theorem and does not count.

Needed infrastructure: equality in law from equality of cdfs, the quantile transform, conditional Jensen's inequality (in Mathlib) turned into the increasing convex order, and Strassen's theorem in dimension one with the transfer of a coupling to a space carrying a uniform random variable. The last two are reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas such as the cdf characterization of equality in law, are welcome.

Selected references

• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (Theorem 1.2.8, Corollary 1.5.21). https://www.wiley.com/en-us/Comparison+Methods+for+Stochastic+Models+and+Risks-p-9780471494461
• V. Strassen, The existence of probability measures with given marginals, Annals of Mathematical Statistics 36(2):423–439, 1965. https://doi.org/10.1214/aoms/1177700153
• D. Blackwell, Equivalent comparisons of experiments, Annals of Mathematical Statistics 24(2):265–272, 1953. https://doi.org/10.1214/aoms/1177729032
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Random growth models and random matrices share limit laws. The first exact instance was found by Johansson (Shape fluctuations and random matrices, Comm. Math. Phys. 2000), who showed that the last passage time of a lattice model with geometric or exponential weights has the law of the largest eigenvalue of a Laguerre (complex Wishart) random matrix. Baik, Ben Arous and Péché (Ann. Probab. 33 (2005)) extended the identity to weights whose rate depends on the row. On the matrix side this is a sample covariance matrix with a general population covariance $\Sigma$; on the growth side it is a corner growth model, or a series of exponential queues, with inhomogeneous service rates.

The identity is the reason the paper's main result, the phase transition of the largest sample eigenvalue as a few population eigenvalues ("spikes") cross the critical value $1 + \gamma^{-1}$, is also a theorem about last passage percolation and tandem queues. In the queueing reading, a spike is a slow server, and the phase transition describes how slow a few servers must be before they change the centring and the fluctuation scale of the exit time.

Timeline:

• 2000, Johansson: equal rates; the geometric and exponential last passage time has the law of the largest Laguerre eigenvalue (his Proposition 1.4 is the case $\pi_1 = \cdots = \pi_N$ of (307)).
• 2001, Baryshnikov and, independently, Gravner, Tracy and Widom: the tandem-queue and GUE-minor descriptions of the same object.
• 2005, Baik, Ben Arous and Péché: row-dependent rates $\pi_i$ (Proposition 6.1), via the Robinson–Schensted–Knuth (RSK) formula for geometric weights (310) and a scaling limit.

Setting

Last passage time. Attach a real weight $X(i,j)$ to every site of the grid $\{1,\ldots,N\}\times\{1,\ldots,M\}$. An up/right path from $(1,1)$ to $(N,M)$ is a sequence of $N+M-1$ sites starting at $(1,1)$, ending at $(N,M)$, each step adding $(1,0)$ or $(0,1)$. The last passage time is

$$L(N,M) = \max_{\pi:(1,1)\nearrow(N,M)} \sum_{(i,j)\in\pi} X(i,j). \qquad (306)$$

Exponential environment. Given positive numbers $\pi_1,\ldots,\pi_N$, the $X(i,j)$ are independent and $X(i,j)$ is exponential of mean $1/(\pi_iM)$, i.e. density $\pi_iMe^{-\pi_iMx}$ on $x\ge0$. All $M$ sites of row $i$ share one rate.

Sample covariance matrix. Let $g_{kj}$, $1\le k\le M$, $1\le j\le N$, be independent standard complex Gaussians (real and imaginary parts independent $N(0,1/2)$). For a unitary $U$ and $\ell_j = \pi_j^{-1}$ (308), the samples $\vec y_k = U\,\mathrm{diag}(\sqrt{\ell_j})\,g_k$ are mean-zero complex Gaussian vectors with covariance $\Sigma = U\,\mathrm{diag}(\ell)\,U^*$, and

$$S = \frac1M\sum_{k=1}^M \vec y_k\vec y_k^{\,*}, \qquad \lambda_1 = \text{largest eigenvalue of } S.$$

Schur functions and geometric weights. For a partition $\lambda$, the Schur function $s_\lambda(x)$ is the sum over semistandard Young tableaux $T$ of shape $\lambda$ of $\prod_{c}x_{T(c)}$. A geometric variable of parameter $q\in[0,1)$ has $\mathbb P(Y = k) = (1-q)q^k$.

Formalization targets

Goal: Proposition 6.1

For $1\le N\le M$, positive $\pi_1,\ldots,\pi_N$ and every unitary $U$,

$$\mathbb P\big(L(N,M)\le x\big) = \mathbb P\big(\lambda_1(M,N)\le x\big) \qquad \text{for all } x\in\mathbb R. \qquad (309)$$

The two sides are defined independently: one by a maximum over lattice paths of exponential weights, the other by the spectrum of a Gaussian random matrix.

Milestones

1. The recurrence (313): for every array of weights and every site with $a, b\ge2$,

$$L(a,b) = \max\{L(a-1,b), L(a,b-1)\} + X(a,b).$$

2. The Cauchy identity (311): $\sum_\lambda s_\lambda(x)s_\lambda(y) = \prod_{i,j}(1-x_iy_j)^{-1}$ for $x_i,y_j\ge0$, $x_iy_j<1$.
3. The geometric formula (310): for independent geometric weights $Y(i,j)$ of parameter $x_iy_j$, $x_i,y_j\in[0,1)$,

$$\mathbb P\big(G(N,M)\le n\big) = \prod_{i,j}(1-x_iy_j)\sum_{\lambda:\lambda_1\le n}s_\lambda(x)s_\lambda(y).$$

4. The exponential formula (307): for $M\ge N$ and distinct $\pi_i$,

$$\mathbb P\big(L(N,M)\le x\big) = \frac1C\int_{[0,x]^N}\frac{\det(e^{-M\pi_i\xi_j})}{V(\pi)}V(\xi)\prod_{j}\xi_j^{M-N}\,d\xi.$$

Significance

The proposition makes every distributional statement about $\lambda_1$ in the paper a statement about last passage percolation with row-dependent rates: the $F_k$ (generalised Tracy–Widom) fluctuations at the critical spike value, the Gaussian fluctuations above it, and the fixed-dimension limit. Through (312)–(313) it also covers the exit time of $M$ customers from $N$ exponential servers in series, an operations research object. The geometric formula (310) is the entry point of the RSK method for exactly solvable growth models.

These results are proved in the literature; the paper cites (310) and (311) and derives (307) from them by a limit. None of them is machine-checked as far as this series knows. Formalizing them requires a Lean development of Schur functions, the Cauchy identity and the RSK correspondence on matrices with nonnegative integer entries, and of the Wishart eigenvalue density, each reusable well beyond this mission.

Difficulty

The recurrence (313) is elementary. Everything else is not. The geometric formula (310) needs the RSK bijection between nonnegative integer matrices and pairs of semistandard tableaux of the same shape, together with Schensted's theorem that the first row of the shape is the last passage time; neither is in Mathlib. The passage from (310) to (307) is a scaling limit $x_i = 1 - M\pi_i/L$, $n = xL$, $L\to\infty$, in which a sum over partitions must converge to a multiple integral. The matrix side needs the joint eigenvalue density of a complex Wishart matrix with general $\Sigma$, which uses the Harish-Chandra–Itzykson–Zuber integral. A direct coupling of the two sides is not known; the identity is an equality of laws, proved by computing both.

Formalization scope

The development lives in the namespace SpikedWishart.LastPassage. Conventions:

• Sites and indices are 0-based; the paper's $(1,1)$ and $(N,M)$ are $(0,0)$ and $(N-1,M-1)$, and $N, M\ge1$.
• $L$ is defined as the maximum over paths (306), never by the recurrence (313), so (313) is a genuine statement.
• The exponential law is Mathlib's expMeasure with rate $\pi_iM$.
• The sample model is mean zero, uncentred, with factor $1/M$ and $\mathbb E|g|^2 = 1$; this is the model of (59), (61) and (307), and the page's centring by the sample mean and $S = (1/N)XX^*$ are printed slips. The covariance is $U\,\mathrm{diag}(\pi^{-1})U^*$ for every unitary $U$; specialising to diagonal $\Sigma$ would prove a special case.
• $N\le M$ is a disclosed addition to the goal, matching the page's "for $M\ge N$" in (307).
• Proposition 6.1 prints $L(M,N)$; the object is (306)'s $L(N,M)$.
• Schur functions are the tableau sum with variables extended by zero. The Cauchy identity is stated with the exponent $-1$ that the page omits. In (307) the constant $C$ is the integral of the same integrand over $(0,\infty)^N$, and the $\pi_i$ are distinct so that $V(\pi)\ne0$; the goal has no distinctness hypothesis.

A formalization in which either side of (309) is defined through the other, or through (307), would be trivial and is excluded: both laws are defined from scratch. Contributions are welcome on RSK and Schur function infrastructure, on the Wishart density, and on the measurability of $\lambda_1$.

Selected references

• J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5):1643–1697, 2005. https://doi.org/10.1214/009117905000000233
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209:437–476, 2000. https://doi.org/10.1007/s002200050027
• Y. Baryshnikov, GUEs and queues, Probab. Theory Related Fields 119:256–274, 2001. https://doi.org/10.1007/PL00008760
• J. Gravner, C. A. Tracy, H. Widom, Limit theorems for height fluctuations in a class of discrete space and time growth models, J. Stat. Phys. 102:1085–1132, 2001. https://doi.org/10.1023/A:1004879725949
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Cambridge University Press, 1999 (the paper's reference [36] for the Cauchy identity). https://doi.org/10.1017/CBO9780511609589

Motivation

Potential games (Monderer and Shapley, 1996) are the finite games whose unilateral payoff differences are all differences of a single function, the potential. They always have a pure Nash equilibrium, and many natural learning dynamics (best response, fictitious play, logit response) converge in them. Most games met in applications are not exactly potential games, so a recurring question is how much of this theory survives for a game that is close to a potential game.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405, journal version Math. Oper. Res. 36(3), 2011) decompose the space of finite games into potential, harmonic and nonstrategic components. Section 6 of the paper equips the space of games with a weighted inner product under which this decomposition is orthogonal, computes the closest potential game to any game in closed form, and shows that approximate equilibria of a game and of its closest potential game correspond, with an explicit loss controlled by the distance between them. This mission formalizes that last result together with the statements it rests on.

Setting

A finite game has a finite set of players $\mathcal M$; each player $m$ has a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements, and a utility $u^m : E \to \mathbb R$ on the set of strategy profiles $E = \prod_m E^m$. For a profile $p$, $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$.

A profile $p$ is an $\epsilon$-equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m}) - \epsilon$ for every player $m$ and strategy $q^m$ (equation (2) of the paper). A game is a potential game if there is $\varphi : E \to \mathbb R$ with $\varphi(p^m, p^{-m}) - \varphi(q^m, p^{-m}) = u^m(p^m, p^{-m}) - u^m(q^m, p^{-m})$ for all $m$, $p^m$, $q^m$, $p^{-m}$ (Definition 2.1).

A game is identified with its tuple of utilities, an element of $C_0^M$ where $C_0 = \{f : E \to \mathbb R\}$. The game graph has the profiles as nodes, with an edge between two profiles that differ in exactly one player's strategy. The operator $D_m$ sends $u^m$ to its differences along the edges where player $m$ deviates, $D = \sum_m D_m$, $\delta_0$ is the gradient of the game graph, $\Pi_m = D_m^\dagger D_m$, and $\dagger$ is the Moore–Penrose pseudoinverse. Definition 4.2 defines the potential, harmonic and nonstrategic subspaces

$$\mathcal P = \{u = \Pi u,\ Du \in \operatorname{im}\delta_0\},\qquad \mathcal H = \{u = \Pi u,\ Du \in \ker\delta_0^*\},\qquad \mathcal N = \ker D ,$$

and a harmonic game is a game in $\mathcal H \oplus \mathcal N$.

Section 6 introduces the weighted inner product and norm

$$\langle G, \hat G\rangle_{M,E} = \sum_{m} h_m \sum_{p \in E} u^m(p)\,\hat u^m(p), \qquad \|G\|_{M,E}^2 = \langle G, G\rangle_{M,E} .$$

A closest potential game to $G$ is a potential game $\hat G$ with $\|G - \hat G\|_{M,E} \le \|G - G'\|_{M,E}$ for every potential game $G'$; a closest harmonic game is defined in the same way.

Formalization targets

Goal: Theorem 6.3

Let $\hat G$ be the closest potential game to $G$ and $\alpha = \|G - \hat G\|_{M,E}$. Then for every $\epsilon_1$, every $\epsilon_1$-equilibrium of $\hat G$ is an $\epsilon$-equilibrium of $G$, and every $\epsilon_1$-equilibrium of $G$ is an $\epsilon$-equilibrium of $\hat G$, where

$$\epsilon = \max_{m \in \mathcal M} \frac{2\alpha}{\sqrt{h_m}} + \epsilon_1 .$$

Milestones

1. Lemma 2.1. If $|u^m(p) - \hat u^m(p)| \le \epsilon_0$ for all $m$ and $p$, every $\epsilon_1$-equilibrium of one game is a $(2\epsilon_0 + \epsilon_1)$-equilibrium of the other.
2. Theorem 5.1. The set of potential games is the subspace $\mathcal P \oplus \mathcal N$.
3. Theorem 6.1. Under $\langle\cdot,\cdot\rangle_{M,E}$ the subspaces $\mathcal P$, $\mathcal H$, $\mathcal N$ are pairwise orthogonal.
4. Theorem 6.2. With $\varphi = \delta_0^\dagger D u$, the closest potential game to $G$ has utilities $\Pi_m \varphi + (I - \Pi_m)u^m$, and the closest harmonic game has utilities $u^m - \Pi_m\varphi$.

Significance

The result. Theorem 6.3 reduces the study of approximate equilibria of an arbitrary finite game to a potential game, where pure equilibria exist and are maximizers of the potential. Section 7 of the paper reports that, in a companion paper, best-response and fictitious-play dynamics are shown to converge to a neighbourhood of equilibria in near-potential games, with the size of the neighbourhood governed by the distance of the game to its closest potential game. Theorems 6.1 and 6.2 make that distance computable: the closest potential game is an orthogonal projection, given by linear operators of the game graph.

Formalizing it. All four statements are proved in the paper; none of them is machine-checked anywhere known to this mission. A formal development produces a verified operator layer for games on the game graph (gradient, pseudoinverses, the projections $\Pi_m$), a verified proof that the weighted inner product, and not the unweighted one, makes the decomposition orthogonal, and a reusable perturbation lemma for $\epsilon$-equilibria.

Difficulty

Lemma 2.1 and the final step of Theorem 6.3 are elementary inequalities. The obvious way to approximate a game by a potential game, taking the identical-interest part of its zero-sum/identical-interest split, does not give the closest potential game: the paper's Table 7 (p. 35) shows a potential game whose identical-interest part is far from it. The closest potential game has to come from the projection of Section 6. The weight of the mission is in Theorems 5.1, 6.1 and 6.2. They need the decomposition theorem of Section 4 (every game splits uniquely into $\mathcal P$, $\mathcal H$, $\mathcal N$) and properties of pseudoinverses of the operators $D_m$ and $\delta_0$ that Mathlib does not provide: Mathlib has no operator pseudoinverse at all. The orthogonality $\mathcal P \perp \mathcal H$ under the weighted product rests on the specific spectral structure of the Laplacian of the graph of a single player's deviations; it is not a general fact, and it fails for the unweighted product when the $h_m$ differ, so the standard orthogonal-complement machinery cannot be applied to $C_0^M$ with its default inner product.

Formalization scope

Players are a finite type ι with decidable equality; strategy sets are finite types E m. Utilities are plain functions u : ι → (∀ m, E m) → ℝ, the shape used by the published MondererShapley.ClosedPath.IsPotentialGame, which is referenced for Definition 2.1. The operator layer works in PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted inner product of Section 4; edge flows carry the inner product $\tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$ of (7). The weighted inner product (55) and norm (56) are plain functions, not a second instance on the same type. "Closest" is the minimizing property itself, not an infimum of distances.

Hypotheses made explicit: every strategy set is nonempty (the paper's $E^m = \{1,\dots,h_m\}$), so $h_m \ge 1$; in Theorem 6.3 the set of players is nonempty, which the maximum over players needs. The paper's "an $\epsilon$-equilibrium for some $\epsilon \le B$" is stated as "a $B$-equilibrium", which is equivalent because (2) is monotone in $\epsilon$. Both directions of Lemma 2.1 and Theorem 6.3 are included.

The goal is stated for the closest potential game, as printed. A version for an arbitrary potential game at distance $\alpha$ would be a different theorem, and the hypothesis is not vacuous: Theorem 6.2 shows the closest potential game exists. Theorem 6.2 is stated as an "if and only if" characterization, so it gives existence and uniqueness as well as the formula.

Contributions welcome: the Penrose identities for the pseudoinverse, the identities $D^\dagger D = \Pi$ and $\Delta_{0,m} = h_m \Pi_m$, and the decomposition theorem of Section 4, all of which are reusable by the other missions of this series.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Math. Oper. Res. 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games Econ. Behav. 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044

Motivation

This mission asks for a formal proof that the matrix multiplication exponent is at most $2.25=9/4$ over every field. It is proposed for the Matrix multiplication exponent campaign, using the campaign's existing tensor-rank definition. The target is deliberately non-strict: equality with $9/4$ is allowed.

The starting point is OpenAI's October 2026 matrix-multiplication material, whose original arithmetic-exponent theorem is stated over the complex numbers. An all-fields adaptation has been checked separately in Lean. This mission asks for the corresponding result in the campaign's precise mathematical model; that connection still requires proof.

Setting

Let $K$ be any field, finite or infinite and in any characteristic. For a positive integer $n$, the square matrix multiplication tensor is the sum of $e_{ij}\otimes e_{jk}\otimes e_{ki}$ over all indices $i,j,k<n$. Each factor is the vector space of functions from pairs of indices to $K$. Its tensor rank is the least number of pure tensors in an exact decomposition over $K$.

The imported definition MME.matMulExp takes the infimum of the ratios $\log R_K(MM_n)/\log n$ for integer $n\ge2$, together with the value $3$ at sizes zero and one. The goal refers to this existing definition without modifying it. An upper bound on the infimum need not be attained at any one matrix size.

Target

For every field $K$, prove

$$\operatorname{MME.matMulExp}(K)\le 2.25=\frac94.$$

The Lean theorem is mme_omega_le_225, with the sole typeclass hypothesis [Field K]. The decimal is interpreted exactly as a real rational, not as a floating-point approximation. There is no restriction to characteristic zero, infinite fields, algebraically closed fields, or the complex numbers.

The campaign template currently uses a strict inequality. This proposal intentionally requests the non-strict bound $\le2.25$ and should be reviewed on that basis. It does not assert $\omega<2.25$. The proposed numeric campaign value is $2.25$.

Significance

A proof of this goal would place the nine-fourths bound in the same formal tensor-rank model used by other entries in this campaign. Reusing the foundation makes its assumptions and numeric value directly inspectable. Establishing the comparison between the arithmetic and tensor formulations would also produce reusable results for future matrix multiplication missions.

The all-fields quantifier matters: constructions that use interpolation or roots of unity must justify their applicability and any descent back to the original field. A result over the complex numbers alone does not establish this goal.

Difficulty

The available checked adaptation proves the nine-fourths bound for the OAI arithmetic exponent and its exact-rank exponent. A remaining task is to connect that exact-rank representation to the campaign's tensor product and rank definition. This requires checking the coordinate conventions, converting rank decompositions, and transporting the bound through the infimum and logarithms.

The proof must also compile in the campaign's pinned Lean environment. Success in a different Lean or Mathlib version is useful evidence for the source proof, but it does not verify this mission's theorem.

Formalization scope

This draft imports the campaign's published mme_omega definition and contains one open goal. It preserves the campaign environment, Mathlib 777aaa6 with Lean 4.29.0-rc3. The separate all-fields OAI adaptation was checked using Lean 4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; its proof is not yet an accepted Prove2me solution to this goal.

In particular, the bridge to MME.matMulExp and the environment port remain unproved here. The mission should remain open until Prove2me accepts a proof of this exact statement. An independent auditor read the Lean goal and imported definition without seeing the intended wording; that read-back is included verbatim in the goal's natural-language statement for review.

Selected references

• OpenAI matrix multiplication preprint, October 2, 2026.
• OpenAI ComparatorChallenges Lean source.
• Matrix multiplication exponent campaign.

The all-fields adaptation and the proposed connection to the campaign definition are additional formalization work; they are not attributed to the original complex-field statement.

Motivation

All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an $n$-vertex weighted directed graph. Floyd–Warshall solves it in $O(n^3)$ time, and for decades no algorithm beat $n^{3-\delta}$ for any constant $\delta>0$ on graphs with polynomially bounded integer weights. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) gave a deterministic $O(n^{2.99942})$ algorithm, the campaign's first entry. Later entries tightened the accounting to $2.9983$ and $2.99791$.

This entry records the deterministic exponent $2.996001$. It roughly doubles the saving below $3$ compared with $2.99791$, and it matches what was previously only known with randomized hashing.

Setting

The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo $2^W$, indirect load and store, a sign branch, and accept or reject, on words of width $W \ge b(\log_2 n + 1)$. Inputs have integer weights of absolute value at most $n^\kappa$ for a fixed $\kappa$, and there are no negative cycles. The machine has no source of randomness; the algorithm behind this entry is deterministic.

Formalization target

The goal is the campaign template with the value $2.996001$:

$$\texttt{TrulySubcubicAPSP.APSP.SolvedInTime}\ 2.996001,$$

which says there is a deterministic word-RAM program that solves APSP in $O(n^{2.996001})$ steps.

How the bound arises

The algebraic core is the thin-product data structure of Alman and Vassilevska Williams: for an $N\times D$ by $D\times N$ integer product it answers requested entries $W$ in $\tilde O(N^2D^{-\Gamma} + N D^{a} + |W| D^{q})$. Two local refinements of that construction sharpen the exponents:

1. Pruned encodings. Encoding branches with more than $m$ copies of the distinguished symbol $P_0$ are never materialized, giving $a(c) = \bigl(\tfrac12 cH(1/c) + (c-1)\ln 3\bigr)/\ln 4$.
2. Exact binomial tail. The box preprocessing is bounded by its actual binomial sum, giving $\Gamma(c,\theta) = \bigl(cH(1/c) - cH((1-\theta)/c) - \theta\ln 9\bigr)/\ln 4$, with $q(\theta) = \bigl(H(\theta)+\theta\ln 9\bigr)/\ln 4$.

The main new step is a deterministic filtering reduction. Moduli are chosen one small prime factor at a time, using exact thin-product witness counts to certify positive answers and to eliminate whole blocks of unresolved queries. Repeated filtering removes the need to scan individual modular witnesses, which was the bottleneck of earlier deterministic reductions (the prime-by-prime idea is suggested in footnote 9 of the source paper, after Fischer, Kaliciak and Polak). With middle blocks of size $n^{\varepsilon/2}$ this yields all-edges Exact Triangle in $n^{3-\delta+o(1)}$, where

$$\delta = \min\{\varepsilon\Gamma,\ 1-\varepsilon a,\ \varepsilon(1/2-q)\},$$

and deterministic bit scaling transfers the bound to min-plus product and APSP with polylogarithmic overhead.

The exact rational parameters $c = 21.2733$, $\theta = 0.111731$ and $\varepsilon = 0.056846$ satisfy the thin regime $\varepsilon(a+\Gamma) < 1$ with margin $1.16\times10^{-6}$, and give $\delta > 0.00399928$. Hence APSP runs in $n^{2.99600072+o(1)}$, and the gap $2.996001 - 2.99600072 > 0$ absorbs the subpolynomial factor.

Significance

This is the first deterministic entry near $2.996$. Earlier analyses reached about $2.99601$ only by repeating random-prime hashing, which this word-RAM model cannot express. The deterministic filtering closes that gap.

Selected references

• J. Alman and V. Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs (2026). https://arxiv.org/abs/2610.06783
• Deterministic APSP in $O(n^{2.996001})$: an explicit refinement of the thin-product method, technical note, 6 October 2026. This is the source of $2.996001$ and has not been peer reviewed.

Motivation

The $\beta$-model is the simplest exponential random graph model in which every vertex has its own parameter. It was studied by Holland and Leinhardt (1981) in the directed case and by Park and Newman (2004) and Blitzstein and Diaconis (2011) in the undirected case, and it is a close relative of the Bradley–Terry model for paired comparisons. Its sufficient statistic is the degree sequence of the observed graph, so fitting the model to data means solving a system of $n$ nonlinear equations in $n$ unknowns, one per vertex, where $n$ can be in the thousands.

Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 21 (2011)) give a simple iteration for this system and prove that it converges geometrically fast whenever a solution exists, at a rate that does not deteriorate with the number of vertices, and that it detects when no solution exists. The same estimate is then used in the paper's consistency theorem for the maximum likelihood estimator (Theorem 1.3) and in its graph-limit theorem (Theorem 1.1). This mission formalizes that algorithmic result, Theorem 1.5, together with the chain of numbered displays in Section 2 that proves it.

Setting

Let $n\ge 3$ and label the vertices $1,\dots,n$. For $\beta=(\beta_1,\dots,\beta_n)\in\mathbb R^n$, the $\beta$-model puts an edge between distinct vertices $i$ and $j$ independently with probability

$$p_{ij}(\beta)=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}}.$$

Given an observed graph with degrees $d_1,\dots,d_n$, the maximum likelihood estimate $\hat\beta$ must satisfy the ML equations

$$d_i=\sum_{j\ne i}\frac{e^{\hat\beta_i+\hat\beta_j}}{1+e^{\hat\beta_i+\hat\beta_j}},\qquad i=1,\dots,n.\tag{3}$$

The sup norm of $x\in\mathbb R^n$ is $|x|_\infty=\max_i|x_i|$. For $i\ne j$ put $r_{ij}(x)=1/(e^{-x_j}+e^{x_i})$, and define the map $\varphi:\mathbb R^n\to\mathbb R^n$ by

$$\varphi_i(x)=\log d_i-\log\sum_{j\ne i}r_{ij}(x).$$

Starting from any $x_0\in\mathbb R^n$, the fixed-point iteration is $x_{k+1}=\varphi(x_k)$. The fixed points of $\varphi$ are exactly the solutions of (3).

For an $n\times n$ matrix $A=(a_{ij})$, the $L^\infty$ operator norm is $|A|_\infty=\max_i\sum_j|a_{ij}|$. For $\delta>0$, the class $\mathcal L_n(\delta)$ consists of the matrices with $|A|_\infty\le 1$, $a_{ii}\ge\delta$ and $a_{ij}\le-\delta/(n-1)$ for $i\ne j$. For $x,y\in\mathbb R^n$, $J(x,y)$ is the matrix with entries $J_{ij}(x,y)=\int_0^1\frac{\partial\varphi_i}{\partial x_j}(tx+(1-t)y)\,dt$.

Formalization targets

Goal: Theorem 1.5

There are functions $\Theta(a,b)\in[0,1)$ and $C(a,b)$, $C$ continuous, independent of $n$ and $d$, such that for every $n\ge3$ and every $d\in(0,\infty)^n$: if (3) has a solution $\hat\beta$, then $\hat\beta=\varphi(\hat\beta)$, it is the unique solution of (3), and for all $x_0$ and $k$

$$|x_k-\hat\beta|_\infty\le\Theta(|\hat\beta|_\infty,|x_0|_\infty)^{\lfloor k/2\rfloor}|x_0-\hat\beta|_\infty,\qquad |x_0-\hat\beta|_\infty\le C(|\hat\beta|_\infty,|x_0|_\infty)\,|x_0-x_1|_\infty;$$

and if (3) has no solution, then every orbit $\{x_k\}$ is unbounded.

Milestones, in the order the proof uses them

1. p. 9: $\varphi(x)=x$ if and only if $x$ solves (3).
2. (6)–(7), p. 12: on $|x|_\infty\le K$, $-\frac{e^{2K}}{n-1}\le\frac{\partial\varphi_i}{\partial x_j}\le-\frac{e^{-4K}}{2(n-1)}$ for $i\ne j$, and $\frac12e^{-4K}\le\frac{\partial\varphi_i}{\partial x_i}\le e^{2K}$.
3. (8), pp. 12–13: $\varphi(x)-\varphi(y)=J(x,y)(x-y)$; off-diagonal partials are negative, diagonal ones positive, and every row of the Jacobian has absolute sum $1$.
4. Lemma 2.1, p. 11: for $A,B\in\mathcal L_n(\delta)$,

$$|AB|_\infty\le 1-\frac{2(n-2)\delta^2}{n-1}.$$

5. (9), p. 13: with $K$ the largest of $|x|_\infty,|y|_\infty,|\varphi(x)|_\infty,|\varphi(y)|_\infty$ and $\delta=\frac12e^{-4K}$,

$$|\varphi(\varphi(x))-\varphi(\varphi(y))|_\infty\le\Big(1-\frac{2(n-2)\delta^2}{n-1}\Big)|x-y|_\infty,$$

and $|\varphi(x)-\varphi(y)|_\infty\le|x-y|_\infty$. 6. (10), p. 13: a single $\theta=\Theta(|\hat\beta|_\infty,|x_0|_\infty)\in[0,1)$, continuous in its arguments, with $|x_{k+3}-x_{k+2}|_\infty\le\theta|x_{k+1}-x_k|_\infty$ and $|x_{k+2}-\hat\beta|_\infty\le\theta|x_k-\hat\beta|_\infty$.

Significance

The theorem turns an implicit statistical object, the MLE of an $n$-parameter model, into the limit of an explicit iteration with three guarantees: a convergence rate that depends on the size of the parameters but not on $n$; an a posteriori error bound in terms of the computable step $|x_0-x_1|_\infty$; and a certificate of non-existence. The uniqueness of the MLE comes out of the same estimate. In the paper, the a priori bound $|x_0-\hat\beta|_\infty\le C|x_0-x_1|_\infty$ is the device that proves consistency of the MLE (Theorem 1.3, applied with $x_0=\beta$), and the two-step contraction is reused in the proof of the graph-limit theorem.

The result is proved in the paper; no machine-checked proof of it is known. The work here is to formalize the known proof. The matrix inequality of Lemma 2.1 and the derivative bounds (6)–(7) are self-contained and can be attacked independently of the iteration.

Difficulty

The obvious approach is to show that $\varphi$ is a contraction and apply Banach's fixed-point theorem. This fails: every row of the Jacobian of $\varphi$ has absolute sum exactly $1$, so $\varphi$ is only non-expansive in the sup norm, never strictly contracting. Contraction appears only for the two-step map $\varphi\circ\varphi$, through the sign pattern of the Jacobian (positive diagonal, uniformly negative off-diagonal), and only on bounded sets, with a factor that tends to $1$ as the norms grow. A second difficulty is uniformity: the factor must be bounded away from $1$ independently of $n$, which needs $(n-2)/(n-1)\ge\frac12$, hence $n\ge3$. For the converse, there is no fixed point to anchor the orbit, so boundedness of the orbit has to be converted into convergence before a fixed point exists.

Formalization scope

• Vertices are Fin n $=\{0,\dots,n-1\}$; vectors are Fin n → ℝ, whose Mathlib norm is the sup norm $|x|_\infty$. Matrix norms are the explicit maximal absolute row sum.
• The degrees $d_i$ are arbitrary positive reals. This is a generalization of the page (degrees of a graph), and it is all the proof uses; positivity is required because $\log d_i$ is junk in Lean at $0$.
• $n\ge3$ is a hypothesis of the goal and of (10). It is not on the page but is necessary: for $n=2$, (3) reads $d_1=d_2=p_{12}$, whose solutions form a line, so uniqueness fails, and the factor in Lemma 2.1 equals $1$.
• Partial derivatives are Fréchet derivatives applied to unit vectors; $J(x,y)$ uses the interval integral over $[0,1]$.
• "Geometrically fast, with rate depending only on $(|\hat\beta|_\infty,|x_0|_\infty)$" is stated with the function $\Theta$ quantified before $n$, $d$, $\hat\beta$ and $x_0$, and "$C$ is a continuous function of the pair" likewise. A version that chooses the rate after fixing $n$, $d$ and $x_0$ is strictly weaker and nearly says only that a convergent sequence converges; it is not the target.
• "A divergent subsequence" is stated as unboundedness of $\{|x_k|_\infty\}$, which is equivalent for sequences in $\mathbb R^n$.
• The paper's remark that $\theta$ is "uniformly bounded away from 1 on subsets of $\mathbb R^n\times\mathbb R^n$" holds only on bounded subsets; it is not stated separately, and its quantitative content is (10).

Needed infrastructure: calculus of $\varphi$ (derivatives of $\log$ of a sum of exponentials), the integral form of the mean value theorem for maps $\mathbb R^n\to\mathbb R^n$, and elementary matrix-norm estimates. The class $\mathcal L_n(\delta)$ and Lemma 2.1 are reusable for other diagonally dominant iterations. Proofs of any milestone are welcome, in any order.

Selected references

• S. Chatterjee, P. Diaconis and A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4), 1400–1435, 2011. arXiv:1005.1136v5, DOI 10.1214/10-AAP728
• P. W. Holland and S. Leinhardt, An exponential family of probability distributions for directed graphs, J. Amer. Statist. Assoc. 76, 33–65, 1981. DOI 10.1080/01621459.1981.10477598
• J. Park and M. E. J. Newman, Statistical mechanics of networks, Phys. Rev. E 70, 066117, 2004. arXiv:cond-mat/0405566
• J. Blitzstein and P. Diaconis, A sequential importance sampling algorithm for generating random graphs with prescribed degrees, Internet Mathematics 6(4), 489–522, 2011. DOI 10.1080/15427951.2010.557277