All missions

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

Motivation

Many optimization problems ask for the largest root of a concave function of one real variable that can only be accessed through oracles. In linear fractional combinatorial optimization, minimizing a ratio $c^\top x/d^\top x$ over $x\in D\subseteq\{0,1\}^m$ reduces to finding the largest root of the concave, piecewise linear function $\delta\mapsto\min_{x\in D}(c-\delta d)^\top x$. The same reduction underlies parametric submodular minimization, minimum-ratio cycles, and the feasibility of two variables per inequality (2VPI) linear systems. The classical tool is the Newton–Dinkelbach method: from the current point it follows a supergradient to the root of the tangent line and repeats. Its strongly polynomial iteration bounds go back to Radzik's analysis of fractional combinatorial optimization.

Dadush, Koh, Natura and Végh (arXiv:2004.08634v4, 2021; later in Mathematics of Operations Research, 2022) add a look-ahead step to the method. They analyse it through a Bregman divergence and obtain a strongly polynomial algorithm for 2VPI feasibility and for deterministic Markov decision processes. This mission formalizes the core of that analysis: the look-ahead method halves a Bregman divergence every two iterations.

Timeline:

• 1967. Dinkelbach's method for nonlinear fractional programming.
• 1990s. Radzik proves strongly polynomial bounds for Newton's method on linear fractional combinatorial optimization, surveyed in his 1998 handbook chapter (reference [26] of the paper).
• 2017. Goemans, Gupta and Jaillet obtain a strongly polynomial bound for discrete Newton's method on parametric submodular minimization (IPCO 2017, reference [10] of the paper).
• 2020–2021. Dadush, Koh, Natura and Végh introduce the look-ahead method and the Bregman-divergence potential (Lemma 3.4). The potential gives an $O(m\log m)$ iteration bound for linear fractional combinatorial optimization (previously $O(m^2\log m)$) and a strongly polynomial label-correcting algorithm for 2VPI feasibility with $O(mn)$ iterations, strengthening Madani's weakly polynomial bound (2002) for deterministic MDPs.

Setting

Let $\bar{\mathbb R}=\mathbb R\cup\{\pm\infty\}$ and let $f:\mathbb R\to\bar{\mathbb R}$ be a proper concave function with effective domain $\operatorname{dom}(f)=\{x:-\infty<f(x)<\infty\}$. For $x_0\in\operatorname{dom}(f)$ the set of supergradients is

$$\partial f(x_0)=\{g:\ f(x)\le f(x_0)+g(x-x_0)\ \forall x\in\mathbb R\}.$$

Assume that $f$ has a root or attains its maximum, and let

$$\delta^*=\max\bigl(\{\delta: f(\delta)=0\}\cup\arg\max f\bigr),$$

the largest root if one exists, and otherwise the largest maximizer.

Algorithm 1 (Look-aheadNewton) receives $\delta^{(1)}\in\operatorname{dom}(f)$ and $g^{(1)}\in\partial f(\delta^{(1)})$ with $f(\delta^{(1)})\le0$ and $g^{(1)}<0$. While $f(\delta^{(i)})<0$, it does the following.

1. It computes the Newton–Dinkelbach point $\delta=\delta^{(i)}-f(\delta^{(i)})/g^{(i)}$ and queries $g\in\partial f(\delta)$.
2. It reports NO ROOT if $f(\delta)=-\infty$, or if $f(\delta)<0$ and $g\ge0$.
3. It tries the look-ahead guess $\delta'=2\delta-\delta^{(i)}$. If $-\infty<f(\delta')<0$ and the queried $g'\in\partial f(\delta')$ is negative, it moves to $(\delta',g')$; otherwise it moves to $(\delta,g)$.

The Bregman divergence of $f$ (Definition 3.2) is

$$D_f(\delta',\delta)=f(\delta)+\sup_{g\in\partial f(\delta)}g(\delta'-\delta)-f(\delta')\quad(\delta\ne\delta'),\qquad D_f(\delta,\delta)=0 .$$

