All missions

Motivation

Many problems in statistics, signal processing and machine learning minimize a smooth function over a set defined by smooth equations, $\min_{x\in\mathbb R^n} f(x)$ subject to $c(x)=0$: orthogonality constraints (the Stiefel manifold), unit-norm constraints (spheres and oblique manifolds), fixed-rank and symplectic constraints. Riemannian optimization treats the feasible set as a manifold and moves along it with retractions and vector transports, which have to be designed and implemented for each manifold (Absil, Mahony & Sepulchre 2008). Exact penalty methods avoid that geometry, but the classical smooth exact penalty of Fletcher (1970) needs second derivatives of $f$ just to evaluate its gradient.

Xiao, Liu & Toh (arXiv:2203.10319v3) propose the constraint dissolving function (CDF), an unconstrained smooth function whose gradient needs only $\nabla f$. They prove that, near the feasible set and above an explicit penalty threshold, the CDF and the constrained problem have the same stationary points and the same local minimizers. Any unconstrained solver can then be applied to the CDF directly. The paper later appeared in Mathematics of Operations Research (2024); this mission follows the arXiv v3 numbering throughout.

Setting

Let $f:\mathbb R^n\to\mathbb R$ and $c:\mathbb R^n\to\mathbb R^p$, and let $\mathcal M=\{x: c(x)=0\}$ be the feasible region of (OCP). The transposed Jacobian $J_c(x)\in\mathbb R^{n\times p}$ has the gradients $\nabla c_i(x)$ as columns. Assumption 1.1 asks that $\nabla f$ and $J_c$ be locally Lipschitz and that LICQ hold on $\mathcal M$: $J_c(x)$ has full column rank for $x\in\mathcal M$.

A constraint dissolving operator is a map $\mathcal A:\mathbb R^n\to\mathbb R^n$ with locally Lipschitz Jacobian $J_{\mathcal A}$ such that $\mathcal A(x)=x$ and $J_{\mathcal A}(x)J_c(x)=0$ for every $x\in\mathcal M$ (Assumption 1.2). For the unit sphere one can take $\mathcal A(x)=2x/(1+\|x\|^2)$. The CDF with penalty parameter $\beta$ is

$$h(x)=f(\mathcal A(x))+\frac\beta2\|c(x)\|^2 .$$

Around a feasible point $x$ the paper introduces local constants (§2.3, p.7). These are:

• $\sigma_{x,c}=\sigma_{\min}(J_c(x))$;
• a radius $\rho_x\le1$ on whose closed ball $\Theta_x$ one has $\sigma_{\min}(J_c(y))\ge\frac12\sigma_{x,c}$;
• the suprema $M_{x,f}$, $M_{x,c}$, $M_{x,A}$ of $\|\nabla f(\mathcal A(y))\|$, $\|J_c(y)\|$, $\|J_{\mathcal A}(y)\|$ over $\Theta_x$;
• the Lipschitz constants $L_{x,g}$, $L_{x,c}$, $L_{x,A}$, $L_{x,b}$ of $\nabla(f\circ\mathcal A)$, $J_c$, $J_{\mathcal A}$ and $J_{\mathcal A}(\cdot)J_c(\mathcal A(\cdot))$ on $\Theta_x$.

From these it builds a radius $\varepsilon_x$, two closed balls $\bar\Omega_x\subset\Omega_x$ around $x$, and the threshold

$$\beta_x=\max\Big\{\frac{128L_{x,g}(M_{x,A}+1)^2}{\sigma_{x,c}^2},\ \frac{64M_{x,f}(M_{x,A}+1)L_{x,b}}{\sigma_{x,c}^3},\ \frac{16M_{x,f}L_{x,A}(2M_{x,A}+1)}{\sigma_{x,c}^2}\Big\}.$$

The Lean development uses the same names: transJac, cdf, rhoX, MXA, LXb, epsX, omegaBarRadius, betaX, Ainf.

Formalization targets

Goal: Theorem 3.18

For every $x\in\mathcal M$, every $\beta\ge\beta_x$ and every $z\in\bar\Omega_x$:

$$z\ \text{local minimizer of (OCP)}\ \Longrightarrow\ z\ \text{local minimizer of } h,$$ $$\beta>0\ \text{and}\ z\ \text{local minimizer of } h\ \Longrightarrow\ z\ \text{local minimizer of (OCP)}.$$

The condition $\beta>0$ in the second implication corrects the printed statement: $\beta_x$ can be $0$, and with $\beta=0$ the implication fails.

Milestones, in proof order

• The operator $\mathcal A$ (Lemmas 3.1–3.4). An error bound $\frac{1}{M_{x,c}}\|c(y)\|\le\operatorname{dist}(y,\mathcal M)\le\frac{2}{\sigma_{x,c}}\|c(y)\|$ on $\Omega_x$. Then $\|\mathcal A(y)-y\|=O(\|c(y)\|)$ and $\|c(\mathcal A(y))\|=O(\|c(y)\|^2)$. Finally, the iterates $\mathcal A^k(y)$ converge to a feasible point $\mathcal A^\infty(y)$ for $y\in\bar\Omega_x$.
• The linear algebra of $J_{\mathcal A}$ (Lemmas 3.5–3.7). On $\mathcal M$, $J_{\mathcal A}(x)$ is idempotent with null space the normal space $\mathcal N_x$, and $J_{\mathcal A}(x)^\top$ fixes the tangent space $\mathcal T_x$.
• Calculus of the CDF (Propositions 3.8, 3.9). The formula $\nabla h=J_{\mathcal A}\nabla f(\mathcal A)+\beta J_cc$ and the Hessians. Stationary points of OCP and of CDF coincide on $\mathcal M$.
• Exactness estimates (Theorem 3.10, Proposition 3.13). The bound $\|\nabla h(y)\|\ge\frac{\beta\sigma_{x,c}}{8(M_{x,A}+1)}\|c(y)\|$ holds on $\Omega_x$. Applying $\mathcal A$ decreases $h$: $h(\mathcal A(y))-h(y)\le-\frac\beta8\|c(y)\|^2$ and $h(\mathcal A^\infty(y))-h(y)\le-\frac\beta4\|c(y)\|^2$ on $\bar\Omega_x$.

Significance

Theorem 3.18 makes the CDF an exact penalty for local minimization. With a penalty parameter above $\beta_x$, unconstrained local minimization of $h$ near $\mathcal M$ finds exactly the constrained local minimizers. Together with Theorem 3.10, this lets convergence and complexity results for unconstrained methods transfer to Riemannian optimization without retractions (§3.3 of the paper). The bounds of Lemmas 3.1–3.4 also justify the post-processing step $x\leftarrow\mathcal A(x)$ used to restore feasibility.

The results are proved in the paper, and to our knowledge none of them has a machine-checked proof. Formalizing them yields a checked exact-penalty theorem with explicit constants. It also yields reusable infrastructure: an error bound for LICQ-regular equality constraints, nearest-point arguments for the zero set of a smooth map, and fixed-point iteration estimates near a manifold.

Difficulty

