Inventory and Supply Chain

One stage at a time

A serial supply chain is the simplest multiechelon system: a retailer orders from a warehouse, which orders from a plant, which orders from an outside supplier with unlimited stock. Only the retailer sees customer demand, only the retailer pays a stockout penalty, and every stage pays to hold inventory. Choosing how much each stage should hold looks like a joint optimization over all stages at once, because an upstream stockout delays every downstream replenishment. Clark and Scarf (1960) showed that it is not: measured in echelon terms, the optimal policy is a base-stock policy at every stage, and the optimal levels can be found one stage at a time from the customer upward, each step a single-variable convex minimization. Chapter 6 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents the infinite-horizon form of that result as its Theorem 6.3, the bounds of Shang and Song (2003) that make the levels cheap to approximate, and the contrasting guaranteed-service model of Graves and Willems (2000), in which stages quote delivery times rather than fill rates and the optimal safety stocks are all-or-nothing. This mission formalizes the chapter's numbered results, with Theorem 6.3 as its goal.

Setting

Stages are numbered $1, \dots, N$ from the customer upward. Stage $j$ has a local holding cost $h'_j$ per unit per period; its echelon holding cost is $h_j = h'_j - h'_{j+1}$ with $h'_{N+1} = 0$, so that $h'_j = \sum_{i \ge j} h_i$ (localHolding, echelonHolding). Stage $j$'s echelon consists of stages $j, j-1, \dots, 1$, and its echelon on-hand inventory $I_j$ (echelonOnHand) is all on-hand and in-transit stock in that echelon. Stage 1 pays a stockout cost $p$ per unit per period. Orders placed by stage $j$ arrive after a lead time $L_j$ if stage $j+1$ can ship them; $D_j$ denotes the lead-time demand at stage $j$.

An echelon base-stock policy gives each stage a level $S_j$ and orders to keep its echelon inventory position at $S_j$. The chapter derives, from conservation of flow, a recursion that evaluates the expected cost of any echelon base-stock vector $S$ (csBar, csHat, csG):

$$\bar g_0(x) = (p + h'_1)x^-, \qquad \hat g_j(x) = h_j x + \bar g_{j-1}(x), \qquad g_j(y) = \mathbb{E}[\hat g_j(y - D_j)], \qquad \bar g_j(x) = g_j(\min\{S_j, x\}),$$

and the expected cost of the system under $S$ is $g_N(S_N)$. The term $\bar g_j$ is the implicit penalty function: it charges stage $j+1$ for the downstream consequences of running short. A vector is sequentially optimal (CSSequential) when each $S_j$ minimizes $g_j$, which depends only on $S_1, \dots, S_{j-1}$.

The Shang-Song bounds compare $g_j$ with the cost of the $j$-stage truncated system when all its local holding costs are set to one value, $h_j$ for the lower bound and $\sum_{k \le j} h_k$ for the upper (ssLower, ssUpper). With equal holding costs all stock is held at stage 1, so each bound is a single-stage newsvendor cost for the demand $\tilde D_j = D_1 + \dots + D_j$ over the cumulative lead time (tildeLaw) with stockout cost $p + h'_{j+1}$, plus the holding cost of the stock in transit to stages $1, \dots, j-1$, whose mean is $\mathbb{E}[D_1] + \dots + \mathbb{E}[D_{j-1}]$ (pipelineMean).

In the guaranteed-service model each stage $i$ has a processing time $T_i$, quotes a committed service time $S_i$ to its customer, and receives an inbound time $SI_i = S_{i+1}$ from its supplier (gsInbound), $SI_N$ being external. Demand is bounded, so the stage can meet every order within $S_i$ by holding safety stock $k\sqrt{SI_i + T_i - S_i}$ with $k = z_\alpha\sigma$, and the holding cost is $g(S) = \sum_i h_i k \sqrt{SI_i + T_i - S_i}$ (gsCost) over the feasible times $0 \le S_i \le SI_i + T_i$ (GSFeasible).

Formalization targets

Goal: Theorem 6.3

For echelon holding costs $h_j \ge 0$, stockout cost $p \ge 0$ and lead-time demands of finite mean, if $S^*$ is sequentially optimal then for every echelon base-stock vector $S$,

$$g_N(S^*_N \mid S^*) \;\le\; g_N(S_N \mid S),$$

and $g_N(S^*_N \mid S^*)$ is the optimal cost. This is clark_scarf_sequential.

Supporting targets

Proposition 6.1, $\sum_j h_j I_j = \sum_j h'_j (I'_j + IT_{j-1})$; the stage-1 identities (6.29) and (6.30), that $g_1$ is a newsvendor cost with penalty $p + h'_2$ and its minimizer solves $F_1(S^*_1) = (p + h'_2)/(h_1 + p + h'_2)$; convexity of every $g_j$ under sequential optimality; existence of a sequentially optimal vector when $h_j > 0$ and $p > 0$; Theorem 6.4, $g^l_j \le g_j \le g^u_j$, and $S^l_j \le S^*_j \le S^u_j$ where $S^u_j$ minimizes $g^l_j$ and $S^l_j$ minimizes $g^u_j$ (the book's pairing, p. 200); and Theorem 6.5, that in the guaranteed-service serial system with $s_1 = 0$ every optimal $S^*_i$ is $0$ or $S^*_{i+1} + T_i$.

Theorem 6.2, the optimality of echelon base-stock policies among all policies, is stated in the book without a model of the policy space and is not a target here; Theorem 6.3 is the optimization it licenses.

Significance

Theorem 6.3 is what Zipkin calls the fundamental equations of supply chain theory. It reduces a joint optimization over $N$ coupled levels to $N$ one-dimensional convex problems, and every exact method and most heuristics for serial and assembly systems, Rosling's reduction of assembly systems to serial ones included, run through it. Theorem 6.4 turns the recursion into closed-form bounds and the Shang-Song heuristic, which the book reports as accurate to within a fraction of a percent. Theorem 6.5 explains the shape of optimal safety stock placement under guaranteed service and why its dynamic program only needs to examine endpoints.

