Optimization

Why the topology of payment-channel networks matters

The Lightning Network (LN) is a second-layer payment system for Bitcoin. Instead of recording every payment on the blockchain, two parties lock funds in a payment channel and settle many payments off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it carries. Which channel topology supports a given pattern of payments at least total cost is therefore an economic design question for the network's participants.

Guasoni, Huberman and Shikhelman (SSRN 4439190, 2023; published in Management Science, 2024) study this question for a general cost function, assuming only a few qualitative properties derived in their earlier work on channel economics ([GHS22], Lightning Network Economics: Channels). This mission covers §3.1 of the paper, local channel reconfiguration: a relaying node can be bypassed at lower cost, odd cycles are never optimal, and a cost-minimizing network is bipartite with every net flow going from one side to the other. Three companion missions (II–IV of this series) cover hermetization by a routing hub (§3.2) and bounds on the global minimal cost (§3.3).

Setting

Let $V$ be a finite set of nodes. A payment flow is a vector $F=(f_i)_{i\in V}$ of net flows with $\sum_i f_i=0$. A Lightning Network on $V$ is an anti-symmetric real matrix $\Lambda=(\lambda_{u,v})_{u,v\in V}$, $\lambda_{u,v}=-\lambda_{v,u}$, where $\lambda_{u,v}$ is the net flow from $u$ to $v$ in the channel between them and $\lambda_{u,v}=0$ means there is no channel. The network supports $F$ if

$$\sum_{j\in V}\lambda_{i,j}=f_i\qquad\text{for every } i\in V .$$

A channel cost function is $c:\mathbb R\to\mathbb R_{\ge0}$ with

• (MO) $c(x)>c(y)$ for $x>y\ge 0$;
• (SY) $c(-x)=c(x)$;
• (CI) $c(0)=0$;
• (SA) $c(x+y)<c(x)+c(y)$ for $x,y>0$.

The cost of a network is $c(\Lambda)=\tfrac12\sum_{i,j}c(\lambda_{i,j})$, the sum of $c$ over its channels. A network is cost-minimizing for $F$ if it supports $F$ and no Lightning Network on the same node set $V$ that supports $F$ has smaller cost.

The paper's channel notation: $\overrightarrow{uv}^{\lambda}$ is a channel with net flow $\lambda$ from $u$ to $v$, and ${}^{a}\overleftrightarrow{xy}^{b}$ is a channel in which $y$ sends $a$ and $x$ sends $b$, so the net flow from $x$ to $y$ is $b-a$.

Formalization targets

Goal: Corollary 3.3

If $\Lambda$ is cost-minimizing for $F$, there is a set $A\subseteq V$ with $B=V\setminus A$ such that the channel graph ($i\sim j$ iff $\lambda_{i,j}\ne0$) is bipartite with parts $A,B$, and

$$\lambda_{i,j}>0\ \Longrightarrow\ i\in A,\ j\in B .$$

The statement is conditional and does not assert that a minimizer exists.

Milestones

1. Theorem 3.1. For distinct $u,v,w$ and $\lambda_1,\lambda_2>0$, the structure $\overrightarrow{uv}^{\lambda_1},\overrightarrow{vw}^{\lambda_2}$ is not cost-minimizing; if $\lambda_1\le\lambda_2$ the structure $\overrightarrow{uw}^{\lambda_1},{}^{\lambda_1}\overleftrightarrow{vw}^{\lambda_2}$ supports the same flow at strictly lower cost, and if $\lambda_1\ge\lambda_2$ so does ${}^{\lambda_2}\overleftrightarrow{uv}^{\lambda_1},\overrightarrow{uw}^{\lambda_2}$.
2. The in-and-out claim (proof of Corollary 3.2). In an arbitrary network supporting $F$, if $\lambda_{u,v}>0$ and $\lambda_{v,w}>0$ for some $u,v,w$, the network is not cost-minimizing.
3. Corollary 3.2. A network containing a cycle of odd length is not cost-minimizing.
4. Corollary 3.11 (a sibling corollary of Theorem 3.1, not on the path to the goal). If $f_{i_1},f_{i_2}>0>f_{j_1},f_{j_2}$ for distinct $i_1\ne i_2$, $j_1\ne j_2$, no star network is cost-minimizing.

Significance

Corollary 3.3 says that in an optimal Lightning Network every node is a pure sender or a pure receiver, and that no node relays payments. This sits in tension with the observed LN, which is organized around large routing hubs; the paper reconciles the two in §3.2 by allowing new nodes. Corollary 3.11 shows that the star, the intuitive candidate for a cheapest topology, is optimal only with a single net payer or a single net payee.

The results are proved in the paper, with short arguments in its Appendix A, and they have no machine-checked proof. This mission adds a precise version of the model, in which the meaning of "cost-minimizing", the sign conventions and the corrected cost axioms are fixed, and a formal proof of the chain Theorem 3.1 → odd cycles → bipartite structure for an arbitrary cost function satisfying the axioms.

Difficulty

Theorem 3.1 on its own is a two-line computation. The difficulty is in applying it inside an arbitrary network. When $u$ and $w$ already share a channel, adding $\lambda_1$ or $\lambda_2$ to it requires $c(a+b)\le c(a)+c(b)$ for reals of either sign. That inequality is not among the axioms and has to be derived from them. The odd-cycle step needs a pigeonhole argument on channel orientations around a cycle. The bipartite step needs either König's characterization of bipartite graphs or a direct construction of the parts from the flow directions. The naive formalization that re-states Theorem 3.1 only for a network with exactly two channels does not reach the corollaries.

Formalization scope

• The node set is an arbitrary finite type V, not $\{1,\dots,n\}$. The matrix is Λ : V → V → ℝ, because λ is a Lean keyword.
• Sign convention. Support is the row-sum display $\sum_j\lambda_{i,j}=f_i$ of §2.1, under which a net payer has $f_i>0$. The paper's examples (§2, Figure 1, proof of Theorem 3.1) use the opposite sign. Every statement here is invariant under $F\mapsto-F$, and Theorem 3.1 is stated with "the same flow" given by Supports, which is independent of the sign.
• Cost is the form $\tfrac12\sum_{i,j}c(\lambda_{i,j})$, which needs no order on $V$.
• Cost-minimizing compares with networks on the same node set $V$; a network with an added hub (§3.2) is not an alternative.
• Axiom correction (SA). The paper prints (SA) as "$c(x+y)<c(x)+c(y)$ for $x>y\ge0$", which fails at $y=0$, so every theorem would hold vacuously. The formalization uses $x,y>0$, the form verified in Appendix D. The stronger axiom (SA+) is not used in this mission.
• Cycles are injective maps Fin k → V, $k\ge3$ odd, with cyclic successor finRotate k. A channel is a nonzero entry in either direction.
• Bipartite is Mathlib's SimpleGraph.IsBipartiteWith A Aᶜ on the channel graph, with the flow-direction clause stated separately as the stronger content.
• The star is the network whose only channels join each $i\ne h$ to the hub $h$ with net flow $f_i$; Corollary 3.11 assumes $\sum_i f_i=0$.

