All missions

Motivation

A seller who offers several goods to a buyer with private values has to choose a selling mechanism. For one good the optimal mechanism is known: post the best take-it-or-leave-it price (Myerson 1981). For two or more goods the optimal mechanism can be complicated: it may use lotteries, its menu may be infinite, and it may not be computable in closed form even for simple value distributions. Sellers therefore use simple mechanisms, such as selling each good separately or selling all goods as one bundle, and the question is how much revenue this costs.

Hart and Nisan (arXiv:1204.1846v3, J. Econ. Theory 2017) answer this with guaranteed fractions of the optimal revenue. Their basic tool is a decomposition theorem: when the goods split into two groups whose values are independent, the optimal revenue from all goods together is bounded by revenues computed from each group separately. This mission formalizes that theorem (Theorem 7) and the paper's first headline result, Theorem A, which is its two-good case.

Setting

There are $k \ge 1$ goods and one buyer with additive values. A valuation is a vector $x \in \mathbb{R}^k_+$, and a $k$-good random valuation $X$ is a random vector in $\mathbb{R}^k_+$ whose law the seller knows.

A mechanism $\mu = (q, s)$ consists of an allocation $q : \mathbb{R}^k_+ \to [0,1]^k$, where $q_i(x)$ is the probability that the buyer receives good $i$ when reporting $x$, and a payment $s : \mathbb{R}^k_+ \to \mathbb{R}$. The buyer's payoff from truthful reporting is $b(x) = q(x)\cdot x - s(x)$. The mechanism is

• incentive compatible (IC) if $b(x) \ge q(\tilde x)\cdot x - s(\tilde x)$ for all $x, \tilde x \in \mathbb{R}^k_+$;
• individually rational (IR) if $b(x) \ge 0$ for all $x$;
• no positive transfer (NPT) if $s(x) \ge 0$ for all $x$.

Let $\mathcal M$ be the class of IC and IR mechanisms. The expected revenue of $\mu \in \mathcal M$ is $R(\mu; X) = \mathbb{E}[s(X)]$, which lies in $(-\infty, +\infty]$, and the optimal revenue is

Two benchmarks reduce to one-good problems: the separate revenue $\mathrm{SRev}(X) = \mathrm{Rev}(X_1) + \dots + \mathrm{Rev}(X_k)$ and the bundled revenue $\mathrm{BRev}(X) = \mathrm{Rev}(X_1 + \dots + X_k)$. Finally $\mathrm{Val}(X) = \mathbb{E}[\sum_i X_i]$ is the expected total value.

For the decomposition, $Y$ is a random valuation for $k_1 \ge 1$ goods and $Z$ one for $k_2 \ge 1$ goods. The coordinates of $Y$ may be arbitrarily dependent, and so may those of $Z$, but the vectors $Y$ and $Z$ are independent. $\mathrm{Rev}(Y, Z)$ is the optimal revenue from selling all $k_1 + k_2$ goods together, and $X\mathbf 1_{X \in A}$ is the random valuation equal to $X$ on the event $X \in A$ and to $0$ otherwise.

Formalization targets

Goal: Theorem 7 (p. 18)

If $Y$ and $Z$ are independent, then

Both inequalities are part of the goal, with the same middle term.

Milestones, in the order of the paper's proof

1. Proposition 6 (iii), p. 14: $\mathrm{Rev}(X)$ is the supremum of $R(\mu; X)$ over IC, IR and NPT mechanisms.
2. The NPT split, p. 20: $\mathrm{Rev}(Y,Z) \le \mathrm{Rev}\big((Y,Z)\mathbf 1_{\sum_i Y_i \ge \sum_j Z_j}\big) + \mathrm{Rev}\big((Y,Z)\mathbf 1_{\sum_j Z_j \ge \sum_i Y_i}\big)$.
3. Proposition 6 (iv), p. 14: for $\mu \in \mathcal M$ and a set $A$ of values, $\mathbb{E}[s(X)\mathbf 1_{X\in A}] \le \mathrm{Rev}(X\mathbf 1_{X\in A}) \le \mathrm{Rev}(X)$.
4. Lemma 8, p. 19: $\mathrm{Rev}\big((Y,Z)\mathbf 1_{(Y,Z)\in A}\big) \le \mathrm{Rev}(Y) + \mathrm{Val}\big(Z\mathbf 1_{(Y,Z)\in A}\big)$.
5. Lemma 9, p. 20: for one-dimensional independent $Y, Z$, $\mathrm{Val}(Z\mathbf 1_{Y \ge Z}) \le \mathrm{Rev}(Y)$.
6. Lemma 10, p. 20: $\mathrm{Val}\big(Z\mathbf 1_{\sum_i Y_i \ge \sum_j Z_j}\big) \le \mathrm{BRev}(Y)$.
7. BRev ≤ Rev, p. 18.

Companions

Theorem A in the form (2), p. 16: for two independent goods $Y, Z$, $\mathrm{Rev}(Y, Z) \le 2(\mathrm{Rev}(Y) + \mathrm{Rev}(Z))$. Also posed is display (5), p. 17: $z\cdot\mathbb{P}[Y \ge z] \le \mathrm{Rev}(Y)$ for one good and every $z \ge 0$.

Significance

