All missions

Motivation

The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every $n$, not just in the limit.

Timeline.

• 1933–1944. Kolmogorov and Smirnov introduce the statistics, prove that their laws do not depend on the continuous distribution, and find the limit laws, e.g. $\lim_n P(D_n^->\lambda)=\exp(-2\lambda^2)$. Smirnov (1944) also gives the exact law of the one-sided statistic and the expansion $P(D_n^->\lambda)=\exp(-2\lambda^2)\bigl(1-\frac{2\lambda}{3\sqrt n}+O(n^{-1})\bigr)$.
• 1956. Dvoretzky, Kiefer and Wolfowitz prove $P(D_n^->\lambda)\le C\exp(-2\lambda^2)$ for every $n$, with an unspecified constant $C$ (Ann. Math. Statist. 27).
• 1958. Birnbaum and McCarty conjecture that $C=1$ is admissible.
• 1979–1985. Explicit constants: $C\le306$ (Devroye and Wise), $C\le29$ (Shorack and Wellner), $C\le2\sqrt2$ (Hu).
• 1990. Massart proves the conjecture under a mild lower bound on $\lambda$, and deduces the two-sided bound with the optimal constant $2$ (Ann. Probab. 18).

Setting

Let $x_1,\dots,x_n$ ($n\ge1$) be independent, identically distributed real random variables with a continuous distribution function $F$. The empirical distribution function is

$$\hat F_n(x)=\frac1n\sum_{i=1}^n\mathbb 1_{(x_i\le x)},$$

and the centred, normalised empirical process is $Z_n=\sqrt n(\hat F_n-F)$. The statistics are

$$D_n^+=\sup_{x\in\mathbb R}Z_n(x),\qquad D_n^-=\sup_{x\in\mathbb R}\bigl(-Z_n(x)\bigr),\qquad D_n=\sup_{x\in\mathbb R}|Z_n(x)|.$$

In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), $F$ is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter $\lambda$ is written l.

The proof works with Smirnov's point probabilities $p_{\lambda,n}(j)=\lambda\sqrt n\,(j+\lambda\sqrt n)^{j-1}(n-j-\lambda\sqrt n)^{n-j}n^{-n}\binom nj$, whose sum over $0\le j<n-\lambda\sqrt n$ is $P(D_n^->\lambda)$, with Csáki's density $f_\lambda(s)=\frac{\lambda}{\sqrt{2\pi}}s^{-3/2}(1-s)^{-1/2}\exp\bigl(-\frac{\lambda^2}{2s(1-s)}\bigr)$ of the first passage of a Brownian bridge at level $\lambda$, and with the ratio $C_{\lambda,n}=\exp(2\lambda^2)P(D_n^->\lambda)$.

Formalization targets

Goal: Theorem 1

For every $n\ge1$ and every $\lambda\ge\sqrt{\log(2)/2}\wedge\gamma n^{-1/6}$, with $\gamma=1.0841$,

$$P(D_n^->\lambda)\le\exp(-2\lambda^2).$$

Here $\wedge$ is the minimum. The constant $1$ in front of the exponential is the point of the theorem; the threshold on $\lambda$ is the paper's.

Milestones

The milestones follow the proof in the paper's order of attack:

1. the reduction to the uniform law, and Smirnov's exact formula (2.3);
2. the identity $\int_0^1f_\lambda=\exp(-2\lambda^2)$ (2.4);
3. the local comparison of $p_{\lambda,n}(j)$ with $f_\lambda$: (2.7), Lemma 2, Claims 1–3, and Proposition 1;
4. the midpoint bound for log-convex integrands (Lemma 3) and the closed forms of Lemma 4;
5. the nonasymptotic expansion (2.11), the negativity of its right side $\eta_n$, and with them Theorem 1 for $n\ge39$, $\lambda\le\sqrt n/2$;
6. Proposition 2 on the slope of $C_{\lambda,n}$, the crude bounds (2.13)–(2.14), and the finite grid check (2.15) for $n\le38$.

Companions

The equality in law of $D_n^+$ and $D_n^-$, Comment 1 ((1.4) whenever $\exp(-2\lambda^2)\le1/2$), the reduction $P(D_n>\lambda)\le2P(D_n^->\lambda)$, and Corollary 1:

$$P(D_n>\lambda)\le2\exp(-2\lambda^2)\qquad(\lambda>0).$$

Significance

The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, $1$ and $2$, which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.

Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified $C$. The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, $\eta_{39}$); turning those into checked certificates is part of the work.

Difficulty

The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison $P(\tau_n=t)\le\frac1nf_\lambda(t-\varepsilon/3)$ is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time $t$ is close to $\varepsilon=\lambda/\sqrt n$. Controlling that factor uniformly in $j$ while keeping the leading constant exactly $1$ is what forces the delicate constants ($\theta=0.4833$, $\beta=0.826$, $\mu=0.4345$, $\gamma=1.0841$). For small $n$ the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on $\lambda\mapsto C_{\lambda,n}$ plus a finite numerical check over a grid; neither half suffices alone.

Formalization scope

Conventions:

• $n\ge1$; the sample is indexed by Fin n; $F$ is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.
• Probabilities are measures of events in $[0,\infty]$ and are compared with ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in $[-1,1]$, hence a genuine real supremum.
• $p_{\lambda,n}(j)$ uses an integer power at $j-1$, so that $p_{\lambda,n}(0)=(1-\varepsilon)^n$. $C_{\lambda,n}$ is defined from the exact formula (2.3); it equals $\exp(2\lambda^2)P(D_n^->\lambda)$ by the (2.3) milestone, so the analytic milestones carry no probability.
• Statements that the page gives through derivatives of $C_{\lambda,n}$ (Proposition 2(i), (iii)) are stated as monotonicity and as an increment bound, because $C_{\lambda,n}$ has kinks.

Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of $j$), (2.8) (swapped numerators) and Proposition 2(i) ("$\ge0$" for nonincreasing) are corrected; Claim 2 carries the hypothesis $\varepsilon\le3s'$, without which the corrected claim is false; Lemma 3 uses strict inequalities $\delta<s<1-\delta$; Comment 1 makes the implicit $\lambda>0$ explicit; (2.14) carries Proposition 2's standing range $n\ge2$, $0<\lambda<\sqrt n$.

The goal does not mention $p_{\lambda,n}$, $f_\lambda$, $C_{\lambda,n}$, the case split at $n=39$, or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.

Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on $]0,1[$; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.

Selected references

• P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Ann. Probab. 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
• A. Dvoretzky, J. Kiefer, J. Wolfowitz, Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator, Ann. Math. Statist. 27:642–669, 1956. https://doi.org/10.1214/aoms/1177728174
• Z. W. Birnbaum, R. C. McCarty, A distribution-free upper confidence bound for P(Y<X), based on independent samples of X and Y, Ann. Math. Statist. 29:558–562, 1958.
• N. V. Smirnov, Approximate laws of distribution of random variables from empirical data, Uspekhi Mat. Nauk 10:179–206, 1944.
• E. Csáki, Investigations concerning the empirical distribution function, Magyar Tud. Akad. Mat. Fiz. Oszt. Közl. 23:239–327, 1974; English translation in Selected Transl. Math. Statist. Probab. 15:229–317, 1981.
• G. R. Shorack, J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986.

Motivation

Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.

Timeline of the LP approach to average-cost problems:

• 1960 — Manne: the inventory model as a linear program in the joint probabilities of (stock level, production quantity); mixed strategies allowed; the decision rule is read off as a conditional probability.
• 1960 — H. M. Wagner, in a companion note in the same issue, shows that an optimal solution consisting of pure strategies exists.
• 1962 — C. Derman (Management Science 9(1), 1962) gives the general finite-state, finite-action version, assuming every stationary randomized rule yields an irreducible chain.
• 1960 — F. d'Epenoux (Revue Française de Recherche Opérationnelle 4, No. 14; English translation 1963) treats the discounted criterion by linear programming, as Manne's closing note records.

Setting

A positive integer $T$ bounds inventory accumulation; the stock levels are $0,1,\dots,T$. At the start of a month the initial stock $i$ is observed and a production quantity $j$ is chosen; the available stock is $k=i+j$. The month's demand $n\in\{0,1,2,\dots\}$ is independent of everything else and has law $p_n$. Backlogs are excluded, so the terminal stock is $t=\max(0,k-n)$, which becomes the next initial stock. A finite set $A$ of admissible pairs $(i,j)$, all with $i+j\le T$ and containing $(i,0)$ for every $i\le T$, lists the decisions available at each stock level. Costs are three arbitrary real functions: $C_1(i)$ of the initial stock, $C_2(j)$ of the production quantity, and $C_3(n-k)$ of the shortage level.

A stationary randomized decision rule $q(j\mid i)$ is a conditional probability of producing $j$ at stock $i$, supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of $q$ is a stationary distribution $y=(y_0,\dots,y_T)$ of that chain: the law $y'$ of the terminal stock equals the law $y$ of the initial stock, (2). The expected monthly cost (1) of $q$ in the equilibrium $y$ is

$$\mathcal EC_1(i)+\mathcal EC_2(j)+\mathcal EC_3(n-k),$$

the expectation taken under the joint law $y_i\,q(j\mid i)\,p_n$ of (initial stock, production, demand).

The linear program has one unknown $x_{ij}$ per admissible pair, the joint probability of (initial stock $i$, production $j$). Its constraints are $x_{ij}\ge0$, (4) $\sum_{i,j}x_{ij}=1$, and the equilibrium equations

$$\text{(8.t)}\qquad \sum_j x_{tj}=\sum_{\substack{i,j,n:\\ i+j-n=t}}p_nx_{ij}\qquad(t=1,\dots,T),$$

and its objective (9) is $\sum_{i,j}c_{ij}x_{ij}$ with the cost coefficients (10)

$$c_{ij}=C_1(i)+C_2(j)+\sum_np_nC_3(n-i-j).$$

The companion equation (8.0) for $t=0$ has right-hand side $\sum_{i+j-n\le0}p_nx_{ij}$ and is omitted from the constraints. A feasible $x$ is decoded into $y_i=\sum_jx_{ij}$ and $q(j\mid i)=x_{ij}/y_i$.

Formalization targets

The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.

Goal: an LP optimum gives an optimal stationary rule

Assume $\sum_np_n|C_3(n-i-j)|<\infty$ for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution $x^*$, with decoding $(q^*,y^*)$, $q^*$ is a stationary randomized rule, $y^*$ is a statistical equilibrium of $q^*$, and

$$\mathrm{Cost}(q^*,y^*)=\sum_{i,j}c_{ij}x^*_{ij}\le \mathrm{Cost}(q,y)$$

for every stationary randomized rule $q$ and every statistical equilibrium $y$ of $q$.

Milestones

1. (7): under a rule in a distribution $y$, the law of the terminal stock is the right-hand side of (7)/(8) evaluated at $x_{ij}=y_iq(j\mid i)$.
2. (8.0)–(8.T): a rule in statistical equilibrium yields a point satisfying $x\ge0$, (4) and all of (8.0)–(8.T).
3. (8.0) is redundant: (4) and (8.1)–(8.T) imply (8.0).
4. §3, N.B.: every feasible $x$ equals $y_iq(j\mid i)$ for its decoding $(q,y)$, with $y$ an equilibrium of $q$.
5. (10): the expected monthly cost (1) under the joint law $x_{ij}p_n$ equals $\sum c_{ij}x_{ij}$.
6. Table 1: the cost coefficients of the §6 example ($T=3$, $p=(2/3,0,1/3)$, $C_1(i)=i$, $C_2(j)=3j$, $C_3(m)=\max[0,6m]$, $j\in\{0,1\}$) are $4,5,3,4,2,5,3$.
7. Table 2, footnote 3: $x_{01}=1/3$, $x_{11}=2/9$, $x_{20}=4/9$ is optimal with cost $31/9$; the do-nothing solution costs $4$.
8. Footnote 5: the implicit prices $-7/3,-13/3,-11/3$ of (8.1)–(8.3), with $31/9$ on (4), are an optimal dual solution.

Significance

The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.

The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient $x_{ij}/\sum_jx_{ij}$ is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.

Difficulty

Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over $(i,j,n)$ with conditions $i+j-n\le0$ and $i+j-n=t$, and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and $\sum_np_n=1$. The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level $0$ must be recovered from (4) and the bound $i+j\le T$. And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.

Formalization scope

All statements live in the namespace ManneLP.Equilibrium. Conventions:

• Stock levels and production quantities are natural numbers; a model carries $T>0$, the admissible set $A$ (a Finset (ℕ × ℕ) with $i+j\le T$ and every $(i,0)\in A$), a demand law $p:\mathbb N\to\mathbb R$ with $p_n\ge0$ and HasSum p 1, and costs $C_1,C_2:\mathbb N\to\mathbb R$, $C_3:\mathbb Z\to\mathbb R$. The shortage level $n-i-j$ is an integer; no convexity, sign or monotonicity of the costs is assumed.
• The admissible set is a parameter: §6 imposes a capacity limit $j\le1$. Reading of the page: $i+j\le T$ is how §2's requirement $\max(0,k-n)\le T$ holds whatever the demand; $(i,0)\in A$ (producing nothing is possible) is implicit in §2.
• The terminal stock is computed by truncated subtraction in $\mathbb N$, which equals $\max(0,k-n)$. Sums over demands are tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.
• A statistical equilibrium is a stationary distribution of the chain of the rule, defined from the transition probabilities, not from (8). The expected monthly cost is defined from the joint law of (stock, production, demand), not as $\sum c_{ij}x_{ij}$. The LP constraint set omits (8.0), exactly as the page does.
• The decoded rule uses the default action $j=0$ at stock levels with $\sum_jx_{ij}=0$; any admissible default would do.
• Table 2's $x_{30}=\varepsilon$ is the paper's device against degeneracy; the example's solution has $x_{30}=0$. Footnote 5 prints no price for (4); $31/9$ is the price forced by equal objectives, and the dual optimum is not claimed unique.

Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as $\sum c_{ij}x_{ij}$ (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.

Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.

Selected references

• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963 (translation of the 1960 French paper). https://doi.org/10.1287/mnsc.10.1.98

Motivation

The simplex method and every other edge-following linear programming algorithm moves from vertex to vertex of the feasible region along its edges. The number of steps such an algorithm needs in the worst case is at least the combinatorial diameter of the feasible polyhedron: the largest distance, counted in edges, between two of its vertices. Klee and Walkup introduced the two functions that measure this worst case, $\Delta(d,n)$ for polyhedra and $\Delta_b(d,n)$ for bounded polyhedra of dimension $d$ with $n$ facets, and wrote that $\Delta(d,n)$ "represents, in a sense, the number of iterations required to solve the 'worst' linear program of $n$ inequalities in $d$ variables using the 'best' edge-following algorithm" (Klee and Walkup 1967, p. 54).

The Hirsch conjecture, reported by Dantzig in 1963, asserted $\Delta(d,n)\le n-d$. Its diagonal cases $\Delta(d,2d)\le d$ and $\Delta_b(d,2d)\le d$ are the general and the bounded $d$-step conjectures.

Timeline.

• 1957–1963: W. M. Hirsch's conjecture, reported in Dantzig's Linear Programming and Extensions (1963, pp. 160, 168), with the claim that it holds for $m\le 4$.
• Before 1967: Klee determines $\Delta(3,n)=n-3$ and $\Delta_b(3,n)=\lfloor 2n/3\rfloor-1$ and settles $\Delta_b(d,n)$ for $n\le d+4$ (Canad. J. Math. 16 and the papers cited as [9], [12], [13] by Klee and Walkup, p. 55).
• 1967: Klee and Walkup (Acta Math. 117) prove $\Delta_b(5,10)=5$, show that $\Delta_b(d,2d)\le d$ for all $d$ is equivalent to the bounded Hirsch conjecture, and disprove the unbounded conjecture with $\Delta(4,8)=5$.
• 2012: Santos disproves the bounded Hirsch conjecture with a 43-dimensional polytope with 86 facets (Ann. Math. 176). The bounded $d$-step conjecture therefore fails for some $d$, and the smallest failing $d$ is unknown; it is at least 6.

Setting

A polyhedron in $\mathbb R^d$ is a nonempty set $P=\{x:\langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}$; a polytope is a bounded polyhedron. $P$ is a $d$-polyhedron with $n$ facets when it has nonempty interior and none of the $n$ inequalities is redundant; then the rows are in bijection with the facets, and row $i$ is tight at $v$ exactly when $v$ lies on the $i$-th facet. The vertices of $P$ are its extreme points. Two vertices $u\ne v$ span an edge when the segment $[u,v]$ is an extreme subset of $P$. A path of length $l$ is a sequence of $l$ edges $[x_0,x_1],\dots,[x_{l-1},x_l]$, and $\delta_P(x,y)$ is the least length of a path from $x$ to $y$. Then

$$\Delta_b(d,n)=\max\{\delta_P(x,y): P\text{ a }d\text{-polytope with }n\text{ facets},\ x,y\text{ vertices of }P\}.$$

$P$ is simple when every vertex lies on exactly $d$ facets. A face is $P$ itself or the intersection of $P$ with a supporting hyperplane, never $\emptyset$; its dimension is that of its affine hull. A $(k_1,\dots,k_r)$-path from $x$ to $y$ is a sequence of faces $K_1,\dots,K_r$ with $x\in K_1$, $y\in K_r$, $\dim K_i=k_i$ and $K_i\cap K_{i+1}\ne\emptyset$. A $d$-dimensional Dantzig figure $(P,x,y)$ is a $d$-polyhedron $P$ with $2d$ facets and two vertices $x,y$ such that exactly $d$ facets are incident to $x$ and the other $d$ to $y$. A $d$-polytope $Q$ has property A when it has between $2d$ and $2d+2$ facets and the following holds: if its facets are split into two classes $\mathfrak X,\mathfrak Y$ of at most $d+1$ facets each, and both sets $X$, $Y$ of vertices all of whose facets lie in $\mathfrak X$, respectively $\mathfrak Y$, are nonempty, then some vertex of $X$ is joined to some vertex of $Y$ by a path of length at most $d$.

Formalization targets

Goal: 4.3 THEOREM

$$\Delta_b(5,10)=5.$$

In two halves: every $5$-polytope with $10$ facets satisfies $\delta_P(x,y)\le 5$ for all vertices $x,y$, and some $5$-polytope with $10$ facets has two vertices with $\delta_P(x,y)>4$.

Milestones, in the order the proof uses them

1. 2.8 THEOREM (bounded part): $\Delta_b(d,n)$ is attained by two vertices of a simple $d$-polytope with $n$ facets, and for $n\ge 2d$ by two vertices on no common facet. For $n=2d$ this is a bounded simple Dantzig figure.
2. 3.4 PROPOSITION (a): every simple Dantzig figure admits a $(k_1,1,k_3)$-path for positive $k_1+1+k_3=d$.
3. 3.1 PROPOSITION: (a) facial paths in all $d$-dimensional simple Dantzig figures, (b) facet-avoiding facial paths in simple $d$-polytopes with $2d+1$ facets, and (c) facet-avoiding $(1,k_1,\dots,k_r)$-paths in bounded $(d+1)$-dimensional figures are equivalent.
4. 3.4 PROPOSITION (b): every bounded simple Dantzig figure admits a $(1,k_2,1,k_4)$-path for positive $1+k_2+1+k_4=d$.
5. Remark after 3.4: adjacent terms of a facial path in a simple figure merge into their sum.
6. Remark after 3.4, p. 68: bounded simple Dantzig figures of dimension $d\ge 2$ admit $(1,d-2,1)$-paths.
7. 4.1 PROPOSITION: if the middle face $Q$ of a $(1,d-2,1)$-path $([x,x'],Q,[y',y])$ has property A, then $\delta_P(x,y)\le d$.
8. 4.2 LEMMA: every simple $3$-polytope with $6$, $7$ or $8$ facets has property A.

Significance

The result. By the paper's reductions, $\Delta_b(d,2d)\le d$ for a given $d$ is equivalent to the bounded Hirsch bound $\Delta_b(d',d'+d)\le d$ for every $d'$. So 4.3 gives $\Delta_b(d,n)\le n-d$ for all $n\le d+5$, which is the column $n-d=5$ of the paper's Fig. 2. Since Santos's counterexample, the smallest $d$ with $\Delta_b(d,2d)>d$ is a well-defined open number. This theorem was the first to show it is at least $6$; later computer-assisted work treated further small cases, including the bounded $6$-step case (Bremner and Schewe 2011). Santos's construction starts from exactly the reduction to Dantzig figures (the "strong $d$-step theorem" for spindles) that this paper uses.

Formalizing it. The result has been proved since 1967; no machine-checked proof of $\Delta_b(5,10)=5$ exists. The platform has the Hirsch bound in dimension $\le 3$ (Hirsch.dimension_three_bound, Hirsch.klee_three_dimensional_bound), the Klee–Walkup wedge reduction at the level of inequality descriptions (Hirsch.balanced_hpoly_transfer), products (Hirsch.diamLE_prod) and Santos's counterexample. The mission adds the facial-path calculus of §3 and the property-A argument of §4. Both are reusable in any later formal treatment of small $d$-step cases.

Difficulty

The obvious approach, a direct case analysis of $5$-polytopes with $10$ facets, is out of reach: there are far too many combinatorial types, and nothing bounds the search. The paper first reduces to simple polytopes, and the reduction itself (2.8) rests on a perturbation lemma (2.6) whose proof is deferred to a separate paper by Walkup: simplicity must be gained without shrinking any distance. The facial-path results then pass between bounded and unbounded figures through truncation and the wedge (3.1), and a statement about all unbounded $d$-dimensional figures is what yields one about bounded $(d+1)$-dimensional ones. Finally the $(d-2)$-face $Q$ must be shown to have property A. That property fails for some simple polytopes of classes $(4,10)$ and $(5,11)$ (p. 69), so 4.2 depends on the dimension being $3$ and on the facet count being at most $8$. Its proof uses Euler's relation and Balinski's theorem that the graph of a $3$-polytope is $3$-connected (posed on the platform as Balinski61.Connectivity.disjoint_paths_between_vertices).

Formalization scope

Polyhedra are Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d); edges and walks are Hirsch.Adj and Hirsch.Reach from the published Hirsch_model and Hirsch_walk. The conventions are:

• "$d$-polyhedron with $n$ facets" is a facet presentation: nonempty interior and no redundant row. The rows are exactly the facets; a statement over arbitrary inequality systems would count redundant rows as facets and is not the paper's.
• $\delta_P(x,y)\le L$ is Hirsch.Reach P L x y, a walk of $L$ steps that may stand still. $\Delta_b(5,10)=5$ is an upper bound for every polytope plus a witness, never a supremum of reals. A version proving only the upper bound, or only the lower bound, is not the goal.
• Simple means pointed with exactly $d$ tight rows at every vertex. On a facet presentation this is equivalent to the paper's "exactly $d$ edges at each vertex".
• Faces are nonempty sets $\{x\in P:\langle a_i,x\rangle=b_i,\ i\in I\}$, and dimension is the dimension of the affine span. A Dantzig figure has Fin (2 * d) rows.
• Property A is defined for a bounded face $Q$ of dimension $m$: its facets are the $(m-1)$-faces of $P$ inside $Q$, and the path runs in $Q$. This keeps 4.1, where $Q$ is a $(d-2)$-face of a polytope in $\mathbb R^d$, and 4.2, where $Q=P$, under one notion. Facet counts use Set.encard.
• Explicit readings: 2.8's "$\Delta_b$ can be realized as the distance … of a simple polytope" is stated polytope by polytope ($\delta_P(u,v)\le\delta_{P'}(x,y)$). Only the $\Delta_b$ sentences of 2.8 are stated. 3.4's joint hypothesis on $k_1,\dots,k_4$ is split by part. The merging remark carries the needed hypothesis $k_i+k_{i+1}\le d$. The printed "3.5 implies" on p. 67 is read as 3.4.