Trivializing formalizations are ruled out: the cost function is arbitrary subject to the axioms (no $\sqrt{|x|}$ or linear cost); cost-minimization ranges over all networks on $V$, not over a fixed edge set; $V$ is not fixed to three nodes; the in-and-out claim is stated for arbitrary networks; and $A$ and $B$ are complementary, so they cannot overlap.

König's theorem is in Mathlib (SimpleGraph.two_colorable_iff_forall_loop_even) and proved on the platform (FamousTheorems.two_colorable_iff_no_odd_cycle_6b), so it is not posed here. The derived two-sided subadditivity of $c$, and a lemma rerouting a relayed flow inside an arbitrary network, are reusable in the other missions of the series. Contributions of such auxiliary lemmas are welcome.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Topology, SSRN working paper 4439190, version of February 3, 2023. https://ssrn.com/abstract=4439190 (published in Management Science, 2024, https://doi.org/10.1287/mnsc.2023.03872).
• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, working paper, 2022 ([GHS22] in the paper; the source of the cost axioms).
• D. Kőnig, Theorie der endlichen und unendlichen Graphen, Akademische Verlagsgesellschaft, Leipzig, 1936.
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, 2015 (as cited in the paper). https://lightning.network/lightning-network-paper.pdf

Motivation

Inverse optimization asks for the objective of an optimization problem when only its optimal decisions are observed. It was formalized for linear programs by Ahuja and Orlin (Operations Research 2001) and has since been used to infer costs, preferences and utilities from observed choices, for instance in routing, pricing and the imitation of expert planners (see the survey discussion in Chan, Lee and Terekhov, Management Science 2019, and the noisy-data setting of Aswani, Shen and Siddiq, Operations Research 2018).

Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) study a contextual version: the problems a decision-maker faces change from instance to instance, and the observed expert decisions constrain a fixed but unknown cost vector. Their question is not how to estimate the cost, but which decisions to take so that the loss against the expert is as small as possible in the worst case. This mission formalizes the answer in the offline setting, where a finite data set is given in advance. The text used is the arXiv preprint v3 (1 July 2023); all theorem numbers refer to it.

Setting

Actions live in $\mathbb R^n$ and costs in $\mathbb R^d$, both with the Euclidean norm, and $d\ge2$. The unknown cost $c^\star$ lies on the unit sphere $S^d=\{c:\|c\|=1\}$.

An instance is a pair $(\mathcal X,f)$: a feasible set $\mathcal X\in\mathcal B$, i.e. a nonempty compact subset of $\mathbb R^n$ with diameter at most $1$, and a context function $f\in\mathcal F$, i.e. a $1$-Lipschitz map $\mathbb R^n\to\mathbb R^d$. Given a cost $c$, the forward problem is

$$\psi(c,\mathcal X,f)=\operatorname*{arg\,min}_{x\in\mathcal X} f(x)'c,$$

a set of minimizers.

The offline data are $\mathcal D=\{(\mathcal X_i,f_i,x^\star_i)\}_{i=1}^N$ with $x^\star_i\in\psi(c^\star,\mathcal X_i,f_i)$. The costs compatible with them form the knowledge set

$$C(\mathcal D)=\{c\in S^d:\ c'f_i(x^\star_i)\le c'f_i(x)\ \ \forall x\in\mathcal X_i,\ i=1,\dots,N\}.$$

A policy maps the data and a new instance $(\mathcal X,f)$ to an action $x^\pi\in\mathcal X$, and its regret on the instance is $(f(x^\pi)-f(x^\star))'c^\star$ with $x^\star\in\psi(c^\star,\mathcal X,f)$. The worst-case regret $\mathcal{WCR}^\pi(\mathcal D)$ is the supremum of the regret over $c^\star\in C(\mathcal D)$, $\mathcal X\in\mathcal B$ and $f\in\mathcal F$.

The angle between two vectors is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$, with $\theta(c,0)=\theta(0,\hat c)=0$. The uncertainty angle of a set $C$ is

$$\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\ \theta(c,\hat c),$$

and a circumcenter $\hat c(C)$ is a point of $S^d$ attaining the infimum. Geometrically, $\alpha(C)$ is the aperture of the narrowest revolution cone containing $C$ and $\hat c(C)$ is its axis. The circumcenter policy answers an instance with any $x^\pi\in\psi(\hat c(C(\mathcal D)),\mathcal X,f)$. Write $g(a)=\mathbf 1\{a<\pi/2\}\sin a+\mathbf 1\{a\ge\pi/2\}$.

Formalization targets

Goal: Theorem 1 (offline minimax regret), p. 12

For every realizable data set,

$$\mathcal{WCR}^{\pi}(\mathcal D)\ \le\ g\big(\alpha(C(\mathcal D))\big)$$

for the circumcenter policy $\pi$, whatever circumcenter and whatever minimizer it picks. Conversely, for every $\bar\alpha\in[0,\pi]$ there is an information set $C\subseteq S^d$ with $\alpha(C)=\bar\alpha$ on which every policy suffers regret at least $g(\bar\alpha)$ on some instance. The upper bound and the lower bound are one statement.

Milestones

1. Lemma 1 (p. 11). For a proxy cost $c^\pi\in S^d$ and a true cost $c^\star\in S^d$, the worst-case regret over instances and over minimizers $x^\pi\in\psi(c^\pi,\mathcal X,f)$ is attained and equals $g(\theta(c^\star,c^\pi))$:

$$\mathcal L(c^\pi,c^\star)=\begin{cases}\sin\theta(c^\star,c^\pi)&\theta(c^\star,c^\pi)<\pi/2,\\1&\text{otherwise.}\end{cases}$$

2. Lemma 2 (p. 12). Every nonempty $C\subseteq\mathbb R^d$ has a circumcenter; it is unique when $C\setminus\{0\}\neq\emptyset$ and $\alpha(C)<\pi/2$.

Significance

Theorem 1 identifies the minimax offline regret of contextual inverse optimization with a single geometric number of the knowledge set, $\sin\alpha(C(\mathcal D))$ (or $1$), and shows that one explicit policy, acting as if the cost were the circumcenter, attains it uniformly over all instances. It reduces the design of offline policies to computing a circumcenter, and it is the benchmark that the paper's online analysis (§4–§5) compares against: the online policies are judged by how fast they shrink the uncertainty angle.