The obvious argument for the first implication of the goal compares $h(y)$ with $f$ at a nearby feasible point. No such point is directly available: Lean has no projection onto $\mathcal M$, and the paper's projection argument needs the first-order optimality condition $y-z\in\operatorname{range}J_c(z)$ at a nearest point. That condition requires a Lagrange multiplier theorem under LICQ. The paper instead uses $\mathcal A^\infty(y)$, whose existence (Lemma 3.4) is a quantitative contraction argument: one must show that the iterates never leave $\Omega_x$. The printed proof of the goal also applies Proposition 3.13 at the minimizer $z$ with the constants of $z$, although the hypothesis concerns $\beta_x$. A correct proof reruns the estimates with the constants of $x$ on a small ball around $z$ inside $\Omega_x$.

The step $|f(\mathcal A^2(y))-f(\mathcal A(y))|\le M_{x,f}\|\mathcal A^2(y)-\mathcal A(y)\|$ in the proof of Proposition 3.13 bounds $\nabla f$ along a segment where $M_{x,f}$ does not apply directly, and needs a separate argument. Every constant in the statements has to be tracked exactly, since the threshold $\beta_x$ is explicit.

Formalization scope

• Spaces and maps. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Transposed Jacobians are adjoints of Fréchet derivatives, with the $\ell_2$ operator norm, and $\sigma_{\min}(B)$ is the infimum of $\|B\nu\|$ over unit $\nu$. Theorems that use $\sigma_{x,c}$ assume $p\ge1$.
• Constants. The constants of §2.3 are sSups over the closed ball $\Theta_x$. They are finite under the assumptions, and no boundedness hypothesis is added. $\varepsilon_x$ is the largest $\varepsilon\in(0,\rho_x/2]$ satisfying the two linear constraints. This is the printed minimum with $\sigma/0=+\infty$, so an affine constraint (where $L_{x,c}=0$) does not collapse $\Omega_x$ to a point; a proved sanity check confirms $\varepsilon_x>0$ on such an instance.
• Local minimizers. A local minimizer of OCP is a feasible point minimizing $f$ on $\mathcal M$ near it. A local minimizer of CDF minimizes $h$ on a full neighbourhood in $\mathbb R^n$. Restricting the CDF neighbourhood to $\mathcal M$ or to $\bar\Omega_x$ would trivialize the second implication.
• Penalty threshold. The threshold is the printed $\beta_x$. Replacing it by "$\beta$ large enough" is a weaker theorem and not acceptable.
• Proposition 3.8. The Hessian terms $\mathcal D_{J_{\mathcal A}}(x)[\nabla f(\mathcal A(x))]$ and $\mathcal D_{J_c}(x)[c(x)]$ are stated as $\sum_k\partial_kf(\mathcal A(x))\nabla^2\mathcal A_k(x)$ and $\sum_ic_i(x)\nabla^2c_i(x)$. The literal directional-derivative reading of (3.9) is false.

Welcome contributions are a Lagrange multiplier rule for nearest points of $\{c=0\}$ under LICQ, Lipschitz-on-compact lemmas for locally Lipschitz maps, and proofs of the milestones in order.

Selected references

• N. Xiao, X. Liu, K.-C. Toh, Dissolving Constraints for Riemannian Optimization, arXiv:2203.10319v3, 2022; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2203.10319
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• R. Fletcher, A class of methods for nonlinear programming with termination and convergence properties, in Integer and Nonlinear Programming, North-Holland, 1970.

Motivation

Simulation models of service systems, supply chains and financial products depend on input parameters that are themselves estimated from data, such as arrival rates or demand distributions. When a decision maker compares $k$ candidate designs by simulation, this input uncertainty means that the best design may differ from one plausible parameter value to the next. Kim, Kim and Song (arXiv:2207.07533, Operations Research, 2025) propose to select the most probable best (MPB): the design that is optimal with the largest probability under a distribution $\pi$ on the parameter.

Finding the MPB is a nested ranking-and-selection problem: an inner problem identifies the best design at each parameter, and an outer problem compares how often each design wins. The question the paper answers is how to split a simulation budget among all design–parameter pairs so that the probability of selecting the wrong MPB decays as fast as possible. The paper relaxes the exact large-deviations rate of this probability into a tractable max–min problem, (20), and characterizes its solutions by a short system of equations, Theorem 3. Its sequential sampling algorithms are plug-in versions of that system.

This follows the optimal computing budget allocation (OCBA) line of work for classical ranking and selection, in particular the large-deviations analysis of Glynn and Juneja (Proceedings of the 2004 Winter Simulation Conference, pp. 577–585), whose pairwise rate is the building block $G_i(\theta_b)$ below.

Setting

There are $k\ge2$ solutions $i$ and $B$ parameters $\theta_1,\dots,\theta_B$ with probabilities $p_b>0$, $\sum_bp_b=1$. The conditional mean of solution $i$ at $\theta_b$ is $y_i(\theta_b)$ (smaller is better), and its simulation output has standard deviation $\lambda_i(\theta_b)>0$.

• The conditional optimum at $\theta_b$ is $i^b=\arg\min_iy_i(\theta_b)$; the paper assumes the means at each $\theta_b$ are pairwise distinct.
• The preference probability of $i$ is $\sum_bp_b\mathbf 1\{i=i^b\}$, the probability of its favorable set $\Theta_i=\{\theta_b:i=i^b\}$. The MPB $i^*$ is its unique maximizer.
• The gap $d_j=\sum_bp_b\mathbf 1\{i^*=i^b\}-\sum_bp_b\mathbf 1\{j=i^b\}$ is positive for $j\ne i^*$.
• $\Xi=\{(i,\theta_b):i\ne i^*,\,i\ne i^b\}$ is the set of pairs whose misranking can cause a false selection.
• The balance weight of $(i,\theta_b)\in\Xi$ is $W_i(\theta_b)=\max\{\min(\min_{j\ne i^*}d_j,d_i/2)/p_b,1\}$ if $\theta_b\in\Theta_{i^*}$ and $\max\{d_i/p_b,1\}$ otherwise.

An allocation $\boldsymbol\alpha=\{\alpha_i(\theta_b)\}$ is a point of the $kB$-simplex: $\alpha_i(\theta_b)$ is the fraction of the budget spent on $(i,\theta_b)$. The pairwise rate is

$$G_i(\theta_b)=\frac{(y_i(\theta_b)-y_{i^b}(\theta_b))^2}{2\big(\lambda_i^2(\theta_b)/\alpha_i(\theta_b)+\lambda_{i^b}^2(\theta_b)/\alpha_{i^b}(\theta_b)\big)}$$

if both ratios are positive, and $0$ otherwise. The relaxed OCBA problem is

$$\max_{\boldsymbol\alpha}\ \underline{\mathrm{LDR}}(\boldsymbol\alpha)=\min_{(i,\theta_b)\in\Xi}W_i(\theta_b)G_i(\theta_b)\quad\text{s.t.}\quad\sum_{i,b}\alpha_i(\theta_b)=1,\ \alpha\ge0. \tag{20}$$

Formalization targets

Goal: Theorem 3

A feasible $\boldsymbol\alpha$ is optimal for (20) if and only if

$$\frac{\alpha_{i^b}^2(\theta_b)}{\lambda_{i^b}^2(\theta_b)}=\sum_{i\ne i^b,i^*}\frac{\alpha_i^2(\theta_b)}{\lambda_i^2(\theta_b)}\ \ \forall b,\qquad W_iG_i(\theta_b)=W_jG_j(\theta_{b'})\ \ \forall(i,\theta_b),(j,\theta_{b'})\in\Xi,\qquad \alpha_{i^*}(\theta_b)=0\ \ \forall\theta_b\in\Theta^c_{i^*}.$$

