All missions

Motivation

A retailer choosing which products to offer (an assortment) must predict how customers substitute between products. Discrete choice models make this prediction, and the paired combinatorial logit (PCL) model is a generalization of the multinomial and nested logit models in which every pair of products forms a nest, so that the correlation between the utilities of any two products can be set separately. Assortment optimization under the PCL model is NP-hard even without constraints, and practical instances carry constraints on the number of products displayed.

R. Ghuge, J. Kwon, V. Nagarajan and A. Sharma (Oper. Res. 70(2):786–804, 2022) reduce PCL assortment optimization to the maximum directed cut problem and obtain constant-factor approximation algorithms under cardinality, knapsack and matroid constraints.

Timeline.

• Ageev, Hassin and Sviridenko (2001): a 0.5-approximation for max-dicut with a cardinality constraint, by pipage rounding of the half-integral LP relaxation.
• Zhang, Rusmevichientong and Topaloglu (2020): an LP-based fixed-point framework for PCL assortment optimization, with a 0.25-approximation under a cardinality constraint.
• Ghuge, Kwon, Nagarajan and Sharma (2022): the reduction to max-dicut, and a 0.5-approximation for the cardinality-constrained problem (Theorem 6), the result formalized here.

Setting

There are $n$ products $[n]=\{1,\dots,n\}$. Product $i$ has revenue $r_i\ge0$ and preference weight $v_i\ge0$, and $v_0>0$ is the weight of not buying. Each ordered pair $(i,j)$, $i\ne j$, is a nest with dissimilarity parameter $\gamma_{ij}\in(0,1]$. An assortment is $x\in\{0,1\}^n$ (in Lean, a Finset (Fin n)). With $V_{ij}(x)=v_i^{1/\gamma_{ij}}x_i+v_j^{1/\gamma_{ij}}x_j$ and $R_{ij}(x)=(r_iv_i^{1/\gamma_{ij}}x_i+r_jv_j^{1/\gamma_{ij}}x_j)/V_{ij}(x)$, the expected revenue is

$$\pi(x)=\frac{\sum_{(i,j)}V_{ij}(x)^{\gamma_{ij}}R_{ij}(x)}{v_0+\sum_{(k,l)}V_{kl}(x)^{\gamma_{kl}}},$$

and $z^*=\max\{\pi(x): \sum_ix_i\le c\}$ is the optimal revenue under the cardinality constraint $c$.

The ratio is linearized by $h_z(x)=\sum_{(i,j)}V_{ij}(x)^{\gamma_{ij}}(R_{ij}(x)-z)$: $\pi(x)\ge z$ if and only if $h_z(x)\ge v_0z$. The reduction graph $G_z$ has a vertex for each product and a dummy vertex $n+1$, edges $(i,j)$ and $(i,n+1)$, and explicit weights $w_{ij}(z)$, affine in $z$, such that $h_z(\mathbf 1_S)$ is the weight of the edges leaving $S$ (pclWeight, pclEdges). $\tilde G_z$ keeps the edges of nonnegative weight.

For a digraph $(V,E)$ with weights $w$, sizes $s$ and capacity $c$, the LP (9) is

$$\max\sum_{(i,j)\in E}w_{ij}y_{ij}\quad\text{s.t.}\quad y_{ij}\le x_i,\ y_{ij}\le1-x_j,\ x_i\le1,\ \textstyle\sum_is_ix_i\le c,\ x,y\ge0,$$

and LP$(z)$ is this LP on $G_z$ with $x_{n+1}=0$; its value $g(z)$ is an upper bound on $\max_x h_z(x)$. Algorithm 1 takes an optimal basic solution of (9), possibly shifts it along the coordinates equal to $\delta$ and $1-\delta$, applies pipage rounding (repeatedly moving mass between two fractional coordinates in the direction that does not decrease $F(x)=\sum w_{ij}x_i(1-x_j)$), and outputs the better of the rounded set and that set plus the last fractional vertex.

Formalization targets

Goal: Theorem 6

For every finite loopless digraph with $w\ge0$, every $c\in\mathbb N$ and unit sizes, and every optimal basic solution of LP (9) with value $LP^*$, Algorithm 1 has an output, and every output $T$ satisfies

$$|T|\le c,\qquad \mathrm{cut}(T)\ge 0.5\cdot LP^*.$$

For every PCL instance and $c\in\mathbb N$, $g(\cdot)/v_0$ has a fixed point $\hat z$; Algorithm 1 run on $\tilde G_{\hat z}$ has an output; and for every output $T$ the assortment $S=\{i: i\in T,\ r_i\ge\hat z\}$ satisfies

$$|S|\le c,\qquad \pi(S)\ge 0.5\cdot z^*.$$

Milestones

