Operations Research

Motivation

Online marketplaces such as Amazon are both the storefront of third-party sellers and a retailer in their own right. A platform that observes how well a seller's product sells can later launch a competing product in the same space, and empirical work finds that it does so selectively: Zhu and Liu (2018, Strategic Management Journal) report that Amazon is more likely to enter product spaces with high sales and ratings. A seller who anticipates this faces a strategic choice about how much to invest in her product before the platform decides.

Qi, Song and Xiao (Management Science, 2025) model this interaction as a two-stage game and ask how the seller's investment responds to the threat of entry. Their answer depends on whether the seller ultimately benefits from the platform's entry, which can happen through spillovers: the platform's own investment in the product space also raises the value of the seller's product. This mission formalizes the case in which the seller does not want the platform to enter, the protective regime, and the paper's characterization of her optimal effort there (Proposition 3).

Setting

The parameters are a degree of spillover $\delta\in[0,1]$, a referral rate $f\in[0,1)$ (the share of the seller's revenue paid to the platform), a competition intensity $\beta\in[0,1]$, the seller's effort-cost coefficient $c_S>1/2$, and the platform's fixed entry cost $K>0$. The platform's own cost coefficient is normalized to $c_P=1/2$.

In the first stage the seller's product has base value $a$; she chooses an effort $e_S$ at cost $c_Se_S^2$, raising the value to $a+e_S$, and sells a quantity $q_1$ at price $a+e_S-q_1$, keeping the fraction $1-f$ of revenue. In the second stage the platform, having inferred $a+e_S$, decides whether to enter. If it does, it invests in the product space and the two compete in quantities.

The paper reduces the second stage to closed forms. Write $N_5$ for the left side of condition (5),

$$N_5=4(1+\delta)-2\beta(2-\delta+\delta^2)+\beta^3(1+f)-\beta^2(2+f+\delta f)>0,$$

which says that the seller stays in the market after entry and is assumed throughout. With an explicit polynomial denominator $D$, set $H=N_5^2/D^2$ (equation (8)). The seller's two-stage profits under non-entry and entry are

$$\Pi^S_N(e_S)=\frac{(1-f)(a+e_S)^2}{2}-c_Se_S^2,\qquad \Pi^S_E(e_S)=\Big(\frac14+H\Big)(1-f)(a+e_S)^2-c_Se_S^2 .$$

The platform enters iff the product value exceeds a threshold $\Delta=\sqrt{-4KD/E_N}$, where $E_N$ is a second explicit polynomial in $(\delta,f,\beta)$ (Proposition 1). Hence the seller's total profit is

$$\Pi^S(e_S)=\begin{cases}\Pi^S_N(e_S)&e_S+a\le\Delta,\\ \Pi^S_E(e_S)&e_S+a>\Delta.\end{cases}$$

The protective regime is $\overline\Omega=\{(\delta,f,\beta): H\le 1/4\}$; there $\Pi^S_N\ge\Pi^S_E$ for every effort. The benchmark efforts $e^B_N(a)=(1-f)a/(f+2c_S-1)$ and $e^B_E(a)=a(1-f)(1+4H)/(4c_S-(1-f)(1+4H))$, equations (9)–(10), maximize $\Pi^S_N$ and $\Pi^S_E$ respectively.

Formalization targets

Goal: Proposition 3

In the protective regime, with $\underline a_1$ defined by $\underline a_1+e^B_N(\underline a_1)=\Delta$, there is $\bar a_1\ge\underline a_1$ such that an optimal effort is

$$e^*_S(a)=\begin{cases}e^B_N(a)&a\le\underline a_1,\\ \Delta-a&a\in(\underline a_1,\bar a_1),\\ e^B_E(a)&a\ge\bar a_1,\end{cases}$$

and the optimal first-stage quantity is $q_1^*=(a+e^*_S(a))/2$.

Milestones

1. Proposition 1: under (5) and $K>0$, $\Delta>0$ and the platform's gain from entry is positive iff $a+e_S>\Delta$.
2. Equations (9)–(10): $e^B_N$ and $e^B_E$ are the unique unconstrained maximizers.
3. $e^B_N(a)\ge e^B_E(a)$ for $a>0$ when $H\le 1/4$.
4. With $M(a)=\Pi^S_N(\Delta-a)-\Pi^S_E(e^B_E(a))$: $dM/da=2c_S(\Delta-a-e^B_E(a))$.
5. $M(\underline a_1)\ge 0$.
6. Cases 1.1, 1.2 and 1.3 of the proof: optimality of each of the three efforts on its region.

Significance

The result identifies strategic underinvestment as the seller's response to an unwelcome entrant: for intermediate base values she chooses less effort than her first-best so that the product's value sits exactly at the entry threshold. For low base values no distortion is needed, and for high ones the required distortion costs more than entry does. This explains why a seller's investment may fall short of what her own costs and demand would justify, and it is the starting point of the paper's analysis of non-entry commitments (Proposition 5).

The result is proved in the paper; nothing here is open. No part of it is formalized. A machine-checked version adds a complete check of a proof that compresses several steps into "verifiable" remarks: the positivity of $D$ and the sign of $E_N$ under (5), and the single sign change of $dM/da$ that defines $\bar a_1$.

Difficulty

The seller's objective $\Pi^S$ is discontinuous at $e_S=\Delta-a$, so the first-order condition alone does not locate the optimum: the candidates are the two unconstrained maximizers and the cutoff, and which one wins depends on $a$. The step that needs care is the existence of a single switching point $\bar a_1$: it requires comparing the value of the constrained non-entry problem with the unconstrained entry optimum as a function of $a$, and showing that the comparison changes sign once. The polynomial sign facts behind $\Delta$, namely $D>0$ and $E_N<0$ on the parameter box under (5), are elementary but involve quartic polynomials in three variables.

Formalization scope

All quantities are real numbers. The standing ranges $\delta,\beta\in[0,1]$, $f\in[0,1)$, $c_S>1/2$ are hypotheses, as are condition (5) (assumed by the paper from p. 12 on) and $K>0$ (not stated by the paper, but presupposed by its formula for $\Delta$; with $K\le 0$ the threshold degenerates to 0). Only the branch of $\Delta$ and $\Pi^P_{E-N}$ for which (5) holds is formalized; the paper's proof also covers the regime where (5) fails, with $H=0$.

The closed forms (6), (7), the entry gain $\Pi^P_{E-N}$ and $\Delta$ are definitions taken from the paper. Their derivation from the second-stage Cournot game (Lemmas 1–2) is the subject of the companion mission On the Platform’s Entry I. The piecewise profit $\Pi^S$ is the printed one, with the tie $e_S+a=\Delta$ assigned to non-entry.

Efforts range over all of $\mathbb R$. This is the paper's implicit domain and it matters: the optimal effort $\Delta-a$ is negative for some parameters (for instance $\delta=f=0$, $\beta=1/2$, $c_S=K=1$ and $a$ slightly above $\Delta$), so a version restricted to $e_S\ge 0$ would be false. "Optimal" means a global maximizer, with ties allowed; at $a=\bar a_1$ two efforts are optimal and at $H=1/4$ the middle interval is empty.

Trivializing formalizations are ruled out: $\underline a_1$ is pinned by its defining equation rather than chosen, every hypothesis is satisfiable (at $\delta=f=0$, $\beta=1/2$ one has $H=676/9409\le 1/4$), and the sign conditions keep $\Delta$ from collapsing to a junk value of division or square root.

A complete development needs only real analysis of quadratics and polynomial inequalities on a box; contributions of reusable lemmas on maximizing concave quadratics under a threshold constraint are welcome.

Selected references

• L. Qi, H. Song, W. Xiao, Coopetition in Platform-Based Retailing: On the Platform’s Entry, Management Science, 2025. https://doi.org/10.1287/mnsc.2023.00260
• F. Zhu, Q. Liu, Competing with complementors: An empirical look at Amazon.com, Strategic Management Journal 39(10), 2018. https://doi.org/10.1002/smj.2932

Motivation

Retail chains increasingly run their physical stores and online channels as one network. A customer who walks into a store and finds nothing she wants can be shown products stocked in other stores of the chain, to be shipped or picked up later. This raises a basic assortment question: when every store can point its customers to the rest of the network, should the stores still carry the assortment each would choose on its own, or should they coordinate?

Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) compare two ways of showing the network's products. Under simultaneous recommendation (SMR), a customer sees her store's products and the other stores' products at the same time. Under sequential recommendation (SQR), she sees the other stores' products only after declining everything in her own store. This mission formalizes the paper's result for SMR, Theorem 1, together with the lemmas of its proof and two consequences (Theorem 5(a) and Proposition 2). The single-store model it builds on is the multinomial logit (MNL) assortment problem of Talluri and van Ryzin (2004).