Theorem A says that for two independent goods, selling them separately guarantees half of the optimal revenue, whatever the distributions. Theorem 7 extends this to two independent groups of goods. It is the induction step behind the paper's bounds for many goods: separate selling guarantees a fraction $c/\log^2 k$ of the optimal revenue for $k$ independent goods (Theorem C), and bundling guarantees $c/\log k$ for $k$ i.i.d. goods (Theorem D). These are other missions of this series, and both use Theorem 7 as a black box. The same approach underlies later work on simple versus optimal mechanisms, for example Babaioff, Immorlica, Lucier and Weinberg (FOCS 2014) and Li and Yao (PNAS 2013).

All results posed here are proved in the paper. As far as we know, none has a machine-checked proof. A formal proof would give a reusable development of mechanism design with multi-dimensional types: IC and IR mechanisms on $\mathbb{R}^k_+$, revenue as an extended-real expectation, restriction of mechanisms to subdomains, and marginal mechanisms obtained by fixing some coordinates of an independent product.

Difficulty

The proofs are short on paper but rest on measure theory the prose passes over. Lemma 8 conditions on $Z = z$ and applies Proposition 6 (iv) to a one-group mechanism for each fixed $z$. Formally this is a Tonelli argument on a product measure, with an integrand that may be negative on part of the space and $+\infty$ in expectation. The induced mechanism $s^z(y) = s(y, z) - \sum_j q_j(y,z) z_j$ involves the allocation $q$, which is not assumed measurable. Proposition 6 (iv) bounds a mechanism with possibly negative payments by the optimal revenue on a modified valuation $X\mathbf 1_{X \in A}$, and this requires shifting the mechanism to make it NPT. Finally, every revenue may be infinite, so the inequalities must be handled in $[0,\infty]$ and in the extended reals, without cancelling.

A natural first idea is to apply Theorem A coordinate by coordinate. This fails, because the coordinates inside $Y$ may be dependent. Only the independence of $Y$ from $Z$ is available, and the bound must go through the bundled revenue $\mathrm{BRev}$.

Formalization scope

• Valuations as laws. A random valuation is represented by its law, a probability measure on ι → ℝ≥0 for a finite type ι of goods. Every quantity of the paper depends only on the law. One good is ι = Unit.
• Independence as a product law. The law of $(Y,Z)$ is the product of the laws of $Y$ and $Z$, transported to ι₁ ⊕ ι₂ → ℝ≥0. Theorems that need independence are never stated over an arbitrary joint law with given marginals, since they are false for correlated groups. The NPT split in the proof of Theorem 7 is stated for independent groups, as on the page. Proposition 6 applies to an arbitrary law.
• The class $\mathcal M$. $\mathcal M$ requires $q \in [0,1]^k$, IC, IR and a measurable payment $s$, the last as allowed by the paper's footnote 12. $q$ is not required to be measurable.
• Revenue. $R(\mu;X)$ is $\int s^+ - \int s^-$ in the extended reals, so that $\mathbb{E}[s(X)] = +\infty$ is kept. Since $s \ge s(0)$ under IC, the negative part is finite. The Bochner integral is not used, because it would assign $0$ to a non-integrable payment. $\mathrm{Rev}$, $\mathrm{SRev}$, $\mathrm{BRev}$ and $\mathrm{Val}$ take values in $[0,\infty]$.
• Subdomains. $X\mathbf 1_{X\in A}$ is the image law under $x \mapsto x\mathbf 1_A(x)$, and $A$ is assumed measurable. The regions of the proof of Theorem 7 are both closed, so the diagonal is counted twice, as in the paper.
• Not trivializable. A formalization in which $\mathrm{Rev}$ is computed with a Bochner integral, the expected revenue is clipped before comparing a single mechanism with $\mathrm{Rev}$, or independence is dropped does not state the paper's theorem, and none of these is used.
• Not posed. The ratio form of Theorem A ($\mathrm{GFOR} \ge 1/2$) is not posed, because of its conventions $0/0 = 1$ and $\infty/\infty$. Theorems B, C, D, 16 and 33 are separate missions of this series.

Contributions are welcome at every level: Proposition 6 (the NPT shift and subdomain restriction), the marginal-mechanism construction behind Lemma 8, and the one-good facts (5) and Lemma 9 are all reusable in the sibling missions on Theorems C and D.

Selected references

• S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory 172 (2017); preprint arXiv:1204.1846v3, 2017. https://arxiv.org/abs/1204.1846
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6 (1981) 58–73. https://doi.org/10.1287/moor.6.1.58
• S. Hart and P. J. Reny, Maximal Revenue with Multiple Goods: Nonmonotonicity and Other Observations, Theoretical Economics 10 (2015) 893–922. https://doi.org/10.3982/TE1517
• M. Babaioff, N. Immorlica, B. Lucier and S. M. Weinberg, A Simple and Approximately Optimal Mechanism for an Additive Buyer, FOCS 2014. https://arxiv.org/abs/1405.6146
• X. Li and A. C.-C. Yao, On Revenue Maximization for Selling Multiple Independently Distributed Items, PNAS 110 (2013) 11232–11237. https://doi.org/10.1073/pnas.1309533110

Why online matching needs a stronger rounding guarantee

In online selection, candidate items reveal themselves one at a time and an algorithm must decide immediately whether to keep each one. When the kept items must form a matching, accepting one edge can prevent a later edge sharing an endpoint from being accepted. A fractional solution supplies useful marginal probabilities, but it does not by itself specify which active edges can be kept under an unfavorable arrival order. Online contention resolution schemes provide that missing rounding step: they turn independent edge activity into a feasible online selection while guaranteeing each edge a chance of selection. Feldman, Svensson, and Zenklusen introduced the strong selectability guarantee used here, which protects an edge even against an arrival order chosen with knowledge of all random outcomes (Feldman–Svensson–Zenklusen, §1.1).

