The OR Formalization Drive

Two decisions that are usually taken separately

An $(R,Q)$ policy has two parameters. Chapter 4 of Axsäter's Inventory Control chooses the batch quantity $Q$ from a deterministic model, and Chapter 5 chooses the reorder point $R$ from a stochastic one with $Q$ held fixed; the book presents this two-step practice as an adequate approximation. Section 6.1 asks what is lost by it and shows how to optimize both parameters jointly in one stochastic model. For discrete demand the answer, due to Federgruen and Zheng (1992), is an algorithm of remarkable simplicity: increase $Q$ one unit at a time, keep the reorder point optimal along the way by a one-line rule, and stop at the first $Q$ for which the cost goes up. The claim that this stopping rule finds the global optimum over all pairs $(R, Q)$ is the capstone of Sect. 6.1.1.1 and the goal of this mission. The same idea is reused in the book for $(s,S)$ policies (Sect. 6.1.1.2) and, in continuous form, for normally distributed demand (Sect. 6.1.2).

Setting

An item is controlled by a continuous review $(R,Q)$ policy with integral reorder point $R$ and batch quantity $Q \ge 1$. Demand is discrete and stationary; the lead-time demand $D(L)$ takes values in the nonnegative integers with probabilities $p_j = \Pr[D(L) = j]$ and has a finite mean $\mu'$. The average demand per unit of time is $\mu$. Costs are a holding cost $h$ and a shortage cost $b_1$, both per unit and time unit, and an ordering cost $A$ per batch.

The building block is the cost of an $(S-1,S)$ policy that keeps the inventory position at a fixed integer $k$. By the standard argument of Sect. 5.3.2 the inventory level a lead-time later is $k - D(L)$, and the average holding and shortage cost rate is (Eq. 6.3)

$$g(k) \;=\; -b_1\,(k - \mu') + (h + b_1)\sum_{j=1}^{k} j\,\Pr[D(L) = k - j].$$

Under the $(R,Q)$ policy the inventory position is uniformly distributed on $\{R+1, \dots, R+Q\}$ (Proposition 5.1), so the total average cost rate is (Eq. 6.4)

$$C(R, Q) \;=\; \frac{A\mu}{Q} + \frac{1}{Q}\sum_{k=R+1}^{R+Q} g(k),$$

and $C(Q) = \min_R C(R,Q)$ (Eq. 6.5), attained at an optimal reorder point $R^{*}(Q)$. The ready rate $S_3(R) = \Pr[IL > 0] = \frac{1}{Q}\sum_{k=R+1}^{R+Q}\Pr[D(L) \le k-1]$ links the cost to service: raising the reorder point by one unit changes the cost by $-b_1 + (h + b_1)S_3(R+1)$ (Eq. 5.60).

Formalization targets

Goal — the Federgruen-Zheng stopping rule is optimal

Let $Q^{*} \ge 1$ be the smallest batch quantity with $C(Q^{*}+1) \ge C(Q^{*})$ and let $R^{*}$ be an optimal reorder point for $Q^{*}$. Then

$$C(R^{*}, Q^{*}) \;\le\; C(R, Q) \qquad\text{for all } R \in \mathbb{Z},\ Q \ge 1.$$

Supporting targets

The increment identity $g(k+1) - g(k) = -b_1 + (h+b_1)\Pr[D(L) \le k]$; convexity of $g$ on $\mathbb{Z}$ together with $g(k) \to \infty$ as $|k| \to \infty$; Eq. (5.60) and the convexity of $C(\cdot, Q)$ in $R$; Eq. (5.61), that the largest $R$ with $S_3(R) \le b_1/(h+b_1)$ is optimal for its $Q$; existence of an optimal $R$ for every $Q$; the recursion (6.6)-(6.7), $R^{*}(Q+1) \in \{R^{*}(Q) - 1, R^{*}(Q)\}$ chosen by comparing $g(R^{*}(Q))$ with $g(R^{*}(Q)+Q+1)$, and $C(Q+1) = C(Q)\frac{Q}{Q+1} + \min\{g(R^{*}(Q)), g(R^{*}(Q)+Q+1)\}\frac{1}{Q+1}$; the equivalence $C(Q+1) \ge C(Q) \iff \min\{\cdot\} \ge C(Q)$ and the monotonicity of that minimum in $Q$; and the existence of some $Q$ at which the costs stop decreasing.

Significance

The result itself. Joint optimization typically enlarges the batch and lowers the reorder point relative to the two-step procedure, and the book's Example 6.1 puts the resulting cost saving at a few percent. The Federgruen-Zheng procedure makes the exact joint optimum for discrete demand as cheap to compute as the two-step approximation, because each step of the recursion evaluates $g$ at two points. It is the exact benchmark against which the book's approximate techniques for normal demand (Sects. 6.1.2 and 6.1.3) are judged, and its structural core, that the optimal window of $Q$ consecutive inventory positions grows one neighbour at a time, is the discrete-convexity fact behind the whole of Sect. 6.1.

Formalizing it. The mathematics is settled. What the mission produces is a Lean development in which the steps the book marks "evident" and "obvious" are separate statements: that the recursion preserves optimality, that the marginal cost of enlarging the batch is monotone, and that a minimum over $R$ exists at all. None of the statements has a machine-checked proof yet.

Difficulty

The obvious first idea, to argue that $C(Q)$ is convex in $Q$ and stop at its first increase, does not work as stated: $C(Q)$ is a minimum over $R$ of a ratio and is not convex in general. What is true, and what the proof uses, is that the marginal cost $(Q+1)C(Q+1) - QC(Q)$ is nondecreasing, because it equals the smaller of the two $g$-values adjacent to the optimal window. Establishing the recursion (6.6) is where discrete convexity is needed: one must show that the best window of $Q+1$ consecutive positions is obtained from the best window of $Q$ by adding a neighbour, which fails for non-convex $g$. The window sums $R \mapsto \sum_{k=R+1}^{R+Q} g(k)$ are themselves convex in $R$ with increments $g(R+Q+1) - g(R+1)$, and the argument compares a competing window with the optimal one through the end terms. The remaining steps are finite algebra and an induction on $Q$ from $Q^{*}$.

Formalization scope

A DiscreteDemand is a function $p : \mathbb{N} \to \mathbb{R}$ with $p \ge 0$, $\sum p = 1$ and a summable first moment; $\Pr[D(L) \le k]$ is a finite sum over $0 \le j \le k$, empty for $k < 0$. The reorder point ranges over $\mathbb{Z}$ and the batch quantity over $\mathbb{N}$, with $Q \ge 1$ assumed in every statement because Lean's division by $0$ is $0$. Convexity of a function on $\mathbb{Z}$ is stated as nondecreasing increments, and divergence as Tendsto g (cocompact ℤ) atTop.

$C(Q)$ enters the goal as a function CQ together with the hypothesis that CQ Q is the least value of $R \mapsto C(R, Q)$; the stopping index $Q^{*}$ is characterized by the two conditions that define "the smallest $Q$ with $C(Q+1) \ge C(Q)$", and $R^{*}$ by optimality at $Q^{*}$. That these objects exist is the content of two separate items, so the goal is not vacuous: a minimum over $R$ exists for every $Q$ because $g \to \infty$, and the costs cannot decrease forever because the average of the $Q$ smallest values of $g$ tends to infinity. The positivity of $A$ and $\mu$ is the book's setting and is assumed where it appears.

The uniform inventory position of Proposition 5.1, which needs the book's assumption that not all demands are multiples of an integer larger than one, is taken as given in the cost formula (6.4), as the book does; the proposition itself is the subject of the next mission of this series. The definitions are reusable for the $(s,S)$ optimization of Sect. 6.1.1.2 and for the multi-echelon batch-ordering results of Sect. 10.5; contributions formalizing the Zheng-Federgruen $(s,S)$ algorithm on top of them are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sects. 5.9.1 and 6.1.1. DOI 10.1007/978-3-319-15729-0
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal $(r,Q)$ Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4), 1992, pp. 808-813. DOI 10.1287/opre.40.4.808
• Yu-Sheng Zheng and Awi Federgruen, Finding Optimal $(s,S)$ Policies Is About as Simple as Evaluating a Single Policy, Operations Research 39(4), 1991, pp. 654-665. DOI 10.1287/opre.39.4.654
• Paul Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.