Setting

A seller operates $m$ stores and sells $n$ products, indexed $1,\dots,n$, with revenues $r_1>r_2>\dots>r_n>0$. Product $k$ has attraction value $v_k=\exp(u_k)>0$, where $u_k$ is its utility; the no-purchase option has attraction value $1$. A fraction $\lambda_i\ge0$ of customers first visits store $i$, and $\sum_i\lambda_i=1$.

An assortment profile $\mathbf S=(S_1,\dots,S_m)$ lists the set $S_i\subseteq\mathcal N=\{1,\dots,n\}$ offered by each store. Write $\bar S=S_1\cup\dots\cup S_m$ for the products offered somewhere. A customer of store $i$ who buys product $k$ from store $j$ suffers a utility discount $c_{ij}^k\ge0$, with $c_{ii}^k=0$. She buys from the cheapest store that offers $k$, so the effective discount is $c_i^k(\mathbf S)=\min\{c_{ij}^k: k\in S_j\}$, and $c_i^k(\mathbf S)=\infty$ if no store offers $k$.

Under SMR, the customer of store $i$ chooses product $k$ with the MNL probability

$$p^M_{ik}(\mathbf S)=\begin{cases}\dfrac{v_k}{D_i(\mathbf S)},&k\in S_i,\\[2mm]\dfrac{v_ke^{-c_i^k(\mathbf S)}}{D_i(\mathbf S)},&k\in\bar S\setminus S_i,\\[2mm]0,&\text{otherwise},\end{cases}\qquad D_i(\mathbf S)=1+\sum_{l\in S_i}v_l+\sum_{l\in\bar S\setminus S_i}v_le^{-c_i^l(\mathbf S)}.$$

The seller's problem is

$$\max_{\mathbf S}\ R_M(\mathbf S)=\sum_{i=1}^m\lambda_i\sum_{k=1}^nr_k\,p^M_{ik}(\mathbf S).\tag{SMR}$$

The single-store problem is

$$R^*=\max_{S\subseteq\mathcal N}\frac{\sum_{k\in S}r_kv_k}{1+\sum_{k\in S}v_k}.\tag{3}$$

An assortment is revenue-ordered if it is $\{1,\dots,k\}$ for some $k\in[n]$. The paper writes $\tilde S$ for the smallest revenue-ordered optimal solution of (3).

Formalization targets

Goal: Theorem 1

$$R_M(\mathbf S)\ \le\ R_M(\tilde S,\tilde S,\dots,\tilde S)\qquad\text{for every profile }\mathbf S.$$

Offering the single-store optimal assortment in every store is optimal under SMR. The goal asserts optimality, not uniqueness: with ties, other profiles can be optimal too.

Milestones

1. Existence of $\tilde S$ (p. 11): some revenue-ordered assortment is optimal for (3).
2. Proposition A.1: in the two-store problem (A.1), store 1 offers products 1 through some threshold. A product belongs to the smallest revenue-ordered optimum if and only if its revenue exceeds the optimal value.
3. Proposition A.2: the optimal value of (A.1) does not decrease when the discounts increase.
4. The store-wise reduction: store $i$'s SMR revenue equals the objective of problem (A.2), the single-store problem with the other stores' products as discounted alternatives.
5. The store-wise bound: every store earns at most $R^*$ under any profile, and exactly $R^*$ under $(\tilde S,\dots,\tilde S)$.

Companions

• Theorem 5(a): $\max_{\mathbf S}R_Q(\mathbf S)\ge\max_{\mathbf S}R_M(\mathbf S)$, where $R_Q$ is the SQR revenue built from the sequential choice probabilities (2).
• Proposition 2: when store $m$ is an online channel with $S_m=\mathcal N$, and $c_{im}^k=c^k>0$ for every physical store $i$, some optimal profile among those with $S_m=\mathcal N$ offers one and the same revenue-ordered assortment $\hat S\supseteq\tilde S$ in every physical store.

Significance

Theorem 1 says that under simultaneous recommendation the network adds nothing for the seller: the revenue of independently run stores, $R^*$, is the best achievable. The paper calls this revenue the benchmark. Every later comparison is made against it. The sequential strategy beats it (Theorem 5(a)), and the paper's structural results on SQR and its ½-approximation are phrased relative to $\tilde S$ and $R^*$. Proposition 2 shows that adding an online channel enlarges the optimal assortments of the physical stores.

The results are proved in the paper, partly in an Additional Supplement. As far as is known, none of them has a machine-checked proof. The mission produces a reusable Lean model of multi-store MNL choice with cross-store discounts, the SQR choice probabilities, and checked proofs of the single-store threshold structure with discounted outside products (Propositions A.1 and A.2).

Difficulty

A store's SMR revenue depends on every other store's assortment, through both the denominator $D_i(\mathbf S)$ and the products of $\bar S\setminus S_i$. The objective does not separate across stores, so the obvious idea of optimizing each store on its own does not directly apply. Products of other stores enter at reduced weight $e^{-c_i^k}$, so the standard MNL result for (3) does not cover (A.1).

Proposition A.1's exchange argument has two cases, depending on whether the added product is already available elsewhere. In the second case the gain is weighted by $1-e^{-c^k}$, which vanishes when $c^k=0$. Proposition A.2 compares optimal values across two discount vectors whose optimal assortments differ.

Formalization scope

