Operations Research

Motivation

Max $k$-cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number $k$; the task is to choose $k$ subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.

The greedy algorithm covers at least a $1-1/e\approx 0.632$ fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any $\epsilon > 0$, max $k$-cover cannot be approximated in polynomial time within a ratio of $(1 - 1/e + \epsilon)$, unless $P = NP$." Together with the greedy bound, it makes $1-1/e$ the exact approximation threshold of max $k$-cover.

Timeline:

• 1978: Nemhauser, Wolsey and Fisher prove the greedy $1-1/e$ bound for monotone submodular maximization.
• 1992: Arora, Lund, Motwani, Sudan and Szegedy prove the PCP theorem. With Papadimitriou–Yannakakis (1991) it gives Theorem 2.1.1 of the paper: MAX 3SAT-B has a constant gap unless P = NP.
• 1994: Lund and Yannakakis introduce partition-system reductions from multi-prover proof systems to set cover.
• 1995: Raz proves the parallel repetition theorem (Theorem 2.2.2 of the paper).
• 1998: Feige proves the ln n threshold for set cover (the subject of mission I of this series) and the $1-1/e$ threshold for max $k$-cover.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$, a list of subsets $S_1,\dots,S_s$ of the points, and a number $k$. Its value $\mathrm{opt}$ is the largest number of points covered by at most $k$ of the sets. Instances are written over a three-letter alphabet:

• $n$ in unary;
• each set as its characteristic bit-vector;
• $k$ in unary.

Following p. 648, a polynomial-time algorithm approximates max $k$-cover within a ratio $\delta$ if on every input it outputs a number $v$ with

$$\delta\cdot\mathrm{opt}\le v\le\mathrm{opt}.$$

The algorithm need not name the sets. This is the non-constructive notion of approximation.

The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a $k$-prover proof system for such a formula $\varphi$ with $M$ clauses:

• The verifier picks $\ell$ clauses at random, and a distinguished variable in each; there are $R=(3M)^\ell$ random strings $r$.
• Each prover $P_i$ is attached to a code word of length $\ell$ and weight $\ell/2$; distinct words are at Hamming distance at least $\ell/3$.
• On coordinate $j$, prover $P_i$ receives the clause if its bit is 1, and the distinguished variable if its bit is 0.
• Answers are satisfying assignments of the received clauses and bits for the received variables.
• Two provers are consistent if they assign the same values to the distinguished variables. The verifier weakly accepts if some pair of distinct provers is consistent, and strongly accepts if every pair is.

The max $k'$-cover instance of §5 attaches to every random string $r$ a copy $B_r$ of the explicit partition system. Its points are the vectors in $\{0,\dots,k-1\}^L$ with $L=2^\ell$, so $m=k^L$. Its $L$ partitions are labelled by the $\ell$-bit strings, and each splits the points by the value of one coordinate. There are $N=mR$ points in all. For each prover $i$, question $q$ and answer $a$, the set $S_{(q,a,i)}$ collects, for every $r$ on which $P_i$ receives $q$, the $i$th part of the partition of $B_r$ labelled by the values that $a$ gives to the distinguished variables of $r$. The budget is $k'=kQ$, where $Q$ is the number of questions a single prover can receive.

Formalization targets

Goal: Theorem 5.3

$$\forall\varepsilon>0:\quad \text{max } k\text{-cover is approximable within } 1-\tfrac1e+\varepsilon \ \Longrightarrow\ \mathrm{P}=\mathrm{NP},$$

conditional on the two cited results below. The ratio is left free (any $\varepsilon>0$), so the goal records the shape of the threshold and not a particular constant.

Milestones

