The OR Formalization Drive

Motivation

The continuous-review $(Q, r)$ policy is the standard control rule for a single stocked item with random demand: whenever the inventory position falls to the reorder point $r$, an order of fixed size $Q$ is placed. It is implemented in a large share of commercial inventory systems. Choosing the two parameters jointly has traditionally required numerical search (Hadley and Whitin, 1963; Federgruen and Zheng, 1992). In practice the order quantity is therefore often taken from the deterministic economic order quantity (EOQ) formula with backorders, and the reorder point is then set for the random demand.

Zheng (1992) turned this practice into a question with an exact answer: how does the optimal order quantity $Q^*$ of the stochastic model compare with the EOQ quantity $Q^*_d$ computed from the same cost data and the same mean demand? Its Theorem 2 answers it with a two-sided bound. This mission formalizes that theorem. Companion missions of the same series formalize the paper's cost bounds (Theorem 3), the flatness of the cost curve (Theorem 4) and the $1/8$ bound on the cost of using the EOQ quantity (Theorem 5).

Setting

Demand arrives at rate $\lambda > 0$ and replenishment orders arrive after a fixed leadtime $L > 0$. Shortages are backordered. Holding costs accrue at rate $h > 0$ per unit held, backorder penalties at rate $p > 0$ per unit short, and every order costs $K > 0$. The leadtime demand $D$ is a nonnegative random variable with law $\mu$ and mean $\mathbb{E}(D) = \lambda L$. The expected inventory cost rate at inventory position $y$ is the newsvendor cost

$$G(y) = \mathbb{E}\big[h(y - D)^+ + p(D - y)^+\big],$$

assumed, as in the paper, to attain its minimum at a unique point $y^0$. The long-run average cost of the policy $(Q, r)$ is

$$c(Q, r) = \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}.$$

For each $Q > 0$, let $r(Q)$ be an optimal reorder point, i.e. a minimizer of $c(Q, \cdot)$. The analysis runs through the curves

$$H(Q) = G(r(Q))\ (Q > 0),\quad H(0) = G(y^0),\qquad H_0(Q) = H(Q) - G(y^0),\qquad A(Q) = QH(Q) - \int_0^Q H(y)\,dy,$$

and through the cost $C(Q) = c(Q, r(Q))$ of order quantity $Q$ with the reorder point set optimally. The optimal order quantity $Q^*$ is the minimizer of $C$ over $Q > 0$.

The EOQ model is the case of a constant leadtime demand $\lambda L$. Its cost rate is $G_d(y) = h(y - \lambda L)^+ + p(\lambda L - y)^+$, and the same construction gives $r_d$, $H_d$, $A_d$ and the optimal quantity

$$Q^*_d = \sqrt{\frac{2\lambda K(h+p)}{hp}}.$$

Formalization targets

Goal: Theorem 2 (p. 96)

For $K > 0$, let $\bar Q$, $\bar Q_1$, $\bar Q_2$ be the positive solutions of

$$Q H_0(Q) = 2\lambda K,\qquad H_0(Q) = H_d(Q^*_d),\qquad \int_0^Q H_0(y)\,dy = \lambda K.$$

Each has exactly one positive solution, and

$$Q^*_d \le Q^* \le \bar Q,\qquad \bar Q \le \bar Q_1,\qquad \bar Q \le \bar Q_2.$$

Moreover, with $\lambda, L, h, p$ and the demand law fixed, $K \mapsto \bar Q_1(K) - Q^*_d(K)$ is nondecreasing on $(0, \infty)$ and converges to a finite constant as $K \to \infty$.

Milestones

The milestones are the paper's own numbered results that feed Theorem 2, listed in the order the argument uses them:

1. Lemma 2 (p. 90): for $Q > 0$, $r$ is optimal iff $G(r) = G(r + Q)$.
2. Eq. (7) (p. 91): $C(Q) = (\lambda K + \int_0^Q H(y)\,dy)/Q$.
3. Lemma 4 (p. 91): $H$ is increasing and convex with asymptotic slope $hp/(h+p)$.
4. Lemma 6 (p. 92): $A$ is increasing and convex, and $Q = Q^*$ iff $A(Q) = \lambda K$.
5. Eqs. (18), (20) (p. 94): $H_d(Q) = \frac{hp}{h+p}Q$, and $Q^*_d$ is optimal for the EOQ model.
6. Lemma 7 (p. 95): $H_0 \le H_d \le H$ and $A \le A_d$.
7. Lemma 8 (p. 95): $\int_0^Q H \ge \tfrac12 QH(Q) \ge A(Q) \ge \tfrac12 QH_0(Q) \ge \int_0^Q H_0$, with equalities for deterministic demand.

Significance

The result. Theorem 2 says that the EOQ formula always underestimates the optimal order quantity when leadtime demand is random. The underestimate is bounded by $\bar Q_1 - Q^*_d$, a quantity that stays bounded however large the ordering cost is. So the relative error of the EOQ quantity vanishes as $K$ grows. The first inequality, $Q^*_d \le Q^*$, is also an ingredient of the paper's Theorem 3 (cost bounds) and Theorem 5 (the EOQ quantity raises costs by at most $1/8$). The explicit bounds $\bar Q$, $\bar Q_1$, $\bar Q_2$ bracket $Q^*$ and give a search interval for it.

Formalizing it. The theorem has been proved on paper since 1992. No machine-checked version of it, or of the continuous-review $(Q, r)$ cost of Eq. (1), exists on this platform. The inventory items already here treat the discrete cost with integer order quantities, a normally distributed demand, or the EOQ without backorders. This mission provides a machine-checked version of the paper's optimality conditions for a general demand distribution. The paper's argument differentiates $G$ twice, i.e. it tacitly assumes a density. The formal statements do not, so a formal proof must redo those steps with one-sided (convexity) arguments. The printed argument for the limit in part (b) shows only that a derivative tends to zero. A complete proof of convergence is part of the work.

Difficulty

The obvious route to $Q^*_d \le Q^*$ compares the two cost curves $C$ and $C_d$ directly. It fails because $C \ge C_d$ pointwise, and a pointwise inequality between two convex functions says nothing about the order of their minimizers. The stochastic curve $H$ is defined only implicitly, as $G$ evaluated at a minimizer of a parametric integral, so its growth relative to the linear $H_d$ has to be established before any comparison of order quantities. For part (b), a vanishing derivative does not imply convergence ($\log K$ also has a vanishing derivative), so the printed proof of the limit does not go through as written.

