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

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

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

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

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

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

Online bipartite matching models decisions that must be made as requests arrive: an advertiser can be assigned to a compatible request once, and an assignment cannot be revised when later requests reveal a better alternative. Display advertising is the motivating example in Feldman, Mehta, Mirrokni, and Muthukrishnan's 2009 preprint: an ad server knows which advertisers accept each kind of impression and has estimates of how frequently those kinds will arrive. The question is how much this advance distributional information helps when decisions still have to be immediate.

This mission studies the paper's first offline-guided algorithm. It computes a maximum matching for the expected traffic and follows that matching during the actual random run. The paper shows that this natural policy reaches the familiar $1-1/e$ performance level and that its own analysis cannot be improved for this policy, even if performance is averaged over runs. The result sets the baseline for the paper's later two-suggested-matchings algorithm, which improves on that level under its stated assumptions. Feldman et al., §§1 and 4.1

Setting

An instance consists of a finite advertiser set $A$, a finite impression-type set $I$, and allowed edges $E\subseteq A\times I$. For each type $i$, the nonnegative integer $e_i$ is its expected number of arrivals. There are $n=\sum_{i\in I}e_i>0$ arrivals. Each arrival independently has type $i$ with probability $e_i/n$. A type with $e_i=0$ remains in the graph but has zero arrival probability. On an arrival of type $i$, an online algorithm may assign it to an adjacent advertiser that has not been assigned before, or may leave it unassigned. The hindsight optimum, $\mathrm{OPT}(\omega)$, is the largest matching in the realization graph with one vertex for every arrival position, including separate vertices for repeated types. Feldman et al., §2, pp. 3–4

The suggested matching algorithm first selects any maximum integral flow in the expected-instance network. Each advertiser has capacity one, and each type $i$ has capacity $e_i$. Equivalently, the selected edges form a maximum degree-capped bipartite matching $M\subseteq E$. Let $A^*$ be the advertisers covered by $M$. When type $i$ arrives, the algorithm chooses each advertiser joined to $i$ by a selected edge with probability $1/e_i$; any remaining probability chooses no advertiser. It assigns the chosen advertiser if available and otherwise makes no assignment. Its number of assignments is $\mathrm{ALG}(\omega)$. This rule includes the algorithm's random choice in addition to the random arrival types. Feldman et al., §4.1, p. 5

The canonical residual cut of $M$ places each advertiser and impression type on the source side if it is reachable from the source by residual edges. Write $A_T$ for advertisers on the sink side and $I_S$ for types on the source side. These sets describe the comparison between the expected-instance matching and the optimum of a realized run. The mission also uses occupancy: after $n$ independent uniform throws into $n$ bins, count how many bins in a fixed subset receive at least one ball. Feldman et al., §§2.1 and 4.1

Formalization targets

Theorem 4's general-instance guarantee is expressed in the additive form established by its analysis. For every $\varepsilon>0$, there are $\delta>0$ and $N$, uniform across all finite instances, all maximum integral flows, and all valid ways of realizing the algorithm's random choice, such that $n\ge N$ implies

The complete bipartite family gives the tightness target. When $A=I=\{0,\ldots,n-1\}$ and every $e_i=1$, every maximum expected-instance matching is perfect. For every run, $\mathrm{OPT}=n$, and

The milestone list follows the paper's Fact 1 and the named passages “Bounding ALG,” “Bounding OPT,” and “Tightness of the Analysis” in §4.1. The cut identity $|A^*|=|A_T|+\sum_{i\in I_S}e_i$ is a separate deterministic milestone. Feldman et al., Theorem 4 and §4.1, pp. 5–6

Significance

The result establishes exactly what this one-matching policy achieves under integer-frequency independent arrivals. It gives a guarantee for the actual number of assignments relative to the best assignment made with hindsight, and a family on which the limiting expected ratio equals the guarantee. That tight family explains why the paper introduces a second suggested matching rather than seeking a stronger bound for the same policy. Feldman et al., §4

The mathematical theorem is proved in the paper; the mission asks for its machine-checked formalization. The development would also provide reusable finite models of repeated-type realizations, integral degree-capped bipartite matchings, uniform occupancy, and residual reachability cuts. No machine-checked proof of these mission items is being claimed by this draft.

Difficulty