The results are proved in the paper (App-3–App-9). To our knowledge none of them has a machine-checked proof. Formalizing them yields a verified statement of the minimax value, a reusable notion of uncertainty angle and circumcenter for arbitrary subsets of $\mathbb R^d$, and the exact tightness of the bound, including the regime $\alpha\ge\pi/2$ where nature can force the maximal regret.

Difficulty

The upper bound is not a direct consequence of the definitions: the regret involves an arbitrary compact action set and an arbitrary $1$-Lipschitz context, and the only link between the circumcenter's choice and $c^\star$ is that $x^\pi$ is optimal for the wrong cost. Lemma 1 is where this link is turned into an angle, and its value must be matched exactly, not up to constants. Lemma 2 requires care because the objective $\hat c\mapsto\sup_{c\in C}\theta(c,\hat c)$ is a supremum over an arbitrary, possibly non-closed, set and the angle convention at $0$ breaks continuity. The lower bound must hold for every policy, including ones that exploit tie-breaking, so the hard instance must be chosen after the policy.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin d). The angle vecAngle is defined directly with value $0$ when either argument is $0$; Mathlib's InnerProductGeometry.angle (which is $\pi/2$ there) is not used. $\alpha$ is a real infimum over the sphere of a real supremum over $C$; the angles lie in $[0,\pi]$, so both are genuine when $C$ is nonempty. Action sets are nonempty compact sets of diameter at most $1$ (nonemptiness is added: an empty feasible set has no action), contexts are $1$-Lipschitz, and data are indexed by Fin N.

Committed conventions and pins:

• $d\ge2$ is the paper's standing assumption (p. 7). $n\ge1$ is added on Lemma 1 and on Theorem 1: in $\mathbb R^0$ every regret is $0$ and the lower bounds would be false.
• Theorem 1's upper bound assumes realizable data (some $c_0\in S^d$ explains every observation), as the paper's data model does; this makes $C(\mathcal D)$ nonempty.
• Worst-case regrets are never written as real suprema. The upper bound quantifies over every $c^\star\in C(\mathcal D)$, instance, circumcenter, policy minimizer and expert minimizer. Lemma 1 is stated with IsGreatest, and the lower bound of Theorem 1 in attained form, which implies the paper's statement about the supremum.
• In the lower bound the quantifiers are ordered as in the paper: the set $C$, then the policy (any map from instances to feasible actions), then nature's instance.

A formalization that bounds the regret only for one selected minimizer of the forward problem, or that chooses the hard instance before the policy, proves a different and weaker theorem and is excluded.

The development needs: compactness and lower semicontinuity on the sphere (existence of a circumcenter), elementary spherical geometry for the uniqueness and for $\sin\theta$ as the value of a two-point instance, and monotonicity of $g$ on $[0,\pi]$. The angle, uncertainty angle and circumcenter definitions are reusable for the online missions of this series. Proofs of the two lemmas are the natural first contributions.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv preprint v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015v3
• R. K. Ahuja, J. B. Orlin, Inverse optimization, Operations Research 49(5):771–783, 2001. https://doi.org/10.1287/opre.49.5.771.10607
• T. C. Y. Chan, T. Lee, D. Terekhov, Inverse optimization: closed-form solutions, geometry, and goodness of fit, Management Science 65(3):1115–1135, 2019. https://doi.org/10.1287/mnsc.2017.2992
• A. Aswani, Z.-J. Shen, A. Siddiq, Inverse optimization with noisy data, Operations Research 66(3):870–892, 2018. https://doi.org/10.1287/opre.2017.1705
• R. Henrion, A. Seeger, Inradius and circumradius of various convex cones arising in applications, Set-Valued and Variational Analysis 18(3–4):483–511, 2010. https://doi.org/10.1007/s11228-010-0150-z

Motivation

Optimal control problems governed by partial differential equations (PDEs) often carry uncertainty in their data, for example a random source term. When the state must stay below a threshold, there are several ways to impose the constraint: with high probability (chance constraints), almost surely, or for every value in a fixed uncertainty set (robust constraints). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive first-order optimality conditions for all three models for the same elliptic model problem. This mission covers the robust model of §3.2 (pp. 23–25). Its Karush–Kuhn–Tucker (KKT) system has a Radon measure as multiplier, and it is related to the semi-infinite programming view of the same problem.

Robust state constraints are also the limiting case of the almost-sure model: by Lemma 3.4 of the paper (p. 19), an almost-sure constraint and the constraint for every parameter in the support of the distribution coincide when the constraint function is lower semicontinuous in the parameter. The robust multipliers live in $C(\bar D\times\Xi)^*$, which is a space of measures, whereas the almost-sure multipliers of §3.1 contain singular functionals with no such representation.

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$ such that $\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$. Let $\Xi\subset\mathbb R^m$ be compact, let $f_0,\varphi_1,\dots,\varphi_m\in L^2(D)$, and set $f(x,z)=f_0(x)+\sum_{i=1}^m z_i\varphi_i(x)$ (Assumption 1.1, eq. (3)). The solution operator $A^{-1}:L^2(D)\to C(\bar D)$ maps $F$ to the unique weak solution $y\in H^1_0(D)\cap C(\bar D)$ of $-\Delta y=F$ in $D$, $y=0$ on $\partial D$.

For a control $u\in L^2(D)$, a cost $F:L^2(D)\to\mathbb R$ and a threshold $\alpha\in\mathbb R$, the robust problem (63) is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad -\Delta\hat y(\cdot,z)=u+f(\cdot,z)\ \text{in }D,\quad \hat y(\cdot,z)=0\ \text{on }\partial D,\quad \hat y(x,z)\le\alpha\ \ \forall (x,z)\in D\times\Xi.$$

The state is $\hat{\mathcal S}(u)\in C(\bar D\times\Xi)$, $[\hat{\mathcal S}(u)](x,z)=[A^{-1}(u+f(\cdot,z))](x)$, and $\hat{\mathcal G}(u)=\hat{\mathcal S}(u)-\alpha$. The cone is $\hat{\mathcal K}=\{y\in C(\bar D\times\Xi):y\le0\}$ and its polar cone is $\hat{\mathcal K}^-=\{y^*\in C(\bar D\times\Xi)^*:\langle y^*,y\rangle\le0\ \forall y\in\hat{\mathcal K}\}$. The linear part of the state is $[\hat{\mathcal A}^{-1}\hat{\mathcal B}h](x,z)=[A^{-1}h](x)$. The active set is $M(u)=\{(x,z)\in\bar D\times\Xi:[\hat{\mathcal S}(u)](x,z)=\max_{\bar D\times\Xi}\hat{\mathcal S}(u)\}$.

Formalization targets

Goal: Lemma 3.14 refined to (66), pp. 23–24