This mission isolates the matching result of their paper. It concerns a degree relaxation that is weaker than the full matching polytope, so the result applies even when the input fractional point satisfies only local vertex constraints. The source states the existence theorem as Theorem 2.7 and gives its numerical guarantee explicitly (Theorem 2.7, p. 13).

Finite graphs, fractional edges, and greedy families

Let $G=(V,E)$ be a finite graph. An edge $g$ has two distinct endpoints; multiple edges may have the same endpoints. A matching is a set of edges with no shared vertex. For a vertex $u$, write $\delta(u)$ for its incident edges. The degree relaxation is

Since each edge meets a vertex, these constraints also give $x_g\le1$. Every matching has a characteristic vector in $P_G$. The degree relaxation can contain points outside the convex hull of matchings, which makes the theorem stronger than a statement restricted to the matching polytope (§2.2, p. 13).

For $x\in[0,1]^E$, the active set $R(x)$ includes each edge $g$ independently with probability $x_g$. A greedy family $\mathcal F_x$ is a downward closed family of matchings containing the empty set. A greedy online scheme accepts an active edge if adding it to the already accepted set remains in $\mathcal F_x$. The family may itself be random, sampled independently of $R(x)$.

An edge $g$ is selectable for a realized active set and greedy family when every member $I\in\mathcal F_x$ with $I\subseteq R(x)$ can be extended by $g$ while staying in $\mathcal F_x$. Thus selectability promises acceptance regardless of which eligible active edges preceded $g$. A scheme is $(b,c)$-selectable if this event has probability at least $c$ for every $x\in bP_G$ and every edge. The probability includes both the active-set draw and any random family draw (Definitions 1.3–1.5, pp. 3–4).

Formalization targets

Theorem 2.7: a randomized matching scheme

For every $b\in[0,1]$ and every finite loopless graph $G$,

Equivalently, for each $x\in bP_G$ and each edge $g\in E$, the probability that $g$ is selectable is at least $e^{-2b}$. The statement includes edges with $x_g=0$; the selectability event concerns the ability to add an edge, rather than the probability that it becomes active. The milestones are the steps the source states in its proof, in attack order (proof of Theorem 2.7, pp. 13–14):