Products are Fin n (the paper's product $k$ is index $k-1$), stores are Fin m, and a profile is a function Fin m → Finset (Fin n). The attraction values $v_k>0$ are the primitive parameters. The discount factor $e^{-c_i^k(\mathbf S)}$ is the largest $e^{-c_{ij}^k}$ over the offering stores, and $0$ when none offers $k$. In (A.1) the discounts are encoded by the factors $\beta_k=e^{-c^k}\in[0,1]$, with $\beta_k=0$ for $c^k=\infty$. $\tilde S$ and $S^*_M(\mathbf c)$ are predicates: revenue-ordered (hence nonempty), optimal, and of least cardinality among revenue-ordered optima. "Optimal" means a global maximizer, and comparisons of optimal values are written as "for every $T$ there is an $S$ with $f(T)\le g(S)$", with no maximum operator. The SMR and SQR objectives are written from the choice probabilities (1) and (2), exactly as the paper writes them.

The standing assumptions are explicit hypotheses: $\lambda_i\ge0$, $\sum_i\lambda_i=1$, $r$ strictly decreasing, $v_k>0$, $c_{ij}^k\ge0$, $c_{ii}^k=0$. Two hypotheses are pinned. The first is $r_k>0$: revenues are prices, which the paper uses but never states as a sign condition. The second applies only to the second part of Proposition A.1: $c^k>0$, because its "if and only if" fails at $c^k=0$; the existence of a revenue-ordered optimum is stated for every $\mathbf c\ge0$. The goal and Proposition A.2 keep $c_{ij}^k\ge0$, so zero cross-store discounts are allowed. The Gumbel derivation of (2) (Proposition 1, cited from Gao et al. 2021) is not formalized; (1) and (2) are the model.

The hypothesis on $\tilde S$ is satisfiable: its existence is the first milestone. A statement that assumed some optimal profile, or that defined $R^*$ through a junk-valued supremum, would be trivial or vacuous, and the formalization avoids both. Contributions are welcome on any milestone. Propositions A.1 and A.2 are reusable for other multi-store and omnichannel MNL problems.

Selected references

• Y. Liu, X. A. Chen, Y. Liu, Z. Wan, Simultaneous vs. Sequential: Optimal Assortment Recommendation in Multistore Retailing, Manufacturing & Service Operations Management, 2025. https://doi.org/10.1287/msom.2024.0761 (cited from the authors' manuscript of 2024-09-17 with its Online and Additional Supplements)
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Gao, Y. Ma, N. Chen, G. Gallego, A. Li, P. Rusmevichientong, H. Topaloglu, Assortment Optimization and Pricing Under the Multinomial Logit Model with Impatient Customers: Sequential Recommendation and Selection, Operations Research 69(5):1509–1532, 2021.

Motivation

Optimal control of partial differential equations under uncertainty asks for a single deterministic control $u$ that performs well when the data of the PDE are random. When a constraint on the state must hold, the modeller has to decide how strictly: with high probability (a probabilistic constraint), for almost every realization (an almost-sure constraint), or for every realization in a support set (a robust constraint). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for all three forms on a common model problem. This mission covers §3.1 of that paper, the almost-sure case.

Almost-sure state constraints are the natural model when a bound (a temperature, a stress, a concentration) must never be violated, and they appear throughout risk-averse PDE-constrained optimization (Geiersbach and Wollner, SIAM J. Optim. 2021; Geiersbach and Hintermüller, ESAIM:COCV 2022). Their difficulty is functional-analytic: the constraint lives in $L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D))$, a space whose dual is not a function space, so Lagrange multipliers are a priori only finitely additive objects.

Setting

Let $D\subseteq\mathbb R^d$, $d\in\{1,2,3\}$, be open, bounded and of class S: there are $\gamma\in(0,1)$ and $r_0>0$ with $\operatorname{meas}(B_r(x)\setminus D)\ge\gamma\operatorname{meas}(B_r(x))$ for all $x\in\partial D$ and $0<r<r_0$. For $F\in L^2(D)$ the Dirichlet problem $-\Delta y=F$ in $D$, $y=0$ on $\partial D$ has a unique weak solution $y\in H^1_0(D)\cap\mathcal C(\bar D)$; the solution map is a continuous linear operator $A^{-1}:L^2(D)\to\mathcal C(\bar D)$.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $\tilde f\in L^\infty_{\mathbb P}(\Omega,L^2(D))$ a random source. For a control $u\in L^2(D)$ the random state $y(\cdot,\omega)$ solves $-\Delta y(\cdot,\omega)=u+\tilde f(\cdot,\omega)$, $y(\cdot,\omega)=0$ on $\partial D$. With $\mathcal B$ the embedding of $L^2(D)$ into constant elements of $L^\infty_{\mathbb P}(\Omega,L^2(D))$ and $[\mathcal A^{-1}y](\omega)=A^{-1}y(\cdot,\omega)$, the control-to-state operator is $\mathcal S(u)=\mathcal A^{-1}(\mathcal Bu+\tilde f)$ and the constraint map is $\mathcal G(u)=\mathcal S(u)-\boldsymbol\alpha$, where $\boldsymbol\alpha$ is the constant function $\alpha\in\mathbb R$. The problem is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad\mathcal G(u)\in\mathcal K,\qquad(51)$$