Let $F$ be convex and continuously Fréchet differentiable, and assume the constraint qualification $0\in\operatorname{int}\{\hat{\mathcal G}(L^2(D))-\hat{\mathcal K}\}$. Then $u^*$ is a solution of (63) if and only if there is a nonnegative finite Borel measure $\mu^*$ on $\bar D\times\Xi$ with, for $y^*=\hat{\mathcal S}(u^*)$,

$$\langle DF(u^*),h\rangle+\int_{\bar D\times\Xi}[A^{-1}h](x)\,d\mu^*(x,z)=0\quad\forall h\in L^2(D),$$ $$y^*\le\alpha\ \text{on }\bar D\times\Xi,\qquad\int_{\bar D\times\Xi}(y^*-\alpha)\,d\mu^*=0.$$

The page derives (66) from the abstract system (65) of Lemma 3.14 (necessity). Sufficiency is the converse direction of Lemma 3.14, since a nonnegative measure defines a multiplier in $\hat{\mathcal K}^-$ by integration. Both directions are part of the goal.

Milestones

1. Lemma 3.13: unique solvability of (63b)–(63c) in $C(\bar D\times\Xi)$ with the bound (64).
2. Lemma 3.14: the abstract KKT system (65) with $\lambda^*\in C(\bar D\times\Xi)^*$.
3. The identification $C(\bar D\times\Xi)^*\cong\mathcal M(\bar D\times\Xi)$ (p. 23): every $\lambda^*$ is integration against a signed measure.
4. Nonnegativity (p. 24): $\lambda^*\in\hat{\mathcal K}^-$ gives a nonnegative $\mu^*$.
5. Lemma 3.15: (66) is equivalent to the scalar-multiplier form (67): $\lambda^*\ge0$ and a probability measure $\tilde\mu$ on $M(u^*)$ with $\langle DF(u^*),h\rangle+\lambda^*\int[A^{-1}h](x)\,d\tilde\mu=0$, $\max y^*\le\alpha$, $\lambda^*(\max y^*-\alpha)=0$.
6. Lemma 3.16: the convex-hull condition (68) is equivalent to the existence of such a $\tilde\mu$.
7. Lemma 3.4: for lower semicontinuous $h$, $h(\xi)\le0$ almost surely if and only if $h\le0$ on the support of the law of $\xi$.

Significance

The goal gives the robust problem a KKT system whose multiplier is a nonnegative measure on $\bar D\times\Xi$ that is carried by the points where the constraint is active. Lemmas 3.15 and 3.16 turn this into a scalar multiplier times a probability measure on the active set, and into a convex-hull condition. These are the forms used by semi-infinite programming algorithms and by discretizations that approximate the measure by finitely many atoms. Together with Lemma 3.4, they say when the KKT system of the almost-sure model (§3.1, with its singular multipliers) can be replaced by the measure-valued system of the robust model.

All statements of the mission are proved in the paper, some by reference: Lemma 3.14's proof refers to the argument of Lemma 3.7, and Lemma 3.16 relies on Phelps's barycenter theorem. None of them is formalized. A formal development would also check two points that the page leaves implicit. Lemma 3.15's proof divides by the total mass of $\mu^*$ and does not treat $\mu^*=0$. Condition (68) is printed per direction $h$, while (67a) needs one measure for all $h$.

Difficulty

The necessity direction of the goal needs a Lagrange multiplier theorem in a Banach space whose constraint cone $\hat{\mathcal K}$ has nonempty interior. The multiplier is a priori only an element of $C(\bar D\times\Xi)^*$, and the Riesz–Markov–Kakutani theorem on the compact space $\bar D\times\Xi$ turns it into a measure. The state $\hat{\mathcal S}(u)$ must also be shown to lie in $C(\bar D\times\Xi)$. Continuity of each slice in $x$ is the regularity of Lemma 1.2 (continuity of $H^1_0$ solutions up to the boundary for class-S domains, from Kinderlehrer–Stampacchia), and joint continuity needs the bound (64), uniform in $z$. Working pointwise in $z$ does not give these: a family of continuous slices need not be jointly continuous without an estimate that is uniform in the parameter.

Formalization scope

$\bar D$ and $\Xi$ are subtypes of Euclidean spaces with CompactSpace instances, so $C(\bar D\times\Xi)$ carries its sup norm. Measures on $\bar D\times\Xi$ are Borel measures; on this compact metric space every finite Borel measure is regular, so "regular Borel (Radon) measure" is IsFiniteMeasure, and nonnegativity (66c) is built into Lean's Measure type. The solution operator is a hypothesis: a bounded linear map $L^2(D)\to C(\bar D)$ such that $A^{-1}F$ is, for every $F$, the weak solution in $H^1_0(D)\cap C(\bar D)$, encoded with the published weak-derivative definitions HunterPDE.Shared.WeakDeriv. The page's "$\le0$ in $D\times\Xi$" is encoded on $\bar D\times\Xi$, the same condition for continuous functions. "Solution" means global minimizer over the feasible set. $L^2(D)^*$ is identified with $L^2(D)$ through the Riesz map. In Lemma 3.16 the clco of (68) is the norm closure of the convex hull, which equals the weak closure.

Added hypotheses: $D$ and $\Xi$ nonempty in Lemmas 3.15 and 3.16 (no probability measure exists on an empty set). Pinned reading: (68) is posed as one inclusion $0\in DF(u^*)+\lambda^*\,\overline{\operatorname{co}}\{u_x:(x,z)\in M(u^*)\}$ in $L^2(D)$, where $u_x$ represents $h\mapsto[A^{-1}h](x)$. The page derives (68) from exactly this inclusion. The closed hull is kept because the page's remark that "co" suffices is not proved in infinite dimension.

Several trivializing formalizations are ruled out. The state operator is tied to the PDE and is never an arbitrary map into $C(\bar D\times\Xi)$. The multiplier carries its sign (a nonnegative measure, or $\lambda^*\in\hat{\mathcal K}^-$) together with complementarity. Optimality is global minimality, not a stationarity condition. All integrands are continuous functions on a compact space against finite measures, so no integral takes a junk value.