None of these results has a machine-checked proof. The book proves none of them in full: Theorem 6.3 is asserted after an informal derivation, Theorem 6.4 is cited, and Proposition 6.1 and Theorem 6.5 are left as exercises. Formalizing the recursion's convexity and the exchange argument behind Theorem 6.3 produces a reusable treatment of the implicit penalty function; the concavity-on-a-polytope argument for Theorem 6.5 is reusable for the tree systems of Sect. 6.3.5.

Difficulty

The obvious attack on Theorem 6.3, differentiating the system cost in each $S_j$, fails immediately: the cost depends on $S_j$ through $\min\{S_j, x\}$ inside nested expectations and is not convex in $S$ jointly. The argument that works is an induction along the recursion, comparing $g_j(\cdot \mid S)$ with $g_j(\cdot \mid S^*)$ pointwise. Its key step is that, for the convex $g_j(\cdot \mid S^*)$ minimized at $S^*_j$, the value $g_j(\min\{S^*_j, x\})$ is the least value of $g_j$ on $(-\infty, x]$, so that any other truncation point can only cost more. That step needs convexity of $g_j(\cdot \mid S^*)$, which needs $\bar g_{j-1}(\cdot \mid S^*)$ convex, which needs $S^*_{j-1}$ to be a minimizer; for an arbitrary $S$ the functions $\bar g_j(\cdot \mid S)$ are not convex, and the induction must carry both vectors at once.

Integrability is a second, silent obstacle. Each $g_j$ is an expectation of translates of $\hat g_j$; the recursion preserves Lipschitz continuity with a constant growing with the costs, and finite means are exactly what make every integral in the recursion a genuine expectation rather than Lean's default value zero.

Theorem 6.4 requires relating the recursion, in which demands enter one stage at a time, to a single newsvendor cost in the sum $\tilde D_j$, which is a convolution; the inequalities come from the structure of (6.31) in the two extreme holding-cost profiles and are not obvious from the recursion's formulas. Theorem 6.5 is a statement about every minimizer, not the existence of an extreme one, so the proof must show the cost is strictly concave along every feasible direction that changes a net lead time and then classify the vertices of the feasible region.

Formalization scope

Stages are indexed by natural numbers $1, \dots, N$; the cost functions take total functions on $\mathbb{N}$ and never read values outside that range. The recursion is defined for every vector $S$, so the theorem compares values of one family of functions rather than a separately defined system cost; the identification of $g_N(S_N \mid S)$ with the steady-state expected cost of the physical system is the book's derivation and is not restated. Expectations are Lebesgue integrals under the lead-time demand laws, assumed to be probability measures on $\mathbb{R}$ with finite means. Sequential optimality is a hypothesis of the goal; a separate target shows it is satisfiable when $h_j > 0$ and $p > 0$, so the goal is not vacuous.

The bounding functions of Theorem 6.4 keep the holding cost of pipeline stock that the truncated cost (6.31) charges. The book omits that constant when it writes their minimizers, which it does not affect, but part (a) compares values, and without the constant the upper bound fails already in the book's own Example 6.1. For part (b) the minimizers of the bounding functions are asserted to exist and to bracket $S^*_j$; when the fractiles of $\tilde D_j$ are unique these are the book's quantile values. Theorem 6.5 is stated over real service times; because the feasible region's vertices are integral when the data are, every integer-optimal vector is optimal over the reals, so the real statement contains the book's integer program (6.38) to (6.42). Proposition 6.1 is stated with $IT_0 = 0$ built into the echelon sum.

The definition module is shared by all nine items. The dynamic program (6.43) to (6.44) for guaranteed-service serial systems and the tree-system algorithm of Sect. 6.3.6 are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 6. https://doi.org/10.1002/9781119584445
• A. J. Clark and H. Scarf, Optimal policies for a multi-echelon inventory problem, Management Science 6(4), 1960. https://doi.org/10.1287/mnsc.6.4.475
• F. Chen and Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1994. https://doi.org/10.1287/mnsc.40.11.1426
• K. H. Shang and J.-S. Song, Newsvendor bounds and heuristic for optimal policies in serial supply chains, Management Science 49(5), 2003. https://doi.org/10.1287/mnsc.49.5.618.15147
• S. C. Graves and S. P. Willems, Optimizing strategic safety stock placement in supply chains, Manufacturing & Service Operations Management 2(1), 2000. https://doi.org/10.1287/msom.2.1.68.23267

Motivation

Where to hold safety stock in a multi-stage supply chain is a basic question of inventory planning. Graves and Willems (MSOM 2(1), 2000) optimize safety-stock placement under the guaranteed-service assumption: each stage quotes a service time to its customers and always meets it. That assumption makes the placement problem tractable, and it is the basis of the dynamic program in the body of the paper and of later work built on it. It also has a price. A stage that promises a service time must hold enough stock to keep the promise even when it would be cheaper to let a downstream stage absorb an occasional delay.

