All missions

Motivation

Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.

D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.

Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.

Setting

Fix $n, m \in \mathbb N$, a vector $a \in \mathbb R^n$, a symmetric positive definite $n\times n$ matrix $G$, an $n\times m$ matrix $C$ with columns $n_1,\dots,n_m$, and $b \in \mathbb R^m$. The quadratic program (1.1) is

$$\min_x\ f(x) = a^{\mathsf T}x + \tfrac12 x^{\mathsf T}Gx \quad\text{subject to}\quad s_i(x) = n_i^{\mathsf T}x - b_i \ge 0,\quad i \in K = \{1,\dots,m\}.$$

The gradient is $g(x) = Gx + a$. For $J \subseteq K$, the subproblem $P(J)$ keeps only the constraints indexed by $J$; $P(\emptyset)$ is solved by $x^0 = -G^{-1}a$. A set $A \subseteq K$ is linearly independent if the normals $n_i$, $i\in A$, are.

For an independent $A$, let $N$ be the matrix with columns $n_i$, $i\in A$, and define

$$N^* = (N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1},\qquad H = G^{-1} - G^{-1}N(N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1}.$$

The multipliers are $u(x) = N^*g(x)$; for a constraint $p \notin A$ with normal $n^+ = n_p$ the infeasibility multipliers are $r = N^*n^+$; a superscript $+$ denotes the same objects for $A^+ = A\cup\{p\}$.

An S-pair $(x, A)$ is an independent active set $A$ with $s_i(x) = 0$ for $i\in A$ and $x$ optimal for $P(A)$. A V-triple $(x, A, p)$ has $p\notin A$, $A^+$ independent, $s_p(x) < 0$, $s_i(x) = 0$ for $i \in A$, $H^+g(x) = 0$ and $u^+(x) = (N^+)^*g(x) \ge 0$.

The dual algorithm starts from $(x^0, \emptyset)$. In Step 1 it stops if $x$ is feasible; otherwise it picks any violated constraint $p$. In Step 2 it moves along the primal direction $z = Hn^+$ and the dual direction $(-r; 1)$ with step $t = \min\{t_1, t_2\}$, where $t_1$ is the largest step that keeps the multipliers nonnegative and $t_2 = -s_p(x)/z^{\mathsf T}n^+$ makes constraint $p$ active. If both are infinite it reports infeasibility. A full step ($t = t_2$) adds $p$ and returns to Step 1. A partial step ($t = t_1 < t_2$), or a dual step ($z = 0$), drops a constraint $k$ attaining $t_1$ and repeats Step 2.

Formalization targets

Goal: Theorem 3 (p. 11)

For every choice of the violated constraint $p$ and of the dropped constraint $k$:

$$\text{no run from } (x^0,\emptyset) \text{ is infinite, and every run that cannot continue ends in } \begin{cases}\text{STOP at an optimal } x \text{ of (1.1)}, \text{ or}\\ \text{STOP with } \{x : C^{\mathsf T}x \ge b\} = \emptyset.\end{cases}$$

Milestones, in attack order

1. Properties (2.6)–(2.9) (p. 5): $Hw = 0 \iff w \in \operatorname{range} N$; $H \succeq 0$; $HGH = H$; $N^*GH = 0$.
2. Optimality conditions (2.3)–(2.4) (p. 5): on the manifold of $A$, $x$ solves $P(A)$ iff $N^*g(x) \ge 0$ and $Hg(x) = 0$.
3. Lemma 1 (p. 8): along $\bar x = x + tHn^+$ from a V-triple, $H^+g(\bar x) = 0$, the constraints of $A$ stay active, $u^+(\bar x) = u^+(x) + t(-r;1)$ and $s_p(\bar x) = s_p(x) + t\,z^{\mathsf T}n^+$.
4. Theorem 1 (pp. 8–9): the step $t = \min\{t_1,t_2\}$ increases $s_p$ and $f$; a partial step yields a V-triple, a full step an S-pair.
5. Theorem 2 (p. 10): if $n_p = Nr$ and $s_p(x) < 0$ at an S-pair, then $r \le 0$ means $P(A\cup\{p\})$ is infeasible; otherwise dropping a minimizing $k$ gives a V-triple.
6. One round of Step 2 (p. 11): from an S-pair and a violated $p$, at most $|A|$ partial or dual steps and one final step end either in infeasibility of (1.1) or in a new S-pair $(\bar x, \bar A \cup\{p\})$ with $\bar A\subseteq A$ and $f(\bar x) > f(x)$.

Significance

Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.

The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for $N^*$ and $H$, a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.

Difficulty

The obvious termination argument is that $f$ increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave $x$ unchanged (the dual steps of Step 2(c)(ii)), so $f$ is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move $x$. Any such argument relies on invariants (independence of $A^+$, nonnegativity of the multipliers, $s_p < 0$ along partial steps) that hold only on reachable states, and the operators $N^*$ and $H$ are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.

