Submission hold — source-fidelity repair (2026-09-04). The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.

Motivation

A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.

This mission turns CUHK-Shenzhen AI Math Problem 13, First-passage time of Brownian motion to an exponentially decaying boundary, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.

Suggested attack route

Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.

Formalization scope

The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.

Milestones

For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original CUHK-Shenzhen problem

Motivation

Blood platelets, fresh produce and many pharmaceuticals have a fixed lifetime: a unit not used within $m$ periods of its arrival must be discarded. Optimal ordering for such products depends on the whole age profile of the stock, and the dynamic program that describes it has an $(m-1)$-dimensional state. It is intractable beyond small $m$ (Nahmias, 1982; Nandakumar & Morton, 1993), so practice relies on base-stock policies, which raise the total stock to a fixed level $S$ every period.

Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first performance guarantees for base-stock policies in this system. Under first-in-first-out (FIFO) issuance a heuristic base-stock level is asymptotically optimal in the lifetime, the demand population, the penalty cost and the outdating cost (missions 1–4 of this series). Under last-in-first-out (LIFO) issuance, which models a customer who picks the freshest unit from the shelf, a simple base-stock level is asymptotically optimal in the penalty cost and, when demand can be arbitrarily small, in the outdating cost (Theorem 5, mission 5). This mission formalizes the complementary negative result: when the demand is bounded away from zero, no base-stock policy is asymptotically optimal under LIFO as the outdating cost grows.

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0 < \mathbb E[D] < \infty$ and distribution function $F$. The lower support is $\underline D = \inf\{x : F(x) > 0\}$, and the newsvendor level is $S^{NP} = F^{-1}(p/(p+h))$ with $F^{-1}(x) = \inf\{y : F(y) \ge x\}$.

The product has lifetime $m \ge 1$. At the start of period $t$ the state is $x_t = (x_{t,1}, \dots, x_{t,m-1})$, where $x_{t,i}$ is the stock with remaining lifetime at most $i$; the system starts empty. The firm orders $q_t \ge 0$, which arrives at once, raising the total stock to $x_{t,m} = x_{t,m-1} + q_t$. Demand $D_t$ is served youngest stock first, unmet demand is lost, and stock reaching the end of its lifetime outdates. Under LIFO the outdated amount and the next state are

$$o_t = \min\{(x_{t,m} - D_t)^+, x_{t,1}\}, \qquad x_{t+1,i} = \min\{(x_{t,m} - D_t)^+, x_{t,i+1}\} - o_t .$$

Each period costs $C^\pi_t = h(x_{t,m} - D_t)^+ + p(D_t - x_{t,m})^+ + \theta o_t$ with $h, p > 0$ and $\theta \ge 0$. A policy is admissible if its order in period $t$ is a nonnegative measurable function of the current state. Its long-run average cost is $C^\pi = \limsup_T \frac1T \sum_{t=1}^T \mathbb E[C^\pi_t]$, and $\mathrm{OPT}^{LIFO} = \inf_\pi C^\pi$. The base-stock policy $\pi_S$ orders $(S - x_{t,m-1})^+$, with cost $C^{LIFO}(S)$. The subscript $\theta$ marks the outdating cost; $h$, $p$, $m$ and the demand law are fixed.

Formalization targets

Goal: Proposition 1 (p. 17)

If $m \ge 2$ and $S^{NP} > \underline D > 0$, then

$$\lim_{\theta\to\infty}\big(C^{LIFO}_\theta(S^{LIFO,*}_\theta) - \mathrm{OPT}^{LIFO}_\theta\big) > 0,$$

where $C^{LIFO}_\theta(S^{LIFO,*}_\theta) = \inf_{S \ge 0} C^{LIFO}_\theta(S)$ is the best base-stock cost. The goal asserts that both costs are finite, and that the limit exists and is strictly positive.

Milestones (Appendix C.3, pp. ec8–ec9)

1. Under $m\ge2$ and $S^{NP}>\underline D>0$, $\lim_{\theta\to\infty} \min_{S\ge0} \hat C_{L,\theta}(S) = p(\mathbb E[D] - \underline D)$, where $\hat C_L(S) = h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+] + \frac{\theta}{m}\mathbb E[(S - \max\{D_1,\dots,D_m\})^+]$ is the lower bound (11).
2. Under the same hypotheses, $\lim_{\theta\to\infty} C_\theta(S^{LIFO,*}_\theta) = p(\mathbb E[D] - \underline D)$.
3. Under the same hypotheses, $h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+] \le p(\mathbb E[D] - \underline D)$ for all $S \in [\underline D, \min\{S^{NP}, m\underline D\}]$.
4. The policy that orders $\min\{S^{NP}, m\underline D\}$ units in periods $1, m+1, 2m+1, \dots$ and uses base-stock level $\underline D$ otherwise is admissible, and its long-run average cost is strictly less than $p(\mathbb E[D] - \underline D)$ and independent of $\theta$.
5. $\lim_{\theta\to\infty} \mathrm{OPT}^{LIFO}_\theta < p(\mathbb E[D] - \underline D)$.

The proof also uses Lemma 3 ($\hat C_L \le C^{LIFO} \le \hat C_U$, p. 16) and inequality (EC.22) (p. ec8). Both are milestones of mission 5 of this series and are not restated here.

Significance

Proposition 1 marks the boundary of Theorem 5(c). Together they show that under LIFO, with a large outdating cost, base-stock policies are asymptotically optimal exactly in the trivial cases $m = 1$ or $S^{NP} \le \underline D$, and when $\underline D = 0$. In the remaining case some optimality gap persists however large $\theta$ is. Under FIFO the heuristic level is asymptotically optimal in $\theta$ without conditions (Theorem 4), so the result separates the two issuance rules: a manager facing fresh-first customers and costly waste should look beyond base-stock policies.