A complete development needs elliptic regularity in $C(\bar D)$ for class-S domains, a Banach-space Lagrange multiplier theorem under a Robinson-type constraint qualification, the Riesz–Markov–Kakutani theorem for $C(K)^*$ with signed measures (the platform's FamousTheorems.riesz_markov_kakutani covers positive functionals on $C_c$), and barycenters of probability measures on compact convex sets. The last three are reusable beyond this mission. Contributions of proofs for any of them 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
• F. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980 (SIAM reprint 2000). https://doi.org/10.1137/1.9780898719451
• R. R. Phelps, Lectures on Choquet's Theorem, 2nd ed., Lecture Notes in Mathematics 1757, Springer, 2001. https://doi.org/10.1007/b76887
• H. W. Alt, Lineare Funktionalanalysis, Springer, 2012. https://doi.org/10.1007/978-3-662-08386-4

Motivation

Many accounting frauds have come to light through whistleblowers rather than through audits, and regulators now run programs to encourage tips: since the Dodd–Frank Act of 2010 the U.S. Securities and Exchange Commission pays awards for original information that leads to a successful enforcement action. Empirically, whistleblower involvement is associated with better enforcement outcomes (Call, Martin, Sharp & Wilde, 2018), and employees are a leading source of fraud detection (Dyck, Morse & Zingales, 2010). A natural conjecture is that more whistleblowing raises the chance that an audit failure is caught, and so pushes auditors to work harder.

Nan, Tang & Ye (Management Science, 2025) show in a small game that this conjecture can fail. Their main result, Proposition 2, characterizes exactly when increasing whistleblowing intensity lowers equilibrium audit quality. This mission formalizes that result together with the equilibrium it is about.

Setting

A firm is good ($G$) with probability $p\in(0,1)$ and bad ($B$) otherwise.

1. Auditor. She chooses an audit quality $a\in(0,1)$ at cost $\tfrac12ka^2$. She always issues a clean opinion $g$ on a good firm and detects a bad firm with probability $a$.
2. Whistleblower. After a clean opinion he receives a signal with $\Pr(s_l\mid B)=\Pr(s_h\mid G)=\beta\in(\tfrac12,1)$. On the signal $s_l$ he blows the whistle (event $W_1$) with probability $\tau\in(0,1)$, the whistleblowing intensity; otherwise the enforcer sees silence ($W_0$).
3. Enforcer. Having seen $W\in\{W_1,W_0\}$, he chooses an investigative effort $e_W\in[0,1]$ at cost $\tfrac12\gamma e_W^2$ and catches a bad firm with probability $e_W$. He maximizes

$$\Pr(B\mid g,W)\,e\,R-\tfrac12\gamma e^2,\tag{3}$$

where the posterior is computed by Bayes' rule from the probabilities above. 4. Auditor's program. She pays damages $D$ when an audit failure is caught, and minimizes

$$(1-p)(1-a)\Pr(r_b\mid B,g)\,D+\tfrac12ka^2,\qquad \Pr(r_b\mid B,g)=\beta\tau e_1+(1-\beta\tau)e_0.\tag{4, 6}$$

An equilibrium at intensity $\tau$ is a triple $(a^*,e_1^*,e_0^*)$ of mutual best responses in which the enforcer's posteriors are computed at the actual $a^*$. The paper assumes $R/\gamma<1/(1-p)$ and $D/k<1/(1-p)$. Write $r=R/\gamma$ for the enforcer's incentive and $d=D/k$ for the auditor's incentive.

In Lean, a Model carries $p,\beta,R,\gamma,D,k$ with these restrictions. The posteriors are postW1, postW0; the best-response predicates are IsEnforcerBR and IsAuditorBR; the equilibrium is IsEquilibrium M τ a e1 e0. An equilibrium path A (IsEquilibriumPath M A) assigns to every $\tau\in(0,1)$ an equilibrium audit quality $A(\tau)$.

Formalization targets

Goal: Proposition 2

Fix $p,\beta,r$ and $\tau\in(0,1)$, and let

$$r^*=\frac{\beta\,[\tau(\beta-2\beta p+p)-1]^2}{(p-1)(\beta\tau-1)\,[\beta-\beta^2\tau+(2\beta-1)p(\beta\tau+1)]}.$$

There is a threshold $d^*$, depending only on $(p,\beta,r,\tau)$ and positive when $r>r^*$, such that for every model with these $p,\beta$ and $R/\gamma=r$, and every equilibrium path $A$,

$$A\ \text{is differentiable at}\ \tau\ \text{with}\ A'(\tau)<0\iff \frac R\gamma>r^*\ \text{and}\ \frac Dk<d^*.$$

Milestones

The milestones follow the paper's equilibrium analysis and its proof of Proposition 2:

• the enforcer's best responses $e_1,e_0$, with $e_1>e_0$ and $e_0<1$ (p. 12);
• the auditor's best response $a=(D/k)(1-p)\Pr(r_b\mid B,g)$ (pp. 12–13);
• Proposition 1: existence, uniqueness and the characterization (7)–(9) (p. 13);
• the silence effect: $e_0^*$ decreases in $\tau$ (p. 32);
• the gap function $V$ (28) is strictly increasing and its root is the equilibrium (pp. 32–33);
• on the branch $e_1^*=1$: $\lim_{a\to0}\partial V/\partial\tau>0\iff r>r^*$; $\partial V/\partial\tau$ decreases in $a$, giving a threshold $a_1$ that does not depend on $d$; and $a^*$ increases in $d$, giving $d^*$ (p. 33);
• the region $e_1^*=1$ is $r>r_2$, $a^*<a_2$, with $r_2<r^*$ and $a_1<a_2$ (p. 33);
• the closed form of $\partial V/\partial\tau<0$ when $e_1^*<1$ (p. 34).

Significance

Proposition 2 separates two effects of intensity. The direct effect is that a tip triggers high investigative effort more often, which raises detection and audit quality. The indirect effect, the silence effect, is that with more intense whistleblowing silence becomes reassuring, so the enforcer investigates less without a tip. The result says the indirect effect dominates exactly when the enforcer's incentive is above an explicit threshold and the auditor's incentive is below a threshold. The paper builds its welfare analysis on it: the planner's optimal intensity (Lemma 2, Proposition 3) and the reward-design extension of §4.

The theorem is proved in the paper (Appendix, pp. 31–34), and Proposition 1 is stated without a printed proof. As far as is known, none of it has been machine-checked. A formal proof would check the computer-algebra steps the paper summarizes as "it is simple to verify" or "after some algebra manipulation". It would also make precise two points the printed proof leaves loose. First, the derivative of $a^*$ in $\tau$ fails to exist where the equilibrium crosses the kink of $e_1=\min\{1,\cdot\}$. Second, the printed comparison "$r_2>r^*$" is reversed: $r_2<r^*$ is what holds and what the argument needs.

Difficulty

The equilibrium audit quality has no closed form; it is the root of the gap function $V$, which involves a $\min$ and rational functions of $(a,\tau)$. The obvious attempt, differentiating the closed-form equations (7)–(9) in $\tau$, gives an expression whose sign is not visible. Its sign depends on $r$, $d$ and on which branch of the $\min$ the equilibrium lies.

The paper splits by branch. On $e_1^*=1$, the sign of $\partial V/\partial\tau$ is controlled by a single-crossing property in $a$ and by the limit at $a=0$, which yields $r^*$. Turning this into a threshold on $d$ requires the comparative static of $a^*$ in $d$. Each of these steps is a polynomial inequality in four or five variables over a box. They are routine to check numerically, but proving them requires explicit sign certificates.

Formalization scope

• Model. All parameters are real. The restrictions $0<p<1$, $\tfrac12<\beta<1$, $R,\gamma,D,k>0$, $R/\gamma<1/(1-p)$, $D/k<1/(1-p)$ are fields of Model. The intensity $\tau\in(0,1)$ is a hypothesis of each statement, not a field.
• Efforts. The enforcer's effort lies in $[0,1]$, which is where the $\min\{1,\cdot\}$ comes from. The auditor's effort lies in the open interval $(0,1)$, as on p. 6.
• Posteriors. They are defined from the joint probabilities by Bayes' rule, not as the simplified fractions. The best-response formulas are therefore theorems.
• Omitted. The firm's cash flow $X$, the investment $I$, the fee $F$, the investors and Lemma 1, and the restrictions $R<I$, $D\le I-R$ of p. 9 are omitted, because none of them enters (3)–(9). The social planner (§3.4), the reward micro-foundation (§4.1) and the Online Appendix extensions are out of scope.
• "Impairs". It means that the equilibrium path has a derivative at $\tau$ and that the derivative is negative. Mathlib's deriv is not used for this, because it returns $0$ at a kink. By Proposition 1 the path is unique on $(0,1)$.
• Quantifier order. $r^*$ is the explicit formula. The threshold $d^*$ is existential but is chosen before the model, so it may depend on $(p,\beta,r,\tau)$ and not on $D$ or $k$. Choosing $d^*$ after the model would make the equivalence a tautology ($d^*=D/k\pm1$ according to the sign). The threshold $a_1$ is likewise chosen before the model, which encodes "$a_1$ does not depend on $d$".
• Derivatives in the proof. Derivative claims of the proof that fail at the kink ($de_0^*/d\tau<0$, $\partial V/\partial a^*>0$) are stated as strict monotonicity. The two printed slips, "$\ge1\iff$" and "$r_2>r^*$", are stated in corrected form, and the milestone quotes keep the printed text.

Contributions that are welcome include sign certificates for the polynomial inequalities of p. 33, an implicit-function argument for the derivative of the equilibrium path off the kink and a proof of Proposition 1, for which the paper prints none.

Selected references

• L. Nan, C. Tang, M. Ye, Auditing with a Chance of Whistleblowing, Management Science, 2025 (author manuscript dated December 30, 2024). https://doi.org/10.1287/mnsc.2024.04808
• A. C. Call, G. S. Martin, N. Y. Sharp, J. H. Wilde, Whistleblowers and Outcomes of Financial Misrepresentation Enforcement Actions, Journal of Accounting Research 56(1), 123–171, 2018. https://doi.org/10.1111/1475-679X.12192
• A. Dyck, A. Morse, L. Zingales, Who Blows the Whistle on Corporate Fraud?, Journal of Finance 65(6), 2213–2253, 2010. https://doi.org/10.1111/j.1540-6261.2010.01614.x

Motivation

A portfolio manager who observes a covariate today, say a vector of macroeconomic indicators $x_0$, wants an allocation that performs well on the returns $Y$ that follow such a covariate. With finitely many historical pairs $(\hat x_i,\hat y_i)$ the conditional law of $Y$ given $X=x_0$ is poorly estimated: usually no sample has covariate exactly $x_0$, and few have covariates near it. Distributionally robust optimization hedges against this estimation error by optimizing against the worst distribution in a ball around the empirical one. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451, Operations Research, 2025) study this problem with an optimal transport ball and a conditional objective. Before giving tractable reformulations they identify the regimes in which the robust problem is degenerate. This mission covers one of those regimes, a transport budget large enough to empty a fiber of positive radius.

