Operations Research

Motivation

Binary decisions arise when a variable records whether a project is selected, a facility is opened, or an action is taken. Linear constraints then describe the resources or conditions those choices must satisfy. Egon Balas's 1965 paper gives a direct algorithm for a finite linear program with zero-one variables: it begins with all variables at zero, adds variables with value one, and uses explicit tests to discard assignments that cannot improve the best feasible assignment found so far. The paper states that the procedure eventually produces an optimal feasible solution or a conclusion that none exists. Its numbered convergence theorem is the target of this mission. Balas (1965)

The result is historically distinct from algorithms that solve a continuous relaxation and then enforce integrality. Balas describes his method as a direct combinatorial search over binary assignments, with additions and subtractions used to update costs and slacks. The theorem concerns the correctness and finite termination of the particular steps printed in the paper, including their backward scan and cancellation rules. The local catalog contains work on branch and bound for a biconvex program, but no existing platform item about a zero-one programming algorithm with these steps; the biconvex result concerns a different model and algorithm. Balas (1965)

Setting

Let $N$ be a finite set of binary coordinates and $M$ a finite set of constraints. The data are a real matrix $A=(a_{ij})_{i\in M,j\in N}$, a real vector $b=(b_i)_{i\in M}$, and nonnegative objective coefficients $c_j\ge0$. A binary assignment is represented by the set $J\subseteq N$ of coordinates assigned one; all other coordinates are zero. Its slack and cost are

$$y_i(J)=b_i-\sum_{j\in J}a_{ij},\qquad z(J)=\sum_{j\in J}c_j.$$

The assignment is feasible when $y_i(J)\ge0$ for every $i\in M$. It is optimal when it is feasible and has no greater cost than any other feasible assignment. These are Balas's problem $P$ and solutions (1)–(8). The coefficients of $A$ and $b$ may have either sign; $N$ and $M$ may be empty. Balas (1965), pp. 519, 523

The algorithm generates assignments $J_0,J_1,\ldots,J_s$, starting at $J_0=\varnothing$. Among the generated feasible assignments, their least cost is the ceiling $z^{*(s)}$; if there are none, $z^{*(s)}=+\infty$. Each generated assignment has an improving set $N_p$ formed when it first appears. Later steps cancel candidate indices and keep records $C_k^s$ of which values attached to an earlier assignment have been cancelled by the time $J_s$ is generated. The algorithm either processes the latest assignment, scans earlier strict subsets in descending order, or stops. Its value-based choice rule permits several choices when both value and cost tie. Balas (1965), pp. 523–528

Formalization targets

The paper's two lemmas and Theorem 1 establish the cancellation claims used by its convergence theorem. Lemma 1 says a feasible completion $J_t\supset J_s$ below the current ceiling adds no index in $C^s$; Lemma 2 makes the corresponding assertion for an earlier assignment under its stated complete-cancellation hypothesis. Theorem 1 says that an abandoned assignment has no better feasible completion. The two numbered parts of the convergence proof assert that a single iteration cannot continue indefinitely and that no assignment is generated twice. A remark after (16) records that a feasible generated assignment has an empty improving set. Balas (1965), pp. 529–533

The mission's goal is Convergence Theorem 2:

$$\text{every run from }J_0=\varnothing\text{ stops after finitely many steps, with either an optimal feasible assignment or a valid infeasibility verdict.}$$

The finite-step assertion includes progress: every reachable state before a stopping situation has a successor. At a stop, $z^{*(s)}=+\infty$ means no feasible binary assignment exists; if the ceiling is finite, a generated assignment attaining it exists and every generated assignment at that cost is optimal for $P$. These clauses make the paper's two possible outcomes explicit. Balas (1965), Convergence Theorem 2 and step 5a

Significance

The theorem certifies the algorithm as a complete decision and optimization procedure for the stated finite binary program. The infeasibility outcome concerns every possible binary assignment, not only the assignments the algorithm happened to visit. The optimality outcome similarly compares the reported assignment against all feasible assignments. Without these global claims, reaching a stopping situation would only show that the current search path has no remaining candidates. Balas (1965), pp. 526, 533

The result was proved in the 1965 paper. The work here is to state its algorithm and correctness claims in Lean and provide a target for a machine-checked proof; the submitted theorem files are open statements. The finite binary-program model, cost and slack functions, ceiling with infinity, and state-transition vocabulary can also support formal analyses of other exact enumeration procedures. The particular cancellation and backward-scan rules belong to Balas's algorithm. Balas (1965)

Difficulty

It is immediate that there are finitely many binary assignments. That alone does not show finite termination: the paper's step 5 may revisit earlier generated assignments, and the rules must prevent repeated work within one iteration as well as repeated generated assignments across iterations. It also does not justify pruning. When an improving set becomes empty, the remaining challenge is to show that no feasible assignment omitted by the search improves the ceiling. These are the separate claims recorded in parts (a) and (b), Lemmas 1–2, and Theorem 1. Balas (1965), pp. 529–533

Formalization scope

Lean uses Fin n and Fin m for the paper's one-based index sets. A binary assignment is a Finset (Fin n). A general finite zero-one linear program is its own definition; problem $P$ adds the paper's standing assumption $c_j\ge0$. There is no positive-size assumption on either index set. The algorithm stores generated assignments, each improving set as formed, cancellation snapshots, current cancellations, and its program point. Slack and cost are recomputed from the assignment by (6) and (21). Reachability is the reflexive transitive closure of the printed steps, and all milestone claims about states are restricted to reachable ones. The strict symbol $\subset$ means proper inclusion as the paper's footnote specifies. Balas (1965), pp. 523–525

