Optimization

Motivation

Online marketplaces match buyers with sellers and charge a fee per transaction. Once a buyer has found a seller on the platform, both have an incentive to complete the sale off the platform and split the fee they save. This leakage (also called disintermediation) is a central concern for service marketplaces such as Upwork, Thumbtack or AngelList, and several of them respond by hiding the identity of the parties and blocking direct messages until a transaction is committed.

A. Hagiu and J. Wright, Marketplace Leakage (Management Science, 2023; doi:10.1287/mnsc.2023.4757), build a model of a marketplace that cannot prevent leakage by contract and study six strategies against it. Section 5.2 studies the bluntest of them: banning buyer–seller communication. A ban stops leakage, but it also prevents buyers from learning whether the product suits them. Proposition 3 says exactly when the marketplace gains from the ban. This mission formalizes that proposition and the lemmas of its proof (Appendix §8.4).

Setting

There is one marketplace $M$, one seller $S$ and a unit mass of buyers with unit demand. The product has value $v$ for buyers who want it and marginal cost $c<v$; the outside option is worth $0$.

Allowing communication (the baseline). $M$ sets a fee $f$ per transaction. $S$ sets the on-platform price $p_m=v$ and a direct price $p_d\le v$. A buyer who buys directly bears a switching cost $s$ with distribution $G$; with the uniform distribution of the paper,

$$G(s)=\min\{\max\{s/\mu,0\},1\},\qquad \mu>0 .$$

The seller maximizes its profit (1),

$$\pi(p_d)=(p_d-c)\,G(v-p_d)+(v-c-f)\,\bigl(1-G(v-p_d)\bigr),$$

and $M$ earns $f\,(1-G(v-p_d))$, choosing $f\le v-c$. The equilibrium profit of $M$ is $\Pi^*$. With communication allowed, a buyer values the product at $v$ only with probability $q\in(0,1)$, but learns their valuation; every payoff is multiplied by $q$, so $M$ earns $q\Pi^*$.

Banning communication. Under a ban there is no leakage, but a buyer learns their valuation only with probability $\eta\in[0,1]$. Facing the fee $f$, the seller has two options: the high price $p_m=v$, selling to the fraction $\eta q$ of informed high-value buyers and earning $\eta q\,(v-c-f)$; and the low price $p_m=qv$, selling also to the $1-\eta$ uninformed buyers and earning $(1-\eta+\eta q)(qv-c-f)$. It takes the better option (ties to the low price) and lists if that option pays at least $0$. $M$ earns $f$ per transaction and chooses $f\in\mathbb R$. Its maximal revenue is the ban value $V(\eta)$. Two closed forms appear:

$$\Pi_H(\eta)=\eta q(v-c),\qquad \Pi_L(\eta)=(1-\eta+\eta q)\Bigl(\frac{(1-(2-q)\eta)qv}{1-\eta}-c\Bigr).$$

$M$ prefers to ban if $V(\eta)>q\Pi^*$ and prefers to allow if $V(\eta)<q\Pi^*$.

Formalization targets

Goal: Proposition 3 (pp. 15–16)

For $0<\Pi^*<v-c$:

1. $M$ prefers to ban for every $\eta$ with $\Pi^*/(v-c)<\eta\le 1$;
2. if $q>c/(v-\Pi^*)$, there is a unique $\eta_L\in[0,1)$ with $\Pi_L(\eta_L)=q\Pi^*$, it is positive, and $M$ prefers to ban for every $\eta\in[0,\eta_L)$;
3. there is $q_0<1$ such that for $q\in(q_0,1)$, $M$ prefers to ban for every $\eta\in[0,1]$;
4. with uniform switching costs, $c\ge 0$, and $\Pi^*=\Pi^*(\mu)$ the baseline equilibrium profit: for each $\eta\in(0,1)$, $M$ prefers to ban for all sufficiently small $\mu>0$ and prefers to allow for all sufficiently large $\mu$.

Milestones

$$f>\frac{(1-(2-q)\eta)qv}{1-\eta}-c\iff \text{the seller prefers the high price}\qquad(\text{p. 15})$$ $$V(\eta)=\max\{\Pi_H(\eta),\Pi_L(\eta)\}\qquad(\text{p. 15})$$ $$\frac{d\Pi_L}{d\eta}=-\frac{(1-q)qv}{(1-\eta)^2}\bigl((2-\eta)q\eta+2(1-\eta)^2\bigr)+c(1-q)<0\ \text{ when } qv>c\qquad(\text{p. 38})$$ $$\Pi_L(\eta)\le\Pi_H(\eta)\iff\eta\ge\eta^*,\quad \eta^*=\frac{qv(2-q)-c-q\sqrt{(1-q)v(v-c)}}{qv(3(1-q)+q^2)-c}\in(0,1)\qquad(\text{p. 38})$$ $$\lim_{q\to1^-}\eta^*=1\qquad(\text{p. 38})$$

Significance

The proposition separates three regimes. When information loss is small ($\eta$ near $1$) a ban costs almost nothing and removes leakage, so the marketplace bans. When information loss is large and buyers are a priori likely to value the product, the marketplace can induce the low price $qv$ and sell to everyone, so a ban pays again. In between, allowing communication can win. With uniform switching costs, the comparison turns on how much leakage costs: when switching is cheap (small $\mu$) the baseline profit $\mu/2$ is small and the ban wins; when it is expensive, leakage is rare and allowing communication wins. The result is proved in the paper by an informal appendix argument. No part of it has been machine-checked. A formal version pins down what the paper leaves implicit: the seller's tie-breaking, the domain of $\eta$ on which $\Pi_L$ is defined, which endpoints the strict preferences hold at, and the order of the quantifiers in "sufficiently close to zero (sufficiently large)".

Difficulty

The obvious argument compares two closed forms, but the ban value is not a closed form: it is a maximum over a fee that switches the seller's option and its listing decision. Showing that the maximum is $\max\{\Pi_H,\Pi_L\}$ requires checking that the threshold fee keeps the seller listing, and that fees above the threshold earn at most $\Pi_H$. The second obstacle is the shape of $\Pi_L$: it is a rational function with a pole at $\eta=1$, and its monotonicity rests on the sign of the printed derivative. The comparison point $\eta^*$ involves a square root, so the equivalence $\Pi_L\le\Pi_H\iff\eta\ge\eta^*$ is a quadratic-root argument rather than a one-line inequality. Finally, part 4 needs the baseline equilibrium profit $\Pi^*(\mu)$ from the full baseline game, i.e. a solution of the seller's problem (1) and the marketplace's problem (3) under uniform $G$.

Formalization scope

All objects are real-valued, with the paper's letters: v c μ q η f; PiStar stands for $\Pi^*$. The standing assumptions $c<v$, $0<q<1$ and $0\le\eta\le 1$ are explicit hypotheses. The statements use the reduced seller problem (1) with $p_m=v$, as the paper does after its Lemma 1; Lemma 1 itself is not posed. The uniform $G$ is the clamped CDF. Seller optimality, the baseline equilibrium and the ban value are optimality predicates (IsGreatest over the fees), never sSup or a chosen maximizer.