It is nonnegative and may be $+\infty$.

Formalization targets

Goal: Lemma 3.4

For every iteration $i>2$ of Algorithm 1,

$$D_f(\delta^*,\delta^{(i)})<\tfrac12\,D_f(\delta^*,\delta^{(i-2)}).$$

This holds for every proper concave $f$ for which $\delta^*$ exists, for every valid start, for every answer of the oracle, and up to the last iterate.

Milestones

1. Invariant (p.6). $g^{(i)}<0$ whenever $f(\delta^{(i)})<0$, and $\delta^{(i)}=\delta^*$ when $f(\delta^{(i)})=0$.
2. Lemma 3.1. $\delta^*\le\delta^{(i)}<\delta^{(i-1)}$, $f(\delta^*)\ge f(\delta^{(i)})>f(\delta^{(i-1)})$ and $g^{(i)}\ge g^{(i-1)}$, with the exact equality case, and

$$\frac{f(\delta^{(i)})}{f(\delta^{(i-1)})}+\frac{g^{(i)}}{g^{(i-1)}}\le1.$$

3. Lemma 3.3. $D_f(\delta^*,\delta^{(i)})\le D_f(\delta^*,\delta^{(i-1)})$, with the exact equality case.
4. The right derivative. $g_+^{(i)}=\min\partial f(\delta^{(i)})$ exists, and $D_f(\delta^*,\delta^{(i)})=f(\delta^{(i)})+g_+^{(i)}(\delta^*-\delta^{(i)})-f(\delta^*)$.
5. Successful look-ahead. $0<-2g_+^{(i)}\le-g^{(i-1)}$.
6. Failed look-ahead. $2\delta^{(i)}-\delta^{(i-1)}\le\delta^*$.

Milestones 1–5 are stated for runs that may mix standard and successful look-ahead steps freely, which covers the classical method and Algorithm 1. Milestone 6 needs Algorithm 1's rule.

Significance

Lemma 3.4 turns the Bregman divergence into a potential that halves every two iterations. Theorem 3.6 of the paper combines it with a lemma of Radzik on geometrically decreasing sequences (Lemma 3.5) and so bounds the look-ahead method by $O(m\log m)$ iterations for linear fractional combinatorial optimization. Theorem 4.11 uses it inside each phase of a 2VPI algorithm, which gives a strongly polynomial algorithm for 2VPI feasibility and for deterministic MDPs. A formal proof of the lemma is the reusable core of both arguments.

The paper proves the lemma on half a page of inequalities, and Lemmas 3.1 and 3.3 in the appendix. No machine-checked proof of any of them is known. The mission also builds the infrastructure that later missions need: supergradients and Bregman divergences of extended-real concave functions on the line, and an oracle-level model of the method's runs. Theorem 3.6 and the 2VPI results would build on these definitions.

Difficulty

The paper writes "It is easy to verify that Lemmas 3.1 and 3.3 also hold for Algorithm 1"; for the formal proof this step has to be done explicitly. Concave functions here are not differentiable. Supergradients are arbitrary oracle answers, $\partial f$ can be unbounded or empty at the boundary of the domain, and the divergence can be infinite at the start. A proof that implicitly uses derivatives, or a fixed choice of supergradient, does not cover the statement.

The two-case structure of Lemma 3.4 hides a subtle step. After a failed look-ahead, the claim $2\delta^{(i)}-\delta^{(i-1)}\le\delta^*$ needs an argument that a guess strictly between $\delta^*$ and $\delta^{(i)}$ would have passed the test for every possible oracle answer. That requires interiority, continuity of concave functions on the interior of the domain, and the defining property of $\delta^*$ in both the root and the no-root case.

Formalization scope

A proper concave $f:\mathbb R\to\bar{\mathbb R}$ is a pair (dom, f) with f : ℝ → ℝ and ConcaveOn ℝ dom f; "$f(x)=-\infty$" is $x\notin$ dom. Supergradients (superdiff) quantify over dom. The divergence (bregman) is EReal-valued, and the supremum is an EReal supremum, so the value $+\infty$ is represented faithfully. $\delta^*$ is a hypothesis IsDeltaStar (a greatest element via IsGreatest), never a real sSup.

