All missions

Certify the classical quadratic separation between sensitivity and block sensitivity: $\alpha\ge2$.

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$, write $x^B$ for the input obtained by flipping the coordinates in $B$. Its sensitivity is $s(f)=\max_x|\{i:f(x^{\{i\}})\ne f(x)\}|$. Its block sensitivity $bs(f)$ is the largest number of pairwise disjoint nonempty sets $B$ that satisfy $f(x^B)\ne f(x)$ at a common input $x$.

The goal is to prove that for every $\varepsilon>0$ and every integer $S\ge2$, there is a total Boolean function with

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{2-\varepsilon}.$$

The construction milestone is Rubinstein’s quadratic separation: for each integer $m\ge1$, there is a function on $(2m)^2$ bits with

$$s(f)=2m,\qquad bs(f)=2m^2.$$

These exact bounds imply the goal because $bs(f)=s(f)^2/2$ and sensitivity grows without bound. This is a known theorem; the task is to formalize it using the campaign’s shared definitions.

The main combinatorial work is controlling sensitivity at every input and proving the matching block-sensitivity bounds. Lean represents functions as (Fin n → Bool) → Bool; both measures are maxima over all inputs. The goal reuses SensitivityCampaign.AchievesExponent, so it has exactly the same meaning as the campaign’s stronger targets. No composition theorem is required for this family argument.

References: David Rubinstein, Sensitivity vs. block sensitivity of Boolean functions, Combinatorica 15 (1995), 297–299, DOI. The statement and construction are also recalled in Theorem 1 of Madars Virza, Sensitivity versus block sensitivity of Boolean functions (2010), arXiv:1008.0521.

Motivation

A firm can learn a customer's preference before choosing a customized product, or it can let the customer choose a requested design. The two approaches assign the design decision to different parties. That matters when design changes both the value of a sale and a cost the seller must incur before the price is negotiated. Guo's study of customer voice in customization compares these approaches in a model where a buyer has private information about how much it values quality. The payoff comparison asks who gains from holding the design right and whether the answer survives a modest fixed cost of using that approach.

This mission concerns Proposition 8 of the SSRN author copy, printed page 23. The result is a comparative statement about two already specified separating equilibrium outcomes. Earlier results in the same paper characterize when the outcomes arise: Proposition 1 treats communication before seller design, and Proposition 3 treats a buyer's design request. Proposition 8 compares the parties' payoffs at the qualities associated with those outcomes. Its four clauses distinguish gross payoff rankings from net rankings after an incremental fixed cost. The paper states Proposition 8 without a separate proof; its surrounding discussion explains its interpretation. All page and result numbers here follow the SSRN version of 2023-11-29.

Setting

There is one seller and a unit mass of buyers. Each buyer has one-unit demand and a privately known quality preference $\theta_i$, with type $i\in\{H,L\}$ and $\theta_H>\theta_L>0$. The high type has population share $\alpha\in(0,1)$, while the low type has share $1-\alpha$. A product's quality is a nonnegative real number $q$. Producing a unit of quality $q$ costs $kq^2$, and offering that product incurs a selling cost $sq^2$, where $k,s>0$. The selling cost is incurred before the price is settled. The seller makes a take-it-or-leave-it offer with probability $\gamma\in(0,1)$; the buyer does so with probability $1-\gamma$. These primitives and the timing are specified in Section 2.

In A-Learning, the buyer sends a costless message about its preference and the seller chooses the design. In O-Learning, the buyer requests a quality and the seller decides whether to accept it. The paper compares separating outcomes, so each type is associated with its true preference when the equilibrium payoff is evaluated. The pricing stage is represented by the paper's payoff formulas. If the seller regards a buyer's preference as $\hat\theta$, its payoff from quality $q$ is

$$v(q,\hat\theta)=\gamma(\hat\theta q-kq^2)-sq^2.$$

The buyer's payoffs $u^A(\theta,\hat\theta,q)$ and $\mu(q,\theta,\hat\theta)$ retain the nonnegative parts in equations (5) and (9): each is $\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}$, with its arguments ordered as in the relevant equation. For type $i$, the paper's A-Learning and O-Learning equilibrium qualities are

$$q^A_i=\frac{\gamma\theta_i}{2s+2\gamma k},\qquad q^O_i=\min\left\{\frac{\gamma\theta_i}{s+\gamma k},\frac{\theta_i}{2k}\right\}.$$

Write $\alpha_H=\alpha$ and $\alpha_L=1-\alpha$. The seller's expected gross payoffs are $V^A=\sum_i\alpha_i v(q^A_i,\theta_i)$ and $V^O=\sum_i\alpha_i v(q^O_i,\theta_i)$. The buyer payoffs $U^A_i$ and $U^O_i$ evaluate $u^A$ and $\mu$ at type $i$'s quality and truthful preference. These are the payoffs defined around equations (8) and (13) of the paper.

Formalization targets

The first comparison says that the seller earns more from its own design, while each buyer type earns more from its requested design:

$$V^A>V^O,\qquad U^A_i<U^O_i\quad(i\in\{H,L\}).$$

The two fixed-cost clauses hold the preference levels, population share, bargaining weight, and production-cost coefficient fixed while the positive selling-cost coefficient $s$ varies. For every seller-side incremental fixed cost $F>0$, there is a positive threshold $\tilde s_F$ such that

$$0<s<\tilde s_F\quad\Longrightarrow\quad V^A(s)-F<V^O(s).$$

For every buyer-side incremental fixed cost $G>0$ and each type $i$, there is a positive threshold $\tilde s_{iG}$ such that

$$0<s<\tilde s_{iG}\quad\Longrightarrow\quad U^A_i(s)>U^O_i(s)-G.$$

The goal is the conjunction of these four clauses, exactly the payoff content of Proposition 8. The milestone list also includes the paper's strict quality comparison $q^A_i<q^O_i$ and its observation that the quality difference tends to zero as $s$ tends to zero. The printed statement and discussion are on pages 22–23.

Significance

The gross comparisons separate the seller's and buyers' preferences over who chooses quality. The fixed-cost clauses show why the party favored by the gross comparison need not favor that approach once its own extra effort or implementation expense is counted. The thresholds make this claim uniform over all sufficiently small positive selling costs, rather than treating the single case $s=0$. This distinction is relevant when comparing preference solicitation, which requires seller effort, with buyer-led design, which requires customer effort.

Formalizing the result gives a reusable two-type model of quadratic production and selling costs, the two reduced-form buyer payoffs, and a finite-population expected-payoff calculation. It also creates separate targets for each clause, so the gross-payoff and small-cost claims can be checked independently. The result is proved in the mathematical paper only to the extent of its stated Proposition 8 and accompanying discussion; the local Lean statements in this proposal compile with proof placeholders and do not yet constitute machine-checked proofs.

Difficulty

The two approaches select different quality formulas, and O-Learning uses a minimum of two expressions. As $s$ changes, that minimum can switch branches. The buyer payoff formulas also contain maxima with zero, so replacing them unconditionally with simplified quadratic expressions would change the model. A valid payoff comparison must account for the relevant branch and preserve the strict inequalities for both buyer types. For the fixed-cost clauses, pointwise closeness at $s=0$ does not itself state a uniform claim for every sufficiently small positive $s$; the threshold must be positive and chosen before $s$.

Formalization scope

The Lean model uses a two-constructor buyer type, real parameters $\theta_H,\theta_L,\alpha,\gamma,k,s$, and a Standing predicate carrying every displayed positivity and interval assumption. Qualities are real-valued, with the paper's intended domain $q\geq0$; the closed-form equilibrium qualities in this mission are nonnegative under those assumptions. Expected seller payoffs use a finite sum over exactly the high and low types, weighted by $\alpha$ and $1-\alpha$. Buyer payoffs use the original maxima with zero. The pricing stage is in reduced form through equations (4), (5), and (9). The model and payoff notation are local to CustomerVoice.Payoffs, because the other missions' definitions are unpublished drafts.

