Optimization

Motivation

Many problems in scientific computing and statistics ask for a solution of a linear system $Ax\approx b$ that uses as few unknowns as possible. In statistics this is subset selection (Golub and Van Loan, Matrix Computations, 1983). In coding theory over binary matrices it is the minimum weight solution problem (Gallager, 1968). Natarajan's own motivation was radial basis interpolation (Hardy, 1988). There the coefficients of the interpolant solve a square nonsingular linear system (Michelli, 1986). Few nonzero coefficients make the interpolant cheap to evaluate and, by Occam's razor, less prone to fitting noise.

Natarajan's paper (SIAM J. Comput. 24 (1995) 227–234) makes two contributions. First, finding the sparsest approximate solution over the reals is NP-hard (Theorem 1, the subject of the companion mission). Second, the obvious greedy heuristic, a QR factorization whose column pivots are chosen by their correlation with the right-hand side, is provably good (Theorem 2). This mission formalizes Theorem 2. The greedy method is known today as orthogonal least squares (OLS), a variant of orthogonal matching pursuit. Natarajan's bound is among the earliest worst-case guarantees for this family of algorithms and is widely cited in the sparse approximation and compressed sensing literature.

Setting

Let $A\in\mathbb R^{m\times n}$ have columns $a_1,\dots,a_n$, let $b\in\mathbb R^m$ and $\varepsilon>0$. Write $\|\cdot\|_2$ for the Euclidean norm and $\|x\|_0$ for the number of nonzero entries of $x$. The sparse approximate solution problem asks for $x$ with $\|Ax-b\|_2\le\varepsilon$ and $\|x\|_0$ minimal. Define

$$\operatorname{Opt}(\delta)=\min\{\|x\|_0 : \|Ax-b\|_2\le\delta\}.$$

Let $\mathbf A$ be $A$ with every column divided by its Euclidean norm. Let $\mathbf A^+$ be its Moore–Penrose pseudo-inverse, the unique matrix $P$ with $\mathbf AP\mathbf A=\mathbf A$, $P\mathbf AP=P$ and $\mathbf AP$, $P\mathbf A$ symmetric. Let $\|\mathbf A^+\|_2$ be its spectral norm, the $\ell_2\to\ell_2$ operator norm.

Algorithm Greedy keeps a working matrix $A^{(r)}$ with columns $a^{(r)}_j$, a working vector $b^{(r)}$ and a set $\tau$ of chosen indices. It starts from $A^{(0)}=\mathbf A$, $b^{(0)}=b$, $\tau=\emptyset$. While $\|b^{(r)}\|_2>\varepsilon$, it chooses an index $k\notin\tau$ that maximizes $|a_k^{(r)T}b^{(r)}|$ and replaces $b^{(r)}$ by its projection onto the orthogonal complement of $a^{(r)}_k$. It adds $k$ to $\tau$ and replaces every column outside $\tau$ by its normalized projection onto that complement. If every correlation $a_j^{(r)T}b^{(r)}$ vanishes, the algorithm stops ("no solution exists"). A final solution phase solves the linear system $Bx=b^{(0)}-b^{(r)}$ in the chosen columns $B$ of $A$. The number of nonzero entries of the output is therefore at most the number $t$ of selection iterations.

Formalization targets

Goal: Theorem 2, for $A$ with linearly independent columns

If the columns of $A$ are linearly independent and some $x$ satisfies $\|Ax-b\|_2\le\varepsilon/2$, then every run of the selection phase, with any tie-breaking, performs

$$t\le\Big\lceil 18\,\operatorname{Opt}(\varepsilon/2)\,\|\mathbf A^+\|_2^2\,\ln\frac{\|b\|_2}{\varepsilon}\Big\rceil$$

iterations. The paper prints the theorem without the independence hypothesis. The hypothesis is needed (see Formalization scope).

Milestones

The proof on pp. 230–233 passes through the following statements, in order:

1. (12): some column satisfies $|a_j^{(r)T}b^{(r)}|\ge\|b^{(r)}\|_2^2/(2\sqrt{N^{(r)}}\|u^{(r)}\|_2)$. Here $u^{(r)}$ is a sparsest vector with $\|A^{(r)}u^{(r)}-b^{(r)}\|_2\le\varepsilon/2$ and $N^{(r)}=\|u^{(r)}\|_0$.
2. (18): $\|b^{(r+1)}\|_2^2\le(1-1/\rho)\|b^{(r)}\|_2^2$ whenever $\rho\ge 4N^{(r)}\|u^{(r)}\|_2^2/\|b^{(r)}\|_2^2$.
3. Lemma 1: $t\le\lceil2\rho\ln(\|b\|_2/\varepsilon)\rceil$ for any such $\rho$ valid at every iteration.
4. Lemma 3: $N^{(r+1)}\le N^{(r)}\le N^{(0)}$.
5. $N^{(0)}=\operatorname{Opt}(\varepsilon/2)$.
6. The columns of $\mathbf A$ indexed by the support $\sigma$ of $u^{(r)}$ and by the chosen set $\tau$ are linearly independent, and $\sigma\cap\tau=\emptyset$.
7. (31): $\|u^{(r)}\|_2\le\frac32\|Z^+\|_2\|b^{(r)}\|_2$ for the matrix $Z$ of those columns.
8. The singular-value comparison $\|Z^+\|_2\le\|M^+\|_2$ for a column submatrix $Z$ of a matrix $M$ with independent columns.
9. Lemma 2: $\|u^{(r)}\|_2\le\frac32\|\mathbf A^+\|_2\|b^{(r)}\|_2$, for $A$ with independent columns.

Items 1–7 hold for every matrix $A$. Items 8, 9 and the goal carry the independence hypothesis.

Significance

Theorem 2 is a bicriteria approximation guarantee for an NP-hard problem. The greedy output meets the error $\varepsilon$ with at most a factor $18\|\mathbf A^+\|_2^2\ln(\|b\|_2/\varepsilon)$ more nonzeros than the best solution at error $\varepsilon/2$. The factor depends only on the conditioning of the normalized matrix and logarithmically on the required accuracy. Its structure follows Johnson's analysis of the greedy set cover algorithm (1974): a potential decreases by a constant factor per step, which gives a logarithmic number of steps. The intermediate facts (12), (18) and Lemma 1 are the template of many later analyses of matching pursuit and OLS.

