All missions

Counting Nash equilibria of bimatrix games

A bimatrix game is a two-player game in strategic form, given by two payoff matrices. Its central solution concept is Nash equilibrium, a pair of randomized strategies that are optimal against each other (Nash 1951). How many Nash equilibria a game can have matters for algorithms that find one or all of them, and for the combinatorics of the polytopes that encode the game.

Quint and Shubik conjectured that a non-degenerate $n\times n$ game has at most $2^n-1$ Nash equilibria. The bound is attained by the coordination game, in which both payoff matrices are the identity.

• 1997. Quint and Shubik state the conjecture. It is immediate for $n\le3$ from a count of polytope vertices.
• 1997–1999. The case $n=4$ is proved by Keiding and by McLennan and Park.
• 1999. von Stengel refutes the conjecture for $n\ge6$ with a $6\times6$ game with 75 equilibria, and constructs games with about $2.4^n/\sqrt n$ equilibria. The case $n=5$ stays open.
• 2025. Ickstadt, Theobald and von Stengel prove the case $n=5$.

Best-response polytopes, labels and the index

Let $(A,B)$ be a pair of real $m\times n$ matrices. A mixed strategy is a probability vector over a player's pure strategies. The game is non-degenerate if, for any mixed strategy $z$ of a player, at most $|\mathrm{supp}(z)|$ pure strategies are best responses to $z$. Up to adding a constant to the payoffs, which changes no best response, the polyhedra

$$P=\{x\in\mathbb R^m\mid x\ge0,\ B^\top x\le\mathbf 1\},\qquad Q=\{y\in\mathbb R^n\mid Ay\le\mathbf 1,\ y\ge0\}$$

are bounded, and these best-response polytopes carry the $m+n$ labels of their inequalities. A pair $(x,y)\in P\times Q$ is an equilibrium if every label is binding at $x$ or at $y$. This includes the artificial pair $(0,0)$, and every other equilibrium is a Nash equilibrium after rescaling.

A face arises by turning inequalities into equalities. A $d$-polytope is simple if every vertex lies in exactly $d$ facets, and dual-neighborly if any $\lfloor d/2\rfloor$ of its facets meet. The index of a completely labeled vertex is the sign of a determinant of facet normals, normalized so that $0$ has index $-1$. For a graph $G$, the stable-set bound $b(G)$ is twice the largest size of a pair of disjoint stable sets of equal size. $\mathcal P^d_k$ denotes the set of combinatorial types of simple $d$-polytopes with $k$ facets.

Formalization targets

Goal

The goal is Theorem 5 of the paper: for all $A,B\in\mathbb R^{5\times5}$ with $(A,B)$ non-degenerate,

$$\#\{(x,y)\mid (x,y)\text{ is a Nash equilibrium of }(A,B)\}\le 31.$$

The statement refers to no polytope. No positivity or finiteness is assumed.

Milestones

The milestones follow the paper. The polytope layer: Lemma 2 (maximal vertex numbers), Lemma 3 (non-degeneracy in polyhedral form) and Lemma 4 (from polytopes back to games). The index layer: Theorems 1 and 2 (parity and index on labeled polytopes) and Lemma 5 (adjacent equilibrium vertices have opposite index). The stable-set bounds:

$$\#\{\text{equilibria}\}\le 2|S_1|$$

for a maximal stable pair of the graph of $P$ (Theorem 3), with a version for facets (Theorem 4). The case analysis: Theorem 6 (dual-neighborly case), the tables (8) and (9) of pairs $(V,b)$ for $\mathcal P^4_8,\dots,\mathcal P^4_5$, Theorem 7 (facts on $\mathcal P^4_9$) and Lemmas 7, 8, 9.

What the result gives

Theorem 5 completes the answer to the Quint–Shubik question: the bound $2^n-1$ holds exactly for $n\le5$. The stable-set bound of Theorem 3 is a new obstruction, usable for other game sizes, that strengthens the parity argument of Lemke and Howson through the index of Shapley (1974).

The paper's proof is mathematically complete but rests on computer calculations over published lists of polytopes: the 159,375 dual-neighborly types of Firsching (2017) for Theorem 6, the 1,142 types of $\mathcal P^4_9$ for Theorem 7, and tables (8) and (9). No machine-checked proof of these results has been located. The mission records these inputs as precise statements and asks for proofs. A complete formal proof would also certify the computational classification on which the paper depends, and the polytope layer is usable well beyond this result.

The central difficulty

The obvious approach counts vertices. It is not enough: a simple 5-polytope with 10 facets can have 42 vertices, and a non-neighborly one up to 40, while the target is 32 equilibria. The two disjoint facets of a non-neighborly polytope are 4-polytopes, each carrying at most 16 equilibria, but equilibria may also have vertices on neither facet. So each equilibrium has to be traced through both polytopes at once.

For Lean, the main obstacle is that the classification statements have no short human proof. Displays (8) and (9) and Theorems 6 and 7 are finite facts about all combinatorial types, and no list of the types is in Mathlib. A proof needs either a verified enumeration or a new argument.

Formalization scope

Polyhedra are finite systems $Cz\le q$ in $\mathbb R^N$, and every notion is defined for a face of a system, so a facet of $P$ is a polytope without a change of coordinates. Faces are nonempty, dimension is that of the affine hull, and facets satisfy $\dim G+1=\dim F$. Combinatorial type is an order isomorphism of face posets. Labels of $[m+n]$ are Fin m ⊕ Fin n, and the label of a row is the row index. "Equilibria" counts $(0,0)$; "Nash equilibria", the published IsNE, does not. Counts use Set.encard, so finiteness is part of each claim. "At least $t$ obstruction vertices" is $t+b\le V$, as on p.16 of the paper.

Non-degeneracy ranges over all mixed strategies of both players, and it fails for the zero game, so the goal cannot hold vacuously. The stable-set bound is pinned down by proved checks on the triangle and the 4-cycle, and the face encoding by the unit square.

Theorems 1, 2 and 3 add $d\ge1$, $d\ge1$ and $m\ge1$, because the printed statements fail for the zero-dimensional polytope and the $0\times0$ game.

A complete development needs Lemke–Howson paths on simple polytopes, the sign of a determinant along an edge, the face lattice of a simple polytope, the upper bound theorem, and the enumerations. All of these are reusable. Contributions to any layer are welcome, including independent proofs of the tables and of the classification.

Selected references

• C. Ickstadt, T. Theobald, B. von Stengel, A stable-set bound and maximal numbers of Nash equilibria in bimatrix games, arXiv:2411.12385v3, 2025. https://arxiv.org/abs/2411.12385v3
• T. Quint, M. Shubik, A theorem on the number of Nash equilibria in a bimatrix game, Int. J. Game Theory 26, 1997. https://doi.org/10.1007/BF01263276
• H. Keiding, On the maximal number of Nash equilibria in an $n\times n$ bimatrix game, Games Econ. Behav. 21, 1997. https://doi.org/10.1006/game.1997.0531
• A. McLennan, I.-U. Park, Generic $4\times4$ two person games have at most 15 Nash equilibria, Games Econ. Behav. 26, 1999. https://doi.org/10.1006/game.1998.0640
• B. von Stengel, New maximal numbers of equilibria in bimatrix games, Discrete Comput. Geom. 21, 1999. https://doi.org/10.1007/PL00009438
• L. Shapley, A note on the Lemke–Howson algorithm, Math. Programming Study 1, 1974. https://doi.org/10.1007/BFb0121248
• M. Firsching, Realizability and inscribability for simplicial polytopes via nonlinear optimization, Math. Program. 166, 2017. https://doi.org/10.1007/s10107-017-1120-0

Motivation