Why the policy class is not up for debate

Every model in Chapters 5 and 6 of Axsäter's Inventory Control assumes at the outset that the ordering policy is of $(R,Q)$ or $(s,S)$ type. Section 6.2 asks whether better policies exist and answers, for the case in which there are no ordering costs but every order must be a multiple of a fixed batch quantity $Q$, that none do: Proposition 6.1, "an $(R,Q)$ policy is optimal", with a proof the book attributes to Chen (2000). For $Q = 1$ it is the optimality of an order-up-to-$S$ policy in the absence of ordering costs, and for continuous or Poisson demand it transfers to $(s,S)$ policies, which are then the same thing. The proposition is the one place in the book where a policy is compared against every feasible alternative rather than against other members of its own family, and its proof is short enough to be given in full, which makes it the natural capstone of Chapter 6.

Setting

Demand is compound Poisson: customers arrive according to a Poisson process with rate $\lambda$ and each demands an integral number of units, with sizes $D_0, D_1, \dots$ independent and identically distributed with law $f$ on the positive integers, independent of the arrival process. The book's standing assumption that not all demands are multiples of some integer larger than one is kept. Writing $T_n$ for the $n$-th arrival time, $N(t)$ for the number of arrivals by time $t$ and $S_n = D_0 + \dots + D_{n-1}$, the total demand by time $t$ is $S_{N(t)}$.

The replenishment lead-time $L$ is constant and $D(L)$, the demand over a lead-time, has law $D$. A holding cost $h > 0$ and a shortage cost $b_1 > 0$ per unit and time unit are charged. There are no ordering costs, but all orders must be multiples of a given batch quantity $Q \ge 1$ and can only be triggered by customer demands. A policy is therefore any rule $m$ that decides at each demand epoch how many batches to order; with initial position $y_0$ the inventory position evolves as $y_{n+1} = y_n - D_n + m_nQ$ (Eq. 6.22), and $y_t = y_{N(t)}$.

The standard argument of Sect. 5.3.2 gives the cost rate at time $t + L$ as

$$g(y_t), \qquad g(k) = -b_1(k - \mu') + (h+b_1)\sum_{j=1}^{k} j\,\Pr[D(L) = k - j],$$

the expected holding-plus-shortage cost rate of an inventory level $k - D(L)$ (Eq. 6.20), which is convex in $k$ with $g(k) \to \infty$ as $|k| \to \infty$. The band cost is $\bar g(y) = \sum_{j=1}^{Q} g(y+j)$ and $R$ denotes an integer minimizing $\bar g$. The $(R,Q)$ policy orders, as soon as the position is at or below $R$, the smallest number of batches that brings it above $R$; its position lives in the band $\{R+1, \dots, R+Q\}$ from the first order on. The performance measure is the long-run average cost rate $\frac{1}{T}\int_0^T g(y_{t-L})\,\mathrm{d}t$ as $T \to \infty$.

Formalization targets

Goal — Proposition 6.1

Almost surely, (1) for every policy $m$ and every $y_0$,

$$\liminf_{T\to\infty} \frac{1}{T}\int_0^T g\big(y^{m}_{t-L}\big)\,\mathrm{d}t \;\ge\; \frac{\bar g(R)}{Q},$$

and (2) the $(R,Q)$ policy attains it:

$$\frac{1}{T}\int_0^T g\big(y^{(R,Q)}_{t-L}\big)\,\mathrm{d}t \;\longrightarrow\; \frac{\bar g(R)}{Q}.$$

Supporting targets

Lemma 6.1, that $x \mapsto g(z + xQ)$ is convex and minimized at the representative of $z$ in the band; the closed form of the $(R,Q)$ position, $y_0 - S_n$ until the first order and the band representative of $y_0 - S_n$ afterwards; the uniform occupation of the band by the reduced process $y_t'$, the book's "the steady state distribution can be shown to be uniform", and its consequence that the long-run average of $g(y_t')$ is $\bar g(R)/Q$; Proposition 5.1 in the same ergodic form for the $(R,Q)$ policy; and the two halves of the goal as separate statements.

Significance

The result itself. Proposition 6.1 is what licenses the two-parameter policies on which the rest of the book's single-echelon theory is built, and it does so for the practically important case of batch ordering (pallets, containers, production lots). Its proof also explains why the policy works: the only quantity a policy controls is the residue class of the inventory position modulo $Q$, which no policy can influence, and the position within that class, which the $(R,Q)$ policy always sets to the cheapest possible value. The book extends the same reasoning to other cost structures and to periodic review.

Formalizing it. The proposition is a theorem about the class of all policies, and the book's proof is pathwise: Lemma 6.1 compares any policy with the reduced process instant by instant, and an ergodic statement about the reduced process does the rest. Formalizing it therefore forces the policy class, the demand process and the long-run average to be written down exactly, which the book never does. Nothing here is open; no statement has a machine-checked proof yet.

Difficulty

The pointwise comparison is elementary once Lemma 6.1 is available, and Lemma 6.1 is discrete convexity. The difficulty is entirely in the ergodic statement: that the reduced position $y_t' =$ (the band representative of $y_0 - S_{N(t)}$) spends a fraction $1/Q$ of the time at each point of the band, almost surely. In discrete time this is the convergence of occupation frequencies for an irreducible random walk on $\mathbb{Z}/Q\mathbb{Z}$ with step law $f$ modulo $Q$, where irreducibility is exactly the aperiodicity assumption on $f$, and the book's double-stochasticity argument (Eq. 5.33-5.34) identifies the uniform law as stationary. Passing to continuous time adds the exponential holding times: the time average is the arrival average weighted by i.i.d. holding times independent of the walk, which a strong law of large numbers turns back into the discrete statement. Mathlib has the strong law and the exponential law but no ergodic theorem for finite Markov chains, so that is the groundwork a solver must build. The naive route through the stationary distribution of the embedded chain at demand epochs is not enough on its own: for pure Poisson demand that chain is periodic, and the book itself notes it.

Formalization scope

A CompoundPoissonDemand on a probability space packages the rate, the size law with $f_0 = 0$ and the aperiodicity condition, and two sequences of random variables, the gaps and the sizes, with their laws (expMeasure lam, the given pmf), independence within each sequence, and independence between the sequences. Arrival times are partial sums of the gaps, count t is the supremum of $\{n : T_n \le t\}$, and cumDemand n is the partial sum of the sizes. A policy is a function m : ℕ → Ω → ℕ with no measurability requirement; ipPath and ipAt are the position after the $n$-th demand and at time $t$; rqIP and rqOrders are the $(R,Q)$ policy, with a theorem identifying rqOrders as a policy in the general sense. avgCost is $\frac{1}{T}\int_0^T g(y_{t-L})\,\mathrm{d}t$ with $y_s = y_0$ for $s < 0$. The cost function $g$ is sPolicyCost from the previous mission, applied to a DiscreteDemand that the hypotheses tie to the process as the law of the demand in $(0, L]$.

Conventions: $Q \ge 1$, $L \ge 0$, $h, b_1 > 0$; $R$ is any minimizer of $\bar g$ (it exists by the divergence of $g$, proved in the previous mission); $y_0$ is arbitrary. count and the interval integral take junk values on the null set where arrivals do not tend to infinity, which the almost-sure conclusions absorb. "$\liminf \ge c$" is stated as "for every $\varepsilon > 0$, eventually $\ge c - \varepsilon$", avoiding a liminf on $\mathbb{R}$ that could be junk.

Two readings that would trivialize the goal are excluded: the lower bound is over every rule, not over stationary or measurable ones, and the achievability half is a genuine limit, not a bound. The demand model and the occupation-frequency theorems are reusable for Proposition 10.1 and the batch-ordering models of Sect. 10.5; contributions establishing the ergodic theorem for irreducible chains on a finite cyclic group are welcome and would close most of this mission.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sects. 5.3.1 and 6.2.1. DOI 10.1007/978-3-319-15729-0
• Fangruo Chen, Optimal Policies for Multi-Echelon Inventory Problems with Batch Ordering, Operations Research 48(3), 2000, pp. 376-389. DOI 10.1287/opre.48.3.376.12427
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal $(r,Q)$ Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4), 1992, pp. 808-813. DOI 10.1287/opre.40.4.808
• Evan L. Porteus, Foundations of Stochastic Inventory Theory, Stanford University Press, 2002.

Why orders swing more than sales

Procter & Gamble observed in the 1990s that the orders its distributors placed for diapers were far more variable than the retail sales of diapers, and that its own orders to suppliers were more variable still, although the end demand for diapers is about as stable as demand gets. The phenomenon, a growing amplification of variability as one moves upstream in a supply chain, is the bullwhip effect. Lee, Padmanabhan and Whang (1997) argued that it is not a symptom of irrational behaviour: four rational responses of an inventory manager to their own environment each produce it. Chapter 13 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) makes three of the four quantitative, following Chen, Drezner, Ryan and Simchi-Levi (2000) for demand signal processing, Lee et al. for the rationing game, and Cachon (1999) for order batching. This mission formalizes those three models and the theorems the chapter proves about them.

