All missions

Motivation

Finite games in strategic form are the basic model of interaction between self-interested agents in economics, engineering and computer science. Among them, potential games (Monderer and Shapley, 1996) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics such as best response and fictitious play converge to one. A natural question is what lies at the opposite end of the space of games, and how far a general game is from that tractable class.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) answer this with a canonical decomposition of every finite game into a potential, a harmonic and a nonstrategic component, obtained by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games, those whose potential component vanishes, are the complement of potential games, and the paper shows that their equilibrium behaviour is opposite as well. This mission formalizes the first such result: harmonic games generically have no pure Nash equilibrium, so the guaranteed existence of pure equilibria in potential games has no counterpart on the harmonic side. The decomposition has since been used to study near-potential games and the convergence of learning dynamics in them.

Setting

A finite game has a finite set of players $\mathcal M$ with $M = |\mathcal M|$ and, for each player $m$, a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$, and $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$. The utilities $u = (u^m)_m$ assign to each player a function $u^m : E \to \mathbb R$; for fixed $\mathcal M$ and $E$ a game is identified with its utilities, an element of $C_0^M$, where $C_0 = \{f : E \to \mathbb R\}$ carries the inner product $\langle \varphi_1,\varphi_2\rangle_0 = \sum_p \varphi_1(p)\varphi_2(p)$.

A profile $p$ is a pure Nash equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m})$ for every player $m$ and every $q^m \in E^m$.

Two profiles are $m$-comparable if they are distinct and differ only in player $m$'s strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function $X$ on ordered pairs of profiles with $X(p,q) = -X(q,p)$ on edges and $X = 0$ off edges; the space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$. The combinatorial gradient is $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$, with $W$ the edge indicator, and $\delta_0^*$ is its adjoint. Restricting to $m$-comparable pairs gives $D_m : C_0 \to C_1$, and $D u = \sum_m D_m u^m$ is the flow of payoff differences of the game $u$. With $\Pi_m = D_m^\dagger D_m$ (Moore–Penrose pseudoinverse) and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$, the paper's Definition 4.2 sets

A game is a harmonic game if $u \in \mathcal H \oplus \mathcal N$: its payoff differences form a flow with no source or sink at any profile.

Formalization targets

Goal: Proposition 5.1

For finite games in which at least two players have at least two strategies each, and for any additive Haar measure $\mu$ on the finite-dimensional space $\mathcal H \oplus \mathcal N$,

This is the paper's "harmonic games generically do not have pure Nash equilibria", with "generically" read as the paper defines it: true except on a set of measure zero within the harmonic games.

Stronger structural form

For each profile $p$, the harmonic games having $p$ as a pure Nash equilibrium form a proper linear subspace of $\mathcal H \oplus \mathcal N$. The exceptional set of the goal is then a finite union of lower-dimensional subspaces.

Milestones

1. Lemma 5.1: at a pure Nash equilibrium of a harmonic game, every player is indifferent among all of their strategies.
2. Proposition 4.1: $\dim\mathcal P = \prod_m h_m - 1$, $\dim\mathcal H = (M-1)\prod_m h_m - \sum_m\prod_{k\ne m}h_k + 1$, $\dim\mathcal N = \sum_m\prod_{k\ne m}h_k$.

Significance

The result separates harmonic games sharply from potential games. A finite potential game always has a pure equilibrium; a harmonic game almost never has one. Together with the decomposition theorem, it says that the obstruction to pure equilibria in a general game is carried by its harmonic component, and it motivates the paper's later results on mixed equilibria of harmonic games (the uniformly mixed profile is always a mixed equilibrium). Proposition 4.1, a milestone here, also gives the dimension of the harmonic games, $(M-1)\prod_m h_m + 1$, and so measures how large that class is.

The results are proved in the paper; none of them is machine-checked. Formalizing them requires the paper's operator layer (flows on the game graph, the gradient with its adjoint, pseudoinverses) in Lean for the first time, and pins down two points the paper leaves informal: the measure with respect to which "generically" is meant, and the shape condition on the game under which the statement holds.

Difficulty