The ceiling is represented in WithTop ℝ, with $\top$ for $+\infty$. The cost tests (14), (17), (24), and (29) are written additively so they retain the paper's meaning when no feasible assignment has yet been generated. The improving set $N_p$ remains fixed after generation; the step-5 scan uses $N_k^s=N_k-(C_k^s\cup D_k^s)$ with the stored snapshot $C_k^s$, as in (18). Step 1a cancels the cost-bound indices for every earlier assignment, and steps 6a and 7b resume the scan below the index just checked. The final tie break permits any index still tied after minimizing its cost. “In a finite number of iterations” is encoded as no infinite run plus a next step at each reachable non-stopped state. “No feasible solution” quantifies over all binary assignments. “Abandoned” is the predicate specified before Theorem 1: $u^k$ is abandoned when the algorithm is instructed to stop, or to check some $N_p^s$ with $p<k\le s$, including the indices step 5 passes over because their remaining improving set is empty. Lemma 2 reads $C_p^{s+1}$ either as the cancellations accumulated so far during iteration $s+1$ or as the cancellation records at the transition that obtains $u^{s+1}$. Balas (1965), pp. 525–533

The paper prints $z^{*(k)}$ in Theorem 1, but its algorithm and proof use the ceiling at the abandonment iteration, $z^{*(s)}$; the Lean theorem states that corrected version and retains the original wording in the milestone record. A transition system that is stuck before a declared stopping situation, a ceiling encoded as a finite real sentinel, or a verdict quantified only over generated assignments would make the goal weaker than the paper's claim. Contributions toward the milestone proofs, state invariants, and reusable finite-search lemmas are in scope. The preliminary reduction of a general binary program to $P$, the efficiency remarks, numerical examples, and the modified algorithm of Remark II are outside this mission. Balas (1965), pp. 519, 528–533

Selected references

• Egon Balas, An Additive Algorithm for Solving Linear Programs with Zero-One Variables, Operations Research 13(4), 517–546, 1965. DOI: 10.1287/opre.13.4.517

Motivation

A component with a random lifetime $X$ that has survived to age $t$ still has a random residual life time $X - t$. Reliability engineering, actuarial science and the statistics of exceedances over high thresholds all ask how the conditional law of $X - t$ given $X > t$ behaves when the age $t$ is large. If $X$ is exponential, the residual life has the same law at every age (lack of memory). In general it changes with $t$, and the natural question, as in the limit theory of sample maxima, is which laws can arise as limits once the residual life is suitably rescaled and shifted.

A. A. Balkema and L. de Haan answered this question in Residual Life Time at Great Age (The Annals of Probability 2, 1974). The answer — a short list of limit types — later underlies the peaks-over-threshold method of extreme value statistics, where the continuous limit laws reappear as the generalized Pareto family (Pickands, 1975). This mission formalizes the classification theorem of the paper, Theorem 1, together with the steps of its proof in §1.

Setting

Let $X$ be a real random variable with distribution function $F$ and distribution tail $R(x) = 1 - F(x) = P\{X > x\}$. Throughout, $R(x) > 0$ for every $x$ (equivalently $F(x) < 1$ for all $x$), so that the conditioning event $\{X > t\}$ never has probability zero. The residual life distribution function at age $t$ is

$$F_t(x) = P\{X - t \le x \mid X > t\}, \tag{1}$$

which vanishes for $x < 0$.

A family of distribution functions $H_t$ converges weakly to $G$ as $t \to \infty$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$. A distribution function $G$ is nondegenerate if it is not the distribution function of a point mass. $G$ is of type $K$ if $G(x) = K(ax + b)$ for all $x$, with $a > 0$ and $b$ real.

The limit laws are the following distribution functions, all equal to $0$ for $x < 0$; for $x \ge 0$,

$$\Pi(x) = 1 - e^{-x}, \qquad \Gamma_\alpha(x) = 1 - (1+x)^{-\alpha},$$ $$\Pi_\gamma(x) = 1 - \exp\big(-\gamma\,[1 + x]\big), \qquad \Gamma_{\gamma,\alpha}(x) = 1 - \exp\big(-\gamma\,[1 + \alpha\log(1+x)]\big),$$

with $\alpha, \gamma > 0$ and $[a]$ the integer part of $a$. The first two are continuous; the last two are discrete, with jumps where $1 + x$, respectively $1 + \alpha\log(1+x)$, crosses an integer.

The lemmas of §1 use a second normalization, which shifts $X$ instead of $X - t$:

$$P\Big(\frac{X - b(t)}{a(t)} > x \;\Big|\; X > t\Big) = \min\Big(1, \frac{R(b(t) + x a(t))}{R(t)}\Big) \to S(x) \quad \text{weakly}, \tag{2–3}$$

where $1 - S$ is a nondegenerate distribution function. The two normalizations differ by $b(t) \mapsto b(t) + t$.

Formalization targets

Goal: Theorem 1 (p. 796)

If $F(x) < 1$ for all $x$, $a(t) > 0$, and

$$F_t\big(b(t) + x a(t)\big) \to G(x) \quad \text{weakly as } t \to \infty$$

for a nondegenerate distribution function $G$, then $G$ is of type $\Pi$, $\Pi_\gamma$, $\Gamma_\alpha$ or $\Gamma_{\gamma,\alpha}$ for some $\alpha, \gamma > 0$.