The expected-instance matching is selected before the arrivals, but the hindsight optimum can exploit the actual multiplicities of every type. Counting only the ads selected online does not compare the algorithm with that hindsight optimum. Also, a type may have several selected advertisers when $e_i>1$, so replacing the algorithm's random choice by a deterministic designated ad would change its law. The cut and concentration statements have to apply uniformly to every maximum integral flow, including flows chosen by different tie-breaking rules. Feldman et al., §4.1, pp. 5–6

Formalization scope

Advertisers and types are finite Lean types. The edge relation is a finite set, and $e_i$ and $n$ are natural numbers with $n=\sum_i e_i>0$. An integral maximum flow is represented by a maximum cardinality edge set with advertiser degree at most one and type-$i$ degree at most $e_i$. The theorem quantifies over every such set. This is the unit-advertiser, integer-type-capacity flow used in §4.1, without a separate real-valued flow object. The canonical cut is defined through residual reachability. The hindsight optimum maximizes over matchings of the realized graph, with each arrival position distinct.

The run uses $n$ independent uniform draws from $\sum_i\{0,\ldots,e_i-1\}$. A valid labelling assigns each selected advertiser at type $i$ to a distinct copy. The drawn copy determines the type and, if labelled, the ad selected by the algorithm. This gives type probability $e_i/n$, conditional ad probability $1/e_i$ on selected edges, and the remaining “no ad” probability. Counts, probabilities, and expectations use finite sums, so there is no integrability convention. Since $n>0$, the run sample space is nonempty; no value of $\mathrm{ALG}/\mathrm{OPT}$ at $\mathrm{OPT}=0$ is needed. The complete-graph family has $n\ge1$.

The paper writes $1-e^{-\Omega(n)}$ in both bounding passages. The Lean statements spell this out as $\forall\varepsilon>0,\ \exists\delta>0,\ \exists N,\ \forall$ instances with $n\ge N$, with $\delta,N$ preceding the instance. Theorem 4's ratio language is represented by the additive estimate its proof yields; a vanishing ratio error requires a separate lower bound on $\mathrm{OPT}/n$. The exact finite-$n$ expectation and its limit make “tight, even in expectation” precise. The printed Fact 1 exponent is $\varepsilon n/2$, while its Appendix A proof yields $\varepsilon^2n/2$; the formalized concentration statement uses the proved exponent and the milestone retains the printed wording. Neither a ratio with a zero denominator nor a labelling that changes the algorithm's choice law is accepted as a shortcut.

Contributions toward the occupancy bound, the residual cut identity, the realized matching bound, and the complete-graph expectation are welcome. The finite occupancy and matching interfaces are intended for reuse beyond this specific algorithm.

Selected references

• Jon Feldman, Aranyak Mehta, Vahab Mirrokni, and S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, arXiv:0905.4100v1, 2009; FOCS 2009. Preprint

Motivation

Consensus asks $N$ processors, each starting with a value, to agree on one value although some of them may be faulty. It underlies replicated databases, atomic commitment and state-machine replication. Two classical models bracket the problem. In a fully synchronous system, with known bounds on message delay and processor speed, consensus is solvable for many fault types. In a fully asynchronous system, Fischer, Lynch and Paterson showed in 1985 that no deterministic protocol tolerates even one fail-stop fault (FLP, J. ACM 1985).

Dwork, Lynch and Stockmeyer (J. ACM 35(2), 1988, 288–323) introduced partial synchrony between these extremes: message delays are bounded, but either the bound is unknown, or it holds only from an unknown global stabilization time (GST) on. This model, and the GST abstraction in particular, became the standard assumption under which practical consensus protocols (Paxos-style and Byzantine fault-tolerant replication) are proved live. The paper determines, for each fault type, the largest number $t$ of faults that consensus can tolerate under partial synchrony. This mission formalizes its first positive result: for fail-stop and omission faults, $N \ge 2t+1$ processors suffice.

Setting

There are $N$ processors $p_1,\dots,p_N$, an integer $t \le N$, and an arbitrary set $V$ of values; processor $p_i$ starts with $\mathrm{init}(p_i)\in V$.

In the basic round model (Section 3.1 of the paper), computation proceeds in rounds $r = 1, 2, 3, \dots$. In each round every processor sends messages, each message is either delivered in that round or lost, and every processor then performs a state transition on the messages it received. Losses are described by a predicate $\mathrm{deliv}(r,q,p)$. A set $C$ of processors (the correct ones) and a round $\mathrm{GST}$ constrain it: every message sent at a round $r \ge \mathrm{GST}$ from a processor of $C$ to a processor of $C$ is delivered. Before GST any message may be lost, and messages from or to processors outside $C$ may be lost at any time. Processors outside $C$ follow the protocol but lose sends and receptions (omission faults, which include fail-stop faults).