The result is proved in the paper; nothing in it is machine-checked. A formal proof would give the first verified statement about the long-run cost of a perishable inventory system. It would also produce reusable pieces: the LIFO recursion, the base-stock cost under LIFO, and a time-dependent policy whose cost can be computed exactly.

Difficulty

The obvious argument compares two limits. The limit of the best base-stock cost needs a lower bound valid for every base-stock level at once, and that bound must be uniform as $\theta$ changes. The lower bound $\hat C_L$ of Lemma 3 controls the outdating only through $\mathbb E[(S - \max_i D_i)^+]$, so the limit of its minimum has to be computed separately. The upper side cannot use a base-stock policy at all. It needs an explicit policy that is not stationary. That policy must be shown never to outdate along every demand path, and its periodic cost has to be bounded strictly below $p(\mathbb E[D]-\underline D)$. The strictness needs the facts that $S^{NP} > \underline D$ and that $m\underline D > \underline D$, which is where $m \ge 2$ and $\underline D > 0$ enter. A long-run average over a non-stationary policy is a $\limsup$ of Cesàro means, and the step from per-period bounds to the average has to be made explicitly.

Formalization scope

• Demand is the published CappedBaseStock.DemandLaw: a probability law on $[0,\infty)$ with finite positive mean. The demand path carries the i.i.d. product law. The newsvendor cost $h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+]$ and $S^{NP}$ are backorderCost and newsvendorLevel of the published LostSalesOrderUpTo.Asymptotic.Backorder.
• Time is zero-based: Lean period $t$ is the paper's period $t+1$, and the cyclic policy's periods $1, m+1, \dots$ are Lean periods with $t \bmod m = 0$.
• The state is a vector of cumulative levels Fin (m - 1) → ℝ with $x_{t,0} := 0$, so $m = 1$ is allowed. Levels $S$ range over $[0,\infty)$.
• Period costs are in $[0,\infty]$, and expectations are lower Lebesgue integrals over the path law. $C^\pi$ is the $\limsup$ of Cesàro averages.
• $\Pi$ is the paper's class: time-dependent, deterministic, measurable functions of the current state. $\mathrm{OPT}^{LIFO}$ is the infimum over all of $\Pi$, not over base-stock policies.
• $C(S)$ is the simulated long-run average cost of $\pi_S$, not a formula. The best base-stock cost is $\inf_{S\ge0} C(S)$, because existence of a minimizer under LIFO is not shown. "min" in milestone 1 is likewise an infimum of a nonnegative real function.
• Limits in $\theta$ are along $\theta \in [0,\infty)$ with the other parameters fixed. The goal subtracts real values only after asserting finiteness, so neither $\infty - \infty$ nor a truncated subtraction can make it true. A formalization that fixes $\theta$, sets $m = 1$, restricts $\mathrm{OPT}$ to base-stock policies or defines $C(S)$ by the bound of Lemma 3 would trivialize or falsify the statement, and is ruled out.

The work needs a Cesàro-limit toolkit for $[0,\infty]$-valued sequences, the LIFO sample-path recursion, and convexity facts for the newsvendor cost. Proofs of the milestones, and of the definitional sanity facts ($\pi_S \in \Pi$, $C(S) < \infty$), are welcome.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, SSRN 3724966, 2022. https://ssrn.com/abstract=3724966 (version of record: Management Science, 2022, doi:10.1287/mnsc.2022.4400).
• S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 680–708, 1982. https://doi.org/10.1287/opre.30.4.680
• P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1490–1498, 1993. https://doi.org/10.1287/mnsc.39.12.1490

Perishable inventory with backlogging and lead times

Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that is not used within $m$ periods of its arrival must be discarded. Managing such products is a classical problem of inventory theory (Nahmias 1982, Operations Research 30(4), doi:10.1287/opre.30.4.680). The optimal ordering policy depends on the entire age profile of the stock, so it is computationally intractable beyond very short lifetimes, and practitioners use base-stock policies, which raise a single aggregate quantity to a fixed level $S$ every period.

Bu, Gong and Chao (SSRN 3724966, accepted manuscript, 2022; Management Science) give the first theoretical performance guarantees for base-stock policies in perishable systems. This mission covers §5 of the paper: the backlogging system with a positive replenishment lead time $L$, where unmet demand waits and orders arrive $L$ periods after they are placed. Earlier missions of this series treat the zero-lead-time lost-sales system under FIFO issuance (missions 1–4) and under LIFO issuance (missions 5–6).

Setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$. The product has lifetime $m\ge1$, the lead time is $L$, and the unit costs are $h>0$ (holding, per unit left over), $b>0$ (backlogging, per unit per period) and $\theta$ (outdating, in addition to holding). Throughout, $\theta\ge hL$.

In period $t$ the order placed in period $t-L$ arrives and serves backorders first. The firm then observes the state $\mathbf x_t=(x_{t,1},\dots,x_{t,m+L-1})$: for $i\le m$, $x_{t,i}$ is the on-hand stock with remaining lifetime at most $i$ minus the backorders, and for $m<i<m+L$ it adds the pipeline orders that arrive by period $t+i-m$. The firm orders $q_t\ge0$, which raises the inventory position to $x_{t,m+L}=x_{t,m+L-1}+q_t$. Demand $D_t$ is served oldest-first (FIFO), the shortfall is backlogged, and with the outdated quantity $o_t=(x_{t,1}-D_t)^+$ the state moves by

$$x_{t+1,i}=x_{t,i+1}-D_t-o_t,\qquad i=1,\dots,m+L-1 .$$

The system starts empty. The cost of period $t$ is $C^\pi_t=h(x_{t,m}-D_t)^++b(D_t-x_{t,m})^++\theta o_t$, where $x_{t,m}$ is the net on-hand inventory.

An admissible policy $\pi\in\Pi$ orders $\varphi^\pi_t(\mathbf x_t)\ge0$ with each $\varphi^\pi_t$ measurable. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$, and $\mathrm{OPT}^L=\inf_{\pi\in\Pi}C^\pi$. The base-stock policy $\pi_S$ orders $(S-x_{t,m+L-1})^+$; its cost is $C^L(S)$. The heuristic level $\widetilde S^L$ is any minimizer over $[0,\infty)$ of