Setting

Demand signal processing. A retailer faces a demand process $D_t$, $t \in \mathbb{Z}$, that follows the stationary first-order autoregressive model

$$D_t = d + \rho D_{t-1} + \epsilon_t,$$

with a constant $d \ge 0$, a correlation constant $-1 < \rho < 1$, and errors $\epsilon_t$ that are independent $N(0, \sigma^2)$ variables, each independent of the demands before period $t$. In steady state every $D_t$ has the law $N\big(d/(1-\rho),\ \sigma^2/(1-\rho^2)\big)$. The retailer replenishes with a lead time of $L$ periods under a base-stock policy but does not know the demand parameters, so it estimates the lead-time demand from a moving average of the previous $m \ge 1$ demands:

$$\hat\mu^L_t = \frac{L}{m}\sum_{i=1}^m D_{t-i}, \qquad \hat\sigma^L_{et} = C\sqrt{\frac{1}{m}\sum_{i=1}^m e_{t-i}^2}, \qquad e_t = D_t - \hat\mu^1_t,$$

and sets the base-stock level $S_t = \hat\mu^L_t + z_\alpha \hat\sigma^L_{et}$, where $z_\alpha$ is a safety factor. The book writes the constant in $\hat\sigma^L_{et}$ as $C_{L\rho}$ and does not give its form; here it is a free parameter $C$. Each period the retailer orders $Q_t = S_t - S_{t-1} + D_{t-1}$, which may be negative. In Lean the process is the structure AR1Demand, whose fields are the parameters, the errors, the demands, the recursion, the independence properties and the stationary law; muHat, err, sigmaHat, baseStock and order are the five quantities above.

Order batching. $N$ retailers face independent $N(\mu, \sigma^2)$ demands in every period and each orders once every $R \ge 1$ periods, the order being its demand over the previous $R$ periods. The supplier's order in a given period is the total ordered by the retailers whose ordering day falls in that period. Three patterns are compared: random ordering, in which each retailer's day is uniform over the $R$ days, so the number $X$ of retailers ordering on a given day is binomial$(N, 1/R)$; positively correlated ordering, in which all retailers order on the same day, so $X = N$ with probability $1/R$ and $0$ otherwise; and balanced ordering, in which the retailers are spread as evenly as possible, so with $N = MR + k$, $0 \le k < R$, $X$ is $M+1$ with probability $k/R$ and $M$ otherwise. The structure BatchOrders P N R mu sigma carries the demands, the ordering count $X$ independent of them, and supplierOrder, the sum of the last $R$ demands of retailers $1, \dots, X$; each pattern enters a theorem as a hypothesis on the law of $X$.

Rationing game. Two identical retailers face single-period demand with distribution function $F$, holding cost $h$ and stockout penalty $p$, so the newsvendor quantity $Q^*$ satisfies $F(Q^*) = p/(h+p)$. With probability $r$ the supplier can deliver only $A_1 < 2Q^*$ units in total and allocates them pro rata to the orders, retailer 1 receiving $A_1 Q_1/(Q_1 + Q_2)$; with probability $1 - r$ supply is unlimited. Retailer 1's expected cost when the retailers order $Q_1$ and $Q_2$ is

$$g_1(Q_1) = (1-r)\,\mathrm{nv}(Q_1) + r\,\mathrm{nv}\!\Big(\frac{A_1 Q_1}{Q_1 + Q_2}\Big),$$

with $\mathrm{nv}$ the newsvendor cost; this is rationingCost.

Formalization targets

Goal: Theorem 13.2, demand signal processing

$$\frac{\mathrm{Var}[Q_t]}{\mathrm{Var}[D_t]} \;\ge\; 1 + \Big(\frac{2L}{m} + \frac{2L^2}{m^2}\Big)(1 - \rho^m),$$

with equality when $z_\alpha = 0$. This is bullwhip_signal_processing. The bound exceeds $1$ whenever $L > 0$, whatever the value of $\rho$: a lead time and a moving-average forecast are enough to produce the effect.

Supporting targets