• Proposition 2.1.2 (p. 640): for some $\varepsilon>0$ it is NP-hard to distinguish satisfiable 3CNF-5 formulas from those in which at most a $(1-\varepsilon)$-fraction of the clauses can be satisfied simultaneously.
• Lemma 2.3.1 (p. 643): a satisfiable $\varphi$ admits a strategy that always strongly accepts; on a far-from-satisfiable $\varphi$ the weak acceptance probability is at most $k^2\,2^{-c\ell}$.
• Coverage of the explicit partition system (p. 649): $j$ subsets from pairwise different partitions cover exactly $(1-(1-1/k)^j)m$ points.
• Proposition 5.4 (p. 649): if at most $kQ$ sets cover a $(1-1/e+\varepsilon)$-fraction of the points, then at least an $\varepsilon/3$-fraction of the random strings are good. Here $r$ is good if $w_r\le3k/\varepsilon$ sets meet $B_r$ and two of them from different provers lie in the same partition.
• Decoding (p. 649): such a covering yields a strategy that weakly accepts with probability at least $(\varepsilon/3)(\varepsilon/3k)^2$.
• Gap (p. 649): a satisfiable formula gives a cover of all $N$ points by $kQ$ sets. If at most a $(1-\varepsilon')$-fraction of the clauses are satisfiable, $kQ$ sets cover at most $(1-1/e+g(k))N$ points, where $g(k)\to0$, for all large $\ell$.
• Proposition 5.1 (p. 647): every greedy run covers at least $(1-1/e)\,\mathrm{opt}$ points.

Significance

The result closes the approximability of max $k$-cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:

• Submodular maximization. Coverage functions are monotone submodular, so the bound transfers to monotone submodular maximization under a cardinality constraint, whenever the function is given in a form that encodes a coverage instance.
• Other problems. Hardness results for facility location, budgeted allocation, and welfare maximization with coverage valuations reduce from it.
• The reduction itself. The $\ell$-fold $k$-prover system combined with a partition system that is exactly countable is the template for later $1-1/e$ hardness proofs.

Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:

• a machine-checked reduction from MAX 3SAT-5 to max $k$-cover;
• an exact counting lemma for product partition systems;
• the averaging and concavity argument of Proposition 5.4;
• a formal statement of the greedy bound for coverage.

The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.

Difficulty

The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly $h(j)=(1-(1-1/k)^j)m$, a concave function of the number $j$ of sets used. Since the sets meet a random string $k$ times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about $(1-(1-1/k)^k)$, which tends to $1-1/e$. A further obstacle is that the reduction must run in polynomial time. The paper therefore takes $\ell$ and $k$ constant (unlike the set-cover reduction, where $\ell=\Theta(\log\log n)$), and the soundness bound $k^2 2^{-c\ell}$ must beat $(\varepsilon/3)(\varepsilon/3k)^2$ at a constant $\ell$. The quantifier order ($k$ large first, then $\ell$ large) is part of the difficulty.

A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.

Formalization scope

• Machine model. CookPvsNP_defs (a published platform definition): one-tape Turing machines, $\mathrm{P}$, $\mathrm{NP}$, polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.
• Cited results as hypotheses. Theorem 2.1.1 enters as Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the $\ell$-fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most $2^{-c\ell}$. This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max $k$-cover is assumed.
• Approximation. The value form above, with no size threshold. For $\varepsilon>1/e$ the ratio exceeds one and the hypothesis is unsatisfiable on any instance with $\mathrm{opt}>0$; those values are vacuous, as in the paper.
• $\mathrm{opt}$. Taken over at most $k$ sets. This agrees with the paper's "exactly $k$" whenever $k\le s$.
• Probability and counting. Probabilities are uniform counts over the $(3M)^\ell$ random strings. Fractions in lower-bound statements are written as counts compared with multiples of $R$.
• Canonical answers. The type of answers is restricted to satisfying assignments of the received clauses, following the paper's "without loss of generality" (p. 643). All indices are 0-based.
• Partition system. The §4 construction is defined for any partition system with $\ell$-bit partition labels and instantiated with the explicit product system. Its $L=2^\ell$ coordinates are the $\ell$-bit strings themselves.
• Not formalized. The running time of the greedy algorithm, and the constructive variant (Proposition 5.2), which belongs to the set-cover mission.

A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max $k$-cover, and the approximation hypothesis is satisfiable for ratios up to $1$.

Needed infrastructure, reusable beyond this mission:

• composition and simulation lemmas for Cook's machines;
• the uniformity of the verifier's questions on 3CNF-5 formulas;
• concavity of $j\mapsto 1-(1-1/k)^j$;
• $(1-1/k)^k\to 1/e$ bounds.

Contributions to any of these, or to either cited theorem, are welcome.

Selected references

• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4) (1998) 634–652. https://doi.org/10.1145/285055.285059
• R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3) (1998) 763–803 (STOC 1995). https://doi.org/10.1137/S0097539795280895
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3) (1998) 501–555. https://doi.org/10.1145/278298.278306
• C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3) (1991) 425–440. https://doi.org/10.1016/0022-0000(91)90023-X
• C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5) (1994) 960–981. https://doi.org/10.1145/185675.306789
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions—I, Math. Programming 14 (1978) 265–294. https://doi.org/10.1007/BF01588971
• S. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about $\ln n$ times larger than the optimum on an instance with $n$ points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.