1. for $t>0$, $0\le(1-e^{-t})/t\le1$, so that an edge can be put into a random set $K$ of potential edges with probability $(1-e^{-x_g})/x_g$;
2. drawing $K$ this way and using the matchings inside $K$ as the family is a randomized greedy scheme;
3. an edge $g'$ with ends $u,v$ is selectable exactly when $g'\in K$ and $A\cap K\cap(\delta(u)\cup\delta(v)\setminus\{g'\})=\varnothing$;
4. the probability of that event equals $\frac{1-e^{-x_{g'}}}{x_{g'}}\,e^{-\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g}$;
5. for $x\in bP_G$, $\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g\le2(b-x_{g'})$;
6. for $t>0$, $e^{t}(e^{t}-1)/t\ge1$.

Remark (p. 14): the deterministic variant

Taking $K=E$, the deterministic greedy scheme whose family is the set of all matchings is $(b,(1-b)^2)$-selectable for $P_G$, $b\in[0,1]$:

This companion is weaker than Theorem 2.7 for every $b\in(0,1]$ and is not used by it (Remark, p. 14).

What the result contributes

The theorem gives a constant probability bound against the paper's strongest, “almighty” arrival-order adversary. The guarantee is available from vertex degree inequalities alone. Consequently it applies to points of the exact matching polytope as well, without asking the online rounding procedure to exploit its additional odd-set inequalities. The paper places this result beside analogous existence claims for matroids and knapsacks in Theorem 1.8, and uses greedy schemes as components in more general selection results (Theorem 1.8, p. 4).

The existence theorem is proved in the source; it is an open formalization target here. A completed Lean development would supply a reusable finite model of independent active sets, random greedy families, edge selectability, and matching degree relaxations. It would also put the exact $e^{-2b}$ constant and its endpoint cases under machine checking. The definitions can support future formalizations of the paper's combination and application results, although this mission claims only Theorem 2.7 and its local proof milestones.

Where the argument is delicate

The local degree constraints bound the fractional weight at each endpoint separately, while selectability must survive conflicts at either endpoint under any arrival order. Merely ensuring that the algorithm outputs a matching gives no lower bound for a particular edge: the adversary can expose competing active edges first. The theorem therefore asks for a stronger event that certifies an edge could be added after every eligible previously selected matching. The numerical guarantee must hold uniformly over all edges, even when a coordinate is zero (Definitions 1.4–1.5, pp. 3–4; proof of Theorem 2.7, p. 13).

Formalization scope

The ground set is the finite edge type $E$. The published EdmondsMatching65.Polyhedron.Graph structure represents a graph by a map from edges to unordered pairs of vertices and includes a proof excluding self-loops; its matching predicate is reused directly. This admits parallel edges, a harmless generalization of the page's graph language. Incident edge sets and matchings are finite sets. The polytope is the set of real edge vectors satisfying precisely the nonnegativity and vertex degree inequalities above. Scaling is the pointwise set operation $bP_G$, so $b=0$ remains meaningful. The parameter range $0\le b\le1$ is explicit.

Probability is represented by finite sums of product weights. A randomized scheme is a weight function on finite greedy families, independent of the active-set draw. Each family contains the empty set and lies inside the matchings; allowing an empty family would make selectability vacuous. The degree inequalities keep relevant coordinates in $[0,1]$, so active-set weights are genuine probabilities. The source's ratio $(1-e^{-x_g})/x_g$ is given its continuous value $1$ at $x_g=0$. For inputs outside the nonnegative domain, which the theorem never uses, that inclusion probability is also assigned $1$ to keep the distribution well formed. These choices and the loopless graph convention are recorded with the draft statements.

The formalization needs finite product probability identities, elementary exponential inequalities, and set facts about matchings and incident edges. Contributions proving the six listed milestones, the deterministic Remark, or the full existential theorem are welcome. The finite model of active sets, greedy families and selectability is shared with the other missions of this series (matroids, knapsack, combinations of schemes, submodular rounding).

Selected references

• Moran Feldman, Ola Svensson, and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015, preprint. Published as Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing, 2021.

Motivation

Many online selection problems ask an algorithm to accept or reject items one at a time, irrevocably, while keeping the accepted set feasible: independent in a matroid, a matching in a graph, or within a knapsack budget. In Bayesian versions, such as prophet inequalities and posted-price mechanisms, a fractional point $x$ of a relaxation of the feasible sets is available in advance, and each item is active independently with probability $x_e$. An online contention resolution scheme (OCRS), introduced by Feldman, Svensson and Zenklusen, turns this random active set into a feasible selection as items arrive.

The quality of an OCRS is measured by its selectability: the probability that every element is accepted when it is active, whatever the arrival order. Applications, however, care about the value of the selected set, often a submodular function such as a coverage or a utility with diminishing returns. Theorem 1.10 of the paper is the bridge between the two: a selectability guarantee $c$ yields an approximation guarantee $c$ for every monotone submodular objective, and $c/4$ for non-monotone ones, even against an adversary who sees every random outcome before fixing the order. The other four missions of this series construct selectable OCRSs for matroids, matchings and knapsacks and combine them; this mission formalizes what such a guarantee is worth.

The offline counterpart is the theory of contention resolution schemes (CRSs) of Chekuri, Vondrák and Zenklusen (SIAM J. Comput. 2014), whose Theorem 1.3 shows that a monotone balanced CRS rounds the multilinear extension of a submodular function with the balancedness factor. The proof of Theorem 1.10 reduces the online statement to that offline result.

Setting

Let $N$ be a finite ground set and $\mathcal F\subseteq 2^N$ a down-closed family of feasible sets. A polytope $P\subseteq[0,1]^N$ is a relaxation of $\mathcal F$ if it contains exactly the characteristic vectors $\mathbf 1_I$ with $I\in\mathcal F$ among the $\{0,1\}$-points. For $x\in[0,1]^N$, the random set $R(x)$ contains every $e$ independently with probability $x_e$.

A greedy OCRS fixes, for each input $x$, a down-closed family $\mathcal F_x\subseteq\mathcal F$ containing $\emptyset$ (deterministically, or drawn from a distribution independent of $R(x)$). The elements then arrive one by one; an arriving active element is selected if, together with the elements already selected, it forms a set in $\mathcal F_x$. An element $e$ is selectable for the active set $A$ if $I\cup\{e\}\in\mathcal F_x$ for every $I\subseteq A$ with $I\in\mathcal F_x$. For $b,c\in[0,1]$ the OCRS is $(b,c)$-selectable if for every $x\in bP$ and every $e\in N$

The arrival order is chosen by the almighty adversary, which knows $R(x)$, the realized family $\mathcal F_x$ and every random bit of the algorithm before choosing it.

For $f:2^N\to\mathbb R$, the multilinear extension is $F(x)=\mathbb E[f(R(x))]$. The function $f$ is submodular if $f(A\cup B)+f(A\cap B)\le f(A)+f(B)$ for all $A,B$, and monotone if $A\subseteq B$ implies $f(A)\le f(B)$. For a set $S$, $S(1/2)$ keeps every element of $S$ independently with probability $1/2$.

An (offline) CRS $\pi$ for $P$ maps each $S\subseteq N$, possibly at random, to a subset $\pi(S)\subseteq S$ with $\mathbf 1_{\pi(S)}\in P$. It is $(b,c)$-balanced if $\Pr[e\in\pi(R(x))\mid e\in R(x)]\ge c$ for $x\in bP$ and $x_e>0$, and monotone if $\Pr[e\in\pi(S_1)]\ge\Pr[e\in\pi(S_2)]$ whenever $e\in S_1\subseteq S_2$. The characteristic CRS of a greedy OCRS is $\bar\pi(A)=\{e\in A : e \text{ selectable for } A\}$.

Formalization targets

Goal: Theorem 1.10

Let $P$ be a relaxation of $\mathcal F$, let $\pi$ be a $(b,c)$-selectable greedy OCRS for $P$, let $x\in bP$, and let $f\ge0$ be submodular. Against every almighty adversary, the selected set $S$ satisfies

where in the second case the coins defining $S(1/2)$ are known to the adversary. The constants are the paper's and are not parameters to be improved here.

Milestones

1. Observation 3.3: for every greedy family, active set and order, $\bar\pi(A)$ is contained in the selected set.
2. The remark after Definition 3.2: $\bar\pi$ is a CRS for $P$.
3. Lemma 3.4: the characteristic CRS of a $(b,c)$-selectable greedy OCRS is $(b,c)$-balanced and monotone.
4. Lemma 3.5 (from Chekuri–Vondrák–Zenklusen): for every non-negative submodular $f$ there is a pruning map $\eta_f$, with $\eta_f(S)\subseteq S$, such that $\mathbb E[f(\eta_f(\pi(R(x))))]\ge c\cdot F(x)$ for every monotone $(b,c)$-balanced CRS $\pi$ and every $x\in bP$.
5. Lemma 3.6 (Feige–Mirrokni–Vondrák, Lemma 2.2): if $T_p\subseteq T$ contains every element of $T$ with probability $p$, not necessarily independently, then $\mathbb E[g(T_p)]\ge(1-p)g(\emptyset)+p\,g(T)$ for submodular $g$.
6. Lemma 3.7 (Buchbinder–Feldman–Naor–Schwartz, Lemma 2.2): if $N_p$ contains every element with probability at most $p$, then $\mathbb E[g(N_p)]\ge(1-p)g(\emptyset)$ for non-negative submodular $g$.

Significance

Theorem 1.10 is what makes selectability useful. Combined with the paper's OCRSs for matroids, matchings and knapsacks (Theorem 1.8) and the combination rule (Theorem 1.9), it gives constant-factor online algorithms for submodular objectives under intersections of these constraints, and through them the paper's applications to prophet inequalities, posted-price mechanisms and stochastic probing. The guarantee holds against the strongest adversary considered, so it applies whatever arrival order the application imposes.

The theorem and its proof are published; none of the statements of this mission has a machine-checked proof. Formalizing it produces a reusable interface between online and offline contention resolution, and machine-checked versions of two standard lemmas on correlated random subsets of submodular functions (Lemmas 3.6 and 3.7) used throughout submodular maximization. Lemma 3.5 is the substantial imported ingredient: its formal proof amounts to formalizing the rounding theorem of Chekuri, Vondrák and Zenklusen for non-monotone objectives.

Difficulty

The first idea is to compare the online selection directly with $F(x)$ element by element: each element is selected with probability at least $c\,x_e$. For a linear objective this suffices. For a submodular objective it does not, because the marginal value of an element depends on which other elements are selected, and the adversary controls this through the order. The reduction to the characteristic CRS removes the order, but the offline rounding result (Lemma 3.5) then needs the full CRS machinery, including a pruning step that depends on $f$ alone.

For non-monotone $f$, selecting extra elements can lose value, and the adversary decides which elements beyond $\bar\pi(A)$ are selected, after seeing the coins. Controlling this requires the correlated-sampling bounds of Lemmas 3.6 and 3.7 rather than independence.

Formalization scope

The ground set is a finite type α : Type with decidable equality; sets are Finset α; vectors are α → ℝ. All probabilities and expectations are exact finite sums of product weights, without measure theory. $bP$ is the pointwise scaling b • P, which handles $b=0$. The multilinear extension and submodularity are the published definitions NonmonotoneSubmod.Shared.F and NonmonotoneSubmod.Shared.Submodular.

A randomized greedy OCRS is a weight function on families Finset (Finset α), a CRS a weight function on maps Finset α → Finset α; a deterministic OCRS is a point mass. The almighty adversary is any function from the realized family and active set (and, in part 2, the coin set $C$, with $S(1/2)=S\cap C$ and $C$ uniform and independent of everything else) to an order listing every element once. The standing assumptions of Definition 1.3 are explicit hypotheses: $\mathcal F$ down-closed, $P$ a polytope contained in $[0,1]^N$ and a relaxation of $\mathcal F$, and $b,c\in[0,1]$. A polytope is encoded as the convex hull of finitely many vectors. Every greedy family contains $\emptyset$, so the empty family cannot make every element vacuously selectable, and the inputs $x\in bP$ lie in $[0,1]^N$, so the product weights are probabilities.

Definition 3.1 is printed with "$\ge c\cdot x_e$"; the formalization uses "$\ge c$", as the proof of Lemma 3.4 and Definition 4.5 do. Lemma 3.5 keeps the paper's quantifier order: $\eta_f$ is fixed before $P$, $b$, $c$, $\pi$ and $x$.

Welcome contributions: proofs of the milestones in any order; Lemmas 3.6 and 3.7 are self-contained and reusable; Lemma 3.5 may be split further along the proof of Chekuri–Vondrák–Zenklusen.

Selected references

• M. Feldman, O. Svensson, R. Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015; Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM J. Comput. 50(2), 2021. https://arxiv.org/abs/1508.00142v2
• C. Chekuri, J. Vondrák, R. Zenklusen, Submodular Function Maximization via the Multilinear Relaxation and Contention Resolution Schemes, SIAM J. Comput. 43(6), 2014. https://doi.org/10.1137/110839655
• U. Feige, V. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, Submodular Maximization with Cardinality Constraints, SODA 2014. https://doi.org/10.1137/1.9781611973402.106

Motivation

In online selection, useful items arrive one at a time and must be accepted or rejected before the next arrival. A knapsack constraint limits the total size of accepted items to one unit. When the order may depend on all of the random outcomes, an algorithm needs a guarantee that survives every such order. Feldman, Svensson, and Zenklusen introduced online contention resolution schemes (OCRSs) to provide this guarantee for fractional relaxations of selection problems. Their knapsack theorem gives an explicit guarantee for a randomized greedy scheme and contrasts with a size-dependent obstruction for deterministic greedy schemes (Feldman–Svensson–Zenklusen, §2.3).

The knapsack result is one of the three concrete existence results summarized in Theorem 1.8 of the paper. The surrounding framework is designed to convert fractional solutions into feasible online selections under an almighty adversary, who knows the active items and the scheme's random choices before choosing their arrival order. This makes the selectability requirement stronger than a performance claim for one fixed order (Feldman–Svensson–Zenklusen, Definitions 1.3–1.5).

Setting

Let $N$ be a finite ground set. Each element $e\in N$ has a size $s_e\in[0,1]$. A subset $I\subseteq N$ is feasible when its total size is at most one. The natural fractional polytope is

For a vector $x\in[0,1]^N$, the random active set $R(x)$ includes each element $e$ independently with probability $x_e$. A greedy family $F_x$ is a downward-closed family of feasible subsets. The online rule accepts an active arriving element when adding it to the accepted set keeps that set inside $F_x$. A randomized greedy OCRS chooses the family at random, independently of $R(x)$. The paper studies the probability that an element $e$ is selectable: for every possible accepted set $I\subseteq R(x)$ with $I\in F_x$, the enlarged set $I\cup\{e\}$ still belongs to $F_x$. Such an event makes $e$ acceptable regardless of the arrival order (Feldman–Svensson–Zenklusen, §1.1).

Write $bP=\{bp:p\in P\}$. An OCRS is $(b,c)$-selectable when, for every $x\in bP$ and every $e\in N$, the probability that $e$ is selectable is at least $c$. The paper divides elements at size $1/2$: $N_{\mathrm{big}}=\{e:s_e>1/2\}$, while equality belongs to the small elements. Its construction randomly chooses between the feasible subsets using only big elements and those using only small elements (Feldman–Svensson–Zenklusen, proof of Theorem 2.9).

Formalization targets

Main theorem

Theorem 2.9 asserts that for every $b\in[0,1/2]$ and every such knapsack polytope, a randomized greedy OCRS exists with

The goal quantifies over every finite ground set and every allowed size vector. At the endpoint $b=1/2$, the claimed lower bound is zero; at $b=0$, it is $1/2$. The denominator remains positive throughout the stated interval. The goal is an existence statement; its witnesses are arbitrary randomized greedy families meeting the definition, so the paper's particular construction is named separately in the supporting definitions (Feldman–Svensson–Zenklusen, Theorem 2.9, p. 14).

Supporting targets

The milestones include the paper's bound $0\le b_{\mathrm{big}}\le b$ for $b_{\mathrm{big}}=\sum_{e\in N_{\mathrm{big}}}s_ex_e$, the big and small element selectability bounds for the paper's construction, and Proposition 2.8. That proposition says that, for every ground-set size $n\ge1$, some knapsack constraint defeats every deterministic greedy OCRS whenever $c>(1-b)^{n-1}$ for $b\in[0,1]$ (Feldman–Svensson–Zenklusen, §2.3, pp. 14–15).

Significance

The theorem supplies a concrete selectable OCRS for the natural fractional knapsack relaxation. Its guarantee applies to every element and every fractional point in $bP$, under the paper's strongest arrival-order adversary. Proposition 2.8 explains why randomization matters here: a deterministic greedy scheme cannot retain an analogous positive constant independent of the number of elements on every knapsack instance. These results serve as the knapsack component in the paper's broader OCRS framework and can be combined with schemes for other constraints in the paper's later combination result (Feldman–Svensson–Zenklusen, Theorem 1.9).

The mathematical theorem and proposition have proofs in the cited paper. This mission asks for machine-checked proofs of their formal statements and of the stated intermediate bounds. The current draft declarations contain proof placeholders; compilation establishes only that their statements and definitions are well formed. A completed development would also leave reusable finite active-set probabilities, greedy-family predicates, and explicit knapsack constructions for later online-rounding work.

Difficulty

A family that contains every feasible subset is not automatically useful for online selection: one active set may contain several subsets whose accepted elements block the tested element. The requirement quantifies over every feasible accepted subset of the realized active set, reflecting the almighty adversary rather than a fixed order. In a knapsack, elements larger than one half behave differently from smaller ones, and a single deterministic family cannot give a ground-set-independent selectability guarantee on all instances. The randomized construction must assign valid probabilities to its two families and obtain the same lower bound in both size regimes (Feldman–Svensson–Zenklusen, Proposition 2.8 and Theorem 2.9).

Formalization scope

The Lean ground set is a finite type, and subsets are Finsets. The polytope is the set of real vectors satisfying both the box inequalities and the unit-capacity inequality. The feasible family uses the same sizes and unit capacity. Active-set and family-choice probabilities are finite sums, with independent Bernoulli factors for $R(x)$. The scaling $bP$ is pointwise set scalar multiplication, so the case $b=0$ retains its intended meaning. The size assumptions $s_e\in[0,1]$ and the ranges of $b$ are explicit theorem hypotheses. No nonemptiness assumption is added to the ground set; the statements include the empty case.

The greedy-family definition requires the empty set, making it impossible to satisfy selectability by using an empty family. Every family chosen with positive probability is downward closed and consists of feasible sets. The polytope's box constraints keep every active-set weight a probability. The construction's mixing probability is used exactly on $x\in bP$; on other vectors its totalized value chooses the small family, where the paper makes no performance claim. The two branch weights are added if their families coincide, as they can on an empty ground set.

One display on page 15 includes the tested element in a load sum, while the next displayed equality treats that element as excluded. The pointwise supporting item uses the excluded-element form needed for the stated argument; the printed display is preserved in the milestone quotation and the discrepancy is detailed in MODERATION_NOTES.md. Contributions toward either size regime, the finite probability bounds, or the deterministic obstruction are welcome. The finite probability and greedy-family definitions are the parts most directly reusable beyond knapsack.

Selected references

• Moran Feldman, Ola Svensson, and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015, §1.1 and §2.3, pp. 2–4 and 14–15. arXiv.

Motivation

Social networks exhibit triadic closure: two people with a common friend are more likely to be friends themselves than two people chosen at random, and the more common friends they have, the more likely they are to be connected. The principle goes back to sociology (Granovetter 1973) and is documented on large network data sets (see the Enron e-mail graph in Figure 1 of Fox, Roughgarden, Seshadhri, Wei and Wein).

A common computational task on such networks is to list all maximal cliques, the groups of mutually connected vertices that cannot be enlarged. On an arbitrary graph this is hopeless in the worst case: Moon and Moser showed in 1965 that an $n$-vertex graph can have $3^{n/3}$ maximal cliques, and that no graph has more (Moon and Moser 1965). Yet clique enumeration on real social networks runs quickly. Fox, Roughgarden, Seshadhri, Wei and Wein proposed a distribution-free graph class, defined by a coarse form of triadic closure, on which the worst case is provably polynomial. This mission formalizes their first bound, for the class of weakly $c$-closed graphs (Theorem 2.2 of the paper, also stated as Theorem 1.5), together with the peeling argument that proves it.

Setting

All graphs are finite, simple and undirected. For a graph $G$ with vertex set $V$ and a vertex $v$, $N(v)$ is the set of neighbours of $v$; for $W \subseteq V$, $G[W]$ is the subgraph induced by $W$. The common neighbours of two vertices $u, v$ are the vertices of $N(u) \cap N(v)$.

• $c$-closed graph (Definition 1.1). For a positive integer $c$, $G$ is $c$-closed if every two distinct vertices with at least $c$ common neighbours are adjacent. A 1-closed graph is a disjoint union of cliques; every graph on $n$ vertices is $(n-1)$-closed.
• Bad pair (Definition 1.2). Given $c$, a bad pair of a graph is a pair of distinct, non-adjacent vertices with at least $c$ common neighbours. A graph is $c$-closed exactly when it has no bad pair.
• Weakly $c$-closed graph (Definition 1.3). A graph on $n$ vertices is weakly $c$-closed if its vertices can be ordered $v_1, \dots, v_n$ so that for every $i$, the vertex $v_i$ is in no bad pair of the induced subgraph $G[\{v_i, v_{i+1}, \dots, v_n\}]$. Common neighbours are counted inside that subgraph.
• Maximal clique. A clique is a set of pairwise adjacent vertices. It is maximal if no other vertex can be added to it. Write $\mathrm{mc}(G)$ for the number of maximal cliques of $G$ and $\mathrm{mc}(G[W])$ for that of an induced subgraph. The paper writes $F(n,c)$ for the largest value of $\mathrm{mc}(G)$ over $c$-closed graphs $G$ on $n$ vertices.

Every $c$-closed graph is weakly $c$-closed, but not conversely. The paper's example: a clique on $k$ vertices with one edge $\{u,v\}$ removed is not $c$-closed for any $c < k-2$, but it is weakly 1-closed (order $u$ and $v$ last).

In the Lean development these objects are IsCClosed, IsBadPairIn, IsWeaklyCClosed, maxCliquesIn, numMaxCliquesIn and numMaxCliques, in the namespace CClosedGraphs.Peeling.

Formalization targets

Goal: Theorem 2.2

For all positive integers $c$ and $n$, every weakly $c$-closed graph $G$ on $n$ vertices satisfies

Milestones

The milestones follow the proof of Theorem 2.1 in §2.1 and the remark that extends it to Theorem 2.2. Fix a graph, an induced subgraph $G[W]$ and a vertex $v \in W$. A maximal clique $K$ of $G[W]$ is of type 1 if $v \notin K$, of type 2 if $v \in K$ and $K \setminus \{v\}$ is maximal in $G[W \setminus \{v\}]$, and of type 3 otherwise.

1. Moon–Moser bound (cited as [45], p. 7): $\mathrm{mc}(G[W]) \le 3^{|W|/3}$.
2. Types 1 and 2 (p. 6): there are at most $\mathrm{mc}(G[W \setminus \{v\}])$ of them.
3. Type-3 structure (p. 7, properties A–C): for a type-3 clique $K$ there is $u \in W \setminus (N(v) \cup \{v\})$ such that $K \setminus \{v\}$ is a maximal clique of $G[W \cap N(v) \cap N(u)]$.
4. Inequality (1) (p. 7): the number of type-3 cliques is at most $\sum_{u \in W \setminus (N(v)\cup\{v\})} \mathrm{mc}(G[W \cap N(u) \cap N(v)])$.
5. One-vertex recursion (pp. 7–8): if $v$ is in no bad pair of $G[W]$, then $\mathrm{mc}(G[W]) \le \mathrm{mc}(G[W \setminus \{v\}]) + 3^{(c-1)/3}|W|$.
6. Theorem 2.1 (p. 6): every $c$-closed graph on $n \ge 1$ vertices has $\mathrm{mc}(G) \le 3^{(c-1)/3} n^2$.

Significance

For fixed $c$, the theorem makes the number of maximal cliques of a weakly $c$-closed graph polynomial in $n$, against $3^{n/3}$ for general graphs. Since all maximal cliques can be listed in polynomial time per clique, this makes maximal-clique enumeration fixed-parameter tractable in $c$ on the class. The paper's Theorem 2.3 turns the proof into an enumeration algorithm. Weak $c$-closure is the version that matters in practice: Table 1 of the paper reports social networks with thousands of vertices that are weakly $c$-closed for modest $c$ while being $c$-closed only for much larger $c$. The bound is the starting point of the paper's sharper Theorem 3.1 ($4^{(c+4)(c-1)/2} n^{2-2^{1-c}}$) and its lower bound Theorem 4.1, which are separate missions of this series.

The result is proved in the paper, and the proof is short. No machine-checked proof of it or of the Moon–Moser bound exists in Mathlib at the pinned revision or on Prove2Me. This mission produces both, together with a reusable vocabulary for counting maximal cliques of induced subgraphs. Proofs of the sharp Moon–Moser values, or of the sharper $|W|-1$ in the recursion, are welcome as further contributions but are not milestones.

Difficulty

The counting argument is elementary. The work lies in two places. First, the Moon–Moser bound $3^{k/3}$ is not in Mathlib and needs its own proof, and its exponential bound must be handled with real powers. Second, the type decomposition must be handled exactly: a type-3 clique $K$ is charged to a pair $(u, K \setminus \{v\})$, and the charge has to be injective while $u$ ranges over all vertices outside $N(v) \cup \{v\}$. The degenerate cases are real. When $v$ is isolated in $G[W]$ and $W \ne \{v\}$, the clique $\{v\}$ is of type 3 and $K \setminus \{v\} = \varnothing$. The peeling for weakly $c$-closed graphs must also follow the given vertex ordering, with closure checked in the shrinking induced subgraphs rather than in $G$.

Formalization scope

• Graphs on $n$ vertices are SimpleGraph (Fin n). Auxiliary statements are generic over a finite type with decidable equality.
• The weakly closed ordering is a permutation $\sigma$ of Fin n with $v_i = \sigma(i)$. The set $\{v_i, \dots, v_n\}$ is $\{x : i \le \sigma^{-1}(x)\}$.
• Common-neighbour counts are Set.ncard, which is exact on a finite type. "At least $c$" is $c \le |\cdot|$, not $c < |\cdot|$.
• Maximal cliques of $G[W]$ are counted as finite vertex sets $K \subseteq W$ of the ambient type that are maximal among cliques contained in $W$. Removing $v$ from the current graph $G[W]$ is $G[W \setminus \{v\}]$, and $G[N(v) \cap N(u)]$ is $G[W \cap N(v) \cap N(u)]$.
• All bounds are real numbers: $3^{(c-1)/3}$ and $3^{|W|/3}$ are real powers.
• The hypotheses $c \ge 1$ and $n \ge 1$ are on the page. The second is needed, since the graph with no vertices has one maximal clique, the empty one.
• No hypothesis is added relative to the paper. In property C, "$u \notin N(v)$" is read as $u \notin N(v) \cup \{v\}$, as in Figure 2 and in (1).
• The paper's $F(\cdot, c)$ is a maximum over graphs. The milestones use the actual count of the relevant induced subgraph instead, which is at most $F$; the goals bound the count for every graph in the class, which is the same content.

Three trivializing readings are ruled out. The count is of maximal cliques, not of all cliques or of cliques of a given size. A bad pair needs at least $c$ common neighbours, not more than $c$. In the weakly closed definition, common neighbours are counted inside $\{v_i, \dots, v_n\}$, not in $G$; counting them in $G$ would make the hypothesis stronger and the theorem weaker.

A complete development needs a Moon–Moser lemma for induced subgraphs, the injections behind milestones 2 and 4, and a peeling induction over a vertex ordering. The first two are reusable for any maximal-clique counting argument. The induced-subgraph counts numMaxCliquesIn are also used by the later missions of this series, which repeat the definitions in their own namespaces.

Selected references

• J. Fox, T. Roughgarden, C. Seshadhri, F. Wei, N. Wein, Finding cliques in social networks: a new distribution-free model, arXiv:1804.07431v1, 2018; SIAM Journal on Computing 49(2), 2020. https://arxiv.org/abs/1804.07431v1, https://doi.org/10.1137/18M1210459
• J. W. Moon, L. Moser, On cliques in graphs, Israel Journal of Mathematics 3, 23–28, 1965. https://doi.org/10.1007/BF02760024
• M. S. Granovetter, The strength of weak ties, American Journal of Sociology 78(6), 1360–1380, 1973. https://doi.org/10.1086/225469
• E. Tomita, A. Tanaka, H. Takahashi, The worst-case time complexity for generating all maximal cliques and computational experiments, Theoretical Computer Science 363(1), 28–42, 2006. https://doi.org/10.1016/j.tcs.2006.06.015