$$\widetilde C^L(S)=h\mathbb E\Big[\Big(S-\sum_{i=1}^{L+1}D_i\Big)^+\Big]+b\mathbb E\Big[\Big(\sum_{i=1}^{L+1}D_i-S\Big)^+\Big]+\frac{\theta-hL}{m+L}\mathbb E\Big[\Big(S-\sum_{i=1}^{m+L}D_i\Big)^+\Big].$$

Formalization targets

Goal: Theorem 7 (p. 20)

For $L\ge1$ and every minimizer $\widetilde S^L$, the gap $C^L(\widetilde S^L)-\mathrm{OPT}^L$

(a) is at most $K_1e^{-K_2m}$ for all lifetimes $m\ge1$, with $K_1,K_2>0$ independent of $m$;

(b) if the one-period demand has the population form $D(n)=\sum_{j=1}^{N(n)}\hat D_j$ of (7), with $N(n)=\sup\{N:\sum_{k=1}^NX_k/n\le1\}$ and the moment assumptions of Theorem 2, is at most $K_1e^{-K_2n}$ for all large $n$, for every fixed lifetime $m\ge2$;

(c) tends to $0$ as $\theta\to\infty$, for every choice $\theta\mapsto\widetilde S^L_\theta$ of minimizers.

Milestones

$$x^\pi_{t+L,m}=x^\pi_{t,m+L}-\sum_{i=t}^{t+L-1}D_i-\sum_{i=t}^{t+L-1}o^\pi_i,\qquad \sum_{i=t}^{t+m+L-1}o^\pi_i\ge\Big(x^\pi_{t,m+L}-\sum_{i=t}^{t+m+L-1}D_i\Big)^+ \quad\text{(EC.29), (EC.30)}$$

Lemma 5 (p. 19): for $L\ge0$ and $S\ge0$, $C^L(S)\ge\widetilde C^L(S)$, and $C^L(S)$ is at most the same expression with $\frac{\theta-hL}{m+L}$ replaced by $\theta+bL$. Proposition 4 (p. 23): $\mathrm{OPT}^L\ge\widetilde C^L(\widetilde S^L)$ for $L\ge1$. Inequality (28) (p. 24):

$$C^L(\widetilde S^L)-\mathrm{OPT}^L\le\frac{(m-1)\theta+(b(m+L)+h+\theta)L}{m+L}\,\mathbb E\Big[\Big(\widetilde S^L-\sum_{i=1}^{m+L}D_i\Big)^+\Big].$$

Significance

Theorem 7 says that a policy computed from one convex function of one variable is nearly optimal for a control problem whose state has dimension $m+L-1$, in three practically relevant regimes: long shelf life, high-volume demand, and expensive waste. The bound (28) is explicit and computable from the demand distribution, so it also certifies, for any given instance, how far $\pi_{\widetilde S^L}$ can be from optimal. Lemma 5 gives two-sided bounds on the cost of every base-stock policy without solving for a stationary distribution of the age profile.

The paper proves Theorem 7 by sketch (§6.2: "We omit the details for brevity"), relying on the arguments for the zero-lead-time Theorems 1, 2 and 4. None of these results has a machine-checked proof. The mission's work is therefore to formalize the lead-time bookkeeping (EC.29)–(EC.33), the lower bound of Proposition 4 with its conditional-Jensen step, the convergence argument in each regime, and the omitted details of the sketch.

Difficulty

The lower bound on $\mathrm{OPT}^L$ must hold for every admissible policy, including those that use the full age profile and the pipeline, whose optimal form is unknown. The obvious route, comparing with the non-perishable backlogging system where a base-stock policy is optimal (Karlin–Scarf), gives a lower bound that ignores outdating entirely and is too weak to make the gap vanish; outdating costs incurred by an arbitrary policy have to be accounted for, and the lead time means that units outdate up to $m+L$ periods after the order that created them. The standing assumption $\theta\ge hL$ is exactly what keeps the coefficient of the outdating term in $\widetilde C^L$ nonnegative. The upper bound requires the long-run cost of $\pi_S$ although the age-profile chain need not have a stationary law that is easy to describe.