Timeline of the lower bounds:

• 1992. The PCP theorem (Arora, Lund, Motwani, Sudan, Szegedy) implies that set cover cannot be approximated within some constant $1+\varepsilon$ unless P = NP.
• 1994. Lund and Yannakakis showed that set cover cannot be approximated within $\tfrac14\log_2 n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\mathrm{polylog}\, n)})$, and within $\tfrac12\log_2 n\approx 0.72\ln n$ under a randomized assumption.
• 1998. Feige showed that for every $\varepsilon>0$, set cover cannot be approximated within $(1-\varepsilon)\ln n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\log\log n)})$ (J. ACM 45(4), 634–652). This matches the greedy bound up to lower-order terms.
• 2014. Dinur and Steurer replaced the assumption by P ≠ NP (STOC 2014).

This mission formalizes Feige's theorem, the result that fixed $\ln n$ as the threshold.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$ and a list of subsets $S_1,\dots,S_s$. A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some $S_i$. It is written as a string: $n$ in unary, then each subset as its characteristic vector.

A deterministic polynomial-time algorithm approximates set cover within $\rho(n)$ if, for some threshold $n_0$ and every coverable instance with $n \ge n_0$ points, the value $v$ it outputs satisfies $\mathrm{OPT}\le v\le\rho(n)\cdot\mathrm{OPT}$, where $\mathrm{OPT}$ is the size of a smallest cover.

$\mathrm{TIME}(n^{O(\log\log n)})$ is the class of languages that a deterministic one-tape Turing machine decides within $|w|^{c(\log_2\log_2|w|+1)}+c$ steps, for some constant $c$. Machines, $\mathrm{P}$ and $\mathrm{NP}$ are those of the published definition CookPvsNP_defs.

The proof passes through three objects, each defined in the mission:

1. 3CNF-5 formulas: CNF formulas in which every clause has three literals on distinct variables and every variable occurs in exactly five clauses.
2. The $k$-prover proof system of §2.3. A verifier picks $\ell$ random clauses and a distinguished variable in each. Each prover, according to its code word, receives some of these clauses and the distinguished variables of the others. Under the weak acceptance predicate, some two provers give consistent answers on the distinguished variables. Under the strong acceptance predicate, all provers do.
3. Partition systems $B(m,L,k,d)$ (Definition 3.1). These are $L$ partitions of $m$ points, each into $k$ parts, such that covering the points with parts taken from pairwise different partitions needs at least $d$ parts.

Formalization targets

Goal: Theorem 4.4

$$\exists\,\varepsilon>0:\ \text{set cover is approximable within }(1-\varepsilon)\ln n\ \Longrightarrow\ \mathrm{NP}\subseteq\mathrm{TIME}\big(n^{O(\log\log n)}\big).$$

The statement fixes no constant beyond $\varepsilon$. The parameters $k$, $\ell$ and $m$ of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.

Milestones, in the order the proof uses them

1. Proposition 2.1.2: MAX 3SAT-5 is gap NP-hard.
2. Proposition 2.2.1: the one-round clause–variable game has value $1-\varepsilon/3$.
3. Lemma 2.3.1: the $k$-prover system is complete with strong acceptance and has soundness $k^2 2^{-c\ell}$ for weak acceptance.
4. Lemma 3.2: partition systems with $d=(1-2/k)k\ln m$ exist.
5. Propositions 4.2 and 4.3: a cover with $(1-\delta)kQ\ln m$ subsets yields a prover strategy that is weakly accepted with probability at least $2\delta/(k\ln m)^2$.
6. Lemma 4.1: the gap between $kQ$ and $(1-2f(k))kQ\ln m$.

Significance

The result. Combined with the greedy algorithm, Theorem 4.4 shows that $\ln n$ is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The $k$-prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.

Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any $\Omega(\log n)$ inapproximability of set cover is known. This mission contributes:

• a Lean model of multi-prover proof systems with uniform-count probabilities;
• partition systems and their probabilistic existence proof;
• a gap-preserving reduction whose running time is analysed on Turing machines, not merely asserted.

Difficulty

