Completed

Mechanism Design·Captain: Shuze Chen

Algorithmic Game Theory III: Arrow and Gibbard–SatterthwaiteTextbook

Algorithmic Game Theory III: Arrow and Gibbard–Satterthwaite

Motivation

Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard (1973) and Satterthwaite (1975) showed the voting analogue: any non-dictatorial voting rule onto three or more candidates can be strategically manipulated. These two results frame all of mechanism design — they are the reason Chapter 9 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), this mission's source, introduces money and quasilinear utilities immediately after proving them: without transfers, incentive compatibility is an impossibility, not a design constraint.

A timeline: Arrow proved the aggregation impossibility in his 1951 monograph Social Choice and Individual Values; Gibbard (1973) established the manipulability of non-dictatorial voting schemes via game forms, Satterthwaite (1975) independently via a direct argument; the derivation of Gibbard–Satterthwaite as a corollary of Arrow's theorem, which the book follows and this mission adopts as its attack path, is standard since the 1970s.

Setting

Fix a finite set $A$ of alternatives (candidates) and a finite set $\iota$ of voters. A preference is a strict total order on $A$ ; we write the relation as $r(a,b)$ , read " $a$ is strictly preferred to $b$ " (the book writes $b \prec a$ ). A preference profile assigns a preference to each voter. A social welfare function $F$ maps profiles to a social preference; a social choice function $f$ maps profiles to a single chosen alternative (Definition 9.1).

The properties at stake (Definitions 9.2, 9.4, 9.5, 9.7):

$F$ satisfies unanimity if on every profile where all voters hold the identical preference $r$ , the social preference is $r$ .
$F$ satisfies independence of irrelevant alternatives (IIA) if the social preference between $a$ and $b$ depends only on the voters' preferences between $a$ and $b$ .
Voter $i$ is a dictator in $F$ if the social preference always equals $i$ 's; in $f$ , if $f$ always elects $i$ 's top alternative.
$f$ is incentive compatible if no voter, by misreporting, can obtain an outcome they strictly prefer (under their true preference) to the truthful outcome; $f$ is monotone if whenever a single voter's change of vote moves the outcome from $a$ to $a' \ne a$ , that voter ranked $a$ above $a'$ before and $a'$ above $a$ after.
$f$ is onto if every alternative is elected on some profile.

Formalization targets

Goal (capstone) — Theorem 9.8, Gibbard–Satterthwaite

|A| \ge 3,\ f \text{ incentive compatible and onto } A \implies f \text{ is a dictatorship.}

Theorem 9.3 — Arrow

|A| \ge 3,\ F \text{ a social welfare function satisfying unanimity and IIA} \implies F \text{ is a dictatorship.}

Proposition 9.6 — incentive compatibility = monotonicity

f \text{ is incentive compatible} \iff f \text{ is monotone},

with no cardinality or finiteness assumptions: the two properties are quantifier-for-quantifier the same data viewed twice.

Significance

These are the two foundational impossibility theorems of social choice, and the pivot of the whole mechanism-design part of this series: the VCG mission that follows exists because Gibbard–Satterthwaite closes the door on non-trivial strategyproof choice without money. The chapter derives Gibbard–Satterthwaite from Arrow through the top-set extension (Definition 9.9, Lemmas 9.10–9.11), so a solver of the capstone gets Arrow as a stepping stone, not a detour.

Formalizing them produces the platform's first social-choice library: preference profiles as strict total orders, the aggregation vocabulary, and the impossibility pair. Arrow's theorem has been formalized before in other proof assistants (Nipkow's Isabelle formalization, 2009; a Mizar formalization by Wiedijk), which is evidence the statement shapes here are the standard ones — but no Lean 4/mathlib formalization exists, and none on this platform.

Difficulty

The proofs are short on paper and famously slippery in the details. Arrow's proof (the book gives Geanakoplos's pairwise-neutrality route) is a sequence of profile surgeries: each step swaps one voter's ranking of a pair and tracks the social outcome through IIA; the formal cost is constructing the intermediate profiles and proving they remain strict total orders — pure bookkeeping, but a lot of it. The hybrid-profile argument needs, over three or more alternatives, custom orders placing chosen pairs at chosen positions; building these on an abstract finite type is where most of the work lies. For the capstone, the book's route through the top-set extension $\prec^S$ (move $S$ to the top, Definition 9.9) requires proving the extension is again a strict total order (Lemma 9.10) and inherits unanimity, IIA, and non-dictatorship (Lemma 9.11); a solver may equally take any direct proof of Gibbard–Satterthwaite — the statement fixes no route. Proposition 9.6 is a genuine warm-up: unfolding both definitions and rearranging quantifiers.

Formalization scope

Preferences are relations A → A → Prop carrying IsStrictTotalOrder; r a b means " $a$ is strictly preferred to $b$ ", the reverse of the book's $\prec$ — every definition's docstring states this orientation. Aggregators are total functions on all relation-valued profiles; every property quantifies only over genuine preference profiles, so behavior on invalid inputs is irrelevant, and nothing can be smuggled through junk inputs. Unanimity is the book's identical-profile form (Definition 9.2), which together with IIA yields the pairwise form used in proofs. Both alternatives and voters are finite types; |A| ≥ 3 enters as 2 < Fintype.card A. Arrow's theorem carries Nonempty ι, matching the book's setting of $n \ge 1$ voters; it is not needed for truth — with zero voters the identical-profile unanimity is already unsatisfiable over three or more alternatives, so that case is vacuous either way. Gibbard–Satterthwaite deliberately omits it: with zero voters ontoness onto three alternatives is unsatisfiable, and the statement holds vacuously. Dictatorship for choice functions is Definition 9.7 exactly: whenever some alternative is the dictator's unique maximum, it is elected.

Selected references

K. J. Arrow, Social Choice and Individual Values, Wiley, 1951 (2nd ed. 1963). Link
A. Gibbard, Manipulation of voting schemes: a general result, Econometrica 41 (1973), 587–601. DOI
M. A. Satterthwaite, Strategy-proofness and Arrow's conditions, Journal of Economic Theory 10 (1975), 187–217. DOI
J. Geanakoplos, Three brief proofs of Arrow's impossibility theorem, Economic Theory 26 (2005), 211–215. DOI
T. Nipkow, Social choice theory in HOL: Arrow and Gibbard–Satterthwaite, J. Automated Reasoning 43 (2009), 289–304. DOI
N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 9, §9.2. DOI

4 thms2 active usersReviewed

Completed

Algorithmic Game Theory·Captain: Shuze Chen

Algorithmic Game Theory II: No-Regret Learning and Correlated EquilibriaTextbook

Motivation

Equilibrium concepts are static; play is dynamic. The bridge between the two is regret minimization: simple adaptive rules that, against arbitrary — even adversarial — opponents, perform nearly as well as the best fixed alternative in hindsight. The subject begins with Hannan (1957) and Blackwell (1956), whose consistency theorems predate most of computational learning theory; the modern multiplicative-weights style bounds are due to Littlestone–Warmuth (1994) and Freund–Schapire (1997); the reduction from external to swap regret, and with it the algorithmic route to correlated equilibria, is Blum–Mansour (2005), following Foster–Vohra (1997) and Hart–Mas-Colell (2000). Chapter 4 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Blum and Mansour, is the source text of this mission.

The punchline of the chapter, and of this mission, is that a computationally trivial form of rationality — each player privately running a no-swap-regret algorithm — drives the empirical play of any finite game into an approximate correlated equilibrium (Aumann, 1974). No coordination, no knowledge of the game, no fixed-point computation: the equilibrium concept that Chapter 1 of the series defines through a correlating device is reached by decentralized learning.

Setting

The online model (§4.2): there are $N$ actions. At each time $t$ an online algorithm selects a distribution $p^t$ over actions, as a function of the loss vectors observed so far; then the adversary reveals a loss vector $\ell^t \in [0,1]^N$ and the algorithm suffers $\sum_i p^t_i \ell^t_i$ . Cumulatively, $L_H^T = \sum_{t \le T} \sum_i p^t_i \ell^t_i$ and $L_k^T = \sum_{t \le T} \ell^t_k$ for a fixed action $k$ . The external regret of $H$ is $L_H^T - \min_k L_k^T$ . A modification rule $F : \{1,\dots,N\} \to \{1,\dots,N\}$ rewires the algorithm's play, giving the modified loss $L_{H,F}^T = \sum_t \sum_i p^t_i\, \ell^t_{F(i)}$ ; the swap regret is $L_H^T - \min_F L_{H,F}^T$ over all $N^N$ rules.

A finite game (the vocabulary of Mission I of this series, in loss form): players $\iota$ , finite action sets $S_i$ , cost functions $c_i : \prod_j S_j \to \mathbb{R}$ . A joint distribution $Q$ on action vectors is an $\varepsilon$ -correlated equilibrium (Definition 4.11) if for every player $i$ and every switching rule $F : S_i \to S_i$ ,

\mathbb{E}_{s \sim Q}\big[c_i(s)\big] \;\le\; \mathbb{E}_{s \sim Q}\big[c_i(F(s_i), s_{-i})\big] + \varepsilon.

Formalization targets

Goal (capstone) — Corollary 4.16, explicit form

\forall N, T\ \exists H:\quad \text{swap regret of } H \text{ on every } [0,1]\text{-loss sequence} \;\le\; 2N\sqrt{T \ln N}.

An online algorithm with vanishing per-round swap regret, with the constant the chapter's own route produces.

Theorem 4.6 — Polynomial Weights

L_{PW}^T \;\le\; L_k^T + \eta\, Q_k^T + \frac{\ln N}{\eta}, \qquad Q_k^T = \sum_{t\le T} (\ell^t_k)^2, \quad 0 < \eta \le \tfrac12.

Theorem 4.9 — external regret in constant-sum games

A player with external regret $R$ over $T$ rounds has average loss at most $v_i + R/T$ , where $v_i$ is the game value — no-regret play guarantees the minimax value against any opponent.

Theorem 4.15 — external-to-swap reduction

Any algorithm with external regret $\le R$ on all $[0,1]$ -loss sequences yields one with swap regret $\le N R$ .

Theorem 4.12 — swap regret bounds distance from correlated equilibrium

If every player's swap regret over $T$ steps of mixed play is at most $R$ , the empirical joint distribution is an $(R/T)$ -correlated equilibrium.

Theorem 4.3 — deterministic algorithms fail

Every deterministic algorithm has a $\{0,1\}$ -loss sequence forcing loss $T$ while some action loses at most $\lfloor T/N \rfloor$ : randomization is necessary, not a convenience.

Significance

Correlated equilibrium is the equilibrium concept with a defensible dynamic foundation: Nash equilibria are PPAD-hard to find, but the capstone plus Theorem 4.12 exhibit polynomial-time decentralized dynamics whose empirical play is an $\varepsilon$ -correlated equilibrium after $T = O(N^2 \ln N / \varepsilon^2)$ rounds. Later missions in this series lean on this machinery: the price-of-anarchy chapters bound the cost of no-regret play (not just of exact equilibria), and the routing-game chapter uses precisely the convergence result formalized here.

Formalizing it produces the platform's first online-learning library: the adversarial protocol, regret in both external and swap forms, the multiplicative-weights analysis, and correlated equilibria. The regret vocabulary is directly reusable for the bandit-flavored missions already on the platform. All results are classical, with textbook proofs; the work requested is machine-checked proof, not new mathematics.

Difficulty

The Polynomial Weights bound is a potential-function argument: the total weight $W^t$ falls geometrically with the algorithm's loss and is bounded below by the weight of action $k$ ; the formal work is inequalities for $\ln(1-x)$ on $[0, 1/2]$ and careful bookkeeping of the recursion. The reduction (Theorem 4.15) is the structurally interesting step: the master algorithm runs $N$ copies of the external-regret procedure, feeds copy $i$ the true losses scaled by the master's own probability $p^t_i$ , and — the crux — plays the stationary distribution $p^t = p^t Q^t$ of the column-stochastic matrix assembled from the copies' outputs. Existence of that fixed point is exactly the existence of a stationary distribution of a finite Markov chain, available on this platform as the goal of Markov Chains and Mixing Times I — or provable directly. Theorem 4.12 is an averaging argument, deliberately easy; Theorem 4.3 is an adversary construction; Theorem 4.9 combines the regret bound with the security level the minimax theorem of Mission I supplies, through the opponent's empirical mixture. The capstone is the composition of 4.6 (tuned at $\eta = \min\{\sqrt{\ln N / T}, 1/2\}$ ) with 4.15, plus the arithmetic that turns $N \cdot 2\sqrt{T \ln N}$ into the stated bound.

Formalization scope

An online algorithm is a deterministic function from the observed history (the list of past loss vectors) to the mixed action played next — the standard formal reading of the full-information model; randomization lives in the mixed action, and losses are expected losses. Boundedness of losses ( $[0,1]$ ) is a hypothesis on theorems, never part of a definition. The Polynomial Weights algorithm is defined concretely by its weight recursion, and its learning rate carries the hypothesis $0 < \eta \le 1/2$ : the book writes only $\eta \le 1/2$ , but at $\eta = 0$ the bound's $\ln N / \eta$ term degenerates and the claim is false, so positivity is explicit. Action sets are Fin (n+1), keeping them nonempty. The number of steps $T$ is a known parameter (the book's convention; guess-and-double is out of scope). Correlated equilibria use the switching-rule form of Definition 4.11, over the game vocabulary (IsLottery, IsMixedProfile, profileProb) published with Mission I of this series. In Theorem 4.12 the empirical distribution is the average of product distributions of the played profiles, $T \ge 1$ is required (at $T = 0$ there is no empirical distribution), and costs are not assumed bounded — the averaging is scale-free.

Trivializing readings are ruled out: the existential algorithms in Theorem 4.15 and the capstone are quantified before the loss sequence and the modification rule, so a witness must work uniformly against every adversary — nothing may be chosen with hindsight.

Selected references

A. Blum, Y. Mansour, From external to internal regret, JMLR 8 (2007), 1307–1324. Link
N. Littlestone, M. K. Warmuth, The weighted majority algorithm, Information and Computation 108 (1994), 212–261. DOI
D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. DOI
S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. DOI
N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 4. DOI

7 thms2 active usersReviewed

Quantum Information·Captain: Goku

The Aaronson-Ambainis ConjectureOpen Problem

Motivation

Quantum query algorithms are known to beat classical ones on problems with algebraic structure -- period finding, hidden subgroups, forrelation. No such speedup is known for a problem with no structure at all. Aaronson and Ambainis proposed making that observation into a theorem, and reduced it to a question with no quantum content: a statement about bounded low-degree polynomials on the Boolean cube (Aaronson--Ambainis 2009).

The question has resisted since. A timeline of what is actually established:

2009. Aaronson and Ambainis state the conjecture and prove that it implies almost-everywhere classical simulation of quantum query algorithms.
2012. Montanaro settles the case of block-multilinear forms whose coefficients all have the same magnitude.
2016. O'Donnell and Zhao reduce the general conjecture to a restricted class, the one-block decoupled polynomials.
2019. Aaronson surveys a decade of partial progress (retrospective).
2022. Bansal, Sinha and de Wolf prove the conjecture for completely bounded degree- $d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at constant variance (arXiv:2203.00212).
2024. The conjecture is established for a non-negligible fraction of random restrictions (arXiv:2402.13952).

The cases that are settled are settled under structural hypotheses -- block-multilinearity, complete boundedness, symmetry, Boolean range. The general statement is open.

Setting

Let $N$ be a positive integer. The Boolean cube is $\{0,1\}^N$ , carrying the uniform distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a function $f$ on the cube write

\mathbb{E}[f]=2^{-N}\sum_{x\in\{0,1\}^N}f(x).

The variance of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$ . Writing $x^{\oplus i}$ for $x$ with its $i$ -th bit flipped, the influence of coordinate $i$ on $p$ is

\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big].

These are the combinatorial forms of both quantities, as used in the source; no Fourier--Walsh expansion is required to state anything below. The degree of $p$ is its total degree as a polynomial. Call $p$ bounded when $0\le p(x)\le 1$ at every cube point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$ .

Target

The goal is the conjecture in the shape stated by its authors: there is an absolute constant $C$ such that for all $N$ , all $d$ , every polynomial $p$ of degree at most $d$ that is bounded on the cube, and every $\varepsilon>0$ with $\operatorname{Var}[p]\ge\varepsilon$ , some coordinate $i$ satisfies

\operatorname{Inf}_i[p]\;\ge\;\Big(\frac{\varepsilon}{d}\Big)^{C}.

The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the entire content: bounds that degrade exponentially in $d$ are already known, and a goal naming a specific exponent would be superseded by the next improvement.

Significance

The result itself. Aaronson and Ambainis prove that the conjecture implies that the acceptance probability of any bounded-error $T$ -query quantum algorithm on a Boolean input can be approximated, to small error on all but a small fraction of inputs, by a classical algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure in a precise sense. The conjecture also has purely classical content, asserting that boundedness plus low degree forces variance to concentrate on some single coordinate rather than spread across all $N$ . Without it, no such concentration is known at any rate polynomial in $1/d$ .

Formalizing it. The conjecture is open, so this mission does not formalize a known proof of the goal. What it produces is a machine-checked statement of the conjecture together with formalizations of the partial results above, each currently existing only on paper. The milestone chain also yields reusable infrastructure for analysis of Boolean functions, of which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no variance on the cube.

Difficulty

The elementary bound is the Poincare inequality on the cube, $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$ , which yields a coordinate with influence at least $4\varepsilon/N$ . This is tight for the dictator $p(x)=x_1$ and depends on $N$ , so it says nothing: the conjecture demands a bound free of $N$ entirely.

The natural repair is the route available when $p$ takes only the values $0$ and $1$ . A Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which immediately produces an influential one. That argument does not survive relaxing the range to the interval $[0,1]$ : a bounded real-valued polynomial of low degree need not depend on boundedly many coordinates, and every known substitute loses a factor exponential in $d$ . Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and it is where all of the partial results stop.

Formalization scope