Setting

Let $\mathcal X$ and $\mathcal Y$ be Polish spaces (covariates and returns) and let $(\hat x_i,\hat y_i)\in\mathcal X\times\mathcal Y$, $i\in[N]$, be the data, with empirical distribution $\hat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$. Ground costs $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ combine into the separable cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$. The optimal transport cost $\mathbb W(\mathbb Q,\hat{\mathbb P})$ is the least expected cost $\mathbb E_\pi[\mathbb D]$ over couplings $\pi$ of $\mathbb Q$ and $\hat{\mathbb P}$, and the ambiguity set is the ball

$$\mathbb B_\rho=\{\mathbb Q\in\mathcal M(\mathcal X\times\mathcal Y):\mathbb W(\mathbb Q,\hat{\mathbb P})\le\rho\}.$$

The conditioning event is the fiber $\mathcal N_\gamma(x_0)\times\mathcal Y$, with $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$ and fiber radius $\gamma>0$. For a loss $\ell(y)$ (the loss of a fixed portfolio at return $y$) the worst-case conditional expected loss is

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))>0}\ \mathbb E_{\mathbb Q}\big[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)\big],$$

problem (12) of the paper, where the strict inequality avoids conditioning on null sets. The threshold

$$\rho_{\max}(x_0,\gamma)=\inf\{\mathbb W(\mathbb Q,\hat{\mathbb P}):\mathbb Q(X\in\mathcal N_\gamma(x_0))=0\}$$

is the least budget that empties the fiber. With $\mathcal I_1=\{i:\hat x_i\in\mathcal N_\gamma(x_0)\}$ and $d_i$ the cost from $\hat x_i$ to the boundary $\partial\mathcal N_\gamma(x_0)$, the paper computes it in closed form. Throughout, the paper's Assumption 2.4 holds: the costs are symmetric, nonnegative and continuous, and $\mathbb D$ vanishes exactly on the diagonal; projections onto $\mathcal N_\gamma(x_0)$ are unique; and every boundary point of $\mathcal N_\gamma(x_0)$ has points outside it at arbitrarily small cost.

Formalization targets

Goal: Proposition 4.2

For $\gamma>0$ and $\rho>\rho_{\max}(x_0,\gamma)$, and every loss $\ell$,

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))>0}\mathbb E_{\mathbb Q}\big[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)\big]=\sup_{y\in\mathcal Y}\ell(y).$$

Milestones

1. The decomposition (24): $\mathbb Q\in\mathbb B_\rho$ iff $\mathbb Q=N^{-1}\sum_i\pi_i$ with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D_{\mathcal X}(X,\hat x_i)+\mathbb D_{\mathcal Y}(Y,\hat y_i)]\le\rho$.
2. Proposition 4.1: $\rho_{\max}(x_0,\gamma)=N^{-1}\sum_{i\in\mathcal I_1}d_i$.
3. A conditional expectation of $\ell(Y)$ never exceeds $\sup_y\ell(y)$.
4. For every $y_0$, some $\mathbb Q'\in\mathbb B_\rho$ with positive fiber mass has conditional expected loss $\ell(y_0)$.