• The ratio comes from two gaps at once. One is a gap in acceptance probability. The other is a gap between strong and weak acceptance. A reduction from a two-prover system, as in Lund–Yannakakis, loses a constant factor because a cheating cover can use two parts of the same partition. Feige's analysis must turn every small cover into a strategy under which some pair of provers is consistent (Proposition 4.3), and this averaging argument has to lose only a factor $(k\ln m)^2$.
• Parameters interlock. $\ell=\Theta(\log\log n)$ must make $k^2 2^{-c\ell}$ smaller than $2\delta/(k\ln m)^2$ while keeping the instance of size $n^{O(\log\log n)}$. The time bound must hold for a one-tape machine, including the deterministic partition-system construction.
• Encoding. The reduction must be computed by an explicit machine on string encodings. Showing that a "clearly polynomial" construction meets the time bound on such a machine is substantial work.

Formalization scope

• Cited results as hypotheses. Theorem 2.1.1, Raz's theorem and the Naor et al. construction are not proved in the mission; each is a named proposition (Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
  • RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a $2^{-c\ell}$ error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.
  • NaorPartitionSystems relaxes "time linear in $m$" to polynomial time and renders "$L$ polynomial in $d$" as $L\le\lfloor\log_2 m\rfloor^a$. Both relaxations weaken the hypothesis.
• Approximation in value form. The algorithm outputs a number $v$ with $\mathrm{OPT}\le v\le\rho(n)\mathrm{OPT}$, and only on coverable instances with $n\ge n_0$. Any algorithm that outputs a cover yields such a value, so this hypothesis is weaker than the paper's. The guard $n\ge n_0$ is needed because $(1-\varepsilon)\ln n<1$ for small $n$.
• Machine model. The machines are Cook's deterministic one-tape machines. Multi-tape simulation costs a quadratic factor, which the class absorbs.
• Probabilities are uniform counts over the $(5n)^\ell$ random strings. Strategies are deterministic. Answers are canonical (satisfying on clause coordinates), as the paper assumes without loss of generality.
• Not formalized. Randomized classes (ZTIME) are not defined here, so the following are omitted: the last sentence of Lemma 3.2, Proposition 6.1, and the randomized variants.
• Ruling out a trivial formalization. The gap notion requires far-from-satisfiable formulas to have at least one clause. Otherwise the empty formula would be both a yes-instance and a no-instance, and Theorem 2.1.1 would hold trivially.
• Infrastructure and reuse. The shared layer can serve other PCP-based hardness proofs: 3CNF-5 formulas, the $k$-prover system, partition systems, and the gap-NP-hardness notion. Welcome contributions include:
  • time bounds for list and table manipulations on one-tape machines;
  • a Hadamard-code construction satisfying the weight and distance conditions;
  • the union-bound and averaging lemmas behind Lemma 2.3.1 and Proposition 4.2.

Selected references

• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4), 634–652, 1998. https://doi.org/10.1145/285055.285059
• C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5), 960–981, 1994. https://doi.org/10.1145/185675.306789
• R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3), 763–803, 1998 (STOC 1995). https://doi.org/10.1137/S0097539795280895
• M. Naor, L. J. Schulman, A. Srinivasan, Splitters and near-optimal derandomization, FOCS 1995, 182–191. https://doi.org/10.1109/SFCS.1995.492475
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306
• C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. Syst. Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
• V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4(3), 233–235, 1979. https://doi.org/10.1287/moor.4.3.233
• I. Dinur, D. Steurer, Analytical approach to parallel repetition, STOC 2014, 624–633. https://doi.org/10.1145/2591796.2591884

Motivation

A buyer and a seller negotiate over a single indivisible good. Each knows how much the good is worth to them, but not how much it is worth to the other side. Whether the two will trade, and at what price, then depends on how each party shades its offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this situation as a one-shot game in which both parties submit sealed offers simultaneously, and characterised its Bayesian equilibria.

The model became the standard reference point for bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) showed that no mechanism can guarantee efficient trade in this setting, and that the equilibrium of the Chatterjee–Samuelson game with $k = 1/2$ and uniform values attains the second-best efficiency bound. Later work on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the continuum of equilibria of exactly this game. The object of the present mission, a pair of linked differential equations, is the tool these papers use to construct and classify equilibria.

Setting

A seller has reservation price $v_s \in [\underline v_s, \bar v_s]$ and a buyer has reservation price $v_b \in [\underline v_b, \bar v_b]$. Each knows their own value. The buyer's belief about $v_s$ is a probability measure $\mu_b$ with distribution function $F_b$; the seller's belief about $v_b$ is $\mu_s$ with distribution function $F_s$. The subscript names the player who holds the belief, not the variable. Each belief is regular: $F(\underline v) = 0$, $F(\bar v) = 1$, and $F$ is strictly increasing and differentiable on the value interval, with density $f_b$ (respectively $f_s$).