A sweeping process is the evolution of a point that is pushed by a moving set: given a set-valued map $S:\mathbb R\rightrightarrows\mathbb R^n$, an orbit $\gamma$ stays in $S(t)$ and moves only along inner normals of $S(t)$. J.-J. Moreau introduced the model in the 1970s for elastoplasticity and unilateral mechanics, and it is now a standard object of nonsmooth dynamics, with applications to crowd motion, hysteresis and electrical circuits. A natural question is when every orbit started near a given time has finite length, uniformly.

For gradient flows the answer is the Kurdyka–Łojasiewicz (KL) inequality. Bolte, Daniilidis, Ley and Mazet (Trans. AMS 2010) proved that, for a $C^2$ convex coercive function with an upper-isolated critical value, the KL inequality holds if and only if the lengths of subgradient curves are uniformly controlled, if and only if the "talweg" $r\mapsto\sup_{f(x)=r}1/\|\nabla f(x)\|$ is integrable. Daniilidis and Drusvyatskiy (Sweeping by a tame process, Ann. Inst. Fourier 67 (2017), 2201–2223) showed that a sweeping process with a definable (o-minimal) bounded graph can always be desingularized by a change of time.

Daniilidis and Tapia-García (arXiv:2110.08686v1, published as Oriented Calmness and Sweeping Process Dynamics, Math. Oper. Res. 2024) drop o-minimality and prove a characterization in the spirit of the KL theory for sweeping processes with a smooth graph. The key new object is an oriented modulus of the coderivative, which sees only the direction in which the sets recede.

Setting

Write $\mathcal S=\operatorname{gph}S=\{(t,x)\in\mathbb R\times\mathbb R^n:x\in S(t)\}$ and $\operatorname{dom}(S)=\{t:S(t)\neq\emptyset\}$. For a set $C$, $N_C(x)$ is the limiting normal cone: the limits of Fréchet normals $v_i\in\hat N_C(x_i)$ with $x_i\to x$ in $C$, where $\hat N_C(x)$ consists of the $v$ with $\limsup_{y\to x,\,y\in C}\langle v,y-x\rangle/\|y-x\|\le0$.

• An orbit on an interval $I$ is an absolutely continuous $\gamma$ with $\gamma(t)\in S(t)$ for all $t\in I$ and $-\dot\gamma(t)\in N_{S(t)}(\gamma(t))$ for almost every $t$; $\mathcal{AC}(S,I)$ is the set of orbits, and $\mathcal{PAC}(S,I)$ the set of piecewise absolutely continuous orbits, whose jumps lie in a closed countable set. The length is $\ell(\gamma)=\int_I\|\dot\gamma\|$.
• The coderivative is $D^*S(t,x)(u)=\{a\in\mathbb R:(a,-u)\in N_{\mathcal S}(t,x)\}$, and the oriented modulus is

$$\|D^*S(t,x)|^+=\sup\{a^+:a\in D^*S(t,x)(u),\ \|u\|\le1\},\qquad \sup\emptyset=0.$$

• The oriented talweg is $\varphi^\uparrow(t)=\sup_{x\in S(t)}\|D^*S(t,x)|^+$.
• $S$ is a smooth sweeping process if $\mathcal S$ is closed and connected and either a $C^1$ submanifold of $\mathbb R^{n+1}$ of dimension at most $n$, or a full-dimensional region whose boundary $\partial\mathcal S$ is a $C^1$ hypersurface.
• With $T=\sup\operatorname{dom}(S)$ and $H_S(t)=\partial\mathcal S\cap(\{t\}\times\mathbb R^n)$: (A1) from every $(t,x)\in\mathcal S$ with finite oriented modulus some orbit starts; (A2) at $\bar t<T$, $\varphi^\uparrow<\infty$ on some $(\bar t,\bar t+\delta)$; (A3) at $\bar t<T$, $H_S$ is Pompeiu–Hausdorff continuous on some $(\bar t,\bar t+\delta)$. $\mathcal T$ is the set of $t\in\operatorname{dom}(S)$ where (A2) and (A3) hold.

Formalization targets

Goal: Theorem A (pp.9–10)

For a smooth sweeping process with bounded values satisfying (A1), and $a\in\mathcal T$, the following are equivalent:

• a) there are $b>a$, $\rho>0$ and an increasing homeomorphism $\Psi:[0,\rho]\to[a,b]$, $C^1$ with $\Psi'>0$ on $(0,\rho)$, such that $\|D^*(S\circ\Psi)(r,x)|^+\le1$ for all $r\in(0,\rho)$, $x\in S(\Psi(r))$;
• b) there are $b>a$ and an increasing continuous $\sigma$ with $\sigma(a)=0$ and $\ell(\gamma)\le\sigma(t_2)-\sigma(t_1)$ for all $a\le t_1<t_2\le b$, $\gamma\in\mathcal{AC}(S,[t_1,t_2])$;
• c) there are $b>a$ and $M>0$ with $\ell(\gamma)\le M$ for every $b'\in(a,b]$ and $\gamma\in\mathcal{PAC}(S,[a,b'])$;
• d) there is $b>a$ with

$$\int_a^b\varphi^\uparrow(t)\,dt<\infty.$$

Clause c) is stated in a corrected form. The paper quantifies only over $\mathcal{PAC}(S,[a,b])$ for one $b$, and that class can be empty for large $b$ while d) fails; the goal's item lists a counterexample. The corrected clause is what the paper's proof uses.

Milestones

Lemma 15 (continuity of both moduli on $\partial\mathcal S$), Lemma 16 (continuity of the talwegs), Proposition 17 (time rescaling of orbits), Proposition 18 a)–c) (geometric facts at boundary points), Lemma 19 ($\|\dot\gamma(t)\|=\|D^*S(t,\gamma(t))|^+$), Proposition 20 (concatenation into piecewise orbits), and the exact chain rule $\|D^*(S\circ\Psi)(r,x)|^+=\Psi'(r)\|D^*S(\Psi(r),x)|^+$ behind the last display of the proof (p.15).

Significance

Theorem A reduces a dynamic property (all orbits near $a$ have controlled length) to a static one (integrability of a function computed from normal cones of the graph), and both to the existence of a desingularizing change of time. It extends the Bolte–Daniilidis–Ley–Mazet characterization from gradient curves to sweeping processes, and the o-minimal desingularization of Daniilidis–Drusvyatskiy to non-definable maps with smooth graph. The companion Theorem B adds discrete versions (catching-up algorithms) and is not part of this mission.

The result is proved on paper. As far as is known, no part of it, and no sweeping-process theory at all, has been formalized. The mission produces Lean statements of the paper's definitions (oriented modulus, talweg, smooth sweeping process, orbits and piecewise orbits) and of each step of the proof, so the whole argument can be checked.

Difficulty

The equivalence chains through four different arguments. a) ⇒ b) needs that the speed of an orbit equals the oriented modulus (Lemma 19), which rests on a normal-cone calculus rule for $\{t\}\times S(t)=\mathcal S\cap(\{t\}\times\mathbb R^n)$ and on the tangent geometry of $\partial\mathcal S$; the qualification condition in that rule fails exactly where the modulus is infinite. c) ⇒ d) builds orbits whose speed nearly attains $\varphi^\uparrow$, which needs continuity of $\varphi^\uparrow$ (from the Hausdorff continuity of the boundary slices) and a transfinite gluing of local orbits into one piecewise orbit (Proposition 20). d) ⇒ a) needs the chain rule for the coderivative under a $C^1$ change of time.

The obvious attempt, bounding lengths by $\int\varphi^\uparrow$ directly through Lemma 19, does not give c) ⇒ d): the bound goes the wrong way, and one must exhibit long orbits, not bound short ones.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\mathbb R^{n+1}$ is $\mathbb R\times\mathbb R^n$ with time first (max norm; normal cones and Hausdorff continuity do not depend on the choice of equivalent norm).
• Normal cones and the coderivative are the published platform definitions GenNewtonSubgrad.ProxReg.{gph, limNormal, coderiv} and StrictCQ.CAKKT.limNormal.
• Moduli, talwegs, lengths and the integral of d) take values in $[0,+\infty]$; $a^+$ is ENNReal.ofReal a, empty suprema are $0$, so a real-valued supremum never returns a junk value.
• Absolute continuity on a non-compact interval is absolute continuity on its compact subintervals; length is $\int\|\gamma'\|$, never the variation (jumps of a piecewise orbit do not count).
• Definition 10 is encoded by local $C^1$ defining functions (a submersion for a submanifold, a function with nonvanishing derivative and $\mathcal S=\{g\le0\}$ near the boundary).