Formalization scope

Vectors are Fin n → ℝ, $G$ is Matrix (Fin n) (Fin n) ℝ with G.PosDef, $C$ is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in $A$. Lean's matrix inverse returns $0$ for singular matrices, so every statement about $N^*$ and $H$ assumes $G \succ 0$ and an independent active set (directly, or through an S-pair or V-triple).

The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of $p$ and $k$. Infinite step lengths are separate transitions; a tie $t_1 = t_2$ takes the full step, as the paper tests $t = t_2$ first. The running value of $f$ and the factorizations of Section 4 are not part of the state.

Explicit readings of the paper's words:

• "solves the QPP or indicates infeasibility in a finite number of steps" is: no infinite sequence of Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);
• "S-pair" is: $A$ independent and active at $x$, with $x$ optimal for $P(A)$ (the reading every use in the paper needs);
• in Theorem 1 the partial-step clause carries $t < t_2$ (as in its proof), and the multiplier printed $u^+_{j+1}$ in (3.16) is $u^+_{q+1}$, the entry belonging to $p$;
• "an S-pair can never reoccur" is expressed as the strict increase $f(\bar x) > f(x)$ in milestone 6.

Property (2.10), printed $HH^+ = H^+$, is false unless $G = I$ and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.

A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.

Needed infrastructure: Schur-complement and projector identities for $N^*$ and $H$; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about $N^*$ and $H$, are welcome.

Selected references

• D. Goldfarb and A. Idnani, A numerically stable dual method for solving strictly convex quadratic programs, Mathematical Programming 27 (1983) 1–33. https://doi.org/10.1007/BF02591962
• C. E. Lemke, A method of solution for quadratic programs, Management Science 8 (1962) 442–453. https://doi.org/10.1287/mnsc.8.4.442
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006, Chapter 16. https://doi.org/10.1007/978-0-387-40065-5

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$. Let $n=|V|$ and $m=|E|$, counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$, with $c(v,w)=-c(w,v)$. A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$. Its excess $e_f(v)$ is the sum of flow entering $v$. A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$. An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$-optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$-optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$-optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$. Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

$$R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).$$

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

$$K\leq 3n(n-1)+3nm+3n^2(m+n).$$

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$-optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$-optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$-optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$. Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$, and relabel raises $p(v)$. This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$, $3n(n-1)$, $3nm$, and $3n^2(m+n)$; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
• Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.

Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.

Timeline:

• Talluri and van Ryzin (2004) showed that revenue-ordered assortments are optimal under the multinomial logit model.
• Rusmevichientong, Shmoys, Tong and Topaloglu (2014) showed the problem NP-hard under a mixture of two logit models, and proved that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit.
• Aouad, Farias, Levi and Segev (2018) proved an $\Omega(1/\ln(r_k/r_1))$ guarantee under random utility models, and that the assortment problem there is NP-hard to approximate within $\Omega(1/n^{1-\epsilon})$ and $\Omega(1/\log^{1-\epsilon}(r_k/r_1))$.
• Berbeglia and Joret (2016–2020, Algorithmica) proved the guarantees $1/k$, $1/\sum_{i}(r_i-r_{i-1})/r_i\ge1/(1+\ln(r_k/r_1))$ and a purchase-probability bound under any regular model, and an instance on which all three, in their sum forms, are attained in the limit.

Setting

The products form a finite set $\mathcal C$. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer buys $x$. The no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if

1. $\mathcal P(x,S)\ge0$ for $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$.

Each product has a revenue $r(x)>0$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$.

Let $r_1<\dots<r_k$ be the distinct revenues, with $r_0:=0$, and $S_i=\{x: r(x)\ge r_i\}$. The heuristic earns

$$\mathrm{RO}=\max_{i\in[k]}\mathrm{rev}(S_i).$$

For an optimal $S^*$ let $N_i=\sum_{x\in S^*,\,r(x)\ge r_i}\mathcal P(x,S^*)$, $N_{k+1}=0$, and $\ell$ the largest index with $N_\ell>0$. Section 3 of the paper proves

• (A) $\mathrm{OPT}\le k\cdot\mathrm{RO}$ (Theorem 3.1);
• (B) $\mathrm{OPT}\le D_r\cdot\mathrm{RO}$, with $D_r=\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\le 1+\ln(r_k/r_1)$ (Theorem 3.2);
• (C) $\mathrm{OPT}\le D_N(S^*)\cdot\mathrm{RO}$, with $D_N(S^*)=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le 1+\ln(N_1/N_\ell)$ (Theorem 3.3).

Formalization targets

Goal: Theorem 3.4

For every $k\ge1$ and every $\delta>0$ there are a finite nonempty product set, a regular $\mathcal P$, revenues $r>0$ with exactly $k$ distinct values, and an optimal $S^*$ with $N_1>0$, such that

$$k\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_r\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_N(S^*)\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT}.$$