The statements compare the printed closed-form qualities without adding the separate inequalities that guarantee both separating equilibria exist. Thus their domain is all parameter choices satisfying Section 2's standing assumptions; this is the stronger reading identified in the paper's planning notes for Proposition 8. In the small-$s$ statements, withS changes only the selling-cost coefficient, and the quantified values of $s$ satisfy $0<s<\tilde s$. The proof targets cannot be reduced by deleting the nonnegative parts of the buyer payoffs, allowing a zero threshold, or checking only the limit at $s=0$. Contributions to the elementary quality comparisons, branch-sensitive payoff inequalities, and positive-side limits all support the goal. The finite weighted-payoff and limit infrastructure can be reused in other small-cost comparisons.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, version of 2023-11-29, §§2–3.4 and Proposition 8. SSRN record.
• Liang Guo, The Voice of Customers in Customization, Management Science, 2021. DOI:10.1287/mnsc.2021.04025. The mission's statement indices follow the SSRN copy above.

Why dispatch and pricing interact

A delivery vendor controls both how a courier serves orders and what customers pay. Serving one order per trip avoids waiting for a second order, but serving two together can save travel time when demand is high. If the vendor can change its price, it also changes the rate at which customers join the system. The preferred dispatch rule therefore depends on an economic decision as well as a queueing calculation. Chen and Hu study this interaction for a single courier in a disk-shaped market and compare the vendor's revenue under dedicated and two-order batch delivery in their paper. The present mission concerns their crowded-market results, Propositions 3 and 4, in the authors' SSRN version of 2022-09-21.

The paper first analyzes fixed demand rates, then lets the vendor choose a demand rate by setting a price. The latter decision changes the comparison: customers with a high cost of waiting favor a less crowded, dedicated service, while sufficiently patient customers can make batching more profitable. The service radius has an analogous effect. The paper's threshold is expressed through the product of wait cost and radius, so these two comparative statics describe the same switch Chen and Hu, §5 and Online Appendix A.

Delivery model and limiting revenue

A vendor is located at the center of a disk of radius $r>0$. Customers arrive at locations uniformly distributed over that disk. The vendor has one courier and chooses between dedicated delivery, one order per round trip, and batch delivery, two orders per trip. The effective demand rate is $\lambda$. A customer incurs wait cost at rate $c>0$ and has a valuation in $[0,1]$. The vendor's price induces its chosen demand rate. Chen and Hu give the dedicated service rate $\mu_D=3/(4r)$ and batch service rate $\mu_B=45\pi/[4r(32+15\pi)]$ in equations (4) and (9).

The paper uses the following expected waiting times, with variation coefficients $C_D=9/8$ and $C_B\approx0.583$:

$$W_D(\lambda,\mu,C)=\frac{\lambda C}{2\mu(\mu-\lambda)},\qquad W_B(r,\lambda,\mu,C)=\frac{1}{2\lambda}+\frac{\lambda C}{2\mu(2\mu-\lambda)}+\frac r3.$$

Dedicated delivery is evaluated for $0\le\lambda<\mu_D$; batch delivery for $0<\lambda<2\mu_B$. The first batch term is the wait to form a pair. The final term represents travel while the other order is delivered. The batch in-line wait is the paper's Kingman-based approximation for an $E_2/G/1$ queue, whereas the dedicated in-line wait uses its $M/G/1$ expression equations (5), (11), and (12).

In a finite market, the valuation distribution affects the price needed to induce demand. As the potential arrival rate grows, the paper's crowded-market revenue becomes

$$V_\infty(\lambda,w)=\lambda(1-cw).$$

For each dispatch rule, insert its wait into this function and optimize over its stable demand range. The resulting optimal revenues are denoted $\operatorname{Opt}_D(c,r)$ and $\operatorname{Opt}_B(C_B,c,r)$. The mission uses suprema to express these values. The paper motivates this limiting objective in (14)–(15) and Lemma 1 (16)–(17).

Formalization targets

One threshold for both parameters

The goal is a single $\alpha^*>0$ such that, for every $c,r>0$,

$$\operatorname{Opt}_B(C_B,c,r)>\operatorname{Opt}_D(c,r)\quad\Longleftrightarrow\quad cr<\alpha^*, \qquad \operatorname{Opt}_D(c,r)>\operatorname{Opt}_B(C_B,c,r)\quad\Longleftrightarrow\quad cr>\alpha^*.$$

Thus the wait-cost threshold at a fixed radius is $c_\infty=\alpha^*/r$, and the radius threshold at a fixed wait cost is $r_\infty=\alpha^*/c$. At the threshold the two optimized revenues agree. For the paper's numerical $C_B=0.583$, it reports $\alpha^*\approx0.1355$ Online Appendix (A.7)–(A.8).

Demand and price at the switch

As either $c$ or $r$ increases through its threshold, the optimal demand rate has a downward jump and the corresponding optimal price has an upward jump. The formal statements require both one-sided limits to exist and the inequalities between them to be strict. They cover every selection of optimal demands, including any ambiguity at the tie. These are parts (ii) of Propositions 3 and 4.

The milestones cover strict concavity of the revenue objectives, their explicit optimizers and values where attained, the single crossing of the revenue gap, the demand comparison at the tie, and the two propositions individually. The goal combines those propositions through the common product $cr$.

What the result and formalization establish

The threshold tells the vendor which dispatch rule maximizes limiting revenue after the price has been adjusted optimally. It also locates a discontinuous operational change: a small movement in customer impatience or service area across the threshold changes the chosen mode, demand rate, and price. Comparing the waiting-time formulas at one fixed demand would not provide this revenue decision, because each mode can choose a different demand rate Chen and Hu, §5.

Chen and Hu prove the paper result analytically, while the threshold and its supporting claims here are proposed Lean statements awaiting proofs. A completed formalization would connect exact claims about the rational waiting-time expressions, optimization over open stability ranges, the unique revenue crossing, and one-sided limits. It would also record which conclusions use the paper's approximated batch wait and numerically estimated coefficient. These are reusable patterns for queue-based pricing models, even though this mission formalizes this paper's particular geometry and service rules.

Where the argument is delicate

The two dispatch modes have different singular boundaries and different optimizers. The batch wait diverges as demand tends to zero, yet batch revenue can have a finite boundary supremum that is not attained for some parameter values. The dedicated objective has a different service-rate pole. Consequently, replacing either optimization with an unrestricted real supremum, or asserting that every batch supremum has a maximizer, changes the claim. The revenue comparison also needs one crossing for the full positive range of $cr$, including values beyond the range where the appendix's interior batch optimizer applies. Finally, a strict jump in demand does not by itself supply the existence of both one-sided limits; the formal statements ask for those limits explicitly Online Appendix A.

Formalization scope

Lean uses real-valued $r,c,\lambda$ and the paper's closed-form waits, service rates, and limiting revenue. The name lam denotes $\lambda$. The batch coefficient is a real parameter satisfying $0.58\le C_B\le0.59$, an explicit interval around the paper's numerical $0.583$ rather than a claimed exact evaluation of its integral. Every threshold statement assumes $c,r>0$; the auxiliary optimum statements use the page's $cr<T_B$ range when they assert an interior maximizer. The domains are $[0,\mu_D)$ and $(0,2\mu_B)$, with zero excluded for batch because its $1/(2\lambda)$ wait is singular. The optimal revenues are defined as suprema of the actual objective images. The threshold is existential and is never defined from the desired answer.

The formal development does not construct the Poisson arrival process, random trip lengths, $M/G/1$ queue, or $E_2/G/1$ approximation behind the waits. It takes the paper's equations (5) and (12) as definitions. The finite-density function $V_n$ is recorded for context, but Lemma 1's convergence from finite to limiting optimized revenue is outside this mission's milestone list; the goal is explicitly the crowded-market limit. The printed (A.6)–(A.8) contain a coefficient error in the batch value, so the formal batch value uses the corrected expression and defines the revenue gap directly from the suprema. The printed batch optimization interval includes zero, which the stated waiting-time formula does not support. Definitions for objectives, stable domains, optimal demand, and one-sided jumps are reusable within related pricing formalizations. Contributions that establish the stated optimizer, crossing, or limit claims without changing their domains are within scope Chen and Hu, equations (12), (15), (A.3)–(A.8).