A run (IsRun) is a 1-indexed sequence $\delta^{(1..N)}$, $g^{(1..N)}$ whose input is valid and whose consecutive pairs satisfy a one-step relation. In LookAheadStep (Algorithm 1) and RelaxedStep (standard or successful look-ahead), oracle answers are existentially chosen at every call. An empty superdifferential at the Newton point ends the run; at the look-ahead point it counts as a failed look-ahead. Infima and suprema of $\partial f$ are written IsLeast/IsGreatest.

Several shortcuts would trivialize the goal or weaken it, and none is used:

• fixing the oracle to the right derivative;
• assuming monotonicity of the iterates;
• excluding a start at the right endpoint, where $D_f(\delta^*,\delta^{(1)})=+\infty$;
• dropping the final iterate.

A sanity file checks a concrete run with both kinds of look-ahead, the divergence values $2,1,0,0$ along it, and a start with infinite divergence.

Welcome contributions: one-dimensional facts about concave functions (one-sided derivatives as extreme supergradients, continuity on the interior), proofs of the milestones in order, and a proof of the goal from them.

Selected references

• D. Dadush, Z. K. Koh, B. Natura, L. A. Végh, An accelerated Newton–Dinkelbach method and its application to two variables per inequality systems, arXiv:2004.08634v4, 2021; Math. Oper. Res., 2022. https://arxiv.org/abs/2004.08634v4
• T. Radzik, Fractional combinatorial optimization, in D.-Z. Du and P. M. Pardalos (eds.), Handbook of Combinatorial Optimization, Springer, 1998, pp. 429–478 (cited as [26] in the paper).
• W. Dinkelbach, On nonlinear fractional programming, Management Science 13(7), 1967. https://doi.org/10.1287/mnsc.13.7.492
• M. X. Goemans, S. Gupta, P. Jaillet, Discrete Newton's algorithm for parametric submodular function minimization, Proc. 19th IPCO, 2017, pp. 212–227 (cited as [10] in the paper).

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

Motivation

Display advertising is sold impression by impression in real-time auctions. A publisher rarely sells to advertisers directly: advertisers delegate bidding to intermediaries, ad exchanges, which collect their clients' bids in an internal auction and then bid on the winner's behalf in the publisher's header auction. Since the industry's move to first-price auctions, both layers are first-price auctions, and each layer shades its bids. Zeithammer and Choi (Management Science, 2024) ask what this two-tier bid shading does to the publisher's choice of reserve price and to everyone's surplus. Their answer is a form of double marginalization, the classical channel inefficiency in which successive margins hurt both the upstream seller and the downstream buyers, here produced by auctions at every level rather than by posted prices.

Setting

A publisher sells one impression in a first-price sealed-bid auction with reserve price $R$. Four advertisers have private valuations drawn independently from a distribution $F$ on $[0,1]$ with density $f$. The virtual value is $\psi(x)=x-\frac{1-F(x)}{f(x)}$; $F$ is regular if $\psi$ is increasing. The generalized hazard rate of the maximum of $m$ draws is

$$\lambda_m(x)=\frac{mF^{m-1}(x)f(x)}{1-F^m(x)}.$$

Direct benchmark. The advertisers bid themselves, using the symmetric equilibrium bid of a four-bidder first-price auction with reserve,

$$\beta(v;R)=\frac{RF^3(R)}{F^3(v)}+\frac{1}{F^3(v)}\int_R^v x\,dF^3(x).$$

With $M$ the highest valuation (law $F^4$), the publisher earns $\pi^{dir}_P(R)=\int_R^1\beta(M;R)\,dF^4(M)$, and each advertiser earns $\pi_C(R)=\frac14\int_R^1(M-\beta(M;R))\,dF^4(M)$.