A trivializing formalization is excluded: verification files check that the smoothness predicate is satisfiable, that constant curves are orbits of length $0$, that every orbit is a piecewise orbit, and that the oriented modulus vanishes at interior points of the graph.

Reusable beyond this mission: the oriented modulus and talweg, the orbit classes and the length functional, and the chain rule for a $C^1$ change of time. Proofs of any milestone are welcome; the normal-cone facts for $C^1$ manifolds with boundary are the main missing infrastructure.

Selected references

• A. Daniilidis, S. Tapia-García, Desingularization of the Sweeping Process Mapping, arXiv:2110.08686v1, 2021; published as Oriented Calmness and Sweeping Process Dynamics, Math. Oper. Res., 2024. https://arxiv.org/abs/2110.08686, https://doi.org/10.1287/moor.2021.0269
• J. Bolte, A. Daniilidis, O. Ley, L. Mazet, Characterizations of Łojasiewicz inequalities: subgradient flows, talweg, convexity, Trans. Amer. Math. Soc. 362 (2010), 3319–3363. https://doi.org/10.1090/S0002-9947-09-05048-X
• A. Daniilidis, D. Drusvyatskiy, Sweeping by a tame process, Ann. Inst. Fourier 67 (2017), 2201–2223 (reference [9] of the paper).
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Why indicator variables and low rank

Many optimization models in statistics, machine learning and finance minimize a convex function of a continuous vector $x\in\mathbb R^n$ under logical conditions on its support. Best subset selection, sparse regression and sparse portfolio selection are standard cases. A binary indicator variable $z_i$ models such a condition: $z_i=0$ forces $x_i=0$, and $z_i=1$ leaves $x_i$ free. The complementarity constraint $x_i(1-z_i)=0$ makes these sets nonconvex, and the strength of a mixed-integer formulation is measured by how closely its relaxation approximates the closed convex hull.

Objective terms in these models often have a special shape: a low-dimensional nonlinear function composed with a linear map, such as a squared residual or a logistic loss of $a^\top x$. Disjunctive programming, developed by Balas for polyhedra and extended to convex sets by Ceria and Soares, describes the convex hull of a union of convex sets by creating one copy of the variables per set. Applied to $2^n$ support patterns, it gives a formulation of exponential size. Han and Gómez show that the size depends exponentially only on the rank of the function, not on $n$.

Setting

Fix a $k\times n$ real matrix $A$, a vector $c\in\mathbb R^n$, a subset $I_+\subseteq[n]$ of variables restricted to be nonnegative, and an extended-valued function $g$ on $\mathbb R^k$ with $g(0)=0$. Put

$$f(x)=g(Ax)+c^\top x .$$

A function with such a representation has rank at most $k$ in the sense of the paper (Definition 1). The mixed-integer epigraph is

$$Q=\{(t,x,z)\in\mathbb R^{n+1}\times\{0,1\}^n: t\ge f(x),\ x_i\ge0\ \forall i\in I_+,\ x_i(1-z_i)=0\ \forall i\in[n]\}.$$

For $I\subseteq[n]$, the set $X(I)$ consists of the pairs $(t,x)$ with $t\ge f(x)$, $x_i\ge0$ on $I_+$ and $x_i=0$ off $I$. The set $Z(I)$ consists of the binary vectors with $z_i=1$ on $I$. The pieces are $V(I)=X(I)\times Z(I)$, and $Q=\bigcup_{I\subseteq[n]}V(I)$. The ray set is

$$R=\{(t,x,z):t\ge c^\top x,\ Ax=0,\ x_i\ge0\ \forall i\in I_+,\ z_i=1\ \forall i\in[n]\}.$$

The support function of a set $S$ is $\delta^*(\alpha;S)=\sup_{x\in S}\alpha^\top x$, with values in $[-\infty,+\infty]$.

Formalization targets

Goal

Theorem 1 of the paper, for every $n$, $k$, $A$, $c$, $I_+$ and $g$ as above:

$$\operatorname{cl}\operatorname{conv}(Q)=\operatorname{cl}\operatorname{conv}\Bigl(\Bigl(\bigcup_{I:|I|\le k}V(I)\Bigr)\cup R\Bigr),$$

and, if $\{x\in\mathbb R^n:Ax=0,\ x_i\ge0\ \forall i\in I_+\}=\{0\}$, also

$$\operatorname{cl}\operatorname{conv}(Q)=\operatorname{cl}\operatorname{conv}\Bigl(\bigcup_{I:|I|\le k}V(I)\Bigr).$$

Milestones

In the order of the paper's argument:

1. Proposition 1: for a closed convex set $T$, $T=\operatorname{cl}\operatorname{conv}(S)$ if and only if the support functions of $T$ and $S$ agree.
2. Equation (4): $V(I)\subseteq Q$ for every $I$, and $Q=\bigcup_{I\subseteq[n]}V(I)$.
3. The inclusion $R\subseteq Q$.
4. The unbounded case of the linear program (7): an improving direction $d$ with $Ad=0$ exists.
5. The finite case of (7): an optimal extreme point $x^*$ with $|\operatorname{supp}(x^*)|\le k$ exists.
6. For $(\bar t,\bar x,\bar z)\in Q$ and $x^*$ feasible for (7), $(\bar t+c^\top(x^*-\bar x),x^*,\bar z)\in V(\operatorname{supp}(x^*))$.
7. Under the trivial-cone hypothesis, the feasible region of (7) is bounded.
8. The inequality $\delta^*(\alpha;Q)\le\delta^*(\alpha;S)$, with and without $R$.

Significance

The result. Theorem 1 replaces $2^n$ disjuncts by $O(n^k)$ disjuncts plus one polyhedral set. Disjunctive programming on the smaller union then gives extended formulations of size polynomial in $n$ for fixed $k$. The paper derives from it the $O(n)$-variable formulations for rank one, which recover or generalize known convex hulls with indicator variables, and it reports computational results on rank-two structures.

The formalization. The theorem is proved in the paper; a search of the platform found no machine-checked proof. Beyond the theorem itself, the mission gives a checked account of the disjunctive structure of $Q$ and a reusable statement linking closed convex hulls to support functions in extended-real form. It also records a correction. As printed, (5) reads $t\ge0$ instead of $t\ge c^\top x$, which is false for $c\ne0$. For $n=k=1$, $A=0$, $g\equiv0$, $c=1$, $I_+=\emptyset$, the point $(0,1,1)$ lies in the printed right-hand side, while $\operatorname{cl}\operatorname{conv}(Q)$ lies in $\{t\ge x\}$. The two sets agree for $c=0$, the case of the paper's Section 3.

Difficulty

The set $Q$ is a union of $2^n$ pieces, and for a general convex function all of them matter: a separable function $\sum_i f_i(x_i)$ has full rank, and no bound on the support of the pieces can be expected for it. A reduction therefore has to use the structure $f=g\circ A+c^\top$ itself, and the reduction has to respect the binary part of the point, the sign restrictions on $I_+$, and the value of $t$ at the same time.

