Operations Research

Motivation

Firms increasingly account for, and offset, the greenhouse-gas emissions of their entire supply chain, not only their own operations. Emissions in a supply chain are often jointly produced: the footprint of one process (transport, packaging, a molten-bulk delivery) depends on the abatement efforts of several firms at once. When each firm is charged for "its" emissions, the question is how to allocate the footprint of a jointly produced process so that every firm has the right incentive to abate.

Caro, Corbett, Tan and Zuidwijk (working paper, 2012; published in Manufacturing & Service Operations Management 15(4), 2013) model this as a moral-hazard problem in teams. Their §4 shows that a social planner who wants the first-best efforts must, under joint production, double-count emissions: the marginal payments across firms for one process exceed the carbon price. This mission formalizes §5, which looks at a different institutional arrangement observed in practice. One firm, the carbon leader (the paper's example is the cosmetics company Natura), voluntarily pays for all supply-chain emissions at a carbon price $p$ and compensates the other firms to induce abatement.

Timeline. Holmström (1982) showed that a budget-balanced sharing rule cannot implement efficient efforts in a team. Strausz (1999) showed that sequential moves can restore efficiency. Battaglini (2006) studied joint production with multidimensional output. Caro et al. (2012) placed the carbon leader in this line: a Stackelberg leader whose commitment plays the role of Strausz's sequential structure.

Setting

There are finite sets of firms $\mathcal N$ and processes $\mathcal I$. Firm $n$ chooses efforts $\mathbf e_n\in[0,A]^{m_n}$, one for each of its abatement actions, and the effort profile $\mathbf e$ lies in the box $[0,A]^M$. Firm $n$ earns profit $V_n(\mathbf e_n)$, which is differentiable, concave and componentwise decreasing: effort is costly. Process $i$ emits $f_i(\mathbf e)\ge0$, which is differentiable, convex and componentwise decreasing on the box. The influence matrix $B$ has $b_{n,i}=1$ if firm $n$ influences process $i$, that is, if $\sum_j\partial f_i/\partial e_{n,j}<0$, and $b_{n,i}=0$ otherwise.

The first best at carbon price $c$ maximizes the social value $\sum_n V_n(\mathbf e_n)-c\sum_i f_i(\mathbf e)$ over the box. At the societal cost $c=p_S$ its maximizer is $\mathbf e^*$, assumed unique.

The carbon leader is a firm $N$, written L in Lean. Every other firm $n$ has a reservation profit $\bar\pi_n$. The signed transfer $g_n$ is recorded as a payment by firm $n$; a negative value means compensation from the leader. The leader faces two problems.

• $P_E$ (6)–(8): it sets $g_n(\mathbf e_n)$, contingent on firm $n$'s own effort. It maximizes $V_N(\mathbf e_N)-p\sum_i f_i(\mathbf e)+\sum_{n\ne N}g_n(\mathbf e_n)$ subject to participation, $V_n-g_n\ge\bar\pi_n$, and incentive compatibility, $\mathbf e_n$ being a best response. Its optimal value is $z^E$, attained at efforts $\mathbf e^E$.
• $P_F$ (9)–(11): the same problem, except that the payments $g_n(\mathbf f)$ may depend only on the emissions vector $\mathbf f=\mathbf f(\mathbf e)$, because efforts cannot be verified.

Formalization targets

Goal: Proposition 5 (p. 16)

Let $(g^E,\mathbf e^E)$ be optimal for $P_E$ and define, for $n\neq N$,

$$g_n(\mathbf f)=p\sum_{i\in\mathcal I}b_{n,i}f_i+k_n,\qquad k_n=V_n(\mathbf e^E_n)-p\sum_{i\in\mathcal I}b_{n,i}f_i(\mathbf e^E)-\bar\pi_n.\qquad(12)$$

Then $(g,\mathbf e^E)$ is feasible for $P_F$, its value equals $z^E$, and every feasible solution of $P_F$ has value at most $z^E$:

$$\max P_F \;=\; z^E \;=\; \max P_E .$$

Milestones (proof in App. A.4, p. 26)

1. Reduction of $P_E$ (p. 15). $z^E=\max_{\mathbf e}\big[\sum_n V_n(\mathbf e_n)-p\sum_i f_i(\mathbf e)\big]-\sum_{n\ne N}\bar\pi_n$, attained at $\mathbf e^E$.
2. Participation under (12). $V_n(\mathbf e^E_n)-g_n(\mathbf f(\mathbf e^E))=\bar\pi_n$ for $n\ne N$.
3. First-order identity. $\partial V_n(\mathbf e^E)/\partial e_{n,j}=p\sum_i b_{n,i}\,\partial f_i(\mathbf e^E)/\partial e_{n,j}$ for $n\neq N$.
4. Incentive compatibility under (12). $\mathbf e^E_n$ maximizes $V_n(\mathbf x)-g_n(\mathbf f(\mathbf e^E_{-n},\mathbf x))$ over firm $n$'s box.
5. Upper bound. Every feasible solution of $P_F$ has value at most $z^E$.

Companion: Lemma 6 (p. 17)

If $0\le p<p_S$, each $V_n$ is supermodular and each $f_i$ is submodular, then $\mathbf e^E\le\mathbf e^*$ componentwise.

Significance

The result. Proposition 5 says that, when efforts are unobservable, a carbon leader that can commit loses nothing compared with contracting on efforts. A linear rule, the form footprint accounting already takes in practice, achieves the benchmark. The rule charges each firm the full price $p$ on every footprint it influences, so emissions are double-counted internally, yet the supply chain as a whole pays for carbon once. This is how the paper reconciles its §4 impossibility (a planner must double-count) with a footprint-balanced scheme: the leader moves first and is excluded from the incentive constraints. Lemma 6 then says that a leader paying a price below the societal cost induces weakly less effort than the first best.

Formalizing it. Both results are proved in the paper. As far as the platform's catalog shows, neither is machine-checked anywhere. The proof of Proposition 5 combines a reduction of a bilevel problem with a first-order argument for concave games on a box. The appendix compresses these into three sentences, one of which contains a misprint ("since f is concave" for convex). Formalizing it makes the leader–follower conventions explicit: the leader's tie-breaking choice of follower efforts, and the unilateral deviation in (11).

Difficulty

The paper calls $P_F$ a constrained version of $P_E$, but their feasible sets are not literally nested: $P_F$'s payments are functions of the emission vector and $P_E$'s of a firm's own effort. Establishing the common upper bound therefore requires care with the two payment domains and the participation constraint (10).

The incentive compatibility of (12) is the substantive step. It is a global best-response claim on a closed effort box, while the appendix states only a first-order identity at an interior point. The influence indicator $b_{n,i}=0$ also has to agree with every action-level derivative, rather than only their sum. For Lemma 6, the optimum at price $p$ need not be unique.

Formalization scope

• Indices. Firms, actions and processes are finite types. Efforts are e : (n : ι) → act n → ℝ, and a unilateral deviation is Function.update.
• Partial derivatives. A partial derivative is the one-variable deriv along one coordinate. Every theorem that uses one assumes differentiability.
• Optimality. "Optimal" means feasible with value at least that of every feasible point, never sSup. $z^E$ is the $P_E$ objective at an optimal pair.
• Influence matrix. $B$ is a real 0/1 matrix, and its defining sign condition is assumed at every profile in the box.
• Interiority. $\mathbf e^E$ is assumed interior, the page's "A is a sufficiently large bound to guarantee interior solutions"; the box itself stays closed.
• Followers' efforts. In $P_E$ and $P_F$ the leader chooses the followers' efforts subject to the best-response constraints, as the page assumes.
• Hypotheses not imposed. The row and column sums of $B$, the strictness of $c_n$ and $g_n\le0$ are unused and not imposed.

Rule (12) is a function of the emission vector only, and the deviation in (11) moves only firm $n$'s efforts. A formalization in which payments may depend on efforts, or in which a deviation also moves the leader, would make the goal trivial and is ruled out. A sorry-free instance with two firms checks that every hypothesis of the goal can be satisfied. Supermodularity reuses the published Supermodularity.Monotonicity.SupermodularOn. All other definitions live in CarbonDoubleCount.Leader.Setting.

Proofs of the milestones, or alternative routes such as a Lagrangian argument for incentive compatibility, are welcome. A general lemma that a concave differentiable function on a box is maximized at an interior stationary point would be reusable beyond this mission.

Selected references

• F. Caro, C. J. Corbett, T. Tan, R. Zuidwijk, Double-Counting in Supply Chain Carbon Footprinting, working paper dated December 21, 2012; Manufacturing & Service Operations Management 15(4), 2013. https://doi.org/10.1287/msom.2013.0443
• B. Holmström, Moral Hazard in Teams, Bell Journal of Economics 13(2), 1982. https://doi.org/10.2307/3003457
• R. Strausz, Efficiency in Sequential Partnerships, Journal of Economic Theory 85, 1999. https://doi.org/10.1006/jeth.1998.2488
• M. Battaglini, Joint Production in Teams, Journal of Economic Theory 130(1), 2006. https://doi.org/10.1016/j.jet.2005.03.003
• D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 1978. https://doi.org/10.1287/opre.26.2.305
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526

Motivation

Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).