Conventions and disclosed additions:

• In parts 1–3, $\Pi^*$ is any real in $(0,v-c)$, a generalization of the paper's $\Pi^*$ for a general "well behaved" $G$; the proof uses nothing else.
• Part 4 is posed for each fixed $\eta\in(0,1)$: it fails at $\eta=0$ (ban) when $qv\le c$ and at $\eta=1$ (allow). It adds $c\ge 0$, without which the marketplace bans for every $\mu$ at small $\eta$.
• The milestones on the ban value, the derivative's sign and $\eta^*$ add $v>0$, which the proof uses without stating; each is false for some $v\le 0$.
• $\Pi_L$ and the threshold divide by $1-\eta$ and are stated only for $\eta<1$; the game itself has no division.
• "Prefers" is strict in both directions.

Trivializing formalizations are ruled out: the ban value is not defined as $\max\{\Pi_H,\Pi_L\}$, the thresholds in $\mu$ are quantified after $\eta$ and not before, $\Pi^*$ is constrained to $(0,v-c)$, and preferences are strict.

A complete development needs elementary real analysis only: derivatives of rational functions, the intermediate value theorem on $[0,1)$, limits at $1$, and the baseline solution of (1) and (3) under uniform switching costs. That baseline solution is reusable for the other missions of this series. Proofs of individual milestones are welcome independently.

Selected references

• A. Hagiu, J. Wright, Marketplace Leakage, Management Science, 2023. Authors' manuscript dated March 2023. doi:10.1287/mnsc.2023.4757
• A. Piolatto, F. Schuett, Information vs Competition: How Platform Design Affects Profits and Surplus, TILEC Discussion Paper DP2022-002, 2022 (cited in footnote 8 of the paper for the idea that limiting information exchange reduces transaction value on a platform).

Motivation

A firm that sells a network good (a platform, a communication service, a standard) faces consumers whose benefit from buying grows with the number of other buyers. When these network effects are strong, the buying decisions form a coordination game: everybody buying and nobody buying can both be equilibria at the same price and quality. The firm's choice of quality then depends on which equilibrium it expects consumers to play.

The classical answer, going back to Spence's analysis of monopoly quality (Spence 1975), is that a monopolist sets quality for the marginal consumer. Under the usual equilibrium-selection criteria (Pareto dominance, focality) the network-good monopolist inherits this logic. L. T. Chan, Quality Strategies in Network Markets (Management Science, 2023; SSRN copy 4203818), asks what happens when the firm instead anticipates potential maximization, a generalization of risk dominance to many players introduced through the potential games of Monderer and Shapley (1996). The answer is a different first-order condition for quality, in which every consumer's valuation and every possible number of buyers matter. This mission formalizes that condition, Proposition 5 of the paper, together with the chain of results in §3 that leads to it.

Setting

There are $n\ge 1$ consumers $N=\{1,\dots,n\}$. Consumer $i$ has a valuation $v_i>0$, labelled so that $v_1\ge\dots\ge v_n$. The benefit $f(k,q)\ge 0$ of the good when $k$ consumers buy at quality $q$ is weakly increasing in $k$ and, in $q$, weakly increasing and differentiable. The firm's cost of quality $c(q)\ge 0$ is weakly increasing and differentiable.

In stage 1 the firm chooses a price $p\ge 0$ and a quality $q\ge 0$. In stage 2 consumers simultaneously decide whether to buy. If $B\subseteq N$ is the set of buyers, consumer $i$ receives the payoff (7)

$$u_i(B,p,q)=v_if(|B|,q)-p\ \text{ if } i\in B,\qquad u_i(B,p,q)=0\ \text{ if } i\notin B,$$

and the firm earns $|B|p-c(q)$. A buyer set $B$ is a Nash equilibrium of stage 2 if no buyer gains by leaving and no non-buyer gains by joining. The market has strong network effects at $q$ when $v_if(i,q)$ is strictly increasing in $i$.

The potential (10) of a buyer set is

$$\Phi(B,p,q)=\sum_{i=1}^{|B|}f(i,q)-p\sum_{i\in B}\frac1{v_i}.$$

A potential maximizer is a buyer set maximizing $\Phi(\cdot,p,q)$ over all subsets of $N$. A firm that anticipates potential maximization earns $\Pi(p,q)=np-c(q)$ when all consumers buying is a potential maximizer, and $-c(q)$ otherwise. In Lean these objects are Market, Market.Standing, Market.StrongNE, Market.u, Market.IsNash, Market.pot, Market.IsPotMax and Market.profitPM in the namespace NetworkQuality.PotentialMax.

Formalization targets

Goal: Proposition 5 (p. 15)

Assume the standing assumptions and strong network effects at every $q\ge 0$. If $(p^*,q^*)$ maximizes $\Pi$ over $p\ge 0$, $q\ge 0$ and $q^*>0$, then

$$c'(q^*)=n\Big(\frac1n\sum_{i=1}^n\frac1{v_i}\Big)^{-1}\frac1n\sum_{i=1}^n\frac{\partial f(i,q^*)}{\partial q}.$$

The statement is the necessary first-order condition. It fixes no functional form for $f$ or $c$.

Milestones

1. (11), p. 13. For $i\notin B_{-i}$: $u_i(B_{-i}\cup\{i\})-u_i(B_{-i})=v_i[\Phi(B_{-i}\cup\{i\})-\Phi(B_{-i})]$, so stage 2 is a weighted potential game.
2. §3.5, p. 14. Every potential maximizer is a Nash equilibrium.
3. Proposition 1, p. 10. Under strong network effects the equilibria are exactly $\{N\}$ for $p<v_1f(1,q)$, $\{\emptyset\}$ for $p>v_nf(n,q)$, and $\{N,\emptyset\}$ in between.
4. (12), p. 14. Under strong network effects every potential maximizer is $N$ or $\emptyset$, and $N$ is one iff $p\le\big(\frac1n\sum_i\frac1{v_i}\big)^{-1}\frac1n\sum_i f(i,q)=:p(q)$.
5. (13), p. 14. $v_1f(1,q)\sum_i\frac1{v_i}\le\sum_i f(i,q)\le v_nf(n,q)\sum_i\frac1{v_i}$.
6. (14), p. 15. At each quality the maximal profit over prices $p\ge0$ is $n\,p(q)-c(q)$, attained at $p(q)$.

Significance