Milestones (§1, pp. 794–797)

1. Lemma 1. Under (2), for each continuity point $y$ of $S$ with $0 < S(y) < 1$ there are $A(y) \ge 1$ and $B(y)$ with

$$S(x)\,S(y) = S\big(B(y) + xA(y)\big) \quad \text{whenever } S(x) < 1. \tag{4}$$

2. Corollary. $S(x) > 0$ for all $x$.
3. Lemma 2. An unbounded non-increasing $H$ on $(x_0, \infty)$ that agrees with $S$ where $S < 1$ and solves $H(x)H(y) = H(B(y) + xA(y))$ agrees with $S$ where $H < 1$.
4. Case 1 of the proof: if $A(y) = 1$ for every $y$ in the set $Y$ of continuity points with $S(y) < 1$, then $1 - S$ is of type $\Pi$ or $\Pi_\gamma$.
5. The commutation identity of Case 2: $B(y_1) + A(y_1)B(y_2) = B(y_2) + A(y_2)B(y_1)$ for $y_1, y_2 \in Y$.
6. Case 2 of the proof: if $A(y) > 1$ for some $y \in Y$, then $1 - S$ is of type $\Gamma_\alpha$ or $\Gamma_{\gamma,\alpha}$.
7. The closing display: each of the four laws $G = 1 - S$ reproduces itself, $\min\big(1, S(B(t) + xA(t))/S(t)\big) = S(x)$ for every $t > 0$ and suitable $A(t) > 0$, $B(t)$; so all four types occur as limits.

Significance

Theorem 1 is to residual lives what the extremal types theorem of Fisher–Tippett and Gnedenko is to maxima: it reduces the asymptotic analysis of the residual life to a four-type list, and with it the question of domains of attraction (§§2–3 of the paper) becomes well posed. The continuous types $\Pi$ and $\Gamma_\alpha$ are, after a change of parameters, the exponential and Pareto members of the generalized Pareto family used to model exceedances over high thresholds; the discrete types $\Pi_\gamma$ and $\Gamma_{\gamma,\alpha}$ show that once a shift is allowed, lattice-like tails produce limits with atoms, a phenomenon that the scale-only Theorem 2 excludes.

The theorem has been proved since 1974. It is not formalized in any proof assistant known to us, and Mathlib has neither weak convergence of distribution functions in the form used here, nor types, nor the residual-life limit laws. A formal development provides these objects, the functional equation (4) and its solution on a half line, and a checked proof that the four-type list is exactly right — including the discrete types, which are easy to lose in an informal treatment.

Difficulty

The obvious approach is to pass to the limit in the identity relating the residual lives at ages $t$ and $b(t)$, obtaining a Cauchy-type functional equation for $S$, and to solve it. Two features block a direct application of the classical solution. First, the limit is a minimum with $1$, so convergence carries no information on the half line where $S = 1$: equation (4) holds only where $S(x) < 1$, and it does not determine $S$ by itself (the paper exhibits $S_0(x) = e^{-x}$ for $x \ge 1$, $S_0 = 1$ for $x < 1$, which satisfies (4) with $A = 1$, $B(y) = y$, yet $1 - S_0$ is of no limit type); Lemma 2 is needed to recover $S$ where $S = 1$. Second, the solutions of the shifted equation $\varphi(x) + \varphi(y) = \varphi(B(y) + x)$ for a monotone $\varphi$ are not only linear: a periodic perturbation is possible, and its analysis produces the discrete laws through the integer part. A proof that assumes continuity of $S$ misses $\Pi_\gamma$ and $\Gamma_{\gamma,\alpha}$.

Formalization scope

The law of $X$ is a probability measure $\mu$ on $\mathbb R$; $R(x) = \mu((x,\infty))$ and $F_t(x) = \mu((t, t+x])/\mu((t,\infty))$, with probabilities taken as real numbers. Every statement assumes $\mu((x,\infty)) > 0$ for all $x$, the paper's standing assumption; Lean's division by zero would otherwise make the conditional laws meaningless. The normalizations satisfy $a(t) > 0$ for all $t$ (only large $t$ matter). A limit distribution function is the distribution function of a probability measure $\nu$ on $\mathbb R$, so no mass escapes to $\pm\infty$; nondegenerate means $\nu$ is not a point mass; the limit tail is $S(x) = \nu((x,\infty))$, which is right-continuous. Weak convergence is convergence at the continuity points of the limit and nowhere else. The integer part is Int.floor. Each limit law is defined to be $0$ for $x < 0$.

Theorem 1 is stated in the normalization (1) of the theorem, the lemmas and cases in the normalization (2) of §1, as printed. Theorem 1 names its fourth family $\Gamma_{\alpha,\gamma}$; it is the introduction's $\Gamma_{\gamma,\alpha}$. In Lemma 2 the left endpoint $x_0$ may be $-\infty$ (Case 1 applies the lemma on the whole line), and the condition that $B(y) + xA(y)$ lies in $(x_0, \infty)$ for $x > x_0$ is written out, since (8) presupposes it. "A pair $(A(y), B(y))$ in Lemma 1" and "$A(y) = 1$", "$A(y) > 1$" are stated through pairs satisfying (4); the proof of Lemma 1 shows the pair is unique. The commutation identity is posed without the Case 2 assumption, which its derivation does not use. No hypothesis of the paper is dropped and none is added beyond these readings.