The obvious statement, that the pieces with $|I|\le k$ suffice, is false. For rank zero, $f(x)=c^\top x$ with $I_+=\emptyset$, the only piece with $|I|\le0$ is $V(\emptyset)$, which has $x=0$, while $Q$ contains points with every $x$. So the unbounded directions have to be accounted for separately whenever the cone $\{x:Ax=0,\ x_i\ge0\ \forall i\in I_+\}$ is nontrivial, and the ray set has to carry exactly the right value of $t$. The correction above shows how easily this bookkeeping goes wrong when a linear term is present. In the formal setting, every comparison also has to survive extended values: $f$ can be $+\infty$, and support functions can be $\pm\infty$.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ with $0$-based indices, and points $(t,x,z)$ live in ℝ × (Fin n → ℝ) × (Fin n → ℝ), whose product topology is the Euclidean one. The function $g$ has type (Fin k → ℝ) → EReal, and $f$ is objective g A c, which adds the real number $c^\top x$ coerced to EReal. The matrix is Matrix (Fin k) (Fin n) ℝ, a subset $I$ is a Finset (Fin n), and $z\in\{0,1\}^n$ is ∀ i, z i = 0 ∨ z i = 1. The support function is the published EReal-valued VectorSpaceOpt_support_functional, evaluated at continuous linear functionals. Closed convex hulls are closure (convexHull ℝ ·).

"rank$(f)\le k$" is encoded as a representation with a $k$-row matrix: the theorem holds for every such representation, and $R$ and the cone are built from its $A$. No properness, closedness or convexity of $g$ is assumed, since none is needed. Only $f(0)=0$ is. This covers the paper's $g$, including finite-valued and indicator-type functions, and $k\ge n$ needs no separate treatment.

The statement cannot trivialize: $g$ is not real-valued, $Q$ is not convex in general (for $n=k=1$, $A=0$, $g\equiv0$, $c=0$, the midpoint of $(0,0,0)$ and $(0,0,1)$ is outside $Q$), and $z$ is constrained to be binary in $Q$ and in $V(I)$, so the hull relaxes it. The linear program (7) is stated with its exact constraints, not with $x\ge0$.

A full development needs the separation argument behind Proposition 1, the extreme-point analysis of a polyhedron in one orthant, and a short extended-real calculation. The first two are reusable beyond this mission. Contributions welcome: proofs of the milestones, general lemmas on support functions and on extreme points of polyhedra, and the formulations for rank one derived from the goal.

Selected references

• S. Han and A. Gómez, Compact Extended Formulations for Low-Rank Functions with Indicator Variables, arXiv:2110.14884v2, 2023. https://arxiv.org/abs/2110.14884v2
• E. Balas, Disjunctive programming, Annals of Discrete Mathematics 5, 3–51, 1979. https://doi.org/10.1016/S0167-5060(08)70342-X
• E. Balas, Disjunctive Programming, Springer, 2018. https://doi.org/10.1007/978-3-030-00148-3
• S. Ceria and J. Soares, Convex programming for disjunctive convex optimization, Mathematical Programming 86(3), 595–614, 1999. https://doi.org/10.1007/s101070050106
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• J.-B. Hiriart-Urruty and C. Lemaréchal, Fundamentals of Convex Analysis, Springer, 2001. https://doi.org/10.1007/978-3-642-56468-0

Why suppliers and retailers bargain, and how the outcome is predicted

Wholesale prices between a supplier and a retailer are usually negotiated, not posted. Models of such negotiations almost always use the Nash bargaining solution (Nash, 1950), often in the generalized form with a bargaining power $\theta$ (Binmore, Rubinstein, Wolinsky, 1986). The Nash solution satisfies independence of irrelevant alternatives, which is the axiom most often questioned when a negotiator's outside prospects change. The Kalai–Smorodinsky (KS) solution (Kalai, Smorodinsky, 1975) replaces that axiom by monotonicity, and divides the surplus in proportion to what each party could obtain at best.

Feng, Li and Shanthikumar (2022) compare the two solutions in competing supply chains. This mission formalizes their central finding: under simultaneous negotiation without contingency terms, the KS equilibrium is the Nash equilibrium in which the retailer holds power $0.6$, not the symmetric $0.5$. Each negotiation is treated as a best response to the other, the "Nash-Nash" approach of Davidson (1988); the corresponding Nash bargaining solution for this model was derived by Feng and Lu (2013).

The two competing channels

A supplier produces at marginal cost $c$. Prices in the two channels are

$$p_i(q_i,q_j)=a-bq_i-\eta bq_j,\qquad i\ne j,$$

with $a>c$, $b>0$ and substitutability $\eta\in[0,1]$. Each channel has a wholesale price $w_i\in[c,a]$.

In the one-to-two channel one supplier sells to two retailers, who then choose quantities in a Cournot game. In the two-to-one channel two suppliers sell to one retailer, who then chooses both quantities. In both, the retail stage determines quantities $q^*_i(w)$ and prices $p^*_i(w)$, hence the trade profits

$$R_i=q^*_i(w)(w_i-c),\qquad r_i=q^*_i(w)(p^*_i(w)-w_i).$$

The common party collects both trades: the one-to-two supplier earns $\Pi=R_i+R_j$, and the two-to-one retailer earns $\pi=r_i+r_j$.

There are two bargaining units. Unit $i$ bargains over $w_i$ taking $w_j$ as given. The common party's disagreement point is its profit from the other trade alone, $D_i(w_j)$ or $d_i(w_j)$; the other party's is $0$. The maximum profits $\overline\Pi_i(w_j)$, $\overline\pi_i(w_j)$ are constrained maxima, each subject to the other side's individual rationality. The Nash solution with retailer power $\theta$ maximizes $(\pi-d)^\theta(\Pi-D)^{1-\theta}$. The KS solution is the Pareto optimal allocation with

$$\frac{\pi-d}{\Pi-D}=\frac{\overline\pi-d}{\overline\Pi-D}.$$

A simultaneous equilibrium is a pair $(w_1,w_2)$ in which each contract is the solution of its unit given the other.

Formalization targets

Goal: Proposition 2

For every $a>c$, $b>0$, with

$$\hat w=c+\frac{a-c}5\quad(\eta\in[0,1]),\qquad\check w=c+\frac{(1-\eta)(a-c)}{5-\eta}\quad(\eta\in[0,1)),$$

in the one-to-two and two-to-one channel respectively: the simultaneous KS equilibrium exists, is unique and is the symmetric pair at this price; that pair is a simultaneous Nash equilibrium with power $\theta\in[0,1]$ exactly when $\theta=3/5$; and the Nash equilibrium at $\theta=3/5$ is that same unique pair.

Milestones

1. Lemma 1: the retail stage in both channels.
2. Appendix A: the reduction to $a=b=1$, $c=0$, for profits, responses and equilibria.
3. Displays (17)–(19) and (35)–(37): the normalized payoffs and disagreement points.
4. Lemmas A.1, A.4: the maximum profits, and which contracts are Pareto-dominated.
5. Lemmas A.2, A.5: the Nash and KS best responses as explicit piecewise functions of $w_j$.

What the result gives

The price $0.6$ does not depend on $\eta$ or on the channel structure. A modeller who uses the Nash solution with $\theta=0.6$ therefore obtains the KS prediction in all these simultaneous models, which replaces a comparison of two solution concepts by a single parameter. The result also shows why the symmetric Nash solution is not a neutral benchmark here: the quantity-setting retailer has the higher maximum profit.

The result has a published proof on paper. Neither Proposition 2 nor the best-response lemmas have a machine-checked proof. The formalization adds three things. It fixes what "the KS solution" means on a non-convex allocation set. It checks the four- and five-piece response formulas, whose discriminants have degree six. And it proves uniqueness of the equilibrium over all contract pairs, which requires the full response maps and not only their symmetric fixed point.

The central difficulty

Each bargaining unit's allocation set is a curve and is not convex, because the profits change regime where a quantity hits zero. The maximum profits are themselves piecewise in $w_j$. The naive computation, solving the two first-order conditions at a symmetric interior point, finds the candidate price but proves neither that it is an equilibrium nor that it is the only one: it must be compared with responses in the other regimes, where one retailer or supplier is shut out. Those regimes carry thresholds that are defined only implicitly. The hardest parts are the KS response in the regimes where the maximum profit and the ratio come from different pieces, and the Nash response whose value is a root of a cubic.