Lemma 5.1 is a short counting argument once the divergence-free condition $\delta_0^* D u = 0$ is unpacked, but unpacking it requires knowing that $D$ kills $\mathcal N$ and computing $\delta_0^*$ from the $\tfrac12$-weighted inner product. The main obstacle of the goal is showing that the exceptional subspaces are proper. The proof needs a harmonic game with nonzero payoff differences, that is $\dim\mathcal H > 0$, and the only route the paper offers is the dimension count of Proposition 4.1. That count rests on the full decomposition $C_0^M = \mathcal P\oplus\mathcal H\oplus\mathcal N$, on the kernel of each $D_m$ and on the connectivity of the game graph, all of which must be built in Lean. The measure-theoretic last step, that a finite union of proper subspaces is Haar-null, is in Mathlib.

A tempting shortcut fails: placing Lebesgue measure on all of $C_0^M$ and observing that $\mathcal H \oplus \mathcal N$ is a proper subspace would prove the goal without saying anything about equilibria.

Formalization scope

Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper ($E^m = \{1,\dots,h_m\}$). A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), with the unweighted sum inner product of p. 14. $C_1$ is the subspace of edge flows with the inner product $\tfrac12\sum$ of (7). $\delta_0^*$ is Mathlib's adjoint, and the pseudoinverse is defined directly as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto $\operatorname{im} L$. $\mathcal P,\mathcal H,\mathcal N$ are defined by (28), not by the alternative description (29). Harmonic games are the submodule H ⊔ N, and pure Nash equilibrium is AGT.IsPureNash from the published agt_games definitions.

Added hypothesis. The paper leaves implicit that at least two distinct players have at least two strategies each. Its proof uses this through "dimension of $\mathcal H$ is larger than zero". Without it Proposition 5.1 is false: with two players having $1$ and $h$ strategies, $\dim\mathcal H = (2-1)h - (h+1) + 1 = 0$, every harmonic game is nonstrategic, and every profile is a pure equilibrium of every harmonic game. The goal and the structural theorem therefore carry this hypothesis explicitly.

The measure. The measure is an arbitrary additive Haar measure on the subspace $\mathcal H\oplus\mathcal N$ itself, with the Borel σ-algebra of its subspace topology. A measure on the ambient $C_0^M$ would make the statement trivial, because the whole subspace is null there. Proposition 4.1 is stated as equalities in $\mathbb Z$, so that $M-1$ and the subtraction in part 2 are not truncated.