Both directions, every feasible allocation, every $k\ge2$ and $B\ge1$.

Milestones (steps of the proof on pp.ec8–ec10)

1. Each $G_i(\theta_b)$ and the objective $\underline{\mathrm{LDR}}$ are concave on the nonnegative orthant, so (20) is a convex program.
2. Every optimal allocation satisfies the zero sampling ratio.
3. The uniform allocation has positive value; optimal allocations are positive on $\Xi$ and at $(i^b,\theta_b)$ wherever $\Xi$ has a pair at $\theta_b$ (corrected for $k=2$).
4. Under these properties, optimality is equivalent to the KKT system (EC.17)–(EC.21) (corrected for $k=2$).
5. The partial derivatives of $G_i(\theta_b)$ in $\alpha_i(\theta_b)$ and $\alpha_{i^b}(\theta_b)$, and their ratio (corrected denominator).

Significance

Theorem 3 replaces an optimization over the simplex by a system that can be checked, and tracked, coordinate by coordinate. That is what makes the paper's sequential algorithms possible: each step samples the pair whose condition is most violated, and the consistency theorems of the paper (Theorems 4, 5 and 7) say that the sampling ratios converge to a solution of this system. The third condition is the qualitative finding: unlike classical ranking and selection, where every optimal ratio is positive, the MPB receives no budget at parameters where it is not the conditional optimum.

The result is proved in the paper. It has not been formalized. A machine-checked version gives a verified reference point for the nested ranking-and-selection model, the balance weights and the max–min KKT argument, and it checks three steps of the published proof that are misprinted (see Formalization scope). Theorem 3 itself is unaffected by these misprints.

Difficulty

The objective is a minimum of finitely many concave functions, which is not differentiable where two terms tie, and each term is not differentiable where an allocation ratio vanishes. The standard route rewrites (20) in epigraph form (EC.14) and applies KKT under Slater's condition. That route needs positivity of the optimal ratios first, so that the nonnegativity multipliers vanish and the rates are differentiable. Positivity is not automatic: the MPB's ratios at adversarial parameters are zero at every optimum, and when $k=2$ the conditional optimum's ratio at such a parameter is zero too, because it enters no term of the objective. A proof that assumes interior optima, or applies a smooth KKT theorem on all of $\mathbb R^{kB}$, fails at exactly these coordinates.

The converse direction must rule out a degenerate solution of the system with $W_iG_i\equiv0$ on $\Xi$. Global balance and the zero ratio together exclude it only because the allocation lies on the simplex.

Formalization scope

The Lean development uses the namespace MPBSelect. Solutions are Fin k, parameters Fin B, and an allocation is α : Fin k → Fin B → ℝ. A structure Problem k B carries $p$, $y$, $\lambda$, $i^b$ and $i^*$, with fields for $k\ge2$, $p_b>0$, $\sum_bp_b=1$, assumption (i) (distinct means at each $\theta_b$), the strict-argmin property of $i^b$, the strict-argmax property of $i^*$ (assumption (ii)), and $\lambda>0$. $\lambda$ is a standard deviation: the paper's Model (4) has variance $\lambda^2$. $G$ is defined with an explicit if for its zero branch. The minimum over $\Xi$ is Finset.inf', and $\Xi$ is proved nonempty, so no junk value enters. $W$ is the real formula (17) and is only evaluated on $\Xi$.

The goal is stated for every feasible allocation and with all three conditions. A version restricted to $k\ge3$, to interior allocations, to one direction, or to "some optimal allocation satisfies the conditions" would be a different and weaker theorem.

Three proof steps carry a declared correction. Positivity on all of $(\Xi^{\mathrm{adv}})^c$ and the condition (EC.20) "for all $b$" both fail for $k=2$: with $p=(0.6,0.4)$, $\lambda\equiv1$, $y(\theta_1)=(0,1)$, $y(\theta_2)=(1,0)$, the printed KKT system has no solution. The milestones restrict both to parameters at which $\Xi$ has a pair; for $k\ge3$ that is every parameter. The printed partial derivative of $G_i$ has $\alpha^2$ where $\alpha$ belongs in the denominator ($1/16$ against the true $1/8$ at $\alpha=1/2$); the ratio of the two partials, which is all that (EC.22) uses, is unaffected.

A complete development needs concavity of the harmonic-mean function on the closed quadrant, a KKT theorem for a concave program with a linear equality constraint, differentiable at the point, and finite-sum manipulations. Mathlib supplies ConcaveOn, HasDerivAt and Finset.inf'. A reusable lemma on concavity of $xy/(x+y)$ extended by $0$ to the closed quadrant would be welcome, as would a KKT sufficiency lemma for max–min problems.

Selected references

• T. Kim, K.-K. Kim, E. Song, Selection of the Most Probable Best, arXiv:2207.07533v2, 2024; Operations Research, 2025. https://arxiv.org/abs/2207.07533
• P. Glynn, S. Juneja, A large deviations perspective on ordinal optimization, Proceedings of the 2004 Winter Simulation Conference, pp. 577–585, IEEE, 2004 (as cited in the bibliography of arXiv:2207.07533v2, p.41).
• C.-H. Chen, J. Lin, E. Yücesan, S. E. Chick, Simulation budget allocation for further enhancing the efficiency of ordinal optimization, Discrete Event Dynamic Systems 10(3):251–270, 2000.
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

Motivation

Many problems in statistics, signal processing and operations research have the composite form $\min_x f(x)+h(x)$: a smooth convex loss $f$ plus a convex, possibly nonsmooth term $h$ that encodes a regularizer or a constraint. First-order methods use only $\nabla f$; high-order (tensor) methods also use the derivatives $\nabla^2 f,\dots,\nabla^d f$ and minimize a regularized Taylor model at each step. The question is how fast such a method can be.

For $d$-th order methods on functions with Lipschitz $d$-th derivative, the best possible worst-case rate is $O(k^{-(3d+1)/2})$ after $k$ iterations (Arjevani, Shamir & Shiff 2019; Nesterov 2021). Known accelerated tensor methods reached only $O(k^{-(d+1)})$.

Timeline.

• 2010–2013: Monteiro and Svaiter introduce the accelerated hybrid proximal extragradient (A-HPE) framework and, for $d=2$ without the high-order regularizer, a method with rate $O(k^{-7/2})$ (SIAM J. Optim. 23, 2013).
• 2018: Nesterov's accelerated tensor method attains $O(k^{-(d+1)})$ for every $d$ (CORE DP 2018/05).
• 2018–2020: Jiang, Wang and Zhang (arXiv:1812.06557v3) combine the A-HPE framework with Nesterov's regularized tensor model and prove $O(k^{-(3d+1)/2})$ for every order $d$, matching the lower bound. Independent work of Gasnikov et al. and of Bubeck et al. established similar bounds for the smooth case $F=f$; the three groups announced the common development jointly at COLT 2019 (p.3 of the paper).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be convex and $d$ times differentiable, with $L_d$-Lipschitz $d$-th derivative: $\|\nabla^d f(x)-\nabla^d f(y)\|\le L_d\|x-y\|$, in the tensor operator norm. Let $h:\mathbb R^n\to(-\infty,+\infty]$ be proper closed convex, $F=f+h$, $X_*$ the set of minimizers of $F$ (assumed nonempty), $F_*=\min F$ and $D$ the distance from the starting point $x_0$ to $X_*$.

For $M>0$ the regularized Taylor model at $x$ is