Selected references

• Mingliu Chen and Ming Hu, Courier Dispatch in On-Demand Delivery, SSRN preprint 3675063, version of 2022-09-21. SSRN record and paper.
• Mingliu Chen and Ming Hu, Courier Dispatch in On-Demand Delivery, Management Science, 2023, DOI 10.1287/mnsc.2023.4858. The formal statements use the SSRN version above.

Motivation

Sellers often ask customers what they want before designing a product or service. The answer can affect both the quality delivered and the price paid. Because a customer can send a costless, unverifiable message, the seller cannot assume that a stated preference is true. Guo's customization model asks when the customer's own incentives make truthful communication sustainable. This matters for products with substantial presale effort, such as prototypes, proposals, and sales assistance: the seller incurs that effort before the final transaction price is set. The paper distinguishes this selling cost from the cost of producing the eventual product. This mission concerns the paper's A-Learning game, in which the seller learns through a customer's message before choosing quality.

Setting

Each buyer wants one unit of a product with quality $q\geq0$. A buyer with preference $\theta$ values it at $\theta q$ and can decline to trade. The preference is private and has two possible values, $\theta_H>\theta_L>0$. The high type has prior share $\alpha\in(0,1)$. Producing quality $q$ costs $kq^2$ and selling it costs $sq^2$, with $k,s>0$. The selling cost is incurred at the design stage. In the final price-setting stage, the seller makes a take-it-or-leave-it offer with probability $\gamma\in(0,1)$; the buyer makes the offer with probability $1-\gamma$. These are the assumptions of §2, pp. 5–9.

Under A-Learning, the buyer sends one of two costless messages before the seller chooses quality. A separating message rule sends different messages for the high and low types. On receiving message $m$, the seller believes the type is $\hat\theta(m)\in\{\theta_H,\theta_L\}$. If its belief is $\hat\theta$, the seller's expected payoff from offering quality $q$ is

$$v(q,\hat\theta)=\gamma(\hat\theta q-kq^2)-sq^2.$$

At a given quality, a buyer whose actual type is $\theta$ receives

$$u_A(\theta,\hat\theta,q)=\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}.$$

The maxima preserve the buyer's option not to purchase. In the paper's perfect Bayesian equilibrium, the seller's beliefs agree with the types that send the observed messages, the seller chooses a nonnegative quality maximizing $v$ for each message, and each type chooses a message maximizing its own payoff. With two distinct messages and a separating rule, both messages occur on the equilibrium path. These payoff and equilibrium conditions are stated in §3.2, pp. 11–12, equations (4)–(7).

Formalization targets

The seller's printed optimal design for belief $\hat\theta$ is

$$q(\hat\theta)=\frac{\gamma\hat\theta}{2s+2\gamma k}.$$

With $u(\theta,\hat\theta)=u_A(\theta,\hat\theta,q(\hat\theta))$, the two incentive compatibility conditions are $u(\theta_H,\theta_H)\geq u(\theta_H,\theta_L)$ and $u(\theta_L,\theta_L)\geq u(\theta_L,\theta_H)$. The supporting targets identify the seller's optimal design, characterize informative equilibrium by these two conditions, and express each condition as a threshold on type heterogeneity. They follow §3.2, pp. 12–13.

The goal is Proposition 1: an informative A-Learning equilibrium exists exactly when

$$\frac{\theta_H}{\theta_L}\geq\Delta:=\max\left\{\Delta_H,\Delta_L\right\},\qquad \Delta_H=\frac{\gamma[2s+(1+\gamma)k]}{(1-\gamma)(2s+\gamma k)},\qquad \Delta_L=\frac{2s+\gamma k}{\gamma k}.$$

The weak inequality includes the boundary at which a buyer is indifferent between messages. The Appendix's proof uses strict inequalities in a corresponding line; the statement on p. 13 and Proposition 1 use weak ones. The milestone list retains the source's optimal-design sentence, equations (6)–(7), and the two threshold sentences in their order in the SSRN author copy.

Significance

The theorem gives a precise answer to whether costless buyer communication can transmit preference information before a seller customizes a product. The condition separates the two possible failures of truthful reporting: a high type may prefer the design induced by the low message, and a low type may prefer the design induced by the high message. It also shows why the relevant threshold depends on bargaining power and both cost coefficients, while the prior share $\alpha$ does not enter this particular equilibrium-existence condition. The result is a theorem of the paper; the mission seeks its machine-checked formulation and proof.

The formal development makes the equilibrium claim more than a comparison of two algebraic payoffs. It must connect an actual separating message strategy, beliefs, a seller optimum, and buyer best responses to the two incentive conditions. The model's payoff definitions and equilibrium predicate are reusable for other statements about A-Learning in the paper, including comparisons of equilibrium quality and payoffs. The threshold lemmas can also be reused when comparing A-Learning with O-Learning.

Difficulty

Costless messages alone impose no truthful-reporting discipline. A seller's belief changes both the design chosen after a message and the price a buyer might face. The high and low types therefore face different deviation incentives. A comparison that ignores the seller's design decision misses the equilibrium requirement; a comparison that treats every buyer as purchasing misses the low type's option to refuse an overpriced high-quality product. The second issue is visible in the $\max\{\cdot,0\}$ terms of equation (5). The equilibrium result has to hold at equality in the thresholds as well as above them.

Formalization scope

The Lean model uses real parameters $\theta_H,\theta_L,\alpha,\gamma,k,s$ and a two-constructor type for buyer types. Its standing assumptions are exactly $\theta_H>\theta_L>0$, $0<\alpha<1$, $0<\gamma<1$, $k>0$, and $s>0$. A separate two-constructor type represents the two possible messages. Quality is real and every seller optimization ranges over $q\geq0$; optimality means that the chosen design attains the maximum. Buyer deviations range over both messages. Beliefs identify the types on the equilibrium path. The type's purchase option is kept in both maximum terms of the buyer payoff.

The price-setting stage is represented by the paper's reduced-form payoffs (4) and (5), without a separate bargaining game. The prior share $\alpha$ is retained among the standing primitives even though it cancels from Proposition 1. The closed-form design is used in $u(\theta,\hat\theta)$ and the incentive conditions, while an equilibrium requires actual seller maximization. An equilibrium is not defined as the conjunction of incentive conditions, and $\Delta$ is the printed maximum of the two explicit fractions. Separation rules out a one-message or pooling interpretation. The supporting statements require real arithmetic, optimization on a nonnegative domain, and finite case analysis for the two types and two messages. Contributions that preserve these definitions and the paper's weak boundary are welcome. The known proofs behind the milestones are in the Appendix of the SSRN version, pp. 27–28.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, author-copy version of 2023-11-29. SSRN abstract and paper. Published as a Management Science article, DOI 10.1287/mnsc.2021.04025.

Why estimate a mean with a quantum algorithm?

Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure can be run coherently as a quantum algorithm and its unitary part can also be inverted. The bounded-variance result gives an estimator whose dependence on the requested accuracy is approximately linear in $1/\epsilon$, compared with the quadratic dependence of ordinary sampling, up to logarithmic factors and the paper's model-specific operation counts. The exact asymptotic claims are in Theorem 5 of the pinned preprint, p. 12.

This mission concentrates on the probability and accuracy claim of that theorem. It includes the mean-estimation result for a nonnegative output from Lemma 4, because Algorithm 3 invokes that estimator twice after centering a general real output. The underlying amplitude-estimation theorem is a separate, already posed result, QAmpEst.Est.theorem_12; this mission uses the accuracy guarantee stated in Montanaro's Theorem 3 as the interface to that subroutine.

Outputs, truncations, and estimates

Let $X=v(\mathcal A)$ denote the real output of a quantum algorithm $\mathcal A$ under one run, and let $P$ be its probability law. The mean is $\mathbb E[X]$, and the variance is $\operatorname{Var}(X)=\mathbb E[(X-\mathbb E[X])^2]$. The result assumes a known $\sigma>0$ with $\operatorname{Var}(X)\le\sigma^2$. Although the paper describes a circuit that prepares and measures $X$, its accuracy statements depend on the distribution of $X$; the Lean interface therefore represents a run as a measurable real random variable on a probability space.