Timeline (as recounted on pp. 2–3 of the source):

• 2004: Lipton, Markakis, Mossel and Saberi introduce the envy-graph and cycle-elimination technique and compute allocations now called EF1 (DOI 10.1145/988772.988792).
• 2016: Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang define EFX (DOI 10.1145/2940716.2940726).
• 2018: Plaut and Roughgarden prove EFX allocations of all goods exist for two agents, or for any number of agents with identical valuations (arXiv:1707.04769).
• 2019: Caragiannis, Gravin and Huang introduce EFX with charity: a partial EFX allocation in which each agent gets at least half her value in a Nash-optimal allocation, with no bound on the number or value of donated goods (arXiv:1902.04319).
• 2020: Chaudhury, Garg and Mehlhorn prove existence of complete EFX allocations for three agents with additive valuations (arXiv:2002.05119).
• 2020/2021: the present paper bounds the charity: fewer goods than unenvied agents, and no agent envies the donated set. Its SODA 2020 version assumed gross-substitute valuations; the journal version (arXiv v3) needs only normalized monotone valuations (p. 8, §1.4).

The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.

Setting

There are $n\ge1$ agents, indexed by $N=\{1,\ldots,n\}$ in the paper, and a finite set $M$ of $m$ indivisible goods. Agent $i$ has a valuation $v_i:2^M\to\mathbb R_{\ge0}$. It is normalized if $v_i(\varnothing)=0$ and monotone if $S\subseteq T$ implies $v_i(S)\le v_i(T)$. No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.

A partial allocation $X=(X_i)_{i\in N}$ consists of pairwise disjoint bundles $X_i\subseteq M$. Its pool is the goods not assigned to anyone,

$$P(X)=M\setminus\bigcup_{i\in N}X_i.$$

The allocation is EFX when

$$v_i(X_j\setminus\{g\})\le v_i(X_i) \qquad\text{for all }i,j\in N\text{ and every }g\in X_j.$$

The paper calls allocations partial by default (p. 3, footnote 5). The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ when $v_i(X_i)<v_i(X_j)$. A source is a vertex with no incoming edge. Its reachability component $C(s)$ includes $s$ itself. The social welfare of $X$ is $\phi(X)=\sum_i v_i(X_i)$. These notions are introduced on pp. 8–9 of the source.

For a set $S$ of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset $Z$ is envied, but no strict subset of $Z$ is envied by anyone. An agent who envies such a $Z$ is a most envious agent of $S$; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).

Formalization targets

The goal is the allocation guarantee of Theorem 8:

$$\exists X\text{ partial}:\quad X\text{ is EFX},\qquad v_i(P(X))\le v_i(X_i)\ (i\in N),\qquad |P(X)|<|\operatorname{sources}(G_X)|\le n.$$

Both the stronger source-count bound and its consequence $|P(X)|<n$ are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.

The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if $X$ is EFX then $X'$ is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.

Significance

The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).

The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.

Difficulty

EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.

Formalization scope

Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis $n>0$ is explicit because the paper presumes agents and the strict bound $|P|<n$ is false when $n=0$. The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair $i,j$, including $i=j$, and every good of $X_j$.

The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold $|P|\ge n$ with $|P|\ge|\operatorname{sources}(G_X)|$, the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.

The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an $nmV/\Delta$ iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, arXiv:1907.04596v3, 2020; published in SIAM Journal on Computing, 2021. Pinned preprint.
• R. J. Lipton, E. Markakis, E. Mossel and A. Saberi, On approximately fair allocations of indivisible goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah and J. Wang, The unreasonable fairness of maximum Nash welfare, ACM EC 2016. https://doi.org/10.1145/2940716.2940726
• B. Plaut and T. Roughgarden, Almost envy-freeness with general valuations, SODA 2018. https://arxiv.org/abs/1707.04769
• I. Caragiannis, N. Gravin and X. Huang, Envy-freeness up to any item with high Nash welfare: the virtue of donating items, ACM EC 2019. https://arxiv.org/abs/1902.04319
• B. R. Chaudhury, J. Garg and K. Mehlhorn, EFX exists for three agents, ACM EC 2020. https://arxiv.org/abs/2002.05119

Motivation

Join-the-shortest-queue (JSQ) is the basic load-balancing rule for a system of $n$ parallel single-server queues: every arriving customer joins a queue of minimal length. It is optimal in several senses for homogeneous servers and is the reference policy against which cheaper rules (power-of-$d$ choices, join-the-idle-queue) are measured. In the Halfin–Whitt regime, where the arrival rate is $n\lambda$ with $\lambda = 1-\beta/\sqrt n$ for a fixed $\beta>0$, Eschenfeldt and Gamarnik (arXiv:1502.00999) proved that the suitably centred and scaled numbers of queues of length at least one and at least two converge, on finite time intervals, to a two-dimensional reflected diffusion. Braverman (arXiv:1801.05121) justified the interchange of limits (the stationary distributions of the $n$-server chains converge to the stationary distribution of the diffusion). One ingredient of that result is that the diffusion is exponentially ergodic, so it has a unique stationary distribution that is approached at a geometric rate. This mission formalizes the analytic core of that ingredient: a Foster–Lyapunov drift condition for the diffusion's generator.

Timeline. Eschenfeldt and Gamarnik (2015) proved the process-level diffusion limit, the first analysis of JSQ in this regime. Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) showed that a class of load-balancing schemes shares the same diffusion limit. Braverman (arXiv 2018, v2 2019; Math. Oper. Res. 45(3), 2020) proved tightness of the scaled stationary distributions and exponential ergodicity of the limit, which together give the interchange of limits.

Setting

The state space is the closed quadrant $\Omega = (-\infty,0]\times[0,\infty)$. For $f:\Omega\to\mathbb R$ write $f_1 = \partial f/\partial x_1$, $f_2 = \partial f/\partial x_2$, $f_{11} = \partial f_1/\partial x_1$. On the boundary $\partial\Omega$ these are one-sided derivatives, and $C^2(\Omega)$ denotes the twice continuously differentiable functions in this sense.