The result. Proposition 5 replaces the Spence condition $c'(q)=n\,v_n\,\partial f(n,q)/\partial q$ (Proposition 4 of the paper) by one in which the marginal consumer's valuation $v_n$ is replaced by the harmonic mean of all valuations, and the equilibrium benefit $f(n,q)$ by its uniform average over the number of buyers. Comparing it with the social optimum (Proposition 3, arithmetic mean of valuations) shows that a firm worried about miscoordination underprovides quality relative to the planner, increasingly so as valuations become more dispersed, and that it tends to undersupply (oversupply) quality when the number of buyers and quality are complements (substitutes) in the benefit $f$ (p. 15).

Formalizing it. The paper's arguments are in the main text (§3.2 and §3.5) and are short; some steps are only sketched: Proposition 1's proof treats only buyer sets of the form $\{1,\dots,k\}$, and (12) is derived only in the price range with two equilibria. A machine-checked development makes these steps complete, fixes the tie-breaking convention of the selection, and isolates exactly which assumptions the first-order condition uses (none of the convexity the paper assumes). No part of this result has a machine-checked proof at the time of writing.

Difficulty

The objects are finite and the algebra is elementary, so the difficulty lies in bookkeeping that the paper leaves implicit. The obvious reading of Proposition 1, "consumers $1$ to $k$ buy", is not forced when valuations tie; excluding an arbitrary buyer set of intermediate size needs a comparison between its weakest buyer and its strongest non-buyer, using the ordering of valuations and nonnegativity of $f$. The characterization (12) is a statement about maximizers over all $2^n$ buyer sets, not just about the two candidates the text compares, so it rests on the reduction "potential maximizer ⇒ Nash equilibrium ⇒ $N$ or $\emptyset$". Finally the firm optimizes jointly over price and quality against a discontinuous profit function; the first-order condition only appears after the price has been optimized out at each quality, and it needs differentiability at an interior optimum.

Formalization scope

Consumers are Fin n; the paper's consumer $i$ is Lean index $i-1$, while the first argument of $f$ is a number of buyers in ℕ, so $\sum_{i=1}^n f(i,q)$ is ∑ i : Fin n, M.f (i.val + 1) q. $v_1$ and $v_n$ are M.v ⟨0, _⟩ and M.v ⟨n - 1, _⟩. $f$ and $c$ are total functions on ℝ.

The standing assumptions (Market.Standing, pp. 4 and 9) are: $n\ge1$; $v_i>0$ and $v$ antitone; for $k\ge1$ and $q\ge0$, $f(k,q)\ge0$, $f$ weakly increasing in $k$ and in $q$ on $[0,\infty)$, $f(k,\cdot)$ differentiable on $(0,\infty)$; $c\ge0$ on $[0,\infty)$, weakly increasing there and differentiable on $(0,\infty)$. Statements about a single quality add $q\ge0$, the paper's domain.

Added hypotheses, each disclosed in the items: equilibria are pure (buyer sets); the goal assumes an interior quality $q^*>0$ and strong network effects at every $q\ge0$; the "sufficiently convex" cost of p. 4 is dropped, so the goal is the necessary condition only. The profit under potential maximization selects "all buy" at the tie $\Phi(N)=\Phi(\emptyset)$, as the paper's "if and only if $p\le\dots$" does.

The profit is defined through the selection (IsPotMax over all buyer sets), not as the reduced formula (14), and the goal's optimality hypothesis ranges over price and quality jointly; defining the profit by (14), or restricting maximizers to $\{N,\emptyset\}$, would trivialize the mission and is ruled out. Derivatives are deriv, and the standing assumptions guarantee they are genuine at $q^*>0$.

Everything needed beyond Mathlib (Finset, deriv, IsLocalMax) is in the single definition file. Proofs of the milestones in any order are welcome, as are proofs of the goal that use the milestones as stepping stones.

Selected references