The paper's Appendix measures that price in the simplest setting where it can be computed exactly. The setting is a serial chain in which internal stages promise nothing and only the external customer is guaranteed 100% service. Its one theorem, called the Result, characterizes the optimal base stocks of this relaxed model in closed form. The paper then compares that policy with the guaranteed-service optimum on 36 test instances. The guaranteed-service counterpart of this serial model, Simpson's all-or-nothing property of optimal service times, is on Prove2Me as a separate statement (SupplyChainTheory.gs_all_or_nothing, from Snyder and Shen's textbook). This mission formalizes the other side of the comparison.

Setting

A serial supply chain has $N$ stages. Stage $1$ is the demand node and stage $i$ supplies stage $i-1$ for $i = 2, \dots, N$. Time is discrete, with periods $t \in \mathbb{Z}$. Stage $i$ has a deterministic lead time $T_i \in \mathbb{N}$ and a base stock $B_i \in \mathbb{R}$. It follows a base-stock policy: in each period it observes end-item demand and orders that amount from its supplier.

The end-item demand in period $t$ is $d(t)$. The window demand is $d(a, b] = d(a+1) + \dots + d(b)$, which is $0$ when $a \ge b$. The demand bound $D : \mathbb{N} \to \mathbb{R}$ gives $D(\tau)$, the maximum possible end-item demand over $\tau$ periods, with $D(0) = 0$.

The backlog $Q_i(t)$ is the amount the customer of stage $i$ has ordered but not yet received. It satisfies the recursion (A1):

$$Q_i(t) = \bigl[d(t - T_i, t] + Q_{i+1}(t - T_i) - B_i\bigr]^+, \qquad Q_{N+1} \equiv 0 .$$

Unrolling it gives the closed max-form (A2). The external customer receives 100% service when $Q_1(t) = 0$ for all $t$. When demand never exceeds its bound, this is ensured by the service constraints

$$B_1 + \dots + B_i \ge D(T_1 + \dots + T_i), \qquad i = 1, \dots, N. \tag{A3}$$

Let $h_i$ be the holding cost at stage $i$ and $e_i = h_i - h_{i+1}$ the echelon holding cost. After constant terms are dropped, the expected holding cost gives program $\mathbf P^*$:

$$\min_B\ \sum_{i=1}^N h_i B_i - \sum_{i=2}^N e_{i-1} E[Q_i] \quad\text{s.t. (A3) and } B_i \ge 0 .$$

Demand is random, and $E[Q_i]$ is the expected backlog at stage $i$ in a period $t$.

Formalization targets

Goal: the Result, Eq. (A6)

If the echelon holding costs are nonnegative and $D$ is nondecreasing, then an optimal solution of $\mathbf P^*$ is

$$B_1 = D(T_1), \qquad B_i = D(T_1 + \dots + T_i) - D(T_1 + \dots + T_{i-1}), \quad i = 2, \dots, N. \tag{A6}$$

Formally, (A6) is feasible, and for every period $t$ its objective value is at most that of every feasible vector. The goal names this vector and compares it with every feasible $B$. The weaker claim that "some optimal solution binds all of (A3)" would not be enough.

Milestones

1. Eq. (A2). The closed max-form of $Q_i(t)$, derived from the recursion (A1).
2. Eq. (A3). Under the demand bound $d(a, a+s] \le D(s)$, the constraints (A3) force $Q_1 \equiv 0$ (sufficiency).
3. (A6) is feasible and is the unique binding solution of (A3).
4. Backlog bounds under a transfer. Moving $\Delta \ge 0$ units of base stock from stage $k$ to stage $k+1$ leaves $E[Q_i]$ unchanged for $i > k+1$ and raises it by at most $\Delta$ for $i \le k$. It lowers $E[Q_{k+1}]$ by at most $\Delta$.
5. Eqs. (A7)–(A8). For $k < N$, the transfer that makes the $k$-th constraint binding keeps the vector feasible and does not raise the objective.
6. The case $k = N$. Lowering $B_N$ until the $N$-th constraint binds does not raise the objective.

Significance

The Result shows that, without guaranteed internal service, the optimal base stocks do not depend on the holding costs, provided the echelon costs are nonnegative. Each stage then covers exactly the increment of maximal demand that its own lead time adds. This closed form is the benchmark against which the paper measures the cost of guaranteed service: 26% more safety-stock holding cost on average over its test problems. The paper also remarks, without proof, that Rosling's transformation extends the Result to assembly systems.

The Result is proved in the paper. As far as is known, neither it nor the backlog identity (A2) has been machine-checked. A complete development would yield a verified model of serial base-stock backlogs under bounded demand. It would also verify an exchange argument that recurs in multi-echelon inventory theory: moving stock toward the customer, with echelon costs controlling the sign of the change.

Difficulty

The objective is not linear in $B$. Each $E[Q_i]$ is a convex, nonsmooth function of $B_i, \dots, B_N$ through the maximum in (A2), and the objective subtracts these terms, so $\mathbf P^*$ minimizes a concave function over a polyhedron. The obvious approaches are linear-programming duality and convex first-order optimality conditions on $\mathbf P^*$, and neither applies. The result is a comparison of objective values between arbitrary feasible vectors and (A6). It has to hold pathwise under every demand distribution, and it then has to be carried through expectations. The hypotheses the Result leaves implicit must be recovered from the rest of the paper. Two of them, stated below, are necessary.

Formalization scope

Stages are natural numbers read on the range $\{1, \dots, N\}$. Lead times are natural numbers cast to $\mathbb{Z}$. Base stocks, holding costs and the demand bound are real-valued. A base-stock vector is a function $\mathbb{N} \to \mathbb{R}$, and only indices $1, \dots, N$ are read. The backlog is defined by the recursion (A1), computed in $N + 1 - i$ steps, with $Q_i \equiv 0$ for $i > N$. The closed form (A2) is a theorem. Randomness is a probability space $(\Omega, \mu)$ with a demand path $d(\omega, \cdot)$ whose value in each period is integrable. The integrability of the backlog is not assumed; it follows from the integrability of demand.

The page's informal words are read as follows:

• "The echelon holding costs are nonnegative" means $h_i - h_{i+1} \ge 0$ for $1 \le i < N$, and $h_N \ge 0$, i.e. $e_N \ge 0$ with $h_{N+1} := 0$. The case $k = N$ of the proof uses $h_N \ge 0$. Without it the Result is false ($N = 1$, $h_1 < 0$).
• $D(0) = 0$ is the paper's convention (§2, p. 70) and is added as a hypothesis. Without it (A6) can be infeasible ($D \equiv -1$ is nondecreasing).
• "$D(\,)$ is a nondecreasing function" means Monotone D on $\mathbb{N}$.
• "An optimal solution to $\mathbf P^*$" means feasible, with objective at most that of every feasible vector.
• "$E[Q_i]$" means the expectation of $Q_i(t)$ at a fixed period $t$. Every statement holds for all $t$, and stationarity is not assumed. The paper writes $E[Q_i]$ without $t$ because its demand is stationary, and this reading is at least as strong.
• The demand bound $d(a, a+s] \le D(s)$ appears only in milestone 2. The Result does not use it, so it is not a hypothesis of the goal.
• Eq. (A3) is formalized in the sufficiency direction only. The page's necessity remark ("as we assume that the demand bounds can be realized") is not stated.

A non-integrable backlog would make its Bochner integral $0$ and erase the backlog terms of the objective. The formalization rules this out by assuming integrable demand, which makes the backlogs integrable; it does not assume the backlogs themselves integrable. Out of scope: the spanning-tree dynamic program of §5, the unproved remarks of §§3–4, the Rosling extension, the Kodak application and the computational study.

Useful contributions include a proof of (A2) by downward induction on stages, the integrability of $Q_i(t)$, the pathwise version of milestone 4, and the iteration argument that assembles milestones 3, 5 and 6 into the goal.

Selected references

• S. C. Graves and S. P. Willems, Optimizing Strategic Safety Stock Placement in Supply Chains, Manufacturing & Service Operations Management 2(1):68–83, 2000. https://doi.org/10.1287/msom.2.1.68.23267
• K. F. Simpson, In-Process Inventories, Operations Research 6(6):863–873, 1958. https://doi.org/10.1287/opre.6.6.863
• K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed., 2019. https://doi.org/10.1002/9781119584445

Motivation

Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.

The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.

Timeline:

• Karlin and Scarf (1958), Scarf (1960): structure of optimal single-source backlog policies with a lead time.
• Sheopuri, Janakiraman and Seshadri (2010): reduction of dual-sourcing policies to the truncated regular pipeline and the expedited inventory position (Lemma 1 here).
• Allon and Van Mieghem (2010): the TBS policy, with conjectures and numerical evidence.
• JSS (2015): the TBS cost formula and a convex program for its parameters.
• Xin and Goldberg (2018): proof of the conjecture with an explicit rate (Management Science 64(1), 2018). This mission formalizes that result.

Setting

Let $D$ be a nonnegative random variable with finite mean $\mathbb E[D]$ that is not almost surely constant. Demands $D_1, D_2, \dots$ are i.i.d. copies of $D$. The regular source has lead time $L$, the express source has lead time $L_0 \ge 0$, and $L > L_0 + 1$. In period $t$ the controller orders $q^R_t \ge 0$ and $q^E_t \ge 0$; then $q^R_{t-L} + q^E_{t-L_0}$ arrives and $D_t$ is realized, so the on-hand inventory evolves as $I_{t+1} = I_t + q^R_{t-L} + q^E_{t-L_0} - D_t$ and may be negative. Initially nothing is on order and $I_1 = -\sum_{i=1}^{\hat G} D'_{-i}$, where the $D'_{-i}$ are further i.i.d. copies of $D$ and $\mathbb P(\hat G = k) = 2^{-k}$, $k \ge 1$.

The per-period cost is $c\,q^E_{t-L_0} + G(I_{t+1})$ with $G(y) = h y^+ + b y^-$, where $b, h > 0$ and $c > 0$ is the express premium (the regular unit cost is normalized to $0$). An admissible policy $\pi \in \Pi$ chooses the two orders in period $t$ as deterministic measurable functions of $(q^R_{t-L}, \dots, q^R_{t-1}, q^E_{t-L_0}, \dots, q^E_{t-1}, I_t)$. Its long-run average cost is

$$C(\pi) = \limsup_{T\to\infty}\frac1T\sum_{t=L_0+1}^T \mathbb E[C^\pi_t], \qquad \mathrm{OPT}(L) = \inf_{\pi\in\Pi}C(\pi).$$

With the expedited inventory position $\hat I_t = I_t + \sum_{k=t-L_0}^{t-1}q^E_k + \sum_{k=t-L}^{t-L+L_0}q^R_k$, the TBS policy $\pi_{r,S}$ orders $q^R_t = r$ and $q^E_t = \max(0, S - \hat I_t)$. A best TBS pair $(r^*, S^*)$ minimizes $C(\pi_{r,S})$ over $0 \le r \le \mathbb E[D]$ and $S \in \mathbb R$ (first in $r$ through $F^\infty(r) = \inf_S C(\pi_{r,S})$, then in $S$).

The constants $\epsilon_0$ and $Y_0$ are explicit functionals of the law of $D$ and of $L_0, b, h, c$. They are built from $g = \inf_x\mathbb E[G(x - \sum_{i=1}^{L_0+1}D'_i)]$, $U = c\,\mathbb E[D] + \mathbb E[G(-\sum_{i=1}^{L_0+1}D'_i)]$, $p_0 = \mathbb P(D < \mathbb E[D])$, the mean absolute deviation $\eta_0$, and the large-deviation quantities $\gamma_\epsilon, \vartheta_\epsilon$ of $\phi_\epsilon(\theta) = e^{\theta(\mathbb E[D]-\epsilon)}\mathbb E[e^{-\theta D}]$ (p. 441).

Formalization targets

Goal: Theorem 1 (p. 441)

For all $L_0 \ge 0$, $\epsilon \in (0,1)$ and $L > \epsilon_0^{-2} + Y_0\epsilon^{-2}$,

$$\frac{C(\pi_{r^*,S^*})}{\mathrm{OPT}(L)} < 1 + \epsilon.$$

The threshold does not depend on $L$, so the statement gives an explicit, inverse-polynomial rate. Its limit form $C(\pi_{r^*,S^*})/\mathrm{OPT}(L) \to 1$ is Corollary 1 of the paper.

Milestones

In the order the proof uses them:

• the bound $g \le \mathrm{OPT}(L) \le U$;
• Lemma 1, the reduction to $\hat\Pi$ (quoted from Sheopuri et al.);
• Eq. (3), the TBS cost formula $C(\pi_{r,S}) = c(\mathbb E[D]-r) + \mathbb E[G(I^r_\infty + S - \sum_{i=1}^{L_0+1}D'_i)]$ (quoted from JSS);
• Theorem 2, the existence of a stationary-like vector $(\chi^{*,L}, q^{*,L}, \mathcal I^{*,L})$ with $r_L = \mathbb E[\chi^{*,L}_1]$;
• Corollary 2 and Lemma 2, the lower bound $\mathrm{OPT}(L) \ge c(\mathbb E[D]-r_L) + (1-\alpha)V^{L-L_0}_\alpha(r_L,-\infty)$ through a discounted single-source problem;
• Lemma 3, the Bellman equation and structure of that problem (quoted from JSS and Scarf 1960);
• Lemma 4 (8) and (9), and Corollary 3, the passage to the infinite horizon and to base-stock policies;
• Lemma 5, the random-walk maxima $M^r_k$ (proof omitted in the paper);
• Lemmas 8–9 and Corollary 4: $r_L < \mathbb E[D] - \epsilon_0$ once $L > \epsilon_0^{-2} + L_0 + 1$.

Significance

The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of $L$, so the result yields an algorithm whose running time does not grow with $L$ and whose optimality gap is bounded explicitly for every finite $L$. It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.

Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.

Difficulty

An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding $r_L$ away from $\mathbb E[D]$ requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.

Formalization scope

Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):

• The law of $D$ is a probability measure on $\mathbb R$ with no mass on $(-\infty,0)$, finite mean, and no atom of mass $1$. The paper's "strictly positive (possibly infinite) variance" is read as "not almost surely constant".
• $c_R = 0$, $b > 0$, $h > 0$, $c > 0$, and $L, L_0$ are natural numbers. The paper's standing assumption $L > L_0 + 1$ is a hypothesis wherever the paper states it; in Theorem 1 it follows from the threshold.
• Costs, expectations, $C(\pi)$, $\mathrm{OPT}(L)$, $V^n_\alpha$ and $V^\infty_\alpha$ take values in $[0,\infty]$, so infinite costs are never truncated. The ratio in Theorem 1 is stated as $C(\pi_{r^*,S^*}) < (1+\epsilon)\mathrm{OPT}(L)$, which is equivalent because $0 < g \le \mathrm{OPT}(L) \le U < \infty$.
• $\Pi$ is exactly the paper's class: deterministic, time-dependent, measurable, nonnegative orders that depend on the pipeline and inventory. It is neither restricted to stationary policies nor enlarged to randomized ones. TBS policies are members, so $C(\pi_{r,S}) \ge \mathrm{OPT}(L)$ by construction.
• $\vartheta_\epsilon \in [0,\infty]$ is the supremum of the minimizers of $\phi_\epsilon$ on $[0,\infty)$, and it is $\infty$ if the infimum is not attained; $1/\infty = 0$.
• The existence of a best TBS pair is asserted in the paper via JSS. The goal therefore also asserts that some TBS policy with $0 \le r \le \mathbb E[D]$ meets the bound, so it cannot hold vacuously when no minimizer exists.
• $r_L$ belongs to a witness of Theorem 2, and the results that use it hold for every witness.
• The single-source class $\bar\Pi$ ("feasible nonanticipative policies, as typically defined") is read as nonnegative orders that are measurable functions of past demands. In Lemma 3 "increasing" is read as nondecreasing, and convexity in $x$ includes finiteness.
• The paper states Eq. (3) without a range for $r$; it is stated here for $0 \le r \le \mathbb E[D]$, the TBS parameters over which the paper optimizes. At $r = \mathbb E[D]$ both sides are $+\infty$. In Lemma 8, the range's upper end is $+\infty$ when $\epsilon = 0$.
• Differences such as $V^\infty_\alpha - V^n_\alpha$ and $M^r_\infty - M^r_n$ are stated additively, and the negative terms of (9) and Corollary 3 are moved to the other side.

Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.

A trivializing formalization is ruled out: $\mathrm{OPT}(L)$ ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.

Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.

Selected references

• L. Xin and D. A. Goldberg, Asymptotic Optimality of Tailored Base-Surge Policies in Dual-Sourcing Inventory Systems, Management Science 64(1):437–452, 2018. https://doi.org/10.1287/mnsc.2016.2607
• G. Janakiraman, S. Seshadri and A. Sheopuri, Analysis of Tailored Base-Surge Policies in Dual Sourcing Inventory Systems, Management Science 61(7):1547–1561, 2015.
• G. Allon and J. A. Van Mieghem, Global Dual Sourcing: Tailored Base-Surge Allocation to Near- and Offshore Production, Management Science 56(1):110–124, 2010.
• A. Sheopuri, G. Janakiraman and S. Seshadri, New Policies for the Stochastic Inventory Control Problem with Two Supply Sources, Operations Research 58(3):734–745, 2010.
• H. Scarf, The Optimality of (s, S) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960, pp. 196–202.
• L. Xin and D. A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6):1556–1565, 2016.

Motivation

A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.

Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with $N$ products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector $y^*$; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general $N$-product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).