The statement is not trivialized by dropping nondegeneracy (a point-mass limit is always attainable), by requiring convergence at every $x$ (which would exclude the discrete types), or by defining the limit laws without the integer part (which would turn the discrete types into continuous ones); the formalization does none of these.

A complete development needs: the residual-life distribution function and the normed tail, weak convergence of distribution functions, types, the four limit laws; then monotone solutions of Cauchy-type functional equations on half lines, with their periodic perturbations. The functional-equation results and the closing-display computations are reusable beyond this mission, for instance for the scale-only Theorem 2 and for the domain-of-attraction results of §§2–3. Proofs of any milestone, of alternative routes to Theorem 1, and of the closing display for each family separately are welcome.

Selected references

• A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548 (the source of every statement of this mission: the published article).
• B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44 (1943), 423–453. https://doi.org/10.2307/1968974
• J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966.

Motivation

A discrete-event simulation of a queue, an inventory system or a communication network produces an output process $Y = \{Y(t) : t \ge 0\}$, and the quantity of interest is usually its steady-state mean $\mu$, the long-run average of $Y$. The natural estimator is the time average $\bar Y_n(1) = \frac1n\int_0^n Y(s)\,ds$ of a run of length $n$. A confidence interval for $\mu$ needs the scale of the fluctuations of $\bar Y_n(1)$, the variance constant $\sigma^2$ of the central limit theorem $n^{1/2}(\bar Y_n(1) - \mu) \Rightarrow \sigma N(0,1)$. For correlated simulation output, $\sigma^2$ is a sum of autocovariances at all lags and is hard to estimate consistently.

The method of standardized time series (STS), introduced by Schruben (Schruben 1983), avoids estimating $\sigma$: it divides the centred time average by a functional of the whole observed path that scales like $\sigma$, so that $\sigma$ cancels. Batch means, the standardized sum, and the standardized maximum are all of this form.

Glynn and Iglehart (Glynn & Iglehart 1990) put the method on a general footing. They require only a functional central limit theorem (FCLT) for $Y$, and they identify an abstract class $\mathcal M$ of standardizing functionals for which the cancellation works. This mission formalizes their basic limit theorem, Theorem 2.4, and the four claims of its proof. Two companion results of §2, display (2.2) and the weak law $\bar Y_n(1) \Rightarrow \mu$, are included as further targets.

Setting

$C[0,1]$ is the space of continuous real functions on $[0,1]$ with the uniform norm and its Borel $\sigma$-algebra; $k \in C[0,1]$ is the identity path $k(t) = t$. For $g : C[0,1] \to \mathbb R$, $D(g)$ is the discontinuity set of $g$, the set of $x$ at which $g$ is not continuous. A standard Brownian motion $B$ on a probability space $(\Omega, \mathcal F, P)$ is a random element of $C[0,1]$ with Gaussian finite-dimensional laws, $B(0) = 0$ and $\operatorname{Cov}(B(s), B(t)) = \min(s,t)$.

The output $Y$ is a real-valued measurable process. Its scaled partial-integral process and its centred, rescaled version are

$$\bar Y_n(t) = \frac1n\int_0^{nt} Y(s)\,ds, \qquad X_n(t) = n^{1/2}\bigl(\bar Y_n(t) - \mu t\bigr), \qquad 0 \le t \le 1 .$$

Assumption (2.1) asks for finite constants $\mu$ and $\sigma > 0$ such that $X_n \Rightarrow \sigma B$ as $n \to \infty$, weak convergence of random elements of $C[0,1]$. It holds for $\phi$-mixing, strongly mixing, associated and regenerative output processes, among others.

The class $\mathcal M$ of (2.3) consists of the measurable $g : C[0,1] \to \mathbb R$ with

1. $g(\alpha x) = \alpha g(x)$ for $\alpha > 0$ (positive homogeneity);
2. $g(x - \beta k) = g(x)$ for $\beta \in \mathbb R$ (invariance under subtracting a linear drift);
3. $P\{g(B) > 0\} = 1$;
4. $P\{B \in D(g)\} = 0$.

The proof uses the auxiliary map $h(x) = x(1)/g(x)$ for $g(x) \ne 0$ and $h(x) = 0$ otherwise.

Formalization targets

Goal: Theorem 2.4

For every $g \in \mathcal M$, under Assumption (2.1),

$$\frac{\bar Y_n(1) - \mu}{g(\bar Y_n)} \Rightarrow \frac{B(1)}{g(B)} \qquad (n \to \infty). \tag{2.5}$$

Milestones: the four claims of the proof (p. 3)

1. $P\{\sigma B \in D(h)\} = 0$.
2. $h(X_n) \Rightarrow h(\sigma B)$.
3. $h(\sigma B) = B(1)/g(B)$, by (2.3i).
4. $h(X_n) = (\bar Y_n(1) - \mu)/g(\bar Y_n)$ for $n \ge 1$, by (2.3i) and (2.3ii).

Companions

$$n^{1/2}\bigl(\bar Y_n(1) - \mu\bigr) \Rightarrow \sigma B(1) \tag{2.2}$$

and $\bar Y_n(1) \Rightarrow \mu$.

Significance

Theorem 2.4 is the limit theorem behind every STS confidence interval. The limit $B(1)/g(B)$ is free of $\sigma$ and of the output process, so with $z$ chosen so that $P\{-z \le B(1)/g(B) \le z\}$ equals a prescribed level, the interval $\bar Y_n(1) \pm z\,g(\bar Y_n)$ has asymptotically exact coverage for $\mu$. Each choice of $g \in \mathcal M$ gives a method: batch means with a fixed number of batches, Schruben's standardized sum, the standardized maximum. The later sections of the paper compare the lengths of these intervals with those of consistent-estimation intervals, and those comparisons start from Theorem 2.4.