Algorithm 1 (Section 3.2.1) works as follows. Every processor keeps a set $\mathrm{PROPER}$, initially $\{\mathrm{init}(p)\}$, attaches it to every message, and merges in every PROPER set it receives. A processor may hold locks, each a value with an associated phase number; $v$ is acceptable to $p$ if $p$ has no lock on a value other than $v$. Phase $k \ge 1$ belongs to $p_i$ when $k \equiv i \pmod N$. Trying phase $k$ occupies rounds $4k-3$, $4k-2$, $4k-1$:

1. every processor sends the owner the list of its acceptable values that are in its PROPER set; the owner proposes, by an arbitrary choice, a value appearing in at least $N-t$ of the lists received, if there is one;
2. the owner broadcasts $(\mathrm{lock}\ v, k)$; each receiver locks $v$ with phase $k$;
3. each receiver acknowledges; with at least $t+1$ acknowledgements the owner decides $v$.

Lock-release phase $k$ is round $4k$: every processor broadcasts its locks $(v,h)$, and a lock on $v$ with phase $h$ is released on receipt of some $(w,h')$ with $w \ne v$ and $h' \ge h$.

The correctness conditions (Section 2.4) for the set $C$ are consistency (no two decisions of processors in $C$ differ), termination (every processor in $C$ decides), and strong unanimity (if all $N$ initial values equal $v$, every decision in $C$ is $v$).

Formalization targets

Goal: Theorem 3.1

For all $N, t$ with $N \ge 2t+1$, every value type $V$, all initial values, every $C$ with $|C| \ge N-t$, every $\mathrm{GST}$, every delivery pattern allowed for $C$ and $\mathrm{GST}$, and every admissible choice of proposals,

This is the theorem as printed; it fixes no constants.

Milestones

• Lemma 3.1: no two distinct values acquire locks with the same associated phase.
• Lemma 3.2: if $v$ is decided at the first phase $k$ at which any decision is made, then at least $t+1$ processors lock $v$ at phase $k$, and each keeps, from then on, a lock on $v$ with phase at least $k$.
• Lemma 3.3: immediately after a lock-release round $4k \ge \mathrm{GST}$, the processors of $C$ together hold locks on at most one value.
• Round bound (Section 3.2.1, p. 298): every processor of $C$ decides at some phase $k$ with

Significance

Theorem 3.1 shows that, against omission and fail-stop faults, partially synchronous communication costs nothing in resilience compared with a majority bound: $N \ge 2t+1$ suffices, and Section 4 of the paper shows that $N \le 2t$ does not. The lock-and-release structure of Algorithm 1 (a value is decided only after a quorum locks it, and locks are released only on evidence of a later competing lock) recurs in later partially synchronous protocols, where safety must hold regardless of timing and liveness is obtained only after stabilization. The result separates the two concerns cleanly: consistency and strong unanimity hold in every run, while termination uses GST.

The result is proved in the paper; to the best of the available information it has not been formalized in Lean, and no distributed-computing model exists on Prove2Me. The mission produces a machine-checked model of the basic round model with a GST delivery guarantee, a full executable specification of Algorithm 1, and proofs of its safety and liveness. The paper's own proof of Lemma 3.3 is one line and the termination argument relies on "sufficient communication"; a formal proof must make these steps explicit.

Difficulty

The safety argument is an invariant over an unbounded number of phases with an arbitrary loss pattern: a lock on the decided value must be shown never to be released without being replaced by a higher lock on the same value, while competing locks on other values may exist at faulty or slow processors. The obvious argument ("after a decision, every later proposal must equal the decided value") is circular without a persistence statement for locks such as Lemma 3.2. Liveness requires reasoning about what every correct processor knows after GST (its PROPER set and the locks of the others), and it depends on processors sending lock-release and list messages even when these carry no locks or no acceptable values. Quorum counting with $N-t$ and $t+1$ must be carried out over distinct senders.

Formalization scope

• Processors are Fin N; the paper's $p_i$ is the processor of index $i-1$. Rounds start at $1$; exec … 0 is the initial state and exec … r the state after round $r$. Phases start at $1$.
• The paper's "chooses one arbitrarily" is a parameter pick : ℕ → Set V → V, required only to pick an element of every nonempty candidate set, and universally quantified in every theorem.
• The paper's "the behavior of the processors not in $C$ is allowed by the fault type $F$" is read as: processors outside $C$ run Algorithm 1, and any message from or to them may be lost (omission faults, containing fail-stop).
• The GST guarantee covers a processor's messages to itself when it is in $C$; before GST self-messages may be lost like any other.
• Every processor sends its list in round $4k-3$ and its lock-release message in round $4k$ even when they are empty, since both carry the PROPER set (Section 3.2: PROPER sets are piggybacked on all messages).
• A decision is the event DecidesAt p k v (owner of phase $k$, proposed $v$, at least $t+1$ acknowledgements in round $4k-1$); consistency requires all such events of processors in $C$ to agree.
• "Decide by round $\mathrm{GST}+4(N+1)$" is read as: the deciding phase $k$ satisfies $4k-1 \le \mathrm{GST}+4(N+1)$.
• Not formalized: Remark 1's asymptotic claims, the PROPER simplifications for weak unanimity, Algorithms 2 and 3.

A formalization in which a run cannot exist, the delivery constraint is unsatisfiable, the choice of proposals is fixed, or faulty processors are absent ($C$ = all processors) would trivialize the theorem; the model here admits runs in which processors decide, and $C$ ranges over all sets of at least $N-t$ processors.

Reusable beyond this mission: the round-based message-passing model with a GST delivery guarantee and omission faults. Contributions of general lemmas about runs (monotonicity of PROPER sets, persistence of locks, quorum intersection over Finset) are welcome.

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

Motivation

The single-machine scheduling problem $1|\mathrm{prec}|\sum w_j C_j$ asks for an order in which to process $n$ jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for general precedence constraints is $2$. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) relate the problem to the dimension theory of partial orders: their Theorem 3.2 states that when the precedence constraints are given together with a realizer of size $k$, the problem has a $(2 - 2/k)$-approximation algorithm. Small realizers of structured precedence orders therefore translate directly into better approximation ratios.