$$f_x(y)=\sum_{i=0}^{d}\frac1{i!}\nabla^i f(x)[y-x]^i+\frac{M}{(d+1)!}\|y-x\|^{d+1}.$$

The $\epsilon$-subdifferential is $\partial_\epsilon h(x)=\{u: h(y)\ge h(x)+\langle y-x,u\rangle-\epsilon\ \forall y\}$. A triple $(y,u,\epsilon)$ is a $\hat\sigma$-approximate solution of $\min_y f_x(y)+h(y)+\frac1{2\lambda}\|y-x\|^2$ if $u-\nabla f_x(y)\in\partial_\epsilon h(y)$ and $\|\lambda u+y-x\|^2+2\lambda\epsilon\le\hat\sigma^2\|y-x\|^2$.

Algorithm 2 keeps weights $A_0=0$, $A_{k+1}=A_k+a_{k+1}$ with $a_{k+1}=\big(\lambda_{k+1}+\sqrt{\lambda_{k+1}^2+4\lambda_{k+1}A_k}\big)/2$, and the point $\tilde x_k=\frac{A_k}{A_k+a_{k+1}}y_k+\frac{a_{k+1}}{A_k+a_{k+1}}x_k$. At each iteration it finds a step size $\lambda_{k+1}$ and a $\hat\sigma$-approximate solution $(y_{k+1},u_{k+1},\epsilon_{k+1})$ at $(\lambda_{k+1},\tilde x_k)$ such that

$$\frac{d!\,\sigma_l}{L_d+M}\le\lambda_{k+1}\|y_{k+1}-\tilde x_k\|^{d-1}\le\frac{d!\,\sigma_u}{L_d+M}\qquad(3.7)$$

(or a small-residual alternative that ends the run), sets $v_{k+1}=\nabla f(y_{k+1})+u_{k+1}-\nabla f_{\tilde x_k}(y_{k+1})$ and $x_{k+1}=x_k-a_{k+1}v_{k+1}$. The parameters satisfy $M\ge L_d$, $\hat\sigma\ge0$, $0<\sigma_l<\sigma_u<1$ and $\hat\sigma+\sigma_u<1$.

Formalization targets

Goal: Theorem 3.4

For every $d\ge1$ and every $k\ge1$ such that the step producing $y_k$ satisfies (3.7),

$$F(y_k)-F_*\le\Big(\frac{d+1}2\Big)^{\frac{3d+1}2}\frac{2^d}{(1-(\hat\sigma+\sigma_u)^2)^{\frac{d-1}2}\,d!\,\sigma_l}\,D^{d+1}(L_d+M)\,k^{-\frac{3d+1}2}.$$

The goal keeps the paper's explicit constant.

Milestones, in the order of the proof

1. Lemma 2.1: $\|\nabla f(y)-\nabla f_x(y)\|\le\frac{L_d+M}{d!}\|y-x\|^d$.
2. Lemma 3.1: the A-HPE estimates (3.3)–(3.6), including $\frac12\|x_*-x_k\|^2+A_k(F(y_k)-F_*)+\frac{1-\sigma^2}2\sum_j\frac{A_j}{\lambda_j}\|\tilde y_j-\tilde x_{j-1}\|^2\le\frac12D^2$ and $A_k\ge\frac14(\sum_j\sqrt{\lambda_j})^2$.
3. Proposition 3.2: a step satisfying (3.7) meets the A-HPE error condition with $\sigma=\hat\sigma+\sigma_u$.
4. Theorem 3.3: Algorithm 2 is a run of the A-HPE framework.
5. Eq. (3.14), Proposition 3.5, Eq. (3.15) and the display after (3.18): for $d\ge2$, the lower bound $A_k\ge(\frac12)^{d+1}\frac{d!\sigma_l}{L_d+M}\big(\frac{1-\sigma^2}{D^2}\big)^{\frac{d-1}2}\big(\frac2{d+1}\big)^{\frac{3d+1}2}k^{\frac{3d+1}2}$.

Significance

The theorem shows that the rate $k^{-(3d+1)/2}$ is attained for composite problems at every order $d$, so the lower bound for $d$-th order methods is tight. At $d=2$ it gives a second-order method with rate $k^{-7/2}$ for nonsmooth composite objectives, with inexact subproblem solutions. The A-HPE inequality (Lemma 3.1) and the Taylor gradient bound (Lemma 2.1) are general tools: the first underlies a family of accelerated proximal methods, the second every regularized tensor method.

The result is proved in the paper (with the correction below) but not formalized anywhere. The mission formalizes the A-HPE analysis, which the paper quotes from Monteiro and Svaiter without proof, a Taylor estimate for gradients at every order $d$, and the bootstrapping argument from (3.13) to the closed-form growth of $A_k$. A Lean proof would also confirm the explicit constant.

Difficulty

The classical estimate-sequence argument gives Nesterov's $O(k^{-(d+1)})$ and no better: it discards the term $\sum_j\frac{A_j}{\lambda_j}\|\tilde y_j-\tilde x_{j-1}\|^2$ of (3.3). The improvement needs that term together with the lower half of (3.7), which ties $\lambda_{k+1}$ to a step length that itself depends on $\lambda_{k+1}$ through $\tilde x_k$. Converting the summed bound into growth of $A_k$ requires Hölder's inequality and an induction on exponents $r_i\to\frac{3d+1}2$ whose limit must be taken. Inequality (3.3) is the heart of the A-HPE theory and is not proved in the paper. At general $d$, the gradient of the model must be identified, including the regularizer $\|y-x\|^{d+1}$, and the Taylor remainder must be bounded with iteratedFDeriv.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $f$ is ContDiff ℝ d f with the Lipschitz bound on iteratedFDeriv ℝ d f in the multilinear operator norm, and $L_d\ge0$. $h$ and $F$ take values in EReal; proper closed convex means never $-\infty$, somewhere finite, lower semicontinuous and with convex epigraph. Gradients are Mathlib's gradient. $F_*$ is ⨅ x, F x and $D$ is Metric.infDist to the nonempty set of minimizers. A run of an algorithm is a family of sequences related by its steps for the iterations $0,\dots,k-1$; $A_k$, $a_{k+1}$ and $\tilde x_k$ are computed from them with $A_0=0$. The algorithm's STEP 2 stopping test is part of a run of Algorithm 2.

Correction. STEP 3 allows a step that satisfies only the small-residual alternative instead of (3.7). The printed Theorems 3.3 and 3.4 fail at such a step. A one-dimensional quadratic example satisfies every assumption, yet $F(y_1)-F_*=1/8$ exceeds the printed bound, which is below $0.024$. Every corrected item therefore assumes (3.7) at the step producing $y_k$. Earlier steps satisfy it automatically, since an alternative-only step triggers the stopping test. The A-HPE framework is formalized without its exact stopping test $0\in\partial F(y_k)$, which Algorithm 2 replaces by an approximate one. The goal is stated for $d\ge1$; the paper's formula also holds at $d=1$. The milestones on $A_k$ require $d\ge2$, because their constants contain $1/(d-1)$.

No hypothesis of the goal is vacuous: a one-step run with $f(x)=x^2/2$, $h=0$, $d=2$ satisfies all of them (checked in Lean). The goal concerns the actual iterates of Algorithm 2 and the gap $F(y_k)-F_*$, not abstract sequences satisfying (3.13).