The result is proved on paper, with a gap. The last step of the proof of Lemma 2 compares singular values of a submatrix with those of $\mathbf A$, and this comparison holds only when $\mathbf A$ has full column rank. For general $A$, Theorem 2 and Lemma 2 are false as printed. The formalization produces a machine-checked proof of the corrected theorem and pins down exactly where the hypothesis enters. The hypothesis-free statements (12), (18), Lemma 1, Lemma 3 and (31) form reusable infrastructure for greedy sparse approximation. No existing formalization of this algorithm or of its guarantee, in Lean or elsewhere, was found for this mission.

Difficulty

Each step of the proof is short, but the objects are defined by an iteration. The columns $a^{(r)}_j$ are repeatedly projected and renormalized, and the columns already chosen are left untouched. Every claim about iteration $r$ therefore needs invariants: chosen columns are orthonormal and orthogonal to $b^{(r)}$, and the remaining columns are normalized projections of the original ones onto the orthogonal complement of the chosen ones. A proof has to establish these by induction before any lemma can be applied. The sparsest vector $u^{(r)}$ is defined by minimality, so Lemma 3 and the linear-independence claim are exchange arguments on supports rather than computations. Finally, the passage from (31) to Lemma 2 needs a quantitative fact about pseudo-inverses of column submatrices. Mathlib has neither the Moore–Penrose inverse of a rectangular matrix nor its norm as a reciprocal singular value.

A naive attempt to bound $\|u^{(r)}\|_2$ directly by $\|\mathbf A^+\|_2\|A^{(r)}u^{(r)}\|_2$ fails: $u^{(r)}$ multiplies the projected columns $A^{(r)}$, not $\mathbf A$, and different sparsest solutions can have different norms.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m), so every $\|\cdot\|_2$ is the Euclidean norm. The only $\|\cdot\|_\infty$ is the maximum of $|a_j^{(r)T}b^{(r)}|$, which is written out explicitly. The algorithm is a recursion greedyState A b k r in the sequence of choices k : ℕ → Fin n. A run of $t$ iterations (IsGreedyRun) requires, at each $r<t$: the strict while-condition $\|b^{(r)}\|_2>\varepsilon$, an unchosen index, a nonzero correlation, and maximality over the unchosen columns. The residual and the columns are computed, never assumed. Normalization sends $0$ to $0$, so a column lying in the span of the chosen ones stays zero and is never chosen. $\operatorname{Opt}$ is an infimum over ℕ, and the goal assumes that some $x$ has $\|Ax-b\|_2\le\varepsilon/2$, since otherwise the infimum would be $0$. The ceiling is the natural-number ceiling. It agrees with the printed one whenever the loop runs at least once, because then $\|b\|_2>\varepsilon$. The pseudo-inverse is any matrix satisfying the four Penrose equations. It is never defined as $(\mathbf A^T\mathbf A)^{-1}\mathbf A^T$, which would hide the rank assumption.

Added hypothesis. The goal, Lemma 2 and the singular-value step assume that the columns of $A$ are linearly independent, which forces $n\le m$. Without it, Theorem 2 fails. Take $m=2$, $n=200$, columns $(\cos\theta_j,\sin\theta_j)$ and $(\sin\theta_j,\cos\theta_j)$ for 100 distinct $\theta_j\in[0.001,0.01]$, $b=\sqrt2(1,1)$ and $\varepsilon=1$. Then $\operatorname{Opt}(1/2)=2$ and the bound evaluates to $1$, but Greedy selects two columns. Lemma 2 fails for $\mathbf A=[e_1,e_2,(e_1+e_2)/\sqrt2]$ and $b=\beta(-1,1)/\sqrt2$. The paper's motivating interpolation systems are square and nonsingular, so they satisfy the hypothesis. A hypothesis-free goal would replace $\|\mathbf A^+\|_2$ by the largest $\|Z^+\|_2$ over linearly independent column subsets $Z$ of $\mathbf A$, which is what (31) gives. That quantity is not printed in the paper, so it is not the goal here.

A statement in which the iterates are free sequences constrained by hypotheses, the greedy choice is dropped, or $\operatorname{Opt}$ is taken over an empty set would be trivially true or would not describe this algorithm. The encoding above rules these out.

A complete development needs Gram–Schmidt-type invariants of the iteration, exchange arguments for sparsest solutions, and the Moore–Penrose inverse with its spectral norm. The last of these is reusable well beyond this mission. Contributions of any milestone, of the general Penrose-inverse facts, or of alternative proofs are welcome.

Selected references

• B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM J. Comput. 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
• G. H. Golub and C. F. Van Loan, Matrix Computations, Johns Hopkins University Press, 1983.
• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9:256–278, 1974. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. Penrose, A generalized inverse for matrices, Proc. Cambridge Philos. Soc. 51:406–413, 1955. https://doi.org/10.1017/S0305004100030401

Motivation

Maximum satisfiability asks for a truth assignment satisfying as many clauses of a propositional formula as possible. The paper notes that the restriction $MS(k)$, in which every clause has at least $k$ literals, is polynomial complete for every $k \ge 1$, so exact optimization is out of reach in general and one asks instead how close a fast algorithm is guaranteed to come. David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 256–278) set up a framework for exactly this question — optimization problems, nondeterministic approximation algorithms, and the worst-case ratio between the optimum and the algorithm's output — and applied it to subset-sum, maximum satisfiability, set covering, graph coloring and maximum clique. It is one of the founding papers of the theory of approximation algorithms.

Section 4 of the paper treats maximum satisfiability with two algorithms. This mission covers the first, a greedy literal-selection rule called B1, and its exact worst-case ratio (Theorem 2). A companion mission covers the weighted algorithm B2 (Theorem 3).

Timeline, for orientation:

• 1971–1972: Cook and Karp establish NP-completeness of satisfiability and of many combinatorial problems.
• 1974: Johnson proves that B1 has worst-case ratio exactly $(k+1)/k$ on $MS(k)$ and that the weighted algorithm B2 achieves $2^k/(2^k-1)$ (Theorems 2 and 3).
• 1990s: semidefinite and LP-based algorithms (Goemans–Williamson, SIAM J. Discrete Math. 1994) improve the constants for general MAX-SAT.

Setting

Let $L = \bigcup_{i>0}\{x_i, \bar x_i\}$ be the set of literals; the complement of $x_i$ is $\bar x_i$ and conversely. A clause is a finite set $C \subseteq L$. A truth assignment is a set $T \subseteq L$ containing no complementary pair $\{x_i, \bar x_i\}$; it may leave variables unassigned. $T$ satisfies $C$ if $C \cap T \ne \emptyset$.