This mission formalizes one such structural result, Lemma 4.1 of the paper: every convex bipartite order has a realizer of size $3$. Convex bipartite orders form a class of precedence constraints that lies strictly between strong bipartite orders and general bipartite orders (Möhring, 1989). Combined with Theorem 3.2, the lemma gives a $4/3$-approximation for $1|\mathrm{prec}|\sum w_j C_j$ on this class. According to the authors, the bound $\dim \le 3$ for convex bipartite orders had not been known before.

Setting

A poset is a set $N$ with a reflexive, antisymmetric, transitive relation $P$. Two elements $x, y$ are incomparable, written $x \parallel y$, when neither $(x,y) \in P$ nor $(y,x) \in P$; the set of incomparable pairs is $\mathrm{inc}(P)$. A linear extension of $P$ is a linear order $L$ on $N$ with $P \subseteq L$. A linear order $L$ reverses the pair $(x,y)$ when $y < x$ in $L$. A realizer of size $t$ is a family $L_1, \dots, L_t$ of linear extensions of $P$ such that every incomparable pair $(x,y)$ is reversed by at least one $L_i$. The dimension $\dim(P)$ is the least $t$ for which a realizer of size $t$ exists.

A convex bipartite order has jobs $N = J^- \cup J^+$ split into minus jobs $J^- = \{j_1, \dots, j_a\}$ and plus jobs $J^+ = \{j_{a+1}, \dots, j_n\}$. Each plus job $j_k$ carries two indices $1 \le l(k) \le r(k) \le a$, and a minus job $j_i$ precedes $j_k$ exactly when $l(k) \le i \le r(k)$. There are no other precedences: the predecessors of each plus job form a nonempty interval of consecutive minus jobs.

For the Appendix construction, the incomparable pairs are sorted into three sets $E_1, E_2, E_3$ according to the kinds of the two jobs, the order of their indices and, for a pair (plus job $j_i$, minus job $j_j$), whether $j_j$ precedes some plus job of larger index than $i$. The sets $\bar E_m = E_m \cup P$ describe what the $m$-th linear order of the realizer must contain.

Formalization targets

Goal: Lemma 4.1

Equivalently, $\dim(P) \le 3$. The goal holds for every numbering of the jobs and every choice of interval ends $l, r$.

Milestones