Without a density, $r(Q)$ need not be differentiable. Every derivative in the paper's proofs (of $r$, $H$ and $A$) must be replaced by monotonicity or chord arguments.

Formalization scope

The Lean development uses the namespace ZhengQR.OrderQty. Its conventions:

• Parameters. $\lambda, L, K, h, p$ are reals, all assumed strictly positive. $K > 0$ is implicit in the paper; at $K = 0$ the optimal quantity degenerates.
• Demand. The law $\mu$ of $D$ is a probability measure on $\mathbb{R}$ that is integrable, has mean $\lambda L$ and is carried by $[0, \infty)$. No density is assumed, so discrete laws such as the Poisson of the paper's §4 are allowed.
• Standing assumption. $G$ has a unique global minimizer (p. 90). It is a hypothesis of every statement about the stochastic model.
• Generic machinery. $c$, $r(Q)$, $y^0$, $H$, $C$, $A$, $H_0$ and optimality of $Q$ are defined for an arbitrary cost rate $G$ and applied to both the newsvendor cost and $G_d$. So Eqs. (18) and (20) are theorems, not definitions. $r(Q)$ and $y^0$ are chosen minimizers, never solutions of Lemma 2's equation. $r(Q)$ minimizes $\int_r^{r+Q}G$, which for $Q > 0$ has the same minimizers as $c(Q, \cdot)$, so $H$, $H_0$ and $A$ do not depend on $K$.
• Domains. $H$, $H_0$ and $A$ are used on $[0, \infty)$, $c$ and $C$ for $Q > 0$ only, and $Q^*$ is a $Q > 0$ minimizing $C$ over $(0, \infty)$.
• Readings of informal words.
  • Lemma 4's "increasing" and Lemma 6's "increasing/decreasing" mean strictly.
  • Lemma 4's "asymptotic slope $hp/(h+p)$" means $H(Q)/Q \to hp/(h+p)$ together with the chord bound $H(Q') - H(Q) \le \frac{hp}{h+p}(Q' - Q)$ for $0 \le Q < Q'$.
  • "$\bar Q \overset{\text{def}}{=} \{Q : \dots\}$" means the unique positive solution. The goal quantifies over every positive solution and separately asserts that exactly one exists.
  • Theorem 2's "increasing function of $K$" means nondecreasing, which is what the paper's proof establishes (a nonnegative derivative).
  • "Converges to a constant" means a finite real limit.
  • Lemma 8's "the leadtime demand is deterministic" means the EOQ model with cost rate $G_d$.
• Ruling out trivial readings. The goal's hypotheses are satisfiable (for example by a deterministic leadtime demand). Existence of $Q^*$ (Lemma 6) and of $\bar Q$, $\bar Q_1$, $\bar Q_2$ (the goal itself) is asserted, so neither the bounds nor the limit hold vacuously.

Infrastructure needed includes the following. Much of it is reusable for any single-item inventory model:

• differentiation under the expectation, or one-sided substitutes, for $G$;
• convexity of $H$ as the inverse of the width of the sublevel sets of $G$;
• the envelope identity behind Eq. (7);
• elementary convex-analysis facts about chords.

Contributions welcome: proofs of the milestones in any order, general lemmas on the newsvendor cost, and a complete convergence argument for part (b).

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• A. Federgruen, Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Motivation

The continuous-review $(Q, r)$ policy — order a fixed quantity $Q$ whenever the inventory position falls to the reorder point $r$ — is the textbook policy for a single item with random demand and a positive replenishment leadtime (Hadley and Whitin 1963). Its optimal parameters have no closed form, so practice routinely falls back on the deterministic economic order quantity (EOQ) model with backorders, whose optimum is explicit. How much the deterministic model misjudges the stochastic system's cost is therefore a practical question, and before Zheng (1992) it had been studied only numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978).

Zheng's paper answers it analytically. This mission targets its Theorem 3, which brackets the optimal cost of the stochastic model by the optimal cost of the EOQ model with the same parameters.

Setting

Demands arrive at rate $\lambda>0$ and orders arrive after a fixed leadtime $L>0$. Each order costs $K>0$; holding and backorder costs accrue at rates $h>0$ and $p>0$ per unit per unit time. The leadtime demand $D$ is a nonnegative random variable with $E(D)=\lambda L$. The inventory cost rate at inventory position $y$ is the newsvendor cost

$$G(y)=E\big[h(y-D)^+ + p(D-y)^+\big],$$

assumed to attain its minimum at a unique point $y^0$.

For order quantity $Q>0$ and reorder point $r$, the long-run average cost is

$$c(Q,r)=\frac{\lambda K+\int_r^{r+Q}G(y)\,dy}{Q}.$$

Let $r(Q)$ be a reorder point minimizing $c(Q,\cdot)$, and define $H(Q)=G(r(Q))$ for $Q>0$, $H(0)=G(y^0)$, and $C(Q)=c(Q,r(Q))$. The optimal order quantity $Q^*$ minimizes $C$ over $Q>0$, and $C^*=C(Q^*)$. Write $H_0(Q)=H(Q)-G(y^0)$ and

$$C_0(Q)=\frac{\lambda K+\int_0^Q H_0(y)\,dy}{Q},$$

the controllable cost, so that $C(Q)=G(y^0)+C_0(Q)$; $C^*_0=C_0(Q^*)$. The constant $G(y^0)$ is the newsboy cost.

The EOQ model is the same construction with demand constant at $\lambda L$: $G_d(y)=h(y-\lambda L)^+ + p(\lambda L-y)^+$, with functions $H_d$, $C_d$, optimal quantity $Q^*_d=\sqrt{2\lambda K(h+p)/(hp)}$ and optimal cost $C^*_d=C_d(Q^*_d)$.

Formalization targets

Goal: Theorem 3 (p. 97)

$$C^*_0\le\frac{Q^*_d}{Q^*}\,C^*_d,\qquad C^*_d\le C^*\le G(y^0)+\frac{Q^*_d}{Q^*}\,C^*_d.$$

All three inequalities are part of the goal. The weaker remark after the proof, $C^*_d\le C^*\le C^*_d+G(y^0)$, drops the factor $Q^*_d/Q^*$ and is not the goal.

Milestones

1. Eq. (7): $C(Q)=\big(\lambda K+\int_0^Q H(y)\,dy\big)/Q$ for $Q>0$.
2. Eq. (8): $Q>0$ is optimal iff $H(Q)=C(Q)$.
3. Eqs. (13)–(15): $C(Q)=G(y^0)+C_0(Q)$, and $H_0(Q^*)=C_0(Q^*)$.
4. Lemma 6: $A(Q)=QH(Q)-\int_0^QH$ is increasing and convex; $Q=Q^*$ iff $A(Q)=\lambda K$; $Q^*$ increases and $r^*$ decreases in $K$.
5. Eqs. (18), (20): $H_d(Q)=\frac{hp}{h+p}Q$, and $Q^*_d$ is the EOQ optimum.
6. Lemma 8: $\int_0^QH\ge\tfrac12QH(Q)\ge A(Q)\ge\tfrac12QH_0(Q)\ge\int_0^QH_0$, with equalities for deterministic demand.
7. Eq. (22): $G_d(y)\le G(y)$ for all $y$.

Significance

Theorem 3 says that randomness of leadtime demand raises the total optimal cost above the EOQ's, yet the controllable part of that cost — the part the order quantity actually trades off — is smaller than the EOQ's cost, scaled by $Q^*_d/Q^*$. Combined with $Q^*_d\le Q^*$ (Theorem 2 of the paper), the gap $C^*-C^*_d$ is at most the newsboy cost $G(y^0)$, independent of $K$, so the EOQ cost is a good proxy when $K$ is large relative to $G(y^0)$. The same machinery yields the paper's Theorem 5, that using $Q^*_d$ in the stochastic model costs at most $1/8$ more than the optimum.

The result was proved in 1992; no machine-checked proof is known to exist. Formalizing it requires the continuous $(Q,r)$ model as a whole — optimal reorder points, the one-variable reduction through $H$, and the area function $A$ — none of which is in Mathlib. The companion missions of this series formalize Theorems 2, 4 and 5 of the same paper on the same model.

Difficulty

The middle inequality compares minima of two different functions: $C_d\le C$ pointwise follows from Jensen's inequality, but only after the reorder point of each model is chosen optimally, so the comparison has to pass through the definition of $C$ as a minimum over $r$. The outer inequalities depend on Lemma 8, whose proof uses convexity of $H$ and a slope comparison $H'\le H_d'$ (Lemmas 4 and 7). The paper argues these through first and second derivatives of $r(Q)$ and $G$, which exist only when the leadtime demand has a smooth distribution; the formal statements assume no density, so a proof must either avoid derivatives or handle one-sided ones. Existence of optimal reorder points and of $Q^*$ is asserted in the paper without a separate argument.

Formalization scope

Everything lives in the namespace ZhengQR.CostBounds. The machinery (qrCost, reorderPt, idealPt, Hfun, Cfun, Afun, H0fun, C0fun, IsOptQty) is defined for an arbitrary $G:\mathbb R\to\mathbb R$ and instantiated at the stochastic $G$ and at $G_d$. A structure QRModel holds the parameters, the demand distribution $\mu$ (a probability measure on $\mathbb R$) and the standing assumptions.

Conventions committed to:

• Positivity of $\lambda,L,K,h,p$; $D\ge0$ almost surely; $D$ integrable with $E(D)=\lambda L$; $G$ has a unique minimizer (p. 90). No density is assumed.
• $r(Q)$ is a chosen minimizer of $c(Q,\cdot)$ over $\mathbb R$, not a solution of $G(r)=G(r+Q)$; $y^0$ is a chosen minimizer of $G$. Both use junk value $0$ when no minimizer exists, which never happens under the assumptions.
• $H(0)=G(y^0)$; statements about $H$ and $A$ are on $[0,\infty)$, about $c$, $C$, $C_0$ for $Q>0$.
• "Optimal order quantity" means $Q>0$ and $C(Q)\le C(Q')$ for all $Q'>0$; the goal takes any such $Q^*$ and Lemma 6 states that exactly one exists, so the goal is not vacuous.
• $C^*_d$ is $C_d(Q^*_d)$, with $Q^*_d$ the explicit formula (20); milestone 5 proves it is the EOQ optimum. $C^*_0$ is $C_0(Q^*)$, which equals $\min_{Q>0}C_0$ by (13).
• "Increasing" in Lemma 6 is read strictly, as the proof gives. Lemma 8 is stated for $Q\ge0$; "deterministic" means $\mu$ is the Dirac mass at $\lambda L$.

A formalization in which $C^*_d$ were an arbitrary number, or $Q^*$ an arbitrary positive real, would make the goal false or empty; both are tied to the model above.

Needed infrastructure: existence of minimizers of convex coercive functions on $\mathbb R$, differentiation of parametric integrals $\int_{r(Q)}^{r(Q)+Q}G$, and properties of the newsvendor cost (convexity, coercivity, Jensen). Most of it is reusable for any continuous-review inventory model. Proofs of any milestone, and of lemmas the paper uses but this mission does not list (Lemmas 2–5, 7), are welcome.

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• P. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Motivation

The continuous-review $(Q, r)$ policy is the standard replenishment rule of inventory theory: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$, order a fixed order quantity $Q$. It is used in practice and taught in every operations management course, usually after the deterministic economic order quantity (EOQ) model, which is the same system with a constant demand stream.

Practitioners and textbooks rely on a robustness property of the EOQ: its cost is very insensitive to the choice of order quantity. If the order quantity is off by a factor $\alpha$, the cost rises only by the factor $\tfrac12(\alpha + 1/\alpha)$; ordering 50% too much costs about 8% extra. The insensitivity of the stochastic $(Q, r)$ system to its control parameters had been observed numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), but, as Zheng notes, no analytical result on it was known.

Timeline:

• 1963: Hadley and Whitin derive the $(Q, r)$ cost for Poisson demand.
• 1986: Zipkin proves that the average backorders of a $(Q,r)$ policy are jointly convex in $(Q, r)$ under continuous demand (Zipkin 1986).
• 1992: Zheng derives simple optimality conditions for the continuous $(Q, r)$ model and compares it with the EOQ model under the same cost structure. One of the results is that the stochastic cost curve is flatter in the order quantity than the EOQ curve (Zheng 1992). This mission formalizes that result.

Setting

Demands arrive at rate $\lambda>0$; orders arrive after a fixed leadtime $L>0$; all stockouts are backordered. Each order costs $K>0$; holding costs accrue at rate $h>0$ per unit in stock and penalty costs at rate $p>0$ per unit backordered. The leadtime demand $D\ge 0$ has distribution $\mu$ with finite mean $E(D) = \lambda L$.

The inventory cost rate at inventory position $y$ is

$$G(y) = E\big[h(y-D)^+ + p(D-y)^+\big],$$

assumed to attain its minimum at a unique point $y^0$. The long-run average cost of the policy $(Q, r)$ is

$$c(Q, r) = \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}, \qquad Q>0.$$