An input is a finite set $S$ of clauses. Its feasible solutions are the subsets $S' \subseteq S$ satisfied by a single truth assignment, measured by $|S'|$, and the optimum is

$$S^* = \max\{|S'| : S' \subseteq S,\ \text{some truth assignment satisfies every } C \in S'\}.$$

The subproblem $MS(k)$ admits only inputs whose clauses each contain at least $k$ distinct literals.

Algorithm B1 keeps four variables: SUB (clauses already satisfied), LEFT (clauses not yet satisfied), TRUE (literals made true) and LIT (literals still available). It starts with SUB $=$ TRUE $= \emptyset$, LEFT $= S$, LIT $= L$. While some literal of LIT occurs in a clause of LEFT, it picks a literal $y \in$ LIT contained in the most clauses of LEFT, moves those clauses $YT$ from LEFT to SUB, adds $y$ to TRUE, and removes $y$ and $\bar y$ from LIT. When no literal of LIT occurs in LEFT it returns SUB.

The choice of $y$ is not determined when several literals tie. Following the paper's framework, every output reachable by some sequence of admissible choices is choosable, and the performance of B1 on $S$ is the smallest $|X|$ over choosable outputs $X$. The worst-case ratio on inputs of size at most $n$ is

$$R[B1, MS(k)](n) = \max\{S^*/B1(S) : S \in MS(k),\ |S| \le n\}.$$

Formalization targets

Goal: Theorem 2 (p. 262)

For all $k \ge 1$,

$$R[B1, MS(k)](n) \le \frac{k+1}{k}\quad\text{for all } n > 0,$$

with equality for all sufficiently large $n$. In the size-free form used here: every choosable output $X$ on every $S \in MS(k)$ satisfies $k\,S^* \le (k+1)\,|X|$, and for every $k \ge 1$ some $S \in MS(k)$ has a choosable $X$ with $|X| > 0$ and $k\,S^* = (k+1)\,|X|$.

Milestones (from the proof of Theorem 2, pp. 262–263)

1. In each iteration, the number of clauses saved (added to SUB) is at least the number of clauses remaining in LEFT that are wounded (lose a literal from LIT without being satisfied).
2. When B1 halts, every clause left in LEFT is dead: each of its literals has had its complement made true.
3. When B1 halts on an input of $MS(k)$, $|\mathrm{SUB}| \ge k\,|\mathrm{LEFT}|$, and SUB and LEFT partition $S$.
4. On the four-clause input $\{\{x_1,x_2,x_3\},\{\bar x_1,x_4,x_5\},\{\bar x_2,x_6,x_7\},\{\bar x_3,x_8,x_9\}\}$ of $MS(3)$, $S^* = 4$ while B1 may return three clauses.

Significance

The bound is stronger than a ratio: milestone 3 shows that B1 always satisfies at least $\tfrac{k}{k+1}|S|$ clauses, whatever the optimum. The tightness half shows that this simple greedy rule cannot be analysed any better, which is what motivated the weighted algorithm B2 of the same section, with ratio $2^k/(2^k-1)$. The pair of theorems is an early instance of a now standard pattern: a potential-style counting argument for an upper bound, and an adversarial tie-breaking instance for the matching lower bound.

The result is proved in the paper; it has not, to our knowledge, been machine-checked. This mission produces a formal model of Johnson's framework for a maximization problem with a nondeterministic algorithm, a formal proof of the upper bound through the "saved versus wounded" accounting, and explicit tightness instances for every $k \ge 1$. The paper spells out only $k = 3$ and states that "similar examples can be constructed for any other $k > 0$"; the formal goal requires them for all $k$.

Difficulty

The upper bound needs an invariant over entire runs, not over a single step: a clause wounded in one iteration may be saved in a later one, so wounds and saves must be tallied globally, and the count of wounds received by a clause that ends in LEFT must be matched with its number of literals. That matching relies on the facts that B1 never makes both a literal and its complement true and that a clause containing a true literal has already left LEFT. Clauses containing both $x_i$ and $\bar x_i$ are allowed and have to be handled.

The lower bound cannot be obtained from a fixed tie-breaking rule: the attaining run chooses negative literals whose count merely ties the maximum. For general $k$ the instance has to be built so that every literal occurs in few enough clauses that the adversarial choice is admissible at every step; at $k = 1$ the paper's pattern degenerates and needs adjusting.

Formalization scope

• A literal is a pair (variable index in $\mathbb N$, sign); a clause is a Finset of literals; an input is a Finset of clauses, so duplicate clauses are not allowed, as on the page. Tautological clauses are allowed.
• A truth assignment is a Set of literals without a complementary pair (partial, as in the paper). $S^*$ is the maximum of $|S'|$ over the finite nonempty family of satisfiable subsets, taken with Finset.sup'.
• B1 is a nondeterministic run relation: a state holds SUB, LEFT, TRUE and the set of decided variables (LIT is its complement, since $L$ is infinite); one step chooses any literal of LIT, of either sign, with maximum count; "choosable" is reachability of a halting state with the given SUB. No tie-break is fixed. A formalization that picks a variable and then its better sign, or that resolves ties deterministically, is a different algorithm and would make the tightness half false.
• The ratio $R[B1, MS(k)](n)$, whose problem size is left unspecified in the paper, is replaced by its size-free equivalent, and ratios are written multiplicatively in $\mathbb N$: $k\,S^* \le (k+1)|X|$. The tightness half requires $|X| > 0$, so the empty input cannot witness it.
• The running time $O(n \log n)$ is not stated.

Welcome contributions: proofs of the milestones, the invariants of reachable B1 states (SUB and LEFT partition $S$; TRUE is consistent and exactly covers the decided variables; no clause of LEFT meets TRUE), and the family of tightness instances for general $k$. The run-relation encoding of choosable outputs is reusable for the other algorithms of the paper.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• M. X. Goemans and D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM Journal on Discrete Mathematics 7 (1994), 656–666. https://doi.org/10.1137/S0895480192243516

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.

Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity $b$ so as to fill it as much as possible. For this problem the paper gives a family of algorithms $A_k$, one for each $k \ge 1$, whose guaranteed ratio $(k+1)/k$ tends to $1$. It is one of the first examples of what is now called a polynomial-time approximation scheme: for every $\epsilon > 0$ there is a polynomial-time algorithm within a factor $1 + \epsilon$ of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.

This mission formalizes Theorem 1 of the paper, the performance guarantee of $A_k$ together with its tightness.

Setting

An input $\langle T, s, b\rangle$ of SUBSET-SUM is a finite set $T$, a positive rational size $s(x)$ for every $x \in T$, and a positive rational bound $b$. An approximate solution is a subset $T' \subseteq T$ with $m(T') \le b$, where the measure is $m(T') = \sum_{x \in T'} s(x)$. The problem is a maximization problem with optimal measure