Significance

Proposition 4.2 is a negative result with a practical consequence: when the budget $\rho$ exceeds $\rho_{\max}$, the robust conditional loss equals the worst loss over the whole return space and ignores the data. The modeler must therefore keep $\rho<\rho_{\max}$, and Proposition 4.1 makes that threshold computable from the samples. In that regime the paper replaces the strict constraint by a positive mass requirement (Proposition 4.3) and derives a finite-dimensional dual (Theorem 4.4); those results are separate missions of this series.

The results are proved in the paper; none is formalized. The mission formalizes them in Lean 4 on top of Mathlib, using a published optimal transport cost and a published extended-real integral. The decomposition (24) is reusable for every argument about empirical optimal transport balls with finitely many atoms. The formal statement of Proposition 4.1 makes explicit a regularity condition on the boundary that the paper's proof uses but does not state.

Difficulty

The upper bound is elementary. The lower bound needs, for each $y_0$, a feasible distribution whose conditional law on the fiber is concentrated at $y_0$. The construction printed on p. 46 keeps a positive mass of a sample inside the fiber, so its conditional expectation mixes $\ell(y_0)$ with a sample loss; that construction has to be corrected. Proposition 4.1 needs a matching lower bound on the cost of every fiber-emptying coupling, and an exit cost from the fiber that equals the boundary distance $d_i$. For a general continuous $\mathbb D_{\mathcal X}$ this fails. The decomposition (24) needs an optimal coupling to exist, which on Polish spaces with a lower semicontinuous cost is Villani's existence theorem. Mathlib does not have that theorem.

Formalization scope

• $\mathcal X,\mathcal Y$ are Polish Borel spaces; $[N]$ is Fin N with $N>0$; repeated samples are allowed.
• $\mathbb W$ is RWPI.SqrtLasso.transportCost, an infimum over couplings with a $[0,\infty]$-valued cost; the paper's "min" is not built into the definition.
• Expectations are $\int\ell^+-\int\ell^-$ in EReal (ModelRiskOT.Duality.extIntegral), never a Bochner integral, which would assign $0$ to a non-integrable loss. Both sides of the goal are extended reals; $\sup_y\ell(y)$ may be $+\infty$.
• The loss at a fixed portfolio $(\alpha,\beta)$ is an arbitrary function $L:\mathcal Y\to\mathbb R$, with no measurability or boundedness assumed.
• The conditional expectation is $\mathbb Q(S)^{-1}\cdot\mathbb E_{\mathbb Q}[\ell\,\mathbb 1_S]$ and is evaluated only at measures with $\mathbb Q(S)>0$. The supremum ranges exactly over probability measures in the ball with positive fiber mass.
• The radius enters as ENNReal.ofReal ρ; the hypothesis $\rho_{\max}<\rho$ forces $\rho>0$, and (24) carries $0\le\rho$.
• $\kappa_i$ and $d_i$ are real infima; $\partial$ is the topological frontier in $\mathcal X$.
• Assumption 2.4 is a structure hypothesis on every theorem. Proposition 4.1 additionally carries BoundaryRegular, which is not in the paper: the boundary is nonempty, the exit cost of a sample inside the fiber equals $d_i$, and $d_i=\kappa_i$ for samples outside. It mentions only $\mathbb D_{\mathcal X}$ and the samples and holds when $\mathbb D_{\mathcal X}$ is a norm distance. The goal does not carry it.
• The goal's hypothesis is $\rho>\rho_{\max}$ with $\rho_{\max}$ as defined (an infimum over measures), not its closed form, so Proposition 4.1 is not built into the goal.

Trivializing formalizations are ruled out: no conditional expectation is evaluated at fiber mass zero, the expectation is not a Bochner integral, $\rho<0$ cannot enter through ofReal, and the supremum is over the ball with positive fiber mass, not over all measures.

Needed infrastructure: finitely supported measures and their couplings, convexity of $\mathbb W(\cdot,\hat{\mathbb P})$, and for (24) the existence of optimal couplings on Polish spaces. These are reusable well beyond this paper, and contributions toward them are welcome.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, Operations Research, 2025; arXiv:2103.16451v3. https://arxiv.org/abs/2103.16451
• C. Villani, Optimal Transport: Old and New, Springer, 2009 (Theorem 4.1, existence of optimal couplings). https://doi.org/10.1007/978-3-540-71050-9
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research, 2019. https://doi.org/10.1287/moor.2018.0936

Motivation

A retailer that operates several physical stores can show a customer who finds nothing she likes in her store the products that other stores carry, for example on an in-store screen or a magic mirror, and ship the chosen product from the other store. The customer then buys at a utility discount: shipping takes time and the product cannot be tried on. Liu, Chen, Liu and Wan (2025) compare two ways of making such recommendations. Under simultaneous recommendation (SMR) all products of all stores are shown at once; under sequential recommendation (SQR) the customer first sees the products of her own store and is shown the other stores' products only if she buys nothing. The SQR choice model is the impatient-customer multinomial logit (MNL) model of Gao et al. (2021) applied store by store.

Under SMR the seller can do no better than letting every store offer the single-store optimal assortment (Theorem 1 of the paper, the subject of mission I of this series). Under SQR the seller can do better: the assortment of one store becomes a second-chance offer to the customers of every other store. The SQR problem with general discounts is NP-hard (Proposition 3 of the paper). This mission formalizes the structural result that makes the problem tractable when the discounts depend only on the store a customer visits.

Setting

A seller runs $m\ge2$ stores and sells $n$ products. A fraction $\lambda_i\ge0$ of the customers visits store $i$, with $\sum_i\lambda_i=1$. Product $k$ has revenue $r_k$, with $r_1>r_2>\dots>r_n>0$, and attraction value $v_k>0$; not buying has attraction $1$. A profile $\mathbf S=(S_1,\dots,S_m)$ lists the assortment of each store, and $\bar S=S_1\cup\dots\cup S_m$. A customer of store $i$ who buys product $k$ from store $j$ pays a utility discount $c_{ij}^k\ge0$, with $c_{ii}^k=0$, and $c_i^k(\mathbf S)$ is the smallest such discount over the stores that offer $k$. Under SQR the probability that a customer of store $i$ buys product $k$ is

$$p^Q_{ik}(\mathbf S)=\frac{v_k}{1+V(S_i)}\ \ (k\in S_i),\qquad p^Q_{ik}(\mathbf S)=\frac{v_k e^{-c_i^k(\mathbf S)}}{\big(1+V(S_i)\big)\big(1+V(S_i)+\sum_{l\in\bar S\setminus S_i}v_le^{-c_i^l(\mathbf S)}\big)}\ \ (k\in\bar S\setminus S_i),$$