The chapter's own route to the goal, each a milestone: the steady-state moments (13.2) to (13.4), $\mathbb{E}[D_t] = d/(1-\rho)$, $\mathrm{Var}[D_t] = \sigma^2/(1-\rho^2)$ and $\mathrm{Cov}[D_t, D_{t-k}] = \rho^k \mathrm{Var}[D_t]$; the identity $Q_t = (1 + L/m) D_{t-1} - (L/m) D_{t-m-1} + z_\alpha(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1})$; Lemma 13.1, $\mathrm{Cov}[D_{t-i}, \hat\sigma^L_{et}] = 0$ for $1 \le i \le m$; the vanishing of the cross term (13.12); and the variance of the demand part, $\big(1 + (2L/m + 2L^2/m^2)(1 - \rho^m)\big)\mathrm{Var}[D_t]$.

Order batching, Theorem 13.4: under the three patterns the supplier's order has mean $N\mu$ and

$$\mathrm{Var}[Q^c_t] \ge \mathrm{Var}[Q^r_t] \ge \mathrm{Var}[Q^b_t] \ge N\sigma^2,$$

through the three variance formulas $N\sigma^2 + \mu^2 N(R-1)$, $N\sigma^2 + \mu^2 N^2 (R-1)$ and $N\sigma^2 + \mu^2 k(R-k)$.

The rationing game, Theorem 13.3: if $Q > 0$ is a symmetric Nash equilibrium, that is, $Q$ minimizes $g_1$ over positive order quantities when the other retailer orders $Q$, then $Q > Q^*$.

Significance

The three theorems are the quantitative core of the chapter. Theorem 13.2 is the single-stage building block that Theorems 13.6 and 13.7 later iterate along a serial chain, giving the product-form and the exponential lower bounds on the amplification at stage $k$; its comparative statics, the bound decreasing in $m$ and increasing in $L$, are the basis of the remedies the chapter recommends (shorter lead times, smoother forecasts, sharing point-of-sale data). Theorem 13.4 ranks the ordering patterns and justifies the advice to balance ordering days when batching cannot be avoided. Theorem 13.3 shows that pro-rata rationing alone inflates orders; the book is careful to note that inflated orders are not by themselves inflated variances, and that the variance statement for this model is due to Rong, Shen and Snyder (2017).

None of these results has a machine-checked proof. The book's proofs of Theorems 13.2 and 13.4 are complete but informal, and the proof of Lemma 13.1 is omitted with a citation to Ryan's 1997 thesis; formalizing it requires a self-contained argument. The variance decomposition of $Q_t$ and the conditioning argument for Theorem 13.4 are reusable for the multistage results of Sect. 13.2.5, which are natural follow-up missions on the same definitions.

Difficulty

The obvious computation of $\mathrm{Var}[Q_t]$ expands the order into its demand part and its safety-stock part and hopes the cross term disappears. It does, but not for a reason visible in the formulas: $\hat\sigma^L_{et}$ is a square root of a sum of squares of forecast errors, a nonlinear function of $m + m$ demands, and its covariance with a single demand is zero only because the errors are jointly Gaussian with mean zero and $\hat\sigma$ is an even function of them, so the covariance is the expectation of an odd function of a centred Gaussian vector. That is Lemma 13.1, and the vanishing of the cross term needs two further covariances, $\mathrm{Cov}[D_{t-1}, \hat\sigma^L_{e,t-1}]$ and $\mathrm{Cov}[D_{t-m-1}, \hat\sigma^L_{et}]$, which the book reduces to the lemma through the recursion (the second reduction divides by $\rho$) but which hold for every $\rho$ by the same symmetry. A solver must set up the joint Gaussian structure of the demand vector and prove the odd-function argument; nothing in Mathlib does this directly.

The second obstacle is that the moments (13.2) to (13.4) are not assumed but derived: the structure carries the stationary law of each $D_t$ and the independence of $\epsilon_t$ from the past, and the autocovariance $\rho^k \mathrm{Var}[D_t]$ has to be obtained from the recursion by induction on the lag, with integrability supplied by the Gaussian laws.

For Theorem 13.4 the work is the conditioning on $X$: given $X = x$ the supplier's order is a sum of $xR$ independent normals, so its conditional mean is $xR\mu$ and conditional variance $xR\sigma^2$, and the total variance is $\mathbb{E}[\mathrm{Var}[Q \mid X]] + \mathrm{Var}[\mathbb{E}[Q \mid X]]$. The order is defined by a sum over retailers $i < X$, so the independence of $X$ from the demands has to be used through the indicator structure rather than through a conditional-expectation library result.

For Theorem 13.3 the argument is a first-order condition. It requires that the newsvendor cost be differentiable with derivative $(h+p)F(y) - p$, which holds when $F$ is continuous, and that the symmetric equilibrium be an interior minimizer, which is why $Q > 0$ and the minimization over $Q_1 > 0$ are hypotheses.

Formalization scope

Time is indexed by $\mathbb{Z}$ so that $D_{t-m-1}$ exists for every $t$. AR1Demand asserts the recursion for every outcome, the independence of the whole error family, the independence of $\epsilon_t$ from $(D_s)_{s < t}$, and the stationary law of every $D_t$; these are the "steady-state" assumptions the book makes in words. The structure is satisfiable: the stationary Gaussian AR(1) process on a full-measure set of error sequences has all these properties. The constant $C_{L\rho}$ is a free real parameter $C$; no theorem depends on its value.

The goal divides by $\mathrm{Var}[D_t]$, which is $\sigma^2/(1-\rho^2) > 0$ under the structure's hypotheses $\sigma > 0$ and $|\rho| < 1$, so the ratio is a genuine quotient. Mathlib's ProbabilityTheory.variance and covariance are used; both are the ordinary real quantities for square-integrable variables, which every variable here is, $\hat\sigma^L_{et}$ included.

In BatchOrders the demands are indexed by Fin N × Fin R, the count $X$ is a natural-valued random variable bounded by $N$ and independent of the demand family, and supplierOrder sums the $R$ demands of retailers $1, \dots, X$, the book's "without loss of generality" choice. The laws of $X$ are hypotheses on point probabilities P.real {ω | X ω = j}; with $R \ge 1$ each of the three families of hypotheses is satisfiable by a structure with the corresponding law. The subtractions $R - 1$ and $R - k$ are real.

In the rationing game the demand law is a probability measure on $\mathbb{R}$ whose distribution function is continuous and strictly increasing on $[0, \infty)$; the newsvendor loss is assumed integrable at every order quantity. The pro-rata allocation uses Lean's total division, which is never at $0$ in the theorem since $Q_1 + Q_2 > 0$.

Beyond the ten milestones, the multistage Theorems 13.6 and 13.7 and the centralized-information bound of Theorem 13.5 are welcome as extensions on the same AR1Demand.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13. https://doi.org/10.1002/9781119584445
• H. L. Lee, V. Padmanabhan and S. Whang, Information distortion in a supply chain: the bullwhip effect, Management Science 43(4), 1997. https://doi.org/10.1287/mnsc.43.4.546
• F. Chen, Z. Drezner, J. K. Ryan and D. Simchi-Levi, Quantifying the bullwhip effect in a simple supply chain: the impact of forecasting, lead times, and information, Management Science 46(3), 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• G. P. Cachon, Managing supply chain demand variability with scheduled ordering policies, Management Science 45(6), 1999. https://doi.org/10.1287/mnsc.45.6.843
• Y. Rong, Z.-J. M. Shen and L. V. Snyder, The impact of ordering behavior on order-quantity variability: a study of forward and reverse bullwhip effects, Naval Research Logistics 64(1), 2017. https://doi.org/10.1002/nav.21757