The theorem is classical and its proof is short on paper. What is missing is a machine-checked version. The formal proof needs a continuous mapping theorem for maps that are continuous only almost surely at the limit, on the non-locally-compact space $C[0,1]$; Mathlib has the version for continuous maps only. A formal Theorem 2.4 also makes the class $\mathcal M$ and the C[0,1]-valued FCLT available for the other results of the paper, the expected-length lower bound and its non-attainment, which are formalized in sibling missions.

Difficulty

The algebra (milestones 3 and 4) is elementary. The difficulty is the continuous-mapping step. The map $h$ is in general not continuous: it can be discontinuous wherever $g$ is and wherever $g$ vanishes, and $g$ itself may be discontinuous on a large set (the standardized maximum is). The continuous mapping theorem for continuous maps does not apply. One needs its almost-sure form: if $X_n \Rightarrow X$ and $P\{X \in D(h)\} = 0$, then $h(X_n) \Rightarrow h(X)$. The class $\mathcal M$ controls $D(g)$ only along the law of $B$, and the hypothesis of the almost-sure theorem is about $D(h)$ at the scaled limit $\sigma B$, so the conditions (2.3iii) and (2.3iv) have to be transported from $B$ to $\sigma B$ and from $g$ to $h$.

Formalization scope

$C[0,1]$ is C(unitInterval, ℝ) with its sup-norm topology; the Borel MeasurableSpace instance is declared in the mission's definition file, since Mathlib has none at this commit. Weak convergence is Mathlib's TendstoInDistribution, for the $C[0,1]$-valued FCLT and for the real-valued conclusions. The standard Brownian motion is a measurable $C[0,1]$-valued map whose coordinates agree, for every $\omega$, with a process satisfying Mathlib's IsBrownianReal. $D(g)$ is the set of points where ContinuousAt g fails, and $P\{B \in D(g)\}$ is an outer measure, so no measurability of $D(g)$ is assumed.

$\bar Y_n$ is a $C[0,1]$-valued parameter pinned pointwise by $\bar Y_n(t) = \frac1n\int_0^{nt}Y(s)\,ds$, so it is determined by $Y$. Assumption (2.1) carries joint measurability of $Y$ and local integrability of each path; the second is implicit in the paper and makes $\bar Y_n$ defined. The index $n$ runs over $\mathbb N$, and milestone 4 assumes $n \ge 1$ because (2.3i) is applied with $\alpha = n^{1/2}$. Real division by zero returns $0$ in Lean, which agrees with the paper's convention for $h$; it matters only on events of probability zero in the limit. Condition (2.3iii) is printed "$P\{g(b) > 0\} = 1$" and is read as $P\{g(B) > 0\} = 1$.

Condition (2.3iv) is stated with the discontinuity set, not as continuity of $g$: requiring $g$ continuous everywhere would exclude the standardized maximum of Example 3.10 and would make the continuous-mapping step trivial. The goal assumes nothing about $h$, $D(h)$ or any mapping theorem; these appear only in the milestones.

Contributions welcome: the almost-sure continuous mapping theorem for TendstoInDistribution on a metric space (reusable well beyond this mission), the cone property of $D(g)$ under positive homogeneity, and evaluation at a point as a continuous map on $C[0,1]$. Mathlib does not yet construct a Brownian motion with continuous paths as a $C[0,1]$-valued random element, so the hypotheses cannot be instantiated inside Lean; this is a hypothesis on $B$, not a vacuity.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. https://doi.org/10.1287/moor.15.1.1
• L. Schruben, Confidence interval estimation using standardized time series, Operations Research 31(6):1090–1108, 1983. https://doi.org/10.1287/opre.31.6.1090
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968 (Theorem 5.1, the continuous mapping theorem).
• K. L. Chung, A Course in Probability Theory, 2nd ed., Academic Press, 1974 (p. 93, converging-together lemma).

Motivation

The cutting stock problem asks how to cut standard stock rolls of length $L$ into pieces of demanded lengths $l_1,\dots,l_m$ so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.

Setting

There are $m$ demanded lengths $l_1,\dots,l_m>0$ with linear programming prices $b_1,\dots,b_m\ge0$, and $k$ standard stock lengths $L_1,\dots,L_k$ with costs $c_1,\dots,c_k$. A column for $L_j$ is a vector $(\alpha)_m=(a_1,\dots,a_m)$ of nonnegative integers with $\sum_i l_ia_i\le L_j$. The knapsack problem (1) for $L_j$ is

$$\bar M_j=\max\Big\{\sum_{i=1}^m b_ia_i : a_i\in\mathbb Z_{\ge0},\ \sum_{i=1}^m l_ia_i\le L_j\Big\},$$

and the quantity to compute is $M_j=\max(c_j,\bar M_j)$: a column improves the linear program exactly when $\bar M_j>c_j$.

For a prefix $(\alpha)_s=(a_1,\dots,a_s)$ write $\lambda\cdot(\alpha)_s=\sum_{i\le s}l_ia_i$ and $\beta\cdot(\alpha)_s=\sum_{i\le s}b_ia_i$. Step (1) sorts the data, $b_1/l_1\ge\dots\ge b_m/l_m$ and $L_1>\dots>L_k$, and appends a slack item $a_{m+1}$ with $b_{m+1}=0$, $l_{m+1}=1$. The method then generates vectors in decreasing lexicographic order:

• Steps (2) and (7) fill the coefficients after a prefix greedily, $a_i=[(L-\text{used})/l_i]$, for $L=L_1$ at the start and $L=L_t$ later.
• Step (3) records $\beta\cdot(\alpha)_m$ as the new $M_j$ for each $j\ge t$ with $L_j\ge\lambda\cdot(\alpha)_m$ and $\beta\cdot(\alpha)_m>M_j$.
• Step (4) finds the last nonzero coefficient $a_s$.
• Step (5) lowers $a_s$ by one and looks for the smallest $j$ with $L_j\ge\lambda\cdot(\alpha)_s$ and $(L_j-\lambda\cdot(\alpha)_s)b_{s+1}>(M_j-\beta\cdot(\alpha)_s)l_{s+1}$. This is the bound obtained by relaxing the integrality of $a_{s+1}$.
• Step (6) backs up to the previous nonzero coefficient when no such $j$ exists, and stops when there is none.

In Lean the method is a transition system Step on states (a, s, t, M, phase). Reachable means reachable from the start state of Step (2).

Formalization targets

Goal: the method terminates and computes $M_1$

Under Step (1)'s ordering, with $l_i>0$ and $b_i\ge0$:

$$\text{every run is finite},\quad \text{a non-final state has a successor},\quad M_1^{\text{final}}=\max\big(c_1,\bar M_1\big),$$

and at the end every $M_j$ is $c_j$ or the price of a column for $L_j$, with $c_j\le M_j$. With one stock length ($k=1$) this is the paper's correctness claim in full: the method solves the knapsack problem (1).

Milestones

1. Steps (2)/(7): the greedy completion is the lexicographically largest extension of a prefix that fits the capacity.
2. Step (4): the lexicographic predecessor of a fitting vector extends $(\alpha^1)_s$.
3. The relaxation bound $\beta\cdot(\alpha')_m\le\beta\cdot(\alpha)_s+b_{s+1}(L-\lambda\cdot(\alpha)_s)/l_{s+1}$ for every fitting extension.
4. After the inequality of Step (5)'s test fails, no vector between $(\alpha)_s$ and the successor of Step (6) improves $M$.
5. The vectors tested in Step (3) strictly decrease lexicographically.
6. The invariant on entry to Step (3).
7. Identical prices: among lengths with equal prices only the shortest is needed (p. 869).

Significance

The goal certifies the pricing oracle of the Gilmore–Gomory column-generation method: the knapsack solver it calls returns the true optimum. The pricing step is exact only if that holds, and so is the conclusion "no improving column exists, the LP is solved". Milestones 1–4 are reusable on their own. They are the textbook ingredients of lexicographic and depth-first branch-and-bound for the integer knapsack: the greedy completion, the density-ordered LP bound, and the pruning rule.

The paper's argument is a short paragraph, "clear from the order in which the $m$-vectors are generated". Writing it out shows that the claim is false for several stock lengths as the steps are printed. With $m=1$, $l_1=b_1=1$, $L=(5,2)$ and $c=(0,0)$, the method tests $(5)$. The test of Step (5) at $(4)$ then fails for $j=2$ only because $4>L_2$, Step (6) stops, and the run ends with $M_2=0$ while the column $(2)$ has price 2. This mission therefore states what the printed algorithm does achieve. The result is the full claim for $k=1$ and for the longest stock length in general. A sorry-free Lean proof of the counterexample run accompanies the mission. No part of the method or its correctness has been formalized before, as far as a search of the platform shows.

Difficulty

The method skips large parts of the lexicographic order in three ways:

• Step (7) jumps to the greedy completion for $L_t$ rather than $L_1$.
• Step (6) jumps past every smaller value of $a_s$ once one test fails.
• Step (3) updates only $j\ge t$.

Each skip has to be justified by a bound that holds for every vector skipped, and the justifications interact. A skipped vector may fit a longer stock length but not $L_t$, and the bound for $L_1$ must cover exactly those vectors. The invariant that survives all three moves is not the naive "every vector above the current one has been examined": the vectors are not examined, only bounded. Termination needs the lexicographic decrease together with finiteness of the fitting vectors, and progress needs the reachability invariants $1\le s\le m$ and $a_s\ne0$ that make Step (5) meaningful.

Formalization scope

• Items are Fin m from 0. The paper's level $s$ is a natural number, and the prefix $(\alpha)_s$ is the coordinates with index < s. Stock lengths are Fin k, and $L_1$ is index 0. The slack item enters only through $b_{s+1}$ and $l_{s+1}$ at $s=m$. The lexicographic order is Mathlib's Pi.Lex, and $[x]$ is Nat.floor.

• $M_j=\max(c_j,\bar M_j)$ is the predicate IsKnapsackMax, never a real supremum, which would be 0 on an empty set. The algorithm's output is never defined as the maximum. The goal includes termination and progress, so its correctness clause is not vacuous. Every invariant is stated for reachable states only.

• The goal adds two disclosed hypotheses:

  • $l_i>0$: demanded lengths.
  • $b_i\ge0$: with a negative price the method is wrong, and the paper applies it to cutting-stock prices, which are nonnegative.

  Step (1) is a hypothesis on the data, not a step.

• The goal also makes these corrections:

  • The claim is narrowed. For every $j$ it states $c_j\le M_j$ and attainment, and the upper bound for $L_1$ only (see Significance).
  • The lexicographic order is repaired. The page's definition misses vectors that differ in their first coefficient.
  • Step (7) reads λ·(α)_m. The page's "satisfies $L_t\ge\lambda\cdot(\alpha)_s$" is read as $\lambda\cdot(\alpha)_m$.
  • Step (4) gets a stopping case. On the zero vector, where the page has no case, the method stops.
  • Milestone 4 is stated for the failed inequality, not for a failed test, because the failed test is what makes the page's successor claim false.

• Not formalized:

  • Step (3′), the variant computing $\max_j(M_j-c_j)$.
  • The record of patterns.
  • The dynamic-programming recursion and the timing estimates.

Contributions welcome: proofs of the milestones, and a corrected multi-length variant of the method with a proof that it computes every $M_j$.

Selected references

• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6) (1963), 863–888. https://doi.org/10.1287/opre.11.6.863
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6) (1961), 849–859. https://doi.org/10.1287/opre.9.6.849
• G. B. Dantzig, Discrete-variable extremum problems, Operations Research 5(2) (1957), 266–288. https://doi.org/10.1287/opre.5.2.266