Needed infrastructure: Taylor's theorem with integral remainder for iteratedFDeriv along a segment, the calculus of $\|\cdot\|^{p}$, $\epsilon$-subdifferential sum rules, and Hölder's inequality for finite sums (Real.inner_le_Lp_mul_Lq). The Taylor gradient bound and the A-HPE estimates are reusable beyond this mission. Contributions to any milestone, or to general lemmas they rely on, are welcome.

Selected references

• B. Jiang, H. Wang, S. Zhang, An Optimal High-Order Tensor Method for Convex Optimization, arXiv:1812.06557v3, 2020; Mathematics of Operations Research, 2021. https://arxiv.org/abs/1812.06557
• R. D. C. Monteiro, B. F. Svaiter, An accelerated hybrid proximal extragradient method for convex optimization and its implications to second-order methods, SIAM J. Optim. 23(2), 2013. https://doi.org/10.1137/110833786
• Y. Nesterov, Implementable tensor methods in unconstrained convex optimization, Math. Program. 186, 2021. https://doi.org/10.1007/s10107-019-01449-1
• Y. Arjevani, O. Shamir, R. Shiff, Oracle complexity of second-order methods for smooth convex optimization, Math. Program. 178, 2019. https://doi.org/10.1007/s10107-018-1293-1

Why traceability matters to a manufacturer with market power

A manufacturer that sources from several suppliers faces a recall problem. When a defect is reported and the source cannot be traced, every unit on the shelf is recalled, including goods from suppliers who did nothing wrong. A shared ledger that records provenance changes this: only the defective batch needs to be recalled. A Walmart case study reports tracing times falling from seven days to 2.2 seconds, and the same record can also tell consumers more about the product.

Whether such a system is worth its cost depends on who keeps the gains. In a companion paper, the same authors show that under Bertrand competition among manufacturers the gains are competed away to consumers and the incremental welfare from adoption is zero (Iyengar, Saleh, Sethuraman, Wang, Economics of Permissioned Blockchain Adoption, Management Science 69(6), 2023). The paper formalized here, Iyengar, Saleh, Sethuraman and Wang, Blockchain Adoption in a Supply Chain with Manufacturer Market Power (SSRN 3950580), studies the opposite market structure, a single manufacturer that sets prices on both sides, and reaches the opposite conclusion.

Setting

There are $N\ge1$ homogeneous suppliers, one manufacturer of type $q\in\{A,B\}$, and a unit mass of consumers of types $t\in\{A,B\}$, with types uniform and independent. A consumer values the good at $V=v_0+I(q=t)-I(q\ne t)$ and has an outside option worth $v_0\ge1$. Consumers do not see $q$. Each receives a signal equal to $q$ with probability $a$, where $a=\alpha\in(\tfrac12,1)$ in the regime without blockchain (NB) and $a=\alpha+\delta(1-\alpha)$, $\delta\in(0,1]$, in the regime with blockchain (B). A consumer buys when the conditional expected utility given type and signal, minus the price, is at least $v_0$. Demand $s_r(q,P)$ is the resulting purchase probability.

The manufacturer places an order $(P,\Psi,\Xi)$: a consumer price $P\ge0$, a supplier price $\Psi\ge0$, and a set $\Xi$ of suppliers, each producing a quantity $s/|\Xi|$. A supplier exerts effort $e\in[0,1]$ at unit cost $e/2$, and its whole batch is good with probability $\sqrt e$. Without blockchain any defect recalls everything, so the no-recall probability is $\sqrt{e_j}\,(\sqrt e)^{|\Xi|-1}$. With blockchain only the defective batch is recalled, so it is $\sqrt{e_j}$. A symmetric effort maximizes a supplier's profit per unit given that the others exert the same effort, and a supplier accepts when the profit at that effort is strictly positive.

The manufacturer's random profit $\Pi_r$ sums $(P-\Psi)s/|\Xi|$ over the accepting suppliers whose batch is not recalled, with batches independent. Its objective is the mean-variance utility $\mathcal M_r=\mathbb E[\Pi_r]-\frac\gamma2\mathrm{Var}[\Pi_r]$, $\gamma\in(0,1)$. At an adoption cost $\chi>0$, an equilibrium has suppliers responding after every order, the order optimal in each regime, and adoption exactly when the incremental welfare $\Omega=\mathcal M_{\mathrm B}-\mathcal M_{\mathrm{NB}}$ is at least $\chi$.

Formalization targets

Goal: Proposition 4.1

There is a number $\Omega^\star>0$, independent of the cost, such that for every $\chi>0$ an equilibrium exists and every equilibrium satisfies

$$\Omega=\Omega^\star,\qquad \text{adoption}\iff\chi\le\Omega^\star,\qquad \chi\le\Omega^\star\ \Longrightarrow\ \text{all $N$ suppliers receive and accept the order.}$$

The statement holds for every $N\ge1$, every $\alpha,\delta,\gamma,v_0$ in the stated ranges, and without the paper's Assumption 1, which only the later comparative statics use.

Milestones

1. Proposition 3.1 part 1 (p.17): demand is $\frac12 I(P\le 2a-1)$.
2. The table of $e^*_{\mathrm{NB}}$ (p.33): all symmetric efforts without blockchain, corrected at $\Psi=1$, $|\Xi|=2$.
3. Proposition 3.1 part 2 (p.18): the printed effort and acceptance, in both regimes.
4. Utility (pp.34, 38): $\mathcal M_{\mathrm{NB}}=f(P,\Psi;\gamma)$ and $\mathcal M_{\mathrm B}=f(P,\Psi;\gamma/|\Xi|)$ on the good region, and at most $0$ elsewhere.
5. Properties of $f$ (pp.35, 40): strictly increasing in $P$, strictly concave in $\Psi$, decreasing in the parameter.
6. Proposition 3.1 part 3 (pp.18–19): the root of $\Lambda$ in $(0,P)$, and the optimal orders: one supplier without blockchain, all $N$ with it.
7. Proposition 3.1 part 4 (p.19): existence and the adoption rule.
8. The chain (a)–(c) (p.40).

Significance

The theorem says that the manufacturer always gains from traceability. The gain is explained by the decomposition the paper gives afterwards: a lower profit variance from diversification across suppliers, and a higher expected profit. It separates the monopolist case from the competitive one, where the same technology yields no gain. The solution also shows that adoption changes the sourcing structure, from a single supplier to all of them.

The result is proved in the paper; no machine-checked proof is known. This mission adds a three-layer supply chain game with recalls, Bayesian consumers and mean-variance utility, and it records two corrections of printed statements: the set of symmetric efforts at $\Psi=1$, $|\Xi|=2$, and the uniqueness claim for the cubic $\Lambda$, which holds on $(0,P)$ and not on the real line.

Difficulty

The proof in the paper looks short because Proposition 3.1 carries the work, and the obstacle is exhaustiveness. The optimality condition ranges over every order, including $\Psi\ge1$ and $|\Xi|\ge2$ without blockchain, where the supplier fixed point has several solutions, and including $\delta=1$, where $P^\star_{\mathrm B}=1$. The naive reduction to maximizing $f$ on the good region is valid only after every other order is shown to give utility at most $0$, under every symmetric supplier response. The variance computation over independent batches must produce the factor $1/|\Xi|$, and the strict preference for all $N$ suppliers needs $\Psi^\star<1$.

Formalization scope