Pooling as a design principle

A firm that holds inventory in five warehouses needs more safety stock than one that holds the same inventory in one warehouse, because the demands of five regions do not all run high at once. Eppen (1979) made this precise for a multi-location newsvendor and gave it its name, the risk-pooling effect. Chapter 7 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) follows the same idea through three settings in which pooling happens without physical consolidation: two retailers who ship stock to each other after seeing demand (transshipments, after Tagaras 1989), and plants that can each make more than one product (process flexibility, after Jordan and Graves 1995). The chapter's capstone is the theorem of Simchi-Levi and Wei (2012) that, among designs in which every plant makes two products and every product is made at two plants, a single long chain through all of them is best. This mission formalizes the chapter's numbered results, with that theorem as its goal.

Setting

Risk pooling. $N$ distribution centers face normally distributed per-period demands $D_i \sim N(\mu_i, \sigma_i^2)$ with correlation coefficients $\rho_{ij}$, and each runs a base-stock policy with holding cost $h$ and backorder cost $p$ per unit per period, so its optimal expected cost is the optimal newsvendor cost optNvCost h p D, the infimum over base-stock levels $S$ of $\mathbb{E}[h(S - D)^+ + p(D - S)^+]$. Merging the centers gives one facing the total demand, normal with mean $\sum_i \mu_i$ and variance $\sigma_0^2 = \sum_i \sum_j \sigma_i \sigma_j \rho_{ij}$ (pooledVariance).

Transshipments. Two retailers $i, j$ with base-stock levels $S_i, S_j$ face independent demands. After demand is observed, under complete pooling the retailer with a surplus sends the retailer with a shortage $Y_{ji} = \min\{S_j - D_j,\ D_i - S_i\}$ units (transship), and nothing moves otherwise. The type-1 service level is the probability of no stockout, $\alpha^0_i = \Pr[D_i \le S_i]$ without and $\alpha_i = \Pr[D_i - S_i \le Y_{ji}]$ with transshipments; the type-2 service level is the fill rate, one minus expected unmet demand over expected demand, $\beta^0_i$ and $\beta_i$ likewise.

Process flexibility. A flexibility design on $n$ products and $n$ plants is a set $E$ of (product, plant) pairs, an edge $(i, j)$ meaning plant $j$ can make product $i$. Given a demand realization $d$ and a common plant capacity $C$, the performance $P(d, E)$ (perf) is the maximum sales obtainable by assigning production along the edges of $E$ without exceeding any capacity or demand, the linear program (7.22) to (7.26). A balanced system (BalancedSystem) has equal capacities and an exchangeable demand vector, one whose joint law is invariant under permutations of the products, and $[E] = \mathbb{E}[P(D, E)]$ is the expected performance (expPerf). The named designs are the dedicated design $D_n = \{(i, i)\}$, the long chain $C_n$ in which plant $j$ also makes product $j + 1$ (and plant $n$ makes product $1$), the open chain $L_k$ obtained from $C_k$ by deleting the edge $(1, k)$, and $L^n_k$, the open chain on the first $k$ pairs together with the dedicated edges of the rest. A 2-flexibility design (TwoFlex) is one in which every product has exactly two plants and every plant exactly two products; $C_n$ is one, and so is any union of disjoint shorter chains.

Formalization targets

Goal: Theorem 7.9

For a balanced system of size $n \ge 2$ with exchangeable demand,

$$C_n \in \arg\max_{A \in \mathcal{F}_2} [A],$$

that is, $C_n$ is a 2-flexibility design and $[A] \le [C_n]$ for every 2-flexibility design $A$. This is long_chain_optimal.

Supporting targets

The chapter's route to the goal: Lemma 7.5, supermodularity of sales in the flexible edges of the long chain for every realization, $P(d, E) + P(d, E \setminus \{\alpha, \beta\}) \ge P(d, E \setminus \{\alpha\}) + P(d, E \setminus \{\beta\})$ for $E \subseteq C_n$; Corollary 7.6, the same in expectation; Lemma 7.7, the increments $[L^n_{k+1}] - [L^n_k]$ are nondecreasing in $k$, ending with $[C_n] - [L^n_n]$; and Lemma 7.8, $[C_n] = n([L_n] - [L_{n-1}])$.

Risk pooling, Theorem 7.1: $g^*_C \le g^*_D$, the optimal cost of the merged center is at most the sum of the optimal costs of the separate ones, with the covariance inequality $\sqrt{\sum_i\sum_j \sigma_i\sigma_j\rho_{ij}} \le \sum_i \sigma_i$ as a separate lemma.

Transshipments, Theorems 7.2 to 7.4: $\alpha_i = \alpha^0_i + |\partial\mathbb{E}[Y_{ji}]/\partial S_i|$, $\beta_i = \beta^0_i + \mathbb{E}[Y_{ji}]/\mathbb{E}[D_i]$, and all four post-transshipment service levels are nondecreasing in $S_i$.

Significance

Theorem 7.9 is the analytical answer to a question that had been settled only by simulation: Jordan and Graves reported that one chain through all plants achieves nearly twice the sales benefit of three short chains with the same number of edges, and Simchi-Levi and Wei proved that no arrangement of the same edge budget does better. It is the justification for the chaining guideline used in automotive and semiconductor capacity planning, and Lemma 7.8, which expresses the long chain through open chains, is what makes the long chain's performance computable by a greedy pass. Theorem 7.1 is the quantitative basis for consolidation decisions and for postponement, since a generic product is pooled inventory. Theorems 7.2 to 7.4 quantify what transshipments buy in service, which is the argument for allowing them despite their cost.

None of these results has a machine-checked proof. The book proves Lemma 7.7, Lemma 7.8 and Theorem 7.9 in full given Lemma 7.5, which it cites to Simchi-Levi and Wei, and omits the proofs of Theorems 7.3 and 7.4 and the identity (7.30) behind Lemma 7.8. Formalizing Lemma 7.5 and (7.30) means formalizing the structure of maximum flows on a cycle, which is reusable for the later results of Simchi-Levi and Wei on the long chain's performance relative to full flexibility and for the multi-echelon flexibility models the chapter cites.

Difficulty

The obvious approach to Theorem 7.9 is to compare $C_n$ with an arbitrary 2-flexibility design directly. Nothing in the definitions supports that: the two designs share no structure beyond their degree sequences. The book's argument instead routes everything through the long chain's own edges. Lemma 7.5 gives supermodularity only for subsets of $C_n$, and the decomposition of an arbitrary 2-flexibility design into disjoint cycles, each a relabeled long chain on a subsystem, is what allows the comparison. A solver must therefore prove that a 2-regular bipartite graph is a disjoint union of even cycles, that exchangeability makes every relabeling of a cycle worth the same as $C_{n_j}$ on its subsystem, and that the performance of a disjoint union is the sum of the performances of its parts.