Under the Bargaining Rule, the seller asks $s$ and the buyer offers $b$ simultaneously. If $b \ge s$ the good is sold at $P = kb + (1-k)s$ for a fixed $k \in [0, 1]$; otherwise nothing happens. Profits are $P - v_s$ for the seller and $v_b - P$ for the buyer on trade, and zero otherwise.

An offer strategy is a function $S$ (for the seller) or $B$ (for the buyer) from values to offers. Against $S$, a buyer with value $v$ offering $b$ earns in expectation

$$\pi_b(b, v) = \int \mathbf 1\{S(v_s) \le b\}\,\bigl(v - kb - (1-k)S(v_s)\bigr)\,d\mu_b(v_s),$$

and symmetrically $\pi_s(s, v) = \int \mathbf 1\{s \le B(v_b)\}\,(kB(v_b) + (1-k)s - v)\,d\mu_s(v_b)$. The pair $(S, B)$ is an equilibrium if $B(v)$ maximises $\pi_b(\cdot, v)$ over all real offers for every buyer value $v$, and $S(v)$ maximises $\pi_s(\cdot, v)$ for every seller value $v$.

A strategy is of class $A$ if its offers are bounded, it is nondecreasing, it is strictly increasing except where it sits at its lowest offer $m$ or its highest offer $M$, and it is differentiable wherever its offer lies strictly between $m$ and $M$. A class $A$ equilibrium is an equilibrium in which both strategies are of class $A$.

Formalization targets

Goal: Theorem 2, the linked differential equations

In a class $A$ equilibrium, wherever the seller's strategy is strictly increasing around $y$ and the buyer value $x$ offers $B(x) = S(y)$,

$$k F_b(y) S'(y) + f_b(y) S(y) = x\, f_b(y), \tag{3a}$$

and wherever the buyer's strategy is strictly increasing around $x$ and the seller value $y$ asks $S(y) = B(x)$,

$$(1-k)\bigl(1 - F_s(x)\bigr) B'(x) - f_s(x) B(x) = -\,y\, f_s(x). \tag{3b}$$

The paper writes $x = B^{-1}(S(y))$ in (3a) and $y = S^{-1}(B(x))$ in (3b).

Milestones: the displays of the proof

1. $G_b(S(y)) = F_b(y)$: the buyer's probability that the seller asks at most $S(y)$ equals $F_b(y)$.
2. The buyer's first-order condition: $\partial \pi_b / \partial b = (v - b) g_b(b) - k G_b(b)$ at $b = S(y)$, with offer density $g_b(S(y)) = f_b(y)/S'(y)$, and it vanishes at an equilibrium offer.
3. The seller's first-order condition: $\partial \pi_s / \partial s = (v - s) g_s(s) + (1-k)(1 - G_s(s))$ at $s = B(x)$, and it vanishes at an equilibrium ask.

The milestones assume $S'(y) > 0$ (respectively $B'(x) > 0$), which the paper's formula for the offer density needs. The goal does not assume it.

Significance