Setting

There are $N$ products and $N$ demand classes, both numbered $1,\dots,N$. Class $i$ can be served by product $j$ whenever $j \le i$, at a unit substitution cost $b$ when $j < i$. Each class $i$ has unit revenue $p_i$ and unit backorder cost $\pi_i$; each product $j$ has unit purchase cost $c_j$ and effective unit salvage value $s_j$ (salvage value minus holding cost, possibly negative). Put $a_{ji} = p_i$ if $j = i$, $a_{ji} = p_i - b$ if $j < i$, and $T_k = p_k + \pi_k - b$. The standing assumptions are: (1) $\pi_i + p_i \ge \pi_j + p_j$ for $i < j$; (2) $s_i \ge s_j$ for $i < j$; (3) $a_{ij} + \pi_j - s_i \ge 0$ for $i \le j$.

The sequence of events: the starting inventory $x$ is observed; stock is raised to $y \ge x$ at unit costs $c$; the demand vector $d$ is realized; stock is allocated to classes; leftovers are salvaged. For fixed $y$ and $d$ the allocation is the linear program

$$G(y,d) = \max \sum_{i}\sum_{j \le i} a_{ji} w_{ji} + \sum_i s_i v_i - \sum_i \pi_i u_i$$

subject to $u_i + \sum_{j\le i} w_{ji} = d_i$, $v_j + \sum_{i \ge j} w_{ji} = y_j$, and $w, u, v \ge 0$, where $w_{ji}$ is the amount of product $j$ given to class $i$, $u_i$ the shortage of class $i$ and $v_j$ the leftover of product $j$. The expected profit is