In the limits, the heuristic level $\widetilde S^L$ moves with the varying parameter. For (a), a uniform bound on $\widetilde S^L_m$ in $m$ is needed; for (b), the newsvendor level of the compound demand grows with $n$ and concentration of $N(n)$ is required (Scarf's bound and a Bernstein inequality in the zero-lead-time case); for (c), $\theta\,\mathbb E[(\widetilde S^L_\theta-\sum_{i=1}^{m+L}D_i)^+]\to0$ must be shown although the coefficient of (28) grows linearly in $\theta$.

Formalization scope

• Namespace PerishBaseStock.Backlog. Demand laws, the i.i.d. path law, the lead-time sum law and the newsvendor expectations are imported from the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.
• Time is zero-based: Lean period $t$ is the paper's period $t+1$, and the demand d t is $D_{t+1}$.
• The state is a signed vector Fin (m + L - 1) → ℝ of cumulative levels; when $m+L=1$ it is empty and $x_{t,0}:=0$.
• Base-stock levels range over $[0,\infty)$ (ℝ≥0).
• Costs live in $[0,\infty]$; expectations are lower Lebesgue integrals over the demand path law. The long-run average is a limsup of Cesàro means. $\Pi$ is the paper's class: deterministic, time-dependent, measurable functions of the current state.
• $C^L(S)$ is the simulated long-run average cost of $\pi_S$, never the formula of Lemma 5.
• "$\widetilde S^L$ is a minimizer" is a predicate, and every statement quantifies over every minimizer (over every selection of minimizers in (c)).
• Gaps are stated as $C^L(\widetilde S^L)\le\mathrm{OPT}^L+B$; in (c) as a difference of real values together with finiteness of $C^L(\widetilde S^L_\theta)$.
• The standing assumptions $m\ge1$, $h,b>0$, $\theta\ge hL$ are the predicate Params.Standing; $L\ge1$ is an explicit hypothesis of Proposition 4, (28) and Theorem 7. Proposition 4 is formalized for FIFO issuance, the only issuance rule the paper specifies for this system.
• Part (b) is posed for lifetimes $m\ge2$. The page states it for every $m\ge1$, but at $m=1$ the bound (28) does not decay in $n$ (both $\widetilde S^L_n$ and $\sum_{i=1}^{1+L}D_i$ are of order $(L+1)n\,\mathbb E[\hat D_1]$), and the Theorem 2 argument the paper invokes needs $m\ge2$ (p. 12).
• In (b), the demand of form (7) is built on a product of two independent i.i.d. sequences; $N(n)$ is $\mathbb N\cup\{\infty\}$-valued and $D(n)$ is set to $0$ on the null event where it is infinite.

Trivializing formalizations are ruled out: $\mathrm{OPT}^L$ is an infimum over all measurable state-feedback policies, not over base-stock policies; $C^L(S)$ is the long-run average of the simulated cost; neither $m$, $L$, $\theta$ nor the demand law is fixed; and no gap is stated through a truncated subtraction or an infinite $\mathrm{OPT}^L$.

A complete development needs the long-run behaviour of the base-stock dynamics, conditional Jensen for policies adapted to past demand, exponential tail bounds for sums of i.i.d. demands, and, for (b), renewal-count moments and concentration. The sample-path lemmas (EC.29)–(EC.30) and Lemma 5 are reusable for other perishable models with lead times. Proofs of any milestone and of the individual parts (a), (b), (c) are welcome.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, SSRN 3724966, 2022; Management Science. https://ssrn.com/abstract=3724966
• S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680
• S. Karlin, H. Scarf, Inventory Models of the Arrow–Harris–Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• J. F. C. Kingman, Some Inequalities for the Queue GI/G/1, Biometrika 49(3/4):315–324, 1962. https://doi.org/10.2307/2333566

Motivation

Blood platelets, fresh produce, bakery items and many pharmaceuticals have a fixed lifetime: a unit that is not used within $m$ periods of arrival must be discarded. Replenishing such a product is a classical problem of inventory theory (Nahmias 1982), and its optimal policy depends on the whole age profile of the stock, so it cannot be computed for realistic lifetimes. Practice therefore relies on base-stock policies, which raise total stock to a fixed level every period.

Bu, Gong and Chao give the first theoretical guarantees for such a policy. Under first-in-first-out (FIFO) issuance they choose the level $\widetilde S$ by minimizing an explicit surrogate of the long-run cost and show that its optimality gap vanishes in four regimes. This mission is the fourth: a large unit outdating cost $\theta$. The regime matters in practice because outdating is expensive. Slonim et al. (2014) put the component cost of a unit of blood sold to U.S. hospitals at about $570, and disposing of expired products often requires costly handling.

Setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a non-negative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F$. The product lives $m\ge1$ periods. At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$, where $x_{t,i}$ is the stock with remaining lifetime at most $i$. The firm orders $q_t\ge0$, raising the total stock to $x_{t,m}=x_{t,m-1}+q_t$ (lead time zero). Demand is served oldest first and unmet demand is lost. The quantity $o_t=(x_{t,1}-D_t)^+$ outdates, and the state evolves by

$$x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1.$$

The system starts empty. The period cost is

$$C^\pi_t=h(x^\pi_{t,m}-D_t)^+ + p(D_t-x^\pi_{t,m})^+ + \theta o^\pi_t,$$

with holding cost $h>0$, lost-sales penalty $p>0$ and outdating cost $\theta\ge0$.

A policy is admissible if each period's order is a non-negative measurable function of the current state. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$, and $\mathrm{OPT}_\theta$ is the infimum of $C^\pi$ over admissible policies. The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$, and $C_\theta(S)$ is its long-run average cost. The heuristic level $\widetilde S_\theta$ is any minimizer over $[0,\infty)$ of

$$\widetilde C_\theta(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac\theta m\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big].$$

The lower support of demand is $\underline D=\inf\{x:F(x)>0\}$.

Formalization targets

Goal: Theorem 4 (p. 14)

$$\lim_{\theta\to\infty}\big(C_\theta(\widetilde S_\theta)-\mathrm{OPT}_\theta\big)=0,$$

for every selection $\theta\mapsto\widetilde S_\theta$ of minimizers, with $h$, $p$, $m$ and the demand law fixed. The statement holds for every demand law, whether $\underline D$ is zero or positive.

Milestones (Appendix B.3 and §6.2)

1. (EC.16): for every $\theta\ge0$, $\widetilde C_\theta(\widetilde S_\theta)\le\min_{0\le S\le m\underline D}\widetilde C_\theta(S)=\min_{0\le S\le m\underline D}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]\}$.
2. $S^0=m\underline D$: $\sup\{S\ge0:\mathbb E[(S-\sum_{i=1}^mD_i)^+]=0\}=m\underline D$.
3. (EC.17): for the least minimizers, $\widetilde S_\infty=\lim_\theta\widetilde S_\theta$ exists, the newsvendor cost of $\widetilde S_\theta$ converges to that of $\widetilde S_\infty$, and the limit is at least $\min_{0\le S\le m\underline D}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]\}$.
4. (24): $\lim_{\theta\to\infty}\theta\,\mathbb E[(\widetilde S_\theta-\sum_{i=1}^mD_i)^+]=0$ for every selection of minimizers.

The goal's proof also uses inequality (21), $C(\widetilde S)-\mathrm{OPT}\le\frac{(m-1)\theta}{m}\mathbb E[(\widetilde S-\sum_{i=1}^mD_i)^+]$. That inequality, together with Lemmas 1–2 and Proposition 2 behind it, is posed in mission 1 of this series and is not restated here.