The paper cites two inputs without proving them: Lemma 2.6 (Walkup's simple perturbation) and Balinski's theorem. A complete development needs face lattices of H-polyhedra, wedges and truncations, and the planar-graph arguments of 4.2. The face and facial-path layer is reusable for the companion mission on $\Delta(4,8)=5$ and for other diameter problems. Contributions are welcome at every milestone, including proofs of 2.6.

Selected references

• V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Mathematica 117 (1967), 53–78. https://doi.org/10.1007/BF02395040
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963.
• V. Klee, Diameters of polyhedral graphs, Canadian Journal of Mathematics 16 (1964), 602–614. https://doi.org/10.4153/CJM-1964-058-5
• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific Journal of Mathematics 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176 (2012), 383–412. https://doi.org/10.4007/annals.2012.176.1.7
• D. Bremner and L. Schewe, Edge-graph diameter bounds for convex polytopes with few facets, Experimental Mathematics 20 (2011), 229–237. https://doi.org/10.1080/10586458.2011.564966

Motivation

The linear complementarity problem asks, for a real square matrix $M$ of order $n$ and a vector $q\in\mathbb R^n$, for a vector $z$ with

$$z\ge 0,\qquad w=Mz-q\ge 0,\qquad z^{\mathsf T}w=0 .$$

It is the common form of the Kuhn–Tucker conditions of linear and convex quadratic programs and of the equilibrium conditions of two-person non-zero-sum (bimatrix) games. In 1964 Lemke and Howson gave a constructive existence proof for equilibrium points of bimatrix games by following a path of adjacent extreme points of a polyhedron (Lemke–Howson 1964). In 1965 Lemke adapted that path-following technique to the general problem above, under a condition on $M$ that covers the positive semidefinite case treated by Dantzig and Cottle and the case $M>0$ (Lemke 1965). The resulting procedure, now called Lemke's algorithm or complementary pivoting, became a standard method for linear complementarity problems and a template for later path-following existence proofs (Cottle, Pang, Stone 1992).

Timeline:

• 1964: Lemke and Howson, adjacent-extreme-point path for bimatrix games.
• 1965: Lemke, existence for matrices satisfying conditions (i)–(ii) below (the goal of this mission), under a non-degeneracy assumption, by an augmented path with an artificial variable $z_0$.
• Later literature names matrices with (i)–(ii) copositive-plus, and removes non-degeneracy by lexicographic perturbation.

Setting

Fix a finite index set of size $n$, a real $n\times n$ matrix $M$ and $q\in\mathbb R^n$. Inequalities between vectors are componentwise and $e$ is the all-ones vector.

• The set $Z=\{z\in\mathbb R^n : z\ge 0,\ w=Mz-q\ge 0\}$; $w$ is always the function $Mz-q$ of $z$.
• An equilibrium point is a point $z\in Z$ with $z^{\mathsf T}w=0$; $S$ is the set of them.
• For any $z\in\mathbb R^n$, the matrix $N(z)$ consists of the columns of $(M^{\mathsf T},I)$ that are kept when one deletes the $i$-th column of $M^{\mathsf T}$ whenever $w_i\ne 0$ and the $i$-th column of $I$ whenever $z_i\ne0$.
• An extreme point of $Z$ is a point $z\in Z$ with $\operatorname{rank}N(z)=n$; $z$ lies on an open edge if $z\in Z$ and $\operatorname{rank}N(z)=n-1$. An open edge is the set of points of $Z$ sharing the matrix $N(z)$ of such a point; a ray is an open edge with exactly one end-point.
• $Z$ is non-degenerate if for every $z\in\mathbb R^n$ the columns of $N(z)$ are linearly independent.
• For an index $s$, $Z_s=\{z\in Z : z^{\mathsf T}w=z_sw_s\}$. An adjacency path is a non-empty connected class of closed edges of $Z$ no three of which meet; its end-points are the extreme points lying on exactly one of its edges.
• The augmented sets: $Z^*=\{(z,z_0) : z\ge0,\ z_0\ge0,\ Mz+z_0e-q\ge0\}$, its subset $Z_0^*$ where $z^{\mathsf T}w=0$, and, for a number $k$, $Z^{**}$, the set of the form above for the bordered data $\begin{pmatrix}M&e\\-e^{\mathsf T}&0\end{pmatrix}$, $\begin{pmatrix}q\\-k\end{pmatrix}$.

Formalization targets

Goal: Theorem 4 (p. 7)

Suppose $Z$ is non-degenerate and that for every $u\ge0$

$$\text{(i)}\ u^{\mathsf T}Mu\ge 0,\qquad \text{(ii)}\ u^{\mathsf T}Mu=0\ \Longrightarrow\ Mu+M^{\mathsf T}u=0 .$$

Then

$$Z\ne\emptyset\ \Longrightarrow\ \exists z\in Z,\ z^{\mathsf T}(Mz-q)=0 .$$

Milestones, in the order the paper's proof uses them

1. Theorem 1 (p. 3): for non-degenerate $Z$, $Z_s$ is empty or a disjoint union of adjacency paths whose end-points are exactly the equilibrium points.
2. Lemma 2 (p. 4): $Z=\emptyset$ iff some $u\ge0$ has $M^{\mathsf T}u\le0$, $u^{\mathsf T}q>0$.
3. Theorem 2 (p. 4): if some $Z_s$ contains precisely one ray of a non-degenerate $Z$, the number of equilibrium points is odd.
4. p. 6: for $k$ chosen as in (12), the starting ray $E_0^*$ ($z=0$) is a ray of $Z^{**}$ inside $Z_0^{**}$, and it is the only one.
5. Lemma 2 (p. 6): $Z^{**}$ has an equilibrium point.
6. Lemma 3 (p. 7): a ray $(\bar z+\theta u,\bar z_0+\theta u_0)$ of $Z^*$ in $Z_0^*$ with $e^{\mathsf T}u=1$ satisfies $u^{\mathsf T}Mu+u_0=0$.
7. (22)–(25) (pp. 7–8): under (i)–(ii) such a ray has $\bar z_0=0$ and $\bar z$ an equilibrium point of $Z$, or $\bar z_0>0$ and $Z=\emptyset$.

Companion results

The Corollary (p. 5: $q=e$, $M>0$ gives an odd number of equilibrium points), Theorem 3 (p. 5: if $z^{\mathsf T}Mz\ge0$ for all $z$, at most one equilibrium point) and Theorem 5 (p. 8: if moreover $Z\ne\emptyset$, $Z$ has at least $n$ rays).

Significance

Theorem 4 is an existence theorem for a class of linear complementarity problems that contains convex quadratic programming (the case $z^{\mathsf T}Mz\ge0$ for all $z$) and strictly positive matrices, and its proof is an algorithm: the path followed is the sequence of pivots of Lemke's method. The parity statements (Theorem 2, the Corollary) are an early instance of the path-following parity arguments later abstracted in the complexity class PPAD (Papadimitriou 1994).

The theorem is classical and proved. To our knowledge neither Lemke's theorem nor the polyhedral path machinery of Theorems 1–2 has a machine-checked proof in Lean or Mathlib. This mission produces the vocabulary of non-degenerate complementarity polyhedra (the matrix $N(z)$, open edges, rays, adjacency paths), the parity theorem, and the existence theorem itself; the Farkas-type Lemma 2 (p. 4) is already available on the platform.

Difficulty

The algebraic part (Lemma 3 and (22)–(25)) is short. The difficulty is combinatorial-geometric: Theorem 1 requires that, under non-degeneracy, every extreme point of $Z$ has exactly $n$ incident edges, that each point of $Z_s$ is an extreme point or lies on an open edge, and that the edges contained in $Z_s$ form paths whose end-points are exactly the equilibrium points; the parity of Theorem 2 then needs finiteness of the set of extreme points. None of this polyhedral structure (edges as zero-pattern classes, their closures and end-points) is in Mathlib. Moreover, the printed proof of Theorem 4 applies Theorem 2 to $Z^{**}$, whose non-degeneracy the paper obtains from an informal perturbation remark, and it sketches the step from the end of the augmented path to a ray of $Z^*$; a complete proof of the goal must supply these steps or take another route.

Formalization scope

• Vectors are functions from a finite index type $\iota$ to $\mathbb R$ ($n=|\iota|$; $\mathrm{Fin}\,n$ is a special case); the bordered system lives on $\iota\oplus\{\ast\}$. $w$ is always $Mz-q$, never a free variable.
• $N(z)$ is the indexed family of its columns, $\operatorname{rank}N(z)$ the dimension of their span; "$\operatorname{rank}N(z)=n-1$" is written $\operatorname{rank}N(z)+1=n$.
• Non-degeneracy (Def. 3) is linear independence of the columns of $N(z)$ for every $z\in\mathbb R^n$. The phrase "(but not all)" is read as excluding only the empty matrix; the other reading differs only when $q=0$, and the formal definition is then the stronger hypothesis.
• An open edge is the set of points of $Z$ with the zero pattern of a point $z_0$ with $\operatorname{rank}N(z_0)=n-1$; closed edges are closures; end-points of an open edge $E$ are the points of $\overline E\setminus E$; a ray has exactly one. Adjacency paths are classes of closed edges.
• Conditions (i)–(ii) are quantified over $u\ge0$ only. "Non-negative definite" (Theorems 3, 5) is $z^{\mathsf T}Mz\ge0$ for all $z$, with no symmetry assumed.
• "An odd number" is finiteness plus odd cardinality; "at least $n$ rays" counts rays as an extended natural number; "at most one" is a subsingleton.
• Equilibrium points include membership in $Z$: $z^{\mathsf T}(Mz-q)=0$ alone holds at $z=0$ and would make the goal trivial. The goal mentions neither $Z^*$, $Z^{**}$, $k$, rays nor paths; in particular non-degeneracy of $Z^{**}$ is not a hypothesis of the goal.
• Deviations: Lemma 2 (p. 6) assumes non-degeneracy of $Z^{**}$ (Def. 3 does not define it for the non-square $Z^*$); milestone 4 holds for every $k$ without non-degeneracy; Lemma 3 and (22)–(25) parametrize the ray as in (15) without requiring $\bar z^*$ to be an extreme point, which makes them stronger.

Contributions welcome: the polyhedral lemmas for non-degenerate $Z$ (extreme points have $n$ edges, finitely many extreme points), the parity argument, and any complete route to Theorem 4.

Selected references

• C. E. Lemke, Bimatrix Equilibrium Points and Mathematical Programming, Management Science 11(7):681–689, 1965. https://doi.org/10.1287/mnsc.11.7.681 (cited from the HAL deposit hal-01885823v1)
• C. E. Lemke, J. T. Howson, Equilibrium Points of Bimatrix Games, J. SIAM 12(2):413–423, 1964. https://doi.org/10.1137/0112033
• R. W. Cottle, J.-S. Pang, R. E. Stone, The Linear Complementarity Problem, Academic Press 1992; SIAM Classics 2009. https://doi.org/10.1137/1.9780898719000
• C. H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Computer and System Sciences 48(3):498–532, 1994. https://doi.org/10.1016/S0022-0000(05)80063-7

Motivation

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.

Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.

A short history of the model:

• Kanet (1981) minimized total absolute deviation from a common due date that is large enough not to constrain the schedule, by a sorting rule. The special case in the middle of §2.1 is the midtime version of this problem.
• Garey, Tarjan and Wilfong (1988) proved the problem with arbitrary preferred times NP-complete (THEOREM 1, this mission), and gave an $O(N\log N)$ algorithm for a fixed task order.
• Hall, Kubiak and Sethi (1991) proved that the common-due-date problem becomes NP-hard when the due date is restrictive. The reduction of THEOREM 1 already uses a common preferred midtime that is not large, together with one extra task that pins the right end.

Setting

There are $N$ tasks $T_1,\dots,T_N$. Task $T_i$ has a length $l_i$ and a preferred midtime $M_i$. A schedule $S$ assigns every task a starting time $s_i\ge0$ such that no two tasks overlap on the single processor: for $i\ne j$, either $s_i+l_i\le s_j$ or $s_j+l_j\le s_i$. Idle time is allowed. The actual midtime of $T_i$ is $m_i(S)=s_i+l_i/2$, and the total discrepancy of $S$ is

$$\mathrm{cost}(S)=\sum_{i=1}^N |m_i(S)-M_i| .$$

The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times $a_i$ are interchangeable through $a_i=M_i-l_i/2$.

Total discrepancy (the decision problem). Given $N,k\in\mathbb Z^+$ and $M_i,l_i\in\mathbb Z^+$, is there a schedule with $\mathrm{cost}(S)\le k$?

Even-odd partition. Given positive integers $x_1<x_2<\dots<x_{2n}$, can they be split into two sets of equal sum so that each set contains exactly one of $x_{2i-1},x_{2i}$ for every $i$?

The special case. For tasks $T_0,\dots,T_{2n}$ with $0<l_0<l_1<\dots<l_{2n}$ and one common preferred midtime $M>\sum_i l_i$, write $A(S)=\{T_i: m_i(S)<M\}$ and $B(S)=\{T_i:m_i(S)>M\}$. A schedule is ordered if, on each side of $M$, shorter tasks lie nearer to $M$. The bracket $[A_n,\dots,A_1,T_0@M,B_1,\dots,B_n]$ is the schedule that puts $T_0$ at midtime $M$ and packs the listed tasks against it in the listed order.

Formalization targets

Goal: THEOREM 1

$$\text{Partition is NP-complete}\ \Longrightarrow\ \text{Total discrepancy is NP-complete.}$$

The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.

Milestones, in attack order

1. Even-odd partition is in NP; the instance $x_1=1$, $x_{2i}=x_{2i-1}+y_i$, $x_{2i+1}=x_{2i}+1$ built from a Partition instance $Y$ is a yes-instance if and only if $Y$ is; and LEMMA 1, even-odd partition is NP-complete.
2. The special case: a minimum cost schedule has no gaps and is ordered; LEMMA 2 (some $m_i(S)=M$), LEMMA 3 ($|A(S)|=|B(S)|$), LEMMA 4 ($m_0(S)=M$), LEMMA 5 (swapping $A_i$ and $B_i$ in a bracket keeps the cost), LEMMA 6 ($\{A_i,B_i\}=\{T_{2i},T_{2i-1}\}$ in a minimum cost bracket), and the minimum cost

$$k=\sum_{i=1}^n(l_{2i}+l_{2i-1})\left(n-i+\tfrac12\right)+l_0\,n .$$

3. At the midtime $M=\frac12\sum_{i=0}^{2n}l_i$ used in the reduction, every schedule of $T_0,\dots,T_{2n}$ costs at least $k$; equality forces the ordered, gap-free form in item 2.
4. The reduction: the instance D with $l_0=x_1-1$, $l_i=x_i$, $l_{2n+1}=2$, $M_j=M=\sum_{i\le 2n}l_i/2$, $M_{2n+1}=2M+1$ has a schedule of cost at most $k$ if and only if $X$ has an even-odd partition. Total discrepancy is in NP.

Significance

THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at $M$, the $i$-th pair of lengths in the $i$-th positions on either side, either member on either side. This characterization holds independently of the reduction.

The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with $M=\sum_i l_i/2$, so they must be restated for every $M$. Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.

Difficulty

The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint $s_i\ge0$ never binds. In D the midtime is $M=\sum_{i=0}^{2n}l_i/2$, exactly half the total length, and the reduction works because the constraint binds. The tasks before $M$ must fit in $[0,M-l_0/2]$, and the extra task $T_{2n+1}$ must sit at $[2M,2M+2]$. Together these force the two sides to have equal total length. A proof that only cites the large-$M$ lemmas proves nothing about D. Conversely, dropping $s_i\ge 0$ makes the reduction false: put the shorter element of every pair after $M$.

The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of $X$, double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.

Formalization scope

• Everything is real-valued except the instance codes. Schedules have real starting times $s_i\ge0$, and integer data are cast to $\mathbb R$. Restricting to integer starting times would be a different problem and is not what is stated.
• Nonnegative starting times are a standing assumption. The paper uses them ("scheduled between 0 and $M-l_0/2$", p. 336) without writing them into the model. Nonoverlap is "one task finishes before the other starts", the reading of "intersect only at their endpoints".
• Tasks are indexed by Fin N from $0$. In the special case $T_i$ is index $i$, and the paper's $T_{2i-1},T_{2i}$ ($1\le i\le n$) are the indices $2k+1,2k+2$ for $k=i-1$.
• Languages use the published CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.
• The goal is not the combinatorial equivalence of milestone 4. It states NP-completeness, so it contains the polynomial-time computation of the reduction and membership in NP. Taking NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.
• Running times of the algorithms of §2.2–§2.4 are out of scope for this mission, as are all results after §2.1.

Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28(4):643–651, 1981. https://doi.org/10.1002/nav.3800280411
• N. G. Hall, W. Kubiak, S. P. Sethi, Earliness–tardiness scheduling problems, II: Deviation of completion times about a restrictive common due date, Operations Research 39(5):847–856, 1991. https://doi.org/10.1287/opre.39.5.847
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Why the timing of a markdown matters

A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.

The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.

Prices, demand, and admissible switches

Let $n\ge1$ be the initial stock and $t\ge0$ the time to go. The seller first charges price $p_1$ and may change once to a lower price $p_2$. Demands at the two prices are independent Poisson counts with positive rates $\lambda_1$ and $\lambda_2$. A lower price produces more arrivals, so $p_2<p_1$ and $\lambda_1<\lambda_2$. Feng and Gallego also assume that lowering the price increases the revenue rate: $p_1\lambda_1<p_2\lambda_2$. There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.

Write $N_1(s)$ for the observed sales count at the initial price by time $s$. If the price changes at deterministic time $s\in[0,t]$, let $J(n,t;s)$ be the expected total revenue. The count after the change is independent of $N_1(s)$, and their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$. The optimal value $J(n,t)$ allows the switch time $\tau$ to depend on the counts observed so far. An admissible $\tau$ lies between zero and $t$, is a stopping time for the history of $N_1$, and occurs before stock is exhausted almost surely. At $s=0$, $J(n,t;0)$ is the revenue from charging $p_2$ immediately. The paper defines these quantities in §3, pp. 1377–1379.

Formalization targets

The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence $x_1<x_2<\cdots$ of inventory-dependent thresholds. When $t\le x_n$, switching immediately earns the optimal value; when $t>x_n$, a correction $F(n,t)$ is added:

$$J(n,t)=\begin{cases} J(n,t;0),&t\le x_n,\\ J(n,t;0)+F(n,t),&t>x_n. \end{cases}$$

The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with $F(0,t)=0$. For $n\ge1$, set $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$, where $G$ is the Poisson-tail expression from §4.1. The threshold $x_n$ is the first nonnegative zero of $L(n,\cdot)$. A function $H(n,\cdot)$ satisfies $\partial_tH=-\lambda_1H+L$ for positive time and $H(n,x_n)=0$; $F$ is zero below $x_n$ and equals $H$ at and above it. If $y_n$ is the first zero of $G(n,\cdot)$, the theorem also gives $x_1=y_1$ and $x_n<y_n$ for $n>1$.

Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of $G$ in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.

What the result provides

The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.

The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.

Where the mathematics is difficult

The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory $n$ depends on the correction at stock $n-1$. Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of $G$, the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.

The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.

Formalization scope

Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.

The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.

For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.

Selected references

• Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.