So none of the bounds (A), (B), (C) stays true when multiplied by $1+\delta$, for any number $k$ of distinct revenues.

The tight instance (milestones)

The paper's witness has products $(i,j)$ with $i\in[k]$ and $j\in[i]$. Product $(i,j)$ has revenue $\varepsilon^{-j}$, and $\mathcal P((i,j),S)=\varepsilon^i$ when $(i,j)\in S$ and $(i,1),\dots,(i,j-1)\notin S$, and $0$ otherwise, for $0<\varepsilon\le\tfrac12$. The milestones follow the proof on pp. 10–11:

• the axiom (iii) bound;
• (7);
• (8);
• (9);
• regularity;
• the distinct revenues $r_i=\varepsilon^{-i}$;
• $\mathrm{RO}=\mathrm{rev}(\mathcal C)<1/(1-\varepsilon)$;
• $\mathrm{OPT}=k$, attained by $\{(i,i)\}$;
• the limits $\mathrm{OPT}/\mathrm{RO}\to k$ and $D_r\to k$;
• $N_i=\varepsilon^i+\dots+\varepsilon^k$ and $D_N\to k$ as $\varepsilon\to0^+$.

Significance

With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters $k$, $D_r$ and $D_N$, revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.

On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.

Difficulty

The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:

• the regularity of the instance at the no-purchase option, (9), which needs the row decomposition (8);
• the claim that $\{(i,i)\}$ is optimal among all $2^{k(k+1)/2}$ offer sets, asserted without proof;
• the claim that the full set is the best threshold set;
• the evaluation of $D_N(S^*)$, which needs $\ell=k$.

The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly $k$ revenues on which all three bounds are nearly attained, for every $k$.

Formalization scope

• Products are an arbitrary finite type C. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. Offer sets are Finset C.
• IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at $x=0$ is essential: without it the guarantees fail.
• $\mathrm{OPT}$ is Finset.sup' over all subsets, including $\emptyset$. $\mathrm{RO}$ is Finset.sup' over the $k$ threshold sets only, and needs Nonempty C.
• The distinct revenues are the sorted image of r, indexed by Fin k from $0$: the Lean index $i$ is the paper's $i+1$, and $r_0=0$ is a separate case. $\ell$ lives in WithBot (Fin k).
• Bounds are multiplicative ($\mathrm{OPT}\le D\cdot\mathrm{RO}$); there is no ratio $\mathrm{RO}/\mathrm{OPT}$ in the goal. Limits are along 𝓝[>] 0.
• The tight instance keeps the paper's 1-based pairs $(i,j)$ as a subtype of Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.

Ruled out:

• a fixed $k$, since "for every $k$" is the content;
• tightness of the logarithmic forms $1/(1+\ln(r_k/r_1))$ and $1/(1+\ln\nu)$, which this instance does not show (there $1+\ln(r_k/r_1)\to\infty$ while $\mathrm{OPT}/\mathrm{RO}\to k$), so only the sum forms are claimed tight;
• an instance whose regularity is assumed;
• a heuristic maximizing over all subsets.

Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of $\{(i,i)\}$, and general lemmas on sorted distinct values of a finite function.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; published in Algorithmica, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724

Motivation

A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).

The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).

Setting

Let $\mathcal C$ be a finite nonempty set of products. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer offered $S$ buys $x$. Buying nothing is the option $0$, with $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular when

1. $\mathcal P(x,S)\ge0$ for products and for $x=0$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4 at $x=0$ says that enlarging the offer set never makes buying nothing more likely.

Prices are a function $r:\mathcal C\to\mathbb R_{>0}$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$. Let $r_1<\dots<r_k$ be the distinct values of $r$, and let $S_i=\{x:r(x)\ge r_i\}$ for $i\in[k]$. The revenue-ordered strategy earns

$$\mathrm{RO}=\max_{1\le i\le k}\mathrm{rev}(S_i).$$

For an assortment $S^*$, the purchase profile is

$$N_i=\sum_{x\in S^*,\ r(x)\ge r_i}\mathcal P(x,S^*)\qquad(i\in[k]),\qquad N_{k+1}:=0,$$

the probability that a customer offered $S^*$ buys something priced at least $r_i$. It is non-increasing in $i$.

Formalization targets

Goal: Theorem 3.3 (p. 9)

Let $S^*$ be optimal, $\mathrm{rev}(S^*)=\mathrm{OPT}$, suppose $N_1>0$, and let $\ell\in[k]$ be maximum with $N_\ell>0$. Then

$$\mathrm{OPT}\le\Big(\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\Big)\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le1+\ln\nu,\quad\nu=\frac{N_1}{N_\ell}.$$

The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form $1/(1+\ln\nu)$.

Milestones (in proof order)