Types and signals are Bool, suppliers are Fin N, and $v_\Delta=1$ is the paper's normalization. Probabilities are finite weighted sums on Fin N → Bool. Everything is real-valued, and $\chi$ is quantified after $\Omega^\star$.

The conventions follow the paper's proofs. The consumer conditions on type and signal, as on p.31. Demand is the purchase probability of a generic consumer, because the continuum integral (8) is not literally definable under independent signals. The supplier objective is per unit. The manufacturer's strategy does not depend on its type. The supplier stage is formalized as in the proof: a symmetric fixed point with exponent $|\Xi|-1$, assuming that all of $\Xi$ produce, with acceptance then evaluated at that effort. An equilibrium requires a symmetric response after every order and leaves its selection free, so the printed selection is one case. The number $\Omega^\star$ precedes $\chi$.

A trivializing formalization defines $\mathcal M$ as $f$ or the supplier response as the printed formula; here demand is the Bayes quotient, supplier behaviour is the arg max, and $\mathcal M$ comes from the random profit, so $f$, $\Lambda$ and the printed efforts enter only as milestones. The existence clause rules out a vacuous goal.

The development needs only Mathlib: Real.sqrt, Real.rpow, StrictConcaveOn, HasDerivAt, and finite sums. The independent-Bernoulli module is reusable. Proofs of the milestones in any order are welcome, and the utility computations are the natural place to start.

Selected references

• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Blockchain Adoption in a Supply Chain with Manufacturer Market Power, SSRN 3950580; published in Management Science, 2023. https://ssrn.com/abstract=3950580, https://doi.org/10.1287/mnsc.2022.02505
• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science 69(6):3415–3436, 2023; SSRN 3602376. https://ssrn.com/abstract=3602376

Motivation

Bayesian persuasion (Kamenica and Gentzkow, 2011) studies a sender who knows the state of the world and commits to a randomized signaling policy before a receiver acts. In the classical model the sender may send as many distinct messages as the receiver has actions, and by the revelation principle an optimal policy simply recommends an action. In many applications the channel is narrower than the action set: a recommender shows $k$ out of $n$ items, a platform has a fixed number of badges, a regulator can publish one of a few grades. With $k<n$ signals the sender can no longer point at every action, and which actions to bundle under one message becomes the core of the problem.

Gradwohl, Hahn, Hoefer and Smorodinsky (arXiv:2007.12489, published in Mathematics of Operations Research, 2022) study this limited-communication model algorithmically. Aybas and Turkel (arXiv:1910.13547) had shown that optimal schemes exist with $k$ signals and that the sender loses at most a $2/k$ fraction of utility when one signal is removed. Dughmi and Xu (arXiv:1503.05988) studied symmetric schemes for algorithmic persuasion with unrestricted signals. The mission formalizes the paper's structural result for symmetric instances: the characterization of an optimal scheme by a common slope on Pareto frontiers.

Setting