Needed infrastructure: kernels of the $D_m$ (the paper's Lemma 4.2), the projection property of $D^\dagger D$, the decomposition theorem, and the connectivity of the game graph. The operator layer is shared with the other missions of this series and is reusable for any work on flows on graphs. Proofs of the milestones, and of the structural form independently of the goal, are welcome.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• X. Jiang, L.-H. Lim, Y. Yao, Y. Ye, Statistical ranking and combinatorial Hodge theory, Mathematical Programming 127(1):203–244, 2011. https://doi.org/10.1007/s10107-010-0419-x

Motivation

The capacitated vehicle routing problem (CVRP) asks for $K$ delivery routes from a depot that serve every client exactly once without exceeding a vehicle capacity, at minimum total length. It was introduced by Dantzig and Ramser in 1959 and is the reference problem of the vehicle routing literature: most exact methods for richer routing models (time windows, heterogeneous fleets, split deliveries) are first developed and benchmarked on it.

Exact CVRP algorithms are driven by the lower bound of a linear relaxation. Two families dominated before 2005. Branch-and-cut works with the edge variables $x_e$ and the rounded capacity inequalities (Lysgaard, Letchford and Eglese 2004, among others); its bound degrades as the number of vehicles grows. Lagrangean and column-generation methods work with q-routes, walks from the depot of bounded total demand that may revisit clients (Christofides, Mingozzi and Toth 1981). Fukasawa, Longo, Lysgaard, Poggi de Aragão, Reis, Uchoa and Werneck combine the two in one linear program over the intersection of the two polytopes, priced by column generation with every cut written on the edge variables. According to the abstract, the resulting branch-and-cut-and-price solves to optimality all instances from the literature with up to 135 vertices. The design is called robust because cuts are written on the edge variables $x$ and therefore never change the structure of the pricing problem.

This mission formalizes the formulation itself (§2 of the paper) and the two exact facts of its column generation (§3.1).

Setting

Let $G=(V,E)$ be an undirected graph on $V=\{0,1,\dots,n\}$. Vertex $0$ is the depot; $V_+=\{1,\dots,n\}$ are the clients, client $i$ having a positive demand $d_i$. Each edge has a length $\ell_e$. There are $K$ vehicles of capacity $C$, both positive integers.

A list of clients $r=(r_1,\dots,r_m)$ describes the closed walk $0\to r_1\to\cdots\to r_m\to 0$. Its edge incidence $q^e(r)$ is the number of times the walk traverses $e$ (a one-client walk $0\to j\to 0$ traverses $\{0,j\}$ twice); its load is $d_{r_1}+\cdots+d_{r_m}$, with repetitions.

• A CVRP route visits pairwise distinct clients with load at most $C$; a CVRP solution is a family $R=(R_1,\dots,R_K)$ of routes visiting every client exactly once. Its edge vector is $\chi(R)_e=\sum_kq^e(R_k)$.
• A q-route without 2-cycles is a walk of load at most $C$ that may revisit clients but contains no subpath $i\to j\to i$ with $i\ne 0$.

For $S\subseteq V$, $\delta(S)$ is the set of edges with one end in $S$, $x(\delta(S))=\sum_{e\in\delta(S)}x_e$, and $k(S)=\lceil d(S)/C\rceil$. The paper's constraints on $x\in\mathbb R^{E}$ and on weights $\lambda_j\ge 0$ of the q-routes $j$ are

$P_1$ is $\{x\ge0:(1)\text{–}(4)\}$; $P_2$ is the set of $x\ge 0$ satisfying (1) together with some $\lambda\ge0$ satisfying (5), (6); the Explicit Master $P_3$ is the projection onto $x$ of the system (1)–(6) with one $\lambda$. The Dantzig–Wolfe Master (DWM) is the LP in $\lambda$ alone obtained by substituting (5) into (1)–(4), giving the rows (8)–(11), with objective (7) $\sum_j\sum_e\ell_eq^e_j\lambda_j$. The bounds are $L_i=\min_{x\in P_i}\ell^\top x$.

Formalization targets

Goal: the formulation theorem

For a loop-free graph with positive demands and capacity, and arbitrary lengths:

with (7) equal to $\ell^\top Q\lambda$. The bounds are stated in lower-bound form: every lower bound of $\ell^\top x$ over $P_1$ or $P_2$ is one over $P_3$, and every lower bound over $P_3$ is at most the cost of every solution.

Milestones

1. $P_3=P_1\cap P_2$ (p. 5).
2. Every CVRP route is a q-route without 2-cycles (p. 2).
3. Validity of (1)–(4): $\chi(R)\in P_1$, with $\ell^\top\chi(R)$ the cost of $R$ (p. 4).
4. Validity of (5)–(6): $\chi(R)\in P_2$, with the routes of $R$ as columns (p. 4).
5. Every integer point of $P_1$ is $\chi(R)$ for a solution $R$ (p. 4).
6. Constraint (6) is implied by (2) and (5) (p. 5).
7. The DWM (8)–(11) is (1)–(4) on $x=Q\lambda$ (p. 5).
8. A generic cut $\sum_ea_ex_e\ge b$ becomes $\sum_j(\sum_ea_eq^e_j)\lambda_j\ge b$ (p. 5).
9. Every integer point of $P_2$ is $\chi(R)$ for a solution $R$ (p. 4).
10. The reduced cost of a column is $\sum_e\bar c_eq^e$ (§3.1, p. 6).
11. Scaling: a q-route for demands $\lceil d_v/g\rceil$ and capacity $\lfloor C/g\rfloor$ is a q-route for $(d,C)$ (§3.1, p. 7).

Significance

The formulation theorem is what makes the algorithm exact: integer points of $P_3$ are solutions, so branching on $x$ terminates at an optimum, and $P_3$ is a relaxation, so $L_3$ is a valid bound that dominates both classical bounds. The DWM description is what makes it computable: $P_3$ is optimized by column generation over q-routes, and milestones 8 and 10 show that any cut on $x$ can be added without changing the pricing problem, which remains a shortest q-route problem with edge costs $\bar c_e$.

The paper proves none of these claims formally; most are stated in a sentence, and milestone 9 is stated with "It can be shown" and no proof. To our knowledge none of them has a machine-checked proof. A formal development produces a library of walks, edge incidences, cut values and column families on a general graph that later missions on branch-cut-and-price (subset-row cuts, ng-routes, other routing variants) can import.

Difficulty

Most items are linear-algebra bookkeeping on finite sums, but they require a working theory of walks: edge incidences along a closed walk, the cut value of an incidence vector, and the fact that a walk from the depot crosses every client set an even number of times. The integrality statements (milestones 5 and 9 and goal part 1) are the hard part: an integer vector satisfying degree constraints need not come from routes through the depot, and the statements must exclude every other structure. For $P_2$ there are no capacity cuts at all, so the capacity of the routes must be recovered from the columns, and the paper states this case without proof. The obvious reduction "an integer point of $P_2$ is an integer combination of q-routes" fails: $\lambda$ may be fractional even when $x$ is integral.

Formalization scope

Vertices are Fin (n+1) with depot 0; edges are Sym2 (Fin (n+1)); the graph is an edge set E assumed loop-free where needed. Edge vectors are functions on all unordered pairs that vanish off E, which encodes $x\in\mathbb R^{|E|}$. Demands $d$, $K$ and $C$ are natural numbers; positive demands, $K>0$ and $C>0$ (the paper's standing assumptions, p. 1) are carried by the integrality statements and the goal, while $\ell\ge0$ is used by no statement and is omitted. Loads count repeated visits. The cut value $x(\delta(S))$, the demand $d(S)$ and $k(S)=\lceil d(S)/C\rceil$ are the published definitions LysgaardCVRP.Shrink.cut, .demand and .roundedCapacityBound. The matrix $Q$ is replaced by finitely supported weights on client lists ranging over all q-routes without 2-cycles. $L_1,L_2,L_3$ and OPT are never real infima, since $P_3$ is empty for infeasible instances.

Three trivializations are ruled out by construction: $P_3$ is defined from the Explicit Master display, not as $P_1\cap P_2$; a CVRP solution is defined by its routes, not as an integer point of a polytope; and the columns are not a fixed finite list, which would turn $P_2$ into a restricted master.

The strictness of "CVRP routes $\subsetneq$ q-routes" (p. 2) depends on the instance and is not stated. Contributions of reusable lemmas on walks and cut values of incidence vectors are welcome, as are proofs of any milestone.

Selected references

• R. Fukasawa, H. Longo, J. Lysgaard, M. Poggi de Aragão, M. Reis, E. Uchoa and R. F. Werneck, Robust branch-and-cut-and-price for the capacitated vehicle routing problem, Mathematical Programming 106 (2006); accepted manuscript. https://doi.org/10.1007/s10107-005-0644-x
• N. Christofides, A. Mingozzi and P. Toth, Exact algorithms for the vehicle routing problem, based on spanning tree and shortest path relaxations, Mathematical Programming 20 (1981). https://doi.org/10.1007/BF01589353
• J. Lysgaard, A. N. Letchford and R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100 (2004). https://doi.org/10.1007/s10107-003-0481-8
• G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6 (1959). https://doi.org/10.1287/mnsc.6.1.80

Motivation

Potential games (Monderer and Shapley, 1996) are the finite games whose incentives are captured by a single function on strategy profiles: every unilateral change of strategy changes the deviator's payoff by exactly the change of a common potential. They have pure Nash equilibria, and natural learning dynamics such as better-reply and fictitious play converge in them. Most games are not potential games, however, and before Candogan, Menache, Ozdaglar and Parrilo there was no canonical way to say how far a given game is from one, or what the remainder looks like.

Their paper (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011) answers this by viewing a game as a flow on a graph. The payoff differences between profiles that differ in one player's strategy form an edge flow on the game graph, and the classical Helmholtz (Hodge) decomposition of edge flows into gradient, harmonic and curl parts (Jiang, Lim, Yao, Ye, 2011) pulls back to a decomposition of the game itself. Every finite game becomes the sum of a potential game, a harmonic game and a component that carries no strategic information. The decomposition is the basis for the rest of the paper (equilibria of harmonic games, projections onto potential games, approximate equilibria) and for later work on dynamics in near-potential games.

Setting

Fix a finite set of players $\mathcal M$ and, for each player $m$, a finite nonempty strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$, and $p^{-m}$ denotes the strategies of the players other than $m$. A game is a family of utilities $u = (u^m)_m$ with $u^m : E \to \mathbb R$, so the space of games is $\mathcal G_{\mathcal M,E} \cong C_0^{\mathcal M}$, where $C_0 = \{E \to \mathbb R\}$ with $\langle \varphi,\psi\rangle_0 = \sum_p \varphi(p)\psi(p)$.

Two profiles are $m$-comparable if they are distinct and differ only in player $m$'s strategy. The game graph has the profiles as nodes and an edge between comparable profiles. An edge flow is a function $X : E\times E\to\mathbb R$ that is antisymmetric on edges and zero off edges; the space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\text{ edge}} X(p,q)Y(p,q)$. Triangular flows $C_2$ live on ordered 3-cliques.

The operators are: the gradient $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$, with $W$ the edge indicator; the curl $(\delta_1X)(p,q,r) = X(p,q)+X(q,r)+X(r,p)$ on 3-cliques; the per-player gradient $(D_m\varphi)(p,q) = W^m(p,q)(\varphi(q)-\varphi(p))$, with $W^m$ the indicator of $m$-comparability; and $D : C_0^{\mathcal M}\to C_1$, $Du = \sum_m D_m u^m$, the flow of pairwise comparisons of $u$. Adjoints are written ${}^*$ and Moore–Penrose pseudoinverses ${}^\dagger$. The space $C_0^{\mathcal M}$ carries the unweighted inner product $\sum_m\langle u^m,v^m\rangle_0$. Further, $\Delta_1 = \delta_1^*\delta_1+\delta_0\delta_0^*$, $\Delta_{0,m} = D_m^*D_m$, $\Pi_m = D_m^\dagger D_m$, and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$.

A game is normalized if $\sum_{p^m} u^m(p^m,p^{-m}) = 0$ for all $p^{-m}$ and $m$ (Definition 4.1). The potential, harmonic and nonstrategic subspaces are (Definition 4.2)

Formalization targets

Goal: Theorem 4.1

and every game $u$ splits as $u = u_P + u_H + u_N$ with

where $\varphi = \delta_0^\dagger Du$ is a potential function of $u_P$, i.e. $Du_P = \delta_0\varphi$.

Milestones

1. Theorem 3.1 (Helmholtz decomposition), on an arbitrary finite graph: $C_1 = \operatorname{im}\delta_0\oplus\ker\Delta_1\oplus\operatorname{im}\delta_1^*$, orthogonally, with $\ker\Delta_1 = \ker\delta_1\cap\ker\delta_0^*$.
2. Lemma 4.1: $\Delta_{0,m} = h_m\Pi_m$.
3. Lemma 4.2: $\ker D_m = \ker\Pi_m = \ker\Delta_{0,m}$, with an explicit basis indexed by $E^{-m}$.
4. Lemma 4.4 (i)–(v): $D_m^\dagger = \tfrac1{h_m}D_m^*$; $(\sum_iD_i)^\dagger D_j = (\sum_iD_i^*D_i)^\dagger D_j^*D_j$; $D^\dagger = [D_1^\dagger;\dots;D_M^\dagger]$; $\Pi = D^\dagger D$; $DD^\dagger\delta_0 = \delta_0$.
5. Lemma 4.5: $u$ normalized $\iff$ $\Pi_mu^m = u^m$ for all $m$ $\iff$ $\Pi u = u$ $\iff$ $u\in(\ker D)^\perp$.

Lemma 4.6 (the unique normalized game with the same pairwise comparisons is $\Pi u$) is included as a supporting theorem.

Significance

The decomposition turns questions about a game into questions about its three components. The potential component inherits the equilibrium and convergence theory of potential games. The harmonic component has a sharply different structure: harmonic games generically have no pure equilibrium, and in each of them the uniformly mixed profile is a mixed equilibrium. The nonstrategic component does not affect any equilibrium notion. The closed-form expressions also give the potential game closest to a given game, and with it bounds relating the approximate equilibria of the two games. The other missions of this series formalize those consequences; all of them rest on the operator layer and the subspaces defined here.

Theorem 4.1 is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces graph-flow infrastructure that Mathlib does not yet have: edge and triangular flows with their inner products, the combinatorial gradient and curl, the Helmholtz decomposition of a finite graph, and an operator Moore–Penrose pseudoinverse on finite-dimensional inner product spaces. The paper leaves Theorem 3.1 to the literature, so a full development needs a proof of it. The pseudoinverse identities of Lemma 4.4 also have a short appendix argument in the paper that a formal proof has to make complete.

Difficulty

The decomposition is not orthogonal decomposition along a single map. The subspaces $\mathcal P$ and $\mathcal H$ are defined through $\Pi$, which is assembled player by player from the $D_m$, while the flow conditions involve $\delta_0$ and the combined operator $D$. Connecting the two requires the player operators to have mutually orthogonal ranges ($D_k^*D_m = 0$ for $k\ne m$) and the explicit form of $D_m^*D_m$ as a scaled projection. Without these, $\Pi = D^\dagger D$ (Lemma 4.4 (iv)) and $DD^\dagger\delta_0 = \delta_0$ (Lemma 4.4 (v)) are not available, and they are what make the formulas for $u_P$ and $u_H$ land in $\mathcal P$ and $\mathcal H$. A direct attempt to apply the Helmholtz decomposition to $Du$ produces a flow decomposition, not a game decomposition; the pullback through $D$ is not formal, because $D$ is neither injective nor surjective.

Formalization scope

Players form a Fintype ι; strategy sets are E : ι → Type with Fintype, DecidableEq and Nonempty instances, and $h_m$ is Fintype.card (E m). Profiles are ∀ m, E m, and $(q^m,p^{-m})$ is Function.update p m q. The game graph is a Mathlib SimpleGraph; comparability requires $p\ne q$, so the graph has no loops, as the Laplacian (15) requires. $C_0$ is EuclideanSpace ℝ on profiles. $C_1$ and $C_2$ are type synonyms of the subspaces of antisymmetric (resp. alternating) functions, with inner products built from (7), including the factor $\tfrac12$ on $C_1$. Lemma 4.4 (i) fails without it. The space of games is PiLp 2 of copies of $C_0$, whose inner product is the unweighted sum used on p. 14, not the weighted inner product of the paper's Section 6. Adjoints are LinearMap.adjoint. The pseudoinverse is defined explicitly as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto $\operatorname{im}L$.

$\mathcal P$, $\mathcal H$ and $\mathcal N$ are defined by (28), not as the ranges of the component maps; the direct-sum part of the goal is stated independently of the formulas, so the goal cannot be satisfied by construction. Lemma 4.4 is split into five items, one per identity. "Orthogonal decomposition" in Theorem 3.1 is stated as pairwise orthogonality plus spanning. The paper's statements have no hypotheses beyond the setting, and none were added except nonemptiness of the strategy sets, which the paper assumes by writing $E^m = \{1,\dots,h_m\}$.

Welcome contributions: a proof of the Helmholtz decomposition on a finite simple graph, general facts about the pseudoinverse (Penrose identities, $L^\dagger L$ is the projection onto $(\ker L)^\perp$, invariance under rescaling of inner products), and the explicit adjoint formulas (12) and (22).

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• X. Jiang, L.-H. Lim, Y. Yao, Y. Ye, Statistical Ranking and Combinatorial Hodge Theory, Mathematical Programming 127:203–244, 2011. https://arxiv.org/abs/0811.1067
• R. Penrose, A generalized inverse for matrices, Mathematical Proceedings of the Cambridge Philosophical Society 51(3):406–413, 1955. https://doi.org/10.1017/S0305004100030401

Motivation

Firms that buy from unreliable suppliers can protect themselves in two ways: they can spread orders across several suppliers, or they can invest in improving a supplier's reliability, for example through supplier-development programmes or joint process-improvement projects. Wang, Gilland and Tomlin (MSOM 12(3):489–510, 2010) compare the two strategies in a newsvendor model with random supplier capacity.

This mission formalizes one part of that comparison: single sourcing with improvement, in which improvement efforts may fail. The firm must then decide when to choose its supplier. Under early commitment it picks one supplier, invests in it, and buys from it whatever the outcome. Under late commitment it invests in both suppliers, observes which efforts succeeded, and only then buys from the better one. Empirical work on supplier development documents both practices and the reluctance of suppliers whose improvement efforts previously failed (Handfield et al. 2000, as cited by Wang et al. 2010, p. 496; Krause et al. 2007). The question is how much the option to postpone the choice is worth.

Setting

A firm sells a single product over one season. It earns a unit revenue $r\ge 0$, salvages leftovers at $v$, and pays a penalty $p\ge 0$ per unit of unmet demand, with $v<r+p$. Demand $X$ is nonnegative with finite mean.

Supplier $i\in\{1,2\}$ has design capacity $K_i>0$, unit cost $c_i\ge 0$ and committed-cost fraction $\eta_i\in[0,1]$. Its capacity loss $\xi_i\ge 0$ has a continuous distribution $G_i(\cdot,a_i)$ that depends on a reliability index $a_i$; a higher index means a stochastically smaller loss. An order $q_i\ge 0$ delivers $y_i=\min\{q_i,(K_i-\xi_i)^+\}$. The firm pays $(\eta_iq_i+(1-\eta_i)y_i)c_i$, and the realized profit of single sourcing from $i$ is

The second-stage expected profit is $\Pi_2(q_i;a_i)=\mathsf E[\pi(q_i)]$, and $P_i(a_i)=\Pi_2^*(a_i)=\sup_{q_i\ge 0}\Pi_2(q_i;a_i)$ is its optimal value.

Improvement. Supplier $i$ starts at index $a_i^0$. Effort to reach index $a_i\ge a_i^0$ costs $m_iz_i(a_i)$, where $z_i$ is convex and increasing with $z_i(a_i^0)=0$. The effort succeeds with probability $\theta_i$; on failure the index stays at $a_i^0$.

• Early commitment to supplier $i$ yields

and $\Pi_1^{*E}=\max_i\sup_{a_i\ge a_i^0}\Pi_{1i}^E(a_i)$.

• Late commitment yields $\Pi_1^L(a_1,a_2)$: the improvement costs, plus, for each of the four success/failure outcomes, its probability times $\max\{P_1(\cdot),P_2(\cdot)\}$ at the realized indices (Eq. (9)). $\Pi_1^{*L}$ is its supremum over $a_1\ge a_1^0$, $a_2\ge a_2^0$.

Formalization targets

Goal: Theorem 5

Let the suppliers be identical except for their unit costs, $c_1\le c_2$, with common $\theta\in(0,1)$, $m$, $z$ and $a^0$, and let $a_2^{*E}$ be an optimal early-commitment index of supplier 2. Then

Milestones, in the paper's order

1. Lemma 2(b), single-supplier instance: $P_i$ is increasing in the index.
2. Theorem 4(a), cost-only instance: if the suppliers differ only in unit cost, the cheaper one is preferred with and without improvement, so $i^*=j^*$.
3. §4.2.2: late commitment weakly dominates early commitment, $\Pi_1^{*E}\le\Pi_1^{*L}$.
4. Lemma 4: $a_i^{*L}\le a_i^{*E}$, in the form valid for non-unique optimizers.
5. §4.2.2: $\Pi_1^{*L}=\Pi_1^{*E}$ if $P_i(a_i^{*E})<P_j(a_j^0)$ for some $i$.
6. Corollary 3(a): strict superiority of late commitment at $c_1=\hat c_1$ persists for every $c_1\in[\hat c_1,c_2]$.

Significance

The results identify when the flexibility of postponing supplier selection has value. Late commitment never hurts. It has no value when one supplier dominates the other, even after the other's improvement. For suppliers that differ only in cost, Theorem 5 gives a checkable sufficient condition for strict value. The condition weighs the gain from switching in the outcome "the costlier supplier improves, the cheaper one does not", which has probability $\theta(1-\theta)$, against the cost of improving the costlier supplier. Together with Lemma 4 the results say that keeping the choice open lowers the reliability target but can raise expected profit. Corollary 3(a) says this value is easiest to obtain when costs are close.

The paper's proofs are in an online appendix that is not used here, and none of these statements has a machine-checked proof. The mission produces formal versions of the statements, with the hypotheses that the printed versions leave implicit made explicit (see Formalization scope), and invites proofs of them.

Difficulty

The late-commitment profit (9) is a probability-weighted sum of maxima of two optimal-value functions. It is "neither concave nor unimodal" (p. 498), so first-order conditions do not characterize its optimum, and optimizers need not be unique.

• Order of the arguments. The comparison results rest on the monotonicity of $P_i$ (Lemma 2(b)). That is a statement about a supremum of expectations under a stochastically ordered family of capacity-loss laws, and must be established before the first-stage results can use it.
• Theorem 5 and Corollary 3(a) compare two suprema, neither of which is assumed to be attained. Strictness has to survive passing to the supremum.
• Corollary 3(a) is a comparative-statics statement in $c_1$. Both $\Pi_1^{*L}$ and $\Pi_1^{*E}$ decrease as $c_1$ grows, so nothing pointwise orders their difference.

Formalization scope

Everything is in the namespace MitigateSupplyRisk.LateCommit, with one definition module Model.

• Model. The demand law is a probability measure $\mu$ on $\mathbb R$ with $\mu(-\infty,0)=0$ and finite mean; no density is assumed. Capacity losses are a family $a\mapsto\nu_a$ of atomless probability measures on $[0,\infty)$, ordered by $\nu_a(-\infty,t]\le\nu_{a'}(-\infty,t]$ for $a\le a'$. Loss and demand are independent (a product measure).
• Optimal values. $\Pi_2$ is the Bochner integral of the realized profit (1). Every optimal value is a sSup over the feasible set. The sign conventions $r,p,c_i\ge 0$, $v<r+p$ make these sets bounded above, so no supremum is a junk value, and no optimum is assumed to be attained.
• Effort. The effort function $z$ is taken as the primitive on $[a^0,\infty)$, which presumes that every index is reachable.
• Identical suppliers. "Identical except for unit costs" means that the two suppliers share the same Supplier record (committed cost, capacity, loss family) and the same Improvement record ($a^0,\theta,m,z$).
• Notation in (9). The paper writes $\Pi_2^*$ for both suppliers in (9); the Lean writes $P_1$ and $P_2$.
• Added or reread hypotheses:
  • Theorem 5 assumes $0<\theta<1$. The printed condition divides by $\theta(1-\theta)$, and Lean's $x/0=0$ would otherwise turn it into $[\cdot]^+>0$, under which the conclusion is false at $\theta=1$.
  • Lemma 4 is stated for arbitrary maximizers: $\max\{a_i^L,a_i^E\}$ is again an early maximizer. This reduces to the printed inequality when the early optimizer is unique.
  • Lemma 2(b) and Theorem 4(a) are the single-supplier and cost-only instances of the paper's statements.
  • Optimizers $a_i^{*E}$ appear as hypotheses (IsMaxOn), never as claims.
• Not trivially true. A statement in which $\Pi_1^{*L}$ or $\Pi_1^{*E}$ is a junk supremum, or in which Theorem 5's condition degenerates at $\theta\in\{0,1\}$, would be trivially true or false; the bounded feasible sets and the hypothesis $0<\theta<1$ exclude both.
• Not formalized: Theorem 4 for other attributes and Theorem 4(b), Lemma 3, and Corollary 3(b), whose printed form needs hypotheses the page does not pin.