The diffusion limit $Y=(Y_1,Y_2)$ solves

$$Y_1(t)=Y_1(0)+\sqrt2W(t)-\beta t+\int_0^t(-Y_1(s)+Y_2(s))\,ds-U(t),\qquad Y_2(t)=Y_2(0)+U(t)-\int_0^tY_2(s)\,ds,$$

with $W$ a standard Brownian motion and $U$ a nondecreasing regulator that increases only when $Y_1=0$. For $f\in C^2(\Omega)$ with the reflection condition $f_1(0,x_2)=f_2(0,x_2)$, its generator acts by

$$G_Yf(x)=(-x_1+x_2-\beta)f_1(x)-x_2f_2(x)+f_{11}(x),\qquad x\in\Omega .$$

The construction of the Lyapunov function uses an auxiliary integer $n\ge1$ and the fluid operator

$$Lf(x)=\Big(-x_1+x_2-\frac{\beta}{\sqrt n}\Big)f_1(x)-x_2f_2(x),$$

the generator of the deterministic fluid path $v_1'=-v_1+v_2-\beta/\sqrt n$, $v_2'=-v_2$. A smoothed indicator $\phi^{(\ell,u)}$ (a piecewise cubic that rises from $0$ at $\ell$ to $1$ at $u$) and two levels $\beta<\kappa_1<\kappa_2$ define the PDEs

$$Lf^{(1)}(x)=-\phi^{(\kappa_1/\sqrt n,\kappa_2/\sqrt n)}(-x_1),\qquad Lf^{(2)}(x)=-\phi^{(\kappa_1/\sqrt n,\kappa_2/\sqrt n)}(x_2),\qquad x\in\Omega,$$

each with the reflection condition. Their solutions are written explicitly in terms of the fluid hitting times $\tilde\tau^{(\kappa)}$ (through the Lambert W function) and $\tau$, and the curves $\Gamma^{(\kappa)}$ that split $\Omega$ into regions $S_0,\dots,S_3$.

Formalization targets

Goal: Theorem 4

For every $\beta>0$ there exist $c>0$, $d>0$, a compact set $K$ and $V\in C^2(\Omega)$ with $V\ge1$ on $\Omega$, $V(x)\to\infty$ as $|x|\to\infty$ in $\Omega$, and $V_1(0,x_2)=V_2(0,x_2)$, such that

$$G_YV(x)\le -cV(x)+d\,1(x\in K),\qquad x\in\Omega .$$

The constants are unspecified and depend only on $\beta$; the statement involves no $n$.

Milestones

1. (5.6)–(5.7): $\phi^{(\ell,u)}$ has an absolutely continuous derivative with $\phi'(\ell)=\phi'(u)=0$, $|\phi'|\le 4/(u-\ell)$ and $|\phi''|\le12/(u-\ell)^2$.
2. Lemma 10: $\tilde\tau^{(\kappa)}$ extends to $\{x_2=0\}$, vanishes on $\{x_1=-\kappa/\sqrt n\}$, and has explicit one-sided partial derivatives.
3. Lemma 11: the explicit $f^{(1)}$ is nonnegative, lies in $C^2(\Omega)$, and has explicit first partials.
4. Lemma 12: the explicit six-case $f^{(2)}$ is well defined, lies in $C^2(\Omega)$, and has the partials (C.8)–(C.9).
5. Lemma 8: for $\epsilon>0$, $\kappa_1=\beta+\epsilon$, $\kappa_2=\beta+2\epsilon$, both PDEs have $C^2(\Omega)$ solutions with

$$f^{(1)}\le\log2,\quad f^{(2)}\le\log2+\tfrac{\epsilon}{\beta}\ \text{on a box},\qquad |f^{(1)}_1|\le\tfrac{4\sqrt n}{\epsilon}\log2,\ |f^{(1)}_{11}|\le\tfrac{12n}{\epsilon^2}\log2,\ |f^{(2)}_1|\le\tfrac{\sqrt n}{\beta},\ |f^{(2)}_{11}|\le\tfrac{n}{\beta\epsilon}\big(1+4\tfrac{\beta+\epsilon}{\epsilon}\big).$$

Significance

By the criterion of Down, Meyn and Tweedie (Ann. Probab. 23, 1995, Theorem 5.2), a drift inequality of the form (5.2) with compact $K$ and $V\to\infty$ implies that the diffusion is positive Harris recurrent and exponentially ergodic in the $V$-norm (Theorem 3 and Corollary 1 of the paper). Together with tightness of the prelimit stationary distributions (mission 1 of this series), this gives convergence of the stationary distributions of the JSQ chains to that of the diffusion. That justifies approximating steady-state JSQ performance by the diffusion.

The construction itself is reusable. Solving the fluid-model PDE $Lf=-(\text{smoothed indicator})$ and exponentiating the solution is a general route from fluid stability to exponential ergodicity of a diffusion. This mission writes that route out for one reflected diffusion with explicit hitting-time formulas.

Status: the result is proved in the paper; no part of it has a machine-checked proof. Theorem 3 and Corollary 1 are not posed, because they rest on the cited Down–Meyn–Tweedie theory and on the existence of the reflected process, neither of which Mathlib has.

Difficulty

The reflecting boundary rules out the first candidates. The condition $V_1(0,x_2)=V_2(0,x_2)$ excludes exponentials of linear functions such as $e^{a(x_2-x_1)}$ unless $a=0$. The natural candidate from the fluid model, the exponential of the fluid time needed to reach a box, has a discontinuous integrand and is not in $C^2(\Omega)$, so $G_Y$ cannot be applied to it. The milestone functions $f^{(1)}$, $f^{(2)}$ are given piecewise across the curves $\Gamma^{(\kappa_1)}$, $\Gamma^{(\kappa_2)}$ and the lines $x_1=-\kappa_i/\sqrt n$, through implicitly defined hitting times. Three things are hard: $C^2$ regularity across these interfaces, the Lambert W asymptotics as $x_2\downarrow0$, and second-derivative bounds that hold uniformly on the unbounded domain $\Omega$ with the stated dependence on $n$ and $\epsilon$.

Formalization scope

• Points of $\Omega$ are pairs ℝ × ℝ, and $\Omega$ is Set.Iic 0 ×ˢ Set.Ici 0. Partials are fderivWithin ℝ f Ω in the coordinate directions, which are one-sided at boundary points. $C^2(\Omega)$ is ContDiffOn ℝ 2 f Ω.
• $G_Y$ is the generator formula of p. 16, and every statement applies it only to $C^2(\Omega)$ functions with the reflection condition. The process (2.1) and the extended generator are not constructed. $V\in C^2(\Omega)$ is part of the conclusion of Theorem 4, so a $V$ whose derivatives within $\Omega$ are undefined (and default to $0$) cannot satisfy (5.2) vacuously. Dropping $V\ge1$, $V\to\infty$, the compactness of $K$, or $c,d>0$ would make (5.2) trivial, and all four are kept.
• The auxiliary $n$ is an integer $n\ge1$; no relation between $\beta$ and $\sqrt n$ is assumed.
• The Lambert W function (principal branch) is defined locally, since Mathlib has none. $\tau$ takes values in WithTop ℝ, with $\infty$ when no solution exists, and its real value is used only where it is finite. $\nu^*$ (the curve $\Gamma^{(\kappa)}$) is the solution of a nonlinear system whose uniqueness is Lemma 5.
• Two printed misprints are corrected. Lemma 8's "for every $\epsilon>0$" is formalized with $\kappa_1=\beta+\epsilon$, $\kappa_2=\beta+2\epsilon$, the choice its proof makes; read literally, the printed statement is false. In (C.5) of Lemma 10 the identity $\tilde\tau_2=-\tilde\tau_1\tilde\tau$ is formalized as $\tilde\tau_2=\tilde\tau_1\tilde\tau$, which is what implicit differentiation gives.
• Lemmas 5, 6 and 9 (properties of $\Gamma^{(\kappa)}$, $\tau$ and $W$) are milestones of mission 1; here their objects are only definitions. Contributions proving those facts in this namespace, or general lemmas on the Lambert W function, are welcome.