Polynomials are MvPolynomial (Fin N) ℝ and degree is Mathlib's totalDegree, so the statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$ rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping is Function.update x i (!x i). Boundedness is asserted at cube points only. Variance and influence are the combinatorial definitions above, published as the definition AaronsonAmbainis.

Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as an existentially quantified natural number with no leading multiplicative constant, since admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The hypothesis $\deg p\le d$ is universally quantified over $d$ , which is equivalent to the source's exact-degree form because the smallest admissible $d$ gives the strongest conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$ fails for a constant polynomial.

A complete development needs, beyond the published definitions, a Fourier--Walsh layer with Parseval's identity, the level- $k$ machinery used by the partial results, and -- for the completely bounded case -- operator-space norms on multilinear forms. All of the Boolean-analysis material is reusable well beyond this mission. Contributions of any milestone are welcome, as are alternative formalizations of the definitions in function-level rather than polynomial-level form.

Out of scope: the quantum simulation consequence is not formalized here. Stating it requires a formal quantum query model, which no Lean library currently provides.

Selected references

S. Aaronson, A. Ambainis, The Need for Structure in Quantum Speedups, Theory of Computing 10 (2014) 133--166; arXiv:0911.0996. Conjecture 6.
N. Bansal, M. Sinha, R. de Wolf, Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms, CCC 2022; arXiv:2203.00212.
Aaronson--Ambainis Conjecture Is True For Random Restrictions, 2024; arXiv:2402.13952.
S. Aaronson, The Aaronson-Ambainis Conjecture (2008-2019), blog retrospective.
S. Arunachalam, J. Briet, C. Palazuelos, Quantum query algorithms are completely bounded forms, SIAM J. Comput. 48 (2019); arXiv:1711.07285.
AIM problem list, Analysis on the hypercube with applications to quantum computing, aimpl.org/hypercubequantum.

4 thms2 active usersReviewed

Completed

Combinatorics Probability·Captain: sr

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Motivation

Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$ . Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.

This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$ . It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$ .

Timeline. Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.

Setting

Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$ . A graph is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$ ; here vertices are labeled $0, \dots, N-1$ . A subset $s \subseteq V$ of size $k$ is a clique if every two distinct vertices of $s$ are adjacent, and an independent set if every two distinct vertices of $s$ are non-adjacent. A $k$ -set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).

The ambient probability space is the uniform distribution over all graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$ . This space has exactly $2^{\binom{N}{2}}$ elements.

A graph with no monochromatic $k$ -set is a graph with neither a $k$ -clique nor an independent $k$ -set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$ ", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.

Formalization targets

Goal: the probabilistic lower bound

R(k) > 2^{k/2}, \qquad k \ge 3

i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$ -set.

Stronger: the three steps of the proof, as separate targets

Count estimate. For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$ ,

\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.

Union-bound principle. In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:

\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.

Pair-count bound. Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$ -set in $G$ is at most

\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.

The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.

Significance

The result. The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).

Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$ .

Difficulty

The central difficulty is that the bad events — "the $k$ -set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$ -sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$ ; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.

A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$ -set ( $2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.

Formalization scope

Representation. Graphs are SimpleGraph (Fin N): a relation on $N$ labeled vertices. A candidate set is a Finset (Fin N) of cardinality $k$ ; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic $k$ -set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic $k$ -sets of $G$ .

Conventions. $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$ . The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$ , is a natural follow-up contribution).

Reusability. The union-bound principle, the monochromatic- $k$ -set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$ ; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.

Selected references

Paul Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$ .
Noga Alon, Joel H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
Stanisław Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.

Context: where this sits in the formalization landscape

This mission is not a duplicate of existing platform content, and the choice of target is deliberate:

Mathlib gap. The pinned environment (mathlib 0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
Existing Ramsey content is a different quantity. The platform's fully-proved Erdos183 mission concerns multicolour triangle Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
Directly load-bearing for a live open problem. The public open problem diagonal_ramsey_asymptotics (same environment 0df444a) asks, eventually in $k$ , for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$ ; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.
Formalization convention. The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$ ; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$ .

5 thms2 active usersReviewed

Completed

Captain: wenxinzhang

Primal-Dual Online Load Balancing on Unrelated MachinesTextbook

The model

Fix $m \ge 1$ machines and $n$ jobs arriving one at a time in the order $0, \dots, n-1$ . Job $i$ carries a whole vector of nonnegative loads $\tilde p(i,j)$ , one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the unrelated machines model. When job $i$ arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and irrevocably, knowing nothing about the jobs still to come. A machine's load is the sum of $\tilde p(i,j)$ over the jobs assigned to it.

The setting formalized here is one normalized phase: loads are already scaled by a guessed makespan, so machine $j$ counts as eligible for job $i$ exactly when $\tilde p(i,j) \le 1$ . The phase is allowed to give up rather than assign badly — it fails if an arriving job has no eligible machine, or if an internal weight grows past $1$ .

The algorithm and the guarantee

The algorithm keeps a weight $x(j)$ per machine, initialized to $1/(2m)$ . Job $i$ goes to the eligible machine $\ell$ minimizing $\tilde p(i,\ell)\, x(\ell)$ ; that machine's weight is then scaled by $1 + \tilde p(i,\ell)/2$ , so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP

\min \sum_j x(j) + \sum_i z(i) \quad \text{s.t.} \quad \tilde p(i,j)\,x(j) + z(i) \ge 1 \ \text{ for every eligible pair } (i,j),

and each assignment raises one dual variable $y(i,\ell)$ to $1$ . The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.

The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load

\sum_{i \,\text{assigned to}\, j} \tilde p(i,j) \ \le\ \frac{\ln(3m)}{\ln(3/2)}.

The source states this as $O(\log m)$ ; the explicit constant is what its proof yields.

Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of succeeded, assigns all, and the bound.

Scope

The doubling wrapper — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an $O(\log m)$ -competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.

Source

Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, Chapter 8, pp. 193–196 (Theorem 8.1). PDF · doi:10.1561/0400000024

10 thms2 active usersReviewed

Combinatorics Machine Learning·Captain: mikedeng1

A Characterization of Multiclass Learnability 1: Classes of Finite DS Dimension Have n → r Sample Compression Schemes with r Polylogarithmic in nResearch Paper

Motivation

In multiclass classification a learner sees examples $(x, y)$ with $x$ in a domain $\mathcal X$ and a label $y$ in a set $\mathcal Y$ , and must predict labels of new points. When $\mathcal Y$ is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite $\mathcal Y$ the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.

Timeline:

1989–1995. Natarajan, then Ben-David et al. and Haussler–Long: for finite $\mathcal Y$ , learnability is equivalent to finite Natarajan dimension, with sample complexity depending on $\log|\mathcal Y|$ .
2011–2015. Daniely, Sabato, Ben-David and Shalev-Shwartz show that ERM can fail for multiclass problems with many labels. Daniely and Shalev-Shwartz (COLT 2014) introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
2022. Brukhim, Carmon, Dinur, Moran, Yehudayoff prove sufficiency, so the DS dimension characterizes multiclass PAC learnability, and show that the Natarajan dimension does not.

Setting

A concept class is a set $\mathcal H\subseteq\mathcal Y^{\mathcal X}$ of functions. For a sequence $S=(x_1,\dots,x_n)$ the projection $\mathcal H|_S\subseteq\mathcal Y^n$ is the set of label words $(h(x_1),\dots,h(x_n))$ , $h\in\mathcal H$ . A finite non-empty set $B\subseteq\mathcal Y^d$ is a pseudo-cube if every $h\in B$ has, in every coordinate $i$ , a neighbour $g\in B$ that differs from $h$ exactly in coordinate $i$ . The sequence $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$ -dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the maximum length of a DS-shattered sequence. The Natarajan dimension $d_N(\mathcal H)\le d_{DS}(\mathcal H)$ is the same with Boolean cubes $\prod_i\{f(i),g(i)\}$ , $f(i)\ne g(i)$ , in place of pseudo-cubes.

A sample $S\in(\mathcal X\times\mathcal Y)^n$ is $\mathcal H$ -realizable if some $h\in\mathcal H$ is consistent with it. An $n\to r$ sample compression scheme for $\mathcal H$ (Littlestone and Warmuth 1986) is a single reconstruction function $\rho:(\mathcal X\times\mathcal Y)^r\to\mathcal Y^{\mathcal X}$ such that every realizable sample of size $n$ contains $r$ of its examples $S'$ with $\rho(S')$ consistent with the whole sample. Logarithms are base $2$ throughout.

Formalization targets

Goal: Theorem 36 (p. 22)

For $\mathcal H$ with $d_{DS}(\mathcal H)=d_{DS}<\infty$ and $d_N(\mathcal H)=d_N$ , and all integers $n,t>0$ , there is an $n\to r$ sample compression scheme, $r\le n$ , with

r\le\left(\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)+10^3d_N\log\left(\binom{d_{DS}+t+1}{t+1}\log(2n)\right)\right)\log(2n).

Milestones

The scheme combines two components, each with its own chain of results:

List learning from the DS dimension. Lemma 13 (orientations of out-degree $\le d$ on $\mathcal Y^{d+1}$ ), Claim 16 (the one-inclusion algorithm is right on some leave-one-out example), Fact 14 (leave-one-out symmetrization), Proposition 32 (a list PAC learner with list size $\binom{d+t}{t}$ and success probability $\frac{t+1}{d+t+1}$ ), Lemma 39 (an $n\to r_1$ list compression scheme with $r_1\le\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)\log(2n)$ and menu size $\le\binom{d_{DS}+t+1}{t+1}\log(2n)$ ).
Learning from a menu via shifting. Claim 22, Corollary 23, Claim 26, Proposition 27 ( $\operatorname{avd}\le4d_E$ ), Corollary 28, Lemma 29 ( $d_E\le5d_N\log p$ ), Lemma 17 (orientations of out-degree $\le20d_N\log p$ on $[p]^n$ ), Proposition 34 (error $\le20d_N\log(p)/n$ given a $p$ -menu), Lemma 40 (an $n\to r_2$ compression scheme given a $p$ -menu with $r_2\le10^3d_N\log(p)\log(2n)$ ).

Significance

Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity $\tilde O(d_{DS}^{3/2}/\epsilon)$ in the realizable case ( $t=\lceil d_{DS}^{1/2}\rceil$ ), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in $n$ for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.

The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.

Difficulty

The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension $1$ and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among $d+1$ leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size $p$ , where the obstacle is controlling one-inclusion graph orientations over $[p]^n$ by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential ( $\operatorname{avd}'$ ) and a new dimension ( $d_E$ ) are needed. Lemma 13 for infinite classes needs a compactness argument.

Formalization scope

Lean conventions:

A class is H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ( $[n]$ is 0-based).
The DS, Natarajan and exponential dimensions are suprema in ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.
Logarithms are Real.logb 2. Menu sizes use Set.encard.
A compression scheme is a reconstruction function fixed before the sample (∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states $r\le n$ explicitly.
Orientations of the one-inclusion graph of $V\subseteq\mathcal Y^m$ are maps sending a direction $i$ and a vertex $v$ to the head of the edge of direction $i$ through $v$ ; the out-degree of $v$ counts directions whose head is not $v$ .
Classes over $[p]$ use labels Fin p; the shifting condition $1\le g(i)\le|e_f|$ becomes $g(i)<|e_f|$ .
The one-inclusion algorithm (Algorithms 1 and 3) is parametrized by a permutation-equivariant choice of minimal orientations, the reading under which the paper's leave-one-out proofs are valid; statements about the algorithm hold for every such choice. Its default output on non-realizable input requires a non-empty label set, assumed in Claim 16 and Propositions 32 and 34. Lemma 40 assumes a non-empty label set because it is false for $\mathcal X\ne\emptyset=\mathcal Y$ .
Distributions are discrete (PMF), and i.i.d. probabilities are sums over $\mathcal Z^m$ . The measure-theoretic generality of the paper is not attempted.

A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be $0$ for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).

Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.

Selected references

N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, FOCS 2022; arXiv:2203.01550v1 (2022). https://arxiv.org/abs/2203.01550
A. Daniely, S. Shalev-Shwartz, Optimal Learners for Multiclass Problems, COLT 2014. https://arxiv.org/abs/1405.2690
N. Littlestone, M. Warmuth, Relating Data Compression and Learnability, unpublished technical report, University of California, Santa Cruz, 1986 (no stable link).
D. Haussler, N. Littlestone, M. Warmuth, Predicting {0,1}-Functions on Randomly Drawn Points, Information and Computation 115(2), 1994. https://doi.org/10.1006/inco.1994.1097
D. Haussler, P. M. Long, A Generalization of Sauer's Lemma, Journal of Combinatorial Theory, Series A 71(2), 1995. https://doi.org/10.1016/0097-3165(95)90006-3
S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of Learnability for Classes of {0,…,n}-Valued Functions, JCSS 50(1), 1995. https://doi.org/10.1006/jcss.1995.1008
B. K. Natarajan, On Learning Sets and Functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

20 thms1 active userReviewed

Combinatorics Operations Research·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 6: The Optimal Value of S_G Lies Between n² − an²(ln 1/a + 2) and n² − an²Research Paper

Motivation

The problem $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ asks for a single-machine sequence of jobs, respecting precedence constraints, that minimizes the weighted sum of completion times. It has been known to be strongly NP-hard since Lawler (1978) and Lenstra and Rinnooy Kan (1978), several different 2-approximation algorithms are known, and closing the approximability gap is listed by Schuurman and Woeginger (1999) as one of ten outstanding open problems in scheduling theory. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) give the first inapproximability result for this problem: under a widely believed complexity assumption it has no polynomial-time approximation scheme (PTAS). The bridge to that result is a quantitative link, Lemma 9.1, between the optimal value of a special bipartite scheduling instance and the maximum edge biclique of a bipartite graph, a problem whose hardness of approximation was established by Ambühl, Mastrolilli and Svensson (FOCS 2007). This mission formalizes that link.

Setting

A schedule of a finite job set is a sequence $\sigma$ listing every job once; the machine processes the jobs in that order from time $0$ without idle time or pre-emption. Job $j$ has a processing time $p_j$ and a weight $w_j$ ; its completion time $C_j$ is the sum of the processing times of the jobs up to and including $j$ , and the value of $\sigma$ is $\mathrm{val}(\sigma)=\sum_j w_jC_j$ . Precedence constraints are a relation $P$ on jobs: $(i,j)\in P$ with $i\ne j$ means job $i$ must be completed before job $j$ starts. A schedule respecting all of them is feasible, and a feasible schedule $\sigma^*$ of least value is optimal.

Let $G=(U,V,E)$ be an $n$ -by- $n$ bipartite graph: $|U|=|V|=n$ and $E\subseteq U\times V$ . An edge biclique is a pair $A\subseteq U$ , $B\subseteq V$ with $A\times B\subseteq E$ , of value $|A|\cdot|B|$ ; the maximum edge biclique problem (Definition 9.1) asks for one of largest value. The bipartite scheduling instance $S_G$ has jobs $U\cup V$ and precedence constraints

P=(U\times V)\setminus E,

so $u\in U$ must precede $v\in V$ exactly when $(u,v)$ is not an edge. Jobs of $U$ have $p=1$ , $w=0$ ; jobs of $V$ have $p=0$ , $w=1$ . Thus $\mathrm{val}(\sigma)=\sum_{v\in V}C_v$ , where $C_v$ is the number of $U$ -jobs scheduled before $v$ . For $i\ge1$ , $\sigma(i)$ denotes the number of $V$ -jobs scheduled before $i$ jobs of $U$ have been scheduled.

In the Lean development these are weightedCompletion, IsOptimalSchedule, IsEdgeBiclique, maxBicliqueValue, precSG, procSG, weightSG, valSG, IsOptimalSG and vBefore in the namespace SingleMachinePrec.Biclique.

Formalization targets

Goal: Lemma 9.1 (p. 666)

If a maximum edge biclique of $G$ has value $an^2$ with $a\in(0,1]$ , then $S_G$ has an optimal schedule and every optimal schedule $\sigma^*$ satisfies

n^2-an^2\Bigl(\ln\frac1a+2\Bigr)\le\mathrm{val}(\sigma^*)\le n^2-an^2 .

Milestones (proof of Lemma 9.1, §9, p. 666)

For every edge biclique $(A,B)$ , a schedule in the block order $U\setminus A\to B\to A\to V\setminus B$ exists, and every such schedule is feasible with

\mathrm{val}(\sigma)=n^2-|A|\cdot|B| .

For every schedule, $\sigma(n+1)=n$ and

\mathrm{val}(\sigma)=\sum_{i=1}^n\bigl(\sigma(i+1)-\sigma(i)\bigr)i=n^2-\sum_{i=1}^n\sigma(i).

For every feasible schedule and $i=1,\dots,n$ ,

\sigma(i)(n-i+1)\le an^2,\qquad \sigma(i)\le n .

Significance

Lemma 9.1 shows that the optimal value of $S_G$ determines the maximum edge biclique of $G$ up to a factor of order $\ln(1/a)$ in the "area above the work line" $n^2-\mathrm{val}(\sigma^*)$ . Combined with the hardness of approximating maximum edge biclique (Theorem 9.1, cited from Ambühl, Mastrolilli and Svensson 2007) it yields Theorem 9.2: $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ has no PTAS unless SAT can be decided by a probabilistic algorithm in time $2^{N^\epsilon}$ for every $\epsilon>0$ . It also makes precise the two-dimensional Gantt chart picture of Eastman, Even and Isaacs (1964) and of Goemans and Williamson (2000), in which every point on the work line of a schedule defines an edge biclique.

The lemma is proved in the paper; it is not formalized anywhere to our knowledge. A formal proof certifies the combinatorial core of the no-PTAS result independently of the complexity-theoretic layer, and its definitions (the bipartite instance $S_G$ , edge bicliques, the profile $\sigma(i)$ ) are reusable for the gap inequality behind Theorem 9.2.

Difficulty