$$P(x,y) = -\sum_k c_k (y_k - x_k) + \mathbb E\, G(y, D),$$

and the ordering problem is $\max_{y \ge x} P(x,y)$; a maximizer is an optimal level $\bar y(x)$.

Allocation Algorithm (A) serves the classes in the order $1,2,\dots,N$, class $i$ first from product $i$ and then from the leftovers of products $i-1,\dots,1$. The subproblem shortage $S^k_j$ is the unmet demand of class $j$ when (A) runs on the classes $k,\dots,j$ with the products $k,\dots,j$ only; $\vec S^k_{a,n} = 0$ means $S^k_m = 0$ for all $a \le m \le n$. The paper's first partial derivatives of $P$ are sums of salvage values, substitution costs and the $T_k$, weighted by probabilities of such shortage events.

Formalization targets

Goal: Theorem 2

With $y^*$ a maximizer of $P(0,\cdot)$ over $y \ge 0$, every optimal level $\bar y$ for every starting inventory $x \ge 0$ satisfies

$$x_i \ge y^*_i \implies \bar y_i = x_i .$$

Milestones

• Proposition 1: Algorithm (A) is feasible and optimal for the allocation LP, and its value is $G(y,d)$.
• Proposition 2: $y \mapsto P(x,y)$ is concave and submodular on $\{y \ge 0\}$.
• Eq. (4): the explicit formula for $\partial P/\partial y_i$ in terms of shortage probabilities.
• Theorem 1: there is $y^* \ge 0$ with $\bar y(x) = y^*$ whenever $0 \le x \le y^*$.
• Lemmas 1, 2, 3, 5: identities and monotonicity properties of the shortage probabilities used to compare $\partial P/\partial y_i$ and $\partial P/\partial y_{i+1}$.