Auction of auctions. Two exchanges each represent two advertisers. Each runs an internal first-price auction with the same reserve, so its advertisers still bid $\beta$. The exchange then bids in the header auction and keeps the difference between its internal winning bid and its own header bid. In terms of the highest valuation $m$ among its two advertisers, its equilibrium bid is

$$\tilde\sigma(m;R)=\frac{RF^2(R)}{F^2(m)}+\frac{1}{F^2(m)}\int_R^m\beta(y;R)\,dF^2(y),$$

and the publisher earns $\pi^{ex}_P(R)=\int_R^1\tilde\sigma(M;R)\,dF^4(M)$. The allocation is unchanged (the highest-value advertiser still wins), so each advertiser's profit at reserve $R$ is again $\pi_C(R)$. The pseudo hazard rate $\tilde\lambda(x)=\frac{2F(x)f(x)}{[1-F(x)][3-F(x)]}$ governs the publisher's reserve in this arrangement. A monopoly exchange representing all four advertisers pays exactly the reserve, so $\pi^{mono}_P(R)=R(1-F^4(R))$.

An optimal reserve of an arrangement is a maximizer of the corresponding publisher revenue over $[0,1]$: $R^{dir}$ for $\pi^{dir}_P$, $R^{ex}$ for $\pi^{ex}_P$.

Formalization targets

Goal: Proposition 2 (Double Marginalization)

For every regular $F$, every maximizer $R^{dir}$ of $\pi^{dir}_P$ and every maximizer $R^{ex}$ of $\pi^{ex}_P$ on $[0,1]$,

$$\pi^{ex}_P(R^{ex})<\pi^{dir}_P(R^{dir})\qquad\text{and}\qquad\pi_C(R^{ex})<\pi_C(R^{dir}).$$

Milestones, in proof order

1. Claim 1. $\lambda_m(x)$ is strictly decreasing in $m$ on $(0,1)$; if $\lambda_1$ is strictly increasing, $x\lambda_m(x)$ is strictly increasing on $[0,1)$.
2. Eq. (7). Every optimal direct reserve lies in $(0,1)$ and solves $\psi(R)=0$, i.e. $R\lambda_1(R)=1$.
3. Lemma 2, (13). $\tilde\sigma(\cdot;R)$ is a symmetric equilibrium of the exchanges' header auction against all bids $s\ge R$, and every strictly increasing symmetric equilibrium equals it.
4. Lemma 2, (14). $\tilde\sigma(m;R)<\beta(m;R)$ for $m\in(R,1]$.
5. Fixed-reserve ranking (§4.1). For $R\in[0,1)$: $R<\tilde\sigma(M;R)<\beta(M;R)$ for $M\in(R,1]$, and $\pi^{mono}_P(R)<\pi^{ex}_P(R)<\pi^{dir}_P(R)$.
6. Derivative (A17)–(A21). $\frac{d}{dR}\pi^{ex}_P(R)=2F^2(R)\big[(1-F(R))(3-F(R))-2RF(R)f(R)\big]$ on $(0,1)$.
7. Proposition 1. Every optimal $R^{ex}$ lies in $(0,1)$ and solves $R^{ex}\tilde\lambda(R^{ex})=1$; $\tilde\lambda<\lambda_1$ on $(0,1)$; $R^{dir}<R^{ex}$ for every pair of optimal reserves; $\tilde\lambda$ is strictly increasing when $\lambda_1$ is.
8. Footnote 24. $\pi_C$ is strictly decreasing on $[0,1]$.

Significance

Proposition 2 says that exchange intermediation with first-price auctions at both levels makes the publisher and the advertisers worse off together, even though at any fixed reserve the allocation is efficient. Proposition 1 locates the mechanism: the publisher responds to the exchanges' extra shading by raising the reserve above the Myerson level, which reduces sales. These results underpin the paper's later comparisons: commission-based exchange compensation that coordinates the channel (Proposition 4), the failure of the Bulow–Klemperer comparison in the presence of exchanges (Proposition 3), and the extension to $K$ exchanges with $N$ advertisers each (Proposition 5).