For real thresholds $a<b$, the truncation $X_{[a,b)}$ returns $X$ when $a\le X<b$ and zero otherwise. The variants $X_{<a}$ and $X_{\ge b}$ retain the output below $a$ and at or above $b$, respectively. They do not clip a value to a threshold. The $L^2$ size is $\|X\|_2=\sqrt{\mathbb E[X^2]}$. These are the output transformations defined in §2.2, p. 9, and used in Lemma 4, pp. 10–11.

Algorithm 2 estimates a nonnegative mean using the base interval $[0,1)$ and the half-open bands $[2^{\ell-1},2^\ell)$ for $1\le\ell\le k$. It sets $k=\lceil\log_2(1/\epsilon)\rceil$ and $t_0=\lceil D\sqrt{\log_2(1/\epsilon)}/\epsilon\rceil$, then adds the base estimate to $2^\ell$ times each band estimate. A successful Algorithm 1 call means that its estimate of a $[0,1]$-valued output $Y$ differs from $\mathbb E[Y]$ by at most $C(\sqrt{\mathbb E[Y]}/t+1/t^2)$, the accuracy bound of Theorem 3, pp. 8–9.

Algorithm 3 rescales $X$ by $\sigma$, draws one sample $m$ from $X/\sigma$, and centers the rescaled output at $m$. It feeds the negative and nonnegative parts, each divided by four, to Algorithm 2 at accuracy $\epsilon/(32\sigma)$ and recombines their estimates. The two calls are specified to fail with probability at most $1/9$ each; the paper describes boosting Algorithm 2's initial success probability for this use on p. 11.

Formalization targets

Lemma 4: nonnegative mean accuracy

When every Algorithm 1 call satisfies its accuracy bound and $0<\epsilon<1/2$, the output $\widetilde\mu$ of Algorithm 2 obeys

$$|\widetilde\mu-\mathbb E[X]|\le\epsilon(\|X\|_2+1)^2.$$

The constant $D>0$ is chosen once for a fixed positive universal constant $C$ from Theorem 3. It is independent of $X$ and $\epsilon$.

Theorem 5: bounded-variance accuracy

For $\operatorname{Var}(X)\le\sigma^2$, $\sigma>0$, and $0<\epsilon<4\sigma$, Algorithm 3 returns $\widehat\mu$ with

$$\Pr\bigl(|\widehat\mu-\mathbb E[X]|\le\epsilon\bigr)\ge\frac23.$$

This is the mission goal. Its probability is over the preliminary sample and both subsequent estimation runs. The milestone list follows the exact displayed statements used in Lemma 4 and the proof of Theorem 5, with their source pages.

What the result supplies

Theorem 5 turns an estimator for nonnegative outputs with finite second moment into one that handles signed outputs whose variance is bounded, without assuming a bound on the magnitude or mean of the output. That extension matters when the quantity being averaged can be negative or has a large offset: a second-moment bound on $X$ itself would then be much stronger than the paper's variance hypothesis. The stated error and success probability are the mathematical guarantee on which the paper's resource comparison rests; the comparison itself includes quantum operations absent from the measure-theoretic statement.

The formal development supplies reusable definitions of truncations, dyadic estimates, and the centered positive and negative parts, together with precisely quantified probability claims. It leaves Lemma 4 and Theorem 5 as open Lean proof targets. The amplitude-estimation statement behind Theorem 3 is already posed separately on Prove2Me, while the composed bounded-variance result and the displayed intermediate claims are the new targets here.

Where the difficulty lies

A bound for one $[0,1]$-valued call does not directly bound the mean of a signed, unbounded output. Truncating after finitely many bands leaves a tail, and the sum of errors over the retained bands can grow with their weights. The theorem must control both effects while keeping $D$ independent of the output distribution. For the signed case, the initial sample is random; its deviation, the two later failures, and the scale of the centered output all contribute to the final probability. Replacing that sample by the exact mean would remove a substantive part of the claim.

Formalization scope

Lean uses probability measures and measurable real outputs for the laws of $v(\mathcal A)$ and Algorithm 3's preliminary sample. The law of that sample is fixed to the image law of $X/\sigma$, so it cannot be selected arbitrarily. The successful-call predicate names the actual truncated outputs and the paper's $k$ and $t_0$ formulas; it does not assume Lemma 4's final error bound. The sample space carrying the later estimates is allowed to encode their joint dependence on the preliminary sample. Events are measured with extended nonnegative real values.

The $L^2$ hypotheses state that the second moment is finite. In Mathlib the real-valued variance and the integral can return a default value on a nonintegrable input, which would make a bare variance inequality or a bare $\|X\|_2$ bound misleading. The paper implicitly uses finite variance where those quantities occur. The condition $0<\epsilon$ makes the divisions and logarithms in the algorithm parameters meaningful. The natural-number expression $\ell-1$ occurs only on bands indexed by $\ell\ge1$.

The quantum circuit for Algorithm 1, the construction of an inverse unitary, and the $O(\cdot)$ copy and operation counts are outside the formal statements. Their interface is Theorem 3's numerical accuracy event. Contributions to the dyadic inequalities, the finite-variance probability bound, and their composition into the final event are in scope. The definitions are also useful for other mean estimators that split a real output into bounded pieces.

Selected references

• Ashley Montanaro, Quantum speedup of Monte Carlo methods, arXiv:1504.06987v3 [quant-ph], 2017, especially §§2.1–2.3, pp. 8–12. Pinned preprint.
• Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp, Quantum Amplitude Amplification and Estimation, Contemporary Mathematics 305, 2002. arXiv preprint.

Budget pacing in contextual auctions

Online advertising platforms sell billions of ad impressions a day, mostly by auction, to advertisers who care about the features of the impression (the user, the page, the time) and who spend under a budget fixed in advance. To keep spending within budget, platforms and advertisers use pacing: every value is multiplied by a factor smaller than one, so that the buyer bids less aggressively and spreads its budget over the whole campaign. Balseiro, Kroer and Kumar (2023) study the equilibria that pacing produces when items carry feature vectors and buyers' values are linear in them. They prove that a pacing-based equilibrium exists in the first price auction (Theorem 1), that the same pacing is an equilibrium of every standard auction with the same expected payments (Theorem 2), and that its liquid welfare is at least half the optimum (Theorem 3).

This mission concerns §6, Structural Properties, of that paper: what the equilibrium pacing multipliers look like as a function of the buyer's type. Its goal, Proposition 3, says that buyers who share a budget and whose weight vectors point in the same direction are paced down to one common weight vector. It is the qualitative statement behind a practical observation: scaling up the targeting weights of a budget-constrained advertiser without raising its budget does not change the outcome.

Setting

An item has a context $\alpha \in A \subset \mathbb{R}^d_+$, drawn from a law $F$ with a density. There are $n$ buyers; each has a type $(w, B)$ consisting of a weight vector $w \in \mathbb{R}^d$ and a budget $B$, drawn independently from a law $G$ with a density on

$$\Theta = (0, U)^d \times (B_{\min}, U).$$

The value of type $(w,B)$ for item $\alpha$ is $w^{\top}\alpha$, and $\omega = \sup_{(w,B)\in\Theta,\ \alpha\in A} w^{\top}\alpha$. The item is sold by first price auction with reserve price $r(\alpha)$, and every buyer must respect its budget in expectation over the context and the other buyers' types.

A pacing function $\mu : \Theta \to \mathbb{R}_{\ge 0}$ shades the value of type $(w,B)$ to the paced value $w^{\top}\alpha/(1+\mu(w,B))$, equivalently replaces $w$ by the paced weight vector $w/(1+\mu(w,B))$. Let $H^\mu_\alpha$ be the distribution function of the highest of $n-1$ independent paced values. The value pacing–based strategy bids $\beta^\mu(w,B,\alpha) = \sigma^\mu_\alpha(w^{\top}\alpha/(1+\mu(w,B)))$, where