• Lemma 2.1 (p. 6): $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• First observation of the proof (p. 9): $N_i\le\sum_{x\in S_i}\mathcal P(x,S_i)$ and $N_ir_i\le\sum_{x\in S_i}\mathcal P(x,S_i)r_i$.
• Inequality (6) (p. 9): $N_ir_i\le\mathrm{RO}$ for every $i\in[k]$.
• Revenue identity (p. 9): $\mathrm{rev}(S^*)=\sum_{i=1}^{\ell}(N_i-N_{i+1})r_i=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}N_ir_i$.
• Logarithmic step (p. 9, the comparison $1/\sum\ge1/(1+\ln\nu)$ in Theorem 3.3, used in the last inequality of the proof): for $N_1\ge\dots\ge N_\ell>0$ and $N_{\ell+1}=0$, $\sum_{i=1}^{\ell}(N_i-N_{i+1})/N_i\le1+\ln(N_1/N_\ell)$. The paper states this step without proof.

Significance

Theorem 3.3 gives a guarantee that is independent of prices. The bound $1+\ln(r_k/r_1)$ of Theorem 3.2 grows when prices are spread out. The bound $1+\ln\nu$ is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the $1/(1+\ln m)$ guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.

The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.

Difficulty

Each step is elementary. The difficulty is bookkeeping. The revenue of $S^*$ has to be regrouped by distinct price levels rather than by products: several products may share a price, and $k$ counts values. The regrouping uses an Abel-type rearrangement with the boundary convention $N_{k+1}=0$. Comparing $N_i$ with the purchase probability of $S_i$ needs regularity twice. First, axiom 4 for products passes from $S^*$ to $S^*\cap S_i$. Then the no-purchase case passes from $S^*\cap S_i$ to $S_i$. A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.

Formalization scope

• Products form a finite type C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's $k\ge1$. Offer sets are Finset C, and $\mathcal P$ is P : C → Finset C → ℝ. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. $\mathrm{RO}$ is Finset.sup' over the indices $1,\dots,k$ of the threshold sets only.
• Indices are 1-based natural numbers. level r i is $r_i$ for $1\le i\le k$. purchaseProfile P r S i is $N_i$ for $1\le i\le k$ and $0$ otherwise, which builds in $N_{k+1}=0$.
• Optimality is the hypothesis $\mathrm{rev}(S^*)=\mathrm{OPT}$. The index $\ell$ is a variable with hypotheses $1\le\ell\le k$, $N_\ell>0$, and $N_i\not>0$ for $\ell<i\le k$. $N_1>0$ is kept as in the paper.
• The approximation factor is stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. Both the sum form and the logarithmic form are stated. $\ln$ is Real.log, applied to $\nu\ge1$.
• The milestones other than the goal are stated for an arbitrary $S^*$, because the proof does not use optimality there.

The following statements are trivial or false and are not this mission: a maximum over all subsets in place of $\mathrm{RO}$; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while $\mathrm{rev}(S^*)$ is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular $\mathcal P$.

A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that $N$ is non-increasing.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371v3
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective $\theta \mapsto V^{\pi_\theta}(\mu)$ is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?

Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an $O(1/t)$ rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.

Setting

A finite MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions ($\mathcal A$ nonempty), a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns to each state a probability vector $\pi(\cdot\mid s)$ on $\mathcal A$. Its value $V^\pi(s)$ is the expected discounted sum of rewards $\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid s_0=s]$ when actions are drawn from $\pi$; its state–action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and its advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. For a distribution $\mu$ on states, $V^\pi(\mu)=\sum_s\mu(s)V^\pi(s)$, and the discounted state visitation distribution is $d^\pi_\mu(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\mu)$. A policy $\pi^\star$ is optimal if $V^{\pi}(s)\le V^{\pi^\star}(s)$ for every policy $\pi$ and every state $s$; $V^\star=V^{\pi^\star}$.

The softmax policy with parameters $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is

$$\pi_\theta(a\mid s)=\frac{\exp(\theta_{s,a})}{\sum_{a'\in\mathcal A}\exp(\theta_{s,a'})}.$$

Softmax policy gradient ascent with step size $\eta$ produces, from an arbitrary $\theta^{(0)}$, the iterates

$$\theta^{(t+1)}=\theta^{(t)}+\eta\,\nabla_\theta V^{(t)}(\mu),\qquad V^{(t)}=V^{\pi_{\theta^{(t)}}} .$$

The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ $=V^{\pi_\theta}(\mu)$, and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.

Formalization targets

Goal: Theorem 5.1

If $\mu(s)>0$ for every state and $0<\eta\le(1-\gamma)^3/8$, then for every state $s$

$$V^{(t)}(s)\longrightarrow V^\star(s)\qquad(t\to\infty).$$

Milestones (Appendices C.1 and D)