Lemma 7.5 itself is where the combinatorics lives. It says that on the cycle $C_n$ the maximum flow is supermodular in the flexible edges, and the proof in Simchi-Levi and Wei goes through the structure of augmenting paths on a cycle. The natural first idea, that supermodularity follows from some general property of maximum flows, is false: maximum flow is not supermodular in arbitrary edge sets, and the lemma is specific to subsets of a single cycle.

Lemma 7.7 is where exchangeability is used, and it is used in a way that is easy to state and tedious to formalize: removing the edge $(2, 1)$ from $L^n_{k+1}$ leaves a design that is $L^n_k$ only after the pair $1$ is moved to the end, so the argument needs the invariance of $[E]$ under relabeling the products and plants by a common permutation. The book notes that Lemma 7.7, unlike Lemma 7.5, is false realization by realization.

For the transshipment theorems, the book differentiates a density formula by Leibniz's rule. Under the weaker hypothesis stated here, laws without atoms and with finite means, the derivative of $\mathbb{E}[Y_{ji}]$ in $S_i$ has to be obtained by dominated convergence from the pointwise derivative of a piecewise-linear function whose kinks lie on null sets.

Formalization scope

perf is a supremum over a set of reals, nonempty because $y = 0$ is feasible when $d \ge 0$ and $C \ge 0$, and bounded by $\sum_i d_i$; the demand is nonnegative for every outcome and the capacity nonnegative in BalancedSystem, and Lemma 7.5 carries these as hypotheses. The supremum is attained, but the definition does not assert it. Expected performance is a Lebesgue integral; the demand is integrable by assumption and $P(d, E)$ is $1$-Lipschitz in $d$, so the integrand is integrable, and a solver must prove this measurability rather than assume it.

Exchangeability is the equality of the laws of $(D_{\sigma(i)})_i$ and $(D_i)_i$ for every permutation $\sigma$. Designs are finite sets of pairs of Fin n; the chains are defined with finRotate, so indices wrap modulo $n$ and the closing edge of $C_n$ is $(1, n)$ in the book's numbering, which is the edge its proofs and Figure 7.3(c) use. Lemma 7.8 involves open chains on subsystems of sizes $n$ and $n - 1$; these are designs on Fin k evaluated on the first $k$ coordinates of the demand (subDemand, subPerf).

Theorem 7.1 states the optimal costs as infima of the newsvendor cost over all base-stock levels, on Mathlib's gaussianReal; a nonpositive pooled variance gives a degenerate law, for which the inequality still holds, so the statement is not trivialized by that convention. The transshipment theorems take the two demand laws as probability measures on $\mathbb{R}$ with no atoms (Theorem 7.2) and finite, positive means; the quantity $Y_{ji}$ is defined for all outcomes and the service levels are probabilities and expectations under the product law.

The definition module is shared by all eleven items. Beyond the milestones, formalizing the identity (7.30) as its own lemma and the disjoint-union additivity of perf would be natural contributions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 7. https://doi.org/10.1002/9781119584445
• G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5), 1979. https://doi.org/10.1287/mnsc.25.5.498
• G. Tagaras, Effects of pooling on the optimization and service levels of two-location inventory systems, IIE Transactions 21(3), 1989. https://doi.org/10.1080/07408178908966208
• W. C. Jordan and S. C. Graves, Principles on the benefits of manufacturing process flexibility, Management Science 41(4), 1995. https://doi.org/10.1287/mnsc.41.4.577
• D. Simchi-Levi and Y. Wei, Understanding the performance of the long chain and sparse designs in process flexibility, Operations Research 60(5), 2012. https://doi.org/10.1287/opre.1120.1082

Batch quantities that cannot be chosen one site at a time

Chapter 9 of Axsäter's Inventory Control opens with the observation that in a multi-echelon system it is not optimal to choose batch quantities installation by installation: the batch at one site is the demand pattern of the next site upstream. Even with constant customer demand the exact optimum can be complicated, and the book's Example 9.4 shows a four-stage serial system whose optimal batch at one stage alternates between two values over time. Roundy (1985, 1986) showed that this complexity can be avoided at a guaranteed price: restrict every batch quantity to be a power of two times a common basic quantity, nested from stage to stage, and the best such policy costs at most 2 % more than the optimum. The book presents the result for a serial system and remarks that the same approach handles assembly and distribution systems and, in Sect. 7.3.1.2, joint replenishments. It is the capstone of Chapter 9 and the multi-echelon payoff of the powers-of-two analysis of Chapter 7.

Setting

A serial system has $N$ installations; installation $i$ produces item $i$ from one unit of item $i+1$, item $N$ is obtained from an outside supplier, and item 1 faces a constant, continuous final demand $d$. Lead-times are zero, shortages are not allowed, production is instantaneous, and each batch quantity $Q_i$ is constant over time. Installation $i$ has an ordering cost $A_i$ per batch and an echelon holding cost $e_i$ per unit and time unit, charged on the echelon stock (the stock at installation $i$ and everything downstream), so that the cost per time unit is the sum of $N$ single-item costs of the chapter 4 form,

$$C(Q) \;=\; \sum_{i=1}^{N}\Big(e_i\frac{Q_i}{2} + A_i\frac{d}{Q_i}\Big) \qquad\text{(Eq. 9.17).}$$

The book first works out the two-level case, where the optimum has $Q_2 = kQ_1$ for a positive integer $k$, the cost (9.9) is the EOQ cost with modified parameters $A_1 + A_2/k$ and $e_1 + ke_2$, and the best $k$ is found from $k^{*} = \sqrt{A_2e_1/(A_1e_2)}$ by a rounding rule.

For $N$ stages, Roundy's constraints (9.16) require $Q_i = 2^{k_i}Q_{i-1}$ with nonnegative integers $k_i$, so that every solution is nested. The relaxed constraints (9.18) require only $Q_{i-1} \le Q_i$; they are implied by (9.16), the relaxed problem is convex with linear constraints, and its solution $Q^{\mathrm{rel}}$ is computed by aggregating consecutive stages whose cost ratios $A_i/e_i$ decrease. Roundy's solution rounds $Q^{\mathrm{rel}}$ to $Q_i = 2^{m_i}q$ for a basic quantity $q$, chosen as in Proposition 7.2.

Formalization targets

Goal — Roundy's 98 % approximation

For $d > 0$, $A_i > 0$, $e_i > 0$ and any minimizer $Q^{\mathrm{rel}}$ of $C$ over positive batch quantities satisfying (9.18), there exist $q > 0$ and integers $m_1 \le \dots \le m_N$ such that $Q_i = 2^{m_i}q$ satisfies (9.16) and

$$C\big(2^{m}q\big) \;\le\; \frac{1}{\sqrt 2\,\ln 2}\,C\big(Q^{\mathrm{rel}}\big).$$

Supporting targets