Significance

Theorem 4 says that when outdating is expensive, a policy computed from a one-dimensional convex function is as good as the optimal age-dependent policy. A base-stock policy does not need to track the age distribution, and its level can be found by simulation and golden-section search between explicit bounds. Together with Theorems 1–3 it shows that $\widetilde S$ is asymptotically optimal in all four regimes of the paper. Remark 2 of the paper notes that the plain newsvendor level $S^{NP}$ fails in this regime.

The result is proved in the paper (Management Science, 2022). It has not been formalized. This mission adds a machine-checked model of the FIFO perishable system with lost sales: the age-structured dynamics, admissible policies, long-run average costs and the optimal cost over all policies. The model is reusable for the other missions of the series and for the wider perishable-inventory literature. The paper's proof leaves several steps to the reader: the monotonicity of $\widetilde S_\theta$, the identity $S^0=m\underline D$, and continuity of the newsvendor cost. Each of these becomes an explicit statement.

Difficulty

The obvious argument compares the heuristic with an optimal policy directly. That fails because the optimal policy has no tractable form. The proof instead goes through (21), a lower bound on $\mathrm{OPT}$ obtained by a sample-path argument, and then has to show that the outdating term of the heuristic level vanishes faster than $\theta$ grows. That needs uniform control of $\widetilde S_\theta$ as $\theta\to\infty$. The level must eventually fall into $[0,m\underline D]$, where no stock survives $m$ periods of demand, and the newsvendor cost there must match the restricted minimum. A naive reading of "$\widetilde S_\theta$ decreases in $\theta$" holds only for the least minimizer. For an arbitrary selection, the argument has to work through the bound (EC.16) alone.

Formalization scope

• Lean 4 with Mathlib. Everything sits in the namespace PerishBaseStock.Outdating and builds on the published demand layer CappedBaseStock_Model (i.i.d. demand path, demand law with $0<\mathbb E[D]<\infty$) and the newsvendor functions of LostSalesOrderUpTo.Asymptotic.Backorder.
• Time is zero-based: Lean period $t$ is the paper's period $t+1$. The state is Fin (m - 1) → ℝ≥0 of cumulative levels, with $x_{t,0}=0$. When $m=1$ the state is empty and everything left over outdates. Levels $S$ range over $\mathbb R_{\ge0}$.
• Costs take values in $[0,\infty]$. Expectations of costs are lower Lebesgue integrals over the demand-path law, and $C^\pi$ is the limsup of Cesàro averages. $\mathrm{OPT}_\theta$ is the infimum over all admissible policies: time-dependent measurable functions of the state, as in the paper.
• $C_\theta(S)$ is the limsup average of the simulated cost of $\pi_S$, never a closed form.
• $\theta$ ranges over $\mathbb R_{\ge0}$, and limits are taken along atTop there. The goal asserts that $C_\theta(\widetilde S_\theta)$ is finite and that the difference of real values tends to $0$, so no $\infty-\infty$ convention enters.
• "A minimizer" means every minimizer. (EC.17) is posed for the least minimizer, the selection for which the paper's monotonicity claim holds.
• $\underline D$, $S^0$ and the restricted minimum are real infima and suprema over nonempty, bounded sets, so Lean's default values never arise.
• The model must not be trivialized: a fixed $m$, $\theta=0$, a restriction of $\mathrm{OPT}$ to base-stock policies, or $\widetilde S_\theta$ replaced by a closed form would each change the theorem, and none is used.
• Welcome contributions: proofs of the milestones, continuity and coercivity of the newsvendor and heuristic costs, monotone comparative statics of $\arg\min$ in $\theta$, and the sample-path lemmas of mission 1.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022 (accepted manuscript, SSRN 3724966). https://ssrn.com/abstract=3724966
• S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 1982. https://doi.org/10.1287/opre.30.4.680
• W. L. Cooper, Pathwise properties and performance bounds for a perishable inventory system, Operations Research 49(3), 2001. https://doi.org/10.1287/opre.49.3.455.11214
• A. W. Chazan, S. Gal, A Markovian model for a perishable product inventory, Management Science 23(5), 1977. https://doi.org/10.1287/mnsc.23.5.512
• R. Slonim, C. Wang, E. Garbarino, The market for blood, Journal of Economic Perspectives 28(2), 2014. https://doi.org/10.1257/jep.28.2.177

Motivation

Blood platelets, fresh food and many pharmaceuticals have a fixed lifetime: a unit that has not been used within $m$ periods of its arrival must be discarded. A retailer of such a product faces the usual trade-off between leftover stock and lost sales, plus the cost of discarding outdated units. The issuance policy, the order in which units of different ages are handed to customers, changes the problem. Under first-in-first-out (FIFO) the oldest units go first, as in a blood bank. Under last-in-first-out (LIFO) the newest units go first, as when shoppers pick the freshest milk at the back of the shelf, so that old stock tends to accumulate and outdate.

The optimal ordering policy of a perishable system depends on the full age profile of the stock (Nahmias 1975) and is intractable to compute except for small lifetimes. Practice uses base-stock policies, which raise the total inventory to a fixed level $S$ in every period. Bu, Gong and Chao (SSRN 3724966, accepted in Management Science, 2022) give the first theoretical guarantees for such policies in perishable systems. This mission covers their LIFO results (§4.1).

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F$. Its lower support is $\underline D=\inf\{x:F(x)>0\}$, and $D$ is unbounded when $F(x)<1$ for every $x$. Units live for $m\ge 1$ periods. Leftover stock costs $h>0$ per unit, a lost sale costs $p>0$, and an outdated unit costs an extra $\theta\ge 0$.

At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$, where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods, and $x_{t,0}=0$. The firm orders $q_t\ge 0$, which raises the total level to $x_{t,m}=x_{t,m-1}+q_t$. Demand is served newest-first and unmet demand is lost. The amount outdated and the next state are