Significance

Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector $y^*$, computed once, determines the decision for every starting inventory in the region $x \le y^*$ and fixes the order of every overstocked product elsewhere. The paper builds its bounds on $y^*$, its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.

The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair $j = i+1$, and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.

Difficulty

The obvious argument for Theorem 2 is the one-dimensional one: if $x_i \ge y^*_i$ then $\partial P/\partial y_i \le 0$ at $\bar y$, so product $i$ should not be raised. It fails because $\partial P/\partial y_i$ depends on the other coordinates: at $\bar y$ some products are raised above $x$ and others kept at $x_j > y^*_j$, and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product $i$ propagates through the greedy allocation of every later class.

Formalization scope

Products and classes are indexed by Fin N (the paper's index $k$ is Lean index $k-1$); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs $w_{ji}$, $i < j$, forbidden (fixed to $0$), as in the paper's proof of Proposition 1; $G$ is the supremum of the LP objective. The demand law is a product $\nu_1 \otimes \dots \otimes \nu_N$. Submodularity is the lattice inequality $P(x, y \vee y') + P(x, y \wedge y') \le P(x,y) + P(x,y')$, which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.

Hypotheses the paper uses without stating, made explicit here:

• the substitution cost is nonnegative, $b \ge 0$ (Proposition 1 is false for $b < 0$);
• the demand classes are independent (product forms in Lemma 3 and Appendix B);
• each demand is nonnegative, has finite mean and has a density;
• $s_i < c_i < p_i + \pi_i$ for every product (Theorem 1's proof);
• every demand law charges every nonempty open interval of $[0,\infty)$, standing in for the uniqueness of the optimal level $\bar y(x)$ that the notation presupposes (Theorems 1 and 2).

The goal quantifies over every maximizer $y^*$ of $P(0,\cdot)$ and every optimal $\bar y$; it is not an existence statement, and $y^*$ is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for $x_i \ge y^*_i$.

A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of $S^k_j$ in $y$ and $d$), are welcome.

Selected references

• Y. Bassok, R. Anupindi, R. Akella, Single-Period Multiproduct Inventory Models with Substitution, Operations Research 47(4):632–642, 1999. https://doi.org/10.1287/opre.47.4.632
• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• E. Ignall, A. F. Veinott, Jr., Optimality of Myopic Inventory Policies for Several Substitute Products, Management Science 15(5):284–304, 1969. https://doi.org/10.1287/mnsc.15.5.284
• A. J. Hoffman, On Simple Linear Programming Problems, in V. Klee (ed.), Convexity, Proceedings of Symposia in Pure Mathematics, Vol. 7, AMS, 1963.

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$, complementary distribution function $\bar F$, finite mean, $f > 0$ on $[0, \mathbb Z]$ ($\mathbb Z \le +\infty$), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$, and $k(q) = S(q)/\bar F(q)$.

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$. The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$, payment follows after a term $t_2$, and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$), the supplier's expected profit is

$$\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),$$

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$, $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$, $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$, and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$. The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$, let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$, $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$, and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ($c_i = p$). With all three schemes available,

$$e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;$$ $$1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.$$

Milestones

1. Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$, and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$, $w = c_{\mathcal F}/\bar F(q)$.
2. Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$.
3. §5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$.
4. §4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$.
5. Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$, $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