• L. T. Chan, Quality Strategies in Network Markets, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4792 (SSRN version of April 2023: https://ssrn.com/abstract=4203818)
• D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
• A. M. Spence, Monopoly, Quality, and Regulation, Bell Journal of Economics 6 (1975), 417–429. https://www.jstor.org/stable/3003302

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits for combinatorial optimization, indexed by a depth $p$ and $2p$ real angles. It has become one of the standard candidate algorithms for near-term quantum hardware, and its MaxCut instance is the usual benchmark on which it is analysed.

The algorithm is run by preparing a quantum state, measuring it in the computational basis to obtain a bit string $z$, and evaluating the classical objective $C(z)$. Its analysis in the paper bounds the mean $F_p$ of $C(z)$. A mean alone does not say what a single run returns. Section III of the paper supplies the missing piece for MaxCut on bounded-degree graphs: the variance of $C(z)$ grows at most linearly in the number of edges, so the measured cut values are concentrated around $F_p$ and a modest number of repetitions reproduces the mean. This mission formalizes that variance bound, equation (30) of the paper, together with the locality and counting facts it rests on.

Setting

Let $G$ be a simple graph on vertices $\{0,\dots,n-1\}$ with edge set $\{\langle jk\rangle\}$ of size $m$, each edge listed once. Vertices are qubits; a computational basis state is a bit string $z\in\{0,1\}^n$.

• The clause operator of an edge is $C_{\langle jk\rangle}=\tfrac12(-\sigma^z_j\sigma^z_k+1)$. It is diagonal: $C_{\langle jk\rangle}(z)=1$ if $z_j\ne z_k$ and $0$ otherwise.
• The MaxCut objective is $C=\sum_{\langle jk\rangle}C_{\langle jk\rangle}$; $C(z)$ is the number of edges cut by $z$.
• The mixer is $B=\sum_j\sigma^x_j$, and $U(C,\gamma)=e^{-i\gamma C}$, $U(B,\beta)=e^{-i\beta B}$.
• The initial state is $|s\rangle=2^{-n/2}\sum_z|z\rangle$.
• For $p\ge1$ and angles $\boldsymbol\gamma=(\gamma_1,\dots,\gamma_p)$, $\boldsymbol\beta=(\beta_1,\dots,\beta_p)$, the QAOA state is

$$|\boldsymbol\gamma,\boldsymbol\beta\rangle=U(B,\beta_p)\,U(C,\gamma_p)\cdots U(B,\beta_1)\,U(C,\gamma_1)\,|s\rangle .$$

• Measuring it gives $z$ with probability $P(z)=|\langle z|\boldsymbol\gamma,\boldsymbol\beta\rangle|^2$. The mean is $F_p(\boldsymbol\gamma,\boldsymbol\beta)=\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle=\sum_zP(z)C(z)$ and the variance is

$$\langle\boldsymbol\gamma,\boldsymbol\beta|C^2|\boldsymbol\gamma,\boldsymbol\beta\rangle-\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle^2 .$$

• The light cone (the paper's subgraph $g(j,k)$) of an edge is the set of qubits at graph distance at most $p$ from $j$ or from $k$.

In Lean these are edgeCut, cutValue, qaoaState, expectCut and edgeTerm in the shared FarhiQAOA.Cubic setting, and edgePairs, cutVariance, edgePairTerm, edgeCov and lightCone in FarhiQAOA.Concentration, all built on the published QAlgorithms definitions of qubit registers, measurement probabilities, the uniform superposition, the problem Hamiltonian and the QAOA unitary.

Formalization targets

Goal: the variance bound (30)

For a $v$-regular graph with $v\ge3$, every depth $p\ge1$ and all real angles,

$$\langle\boldsymbol\gamma,\boldsymbol\beta|C^2|\boldsymbol\gamma,\boldsymbol\beta\rangle-\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle^2\le2\left[\frac{(v-1)^{2p+2}-1}{(v-1)-1}\right]\cdot m .$$

The constant is the paper's, as printed.

Milestones

1. (27)–(28). The variance is the double sum, over ordered pairs of edges, of the covariances $\langle C_{\langle jk\rangle}C_{\langle j'k'\rangle}\rangle-\langle C_{\langle jk\rangle}\rangle\langle C_{\langle j'k'\rangle}\rangle$.
2. Disjoint light cones. If $g(j,k)$ and $g(j',k')$ share no qubit, the covariance of the two edges is $0$.
3. (26). For maximum degree $v\ge3$, $|g(j,k)|\le2\big[((v-1)^{p+1}-1)/((v-1)-1)\big]$.
4. (29). For maximum degree $v\ge3$, at most $2\big[((v-1)^{2p+2}-1)/((v-1)-1)\big]$ edges $\langle j'k'\rangle$ have $g(j',k')$ meeting $g(j,k)$.
5. Summand bound. Each covariance is at most $1$ in absolute value.

Companions, printed in the paper for $v=2$: $|g(j,k)|\le2p+2$ and at most $4p+4$ meeting edges.

Significance

The result. For fixed $v$ and $p$ the bound makes the standard deviation of the cut value $O(\sqrt m)$, while the mean is of order $m$. The algorithm's output is therefore concentrated: a single measurement already returns a cut close to $F_p$ in relative terms, and the paper uses this to argue that the sample mean of polynomially many runs estimates $F_p$ within $1$. The same locality structure, that each edge term depends only on a bounded neighbourhood, is what makes $F_p$ classically computable for fixed $p$ and underlies later analyses of QAOA on bounded-degree and random regular graphs.

Formalizing it. The bound is proved in the paper in a few lines; none of it is machine-checked. A formal proof has to make the paper's operator locality argument precise (the conjugated clause operator is supported on the light cone, and the initial state is a product state), connect it to the computational-basis probabilities, and carry out the graph counting with explicit constants. The resulting locality lemma for QAOA circuits on graphs is reusable for any statement about QAOA at fixed depth.

Difficulty

The algebra of (28) and the bound by $1$ are routine. The substance is in two places.

The vanishing of a covariance requires showing that $U^\dagger C_{\langle jk\rangle}U$, for the full depth-$p$ QAOA unitary $U$, acts only on the qubits of $g(j,k)$, and that for two operators acting on disjoint sets of qubits the expectation in the product state $|s\rangle$ factorizes. Both are statements about operators on $(\mathbb C^2)^{\otimes n}$, whereas the objects in the statement are probabilities of computational basis states; the formal proof must pass between the two. Matrix exponentials of commuting sums have to be split into commuting factors, which in Lean means working with NormedSpace.exp on matrices indexed by bit strings.

The counting (26) and (29) is a ball-growth bound in a graph of bounded degree. The paper's count, via (26) with $p$ replaced by $2p+1$, bounds vertices, while (29) counts edges; the passage between the two, and the extended graph distance on disconnected graphs, must be made exact with the printed constant.

Formalization scope

• Qubits are indexed by Fin n, bit strings are Fin n → Bool with true the bit $1$, and states live in EuclideanSpace ℂ (Fin n → Bool).
• All expectations are sums $\sum_zP(z)\,f(z)$ over the computational basis. This equals the operator expectation in the paper because every operator involved is diagonal.
• Each edge is counted once (pairs $j<k$), in $m$, in $C$, in the double sum of (28) and in the count (29).
• Graph distance is the extended distance SimpleGraph.edist ($+\infty$ between components).
• The goal is stated for $v$-regular graphs with $v\ge3$, the domain of the printed formula. The milestones (26) and (29) assume only maximum degree $\le v$, as printed there.
• The angles range over all of $\mathbb R^p$. The paper restricts them to $[0,2\pi]$ and $[0,\pi]$ by periodicity; the bound does not depend on that restriction.
• The QAOA state is the state itself, not an arbitrary vector: normalisation of the measurement probabilities follows from unitarity and is part of what must be proved.

A variance defined with two different states, or a probability vector that is not normalised, would make the goal vacuous or false; the definitions use the single state $|\boldsymbol\gamma,\boldsymbol\beta\rangle$ throughout.

Out of scope: the $O(\sqrt m)$ standard-deviation reading and the sampling claim after (30), which carry no explicit constant; the measurement-and-repetition procedure, running time, circuit depth and the classical search for the angles.

Welcome contributions: a general light-cone lemma for conjugation by products of exponentials of local Hamiltonians on qubits; factorization of product-state expectations over disjoint qubit sets; ball-size bounds in graphs of bounded degree.

Selected references

• E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028 (v1; Section III, pp. 6–7)
• E. Farhi, J. Goldstone, S. Gutmann, M. Sipser, Quantum Computation by Adiabatic Evolution, arXiv preprint, 2000. https://arxiv.org/abs/quant-ph/0001106

Motivation

Online platforms such as ride-hailing, delivery and advertising marketplaces routinely test new pricing or matching policies on a single market. Randomizing over users is often impossible there: every rider and driver in a city shares one supply pool, so treating some users and not others contaminates the control group. The standard alternative is a switchback experiment: the whole market alternates between the new policy (treatment) and the current one (control) over time, and the effect is estimated from the time series of outcomes. Switchbacks are in production use at ride-hailing and delivery firms (see the industry references in Bojinov, Simchi-Levi and Zhao, 2023).

The design question is when to switch. Switching often produces many nearly independent observations, but a policy change has carryover effects: an outcome is affected by the policy of the last few periods, not only the current one, so frequent switching leaves few periods whose recent history is purely treated or purely control. Bojinov, Simchi-Levi and Zhao formalize this trade-off in a design-based, minimax framework and solve it in closed form. This mission formalizes that solution.

Setting

Time is divided into periods $t\in[T]=\{1,\dots,T\}$. An assignment path is $w_{1:T}\in\{0,1\}^T$, with $w_t=1$ meaning treatment. For every period $t$ and every path there is a fixed, unknown potential outcome $Y_t(w_{1:T})\in\mathbb R$; the collection is $\mathbb Y$. Randomness comes only from the random path $W_{1:T}$.

Three assumptions restrict $\mathbb Y$:

1. Non-anticipation: $Y_t$ does not depend on $w_{t+1:T}$.
2. $m$-carryover: for $t\ge m+1$, $Y_t$ does not depend on $w_{1:t-m-1}$.
3. Boundedness: $|Y_t(w)|\le B$ for every $t$ and every path, with $B>0$.

The set of outcomes satisfying all three is $\mathcal Y$. Under 1–2, $Y_t(\mathbf 1_{m+1})$ and $Y_t(\mathbf 0_{m+1})$ denote the outcome after $m+1$ consecutive treatments, respectively controls. The estimand is the average lag-$m$ effect

$$\tau_m(\mathbb Y)=\frac1{T-m}\sum_{t=m+1}^T\bigl[Y_t(\mathbf 1_{m+1})-Y_t(\mathbf 0_{m+1})\bigr].$$

A regular switchback design $(\mathbb T,\mathbb Q)$ fixes randomization points $\mathbb T=\{t_0=1<t_1<\dots<t_K\}\subseteq[T]$, $K\ge1$, and probabilities $q_{t_k}\in(0,1)$. At each $t_k$ an independent coin with success probability $q_{t_k}$ is flipped, and its outcome is applied to the periods $t_k,\dots,t_{k+1}-1$ (with $t_{K+1}=T+1$). The Horvitz–Thompson estimator $\hat\tau_m$ weights the outcome of each period whose window $w_{t-m:t}$ is all ones (all zeros) by the inverse probability of that event. Its risk is the mean squared error

$$r(\eta_{\mathbb T,\mathbb Q},\mathbb Y)=\mathbb E\bigl[(\hat\tau_m-\tau_m(\mathbb Y))^2\bigr],$$

where the expectation is over the law $\eta_{\mathbb T,\mathbb Q}$ of the path. A design is minimax optimal if it minimizes the worst-case risk $\max_{\mathbb Y\in\mathcal Y}r(\eta_{\mathbb T,\mathbb Q},\mathbb Y)$ over all regular designs.

Formalization targets

Goal: the optimal design (Theorem 2 with Theorem 1)

1. If $m=0$ and $T\ge2$, the unique minimax-optimal regular design has $\mathbb T^*=\{1,2,\dots,T\}$ and fair coins.
2. If $m\ge1$ and $T=nm$ for an integer $n\ge4$, the unique minimax-optimal regular design is

$$\mathbb T^*=\{1,\ 2m+1,\ 3m+1,\ \dots,\ (n-2)m+1\},\qquad q_0=\dots=q_K=\tfrac12 .$$

The goal asserts both existence and uniqueness, and it compares against every regular design with arbitrary probabilities in $(0,1)$.

Milestones

In attack order:

1. Unbiasedness of the estimator (Proposition 1).
2. The moments of the error terms (Lemmas EC.3 and EC.4).
3. The adversary's best responses $\mathbb Y^\pm\equiv\pm B$ (Lemma 1).
4. The product inequality

$$\frac1{\prod_i q_i}+\frac1{\prod_i(1-q_i)}\ge2^{n+1}$$

(Lemma EC.2), and fair coins (Theorem 1). 5. The fair-coin moments (Lemma EC.6). 6. The structure of optimal point sets (Lemmas EC.7 and EC.8). 7. The closed-form risk (EC.8) (Lemma EC.9). 8. The integer optimum of the subset selection objective (7) at $T=nm$:

$$\min_{\mathbb T}\Bigl\{4\sum_{k=0}^{K}(t_{k+1}-t_k)^2+8m(t_K-t_1)+4m^2K-4m^2+4\sum_{k=1}^{K-1}\bigl[(m-t_{k+1}+t_k)^+\bigr]^2\Bigr\}=16mT-32m^2,$$

attained only at $\mathbb T^*$.

Companion statements

These are not milestones:

• Lemma EC.5 (the moments at $\mathbb Y^\pm$ for general $\mathbb Q$).
• Theorem 2's equivalence of (6) and (7), restricted to the goal's horizons.
• The optimal worst-case risk $(16mT-32m^2)B^2/(T-m)^2$.
• Lemma EC.10 on the gaps of minimizers of (7).

Significance

The result. Theorem 2 turns a design question into a rule: randomize once every $m$ periods, except that the first and the last epoch last $2m$ periods. The rule depends only on the carryover order $m$, not on $B$ or on the outcome model. A practitioner who chooses the period length close to the carryover duration gets a design that is robust to a short carryover, since the optimal designs for $m=0$ and $m=1$ nearly coincide. The fair-coin result (Theorem 1) keeps the inverse-probability weights at powers of $2$, which avoids the instability of Horvitz–Thompson estimators with extreme propensities. The same design underlies the paper's asymptotic normality result and its confidence intervals (mission 2 of this series).

Formalizing it. The results are proved in the paper; none of them is machine-checked. The formalization has to make the paper's finite-sample expansion of the risk exact, establish its integer optimum, and connect it to a genuine minimax statement over all regular designs, not only over fair-coin designs. It also pins down where the printed statements need hypotheses. As printed, the first sentence of Theorem 2 and Lemma EC.7 fail for short horizons (at $m=2$, $T=4$ the minimax-optimal point sets are $\{1,2\}$ and $\{1,4\}$, while (7) is minimized by $\{1,3\}$). Their corrected forms are stated here. The strictness part of Lemma 1 fails at $m=0$ (with $T=2$, $\mathbb T=\{1,2\}$, fair coins, outcomes $B$ in period 1 and $-B$ in period 2 tie with $\mathbb Y^+$); it is stated for $m\ge1$.

Difficulty

The risk is a quadratic form in the reduced outcomes whose coefficients depend on the combinatorics of the point set. The coefficients are products of inverse probabilities over the determining randomization points of each window $\{t-m,\dots,t\}$ and over the overlaps of two windows. Writing the risk in closed form requires a case analysis of how windows of length $m+1$ meet the blocks of the design. The paper's closed form (EC.8) holds only under three structural conditions on the points. Showing that every optimal design satisfies them (Lemmas EC.7, EC.8) needs exchange arguments that remove or move a point while keeping the design regular, and these break down at short horizons.

The step from the closed form to the explicit optimum is an integer program. The paper solves its continuous relaxation and observes that the relaxed optimum is integral. A formal proof must handle every point set, including those that violate the structural conditions and for which (EC.8) is not the risk. The obvious approach of minimizing (EC.8) directly is therefore not enough: the minimax optimum must also be compared with designs outside the class where (EC.8) applies.

Formalization scope

Lean represents a path as a function $\mathbb N\to\mathrm{Bool}$ of which only the indices $1,\dots,T$ are read, potential outcomes as a function of the period and the whole path, and the point set as a Finset ℕ. Probabilities are indexed by the randomization point ($q_{t_k}$). The expectation under the law of a regular design is the finite sum over the $2^{K+1}$ coin vectors.

Committed conventions:

• the lag of the estimand equals the carryover order ($p=m$), as throughout §3;
• $m<T$;
• every probability lies in $(0,1)$, so the estimator's denominators are positive;
• $t_{K+1}=T+1$;
• $(a)^+=\max\{a,0\}$.

Minimax optimality is the statement "for every regular design and every admissible $\mathbb Y$ there is an admissible $\mathbb Y'$ whose risk under the other design is at least the risk of $\mathbb Y$ under this one". No supremum over outcome functions is ever taken. $\mathbb Y^\pm$ are the constant outcome functions $\pm B$.

Added hypotheses.

• The case $m=0$ of the goal requires $T\ge2$, the page's condition that $K$ be positive.
• Lemma EC.7 assumes $m=0$ or $T=nm$ with $n\ge4$.
• The strictness clause of Lemma 1 assumes $m\ge1$ (it is false at $m=0$), and its "$\mathbb Y\ne\mathbb Y^\pm$" is read on the reduced outcomes $(Y_t(\mathbf 1_{m+1}),Y_t(\mathbf 0_{m+1}))_{t\ge m+1}$.
• Lemmas EC.7–EC.9 are stated for fair coins against $\mathbb Y^\pm$, as in the paper's EC.3.5.
• Lemma EC.10 is read for minimizers of (7).

Not a trivialization. The goal mentions neither the objective (7) nor the structural conditions, nor the closed form (EC.8). It is stated against the full class of regular designs and asserts existence. A proof cannot replace it by "$\mathbb T^*$ minimizes (7)" (that is a milestone), and Theorem 1 is not vacuous because the goal asserts that optimal designs exist.

A complete development needs finite expectations over independent coin flips, the risk expansion as a quadratic form, and an integer optimization argument. The first two are reusable for the second mission of this series and for other design-based analyses of Horvitz–Thompson estimators. Proofs of any milestone, and of the companion statements, are welcome independently.

Selected references

• I. Bojinov, D. Simchi-Levi, J. Zhao, Design and Analysis of Switchback Experiments, Management Science 69(7), 2023; arXiv:2009.00148v4, 2025. https://arxiv.org/abs/2009.00148
• I. Bojinov, N. Shephard, Time Series Experiments and Causal Estimands: Exact Randomization Tests and Trading, Journal of the American Statistical Association 114(528), 2019. https://doi.org/10.1080/01621459.2018.1527225
• C.-F. J. Wu, On the Robustness and Efficiency of Some Randomized Designs, Annals of Statistics 9(6), 1981. https://doi.org/10.1214/aos/1176345640
• D. G. Horvitz, D. J. Thompson, A Generalization of Sampling Without Replacement from a Finite Universe, Journal of the American Statistical Association 47(260), 1952. https://doi.org/10.1080/01621459.1952.10483446

Motivation

The quantum approximate optimization algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits, indexed by an integer depth $p \ge 1$, that prepare states whose computational-basis measurements are biased toward good solutions of a combinatorial optimization problem. It became the standard candidate for optimization on near-term quantum hardware, and its performance on MaxCut is the benchmark against which later analyses and experiments are measured.

The original paper proves one concrete performance guarantee: at depth $p = 1$, on 3-regular graphs, the algorithm achieves an approximation ratio of at least $0.6924$. Short timeline:

• 2014, Farhi–Goldstone–Gutmann: the $p = 1$ bound $0.6924$ on 3-regular graphs, by reducing the expected cut to three subgraph functions and a numerical minimization (arXiv:1411.4028).
• 2018, Wang, Hadfield, Jiang and Rieffel: closed-form expressions for the $p = 1$ MaxCut expectation on arbitrary graphs (arXiv:1706.02998, Phys. Rev. A 97, 022304).
• Classically, Goemans and Williamson's semidefinite rounding achieves $0.878$ on all graphs (J. ACM 42, 1995), so the $p = 1$ guarantee is, as the paper itself notes, below the best classical algorithms.

Setting

A graph $G$ has vertex set $\{0, \dots, n-1\}$, and 3-regular means every vertex has exactly three neighbours. Each vertex carries a qubit; a computational basis state is a bit string $z = z_0 \cdots z_{n-1}$. For an edge $\langle jk\rangle$ the clause $C_{\langle jk\rangle}(z)$ is $1$ if $z_j \neq z_k$ and $0$ otherwise, and the cut objective is

$$C(z) = \sum_{\langle jk\rangle} C_{\langle jk\rangle}(z),$$

the number of edges cut by the bipartition $z$ defines. As an operator, $C$ is diagonal in the computational basis.

Let $B = \sum_j \sigma^x_j$ and let $|s\rangle = 2^{-n/2}\sum_z |z\rangle$. For angles $\gamma, \beta \in \mathbb R$, the depth-one QAOA state and its expected cut are

$$|\gamma,\beta\rangle = e^{-i\beta B}\, e^{-i\gamma C}\, |s\rangle, \qquad F_1(\gamma,\beta) = \langle\gamma,\beta|\,C\,|\gamma,\beta\rangle = \sum_z |\langle z|\gamma,\beta\rangle|^2\, C(z).$$

The angles may be restricted to $\gamma \in [0, 2\pi]$, $\beta \in [0, \pi]$ by periodicity.

Two kinds of small subgraphs govern the analysis. A crossed square is a set of four vertices spanning exactly five edges (a 4-cycle with one diagonal). An isolated triangle is a triangle whose three outgoing edges end on three distinct vertices. $S$ and $T$ denote their numbers in $G$. Finally, for an edge $\langle jk\rangle$ the subgraph type is the shape of the edge together with its adjacent edges; in a 3-regular graph there are three types $g_4, g_5, g_6$, according as $j$ and $k$ have two, one or no common neighbours. Each type $g$ defines a function $f_g(\gamma, \beta)$, the expectation of the clause of the central edge in the depth-one QAOA state of the subgraph $g$ alone.

Formalization targets

Goal: the depth-one ratio on cubic graphs

For every connected 3-regular graph $G$ there are angles $\gamma \in [0, 2\pi]$, $\beta \in [0, \pi]$ with

$$F_1(\gamma, \beta) \;\ge\; 0.6924 \cdot C(z) \qquad \text{for every bit string } z,$$

that is, $M_1 = \max_{\gamma,\beta} F_1 \ge 0.6924 \cdot \max_z C(z)$. The constant is exactly the paper's $0.6924$, and $K_4$ is included.

Milestones

The paper's argument passes through the following claims, each a milestone:

1. At $p = 1$ each edge term of a 3-regular graph equals $f_{g_4}$, $f_{g_5}$ or $f_{g_6}$ according to its subgraph type (p. 5).
2. In a connected 3-regular graph other than $K_4$, there are $S$ edges of type $g_4$ and $4S + 3T$ of type $g_5$ (pp. 8–9).
3. Equation (32): $F_1 = S f_{g_4} + (4S + 3T) f_{g_5} + (3n/2 - 5S - 3T) f_{g_6}$ (p. 9).
4. $3T + 4S \le n$ (p. 8).
5. Every cut has at most $3n/2 - S - T$ edges (p. 9).
6. For $s, t \ge 0$ with $4s + 3t \le 1$, the scaled ratio (35) $M_1(1, s, t)/(3/2 - s - t)$ is at least $0.6924$ (p. 9).
7. On $K_4$ the depth-one ratio exceeds $0.6924$ (p. 8).

Significance

The result is the first rigorous worst-case guarantee for the QAOA, and the method behind it (the expected objective is a sum of local terms, each depending only on a bounded neighbourhood of an edge) is the template for every later analysis of fixed-depth QAOA on bounded-degree graphs. It shows that a depth-one circuit, of depth independent of $n$, achieves a constant approximation ratio uniformly over an infinite class of graphs.

The paper's proof is complete apart from one numerical step: the minimization of (35) is reported as a numerical evaluation. No machine-checked version of the result exists. A formal proof requires an exact evaluation of the three subgraph functions at suitable angles, an exact combinatorial count of edge types, and a certified inequality in place of the numerical minimization. The margin is small: the exact minimum is $\tfrac12 + \tfrac{1}{3\sqrt 3} \approx 0.692450$, about $5 \cdot 10^{-5}$ above the paper's constant.

Difficulty

The light-cone reduction (milestone 1) is the conceptual step: one must show that conjugating a two-qubit clause by $e^{-i\gamma C}$ and $e^{-i\beta B}$ leaves an operator that involves only the qubits adjacent to the edge, and that the remaining qubits contribute a factor of one. In matrix form on $2^n$-dimensional space this is a statement about tensor-product structure that the definitions do not make visible. The combinatorial count (milestones 2–4) needs a careful case analysis of how triangles sit in a cubic graph, including the exceptional graph $K_4$, where the count fails. The final inequality (milestone 6) has a margin of order $10^{-4}$, so crude bounds on the trigonometric functions $f_{g}$ do not suffice.

Formalization scope

• Representation. Bit strings are Qubits n = Fin n → Bool from the published QAlgorithms layer, with true the bit $1$. States are vectors in EuclideanSpace ℂ (Qubits n); $|s\rangle$, $C$ as a diagonal operator, $B$ and the QAOA unitary are the published definitions uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary. The latter takes mixer angles before phase angles.
• Conventions. Graphs are SimpleGraph (Fin n) with decidable adjacency; "3-regular" is IsRegularOfDegree 3. The cut counts each edge once. $F_1$ is defined as $\sum_z \Pr[z]\,C(z)$, which equals $\langle\gamma,\beta|C|\gamma,\beta\rangle$ because $C$ is diagonal. The constant $0.6924$ is the exact rational $1731/2500$.
• Added hypotheses. Milestones 2 and 3 assume $G$ connected and $n \ne 4$, which excludes $K_4$, the case the paper sets aside on p. 8. No other hypothesis is added.
• Out of scope. The goal concerns the expected cut at good angles, which is what the paper's analysis bounds. Measuring the state, repeating, and the claim that a cut of that size is then found with high probability are not formalized; nor are running time, circuit depth, or the search for optimal angles.
• Ruled-out trivializations. A cut objective counting each edge twice, or an unnormalized state, would leave the ratio statement formally intact but about the wrong objects; the setting counts each edge once and uses the normalized uniform superposition. The goal quantifies over all bit strings, so it cannot be satisfied by bounding a particular cut.
• Contributions welcome. Reusable lemmas on the light-cone locality of conjugated Pauli operators, closed forms of the depth-one MaxCut expectation, and counting lemmas for triangles in cubic graphs all serve beyond this mission.

Selected references

• E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028
• Z. Wang, S. Hadfield, Z. Jiang, E. G. Rieffel, Quantum approximate optimization algorithm for MaxCut: A fermionic view, Phys. Rev. A 97, 022304, 2018. https://arxiv.org/abs/1706.02998
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6), 1995. https://doi.org/10.1145/227683.227684

Motivation

Many transactions are priced by negotiation rather than posted prices: business-to-business procurement, used cars, real estate, the purchase of a company. Before negotiating, a buyer can often spend effort finding out how much the object is actually worth to it, through inspections, trials, consultants or market research. That information serves two purposes. It improves the joint decision of whether to trade at all, and it changes how the surplus of trade is split. Liang Guo's Gathering Information before Negotiation (SSRN 3930651; Management Science, doi:10.1287/mnsc.2022.4360) studies how a buyer's endogenous information acquisition interacts with the two primitives of bargaining: the parties' bargaining powers and the seller's cost.

The first finding of the paper, Proposition 1, concerns how much information the buyer gathers. Its comparative statics in the seller's cost are non-monotone, and this non-monotonicity drives the later results of the paper, in which a seller can be worse off with more bargaining power or a lower cost. This mission formalizes Proposition 1 in its general form, for an arbitrary prior. A companion mission (Gathering Information before Negotiation II) formalizes the payoff reversals under a uniform prior and a linear information cost.

Setting

A seller can supply one unit of a product at cost $c$. A buyer's true value $u$ of the unit is unknown to both parties; the common prior law of $u$ is $F$, with a finite mean $\hat u>0$.

Before negotiating, the buyer acquires a truth-or-noise signal $w$: with probability $\alpha$ the signal equals $u$, and with probability $1-\alpha$ it is an independent draw from $F$. Because the parties are risk neutral, only the buyer's posterior mean

$$v\equiv\alpha w+(1-\alpha)\hat u$$

matters. Ex ante, $v$ has the distribution function

$$G(v,\alpha)\equiv F\!\left(\frac{v-(1-\alpha)\hat u}{\alpha}\right).$$

The buyer chooses the informativeness $\alpha$ in an interval $[\underline\alpha,\bar\alpha]\subseteq(0,1)$ at a cost $k(\alpha)$ that is increasing, with $k(\underline\alpha)=0$ and $k(\bar\alpha)>0$.

After observing $v$, the parties trade exactly when $v>c$ and split the net surplus $v-c$ according to their bargaining powers $\theta_s,\theta_b\in(0,1)$, $\theta_s+\theta_b=1$. Anticipating this, the buyer chooses $\alpha$ to solve

$$\max_{\alpha\in[\underline\alpha,\bar\alpha]}\ U_b(\alpha)=\theta_b\,A(\alpha,c)-k(\alpha),\qquad A(\alpha,c)=\int_c^{\bar v}(v-c)\,dG(v,\alpha),\tag{6}$$

where $A(\alpha,c)$ is the total ex ante surplus (7). A solution of (6) is written $\alpha^*$; in general there may be several, and $\mathcal A^*(\theta_b,c)$ denotes the set of all of them.

Two sets $S,T\subseteq\mathbb R$ are compared in the induced set order $S\sqsubseteq T$ when $\min(s,t)\in S$ and $\max(s,t)\in T$ for all $s\in S$, $t\in T$.

Formalization targets

Goal: Proposition 1 (p. 10)

Whenever the optimal sets compared are nonempty,

$$\theta_b\le\theta_b'\ \Longrightarrow\ \mathcal A^*(\theta_b,c)\sqsubseteq\mathcal A^*(\theta_b',c),$$ $$c\le c'\le\hat u\ \Longrightarrow\ \mathcal A^*(\theta_b,c)\sqsubseteq\mathcal A^*(\theta_b,c'),\qquad \hat u\le c\le c'\ \Longrightarrow\ \mathcal A^*(\theta_b,c')\sqsubseteq\mathcal A^*(\theta_b,c).$$