$$o_t=\min\{(x_{t,m}-D_t)^+,x_{t,1}\},\qquad x_{t+1,i}=\min\{(x_{t,m}-D_t)^+,x_{t,i+1}\}-o_t .$$

The system starts empty. A policy is admissible if each order is a nonnegative measurable function of the current state. Its long-run average cost is

$$C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E\big[h(x_{t,m}-D_t)^++p(D_t-x_{t,m})^++\theta o_t\big],$$

and $\mathrm{OPT}^{LIFO}$ is the infimum of $C^\pi$ over all admissible policies. The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$, and its cost is $C^{LIFO}(S)$.

The paper bounds $C^{LIFO}(S)$ between two explicit functions (Lemma 3):

$$\hat C_L(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\tfrac{\theta}{m}\mathbb E[(S-\max\{D_1,\dots,D_m\})^+],\qquad \hat C_U(S)=\big(h+\tfrac{\theta}{m}\big)\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+].$$

The heuristic level $\hat S$ is any minimizer of $(\hat C_L+\hat C_U)/2$ on $[0,\infty)$. The newsvendor level is $S^{NP}=F^{-1}(p/(p+h))$. The proof also uses $\widetilde C(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac{\theta}{m}\mathbb E[(S-\sum_{i=1}^mD_i)^+]$ and its minimizer $\widetilde S$.

Formalization targets

Goal: Theorem 5 (p. 16)

$$\text{(a)}\quad C^{LIFO}(\hat S)-\mathrm{OPT}^{LIFO}\le\frac{3\theta\,\mathbb E[(S^{NP}-D)^+]}{2m};$$ $$\text{(b)}\quad D\text{ unbounded}\ \Rightarrow\ \lim_{p\to\infty}\frac{C^{LIFO}_p(\hat S_p)-\mathrm{OPT}^{LIFO}_p}{\mathrm{OPT}^{LIFO}_p}=0;$$ $$\text{(c)}\quad \underline D=0\ \Rightarrow\ \lim_{\theta\to\infty}\big(C^{LIFO}_\theta(\hat S_\theta)-\mathrm{OPT}^{LIFO}_\theta\big)=0.$$

All three parts are stated for every minimizer $\hat S$, and in (b) and (c) for every selection of minimizers as the parameter varies.

Milestones, in proof order

1. The LIFO outdating recursion (EC.18) and its consequence (EC.19), $\sum_{j=t}^{t+m-1}\mathbb E[o_j]\ge\mathbb E[(S-\max\{D_1,\dots,D_m\})^+]$.
2. Lemma 3: $\hat C_L(S)\le C^{LIFO}(S)\le\hat C_U(S)$.
3. Proposition 2 for LIFO: $\mathrm{OPT}^{LIFO}\ge\widetilde C(\widetilde S)$.
4. The gap bound (27) and its uniform form (EC.20), $C^{LIFO}(\hat S)-\mathrm{OPT}^{LIFO}\le(m-1)\theta\mathbb E[D]/m$.
5. The limits as $\theta\to\infty$: (EC.21), $\hat S_\theta\to\underline D$ together with the vanishing outdating term, and (EC.22), $\limsup_\theta C^{LIFO}_\theta(\hat S_\theta)\le p(\mathbb E[D]-\underline D)$.

Significance

Part (a) gives a gap of order $1/m$ that holds for every demand law with finite mean. Parts (b) and (c) identify regimes in which a single explicit base-stock level is asymptotically optimal. Part (c) is sharp: the companion Proposition 1 (mission 6 of this series) shows that when $m\ge 2$ and $S^{NP}>\underline D>0$, even the best base-stock policy stays a positive distance from optimal as $\theta\to\infty$. Under FIFO the corresponding gap decays exponentially in $m$ (Theorem 1, mission 1), so the two issuance rules behave differently. Whether the LIFO gap also decays exponentially is left open in the paper.

The results are proved in the paper but are not machine-checked anywhere. Prove2Me has no perishable lost-sales model with LIFO issuance. This mission provides one, built on the published demand layer and newsvendor functions, together with the sample-path recursion (EC.18), which is specific to LIFO.

Difficulty

$C^{LIFO}(S)$ is a long-run average over a Markov chain on an $(m-1)$-dimensional state, and no closed form is known. The upper bound needs an accounting argument over windows of $m$ periods. The lower bound needs the exact recursion (EC.18) for the outdating of a base-stock policy under LIFO, which differs from the FIFO recursion. Treating the system as a newsvendor problem with a correction term fails: the outdating cost of $\pi_S$ lies strictly between the two bounds, and the minimizer of one bound is not a minimizer of the other. In (b) the absolute gap does not vanish, so the argument needs $\mathrm{OPT}^{LIFO}_p\to\infty$. In (c) the levels $\hat S_\theta$ and $\widetilde S_\theta$ move with $\theta$, and the limits must be controlled uniformly over all minimizers.

Formalization scope

• Time is zero-based: Lean period $t$ is the paper's period $t+1$.
• State. The state is Fin (m - 1) → ℝ of cumulative levels, with $x_{t,0}=0$. The case $m=1$ (empty state) is included.
• Admissible policies $\Pi$ are exactly the paper's class: time-dependent measurable state-feedback rules with nonnegative orders.
• Costs take values in $[0,\infty]$, with lower Lebesgue expectations and a limsup Cesàro average. $C(S)$ is the simulated cost of $\pi_S$ and is never defined by a formula.
• Parameters. The standing assumptions $m\ge 1$, $h>0$, $p>0$, $\theta\ge 0$ are a predicate on a parameter record. Limits vary one field and keep the others fixed and general.
• Gaps are stated as $C\le\mathrm{OPT}+B$. The ratio in (b) and the difference in (c) use real parts, and the statements assert the finiteness (and, in (b), the eventual positivity of OPT) that makes them meaningful.
• Minimizers. "A minimizer" is a predicate, and the statements quantify over every minimizer.
• Expectations. $\mathbb E[(S-\max\{D_1,\dots,D_m\})^+]$ is an expectation under the law of the maximum, built as the image of the i.i.d. path law, like the published leadTimeLaw.

No trivializing reading is admitted. OPT ranges over all admissible policies, not only base-stock ones. $C(S)$ is not a formula. No gap can hold through $\infty-\infty$ or division by zero. The parameters $m$, $\theta$, $p$ and the demand law are not specialized.

Proposition 2 holds under any issuance policy. Its FIFO instance and the FIFO lemmas are posed in mission 1 of this series, and only the LIFO instance is posed here. Lemma 3 and (EC.22) are also used in mission 6. Proofs of any milestone are welcome. Reusable infrastructure includes the law of the maximum of i.i.d. demands, convexity and continuity of the newsvendor cost, and existence of minimizers of $\widetilde C$ and $(\hat C_L+\hat C_U)/2$.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science (2022), accepted manuscript SSRN 3724966. https://ssrn.com/abstract=3724966
• S. Nahmias, Optimal Ordering Policies for Perishable Inventory—II, Operations Research 23(4), 735–749, 1975. https://doi.org/10.1287/opre.23.4.735
• W. L. Cooper, Pathwise Properties and Performance Bounds for a Perishable Inventory System, Operations Research 49(3), 455–466, 2001. https://doi.org/10.1287/opre.49.3.455.11221

Motivation

Perishable products (blood platelets, fresh food, pharmaceuticals) have a fixed lifetime: units not sold within $m$ periods expire and are discarded. Managing such inventory well is a classical problem in operations research, going back to Nahmias (1975). The difficulty is that the state of the system is the whole age profile of the stock, so the optimal policy depends on an $(m-1)$-dimensional state and is intractable for realistic lifetimes. In practice firms use base-stock policies, which raise total stock to a fixed level $S$ every period, but until recently there were no theoretical guarantees for them in the perishable setting.

Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first such guarantees. Under FIFO issuance with zero lead time they define a simple heuristic level $\widetilde S$ and bound its optimality gap explicitly (Theorem 1). This mission formalizes their Theorem 2: when demand is generated by a large population of customers, the optimality gap of the heuristic base-stock policy decays exponentially in the population size $n$. This regime corresponds to high-volume products, where demand is the sum of many small individual requests.

Setting

The inventory system. Time is divided into periods $t=1,2,\dots$. The product lasts $m\ge1$ periods. At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$, where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods. The firm orders $q_t\ge0$, raising total stock to $x_{t,m}=x_{t,m-1}+q_t$ (zero lead time). Demand $D_t$ is served oldest-first (FIFO); unmet demand is lost. The quantity $o_t=(x_{t,1}-D_t)^+$ expires, and the remaining stock ages by one period:

$$x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1 .$$

The system starts empty. Each period costs $h(x_{t,m}-D_t)^++p(D_t-x_{t,m})^++\theta o_t$ with $h>0$, $p>0$, $\theta\ge0$. A policy $\pi$ chooses $q_t=\varphi^\pi_t(x_t)$ by a non-negative measurable function of the current state. Its cost is $C^\pi=\limsup_T\frac1T\sum_{t\le T}\mathbb E[C^\pi_t]$, and $\mathrm{OPT}=\inf_\pi C^\pi$. The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$; its cost is $C(S)$.

The heuristic level. With $D_1,D_2,\dots$ i.i.d. copies of the one-period demand $D$, let

$$\widetilde C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\tfrac{\theta}{m}\,\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big],$$