• "Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$, which is what Propositions 2 and 3 prove.
• "Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$, the order forced by the paper's boundaries ($C_s = \mathbb C_1$, $C_s = \mathbb C_3$, $C_r = \mathbb C_2$). Profits are compared, not the $\Lambda_i$.
• "The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$, since $\Lambda_{\mathcal F}$ may be $\le 0$.
• "$C_r > \mathbb C_2$" is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$, i.e. $e^{-\eta_r\tau} < 1-\rho_r$: the stated assumptions give no single crossing in $C_r$.
• "The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$; this part is stated under feasibility.
• "Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
• Continuity of $f$ is read on $[0,\mathbb Z]$, and $\mathbb Z$ as the upper end of the support.
• Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$).
• Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$, "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ($c_i < p$, largest $\Lambda_i$) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$, $k$ and $z$ under strict IFR are welcome.

Selected references

• P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
• D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
• P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

Motivation

Large retailers pay their suppliers weeks or months after delivery, and small suppliers fill the gap with short-term finance. In factoring the supplier sells the receivable to a factor for immediate cash; in reverse factoring the retailer arranges the program with a bank, which pays the supplier early at a rate priced on the retailer's credit rating. Retailers commonly attach a condition: the supplier must accept a longer payment term. Wuttke et al. (Journal of Operations Management, 2019) report that buyers extended payment terms by 54 days on average on adopting reverse factoring and that many suppliers delayed adoption; Corsten (2010) reports suppliers resisting a program because of the demanded payment delay (both as cited by Kouvelis and Xu, pp. 6082–6083). How long an extension a retailer can demand, and what it gains by demanding it, is therefore a practical design question.

Kouvelis and Xu (Management Science 67(10), 2021) answer it inside a Stackelberg supply chain model with credit and liquidity risk. This mission formalizes their answer, Proposition 6 of §5.3: the retailer's optimal payment extension when she keeps the existing wholesale price.

Setting

Demand $D\ge0$ has density $f$, distribution function $F$ and $\bar F=1-F$; $f>0$ on $[0,\mathbb Z]$ with $\mathbb Z\le+\infty$ the upper end of the support, $f$ is continuous there, the mean is finite, and the failure rate $z(\xi)=f(\xi)/\bar F(\xi)$ is strictly increasing. Write $S(q)=\int_0^q\bar F(\xi)\,d\xi$ for expected sales and $k(q)=S(q)/\bar F(q)$.

A retailer (the leader) sets a wholesale price $w$, and a capital-constrained supplier (the follower) chooses a production quantity $q\ge0$; the retail price $p$ exceeds the unit cost $c$. Each firm $j\in\{s,r\}$ has a credit rating $C_j\in(C_{\min},C_{\max})$, a default probability $\rho_j=\rho(C_j)\in[0,1]$ with $\rho$ strictly decreasing, and an interest premium $\eta_j=\eta(C_j)>0$ with $\eta$ decreasing. The lead time is $t_1$, the payment term $t_2$, and $\lambda_s,\lambda_r\ge0$ are the liquidity risks.

Under a post-shipment scheme with coefficient $\Lambda$ the supplier earns

$$\pi(q;w)=(1-\rho_s)\bigl(\Lambda e^{-\lambda_s t_1}wS(q)-c\,q\,e^{\eta_s t_1}\bigr),$$

with $\Lambda_{\mathcal F}=(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}$ (recourse factoring), $\Lambda_{\mathcal N}=e^{-\eta_r t_2}(1-\rho_r)$ (non-recourse factoring) and $\Lambda_{\mathcal R}=e^{-\eta_r(t_2+\tau)}$ (reverse factoring with payment extension $\tau\ge0$). The retailer earns $\Pi=e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and

$$\Pi_{\mathcal R}(w,\tau)=e^{-\lambda_s t_1}(1-\rho_r)(2-e^{-\lambda_r\tau})(p-w)S(q_{\mathcal R})$$

under reverse factoring, where $q_{\mathcal R}$ is the supplier's best response. Its first-order condition is $w\bar F(q_{\mathcal R})=c_{\mathcal R}(\tau)=c\,e^{(\eta_s+\lambda_s)t_1+\eta_r(t_2+\tau)}$ (Eq. (12)).

Before reverse factoring, the supplier uses the better of the two factoring schemes. By Proposition 4 this is non-recourse, with equilibrium $(w^*_{\mathcal N},q^*_{\mathcal N})$, when $\mathbb C_{\mathcal N}<C_s\le\mathbb C_1$, and recourse, with $(w^*_{\mathcal F},q^*_{\mathcal F})$, when $C_s>\mathbb C_{\mathcal F}\vee\mathbb C_1$. The retailer keeps the existing wholesale price $w_s$ and solves problem (13): maximize $\Pi_{\mathcal R}(w_s,\tau)$ over $\tau\ge0$, subject to the supplier's acceptance (his reverse factoring profit is at least his existing one). $\mathbb C^{\max}_{\mathcal R}$ is the rating at which $\Lambda_{\mathcal F}=e^{-\eta_r t_2}$, and $\Xi_{[0,z]}(x)=\max\{0,\min\{z,x\}\}$.

Formalization targets

Goal: Proposition 6

(i) If $C_s\ge\mathbb C^{\max}_{\mathcal R}$, reverse factoring is dominated by recourse factoring. (ii) If $\mathbb C_{\mathcal N}<C_s<\mathbb C^{\max}_{\mathcal R}$, reverse factoring should be offered with

$$\tau^*_{\mathcal R}=\Xi_{[0,\tau_s]}(\tau^*_0),\qquad \lambda_r k(q)z(q)+\eta_r=2\eta_r e^{\lambda_r\tau^*_0},\quad w_s\bar F(q)=c_{\mathcal R}(\tau^*_0),$$

where $\tau_s=-\eta_r^{-1}\ln(1-\rho_r)$ with $w_s=w^*_{\mathcal N}$ in the non-recourse case, and $\tau_s=-\eta_r^{-1}\ln[(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}]-t_2$ with $w_s=w^*_{\mathcal F}$ in the recourse case.

Milestones, in attack order