The buyer's optimal information acquisition increases with its bargaining power, and first increases and then decreases with the seller's cost, turning at the prior mean $\hat u$.

Milestones

1. Display (1), p. 7. $G(v,\alpha)$ is nondecreasing in $\alpha$ for $v<\hat u$ and nonincreasing for $v>\hat u$: the family rotates about $\hat u$.
2. Display (2) and footnote 7, p. 8. The mean of $v$ is $\hat u$ for every $\alpha$, and $\alpha\mapsto A(\alpha,c)$ is nondecreasing.
3. Proof of Proposition 1, p. 30. Integration by parts: $U_b(\alpha)=\theta_b\int_c^{\infty}[1-G(v,\alpha)]\,dv-k(\alpha)$.
4. Proof of Proposition 1, p. 30. $U_b$ has increasing differences in $(\alpha,\theta_b)$.
5. Proof of Proposition 1, p. 30. $U_b$ has increasing differences in $(\alpha,c)$ for $c\le\hat u$ and decreasing differences for $c\ge\hat u$.
6. Topkis's theorem (Topkis 1998, Theorem 2.8.1), already proved on the platform and referenced.

Significance

The result. The first part of Proposition 1 says that a buyer with more bargaining power gathers more information, because it captures a larger share of the surplus that information creates. The second part is the less expected one: a higher seller cost shrinks the gains from trade, yet it raises the buyer's incentive to become informed as long as the cost is below the prior mean $\hat u$, and lowers it only beyond. Information is most valuable when trade is a close call. The paper's later results (Corollary 1, Propositions 2 and 3) build on this: since information acquisition responds to $\theta_b$ and $c$, the seller's equilibrium payoff need not increase in its own bargaining power or decrease in its cost. The paper also notes (p. 11) that the monotonicity in $\theta_b$ needs only that a higher $\alpha$ is a mean-preserving spread, which is why the statement is posed here for every prior with finite mean.