1. Lemma C.1, the gradient formula $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a\mid s)A^{\pi_\theta}(s,a)$.
2. Lemma D.1, smoothness $5\|c\|_\infty$ of $\theta_s\mapsto\sum_a\pi_\theta(a\mid s)c_a$.
3. Lemma D.4 at $\lambda=0$, smoothness $8/(1-\gamma)^3$ of $\theta\mapsto V^{\pi_\theta}(\mu)$.
4. Lemma C.2, pointwise monotone improvement of $V^{(t)}(s)$ and $Q^{(t)}(s,a)$ for $\eta\le(1-\gamma)^2/5$.
5. Lemma C.3, existence of the limits $V^{(\infty)}$, $Q^{(\infty)}$ and the bound (40).
6. Lemma C.4, eventual sign separation (41) of the advantages on $I^s_+=\{a:Q^{(\infty)}(s,a)>V^{(\infty)}(s)\}$ and $I^s_-=\{a:Q^{(\infty)}(s,a)<V^{(\infty)}(s)\}$.
7. Lemma C.5, vanishing gradients, $\pi^{(t)}(a\mid s)\to0$ off $I^s_0=\{a:Q^{(\infty)}(s,a)=V^{(\infty)}(s)\}$, and $\sum_{a\in I^s_0}\pi^{(t)}(a\mid s)\to1$.
8. Lemma C.6, eventual strict monotonicity of $\theta^{(t)}_{s,a}$ on $I^s_\pm$.
9. Lemma C.7, divergence of $\max_{a\in I^s_0}\theta^{(t)}_{s,a}$ and $\min_a\theta^{(t)}_{s,a}$ when $I^s_+\neq\emptyset$.
10. Lemma C.11, lower boundedness of $\theta^{(t)}_{s,a}$ on $I^s_+$ and $\theta^{(t)}_{s,a}\to-\infty$ on $I^s_-$.

The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.

Significance

The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to $V^\star$ at every state, not only on average under $\mu$. It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether $\mu>0$ can be dropped.

The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.

Difficulty

The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from $\nabla_\pi V^\pi(\mu)\to0$, but under softmax $\partial V/\partial\theta_{s,a}=\pi_\theta(a\mid s)\,\partial V/\partial\pi_\theta(a\mid s)$, so a vanishing $\theta$-gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters $\theta^{(t)}_{s,a}$ move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets $I^s_0, I^s_\pm$ and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.

Formalization scope

Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in $[0,1]$, $0\le\gamma<1$); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\theta$; the coordinate $(s,a)$ of the gradient is $\partial/\partial\theta_{s,a}$. Logarithms do not appear. Conventions committed to:

• $V^\star(s)$ is PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.
• The step size satisfies $0<\eta$, which "gradient ascent" presupposes and the page does not write; at $\eta=0$ the theorem is false.
• $\mu(s)>0$ for every $s$ is a hypothesis of the goal and of Lemmas C.5–C.11; Lemmas C.1–C.4 are stated without it, and Lemma C.1 for an arbitrary real weighting $\mu$.
• In Lemmas C.4–C.11 the limits $V^{(\infty)}$, $Q^{(\infty)}$ are parameters with the hypotheses that they are the limits of $V^{(t)}$, $Q^{(t)}$. The paper's $\Delta=\min_{A^{(\infty)}(s,a)\neq0}|A^{(\infty)}(s,a)|$ is replaced by any $\Delta>0$ bounded by every nonzero $|A^{(\infty)}(s,a)|$, which avoids an undefined minimum over an empty set.
• "$\to\pm\infty$" is Tendsto … atTop atTop / atBot; "strictly increasing for $t\ge T_1$" is StrictMonoOn on Set.Ici T1, with $T_1$ existentially quantified.

The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets $I^s_0, I^s_\pm$; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis $I^s_+\neq\emptyset$ of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.

A full development needs: differentiability of $\theta\mapsto V^{\pi_\theta}$ and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for $L$-smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument are welcome.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261
• J. Mei, C. Xiao, C. Szepesvári, D. Schuurmans, On the Global Convergence Rates of Softmax Policy Gradient Methods, ICML 2020. https://arxiv.org/abs/2005.06392
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 1999. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation

Motivation

Consensus asks $N$ processors, each holding an initial value, to agree on one value despite some of them failing. It underlies replicated databases, atomic commit and state-machine replication. Its solvability depends on the timing assumptions. With fully synchronous processors and communication, $t$ fail-stop faults can be tolerated for any $t < N$. With fully asynchronous communication, Fischer, Lynch and Paterson showed that no deterministic protocol tolerates even one fail-stop fault (JACM 1985).

Dwork, Lynch and Stockmeyer (JACM 1988) introduced partial synchrony, a model between these two extremes. Message delays have an upper bound $\Delta$, but either the bound is unknown to the protocol, or it holds only from an unknown time on. For each fault type they found the exact number of faults that can be tolerated. This mission formalizes the lower bound for fail-stop faults: when the processors are synchronous and communication is partially synchronous, no consensus protocol tolerates $t$ faults once $N \le 2t$.