The two-level results of Sect. 9.2.1: the equivalence of the installation and echelon cost forms (9.6) and (9.9); the optimal $Q_1$ and cost (9.10)-(9.11) for a given $k$; the closed form and convexity of $C(k)^2$ (9.12) and the real minimizer $k^{*}$ (9.13); and the integer rounding rule with its corollary that $A_1/e_1 \ge A_2/e_2$ forces $k = 1$. For $N$ stages: existence of the relaxed optimum; the aggregation lemma, that $A_i/e_i < A_{i-1}/e_{i-1}$ forces $Q^{\mathrm{rel}}_i = Q^{\mathrm{rel}}_{i-1}$; that (9.16) implies (9.18), so the relaxed optimum bounds every powers-of-two policy from below; and that rounding to the nearest power of two times $q$ is monotone and lands within a factor $\sqrt 2$.

Significance

The result itself. Roundy's theorem replaces an intractable lot-sizing problem by a closed-form computation with a provable 2 % guarantee, and the policies it produces are the nested, periodic schedules that production planning wants anyway. In Example 9.4 the rounding with $q = 1$ is already within 0.7 % of the relaxed bound. The two-level analysis has its own use: the modified parameters $A_1 + A_2/k$ and $e_1 + ke_2$ are what the Blackburn-Millen heuristic of Sect. 9.3.2 feeds to the Wagner-Whitin algorithm under time-varying demand, and the condition $A_1/e_1 \ge A_2/e_2$ tells when a two-stage system collapses to one stage.

Formalizing it. The book proves the bound in a paragraph that leans on three earlier results: Proposition 7.2 for the rounding, the Lagrangean relaxation for the lower bound, and the aggregation algorithm for the structure of $Q^{\mathrm{rel}}$. Formalizing it makes explicit what the paragraph glosses: that the multipliers vanish off tight constraints, that equal quantities round to equal quantities, and that the comparison class is the class of nested constant-batch policies. The published Proposition 7.2 (pot_two_percent) and the mean value $1/(\sqrt 2\ln 2)$ are cited as reference items. Nothing here is open; no statement has a machine-checked proof yet.

Difficulty

The obvious argument, rounding $Q^{\mathrm{rel}}$ item by item and invoking Proposition 7.2 for each, does not work: Proposition 7.2 bounds the rounded cost relative to each item's unconstrained optimum, and $Q^{\mathrm{rel}}_i$ is generally not that optimum. The proof must pass through the Lagrangean relaxation (9.19)-(9.20), under which $Q^{\mathrm{rel}}$ is the unconstrained optimum for the modified holding costs $e_i' = e_i - 2\lambda_i + 2\lambda_{i+1}$, apply Proposition 7.2 there, and transfer the bound back using complementary slackness: the multiplier $\lambda_i$ is positive only where $Q^{\mathrm{rel}}_i = Q^{\mathrm{rel}}_{i-1}$, and equal quantities round to equal quantities, so the correction terms $\lambda_i(Q_i - Q_{i-1})$ vanish for both $Q^{\mathrm{rel}}$ and its rounding. A solver therefore needs the KKT conditions for this convex program, or an equivalent direct argument through the aggregation structure (within an aggregate all quantities are equal and their sum is an EOQ problem). The two-level statements and the rounding lemma are elementary.

Formalization scope

Stages are indexed by Fin N; the cost is serialCost A e d Q = ∑ i, eoqCost (A i) d (e i) (Q i) with eoqCost imported from the chapter 4 definitions, and the two-level cost is eoqCost (A1 + A2/k) d (e1 + k e2) Q1 by definition, so the published eoq_optimal and eoq_cost_at_eoq apply to it directly. SerialNested and SerialPowerOfTwo are the constraints (9.18) and (9.16) on consecutive indices; for $N \le 1$ both hold vacuously and the goal is Proposition 7.2 for one item. potRound q Q is $\lfloor \log_2(Q/q) + \tfrac12\rfloor$.

All theorems assume $d, A_i, e_i > 0$ and positive batch quantities. The book says "nonnegative ordering and echelon holding costs"; strict positivity is needed for the relaxed problem to have a solution at all ($e_i = 0$ or $A_i = 0$ sends the optimal $Q_i$ to $\infty$ or $0$), and it is what the book's own examples satisfy. The relaxed optimum enters the goal as a hypothesis, with existence stated separately; uniqueness is not used. The constant is the exact $1/(\sqrt 2\ln 2)$.

Two readings are excluded. The bound is not against an arbitrary nested $Q$, for which it would be false, but against the relaxed optimum; and the comparison class is stated as nested constant-batch policies, the class the relaxed problem bounds directly, not the book's larger class of time-varying policies, which would need a dynamic model. The definitions are reusable for assembly systems and for the joint replenishment problem of Sect. 7.3.1.2, whose Roundy analysis is the same with a fictive item 0 of zero holding cost; contributions in that direction are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sect. 9.2. DOI 10.1007/978-3-319-15729-0
• Robin Roundy, 98%-Effective Integer-Ratio Lot-Sizing for One-Warehouse Multi-Retailer Systems, Management Science 31(11), 1985, pp. 1416-1430. DOI 10.1287/mnsc.31.11.1416
• Robin Roundy, A 98%-Effective Lot-Sizing Rule for a Multi-Product, Multi-Stage Production/Inventory System, Mathematics of Operations Research 11(4), 1986, pp. 699-727. DOI 10.1287/moor.11.4.699
• John A. Muckstadt and Robin O. Roundy, Analysis of Multistage Production Systems, in: Handbooks in Operations Research and Management Science 4, Elsevier, 1993, pp. 59-131. DOI 10.1016/S0927-0507(05)80182-4
• Peter L. Jackson, William L. Maxwell and John A. Muckstadt, The Joint Replenishment Problem with a Powers-of-Two Restriction, IIE Transactions 17(1), 1985, pp. 25-32. DOI 10.1080/07408178508975268

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

Safety stock in a chain

Chapter 10 of Axsäter's Inventory Control turns to reorder points and safety stocks in multi-echelon systems, where the installations cannot be treated separately: a large stock downstream lets an upstream site run lean, and a long upstream lead-time argues for stock at the top. The best-known exact technique for serial systems is the decomposition of Clark and Scarf (1960), which the book presents in the infinite-horizon form of Federgruen and Zipkin (1984). It is also where the echelon stock measure comes from. The section's argument is short and self-contained, and its conclusion is a complete description of the optimal policy for a two-level serial system: order-up-to levels at both installations, one of them a newsboy solution, the other the minimizer of a convex function in which upstream shortages appear as an induced cost. It is the capstone of Chapter 10.

Setting

Installation 1 faces normally distributed period demand with mean $\mu$ and standard deviation $\sigma$, independent across periods, so the demand over $n$ periods, $D(n)$, is normal with mean $n\mu$ and standard deviation $\sqrt n\,\sigma$. Installation 1 replenishes from installation 2 with lead-time $L_1$ periods; installation 2 replenishes from an outside supplier with infinite supply and lead-time $L_2$. Demand that cannot be met is backordered. Costs per unit and period are echelon holding costs $e_1, e_2 \ge 0$, so the installation holding costs are $h_1 = e_1 + e_2$ and $h_2 = e_2$, and a shortage cost $b_1$ at installation 1; there are no ordering costs. Events in a period occur in the order: installation 2 orders, its delivery arrives, installation 1 orders, its delivery arrives, demand, cost evaluation.