Formalizing it. The proposition is proved in the paper, in a short appendix argument that differentiates under the integral and appeals to Topkis's theorem. To our knowledge it has not been machine-checked. The mission produces a density-free formalization: the rotation property and the mean-preserving-spread property of the truth-or-noise family, the integration-by-parts identity for the expected positive part, and the two increasing-differences statements, which together with the already formalized Topkis theorem give the goal.

Difficulty

The paper's argument is first-order: it computes cross-partial derivatives such as $\partial^2U_b/\partial c\,\partial\alpha=\theta_b\,\partial G(c,\alpha)/\partial\alpha$ and reads off their signs. Without a density these derivatives need not exist, and the information cost $k$ is assumed only increasing, so $U_b$ need not be differentiable, concave or even continuous in $\alpha$. The statements here are therefore in difference form, and the cross effects must be established as inequalities between integrals over different distributions of $v$.

The second obstacle is the shape of the comparative statics. Topkis's theorem gives a monotone optimal set in the induced set order on a parameter range where increasing differences hold, but the cost $c$ has increasing differences only on $(-\infty,\hat u]$ and decreasing differences on $[\hat u,\infty)$. The referenced platform theorem, by contrast, asks for increasing differences on the whole product of the decision and parameter spaces, so it does not apply to $U_b$ as it stands.