For fixed $Q>0$ let $r(Q)$ be a reorder point minimizing $c(Q,\cdot)$, and let

$$C(Q) = c(Q, r(Q)), \qquad H(Q) = G(r(Q))\ (Q>0), \quad H(0) = G(y^0).$$

$C$ is the cost of the order quantity $Q$ when the reorder point is always chosen optimally for it. An optimal order quantity $Q^*$ minimizes $C$ over $Q>0$, and $C^* = C(Q^*)$.

The EOQ model is the same system with the constant leadtime demand $\lambda L$. Its cost rate is $G_d(y) = h(y-\lambda L)^+ + p(\lambda L-y)^+$, and $r_d$, $H_d$, $C_d$ are the objects above at $G_d$, with optimum $Q^*_d$ and $C^*_d$.

Formalization targets

Goal: Theorem 4

$$\frac{C(\alpha Q^*)}{C^*} \le \frac12\left(\alpha + \frac1\alpha\right) \qquad \forall \alpha>0.$$

The goal holds for every demand distribution satisfying the standing assumptions and every optimal $Q^*$. Both regimes, $\alpha<1$ and $\alpha>1$, are included.

Milestones

In the order the proof uses them:

1. Eq. (7): $\int_{r(Q)}^{r(Q)+Q} G = \int_0^Q H$, hence $C(Q) = \big(\lambda K + \int_0^Q H(y)dy\big)/Q$ for $Q>0$.
2. Lemma 4: $H$ is increasing and convex on $[0,\infty)$ with asymptotic slope $hp/(h+p)$.
3. Eq. (8): an optimal $Q^*$ exists, and $Q>0$ is optimal iff $H(Q) = C(Q)$.
4. Eq. (18): $H_d(Q) = \frac{hp}{h+p}Q$, with $r_d(Q) = \lambda L - \frac{h}{h+p}Q$.
5. Lemma 7: $H_0(Q) \le H_d(Q) \le H(Q)$ and $A(Q)\le A_d(Q)$, where $H_0 = H - G(y^0)$ and $A(Q) = QH(Q) - \int_0^Q H$.
6. Eqs. (26)–(27): $H(\alpha Q)\le \alpha H(Q)$ for $\alpha>1$ and $H(\alpha Q)\ge\alpha H(Q)$ for $0<\alpha<1$.
7. Lemma 9: $\int_Q^{\alpha Q} H(y)\,dy \le \frac{\alpha^2-1}{2}\,Q H(Q)$ for all $\alpha>0$, $Q>0$.