Consider an arbitrary period $t$. After ordering, installation 2 has an echelon inventory position $y_2$, and by the standard argument its echelon stock in period $t + L_2$ is $y_2 - D(L_2)$. Installation 1 then orders, realizing an echelon position $y_1$ that cannot exceed what is available: $y_1 \le y_2 - D(L_2)$ (Eq. 10.1). Its inventory level after the demand in period $t + L_2 + L_1$ is $y_1 - D(L_1+1)$. The expected period costs are $C_2 = h_2\,\mathbb{E}(y_2 - D(L_2) - y_1)$ at installation 2 and $C_1 = h_1\,\mathbb{E}(y_1 - D(L_1+1))^{+} + b_1\,\mathbb{E}(y_1 - D(L_1+1))^{-}$ at installation 1, and the book reallocates the term $-h_2y_1$ to obtain

$$\tilde C_2(y_2) = h_2(y_2 - \mu_2'), \qquad \tilde C_1(y_1) = e_1y_1 - h_1\mu_1'' + (h_1 + b_1)\,\mathbb{E}\big(y_1 - D(L_1+1)\big)^{-},$$

with $\mu_2' = L_2\mu$ and $\mu_1'' = (L_1+1)\mu$. As a function of a free $\hat y_1$, $\tilde C_1$ is the newsboy-type function $\hat C_1$ of Eq. (10.6), minimized at the level $S_1 = \hat y_1^{*}$ given by the fractile equation (10.8). Passing everything available up to $S_1$ to installation 1, $y_1 = \min\{S_1, y_2 - D(L_2)\}$, gives the total cost $\hat C_2(y_2)$ of Eq. (10.9), whose minimizer $S_2 = y_2^{*}$ is the order-up-to level of installation 2.

Formalization targets

Goal — the decomposition

With $S_1$ from (10.8) and $S_2$ a minimizer of $\hat C_2$: for every $y_2$ and every allocation rule $a$ with $a(u) \le y_2 - u$ and finite expected cost,

$$\hat C_2(S_2) \;\le\; \mathbb{E}\big[\tilde C_2(y_2) + \tilde C_1(a(D(L_2)))\big],$$

and the order-up-to policy $(S_1, S_2)$ attains $\hat C_2(S_2)$.

Supporting targets

Eq. (10.3), the stage-1 period cost through the expected backorders; the reallocation (10.4)-(10.5), which leaves the total unchanged; the closed form (10.6) of $\hat C_1$ through the loss function $G$; the convexity of $\hat C_1$, its derivative (10.7), and the fractile characterization (10.8) of its minimizers; the pointwise rule that $\min\{S_1, y_2 - u\}$ is the cheapest feasible $y_1$; the identity (10.9); and the convexity of $\hat C_2$ (Problem 10.1) with the existence of its minimizer when $e_2 > 0$.

Significance

The result itself. The decomposition reduces a two-dimensional stochastic control problem to two one-dimensional convex problems solved in sequence, from downstream to upstream, and it identifies the optimal policy class. The downstream level $S_1$ is a newsboy solution with overage cost $e_1$, the value added, and underage cost $e_2 + b_1$, and it is independent of the upstream installation altogether; the upstream level $S_2$ sees the downstream installation only through the induced shortage cost, the last term of (10.9). The book notes the extensions the argument admits, to more echelons, to batch ordering at the top, and, via Rosling's equivalence, to assembly systems, and its Sect. 10.1.2 adapts it, now only approximately, to distribution systems under the balance assumption. Example 10.1 shows the typical outcome: the optimal average stock at the upstream installation is slightly negative.

Formalizing it. The section's mathematics is a chain of expectations under Gaussian laws and two convexity arguments. Formalizing it fixes what "optimal" means, a per-period comparison against every allocation rule, and separates the two convexity claims the book makes in one clause each. Nothing here is open; no statement has a machine-checked proof yet.

Difficulty

The pointwise allocation rule and the newsboy fractile are the same arguments as in the newsboy mission. The two places where work is needed are the identity (10.9), an expectation of a piecewise function split at $u = y_2 - S_1$, and the convexity of $\hat C_2$, which requires seeing that $x \mapsto \hat C_1(\min\{S_1, x\})$ is convex precisely because $S_1$ is a minimizer of the convex $\hat C_1$ (for any other cut-off the function is not convex), and that convexity is preserved by integrating against the law of $D(L_2)$, which needs the integrability of the linearly growing $\hat C_1$. Existence of $S_2$ then follows from the growth of $\hat C_2$ at both ends, which comes from the asymptotics of the loss function: $G(z) \to 0$ as $z \to \infty$ and $G(z) + z \to 0$ as $z \to -\infty$.

Formalization scope

$D(n)$ is csDemand mu sigma n, the Gaussian law newsboyDemand (n μ) (√n σ) from the newsboy mission, so the loss function $G$ and its closed form are reused as references. The costs are parametrized by $e_1, e_2, b_1$ with $h_1 = e_1 + e_2$ and $h_2 = e_2$ written out; $\tilde C_1$, $\tilde C_2$, the pre-reallocation period cost and $\hat C_2$ are Bochner integrals against these laws. Every statement assumes $\sigma > 0$; the goal and the convexity statements assume $e_1, e_2 \ge 0$ and $b_1 > 0$, the book's cost signs. $L_2 = 0$ is allowed and makes $D(L_2)$ a point mass, which is the setting of the book's Problem 10.2.

$S_1$ enters as any solution of the fractile equation (10.8) and $S_2$ as any minimizer of $\hat C_2$; the other items show that both exist when $e_1, e_2 > 0$. When $e_1 = 0$ the fractile is $1$, no $S_1$ exists, and the goal is vacuous, which is faithful: the book observes that then $S_1 \to \infty$ and installation 2 never carries stock. Symmetrically, when $e_2 = 0$ and $L_2 \ge 1$, $\hat C_2$ decreases towards its infimum without attaining it, so no $S_2$ exists and the goal is again vacuous: with free upstream holding the optimal $y_2$ is unbounded. Allocation rules are arbitrary functions of the realized $D(L_2)$ with an integrability hypothesis; without it Lean's integral of a non-integrable cost would be $0$ and could undercut $\hat C_2(S_2)$, which is negative in Example 10.1's stage-1 term.

What is not modelled is the infinite-horizon dynamic problem: the book's optimality claim is made period by period, and the passage to the stationary policy rests on the remark that the outside supplier has infinite supply, so the same $y_2$ can be chosen in every period. The definitions are reusable for the three-echelon extension and for the distribution system of Sect. 10.1.2; contributions formalizing Problem 10.2 ($L_2 = 0$) as a first step are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sect. 10.1.1. DOI 10.1007/978-3-319-15729-0
• Andrew J. Clark and Herbert Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4), 1960, pp. 475-490. DOI 10.1287/mnsc.6.4.475
• Awi Federgruen and Paul Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4), 1984, pp. 818-836. DOI 10.1287/opre.32.4.818
• Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4), 1989, pp. 565-579. DOI 10.1287/opre.37.4.565
• Geert-Jan van Houtum, Karl Inderfurth and Willem H. M. Zijm, Materials Coordination in Stochastic Multi-Echelon Systems, European Journal of Operational Research 95(1), 1996, pp. 1-23. DOI 10.1016/0377-2217(96)00080-8