Timeline. 1985: Fischer, Lynch, Paterson, impossibility of consensus with one fail-stop fault under asynchrony. 1987: Dolev, Dwork, Stockmeyer, which combinations of synchrony assumptions admit consensus (JACM 1987). 1988: Dwork, Lynch, Stockmeyer, partial synchrony, with matching upper and lower bounds on resiliency for fail-stop, omission, authenticated Byzantine and Byzantine faults. The global stabilization time of the 1988 paper became a common liveness assumption for later fault-tolerant agreement protocols.

Setting

There are $N$ processors $p_1, \dots, p_N$. Each processor holds an initial value $v_i \in \{0, 1\}$. Each runs a deterministic protocol: a transition diagram over a possibly infinite set of states. In each state the next instruction is either $\mathrm{Send}(m, p_j)$, which puts message $m$ in $p_j$'s buffer, or $\mathrm{Receive}(p_i)$, which removes a set $S$ of messages from $p_i$'s buffer and delivers it. The next state depends on the current state and, for a Receive, on $S$. A step never both sends and receives. Each state may record a decision, and the first decision a processor records is final.

Real time is the ticks $1, 2, 3, \dots$. A run fixes the initial values and, at each tick, which processors take a step and which messages each Receive delivers. A message is delivered only after the tick at which it was sent, only to its addressee, and at most once.

• Synchronous processors ($\Phi = 1$): every correct processor takes a step at every tick.
• Fail-stop faults: a faulty processor follows the protocol until it stops, and it never restarts. A processor that stops at time $0$ is initially dead.
• $\Delta$ holds in $[T, \infty)$: a message sent at a tick $s_1 \ge T$ is delivered no later than any Receive of its addressee at a tick $s_2 \ge s_1 + \Delta$.
• Delta holds eventually: $\Delta$ is a fixed positive integer known to the protocol. In every run, $\Delta$ holds in $[T, \infty)$ for some unknown global stabilization time $T$. Messages sent before $T$ may be delayed arbitrarily or lost.
• Delta is unknown: the protocol is fixed first. In every run, some positive $\Delta$ holds in $[1, \infty)$.

A protocol is a $t$-resilient consensus protocol achieving weak unanimity if the following holds for every set $C$ of at least $N - t$ processors and every allowed run in which the processors of $C$ are correct and the others fail-stop. No two processors of $C$ decide differently (consistency). Every processor of $C$ decides (termination). If all initial values are $v$ and no processor is faulty, every decision is $v$ (weak unanimity).

Formalization targets

Goal: Theorem 4.3

For integers $t \le N$ with

$$2 \le N \le 2t,$$

there is no $t$-resilient consensus protocol achieving weak unanimity for binary values with fail-stop faults and synchronous processors. This holds for every positive $\Delta$ when $\Delta$ holds eventually, and when delta is unknown.

Milestones: the three scenarios of the proof

Split the processors into groups $P$ and $Q$ with $1 \le |P|, |Q| \le t$.

• Scenario A: all inputs $0$ and $Q$ initially dead. The processors of $P$ decide by some time $T_A$, and they decide $0$.
• Scenario B: all inputs $1$ and $P$ initially dead. The processors of $Q$ decide $1$ by some time $T_B$.
• Scenario C: all processors alive, $P$ starting with $0$ and $Q$ with $1$, and messages between the groups held back past a time $T$. Up to time $T$, every processor of $P$ is in the same state as in Scenario A, and every processor of $Q$ in the same state as in Scenario B.

Significance

The result. Theorem 4.3 shows that the resiliency $N \ge 2t + 1$ of the paper's fail-stop and omission protocols (Theorems 4.1 and 4.2) is optimal. It holds even under three restrictions: binary values, weak unanimity, and processors in perfect lock-step. Partial synchrony costs a majority of correct processors, whereas full synchrony costs nothing. The same scenarios give the authenticated Byzantine bound $N \ge 3t + 1$ (Theorem 4.4). The halting remark of Section 4.2 rests on an argument of the same kind.

The formalization. The theorem is proved in the paper, and its proof is short. It is not machine-checked anywhere known to the mission. No message-passing model is on the platform. This mission supplies one: a step-level model with buffers, per-message timing, fail-stop faults and both partially synchronous communication models. It also gives a machine-checked impossibility on top of that model. FLP, Theorem 4.4 and the lower bounds of Section 6 are natural follow-ups on the same definitions.

Difficulty

The informal proof is an indistinguishability argument. Making it formal means comparing different runs of the same deterministic protocol. Two points need care.

First, the scenarios must be allowed runs. Scenario C holds messages between the groups back past $\max(T_A, T_B)$. With delta unknown, this needs a $\Delta$ larger than that delay. When $\Delta$ holds eventually, $\Delta$ is fixed before the protocol, and the protocol fixes $T_A$ and $T_B$. So the delay is legal only for messages sent before the global stabilization time, which must therefore be placed after $\max(T_A, T_B)$. Read literally, "every message between the groups takes more than $\max(T_A, T_B)$ steps" is not an allowed run in this model.