with the cone $\mathcal K=\{y\in L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)):y(x,\omega)\le0\text{ on }\bar D,\ \mathbb P\text{-a.s.}\}$ and its polar $\mathcal K^-\subseteq(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$. The cost $F$ is convex and continuously Fréchet differentiable.

For a separable Banach space $X$, a functional $v\in(L^\infty_{\mathbb P}(\Omega,X))^*$ is absolutely continuous if $\langle v,x\rangle=\int_\Omega\langle x^*(\omega),x(\omega)\rangle\,d\mathbb P$ for a weakly measurable $x^*:\Omega\to X^*$ with $\int\|x^*\|\,d\mathbb P<\infty$ (the set $\Lambda_1(X^*)$ of such $x^*$), and singular if it vanishes on every $x$ that vanishes on some $F_n$, for a decreasing sequence of events with $\mathbb P(F_n)\to0$ (the set $\Lambda_\circ(X^*)$).

Formalization targets

Goal: Theorem 3.10

Under the constraint qualification $0\in\operatorname{int}\{\mathcal G(L^2(D))-\mathcal K\}$, $u^*$ solves (51) if and only if there are $\lambda\in\Lambda_1(\mathcal C(\bar D)^*)$, $\lambda^\circ\in\Lambda_\circ(\mathcal C(\bar D)^*)$ and a state $y^*$ with

$$DF(u^*)+\mathbb E[A^{-*}\lambda]+\mathcal B^*\mathcal A^{-*}\lambda^\circ=0,\qquad Ay^*(\cdot,\omega)=u^*+\tilde f(\cdot,\omega),$$ $$y^*(\cdot,\omega)\le\alpha,\quad\lambda(\cdot,\omega)\ge0,\quad\langle\lambda(\cdot,\omega),y^*(\cdot,\omega)-\boldsymbol\alpha\rangle=0\ \ \mathbb P\text{-a.s.},\qquad\lambda^\circ\in\mathcal K^-,\quad\langle\lambda^\circ,y^*-\boldsymbol\alpha\rangle=0.$$

Milestones

1. Lemma 3.6: the random state exists, is a.s. unique, lies in $L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D))$, and obeys the bound (52).
2. Lemma 3.7: the abstract KKT system (53) with a multiplier $\lambda^*\in(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$.
3. Theorem 3.9 (Ioffe–Levin): every $v^*\in(L^\infty_{\mathbb P}(\Omega,X))^*$ splits uniquely as $v^a+v^\circ$ with $\|v^*\|=\|v^a\|+\|v^\circ\|$.
4. The splitting $\langle\lambda^*,\mathcal A^{-1}\mathcal Bh\rangle=\mathbb E[\langle\lambda,A^{-1}h\rangle]+\langle\lambda^\circ,\mathcal A^{-1}\mathcal Bh\rangle$.
5. (57): $\lambda^*\in\mathcal K^-$ passes to both parts.
6. (59) and pointwise complementarity: $\lambda(\omega)\ge0$ and $\langle\lambda(\omega),y^*(\omega)-\boldsymbol\alpha\rangle=0$ almost surely.

Significance

The result. Lemma 3.7 gives a multiplier in the dual of $L^\infty$, which cannot be evaluated scenario by scenario. Theorem 3.10 shows that, for this problem, the multiplier consists of an honest random variable $\lambda(\omega)\in\mathcal C(\bar D)^*$ (a random signed measure on $\bar D$) satisfying sign and complementarity conditions for almost every realization, plus a singular remainder. This is the form needed to write adjoint equations and to design discretizations and algorithms (Proposition 3.12 of the paper). As Remark 3.11 notes, the derivation does not require reflexivity of the state space, unlike earlier work on $L^\infty_{\mathbb P}(\Omega,X)$-constraints.

Formalizing it. The paper's argument is complete, but it rests on two cited results: the regularity theory behind Lemma 1.2/3.6 (Stampacchia-type continuity of weak solutions on class-S domains, Kinderlehrer–Stampacchia) and the Ioffe–Levin decomposition of $(L^\infty_{\mathbb P}(\Omega,X))^*$ (Ioffe–Levin, Appendix 1, Theorem 3, and Levin 1974). Neither is in Mathlib. A formal development produces machine-checked versions of both, of a Robinson-type KKT theorem in Banach spaces, and of the multiplier refinement itself. None of these results has a machine-checked proof as far as the platform's catalog shows.

Difficulty

The obvious route is to apply the Riesz representation pointwise in $\omega$. It fails: $(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$ contains purely finitely additive functionals that are not given by any integrand, so $\lambda^*$ has no density in general. The decomposition theorem isolates them, and the proof of Theorem 3.10 must then show that the sign condition $\lambda^*\in\mathcal K^-$ and the complementarity condition pass to each part separately. The step from $\mathbb E[\langle\lambda,y\rangle]\le0$ for all $y\in\mathcal K$ to "$\lambda(\omega)\ge0$ for almost every $\omega$, simultaneously for all nonnegative test functions" requires the separability of $\mathcal C(\bar D)$; a version with a null set depending on the test function is weaker and is not the statement. Lemma 3.6 needs $\mathcal C(\bar D)$-regularity of weak solutions, which is where class S and $d\le3$ enter.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $L^2(D)$ is Lp ℝ 2 (volume.restrict D) and $L^\infty_{\mathbb P}(\Omega,X)$ is Lp X ⊤ P; their elements are a.e. classes, so every pointwise statement in $\omega$ is stated $\mathbb P$-a.s. $\mathcal C(\bar D)$ is C(closure D, ℝ) with [CompactSpace (closure D)] as an instance argument (implied by boundedness). Weak derivatives use the published HunterPDE.Shared.HasWeakDeriv; a weak solution in $H^1_0(D)\cap\mathcal C(\bar D)$ is encoded as continuity on $\bar D$, zero boundary values, $L^2$ weak gradient and the weak form. $A^{-1}$ is a hypothesis: a continuous linear map $L^2(D)\to\mathcal C(\bar D)$ whose values are weak solutions. "$\le0$ a.e. in $D$" for a function continuous on $\bar D$ is read as "$\le0$ on $\bar D$"; "$\lambda(\cdot,\omega)\ge0$" as positivity of the functional. "Solution of (51)" is a global minimizer. (56a) is stated applied to every direction $h$.

Trivializing formalizations are ruled out: the state operator is tied to the PDE, not an arbitrary bounded operator; the multipliers carry their sign and complementarity conditions; absolutely continuous functionals require a weakly measurable, integrable density; singular functionals are concentrated on a decreasing sequence of events of vanishing probability, not merely "not absolutely continuous"; optimality is global.

Needed infrastructure: Lax–Milgram on $H^1_0(D)$ and continuity of weak solutions (Lemma 3.6); a KKT theorem under Robinson's constraint qualification (Lemma 3.7); the Yosida–Hewitt decomposition for finitely additive measures and a weak*-measurable representation of $L^1(\Omega,X)^*$ (Theorem 3.9). The decomposition theorem is reusable far beyond this mission; contributions toward any of these are welcome.

Selected references

• C. Geiersbach, R. Henrion, Optimality conditions in control problems with random state constraints in probabilistic or almost-sure form, arXiv:2306.03965v2, 2024; Math. Oper. Res. 2025. https://arxiv.org/abs/2306.03965
• A. D. Ioffe, V. L. Levin, Subdifferentials of convex functions, Trudy Moskov. Mat. Obshch. 26, 3–73, 1972 (Appendix 1, Theorem 3).
• V. L. Levin, The Lebesgue decomposition for functionals on the vector-function space $L^\infty_X$, Funct. Anal. Appl. 8(4), 314–317, 1974. https://doi.org/10.1007/bf01075488
• K. Yosida, E. Hewitt, Finitely additive measures, Trans. Amer. Math. Soc. 72, 1952. https://doi.org/10.1090/S0002-9947-1952-0045194-X
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• C. Geiersbach, W. Wollner, Optimality conditions for convex stochastic optimization problems in Banach spaces with almost sure state constraints, SIAM J. Optim. 31(4), 2455–2480, 2021.
• C. Geiersbach, M. Hintermüller, Optimality conditions and Moreau–Yosida regularization for almost sure state constraints, ESAIM: COCV 28, Paper No. 80, 2022. https://doi.org/10.1051/cocv/2022070
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980 (Chapter II, Appendices B and C). https://doi.org/10.1137/1.9780898719451

Motivation

Small third-party sellers on e-commerce marketplaces often lack working capital to buy inventory. Two financing channels compete for them. Under trade credit, the supplier ships now and is paid after sales, bearing the seller's default risk. Under platform financing, the marketplace itself (Amazon Lending, Alibaba's microloans, JD's supply-chain finance) lends the seller the purchase cost at an interest rate it chooses, the supplier is paid upfront, and the platform bears the default risk. A platform that already earns a commission on every sale has a reason to lend that a bank does not: cheaper credit raises orders, and higher orders raise commission income.

R. Huang, G. Lai, X. Wang and W. Xiao study this in Platform Financing vs. Trade Credit for Lending to Third-Party Sellers (Management Science, 2024). Their §5 asks how a platform that can set its loan rate freely would set it. The answer at low demand uncertainty is a clean dichotomy in the production cost: the platform lends at exactly its own capital cost when cost is low, and strictly below its capital cost, subsidizing the loan, when cost is high. This mission formalizes that result, Proposition 8, together with the equilibrium analysis it rests on.

The source is the authors' manuscript on SSRN (abstract 4014045, titled Lending to Third-party Sellers with Platform Loan); every page and label below refers to that manuscript, not to the typeset journal article.

Setting

A seller with no capital buys $q \ge 0$ units from a supplier whose unit production cost is $c > 0$, and sells all of them on a platform at the market-clearing price $p = \tilde a - q$. The market size $\tilde a$ is uniform on $[a - \delta, a + \delta]$ with $0 < \delta < a$; $\delta$ measures demand uncertainty. The platform keeps a share $\varphi \in [0, 1)$ of revenue and passes $(1 - \varphi)pq$ to the seller. The supplier and the platform both have capital cost equal to the risk-free rate $r_f \ge 0$, and selling is profitable in expectation: $(1 - \varphi)a > c(1 + r_f)$.

Under platform financing at loan rate $r > -1$, the game has two stages after $r$ is fixed:

1. the supplier sets an upfront wholesale price $w$ and receives $(w - c)q(1 + r_f)$ in value;
2. the seller, having seen $w$, borrows $wq$ from the platform and chooses $q$ to maximize $\mathbb E\big[((1 - \varphi)(\tilde a - q)q - wq(1 + r))^+\big]$.

The seller has limited liability: if revenue $(1 - \varphi)(\tilde a - q)q$ falls short of the debt $wq(1 + r)$, she hands over all of it. The platform's profit is

$$\Pi^P_p = \mathbb E\big[\varphi(\tilde a - q)q + \min\{(1 - \varphi)(\tilde a - q)q,\ wq(1 + r)\}\big] - wq(1 + r_f).$$

A subgame-perfect equilibrium at rate $r$ is a price $w$ and an order rule $w' \mapsto q(w')$ such that the rule is a best response for the seller at every price, the supplier's price is optimal against the rule, and ties are broken as in the paper. The paper also defines a threshold rate $\hat r_1(\delta)$ (p. 15) below which the seller prefers platform financing to trade credit; the platform chooses $r$ subject to the participation constraint $r \le \hat r_1(\delta)$. Write

$$\delta_2 = \frac{(1 - \varphi)a - c(1 + r_f)}{(2 + \sqrt6)(1 - \varphi)}, \qquad \bar c = \frac{a(1 - \varphi)^2}{1 + r_f}.$$

Formalization targets

Goal: Proposition 8 (p. 22)

Let $\Pi^P_p(r)$ be the platform's profit in a subgame-perfect equilibrium of the stage game at rate $r$, for an arbitrary choice of equilibrium at each feasible rate. If $\delta \le \delta_2$, then

$$c \le \bar c \implies r^* = r_f \text{ is the unique maximizer of } \Pi^P_p \text{ on } \{-1 < r \le \hat r_1(\delta)\},$$ $$c > \bar c \implies \text{a maximizer exists, and every maximizer } r^* \text{ satisfies } r^* < r_f.$$

Milestones

1. Lemma 2 (p. 13): the seller's unique best response to $(w, r)$, with a no-default branch and a default branch.
2. Proposition 2 (p. 13): the stage game has an equilibrium, and in every equilibrium $w^P$ and $q^P$ have the stated closed forms, switching at $\delta_r = \frac{a(1-\varphi) - c(1+r)}{(2+\sqrt6)(1-\varphi)}$.
3. (10) (pp. 35, 41): for $\delta \le \delta_r$, the platform's equilibrium profit is an explicit rational function of $r$.
4. The derivative (p. 43): $\partial \Pi^P_p(r)/\partial r = G_1(r)/(8(1-\varphi)^2(1+r)^2)$ with an explicit cubic $G_1$.
5. Case (a) (p. 43): $c \le \bar c$ implies $G_1 \ge 0$ on $(-1, r_f]$.
6. Case (b) (p. 43): $c > \bar c$ implies $G_1$ is nonnegative up to some $r_7 < r_f$ and negative on $(r_7, r_f]$.

Significance

The result separates two motives for platform lending. At low cost the platform gains nothing by undercutting its own capital cost, so the loan is priced at cost; at high cost the commission earned on the extra units ordered outweighs the interest forgone, so the platform subsidizes. The threshold $\bar c$ is explicit and depends only on the mean market size, the commission share and the risk-free rate. Together with Proposition 7 of the same paper (whether the platform gains relative to trade credit), it is the paper's account of why marketplaces lend below market rates.

The proof in the paper is a chain of closed-form computations whose final steps are stated as "it can be verified". A formalization checks that chain end to end: the equilibrium of a limited-liability Stackelberg game with uniform demand, the reduction of the platform's objective to (10), and the sign analysis of $G_1$. To our knowledge none of these steps has been machine-checked. The model file (uniform expectation, limited-liability payoffs, the equilibrium predicate with tie-breaks) is reusable for the two sister missions on the same paper and for other supply-chain-finance models with a uniform market-clearing price.

Difficulty

The objective is defined through an equilibrium, not a formula. The obvious approach, substituting the closed forms of Proposition 2 into the platform's profit, presupposes that every equilibrium has those closed forms; establishing this means solving the seller's piecewise problem (whose objective changes form where default becomes possible), then the supplier's problem over a piecewise best response, and handling the indifference point $\delta = \delta_r$. Only then does the problem reduce to the one-variable function (10).

On that function, the low-cost case requires a polynomial inequality on a half-open interval in four parameters, and uniqueness needs strict monotonicity, not just a nonnegative derivative. The high-cost case requires both a single sign change of a cubic on $(-1, r_f]$ and the existence of a maximizer on a set that is open at $-1$, where the profit tends to $-\infty$.

Formalization scope

All objects live in the namespace PlatformFinance.EndogRate. Conventions committed to:

• The expectation over $\tilde a$ is $\frac{1}{2\delta}\int_{a-\delta}^{a+\delta}$, an interval integral of a continuous integrand.
• The standing assumptions are hypotheses: $0 < \delta$, $\delta < a$ (the reading of p. 8's "the smallest market size $a - \delta$ is large enough so that the market clearing price is always positive"), $0 \le \varphi < 1$ (the page allows $\varphi = 1$, which $(1 - \varphi)a > c(1 + r_f)$ excludes), $c > 0$, $r_f \ge 0$, $(1 - \varphi)a > c(1 + r_f)$, and for platform financing $r > -1$ and $c(1 + r) < (a + \delta)(1 - \varphi)$ (conditions (iii) and (ii), p. 36).
• The equilibrium carries the paper's two tie-breaks: a seller who cannot earn a positive expected profit orders zero (proofs on pp. 31, 33), and the supplier's equilibrium price is the least optimal one (which puts $\delta = \delta_r$ in Proposition 2's first branch).
• The goal quantifies over an arbitrary family of equilibria, one per feasible rate; Proposition 2 shows such a family exists. The feasible set is $\{r : -1 < r \le \hat r_1(\delta)\}$ with $\hat r_1$ the paper's closed form on p. 15.
• Lemma 2 assumes $w(1 + r) < (1 - \varphi)(a + \delta)$: above it every order earns zero and the maximizer is not unique; the paper's proof restricts to this range.

Corrections relative to the page: (10) is printed under the heading "the equilibrium profits under trade credit" on p. 35, a slip for platform financing; Proposition 8 states $\delta \le \delta_2$ while its proof writes $\delta < \delta_2$, and the statement follows Proposition 8.

A trivializing formalization is ruled out: the goal is stated about the platform's equilibrium profit, not about the closed form (10), and the high-cost clause asserts existence of a maximizer so that "every maximizer is below $r_f$" cannot hold vacuously.

Needed infrastructure: interval integrals of piecewise polynomials, optimization of one-variable piecewise functions, and real-polynomial sign arguments. Proofs of any milestone are welcome, as are alternative proofs of the cubic sign analysis.

Selected references

• R. Huang, G. Lai, X. Wang, W. Xiao, Lending to Third-party Sellers with Platform Loan, SSRN manuscript 4014045. https://ssrn.com/abstract=4014045
• R. Huang, G. Lai, X. Wang, W. Xiao, Platform Financing vs. Trade Credit for Lending to Third-Party Sellers, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.00201

Motivation

Many service systems do not receive random, memoryless traffic: customers are given appointments. Outpatient clinics, airport runways, container terminals and delivery slots all schedule arrivals on a regular grid, and the actual arrival deviates from the appointment by a random lateness or earliness. A queue fed by such scheduled traffic is a basic model for these systems, going back to Winsten (1959) and Mercer (1960, 1973), and Chen and Zhao (1997) used it with deterministic service times to model aircraft landings, proving stability under bounded perturbations.

Classical queueing theory says that a single-server queue fed by stationary traffic is stable when the mean work brought per unit time is below the service rate, and unstable when it is above (Loynes 1962). The boundary case, critical loading, is unstable for renewal traffic with non-degenerate interarrival times: the workload grows like $\sqrt t$. Araman and Glynn ask what happens at critical loading when the traffic is scheduled and every customer brings the same amount of work, and show that the answer depends only on the right tail of the arrival perturbations.

Timeline. Winsten (1959) and Mercer (1960, 1973) analysed queues with scheduled arrivals and obtained waiting-time distributions in implicit form. Loynes (1962) proved the stability dichotomy for stationary input. Kingman (1962) showed that the heavy-traffic limit of the S/G/1 queue coincides with that of D/G/1 when perturbations are positive with finite mean. Chen and Zhao (1997) studied the S/D/1 queue with bounded perturbations. Araman and Glynn (2012) obtained a fractional-Brownian functional limit for scheduled traffic with infinite-mean perturbations, and Araman, Chen, Glynn and Xia (2022) showed that S/D/1 queues with Pareto-like perturbations behave unlike D/D/1 and G/D/1 queues. The present note (arXiv 2022; Operations Research technical note, 2025) settles stability at critical loading.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathbb P)$ and a scheduling interval $h>0$. Customer $j\in\mathbb Z$ is scheduled at time $jh$. Its perturbation $\xi_j$ is a real random variable, and the $\xi_j$ are independent and identically distributed with $\mathbb E|\xi_0|<\infty$. A uniform shift $U$, uniform on $[0,1]$ and independent of $\xi=(\xi_j)_{j\in\mathbb Z}$, makes the arrival process stationary. Customer $j$ arrives at

$$A_j = jh + hU + \xi_j ,$$

and for $t\ge0$ the arrival count is $N(t)=\#\{j : A_j\in(0,t]\}$, so $N(0)=0$.

A single server works at unit rate and every customer brings exactly $h$ units of work (the S/D/1 queue; "D" for deterministic service $V_j=h$). Since one customer is scheduled per $h$ time units, the queue is critically loaded. The system is empty at time $0$, and the workload at time $t\ge0$ is

$$W(t)=\sup_{0\le s\le t}\Big(h\big(N(t)-N(s)\big)-(t-s)\Big).$$

The proof runs in reversed time. With reversed arrival times $R_j = jh+Uh-\xi_j$, let

$$\Lambda(s)=h\cdot\#\{j: R_j\in(0,s]\},\qquad M(t)=\sup_{0\le s\le t}\big(\Lambda(s)-s\big).$$

Write $\xi_0^+=\max(\xi_0,0)$. "$\xi_0^+$ is a bounded random variable" means that $\xi_0\le c$ almost surely for some constant $c$.

Formalization targets

Goal: Theorem 1

$$\exists\,W(\infty)\ \text{finite-valued with}\ W(t)\Rightarrow W(\infty)\ (t\to\infty)\quad\Longleftrightarrow\quad \exists c,\ \ \xi_0\le c\ \text{a.s.}$$

The statement makes no assumption beyond the standing model. In particular the left tail of $\xi_0$ is arbitrary (only $\mathbb E\xi_0^-<\infty$).

The steps of the published proof (milestones)

1. Loynes representation: $W(t)\overset{\mathcal D}{=}M(t)$ for each $t\ge0$.
2. Early customers: $\beta_1(s)\le\Gamma_1$ for all $s$ and $\mathbb E\Gamma_1<\infty$.
3. Upper decomposition: $\#\{j : R_j\in(0,s]\}\le\beta_1(s)+\lfloor s/h\rfloor+1+\beta_2(s)$.
4. Late customers under bounded perturbations: if every $\xi_j\le c$, then $\beta_2(s)\le\lfloor c/h\rfloor+1$.
5. Sufficiency: if $\xi_0^+$ is bounded, then $\sup_{s\ge0}(\Lambda(s)-s)<\infty$ a.s.
6. $Y_n<\infty$ for all $n$ and $\Gamma_2<\infty$, a.s.
7. Lower decomposition: $n+\tilde Y_n\le\Lambda(nh)/h+Y_n+\Gamma_2$.
8. Ergodic recurrence: $\frac1n\sum_{j\le n}I(Y_j\le l)\to\mathbb P(Y_0\le l)$ a.s.
9. If $\xi_0^+$ is unbounded, then $\mathbb P(\tilde Y_0>r)>0$ for every $r$.
10. If $\xi_0^+$ is unbounded and $\mathbb P(Y_0\le l)>0$, then $Y_n\le l$ and $\tilde Y_n>r$ for infinitely many $n$, a.s.
11. Necessity: if $\xi_0^+$ is unbounded, then $\sup_{s\ge0}(\Lambda(s)-s)=\infty$ a.s.

Here $\beta_1,\beta_2$ count reversed arrivals in $(0,s]$ of customers $j\le-1$ and $j\ge\lfloor s/h\rfloor+1$; $\Gamma_1,\Gamma_2,Y_n,\tilde Y_n$ are the counts $\sum_{j\ge1}I(-\xi_{-j}>(j-1)h)$, $\sum_{j\ge1}I(\xi_j\ge(j-1)h)$, $\sum_{j\ge1}I(-\xi_{n+1-j}>(j-2)h)$ and $\sum_{j\ge1}I(\xi^+_{n+j}\ge(j+2)h)$.

Significance

The result. Theorem 1 shows that, unlike renewal traffic, scheduled traffic can keep a critically loaded queue stable, and it identifies exactly when: only late arrivals (the right tail of $\xi_0$) can destabilise the queue, while arbitrarily early arrivals cannot. For appointment systems this says that a server whose capacity exactly matches the schedule has a finite stationary backlog precisely when lateness is bounded, so tardiness, not earliness, determines whether waiting times stay bounded. It complements Corollary 1 of the same note, a diffusion limit $t^{-1/2}W(t)\Rightarrow\sigma X(1)$ for random service times at critical loading.

Formalizing it. The theorem is proved in the paper, but its proof contains several misprints: an identity that omits a term and has an infinite summand, a bound with a wrong constant, a sign error in $Y$, a false inequality $\beta_2(s)\ge\tilde Y_{k(s)}$, and a conditional Borel–Cantelli step applied to non-adapted events. The milestones of this mission state the corrected inequalities, each checked by hand on small instances. A machine-checked proof would settle the argument. No part of it is formalized anywhere at present.

Difficulty

The forward workload $W(t)$ is not monotone in $t$, so its convergence cannot be read off from its paths; the proof needs the time reversal to a monotone running maximum $M(t)$, and the reversal of a perturbed lattice requires its stationarity under the uniform shift. In the unstable direction the obvious first idea is to show that $\Lambda(s)-s$ is large for a fixed large $s$. That fails: for each fixed $s$ the overshoot is a tight random variable. Large values occur only along random times at which many customers just after $s$ are very late while few customers just before $s$ are very early, and producing infinitely many such times needs an ergodic or Borel–Cantelli argument over a dependent stationary sequence. Mathlib has no pointwise ergodic theorem and no conditional Borel–Cantelli lemma, so this step needs new infrastructure.

Formalization scope

All declarations live in the namespace ScheduledQueue.Stability. The standing model is a bundle ScheduledInput P ξ U (measurable, i.i.d. via iIndepFun and IdentDistrib, Integrable (ξ 0), HasLaw U uniform on $[0,1]$, and independence of U from the whole sequence). Customers are indexed by ℤ, time by ℝ, and $t\to\infty$ is the atTop filter on ℝ. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is a probability measure on $\mathbb R$.

Conventions that differ from the printed page:

• the workload is $\sup_{0\le s\le t}(h(N(t)-N(s))-(t-s))$; the printed $\sum_{i=N(s)}^{N(t)}V_i$ counts customer $N(s)$ and would give $W(0)=h\ne0$, contradicting the theorem's hypothesis $W(0)=0$;
• $N$ counts arrivals in half-open intervals $(0,t]$ (the printed closed intervals are not additive; both agree a.s. at fixed times);
• the proof's displays are corrected: the upper decomposition (the page's identity omits $j=0$ and its $\beta_4$ is infinite, and "$M(t)\le\max\beta_1+\max\beta_2$" mixes units), the $\beta_2$ bound ($\lfloor c/h\rfloor+1$ instead of the printed, false $(\lfloor c\rfloor+1)/h$), the sign and range of $Y_n$, and the lower decomposition (the printed $\beta_2(s)\ge\tilde Y_{k(s)}$ is false);
• the Borel–Cantelli milestone states the conclusion ("infinitely many $n$") rather than the stopping times $\tau_i$.

Every count used inside a pointwise inequality is an extended natural number (Set.encard), so that statements such as "$\Gamma_2<\infty$ a.s." are not satisfied by the junk value $0$ of an infinite Set.ncard. The goal's limit is a probability measure on $\mathbb R$, not on the extended reals, because there "$W(t)\Rightarrow\infty$" would also count as convergence. "Bounded" means bounded almost surely, not pointwise. Measurability of $W(t)$ is part of the conclusion of the "if" direction, not a hypothesis.

A complete development needs the stationarity and time reversal of the perturbed lattice point process, tail-sum bounds $\sum_j\mathbb P(X>(j-1)h)\le\mathbb EX/h+1$, a pointwise ergodic theorem for i.i.d. shifts (or a Lévy-type Borel–Cantelli argument), and measurability of suprema over intervals. The ergodic theorem and the reversal lemma are reusable well beyond this mission. Proofs of individual milestones, in any order, are welcome.

Selected references

• V. F. Araman and P. W. Glynn, Stability of a Queue Fed by Scheduled Traffic at Critical Loading, arXiv preprint, 2022; Operations Research (technical note), 2025. https://arxiv.org/abs/2212.04164v1
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781
• H. Chen and Y. J. Zhao, A new queueing model for aircraft landing process, AIAA, 1997. https://doi.org/10.2514/6.1997-3737
• V. F. Araman, H. Chen, P. W. Glynn and L. Xia, On a single server queue fed by scheduled traffic with Pareto perturbations, Queueing Systems 100, 61–91, 2022.
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society, Series B 24(2), 383–392, 1962. http://www.jstor.org/stable/2984229
• A. Mercer, Queues with scheduled arrivals: a correction, simplification and extension, Journal of the Royal Statistical Society, Series B 35(1), 104–116, 1973.
• J. L. Doob, Stochastic Processes, Wiley, 1953.

Motivation

Financial firms owe each other money. When some firms cannot meet their obligations, the payments that actually clear in the network are a fixed point: what a firm can pay depends on what it receives, which depends on what others can pay. Eisenberg and Noe (Management Science, 2001) introduced this clearing model under a fixed pro-rata payment rule. Later work asked what happens when firms choose how to pay their creditors, which turns the clearing problem into a game.

Bertschinger, Hoefer and Schmand (arXiv:1908.01714v3; Mathematics of Operations Research, 2025) study this game in an abstract form, the flow allocation game. Each node of a directed network receives a fixed external supply plus whatever flows in, and decides how to split its total supply among its outgoing edges, subject to edge capacities. Each node wants to maximize its own total outflow (its payments, which in the financial reading is what keeps it solvent). The paper's first main result is that, when strategies rank single units of flow, there is always a strong equilibrium, stable against every coalition, which is at the same time socially optimal for the total flow.

Timeline:

• 2001: Eisenberg and Noe, clearing payments under pro-rata rules, existence of a greatest clearing vector.
• 2018: Csóka and Herings (Management Science): decentralized clearing with integral monotone allocation rules; the feasible flows form a complete lattice (restated for all monotone profiles as Theorem 2 of the present paper).
• 2019–2025: Bertschinger, Hoefer and Schmand, strategic allocation; existence of optimal strong equilibria for unit-ranking strategies (Theorem 9), strong price of anarchy bounded by the min-max cycle length (Theorem 16), hardness results for other welfare functions and for edge-ranking strategies.

Setting

A flow allocation game $\Gamma = (G, (b_v)_{v\in V}, (c_e)_{e\in E})$ consists of a finite directed multigraph $G = (V, E)$, a fixed supply $b_v \in \mathbb N_0$ at each node and a capacity $c_e \in \mathbb N_0$ on each edge. $E^+(v)$ and $E^-(v)$ are the outgoing and incoming edges of $v$, and $c^+_v = \sum_{e\in E^+(v)} c_e$.

Every node is a player. A strategy profile $\mathbf a = (a_e)_{e\in E}$ assigns to each edge an allocation function $a_e : \mathbb N_0 \to \mathbb N_0$: when the tail of $e$ has total supply $y$, it forwards $a_e(y)$ units on $e$. The profile is unit-ranking if for all $y$, $e$, $v$: $a_e(y) \le c_e$ (1); $\sum_{e\in E^+(v)} a_e(y) \le y$ (2); $\sum_{e\in E^+(v)} a_e(y) = \min\{c^+_v, y\}$ (no fraud, (3)); and each $a_e$ is non-decreasing (5). Equivalently, every node ranks the single units of its outgoing capacity.

A flow $\mathbf f \in \mathbb N_0^E$ gives node $v$ the total supply $f_v = b_v + \sum_{e\in E^-(v)} f_e$, and is feasible for $\mathbf a$ if $f_{(v,w)} = a_{(v,w)}(f_v)$ on every edge (4). The clearing state $\hat{\mathbf f}$ of $\mathbf a$ is the coordinatewise supremum of the feasible flows. Player $v$'s utility is $u_v(\mathbf a) = \sum_{e\in E^+(v)} \hat f_e$, and the total flow is $\mathrm{Flow}(\mathbf a) = \sum_{e\in E} \hat f_e$.

A unit-ranking profile $\mathbf a$ is a strong equilibrium if no non-empty coalition $C \subseteq V$ has a joint deviation $\mathbf a'_C$ such that $(\mathbf a'_C, \mathbf a_{-C})$ is unit-ranking and $u_v(\mathbf a'_C, \mathbf a_{-C}) > u_v(\mathbf a)$ for all $v \in C$.

The circulation network $G'$ adds a node $s$, an uncapacitated edge $(v, s)$ and an edge $(s, v)$ of capacity $b_v$ for every $v$. An optimal circulation $f^*$ maximizes the total flow over all edges of $G'$.

Formalization targets

Goal: Theorem 9 (first sentence)

$$\exists\, \mathbf a:\quad \mathbf a \text{ is a strong equilibrium} \ \text{ and } \ \mathrm{Flow}(\mathbf a') \le \mathrm{Flow}(\mathbf a) \text{ for every unit-ranking } \mathbf a'.$$

Milestones (in the order of the proof)

1. Theorem 2 (p. 12, integral version p. 13): for a monotone profile the feasible flows form a non-empty complete lattice; the clearing state is its greatest element.
2. Proposition 5 (p. 17): a feasible flow, with the non-forwarded flow $\max\{0, f_v - c^+_v\}$ sent to $s$, is a circulation of $G'$, and $\sum_v \max\{0, f_v - c^+_v\} = \sum_v b_v$.
3. Proof of Theorem 9, p. 23, first display: an optimal circulation saturates every $(s, v)$ and

$$\sum_{e\in E'} f^*_e = 2\sum_v b_v + \mathrm{Flow}(f^*) \ge 2\sum_v b_v + \mathrm{Flow}(\mathbf a).$$

4. Proof of Theorem 9, p. 23: with thresholds $\tau_e = f^*_e$ and arbitrary rankings, the threshold-ranking profile $\mathbf a^*$ is unit-ranking and its clearing state is $f^*$.
5. Proof of Theorem 9, pp. 23–24: a profitable coalitional deviation from a unit-ranking profile produces a cycle of $G$ on which the new clearing state carries strictly more flow.

Companion: Corollary 12

For every flow-monotone $Q$ (if $\hat{\mathbf f} > \hat{\mathbf f}'$ then $Q(\mathbf a) \ge Q(\mathbf a')$) there is a strong equilibrium maximizing $Q$ over all unit-ranking profiles.

Significance

Strong equilibria rarely exist in network games, and when they do they are usually not efficient. Theorem 9 gives both at once: every unit-ranking game has a strong equilibrium, and one of them maximizes the total flow, so the price of stability for $\mathrm{Flow}$ is $1$. Corollary 12 extends this to every flow-monotone welfare function, including egalitarian welfare, Nash social welfare and the number of solvent firms. In the financial reading, a coalition of firms cannot jointly reorder its payments to make every member better off, and the stable payment pattern can be chosen to clear the largest possible volume of debt.

The results are proved in the paper and, to our knowledge, have no machine-checked proof. Formalizing them yields a reusable Lean development of clearing states (the Knaster–Tarski structure of feasible flows), the circulation representation of feasible flows, and integral maximum circulations with a cycle-augmentation argument. The second mission of this series (strong price of anarchy, Theorem 16) builds on the same model.

Difficulty

The obvious argument fails at the deviation step. After a coalition deviates, the clearing state of the new profile is an implicit object: the greatest fixed point of a map that mixes the deviators' new strategies with everyone else's old ones. Nothing ties it pointwise to the optimal circulation, and comparing utilities alone gives no contradiction, because a deviator's gain can be paid for by flow that appears elsewhere in the network. The increase of flow has to be traced through deviators and non-deviators alike, and the two kinds of node obey different constraints.

A second difficulty is that the threshold profile built from an optimal circulation $f^*$ has clearing state exactly $f^*$. The clearing state is a supremum over all feasible flows, so it is not enough that $f^*$ is feasible. The claim depends on optimality: for a circulation that is not optimal it is false, as a two-node cycle carrying one unit on edges of capacity two already shows.

Formalization scope

All data are natural numbers: supplies, capacities, strategies $a_e : \mathbb N \to \mathbb N$ and flows, as the paper prescribes for unit-ranking games (p. 13). The graph is a finite type of edges with tail and head maps, so multi-edges and self-loops are allowed. A profile is one function on edges. The clearing state is the coordinatewise sSup in $\mathbb N$; the definition does not assume that the supremum is a feasible flow, which is milestone 1. Optimal circulations are optimal among integral circulations, which the paper justifies by integrality of capacities (p. 23). Natural-number subtraction is used only where it is the page's $\max\{0,\cdot\}$.

Coalitions are non-empty. With $C = \emptyset$ the condition "every member strictly gains" holds vacuously and no profile would be a strong equilibrium; the paper reads it the same way (Proposition 4, Proposition 17). Deviations must again be unit-ranking profiles; the broader deviations of Remark 10 are not formalized. The maximization in the goal ranges over all unit-ranking profiles, not over threshold-ranking ones. A goal maximizing only over threshold profiles, or one that drops the optimality conjunct, is a strictly weaker theorem and is ruled out.

Out of scope: the second sentence of Theorem 9 (polynomial-time computation and polynomial-space representation) and the polynomial-space sentence of Corollary 12. Both need a model of computation. The threshold representation behind them is milestone 4.

A complete development needs: Knaster–Tarski on a finite product of intervals (Mathlib's OrderHom fixed-point lattice), flow conservation bookkeeping on finite multigraphs, existence of integral optimal circulations, and extraction of a cycle from an infinite backward walk in a finite graph. The last two are reusable beyond this mission. Proofs of any milestone, and sorry-free lemmas about clearing states, are welcome.

Selected references

• N. Bertschinger, M. Hoefer, D. Schmand, Flow Allocation Games, Mathematics of Operations Research, 2025. Preprint arXiv:1908.01714v3, 2023. https://arxiv.org/abs/1908.01714v3
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• P. Csóka, P. J.-J. Herings, Decentralized Clearing in Financial Networks, Management Science 64(10), 4681–4699, 2018. https://doi.org/10.1287/mnsc.2017.2847
• A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2), 285–309, 1955. https://doi.org/10.2140/pjm.1955.5.285