Significance

In the EOQ model the relative cost of a scaled order quantity is exactly $C_d(\alpha Q^*_d)/C^*_d = \tfrac12(\alpha + 1/\alpha)$ (Eq. (25) of the paper). Theorem 4 shows that the stochastic system is at least as forgiving. The bound holds for every leadtime-demand distribution with a unique newsvendor minimizer, and it does not depend on the parameters $K$, $h$, $p$, $\lambda$ or $L$. Because the reorder point is re-optimized for each quantity, the bound applies to the practical question of how much a misestimated lot size costs when the safety stock is set correctly.

Together with the other results of the paper (the $1/8$ bound for the EOQ heuristic and the bounds between $Q^*$ and $Q^*_d$, which are separate missions of this series), it gives a closed-form account of why the EOQ is a good heuristic for stochastic systems.

The result has a complete published proof. It has not been machine-checked. The work that remains is a formal proof for general distributions: the paper differentiates $G$ and $r(Q)$ twice, and a formal proof has to replace those derivatives with arguments that need no density.

Difficulty

$C(Q)$ is defined through an inner minimization over the reorder point, so its shape in $Q$ is controlled by the implicitly defined function $H(Q) = G(r(Q))$ rather than by $G$ directly. The obvious approach would bound $C(\alpha Q^*)$ with the reorder point fixed at $r(Q^*)$. That approach is the wrong comparison: it bounds a larger quantity, and the resulting bound depends on the distribution.

The paper's proof uses three properties of $H$: that it is convex, that its slope never exceeds the EOQ slope $hp/(h+p)$, and that it dominates $H_d$. The paper obtains these from the derivatives $r'(Q)$ and $H'(Q)$ under a smooth demand distribution. Without a density, $r(Q)$ is only an argmin and $H$ need not be differentiable, so none of these three properties can be read off a derivative formula; the asymptotic slope in particular depends on the finite mean $E(D) = \lambda L$ and on the behaviour of $G$ at $\pm\infty$.

Formalization scope

The mission is set in Lean 4 with Mathlib. All objects are real valued.