Second, "the processors of $P$ act exactly as they do in Scenario A" is a claim about whole runs. Two runs must agree on states, on which messages are in which buffer, and on when each message is delivered, tick by tick up to $T$. With one-to-one sends and atomic steps, "delivered in exactly time 1" also needs a reading: a processor that sends at the next tick cannot receive at that tick.

Formalization scope

All declarations live in the namespace DLSConsensus.LowerBound. Processor $p_i$ is the index $i - 1$ of Fin N. Values are Bool. The protocol's state type and message type are arbitrary types in Type, finite or infinite. R.state i n is the state after tick $n$. A message instance is identified in the run by its sender and send tick. A Receive hands the protocol each delivered message as (sender, content); the absolute send tick is not exposed.

Explicit readings and conventions:

• "Fail-stop or omission faults": the goal is the fail-stop impossibility. It implies the omission case, because a fail-stop processor looks to the others like one whose sends are all omitted. The omission case is not a separate item.
• A fail-stop processor may skip ticks before its final stop. The processor timing bound $\Phi = 1$ applies to correct processors.
• "Decides": the first state that records a decision. Irreversibility therefore holds by definition.
• "Delivered in exactly time 1": the message is delivered no later than the addressee's first Receive at least one tick after the send.
• "Within time $T_A$" and "for some finite $T_B$": an explicit $\exists$ before the decision bound.
• "Messages between the groups take more than $\max(T_A, T_B)$ steps": no message between the groups is delivered at a tick $\le T$, for any given $T$.
• "Act exactly as they do": equal local states at every tick $n \le T$.
• Quantifier order: when $\Delta$ holds eventually, $\Delta$ is chosen first, then the protocol, then the run with its stabilization time. When delta is unknown, the protocol is chosen first and each run carries its own $\Delta$. In both models $\Delta > 0$.

Trivializing formalizations are ruled out. The model has allowed runs for every protocol, so Resilient is never vacuously true. Correct processors step at every tick, so termination does not fail for the wrong reason. Unanimity is the weak form, applied only when no processor is faulty.

Contributions welcome: a general simulation lemma (equal inputs up to a tick give equal states up to that tick), the construction of runs from a delivery schedule, and proofs of the scenarios. These parts are reusable for the other lower bounds of the paper.

Selected references

• C. Dwork, N. Lynch, L. Stockmeyer, Consensus in the presence of partial synchrony, Journal of the ACM 35(2), 1988, 288–323. https://doi.org/10.1145/42282.42283
• M. J. Fischer, N. A. Lynch, M. S. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM 32(2), 1985, 374–382. https://doi.org/10.1145/3149.214121
• D. Dolev, C. Dwork, L. Stockmeyer, On the minimal synchronism needed for distributed consensus, Journal of the ACM 34(1), 1987, 77–97. https://doi.org/10.1145/7531.7533

Motivation

The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph, its 1-skeleton. Whether this number is bounded by a polynomial in the dimension $d$ and the number of facets $n$ is a long-standing open question in polyhedral combinatorics; edge walks are the moves of vertex-following methods such as the simplex method, so the question bounds what any such method can achieve in the worst case. For fixed dimension, Larman proved in 1970 that the diameter grows at most linearly in $n$, with a constant exponential in $d$ (Larman 1970).

Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry of polyhedra such upper bounds actually use. They isolate a single combinatorial path property shared by the graphs of non-degenerate polyhedra and announce that the known upper bounds, Larman's among them, "continue to hold in the base abstraction" defined by that property (Dagstuhl abstract, p. 3). The next sentence of the abstract reads: "While the first bound is merely an adaption of the proof in [13], our proof of the second bound is much simpler than the one which was proved for polyhedra in [16]."

The held source is the five-page Dagstuhl extended abstract dated June 15, 2010, which states the results and proves none of them. The full proofs appear in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted theorem of the paper, not an open conjecture; the formal proof remains to be supplied.

Setting

Let $[n]=\{1,\ldots,n\}$ and write $\binom{[n]}{d}$ for the family of its $d$-element subsets. A graph $G=(V,E)$ in the base abstraction has a nonempty vertex set $V\subseteq\binom{[n]}{d}$: every vertex is a $d$-element set of labels, and distinct vertices carry distinct sets. The edges are arbitrary subject to condition i): for each $u,v\in V$ there exists a path connecting $u$ and $v$ whose intermediate vertices all contain $u\cap v$. Condition i) makes $G$ connected. The class of all such graphs is $\mathcal B_{d,n}$; $d$ is called the dimension and $n$ the number of facets of the abstraction, and $D(d,n)$ denotes the largest diameter of a graph in $\mathcal B_{d,n}$ (p. 2).