The obvious shortcut of picking a selection from the optimal set and proving it monotone does not work: the cross differences are only weakly positive (they vanish when $c$ lies outside the support of $v$), so the strict version of Topkis's theorem does not apply, and two different maximizers need not be ordered.

Formalization scope

The prior is a probability measure $\mu$ on $\mathbb R$ with integrable identity and positive mean $\hat u=\int w\,d\mu$. The paper's additional assumptions on $F$ (continuous and differentiable, strictly positive density on a bounded support $[\underline u,\bar u]$) and $c\in(\underline u,\bar u)$ are dropped: every statement is posed for all priors with finite mean and all real $c$, which implies the paper's case. $F$ is ProbabilityTheory.cdf μ, and $G$ is defined from it by the page's formula. The interval $[\underline\alpha,\bar\alpha]$ satisfies $0<\underline\alpha<\bar\alpha<1$; $k$ is monotone on it with $k(\underline\alpha)=0<k(\bar\alpha)$; $\theta_b\in(0,1)$ in every statement.

The total ex ante surplus is defined as $A(\alpha,c)=\int\max(\alpha w+(1-\alpha)\hat u-c,0)\,d\mu(w)$, which is (7) after the change of variables $v=\alpha w+(1-\alpha)\hat u$. The bargaining stage is not modelled; the paper's reduction to (6) is built into $U_b$. The optimal level $\alpha^*$ is the set of maximizers of $U_b$ over $[\underline\alpha,\bar\alpha]$ (optSet), never a chosen element. "Increases" is the induced set order, and every comparison assumes both optimal sets nonempty, which is the paper's presumption that (6) has a solution.