The results are proved in the paper; none of them is formalized elsewhere. The mission produces machine-checked statements of the model and of the chain from Lemma 2 to Proposition 2, with each paper statement placed in its exact domain. It also records one correction. The paper calls $\tilde\lambda$ "increasing" for every regular $F$; that clause is false for some regular distributions (for instance the one with $1/\lambda_1(x)=(1-x)(0.05(1-x)+4x^2(1-x)+x^3)$, for which $\tilde\lambda$ decreases on $[0.1,0.5]$). The mission states that clause under the hypothesis of Claim 1, $\lambda_1$ increasing, which the paper's proof uses. The other clauses of Proposition 1, and Proposition 2, hold for every regular $F$ and are stated at that strength.

Difficulty

The paper's proof of $R^{ex}>R^{dir}$ compares the roots of $1-x\tilde\lambda(x)$ and $1-x\lambda_1(x)$ and needs $x\tilde\lambda(x)$ to be increasing, which regularity alone does not provide. Under regularity alone an argument must work with the revenue $\pi^{ex}_P$ itself: its derivative in $R$ and the sign of $1-R\tilde\lambda(R)$ on $(0,R^{dir}]$. Computing that derivative is the main analytic step. $\pi^{ex}_P$ is a triple integral in which the reserve appears in every lower limit and inside the integrand at every level (through $\beta(\cdot;R)$ inside $\tilde\sigma(\cdot;R)$). The divisions by $F^3$ and $F^2$ also need control near $0$ when $R=0$.

Lemma 2 is an equilibrium statement. The exchange's best response has to be checked against every bid $s\ge R$, including bids outside the range of $\tilde\sigma$. Uniqueness among increasing strategies cannot assume differentiability of the strategy, which the paper's first-order derivation (A33)–(A39) does assume.

Formalization scope

The valuation distribution is a structure holding the density $f$, continuous on $[0,1]$, nonnegative, strictly positive on $(0,1)$, with integral $1$; $F(x)=\int_0^x f$. Endpoint values $f(0)=0$ or $f(1)=0$ are allowed. Regularity is weak monotonicity of $\psi$ on $(0,1)$. Every integral $\int g\,dF^k$ is written with the density $kF^{k-1}f$. The formulas (3), (4), (5), (8), (13), (18) and (19) are transcribed literally; the closed forms of the uniform case and the rewritten integrals (A16)–(A17) are not used as definitions.

Optimal reserves are arbitrary maximizers (IsMaxOn on $[0,1]$) of the transcribed revenues, quantified universally; neither uniqueness nor a first-order condition is assumed. Defining $R^{dir}$ or $R^{ex}$ as roots of $R\lambda_1(R)=1$ or $R\tilde\lambda(R)=1$ would empty Proposition 2 of its model content and is excluded.

The advertisers' equilibrium in the auction of auctions, eq. (10) (they keep bidding $\beta$), is argued in prose in the paper and is taken as the model: the exchanges' payoff uses the internal winning bid $\beta(m;R)$, and by (16) the advertisers' profit in every arrangement is $\pi_C$ at the reserve set there. The exchanges' header auction is encoded in terms of types: the rival's type has law $F^2$, it stays out below $R$, and ties lose (a null event under increasing strategies).

The development needs only Mathlib's interval integrals, derivatives and order theory. Contributions are welcome on the calculus of parameter-dependent interval integrals (Leibniz rule with variable limits), which every revenue statement uses, and on an envelope-theorem argument for first-price equilibria that does not assume differentiable strategies.

Selected references

• R. Zeithammer, W. J. Choi, Auctions of Auctions, Management Science, 2024. https://doi.org/10.1287/mnsc.2024.05233
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009. https://doi.org/10.1016/C2009-0-22474-3
• J. Bulow, P. Klemperer, Auctions versus Negotiations, American Economic Review 86(1), 1996. https://www.jstor.org/stable/2118262
• S. R. Balseiro, O. Candogan, Optimal Contracts for Intermediaries in Online Advertising, Operations Research 65(4), 2017. https://doi.org/10.1287/opre.2017.1593