The upper bound is a direct computation on one explicit schedule. The lower bound is a statement about every feasible schedule, of which there are exponentially many, and it must hold with the explicit constant $2$ and the factor $\ln(1/a)$ for every $a\in(0,1]$ . The printed argument splits the sum at $i=(1-a)n$ and uses $\lfloor an\rfloor$ , treating $an$ as an integer; for general $a$ (for example $n=3$ , value $2$ , $an=2/3$ ) the split point is not an integer, so the printed estimate does not apply verbatim and the constant $2$ has to be re-checked for non-integral $an$ . On the formal side, the value identity requires relating completion times in a list to counting $U$ -jobs before each $V$ -job, with ties among zero-length jobs.

Formalization scope

Jobs are the disjoint union U ⊕ V of two finite types with Fintype.card U = Fintype.card V = n; $E$ is a relation U → V → Prop. A schedule is a duplicate-free list containing every job; feasibility is the published LawlerPrec.MinMax.IsFeasible and completion times are the published MooreLateJobs.Shared.completionTime (time $0$ start, no idle time). Processing times and weights are reals, here in $\{0,1\}$ . The maximum edge biclique value is the maximum of $|A|\cdot|B|$ over all edge bicliques, the empty ones included, so the hypothesis $a>0$ means $E\ne\emptyset$ . The logarithm is natural (Real.log).

Conventions and readings committed to:

The goal is stated for every optimal schedule, and the existence of an optimal schedule is a separate conclusion, so the bounds cannot hold vacuously. Proving the bounds for one particular schedule, or for an optimal value defined as an infimum that could be a junk default, would not be this lemma.
No integrality hypothesis on $an$ is added.
Milestones 2 and 3 are stated for every schedule (respectively every feasible schedule), not only for $\sigma^*$ ; milestone 1 states the value of the block-order schedule as an equality, where the paper writes " $\le\cdots=$ ".
The paper's $P=(U\times V)\setminus E$ is irreflexive; feasibility only constrains distinct jobs, so it agrees with the reflexive partial order of §1.

Not formalized: Theorem 9.1 (cited hardness of maximum edge biclique) and Theorem 9.2 (no PTAS under a complexity assumption); no polynomial-time or complexity-theoretic statement appears in the mission. Contributions welcome: proofs of the three milestones and of the goal; Mathlib's bounds on harmonic numbers (Mathlib/NumberTheory/Harmonic/Bounds.lean) are the relevant library.

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
C. Ambühl, M. Mastrolilli, O. Svensson, Inapproximability results for sparsest cut, optimal linear arrangement, and precedence constraint scheduling, Proc. 48th IEEE FOCS, 329–337, 2007 (reference [4] of the paper).
W. L. Eastman, S. Even, I. M. Isaacs, Bounds for the optimal scheduling of n jobs on m processors, Management Science 11(2):268–279, 1964 (reference [11]).
M. X. Goemans, D. P. Williamson, Two-dimensional Gantt charts and a scheduling algorithm of Lawler, SIAM J. Discrete Math. 13(3):281–294, 2000 (reference [15]).
P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 2(5):203–213, 1999 (reference [36]).

8 thms1 active userReviewed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 1: A k-Fold Realizer of Size t Yields a Vertex Cover of Expected Weight at Most (2 − 2/(t/k)) Times OptimalResearch Paper

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$ -approximations for orders of fractional dimension at most $f$ . This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$ .

Two jobs $x,y$ are incomparable, $x\parallel y$ , when neither $(x,y)$ nor $(y,x)$ lies in $P$ . The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$ ; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$ . A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$ -realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$ -realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$ , or $j=k$ and $(i,\ell)\in P$ , or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$ , and $w(C)=\sum_{u\in C}w_u$ . $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ . The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$ . For a solution $x$ write $V_a=\{u: x_u=a\}$ , and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$ .

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$ , a $k:t$ -realizer $L_1,\dots,L_t$ of $P$ , and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$ . Then every $C_i$ is a vertex cover of $G^S_P$ , and

\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.

Milestones

Proposition 3.2 (p. 657): $G^S_P=G_P$ .
Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$ .
Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$ .
Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$ .
Hochbaum's observation (§5, p. 659): for half-integral feasible $x$ , $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$ .
Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$ -approximate vertex cover of $G^S_P$ into an $\alpha$ -approximate schedule, Theorem 5.1 gives a $(2-2/f)$ -approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$ . The paper applies it to interval orders ( $3/2$ ), convex bipartite orders and semiorders ( $4/3$ ), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$ -fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$ .