Selected references

• A. Braverman, Steady-State Analysis of the Join-the-Shortest-Queue Model in the Halfin-Whitt Regime, Math. Oper. Res. 45(3), 2020; preprint arXiv:1801.05121v2, 2019. https://arxiv.org/abs/1801.05121, https://doi.org/10.1287/moor.2019.1023
• P. Eschenfeldt, D. Gamarnik, Join the Shortest Queue with Many Servers. The Heavy-Traffic Asymptotics, 2015 (Math. Oper. Res. 43(3), 2018). https://arxiv.org/abs/1502.00999
• D. Down, S. P. Meyn, R. L. Tweedie, Exponential and Uniform Ergodicity of Markov Processes, Ann. Probab. 23, 1671–1691, 1995. https://doi.org/10.1214/aop/1176987798
• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of Load Balancing Schemes on the Diffusion Scale, J. Appl. Probab. 53, 1111–1124, 2016. https://projecteuclid.org/euclid.jap/1481132840

Motivation

Many scheduling decisions are not owned by a single decision maker. A machine shared by two departments, a production line serving two customers, or a computing resource shared by two users must process the jobs of two agents, each of which judges a schedule by its own criterion. Agnetis, Mirchandani, Pacciarelli and Pacifici introduced this model in Scheduling Problems with Two Competing Agents (Operations Research, 2004, doi:10.1287/opre.1030.0092), and it became the starting point of the literature on multi-agent scheduling (surveyed in Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer, 2014, doi:10.1007/978-3-642-41880-8).

When neither agent can impose its criterion on the other, the natural object to compute is the set of compromises that cannot be improved for one agent without hurting the other: the Pareto frontier. Section 11 of the paper asks how large that frontier can be for each pair of criteria it studies, because the size of the frontier decides whether it can be listed in polynomial time. This mission formalizes the answer for one agent minimizing its total completion time against the other agent's maximum cost.

Setting

Agent $A$ owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent $B$ owns jobs $J^B_1,\dots,J^B_{n_B}$, with $n_B\ge 1$. Every job $J_j$ has a positive processing time $p_j$, is available at time $0$, and is processed without interruption on a single machine that handles one job at a time. Since both criteria below are nondecreasing in completion times, a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed in that order from time $0$ without idle time, and $C_j(\sigma)$ denotes the completion time of $J_j$.

• Agent $A$ wants to minimize its total completion time $\sum_{h=1}^{n_A} C^A_h(\sigma)$.
• Each $B$-job has a nondecreasing cost function $f^B_k$ of its completion time, and agent $B$ wants to minimize its maximum cost $f^B_{\max}(\sigma)=\max_k f^B_k(C^B_k(\sigma))$.

A schedule $\sigma$ is nondominated if no schedule $\bar\sigma$ has $\sum C^A_h(\bar\sigma)\le\sum C^A_h(\sigma)$ and $f^B_{\max}(\bar\sigma)\le f^B_{\max}(\sigma)$ with at least one inequality strict. Its nondominated pair is $\bigl(\sum C^A_h(\sigma),f^B_{\max}(\sigma)\bigr)$. The constrained problem $1\|\sum C^A_i : f^B_{\max}\le Q$ asks for a schedule with $f^B_k(C^B_k)\le Q$ for every $B$-job that minimizes $\sum C^A_h$ among such schedules; such a schedule is optimal for the bound $Q$.

The $A$-jobs of a schedule follow the SPT order when they appear by nondecreasing processing time, equal lengths in index order. A $B$-job overtakes an $A$-job when it moves from after it to before it.

Formalization targets

Goal: Theorem 11.6, corrected

$$\bigl|\{(\textstyle\sum C^A_h(\sigma),\,f^B_{\max}(\sigma)) : \sigma\ \text{nondominated}\}\bigr|\ \le\ n_A\,n_B+1.$$

The paper prints the bound $n_An_B$. That bound is false: with one job per agent, unit processing times and $f^B(t)=t$, the schedules $AB$ and $BA$ give the two nondominated pairs $(1,2)$ and $(2,1)$. The corrected bound $n_An_B+1$ is the one the printed argument supports.

Milestones

1. Lemma 5.4 (p. 234): if no $B$-job can complete last within the bound, every optimal schedule ends with a longest $A$-job. This is the reason the $A$-jobs of optimal schedules are in SPT order.
2. Lemma 11.4 (p. 240): for $Q'<Q$ and optimal schedules $\sigma,\sigma'$ for $Q$ and $Q'$ whose $A$-jobs follow the SPT order, $C_j(\sigma')\ge C_j(\sigma)$ for every $A$-job $j$.
3. Lemma 11.5 (p. 240): under the same hypotheses, if a $B$-job precedes an $A$-job in $\sigma$, it precedes it also in $\sigma'$.

Significance

A frontier of size at most $n_An_B+1$ means that the scheme the paper calls PP, which solves the constrained problem for a decreasing sequence of bounds, lists every nondominated pair with polynomially many calls to a polynomial algorithm (Theorem 5.5 of the paper). The contrast with the other criteria of §11 is the point: for two total-completion-time agents the paper exhibits an exponential frontier (Example 11.7). The bound therefore separates criteria whose compromises can be negotiated over an explicit list from those where they cannot.

Formalizing it adds three things. First, the printed statements need corrections: the bound is off by one, and Lemmas 11.4 and 11.5 are false when identical $A$-jobs may be ordered differently in the two schedules. A machine-checked version fixes the exact hypotheses. Second, the monotonicity of overtakes (Lemma 11.5) is a reusable structural fact about parametric scheduling under a tightening constraint. Third, no part of this paper or of two-agent scheduling has been machine-checked before, to our knowledge; the published sequence model the mission builds on comes from the formalization of Moore's 1968 algorithm.

Difficulty

The obvious argument counts overtakes: as the bound decreases, each $B$-job overtakes each $A$-job at most once, so consecutive frontier points differ by at least one new overtake. The step that does not go through as printed is "at most once". Optimal schedules for a given bound are not unique, and two optimal schedules can disagree on the order of identical $A$-jobs and on the position of a $B$-job between them. Then an "overtake" can be undone between two bounds without any change in the objectives. The counting is valid only for a consistently chosen family of schedules, and turning the comparison of optimal schedules for two different bounds into a strict improvement needs an exchange argument with careful bookkeeping of which jobs shift. A second, smaller gap is the base case: the first schedule of the chain carries no overtake and must be counted separately.

Formalization scope

Jobs are Fin nA ⊕ Fin nB, 0-based, and a schedule is a duplicate-free list of all jobs; completion times come from the published definition MooreLateJobs.Shared.completionTime (Moore 1968 series), referenced rather than redefined. Processing times are real and strictly positive, the paper's standing convention, which the exchange arguments use. The bound $Q$ is real; the paper's integer $Q$ is a special case. Feasibility for the bound is stated job by job. The maximum cost $f^B_{\max}$ is a finite maximum and requires $n_B\ge 1$.

Explicit readings of the paper's phrases:

• "Nondominated schedules" in Theorem 11.6 is read as nondominated pairs, one schedule per pair, as §11 defines the set it enumerates. Counting schedules would count swaps of identical jobs separately.
• The count is Set.encard of a set of real pairs, so the goal asserts finiteness as well as the bound; it is not a Set.ncard, which would be $0$ on an infinite set.
• "The $A$-jobs are always SPT ordered" (p. 240) is read as the SPT order with ties broken by index, imposed as a hypothesis on both schedules in Lemmas 11.4 and 11.5. Without a fixed tie-break both lemmas are false.
• Lemma 5.4 is restated with $n_A\ge 1$, since an empty schedule has no last job. It is also a milestone of mission 3 of this series and is restated here identically because draft items cannot import each other.

Nothing in the statements is trivial by construction. The goal is about every instance with positive data, its hypotheses are satisfiable, and the counterexample to the printed bound is checked in Lean. The milestones' SPT hypotheses are met by some optimal schedule of every feasible instance, so they are not vacuous. Running times, including the polynomiality of PP and the choice of the decrement $\epsilon$ in Figure 4, are not formalized.

A complete development needs exchange lemmas for single-machine sequences (moving a job, swapping two adjacent jobs, and their effect on completion times), the existence of SPT-ordered optimal schedules, and a chain-counting argument for nested sets of overtakes. The exchange lemmas are reusable for any single-machine sequencing mission. Contributions of any of these, and of a proof of the corrected bound that avoids the scheme PP, are welcome.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2), 229–242, 2004. https://doi.org/10.1287/opre.1030.0092
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1), 102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer, 2014. https://doi.org/10.1007/978-3-642-41880-8

Motivation

Many constrained optimization problems in operations research have objective and constraint functions that are continuous but not differentiable: maxima of finitely many smooth functions, value functions of inner optimization problems, piecewise-linear costs. For such problems the classical Karush–Kuhn–Tucker theory does not apply directly, and algorithms need a nonsmooth replacement for the condition "the gradient of the Lagrangian vanishes". R. Mifflin's report Semismooth and semiconvex functions in constrained optimization (IIASA RR-76-21, 1976; SIAM J. Control Optim. 15(6), 1977) supplies one. It introduces a point-to-set map $M$ built from Clarke's generalized gradients and shows, in §5, that $0 \in M(\bar x)$ is necessary for optimality of locally Lipschitz problems and, for a class of semiconvex functions, also sufficient as soon as a strictly feasible point exists. The map $M$ goes back to Merrill's fixed-point work on differentiable and convex problems; Mifflin's own algorithm for semismooth problems converges to points satisfying $0 \in M(\bar x)$, so the sufficiency result says when such points are actual minimizers.

This mission is the third of three on the report. Mission I treats pointwise maxima of compact families of smooth functions, mission II the chain rule for semismooth compositions.

Setting

Write $\mathbb R^n$ for Euclidean space with inner product $\langle\cdot,\cdot\rangle$. For $F:\mathbb R^n\to\mathbb R$, a point $x$ and a direction $d$, the generalized directional derivative is

$$F^0(x;d)=\limsup_{h\to 0,\ t\downarrow 0}\frac{F(x+h+td)-F(x+h)}{t},$$

and the generalized gradient is the set $\partial F(x)=\{g:\langle g,d\rangle\le F^0(x;d)\text{ for all }d\}$. When $\lim_{t\downarrow 0}[F(x+td)-F(x)]/t$ exists it is the directional derivative $F'(x;d)$; $F$ is quasidifferentiable at $x$ if $F'(x;d)$ exists and equals $F^0(x;d)$ for every $d$.

Let $X\subseteq\mathbb R^n$. $F$ is semiconvex at $x\in X$ with respect to $X$ (Definition 2) if (a) $F$ is Lipschitz on a ball about $x$, (b) $F$ is quasidifferentiable at $x$, and (c) $x+d\in X$ and $F'(x;d)\ge 0$ imply $F(x+d)\ge F(x)$. It is semiconvex on $X$ if this holds at every point of $X$. Convex functions and differentiable pseudoconvex functions are semiconvex.

The problem of §5 is to minimize $f(x)$ subject to $h(x)\le 0$, where $h(x)=\max_{1\le i\le m}h_i(x)$. A point is feasible if $h(x)\le 0$ and strictly feasible if $h(x)<0$; $\bar x$ is optimal if it is feasible and $f(\bar x)\le f(x)$ for every feasible $x$. The map $M$ is

$$M(x)=\begin{cases}\partial f(x) & h(x)<0,\\ \operatorname{conv}\{\partial f(x)\cup\partial h(x)\} & h(x)=0,\\ \partial h(x) & h(x)>0,\end{cases}$$

and $\bar x$ is stationary if $h(\bar x)\le 0$ and $0\in M(\bar x)$. In Lean these are genGrad, HasDirDeriv, QuasidiffAt, SemiconvexAt/SemiconvexOn, IsFeasible, IsOptimal, Mmap and IsStationary in the namespace MifflinSemismooth.Optimality; $F^0$ is the published ClarkeGradients.Shared.genDirDeriv.

Formalization targets

Goal: Theorem 9 (p. 20)

Suppose $f$ and $h$ are semiconvex on $\mathbb R^n$ and $0\in M(\bar x)$. Then

$$h(\bar x)>0\ \Longrightarrow\ h(x)\ge h(\bar x)>0\ \text{ for all }x,$$ $$h(\bar x)\le 0\ \Longrightarrow\ \bar x\text{ is optimal, or } h(x)\ge 0\text{ for all }x.$$

The first alternative says the problem is infeasible, the last that it has no strictly feasible point. The theorem carries no constants and holds for any constraint function $h$, not only a finite maximum.

Milestones

The proof uses, in order: a point with $0\in\partial F(\bar x)$ minimizes a semiconvex $F$ over $\mathbb R^n$ (p. 20); on the boundary $h(\bar x)=0$, the condition $0\in M(\bar x)$ yields $\lambda\in[0,1]$, $\bar g\in\partial f(\bar x)$, $\hat g\in\partial h(\bar x)$ with $\lambda\bar g+(1-\lambda)\hat g=0$ (p. 20); Proposition 1(b), $F^0(x;d)=\max\{\langle g,d\rangle:g\in\partial F(x)\}$ (p. 3); Theorem 8, for $F$ semiconvex on a convex $X$, $F(x+d)\le F(x)$ implies $F'(x;d)\le 0$ (p. 19); and, if $\lambda>0$, $\langle\bar g,x-\bar x\rangle\ge 0$ for every feasible $x$ (p. 21).

Companion results

Theorem 7 (p. 18): for locally Lipschitz $f,h$, an optimal point is stationary. Theorem 6 (p. 17): for locally Lipschitz $h_1,\dots,h_m$, $h=\max_i h_i$ is locally Lipschitz with $\partial h(x)\subseteq\operatorname{conv}\bigcup_{i\in A(x)}\partial h_i(x)$, where $A(x)=\{i:h(x)=h_i(x)\}$; semismoothness, semiconvexity and quasidifferentiability on $X$ pass from the $h_i$ to $h$, and in the last two cases the inclusion is an equality at points of $X$.

Significance

Theorems 7 and 9 together give a nonsmooth Karush–Kuhn–Tucker theory: for semiconvex problem functions with a strictly feasible point, stationarity in the sense of $M$ is equivalent to global optimality. For differentiable functions this recovers the sufficiency of the Fritz John conditions for pseudoconvex objectives and constraints (Mangasarian, Nonlinear Programming, Theorem 10.1.1); for convex functions it recovers the saddle-point characterization. Since Mifflin's algorithm produces stationary points, Theorem 9 is the certificate that turns its output into a global minimizer. Theorem 6 lets the constraint $\max_i h_i\le 0$ stand for a finite system $h_i\le 0$.