• Model. The structure QRModel bundles $\lambda, L, K, h, p>0$, a probability measure $\mu$ on $\mathbb{R}$ with integrable identity, $\int x\,d\mu = \lambda L$, $D\ge 0$ almost surely, and the unique-minimizer hypothesis on $G$. $K>0$ is implicit in the paper and made explicit here. No density is assumed; deterministic and discrete demands are allowed, and the paper's own numerical study uses Poisson demand.
• Generic machinery. $c$, $r(Q)$, $y^0$, $H$, $H_0$, $C$ and $A$ are defined for an arbitrary cost rate and instantiated at $G$ and at $G_d$. $r(Q)$ and $y^0$ are chosen minimizers; they are never defined by the equation $G(r) = G(r+Q)$, which is a lemma of the paper. $H(0) = G(y^0)$. Values at $Q<0$ (and of $c$, $C$ at $Q\le 0$) are junk, and every statement restricts to $Q>0$ or $Q\ge 0$.
• Readings of informal words. "Increasing" in Lemma 4 is strict on $[0,\infty)$, since the proof shows $H'>0$. "Asymptotic slope $hp/(h+p)$" is stated as $H(Q)/Q\to hp/(h+p)$ together with the chord bound $H(Q_2)-H(Q_1)\le \frac{hp}{h+p}(Q_2-Q_1)$ for $0\le Q_1\le Q_2$. The chord bound is the derivative-free form of $H'\le hp/(h+p)$ that the proofs of Lemmas 7–9 use. "The optimal order quantity" is IsOptQty Q, meaning $Q>0$ and $C(Q)\le C(Q')$ for all $Q'>0$. Its existence is asserted in the Eq. (8) milestone, so the goal is not vacuous. "$\forall\alpha>0$" is a real $\alpha>0$ with real division $1/\alpha$. In Lemma 9 the integral $\int_Q^{\alpha Q}$ is oriented, as on the page.
• Ruling out trivializations. $C(\alpha Q^*)$ re-optimizes the reorder point for $\alpha Q^*$; holding it at $r(Q^*)$ would be a different theorem. $C^*>0$ is a consequence of the model, not a hypothesis.

A complete development needs the following:

• integrability and continuity of $G$;
• existence of the optimal reorder point;
• convexity of $H$;
• the asymptotics $G - G_d\to 0$ at $\pm\infty$;
• Jensen's inequality $G_d\le G$ (Eq. (22));
• existence of $Q^*$.

These facts about newsvendor cost functions are reusable in the other missions of this series. Contributions of any of them as separate lemmas are welcome.

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• P. H. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• H. M. Wagner, M. O'Hagan and B. Lundh, An Empirical Study of Exactly and Approximately Optimal Inventory Policies, Management Science 11(7):690–723, 1965. https://doi.org/10.1287/mnsc.11.7.690
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Motivation

Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves $1/4$ of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats $1/4$ and reaches $1/3$.

Timeline. For Max Directed Cut, a random cut achieves $1/4$. Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved $1/4$ for a random set and $1/3$ nonadaptively for general nonnegative submodular functions, $1/3$ and $2/5$ by adaptive local search, and that $1/2$ requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal $1/2$ with a randomized double-greedy algorithm.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements. A function $f : 2^X \to \mathbb{R}$ is submodular (Definition 1.1) if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X .$$

Throughout, $f$ is nonnegative, the paper's standing assumption, and $OPT = \max_{S \subseteq X} f(S)$.

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; $R = X(1/2)$ is a uniformly random subset. For a set $A \subseteq X$, $A(p)$ is the analogous random subset of $A$. The averaged marginal value of an element (Definition 2.4) is

$$\omega(x) = \mathbf{E}\big[f(R \cup \{x\}) - f(R \setminus \{x\})\big], \qquad R = X(1/2).$$

Algorithm NA (p. 1139):

1. by random sampling, compute estimates $\tilde\omega(x)$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$, with high probability;
2. independently, sample $R = X(1/2)$;
3. with probability $8/9$ return $R$;
4. with probability $1/9$ return $A = \{x \in X : \tilde\omega(x) > 0\}$.

Given the estimates, the expected value NA returns is $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$.

Formalization targets

Goal: Theorem 2.6 in the explicit form of its proof

For every nonnegative submodular $f$ and every estimate $\tilde\omega$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$,

$$\frac89\,\mathbf{E}[f(X(1/2))] + \frac19\, f\big(\{x : \tilde\omega(x) > 0\}\big) \ \ge\ \Big(\frac13 - \frac{4}{9n}\Big)\, OPT .$$

The printed theorem says "at least $(1/3 - o(1))\,OPT$"; the term $4/(9n)$ is what the proof establishes (p. 1140, last display).

Milestones

1. Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$ for submodular $g$.
2. Lemma 2.3: $\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B)$ for independently sampled, possibly overlapping $A, B$.
3. For $B = X \setminus A$ and any $C$: $f(A) + f(B \cap C) + f(B \cup C) \ge f(C)$.
4. If $\omega \le OPT/n^2$ on $B$: $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$.
5. $\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B \cap C) + \tfrac14 f(C)$.
6. If $\omega \ge -OPT/n^2$ on $A$ and $B = X \setminus A$: $\mathbf{E}[f(R)] \ge \mathbf{E}[f(R \cap (B \cup C))] - OPT/(2n)$.
7. $\mathbf{E}[f(R \cap (B \cup C))] \ge \tfrac14 f(C) + \tfrac14 f(B \cup C)$.

Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of $C$.

Significance

The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a $1/3$-approximation of unconstrained nonnegative submodular maximization, strictly better than the $1/4$ of any algorithm that must return one of its queried sets (the paper shows $1/4$ is optimal in that class, §4.2). The quantity $\omega$ generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.

Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the $1/3$ argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.

Difficulty

The two regimes the proof separates, "$A$ is already good" and "one of $f(B \cap C)$, $f(B \cup C)$ is large", must be tied to the value of a uniformly random set, whereas the elements of $A$ and $B$ are chosen from estimated averages, not from the optimal set $C$. The natural attempt, comparing $f(R)$ with $f(C)$ element by element, fails because $f$ is not monotone: adding elements of $C$ to $R$ can decrease the value. The accuracy $OPT/n^2$ of the estimates must also be propagated through a sum over up to $n$ elements, which is where the error term $4/(9n)$ comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.

Formalization scope