$$\sigma^\mu_\alpha(x) = x - \int_{r(\alpha)}^{x} \frac{H^\mu_\alpha(s)}{H^\mu_\alpha(x)}\,ds \qquad (x \ge r(\alpha)),$$

with $\sigma^\mu_\alpha(x) = 0$ when $H^\mu_\alpha(x) = 0$ and $\sigma^\mu_\alpha(x) = x$ below the reserve. A buyer of type $(w,B)$ facing competitors who bid $\beta^\mu$ has the dual function

$$q^\mu(w,B,t) = \sup_{b}\ \mathbb{E}\Big[\big(w^{\top}\alpha - (1+t)\,b(\alpha)\big)\,\mathbf 1\{b(\alpha) \ge \max(r(\alpha),\{\beta^\mu(\theta_i,\alpha)\}_i)\}\Big] + tB,$$

the supremum over bid functions $b \ge 0$; $t$ is the Lagrange multiplier of its budget constraint.

§6 assumptions. Reserve prices are zero; the support $\delta(G)$ of $G$ is convex and compact; and $\mu$ takes values in $[0, \omega/B_{\min}]$ with

$$\mu(w,B) = \operatorname*{arg\,min}_{t \in [0,\omega/B_{\min}]} q^\mu(w,B,t) \quad \text{for all } (w,B) \in \delta(G),$$

the minimizer being unique. This is uniqueness of the best response, not of the equilibrium. A type with $\mu(w,B) = 0$ is unpaced, and paced otherwise. Norms are Euclidean.

Formalization targets

Goal: Proposition 3 (p. 14)

Let $\hat w \in \mathbb{R}^d_+$ be a unit vector and $B > 0$ such that $w/\|w\| = \hat w$ for some $(w,B) \in \delta(G)$.

1. If $(w_1,B),(w_2,B) \in \delta(G)$, $w_1/\|w_1\| = w_2/\|w_2\| = \hat w$ and $\mu(w_1,B),\mu(w_2,B) > 0$, then

$$\frac{w_1}{1+\mu(w_1,B)} = \frac{w_2}{1+\mu(w_2,B)}.$$

2. If some $(w,B)\in\delta(G)$ on the ray is unpaced, let $w_0$ be the largest unpaced weight vector along $\hat w$ with budget $B$. Then $w/(1+\mu(w,B)) = w_0$ for every paced $(w,B) \in \delta(G)$ on the ray.

Milestones (p. 14)