The results are proved in the report. None of them, and neither the notion of semiconvexity nor the map $M$, has a machine-checked proof on Prove2Me or in Mathlib as far as the platform search shows; Mathlib has no Clarke generalized gradient. The work is to formalize the known proofs, which also produces reusable facts about $\partial F$ (nonemptiness, compactness, the max formula) and about semiconvex functions on convex sets.

Difficulty

The case analysis of Theorem 9 is short; the weight sits in its ingredients. Theorem 8 is the delicate step. Semiconvexity constrains $F$ only along directions where $F'(x;d)\ge 0$, so it says nothing directly about a direction along which $F$ does not increase; and a mean value inequality along the segment from $x$ to $x+d$ ignores quasidifferentiability and does not determine the sign of $F'(x;d)$. Proposition 1(b) is an attainment statement for a sublinear function whose finiteness rests on the Lipschitz hypothesis, and it fails for the real-valued limsup without that hypothesis. The convex-combination step depends on $\partial f(\bar x)$ and $\partial h(\bar x)$ being nonempty and convex: the convex hull of a union of two sets need not consist of two-point combinations otherwise. Theorem 7 needs $M(\bar x)$ to be closed, which in the boundary case is a statement about the convex hull of two compact sets.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $F^0$ is a real limsup and equals $0$ when the difference quotient is unbounded; every statement therefore has a Lipschitz hypothesis at the points where $F^0$ or $\partial F$ is used, and semiconvexity includes "Lipschitz on a ball". $\partial F$ is the paper's support-set definition, not the hull of gradient limits. $F'(x;d)$ is a relation (HasDirDeriv), never a function with a default value, so Definition 2(c) cannot hold vacuously. "Semiconvex on $\mathbb R^n$" means with respect to $X=\mathbb R^n$. "max" is IsGreatest, which asserts attainment. Lipschitz constants are nonnegative reals, which is equivalent to the page's positive constants.

The goal, Theorems 7, 8 and 9 are stated for an arbitrary constraint function $h$; the paper's $h=\max_i h_i$ is the special case maxConstraint hs with $m\ge 1$, and Theorem 6 is the bridge. Theorem 9's hypothesis is $0\in M(\bar x)$ alone, without feasibility. Theorem 6(c) as printed asserts $\partial h(x)=\operatorname{conv}\bigcup_{i\in A(x)}\partial h_i(x)$ "for each $x\in\mathbb R^n$"; that is false when $X\neq\mathbb R^n$ ($h_1=-|x|$, $h_2=-2|x|$, $X=(1,2)$, $x=0$), so it is stated for $x\in X$. A formalization with the hull-of-limits $\partial$, a junk-valued $F'$, a feasibility hypothesis added to Theorem 9, or semiconvexity with respect to a smaller set would prove a different and weaker theorem, and is ruled out.

A complete development needs the basic theory of the generalized gradient (Proposition 1(a), (b)), a Lebourg-type mean value theorem for case analysis along segments, and the finite-max rule. These are reusable beyond this mission, by missions I and II of the series in particular. Proofs of the milestones in any order are welcome, as are proofs of Proposition 1(a) as an auxiliary lemma.

Selected references

• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, IIASA Research Report RR-76-21, December 1976, https://pure.iiasa.ac.at/id/eprint/524/ ; journal version: SIAM J. Control Optim. 15(6) (1977) 959–972, https://doi.org/10.1137/0315061
• F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975) 247–262. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969 (SIAM Classics reprint 1994). https://doi.org/10.1137/1.9781611971255
• G. Lebourg, Valeur moyenne pour gradient généralisé, C. R. Acad. Sci. Paris Sér. A 281 (1975) 795–797.
• B. N. Pshenichnyi, Necessary Conditions for an Extremum, Marcel Dekker, 1971.

Motivation

Mean field control studies the optimal control of a very large population of interacting agents through the limit in which the population is replaced by its distribution. The limit problem is a McKean–Vlasov (MKV) control problem: the dynamics and the cost of a representative agent depend on the law of its own state. Such problems arise in systemic risk, crowd motion, energy management and the planning of large distributed systems; the reference account is Carmona and Delarue, Probabilistic Theory of Mean Field Games with Applications I–II (Springer, 2018).

MKV control problems are rarely solvable in closed form, and grid-based numerical methods suffer from the dimension of the state. A practical alternative is to simulate a finite population on a time grid, parametrize the feedback control by a neural network, and minimize the simulated cost by stochastic gradient descent. Carmona and Laurière, Convergence analysis of machine learning algorithms for the numerical solution of mean field control and games: II — the finite horizon case (Ann. Appl. Probab. 32(6), 2022, doi:10.1214/21-AAP1715), quantify how close this computable proxy is to the true optimum. This mission formalizes the statement of their main result and of the propositions and lemmas its proof is built from.

Setting

Fix a horizon $T>0$, a state dimension $d$, a control dimension $k$ (controls take values in $A=\mathbb R^k$), an initial law $\mu_0$ on $\mathbb R^d$, a drift $b(t,x,\mu,\alpha)$, a volatility $\sigma(t,x,\mu)$ (not controlled), a running cost $f(t,x,\mu,\alpha)$ and a terminal cost $g(x,\mu)$; $\mu$ ranges over $\mathcal P_2(\mathbb R^d)$, the probability measures with finite second moment, compared with the Wasserstein distance $W_2$.

Problem 1 (the MKV problem). On a probability space carrying a $d$-dimensional Wiener process $W$ and an independent $X_0\sim\mu_0$, minimize over progressively measurable square-integrable controls $\alpha\in\mathbb A$

$$J(\alpha)=\mathbb E\Big[\int_0^Tf(t,X_t,\mathcal L(X_t),\alpha_t)\,dt+g(X_T,\mathcal L(X_T))\Big],\qquad dX_t=b(t,X_t,\mathcal L(X_t),\alpha_t)\,dt+\sigma(t,X_t,\mathcal L(X_t))\,dW_t,$$

where $\mathcal L(X_t)$ is the law of $X_t$.

Problem 3 (the $N$-agent problem). $N$ agents with independent Wiener processes $W^i$ and i.i.d. initial states $X^i_0\sim\mu_0$ use a common feedback function $v(t,x)$; the law is replaced by the empirical measure $\mu^N_t=\frac1N\sum_j\delta_{X^j_t}$, and the cost is $J^N(v)=\frac1N\sum_i\mathbb E[\int_0^Tf(t,X^i_t,\mu^N_t,v(t,X^i_t))\,dt+g(X^i_T,\mu^N_T)]$.

Problem 2 (the computable proxy). With $\Delta t=T/N_T$ and $t_n=n\Delta t$, the $N$ agents follow the Euler scheme

$$\check X^i_{t_{n+1}}=\check X^i_{t_n}+b(t_n,\check X^i_{t_n},\check\mu_{t_n},\varphi(t_n,\check X^i_{t_n}))\Delta t+\sigma(t_n,\check X^i_{t_n},\check\mu_{t_n})\Delta\check W^i_n$$

with i.i.d. Gaussian increments $\Delta\check W^i_n\sim\mathcal N(0,\Delta t\,I_d)$, and $\check J^N(\varphi)$ is the expected time-discretized cost. The feedback $\varphi$ ranges over $\mathbf N^\psi_{d+1,n_{\rm in},k}$, the one-hidden-layer neural networks from $(t,x)\in\mathbb R^{d+1}$ to $\mathbb R^k$ with $n_{\rm in}$ hidden neurons and activation $\psi$; $\psi$ is $2\pi$-periodic, of class $\mathcal C^3$, with $\hat\psi_1=\int_{-\pi}^{\pi}\psi(x)e^{-ix}\,dx\ne0$.