$$\langle T, s, b\rangle^* = \max\{\, m(T') : T' \subseteq T,\ m(T') \le b \,\}.$$

Fix $k \ge 1$ and call $x$ big if $s(x) > b/(k+1)$ and small otherwise. Algorithm $A_k$ keeps a set $\mathrm{SUB}$, its measure $\mathrm{SUM}$, and the remaining elements $\mathrm{LEFT}$:

1. $\mathrm{SUB}$ is a subset of the big elements whose measure is as large as possible without exceeding $b$; $\mathrm{SUM} = m(\mathrm{SUB})$ and $\mathrm{LEFT} = T \setminus \mathrm{SUB}$.
2. If $s(x) + \mathrm{SUM} > b$ for every $x \in \mathrm{LEFT}$, return $\mathrm{SUB}$.
3. Otherwise pick $y \in \mathrm{LEFT}$ with $s(y) + \mathrm{SUM}$ as large as possible without exceeding $b$, move it from $\mathrm{LEFT}$ to $\mathrm{SUB}$, add $s(y)$ to $\mathrm{SUM}$, and return to step 2.

Steps 1 and 3 may have ties. Following the paper, a set $T_1$ is choosable by $A_k$ if some resolution of all ties produces it, and the performance $A_k(u)$ on input $u$ is the smallest measure of a choosable output. The ratio is $r(A_k, u) = u^*/A_k(u) \ge 1$, and $R[A_k](n)$ is its maximum over inputs of size at most $n$.

Formalization targets

Goal: Theorem 1 (p. 260)

For $k \ge 1$ and $n > 0$,

$$R[A_k](n) \le \frac{k+1}{k}, \qquad \lim_{n \to \infty} R[A_k](n) = \frac{k+1}{k}.$$

Formally, for every $k \ge 1$: every choosable output $T_1$ of every input satisfies $k\,\langle T,s,b\rangle^* \le (k+1)\,m(T_1)$; and for every $\delta > 0$ some input has a choosable output $T_1$ with $m(T_1) > 0$ and $\langle T,s,b\rangle^* > \big(\tfrac{k+1}{k} - \delta\big)\,m(T_1)$.

Milestones

1. For $T_1$ choosable and $T_0$ any approximate solution, $m(T_1^{\mathrm{BIG}}) \ge m(T_0^{\mathrm{BIG}})$ (p. 260).
2. If a small $x \in T$ is not in a choosable $T_1$, then $s(x) + m(T_1) > b$, hence $m(T_1) > kb/(k+1) \ge \tfrac{k}{k+1}\langle T,s,b\rangle^*$ (p. 261).
3. The stronger dichotomy: $m(T_1) = \langle T,s,b\rangle^*$ or $m(T_1) \ge \tfrac{k}{k+1}\,b$ (p. 260).
4. The lower-bound input $T = \{a_1,\dots,a_{k+2}\}$, $s(a_1) = 1+\varepsilon$, $s(a_i) = 1$ otherwise, $b = k+1$: its optimum is $k+1$, some output is choosable, and every choosable output has measure $k + \varepsilon$ (p. 261).

Significance

Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above $1$, in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms $A_k$ are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of $A_k$ itself cannot be sharpened.

The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly $(k+1)/k$. The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.

Difficulty

The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing $A_k$ as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as $\mathrm{SUM}$ always equalling $m(\mathrm{SUB})$ or which elements can enter $\mathrm{SUB}$ after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general $k$: exactly $k-1$ unit elements are added after $a_1$, and this must be shown for every choosable run, not only for one.

Formalization scope

• Numbers. Sizes and the bound are rationals (ℚ), as in the paper; sizes are required to be positive on $T$ and $b > 0$. The index $k$ is a natural number with $1 \le k$ as a hypothesis; $b/(k+1)$ is rational division, and "big" is the strict inequality $s(x) > b/(k+1)$.
• Optimum. opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains $\emptyset$; it is $0$ when no element fits.
• Run relation. Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning $T_1$. Every "closest to, without exceeding" is an existential choice among all maximizers.
• Size-free restatement. The paper's input size $|u|$ ("in some standard notation") is never fixed, so the goal quantifies over all inputs instead of over sizes. The upper bound for all choosable outputs is equivalent to $R[A_k](n) \le (k+1)/k$ for all $n$; since $R[A_k]$ is nondecreasing, the limit claim is equivalent to the supremum of the ratio over all inputs being $(k+1)/k$, which is the second part.
• Multiplicative ratios. No ratio is written as a division, so an output of measure $0$ cannot satisfy a bound vacuously; the lower-bound part requires $m(T_1) > 0$. The value $(k+1)/k$ is not claimed to be attained: the paper's family has ratio $(k+1)/(k+\varepsilon)$.
• Lower-bound input. A def on Fin (k + 2) exactly as on the page, with $0 < \varepsilon < 1$ (the page leaves the range implicit; $\varepsilon < 1$ keeps $a_1$ the only big element that fits when $k = 1$).
• Ruled out. A formalization with a deterministic tie-break, with a bound of the form $\mathrm{opt}/m \le c$ in a field where $x/0 = 0$, or with tightness for a single fixed $k$ would be trivial or weaker; none of these is the target.

Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ($O(n^k)$ for step 1) and Sahni's knapsack extension are not part of the mission.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• S. Sahni, Approximate algorithms for the 0/1 knapsack problem, Journal of the ACM 22 (1975) 115–124. https://doi.org/10.1145/321864.321873
• O. H. Ibarra, C. E. Kim, Fast approximation algorithms for the knapsack and sum of subset problems, Journal of the ACM 22 (1975) 463–468. https://doi.org/10.1145/321906.321909
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

A single machine must process a set of jobs, each with a processing time and a due-date, and a job that finishes after its due-date is late. Counting late jobs is the natural objective when a late order is simply lost, whatever its lateness. In the three-field notation of scheduling theory this is the problem $1\,\|\,\sum U_j$, and it is one of the few single-machine problems with a due-date objective that a simple greedy rule solves exactly.

J. Michael Moore gave that rule in 1968 (Management Science 15(1):102–109). The only exact method previously available was the Held–Karp dynamic program, which is exponential in the number of jobs. Moore's algorithm is two sorts plus at most $n(n+1)/2$ additions and comparisons. The rule, and the variant from the paper's Author's Supplement (credited to T. J. Hodgson and today called the Moore–Hodgson algorithm), is in every scheduling textbook, for example Brucker, Scheduling Algorithms, Ch. 4, and is the base case of later work on weighted and release-date variants.

Timeline:

• 1955: J. R. Jackson shows that a job set can be scheduled with no late job if and only if the earliest-due-date order has none (Management Science Research Project report 43, UCLA).
• 1968: Moore publishes the algorithm and its proof of optimality, with Hodgson's variant stated without proof.
• 1970s onward: the weighted version $1\,\|\,\sum w_jU_j$ is shown NP-hard (Karp 1972, via knapsack), and $1\,|\,r_j\,|\,\sum U_j$ likewise (Lenstra, Rinnooy Kan and Brucker 1977), so Moore's greedy rule does not extend to them.

Setting

A finite set $J$ of jobs is given. Job $j$ has a processing time $t_j \ge 0$ and a due-date $D_j$, and the paper assumes $t_j \le D_j$ for every job (a job that cannot finish on time even if started at time $0$ is removed beforehand). The machine starts at time $0$ and processes the jobs one after another, without idle time or preemption.

A schedule $S$ of $J$ is an ordering $(J_{i_1},\dots,J_{i_n})$ of all jobs of $J$. The job in position $k$ completes at $C_{i_k} = t_{i_1} + \dots + t_{i_k}$. The late set is $L = \{J_i : C_i > D_i\}$ and the early set is $E = \{J_i : C_i \le D_i\}$. A schedule is optimal if no schedule of $J$ has fewer late jobs. $A$ and $R$ denote the early and late jobs of $S$, each kept in their order in $S$.

Moore's algorithm works on a current sequence and a list of rejected jobs.

• Step 1: order the jobs by non-decreasing processing time (the shortest processing time rule).
• Step 2: find the first late job $J_{i_q}$ of the current sequence. If there is none, stop.
• Step 3: re-order $J_{i_1},\dots,J_{i_q}$ by non-decreasing due-date. If all of them are then early, keep the re-ordered sequence. Otherwise reject $J_{i_q}$ and remove it. Return to Step 2.

The output is the final current sequence sorted by due-dates, followed by the rejected jobs in any order.

In Lean, a schedule is IsSchedule J l, the late set is lateSet t D l, optimality is IsOptimal t D J l, $A$ and $R$ are earlyPart/latePart, and one pass of Steps 2–3 is the relation MooreStep t D, all in the namespace MooreLateJobs.NumLate.

Formalization targets

Goal: Moore's algorithm is optimal (The Algorithm, Step 2, p. 103)

Let $l_0$ be a shortest-processing-time schedule of $J$, and let a run of MooreStep from $(l_0,[\,])$ reach a state $(\mathrm{cur},\mathrm{rej})$ in which $\mathrm{cur}$ has no late job. Then for every due-date ordering $A_D$ of $\mathrm{cur}$ and every ordering $P$ of $\mathrm{rej}$,

$$(A_D,\,P)\ \text{is an optimal schedule for } J.$$

All tie-breaks in both sorts are covered.

Milestones

In attack order:

1. Lemma 1 (p. 105): every optimal schedule has the same number of late jobs as $(A,R)$ and as every $(A,P)$.
2. Jackson's lemma (p. 105).
3. Lemma 2 (p. 105): re-ordering $A$ by due-dates keeps an optimal $(A,R)$ schedule optimal.
4. Lemma 3 (p. 105): a job that is late in some optimal schedule can be removed and appended.
5. The repeated-elimination claim (p. 106): after removing jobs late in successive optimal schedules until the rest is feasible, $(A_D,P)$ is optimal.
6. Cases 2) and 3) of the Selection Algorithm (p. 107): in either case the job $J_q$ is late in some optimal schedule.
7. Progress and termination of the algorithm (p. 108).

A companion item states the p. 104 remark that the final current sequence need not be re-sorted: $(\mathrm{cur},P)$ is already optimal.

Significance

The theorem shows that the minimum number of late jobs on one machine can be found in $O(n\log n)$ time, by a rule that also produces an optimal schedule of a very particular shape: due-date ordered early jobs first, then the late jobs in any order. Lemma 3's decomposition, that jobs late in some optimal schedule may be discarded one at a time, is the template reused for many related greedy results in scheduling.

The result is classical and fully proved on paper. To our knowledge no machine-checked proof of Moore's algorithm, of the Moore–Hodgson variant, or of Jackson's rule exists in Mathlib. This mission produces a checked proof of the algorithm as stated in the paper, with every tie-break allowed, together with reusable single-machine objects (schedules as lists, completion times, late sets) and Jackson's earliest-due-date feasibility lemma.

Difficulty

Neither ordering rule works alone. Sorting by due-dates alone gives a schedule with no late job whenever one exists, but it can make many jobs late once any must be. Keeping the shortest jobs first does not respect the due-dates at all. The step that fails in a direct greedy argument is the claim that the specific job $J_{i_q}$, the one just found late, belongs to the late set of some optimal schedule. That job is not in general the longest job of the prefix, and the paper has to treat separately the two cases in which it is rejected. On top of this, the algorithm re-sorts prefixes on the fly, so the claim has to be tied to the invariants of the run: the prefix is early and due-date sorted, and the jobs after it are at least as long as $J_{i_q}$.

Formalization scope

• Jobs and times. Jobs form a type ι with decidable equality; $J$ is a Finset ι; $t, D : ι \to \mathbb{R}$.
• Standing hypotheses. Every statement that involves schedules assumes $t_j \ge 0$ and $t_j \le D_j$ on $J$. The first is added: processing times are durations, and Jackson's lemma fails for negative times. The second is the paper's assumption on p. 102.
• Schedules and completion times. A schedule is a duplicate-free list with exactly the jobs of $J$. Positions are 0-based, and the job in position $k$ completes at the sum of the first $k+1$ processing times. Lateness is strict ($C_j > D_j$).
• Optimality compares against every schedule of the same job set.
• Ties. Orderings "by due-dates" and "by processing times" are List.Pairwise with ≤. Ties are arbitrary, and every statement quantifies over all such orderings.
• The algorithm. Steps 2–3 are the relation MooreStep. The re-ordered prefix is any due-date sorted permutation of the first $q+1$ jobs, and case 2) rejects the first late job $J_{i_q}$ itself, not the longest job of the prefix (that is Hodgson's variant). A run is Relation.ReflTransGen.

The goal must concern runs of this step relation from a shortest-processing-time schedule of $J$. Replacing the run by an arbitrary set of rejected jobs satisfying invariants would state a different theorem. The goal is not vacuous: the progress and termination milestones show that a terminal state is always reached.

Contributions are welcome at every level. Useful ones include general lemmas on completion times under permutation and filtering of lists, a proof of Jackson's lemma, proofs of the Selection Algorithm cases, and a proof of Hodgson's variant.

Selected references

• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• M. Held and R. M. Karp, A Dynamic Programming Approach to Sequencing Problems, J. SIAM 10(1):196–210, 1962. https://doi.org/10.1137/0110015
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

Motivation

A processor, a machine shop or a single server must work through a set of jobs one at a time, and each job is costly when it is late. Deciding the order is the single-machine sequencing problem, the simplest and most studied model of scheduling theory. Robert McNaughton's 1959 article Scheduling with Deadlines and Loss Functions (Management Science 6(1):1–12) treats it for a computer that must run several tasks, each with a deadline and a loss that grows linearly with the lateness. Its §2 gives the first sufficient condition under which a simple ratio rule is optimal in the presence of deadlines, and shows that interrupting and resuming tasks ("splitting", now called preemption) never helps on one processor.

Timeline.

• 1956: W. E. Smith, Various optimizers for single-stage production (Naval Research Logistics Quarterly 3), proves that sequencing jobs by non-increasing weight-to-processing-time ratio minimizes the total weighted completion time over non-preemptive sequences.
• 1959: McNaughton, §2 of the present paper, proves independently that the same ratio order is optimal against all schedules, split or not and with idle time (Theorem 2.3), and extends it to deadlines when no task finishes early in that order (Theorem 2.4). §3 of the same paper gives the "wrap-around" rule for preemptive makespan on identical processors, and §4 the non-preemptive optimality for weighted completion time on several processors.
• 1977: J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker show that minimizing total weighted tardiness on one machine, the general problem of §2, is strongly NP-hard (Annals of Discrete Mathematics 1); this is why §2 gives a sufficient condition and not an algorithm.

Setting

There are $m$ tasks $(1),\dots,(m)$ for a single processor, and the present is time $0$. Task $(i)$ takes $a_i > 0$ units of processing time, has a deadline $d_i$ and a penalty rate $p_i \ge 0$. If $(i)$ is finished at time $C_i \le d_i$ there is no loss; otherwise the loss on $(i)$ is $p_i x$, where $x = C_i - d_i$ is the time from the deadline to the completion. Thus the loss on a task completed at time $t$ is

$$\ell_i(t) = p_i \max(0,\ t - d_i).$$

The ratio of task $(i)$ is $r_i = p_i / a_i$.

A task may be split: part of it may run between times 4 and 6 and the remainder between times 8 and 11, and similarly in any finite number of parts. A schedule $S$ is therefore a finite list of pieces, each a task together with a start and a stop time. It is feasible when every piece lies in $[0,\infty)$ with start $\le$ stop, no two pieces overlap in time, and the pieces of each task $(i)$ have total length exactly $a_i$. The completion time $C_i(S)$ is the latest stop time of a piece of $(i)$, and the total loss is

$$c(S) = \sum_{i=1}^{m} \ell_i\bigl(C_i(S)\bigr).$$

For an order $\sigma$ of the tasks ($\sigma(k)$ in position $k$), the sequenced schedule $S_\sigma$ runs the tasks without splits and without unused time: $\sigma(k)$ occupies $\bigl[\sum_{l<k} a_{\sigma(l)},\ \sum_{l\le k} a_{\sigma(l)}\bigr]$. The order is in decreasing $r_i$ when $k \le l$ implies $r_{\sigma(l)} \le r_{\sigma(k)}$. Finally $c^*(S)$ denotes the total loss of $S$ computed as if $d_1 = \dots = d_m = 0$.

Formalization targets

Goal: Theorem 2.4 (p. 5)

If $\sigma$ is in decreasing $r_i$ and no task finishes before its deadline in $S_\sigma$, i.e. $d_i \le C_i(S_\sigma)$ for every $i$, then $S_\sigma$ is feasible and

$$c(S_\sigma) \le c(S') \qquad \text{for every feasible schedule } S'.$$

The competitors $S'$ may split tasks and leave the processor idle. The condition is sufficient but not necessary.

Milestones, in attack order

1. Theorem 2.1 (p. 4): if both $(i)$ and $(j)$ run in the $a_i + a_j$ consecutive units of time after a time $t$ past both deadlines and $r_i > r_j$, their joint loss is strictly smaller when $(i)$ goes first:

$$\ell_i(t+a_i) + \ell_j(t+a_i+a_j) < \ell_j(t+a_j) + \ell_i(t+a_j+a_i).$$

2. The reduction in the proof of Theorem 2.2 (pp. 4–5): a feasible schedule with more than $m$ pieces can be replaced by a feasible one with fewer pieces and no greater loss.
3. Theorem 2.2 (p. 4): some optimal schedule, optimal among all feasible schedules, splits no task.
4. Theorem 2.3 (p. 5): if $d_1 = \dots = d_m = 0$, the sequenced schedule in decreasing $r_i$ minimizes the total loss over all feasible schedules.
5. The display of the proof of Theorem 2.4 (p. 6): if no task finishes early in $S = S_\sigma$, then for every feasible $S'$,

$$c(S') - c(S) \ge c^*(S') - c^*(S).$$

Significance

The result. Theorem 2.3 is the ratio rule for total weighted completion time, in its strongest single-machine form: it holds against preemptive schedules and schedules with idle time, not only against permutations. Theorem 2.4 carries the rule over to deadlines and linear tardiness penalties under a checkable condition on one schedule. Since weighted tardiness is strongly NP-hard in general, a condition of this kind is what one can hope for, and the paper's two-step heuristic for general deadlines (p. 6) is built on it. Theorem 2.2, as the paper remarks (p. 6), "does not depend on the linear loss function": it makes non-preemptive scheduling without loss of generality for single-machine objectives of this kind.

Formalizing it. All results of §2 are proved in the paper and are textbook material; none has a machine-checked proof on the platform. The platform's Scheduling Algorithms V mission formalizes the multi-processor results of §§3–4 (via Brucker's textbook), and nothing there states a single-processor ratio rule with deadlines. This mission supplies a single-processor schedule model with splitting, the interchange lemma, the non-preemption theorem and the ratio rule, each over all feasible schedules.

Difficulty

The interchange argument of Theorem 2.1 compares only two schedules that differ in the order of two adjacent tasks. Turning it into optimality against every feasible schedule requires two further steps, and each fails if done naively. First, a competitor may split tasks and leave gaps; the interchange argument does not apply to such schedules, so a separate argument must remove splits without raising any completion time. Second, with deadlines the loss $\max(0, t - d_i)$ is not linear in the completion time, so the ratio order is in general not optimal; the obvious attempt to repeat the interchange argument fails as soon as a task can finish before its deadline, since moving such a task later costs nothing. This is why Theorem 2.4 needs its hypothesis that no task finishes early, and why the paper leaves the general case to a heuristic.

Formalization scope

Tasks and positions are the zero-based indices of Fin m; times, lengths, deadlines and penalties are real numbers. A schedule is a List of pieces (task, start, stop), mirroring the public definition SchedulingAlgorithms_ParallelMachines with one processor. Feasibility requires $0 \le$ start $\le$ stop, pairwise disjoint pieces, and exact total length $a_i$ per task; zero-length pieces and unsorted lists are allowed. The completion time is the maximum stop time of the task's pieces ($0$ for a task with no pieces, which feasibility excludes). "No split" means exactly one piece per task, so two abutting pieces count as a split. "Decreasing $r_i$" is non-increasing, with ties in any order. "Minimal" and "optimal" are stated as $\le$ against every feasible schedule, never as an infimum.

Standing assumptions, stated in every item: $a_i > 0$ (tasks take time, and $r_i = p_i/a_i$ needs $a_i \ne 0$), and $p_i \ge 0$ for Theorems 2.2–2.4 and the proof steps (penalties are non-negative; with a negative penalty and idle time allowed the loss is unbounded below). Theorem 2.1 carries no sign condition. No condition is placed on the deadlines.

A formalization that restricts the competitors of Theorems 2.2–2.4 to unsplit schedules, or to sequenced schedules of other orders, states a weaker theorem and is ruled out: every statement quantifies over all feasible schedules.

A complete development needs: sums over sublists of pieces, rearrangements of pieces of a schedule and their effect on completion times, and optimality over permutations of a finite set of tasks. The schedule model and the non-preemption argument are reusable for any single-machine regular objective. Contributions of intermediate lemmas on these points are welcome.

Selected references

• R. McNaughton, Scheduling with Deadlines and Loss Functions, Management Science 6(1):1–12, 1959. https://doi.org/10.1287/mnsc.6.1.1
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3(1–2):59–66, 1956. https://doi.org/10.1002/nav.3800030106
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$. In engineering applications the coefficient matrices are rarely known exactly: they come from measurements, from a model of a physical plant, or from a finite-precision implementation. El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for solutions that remain feasible for every admissible value of the uncertain data, and showed how to compute such robust solutions by semidefinite programming. The paper appeared alongside Ben-Tal and Nemirovski's robust convex programming (Math. Oper. Res. 23(4), 1998) and is one of the two founding treatments of robust SDP.

When the uncertainty has structure (a block-diagonal perturbation, repeated scalar parameters, a symmetric matrix), the exact robust problem is NP-hard (El Ghaoui and Lebret, SIAM J. Matrix Anal. Appl. 18, 1997). This is the same obstacle that robust control meets in computing the structured singular value, and the remedy the paper uses, scaling matrices that commute with the perturbation structure, goes back to that literature (Doyle, IEE Proc. D 129, 1982; Fan, Tits and Doyle, IEEE Trans. Automat. Control 36, 1991). This mission formalizes the resulting tractable conservative approximation, Theorem 3.2 of the paper, together with the lemma it rests on and an application to integer feasibility problems.

Setting

Fix natural numbers $m, n, p, q$. The decision variable is $x \in \mathbb{R}^m$. The nominal data are affine maps

$$F(x) = F_0 + \sum_{i=1}^m x_i F_i \in \mathbb{R}^{n\times n}, \qquad R(x) = R_0 + \sum_{i=1}^m x_i R_i \in \mathbb{R}^{q\times n},$$

with every $F_i$ symmetric, and fixed matrices $L \in \mathbb{R}^{n\times p}$, $D \in \mathbb{R}^{q\times p}$. A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$, and the perturbed constraint matrix is the linear-fractional representation (LFR)

$$\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,$$

which is defined when $\det(I - D\Delta) \neq 0$. The perturbation ranges over a linear subspace $\mathcal{D} \subseteq \mathbb{R}^{p\times q}$, which encodes the structure, and is bounded by a level $\rho > 0$ in the spectral norm $\|\Delta\|$ (the largest singular value). The robust feasible set is

$$\mathcal{X}_\rho = \{x : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \det(I - D\Delta) \neq 0 \text{ and } \mathbf{F}(x,\Delta) \succeq 0\},$$

and the robust SDP (RSDP) is to minimize $c^Tx$ over $\mathcal{X}_\rho$.

The scaling set of $\mathcal{D}$ is the linear subspace

$$\mathcal{B} = \{(S,T,G) \in \mathbb{R}^{p\times p}\times\mathbb{R}^{q\times q}\times\mathbb{R}^{p\times q} : S\Delta = \Delta T,\ G\Delta^T = -\Delta G^T \text{ for every } \Delta \in \mathcal{D}\}.$$

Formalization targets

Goal: Theorem 3.2 (p. 37), as an inclusion of feasible sets

For every $x$: if some $(S,T,G) \in \mathcal{B}$ has $S \succ 0$, $T \succ 0$ and

$$\begin{bmatrix} F(x) - LSL^T & R(x)^T - LSD^T + LG \\ R(x) - DSL^T + G^TL^T & \rho^{-2}T - DSD^T + DG + G^TD^T\end{bmatrix} \succ 0,$$

then $x \in \mathcal{X}_\rho$, and in fact $\mathbf{F}(x,\Delta) \succ 0$ for every $\Delta \in \mathcal{D}$ with $\|\Delta\| \le \rho$. A companion item states the consequence for optimal values: the SDP value is an upper bound on the RSDP value, with both infima taken in the extended reals.

Milestones

1. Lemma 3.2 (p. 37): the same implication for constant $F$, $R$ and $\rho = 1$, with the matrix (13).
2. The full-perturbation case (p. 37): for $\mathcal{D} = \mathbb{R}^{p\times q}$ and $p, q \ge 1$, $\mathcal{B}$ consists exactly of the triples $(\tau I_p, \tau I_q, 0)$, with $\tau \ge 0$ when $S \succeq 0$.
3. Theorem 5.6 (p. 48): if $F_i = 2L_iR_i$ with $r_i = \operatorname{rank} F_i$, and $x_{\mathrm{feas}}$ satisfies, for some $\lambda \ge 0$ and block-diagonal $S = S^T$, $G = -G^T$,

$$\begin{bmatrix} F(x_{\mathrm{feas}}) - \lambda I - LSL^T & \tfrac12R^T + LG \\ \tfrac12R - GL^T & S\end{bmatrix} \succ 0,$$

then every integer vector closest to $x_{\mathrm{feas}}$ in the maximum norm satisfies $F(z) \succeq 0$.

Significance

The result. Theorem 3.2 replaces an NP-hard semi-infinite constraint, one matrix inequality for each admissible perturbation, by a single linear matrix inequality in the enlarged variable $(x, S, T, G)$. Every point it certifies is robustly feasible, so its optimal value is a certified upper bound on the robust optimum and its optimizer is a usable robust solution. In the full case the scalings collapse to one multiplier $\tau$ (milestone 2), which connects the bound to the exact reformulation of Section 3.1 of the paper. Theorem 5.6 shows the same machinery at work on a combinatorial problem: robustness against perturbations of size $1/2$ in each coordinate of $x$ turns an SDP-feasible point into an integer solution by rounding.

Formalizing it. The results are proved in the paper (Lemma 3.2 with the proof deferred to [16]); none of them has a machine-checked proof that this mission is aware of, and the platform has no linear-fractional or structured-perturbation results. The formalization also settles the exact form of the certificate: as printed, the matrix (13) and the LMI of Theorem 3.2 contain products that are dimensionally undefined, and this mission states the condition the proof actually yields (see the scope section).

Difficulty

The inequality to be proved is a statement about infinitely many perturbations, and $\mathbf{F}(x,\Delta)$ depends on $\Delta$ through a matrix inverse. The natural first step, eliminating $\Delta$ by an exact S-procedure as in the full case, is not available: with a structured $\mathcal{D}$ the set of pairs of vectors linked by some $\Delta \in \mathcal{D}$ is not described by one quadratic inequality, and losslessness fails. The scalings in $\mathcal{B}$ give several valid quadratic inequalities instead, and one must show that their combination controls every $\Delta$ in the norm ball, including the well-posedness claim $\det(I - D\Delta) \neq 0$, which is part of the conclusion rather than an assumption. The commutation condition $S\Delta = \Delta T$ must be turned into an inequality for $\|\Delta\| \le 1$, which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between $\rho = 1/2$ and the stated matrix must be matched to the general lemma.

Formalization scope

Matrices are Matrix (Fin a) (Fin b) ℝ; $\succ 0$ and $\succeq 0$ are Matrix.PosDef and Matrix.PosSemidef (both include symmetry); block matrices are Matrix.fromBlocks on Fin n ⊕ Fin q. The norm of a perturbation is the $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), i.e. the largest singular value; the maximum norm in Theorem 5.6 is Mathlib's sup norm on Fin m → ℝ. $\mathcal{D}$ is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is $0$ at a singular matrix, so every statement pairs the LFR with $\det(I - D\Delta) \neq 0$. The standing assumption $\rho > 0$ of Section 3 is a hypothesis.