• Lemma A.1. $E_1, E_2, E_3$ partition $\mathrm{inc}(P)$, and for each $m$, $(x,y) \in E_m$ implies $(y,x) \notin E_m$.
• Lemma A.2. Under the Appendix's numbering of the plus jobs ($i < j$ implies $l(i) \le l(j)$), each $\bar E_m$ is contained in a linear order on $N$.

Significance

The result. Lemma 4.1 places convex bipartite orders among the classes of precedence constraints for which $1|\mathrm{prec}|\sum w_j C_j$ has an approximation ratio strictly below $2$, namely $4/3$ through Theorem 3.2 of the paper. The bound is tight: a bipartite order has dimension $2$ exactly when it is a strong bipartite order (Möhring), so the bound $3$ cannot be lowered for the class of convex bipartite orders. Since $\dim(P) = 3$ also gives $\chi(G_P) = 3$ for the graph of incomparable pairs, a $3$-realizer yields an optimal colouring of that graph.

Formalizing it. The result is proved in the paper, with a short case analysis in the Appendix. No machine-checked proof is known to exist. Mathlib has no dimension theory of posets: realizers, reversals of incomparable pairs and the construction of linear extensions containing a given acyclic relation have to be set up here. The definitions of realizer and linear extension are stated for an arbitrary relation and can be reused for other dimension bounds (interval orders, semiorders, the other missions of this series).

Difficulty

The three relations $\bar E_m$ are not partial orders. $\bar E_2$, for instance, is not transitive: with two minus jobs and one plus job $j_3$ with $l(3) = r(3) = 2$, the pairs $(j_1, j_2) \in E_2$ and $(j_2, j_3) \in P$ are present but $(j_1, j_3)$ lies in $E_1$. The step that requires work is to show that each $\bar E_m$ has no cycle, so that it extends to a linear order. For $\bar E_2$ this depends on the convexity of the predecessor intervals and on the numbering of the plus jobs by their left ends: it is not a consequence of bipartiteness alone. The goal itself carries no numbering assumption, so any proof must also account for renumbering the plus jobs.

Formalization scope

All declarations live in the namespace SingleMachinePrec.ConvexBipartite.

• Relations. A relation on $N$ is a predicate N → N → Prop. Linear orders use Mathlib's unbundled class IsLinearOrder. A linear extension of $P$ is a linear order $L$ with $P \subseteq L$; $L$ reverses $(x,y)$ when $L\,y\,x$ and $y \ne x$. A realizer of size $t$ is a function Fin t → N → N → Prop, so repeated members are allowed, as in the paper's multisets.
• Convex bipartite orders. The jobs are the type Fin a ⊕ Fin b: Sum.inl i is the minus job $j_{i+1}$, Sum.inr k the plus job $j_{a+k+1}$, with indices starting at $0$. The interval ends are maps l r : Fin b → Fin a with l k ≤ r k, and $P$ is equality together with the pairs (minus $i$, plus $k$) with $l(k) \le i \le r(k)$. A file-level instance records that $P$ is a partial order. Any convex bipartite order in the paper's sense is one of these after naming its jobs. The cases $a = 0$ and $b = 0$ are allowed.
• $E_1, E_2, E_3$. Each set is defined as "incomparable and satisfies the paper's case condition". In the plus–minus clauses, "$k > i$" compares plus indices, because $k$ exceeds the index of a plus job.
• Lemma A.2. "$\bar E_m$ is an extension of $P$" is formalized as "there is a linear order containing $\bar E_m$", which is what the paper's proof establishes (absence of cycles) and what its final paragraph uses. Reading it as "$\bar E_m$ is a partial order" would make the lemma false (see Difficulty). The Appendix's numbering assumption is the hypothesis Monotone l of this milestone only.
• Algorithmic wording not formalized. The paper states Lemma 4.1 as "a realizer of size 3 can be computed in polynomial time". What is formalized is the existence of the realizer; the running time is not.

A trivializing formalization would let the members of the realizer be arbitrary relations, which makes reversing every pair free. Here every member must be a linear order containing $P$.

Contributions welcome: proofs of the two milestones and of the goal; a general lemma that a relation whose transitive closure is antisymmetric extends to a linear order on a finite type; and the renumbering argument that removes the numbering assumption.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992.
• R. H. Möhring, Computationally tractable classes of ordered sets, in I. Rival (ed.), Algorithms and Order, NATO ASI Series 255, Kluwer, 1989, pp. 105–193.
• W. T. Trotter, Combinatorics and Partially Ordered Sets: Dimension Theory, Johns Hopkins University Press, 1992.