• Reduction: Lemma 1 ($h_z$ is a cut function), Lemma 2 (sign structure, corrected), Lemmas 5 and 6 (the integer programs IP$_1(z)$, IP$_2(z)$ and max-dicut on $G_z$, $\tilde G_z$).
• Framework: Theorem 2 ($\pi(\hat x)\ge\alpha\hat z\ge\alpha z^*$), Lemma 7, Observation 1, Lemmas 8 and 9 (the fixed point of $g(\cdot)/v_0$ through the LP (D)).
• Rounding: Theorem 4 (pipage rounding with a knapsack constraint), Theorem 5 (basic solutions of (9) take values in $\{0,\delta,\frac12,1-\delta,1\}$), Lemmas 10–12 (the shift $x'$ and the two cases of the 0.5 bound).

Significance

The theorem doubles the best previous factor (0.25) for cardinality-constrained PCL assortment optimization and carries the factor 0.5 of Ageev et al. (2001) for cardinality-constrained max-dicut over to assortment optimization (Table 1 of the paper). The reduction of Lemma 1 is reusable: any LP-based approximation for constrained max-dicut with nonnegative weights becomes an approximation for PCL assortment optimization through the framework of Theorem 2. Theorem 5 extends the half-integrality of Ageev et al. from cardinality to general knapsack constraints, and is also the basis of the paper's knapsack results (Theorem 7 and the $(0.5-\epsilon)$-approximation of §5).

The proofs of most of these statements are in the online appendices of the paper. None of the results has a machine-checked proof; this mission produces the first, together with Lean statements of the PCL model, the max-dicut LP and pipage rounding.

Difficulty

The ratio objective $\pi$ is neither submodular nor linear, and the reduction graph has negative edge weights, so max-dicut algorithms do not apply directly; Lemmas 2, 6 and 7 are what allow deleting the negative edges. The main obstacle is Theorem 5: the knapsack constraint destroys the half-integrality of the max-dicut polytope, and the proof must show that a single extra value $\delta$ (and $1-\delta$) suffices for every extreme point. Pipage rounding alone does not give the 0.5 bound at such points; the shift $x'$ of equation (10) and the case analysis of Lemma 11 are needed, and the bound is tight there.

Formalization scope

Products are Fin n; the vertices of $G_z$ are Option (Fin n) with none the dummy. Real powers are Real.rpow, and $\gamma_{ij}>0$ is part of PCLInstance, so that empty nests contribute $0$ (Lean's $0/0=0$). Optimal values over finite families are suprema over finite nonempty sets; $g(z)$ is an sSup over a nonempty polytope. "Basic feasible solution" is Set.extremePoints of the feasible set of (9) in the joint $(x,y)$ space, with $y$ fixed to $0$ off $E$. Algorithm 1 and pipage rounding are relations: every nondeterministic choice is quantified, the goal asserts that an output exists and that every output satisfies the bound, and running time is not formalized. For the PCL part, Algorithm 1 runs on $\tilde G_{\hat z}$ with all $n+1$ vertices of size $1$, and the output is intersected with $\{r_i\ge\hat z\}$.

The statement "some assortment with at most $c$ products earns at least $z^*/2$" is trivially true (take the optimum) and is not the theorem; the goal is about the outputs of Algorithm 1. Lemma 2 is corrected: its first clause holds with "nonpositive", not "negative".

A complete development needs LP duality and the existence of optimal extreme points for bounded polyhedra, the extreme-point analysis of Theorem 5, and the termination of pipage rounding. The max-dicut LP and pipage rounding definitions do not depend on the PCL model and can be reused for other rounding results. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

• R. Ghuge, J. Kwon, V. Nagarajan, A. Sharma, Constrained Assortment Optimization Under the Paired Combinatorial Logit Model, Operations Research 70(2):786–804, 2022. https://doi.org/10.1287/opre.2021.2188
• H. Zhang, P. Rusmevichientong, H. Topaloglu, Assortment Optimization Under the Paired Combinatorial Logit Model, Operations Research 68(3):741–761, 2020. https://doi.org/10.1287/opre.2019.1930
• A. Ageev, R. Hassin, M. Sviridenko, A 0.5-Approximation Algorithm for MAX DICUT with Given Sizes of Parts, SIAM Journal on Discrete Mathematics 14(2):246–255, 2001. https://doi.org/10.1137/S089548010036813X
• A. Ageev, M. Sviridenko, Approximation Algorithms for Maximum Coverage and Max Cut with Given Sizes of Parts, IPCO 1999, LNCS 1610:17–30. https://doi.org/10.1007/3-540-48777-8_2

Learning in games without knowing the curvature

When several agents repeatedly choose actions and pay costs that depend on everyone's choices, each agent faces an online learning problem whose environment is the other agents. Online gradient descent (OGD) is the standard learner in this setting. It is doubly optimal under strong convexity: a single agent facing arbitrary strongly convex costs has $\Theta(\log T)$ regret, and when every agent of a strongly monotone game runs it, the joint action converges in the last iterate to the Nash equilibrium at rate $\Theta(1/T)$ (Zhou et al. 2021, as summarized in Jordan, Lin and Zhou, Theorem 3.5). Both guarantees need the strong monotonicity modulus $\beta$ to set the step size $\eta^{t+1}=\beta(t+1)$, and in a game no agent knows $\beta$.

Jordan, Lin and Zhou remove this requirement with a randomized step size. Each agent draws independent geometric variables $M^t\sim\mathrm{Geometric}(p_0)$, $p_0=1/\log(T+10)$, and uses $\eta^{t+1}=(t+1)/\sqrt{1+\max\{M^1,\dots,M^t\}}$. Their Theorem 2.5 treats one agent and their Theorem 3.7, the target of this mission, treats the game.

Setting

A continuous game has agents $i\in\{1,\dots,N\}$, nonempty convex compact action sets $\mathcal X_i\subseteq\mathbb R^{d_i}$, the joint set $\mathcal X=\prod_i\mathcal X_i$ with the Euclidean norm $\|x\|^2=\sum_i\|x_i\|^2$, and costs $u_i:\mathcal X\to\mathbb R$ that are continuous and differentiable in the agent's own action. The gradient profile is $v(x)=(\nabla_{x_1}u_1(x),\dots,\nabla_{x_N}u_N(x))$, continuous on $\mathcal X$. The game is $\beta$-strongly monotone if $\langle x'-x,v(x')-v(x)\rangle\ge\beta\|x'-x\|^2$ on $\mathcal X$. A Nash equilibrium $x^\star\in\mathcal X$ is a profile from which no agent can lower its cost by a unilateral deviation. The diameter of $\mathcal X$ is at most $D$.

At round $t$ every agent observes a noisy gradient $\xi_i^t$ with $\mathbb E[\xi^t\mid x^t,\{\eta_i^s\}]=v(x^t)$ and $\mathbb E[\|\xi^t\|^2\mid x^t,\{\eta_i^s\}]\le G^2$, the conditioning being on the current joint action and all step sizes. MA-AdaOGD (Algorithm 3) then sets, for each agent independently,

$$\eta_i^{t+1}=\frac{t+1}{\sqrt{1+\max\{M_i^1,\dots,M_i^t\}}},\qquad x_i^{t+1}=\operatorname*{argmin}_{x_i\in\mathcal X_i}\Big\{(x_i-x_i^t)^\top\xi_i^t+\frac{\eta_i^{t+1}}2\|x_i-x_i^t\|^2\Big\},$$

with $\{M_i^t\}_{1\le i\le N,1\le t\le T}$ i.i.d. Geometric($p_0$) on $\{1,2,\dots\}$.

Formalization targets

Goal: Theorem 3.7 (p.16)

The game has a unique Nash equilibrium $x^\star$, and

$$\mathbb E\|x^T-x^\star\|^2\le\frac{D^2}{T}\Big(1+e^{\frac1{4\beta^2\log(T+10)}}\Big)\sqrt{1+\log(T+10)+\log(NT)\log(T+10)}+\frac{G^2}{T}\log(T+1)\big(1+\log(T+10)+\log(NT)\log(T+10)\big),$$

for every $N,T\ge1$, $\beta,G,D>0$. The constant is the paper's, stated in full; the $O(\log^3T/T)$ rate is its consequence.

Milestones

1. Strongly monotone games are individually convex (§3.1); Nash equilibria of individually convex games are the solutions of the variational inequality $(x-x^\star)^\top v(x^\star)\ge0$ (Proposition 3.4); a strongly monotone game has exactly one Nash equilibrium (§3.1).
2. Lemma 3.10: the descent inequality for $\sum_i\eta_i^T\,\mathbb E[\|x_i^T-x_i^\star\|^2\mid\{\eta_i^t\}]$.
3. Display (3.3): $\sum_{t=1}^{T-1}\max_i 1/\eta_i^{t+1}\le\log(T+1)\sqrt{1+\max_{i,t}M_i^t}$.
4. Display (3.4): $T\,\mathbb E\|x^T-x^\star\|^2\le D^2\,\mathrm I+G^2\log(T+1)\,\mathrm{II}+D^2\,\mathrm{III}$, with I, II, III expectations of functions of the draws.
5. Proposition A.1: $\sum_{n\ge1}\mathbb P(\bar X_n\le x)\le(1-p_0)^{-x}$ (A.1, corrected) and $1\le\mathbb E[\bar X_n]\le(1+\log n)/p_0$ (A.2) for the maximum $\bar X_n$ of $n$ i.i.d. geometric variables.
6. Displays (3.5) and (3.6): $\mathrm I\le\sqrt{1+\log(T+10)+\log(NT)\log(T+10)}$ and $\mathrm{II}\le1+\log(T+10)+\log(NT)\log(T+10)$.

Significance

The theorem gives a learning rule for games that is feasible: each agent uses only its own gradient feedback, the horizon $T$ and its own random draws, with no knowledge of $\beta$, $G$, $D$, $N$ or the other agents. Its last iterate converges to the Nash equilibrium at rate $O(\log^3T/T)$, within logarithmic factors of the $\Omega(1/T)$ lower bound for strongly convex optimization. With Theorem 2.5 it makes the same rule doubly optimal. The proof never uses that $v$ is a gradient profile, so the bound also covers stochastic strongly monotone variational inequalities (Corollary 3.11).

Nothing in this mission is formalized elsewhere: the platform has no continuous-game, strong-monotonicity-on-a-set or Nash-equilibrium layer of this kind, and no result on maxima of geometric variables. The game layer (Definitions 3.1–3.3, Proposition 3.4, existence and uniqueness of equilibria) is reusable by any mission on monotone games or variational inequalities.

Difficulty

The deterministic parts are short: the descent inequality follows from the optimality condition of the projection step, strong monotonicity and the variational inequality at $x^\star$. The difficulty is the expectation of the random step sizes. The paper bounds the third term III of (3.4) in display (3.7) by $e^{1/(4\beta^2\log(T+10))}\sqrt{1+\log(T+10)+\log(NT)\log(T+10)}$. That step is not valid as printed: it replaces a conditional expectation given the argmax agent by an unconditional one, uses a ratio bound that fails when one agent holds the overall maximum, and relies on (A.1), whose printed bound $e^{xp_0}$ is false. A Monte Carlo estimate of III exceeds the printed (3.7) for $N\approx10^6$. The paper's proof of Theorem 3.7 is therefore incomplete. No counterexample to Theorem 3.7 itself is known, and the goal is posed as printed. A proof needs a different bound on III, or a different route from Lemma 3.10 to the goal; (3.7) is deliberately not a milestone.

Existence of the Nash equilibrium needs a fixed-point or variational-inequality existence argument on a compact convex set, which Mathlib does not provide.

Formalization scope

Agents are Fin N, agent $i$'s space is EuclideanSpace ℝ (Fin (d i)), and the joint space is PiLp 2, so every norm and inner product is the Euclidean one of the product. Costs and gradients are total functions constrained on $\mathcal X$ only, and $v_i$ is a gradient within $\mathcal X_i$ (HasGradientWithinAt). The goal and the existence of equilibria take compact action sets, as on the paper's p.1; Definition 3.1 says "bounded", under which neither the argmin nor the equilibrium need exist. Lemma 3.10 and (3.4) assume a run and an equilibrium, so they need no compactness. The conditional moments of $\xi^t$ are taken given $x^t$ and all step sizes $\{\eta_i^s\}$, the conditioning written in the paper's Appendix D (p.40); the paper's p.13 writes $\mathbb E[\cdot\mid x^t]$ alone. Geometric variables live on $\{1,2,\dots\}$, and $\eta_i^1=1$. Expectations are Bochner integrals, and every bounded expectation comes with an integrability clause, so no bound holds because an integrand fails to be integrable.

Proposition A.1 (A.1) is posed with the bound $(1-p_0)^{-x}$ that the printed proof derives, in place of the false $e^{xp_0}$. Contributions are welcome at every level: the game layer, the probabilistic lemmas on geometric maxima, the descent lemma, and above all a valid bound on III.

Selected references

• M. I. Jordan, T. Lin, Z. Zhou, Adaptive, Doubly Optimal No-Regret Learning in Strongly Monotone and Exp-Concave Games with Gradient Feedback, arXiv:2310.14085v4, 2024; Operations Research, 2025. https://arxiv.org/abs/2310.14085v4
• Z. Zhou, P. Mertikopoulos, A. L. Moustakas, N. Bambos, P. Glynn, Robust Power Management via Learning and Game Design, Operations Research 69(1):331–345, 2021 (reference [Zhou et al., 2021] of the paper, https://arxiv.org/abs/2310.14085v4, p.35).
• G. Debreu, A Social Equilibrium Existence Theorem, PNAS 38(10), 1952. https://doi.org/10.1073/pnas.38.10.886
• F. Facchinei, J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2007. https://doi.org/10.1007/b97543
• J. B. Rosen, Existence and Uniqueness of Equilibrium Points for Concave N-Person Games, Econometrica 33(3), 1965. https://doi.org/10.2307/1911749

Motivation

Fair division of divisible items usually assumes that everything being shared is desirable. Many allocation problems also involve bads (chores): tasks, liabilities or emissions cuts that some or all participants would rather avoid. A mixed manna contains both. The competitive equilibrium is the standard fair and efficient solution concept for goods: it is envy-free when budgets are equal and Pareto optimal. For a mixed manna, Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya showed that competitive allocations still exist and keep these properties (Econometrica 2017). Their equilibrium set can be disconnected and is not given by a convex program, so computing an equilibrium is a real question.

Chaudhury, Garg, McGlaughlin and Mehta (arXiv:2008.02753, 2020; Mathematics of Operations Research, 2023) give a complementary pivot algorithm for exchange markets with a mixed manna under separable piecewise-linear concave utilities. Its correctness is the subject of this mission.

Timeline:

• 1965: Lemke's complementary pivoting algorithm for linear complementarity problems.
• 1976: Eaves computes exchange-market equilibria with linear utilities by Lemke's scheme.
• 2015: Garg, Mehta, Sohoni and Vazirani handle SPLC utilities for goods only.
• 2017: Bogomolnaia et al. prove that competitive allocations of a mixed manna exist.
• 2020: Chaudhury et al. give the first pivoting algorithm for a mixed manna. Their LCP admits secondary rays and a spurious solution, which earlier goods-only formulations did not.

Setting

There are finite sets $N$ of agents and $M$ of divisible items. Agent $i$ brings $W_{ij}\ge 0$ of item $j$, and each item has unit supply, $\sum_i W_{ij}=1$. Agent $i$ values item $j$ through a separable piecewise-linear concave (SPLC) function $u_{ij}$. Its segments $k=1,\dots,|u_{ij}|$ have strictly decreasing slopes $U_{ijk}$ and lengths $L_{ijk}$, and the last segment is infinite. Item $j$ is a good ($j\in M^+$) if some agent has $U_{ij1}>0$, and a bad ($j\in M^-$) otherwise. On a bad every slope is negative, with disutility $D_{ijk}=|U_{ijk}|>0$.

A competitive equilibrium is a price vector $p$ and an allocation $x$ such that each $x_i$ maximizes $u_i(y)=\sum_j u_{ij}(y_j)$ subject to $\sum_j y_jp_j=\sum_j W_{ij}p_j$, $y\ge 0$, and every item clears, $\sum_i x_{ij}=\sum_iW_{ij}$. Bads get negative prices, so agents earn money by taking chores. The paper assumes that the desire for each good exceeds 1, that each agent brings some good and some bad (Condition 1), and that the economy graph is strongly connected (Condition 2). In that graph, $a\to b$ when $a$ is non-satiated for a good that $b$ brings.

The algorithm works on the augmented LCP (14). Its variables are $(p,f,r,s,z)$: shifted prices $p$ (relative price $P-p_j$ for goods, $-(P-p_j)$ for bads), spendings $f_{ijk}$, agent variables $r_i$, supplementary prices $s_{ijk}$, and Lemke's scalar $z$. The parameters are $P>0$, a large $R$, coefficients $\delta_j\in(1,1+1/m)$ and last-segment length $1+\varepsilon$. Write $\mathcal P$ for the polyhedron of LCP (14). Algorithm 1 starts at the primary ray $S_0=(0,z_0)$ and walks from vertex to vertex of $\mathcal P$ along edges of the LCP's solution set, pivoting at the double label, until $z=0$. Every vertex with $z=0$, $p<P$, $r<R$ decodes to the equilibrium $p^*_j=\pm(P-p_j)$, $x^*_{ij}=\sum_kf_{ijk}/(P-p_j)$.

Formalization targets

Goal: Theorem 14

$$\text{nondegenerate }\mathcal P\text{ on }\{z>0,\ p<P,\ r<R\}\ \Longrightarrow\ \begin{cases}\text{some path of Algorithm 1 from }S_0\text{ reaches }z=0,\\ \text{every such path ends at }p<P,\ r<R,\text{ decoding to a competitive equilibrium,}\end{cases}$$

for every instance meeting the standing assumptions, every $P>0$, all sufficiently large $R$, every admissible $\delta$ and every $\varepsilon>0$.

Milestones

• Claim 1 and Lemma 15: properties of every LCP (14) solution. Final segments are never forced when $p<P$, and $p\le P$. Lemma 15 is stated in corrected form, because its printed clause $r\le R$ fails at some solutions.
• Lemmas 16–19: the path never reaches the boundary $p_j=P$ or $r_i=R$, and never reaches the degenerate solution $p=P$, $r=R$.
• Theorem 20: the path never enters a secondary ray.
• Lemmas 7 and 9: equilibria and the market-clearing system (11), and decoding an LCP (13) solution to an equilibrium. Lemma 7 is stated in corrected form: its first half needs the sign pattern of p.14 as a hypothesis, because the budget equality does not imply it.

Significance

Theorem 14 gives a constructive proof that competitive equilibria of a mixed manna exist under strong connectivity, and that a rational instance has a rational equilibrium (Theorem 21). It also places the problem in PPAD (Theorem 22) and gives an odd number of equilibria for nondegenerate instances (Theorem 23). Experiments in the paper find the algorithm practical. Unlike convex-programming methods, it applies to exchange (not only Fisher) markets with chores.

The result is proved in the paper but has not been formalized. A Lean development would check the delicate parts: the treatment of secondary rays and of the spurious degenerate solution, and the limiting arguments of Lemmas 16–18. The formalization already corrects three printed statements. Lemma 15's bound $r\le R$ fails at solutions where every bad has $p_j=P$; Lean checks a counterexample on the paper's Example 6. Lemma 7's first half fails for equilibria with the wrong sign pattern, which an equality budget admits. Lemma 16's printed conclusion "$p_{j'}<P$" contradicts its own proof and is read as "$p_{j'}=P$".

Difficulty

The obvious argument is the one that works for goods: Lemke's scheme follows a path, and the path ends either at a solution or on a secondary ray. For goods-only LCPs, copositivity-type arguments exclude secondary rays. Here secondary rays exist. Setting $p_j=P$ on any subset of bads, with everything else zero, gives one. The LCP also has a solution that is not an equilibrium. So the proof must track the path itself: it must show that the walk from the primary ray never sets any price to its bound. This uses the economy graph (Lemma 16) and limits along the last edge (Lemmas 17–18). The termination argument also depends on nondegeneracy away from $z=0$, while $z=0$ is inherently degenerate: summing the market-clearing rows gives an identity.

Formalization scope

Agents and items are finite types, and every quantity is real. Segments are indexed from 0. A segment of a good carries variables only if the agent's first slope on it is positive. The utility uses the infinite last segment, and the LCP uses length $1+\varepsilon$. The budget in the equilibrium definition is an equality, and prices are not normalized, so $(-p,x)$ is an equilibrium whenever $(p,x)$ is.

The printed hypothesis "U, W, L have no polynomial relationship" is undefined. Read as algebraic independence it never holds, since $\sum_iW_{ij}=1$, and the goal would be vacuous. It is therefore replaced by the conclusion of Theorem 11, which is all the proof uses: every vertex of $\mathcal P$ with $z>0$, $p<P$, $r<R$ is nondegenerate, meaning exactly as many inequalities are tight as there are variables. Algorithm 1 is encoded as a Lemke path: a sequence of distinct vertices from $S_0$, each consecutive segment inside the LCP's solution set, with $z>0$ before the end. A goal that only asserts that an equilibrium exists, or that some solution has $z=0$, is not Theorem 14. The goal requires both the termination clause and the correctness clause for every such path. "Sufficiently large $R$" is an existential threshold depending on the instance and $P$. The randomly drawn $\delta_j$ and the "small" $\varepsilon$ are generalized to every admissible value.

A complete development needs vertices, edges and degeneracy of polyhedra, Lemke's path-following lemma (two edges of the solution set at a nondegenerate vertex), and the KKT characterization of optimal SPLC bundles. The polyhedral and Lemke-path parts are reusable for other LCP-based algorithms. Contributions to any milestone, or to the optimal-bundle characterization of §4, are welcome.

Selected references

• B. R. Chaudhury, J. Garg, P. McGlaughlin, R. Mehta, Competitive Allocation of a Mixed Manna, arXiv:2008.02753v1, 2020; A Complementary Pivot Algorithm for Competitive Allocation of a Mixed Manna, Mathematics of Operations Research, 2023. https://arxiv.org/abs/2008.02753v1
• A. Bogomolnaia, H. Moulin, F. Sandomirskiy, E. Yanovskaya, Competitive Division of a Mixed Manna, Econometrica 85(6), 2017. https://doi.org/10.3982/ECTA14109
• C. E. Lemke, Bimatrix Equilibrium Points and Mathematical Programming, Management Science 11(7), 1965. https://doi.org/10.1287/mnsc.11.7.681
• B. C. Eaves, A Finite Algorithm for the Linear Exchange Model, Journal of Mathematical Economics 3(2), 1976. https://doi.org/10.1016/0304-4068(76)90019-7
• J. Garg, R. Mehta, M. Sohoni, V. V. Vazirani, A Complementary Pivot Algorithm for Market Equilibrium under Separable, Piecewise-Linear Concave Utilities, SIAM Journal on Computing 44(6), 2015. https://doi.org/10.1137/130910155

Patrolling against short attacks

A security agency guards a network of roads, pipelines or corridors against an infiltrator who needs a fixed amount of uninterrupted time at one spot to do damage. The agency moves a single patroller at bounded speed and wants to maximize the probability of catching the attack in progress. Patrolling games model this as a zero-sum game between a Patroller and an Attacker. The discrete version on graphs was introduced by Alpern, Morton and Papadaki (2011); the continuous version, where both the network and time are continuous, was studied on the line segment by Alpern, Lidbetter, Morton and Papadaki (2016), and Garrec (2019) proved that the continuous game always has a value. The mission formalizes the main general result of Alpern, Bui, Lidbetter and Papadaki, Continuous Patrolling Games (arXiv:2008.07369v2): the exact value of the game on every network when the attack is short compared with the network's cycles and leaf arcs.

Timeline: 2011, discrete patrolling games on graphs (Alpern, Morton, Papadaki); 2016, the continuous game on a line segment (Alpern, Lidbetter, Morton, Papadaki); 2019, existence of the value on general networks and its solution on Eulerian networks (Garrec); 2022, this paper: networks without leaves for attacks no longer than the girth, every network for attacks no longer than the generalized girth, trees under a leaf condition, and symmetric skewed stars.

Setting

A network $Q$ is built from a finite connected multigraph (loops and parallel edges allowed) by giving every edge $e$ a length $\lambda(e)>0$ and identifying it with an open interval of that length. Its points are the vertices and the interior points of the edges; its metric $d(x,y)$ is the minimum length of a path from $x$ to $y$; its length measure $\lambda$ is Lebesgue measure on each edge, and $\mu=\lambda(Q)$ is its total length. A leaf node is a vertex of degree $1$, and $l\ge0$ is the number of leaf nodes. The line segment is excluded.

The game $(Q,\alpha)$ has an attack duration $\alpha>0$.

1. A patrol is a path $S(t)$, $t\ge0$, with $d(S(t),S(t'))\le|t-t'|$.
2. A pure attack is a point $x$ and a start time $\tau\ge0$; it is intercepted by $S$ if $x\in S([\tau,\tau+\alpha])$.
3. The Patroller's payoff is $1$ on interception and $0$ otherwise. The value $V$ is the interception probability under optimal mixed play.

A circuit is a closed path of distinct arcs; the girth $g$ is the shortest circuit length ($g=\infty$ for a tree). The generalized girth counts a leaf arc of length $L$ as a circuit of length $2L$:

$$g^*=\min\Big(g,\;2\min_{\text{leaf arcs }a}\lambda(a)\Big).$$

Two strategies carry the solution. The independent attack strategy on the set $I$ of leaf nodes attacks a random leaf at a start time uniform on $[0,\alpha]$ with probability $p=l\alpha/(\lambda(W^c)+l\alpha)$, and otherwise attacks a uniformly random point of $W^c$ at time $\alpha/2$, where $W$ is the set of points within $\alpha/2$ of a leaf. The leaf-pausing double tour $S_2^\alpha$ follows a closed tour $S_2$ that traverses every arc twice and turns back only at leaf nodes, pausing for time $\alpha$ at each leaf; the Patroller repeats it periodically from a uniformly random starting phase.

Formalization targets

Goal: Theorem 6

For every network $Q$ and every $\alpha$ with $0<\alpha\le g^*$,

$$V=\frac{\alpha}{\mu+l\alpha/2},$$

the randomized periodic extension of $S_2^\alpha$ guarantees this interception probability for every admissible tour $S_2$, and the independent attack strategy on the leaf nodes holds every patrol to it. The value is stated as equality of the lower and upper values, so the statement includes existence.

Milestones

• Lemma 1 (the uniform attack gives $V\le\alpha/\mu$) and Theorem 1 (the independent attack gives $V\le\alpha/(\lambda(W^c)+l\alpha)$, and $V\le\alpha/(\mu+l\alpha/2)$ when the leaf arcs are at least $\alpha/2$).
• Theorem 2: a closed unit-speed tour of period $L$ visiting every point $k$ times, $\alpha$ apart cyclically, guarantees $k\alpha/L$.
• Lemma 3 and Theorem 3: an Eulerian tour avoiding prescribed pairs of passages, and the double tour $S_2$.
• Proof of Lemma 4: $S_2^\alpha$ has period $2\mu+l\alpha$ and visits every point twice, $\alpha$ apart, when $\alpha\le g$.
• Lemma 4 ($V\ge\alpha/(\mu+l\alpha/2)$ for $\alpha\le g$) and Lemma 5 ($V\le\alpha/(\mu+l\alpha/2)$ for $\alpha\le g^*$; the printed "less than" is corrected to "at most").

Significance

Theorem 6 solves the continuous patrolling game for all sufficiently short attacks on every network, since $g^*>0$. It extends the paper's Theorem 4 on networks without leaves ($l=0$, value $\alpha/\mu$) to networks with leaves, and specialized to trees it gives the equality case of the paper's Corollary 2. The formula has a direct reading: leaves cost the Patroller as if each added $\alpha/2$ of extra length, because a leaf must be revisited after turning back.

The result is proved in the paper; none of it has a machine-checked proof. Formalizing it requires the metric and measure theory of finite metric graphs, a measure-theoretic definition of mixed strategies in a game with continuum strategy sets, and a graph-theoretic tour construction (a refinement of Euler's theorem). The tour result of Theorem 3 is classical (the paper credits Sabidussi, 1977, with an earlier proof); Lemma 3 gives a new elementary proof.

Difficulty

The value formula follows from two matching bounds, and each is delicate. On the Attacker side, the paper's proof of Theorem 1 sorts patrols by where they spend the attack window (inside $W$, inside $W^c$, or crossing from $W^c$ to a leaf) and balances them through the choice of $p$; a complete proof has to handle every patrol, including ones that cross between $W$ and $W^c$ several times. On the Patroller side, the double tour must revisit every point at least $\alpha$ later, which fails for a tour that turns back in the middle of an arc; the non-backtracking property of $S_2$ and the girth condition are exactly what rule this out, and constructing $S_2$ needs control over the transitions of an Eulerian tour at every node. Both bounds also need measurability of the interception events, which is not automatic for arbitrary random patrols.

Formalization scope

The Lean development lives in the namespace ContPatrol.

• A network is a MetricGraph V E (finite types, src/tgt maps, positive len) satisfying IsNetwork: at least one edge, connected, and not a line segment. Vertices of degree $2$ are allowed, so the circle is one loop at a degree-2 vertex; leaf-arc lengths, girth and tour reversals are defined so that subdividing an arc changes nothing.
• Points are vertices or interior points of edges; the metric dist is the shortest-path distance and lengthMeasure is Lebesgue measure on the edges.
• A mixed patrol is a family of patrols on a probability space with measurable evaluations; a mixed attack is a probability measure on (point, start time) with no mass at negative times. There is no time horizon.
• lowerValue and upperValue are the sup of Patroller guarantees and the inf of Attacker guarantees; "$V=v$" means both equal $v$. The value's existence is not assumed.
• $\alpha\le g^*$ is stated as two conditions: every circuit has length at least $\alpha$, every leaf arc at least $\alpha/2$.
• The paper's standing assumption $\alpha<\bar\mu$ (the Chinese postman length) is not imposed; under $\alpha\le g^*$ it excludes only a circle with $\alpha=\mu$, where $V=1$.

No statement is vacuous: the sanity checks prove that constant paths are patrols and jumps are not, that a Dirac attack cannot hold the Patroller below $1$, that $\lambda(Q)=\mu$, and that the circle satisfies $\alpha\le g^*$ exactly for $\alpha\le\mu$.

Needed infrastructure: shortest paths and Lipschitz paths on metric graphs, Fubini on (patrol, attack) pairs, measurability of interception events, and Eulerian tours of multigraphs with loops. The metric-graph layer and the Euler-tour lemma are reusable beyond this mission. Proofs of any milestone, and lemmas on the metric (triangle inequality, Borel structure), are welcome.

Selected references

• S. Alpern, T. Bui, T. Lidbetter, K. Papadaki, Continuous Patrolling Games, arXiv:2008.07369v2, 2022 (Operations Research, 2022). https://arxiv.org/abs/2008.07369
• S. Alpern, A. Morton, K. Papadaki, Patrolling games, Operations Research 59(5):1246–1257, 2011. https://doi.org/10.1287/opre.1110.0983
• T. Garrec, Continuous patrolling and hiding games, European Journal of Operational Research 277(1):42–51, 2019. https://doi.org/10.1016/j.ejor.2019.02.016
• J. Edmonds, E. L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5(1):88–124, 1973. https://doi.org/10.1007/BF01580113

Motivation

Internal theft is a recurring cost of retail operations: a store manager who handles both the stock and the till can divert inventory or its procurement budget before customers arrive, and can skim cash after sales are made. Survey figures quoted by Chen, Tian and Zuo put internal theft among the leading sources of retail loss, and a common managerial response is to raise prices to recover the lost margin. The paper (Chen–Tian–Zuo 2025) asks what a firm that designs the manager's compensation optimally should do with its price and its capacity as theft becomes more efficient.

The model joins two lines of work. Optimal-contracting models with cash diversion and limited liability (Innes 1990; de Véricourt–Gromb 2018, 2019) show that debt-like contracts deter ex ante diversion; price-setting newsvendor models (Petruzzi–Dada 1999) describe how a monopolist prices against random multiplicative demand. Here both forms of theft act at once, and the firm chooses commission, capacity and price jointly.

Setting

A principal (the firm) gives an agent (the store manager) capacity $q\ge0$ at unit cost $c>0$ and sets a retail price $p>0$. Demand is multiplicative, $D_p=a\,p^{-b}\varepsilon$ with $a>0$, $b>1$, where the nonnegative shock $\varepsilon$ has a continuous, invertible distribution. The firm observes neither the deployed capacity nor the realized revenue.

• Ex ante theft. The agent deploys only $q'\in[0,q]$ and earns $\theta c$ per diverted unit, $0\le\theta<1$. Revenue is $P_{p,q'}=p\,(D_p\wedge q')$.
• Ex post theft. After observing revenue $r$, the agent reports $\gamma(r)\le r$ and keeps $\lambda(r-\gamma(r))$, $0\le\lambda<1$.
• Contract. A revenue-splitting rule $R$ is nondecreasing with limited liability $R(r)\le r$; the principal receives $R(\gamma(r))$ and the agent keeps the rest.

The agent's utility is $U(q',\gamma\mid p,q)=\theta c(q-q')+\mathbb E[\lambda(P_{p,q'}-\gamma(P_{p,q'}))+\gamma(P_{p,q'})-R(\gamma(P_{p,q'}))]$. The principal's problem (5)–(7) maximizes $\mathbb E[R(\gamma(P_{p,q'}))]-cq$ over $(p,q,R)$, subject to $(q',\gamma)$ being a best response of the agent; ties are broken in the principal's favour. An optimal pair $(p,q)$ is the price and capacity of an optimal solution.

The threshold commission $R_{\bar r}(r)=(1-\lambda)(r\wedge\bar r)$ plays the role of a debt contract. With $\bar F_p(q)=\mathbb P(D_p>q)$, the reduced value of a price $p$ is the function $V(p)$ of Corollary 1, built from the quantiles $q^*=\bar F_p^{-1}((1+\theta)c/p)$, $\tilde q=\bar F_p^{-1}(\theta c/(\lambda p))$ and $\bar F_p^{-1}(c/((1-\lambda)p))$. For the main theorem, $\varepsilon$ is uniform on $[1-\alpha,1+\alpha]$ with $0<\alpha\le1$.

Formalization targets

Goal: Theorem 2 (p. 16)

Fix $\theta\in[0,1)$ and uniform demand. There are thresholds $\underline\lambda<\bar\lambda\le\theta/(1+\theta)$ and functions $P,Q$ with

$$(p,q)\ \text{optimal for (5)–(7) at }\lambda\iff p=P(\lambda),\ q=Q(\lambda)\qquad(\lambda\in[0,1)),$$

such that $P,Q$ are constant on $\lambda\le\underline\lambda$; on $(\underline\lambda,\bar\lambda]$, $P$ strictly decreases and $Q$ strictly increases; and on $\lambda>\bar\lambda$, $P$ strictly increases and $Q$ strictly decreases. The thresholds are not given in closed form, so the goal survives any sharper description of them.

Milestones

1. Lemma 1 (p. 10): no-stealing contracts are without loss; (5)–(7) has the value of problem (8) with constraints (LL), (Ex Ante IC), (Ex Post IC).
2. Lemma 2 (p. 11), corrected: every incentive-compatible $R$ is replicated, or improved, by a threshold commission $R_{\bar r}$, $\bar r\in[0,pq]$.
3. Proposition 1 (p. 13): at a fixed price, the optimal capacity and threshold in four cases; the threshold strictly increases in $\lambda$.
4. Corollary 1 (pp. 14–15), corrected: the fixed-price value of (5) is $V(p)$.
5. Proposition EC.3 (pp. ec9–ec10): for uniform demand, the optimal price $p^*$ in four $\lambda$-scenarios split at $\lambda_1\le\lambda_2\le\theta/(1+\theta)$.
6. Lemma EC.1 (p. ec12): the function $g$ of (EC.25), which carries the sign of $\partial p^*/\partial\lambda$ in the third scenario, has at most one zero on $(\lambda_2,\theta/(1+\theta))$.

Significance

The theorem reverses the intuition that a firm should pass theft losses on to consumers. When ex post theft is mild, the optimal commission is debt-like and the price does not respond. As cash diversion becomes more efficient, the firm first lowers its price and expands capacity, and only later raises the price; in the last regime ($\lambda\ge\theta/(1+\theta)$) the optimal commission is a fixed revenue share. The earlier milestones are reusable on their own: Lemma 1 is a revelation-principle style reduction for joint ex ante/ex post diversion, and Lemmas 1–2 with Proposition 1 hold for any continuous demand law.

The result is proved in the paper (main text and e-companion); none of it has been machine-checked. A formal development would also settle three points the printed text leaves open: Lemma 2 needs the "or improved" correction when the expected repayment is negative; the second branch of (13) should read $+\theta c\tilde q$; and the strict inequality $\underline\lambda<\bar\lambda$ is not covered by the paper's argument at $\alpha=1$, where $\lambda_1=\lambda_2$.

Difficulty

The obvious route is to optimize over threshold contracts and differentiate the closed-form price. That does not prove the theorem. The goal is about the original problem, in which the agent may divert capacity and under-report revenue with any measurable reporting rule, and the firm may use any nondecreasing rule with limited liability. Reaching the closed forms needs a replacement argument over arbitrary reporting functions (Lemma 1), a replication argument over an infinite-dimensional contract space (Lemma 2), and a case analysis of concave newsvendor problems with an incentive constraint at a fixed price (Proposition 1). The price problem is then piecewise, glued at $p=\theta c/\lambda$, and its third branch has an interior optimum whose monotonicity depends on the sign of $g$. Uniqueness of the optimal pair is asserted but not proved separately in the paper: it requires that stealing is strictly dominated and that each branch has a unique maximizer. Finally $\underline\lambda<\bar\lambda$ needs $g$ to vanish inside $(\lambda_2,\theta/(1+\theta))$ whenever $\lambda_1=\lambda_2$.

Formalization scope

All statements live in namespace RetailTheft. The model is a structure Params with $a,b,c$ and the law $\mu$ of $\varepsilon$; $\theta$ and $\lambda$ (lam) are explicit arguments. Expectations are Bochner integrals against $\mu$; demand uses Real.rpow. Committed conventions:

• prices are positive, capacities nonnegative, and $\theta,\lambda\in[0,1)$;
• revenue-splitting rules are Monotone on $\mathbb R$ with $R(r)\le r$ for $r\ge0$; reports are measurable with $0\le\gamma(r)\le r$;
• the optimum is that of problem (5)–(7), over all rules, deployed capacities and reports with the best-response constraint; it is never defined through $V$, a closed form, or threshold contracts;
• $\bar F_p^{-1}(y)$ is the largest $q\ge0$ with $\bar F_p(q)\ge y$, used only for $y\in(0,1]$;
• every branch condition is multiplied out ($\lambda p\le\theta c$ rather than $p\le\theta c/\lambda$), so no division by $\lambda$ occurs at $\lambda=0$;
• the uniform law is $(2\alpha)^{-1}$ times Lebesgue measure on $[1-\alpha,1+\alpha]$.

A formalization in which the agent cannot steal, or in which "optimal" means the argmax of $V$, would make Lemmas 1–2 and Proposition 1 disappear from the goal; the definitions rule this out. The thresholds $\underline\lambda,\bar\lambda$ are arbitrary reals: at $\theta=0$ one needs $\underline\lambda<0$.

A complete development needs: integrals of bounded monotone compositions against a probability law, quantile functions of continuous laws, concave newsvendor optimization, and one-variable calculus for the price branches. The newsvendor and quantile lemmas are reusable beyond this mission. Contributions of proofs for any milestone, of the uniqueness argument, and of the case $\alpha=1$ of $\underline\lambda<\bar\lambda$ are welcome.

Selected references

• M. Chen, F. Tian, R. Zuo, Optimal Capacity and Price Designs Under Ex Ante and Ex Post Theft, Manufacturing & Service Operations Management, 2025. https://doi.org/10.1287/msom.2025.0024
• F. de Véricourt, D. Gromb, Financing Capacity Investment Under Demand Uncertainty: An Optimal Contracting Approach, Manufacturing & Service Operations Management 20(1):85–96, 2018.
• F. de Véricourt, D. Gromb, Financing Capacity with Stealing and Shirking, Management Science 65(11):5128–5141, 2019.
• R. D. Innes, Limited Liability and Incentive Contracting with Ex-Ante Action Choices, Journal of Economic Theory 52(1):45–67, 1990. https://doi.org/10.1016/0022-0531(90)90066-S
• N. C. Petruzzi, M. Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2):183–194, 1999. https://doi.org/10.1287/opre.47.2.183

Why organizations misjudge data

Data has become cheap to collect and store, yet firms still rely on people to design tests, analyse the results and report them, and those people often want a particular decision. Alonso and Câmara (Management Science 70(5), 2024) ask how a firm should organize this work. Should the person who designs a test also report it? How often should reports be audited? How hard should falsifying data be?

The model joins two strands of the persuasion literature. In the first, a sender commits to a public experiment (Kamenica–Gentzkow 2011). In the second, the sender may tamper with the result or the receiver may fail to observe it, as in costly misreporting (Kartik 2009) and in persuasion through weak institutions (Lipnowski–Ravid–Shishkin 2022). Its central claim runs against the usual view of data integrity: the principal should not eliminate tampering, because a credible doubt about reports is what forces the designer to run an informative test.

Setting

A state $\theta\in\{0,1\}$ has prior $\mu=\Pr[\theta=1]$. A principal chooses between the status quo $d_S$, worth $q_H$ to her, and an innovation $d_H$, worth $\theta$. So she approves only at a posterior of at least $q_H$, and $0<\mu<q_H<1$ means she retains the status quo uninformed. A designer and an agent both gain $\Delta>0$ from $d_H$.

The principal fixes a task allocation $k$ (integration $I$ or separation $S$), an audit intensity $\lambda\in[0,1]$ and a cost distribution $F$ of tampering costs on $[0,\infty)$. The designer then picks a status-quo experiment $\pi_S(\alpha)$, a pass/fail test with outcomes $s\in\{S,H\}$, $\Pr[s=H\mid\theta=1]=1$ and type-I error $\Pr[s=H\mid\theta=0]=\alpha$. The agent sees $s$ and a cost $c\sim F$, and may pay $c$ to report $m=H$ after $s=S$. With probability $\lambda$ the audit is conclusive and the principal sees $s$.

An outcome $(\alpha,t,\tau,\sigma)$ records the experiment, the tampering probability, and the approval probabilities after an unaudited $m=H$ and an audited $s=H$. In a continuation equilibrium, the agent best-responds to the gain $g=(1-\lambda)\tau\Delta$, so $F_<(g)\le t\le F_\le(g)$, and the principal best-responds to Bayesian posteriors, mixing only at $q_H$. The designer's payoff is $\Delta$ times the approval probability, minus the expected tampering cost under integration only. The commitment experiment has type-I error $\alpha_H=\mu(1-q_H)/((1-\mu)q_H)$.

Formalization targets

The goal is Proposition 7:

$$\lambda^*=\frac{1}{2-q_H},\qquad \alpha^*=0,\qquad U^*=q_H+\frac{\mu(1-q_H)}{2-q_H}.$$

Every designer-optimal outcome of every design gives the principal at most $U^*$, and every optimal design has $\lambda=\lambda^*$ and $\alpha=0$. The policy $F^*_{opt}$, with mass $\alpha_H$ at $0$ and $1-\alpha_H$ at $(1-q_H)\Delta/(2-q_H)$, attains $U^*$ under both task allocations with zero expected tampering cost. Another policy is also optimal, and a dual internal–external audit attains the same value.

The milestones are the steps of the paper's argument, in proof order:

• eqs. (13)–(14): at every designer-optimal outcome, $U=q_H+\lambda(1-\mu)q_H(\alpha_H-\alpha)$;
• Proposition 6(i): $\alpha\ge\underline\alpha(\lambda)=\frac{2\lambda-1}{\lambda}\alpha_H-\frac{\mu(1-\lambda)}{(1-\mu)\lambda}$ for every policy;
• Proposition 6(ii): several policies attain the bound, and all satisfy $F(c)\ge c/\big(c+\lambda\tfrac{p^C_S}{1-p^C_S}\Delta\big)$ on $[0,(1-\lambda)\Delta]$;
• eq. (A.9): a two-point policy attains the bound with $\tau=1$ and zero expected tampering cost.

Significance

The result gives a closed-form audit intensity that depends only on the principal's threshold, always lies strictly between $1/2$ and $1$, and is independent of the prior. It separates the two audit layers: the internal audit's strength depends on the prior, and its result must stay hidden from the principal, since the designer would otherwise pick the commitment experiment.

The proposition is proved on paper; no machine-checked proof of it is known. The formalization adds three things. It pins down the equilibrium selection on which the statement depends, it records the corrections below against the printed text, and it gives a reusable template for an audited persuasion game with atomic cost distributions.

Difficulty

The obvious route computes the designer's best experiment from the threshold equation (6) and optimizes over it. That route fails exactly where the theorem lives: the optimal policy is atomic, so (6) need not have a solution, and at $F^*_{opt}$ many continuation equilibria coexist. The argument has to work with the agent's tie conditions directly and quantify over every deviation of the designer, for every cost distribution. A second difficulty is that at the optimum the designer is exactly indifferent between $\alpha=0$ and the commitment experiment, so the order of the selections matters.

Formalization scope

Everything is in the namespace OrgAnalytics, with lam, mu, qH for $\lambda,\mu,q_H$, and the model is the single definition OrgAnalytics.Model. A cost distribution is a probability measure on $\mathbb R$ with no mass below $0$; atoms are allowed, and no density is assumed.

The conventions, each declared on the items that use it, are:

• Status-quo experiments. The design problem is posed over status-quo experiments, as the paper does after Proposition 2, with $\alpha\in[0,1]$. Propositions 1–2 on general experiments are not formalized.
• Selection. Continuation equilibria allow ties at atoms of $F$, the designer selects the continuation together with the experiment, and designer ties go to the principal.
• Corrections to the printed text. Display (1) prints the product $q_H(1-q_H)$ for the odds $q_H/(1-q_H)$. The cut-off in (20) lacks the factor $\Delta$, as the proof shows. The posterior $q$ in (13) is the one after a true $s=H$.
• No Assumption 1. $F^*_{opt}$ itself violates Assumption 1 of the paper, so the design space is every cost distribution, and the optimal policy of the multiplicity clause does satisfy it.

The statements are not trivial readings of the formulas: the designer's choice is an argmax over all continuation equilibria, the principal's utility is her primitive expected payoff, and the closed forms are theorems. Keeping $\mu>0$ and $\Delta>0$ rules out the degenerate cases. All this is elementary real analysis plus masses of half-lines and one set integral, so the proofs need no new library. Contributions of proofs of the milestones in any order are welcome; a general lemma on two-point cost distributions would be reusable across them.

Selected references

• R. Alonso, O. Câmara, Organizing Data Analytics, Management Science 70(5), 2024, 3123–3143. https://doi.org/10.1287/mnsc.2023.00207
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011, 2590–2615. https://doi.org/10.1257/aer.101.6.2590
• N. Kartik, Strategic Communication with Lying Costs, Review of Economic Studies 76(4), 2009, 1359–1395. https://doi.org/10.1111/j.1467-937X.2009.00559.x
• E. Lipnowski, D. Ravid, D. Shishkin, Persuasion via Weak Institutions, Journal of Political Economy 130(10), 2022, 2705–2730. https://doi.org/10.1086/720462

Motivation

When a team's reward depends on the total effort of its members and the reward is shared equally, every member bears her own effort cost but receives only a small share of what that effort adds. With a continuum of members, each member's effort has no effect on the shared reward, so in a Nash equilibrium nobody works: the extreme case of free riding. Firms, sales forces and research groups counter this with relative performance criteria (RPCs), rules that redistribute the reward according to each member's performance relative to the rest of the team.

Zhou's paper (SSRN 3742584, version of November 13, 2022; later published in Mathematics of Operations Research, doi:10.1287/moor.2022.1337) asks which RPC is optimal, meaning that under it some Nash equilibrium gives every member the value of full cooperation. It answers this in one period (§2), in discrete time with common noise (§3), and then for a two-layer mean-field game (§4): a continuum of teams competes, each team's reward depends on its achievement relative to the other teams, and inside each team the members play the contribution game under an RPC that the team chooses. The paper calls the two-layer formulation its main mathematical contribution. This mission formalizes §3–§4, ending with the two-layer equilibrium theorem.

Setting

There are $N\ge1$ periods. On a probability space, $X=(X_1,\dots,X_N)$ with $X_k\in\mathbb R^d$ is a member's idiosyncratic noise and $Y=(Y_1,\dots,Y_N)$ with $Y_k\in\mathbb R^e$ is the team's common noise. $X$ is independent of $Y$, and $X_1,\dots,X_N$ are independent. Write $\mathcal F^Y_k=\sigma(Y_1,\dots,Y_k)$. A control $a=(a_0,\dots,a_{N-1})$ is a sequence of nonnegative efforts. It lies in $\mathcal A$ if $a_k$ is $\mathcal F^Y_k$-measurable, and in $\tilde{\mathcal A}$ if $a_k$ may also depend on $X_1,\dots,X_k$. Effort $a$ in period $k$ produces the random performance $\phi_k(a,X_{k+1})$, with $\mathbb E[\phi_k(a,X_{k+1})]=a$. Effort costs $C_k(a)$, where $C_k$ is strictly increasing and strictly convex with $C_k(0)=C_k'(0)=0$.

The team's reward is $R(x,Y)\ge0$, where $x$ is the team's aggregate effort; its achievement is $G(x,Y)\ge0$. A team using $a\in\mathcal A$ while all other teams use $a^*$ receives

$$\mathbb V(a,a^*)=\mathbb E\Big[R\Big(\sum_ta_t\Big)\Big((1-\theta)+\theta\frac{G(\sum_ta_t)}{\mathbb E[G(\sum_ta^*_t)]}\Big)-\sum_tC_t(a_t)\Big],$$

where $\theta\in(0,1)$ is the intensity of competition among teams. A team-wise equilibrium is a control $a^*\in\arg\max_{a\in\mathcal A}\mathbb V(a,a^*)$.

Inside a team, a member using $a\in\tilde{\mathcal A}$, while her teammates use $a'$ and all members of other teams use $a''$, is paid under the ratio-based RPC with weight $\beta$:

$$\mathfrak V(a;a',\beta,a'')=\mathbb E\Big[\Big((1-\beta)+\beta\frac{\sum_t\phi_t(a_t,X_{t+1})}{\sum_t\bar a'_t}\Big)R\Big(\sum_t\bar a'_t\Big)\Big((1-\theta)+\theta\frac{G(\sum_t\bar a'_t)}{\mathbb E[G(\sum_t\bar a''_t)]}\Big)-\sum_tC_t(a_t)\Big].$$

Here $\bar a'_t=\mathbb E[a'_t\mid\mathcal F^Y_t]$ and $\bar a''_t=\mathbb E[a''_t\mid\mathcal F^Y_t]$ are the team aggregates. A pair $(\beta^*,a^*)$ is an equilibrium of the two-layer game if $a^*$ maximizes $\mathfrak V(\cdot\,;a^*,\beta^*,a^*)$ over $\tilde{\mathcal A}$, and if its payoff equals $\sup_{a'\in\tilde{\mathcal A}}\mathbb V(\bar a',\bar a^*)$. The second condition says that the team cannot do better with another RPC.

Formalization targets

Goal: Theorem 4.2 (p.20)

Under Assumption 4.1, there is a team-wise equilibrium $a^*$. It is unique up to almost-sure equality, it satisfies $0<\mathbb E[G(\sum_ta^*_t)]<\infty$, and $(\beta^*,a^*)$ is an equilibrium of the two-layer game for

$$\beta^*=\frac{R'(\sum_ta^*_t)\sum_ta^*_t}{R(\sum_ta^*_t)}+\frac{\theta G'(\sum_ta^*_t)\sum_ta^*_t}{\theta G(\sum_ta^*_t)+(1-\theta)\mathbb E[G(\sum_ta^*_t)]}.$$

Milestones

• Remark 3.1, Lemma 3.1, Proposition 3.1 concern the centralized problem $V=\sup_{a\in\mathcal A}\mathbb E[R(\sum a_k)-\sum C_k(a_k)]$. Under H Hypothesis (Definition 3.1: concave, increasing, integrably bounded by the costs), an interior optimum exists and satisfies the first-order condition $C_k'(a^*_k)=\mathbb E[R'(\sum a^*)\mid\mathcal F^Y_k]$.
• Theorem 3.1(a): the ratio-based RPC with $\beta=R'(\sum a^*)\sum a^*/R(\sum a^*)$ is optimal.
• Lemmas 4.1–4.8 concern the backward value recursion $V_t(x)=\sup_{a\ge0}\{\mathbb E_t[V_{t+1}(x+a)]-C_t(a)\}$. They show that it preserves H Hypothesis, prove its comparison and continuity properties and those of the feedback controls, and show that the competition-adjusted reward $R((1-\theta)+\theta G/b)$ satisfies H Hypothesis.
• Theorem 4.1 gives existence and uniqueness of the team-wise equilibrium.

Significance

Theorem 4.2 characterizes the optimal intra-team incentive explicitly. The first term of $\beta^*$ is the weight of the single-team problem (Theorem 3.1). The second term is the extra intra-team competition that competition among teams calls for, and it increases with $\theta$.

The results are proved in the paper. Their proofs run through a stochastic first-order condition, Komlós-type compactness for existence, an envelope theorem along a backward induction, Dini's theorem, and an intermediate-value fixed-point argument. None of them has been machine-checked. A formalization would also settle the hypotheses. The printed Lemma 3.1 and Theorem 3.1 omit concavity of the reward and are false without it. The mission states them with concavity added; the counterexample is given in the milestone statements. The goal itself is unaffected, because Assumption 4.1 contains concavity.

Difficulty

The obvious argument for Theorem 3.1(a) differentiates $\mathbb E[R(\sum a)\mid\mathcal F^Y_k]$ under the conditional expectation. Continuous differentiability and finiteness of the conditional expectation of $R'$ do not justify this; concavity does, through monotone difference quotients. For Theorem 4.1, the team-wise equilibrium is a fixed point of a map from the other teams' average achievement $b$ to $\mathbb E[G]$ at the team's optimum. That map is not obviously continuous. Its continuity needs convergence of optimal feedback controls under perturbation of the reward (Lemmas 4.3–4.5), and its monotonicity needs comparison results for value-function derivatives (Lemmas 4.2, 4.6). Existence in the centralized problem needs a compactness argument in $L^1$, because the control set is not compact.

Formalization scope

• Model. One representative player and one representative team. The continuum enters only through the conditional expectations given $\mathcal F^Y$. Periods are 0-based in Lean: X ω k is $X_{k+1}$. Controls are families of real random variables measurable for the prefix $\sigma$-algebras.
• Derivatives. "Continuously differentiable" means footnote 2 of the paper: continuous on $[0,\infty)$ and $C^1$ on $(0,\infty)$, so $R(x)=\sqrt x$ is allowed. Derivatives are taken within $[0,\infty)$.
• Conditional expectations and value functions. Conditional expectations that must be pointwise or $[0,\infty]$-valued are integrals against regular conditional distributions. The value functions take values in $[0,\infty]$.
• Expectations and suprema. Payoff comparisons, equilibrium values and the supremum in (4.5) are taken in the extended sense.
• Uniqueness is up to almost-sure equality.
• No trivial encodings. Bochner integrals of non-integrable functions and real suprema of unbounded sets would give junk zeros, so the mission states finiteness and integrability explicitly. In particular, $0<\mathbb E[G(\sum a^*)]$ is a clause of the goal.

All definitions are local: Mathlib supplies conditional expectation, regular conditional distributions, independence and convexity, but no stochastic-control or game vocabulary. A full development needs:

• a measurable dynamic-programming principle;
• an envelope theorem for concave value functions;
• a Komlós-type lemma;
• Dini's theorem on $[0,\infty)$.

These are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 4.1, are welcome.

Selected references

• Z. Zhou, Optimal relative performance criteria in mean field contribution games, SSRN 3742584, version of November 13, 2022. https://ssrn.com/abstract=3742584
• Z. Zhou, Optimal relative performance criteria in mean field contribution games, Mathematics of Operations Research, 2023. https://doi.org/10.1287/moor.2022.1337