Formalization scope

The Lean development works over ℝ, with parameters as above. Conventions fixed by the formalization:

• BargainingUnit is a general structure: contracts, two payoff functions, a disagreement point. The KS solution is individual rationality, Pareto optimality and the equation above cross-multiplied. Pareto optimality rules out the trivial solution: every contract with the disagreement allocation satisfies the equation as $0=0$.
• $\overline\Pi$, $\overline\pi$ are sSups of constrained images, and the milestones prove attainment. Without this sSup could silently be $0$.
• The Nash product uses Real.rpow, compared only over individually rational contracts, with $0^0=1$ at $\theta\in\{0,1\}$.
• Lemma 1's case conditions and the sets $\hat{\mathcal C}$, $\check{\mathcal C}$ have cleared denominators, so $\eta=0$ and $w_j=a$ are meaningful. Prices come from the demand function, so Lemma 1's prices are results.
• The two-to-one channel requires $\eta<1$: at $\eta=1$ the retail quantities are not determined on the diagonal $w_i=w_j$, where the claimed equilibrium sits.
• The appendix lemmas are stated for $a=b=1$, $c=0$, as printed; the normalization milestone carries them to general parameters.

Bargaining units and their solution concepts are reusable for any contract-parametrized bilateral negotiation. Contributions are welcome at any milestone, and alternative proofs of the uniqueness in Proposition 2 that avoid the full closed forms are of interest.

Selected references

• Q. Feng, Y. Li, J. G. Shanthikumar, Negotiations in Competing Supply Chains: The Kalai-Smorodinsky Bargaining Solution, Management Science, 2022. https://doi.org/10.1287/mnsc.2021.4184. Accepted manuscript: https://ssrn.com/abstract=3447674
• E. Kalai, M. Smorodinsky, Other solutions to Nash's bargaining problem, Econometrica 43(3), 1975. https://doi.org/10.2307/1914280
• J. F. Nash, The bargaining problem, Econometrica 18(2), 1950. https://doi.org/10.2307/1907266
• K. Binmore, A. Rubinstein, A. Wolinsky, The Nash bargaining solution in economic modelling, RAND Journal of Economics 17(2), 1986. https://doi.org/10.2307/2555382
• C. Davidson, Multiunit bargaining in oligopolistic industries, Journal of Labor Economics 6(3), 1988. https://doi.org/10.1086/298189
• Q. Feng, L. X. Lu, Supply chain contracting under competition: Bilateral bargaining vs. Stackelberg, Production and Operations Management 22(3), 2013. https://doi.org/10.1111/j.1937-5956.2012.01417.x

Why link choices in a PageRank network are worth studying

PageRank centrality (Brin–Page 1998) scores the nodes of a directed graph by the long-run frequency with which a random surfer visits them. In citation networks, the Web and social networks, each node controls where its own out-links point and has an interest in being visible. Earlier work asked how adding a link changes PageRank (Avrachenkov–Litvak 2006) and which outlinks of a single node maximize its score (de Kerchove–Ninove–Van Dooren 2008).

Catalano, Castaldo, Como and Fagnani turn the question into a network formation game in the line of Bala–Goyal 2000: all nodes choose at once, each with a fixed budget of out-links, and each seeks to maximize its own centrality. This mission formalizes the paper's structural result on best responses and the hitting-time machinery behind it.

The centrality game

Let $\mathcal V$ be a finite set of $n$ nodes. A graph is a directed graph on $\mathcal V$ with no self-loops and no sinks, with out-neighbourhoods $\mathcal N_i$ and out-degrees $d_i=|\mathcal N_i|\ge 1$. Its normalized adjacency matrix $R$ has $R_{ij}=1/d_i$ for $j\in\mathcal N_i$ and $0$ otherwise. For a discount factor $\beta\in(0,1)$ and an intrinsic centrality $\eta$, a probability vector with positive entries, the PageRank vector is

$$\pi=(1-\beta)(I-\beta R^\top)^{-1}\eta.$$

It is the stationary distribution of the chain $P=\beta R+(1-\beta)\mathbf 1\eta^\top$: from $j$, follow a uniform out-link with probability $\beta$, otherwise jump according to $\eta$. Let $T_i=\min\{t\ge 0:V_t=i\}$ and let $\tau^i_j=\mathbb E[T_i:V_0=j]$ be the expected hitting time of $i$ from $j$.

A walk of length $l$ is a tuple $(r_0,\dots,r_l)$ of consecutive links; a path is a walk with no repeated node, except possibly $r_0=r_l$. The set $\mathcal N_i^{-l}$ collects the nodes with a walk of length at most $l$ to $i$, and $\mathcal N_i^{-\infty}=\bigcup_{l\ge 0}\mathcal N_i^{-l}$ collects all nodes reaching $i$. Both contain $i$. For distinct $i,j$, a cut-set between them is a set $\mathcal C\subseteq\mathcal V\setminus\{i,j\}$ that meets every path from $i$ to $j$.

In the centrality game, $\mathbf d\in\{1,\dots,n-1\}^{\mathcal V}$ is given, an action of player $i$ is a set $x_i\subseteq\mathcal V\setminus\{i\}$ of size $d_i$, and a configuration $x$ determines the graph $\mathcal G(x)$ with $\mathcal N_i=x_i$. The utility of $i$ is $u_i(x)=\pi_i(x)$, and the best response set is

$$\mathcal B_i(x_{-i})=\{a\in\mathcal A_i\mid u_i(a,x_{-i})\ge u_i(b,x_{-i}),\ \forall b\in\mathcal A_i\}.$$

Formalization targets

Goal: Theorem 1

For every player $i$ and profile $x_{-i}$:

$$\text{(i)}\quad\mathcal B_i(x_{-i})\text{ does not depend on }\eta;$$ $$\text{(ii)}\quad|\mathcal N_i^{-\infty}|>d_i,\ x_i\in\mathcal B_i(x_{-i})\implies x_i\subseteq\mathcal N_i^{-d_i}\setminus\{i\},$$

and from each $j\in x_i$ a path $(r_0=j,\dots,r_l=i)$ with $r_k\in x_i$ for $k<l$ along which $\tau^i_{r_0}>\tau^i_{r_1}>\dots>\tau^i_{r_l}=0$;

$$\text{(iii)}\quad|\mathcal N_i^{-\infty}|\le d_i\implies\big(x_i\in\mathcal B_i(x_{-i})\iff x_i\supseteq\mathcal N_i^{-d_i}\setminus\{i\}\big).$$

Milestones

In proof order:

1. First-step system (4): $(\tau^i_j)_j$ is the unique solution of $\tau^i_i=0$, $\tau^i_j=1+(1-\beta)\sum_k\eta_k\tau^i_k+\frac{\beta}{d_j}\sum_{k\in\mathcal N_j}\tau^i_k$ for $j\ne i$.
2. Lemma 1: $\pi_i=\big(1+(1-\beta)\tau^i_\eta+\frac{\beta}{d_i}\sum_{j\in\mathcal N_i}\tau^i_j\big)^{-1}$, with $\tau^i_\eta=\sum_j\eta_j\tau^i_j$.
3. Proposition 2: $x_i$ is a best response iff $\tau^i_k\ge\max_{j\in x_i}\tau^i_j$ for every $k\notin x_i$, $k\ne i$.
4. Proposition 3(i): the relative order of $\{\tau^i_j\}_j$ does not depend on $\eta$.
5. Proposition 3(iii): nodes outside $\mathcal N_i^{-\infty}$ share one hitting time, strictly above that of every node in $\mathcal N_i^{-\infty}$.
6. Proposition 3(iv): for $k\in\mathcal N_i^{-\infty}$ and a cut-set $\mathcal C$ between $k$ and $i$, $\tau^i_k>\min_{j\in\mathcal C}\tau^i_j$.