Motivation

In the cutting stock problem, stock rolls of length $L$ are cut into pieces of lengths $l_1,\dots,l_m$ to fill orders. Part I of Gilmore and Gomory's work (Opns. Res. 9 (1961)) solved its linear programming relaxation by the simplex method with column generation: the columns (cutting patterns) are too many to list, so each simplex iteration finds an improving column by solving a knapsack problem. Part II (Opns. Res. 11 (1963)) extends the method in several directions. One of them, customer tolerances, lets the amount produced of each length lie in a range $[N_i',N_i'']$ instead of matching a fixed demand. Total roll usage then stops being a good measure of quality, because overproducing within the tolerance is free. The natural objective becomes the fraction of waste: total waste divided by total material cut. This objective is a ratio of two linear functions, not a linear one.

The paper's answer, on p. 882, is that the ordinary simplex method still works for such an objective. It moves from vertex to vertex, at each vertex asks whether some edge improves the objective, and stops when none does. Ratio objectives of this kind, called linear-fractional programs, were studied in the same years by Isbell and Marlow (1956), Martos (1960–61, in Hungarian; in English in 1964), Charnes and Cooper (1962) and Dinkelbach (1962; see also 1967). Gilmore and Gomory say that their method is closest to Martos's. They derive the edge test for the ratio and show that, for cutting stock, choosing the entering column is again a knapsack problem.

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb R^m$ and $c,d\in\mathbb R^n$. The linear-fractional program is

$$\text{minimize}\quad \zeta(x)=\frac{z_1(x)}{z_2(x)}=\frac{\sum_i c_ix_i}{\sum_i d_ix_i}\qquad\text{subject to}\quad Ax=b,\ x\ge 0 .$$

In the cutting stock instance (p. 881), column $j$ is either a cutting pattern $a_j\in\mathbb Z^m_{\ge0}$ with $\sum_ia_{ij}l_i\le L$ or a slack column $-e_i$. The right-hand side is $b_i=N_i'$. The numerator coefficient of a pattern is its waste $w_j=L-\sum_ia_{ij}l_i$ (eq. (4)), and $d_j=1$ on patterns and $0$ on slacks, so $\zeta$ is waste per roll cut. The paper drops the upper bounds $s_i\le N_i''-N_i'$ on the slacks from the discussion (p. 882), and so does this mission.

A basis is a set $B$ of $m$ column indices whose columns of $A$ are linearly independent. A basic feasible solution $\bar x$ with basis $B$ is a feasible point with $\bar x_k=0$ for every $k\notin B$. For a nonbasic $j\notin B$, the edge direction of $x_j$ is the vector $v$ with $Av=0$, $v_j=1$ and $v_k=0$ for the other nonbasic $k$. This is "the edge that would be traced out if $x_j$ were increased, but all other nonbasic variables kept zero" (p. 883). The quantity the simplex test inspects is the rate of change along the edge,

$$\frac{d\zeta}{dx_j}=\frac{d}{d\tau}\,\zeta(\bar x+\tau v)\Big|_{\tau=0}.$$

Formalization targets

Goal: the edge criterion (p. 882)

Assume $\sum_id_ix_i>0$ for every feasible $x$. Let $\bar x$ be a basic feasible solution with basis $B$, and suppose $d\zeta/dx_j\ge0$ for every $j\notin B$ and every edge direction of $x_j$. Then

$$\zeta(\bar x)\le\zeta(x)\qquad\text{for every } x\ge0 \text{ with } Ax=b .$$

Milestones (p. 882–883)

1. Monotonicity along lines. On an interval where the denominator does not vanish, $\tau\mapsto\zeta(x+\tau v)$ is strictly increasing, strictly decreasing or constant. Moreover $f'(\tau)\,D(\tau)^2$ is constant, where $D$ is the denominator.
2. Equation (5), first line.

$$\frac{d\zeta}{dx_j}=\frac{z_2\,(dz_1/dx_j)-z_1\,(dz_2/dx_j)}{z_2^2}.$$