and let $\widetilde S$ be any minimizer of $\widetilde C$ over $[0,\infty)$. $S^{NP}=F^{-1}(p/(p+h))$ is the newsvendor level of $D$.

Demand population form (7). For a positive integer $n$, the one-period demand is

$$D(n)=\sum_{j=1}^{N(n)}\hat D_j,\qquad N(n)=\sup\Big\{N\in\mathbb N:\sum_{k=1}^NX_k/n\le1\Big\},$$

where the customer demands $\hat D_j$ are i.i.d., non-negative, with mean $\mu>0$ and variance $\sigma^2<\infty$, and the $X_k$ are i.i.d., non-negative, independent of the $\hat D_j$, with $\mathbb E[X_1]=1$, variance $\sigma_X^2<\infty$, and $\mathbb E[e^{sX_1}]<\infty$ for some $s>0$. Thus $N(n)$ is the number of renewals in $[0,n]$; $N(n)=n$ when $X_k\equiv1$, and $D(n)$ is compound Poisson with mean $n\mu$ when the $X_k$ are exponential. $C_n$, $\mathrm{OPT}_n$, $\widetilde C_n$, $S^{NP}_n$ denote the objects above for demand $D(n)$, with $m,h,p,\theta$ fixed.

Formalization targets

Goal: Theorem 2 (p. 12)

There exist constants $K_1>0$, $K_2>0$ such that, for all sufficiently large $n$ and every minimizer $\widetilde S_n$ of $\widetilde C_n$,

$$C_n(\widetilde S_n)-\mathrm{OPT}_n\le K_1e^{-K_2n}.$$

The constants may depend on $m,h,p,\theta$ and the laws of $\hat D_1$ and $X_1$. The goal asserts only the exponential rate, not the explicit constants of the proof.

Milestones (proof order)