Significance

Theorem 1 removes $\eta$ from the analysis of best responses, and therefore from the set of Nash equilibria. It also shows that rational wiring is local: when enough nodes reach $i$, a best response stays within incoming distance $d_i$ and is connected to $i$ through its own targets. In the paper, the theorem underlies the necessary conditions on equilibria and the classification for out-degrees $1$ and $2$.

The published proofs are on paper only. As of this writing no machine-checked version of these results is known, and the platform holds no statement of them. A completed mission adds PageRank, its chain, the hitting-time linear system for a positive restart distribution, and a Kac-type formula for PageRank.

Difficulty

Hitting times depend on the rest of the graph, on $\beta$ and on $\eta$, and comparing them across nodes has no closed form. The natural idea of comparing shortest-path distances to $i$ fails: expected hitting time is not monotone in graph distance, and the walk's restarts make every node reach every other in the chain. The result rests on the first-step system alone, so the difficulty is finding the inequalities that survive for every graph, every $\beta$ and every $\eta$, and handling nodes that cannot reach $i$ through links although the chain still reaches them through restarts.

On the formal side, the expected hitting time is a series of trajectory sums, and the step from it to the linear system (4) and to the inverse-matrix definition of PageRank is real work.

Formalization scope

• Graphs. $\mathcal V$ is a Fintype with DecidableEq; a graph is N : V → Finset V with IsGraph N (no self-loops, no sinks); a configuration x : V → Finset V is used directly as N.
• Walks. Tuples are Fin (l + 1) → V. reachWithin and reachSet are defined from walks and count $i$ as a member. Cut-sets follow the source's paths and require distinct endpoints.
• Hitting times. hittingTime is the published MarkovMixing.expSetHitTime of the chain at $\{i\}$, a tail sum $\sum_{t\ge0}\mathbb P_j(T_i>t)$, not the solution of (4); that link is a milestone. The time is counted from $t\ge 0$, so $\tau^i_i=0$.
• PageRank. pageRank uses Mathlib's matrix inverse. No invertibility or summability hypothesis appears: both follow from the setting.
• Best responses. bestResponse is defined from utilities through Function.update x i a, never from hitting times, so Proposition 2 is a theorem. Statements take a full configuration $x$; the sets and times do not depend on $x_i$.
• Corrections. $\eta$ has positive entries. The source's $\mathbb R^{\mathcal V}_+$ read as nonnegative makes Theorem 1 false, while the source asserts irreducibility of $P$, which needs positivity. Proposition 2 excludes $k=i$. Each item lists its differences from the source.

Encoding $\tau$ as the solution of (4), or $\mathcal B_i$ as the actions with smallest hitting times, would make milestones true by definition and is ruled out.

Reusable parts are the PageRank chain and its hitting-time system. Contributions welcome: proofs of any milestone, the geometric bound on hitting tails, and a stationarity lemma for $\pi$ under $P$.

Selected references

• C. Catalano, M. Castaldo, G. Como, F. Fagnani, On a Network Centrality Maximization Game, Mathematics of Operations Research, 2025; preprint v3 cited here. https://arxiv.org/abs/2211.03685
• S. Brin, L. Page, The anatomy of a large-scale hypertextual Web search engine, Computer Networks and ISDN Systems 30, 1998. https://doi.org/10.1016/S0169-7552(98)00110-X
• K. Avrachenkov, N. Litvak, The effect of new links on Google PageRank, Stochastic Models 22(2), 2006. https://doi.org/10.1080/15326340600649052
• C. de Kerchove, L. Ninove, P. Van Dooren, Maximizing PageRank via outlinks, Linear Algebra and its Applications 429(5–6), 2008. https://doi.org/10.1016/j.laa.2008.01.023
• V. Bala, S. Goyal, A noncooperative model of network formation, Econometrica 68(5), 2000. https://doi.org/10.1111/1468-0262.00155
• J. R. Norris, Markov Chains, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511810633

Motivation

Subgradient methods are the basic tool for minimizing a nonsmooth function $f:\mathbb R^d\to\mathbb R$ from first-order information alone. At a sharp minimum, where $f$ grows at least linearly away from its solution set, the Polyak step $x^+=x-\frac{f(x)-f^*}{\|v\|^2}v$ converges linearly (Polyak 1969; in the convex and weakly convex settings, Davis, Drusvyatskiy, MacPhee, Paquette 2018). Linear is the best a single subgradient step can do in general. Newton-type methods for nonsmooth equations reach superlinear rates, but they need a semismooth structure (Mifflin 1977) and an equation to solve.

Charisopoulos and Davis (arXiv:2201.04611, published in Mathematics of Operations Research, 2024) show that first-order information suffices. Their PolyakBundle step collects up to $d$ Polyak-type linearizations of $f$ around the current point and solves them jointly with a pseudoinverse. Under sharpness and a uniform semismoothness condition the gap $f-f^*$ improves superlinearly in a single step. The setting covers nonconvex problems such as low-rank matrix sensing, nonlinear root finding and feasibility problems for semialgebraic sets.

Setting

Fix $f:\mathbb R^d\to\mathbb R$, locally Lipschitz, with solution set $X^*=\operatorname{argmin}f\neq\emptyset$ and optimal value $f^*$. Fix $\bar x\in X^*$ and $\delta>0$. Write $B_\varepsilon(x)$ for the open ball, $\operatorname{dist}(x,X)=\inf_{y\in X}\|y-x\|$, and $P_X(x)$ for the set of nearest points of $X$ to $x$.

• (A1) Sharpness. For some $\mu>0$, $f(x)-f^*\ge\mu\operatorname{dist}(x,X^*)$ for all $x\in B_\delta(\bar x)$.
• (A2) $(b)$-regularity. A nonempty-valued, locally bounded set-valued map $g:\mathbb R^d\rightrightarrows\mathbb R^d$ (the generalized gradient) and constants $C_{(b)},\eta>0$ satisfy

$$|f(x)+\langle v,y-x\rangle-f^*|\le C_{(b)}\|y-x\|^{1+\eta}$$

for all $x\in B_\delta(\bar x)$, $v\in g(x)$ and $y\in X^*\cap B_{2\delta}(\bar x)$.

• The constant $L$ bounds $\|v\|$ over $g(B_\delta(\bar x))$ and is a Lipschitz constant of $f$ on $B_\delta(\bar x)$.

PolyakBundle$(x,\tau)$ (Algorithm 2) sets $y_0=x$ and picks $v_0\in g(y_0)$. For $i=1,\dots,d$ it sets

$$y_i=y_0-A_i^\dagger\big[f(y_j)-f^*+\langle v_j,y_0-y_j\rangle\big]_{j=0}^{i-1},\qquad A_i=[v_0^\top;\dots;v_{i-1}^\top],$$

and picks $v_i\in g(y_i)$. Here $A_i^\dagger$ is the Moore–Penrose pseudoinverse: $y_i$ is the point closest to $y_0$ satisfying the $i$ linearized equations $f(y_j)-f^*+\langle v_j,y-y_j\rangle=0$. The step returns $\tilde x=y_s$, where $s$ minimizes $f(y_i)$ over the indices with $\|y_i-y_0\|\le\tau(f(y_0)-f^*)$. The choices of $v_i\in g(y_i)$ and of the minimizing index are arbitrary.

Formalization targets

Goal: Theorem 2.2 (Superlinear Improvement)

There is $C_s>0$ such that for every $\tau>3/\mu$ and every $x$ with $\|x-\bar x\|<\delta/4$ and $\operatorname{dist}(x,X^*)\le\min\{(\mu/2C_{(b)})^{1/\eta},(\mu^{1-\eta}/LC_s)^{1/\eta}\}$, every output of PolyakBundle$(x,\tau)$ satisfies