3. The edge test. If $d\zeta/dx_j<0$, increasing $x_j$ strictly decreases $\zeta$ along any segment where the denominator does not vanish. Otherwise $\zeta$ does not decrease anywhere on that segment.
4. Column choice is a knapsack problem. With $k=Lz_2-z_1$ and $\bar\Pi_i=-(z_1\Pi^2_i-z_2\Pi^1_i-z_2l_i)$, the numerator of $d\zeta/dx_j$ for pattern $a$ equals $k-\sum_i\bar\Pi_ia_i$. Hence, for $z_2\ne0$, the most negative $d\zeta/dx_j$ is attained exactly by the patterns maximizing $\sum_i\bar\Pi_ia_i$ subject to $\sum_ia_il_i\le L$.

Significance

The result. The edge criterion turns a nonconvex problem into one the simplex method solves. A ratio of linear functions is neither convex nor concave, so a point where no feasible direction improves the objective locally is not obviously a global minimum. The criterion says that, on a polyhedron where the denominator keeps its sign, this local test at a vertex certifies global optimality, exactly as for a linear objective. It underlies the convergence of Martos's method and of every simplex-type algorithm for linear-fractional programming. Together with milestone 4, it is what makes column generation with a knapsack pricing step applicable to the waste-fraction objective of cutting stock.

Formalizing it. The result is classical and proved; no machine-checked version is known to exist. The published platform items closest to it are Derman's Charnes–Cooper transformation of a linear-fractional program into a linear program and Matoušek's reduced-cost optimality criterion for a linear objective. Neither states an edge criterion for a ratio. A formal proof here also settles the paper's own imprecisions (see below), and yields reusable lemmas about ratios of affine functions along lines.

Difficulty

The obvious argument does not reach the goal. Along any single segment the objective is monotone (milestone 1), so a nonnegative derivative at $\bar x$ in the direction of the segment would settle it. But the test at $\bar x$ inspects only the $n-m$ edge directions, while a feasible point $x$ lies in the direction $x-\bar x$, which is in general not an edge. Monotonicity along each edge says nothing directly about other directions, and $\zeta$ is neither convex nor concave, so local optimality along a few lines does not by itself transfer to the whole polyhedron. The step that has to be supplied is the passage from the edges to all feasible directions at a basic solution. It fails without the basis: at a feasible point that is not basic, or with linearly dependent columns, the edge directions need not reach every feasible point. At a degenerate vertex some edge directions leave the feasible set at once, and a test restricted to the feasible edges does not certify optimality.

Formalization scope

The feasible set and the objective are the published definitions DermanSeqDecisions.LinProg.IsFeasible11 ($x\ge0$, $Ax=b$) and DermanSeqDecisions.LinProg.fracObj ($(\sum c_ix_i)/(\sum d_ix_i)$). The basis is the published MatousekLP.BFS.IsBasis. Indices are 0-based. A mission definition adds the basic feasible solution and the relational edge direction. The edge direction is given by its defining equations, not through a basis inverse, and is not required to be feasible.

Committed conventions and disclosed choices:

• The goal is stated for minimization, the paper's problem; the paper's sentence says "maximize", which is the same statement for $-c$.
• "In a domain where the denominator does not vanish" is the hypothesis $\sum_id_ix_i>0$ for every feasible $x$ (the paper's footnote: $\sum_jx_j>0$). It is not required on all of $\mathbb R^n$, where it would be unsatisfiable for the cutting stock $d$.
• The derivative in the test is Mathlib's deriv of $\tau\mapsto\zeta(\bar x+\tau v)$ at $0$: the actual rate of change, not a formula assumed to equal it.
• The page says that along a line the derivative "will have the same value". This is false when the denominator varies along the line. Milestone 1 states the correct version: the derivative times the squared denominator is constant, so the sign is constant.
• In the formula after substituting (4), the page prints the coefficient $-l_i$ where $-z_2l_i$ is meant. Milestone 4 uses the corrected coefficient.
• The slack upper bounds are dropped, as on p. 882.

The following would trivialize the goal and are excluded: an edge hypothesis over all directions $v$ instead of the edge directions, which turns the goal into quasi-convexity along segments; an edge hypothesis stated as the global inequality; a positivity hypothesis on the denominator over all of $\mathbb R^n$; and dropping the basis, under which the goal is false.

The development needs elementary real calculus (derivatives of quotients, monotonicity from the sign of the derivative) and the linear algebra of a basis (existence, uniqueness and spanning of the edge directions). The lemmas about ratios of affine functions along lines and about edge directions of a basis are reusable for any simplex-type method. Contributions of proofs of the milestones, and of auxiliary lemmas on edge directions, are welcome.

Selected references

• P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6), 863–888, 1963. https://doi.org/10.1287/opre.11.6.863
• P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting stock problem, Operations Research 9(6), 849–859, 1961. https://doi.org/10.1287/opre.9.6.849
• B. Martos, Hyperbolic programming, Naval Research Logistics Quarterly 11(2), 135–155, 1964. https://doi.org/10.1002/nav.3800110204
• A. Charnes and W. W. Cooper, Programming with linear fractional functionals, Naval Research Logistics Quarterly 9(3–4), 181–186, 1962. https://doi.org/10.1002/nav.3800090303
• W. Dinkelbach, Die Maximierung eines Quotienten zweier linearer Funktionen unter linearen Nebenbedingungen, Zeitschrift für Wahrscheinlichkeitstheorie 1, 141–145, 1962 (cited by the paper as [11]).
• W. Dinkelbach, On nonlinear fractional programming, Management Science 13(7), 492–498, 1967. https://doi.org/10.1287/mnsc.13.7.492
• J. R. Isbell and W. H. Marlow, Attrition games, Naval Research Logistics Quarterly 3, 71–94, 1956 (cited by the paper as [9]).