There are $n$ actions $[n]$ and a finite type set $T$. A state $\boldsymbol\theta=(\theta_1,\dots,\theta_n)\in T^n$ is drawn with probability $q_{\boldsymbol\theta}$. A type $t$ carries a value pair $(\varrho(t),\xi(t))$: the receiver $R$ gets $\varrho(\theta_i)$ and the sender $S$ gets $\xi(\theta_i)$ if $R$ takes action $i$. The instance is symmetric if $q_{\boldsymbol\theta}=q_{\boldsymbol\theta'}$ whenever $\boldsymbol\theta'$ is a permutation of $\boldsymbol\theta$. Types within a state of positive probability are assumed distinct.

A $k$-signal scheme $\varphi$ sends signal $\sigma\in[k]$ in state $\boldsymbol\theta$ with probability $\varphi(\boldsymbol\theta,\sigma)$, where $2\le k\le n$. Write

$$w_\sigma(i)=\sum_{\boldsymbol\theta}q_{\boldsymbol\theta}\varphi(\boldsymbol\theta,\sigma)\varrho(\theta_i),\qquad v_\sigma(i)=\sum_{\boldsymbol\theta}q_{\boldsymbol\theta}\varphi(\boldsymbol\theta,\sigma)\xi(\theta_i)$$

for the joint utilities of signal $\sigma$ and action $i$. The receiver best responds to each signal and breaks ties in favour of the sender, so the sender's utility is $u_S(\varphi)=\sum_\sigma\max\{v_\sigma(i): i\in\arg\max_j w_\sigma(j)\}$. A scheme is optimal if no $k$-signal scheme gives a larger $u_S$. A direct scheme recommends an action with each signal; it is persuasive if following the recommendation is a best response. The quantity $\varrho_E=\max_i\sum_{\boldsymbol\theta}q_{\boldsymbol\theta}\varrho(\theta_i)$ is the best the receiver gets from a fixed action.

For a direct scheme recommending action $j$ with signal $j\in[k]$, let $C$ be the set of types of the first $k$ actions and $q_C$ its probability. The recommendation point $p(C)=(\mathbb E[u_R\mid C],\mathbb E[u_S\mid C])$ lies in the convex hull of $\{(\varrho(c),\xi(c)):c\in C\}$. A point collection $\mathcal P$ assigns to each $C$ a point $p(C)=(p_R(C),p_S(C))$ in that hull, with $u_S(\mathcal P)=\sum_C q_Cp_S(C)$ and $u_R(\mathcal P)=\sum_Cq_Cp_R(C)$. For $s\le0$, $\mathcal P$ is $s$-Pareto (Definition 1) if every $p(C)$ is on the Pareto frontier of $C$, the line of slope $s$ through $p(C)$ is tangent to that frontier, and $u_R(\mathcal P)\ge\varrho_E$.

Formalization targets

Goal: Theorem 1 (p.6)

For every symmetric instance there are an optimal $k$-signal scheme $\varphi$ and a slope $s\le0$ such that $\varphi$ is direct and persuasive with recommendations from $[k]$, its recommendation points $\mathcal P(\varphi)$ are $s$-Pareto, and

$$u_S(\mathcal P')\le u_S(\mathcal P(\varphi))\qquad\text{for every }s'\text{-Pareto collection }\mathcal P',\ s'\le0.$$

The type set, the prior, the values and $k$ are arbitrary; no independence or special distribution is assumed.

Milestones

1. Lemma 1 (p.5): some optimal $k$-signal scheme is direct and persuasive with $k$ distinct recommended actions, and these can be $[k]$ in symmetric instances.
2. §2 display (p.5): in a symmetric instance $\varrho_E=\sum_{\boldsymbol\theta}q_{\boldsymbol\theta}\varrho(\theta_i)$ for every $i$.
3. §3.1 observation (p.6): recommendation points form a point collection with the scheme's utilities.
4. Lemma 2 (p.6): every direct persuasive scheme is weakly improved by an $s$-Pareto collection.
5. Lemma 3 (p.7): a symmetric scheme is persuasive iff $u_R(\varphi)\ge\varrho_E$.
6. Lemma 4 (p.8): every $s$-Pareto collection is realized by a symmetric, direct, persuasive scheme.

Significance

Theorem 1 replaces an optimization over all randomized maps from $T^n$ to $[k]$ by a one-parameter family: guess the common slope $s$, then each frontier contributes at most one segment, and the remaining choice is a linear program in the positions on those segments. This is the basis of the paper's Slope-Algorithm, which computes an optimal scheme in polynomial time given oracles for the probabilities of frontier segments, and of the polynomial-time oracles for IID, random-order and prophet-secretary distributions. It also underlies the paper's tight $k/n$ comparison between limited and unlimited signaling in symmetric instances.

The result is proved in the paper; it has not been machine-checked. The mission produces a finite, self-contained formal model of persuasion with limited signals and sender-favourable tie-breaking, which other limited-communication results can reuse, together with formal statements of each step of the characterization.

Difficulty

The obvious argument fails at two points. First, Lemma 2's exchange argument in the paper moves pairs of points along their frontiers until all share a slope, and does not argue that this terminates, so a complete proof has to supply a terminating argument. Second, optimality in Theorem 1 is against all $k$-signal schemes with the receiver's tie-broken best response, not only against direct persuasive ones. Closing the circle needs Lemma 1, the realization of an $s$-Pareto collection by a scheme (Lemma 4), and the fact that for symmetric schemes the $k\cdot n$ obedience constraints collapse to one inequality (Lemma 3), whose "if" direction uses the symmetry of both the instance and the scheme.

Formalization scope

The Lean development fixes the following conventions. All actions share one Fintype of types T; states are Fin n → T; the prior is a weight function q ≥ 0 with total mass 1; values ρ, ξ : T → ℝ are arbitrary. Signals are Fin k, and action j ∈ [k] is Fin.castLE hkn j. The receiver's response is formalized with the unnormalized sums $w_\sigma(i)$ and $v_\sigma(i)$ above, so a null signal involves no division and imposes no constraint; ties are broken toward the sender by taking the largest $v_\sigma$ over the receiver's maximizers. For a direct scheme, $u_S(\varphi)$ and $u_R(\varphi)$ in §3 (recommendation points, Lemmas 2–4) are the utilities when the receiver follows the recommendation; Theorem 1 and Lemma 1 additionally state that this equals the best-response utility for the scheme they produce. $q_C$ sums $q_{\boldsymbol\theta}$ over states whose first $k$ types form the Finset $C$, and every condition on a point collection is imposed for the sets $C$ with $q_C\ne0$. Points are in $\mathbb R\times\mathbb R$ with the receiver coordinate first. A point $p$ is on the Pareto frontier of $C$ if it lies in the convex hull and no hull point is strictly larger in both coordinates, which keeps the horizontal and vertical end segments of the paper's picture (p.6); $p$ corresponds to slope $s$ if $x_S-s\,x_R\le p_S-s\,p_R$ for every hull point $x$. Symmetric schemes are stated through cross-multiplied equalities of conditional type distributions, not through permutation-equivariance of $\varphi$.

A statement in which $s$-Pareto conditions were required for every set of types, including the empty set, would make every $s$-Pareto condition unsatisfiable and the sender-optimality clause vacuous; the $q_C\ne0$ guard rules this out, and a two-action example with an explicit $(-1)$-Pareto collection has been checked. Optimality is never restricted to direct, persuasive or symmetric schemes.

Needed infrastructure: convex hulls in $\mathbb R^2$ (Mathlib's convexHull), finite sums, permutations of Fin n, and an existence argument for an optimal scheme (compactness of the direct persuasive polytopes). The model definitions are reusable for the paper's other results (independent instances, approximation schemes), which are not part of this mission. Proofs of any milestone, and alternative proofs of Lemma 2, are welcome.

Selected references

• R. Gradwohl, N. Hahn, M. Hoefer, R. Smorodinsky, Algorithms for Persuasion with Limited Communication, arXiv:2007.12489v2, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2007.12489
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• Y. Aybas, E. Turkel, Persuasion with Limited Signal Spaces, arXiv:1910.13547, 2019. https://arxiv.org/abs/1910.13547
• S. Dughmi, H. Xu, Algorithmic Bayesian Persuasion, STOC 2016. https://arxiv.org/abs/1503.05988

Motivation

Percolation games were introduced by Garnier and Ziliotto (arXiv:2110.12227, published in Mathematics of Operations Research, 2022) as discrete toy models for the stochastic homogenization of non-convex Hamilton–Jacobi equations. In homogenization one asks whether a control or game problem in a random, spatially varying environment behaves, over long horizons, like a problem in a deterministic averaged environment. For convex Hamiltonians (one controller) this is classical; for non-convex Hamiltonians, which arise from two-player zero-sum differential games, homogenization can fail (Ziliotto, Comm. Pure Appl. Math. 2017; Feldman–Souganidis, J. Math. Pures Appl. 2017). Percolation games keep the two-player structure and the random environment but replace the continuum by the lattice $\mathbb Z^d$, and ask the corresponding question about the limit value of a repeated game: does the value of the $n$-stage game converge as $n\to\infty$, and to a deterministic constant?

The limit value question is central in the theory of zero-sum stochastic games (counterexamples to its existence by Vigeral, Dyn. Games Appl. 2013, and Ziliotto, Ann. Probab. 2016). Percolation games are stochastic games with infinitely many states, deterministic transitions and a random payoff field, a class for which none of these general results applies.

Setting

Fix $d\ge1$, finite nonempty action sets $I$ (Player 1) and $J$ (Player 2), and a transition function $q:I\times J\to\mathbb Z^d$. A probability space $(\Omega,\mathbb P)$ carries a payoff field $g_\omega(z,i,j)\in\mathbb R$, $(z,i,j)\in\mathbb Z^d\times I\times J$, that is uniformly bounded.

Given $\omega$ (known to both players) and an initial state $z_1=z$, at each stage $m\ge1$ Player 1 chooses $i_m$; then Player 2, knowing $i_m$, chooses $j_m$; Player 1 receives $g_\omega(z_m,i_m,j_m)$ from Player 2, and the state moves to $z_{m+1}=z_m+q(i_m,j_m)$. A strategy for Player 1 maps the past $(z_k,i_k,j_k)_{k<m}$ and the current state $z_m$ to an action; a strategy for Player 2 also receives $i_m$. The $n$-stage payoff and value are

$$\gamma^\omega_n(z,\sigma,\tau)=\frac1n\sum_{m=1}^n g_\omega(z_m,i_m,j_m),\qquad v^\omega_n(z)=\max_{\sigma}\min_{\tau}\gamma^\omega_n(z,\sigma,\tau)=\min_\tau\max_\sigma\gamma^\omega_n(z,\sigma,\tau).$$

Write $v_n(z)$ for the random variable $\omega\mapsto v^\omega_n(z)$ and $\mathbb E(v_n)=\mathbb E(v_n(0))$.

The game is oriented (Definition 2.1) if there is $u\in\mathbb Z^d$ with $q(i,j)\cdot u>0$ for every $(i,j)$: the state's coordinate along $u$ strictly increases, whatever the players do. It is i.i.d. (Definition 2.2) if the site vectors $\omega\mapsto(g_\omega(z,i,j))_{(i,j)\in I\times J}$, $z\in\mathbb Z^d$, are independent and identically distributed.

Formalization targets

Goal: Theorem 2.3

In an i.i.d., oriented percolation game there is a constant $v_\infty\in\mathbb R$ such that, for every $z\in\mathbb Z^d$, $v_n(z)\to v_\infty$ almost surely; there are $A,B>0$ such that for all $n\ge1$, $z\in\mathbb Z^d$ and $\lambda\ge0$,

$$\mathbb P\Bigl(|v_n(z)-v_\infty|\ge\lambda+A\ln(n+1)^{1/2}n^{-1/2}\Bigr)\le\exp(-B\lambda^2n);\tag{2.1}$$

and $|\mathbb E(v_n(z))-v_\infty|\le A'\ln(n+1)^{1/2}n^{-1/2}$ for some $A'>0$ and all $n\ge1$, $z$. The constants depend on the game, never on $n$, $z$ or $\lambda$.

Milestones

1. The $n$-stage game has a value in pure strategies (p.3).
2. $v_n(z)$ and $v_n(0)$ have the same law (p.5).
3. Changing the payoff on one hyperplane $\{z\cdot u=h\}$ moves every $\gamma_n$, and $v_n$, by at most the change divided by $n$ (pp.4–5).
4. (3.1): $|\mathbb E(v_n(0)\mid\mathcal F_{r+1})-\mathbb E(v_n(0)\mid\mathcal F_r)|\le2\|g\|_\infty/n$ a.s., where $\mathcal F_r$ is generated by the payoffs on $r$ hyperplanes.
5. (3.2), corrected: $\mathbb P(|v_n(0)-\mathbb E(v_n)|\ge\lambda)\le2\exp(-\lambda^2n/(8CM^2))$ for a constant $C$ depending on $q$ only and any uniform bound $M$ on the payoffs.
6. $\mathbb E(\min_{z\in\mathcal C_n}v_n(z))\ge\mathbb E(v_n)-D\ln(n+1)^{1/2}n^{-1/2}$, and the symmetric bound for the max (p.6).
7. Concatenation: $v_{m+n}(0)\ge\frac m{m+n}v_m(0)+\frac n{m+n}\min_{z\in\mathcal C_n}v_n(z)$ for $1\le m\le n$, and symmetrically (p.6).
8. (3.3) and its symmetric counterpart.
9. De Bruijn–Erdős: a subadditive sequence with an error term $f$, $\sum f(n)/n^2<\infty$, has $a_n/n$ convergent in $[-\infty,\infty)$.
10. $|\mathbb E(v_{2^\ell n})-\mathbb E(v_n)|\le D\sum_{k<\ell}\ln(2^kn+1)^{1/2}2^{-k/2}n^{-1/2}\le A\ln(n+1)^{1/2}n^{-1/2}$ for all $\ell,n\ge1$.
11. $\mathbb E(v_n)\to v_\infty$ with $|v_\infty-\mathbb E(v_n)|\le A\ln(n+1)^{1/2}n^{-1/2}$.

Significance

Theorem 2.3 gives a deterministic limit value for a class of zero-sum stochastic games with infinitely many states in a random environment, with a quantitative rate: fluctuations of order $n^{-1/2}$ up to a logarithm, as for sums of independent variables. In the homogenization picture it says that the oriented, i.i.d. discrete game homogenizes. Theorem 2.4 of the same paper shows that orientation alone does not suffice: there is an oriented game on $\mathbb Z^3$ with an ergodic but non-i.i.d. payoff field whose value oscillates between $0$ and $1$. Together they locate the dividing line.

The result is proved on paper; it has no machine-checked proof. The mission produces a formal model of percolation games (plays, history-dependent strategies, values), the existence of the value for finite perfect-information games of this form, and a complete formal proof of Theorem 2.3. Two printed statements in the proof need repair, and the formal versions fix them: the concentration bound (3.2) is false as printed (it lacks the factor $2$ of the two-sided Azuma inequality and the number of martingale steps), and the cube $\mathcal C$ must be symmetric around the origin, without which the concatenation step and the first inequality of (3.3) fail. Neither repair affects Theorem 2.3, whose constants are existential.

Difficulty

The obvious route, subadditivity of $n\mapsto n\,v^\omega_n(0)$ pathwise followed by a subadditive ergodic theorem, fails: after $m$ stages the game restarts from a state $z_{m+1}$ chosen by the players, not from a fixed site, so there is no pathwise subadditive inequality. The paper's argument replaces it by two separate controls. Concentration: $v_n(0)$ is a function of independent site vectors in which each hyperplane $\{z\cdot u=h\}$ is visited at most once, so the Doob martingale over hyperplanes has increments $O(1/n)$ and Azuma gives Gaussian concentration. Convergence of the mean: concentration and a union bound over the polynomially many possible restart states give near-subadditivity of $-n\mathbb E(v_n)$ with an error term $O(\sqrt{n\ln n})$, which the de Bruijn–Erdős lemma, not Fekete's lemma, handles. Formally, the delicate parts are the strategy concatenation (shifting histories and restarting optimal strategies), the measurability of $v_n(z)$, and the conditional-independence step behind (3.1).

Formalization scope

$\mathbb Z^d$ is Fin d → ℤ. Strategies are pure and history-dependent, indexed from stage $0$ with histories Fin m → ℤ^d × I × J; Player 2's strategy receives Player 1's current action. The value is ⨆ σ, ⨅ τ, gamma … over all strategies; for finite $I,J$ only finitely many histories are reachable in $n$ stages, so the supremum and infimum are of finite families for every payoff function, and milestone 1 proves they are attained and equal to the min–max. The play depends on the strategies and the transition only, never on the payoffs.

The i.i.d. hypothesis is: every $g(z,i,j)$ is measurable, the site vectors are mutually independent (iIndepFun) and identically distributed (IdentDistrib). The paper's model also carries an ergodic measure-preserving $\mathbb Z^d$-action and a stationarity condition; these are dropped, since i.i.d. sites already have a translation-invariant law and the proof uses nothing more. "Uniformly bounded" is one bound $M$ for all $\omega,z,i,j$. Expectations are Bochner integrals and probabilities are measures of sets; $v_n(z)$ is bounded and measurable (milestone 2), so neither convention is degenerate. A trivializing encoding, a value that is a junk constant, is ruled out by the sanity checks in the development: with one action each and $q=1$ the value is the path average, and for $n=1$ it is $\max_i\min_j g(z,i,j)$.

A complete development needs: backward induction for the finite perfect-information game, a translation-equivariance lemma for values, the Doob martingale over hyperplanes with a conditional-independence argument, Azuma's inequality (available on the platform as ModernOnlineLearning.OnlineToBatch.theorem_3_9), Borel–Cantelli, and the de Bruijn–Erdős lemma, which is not in Mathlib and is reusable on its own. Contributions to any milestone are welcome, including alternative proofs of the de Bruijn–Erdős lemma.

Selected references

• G. Garnier, B. Ziliotto, Percolation games, arXiv:2110.12227v2, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2110.12227
• N. G. de Bruijn, P. Erdős, Some linear and some quadratic recursion formulas II, Proc. Koninklijke Nederlandse Akademie van Wetenschappen, Series A, 14, 152–163, 1952.
• B. Ziliotto, Stochastic homogenization of nonconvex Hamilton–Jacobi equations: a counterexample, Communications on Pure and Applied Mathematics 70(9), 1798–1809, 2017.
• W. M. Feldman, P. E. Souganidis, Homogenization and non-homogenization of certain non-convex Hamilton–Jacobi equations, Journal de Mathématiques Pures et Appliquées 108(5), 751–782, 2017.
• B. Ziliotto, Zero-sum repeated games: counterexamples to the existence of the asymptotic value and the conjecture maxmin = lim v(n), Annals of Probability 44(2), 1107–1133, 2016. https://doi.org/10.1214/14-AOP997
• G. Vigeral, A zero-sum stochastic game with compact action sets and no asymptotic value, Dynamic Games and Applications 3(2), 172–186, 2013.