$$f(\tilde x)-f^*\le C_s\,(f(x)-f^*)^{1+\eta}.$$

The constant $C_s$ is existential. The paper's proof gives $C_s=O(d\max\{L/\mu,L\}(8\sqrt2L/\mu)^d)$, and the goal does not fix it.

Milestones

1. Lemma 4.1: nearest points of $X^*$ to $x\in B_{\delta'}(y)$ lie in $B_{2\delta'}(y)$.
2. Lemma 4.2 (Aiming): $\langle v,x-\hat x\rangle\ge\frac\mu2\operatorname{dist}(x,X^*)$ near $\bar x$, so $\|v\|\ge\mu/2$ off $X^*$.
3. Lemma A.2: appending a row $v^\top$ with $\|P_{\ker A}v\|>\alpha$ gives $\sigma_{k+1}\ge\frac{\alpha}{\sqrt2}\min\{1,\sigma_k(A)/L\}$.
4. Proposition 4.1: under the same condition at every step, $\operatorname{rank}(A_{i+1})=i+1$ and $\sigma_{i+1}(A_{i+1})\ge\min\{\|v_0\|,1\}(\alpha/L\sqrt2)^i$.
5. Lemma 4.5: the decomposition of $y_i-\hat y_0$ into a $\ker(A_i)$ part and a pseudoinverse part.
6. Lemma 4.6 (Distance reduction).
7. Claim 1 in the proof of Lemma 4.7.
8. Lemma 4.7 (Alternatives): either the invariants (19) persist and the rank grows, or $y_{i+1}$ is already superlinearly close to $X^*$.

Significance

Theorem 2.2 is the engine of the paper's SuperPolyak method (Theorem 2.4). That method interleaves PolyakBundle with a linearly convergent fallback such as PolyakSGM, and it converges locally superlinearly; each bundle step costs at most $d+1$ evaluations of $g$ and $d$ pseudoinverse solves. Unlike Newton-type methods it needs no Hessian-like object and no equation structure, and the theorem applies to nonconvex $f$ with non-isolated minimizers.

The result is proved in the paper, and no part of it has been machine-checked. A formalization has to make several conventions of the proof precise that the printed text leaves loose. These are the convention $f^*=0$, the indexing of the bundle matrices, and the role of the arbitrary choices in the algorithm. It also has to correct two statements. Lemma 4.2 holds on the open ball only, and Item 1 of Lemma 4.7 needs the iterates to lie off $X^*$. The singular-value estimate of Lemma A.2 rests on Weyl's inequality and a Davis–Kahan angle bound, and both are independent linear-algebra contributions.

Difficulty

The obvious argument would bound $\|y_i-\hat y_i\|$ for each $i$ directly by $(b)$-regularity. This fails because the pseudoinverse $A_i^\dagger$ can have arbitrarily large norm when the generalized gradients are nearly dependent. The proof instead runs an induction with a lemma of alternatives (Lemma 4.7). Either the newest gradient has a component of size at least $\mu/8$ outside the span of the previous ones, in which case Proposition 4.1 keeps $\|A_{i+1}^\dagger\|$ bounded and the rank grows, or the iterate already improves superlinearly. Since the rank cannot exceed $d$, the second alternative must occur. Each step must also keep the iterates inside the balls where (A1) and (A2) hold.

On the linear-algebra side, Lemma A.2 needs a lower bound on the smallest nonzero singular value after a rank-one row update. Mathlib has singular values but neither Weyl's inequality for them nor a Davis–Kahan theorem.

Formalization scope

• Space and objects. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), and $f^*$ is written $f(\bar x)$ with $\bar x\in X^*$ as a hypothesis. $\operatorname{dist}$ is Metric.infDist, and $P_X(x)$ is a set of nearest points.
• The generalized gradient. $g$ is an arbitrary map E → Set E, not the Clarke subdifferential.
• Gaps. The paper's $f(\cdot)$ in (9), in the return radius and in §4.2 is the gap $f(\cdot)-f^*$.
• The algorithm. A run is a pair of sequences constrained at indices $0,\dots,d$, and an output is any minimizing index of any run. The goal is stated for every output, never for one selection.
• Bundle matrices. $A_i$ has rows $v_0,\dots,v_{i-1}$, and $A_0$ is empty with $\ker A_0=\mathbb R^d$.
• Pseudoinverse. $A^\dagger$ is defined from the published predicate VectorSpaceOpt.IsPseudoinverse (minimum-norm least squares), whose existence and uniqueness is the Proved platform theorem VectorSpaceOpt.pseudoinverse_exists_unique.
• Singular values and norms. $\sigma_k$ is Mathlib's 0-indexed LinearMap.singularValues (k-1), and $\|\cdot\|_2$ is the operator norm.
• Excluded trivializations. The goal is not vacuous: a run and an output exist from every starting point, and the hypotheses are satisfied by $f=|\cdot|$ on $\mathbb R$ with $g=\operatorname{sign}$. The constant $C_s$ is chosen before $\tau$ and $x$.

Reusable beyond this mission are the PolyakBundle run predicate, the pseudoinverse operator, and the singular-value estimate of Lemma A.2 (an incremental rank-growth bound for matrices). Proofs of Lemma A.2 via Weyl's inequality for singular values and of the projection identities $I-A^\dagger A=P_{\ker A}$ are welcome as separate contributions.

Selected references

• V. Charisopoulos, D. Davis, A superlinearly convergent subgradient method for sharp semismooth problems, arXiv:2201.04611v1, 2022; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2201.04611
• B. T. Polyak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9(3), 1969. https://doi.org/10.1016/0041-5553(69)90061-5
• D. Davis, D. Drusvyatskiy, K. J. MacPhee, C. Paquette, Subgradient methods for sharp weakly convex functions, Journal of Optimization Theory and Applications 179, 2018. https://arxiv.org/abs/1803.02461
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM Journal on Control and Optimization 15(6), 1977. https://doi.org/10.1137/0315061
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM Journal on Numerical Analysis 7(1), 1970. https://doi.org/10.1137/0707001

Motivation

A seller has $k$ identical units and faces $n$ buyers who arrive one at a time. Each buyer's value is drawn independently from a known distribution, but the arrival order is adversarial and unknown. The simplest selling policy posts one static price to every buyer until the units run out. Prophet inequalities compare such a policy with a prophet who sees all values in advance and allocates the units to the $k$ highest. For $k=1$, Samuel-Cahn (1984) showed that a single threshold earns half of the prophet's expected value. For large supply static pricing should do much better, since selling many units averages out the randomness. Chawla, Devanur and Lykouris (arXiv:2007.07990v4, Operations Research 2024) give the exact worst-case ratio of a natural static pricing scheme for every $k$. Posted prices are anonymous, non-adaptive and order-oblivious, which is why they are used in revenue management and online marketplaces.

Timeline:

• 1984: Samuel-Cahn, ratio $1/2$ for $k=1$ with a median threshold.
• 2010: Chawla, Hartline, Malec and Sivan, ratio $1/2$ for $k$ units via thresholds.
• 2020 (arXiv v1): this paper, ratio $\phi_k$ for every $k$, with $\phi_k=1-O(\sqrt{\log k/k})$.
• 2022: Arnosti and Ma extend the analysis to random-order arrivals, and Jiang, Ma and Zhang show $\phi_k$ is tight for static prices.

Setting

An instance is a list of $n$ distributions $F_1,\dots,F_n$ on $[0,\infty)$; buyer $t$ is the $t$-th to arrive, and her value $v_t$ is drawn independently from $F_t$. At a price $p$, buyer $t$ buys iff $v_t\ge p$ and fewer than $k$ earlier buyers bought. $\mathrm{Welfare}(p,k,\mathcal F)$ is the expected total value of the buyers who buy. $\mathrm{Opt}(k,\mathcal F)=\mathbb E[\max_{|S|\le k}\sum_{t\in S}v_t]$ is the expected sum of the $k$ highest values.