The standing assumptions (§2.2 and Appendix A of the paper) make $b,\sigma$ affine in $(x,\bar\mu,\alpha)$ (A1), make $f,g$ differentiable in $(x,\alpha,\mu)$ (in $\mu$ in the sense of the L-derivative) with Lipschitz derivatives (A2)–(A3), make $f$ strongly convex in $\alpha$ (A4), and add the regularity (B1)–(B3), (C1)–(C3). Under them the reduced Hamiltonian $b\cdot y+f$ has a minimizer $\hat\alpha(t,x,\mu,y)$, the Pontryagin forward–backward system has a solution $(X,Y,Z)$ with marginal flow $\mu_t$, and $Y_t=V(t,X_t)$ for a regular decoupling field $V$. The optimal feedback is $\hat v(t,x)=\hat\alpha(t,x,\mu_t,V(t,x))$.

Formalization targets

Goal: Theorem 3 (p. 4070)

$$\inf_{\alpha\in\mathbb A}J(\alpha)\ \ge\ \inf_{\varphi\in\mathbf N^\psi_{d+1,n_{\rm in},k}}\check J^N(\varphi)-C\Big(N^{-1/\max(d,4)}\sqrt{1+\ln(N)\mathbf 1_{\{d=4\}}}+n_{\rm in}^{-1/(3(d+1))}+\sqrt{\Delta t}\Big)$$

for a constant $C$ depending only on the data and on $\psi$, for all $N,n_{\rm in},N_T\ge1$.

The three steps

1. Proposition 7 (finite population): $\inf_\alpha J(\alpha)\ge J^N(\hat v)-c_1\sqrt{N^{-2/\max(d,4)}(1+\ln(N)\mathbf 1_{\{d=4\}})}$.
2. Proposition 8 (network class): some $\hat\varphi\in\mathbf N^\psi_{d+1,n_{\rm in},k}$ with bounded Lipschitz constants has $J^N(\hat v)\ge J^N(\hat\varphi)-K_2n_{\rm in}^{-1/(3(d+1))}$.
3. Proposition 15 (time step): $|J^N(\varphi)-\check J^N(\varphi)|\le C\sqrt{\Delta t}$ for regular feedbacks.

Supporting results

Lemma 18 (Lipschitz continuity of $\hat\alpha$), Proposition 10 (network approximation of a function and its first two $x$-derivatives at rate $n_{\rm in}^{-1/(2(d+1))}$ on $[0,T]\times\bar B_d(0,R)$), (C.2) (moment bounds uniform in $N$), Proposition 13 (stability of $J^N$ under feedbacks close on a ball), Lemma 19 (time regularity of the particle system) and Lemma 14 (strong error $CN\Delta t$ of the Euler scheme).

Significance

The theorem certifies the standard deep-learning approach to mean field control: the value computed by minimizing the simulated finite-population, discrete-time cost over networks is, up to an explicit error with separate rates for population size, network width and time step, no larger than the true MKV value. The rates also expose where the method loses: the $n_{\rm in}^{-1/(3(d+1))}$ term is a curse of dimensionality in the network step (Remark 11).

The result is proved in the paper (§3 and Appendices B–D); the proof of Proposition 7 is a modification of Carmona–Delarue, Vol. II, Theorem 6.17. None of it is formalized. A formal development would provide the first machine-checked bridge between a stochastic control problem of McKean–Vlasov type and a concrete learning architecture, and its intermediate results (moment and stability estimates for interacting particle systems, the strong error of an Euler scheme with constants independent of the number of particles, simultaneous approximation of a function and its derivatives by periodic networks) are reusable on their own.

Difficulty

Each step rests on research-level analysis. Proposition 7 needs the Pontryagin principle for McKean–Vlasov control, the propagation of chaos for the optimally controlled system, and the Fournier–Guillin rate for empirical measures, whose $\max(d,4)$ exponent and logarithmic correction at $d=4$ appear in the bound. Proposition 8 requires approximating the optimal feedback together with its first two derivatives in $x$, because the time-discretization step needs regularity of the approximating network; standard universal approximation results give no control of derivatives, and the available simultaneous approximation results hold only for periodic functions, which forces a localization to a ball whose radius must be balanced against the approximation rate. Proposition 15 cannot be obtained from classical Euler estimates for a system of $Nd$ equations, whose constants grow with $N$: the estimates must be done agent by agent through the empirical measure.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with the sup norm; every constant is existential, so all statements are norm-independent. Time is ℝ≥0 for processes. Solutions of (2.2) and (3.2) use the published Itô-process predicate Peng1990.SMP.IsItoProcess (for $X-X_0$, with continuous paths and the natural filtration of the initial data and the noise); the backward equation of the Pontryagin system uses Peng1990.SMP.SolvesBSDE; $W_2$ is the published WassersteinDRO.Duality.wassersteinDistance. Problem 2 is law-level: the Euler scheme is a deterministic map of initial positions and increments, integrated against $\mu_0^{\otimes N}\otimes\mathcal N(0,\Delta t I_d)^{\otimes NN_T}$; Lemma 14 couples it with the continuous system through the Brownian increments, as the paper does.

The hypotheses are bundled as Coeff ((A1)–(A4), (B1), (B3), (C1), with witnesses for every derivative; the L-derivative is the Fréchet derivative of the lift on $L^2([0,1])$) and DecouplingField ((2.6), existence of a solution of (2.7) on some Problem-1 space, $Y_t=V(t,X_t)$, (B2), (C2), (C3)). Disclosed readings: $g$'s L-convexity is (A4) without $\alpha$ and with right-hand side $0$; unique solvability of (2.7), uniqueness and Lipschitz continuity of $\hat\alpha$ are not assumed (the last is Lemma 18); Proposition 13 lets its constant depend on bounds for $|v(0,0)|,|w(0,0)|$, as its proof does; Proposition 15 reads the first bound of (3.16) as $C_1(1+|(t,x)|)$. Infima are stated pointwise ($\forall\alpha\,\forall\eta>0\,\exists\varphi$), never as a real ⨅, and $N,n_{\rm in},N_T\ge1$ throughout. The hypothesis bundle is not vacuous: a sorry-free check exhibits the model $b=\sigma=0$, $f=|\alpha|^2$, $g=0$, $\mu_0=\delta_0$ with $\hat\alpha=0$, $V=0$ satisfying every assumption on any Problem-1 space. Junk values cannot trivialize the goal: the costs are Bochner integrals whose integrability follows from the assumptions, so a non-integrable cost would only make the claimed inequality harder, never vacuous.

Contributions are welcome at every level: proofs of the milestones, in particular the self-contained Lemmas 14 and 19, (C.2) and Proposition 13; infrastructure for the L-derivative, Itô's formula for the published Itô processes, empirical-measure convergence rates, and trigonometric approximation of $\mathcal C^r$ periodic functions.

Selected references

• R. Carmona, M. Laurière, Convergence analysis of machine learning algorithms for the numerical solution of mean field control and games: II — the finite horizon case, Ann. Appl. Probab. 32(6) (2022), 4065–4105. https://doi.org/10.1214/21-AAP1715
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I–II, Springer (2018). https://doi.org/10.1007/978-3-319-58920-6
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probab. Theory Relat. Fields 162 (2015), 707–738. https://doi.org/10.1007/s00440-014-0583-7
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4) (1990), 966–979. https://doi.org/10.1137/0328054

Motivation