Trivializing formalizations are ruled out: $A$ is never given by a closed form or by the integration-by-parts expression (that identity is a milestone), $\alpha^*$ is never defined by a formula or a threshold rule, and the nonemptiness hypotheses prevent the induced set order from holding vacuously on an empty optimal set.

The development reuses the platform definitions Supermodularity.Lattices.InducedSetOrder and Supermodularity.Monotonicity.IncreasingDifferencesOn and the proved theorem Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences. The rotation and mean-preserving-spread lemmas for truth-or-noise signals, and the tail-integral identity $\mathbb E[(X-c)^+]=\int_c^\infty P(X>x)\,dx$ for integrable $X$, are reusable beyond this mission. Contributions of any of the milestones, of alternative proofs that avoid the integration by parts, and of the strict versions under the paper's density assumption are welcome.

Not posed in this mission: the benchmark (3)–(5), Corollary 1, Propositions 2–7, and the extensions of §4–§5.

Selected references

• L. Guo, Gathering Information before Negotiation, author's manuscript of 15 Feb 2022, SSRN 3930651. https://ssrn.com/abstract=3930651 ; published in Management Science (2022), https://doi.org/10.1287/mnsc.2022.4360
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• J. P. Johnson and D. P. Myatt, On the Simple Economics of Advertising, Marketing, and Product Design, American Economic Review 96(3), 756–784, 2006. https://doi.org/10.1257/aer.96.3.756