and $0$ otherwise, where $V(S)=\sum_{k\in S}v_k$ and $W(S)=\sum_{k\in S}r_kv_k$. The seller maximizes the expected revenue

$$R(\mathbf S)=\sum_{i=1}^m\lambda_i\sum_{k=1}^n r_k\,p^Q_{ik}(\mathbf S)\qquad\text{(SQR)}.$$

The discounts are universally homogeneous if $c_{ij}^k=c>0$ for all $i\ne j$, and store-wise homogeneous if $c_{ij}^k=c_i>0$ for all $i\ne j$: the discount depends only on the store the customer visits. The single-store problem is $R^*=\max_S W(S)/(1+V(S))$ (3). An assortment is revenue-ordered if it equals $\{1,\dots,k\}$ for some $k\in[n]$, and $\tilde S$ denotes the smallest revenue-ordered optimal solution of (3).

Formalization targets

Goal: Theorem 4 (p. 17)

If the discounts are store-wise homogeneous, $\lambda_m=\min\{\lambda_1,\dots,\lambda_m\}$ and $c_1\le c_2\le\dots\le c_m$, then some optimal solution of (SQR) satisfies

$$S_1^*\subseteq S_2^*\subseteq\dots\subseteq S_{m-1}^*\subseteq\tilde S\subseteq S_m^*,$$

with every $S_i^*$ revenue-ordered.

Milestones

1. Existence of $\tilde S$ (p. 11): a smallest revenue-ordered optimal solution of (3) exists.
2. Lemma B.3 (p. 36): a three-store, four-product comparison of three explicit profiles.
3. Proposition B.1 (p. 35): if $\lambda_m$ is minimal and $c_m$ maximal, some optimal solution has $S_i^*\subseteq S_m^*$ for all $i$.
4. Lemma B.2 (p. 35): the one-store problem (8) with a fixed second-step set has an optimum that is revenue-ordered within that set.
5. Claim in the proof of Lemma B.1 (p. 38): a unique optimum of (8) shrinks as the discount factor grows.
6. Lemma B.1 (p. 35): under the hypotheses of Theorem 4, some optimal solution is nested, $S_1^*\subseteq\dots\subseteq S_m^*$.
7. Lemma B.4 (p. 39): $f(x)=\sum_i(a_i+b_ix)/(d_i+x)$ is quasi-convex on $x\ge0$ when $a_i/b_i$ decreases and $d_i$ increases.
8. (B.4) and (B.5) (pp. 40–41): for a nested profile whose last store misses product $k$, adding $k$ or truncating the last store does not lose revenue.
9. Proposition B.2 (p. 35): some optimal solution is nested and all revenue-ordered.
10. Step 3, Cases 1 and 2 (p. 43): moving stores $k+1,\dots,m-1$ to $\tilde S$, or growing store $m$ towards $\tilde S$, does not lose revenue.
11. Theorem 3 (p. 16) and Theorem 2 (p. 15): the universally homogeneous $m$-store and two-store versions.

Significance

Theorem 4 reduces the SQR problem with store-wise homogeneous discounts from a search over $2^{mn}$ profiles to a search over nested chains of prefixes, of which there are polynomially many for fixed $m$. It also gives an operational rule: the store with the lowest demand and the largest discount for its customers carries the widest assortment, wider than the single-store optimum $\tilde S$, and every other store carries a prefix that fits inside $\tilde S$. Example 2 of the paper (p. 18) shows that when the two orderings point in opposite directions an optimal solution need not be revenue-ordered, so both hypotheses carry weight.

The result is proved in the paper's Online and Additional Supplements. None of it is machine-checked. A formal development would also settle two places where the printed proof is incomplete: the proof of Proposition B.2 ends with "If we continue the analysis, one can show…", and it applies Lemma B.4 with some coefficients $a_i=0$ and a reordered index, outside the lemma's stated hypotheses.

Difficulty

The revenue of one store depends on the assortments of all others through $\bar S\setminus S_i$, and the objective is a sum of ratios of ratios. The classical argument for MNL assortment problems, that a product with revenue above the current optimum should be added, does not transfer: adding a product to store $i$ raises store $i$'s first-step revenue but also changes the second-step offer to every other store's customers, and removing it from store $i$ moves it into the second step. A local exchange that improves one store can hurt another, so revenue-ordering has to be established jointly with the nesting, and the order of the stores (by $\lambda_i$ and by $c_i$) determines which exchanges are safe.

Formalization scope

Products are Fin n and the paper's product $k$ is index $k-1$; stores are Fin (M + 2), so $m\ge2$ and stores $m-1$, $m$ are the last two indices. Assortments are Finset (Fin n). The attraction values $v_k$ are the primitive data. The factor $e^{-c_i^k(\mathbf S)}$ is the largest $e^{-c_{ij}^k}$ over the stores offering $k$, and $0$ when none does. The choice probabilities (2) and the objective (SQR) are the model; the Gumbel derivation of (2) (Proposition 1, from Gao et al. 2021) is not formalized. Store-wise homogeneity is a predicate on a general discount array, not a separate model.

The standing assumptions of §3 are explicit hypotheses everywhere: $\lambda_i\ge0$, $\sum_i\lambda_i=1$, $r_1>\dots>r_n$, $v_k>0$, $c_{ii}^k=0$. Two hypotheses are pinned and disclosed: $r_k>0$ (revenues are prices; Lemma B.3 is false with a negative revenue), and $n\ge1$ wherever revenue-ordered sets appear, since $\{1,\dots,k\}$ with $k\in[n]$ is nonempty. Lemma B.3 takes nonnegative revenues and attraction values, because the proof of Proposition B.1 applies it to proxy products that may be empty.

"Optimal" means a global maximizer of (SQR) over all profiles, ties allowed. $\tilde S$ enters as the hypothesis that a given set is the smallest revenue-ordered optimum of (3); the first milestone shows the hypothesis can be met, so the goal is not vacuous. A formalization in which $\tilde S$ is an arbitrary optimum, the discount factor ignores which store offers a product, or $m$ is fixed to $2$ would be a different theorem and is ruled out. The inequalities (B.4), (B.5) and those of Step 3 are stated for every profile of the stated shape rather than only for an optimal one, since for an optimal profile they would hold trivially.

A complete development needs finite-sum manipulations of MNL ratios, a reusable lemma that the single-store MNL problem has a revenue-ordered optimum, and quasi-convexity of sums of linear-fractional functions (Lemma B.4, a pure real-analysis statement of independent use). Contributions of any milestone, of alternative proofs of Theorem 4, and of proofs of the companion Theorems 2 and 3 are welcome.

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 (formalized from the authors' manuscript of 2024-09-17 with its Online and Additional Supplements).
• 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. https://pubsonline.informs.org/journal/opre
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147