Theorem 2 reduces the search for equilibria to the analysis of a pair of ordinary differential equations. Every explicit equilibrium in the paper and in the later $k$-double-auction literature is found as a solution of (3a)–(3b) with suitable boundary conditions: the linear equilibrium for uniform beliefs (the paper's Example 1), the one-parameter families of Satterthwaite–Williams, and the non-linear equilibria of Leininger–Linhart–Radner. The equations also expose how the split parameter $k$ distributes bargaining power: at $k = 1$ equation (3b) forces the seller to ask their own value, and at $k = 0$ equation (3a) forces the buyer to bid theirs.

The result is proved in the paper. To the best of a search of the platform, no formalization of it or of the bargaining model exists. This mission produces a machine-checked version of the necessary conditions. Its definitions of beliefs, expected profits, equilibrium and class $A$ are also the basis for companion missions on the uniform linear equilibrium and its trade probability.

Difficulty

The paper's proof is four lines: differentiate the expected profit, set the derivative to zero, substitute. Three steps of that argument do not survive a careful reading.

First, the paper differentiates under an offer density $g_b$ that exists only if $S$ is strictly increasing and has a positive derivative. Class $A$ allows $S$ to be flat at its bounds, to jump between them, and to have zero derivative. The formal goal assumes none of this. It must handle the case $S'(y) = 0$, where the offer distribution has an infinite density at $S(y)$ and the first-order condition becomes a one-sided argument.

Second, identifying $G_b(S(y))$ with $F_b(y)$ requires that no seller value outside a neighbourhood of $y$ makes the same offer. That is a global statement about $S$, and it is where monotonicity on the whole interval and the "flat only at the bounds" clause of class $A$ enter.

Third, the first-order condition needs the equilibrium offer $S(y)$ to be an interior maximiser of a function of $b$ that is differentiable there. The profit $\pi_b$ is an integral over the belief, and its differentiability at $S(y)$ must be derived from the differentiability of $S$ at the single point $y$ and of $F_b$. Neither $S$ nor $\pi_b$ is assumed continuous elsewhere.

Formalization scope

Values, offers and $k$ are real numbers. Beliefs are probability measures on $\mathbb R$, with distribution function Mathlib's ProbabilityTheory.cdf. Expected profits are Bochner integrals over the opponent's value, not over an offer density. The two agree whenever the density exists, and the integral form needs none. Integrability is not assumed: for a class $A$ strategy and a regular belief supported on the value interval, the integrand is bounded and almost everywhere measurable. Ties ($b = s$) trade. Deviations range over all real offers. Strategies are arbitrary functions $\mathbb R \to \mathbb R$ whose values outside the value interval play no role.

The derivative $S'(y)$ is deriv S y. The paper's inverses $B^{-1}$ and $S^{-1}$ are not introduced as functions. The matching value is a universally quantified variable $x$ with $B(x) = S(y)$, so no junk value of an inverse can make an equation true or false. The equations are asserted only at values $y$ interior to an open subinterval on which $S$ is strictly increasing. A formalization that assumed the first-order condition, or restricted to strategies with $S' > 0$ everywhere, would be a different and weaker theorem.

A complete development needs: differentiation of parametric integrals of indicator type (the derivative of $b \mapsto \int \mathbf 1\{S \le b\}\,h\,d\mu$), the change of variables from values to offers under a strictly increasing strategy, and Fermat's rule (IsLocalMax.hasDerivAt_eq_zero). The first two are reusable for auctions and other Bayesian games with monotone strategies. Proofs of the milestones, alternative proofs of the goal, and general lemmas about monotone strategies are welcome.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

Variational inequalities and complementarity problems are the standard formulation of equilibrium in operations research and mathematical economics: traffic equilibria, spatial price equilibria, Nash equilibria of convex games, and the optimality conditions of constrained optimization all take this form. Many applications have two features that the classical theory does not cover. The feasible set of a player or a flow can depend on the current state (a quasi-variational inequality, as in generalized Nash games with shared constraints), and the response map can be set-valued (a subdifferential, or a best-response correspondence). D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the generalized quasi-variational inequality covering both, proved existence theorems for it, and derived existence for a new generalized implicit complementarity problem.

Timeline of the results this mission builds on:

• 1966: Hartman and Stampacchia prove existence for the variational inequality on a compact convex set.
• 1973: Bensoussan, Goursat and Lions introduce quasi-variational inequalities for impulse control.
• 1976: Saigal extends the complementarity problem to set-valued maps.
• 1974: Moré gives coercivity conditions for nonlinear complementarity problems; a special version of the lemma of §3 appears there.
• 1979: Fang and Peterson prove a general existence theorem for generalized variational inequalities (report, University of Maryland Baltimore County); the lemma of §3 and the constant-$K$ case of Theorem 3.2 are taken from there.
• 1982: Chan and Pang prove existence for the generalized quasi-variational inequality using the Eilenberg–Montgomery fixed point theorem, and derive existence for the generalized implicit complementarity problem under strong copositivity (Theorem 4.2), the goal of this mission.

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $x^T y$ and norm $\|x\|$. A point-to-set mapping $K$ assigns to each $x\in\mathbb R^n$ a set $K(x)\subseteq\mathbb R^n$. Given point-to-set mappings $K$ and $f$, the problem $\mathrm{GQVI}(K,f)$ asks for vectors $x,y$ with

$$x\in K(x),\qquad y\in f(x),\qquad (x'-x)^T y\ge 0\ \text{ for all } x'\in K(x).$$

A cone is a convex set containing $0$ and closed under nonnegative scaling. The dual cone of a set $S$ is $S^*=\{y : y^T x\ge 0 \text{ for all } x\in S\}$. For a point-to-point map $m$, a cone-valued map $L$ and a point-to-set map $f$, the problem $\mathrm{GICP}(L,m,f)$ asks for $x,y$ with

$$x\in m(x)+L(x),\qquad y\in f(x)\cap L(x)^*,\qquad y^T\big(x-m(x)\big)=0 .$$

A mapping $f$ is upper semicontinuous on a set $C$ at $x\in C$ if for each open $G\supseteq f(x)$ there is a neighbourhood $N$ of $x$ with $f(y)\subseteq G$ for $y\in N\cap C$; lower semicontinuous if for each open $G$ meeting $f(x)$, $f(y)$ meets $G$ for all $y$ near $x$ in $C$; continuous if both. A set $S$ is contractible if some point $x\in S$ and a continuous $g:S\times[0,1]\to S$ satisfy $g(x',0)=x'$, $g(x',1)=x$. $B_r$ is the closed ball of radius $r$ about the origin, $C_r$ its boundary sphere. For point-to-set maps $\mu$ and $K$, the coercivity function is

$$C_{\mu,K}(r,x^0)=\inf_{x\in K(x)\cap C_r}\Big[\inf_{y\in\mu(x)}(x-x^0)^T y\Big]\Big/(r+\|x^0\|),$$

with $\inf\emptyset=+\infty$. The map $\mu$ is strongly copositive with respect to $K$ at $x^0$ if $x^0\in K(x^0)$ and for some $\alpha>0$ and $y^0\in\mu(x^0)$, $(y-y^0)^T(x-x^0)\ge\alpha\|x-x^0\|^2$ for all $x\in K(x)$ and $y\in\mu(x)$. For $\mu$ and $q\in\mathbb R^n$, $(\mu+q)(x)=\{y+q : y\in\mu(x)\}$.

Formalization targets

Goal: Theorem 4.2 (p. 218)

Let $\tilde L$ be a closed cone with nonempty interior, $m$ continuous, $K(x)=m(x)+\tilde L$, and $\mu$ a mapping with nonempty contractible compact values, upper semicontinuous on $\mathbb R^n$. If some $\tilde u$ satisfies $\tilde u-m(x)\in\tilde L$ for all $x$, and $\mu$ is strongly copositive with respect to $K$ at $\tilde u$, then for every $q$

$$\exists\, x,y:\quad x-m(x)\in\tilde L,\quad y\in\mu(x)+q,\quad y\in\tilde L^*,\quad y^T(x-m(x))=0 .$$

Milestones, in the order the proof uses them

• Theorem 3.1 (p. 214): for continuous $\varphi$ quasi-concave in its first argument on a nonempty compact convex $C$, some $u^*\in V(u^*)=K(u^*)\cap C$ and $w^*\in f(u^*)$ satisfy $\varphi(v,u^*,w^*)\le\varphi(u^*,u^*,w^*)$ for all $v\in V(u^*)$.
• Lemma of §3 (p. 215): a variational inequality on $W\cap E$ at a point of $W\cap E^0$ extends to $W$.
• Theorem 3.2 (p. 215): existence for $\mathrm{GQVI}(K,f)$ from a compact truncation $C=U\cap E$ and a boundary condition on $\partial E$.
• Theorem 4.1 (p. 217): if $C_{\mu,K}(r,x^0)\ge 0$, then $\mathrm{GQVI}(K,\mu+q)$ has a solution in $B_r$ whenever $\|q\|\le C_{\mu,K}(r,x^0)$.
• Corollary 4.1 (pp. 217–218): under the coercivity condition (4), $\mathrm{GQVI}(K,\mu+q)$ is solvable for every $q$, with bounded solution set.
• Lemma 4.1 (p. 218): strong copositivity at $x^0$ implies coercivity (4) at $x^0$.
• Proposition 2.1 (p. 213): $\mathrm{GICP}(L,m,f)$ and $\mathrm{GQVI}(m+L,f)$ have the same solutions.

Significance

Theorem 4.2 gives existence for complementarity problems whose cone is translated by a state-dependent map $m$ and whose response map is set-valued. It contains existence for the implicit complementarity problem of Capuzzo-Dolcetta, Mosco and Pang ($\tilde L=\mathbb R^n_+$) with strongly monotone data (Corollary 4.2 of the paper), and Saigal's generalized complementarity problem ($m\equiv0$). Theorems 3.2 and 4.1 are general-purpose existence tools for quasi-variational inequalities with set-valued maps; Theorem 3.2 reduces to the Fang–Peterson theorem when $K$ is constant, and Corollary 3.1 to the Hartman–Stampacchia theorem when in addition $f$ is single-valued.

All results of the paper are proved; none is open. To our knowledge none of them has been formalized: no proof assistant library contains quasi-variational inequalities with set-valued maps, and Mathlib has neither Kakutani's nor the Eilenberg–Montgomery fixed point theorem (nor Brouwer's). A formal proof of the goal therefore also produces a reusable library of set-valued existence theory.

Difficulty

The whole chain rests on Theorem 3.1, whose proof applies the Eilenberg–Montgomery fixed point theorem for upper semicontinuous maps with acyclic (here contractible) compact values; this in turn needs either singular homology or an approximation argument, neither of which is available in Mathlib. Replacing "contractible" by "convex" to use Kakutani's theorem would prove a strictly weaker theorem: the paper states contractible values deliberately. The second difficulty is that the fixed point only solves the problem on the truncation $V(x)=K(x)\cap C$; turning it into a solution over all of $K(x)$ needs the boundary argument of Theorem 3.2, and for Theorem 4.2 the continuity of $x\mapsto (m(x)+\tilde L)\cap B_\rho$, which is where the solidity of $\tilde L$ is used. The obvious approach of applying Theorem 3.2 directly with $C=\mathbb R^n$ fails because $C$ must be compact.

Formalization scope

The space is EuclideanSpace ℝ (Fin n), so all norms and balls are Euclidean (not the sup norm of Fin n → ℝ). Point-to-set mappings are functions into Set; semicontinuity "on $C$" is Mathlib's UpperHemicontinuousOn/LowerHemicontinuousOn with neighbourhoods relative to $C$, and "on $\mathbb R^n$" is UpperHemicontinuous. Cones are PointedCone ℝ _ (convex, containing $0$, as footnote 1 of the paper says). Balls are centred at the origin.

Conventions that the Lean statements make explicit:

• The paper takes its semicontinuity from Berge, whose upper semicontinuous maps have compact values. Theorems 3.1, 3.2, 4.1 and Corollary 4.1 are false without this ($K(x)\equiv(0,1)$, $C=[0,1]$, $f\equiv\{1\}$), so each one carries an explicit closedness hypothesis on $K(x)\cap C$ or $K(x)\cap B_\rho$. Theorem 4.2 needs none, since $m(x)+\tilde L$ is closed.
• Every infimum uses $\inf\emptyset=+\infty$. Bounds of the form $C_{\mu,K}(r,x^0)\ge c$, condition (v) of Theorem 3.2, and the limit (4) are stated in universally quantified form. A real-valued $C_{\mu,K}$ would be wrong: it returns $0$ on an empty set.
• Lemma 4.1 is stated at the same point $x^0$, which is what its proof gives. In Corollary 4.1 the bound $r$ on the solutions is chosen after $q$.
• Three glyphs are illegible in the scan and are read from the proofs: $\le$ in Theorem 3.1, $\ge 0$ in Theorem 3.2(v), and $\ge$ in the Lemma of §3.

A trivializing formalization is ruled out: the GQVI solution tests over all of $K(x)$, not over $V(x)=K(x)\cap C$, and the GICP solution keeps both the dual-cone condition and the complementarity equation. Dropping any of these would turn the goal into a restatement of Theorem 3.1.

A complete development needs: an Eilenberg–Montgomery (or at least Kakutani plus an acyclicity argument) fixed point theorem for set-valued maps, Berge's maximum theorem, and basic facts on hemicontinuity of intersections and translates of set-valued maps. The fixed point theorems, the maximum theorem and the hemicontinuity lemmas are reusable far beyond this mission. Contributions of any of these as separate theorems are welcome.

Selected references

• D. Chan, J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
• S. Eilenberg, D. Montgomery, Fixed point theorems for multi-valued transformations, American Journal of Mathematics 68 (1946) 214–222. https://doi.org/10.2307/2371832
• C. Berge, Topological Spaces, Macmillan, New York, 1963.
• S. C. Fang, E. L. Peterson, Generalized variational inequalities, Mathematics Research Report 79-10, Department of Mathematics, University of Maryland Baltimore County, 1979 (no public link).
• J. J. Moré, Coercivity conditions in nonlinear complementarity problems, SIAM Review 16(1) (1974) 1–16. https://doi.org/10.1137/1016001
• P. Hartman, G. Stampacchia, On some non-linear elliptic differential-functional equations, Acta Mathematica 115 (1966) 271–310. https://doi.org/10.1007/BF02392210
• R. Saigal, Extension of the generalized complementarity problem, Mathematics of Operations Research 1(3) (1976) 260–266. https://doi.org/10.1287/moor.1.3.260