• The ground set is a Fintype X with DecidableEq, assumed Nonempty, so $n = |X| \ge 1$ and the divisions by $n$ and $n^2$ are genuine; sets are Finset X; $f$ is real valued with nonnegativity $\forall S,\ 0 \le f(S)$ as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real $f$ with no sign condition, as printed.
• $OPT$ is Finset.univ.sup' _ f, the true maximum over all subsets.
• Every expectation over an independently sampled random set is the exact finite sum $F(x) = \sum_{S} f(S)\prod_{i \in S} x_i \prod_{i \notin S}(1 - x_i)$; $X(1/2)$ is $x \equiv 1/2$. Expectations over two independent samples (Lemma 2.3) are the corresponding iterated sums. Sampling probabilities carry the hypotheses $0 \le p, q \le 1$.
• The goal quantifies over every estimate $\tilde\omega$ satisfying the printed accuracy $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ (strict), with $A = \{x : \tilde\omega(x) > 0\}$ (strict). The "with high probability" of NA's first step is this hypothesis; the sampling estimate that makes it likely (Lemma 2.5, a Chernoff-bound argument) is not part of the goal. When $OPT = 0$ the hypothesis is unsatisfiable, but then $f \equiv 0$ and nothing is lost.
• The left-hand side is exactly the mixture $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$. A statement with the maximum of the two terms, with exact values $\tilde\omega = \omega$, or with the $o(1)$ replaced by an existential constant or a limit, is a different (and weaker or stronger) theorem and does not close this mission.
• Printed slip corrected: in the second display on p. 1140, the "$=$" before $-|A \setminus C|\,OPT/(2n^2)$ should be "$\ge$"; milestone 6 states the inequality.

Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity $\mathbf{E}[f(R \cup \{x\}) - f(R)] = \tfrac12\omega(x)$, and general lemmas about the operator $F$ (splitting a uniform random set along a partition).

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

Public school districts in many US cities let families rank schools and then assign seats by a centralized procedure. Each school has a limited number of seats, and state or local law gives some students priority at some schools, for example for a sibling already enrolled or for living within walking distance. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) framed this as a mechanism design problem and showed that the mechanism then used in Boston rewards families who misreport their preferences. They proposed two replacements with written proofs of their properties. This mission covers the second one, the top trading cycles mechanism, and its two properties: every outcome is Pareto efficient, and no student can gain by misreporting.

The paper drew on earlier results for simpler allocation problems:

• 1974: Shapley and Scarf introduce housing markets and Gale's top trading cycles algorithm, in which each agent owns one house.
• 1977: Roth and Postlewaite show the algorithm finds the unique core allocation of a housing market.
• 1982: Roth proves the core mechanism for housing markets is strategy-proof.
• 1999: Abdulkadiroğlu and Sönmez adapt the algorithm to house allocation with existing tenants and prove strategy-proofness.
• 2000: Pápai introduces hierarchical exchange rules, a wider class that includes these mechanisms.
• 2003: the paper formalized here extends the algorithm to schools with capacities and school-specific priorities (Propositions 3 and 4).

Setting

A school choice problem consists of a finite set $I$ of students, a finite set $S$ of schools, a capacity $q_s \in \mathbb N$ for each school, a strict preference $P_i$ of each student over all schools, and a strict priority ordering $\succ_s$ of each school over all students. The standing assumption is that there is no shortage of seats:

$$|I| \le \sum_{s\in S} q_s .$$

Preferences are rankings: $P_i(s)\in\{0,\dots,|S|-1\}$ is the rank of $s$ for student $i$, with rank $0$ the favourite. Priorities are rankings of students in the same way, with rank $0$ the highest priority. A matching is a map $\mu : I\to S$ with $\#\{i:\mu(i)=s\}\le q_s$ for every school $s$. A matching $\mu$ is Pareto efficient if no other matching $\nu$ gives every student a weakly better school ($P_i(\nu(i))\le P_i(\mu(i))$) and some student a strictly better one.

A direct mechanism maps the reported preference profile, together with the fixed priorities and capacities, to a matching. It is strategy-proof if no student can ever obtain a school she strictly prefers by changing her own report while the others keep theirs.

The top trading cycles algorithm keeps a counter $c_s$ of free seats at each school, starting at $q_s$. A school is remaining while $c_s>0$. At each step every remaining student points to her favourite remaining school, and every remaining school points to the remaining student with the highest priority for it. A cycle is a list $(s_1,i_1,\dots,s_k,i_k)$ of distinct schools and students in which $s_1$ points to $i_1$, $i_1$ points to $s_2$, and so on, and $i_k$ points to $s_1$. Every student on a cycle is assigned the school she points to and is removed. Each school on a cycle loses one seat. All cycles present at a step are cleared at that same step. The top trading cycles mechanism $\mathrm{TTC}(q,\succ,P)$ returns the resulting assignment.

Formalization targets

Goal: Proposition 4 (strategy-proofness)

For all capacities with no shortage, all priorities, every profile $P$, every student $i$ and every alternative report $Q_i$, student $i$ is assigned schools $s = \mathrm{TTC}(q,\succ,P)(i)$ and $s' = \mathrm{TTC}(q,\succ,(Q_i,P_{-i}))(i)$, and