Readings and corrections of the printed statements:

• (13) as printed is dimensionally inconsistent; we state the condition the proof yields, which coincides with the printed one when $G$ is square and skew-symmetric and $\mathcal{D}$ consists of symmetric matrices. Concretely, (11) prints $G \in \mathbb{R}^{q\times p}$ with $G\Delta = -\Delta^TG^T$ and (13) prints the blocks $R - DSL - GL^T$ and $T - GD^T + DG - DSD^T$; the mission uses $G \in \mathbb{R}^{p\times q}$ with $G\Delta^T = -\Delta G^T$ and the blocks $R - DSL^T + G^TL^T$ and $T - DSD^T + DG + G^TD^T$. The same correction applies to the LMI of Theorem 3.2 (with $\rho^{-2}T$). Theorem 5.6 is stated as printed.
• "An upper bound on the RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the inclusion of the SDP's feasible projection in $\mathcal{X}_\rho$, for every $x$; the goal states it with the strict conclusion $\mathbf{F}(x,\Delta) \succ 0$ as well. The value form is a separate item.
• In the full-perturbation remark, "for some $\tau \ge 0$" is stated under $S \succeq 0$, and "We then recover the exact results of section 3.1" is not formalized.
• In Theorem 5.6, $\mathcal{S}$'s index range "$i = 1,\dots,n$" is read as $i = 1,\dots,m$; the hypothesis $r_i = \operatorname{rank}F_i$ is kept.

Trivializing formalizations are ruled out: $(0,0,0) \in \mathcal{B}$ always, so the hypotheses $S \succ 0$ and $T \succ 0$ are kept outside $\mathcal{B}$; $\mathcal{D}$ is a subspace, not an arbitrary set; and the norm is the spectral norm, not Mathlib's default entrywise norm.

A complete development needs the square root of a positive definite matrix and its commutation with $S$ and $T$, the spectral-norm characterization $\Delta\Delta^T \preceq \|\Delta\|^2 I$, Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating $(I - D\Delta)^{-1}$ to an auxiliary vector. These are reusable well beyond this mission; contributions of any of them, and of the value and rounding corollaries, are welcome.

Selected references

• L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18:1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• M. K. H. Fan, A. L. Tits, J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36:25–38, 1991. https://doi.org/10.1109/9.62265
• J. C. Doyle, Analysis of feedback systems with structured uncertainties, IEE Proc. D 129(6):242–250, 1982. https://doi.org/10.1049/ip-d.1982.0053
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777