1. Eq. (12): the supplier's best response under reverse factoring.
2. Proposition 4: which factoring scheme is in force before reverse factoring.
3. §5.3, $\tau_s$: acceptance holds exactly on $[0,\tau_s]$.
4. §5.3, $\tau^*_0$: the retailer's unconstrained profit is unimodal around $\tau^*_0$.

A follow-on item states Corollary 3(ii): the retailer's profit strictly increases, and the supplier's profit is unchanged when $\tau^*_0\ge\tau_s$.

Significance

Proposition 6 is the paper's prescription for program design. It says which suppliers should be offered reverse factoring: every supplier below the indifference rating $\mathbb C^{\max}_{\mathcal R}$ and above the non-recourse feasibility threshold. It also gives the extension in closed form, the unconstrained optimum clipped to the supplier's acceptance limit. Two consequences are drawn in the paper: non-recourse factoring is dominated once the extension is optimized, and reverse factoring may leave the supplier exactly as well off as before, so it is not necessarily a win-win (Corollary 3).

The proofs are in the paper's Online Appendix B and have not been machine-checked. A formal proof here produces a checked derivation of the projection formula from the model's primitives. It covers the strict-IFR analysis of the follower's response, the reduction of the acceptance constraint to an interval, and the unimodality of the retailer's objective. The same analysis of the pull game with an effective unit cost recurs across the supply chain finance literature.

Difficulty

The retailer's objective depends on $\tau$ through two opposing channels: the liquidity factor $2-e^{-\lambda_r\tau}$ increases, while expected sales $S(q_{\mathcal R}(\tau))$ decrease because the supplier's effective cost rises. Neither factor is concave in $\tau$, and the objective need not be concave. The natural move, to set the derivative to zero and call the root a maximum, proves nothing without a sign analysis. That analysis needs the monotonicity of $k\cdot z$ along the implicitly defined response $q_{\mathcal R}(\tau)$, which is where strict IFR enters. The acceptance constraint compares the supplier's profits in two different games (reverse factoring at $\tau$ against the existing equilibrium). Reducing it to $\tau\le\tau_s$ requires the supplier's best-response profit as an explicit increasing function of his quantity. Identifying the existing equilibrium requires Proposition 4, whose "adopted" compares equilibrium profits of two Stackelberg games.

Formalization scope

The model is a single Lean structure SupplyChainFactoring.Extension.Model. Demand is a probability measure on $\mathbb R$ with a density $f$, and $\mathbb Z$ is an extended real. "Continuous p.d.f. with $f>0$ in $[0,\mathbb Z]$" is read as continuity on $[0,\mathbb Z]$, with $f=0$ outside the support. Credit functions $\rho,\eta$ are real functions constrained on $(C_{\min},C_{\max})$. The finance derivations behind the profit functions (Eqs. (1), (5), (6), Lemma 1) are not formalized: the profit functions are the model.

Readings of informal words, each also recorded in the item's Formalization Note:

• Best response: a maximizer of the supplier's profit over $q\ge0$; equilibrium: a best response pair from which no nonnegative wholesale price with a best response gives the retailer more. Neither is defined through first-order conditions.
• Feasible: some $w\ge0$ with a best response gives the retailer positive profit; adopted (Proposition 4): feasible, with equilibrium supplier profit at least (non-recourse) or strictly above (recourse) the other feasible scheme's.
• Thresholds "the unique value of $C_s$ that satisfies …" are hypotheses in exactly that form; $c_{\mathcal N}=p$ and $c_{\mathcal F}=p$ are cross-multiplied because $\Lambda_{\mathcal F}$ can be $\le0$.
• In (13) $w$ is fixed at $w_s$ (§5.3's first sentence, footnote 23). $\pi^*_{\mathcal R}$ is the supplier's best-response profit under reverse factoring at $(w_s,\tau)$, and $\max\{\pi^*_{\mathcal F},\pi^*_{\mathcal N}\}$ is his profit in the existing equilibrium.
• Dominated (Proposition 6(i)): at every $\tau\ge0$ and every $w$, the supplier's reverse factoring best-response profit is at most his recourse one. Should be offered (6(ii)): $\tau^*_{\mathcal R}$ solves (13) and the retailer's profit is at least her existing equilibrium profit.
• $\tau^*_0$ is a hypothesis: it and some $q\in(0,\mathbb Z)$ solve the paper's two equations (the paper does not argue existence). Its optimality "without the nonnegativity constraint" is stated as unimodality of $\Pi_{\mathcal R}$ on the set of real $\tau$ with $c_{\mathcal R}(\tau)<w$.
• Always increases (Corollary 3(ii)) is strict; may remain unchanged when $\tau^*_0\ge\tau_s$ is read as "is unchanged whenever $\tau^*_0\ge\tau_s$".

Three misprints of the paper are corrected: $\Xi_{[0,z]}(x)=0$ "if $x<z$" is read as "if $x<0$"; "the retailer's maximization problem in (16)" refers to (13); the middle line of the $\Pi_{\mathcal R}$ display on p. 6082 carries a stray factor $w$, and the last line is used.

The hypotheses on $\tau^*_0$ cannot be met when $\lambda_r=0$, and the goal then says nothing about the case, as in the paper. The existing equilibrium, $\tau_s$ and $\tau^*_0$ are never free parameters: $\tau_s$ is the paper's explicit formula, and the reduction of acceptance to $\tau\le\tau_s$ is a milestone to be proved, not an assumption. Every logarithm is applied to a quantity the hypotheses force positive. A formalization that assumed acceptance equivalent to $\tau\le\tau_s$ or assumed unimodality would be trivial and is excluded.

The pull game with an effective cost has the same structure as Cachon's pull contract without salvage value (platform items CachonPushPull.*), but those items assume IGFR demand with a salvage value, so they are not reused. Reusable infrastructure welcome: the strict-IFR lemmas ($k$, $k\cdot z$ and $k(q)-q$ increasing) and the explicit best response of a newsvendor-type follower.

Selected references

• P. Kouvelis, F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• D. A. Wuttke, E. S. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019. https://doi.org/10.1002/joom.1023