Formalization scope

Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
$\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$ -realizer is a family Fin t → LinearExtension P with $t>0$ . Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's " $y>x$ " in Eq. (4) and " $\mathrm{Prob}[j>i]$ " in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
$G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
[CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ , taken over a finite nonempty family.
Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$ , which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$ . The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$ .
Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$ , and equals $2$ when $k=0$ .
The paper assumes $\operatorname{fdim}(P)\ge2$ , i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$ .
Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

10 thms1 active userReviewed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 4: Vertex Cover in Connected Graphs of Degree ≤ 3 Reduces to Weighted Vertex Cover for Interval-Order InstancesResearch Paper

Motivation

In the single-machine scheduling problem $1|\mathrm{prec}|\sum w_jC_j$ , a set $N$ of $n$ jobs, each with a processing time $p_j\ge 0$ and a weight $w_j\ge 0$ , is processed on one machine without interruption, subject to precedence constraints given by a partial order $P$ on $N$ . The aim is to minimize the weighted sum of completion times $\sum_j w_jC_j$ . The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph $G^S_P$ built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.

Setting

A poset $P=(N,P)$ is read as a reflexive relation: $(x,y)\in P$ means $x\le y$ . Jobs $x,y$ are incomparable if neither $(x,y)$ nor $(y,x)$ is in $P$ , and $\operatorname{inc}(P)$ is the set of ordered incomparable pairs. The vertex cover graph $G^S_P$ has one node $(i,j)$ for each incomparable pair, weighted $p_iw_j$ . Two nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$ , or $j=k$ and $(i,\ell)\in P$ , or $(i,\ell)\in P$ and $(k,j)\in P$ . Write $w(C_I)$ for the minimum weight of a vertex cover of $G^S_I$ .

A poset is an interval order if each element $x$ can be assigned a closed real interval $[a_x,b_x]$ such that $x<y$ if and only if $b_x<a_y$ .

The reduction starts from a graph $G=(V,E)$ with vertices $v_1,\dots,v_N$ and a spanning tree $T=(V,E_T)$ rooted at $v_1$ , numbered so that each parent comes before its children. The paper uses a breadth-first search tree.

Stage 1. The graph $G'$ is built from $T$ . Each $v_i$ gets a pendant path $v_i - u^i_1 - u^i_2$ . Each non-tree edge $\{v_i,v_j\}\in E\setminus E_T$ with $i<j$ gets the path $v_i - e^{ij}_1 - e^{ij}_2 - u^j_2$ . The non-tree edges themselves are not edges of $G'$ .
Stage 2. The scheduling instance $S$ has jobs $s_0$ , $s_1,\dots,s_N$ , $m_1,\dots,m_N$ , $e_1,\dots,e_N$ , and $b_{ij}$ for each non-tree edge. Their intervals, processing times and weights are given in a table on p. 662. For example, $s_j$ has interval $[i,j]$ , processing time $1/k^j$ and weight $k^i$ , where $v_i$ is the parent of $v_j$ . The precedence constraints $I$ are the interval order of these intervals. With $n$ the number of jobs, the parameter is $k=n^2+1$ .
The set $D$ . It is $\{(s_0,s_1)\}\cup\{(s_i,s_j): v_i \text{ parent of } v_j\}\cup\{(s_i,m_i),(m_i,e_i)\}\cup\{(s_i,b_{ij}),(b_{ij},m_j)\}$ . The graph $G'_I$ is the subgraph of $G^S_I$ induced by $D$ .

Formalization targets

Goal: Theorem 7.1 (p. 661)

For every connected graph $G$ of maximum degree at most $3$ , every parent-first spanning tree $T$ and every $m\in\mathbb N$ , the precedence constraints $I$ of $S$ form an interval order, and

G \text{ has a vertex cover of size} \le m \iff \lfloor w(C_I)\rfloor \le m + |V| + |E\setminus E_T|.

Milestones, in the order the proof uses them

Claim 1 (p. 662): $\tau(G') = \tau(G)+|V|+|E\setminus E_T|$ , where $\tau$ is the vertex cover number.
Remark 7.1 (p. 662): for jobs with intervals $[a,b]$ and $[c,d]$ and $a\le d$ , $p_i\le 1/k^{\lceil b\rceil}$ and $w_j\le k^{\lceil c\rceil}$ . On incomparable pairs $p_iw_j\in\{1\}\cup[0,1/k]$ . Moreover, $p_iw_j\ge k$ forces $b<c$ , and $p_iw_j=1$ forces $\lceil b\rceil=\lceil c\rceil$ .
Claim 2 (p. 663): an incomparable pair $(i,j)$ has $p_iw_j=1$ if it is in $D$ , and $p_iw_j\le 1/k$ otherwise.
Claim 3 (p. 663): $G'_I\cong G'$ .
§7, p. 664: with $k=n^2+1$ , $\sum_{(i,j)\in\operatorname{inc}(I)\setminus D}p_iw_j<1$ , and hence $w(C'_I)=\lfloor w(C_I)\rfloor$ .

Significance

The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts $1|\mathrm{prec}|\sum w_jC_j$ outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a $3/2$ -approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor $r>1$ on the graphs $G^S_I$ arising from interval orders.

Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:

a gadget argument on unweighted vertex covers (Claim 1, after Alimonti and Kann);
an exact case analysis of incomparable pairs in a concrete interval order (Remark 7.1, Claim 2);
a graph isomorphism (Claim 3);
a rounding argument that links weighted and unweighted optima.

The definitions of $G^S_P$ and of minimum-weight vertex covers are shared with the other missions of this series.

Difficulty

The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as $(b_{ij}, s_\ell)$ , by comparing ceilings of interval endpoints. Half-integer endpoints ( $m_i$ , $b_{ij}$ ) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in $G^S_I$ for all pairs of nodes of $D$ in both directions. The paper writes out two cases in each direction and calls the rest similar.

Claim 1 has a direction that is not simply local. A vertex cover of $G'$ that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.

A natural first idea is to treat the light nodes (weight at most $1/k$ ) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below $1$ , which is what forces $k$ to grow with $n^2$ .

Formalization scope

Graph and tree. $G$ is a SimpleGraph (Fin N); vertex $v_{i+1}$ is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in $G$ . The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".
Hypotheses of the goal. Connectivity and the degree bound ((G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.
Jobs. The jobs form an inductive type with one constructor per row of the table. Their order is a PartialOrder instance: $x\le y$ iff $x=y$ or $b_x<a_y$ . Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses $1/k^j$ and the formalization follows the instance as printed.
Constants. The constants are explicit: $k=n^2+1$ with $n$ the cardinality of the job type, and $c=|V|+|E\setminus E_T|$ . Remark 7.1 and Claim 2 are stated for every real $k>1$ .
Optimum values. $w(C_I)$ is a minimum over the finite family of vertex covers. Unweighted cover numbers are Mathlib's SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because $w(C_I)\ge 0$ .
Not formalized. The goal's wording ("NP-hard") is not formalized. Neither are the NP-completeness of degree-3 vertex cover (Garey, Johnson and Stockmeyer), the polynomial size of the construction, or Theorem 2.1 (cited), which turns a vertex cover of $G^S_I$ into a schedule. What is stated is the correctness of the reduction: the instance has interval-order constraints, and its optimum decides the vertex cover question.
No trivialization. The instance $S$ is built from $G$ and $T$ exactly as in the table. The goal quantifies over all graphs and layouts, never over an instance $S$ assumed to have the properties.
Contributions. Contributions are welcome on any milestone. Claims 1 and 3 are independent of the weights, and Claim 2 is independent of the graph theory.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-1
J. R. Correa, A. S. Schulz, Single machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
P. Alimonti, V. Kann, Some APX-completeness results for cubic graphs, Theoret. Comput. Sci. 237(1–2):123–134, 2000. https://doi.org/10.1016/S0304-3975(98)00158-3
M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1(3):237–267, 1976. https://doi.org/10.1016/0304-3975(76)90059-1
C. H. Papadimitriou, M. Yannakakis, Scheduling interval-ordered tasks, SIAM J. Comput. 8(3):405–409, 1979. https://doi.org/10.1137/0208031

10 thms1 active userReviewed

Graph Theory Operations Research·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 5: An r-Approximate Vertex Cover of the Variable-Cost Graph Yields an (r + ε)-Approximate Vertex Cover of GResearch Paper

Why the variable cost matters

The problem $1|\mathrm{prec}|\sum w_jC_j$ asks for an order in which to process jobs on one machine, respecting precedence constraints, so as to minimize the weighted sum of completion times. It is strongly NP-hard, and for decades the best approximation ratio known has been $2$ , achieved by several unrelated algorithms (LP relaxations, Sidney decompositions, primal–dual methods).

Correa and Schulz (2005) and Ambühl and Mastrolilli (2009) showed that the problem is a special case of weighted vertex cover: its objective splits into a fixed cost, the same for every feasible solution, and a variable cost, which equals the weight of a vertex cover in an auxiliary graph $G^S_{\mathbf P}$ . Approximating vertex cover in $G^S_{\mathbf P}$ within a factor $\alpha$ therefore approximates the scheduling problem within $\alpha$ . Uhan observed that the classical 2-approximations owe their guarantee to the fixed cost and can be arbitrarily bad on the variable cost alone.

Section 8 of Ambühl, Mastrolilli, Mutsanas and Svensson, Math. Oper. Res. 36(4) (2011) (DOI), proves the converse: approximating the variable cost is as hard as approximating vertex cover itself. A better-than-2 algorithm for $1|\mathrm{prec}|\sum w_jC_j$ must therefore either exploit the fixed cost or improve on the best known approximation for vertex cover, a long-standing open question.

Setting

Scheduling instance. A finite set $N$ of jobs, a partial order $\mathbf P = (N,P)$ (reflexive; $(i,j) \in P$ , $i \ne j$ , means $i$ precedes $j$ ), processing times $p_j \ge 0$ and weights $w_j \ge 0$ .

Incomparable pairs. Jobs $x,y$ are incomparable, $x \parallel y$ , if neither $(x,y)$ nor $(y,x)$ lies in $P$ . The set $\operatorname{inc}(\mathbf P)$ consists of the ordered pairs $(x,y)$ with $x \parallel y$ .

The vertex cover graph $G^S_{\mathbf P}$ . One node per incomparable pair $(i,j)$ , of weight $w_{(i,j)} = p_i w_j$ . Distinct nodes $(i,j)$ and $(k,\ell)$ are adjacent when, in one of the two orders, $j=k$ and $i=\ell$ , or $j=k$ and $(i,\ell)\in P$ , or $(i,\ell),(k,j) \in P$ . For a set $C$ of nodes, $w(C) = \sum_{u\in C} w_u$ ; for a vertex cover $C$ this is the variable cost, and $\tau_w(G^S_{\mathbf P})$ is its minimum over all vertex covers.

The instance $S(G,k)$ . Given a graph $G=(V,E)$ with $V = \{v_1,\dots,v_n\}$ and $k > 0$ , the instance has jobs $v'_i$ (processing time $k^{-i}$ , weight $0$ ) and $v''_i$ (processing time $0$ , weight $k^{i}$ ), and precedence constraints $v'_i < v''_j$ and $v'_j < v''_i$ for each edge $\{v_i,v_j\} \in E$ , plus $v'_i < v''_j$ for all $i<j$ . The nodes $(v'_i, v''_i)$ of $G^S_{\mathbf P}$ have weight $1$ and are called heavy; all others are light. For a set $C$ of nodes, $C_G = \{v_i : (v'_i,v''_i)\in C\}$ . The vertex cover number of $G$ is $\tau(G)$ .

Formalization targets

Goal: Theorem 8.1

For every graph $G$ on $n$ vertices, every $r \ge 1$ , $\varepsilon>0$ and every $k \ge 1$ with $k > n^2r/\varepsilon$ : if $C$ is a vertex cover of $G^S_{\mathbf P}$ for $S = S(G,k)$ with $w(C) \le r\,\tau_w(G^S_{\mathbf P})$ , then $C_G$ is a vertex cover of $G$ ,

|C_G| \le r\Bigl(\tau(G) + \frac{n^2}{k}\Bigr),

and, when $E \ne \emptyset$ ,

|C_G| \le r\Bigl(1+\frac{n^2}{k}\Bigr)\tau(G) < (r+\varepsilon)\,\tau(G).

The paper words the theorem as "approximating the variable cost of $1|\mathrm{prec}|\sum w_jC_j$ is as hard as approximating vertex cover"; the statement above is the mathematical content its proof establishes.

Milestones (§8, p. 664)

In $G^S_{\mathbf P}$ , every heavy node has weight $1$ , every light node has weight at most $1/k$ , and the light nodes have total weight at most $n^2/k$ (for $k \ge 1$ ).
Heavy nodes $(v'_i,v''_i)$ and $(v'_j,v''_j)$ are adjacent if and only if $\{v_i,v_j\}\in E$ ; for $k>1$ the subgraph induced by the weight-1 nodes is isomorphic to $G$ via $(v'_i,v''_i) \mapsto v_i$ .

Significance

The result. Theorem 8.1 is one half of an equivalence: by Theorem 2.1 (Correa–Schulz, Ambühl–Mastrolilli), minimizing the variable cost is a special case of weighted vertex cover; by Theorem 8.1, it is also as hard to approximate. Any hardness of approximation for vertex cover (NP-hardness of factor $1.36$ by Dinur and Safra; factor $2-\delta$ under the unique games conjecture by Khot and Regev) transfers to the variable cost. It also explains why the known 2-approximations must rely on the fixed cost, and it frames the later result of Bansal and Khot that the full objective is hard to approximate within $2-\delta$ under a variant of the unique games conjecture.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a checked account of the reduction: the vertex cover graph of an arbitrary precedence-constrained instance, the adjacency-poset instance built from a graph, and the quantitative transfer of approximation ratios. The definition of $G^S_{\mathbf P}$ is shared with the other missions of this series.

Difficulty

The construction is short; the care is in the bookkeeping. One must check that the precedence relation is a partial order, determine exactly which ordered pairs are incomparable, verify that two heavy nodes are adjacent only through the third clause of the adjacency rule and only when the corresponding vertices are adjacent in $G$ , and bound the weights of all remaining nodes, including the many nodes of weight $0$ . The transfer then compares an approximate cover of $G^S_{\mathbf P}$ with an optimal one whose heavy part comes from an optimal cover of $G$ ; the additive error $n^2/k$ must be converted into a multiplicative one, which requires $\tau(G)\ge 1$ .

A first reading of the page suggests that $G^S_{\mathbf P}$ has at most $n^2$ nodes; it does not. The pairs $(v'_i,v'_j)$ and $(v''_i,v''_j)$ with $i\ne j$ are incomparable nodes of weight $0$ , so there can be up to $4n^2-2n$ nodes. Only nodes of positive weight are few.

Formalization scope

Model. Jobs form a finite type; precedence constraints are an explicit reflexive partial-order relation P : N → N → Prop. Processing times and weights are nonnegative reals. The vertex cover graph is a SimpleGraph on the subtype of incomparable ordered pairs, using the symmetric closure of the printed adjacency rule without loops. Vertex covers are Mathlib's SimpleGraph.IsVertexCover; $\tau(G)$ is Mathlib's vertexCoverNum, finite for a finite graph and converted with toNat; $\tau_w(G^S_{\mathbf P})$ is a minimum over finite vertex covers.
The instance. The graph is a SimpleGraph (Fin n); i : Fin n stands for $v_{i+1}$ , so exponents are $i+1$ and the order $i<j$ is that of Fin n. Jobs are Fin n ⊕ Fin n ( $v'$ left, $v''$ right). The parameter $k$ is in $\mathbb R_{\ge 0}$ .
Added hypotheses. $k \ge 1$ , implicit in the page (" $k > n^2r/\varepsilon$ " does not imply it when $\varepsilon$ is large, and for $k<1$ the light nodes outweigh the heavy ones). The isomorphism with $G$ is stated for $k > 1$ , since at $k=1$ some light nodes also have weight $1$ . The multiplicative bound requires $E \ne \emptyset$ ; the additive bound holds for every graph.
Not formalized. The phrases "approximation algorithm", "polynomial time" and "as hard as"; the passage from vertex covers of $G^S_{\mathbf P}$ to schedules (Theorem 2.1, cited from Correa–Schulz and Ambühl–Mastrolilli); the fixed cost. What is stated instead is the explicit map $C \mapsto C_G$ and the ratio it achieves, $r(1+n^2/k) < r+\varepsilon$ . The false count "at most $n^2$ vertices" is not stated.
Ruled out. The goal is not a statement about an arbitrary graph or an assumed cover of $G$ : it concerns the specific instance $S(G,k)$ and every $C$ that is an $r$ -approximate vertex cover of its graph, and the fact that $C_G$ covers $G$ is a conclusion, not a hypothesis.
Welcome contributions. Proofs of the two milestones and of the goal; general lemmas on $G^S_{\mathbf P}$ (weights of vertex covers, behaviour under induced subgraphs) are reusable across the series.

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
J. R. Correa, A. S. Schulz, Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
C. Ambühl, M. Mastrolilli, Single Machine Precedence Constrained Scheduling Is a Vertex Cover Problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-6
I. Dinur, S. Safra, On the Hardness of Approximating Minimum Vertex Cover, Annals of Mathematics 162(1):439–485, 2005. https://doi.org/10.4007/annals.2005.162.439
S. Khot, O. Regev, Vertex Cover Might Be Hard to Approximate to within 2 − ε, Journal of Computer and System Sciences 74(3):335–349, 2008. https://doi.org/10.1016/j.jcss.2007.06.019
N. Bansal, S. Khot, Optimal Long Code Test with One Free Bit, FOCS 2009, 453–462. https://doi.org/10.1109/FOCS.2009.23

5 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments I: Revenue-Ordered Assortments Earn OPT/(1 + ln(r_k/r_1)) Under Any Regular Choice ModelResearch Paper

Motivation

A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).

The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.

Timeline:

2004: Talluri and van Ryzin prove revenue-ordered assortments optimal under the multinomial logit model.
2014: Rusmevichientong et al. show NP-hardness of the assortment problem for mixtures of logits, and prove that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit models.
2016–2019: Berbeglia and Joret prove the guarantees $1/k$ and $1/(1+\ln(r_k/r_1))$ under any regular choice model and show them tight (arXiv v1 2016, v3 2019; Algorithmica 2020). Aouad, Farias, Levi and Segev (2018) show that under random utility models no efficient algorithm does essentially better than these ratios.

Setting

There is a finite nonempty set $\mathcal C$ of products. For a choice set $S\subseteq\mathcal C$ , $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys product $x$ , and $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ is the probability that the customer buys nothing. The system $\mathcal P$ is a regular discrete choice model if

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

Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.

Each product has a positive price $r(x)>0$ . The revenue of $S$ is $\operatorname{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$ , and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\operatorname{rev}(S)$ . Let $0<r_1<\cdots<r_k$ be the distinct prices, so $k$ counts price levels and not products, and set $r_0=0$ . The revenue-ordered assortments are $S_i=\{x\in\mathcal C : r(x)\ge r_i\}$ , $i=1,\dots,k$ , and the heuristic earns

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

Formalization targets

Goal: Theorem 3.2

\mathrm{OPT}\;\le\;\Big(\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\Big)\,\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\;\le\;1+\ln\frac{r_k}{r_1}.

The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).

Milestones

Lemma 2.1: $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$ .
Inequality (5): $\operatorname{rev}(S_i)\ge r_i\sum_{x\in S^*\cap S_i}\mathcal P(x,S^*)$ for every $S^*$ and $i\in[k]$ .
Theorem 3.1: $\mathrm{OPT}\le k\cdot\mathrm{RO}$ .
Rearrangement (proof of Theorem 3.2): $\operatorname{rev}(S^*)=\sum_{\ell}(r_\ell-r_{\ell-1})\sum_{x\in S^*\cap S_\ell}\mathcal P(x,S^*)$ , and $\operatorname{rev}(S^*)\le\sum_\ell\frac{r_\ell-r_{\ell-1}}{r_\ell}\operatorname{rev}(S_\ell)$ .
Logarithmic bound: $\sum_{\ell=1}^k\frac{a_\ell-a_{\ell-1}}{a_\ell}\le1+\ln(a_k/a_1)$ for $0=a_0<a_1<\cdots<a_k$ .

Significance

The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of $k$ or of $r_k/r_1$ , that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.

Difficulty

The argument is short, but two points are easy to get wrong. First, revenues of $S_i$ and of an optimal $S^*$ involve choice probabilities evaluated at different sets, so the comparison must pass through $S^*\cap S_i$ , using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention $r_0=0$ ; indexing by products or dropping $r_0$ gives a different quantity. The comparison of the sum with $\ln(r_k/r_1)$ is a Riemann-sum estimate for $\int dt/t$ and needs a real-analysis lemma not phrased this way in Mathlib.

Formalization scope

Products are a finite nonempty type C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.
IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.
r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is $\operatorname{rev}(S)$ and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.
Price levels are 1-based: level r i is $r_i$ for $1\le i\le k$ and level r 0 = 0; numVals r is $k$ , the number of distinct values. roSet r i is $S_i$ ; roValue P r is the maximum over $i\in\{1,\dots,k\}$ only.
Approximation guarantees are stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$ , never as a ratio. $\ln$ is Real.log, applied to $r_k/r_1\ge1$ .
Ruled out: a maximum over all subsets in place of $\mathrm{RO}$ (which makes the bound trivial), a regularity axiom without its no-purchase case, the logarithmic form alone in place of the sum form, and any specific choice model (logit, Markov chain, random utility) in place of an arbitrary regular $\mathcal P$ .

Needed infrastructure: finite sums over price levels and summation by parts, the comparison of $(b-a)/b$ with $\ln(b/a)$ , and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular are welcome.

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.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
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
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

9 thms1 active userReviewed

Combinatorics Graph Theory Linear algebra·Captain: mikedeng1

Explicit Expanders of Every Degree and Size 3: Deleting Far-Apart Tree-Like Vertices of a Near-Ramanujan Graph and Matching Their Neighbours Keeps λ ≤ 2√(d−1) + εResearch Paper

Motivation

Sparse graphs with small nontrivial eigenvalues, expanders, are basic objects in combinatorics and theoretical computer science. They are used in error-correcting codes, derandomization, sorting networks, and the analysis of random walks. The Alon–Boppana bound says that a $d$ -regular graph on $n$ vertices has a nontrivial eigenvalue of absolute value at least $2\sqrt{d-1}-o(1)$ (Alon 1986; Nilli 1991). Graphs that reach $2\sqrt{d-1}$ are Ramanujan graphs.

The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (1988) and Margulis exist only for degrees $d = p+1$ with $p$ prime, and only for very sparse sequences of vertex counts. Constructions with $\lambda\le 2\sqrt{d-1}+\varepsilon$ for every degree came from Mohanty, O'Donnell and Paredes (STOC 2020, arXiv:1909.06988), but their graphs also do not have every number of vertices. Alon (arXiv:2003.11673, Combinatorica 41, 2021) asked for near-Ramanujan graphs of every degree and every large size. Theorem 1.3 of that paper answers this up to $\varepsilon$ : for every $d$ , every $\varepsilon>0$ and every large $n$ with $nd$ even there is an explicit $(n,d,\lambda)$ -graph with $\lambda\le 2\sqrt{d-1}+\varepsilon$ .

Setting

A $(n,d,\lambda)$ -graph is a $d$ -regular simple graph on $n$ vertices in which every nontrivial eigenvalue of the adjacency matrix $A$ has absolute value at most $\lambda$ . The trivial eigenvalue is $d$ , with the constant eigenvector $\mathbf 1$ . Equivalently, every eigenvalue $\mu$ of $A$ with an eigenvector $f\ne0$ , $\sum_v f(v)=0$ , satisfies $|\mu|\le\lambda$ .

Distances $\operatorname{dist}(v,w)$ are graph distances, and they are $\infty$ between components. The $k$ -neighbourhood of a vertex $v$ is $B(v,k)=\{w:\operatorname{dist}(v,w)\le k\}$ . The $k$ -neighbourhood of an edge $uv$ is $B(u,k)\cup B(v,k)$ , and $N_i$ is the set of vertices at distance exactly $i$ from $\{u,v\}$ . A set contains no cycle if the subgraph induced on it is a forest. A ball contains at most one cycle if its induced subgraph has at most as many edges as vertices.

The construction starts from a $d$ -regular graph $H$ on a vertex set $V$ and a set $U\subseteq V$ . Write $N(U)$ for the set of neighbours of $U$ , and let $m$ be a perfect matching on $N(U)$ . Then $H'$ is the subgraph induced on $V\setminus U$ , $M$ is the graph of matching edges $\{x,m(x)\}$ , and $G=H'\cup M$ .

Formalization targets

Goal: Theorem 1.3, relative to the input graph

Let $d\ge3$ , $\varepsilon>0$ , $r=\lceil 2/\varepsilon\rceil$ . Suppose $H$ is an $(N,d,2\sqrt{d-1}+\varepsilon/2)$ -graph in which the $(2r+4)$ -neighbourhood of every vertex contains at most one cycle, and $r\le\log_{d-1}N$ . Then for every $u$ with $ud$ even and $u\le N/(2d^{2r+3})$ ,

\exists\, G \text{ on } N-u \text{ vertices}:\quad G \text{ is an } \bigl(N-u,\ d,\ 2\sqrt{d-1}+\varepsilon\bigr)\text{-graph}.

The hypotheses on $H$ are what Theorem 3.3 (Mohanty–O'Donnell–Paredes) supplies, and that theorem is not formalized.

Milestones

Lemma 3.1 (p. 10). A $d$ -regular graph whose $(2r+4)$ -balls contain at most one cycle has a set $U$ with $|U|\ge n/(2d^{2r+3})$ , cycle-free $(r+1)$ -balls, and pairwise distances $\ge 2r+3$ .
Lemma 3.2 (p. 11). If the $r$ -neighbourhood of an edge $uv$ contains no cycle and $A f=\mu f$ with $\mu\ge2\sqrt{d-1}$ , then

\sum_{w\in N_i}f^2(w)\ \ge\ \sum_{w\in N_{i-1}}f^2(w),\qquad 1\le i\le r .

The variational characterization of nontrivial eigenvalues (§2.4, p. 8).
In $G=H'\cup M$ : $G$ is $d$ -regular on $|V|-|U|$ vertices and $A_G=A_{H'}+A_M$ . Matching edges have cycle-free $(r-1)$ -neighbourhoods and pairwise disjoint $r$ -neighbourhoods.
Inequalities (9), (10), (11) (p. 13), and the spectral step: for every admissible $U$ and $m$ , $G$ is an $(N-|U|,d,2\sqrt{d-1}+\varepsilon)$ -graph.

Significance

Theorem 1.3 shows that the size restrictions of algebraic Ramanujan constructions cost nothing spectrally: up to an arbitrarily small $\varepsilon$ , the Alon–Boppana bound is attained by explicit graphs on every admissible vertex count. The deletion method is local. It turns any near-Ramanujan graph whose short cycles are sparse into graphs of all nearby sizes, so it applies to future constructions as well. Lemma 3.2 is a self-contained delocalization statement in the tradition of Kahale 1995: eigenvectors of eigenvalues at least $2\sqrt{d-1}$ in absolute value cannot concentrate near tree-like edges.

The result is proved on paper. To our knowledge none of it is formalized; Mathlib has adjacency matrices, extended graph distance and acyclicity, but no theory of expanders. A complete development would give machine-checked versions of a delocalization lemma, of the greedy selection of far-apart vertices away from short cycles, and of the variational eigenvalue bound for induced subgraphs. It would also check two points the paper passes over. The proof of Theorem 1.3 treats only positive eigenvalues $\lambda\ge2\sqrt{d-1}$ . And its claim that the $r$ -neighbourhood of a matching edge is cycle-free fails when two deleted vertices are at distance exactly $2r+3$ . This mission states the corrected forms (see Formalization scope).

Difficulty

The spectral bound for $G$ does not follow from interlacing alone. Deleting vertices is harmless, since by (9) the quadratic form of $H'$ is controlled by $H$ . But the added matching contributes up to $\sum_{x\in N(U)}f(x)^2$ to $f^tA_Gf$ , which can be as large as $\|f\|^2$ for an eigenvector concentrated on $N(U)$ . The obvious estimate therefore gives only $\lambda\le 2\sqrt{d-1}+1+\varepsilon/2$ . Closing the gap requires showing that an eigenvector of a large eigenvalue spreads its mass over the $r$ layers around each matching edge (Lemma 3.2). That in turn needs those neighbourhoods to be trees in $G$ and pairwise disjoint, which is where Lemma 3.1's choice of $U$ is used. The combinatorial part, tracking distances and cycles in $G$ when $G$ mixes edges of $H$ with matching edges, is the main formalization burden.

Formalization scope

Representation. Vertex sets are finite types. Graphs are Mathlib SimpleGraphs with real adjacency matrices adjMatrix ℝ. The (n, d, λ) predicate requires IsRegularOfDegree d, symmetry, row sums $d$ , and $|\mu|\le\lambda$ for every eigenpair $(\mu,f)$ with $f\ne0$ , $\sum f=0$ . Distances use the extended SimpleGraph.edist, never dist (which is $0$ across components). Cycle conditions are on induced subgraphs, and "at most one cycle" on a ball is $|E|\le|V|$ . Deleted vertices are a Finset U; the new graph lives on the subtype {v // v ∉ U}. The matching is a fixed-point-free involution of $N(U)$ .
Explicit quantities replacing the paper's asymptotics. The paper writes "sufficiently large $n$ " and $u=o(n)$ . The goal instead takes any $u\le N/(2d^{2r+3})$ (the size Lemma 3.1 guarantees) with $ud$ even, plus Lemma 3.1's side condition $r\le\log_{d-1}N$ . The equality $r=\lceil2/\varepsilon\rceil$ is used as $\lceil2/\varepsilon\rceil_+\in\mathbb N$ . The paper's "every degree $d$ " becomes $d\ge3$ , the range of its proof.
Corrections. (11) and Lemma 3.2's companion are stated for $|\mu|\ge2\sqrt{d-1}$ , both signs. The matching-edge note is stated for the $(r-1)$ -neighbourhood, which still yields the factor $1/r$ in (11). Lemma 3.2 itself is stated as printed.
Out of scope. Theorem 3.3 ([18]) is a cited input: its graph is the hypothesis $H$ . All claims of explicitness and polynomial running time are out of scope, as is §4's remark on applying the method to LPS graphs directly.
No trivialization. The input hypotheses are exactly Theorem 3.3's conclusions plus Lemma 3.1's side condition, and they are met by high-girth Ramanujan graphs. No hypothesis mentions the spectrum or Rayleigh quotients of the constructed graph, and the goal's graph must be $d$ -regular on exactly $N-u$ vertices.
Reusable infrastructure. Welcome contributions include the variational characterization for symmetric matrices with constant row sums, a forest edge-count lemma for balls, BFS-layer structure of cycle-free balls in regular graphs, and the edge-disjoint decomposition $A_{G}=A_{H'}+A_M$ . Each is useful beyond this mission.

Selected references

N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
S. Mohanty, R. O'Donnell, P. Paredes, Explicit near-Ramanujan graphs of every degree, STOC 2020. https://arxiv.org/abs/1909.06988
A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988). https://doi.org/10.1007/BF02126799
N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986). https://doi.org/10.1007/BF02579166
A. Nilli, On the second eigenvalue of a graph, Discrete Mathematics 91 (1991). https://doi.org/10.1016/0012-365X(91)90112-F
N. Kahale, Eigenvalues and expansion of regular graphs, J. ACM 42 (1995). https://doi.org/10.1145/210118.210136

13 thms1 active userReviewed

Combinatorics Graph Theory Linear algebra·Captain: mikedeng1

Explicit Expanders of Every Degree and Size 2: Attaching New Vertices to a (p+1)-Regular Ramanujan Graph and Adding Loops Keeps Every Nontrivial Eigenvalue at Most √(2(p+1)) + √p + o(1)Research Paper

Motivation

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a $d$ -regular graph is governed by the Alon–Boppana bound $2\sqrt{d-1}$ , and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ( $d = p+1$ with $p$ prime) and special numbers of vertices (orders of $PSL(2,\mathbb F_q)$ or $SL(2,\mathbb F_q)$ ). Applications often need a graph of a prescribed size $n$ .

N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly $n$ vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on $m$ vertices can be enlarged to $n = m + r$ vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.

Setting

Let $V$ be a finite set of $m \ge 1$ vertices. A $(n,d,\lambda)$ -graph is a $d$ -regular graph on $n$ vertices whose adjacency matrix $A$ satisfies $|\mu| \le \lambda$ for every nontrivial eigenvalue $\mu$ , that is, every eigenvalue other than the top eigenvalue $d$ of the constant vector $\mathbf 1$ . For a symmetric $A$ with $A\mathbf 1 = d\,\mathbf 1$ , the nontrivial eigenvalues are those with an eigenvector $f \ne 0$ satisfying $\sum_v f(v) = 0$ . Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry $1$ of $A$ .

Fix an integer $p \ge 0$ and let $H$ be an $(m, p+1, 2\sqrt p)$ -graph on $V$ , a $(p+1)$ -regular Ramanujan graph. Let $R = \{u_1, \dots, u_r\}$ be $r$ new vertices and let $W_1, \dots, W_r \subseteq V$ be pairwise disjoint sets of $p+2$ vertices each. Put $W = \bigcup_i W_i$ and $L = V \setminus W$ . The graph $G$ on $U = V \cup R$ is obtained from $H$ by joining each $u_i$ to every vertex of $W_i$ and adding one loop at each vertex of $L$ . Its adjacency matrix is

A_G = A_H + A_R + A_L,

where $A_H$ is the adjacency matrix of $H$ (zero on $R$ ), $A_R$ that of the stars joining $u_i$ to $W_i$ , and $A_L$ the diagonal matrix of the loops. Every vertex of $G$ has degree $p+2$ .

Formalization targets

Goal: Theorem 1.2, spectral core

A_G \text{ is an } \Big(m+r,\; p+2,\; \sqrt{2(p+1)} + \sqrt p + \frac{(p+1)\,r}{m}\Big)\text{ matrix.}

The paper states $\lambda \le \sqrt{2(d-1)} + \sqrt{d-1} + o(1)$ for $d = p+2$ ; its proof gives $\sqrt{2(p+1)} + \sqrt p + o(1)$ , which is stronger, and the error term it produces is $(p+1)r/m$ . The goal is parametrised by $H$ , $r$ and the sets $W_i$ , so it does not depend on how $m$ and $r$ are chosen.

Milestones

The variational characterization of the nontrivial eigenvalues: for a symmetric matrix with constant row sums and $\lambda \ge 0$ , $|\mu| \le \lambda$ for every nontrivial eigenvalue if and only if $|f^tAf| \le \lambda\|f\|^2$ whenever $\sum f = 0$ .
The Cauchy–Schwarz display: $\sum_U f = 0$ implies $|\sum_V f|^2 = |\sum_R f|^2 \le |R| \sum_R f^2$ .
Inequality (3): $|f^tA_Hf| \le b^2(p+1) + c^2\, 2\sqrt p$ with $b^2 = (\sum_V f)^2/m$ and $c^2 = \sum_V f^2 - b^2$ .
Display (4): $f^tA_Lf = \sum_{v\in L} f^2(v)$ .
Inequality (5): $|f^tA_Rf| \le \frac{p+2}{x}\sum_R f^2 + x\sum_W f^2$ for every $x > 0$ .
Inequality (6): for $\sum_U f = 0$ and $x > 0$ ,

|f^tA_Gf| \le (2\sqrt p+1)\sum_L f^2 + (2\sqrt p+x)\sum_W f^2 + \frac{p+2}{x}\sum_R f^2 + (p+1)\frac rm \sum_R f^2.

Significance

With $H$ the Lubotzky–Phillips–Sarnak graph on $m = |SL(2,\mathbb F_q)|$ vertices for the largest suitable prime $q$ with $m \le n$ , and $r = n - m$ , the distribution of primes in arithmetic progressions gives $r = o(m)$ , and the goal yields an explicit $(n, p+2, \lambda)$ -graph with $\lambda \le (1+\sqrt2)\sqrt{d-1} + o(1)$ for every sufficiently large $n$ . This is within a factor of about $1.21$ of the Ramanujan bound $2\sqrt{d-1}$ , for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.

The result is proved in the paper. No formalization of it, of the $(n,d,\lambda)$ notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.

Difficulty

The vertices of $W$ and $L$ lie in the old graph $H$ , whose spectrum is controlled, but the new vertices of $R$ are not; and a vector orthogonal to $\mathbf 1$ on $U$ need not be orthogonal to the constant vector on $V$ . Bounding $f^tA_Gf$ by applying the Ramanujan bound for $H$ to $f$ restricted to $V$ therefore fails: the restriction has a component along the trivial eigenvector of $H$ , whose eigenvalue $p+1$ is large. The argument must show that this component is small, of order $r/m$ , and must balance the star edges between $R$ and $W$ against the loops on $L$ so that every vertex class gets the same coefficient. The naive bound $|f^tA_Rf| \le \|A_R\|\,\|f\|^2 = \sqrt{p+2}\,\|f\|^2$ added to $2\sqrt p$ for $H$ and $1$ for $L$ gives a constant larger than $\sqrt{2(p+1)}+\sqrt p$ ; the stated constant needs the weighted estimate.

On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace $\mathbf 1^\perp$ , while Mathlib states the spectral theorem for the whole space.

Formalization scope

Vertices of $G$ are the disjoint union $V \oplus \mathrm{Fin}\, r$ . $G$ is represented by its real adjacency matrix, since it has loops; $H$ is a Mathlib SimpleGraph with adjMatrix.
The $(n,d,\lambda)$ predicate is stated for matrices: $|V| = n$ , symmetry, $A\mathbf 1 = d\,\mathbf 1$ , and $|\mu| \le \lambda$ for every eigenpair $(\mu, f)$ with $f \ne 0$ and $\sum f = 0$ . For simple graphs, $d$ -regularity is added.
The paper's $o(1)$ terms are replaced by the explicit quantities its proof produces: $(p+1)r/m$ in the goal, and $(p+1)\frac rm\sum_R f^2$ in (6). Inequality (3) is stated with the corrected relation $b^2 + c^2 = \sum_V f^2$ ; the paper's " $b^2 + c^2 = 1$ " holds only for unit restrictions.
The bound uses $\sqrt p = \sqrt{d-2}$ , as in the proof and the abstract, which implies the printed $\sqrt{d-1}$ .
$p$ is any natural number. The hypothesis " $p$ prime, $p \equiv 1 \pmod 4$ " serves only to obtain $H$ from LPS, and $H$ is a hypothesis here. The sets $W_i$ are arbitrary pairwise disjoint sets of size $p+2$ , not the paper's consecutive blocks of a numbering of $SL(2,\mathbb F_q)$ .
Out of scope: the existence of the prime $q$ and the estimate $n - m = o(m)$ ; the numbering of $SL(2,\mathbb F_q)$ ; the "strongly explicit" and polynomial-time claims; the LPS construction (Theorem 2.1, cited); the variant that replaces loops by a matching for even $n$ .
The goal cannot be satisfied trivially: dropping the condition $\sum f = 0$ makes it false, since $p+2$ is always an eigenvalue, and for $p \ge 2$ and small $r/m$ the bound is below $p + 2$ (for $p = 5$ it is about $5.70 + 6r/m$ ). At $p = 1$ the bound $3 + 2r/m$ is at least the degree $3$ , so that case holds trivially; it is the paper's statement there as well.
Contributions welcome: proofs of each milestone, especially the variational characterization, which is reusable for mission 3 of this series and for any regular-graph spectral argument.

Selected references

N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

9 thms1 active userReviewed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

Solving Linear Programs in the Current Matrix Multiplication Time: The Stochastic Central Path Falls Back to a Classical Step with Probability at Most 10/n² per IterationResearch Paper

Motivation

Linear programming, $\min\{c^\top x : Ax=b,\ x\ge0\}$ with $A\in\mathbb R^{d\times n}$ , is the basic model of operations research, and the complexity of solving it is a central question of algorithm theory. Interior-point methods follow the central path: primal–dual pairs $(x,s)$ with $x,s>0$ and $x_is_i=t$ for every $i$ , as the path parameter $t$ decreases to $0$ . A classical short-step method needs $O(\sqrt n\log(n/\delta))$ iterations, each solving a linear system with the matrix $A\frac XSA^\top$ , for a total of roughly $n^{2.5}$ operations or more.

Cohen, Lee and Song (J. ACM 68(1), 2021; arXiv:1810.07896) showed that linear programs can be solved in time $n^{\omega+o(1)}\log(n/\delta)$ (for the current values of the matrix multiplication exponent $\omega$ and its dual $\alpha$ ), matching the cost of multiplying two $n\times n$ matrices. The analysis has two halves: a data structure that maintains the projection matrix lazily, and the stochastic central path method, which replaces each Newton step by a sparse random step and proves that the iterates still stay close to the central path. This mission formalizes the second half.

Timeline: Karmarkar's projective method (1984) gave the first polynomial interior-point method; Renegar (1988) gave the $O(\sqrt n\log(1/\delta))$ path-following bound; Vaidya (1989) reduced the per-iteration cost with low-rank updates; Lee and Sidford (2014–2015) reduced the iteration count to $\widetilde O(\sqrt d)$ ; Cohen, Lee and Song (STOC 2019, J. ACM 2021) reached $n^\omega$ ; van den Brand (2020) derandomized the result.

Setting

Vectors are in $\mathbb R^n$ and products, quotients and roots of vectors are coordinatewise. For $\epsilon$ and vectors $a,b$ , $a\approx_\epsilon b$ means $(1-\epsilon)b_i\le a_i\le(1+\epsilon)b_i$ for all $i$ ; $a\approx_\epsilon t$ for a scalar $t$ is defined likewise. The number of variables is $n\ge10$ and $A$ has full row rank $d\le n$ .

The potential is $\Phi_\lambda(r)=\sum_{i=1}^n\cosh(\lambda r_i)$ , evaluated at $r=\mu/t-1$ with $\mu=xs$ ; it is small exactly when every $x_is_i$ is close to $t$ .

StochasticStep (Algorithm 1) takes positive $x,s$ , a direction $\delta_\mu$ , a sampling parameter $k$ and the output $\widetilde v$ of a data structure with $x/s\approx_{\epsilon_{\mathrm{mp}}}\widetilde v$ . It rescales to $\overline x=x\sqrt{\widetilde v/w}$ , $\overline s=s\sqrt{w/\widetilde v}$ ( $w=x/s$ ), draws a sparse vector $\widetilde\delta_\mu$ with independent coordinates, $\widetilde\delta_{\mu,i}=\delta_{\mu,i}/p_i$ with probability $p_i=\min(1,k(\delta_{\mu,i}^2/\|\delta_\mu\|_2^2+1/n))$ and $0$ otherwise, and computes the step $(\widetilde\delta_x,\widetilde\delta_s)$ through the projection $\overline P=\sqrt{\overline X/\overline S}A^\top(A\frac{\overline X}{\overline S}A^\top)^{-1}A\sqrt{\overline X/\overline S}$ . The draw is repeated until $\|\overline s^{-1}\widetilde\delta_s\|_\infty$ and $\|\overline x^{-1}\widetilde\delta_x\|_\infty$ are at most $1/(100\log n)$ ; the output is $(x+\widetilde\delta_x,s+\widetilde\delta_s)$ .

Main (Algorithm 2) sets $\epsilon=\frac1{40000\log n}$ , $\epsilon_{\mathrm{mp}}=\frac1{40000}$ , $k=1000\epsilon\sqrt n\log^2n/\epsilon_{\mathrm{mp}}$ , $\lambda=40\log n$ , starts at $t=1$ , and in each iteration sets $t^{\mathrm{new}}=(1-\frac{\epsilon}{3\sqrt n})t$ , takes the direction

\delta_\mu=\Big(\frac{t^{\mathrm{new}}}{t}-1\Big)xs-\frac\epsilon2t^{\mathrm{new}}\frac{\nabla\Phi_\lambda(\mu/t-1)}{\|\nabla\Phi_\lambda(\mu/t-1)\|_2},

runs StochasticStep, and falls back to a deterministic ClassicalStep whenever $\Phi_\lambda(\mu^{\mathrm{new}}/t^{\mathrm{new}}-1)>n^3$ .

Formalization targets

Goal: Lemma 4.14

For every iteration $j$ , almost surely Assumption 4.1 holds for the input of iteration $j$ (in particular $x^js^j\approx_{0.1}t_j$ and $\|\delta_\mu\|_2\le\epsilon t_j$ ), almost surely the resampling loop of iteration $j$ succeeds with positive probability, and

\mathbb P(\text{ClassicalStep is used in iteration }j)\le\frac{10}{n^2}.

The paper writes $O(1/n^2)$ ; its proof gives the constant $10$ .

Milestones

Lemma A.1 (variance of a product), Lemma 4.12 (properties of $\Phi_\lambda$ ), Lemma 4.2 (explicit step), Lemma 4.3 and Claim 4.7 (moments and success probability of the sampled step), Lemma 4.8 (moments of $\mu^{\mathrm{new}}$ ), and Lemma 4.13:

\mathbf E\Big[\Phi_\lambda\Big(\frac{\mu^{\mathrm{new}}}{t^{\mathrm{new}}}-1\Big)\Big]\le\Phi_\lambda\Big(\frac\mu t-1\Big)-\frac{\lambda\epsilon}{15\sqrt n}\Big(\Phi_\lambda\Big(\frac\mu t-1\Big)-10n\Big).

Significance

Lemma 4.14 is what makes the randomized method usable: the iterates stay in the $0.1$ -neighbourhood of the central path along the whole run, and the expensive fallback is rare enough that its expected cost, $\widetilde O(n^{2.5})\cdot 10/n^2$ , is negligible. The paper's cost bound (Lemma 4.16) and its main theorem rest on it. The same potential-based "stochastic central path" analysis was reused in later solvers, for instance for empirical risk minimization (Lee, Song and Zhang, COLT 2019).

The result is proved in the paper; no machine-checked version exists. A formalization pins down the probabilistic model that the paper leaves implicit (independence of the sampled coordinates, the law of the resampling loop, a data structure and fallback that see only the past) and checks the constants, several of which are tight against printed slack (Remark 4.4).

The running-time claims of the paper (Theorem 2.1's expected time $n^{\omega+o(1)}$ , Lemma 4.16, Section 5) are not part of this mission: they live in an arithmetic cost model that Lean does not have. The accuracy guarantee of Theorem 2.1 (Lemma A.6, ClassicalStep from [57]) is also outside the mission.

Difficulty

The obvious argument would bound each quantity under the product law of the sparse direction. But StochasticStep resamples, so the step actually taken is distributed according to that law conditioned on a success event, and expectations and variances shift. A second difficulty is that $\Phi_\lambda$ is controlled only in expectation, while Assumption 4.1 must hold surely at every iteration; this is reconciled by the deterministic ClassicalStep fallback, which caps $\Phi_\lambda$ at $n^3$ , and by an induction over iterations of $\mathbf E[\Phi]\le10n$ under the trajectory law. Claim 4.7 needs a Bernstein inequality, which Mathlib does not yet provide.

Formalization scope

Coordinates are Fin n, vectors Fin n → ℝ, $A$ a Matrix (Fin d) (Fin n) ℝ with A.rank = d, and $\log$ the natural logarithm. $\|\cdot\|_2$ is written out as $\sqrt{\sum_iv_i^2}$ ; $\|\cdot\|_\infty\le c$ is stated coordinatewise. The sampled direction has law Measure.pi of two-point laws; the step taken by StochasticStep has that law conditioned (ProbabilityTheory.cond) on the success event, and every $\mathbf E$ , $\mathbf{Var}$ of Lemmas 4.3, 4.8 and 4.13 is under this conditioned law. mp.Query is replaced by its value $\overline P(\overline X\overline S)^{-1/2}\widetilde\delta_\mu$ ; the data structure and ClassicalStep are arbitrary measurable functions $U_j$ , $C_j$ of the history with the only properties the paper uses. The trajectory is Mathlib's Ionescu-Tulcea measure, with kernels equal to the step law of Main. $n$ is the number of variables of the program the loop runs on.

Deviations from the page, all recorded in the items: Assumption 4.1 is used with $\epsilon\le1/(40000\log n)$ instead of the printed $<$ , because Main sets $\epsilon$ to exactly that value; $O(1/n^2)$ is instantiated as $10/n^2$ , the constant of the paper's proof; the conclusions of Lemma 4.14 are stated for every iteration index rather than while $t>\delta^2/(32n^3)$ ; at $\nabla\Phi_\lambda=0$ the second term of $\delta_\mu$ is $0$ . No hypothesis $k\le n$ is imposed.

A trivializing formalization is ruled out: every statement that integrates against the conditioned law also concludes that this law is a probability measure (so it cannot be the zero measure), the goal concludes that each resampling loop succeeds with positive probability, the oracles $U_j$ , $C_j$ cannot see the coins of the current iteration, and the goal is about the whole iterated process from the initial point, not one step from an arbitrary law.

Contributions welcome: a Bernstein inequality for bounded independent sums, conditional-law lemmas for cond of Measure.pi, and Markov-kernel measurability for the step law; these are reusable beyond this mission.

Selected references

M. B. Cohen, Y. T. Lee, Z. Song, Solving Linear Programs in the Current Matrix Multiplication Time, J. ACM 68(1), Article 3, 2021. https://doi.org/10.1145/3424305 (arXiv:1810.07896, https://arxiv.org/abs/1810.07896)
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984. https://doi.org/10.1007/BF02579150
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40, 1988. https://doi.org/10.1007/BF01580724
P. M. Vaidya, Speeding-up linear programming using fast matrix multiplication, Proc. 30th FOCS, 1989.
Y. T. Lee, A. Sidford, Path finding methods for linear programming, FOCS 2014. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, Z. Song, Q. Zhang, Solving Empirical Risk Minimization in the Current Matrix Multiplication Time, COLT 2019. https://arxiv.org/abs/1905.04447
J. van den Brand, A deterministic linear program solver in current matrix multiplication time, SODA 2020. https://doi.org/10.1137/1.9781611975994.16

11 thms1 active userReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Approximation Algorithms for Stochastic Inventory Control Models 1: The Dual-Balancing Policy Costs at Most Twice the OptimumResearch Paper

Motivation

Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.

Setting

There are $T$ periods $t = 1, \dots, T$ and a known lead time $L \ge 0$ : an order placed in period $t$ arrives in period $t + L$ . Period $t$ has a per-unit holding cost $h_t \ge 0$ and a per-unit backlogging penalty $p_t \ge 0$ . Ordering costs are zero ( $c_t = 0$ ), which is the standing assumption of the paper's §4. The initial data are the net inventory $ni_0$ and the pipeline orders $q_{1-L}, \dots, q_0 \ge 0$ .

Demands $D_1, \dots, D_T$ are nonnegative random variables on a probability space with a filtration $(\mathcal F_t)$ ; $\mathcal F_t$ is the information at the beginning of period $t$ , and $D_t$ is $\mathcal F_{t+1}$ -measurable. A feasible policy $P$ places orders $Q^P_t \ge 0$ that are $\mathcal F_t$ -measurable. Write $D_{[s,t]} = \sum_{j=s}^t D_j$ (with $D_j = 0$ for $j \le 0$ ), $X_t = ni_0 + \sum_{j=1-L}^{t-1} Q_j - D_{[1,t-1]}$ for the inventory position before ordering and $Y_t = X_t + Q_t$ after ordering.

The marginal holding cost of period $t$ is the holding cost that the units ordered in $t$ incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:

H^P_t = \sum_{j=t+L}^{T} h_j\,\bigl(Q^P_t - (D_{[t,j]} - X^P_t)^+\bigr)^+, \qquad \Pi^P_t = p_{t+L}\,\bigl(D_{[t,t+L]} - Y^P_t\bigr)^+ .

The cost of $P$ is $\mathcal C(P) = \sum_{t=1}^{T-L}(H^P_t + \Pi^P_t)$ ; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.

A dual-balancing policy $B$ orders nothing after period $T - L$ , and in each period $t \le T - L$ orders the quantity that balances the two conditional expected marginal costs:

E\bigl[H^B_t \mid \mathcal F_t\bigr] = E\bigl[\Pi^B_t \mid \mathcal F_t\bigr] \quad\text{almost surely.}

Formalization targets

Goal: Theorem 4.1

For every dual-balancing policy $B$ and every feasible policy $P$ ,

E[\mathcal C(B)] \;\le\; 2\,E[\mathcal C(P)] .

The paper writes $P = OPT$ ; quantifying over all feasible $P$ is the same statement whenever an optimum exists and needs no existence assumption.

Milestones

Lemma 4.1. $E[\mathcal C(B)] = 2\sum_{t=1}^{T-L}E[Z_t]$ with $Z_t = E[H^B_t \mid \mathcal F_t]$ .
Lemma 4.2. With $\mathcal T_H = \{t : Y^B_t < Y^P_t\}$ , $\sum_{t\in\mathcal T_H} H^B_t \le \sum_{t=1}^{T-L} H^P_t$ on every realization.
Lemma 4.3. With $\mathcal T_\Pi = \{t : Y^B_t \ge Y^P_t\}$ , $\sum_{t\in\mathcal T_\Pi} \Pi^B_t \le \sum_{t=1}^{T-L} \Pi^P_t$ on every realization.

Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals $\sum_{t=1-L}^{0}\Pi_t + H_{(-\infty,0]} + \sum_{t=1}^{T-L}(H_t + \Pi_t)$ , which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when $h_T > 0$ and the demands are integrable, so the goal is not about an empty class.

Significance

The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.

Difficulty

The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets $\mathcal T_H$ and $\mathcal T_\Pi$ to be determined by the information of period $t$ , so that conditioning on $\mathcal F_t$ commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.

Formalization scope

Periods are integers (ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods $1, \dots, T$ are read, and the pipeline $q_t$ is substituted for $t \le 0$ .
Ordering costs are $c_t = 0$ and there is no discounting, as in the paper's §4; the reduction of §4.6 from general instances is not formalized. The lead time $L$ is general.
Information is an arbitrary Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.
Expected costs are lower Lebesgue integrals in $[0,\infty]$ , so an infinite expected cost is never read as $0$ .
The balancing condition carries integrability of $H^B_t$ and $\Pi^B_t$ , so a conditional expectation of a non-integrable cost (which Mathlib sets to $0$ ) cannot satisfy it vacuously. The existence item rules out an empty policy class.
Lemmas 4.2 and 4.3 are pathwise and do not use the balancing rule. The comparator totals are the marginal totals of Eq. (4), which is the stronger reading.
Eq. (2) prints $X_{t+L}$ and its restatement on p. 292 prints $p_t$ ; both are typos, and the formalization uses $X_t$ and $p_{t+L}$ .

A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded $\mathcal F_t$ -measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.

Selected references

R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. doi:10.1287/moor.1060.0205
D. C. Heath, P. L. Jackson, Modeling the evolution of demand forecasts with application to safety stock analysis in production/distribution systems, IIE Transactions 26(3):17–30, 1994. doi:10.1080/07408179408966604
P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000. ISBN 978-0-256-11379-7.

6 thms1 active userReviewed

Complexity Theory·Captain: hao jia

Weighted Falsifiability of Unambiguous DNFsOpen Problem

Motivation

A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?

This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless $\mathrm{P}=\mathrm{NP}$ , d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.

Historical note

The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.

Setting

Let $X=\{x_0,\ldots,x_{n-1}\}$ be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size $n$ ; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function $\nu:X\to\{0,1\}$ . A positive literal $x_i$ is true when $\nu(x_i)=1$ ; a negative literal $\neg x_i$ is true when $\nu(x_i)=0$ . A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.

The input also contains one positive integer weight $c_i$ for each variable and a positive threshold $t$ . The weight of an assignment is

w(\nu)=\sum_{i=0}^{n-1} c_i\nu(x_i).

The DNF is valid for this problem when every literal index is below $n$ and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least $t$ .

Formalization targets

Partial result — weighted satisfiability

For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least $t$ has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.

Partial result — unary-weight falsifiability

For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.

Goal — binary-weight falsifiability

For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.

The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.

Dependency graph

Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)

Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.

Significance

A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly $t$ ) is a different problem and is outside this mission's scope; the goal here is specifically weight at least $t$ .

Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.

Difficulty

The direct search over all $2^n$ assignments is exponential in $n$ . Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.

Formalization scope

The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.

The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.

The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.

Selected references

Albertine Amarilli, “Weighted falsifiability for unambiguous DNFs,” List of open questions in theoretical computer science, https://a3nm.net/work/research/questions/#weighted-falsifiability-for-unambiguous-dnfs.
Mikaël Monet, “Is this problem on unambiguous DNFs hard?”, Theoretical Computer Science Stack Exchange, https://cstheory.stackexchange.com/questions/53733/is-this-problem-on-unambiguous-dnfs-hard.

4 thms1 active userReviewed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Secretary Problems: Weights and Discounts 5: A 3e-Competitive Algorithm for the Graphic Matroid Secretary ProblemResearch Paper

Motivation

In the secretary problem, $n$ items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a $1/e$ fraction of the arrivals and then takes the first item better than everything seen picks the best item with probability at least $1/e$ (Ferguson 1989).

Babaioff, Immorlica and Kleinberg (SODA 2007; journal version J. ACM 2018) introduced the matroid secretary problem: the kept set must be independent in a known matroid. It models online auctions in which the feasible sets of winners have matroid structure, for example hiring along the edges of a network without closing a cycle. They gave a $16$ -competitive algorithm when the matroid is graphic, i.e. the items are the edges of a graph and a set is feasible when it contains no cycle.

Timeline for graphic matroids:

2007, Babaioff–Immorlica–Kleinberg: $16$ -competitive.
2009, Babaioff–Dinitz–Gupta–Immorlica–Talwar (SODA 2009, Theorem 1.5): $3e\approx 8.15$ -competitive, through a random reduction to partition matroids. This mission formalizes that result.
2009, Korula–Pál (ICALP 2009): $2e$ -competitive, by a different reduction.

Setting

Let $G=(V,E)$ be a finite simple graph. Each edge $e$ has a value $v(e)\ge 0$ . A set $S\subseteq E$ is independent in the graphic matroid of $G$ if the graph $(V,S)$ has no cycle. The offline optimum is

\mathrm{OPT}(G,v)=\max\Big\{\sum_{e\in S}v(e): S\subseteq E\ \text{acyclic}\Big\}.

The edges arrive in a uniformly random order. An algorithm sees each edge and its value on arrival and decides at once whether to select it. The selected set must be acyclic. The algorithm is $\alpha$ -competitive if $\mathrm{OPT}(G,v)\le\alpha\cdot\mathbb E[\text{value of the selected set}]$ for every $G$ and every $v\ge 0$ .

A partition matroid on a subset $U'\subseteq E$ is given by a family $P$ of nonempty, pairwise disjoint parts with union $U'$ : a set is independent when it lies in $U'$ and meets each part at most once. Its max-weight base has value $\mathrm{val}(P,v)=\sum_{p\in P}\max_{e\in p}v(e)$ .

Definition 5.1. A random partition $\mu$ (a probability distribution on such families, chosen from $G$ alone) is an $\alpha$ -partition scheme if every partition in its support has only acyclic independent sets, and for every $v\ge 0$ ,

\mathrm{OPT}(G,v)\le \alpha\cdot\mathbb E_{P\sim\mu}[\mathrm{val}(P,v)].

The random partition of Lemma 5.3. Pick an edge $\{u,w\}$ uniformly at random. With probability $\tfrac12$ colour $u$ red and $w$ blue, otherwise the reverse. Colour every other vertex red or blue independently with probability $\tfrac12$ . Each red vertex $x$ gets a part: the red-blue edges at $x$ . Then repeat on the edges with both endpoints blue, with fresh randomness.

The algorithm. Draw the partition, let the edges arrive, and on each part run the classical secretary rule on that part's arrivals. Output all selected edges.

Formalization targets

Goal: Theorem 1.5

For every finite simple graph $G$ and every $v\ge 0$ :

every possible output of the algorithm is an acyclic set of edges of $G$ ;

\mathrm{OPT}(G,v)\le 3e\cdot\mathbb E[\mathrm{ALG}].

Part 1 is needed for the statement to have content: an algorithm that selects every edge would otherwise satisfy part 2.

Milestones

Section 2, p. 4. On $m\ge1$ arrivals, the classical rule selects the maximum with probability at least $1/e$ .
Theorem 5.4, first clause. For a fixed partition $P$ , the per-part rule outputs a set independent in the partition matroid, and $\mathrm{val}(P,v)\le e\cdot\mathbb E_\pi[\mathrm{ALG}]$ .
Lemma 5.3, independence. Every partition the random construction can produce is a partition matroid on a subset of $E$ , and each of its independent sets is a forest.
Lemma 5.3. The construction is a $3$ -partition scheme.
Section 5, p. 10. Any $\alpha$ -partition scheme for a graphic matroid, combined with the per-part rule, gives a feasible, $e\alpha$ -competitive algorithm.

Significance

The theorem shows that the graphic matroid secretary problem admits a constant-competitive algorithm with a small explicit constant. It does so through a reduction: a random partition matroid that is feasible for the original matroid and loses only a constant factor in expectation. The reduction separates the combinatorics (Lemma 5.3) from the online part (Theorem 5.4). The same framework gives algorithms for uniform and transversal matroids and for the weighted and discounted variants on any matroid with an $\alpha$ -partition property.

The result is proved in the paper; it has not been formalized. The mission contributes a machine-checked version of the reduction, a formal treatment of a recursively defined random partition, and the classical secretary bound in a reusable finite form. The constant $3e$ is not the best known for graphic matroids (Korula–Pál improve it to $2e$ ), so the formal goal is this algorithm's guarantee, not the best possible ratio.

Difficulty

The online half is routine once the classical bound is available: the relative order of the edges in each part is uniform, and the parts are disjoint. The difficulty is Lemma 5.3. The natural idea of using a fixed optimal forest to build the partition is ruled out because the partition must be chosen before the values are seen. The expectation bound must therefore hold for every valuation at once, for a law that depends on the graph only. The construction is recursive and random: its expected value is not a closed-form sum, and any bound has to be carried through the random sequence of blue-blue subgraphs. Feasibility needs an invariant across rounds: the parts created later live inside the blue-blue edges of every earlier round.

Formalization scope

Graph. A SimpleGraph on a Fintype vertex type with decidable adjacency. The edges are G.edgeFinset, and acyclicity of $S$ is (SimpleGraph.fromEdgeSet S).IsAcyclic. Multigraphs are not covered.
Values. Values are a real function v : Sym2 V → ℝ with ∀ e, 0 ≤ v e; only the values on edges matter.
OPT is a Finset.sup' over acyclic subsets of the edge set. A partition is a finite family of nonempty, pairwise disjoint parts inside the edge set. Its max-weight base value is the sum of the part maxima.
Random partition. A PMF defined by well-founded recursion on the number of edges. Empty parts are dropped, and edges with two red endpoints are discarded.
Random order. The edges are numbered by a fixed enumeration. An arrival order is a permutation of the numbers, and expectation over the order is the average over all $|E|!$ permutations.
Classical rule. It samples $\lfloor m/e\rfloor$ arrivals of a part with $m$ edges. Ties are broken by preferring the smaller edge number among equal values.
Constants. Competitiveness is multiplicative ( $\mathrm{OPT}\le 3e\cdot\mathbb E[\mathrm{ALG}]$ ), so a zero expectation is not a loophole.
Ruling out trivial formalizations. In Definition 5.1 the random partition is fixed before the valuation, and the independence requirement holds for every partition in its support. A partition allowed to depend on $v$ would make every matroid $1$ -partitionable.

A complete development needs the classical secretary bound in finite form, the uniformity of induced sub-orders of a uniform permutation, expectations of PMF.bind along a well-founded recursion, and facts about forests in SimpleGraph. The first two, and a general graphic-matroid layer, are reusable beyond this mission. Proofs of any milestone, alternative proofs of Lemma 5.3, and extensions to the uniform and transversal cases of Theorem 5.2 are welcome.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443. https://dl.acm.org/doi/10.5555/1283383.1283429
M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Matroid Secretary Problems, Journal of the ACM 65(6), 2018. https://doi.org/10.1145/3212512
N. Korula, M. Pál, Algorithms for Secretary Problems on Graphs and Hypergraphs, ICALP 2009, LNCS 5556. https://doi.org/10.1007/978-3-642-02930-1_42
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

10 thms1 active userReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Secretary Problems: Weights and Discounts 1: An (8+3e)-Competitive Algorithm for the Weighted Secretary ProblemResearch Paper

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$ , each with a nonnegative value $v(e)$ , and $K$ goods indexed in decreasing order of nonnegative weight:

w(1)\ge w(2)\ge\cdots\ge w(K)\ge0.

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$ . Its value is $\sum_{k=1}^K v(s(k))w(k)$ . Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$ , chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$ , assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$ , the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$ , observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$ . A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$ .

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$ , which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$ :

\mathrm{OPT}\le(8+3e)\,\mathbb E[A].

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$ . Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class- $i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$ , the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$ . The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$ . It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$ . An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$ , so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

7 thms1 active userReviewed

Operations Research Probability·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 3: An Augmented Potential Function Yields an Explicit Deterministic α∘β-Competitive AlgorithmResearch Paper

Motivation

Competitive analysis measures an online algorithm, which must answer each request before seeing the next, against the best off-line answer to the whole request sequence. Randomized online algorithms are often much better than deterministic ones against an oblivious adversary, who fixes the requests in advance; the paging problem is the standard example. Against an adaptive adversary, who sees the algorithm's answers before choosing the next request, the advantage can disappear.

Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; preliminary version STOC 1990) made this precise in an abstract framework of request-answer games. Their Corollary 2.1 says: if a game has a randomized algorithm that is $\alpha$ -competitive against adaptive on-line adversaries and one that is $\beta$ -competitive against oblivious adversaries, then it has a deterministic $\alpha\circ\beta$ -competitive algorithm. That proof is non-constructive: it goes through a game-theoretic determinacy argument. Section 3 of the paper gives a constructive version. Most competitive analyses of randomized algorithms against adaptive adversaries are carried out with a potential function, in the style of Manasse, McGeoch and Sleator (J. Algorithms 11, 1990). The paper shows that such a potential function, together with any oblivious-competitive algorithm $H$ , determines an explicit deterministic algorithm $M$ , answer by answer. This mission formalizes that construction and its guarantee.

Setting

A request-answer game has a request set $R$ , a finite answer set $A$ and cost functions $f_n : R^n \times A^n \to \mathbb R$ . The off-line optimum of $r \in R^n$ is $c(r) = \min_{a \in A^n} f_n(r, a)$ . A deterministic online algorithm $M$ is a sequence of maps $m_i : R^i \to A$ ; on $r = (r_1,\dots,r_n)$ it answers $M(r) = (m_1(r_1), m_2(r_1,r_2), \dots, m_n(r))$ , at cost $c_M(r) = f_n(r, M(r))$ . It is $\alpha$ -competitive if $c_M(r) \le \alpha(c(r))$ for all $r$ . Throughout, $\alpha$ and $\beta$ are affine maps $\mathbb R \to \mathbb R$ (the paper's "linear functions").

A randomized online algorithm $H$ is a probability distribution over deterministic algorithms $H_y$ ; it is $\beta$ -competitive against any oblivious adversary if $\mathbb E_y[f_n(r, H_y(r))] \le \beta(c(r))$ for all $r$ . The algorithm $G$ analysed by the potential function is described by its next-answer laws $g_{n+1}(r r_{n+1}, a)$ on $A$ , given the requests so far, the new request and its own past answers. An adaptive on-line adversary $S$ chooses each request from the algorithm's past answers and answers it itself, before the algorithm does, for at most $d_Q$ rounds; a configuration after $n$ rounds is $(r, a, b) \in R^n \times A^n \times A^n$ : requests, algorithm's answers, adversary's answers.

An augmented potential function for $\alpha$ and $G$ (Definition 3.1) is a family $\Phi_n : R^n \times A^n \times A^n \to \mathbb R$ with (1) $\Phi_0 = 0$ ; (2) $\Phi_n(r,a,b) \le \alpha(f_n(r,b)) - f_n(r,a)$ for every configuration; (3) $\mathbb E_{a_{n+1} \sim g_{n+1}(r r_{n+1}, a)}[\Phi_{n+1}(r r_{n+1}, a a_{n+1}, b b_{n+1})] \ge \Phi_n(r,a,b)$ for every configuration, every $r_{n+1} \in R$ and every $b_{n+1} \in A$ .

Formalization targets

Goal: Theorem 3.1 (p. 15)

Let $\Phi$ be an augmented potential function for $\alpha$ and $G$ , and $H$ a $\beta$ -competitive algorithm against oblivious adversaries. Say that $M$ obeys the potential rule if for every $r \in R^n$ and $r' = rt$ ,

\mathbb E_y\big[\Phi_{n+1}(r', M(r)\,m_{n+1}(r'), H_y(r'))\big] \ \ge\ \mathbb E_y\big[\Phi_n(r, M(r), H_y(r))\big].

Then such an $M$ exists, and every such $M$ satisfies

c_M(r) \le \alpha\big(\beta(c(r))\big) \quad \text{for all } r .

Both parts are part of the goal: the rule can be followed, and following it guarantees $\alpha\circ\beta$ -competitiveness.

Milestones

In every play of $G$ against an adaptive on-line adversary, the expected final potential is nonnegative (proof of Lemma 3.1).
Lemma 3.1, "if" direction: an augmented potential function for $\alpha$ and $G$ makes $G$ $\alpha$ -competitive against any adaptive on-line adversary, $\mathbb E[c_G(S)] \le \mathbb E[\alpha(c_S(G))]$ .
For every $r$ , $t$ and every $a \in A^n$ , some $a' \in A$ satisfies $\mathbb E_y[\Phi_{n+1}(rt, aa', H_y(rt))] \ge \mathbb E_y[\Phi_n(r, a, H_y(r))]$ .
If $M$ obeys the rule, $\mathbb E_y[\Phi_n(r, M(r), H_y(r))] \ge 0$ for every $r$ .
If $M$ obeys the rule, $f_n(r, M(r)) \le \mathbb E_y[\alpha(f_n(r, H_y(r)))]$ for every $r$ : $M$ is $\alpha$ -competitive against the randomized adaptive adversary that serves its requests with $H$ .

Significance

The theorem turns two separate analyses into one deterministic algorithm with an explicit description. The potential function certifies $G$ against the strongest on-line adversary; the oblivious algorithm $H$ need not be related to $G$ , and the paper remarks that $H$ may be $G$ itself. The next answer of $M$ is computable whenever the expected potential under $H$ is (Corollary 3.1, stated informally in the paper), and the paper notes that for the potential functions used in the $K$ -server literature this expectation is computable in time polynomial in the number of nodes and $K$ . Read in this light, a potential-function proof for a randomized algorithm doubles as a deterministic algorithm.

The result is proved in the paper. As far as is known, neither this theorem nor the abstract framework of request-answer games with adaptive adversaries has a machine-checked formalization. The mission produces that framework and a checked derandomization principle that applies to every request-answer game with real costs, not to one problem.

Difficulty

The obvious argument for the existence of $m_{n+1}(r')$ averages property (3) of $\Phi$ ; the work is in seeing which configuration to apply it to. The rule compares $M$ 's configuration against $H_y$ 's answers, not against an adversary playing $G$ , and the paper argues through an auxiliary on-line adversary that asks $r'$ and serves it with $H_y$ . Making this rigorous requires interchanging the expectation over $H$ 's coins with the finite expectation over $G$ 's next answer, and checking that the needed expectations are finite.

The second difficulty is the two kinds of randomness. $G$ enters only through its next-answer laws, while $H$ must be a single distribution over deterministic algorithms: the rule evaluates $H_y(r)$ and $H_y(r')$ with the same coins $y$ . Replacing $H$ by a behavioural description breaks the coupling between consecutive rounds.

Formalization scope

Requests and answers are Lean lists, oldest first, and $f_n(r,a)$ is F.cost r a on lists of common length; values on lists of different lengths are never used. Costs are real: the paper allows $f_n = +\infty$ , so every statement here is about the real-valued games. The answer type is finite and nonempty, so the minimum $c(r)$ exists. Affine maps are written $\alpha(x) = c x + d$ . The goal additionally assumes $\alpha$ nondecreasing: the last step of the paper's proof applies $\alpha$ to an inequality, which needs it, and the paper's examples are positive ratios. In Lemma 3.1 and milestone 5 linearity of $\alpha$ is kept as the paper's standing convention, although with $\alpha$ inside the expectation the argument does not use it.

$G$ is a map from (requests, own answers) to a probability mass function on $A$ (behavioural form); its play against an adaptive on-line adversary is a probability mass function on final configurations, with finite support, and its expectations are finite sums. $H$ is a probability measure on a coin space with a deterministic algorithm per coin, each answer measurable in the coins; expectations over $H$ are Bochner integrals of functions with finitely many values. $\alpha$ stays inside expectations, as in the paper's definition of competitiveness against adaptive adversaries. Adversaries stop by returning none and have a uniform depth bound.

The goal cannot be satisfied vacuously: it states the existence of an algorithm obeying the rule alongside the guarantee for every such algorithm, and Definition 3.1 is required at every configuration, not only at reachable ones.

Not formalized: the "only if" direction of Lemma 3.1, which the paper only sketches, and Corollary 3.1, whose notion of computability the paper leaves unspecified. The definitions of request-answer games, online algorithms, adversaries and competitiveness are reusable for the other missions of this paper and for any problem-specific competitive analysis. Contributions welcome: proofs of the milestones, and a lemma relating the mixed and behavioural forms of a randomized algorithm.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994), 2–14. https://doi.org/10.1007/BF01294260
M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11 (1990), 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
D. Sleator, R. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28 (1985), 202–208. https://doi.org/10.1145/2786.2793
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5

9 thms1 active userReviewed

Operations Research Probability·Captain: mikedeng1

Secretary Problems: Weights and Discounts 2: An Ω(log n / log log n) Lower Bound on the Competitive Ratio of the Discounted Secretary ProblemResearch Paper

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least $1/e$ , so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time $t$ is worth $d(t)\,v(e)$ for a known discount function $d$ . Discounts model settings where a sale is worth more at some times than at others. The case $d(t)=\beta^t$ had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary $d$ . Its answer has two sides: an $O(\log n)$ -competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than $\Omega(\log n/\log\log n)$ -competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.

Setting

There are $n$ elements $e\in\{0,\dots,n-1\}$ with values $v(e)\ge 0$ , and a discount function $d$ on the times. The elements arrive in a uniformly random order $\pi$ : element $\pi(t)$ arrives at time $t$ . A randomized online stopping rule $A$ specifies, for each time $t$ and each sequence of values seen so far $h=(v(\pi(0)),\dots,v(\pi(t)))$ , a probability $p_t(h)\in[0,1]$ of stopping at $t$ if it has not stopped yet. Stopping at $t$ selects $\pi(t)$ and earns $d(t)\,v(\pi(t))$ ; the rule selects at most one element and may select none. The rule knows $n$ and $d$ , but it sees only values, only as they arrive, and it is not told which instance it is facing.

The expected value of $A$ is

\mathbb E[A]=\mathbb E_\pi\Bigl[\sum_t d(t)\,v(\pi(t))\,p_t(h_t)\prod_{s<t}\bigl(1-p_s(h_s)\bigr)\Bigr],

and the benchmark is the expected offline optimum

\mathbb E[\mathrm{OPT}]=\mathbb E_\pi\Bigl[\max_t d(t)\,v(\pi(t))\Bigr],

which is itself a random variable averaged over the order. $A$ is $\alpha$ -competitive on an instance when $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$ .

The hard family (§4.1.1 of the paper): fix an integer $c\ge1$ and put $L=c$ , $n=L^{4c}$ , $n_t=L^{2t}$ for $t\le 2c$ , and $K=n^2$ . The step discount is $d(j)=L^{-1}$ on the times $1\le j\le n_1$ and $d(j)=L^{-t}$ on $n_{t-1}<j\le n_t$ . The instance $\mathcal I_1$ has $n/n_1$ elements of value $K$ and the rest $0$ ; $\mathcal I_{t+1}$ is obtained from $\mathcal I_t$ by raising $n/n_{t+1}$ of its values $K^t$ to $K^{t+1}$ , so $\mathcal I_t$ has $n/n_t$ elements of value $K^t$ .

Formalization targets

Goal: Theorem 4.3 in the form its proof establishes

For every integer $c\ge1$ and every randomized online stopping rule $A$ for horizon $n=c^{4c}$ and the step discount,

\exists\,t\in\{1,\dots,2c\}:\qquad c\cdot\mathbb E[A(\mathcal I_t)]\ <\ 10\cdot\mathbb E[\mathrm{OPT}(\mathcal I_t)].

That is, no online rule is $c/10$ -competitive on all of $\mathcal I_1,\dots,\mathcal I_{2c}$ .

Milestones

Lemma 4.1: $\mathbb E[\mathrm{OPT}(\mathcal I_t)]\ge(1-1/e)K^tL^{-t}$ for $1\le t\le 2c$ .
Coupling step of Lemma 4.2's proof: for every rule and $1\le t<2c$ , the probability of stopping among the first $n_t$ arrivals drops by at most $1/L^2$ from $\mathcal I_t$ to $\mathcal I_{t+1}$ .
Lemma 4.2: a rule that is $c/10$ -competitive on $\mathcal I_1,\dots,\mathcal I_{2c}$ stops among the first $n_t$ arrivals of $\mathcal I_t$ with probability at least $t/c$ .
Theorem 4.3, asymptotic form: for $c\ge2$ and $n=c^{4c}$ , every rule has some $\mathcal I_t$ with

\frac1{40}\cdot\frac{\log n}{\log\log n}\cdot\mathbb E[A(\mathcal I_t)]<\mathbb E[\mathrm{OPT}(\mathcal I_t)].

Significance

The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the $e$ -competitive classical rule). Together with the paper's $O(\log n)$ upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between $\log n/\log\log n$ and $\log n$ up to constants, and it motivates the paper's known- $\mathrm{OPT}$ model (§4.2), where an estimate of $\mathbb E[\mathrm{OPT}]$ restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.

The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the $O(\log n)$ upper bound, and the $\sqrt2$ lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.

Difficulty

The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the $2c$ instances against each other. A rule that does well on $\mathcal I_t$ must commit early, within the first $n_t$ steps, yet the rule cannot distinguish $\mathcal I_t$ from $\mathcal I_{t+1}$ during those steps except with probability $L^{-2}$ . Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time $t$ depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on $\mathcal I_{t+1}$ and its late earnings are both small compared with $\mathbb E[\mathrm{OPT}(\mathcal I_{t+1})]$ , which uses $L\ge 2$ and that $K=n^2$ dwarfs $L^{2c}$ .

Formalization scope

Elements and times are Fin n, 0-based: index $j$ is the paper's time $j+1$ , so the paper's block $(n_{t-1},n_t]$ is the index range $[n_{t-1},n_t)$ . The random order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and every expectation over it is the finite average $\frac1{n!}\sum_\pi$ . Values and discounts are real.
Algorithms are the structure StoppingRule n: stopping probabilities $p_t(h)\in[0,1]$ indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that $p_t(h)$ depends only on $h_0,\dots,h_t$ . The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on $n$ and $d$ but not on the instance index.
OPT is $\mathbb E_\pi[\max_t d(t)v(\pi(t))]$ (a supremum over the finite type Fin n), and competitiveness is multiplicative, $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$ , never a quotient.
Constants. The goal uses the paper's constant $10$ (from "if $A$ is $c/10$ -competitive"); the asymptotic form uses $1/40$ , from $\log n/\log\log n\le 4c$ for $c\ge2$ , with the natural logarithm. $K=n^2$ , the value the paper suggests.
The construction ( $n$ , $n_t$ , $d$ , $K$ , $\mathcal I_t$ ) is fixed by explicit formulas in the definition file. A solver cannot choose the discount or the instances, and the goal is not stated for a restricted class of algorithms; a formalization that let the rule see the instance index or future values, or quantified only over threshold rules, would be a different and trivial or weaker theorem. For $c<10$ the goal is immediate, since $\mathbb E[A]\le\mathbb E[\mathrm{OPT}]$ and $\mathbb E[\mathrm{OPT}(\mathcal I_t)]>0$ ; the content lies in $c\ge10$ . The bound is stated only for the horizons $n=c^{4c}$ the paper constructs.
Needed infrastructure: counting arguments over permutations of Fin n (the probability that a set of $m$ elements misses the first $k$ positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135 (authors' full version, the one cited here: https://www.cs.jhu.edu/~mdinitz/papers/secretary.pdf)
E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR, 1963.
W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3), 1976.
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

7 thms1 active userReviewed

Captain: Goku

QMA Strong Error Reduction with No Witness-Length IncreaseResearch Paper

Motivation

A QMA verifier receives a quantum witness and checks it with a circuit generated efficiently from the input. An acceptance probability separated by an inverse-polynomial gap is enough to define the class, but applications often need the probability of a wrong answer to be exponentially small. Repeating the verifier on many supplied witness registers achieves this error reduction while allowing the witness to grow. Marriott and Watrous proved the stronger statement that the same error reduction can be obtained without increasing the number of witness qubits Quantum Arthur–Merlin Games, Section 3.

The existing Lean development verifies the copy-based theorem, including soundness for witnesses entangled across the copies, and constructs a uniform circuit family with polynomial resources. This mission asks for the separate witness-preserving theorem. The paper already proves that mathematical statement; the open work here is its formalization in the stated QMA circuit model.

Setting

At each input length $n$ , a verifier has $m(n)$ witness qubits, a finite work register, a designated output wire, and a quantum circuit. A uniformly generated family has a polynomial-time classical procedure that emits the complete circuit description, including the witness and work-register sizes. On yes-instances, some normalized witness makes the verifier accept with probability at least $a(n)$ . On no-instances, every normalized witness is accepted with probability at most $b(n)$ . The thresholds satisfy $0\le b(n)\le a(n)\le1$ and $a(n)-b(n)\ge1/q(n)$ for a polynomial $q$ .

The existing formalization represents witnesses as complex amplitude functions on bit strings, requires normalization explicitly, and uses layered circuits over its specified finite gate set. It also represents efficiently available real thresholds by polynomial-time procedures that output dyadic approximations. These are part of the formal statement's interface and must be made visible to users of the mission.

Target

For every polynomial error exponent $r$ and every source verifier satisfying the conditions above, construct a uniformly generated, well-formed, polynomial-resource verifier for the same language, with completeness at least $1-2^{-r(n)}$ and soundness at most $2^{-r(n)}$ , while keeping the witness count exactly $m(n)$ at every input length:

m_{\mathrm{new}}(n)=m_{\mathrm{old}}(n).

This is the witness-preserving strong error-reduction result of Marriott and Watrous (Theorem 4). The existing copy-based result corresponds to the weaker QMA class inclusion in Theorem 3 and will be linked as a proved background result. The mission goal must state the witness-count equation explicitly so that a copy-based amplifier cannot satisfy it.

Significance

Witness-preserving amplification lets a QMA protocol demand much stronger reliability without asking the prover for a longer message. That matters whenever witness size is itself a resource being compared or bounded. The copy-based theorem shows that the QMA class is robust under error reduction, but does not establish this fixed-message guarantee.

Formalizing the stronger result would add a reusable account of a verifier that reuses one witness, proves soundness for every normalized input state, and compiles its behavior into an ordinary uniform circuit family. Those components can support later formalizations that reason about repeated quantum verification under a fixed witness budget.

Difficulty

The completed copy-based proof uses three independent verifier blocks in each amplification round and bounds arbitrary entangled witnesses across those blocks. Its circuit resource analysis therefore allows the witness count to grow. A witness-preserving argument cannot use that construction. It must analyze repeated verification on one register and establish exponentially small error without assuming the input witness has a special spectral form. The formal circuit model currently exposes final-output measurements; any additional measurement behavior used in the analysis must be justified in that model and shown implementable by a finite, uniformly generated circuit.

The central audit point is the exact witness-length equation. A theorem that merely returns another polynomial-size witness, or that changes the source verifier's witness definition, is a useful class-level result but does not prove this mission's target.

Formalization scope

The goal is parameterized by input-length-dependent completeness and soundness thresholds with an inverse-polynomial gap, and by a polynomial target exponent. Every witness quantifier is over normalized states. The output verifier must satisfy the same well-formedness and polynomial-resource conditions as the completed copy-based development. The platform statement uses its existing ShiClassQMAU.UniformQMA circuit-family encoding, which includes the witness and ancilla counts separately. A final proof should be kernel checked with only Lean's standard logical axioms and should not assume an amplification transducer or an unproved measurement lemma.

The paper quantifies over the class poly of unary-time constructible functions. This proposal represents the gap denominator and target exponent as literal Polynomial ℕ values, matching the checked copy-based development. It therefore formalizes a polynomial-parameter instance of Theorem 4 rather than the paper's full function-class generality. The threshold functions are supplied by polynomial-time dyadic approximators in place of the paper's informal efficient-computation convention. These interface choices are explicit in the Lean goal and should not be read as a proof of the broader formulation.

The local copy-based proof is complete and audited, but it has not yet been transplanted to Prove2Me. Its publication is preparatory work for this mission, not evidence that the witness-preserving goal is already solved. The proposal should reference the published copy-based endpoint and include only a few substantial milestones, so each item is meaningful to audit.

Selected references

C. Marriott and J. Watrous, Quantum Arthur–Merlin Games, Computational Complexity 14 (2005), Section 3, Theorems 3 and 4. Paper.
A. Kitaev, A. Shen, and M. Vyalyi, Classical and Quantum Computation, Graduate Studies in Mathematics 47, American Mathematical Society (2002), Section 14.2, cited by Marriott and Watrous for the copy-based amplification proof.

3 thms1 active userReviewed

Machine Learning Operations Research Probability·Captain: mikedeng1

Competitive Caching with Machine Learned Advice: The Competitive Ratio of Predictive MarkerResearch Paper

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$ -competitive, and the best randomized algorithms are $\Theta(\log k)$ -competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

1966: Bélády's furthest-in-future rule is optimal offline.
1985: Sleator and Tarjan show that deterministic online paging is at best $k$ -competitive.
1991: Fiat et al. introduce the Marker algorithm, $2H_k$ -competitive, and the clean-element lower bound on the optimum.
2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$ -accurate predictor.
2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$ . A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$ .

With each request $z_i$ the algorithm receives a real prediction $h_i$ . The true label $y_i$ is the position of the next request of $z_i$ , or $n+1$ if there is none. For a loss function $\ell \ge 0$ , the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$ , and the predictions are $\epsilon$ -accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$ .

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$ .

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$ , the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$ .

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$ , every tie-breaking rule, and every sequence with $\epsilon$ -accurate predictions,

\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).

Milestones

Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$ .
Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$ .
Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$ , where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$ .

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ( $\epsilon = 0$ ) the ratio is a constant, $2(1 + 2S(0))$ , independent of $k$ ; for an arbitrary predictor it is $4H_k$ , within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$ , so the ratio grows like $\sqrt\epsilon$ . The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$ .

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$ , not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$ .

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$ .

The spread takes real arguments and lengths $T \ge 1$ . $S$ must be concave on $[0,\infty)$ , finite, and at least the spread. It must also be continuous at $0$ , which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$ -accuracy is the pointwise condition on the given pair $(\sigma, h)$ . The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$ , with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$ .

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716

10 thms1 active userReviewed

Operations Research Optimization Probability·Captain: mikedeng1

An Optimal On-Line Algorithm for Metrical Task System 2: The Randomized Competitive Ratio of the Uniform Task System Lies Between H(n) and 2H(n)Research Paper

Motivation

Metrical task systems, introduced by Borodin, Linial and Saks (J. ACM 39(4), 1992), are a common abstraction of on-line problems in which a server occupies one of finitely many states, pays a cost for each task depending on its current state, and may pay a transition cost to change state first. Paging, list update and the $k$ -server problem all fit into this framework. The paper's first main result is that every deterministic on-line algorithm on an $n$ -state metrical task system has competitive ratio at least $2n-1$ , and that $2n-1$ is attained. The lower bound comes from an adversary that always charges the state the algorithm currently occupies. That adversary needs to know the algorithm's state, which suggests that randomization can help.

Section 7 of the paper makes this precise for the simplest system, the uniform task system, in which all transitions cost $1$ . There the randomized competitive ratio against an oblivious adversary is between $H(n)$ and $2H(n)$ , where $H(n)=1+\tfrac12+\cdots+\tfrac1n$ is between $\ln n$ and $1+\ln n$ . This was the first logarithmic bound for a task system.

Timeline:

1985: Sleator and Tarjan introduce competitive analysis for list update and paging (CACM 28(2)).
1987/1992: Borodin, Linial and Saks define metrical task systems, prove the deterministic ratio $2n-1$ , and prove $H(n)\le\bar w\le 2H(n)$ for the uniform system (conference version STOC 1987; journal version cited above).
1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the analogous $2H_k$ upper bound for randomized paging (J. Algorithms 12(4)).

Setting

A task system $(S,d)$ is a finite set $S$ of $n$ states with a transition-cost matrix $d$ : $d(i,i)=0$ , $d(i,j)>0$ for $i\ne j$ , and $d(i,k)\le d(i,j)+d(j,k)$ . In the uniform task system, $d(i,j)=1$ for all $i\neq j$ . A task is a vector $T\in\mathbb R_{\ge0}^S$ of processing costs. Given an initial state $s_0$ and tasks $\mathbf T=T^1\cdots T^m$ , a schedule is $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$ , of cost

c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).

The off-line optimum $c_0(\mathbf T)$ is the least cost over all schedules.

A deterministic on-line algorithm chooses $\sigma(i)$ from $s_0$ and $T^1,\dots,T^i$ . A randomized on-line algorithm $R$ chooses $\sigma(i)$ at random, with a distribution that depends on $s_0$ , on $T^1,\dots,T^i$ and on the states $\sigma(0),\dots,\sigma(i-1)$ already visited. The task sequence is fixed before any random choice is made (an oblivious adversary). With $\mathrm{pr}(\sigma\mid\mathbf T)$ the probability that $R$ follows $\sigma$ , the expected cost is $\bar c_R(\mathbf T)=\sum_\sigma c(\mathbf T;\sigma)\,\mathrm{pr}(\sigma\mid\mathbf T)$ . For $w>0$ , $R$ is expected $w$ -competitive if there is a constant $K$ with

\bar c_R(\mathbf T)\le w\,c_0(\mathbf T)+K

for every finite task sequence and every initial state. The randomized competitive ratio $\bar w(S,d)$ is the infimum of all such $w$ over all $R$ .

Formalization targets

Goal: Theorem 7.1

For the uniform task system on $n\ge1$ states,

H(n)\;\le\;\bar w(S,d)\;\le\;2H(n).

Milestones

Upper bound (p. 759). Some randomized on-line algorithm is expected $2H(n)$ -competitive on the uniform task system.
Lemma 7.2 (p. 759). Let $D$ be a distribution on infinite task sequences over a finite task alphabet, with $E(c_0(\mathbf T^j))\to\infty$ , and let $m_j=\inf_A E(c_A(\mathbf T^j))$ over deterministic on-line algorithms. Then every achievable $w$ satisfies

\limsup_{j\to\infty}\frac{m_j}{E(c_0(\mathbf T^j))}\le w .

$m_j\ge j/n$ (p. 760) when the tasks are independent uniformly random unit elementary tasks $U_s$ (cost $1$ in $s$ , $0$ elsewhere).
Coupon collector (p. 760). For i.i.d. uniform states on $S$ , the expected number of draws until every state has appeared is $nH(n)$ .
Off-line cost (p. 760). Under the same distribution, $E(c_0(\mathbf T^j))\le j/(nH(n))+C$ for a constant $C$ independent of $j$ .

Significance

The theorem shows that randomization reduces the competitive ratio of the uniform task system from $2n-1$ to $\Theta(\log n)$ . That is an exponential improvement, and it identifies the adversary's knowledge of the algorithm's state as the source of the deterministic lower bound. Lemma 7.2 is a form of Yao's principle adapted to the additive-constant definition of competitiveness. It is the standard tool for randomized lower bounds in on-line computation, and the same argument shape reappears for paging and $k$ -server lower bounds.

On the formalization side, the result is proved but, as far as is known, has not been machine-checked. A complete development yields a reusable model of randomized on-line algorithms with oblivious adversaries, a Yao-type lemma usable for other on-line problems, and a coupon-collector expectation in the product-measure setting. The upper half additionally needs the continuous-time reduction of the paper's Lemma 3.1 in randomized form, or a direct discrete-time algorithm.

Difficulty

For the upper bound, the natural algorithm is continuous-time. It proceeds in phases, and inside a phase it stays in a state until that state has accumulated cost $1$ . A discrete task can saturate several states at once and straddle a phase boundary. So a discrete algorithm must either simulate the continuous one or be analyzed directly, and the expected transition count per phase must be controlled with the first phase starting in a deterministic state.

For the lower bound, the first obstacle is that the natural statement " $\bar w\ge\limsup m_j/E(c_0)$ " silently assumes that a randomized algorithm's expected cost, averaged over random inputs, is at least that of the best deterministic algorithm. With the behavioural (kernel) definition used here, this requires converting a kernel into a mixture of deterministic algorithms, which is Kuhn's theorem on each finite horizon. The second obstacle is that the paper's claim $E(c_0(\mathbf T^j))\le j/(nH(n))+O(1)$ is supported only by the elementary renewal theorem, which gives a limit of ratios; the additive bound needs a sharper renewal estimate. Mathlib has no renewal theory. The hypothesis $E(c_0(\mathbf T^j))\to\infty$ of Lemma 7.2 must also be established for the uniform distribution; the paper does not prove it separately.

Formalization scope

States form a finite nonempty type S, and $n$ = Fintype.card S; no $n\ge2$ assumption is made (at $n=1$ the goal reads $1\le\bar w\le2$ , and $\bar w=1$ ). $H(n)$ is Mathlib's harmonic n, cast to $\mathbb R$ . The uniform system has unit transition cost.
Tasks are finite and nonnegative. The paper also allows $+\infty$ entries; these are excluded. Task sequences are Fin m → S → ℝ and schedules are Fin (m+1) → S with σ 0 = s₀. $c_0$ is a finite minimum.
A randomized algorithm is a kernel S → List (S → ℝ) → List S → PMF S. This is the paper's scheduler–taskmaster description (p. 758), equivalent to a distribution over deterministic algorithms on every finite task sequence. $\mathrm{pr}(\sigma\mid\mathbf T)$ is the product of kernel probabilities, and $\bar c_R$ is a finite sum. That $\mathrm{pr}(\cdot\mid\mathbf T)$ sums to $1$ has been checked locally.
$\bar w(S,d)$ is the real sInf of $\{w : \exists R,\ R \text{ expected } w\text{-competitive}\}$ . On the empty set this would be $0$ , so the upper bound is stated as the existence of an expected $2H(n)$ -competitive algorithm, and Lemma 7.2 is stated for every achievable $w$ . The goal's lower half forces the set to be nonempty. Statements of the form " $\bar w\le c$ " alone are therefore not acceptable substitutes for milestones 1 and 2.
Lemma 7.2 is restricted to task sequences over a finite alphabet, with the product $\sigma$ -algebra and measurable singletons. This makes every $E(c_A(\mathbf T^j))$ a genuine integral for every deterministic $A$ , and it covers the paper's application. The $\limsup$ of Lemma 7.2 is taken in EReal.
The coupon-collector time takes values in $[0,\infty]$ and its expectation is a lower Lebesgue integral. Milestone 5 renders the paper's $O(1)$ as an explicit constant $C$ chosen before $j$ .

Contributions welcome: proofs of any milestone; a discrete-time randomized phase algorithm; a general Kuhn-type conversion from kernels to mixtures of deterministic algorithms; renewal-theoretic lemmas.

Selected references

A. Borodin, N. Linial, M. Saks, An Optimal On-Line Algorithm for Metrical Task System, J. ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Commun. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
A. C.-C. Yao, Probabilistic Computations: Toward a Unified Measure of Complexity, FOCS 1977, 222–227. https://doi.org/10.1109/SFCS.1977.24
S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970 (the elementary renewal theorem cited as [20] in the paper).

9 thms1 active userReviewed

Information Theory·Captain: marwahaha

Most Informative Boolean Function ConjectureResearch Paper

One bit of a noisy string

Send a uniformly random string $X \in \{0,1\}^n$ through a memoryless binary symmetric channel with crossover probability $p$ : each coordinate is flipped independently with probability $p$ , producing $Y \in \{0,1\}^n$ . An observer sees $Y$ and wants to learn about $X$ — but the summary of $X$ they are allowed to keep is a single bit $f(X)$ , computed by a Boolean function $f$ chosen in advance. Which choice of $f$ makes that one bit most informative about the noisy observation, in Shannon's sense?

The natural candidate is a dictator, $f(x) = x_i$ : keep one coordinate and forget the rest. It achieves $I(f(X); Y) = I(X_i; Y_i) = 1 - H(p)$ , where $H$ is the binary entropy function in bits. Majority, parity, and every other symmetric or balanced construction does worse. Courtade and Kumar conjectured in 2014 that nothing does better: no Boolean function of $n$ noisy-channel inputs, however many coordinates it reads and however it combines them, beats a single coordinate.

Setting

Fix $n \in \mathbb{N}$ , a crossover probability $p \in [0,1]$ , and a Boolean function $f : \{0,1\}^n \to \{0,1\}$ . With $X$ uniform on the cube and $Y$ its image under the channel, all the relevant quantities are finite sums: the joint mass of $(f(X), Y)$ is

\Pr[f(X) = b,\, Y = y] \;=\; 2^{-n}\sum_{x \in \{0,1\}^n} \mathbf{1}[f(x) = b] \prod_{i=1}^{n} \bigl( (1-p)^{\mathbf{1}[x_i = y_i]} p^{\mathbf{1}[x_i \neq y_i]} \bigr),

and mutual information is $I(f(X); Y) = H(f(X)) + H(Y) - H(f(X), Y)$ , all entropies in bits. No measure theory is required, and the endpoints $p \in \{0, 1/2, 1\}$ are included by the conventions $0 \log 0 = 0$ and $\log 0 = 0$ .

Formalization targets

Goal — the general inequality

\forall\, n \in \mathbb{N},\ \forall f : \{0,1\}^n \to \{0,1\},\ \forall p \in [0,1]: \qquad I\bigl(f(X); Y\bigr) \;\le\; 1 - H(p).

The goal quantifies over every dimension, including $n = 0$ , every Boolean function — balanced or not, monotone or not — and every crossover probability including the three endpoints. Nothing is assumed about $f$ : no balance condition, no bound on the number of influential coordinates, no restriction to a range of $p$ . The bound is tight, attained by any dictator, so the statement is exactly the assertion that dictators are the most informative Boolean functions.

Why the bound matters

The inequality is the sharp, one-bit case of a general question in information theory: how much can a lossy summary of a source tell you about a noisy observation of that source? It is the Boolean-function analogue of a hypercontractivity or "small-set expansion" statement — quantities of the form $I(f(X); Y)$ under a noise operator are precisely what appear in the analysis of Boolean functions, in hardness-of-approximation reductions built on noise stability, and in distributed source-coding and common-information problems, where the bound limits what a single bit of a compressed description can carry. Special cases were known and repeatedly used: balanced functions, functions of few coordinates, and asymptotic or high-noise regimes. The general statement resisted those methods, because the extremal structure is a single coordinate while the space of competitors grows doubly exponentially in $n$ .

Why it is hard

Mutual information is neither convex nor concave in $f$ , and the obvious relaxations are false: the corresponding bound for real-valued or non-Boolean summaries fails, so any argument must use Booleanness. Fourier-analytic approaches control noise stability but lose the constant needed for tightness, and the tightness is the whole content — the inequality is an equality for dictators, leaving no slack to absorb approximation. Induction on $n$ requires a statement strong enough to survive restriction, and the known strengthenings become false at the endpoints. The regimes also split: near $p = 1/2$ the problem becomes a perturbative curvature computation around the dictator, while for moderate $p$ the extremal analysis is a global optimization over a two-parameter family, and the two arguments meet only if their boundaries are matched exactly.

Formalization scope

The goal is stated with the entropy and mutual-information definitions of this mission's definition module: binary entropy via Mathlib's Real.binEntropy divided by $\log 2$ (so entropies are in bits), the channel as an explicit product kernel, and the joint and marginal masses as explicit finite sums over the cube. The proposition is a single closed statement — no hypotheses beyond $0 \le p \le 1$ — so a solution must establish it for all dimensions uniformly.

A complete machine-checked proof of this statement exists in Lean 4 (Chen–Gohari–Javanmard–Lin–Mirrokni–Nair–Woodruff, 2026): axioms $\{$ propext, Classical.choice, Quot.sound $\}$ , no sorry and no native_decide, but 45,500 modules and roughly 50 million lines, most of it kernel-checked numerical certificate data. It is therefore not submittable as a single solution, and the mission's supporting structure — the manuscript route's regional statements and its leaf certificate families — will be added as separate theorems as they are transplanted onto the platform.

Selected references

T. A. Courtade, G. R. Kumar. Which Boolean functions maximize mutual information on noisy inputs? IEEE Transactions on Information Theory 60(8):4515–4525, 2014. (The conjecture.)
Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair, D. P. Woodruff. A Proof of the Most Informative Boolean Function Conjecture. arXiv:2609.24931, 2026.
Lean 4 formalization of the above: https://github.com/dpwoodru/general-courtade-kumar-lean
R. O'Donnell. Analysis of Boolean Functions. Cambridge University Press, 2014, Chapters 2 and 9 (noise operators, hypercontractivity).

7 thms1 active userReviewed

Completed

Combinatorics Optimization·Captain: moutei

Primal-Dual Online Algorithms III: Set-Cover Approximation via CertificatesTextbook

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$ . The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$ , giving an $f$ -approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$ , and a nonnegative cost $c : S \to \mathbb{R}$ . Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

(P)\quad \min \sum_{s} c_s x_s \ \text{ s.t. } \sum_{s : e \in A_s} x_s \ \ge\ 1 \ \ (\forall e \in E), \quad x \ge 0,

(D)\quad \max \sum_{e} y_e \ \text{ s.t. } \sum_{e \in A_s} y_e \ \le\ c_s \ \ (\forall s \in S), \quad y \ge 0.

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$ -approximation bound reads $\mathrm{cost}(C) \le 0$ , which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$ , $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$ .

Goal — the primal-dual $f$ -approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$ ,

\sum_{s \in C} c_s \ \le\ f \cdot \sum_{s \in S} c_s x_s .

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

\sum_{s \in C} c_s \ \le\ f \cdot \sum_{e \in E} y_e .

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$ . For such a certificate and any fractional cover $x$ ,

\sum_{s \in C} c_s \ \le\ \rho \cdot \sum_{s} c_s x_s .

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$ ; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$ -approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

10 thms1 active userReviewed

Theoretical Computer Science

Missions