Carbon accounting assigns emissions from a shared supply-chain process to firms that can reduce them. If more than one firm can change the same emissions, charging each firm only a share may leave each with too little incentive to abate. Caro, Corbett, Tan and Zuidwijk study the conflict between avoiding double counting in an emissions ledger and inducing the effort a social planner would choose. Their working paper, published in Manufacturing & Service Operations Management in 2013, states an impossibility result for differentiable, increasing carbon-payment rules. It covers multiple firms, processes, and abatement actions, where a process can be influenced by several firms.

The question matters when a carbon footprint is used as a payment base rather than only as a report. A payment rule changes a firm's private incentive to exert costly effort. The rule may also include transfers between firms, so its incentive effect cannot be judged by looking at a single firm's allocated emissions alone. The paper asks what aggregate marginal payment is necessary if decentralized choices are to reproduce the social first best.

Timeline. Holmström (1982) showed for a team with one joint output and one-dimensional efforts that no budget-balanced sharing rule supports the efficient efforts as a Nash equilibrium (stated in the paper as Proposition 1, p. 11). Charging every team member the full social cost ("charging everything to everyone") is known to restore efficiency, as the paper recalls on p. 12. Caro, Corbett, Tan and Zuidwijk (2012 working paper, 2013 journal version) extend the impossibility to many processes, many abatement actions per firm and an explicit influence structure between firms and processes. They also characterize the linear rules that achieve the first best.

Setting

Let $N$ be a finite set of firms and $I$ a finite set of emission-producing processes. Firm $n$ chooses a vector $e_n=(e_{n,j})_j$ of abatement efforts in $[0,A]^{m_n}$, with $A>0$. The full profile is $e=(e_n)_n$. Firm $n$'s profit before carbon payments is $V_n(e_n)$, concave and componentwise decreasing in its effort. Process $i$'s footprint is $f_i(e)$, convex and componentwise decreasing in the collective effort, and nonnegative on the feasible box. The functions are differentiable, as assumed in the paper's model.

The influence matrix $B=(b_{n,i})$ has entries in $\{0,1\}$. An entry is one when the sum of the partial derivatives of $f_i$ with respect to firm $n$'s actions is negative. The paper treats this matrix as independent of the effort profile. Joint carbon production means that a process has at least two influencing firms: for some $i$, $\sum_n b_{n,i}\ge 2$.

The societal cost per unit of footprint is $p_S>0$. The social first best $e^*$ maximizes

$$S(e)=\sum_{n\in N}V_n(e_n)-p_S\sum_{i\in I}f_i(e)$$

over the effort box. The paper assumes that this solution is unique and that the effort bound is large enough for the relevant optimum to be interior. The first-best footprint is $f(e^*)=(f_i(e^*))_{i\in I}$.

A carbon-based payment rule $h_n(\phi)$ charges firm $n$ as a function of the observed footprint vector $\phi$, rather than the unobserved effort profile. In the social-planner setting of equation (5), $h_n(\phi)=p_S\widehat f_n(\phi)+g_n(\phi)$, where $\widehat f_n$ is its footprint allocation and the transfers balance: $\sum_n g_n(\phi)=0$ for $\phi\ge0$. A Nash equilibrium is a feasible effort profile where no firm improves $V_n(e_n)-h_n(f(e))$ by changing its own entire effort vector while the other firms hold theirs fixed. At a footprint vector $\phi$, the rule double-counts process $i$ when $\sum_n \partial h_n/\partial f_i(\phi)>p_S$.

Formalization targets

The goal is Proposition 2, evaluated at the first-best footprint:

$$\text{joint production}\ \land\ e^*\text{ is Nash under differentiable increasing }h \quad\Longrightarrow\quad \exists i\in I:\ \sum_n\frac{\partial h_n}{\partial f_i}(f(e^*))>p_S.$$

The paper defines double counting existentially over footprint levels. Its Appendix A.1 proves the stronger assertion at $f(e^*)$, which is the target here. The rule remains of the form (5), with balanced internal transfers on the nonnegative footprint domain.

Two source statements form the milestone list. The necessary part of Lemma 7 gives equation (14): at an interior first best that is also a Nash equilibrium, the sum over processes of each footprint derivative times the gap between the firm's marginal payment and $p_S$ is zero, both with and without the influence indicator $b_{n,i}$. Equation (18) says that if aggregate marginal payments do not exceed $p_S$ at $f(e^*)$, every individual process contribution to that sum is zero. The mission also drafts the sufficient part of Lemma 7 and Proposition 3, which characterizes the linear rules $h=p_S A_{\mathrm{mat}}f+k$ with $0\le A_{\mathrm{mat}}\le1$: they implement $e^*$ precisely when $A_{\mathrm{mat}}\ge B$.

Significance

Proposition 2 identifies a limit on footprint-based incentives under joint production. With more than one firm able to lower a process's emissions, a differentiable increasing rule that implements the first best cannot keep every aggregate marginal charge at or below the social carbon price. Balanced transfers among firms do not remove that requirement. Proposition 3 supplies a complementary characterization for linear payments, identifying which firms must bear the full marginal charge for the processes they influence. These are results proved in the paper, not open conjectures.

The formalization contributes a precise, reusable model of finite effort profiles, process footprints, unilateral deviations, and coordinate marginal payments. It also separates a global Nash best-response condition from first-order identities, so the necessary condition in Lemma 7 has mathematical content. The listed Lean theorems are draft statements with proof holes; they do not yet have machine-checked proofs. Completing them would formally verify the paper's stated claims under the declared model conventions.

Difficulty

The obstacle is the interaction between a shared footprint and unilateral decisions. A firm's payment derivative with respect to a process footprint is multiplied by that firm's own effect on the process, while the social objective prices the total footprint at $p_S$. A condition on the sum of marginal payments alone does not specify the charge faced by each influential firm. With several actions and processes, the necessary condition is a sum over process contributions, so it cannot simply be read as a coordinatewise equality without further assumptions. These issues occur even though all effort and process index sets are finite.

Formalization scope

Lean represents firms, each firm's action indices, and processes by finite types. Efforts and footprints are real-valued functions. The firm and collective effort boxes are closed coordinatewise intervals, with $A>0$; optimality and Nash equilibrium quantify over all feasible profiles or unilateral deviations. Coordinate partial derivatives use one-variable derivatives after replacing the corresponding coordinate. Payment rules are functions on real footprint vectors and “increasing” means componentwise nondecreasing.

The source's sign test for $b_{n,i}$ does not name an effort profile. The formalization pins it to every profile in the effort box, matching the paper's use of a fixed influence matrix. Interiority is required only of the named first best. The paper's “without loss of generality” nonempty row and column sums for $B$ are omitted because the results do not use them; the strict part of its cost monotonicity is likewise unused. Its participation condition (3) is outside the decentralized game (4) and is not added to Nash equilibrium. Equation (5) and transfer balance are imposed only for nonnegative footprint vectors, as printed. The effort bound $A$ and Proposition 3's matrix $A_{\mathrm{mat}}$ have distinct names.

The first best is a feasible global maximum, not a default-valued real supremum; Nash equilibrium tests full unilateral deviations, not stationarity. These choices rule out a vacuous first-best target and a first-order surrogate for the game. The supporting definitions of finite effort boxes, coordinate derivatives, social value, and Nash best response are useful beyond the final impossibility statement. Contributions that prove the source's necessary and sufficient conditions, the linear characterization, or the goal against these definitions are within scope.

Selected references

• B. Holmström, Moral Hazard in Teams, Bell Journal of Economics 13(2), 324–340, 1982. DOI.
• F. Caro, C. J. Corbett, T. Tan and R. Zuidwijk, Double-Counting in Supply Chain Carbon Footprinting, working paper dated December 21, 2012, especially §§3–4 and Appendix A. Author-hosted manuscript. Published in Manufacturing & Service Operations Management 15(4), 2013. DOI.