The distance $\operatorname{dist}_G(u,v)$ is the least number of edges of a path from $u$ to $v$. The motivating example is the graph of a non-degenerate polyhedron (each vertex on exactly $d$ facets), each vertex labelled by its $d$ facets: two vertices are joined by a path inside the minimal face containing both, and every vertex of that path lies on the facets the two endpoints share (pp. 2–3). The class $\mathcal B_{d,n}$ is not restricted to such graphs.

Formalization targets

Larman's bound in the base abstraction

The abstract prints the bound as $\Delta_u(d,n)\le 2^{d-1}\cdot n$ and states that it continues to hold in the base abstraction. The target is the pointwise form of $D(d,n)\le 2^{d-1}\, n$:

$$\forall d\ge 1,\ \forall n,\ \forall G\in\mathcal B_{d,n},\ \forall u,v\in V(G):\qquad \operatorname{dist}_G(u,v)\le 2^{d-1}\, n .$$

In Lean this is the existence, for every pair $u,v$, of a walk from $u$ to $v$ with at most $2^{d-1}n$ edges. The statement quantifies over every graph satisfying the paper's definition, not over polyhedron graphs or a chosen family.

Significance

For fixed $d$ the bound is linear in $n$, and it holds for a class defined only by finite sets and one path condition. Together with the almost-quadratic lower bound $D(n/4,n)=\Omega(n^2/\log n)$ announced in the same paper, it shows what this one property of polyhedra can and cannot deliver: linear growth in $n$ for fixed dimension, but not a linear bound uniform in $d$ and $n$. Since the graph of every non-degenerate polyhedron lies in $\mathcal B_{d,n}$ (a separate mission of this series), the result also recovers a Larman-type bound for polyhedra, with constant $2^{d-1}$.

Prove2Me already has proved polytope versions: Hirsch.larman_bound (the sharper constant $n\,2^{d-3}$ for nonempty bounded $H$-polytopes), Hirsch.larman_high_dimension, Hirsch.larman_layer_recursion, and Hirsch.tight_row_interval, the polytope form of the interval property that condition i) abstracts. They concern a different object, the vertex-edge graph of an $H$-polytope, and are credited as prior work; none states the bound for every graph of $\mathcal B_{d,n}$. The platform definition Hirsch_clf (connected layer families) is a related abstraction in layered form and is not the graph class used here.

Difficulty

The class contains graphs with no geometric realization, so a proof cannot use convexity, faces as polyhedra, or linear-algebraic facts about vertices; only labels, intersections and walks are available. Condition i) guarantees a path preserving the common labels of two endpoints, but says nothing directly about the length of that path. Mere connectivity on $d$-subsets of $[n]$ gives only the trivial bound $|V|-1\le\binom{n}{d}-1$, which is far from linear in $n$. A linear bound in $n$ has to be extracted from condition i) alone, uniformly over all graphs of the class. The abstract describes its proof only as much simpler than Larman's for polyhedra and states no intermediate lemma, so the mission carries no milestones.

Formalization scope

• $[n]$ is represented by Fin n, labels $0,\ldots,n-1$; only the number of labels matters.
• A vertex set is V : Finset (Finset (Fin n)) and the graph is G : SimpleGraph V; vertices are therefore distinct label sets, as in the paper. InB d n V G requires V.Nonempty, every vertex of cardinality $d$, and CondI V G.
• CondI asks for a walk all of whose vertices contain $u\cap v$. This is the source's path condition: a walk contains a path on a subset of its vertices, and the endpoints contain $u\cap v$ automatically.
• "Continue to hold in the base abstraction" is read as the bound for every graph of $\mathcal B_{d,n}$ and every pair of its vertices. No numeric $D(d,n)$ is defined, so no supremum with a default value enters; a bounded walk witnesses the distance bound.
• $d\ge 1$ is an explicit hypothesis: $d$ is the dimension, and it makes $d-1$ ordinary subtraction in $\mathbb N$. At $d=0$ the class consists only of the one-vertex graph on $\emptyset$, so nothing is lost. For $n<d$ the class is empty.
• The constant is $2^{d-1}$, the paper's constant for the abstraction; the polytope constant $2^{d-3}$ of Hirsch.larman_bound is not claimed here.

Trivializing formalizations are ruled out: labels are the vertices themselves (not an arbitrary labelling that could repeat), and condition i) is required for all pairs, not for one chosen path or only adjacent vertices. A proof only for polyhedron graphs, for graphs with extra structure, or with a larger constant leaves the goal open. Useful contributions include general lemmas about CondI and walk-length bookkeeping for SimpleGraph on a finite vertex type; these are reusable by the other missions of this series.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211 (Flexible Network Design), 2010. https://drops.dagstuhl.de/opus/volltexte/2010/2724
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35(4), 786–794, 2010. https://doi.org/10.1287/moor.1100.0470
• D. G. Larman, Paths on polytopes, Proceedings of the London Mathematical Society (3) 20, 161–178, 1970. https://doi.org/10.1112/plms/s3-20.1.161