• Monotonicity. Under a unique best response, $\mu(w,B)$ is nondecreasing in each component of $w$ and nonincreasing in $B$ (a consequence of the paper's Lemma 2).
• Continuity. Under a unique best response, $\mu$ is continuous (Lemma 14 of the online appendix).

Significance

Proposition 3 describes equilibrium pacing along each direction of weight space as a single threshold. Along a ray $\{c\,\hat w\}$ with budget $B$, buyers below a critical scale do not exhaust their budget and are unpaced; every buyer above it is paced down to the critical type, which spends its budget exactly. Equilibrium paced values, hence allocations and payments, are therefore constant above the threshold. By the paper's revenue equivalence result the same description holds for the pacing equilibria of all standard auctions, which makes it a statement about budget-constrained advertisers in general, not about one auction format.

The result is proved in the paper, with all proofs in its online appendix; the appendix is not part of the source this mission cites. No part of it has been machine-checked. The mission formalizes the statement on top of a from-scratch model of contextual budget-constrained first price auctions (types, pacing, the bidding function $\sigma^\mu_\alpha$, the buyer's dual function), which is shared with the other missions of this series.

Difficulty

The dual function $q^\mu$ is a supremum over bid functions in which the competitors' bids themselves depend on $\mu$, so the equilibrium condition is a fixed point: $\mu$ appears both inside the objective and as its minimizer. Comparing two buyers on the same ray requires relating their dual problems, and a buyer with weight vector $c\,w$ does not simply face a rescaled problem, because the budget $B$ does not scale with $c$. Part 2 requires in addition that the largest unpaced buyer exists, which needs continuity of $\mu$ on the support; continuity of an argmin requires uniqueness of the minimizer and continuity of $q^\mu$ in the type and the multiplier jointly. The monotonicity statement is a comparative-statics argument for a family of minimization problems parameterized by the type.

Formalization scope

Types are pairs (w, B) : (Fin d → ℝ) × ℝ, values are the explicit sums $\sum_i w_i\alpha_i$, and the Euclidean norm is written as $\big(\sum_i w_i^2\big)^{1/2}$, never Lean's sup norm on Fin d → ℝ. $\delta(G)$ is Mathlib's Measure.support. The expectation is over the product of $F$ and $n-1$ copies of $G$; ties win, as in the paper's tie-breaking rule. Bids are measurable, nonnegative and have an integrable payment, and $q^\mu$ is defined as the supremum over such bids (p. 7), not by its closed form. $\sigma^\mu_\alpha$ is defined by an explicit case split so that the case $H^\mu_\alpha(x) = 0$ gives $0$.

Standing assumptions: $d \ge 2$; $U, B_{\min} > 0$; $A$ measurable inside the strictly positive orthant; $F$ and $G$ probability measures with densities, $F(A) = 1$, $G(\Theta) = 1$; $r$ measurable; and the §6 assumptions above, with the unique best response stated as membership, minimality and uniqueness over $[0,\omega/B_{\min}]$. Disclosed additions: $n \ge 2$; $B_{\min} < U$; $A$ nonempty and bounded (so that $\omega$ is finite); $\delta(G) \subseteq \Theta$, since $\mu$ is defined on $\Theta$ and is evaluated on $\delta(G)$. The maximization set of part 2 is read inside $\delta(G)$ with the budget fixed, and the existence of the maximizer $w_0$ is part of the conclusion, so the statement is not vacuously true when no maximizer exists. The milestones are posed on $\delta(G)$, where uniqueness is assumed.

The development needs the support of a measure, argmin continuity (a maximum theorem for a unique minimizer), and comparative statics of parametric minimization; the auction model is reusable by the other missions of the series. Contributions of supporting lemmas on $q^\mu$ (its convexity in $(w,t)$, continuity, the closed form of p. 8) are welcome.

Selected references

• S. R. Balseiro, C. Kroer, R. Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees, Management Science, Articles in Advance, 2023. https://doi.org/10.1287/mnsc.2023.4719

Motivation

The stochastic block model (SBM) is the standard benchmark for community detection: a random graph whose vertices are split into hidden communities, with denser connections inside a community than across. For two equal communities, the best possible estimator of the hidden partition is the minimum bisection problem, which is NP-hard in the worst case. Its tractable relaxations are therefore compared by asking for which edge densities they still recover the hidden partition exactly.

For semidefinite programming the answer is complete in the logarithmic-degree regime: Abbe, Bandeira and Hall (arXiv:1405.3267) located the information-theoretic threshold $\sqrt\alpha-\sqrt\beta=\sqrt2$, and the SDP relaxation was shown to reach it by Hajek, Wu and Xu (arXiv:1412.6156) and by Bandeira (arXiv:1504.03987). Linear programming relaxations are cheaper and widely used in combinatorial optimization, but their behaviour on the SBM was not known. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research, 2023) study the most common one, the metric relaxation. This mission formalizes their result for the logarithmic-degree regime (Theorem 8): there the LP relaxation fails to recover the hidden partition with high probability, at every choice of the parameters.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\sqcup V_2$ with $|V_1|=|V_2|=n/2$; its cost in a graph $G$ is the number of edges between $V_1$ and $V_2$. Given a fixed planted bisection $V_1,V_2$, an optimization problem recovers it if its unique optimal solution corresponds to $V_1,V_2$.

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of $V_1,V_2$ has $\bar x_{ij}=1$ exactly when $i,j$ lie on different sides. With $a_{ij}=1$ for edges and $0$ otherwise, the metric relaxation is

$$\text{(LP-P)}\quad \min_x \sum_{i<j}a_{ij}x_{ij}\ \ \text{s.t.}\ \ x_{ij}\le x_{ik}+x_{jk},\ \ x_{ij}+x_{ik}+x_{jk}\le2,\ \ \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first family over distinct $i,j,k$ and the second over $i<j<k$, with $x_{ji}:=x_{ij}$. Every bisection's cut vector is feasible.

The distance $\rho_G(i,j)$ is the length of a shortest $i$–$j$ path ($+\infty$ across components). The diameter is $\rho_{\max}(G)=\max_{i,j}\rho_G(i,j)$ and the average distance is $\rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{i<j}\rho_G(i,j)$.

The Erdős–Rényi model $\mathcal G_{n,p}$ draws each edge independently with probability $p$. The SBM $\mathcal G_{n,p,q}$ chooses a bisection $V_1,V_2$ uniformly at random, then draws each pair inside a side with probability $p$ and each pair across with probability $q$, independently, where $p>q$. The logarithmic-degree regime (21) is

$$p=\alpha\frac{\log n}{n},\qquad q=\beta\frac{\log n}{n},\qquad \alpha>\beta>0 .$$

An event $A_n$ holds with high probability if $\mathbb P[A_n]\to1$ as $n\to\infty$.

Formalization targets

Goal: Theorem 8 (p. 18)

$$\alpha>\beta>0\ \Longrightarrow\ \lim_{n\to\infty}\mathbb P_{\mathcal G_{n,p,q}}\big[\text{(LP-P) does not recover }V_1,V_2\big]=1 .$$

Milestones

1. The threshold of [2] (p. 14, strict cases): if $\sqrt\alpha-\sqrt\beta>\sqrt2$, the minimum bisection problem recovers $V_1,V_2$ with high probability; if $\sqrt\alpha-\sqrt\beta<\sqrt2$, it does not.
2. Proposition 13 (p. 29): for $\alpha>1$ and $G\sim\mathcal G_{n,\alpha\log n/n}$, $\rho_{\max}(G)\in\big((1-\epsilon)\frac{\log n}{\log\log n},(1+\epsilon)\frac{\log n}{\log\log n}\big)$ with high probability.
3. Proposition 15 (p. 29, Theorem 1 of Chung–Lu): for $\alpha>1$, $\rho_{\mathrm{avg}}(G)\in\big((1-\epsilon)\frac{\log n}{\log pn},(1+\epsilon)\frac{\log n}{\log pn}\big)$ with high probability.
4. Proposition 19 (p. 30): for $\alpha>\beta>0$ with $\frac{\alpha+\beta}{2}>1$ and $G\sim\mathcal G_{n,p,q}$,

$$(1-\epsilon)\frac{\log n}{\log\log n}\le\rho_{\mathrm{avg}}(G)\le\rho_{\max}(G)\le(1+\epsilon)\frac{\log n}{\log\log n}$$

with high probability.

Two results the proof of Theorem 8 uses are posed in sibling missions of this series and are not restated here: Theorem 5 (a distance-based non-recovery criterion for (LP-P), mission 4) and the coupling Proposition 11 together with the crossing-edge count (26) (mission 6).

Significance

The result. Theorem 8 separates linear from semidefinite programming on a natural statistical problem. In the logarithmic regime the SDP relaxation recovers the planted bisection whenever any method can, while the metric LP fails with high probability for all $\alpha>\beta>0$, including parameters far above the information-theoretic threshold. The paper's Theorem 6 shows that in the very dense regime (constant $p,q$) the LP does succeed when $p-q>1/2$; Theorem 8 shows that at logarithmic degree no such window exists.

Formalizing it. The theorem is proved in the paper, modulo results cited from the random-graph literature. Nothing in this mission is machine-checked yet. Formalization adds a precise account of what the cited distance asymptotics assert; Proposition 19's upper bound is justified in the paper only by reference to "a standard result on the diameter of the SBM" obtained by adapting an argument of Abbe's survey, so a complete proof of it is new work. Propositions 13 and 15 are classical facts about Erdős–Rényi graphs that have no formal proof in any library known to the curators, and are reusable well beyond community detection.

Difficulty

The LP side of the argument is deterministic and finite. The difficulty is probabilistic. The distance results require tight control of breadth-first neighbourhood growth in sparse random graphs near the connectivity threshold, where the average degree is only logarithmic, with error terms small enough to pin the diameter to a $(1\pm\epsilon)$ window. A first-moment estimate of path counts gives only one side of each bound. In the SBM the two edge probabilities make neighbourhood growth inhomogeneous, so the Erdős–Rényi results do not transfer verbatim. The threshold of [2] is a separate sharp large-deviation statement, at the level of individual vertices' in- and out-degrees.

Formalization scope

Vertices are Fin n (0-based); graphs are SimpleGraph (Fin n). A bisection is recorded by its side $V_1$ with $2|V_1|=n$. The LP variable is a symmetric, zero-diagonal array $x:V\times V\to\mathbb R$, which is a point of $\mathbb R^{\binom n2}$; no box constraints are added. LP recovery means that the planted cut vector is the unique optimal solution; minimum-bisection recovery means that every bisection of cost at most the planted one is the planted unordered partition. Distances are in $\mathbb N\cup\{\infty\}$ and the average distance in $[0,\infty]$, so a disconnected sample has infinite diameter. The random-graph laws are finite sums over all graphs; the SBM averages over all bisections. Edge probabilities are clamped into $[0,1]$, which matters only for the finitely many $n$ with $\alpha\log n/n>1$. "With high probability" is a limit of probabilities equal to $1$; for the SBM the limit runs along $n=2m$. Logarithms are natural.

Disclosed choices relative to the printed statements: Theorem 8 prints only $\alpha,\beta>0$, and $\alpha>\beta$ is added as the SBM's standing assumption $p>q$ (p. 13) and that of (21). The threshold of [2] is printed as an "if and only if"; only the two strict implications are posed, and the boundary $\sqrt\alpha-\sqrt\beta=\sqrt2$ is left out.

The statements cannot be satisfied vacuously: the laws are genuine probability distributions for every $n$, the events compare extended-valued distances without truncation, and recovery requires uniqueness over all real feasible points of (LP-P). An encoding with an empty or degenerate feasible set, or with distances truncated to finite reals, would change the theorems and is excluded.

A complete development needs: Erdős–Rényi and SBM laws, breadth-first exploration bounds for sparse random graphs, the coupling of the SBM between two Erdős–Rényi graphs (mission 6), the LP non-recovery criterion (mission 4), and the information-theoretic threshold of [2]. Contributions on the random-graph distance asymptotics are reusable on their own and especially welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023. https://arxiv.org/abs/2006.03213 (v2 is the cited version)
• E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Transactions on Information Theory 62:471–487, 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community detection and stochastic block models: recent developments, Journal of Machine Learning Research 18:1–86, 2018. https://arxiv.org/abs/1703.10146
• F. Chung, L. Lu, The diameter of sparse random graphs, Advances in Applied Mathematics 26(4):257–279, 2001. https://doi.org/10.1006/aama.2001.0720
• F. Chung, L. Lu, The average distances in random graphs with given expected degrees, PNAS 99(25):15879–15882, 2002. https://doi.org/10.1073/pnas.252631999
• B. Hajek, Y. Wu, J. Xu, Achieving exact cluster recovery threshold via semidefinite programming, IEEE Transactions on Information Theory 62(5):2788–2797, 2016. https://arxiv.org/abs/1412.6156
• A. S. Bandeira, Random Laplacian matrices and convex relaxations, Foundations of Computational Mathematics 18(2):345–379, 2018. https://arxiv.org/abs/1504.03987

Motivation

In auctions with interdependent values, the value an agent assigns to an outcome depends not only on her own private information but on the information of the others: a bidder for drilling rights values a tract according to every bidder's geological survey, and a buyer of a used asset values it according to every inspector's report. Each agent observes only her own signal, while the mechanism designer knows how values depend on the full signal profile. Maximizing welfare truthfully is then much harder than with private values: the VCG mechanism no longer applies, and without structural assumptions on the valuations no ex-post truthful mechanism gives a good approximation of the optimal welfare (the source's Examples 1.2–1.3).

Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384) identify submodularity over signals (SOS) as a condition under which constant or near-constant approximations become possible, including for combinatorial auctions, where agents value bundles of items. For single-dimensional signals that take $k$ values, they give a $(k+3)$-approximation under SOS (Theorem 6.1) and, under the stronger condition strong-SOS, a $(2\log_2 k+4)$-approximation (Theorem 6.5). This mission formalizes the second result.

Timeline. Milgrom and Weber (1982) introduced the interdependent value model for auctions; Dasgupta and Maskin (2000) studied efficient auctions under the single-crossing condition. The computer science literature then gave approximation results for simple single-parameter settings (mostly single-item auctions or matroid constraints), again largely under single crossing or its variants, e.g. Roughgarden and Talgam-Cohen (2016) and Eden, Feldman, Fiat and Goldner (2018), as surveyed in the source. The SOS paper (arXiv v2, 2019; journal version in Mathematics of Operations Research, 2024) drops single crossing and gives, in its own words, the first welfare approximation guarantees for multi-dimensional combinatorial auctions with interdependent values.

Setting

There are $n$ agents and $m$ items. Agent $i$ holds a signal $s_i\in\{0,1,\dots,k-1\}$, and $\mathbf s=(s_1,\dots,s_n)$ is the signal profile. For every bundle $T\subseteq[m]$, agent $i$'s value is $v_{iT}(\mathbf s)\ge0$, with $v_{i\emptyset}=0$; for nonempty $T$ it is weakly increasing in every signal and strictly increasing in $s_i$.

A function $w$ of the profile is strong-SOS if for every coordinate $j$, every $\delta\ge0$ and profiles $\mathbf s'\le\mathbf s$ coordinate-wise,

$$w(\mathbf s_{-j},s_j+\delta)-w(\mathbf s)\;\le\;w(\mathbf s'_{-j},s'_j+\delta)-w(\mathbf s').$$

Raising one signal helps less the higher the profile, including the raised coordinate itself; in particular the effect of an agent's own signal is concave. SOS asks this only when the raised coordinate starts from the same value in both profiles.

An allocation $T=(T_1,\dots,T_n)$ gives pairwise disjoint bundles. A deterministic mechanism maps reported signals to an allocation and payments; it is ex-post IC if, whatever the true signals and with the others truthful, no agent gains by misreporting, and ex-post IR if truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

Let $k=2^q$. Random Bucket picks $\ell\in\{1,\dots,\log_2 k\}$ uniformly, calls $N_{B_\ell}=\{i:s_i\ge2^{\ell-1}\}$ the high agents, and allocates to them a bundle assignment maximizing $\sum_{i\in N_{B_\ell}}v_{iS_i}(\mathbf s_{N_{\neg B_\ell}},\mathbf{2^{\ell-1}}_{N_{B_\ell}})$, the values with every high signal lowered to $2^{\ell-1}$; agent $i$ receiving $\bar T_i$ pays $v_{i\bar T_i}(\mathbf s_{-i},2^{\ell-1}-1)$. Random Sampling splits the agents uniformly at random into $A$ and $B$, allocates to $B$ a bundle assignment maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$, and charges nothing. k-SS runs Random Bucket with probability $p_{RB}=\frac{\log_2 k}{\log_2 k+2}$ and Random Sampling otherwise.

Formalization targets

Goal: Theorem 6.5

For strong-SOS valuations, k-SS is universally ex-post IC-IR and, for every grid profile $\mathbf s$ and every feasible allocation $T^*$,

$$\sum_i v_{iT^*_i}(\mathbf s)\;\le\;(2\log_2 k+4)\;\mathbb E\big[\text{welfare of k-SS at }\mathbf s\big].$$

Milestones

1. Strong-SOS implies SOS (p. 19).
2. Display (9), corrected: with $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$,

$$\mathsf{SELF}\le 2\sum_{\ell=1}^{\log_2 k}\sum_{i:2^{\ell-1}\le s_i<2^\ell}v_{iT_i}(\mathbf 0_{-i},2^{\ell-1}_i).$$

3. Lemma 6.4: Random Bucket is ex-post IC-IR and $\mathsf{SELF}\le 2\log_2 k\cdot\mathbb E[\text{welfare of Random Bucket}]$.
4. The combination: $\mathsf{SELF}+\mathsf{OTHER}\le(2\log_2 k+4)\,\mathbb E[\text{welfare of k-SS}]$, where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$.

Significance

The theorem shows that the price of truthfulness in combinatorial auctions with interdependent values grows only logarithmically in the number of signal values once values are concave in the agents' own signals, compared with the linear $(k+3)$ of the SOS mechanism. It also exhibits a decomposition of optimal welfare into a part driven by the other agents' signals (OTHER) and a part driven by the agent's own signal (SELF), each covered by a different randomized mechanism; this template recurs in later work on interdependent values.

The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact model behind a proof that is stated in a few lines and checks it against the paper's own appendix: the printed display (9) omits a factor 2 (it fails for one agent with $v(\mathbf s)=s_1$, $k=4$, $s_1=3$), and the mission states the corrected inequality, which is the $d=1$ case of the paper's display (12) and is what the ratio $2\log_2 k$ requires.

Difficulty

The obvious route compares the mechanism's allocation with the optimal one agent by agent, but the mechanisms allocate by proxy values computed from modified signal profiles, and the optimal allocation's value at the true profile is not directly comparable with any single proxy. Covering SELF requires bounding an agent's own-signal contribution within a bucket by its value at the bucket floor, which needs concavity in the own signal and is false under SOS alone. Covering OTHER requires the Key Lemma 3.1 on random zeroing of signals. Incentive compatibility needs the argmax to be read off the proxy profile alone; an argmax with tie-breaking on the full report fails it.

Formalization scope

Signals are natural numbers and every hypothesis (nonnegativity, monotonicity, SOS, strong-SOS, the selectors' optimality) is quantified over the grid $\{0,\dots,k-1\}^n$ only. $k=2^q$ with $\log_2 k=q$ is a disclosed reading: the buckets cover $\{1,\dots,k-1\}$ only for powers of two. The empty bundle is worth $0$, and the monotonicity clauses apply to nonempty bundles. The argmax of each mechanism is an arbitrary selector that sees only the bucket index (or $B$) and the proxy profile and returns a feasible maximizer; theorems quantify over all such selectors. Random Sampling zeroes all of $B$, the agent's own signal included (the paper's "$v_{ij}$" is read as $v_{iT}$). Expectations are finite uniform averages; at $q=0$ Lean's $0^{-1}=0$ makes the Random Bucket term vanish, matching $p_{RB}=0$.

The approximation is stated for every feasible allocation and with true values at the truthful profile, not with proxy values or a supremum; IC and IR are stated for each deterministic component, not for the mixture's expectation. Replacing the average over partitions by an existential, or the explicit payments by existence of payments, would not be this theorem.

The model layer (signal grid, combinatorial valuations, SOS, ex-post IC-IR, OTHER and SELF, Random Sampling) is shared with the companion missions and lives in InterdepSOS.KHL and InterdepSOS.RSV; strong-SOS, Random Bucket and k-SS are defined in InterdepSOS.KSS. Lemma 6.3 and the decomposition (7), which the proof uses, are posed in the companion mission on k-HL. Proofs of the milestones, and reusable lemmas on concavity in the own signal and on random zeroing, are welcome. The source is the arXiv v2 preprint; the journal version in Mathematics of Operations Research (2024) is not what the mission cites.

Selected references

• A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
• P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
• P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737

Motivation

The minimum bisection problem asks, for a graph on an even number $n$ of vertices, for a split of the vertices into two halves that cuts as few edges as possible. It is NP-hard, and it is the maximum a posteriori estimator for the two-community stochastic block model (SBM), the standard benchmark for community detection (Abbe, 2018). Convex relaxations are the usual way to make such estimators tractable while keeping guarantees. For the semidefinite relaxation, exact-recovery thresholds are known (Abbe, Bandeira, Hall, 2016; Hajek, Wu, Xu, 2016). Linear programming relaxations are cheaper and much used in combinatorial optimization, but their recovery properties were not understood.

Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research, 2023) study the best-known LP relaxation of minimum bisection, the metric relaxation. They give a sufficient condition for it to recover a planted bisection (Theorem 4) and a necessary one (Theorem 5). This mission formalizes the necessary condition. Its consequence, developed in §4 of the paper, is that the metric relaxation fails with high probability in most SBM regimes, including those where the minimum bisection itself succeeds.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,n\}$, and write $(i,j)$ for an edge with $i<j$; set $a_{ij}=1$ if $(i,j)\in E$ and $a_{ij}=0$ otherwise. A bisection is a partition of $V$ into two sets $V_1,V_2$ with $|V_1|=|V_2|=n/2$. One fixed bisection, unknown to the solver, is the planted bisection; $E_0$ is the set of edges with one end in $V_1$ and the other in $V_2$.

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of the planted bisection has $\bar x_{ij}=1$ exactly when $i$ and $j$ lie on different sides. The metric relaxation is the linear program, with $x_{ji}:=x_{ij}$,

$$\min_x\ \sum_{1\le i<j\le n}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk}\ (1),\qquad x_{ij}+x_{ik}+x_{jk}\le 2\ (2),\qquad \sum_{1\le i<j\le n}x_{ij}=\frac{n^2}{4}\ (3),$$

where (1) ranges over distinct $i,j,k$ with $i<j$ and (2) over $i<j<k$. The LP recovers the planted bisection if $\bar x$ is its unique optimal solution. The objective at $\bar x$ is $|E_0|$.

The graph distance $\rho_G(i,j)$ is the length of a shortest $i$–$j$ path ($+\infty$ across components). The diameter and the average distance are

$$\rho_{\max}(G)=\max_{i,j\in V}\rho_G(i,j),\qquad \rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{1\le i<j\le n}\rho_G(i,j).$$

The average is over all $n^2$ ordered pairs, the diagonal included. For $n\ge5$ define

$$c(G)=\max\Big\{0,\ \frac{3\rho_{\max}(G)-4\rho_{\mathrm{avg}}(G)}{1-4/n}\Big\}.\qquad(17)$$

Formalization targets

Goal: Theorem 5

For a connected graph $G$ on $n\ge5$ nodes with a planted bisection,

$$\frac{1+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}\,|E|<|E_0|\quad(18)\qquad\Longrightarrow\qquad\text{(LP-P) does not recover the planted bisection.}$$

Milestones

The proof of Theorem 5 works with the point $\tilde x\in\mathbb R^{\binom n2}$,

$$\tilde x_{ij}=\frac{\rho_G(i,j)+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}.$$

The mission poses three statements about it, for a connected $G$ on $n\ge5$ nodes:

1. display (19), p. 12: for $i<j<k$, $\displaystyle\tilde x_{ij}+\tilde x_{ik}+\tilde x_{jk}\le\frac32\cdot\frac{\rho_{\max}(G)+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}$;
2. p. 13: $\tilde x$ is feasible for (LP-P);
3. p. 13: the objective of (LP-P) at $\tilde x$ equals $\displaystyle\frac{1+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}\cdot\frac{|E|}{2}$.

Significance

The result. Theorem 5 is a deterministic certificate of failure, stated for any connected graph, not for a random model. It reduces the question "does the LP recover?" to comparing two numbers that depend only on the distance profile of $G$ and on the fraction of edges cut by the planted bisection. When typical distances are close to the diameter, $c(G)$ is small and (18) asks only that $|E_0|/|E|$ exceed roughly $1/(2\rho_{\mathrm{avg}}(G))$. In random graphs typical distances are close to the diameter. The paper's Theorems 7 and 8 combine Theorem 5 with known distance asymptotics of Erdős–Rényi graphs (Bollobás, Random Graphs, 2001; Chung, Lu, 2001). They show that the metric relaxation fails with high probability in the dense and logarithmic-degree SBM, in contrast with the semidefinite relaxation. Those theorems are separate missions of this series and use Theorem 5 as a black box.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces a formal metric relaxation of minimum bisection, with LP recovery defined as uniqueness of the optimum, and links it to graph distances through Mathlib's SimpleGraph.edist/ediam. The definitions are written to coincide with those of the other missions of this series, so that one model layer serves the sufficient condition (Theorem 4), the necessary condition (this mission), and the random-graph consequences.

Difficulty

Theorem 5 is not deep, but it is exact. The milestones fix the witness $\tilde x$; the work is in checking it. The obvious candidate, the graph metric $\rho_G$ itself rescaled to satisfy the equality (3), satisfies the triangle inequalities (1). It can violate the perimeter constraints (2) whenever some triangle of vertices is spread out compared with the average distance. The shift by $c(G)$, which depends on $\rho_{\max}$ and on the factor $1-4/n$, is tuned so that (2) holds with no slack in the worst case. A proof has to keep track of the normalization $2/n^2$ (ordered pairs, diagonal included), the factor $1-1/n$, and the sign of $3\rho_{\max}-4\rho_{\mathrm{avg}}$, and must use $n\ge5$ wherever it divides by $1-4/n$. In Lean the further work is converting between sums over ordered pairs, unordered pairs and the edge set, and between extended-valued distances and their real values for a connected graph.

Formalization scope

• Vertices and bisections. Vertices are Fin n (0-based). The planted bisection is a finset $V_1$ with $2|V_1|=n$, and $V_2=V_1^{c}$. $|E_0|$ is the number of pairs $i<j$ adjacent in $G$ and on different sides.
• LP variables. A point of $\mathbb R^{\binom n2}$ is an array $x:\texttt{Fin } n\to\texttt{Fin } n\to\mathbb R$. Feasibility includes symmetry and a zero diagonal, so the free diagonal and lower-triangle entries cannot break uniqueness of the optimum. No bounds $0\le x\le1$ are added; they are not constraints of (LP-P).
• Recovery. LPRecovers G V1 says that the cut vector of $V_1$ is optimal and every optimal point equals it.
• Distances. $\rho_G$ is SimpleGraph.edist (in $\mathbb N\cup\{\infty\}$), $\rho_{\max}$ is SimpleGraph.ediam, and $\rho_{\mathrm{avg}}$ is the printed formula computed in $[0,\infty]$. $c(G)$ and $\tilde x$ use their real values. All statements assume $G$ connected, where these values are finite and $\rho_{\mathrm{avg}}(G)>0$.
• Standing hypotheses. Every statement carries exactly the page's hypotheses: $G$ connected and $n\ge5$, plus, for Theorem 5, the planted bisection. The bisection forces $n$ even, so in effect $n\ge6$; $n\ge5$ is kept as printed. $\tilde x$ is indexed by $i<j$ on the page and is extended symmetrically with zero diagonal.
• Ruled out. A formalization that adds box constraints, drops the symmetric zero-diagonal normalization, averages over $n(n-1)/2$ pairs instead of the printed $2/n^2$, or omits connectivity (where the real value of an infinite distance would be $0$) states a different theorem. None of these is used here.

Contributions welcome: proofs of the three milestones and the goal. Reusable lemmas include the identity $\sum_{i<j}a_{ij}x_{ij}=\sum_{(i,j)\in E}x_{ij}$ for SimpleGraph.edgeFinset, the finiteness of ediam for connected graphs on Fin n, and the bound $\rho_{\mathrm{avg}}(G)\le(1-\frac1n)\rho_{\max}(G)$.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2 (2022). https://arxiv.org/abs/2006.03213
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18 (2018). https://arxiv.org/abs/1703.10146
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1405.3267
• B. Hajek, Y. Wu, J. Xu, Achieving Exact Cluster Recovery Threshold via Semidefinite Programming, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1412.6156
• B. Bollobás, Random Graphs, 2nd ed., Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511814068
• F. Chung, L. Lu, The Diameter of Sparse Random Graphs, Advances in Applied Mathematics 26 (2001). https://doi.org/10.1006/aama.2001.0720