$$P_i(s) \le P_i(s') .$$

Milestones

1. At every step at which some student remains, there is a cycle (Section II.B, p. 15).
2. After $|I|$ steps no student remains, and the outcome is a matching (Section II.B, p. 16).
3. Lemma (Appendix, pp. 28–29): if student $i$ is still remaining at the beginning of a step under two different reports of her own, the remaining students and the remaining schools at that point are the same under both reports.
4. Proposition 3 (p. 17): the outcome is a Pareto efficient matching with respect to the reported profile.
5. When all schools share one priority ordering $\pi$, the mechanism equals the serial dictatorship induced by $\pi$ (Section II.B, p. 16).

Significance

Strategy-proofness means truthful reporting is a dominant strategy for every student. Families need no information about other families' reports. Under the Boston mechanism, ranking a popular school first can cost a student her priority at her second choice. Proposition 3 separates the top trading cycles mechanism from the Gale–Shapley student-optimal stable mechanism, which is also strategy-proof but can select Pareto dominated matchings.

The results are proved in the paper, in short prose arguments in its Appendix. To the best of our knowledge they have no machine-checked proof. The platform already has the housing-market version, AGT.ttc_strategyproof, but that statement covers one house per agent with the mechanism characterised as the core. Capacities, school priorities and the step-by-step algorithm are absent from it. This mission produces a checked account of the algorithm with capacities and counters, together with its termination and invariance properties.

Difficulty

The paper's argument moves from the step at which student $i$ leaves under one report to the step at which she leaves under another. It relies on the claim that the cycles formed before either step are unaffected by $i$'s report. Informally, $i$ is not on a cycle yet, so what she points to does not matter. Formally, "the same cycles form" requires comparing two runs of a simultaneous-clearing procedure step by step. At each step one has to show that the set of cycles, and hence the counters and the remaining schools, agree, even though $i$ points to different schools in the two runs. Reasoning about a single cycle at a time does not work, because the algorithm clears all cycles of a step at once. Termination is also not immediate: without the no-shortage condition the algorithm can leave students unassigned. Seats are counted with multiplicity, so a school can stay in the market for several steps.

Formalization scope

Everything lives in the namespace SchoolChoice.TTC. Students and schools are arbitrary finite types with decidable equality; the set of students may be empty. Capacities are q : S → ℕ, and a school of capacity zero is never remaining. A preference is a bijection S ≃ Fin (card S) and a priority is a bijection I ≃ Fin (card I), in both cases with rank 0 the best. Strictness and completeness of both therefore hold by construction, and every school is acceptable. A state of the algorithm consists of the remaining students, the counters and the assignments made so far. run q pri P t is the state after t completed steps, which is the beginning of the paper's Step t + 1. The mechanism ttc q pri P : I → Option S reads off the assignment after card I steps. Every theorem assumes card I ≤ ∑ s, q s.

The algorithm is a concrete, deterministic definition that clears all cycles at every step. The mechanism is not defined as "some Pareto efficient matching" or characterised by properties, since that would make Proposition 3 trivial. The goal asserts that both outcomes exist, so an unassigned outcome cannot satisfy it vacuously. The misreport, the other students' reports and the priorities are all universally quantified.

A complete development needs termination of the algorithm, a combinatorial account of the pointing graph (cycles in a finite functional graph), and the step-by-step invariance argument of the Lemma. The last two are reusable for the type-specific quota variant and for other trading-cycle mechanisms. Contributions of intermediate lemmas are welcome: counter invariants such as "the sum of the counters is at least the number of remaining students", monotonicity of the remaining sets, and the fact that a student on a cycle receives her favourite remaining school.

Selected references

• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
• Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0
• Alvin E. Roth and Andrew Postlewaite, Weak versus Strong Domination in a Market with Indivisible Goods, Journal of Mathematical Economics 4(2), 131–137, 1977. https://doi.org/10.1016/0304-4068(77)90004-0
• Alvin E. Roth, Incentive Compatibility in a Market with Indivisible Goods, Economics Letters 9(2), 127–132, 1982. https://doi.org/10.1016/0165-1765(82)90003-9
• Atila Abdulkadiroğlu and Tayfun Sönmez, House Allocation with Existing Tenants, Journal of Economic Theory 88(2), 233–260, 1999. https://doi.org/10.1006/jeth.1999.2553
• Szilvia Pápai, Strategyproof Assignment by Hierarchical Exchange, Econometrica 68(6), 1403–1433, 2000. https://doi.org/10.1111/1468-0262.00166

Motivation

Generalized pattern search (GPS) is a class of derivative-free methods for minimizing a function that can only be evaluated, not differentiated. Such objectives arise in engineering design, where one evaluation is an expensive simulation that may fail and return no value at all. The helicopter rotor design problem of Booker et al. is one example: no value was returned for roughly 66% of the trial points (Booker et al., 1999). A method for such problems has to tolerate objectives that are discontinuous or take the value $+\infty$.

Earlier convergence theory for GPS assumed continuous differentiability of the objective on a neighbourhood of the level set. Torczon established it for unconstrained problems (SIAM J. Optim. 7, 1997), and Lewis and Torczon extended it to bound constraints (1999) and to finitely many linear constraints (SIAM J. Optim. 10, 2000). Audet and Dennis (SIAM J. Optim. 13, 2003) replaced these analyses with a single argument. Its conclusions are local and are graded by the smoothness of the objective at the limit point only, through Clarke's generalized directional derivative. That paper is the source of this mission. Its analysis is the basis of the later mesh adaptive direct search (MADS) theory (Audet, Dennis, SIAM J. Optim. 17, 2006).

Setting

The problem is

$$\min_{x\in\Omega} f(x),\qquad f:\mathbb R^n\to\mathbb R\cup\{+\infty\},\qquad \Omega=\{x\in\mathbb R^n:\ell\le Ax\le u\},$$

with $A\in\mathbb R^{m\times n}$ and $\ell\le u$ in $(\mathbb R\cup\{\pm\infty\})^m$. The algorithm works with the barrier function $f_\Omega$, equal to $f$ on $\Omega$ and to $+\infty$ elsewhere.

The algorithm uses a finite set of directions $D=G\bar Z$, the columns $d_j=G\bar z_j$ of the product of a nonsingular $G\in\mathbb R^{n\times n}$ and an integer matrix $\bar Z\in\mathbb Z^{n\times p}$. The directions form a positive spanning set: their nonnegative combinations give all of $\mathbb R^n$. At iteration $k$, with iterate $x_k$ and mesh size parameter $\Delta_k>0$, the mesh is $M_k=\{x_k+\Delta_k Dz: z\in\mathbb Z_+^{p}\}$. A poll set $\{x_k+\Delta_k d: d\in D_k\}$ is drawn from a positive spanning subset $D_k\subseteq D$. Each iteration ends in one of two ways:

1. Improved mesh point. Some $x_{k+1}\in M_k\cap\Omega$ with $f_\Omega(x_{k+1})<f_\Omega(x_k)$ was found, by the free SEARCH step or by the poll. Then $\Delta_{k+1}=\tau^{w_k}\Delta_k$ with $0\le w_k\le w^+$.
2. Mesh local optimizer. $f_\Omega(x_k)\le f_\Omega(x_k+\Delta_k d)$ for every $d\in D_k$. Then $x_{k+1}=x_k$ and $\Delta_{k+1}=\tau^{w_k}\Delta_k$ with $w^-\le w_k\le-1$.

Here $\tau>1$ is rational and $w^-\le-1\le 0\le w^+$ are integers. The assumptions are A1 $f_\Omega(x_0)<\infty$, A2 $A$ is rational, and A3 all iterates lie in a compact set. A refining subsequence is an infinite set of mesh local optimizers $\{x_k\}_{k\in K}$ along which $\Delta_k\to 0$ (Definition 3.5). For $f$ Lipschitz near $\hat x$, Clarke's derivative is

$$f^\circ(\hat x;d)=\limsup_{y\to\hat x,\ t\downarrow 0}\frac{f(y+td)-f(y)}{t}.$$

Formalization targets

Goal: Theorem 3.7

Assume A1–A3. Let $\hat x$ be the limit of a refining subsequence, and let $d\in D$ be a direction polled at a feasible point $x_k+\Delta_k d$ for infinitely many $k$ in the subsequence. If $f$ is Lipschitz near $\hat x$, then

$$f^\circ(\hat x;d)\ \ge\ 0 .$$

Milestones on the way

• Theorem 3.1: the iterates have a limit point, $\lim_k f(x_k)$ exists and dominates $f$ at lower semicontinuity limit points, and all continuity limit points share one value.
• Lemma 3.2: $\min_{u\ne v\in M_k}\|u-v\|\ge\Delta_k/\|G^{-1}\|$ for every norm giving nonzero integer vectors norm at least $1$.
• Lemma 3.3: $\Delta_k\le\Delta_0\tau^{r^+}$ for some positive integer $r^+$.
• Proposition 3.4: $\liminf_{k\to\infty}\Delta_k=0$.
• Theorem 3.6: a convergent refining subsequence exists.

Corollaries

• Theorem 3.9: if $\Omega=\mathbb R^n$ and $f$ is strictly differentiable at $\hat x$, then $\nabla f(\hat x)=0$.
• Theorem 3.14: if the poll sets conform to the boundary of $\Omega$ (Definition 3.13) and $f$ is strictly differentiable at $\hat x$, then $\nabla f(\hat x)^Tw\ge 0$ on the tangent cone $T_\Omega(\hat x)$ and $-\nabla f(\hat x)\in N_\Omega(\hat x)$. So $\hat x$ is a KKT point.

Significance

Theorem 3.7 gives a first-order conclusion at a limit point from a local hypothesis at that point alone. It does not require smoothness elsewhere, finiteness of $f$ elsewhere, or continuity. It turns the heuristic "the method stopped improving on ever finer meshes" into a statement about generalized derivatives. The unconstrained stationarity result (Theorem 3.9) and the linearly constrained KKT result (Theorem 3.14) follow from it, and they recover the Torczon and Lewis–Torczon theorems under weaker smoothness assumptions. The chain Lemma 3.2 → Lemma 3.3 → Proposition 3.4 → Theorem 3.6 shows that the goal's hypothesis is always met. Every run satisfying A1 and A3 has a refining subsequence, which rests on the rationality of $\tau$ and on the integer structure of $D$.

All results in this mission are proved in the source paper. None of them has, to the best of our knowledge, a machine-checked proof. The mission contributes a formal model of the GPS algorithm class as a class of runs, a formal Clarke directional derivative, and checked proofs of the mesh-refinement chain and the main theorem.

Difficulty

Given a refining subsequence, the goal is a comparison of limsups: the poll inequalities give nonnegative difference quotients at the points $(x_k,\Delta_k)$, which converge to $(\hat x,0^+)$. The difficulty lies in two places. First, the objective is extended-valued, and the barrier hides $f$ at infeasible poll points, where the poll inequality $f_\Omega(x_k)\le+\infty$ says nothing. The hypothesis on $d$ has to supply feasibility, and the Lipschitz hypothesis has to supply finiteness near $\hat x$. Second, the existence of refining subsequences is not a compactness argument alone. Coarsening is allowed, so $\Delta_k$ need not decrease, and with an irrational $\tau$ or a direction set that is not an integer lattice image (for instance $D=[-1,+\pi]$ in $\mathbb R$) the meshes can be dense and $\liminf\Delta_k$ can be positive. The lattice argument behind Proposition 3.4 is where the integrality hypotheses are used.

Formalization scope

Points of $\mathbb R^n$ are Fin n → ℝ, $f$ takes values in WithTop ℝ, and the bounds $\ell,u$ are EReal-valued, so $m=0$ gives $\Omega=\mathbb R^n$. The barrier is defined by cases, never by extended addition. Directions are the columns of G * Zbar indexed by Fin p, and $D_k$ is a Finset (Fin p). A GPS run is a structure of sequences $x_k,\Delta_k,D_k,w_k$ and a per-iteration predicate "mesh local optimizer", subject to exactly the two update rules above, $\Delta_0>0$, rational $\tau>1$ and the exponent bounds. The SEARCH step, the choice of $D_k$ and the exponents are left free, since the paper allows any strategy. A subsequence is a strictly increasing map $K:\mathbb N\to\mathbb N$. The Clarke derivative of a real function is an EReal-valued limit superior along $y\to\hat x$, $t\to 0^+$. "$f$ Lipschitz near $\hat x$" means that $f$ agrees near $\hat x$ with a real function Lipschitz there, and the conclusions are stated for every such function. Strict differentiability is the directional notion of Section 3.4 of the paper.

The goal is not trivialized by an empty run class: Theorem 3.6, on the same class, asserts that refining subsequences exist. The mesh-local-optimizer branch requires the complete poll inequality over $D_k$. The Clarke limit superior cannot take a default value. The direction $d$ must be polled at feasible points infinitely often, which is the paper's "$f$ was evaluated".

Contributions welcome: proofs of any milestone, and reusable lemmas on positive spanning sets, lattice points in compact sets, and the Clarke derivative (for instance, that it equals $\nabla f(\hat x)^Td$ under strict differentiability).

Selected references

• C. Audet, J. E. Dennis Jr., Analysis of Generalized Pattern Searches, SIAM J. Optim. 13(3):889–903, 2003. https://doi.org/10.1137/S1052623400378742
• V. Torczon, On the Convergence of Pattern Search Algorithms, SIAM J. Optim. 7(1):1–25, 1997. https://doi.org/10.1137/S1052623493250780
• R. M. Lewis, V. Torczon, Pattern Search Methods for Linearly Constrained Minimization, SIAM J. Optim. 10(3):917–941, 2000. https://doi.org/10.1137/S1052623497331373
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; reprinted SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309
• A. J. Booker, J. E. Dennis Jr., P. D. Frank, D. B. Serafini, V. Torczon, M. W. Trosset, A rigorous framework for optimization of expensive functions by surrogates, Structural Optimization 17:1–13, 1999. https://doi.org/10.1007/BF01197559
• C. Audet, J. E. Dennis Jr., Mesh Adaptive Direct Search Algorithms for Constrained Optimization, SIAM J. Optim. 17(1):188–217, 2006. https://doi.org/10.1137/040603371