Let $X_p=|\{t: v_t\ge p\}|$ and define

$$\delta_k(X)=\mathbb P[X\le k-1],\qquad \mu_k(X)=\tfrac1k\,\mathbb E[\min\{X,k\}].$$

$\delta_k(X_p)$ is the probability that the units do not sell out, and $\mu_k(X_p)$ is the expected fraction sold. The pricing scheme $\boldsymbol\pi$ posts a price $\pi$ with $\delta_k(X_\pi)=\mu_k(X_\pi)$ (3.3). For a Poisson variable $X^\lambda$, the rate $\lambda_k$ solves $\delta_k(X^{\lambda_k})=\mu_k(X^{\lambda_k})$ (1.1), and $\phi_k:=\delta_k(X^{\lambda_k})$.

Formalization targets

Goal: Theorem 1

For every $k\ge1$: the rate $\lambda_k$ exists and is unique; every atomless instance with $n>k$ has a balancing price; and for every instance and every price $p$ with $\delta_k(X_p)=\mu_k(X_p)$,

$$\phi_k\cdot\mathrm{Opt}(k,\mathcal F)\ \le\ \mathrm{Welfare}(p,k,\mathcal F).$$

The constant is not hard-coded. $\phi_k$ is defined by (1.1), with $\phi_1=1/2$, $\phi_2\approx0.585$, $\phi_3\approx0.630$.

Milestones

1. Eq. (1.1): $\mu_k(X^\lambda)$ increases strictly from $0$ to $1$ and $\delta_k(X^\lambda)$ decreases strictly from $1$ to $0$, so $\lambda_k$ is unique.
2. §3, (3.3): monotonicity, endpoint values and continuity of $p\mapsto\delta_k(X_p),\mu_k(X_p)$, and existence of $\pi$.
3. Eq. (4.1): $\mathrm{Opt}\le kp+\sum_t\mathbb E[\max(0,v_t-p)]$.
4. Eq. (4.3): $\mathrm{Utility}\ge\delta_k(X_p)\sum_t\mathbb E[\max(0,v_t-p)]$.
5. Lemma 1: $\mathrm{Welfare}\ge\min(\delta_k(X_p),\mu_k(X_p))\,\mathrm{Opt}$ for every price.
6. Lemma 3: for $n>k$ buyers, the worst ratio equals $\phi^\star_k(n)$, the value of (GenBern : $\min\phi$ s.t. $\delta=\mu=\phi$) over $n$ Bernoulli biases.
7. Lemma 4: (GenBern : $\min\mu$ s.t. $\delta=\phi$) has the same value.
8. Claim 1: with two free biases, that program is the (Min-Revenue) program.
9. Claim 3: the hyperbola $xy+a(x+y)=b$ meets $[0,1]^2$ in a convex or concave decreasing arc.
10. Claim 2: (Min-Revenue) has an optimum with $r_1=r_2$ or a boundary coordinate, and the optimum is unique and diagonal when $Q_2^2-Q_{\ge3}(Q_1-Q_2)>0$.
11. Lemma 5: some minimizer has equal non-degenerate biases.
12. Lemma 6: some minimizer has $n$ equal biases in $(0,1)$.
13. Lemma 7: $|\mu_k(\mathrm{Bin}(n,\lambda))-\mu_k(\mathrm{Bin}(n,\lambda'))|>(1-e^{-\varepsilon/2})/(2k)$ when $|\lambda-\lambda'|>\varepsilon$.
14. §5.4: the balanced equal-bias binomials decrease to $\phi_k$, and their means converge to $\lambda_k$.
15. Lemma 2: $\delta_k(X_\pi)\ge\phi_k$ for every balancing price, and $\phi_k$ is the infimum.

Significance

Theorem 1 gives the exact guarantee of the static pricing scheme for every supply, interpolating between $1/2$ at $k=1$ and $1$ as $k\to\infty$. Jiang, Ma and Zhang (2022) show that no static price does better in the worst case. The revenue–utility decomposition of Lemma 1 holds for every price and every arrival order. It underlies later work on random-order arrivals and on the ex-ante relaxation (Remark 2). The reduction to Poisson-binomial variables (Lemmas 3–6) is an extremal result in the line of Hoeffding (1956) on sums of independent Bernoullis, with an extra constraint.

The result has a published proof but no machine-checked one. This mission formalizes the paper's chain: the decomposition, the reduction to Bernoullis, the two-bias exchange argument and the Poisson limit. The printed proofs contain slips, which the formalization must route around: the proof of Lemma 7 truncates at $k-1$ and asserts $\mathbb P[X\le k-1]\ge1/2$; footnotes 4 and 5 and the $Q_1$ formula of Lemma 6 need repair; the proof of Claim 3 writes $\sqrt{a^2-b}$ for $\sqrt{a^2+b}$. Alternative proofs of Lemma 2 are welcome.

Difficulty

Lemma 1 is close to Samuel-Cahn's argument. The difficulty is Lemma 2. The worst case over all instances is not a compact optimization: the extremal value is reached only in the limit of infinitely many buyers. The obvious step is to fix $n$ and minimize over biases, but the minimizer at fixed $n$ is not unique when $k=1$, and the claim that equal biases are optimal fails for constraint values other than $\phi^\star_k(n)$. Passing to the limit then needs the means $n c_n$ to converge, which does not follow from the convergence of $\delta_n$. Lemma 7 supplies a quantitative separation, and its printed proof is flawed.

Formalization scope

Buyers are Fin n in arrival order. An instance is F : Fin n → Measure ℝ of probability measures with F t (Set.Iio 0) = 0, and values are drawn from Measure.pi F. A buyer buys iff $v_t\ge p$ and $\#\{s<t: v_s\ge p\}<k$. Welfare and Opt are lower integrals in $[0,\infty]$, and the ratio is a product inequality, so no finite-mean assumption is made and $\mathrm{Opt}=\infty$ is covered. Theorem 1's bound clause allows atoms and every balancing price. Its existence clauses keep it from holding vacuously. $\phi^\star_k(n)$ depends on $n$, and Lemmas 4–6 use the same $n$. Poisson quantities are explicit series at rate $\lambda\in\mathbb R_{\ge0}$, and Poisson-binomial ones use the published pmf CommitteeVoting.SingleVoter.pbPMF. A statement with a fixed $k$, a fixed $n$ or i.i.d. buyers, or with $\phi_k$ replaced by a number, is not the theorem.

A complete development needs:

• product-measure computations for Poisson-binomial laws;
• the Poisson limit theorem (on the platform as FamousTheorems.poisson_limit);
• monotonicity of truncated Poisson expectations;
• a two-variable optimization argument.

The Poisson-binomial and Poisson lemmas are reusable beyond this mission.

Selected references

• S. Chawla, N. R. Devanur, T. Lykouris, Static pricing for multi-unit prophet inequalities, arXiv:2007.07990v4, 2023; Operations Research, 2024. https://arxiv.org/abs/2007.07990
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4), 1984. https://doi.org/10.1214/aop/1176993150
• S. Chawla, J. D. Hartline, D. L. Malec, B. Sivan, Multi-parameter mechanism design and sequential posted pricing, STOC 2010 (arXiv title: Sequential posted pricing and multi-parameter mechanism design). https://arxiv.org/abs/0907.2435
• W. Hoeffding, On the distribution of the number of successes in independent trials, Annals of Mathematical Statistics 27(3), 1956. https://doi.org/10.1214/aoms/1177728169
• N. Arnosti, W. Ma, Tight guarantees for static threshold policies in the prophet secretary problem, Operations Research, 2022. https://arxiv.org/abs/2108.12893
• J. Jiang, W. Ma, J. Zhang, Tightness without counterexamples: a new approach and new results for prophet inequalities, arXiv:2205.00588, 2022. https://arxiv.org/abs/2205.00588