1. (23), p. 23: for every $\lambda>0$, $C_n(\widetilde S)-\mathrm{OPT}_n\le\frac{(m-1)\theta}{\lambda me}\big(e^{\lambda S^{NP}_n/m}\,\mathbb E[e^{-\lambda D(n)}]\big)^m$.
2. (EC.6), p. ec3: $S^{NP}_n\le\mathbb E[D(n)]+\sqrt{p\,\mathrm{Var}[D(n)]/h}$.
3. (EC.7), p. ec4: $\mathbb E[D(n)]=\mu\mathbb E[N(n)]$, $\mathrm{Var}[D(n)]=\sigma^2\mathbb E[N(n)]+\mu^2\mathrm{Var}[N(n)]$.
4. Renewal limits, p. ec4: $\mathbb E[N(n)]/n\to1$ and $\mathrm{Var}[N(n)]/n\to\sigma_X^2$.
5. Step-1 claim, p. ec3: for every $k>1$, $S^{NP}_n\le k\mu n$ for all large $n$.
6. (EC.10)–(EC.11), pp. ec4–ec5: there is $\nu>0$, depending only on the law of $X_1$, with $\mathbb P(N(n)<n/(1+\delta))\le\exp(-\delta^2n/(8(1+\delta)^2\nu^2))$ for $0<\delta<\nu$, $n\ge2(1+\delta)/\delta$.
7. (EC.8), p. ec4: under the same quantifiers, $\mathbb E[e^{-\lambda D(n)}]\le e^{-\delta^2n/(8(1+\delta)^2\nu^2)}+(\mathbb E[e^{-\lambda\hat D_1}])^{n/(1+\delta)}$.

The proof also uses the FIFO results (Lemmas 1–2, Proposition 2 and inequality (21)) that are posed in mission 1 of this series; they are not restated here, and (23) is their consequence at the population demand.

Significance

The result. Theorem 2 shows that the heuristic base-stock policy, which is computed from a one-dimensional convex function, is nearly optimal for high-volume perishable products: the loss from ignoring the age profile vanishes exponentially as demand scales. Together with Theorem 1 (exponential decay in the lifetime) it explains why simple base-stock rules perform well in practice, and it gives a quantitative criterion for when a firm can stop worrying about the optimal policy.

Formalizing it. The result is proved in the paper; no part of it is machine-checked. A formalization adds a checked perishable inventory model (FIFO dynamics, admissible policies, long-run average cost), a random-sum demand model built on a renewal counting process, and checked versions of three classical probabilistic tools that the proof cites: Scarf's minimax bound for the newsvendor, Wald's identity with the law of total variance for random sums, and a lower-deviation bound for renewal counts from Bernstein's inequality for sub-exponential variables. The paper's justification of $\mathrm{Var}[N(n)]/n\to\sigma_X^2$ cites convergence in distribution, which does not imply convergence of variances; the statement is still true, and a formal proof has to supply the renewal variance argument.

Difficulty

The cost comparison itself is inherited from Theorem 1; what is new is controlling both factors of (23) as $n\to\infty$. The level $S^{NP}_n$ grows linearly in $n$, so the factor $e^{\lambda S^{NP}_n/m}$ grows exponentially, and must be beaten by the decay of $\mathbb E[e^{-\lambda D(n)}]$. Neither factor is explicit: $S^{NP}_n$ is a quantile of a compound distribution, and $D(n)$ has a random number of summands. Simply replacing $N(n)$ by its mean is not possible, because the lower tail of $N(n)$ must be shown to be exponentially small with a rate that does not degrade with $n$; this needs a concentration inequality for the renewal count, not only a law of large numbers. When $m=1$ the right side of (23) is zero, so the substantive case is $m\ge2$, where the constants must be balanced to make the exponent negative. None of the needed tools (renewal theory, sub-exponential Bernstein, Scarf's bound) is in Mathlib.

Formalization scope

• Namespace PerishBaseStock.Population. Demand laws are CappedBaseStock.DemandLaw (non-negative, finite positive mean); the newsvendor functions come from LostSalesOrderUpTo.Asymptotic.Backorder; the renewal count is the counting variable N of SmithRenewal.Elementary at time $n$.
• Time is zero-based; levels and orders live in $[0,\infty)$, truncated subtraction is $(\cdot)^+$. The state is Fin (m - 1) → ℝ≥0 holding cumulative levels, with $x_{t,0}:=0$; $m=1$ is allowed.
• Costs are lower Lebesgue expectations in $[0,\infty]$; $C^\pi$ is a limsup of Cesàro averages; $\mathrm{OPT}$ is the infimum over all measurable state-feedback policies (the paper's class $\Pi$). $C(S)$ is the simulated cost of $\pi_S$, not a formula.
• "$\widetilde S$ is a minimizer" is a predicate, and every statement quantifies over every minimizer. Gaps are stated as $C\le\mathrm{OPT}+B$.
• The demand $D(n)$ lives on the product of two independent i.i.d. sequence spaces. The family of systems is a sequence of demand laws whose $n$-th law equals that of $D(n)$ for $n\ge1$; on the null event $N(n)=\infty$ the sum is $0$.
• $\mathbb E[\hat D_1]>0$ is assumed (the paper's standing $\mathbb E[D]>0$).
• Trivializing formalizations are ruled out: OPT ranges over all admissible policies, $C(S)$ is the long-run average of the simulated cost, the constants $K_1,K_2$ are required to be positive and to be chosen before $n$, $m$ and $\theta$ are kept general, and the law of $D(n)$ is a genuine pushforward (its measurability is checked).
• Reusable beyond this mission: the compound-renewal demand model and milestones 2–4, 6 and 7, which are statements about random sums and renewal counts independent of inventory. Proofs of any milestone, and of the probabilistic lemmas in isolation, are welcome.

Selected references

• J. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022; accepted manuscript SSRN 3724966. https://ssrn.com/abstract=3724966
• S. Nahmias, Optimal ordering policies for perishable inventory II, Operations Research 23(4):735–749, 1975. https://doi.org/10.1287/opre.23.4.735
• H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• W. L. Smith, Renewal theory and its ramifications, J. R. Statist. Soc. B 20(2), 1958.
• P. Rigollet, J.-C. Hütter, High Dimensional Statistics, lecture notes for course 18.S997, MIT, 2015 (Theorem 1.13, Bernstein's inequality for sub-exponential variables).