Missions · Prove2Me

Completed

Algorithmic Game Theory Convex Optimization Linear Optimization·Captain: mikedeng1

Persuading Risk-Conscious Agents: A Geometric Approach II: In Binary Persuasion with a Convex Non-Adoption Region the Convex Program Reduces to a Linear Program over Ω ∪ K₀₁Research Paper

Motivation

In Bayesian persuasion a sender who observes the state of the world commits to a signaling scheme, a receiver updates her belief by Bayes' rule and acts, and the sender chooses the scheme that maximizes her own expected payoff (Kamenica and Gentzkow 2011). The classical theory assumes the receiver maximizes expected utility, so her payoff is linear in her belief. Many applications violate this: a customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold, a commuter who values route reliability, a buyer who dislikes uncertainty about a product. Anunrojwong, Iyer and Lingenbrink (arXiv:2208.03758v3) call such receivers risk-conscious: the receiver's utility $\rho(\mu,a)$ of action $a$ at belief $\mu$ is an arbitrary function of $\mu$ .

The paper's first result reduces the sender's problem, an optimization over distributions of posteriors, to a finite-dimensional convex program (program (7)). This mission concerns its second main result: in the practically important binary persuasion setting (two actions, the sender always weakly prefers action $1$ ), when the region of beliefs at which the receiver rejects action $1$ is convex, program (7) collapses further to a linear program whose feasible region is the convex hull of finitely many explicit beliefs.

Setting

Let $\Omega$ be a finite set of states and $\Delta(\Omega)\subseteq\mathbb R^{\Omega}$ the simplex of beliefs, with the Euclidean topology. For $\omega\in\Omega$ , $e_\omega$ is the point-mass belief at $\omega$ ; states are identified with their point masses. The prior is $\mu^*\in\Delta(\Omega)$ . The receiver has actions $A=\{0,1\}$ and utility $\rho(\mu,a)$ . The optimality regions are

P_a=\{\mu\in\Delta(\Omega):\ a\in\arg\max_{a'\in A}\rho(\mu,a')\},

and the differential utility is $\hat\rho(\mu)=\rho(\mu,1)-\rho(\mu,0)$ , so $P_1=\{\hat\rho\ge 0\}$ and $P_0=\{\hat\rho\le 0\}$ inside $\Delta(\Omega)$ . The sender's utility is $v(\omega,a)$ with $v(\omega,1)\ge v(\omega,0)$ for every $\omega$ .

Two assumptions are used.

Assumption 1 (standing throughout the paper): $P_0$ and $P_1$ are closed.
Assumption 2: the non-adoption region $P_1^c=\{\mu\in\Delta(\Omega):\hat\rho(\mu)<0\}$ is convex.

From these data the paper builds finitely many beliefs. $K_1=\{\omega: e_\omega\in P_1\}$ and $K_0=\{\omega:e_\omega\in P_0\}$ are the states where action $1$ , respectively $0$ , is optimal under full information, and $L_0=K_0\setminus K_1$ the states where action $0$ is uniquely optimal. For $\omega_0\in L_0$ and $\omega_1\in K_1$ ,

\gamma(\omega_0,\omega_1)=\sup\{g\in[0,1]:\ g e_{\omega_0}+(1-g)e_{\omega_1}\in P_1\},\qquad \chi(\omega_0,\omega_1)=\gamma(\omega_0,\omega_1)e_{\omega_0}+(1-\gamma(\omega_0,\omega_1))e_{\omega_1},

the mixture of $\omega_0$ and $\omega_1$ with the most weight on $\omega_0$ at which action $1$ is still optimal, and $K_{01}=\{\chi(\omega_0,\omega_1):\omega_0\in L_0,\ \omega_1\in K_1\}$ .

A candidate solution is a pair $t=(t_0,t_1)$ of vectors in $\mathbb R^{\Omega}$ , with $t_a(\omega)$ the joint probability of state $\omega$ and action $a$ . The sender's objective is $\sum_\omega v(\omega,1)t_1(\omega)+v(\omega,0)t_0(\omega)$ . Program (7) maximizes it subject to $t_0+t_1=\mu^*$ and $t_a\in\operatorname{Conv}(P_a\cup\{0\})$ ; program (10) subject to $t_0+t_1=\mu^*$ , $t_1\in\operatorname{Conv}(K_1\cup K_{01}\cup\{0\})$ and $t_0\in\operatorname{Conv}(L_0\cup\{0\})$ .

Formalization targets

Goal: Theorem 3

Under Assumptions 1 and 2, with $v(\omega,1)\ge v(\omega,0)$ for all $\omega$ :

\text{(i)}\ \ t \text{ feasible for (10)} \Rightarrow t \text{ feasible for (7)};\qquad \text{(ii)}\ \ t \text{ feasible for (7)} \Rightarrow \exists\, t' \text{ feasible for (10)},\ \ \text{obj}(t)\le\text{obj}(t').

Together these say that (7) and (10) have the same optimal value and every optimal solution of (10) is optimal for (7): (7) "can be optimized by solving" (10).

Milestones

$\chi(\omega_0,\omega_1)\in P_0\cap P_1$ for $\omega_0\in L_0$ , $\omega_1\in K_1$ (Section 5.1, under Assumption 1).
Lemma 6: $\Delta(\Omega)=\operatorname{Conv}(L_0\cup K_{01})\cup\operatorname{Conv}(K_1\cup K_{01})$ , with no assumption on $\rho$ .
Lemma 7: under Assumption 2, $\operatorname{Conv}(P_1)=\operatorname{Conv}(K_1\cup K_{01})$ .

Further results on the same objects

Lemma 3: if $\hat\rho$ is quasiconvex on $\Delta(\Omega)$ , Assumption 2 holds.
Proposition 3: if $v(\omega,1)-v(\omega,0)=\bar v>0$ for all $\omega$ and a strict total order $\prec$ satisfies the monotonicity Assumption 3, every optimal solution of (10) has a threshold $\omega_0\in L_0$ with $t_1(\omega)=\mu^*(\omega)$ for $\omega\prec\omega_0$ and $t_1(\omega)=0$ for $\omega_0\prec\omega$ .
With strict preference $v(\omega,1)>v(\omega,0)$ for all $\omega$ , every optimal solution of (7) is feasible for (10).

Significance

Theorem 3 replaces an optimization over a convex set described only implicitly through $\rho$ by a linear program over an explicit polytope. It identifies a canonical signal set: irrespective of the prior, an optimal scheme only needs to induce beliefs in $\Omega\cup K_{01}$ , that is, either reveal the state or leave the receiver uncertain between one state of $L_0$ and one of $K_1$ . Lemma 7 gives a simple full-persuasion test, $\mu^*\in\operatorname{Conv}(K_1\cup K_{01})$ , and Proposition 3 a threshold structure of the induced actions that the paper uses in its queueing application. For expected-utility receivers the corresponding statements reduce to classical facts about concavification; the content here is that they survive non-linear utilities under a single convexity condition.

On the formal side, the results are proved in the paper and nothing about them is machine-checked. A complete development would give a verified reduction of a family of non-linear persuasion problems to linear programs, and a reusable library of convex-hull facts on the simplex (decompositions of the simplex into hulls of point masses and segment points). The formalization also corrects the paper at one point: the proof of Theorem 3 asserts that every optimal solution of (7) is feasible for (10), which fails when the sender is indifferent between actions in some state; the goal is stated in the form the proof establishes.

Difficulty

The inclusion of (10)'s feasible region in (7)'s is immediate once $K_{01}\subseteq P_1$ . The content lies in the converse: $P_1$ is an arbitrary closed set whose complement in the simplex is convex, and one must show that every point of $P_1$ is a convex combination of point masses in $K_1$ and the boundary points $\chi(\omega_0,\omega_1)$ on the edges of the simplex. The natural first idea, to argue with extreme points of $\operatorname{Conv}(P_1)$ , does not work directly: $P_1$ need not be convex, its convex hull need not be closed a priori, and the extreme points of $P_1$ are not in general on edges of the simplex. Assumption 2 constrains only the complement of $P_1$ , so it has to be transported to a statement about $P_1$ itself. A second difficulty is that $t_0$ in a solution of (7) may put weight on states in $K_0\cap K_1$ or on interior beliefs, and it must be moved to $t_1$ without lowering the objective.

Formalization scope

Beliefs are functions Ω → ℝ with [Fintype Ω] [DecidableEq Ω]; $\Delta(\Omega)$ is Mathlib's stdSimplex ℝ Ω; $e_\omega$ is Pi.single ω 1; actions are Fin 2; $\operatorname{Conv}$ is convexHull ℝ; $0$ is the zero vector.
The receiver's utility is ρ : (Ω → ℝ) → Fin 2 → ℝ, and $P_a$ is defined from it by Eq. (1), intersected with the simplex; values of ρ off the simplex are irrelevant. Assumption 1 is IsClosed (P ρ a) for both actions.
$K_0,K_1,L_0$ are sets of states; they enter convex hulls through their images under $e$ . $\gamma$ is a real sSup, used only for $\omega_0\in L_0$ , $\omega_1\in K_1$ , where the set contains $0$ and is bounded by $1$ .
Programs (7) and (10) are feasibility predicates on t : Fin 2 → Ω → ℝ with a common objective. Theorem 3 is stated as (i) and (ii) above, never through a supremum of objective values. A formalization in which (10) only needs to have some feasible point, or in which the supremum of an empty or unbounded set of values is compared, would be trivial or meaningless and is not the target.
Proposition 3 takes the order of Assumption 3 as a relation given with the data, and assumes $L_0\neq\emptyset$ , which the paper uses implicitly.
Needed infrastructure: convex hulls of finite sets of point masses in the simplex, Carathéodory-type finite decompositions (available in Mathlib), and the decomposition of a convex combination along a segment. Proofs of the milestones, alternative proofs of Lemma 7 (for example by a separation argument), and proofs of the further results are all welcome.

Selected references

Anunrojwong, J., Iyer, K., Lingenbrink, D., Persuading Risk-Conscious Agents: A Geometric Approach, arXiv:2208.03758v3, 2023 (journal version: Operations Research, 2024). https://arxiv.org/abs/2208.03758v3
Kamenica, E., Gentzkow, M., Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590

8 thms3 active usersReviewed

Machine Learning Probability Reinforcement Learning+1·Captain: mikedeng1

Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds II: Along Any h, the Empirical Transition Vector Is within 2√(log(n/ρ)Σγᵢcᵢ²/n) + 3D log(2/ρ)/n of the TruthResearch Paper

Motivation

Model-based reinforcement learning algorithms for Markov decision processes estimate each transition distribution $P_{s,a}$ from the transitions they have observed out of the state–action pair $(s,a)$ . Their regret analyses then need to know how far the empirical distribution $\hat p$ can be from the true one $p$ . The standard tool is an $\ell_1$ bound on $\hat p-p$ , as in UCRL2 (Jaksch, Ortner and Auer, 2010), which costs a factor of order $\sqrt S$ in the number of states $S$ . What the analysis actually uses, however, is the deviation along one direction: the projection $(\hat p-p)^Th$ onto a bias (or value) vector $h$ whose entries differ by at most the MDP's diameter $D$ .

S. Agrawal and R. Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023, as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds) prove a worst-case regret bound of order $\tilde O(D\sqrt{SAT})$ for an optimistic variant of posterior sampling. One ingredient of that analysis is their Proposition 5.2: a Bernstein-type bound on $(\hat p-p)^Th$ whose leading term is governed by a variance of $h$ under $p$ , written in stick-breaking form. This mission formalizes that proposition and the steps of its proof.

Setting

Fix a number of states $S$ and order them $1,\dots,S$ . A probability vector $p\in\Delta^S$ has $p_i\ge0$ and $\sum_ip_i=1$ . A multinoulli trial with parameter $p$ is a random state $X$ with $\mathbb P(X=i)=p_i$ . Draw $n$ independent trials $X_1,\dots,X_n$ and let

\hat p_i=\frac{\#\{t: X_t=i\}}{n}

be the empirical probability vector, the average of the one-hot outcomes. For $p$ and a vector $h\in\mathbb R^S$ define the stick-breaking quantities

\gamma_i=\frac{p_i(p_{i+1}+\cdots+p_S)}{p_i+\cdots+p_S},\qquad H_{i+1}=\frac{1}{\sum_{j=i+1}^Sp_j}\sum_{j=i+1}^Sh_jp_j,\qquad c_i=h_i-H_{i+1}.

Thus $H_{i+1}$ is the mean of $h$ under $p$ conditioned on the states after $i$ , and $c_i$ compares $h_i$ with it. The sum $\sum_{i<S}\gamma_ic_i^2$ equals the variance of $h(X)$ for $X\sim p$ . In Lean these objects are gammaCoef p i, Hnext p h i, cCoef p h i, phat ω i, the law of one trial is cat p and the law of $n$ trials is trialsLaw n p, all in the namespace OptimisticPSRL.Concentration.

Formalization targets

Goal: Proposition 5.2 (p. 9)

Let $h\in\mathbb R^S$ satisfy $|h_i-h_{i'}|\le D$ for all $i,i'$ , let $n\ge96$ and $\rho\in(0,1)$ . Then, with probability at least $1-\rho$ ,

\big|(\hat p-p)^Th\big|\le2\sqrt{\log(n/\rho)\sum_{i<S}\frac{\gamma_ic_i^2}{n}}+3D\,\frac{\log(2/\rho)}{n}.

Milestones

Fact 1 (p. 17), a deterministic identity: for probability vectors $\tilde p,\bar p$ with stick-breaking ratios $\tilde y_i=\tilde p_i/(\tilde p_i+\cdots+\tilde p_S)$ and $\bar y_i$ ,

(\tilde p-\bar p)^Th=\sum_i(\tilde y_i-\bar y_i)(h_i-\tilde H_{i+1})(\bar p_i+\cdots+\bar p_S)=\sum_i(\tilde y_i-\bar y_i)(h_i-\bar H_{i+1})(\tilde p_i+\cdots+\tilde p_S).

The projection as a sum of martingale differences (proof, p. 21): with $Z_{t,i}=c_i\mathbb 1(X_t=i)-c_i\frac{p_i}{p_i+\cdots+p_S}\mathbb 1(X_t\ge i)$ and $Z_t=\sum_iZ_{t,i}$ ,

\frac1n\sum_{t=1}^nZ_t=(\hat p-p)^Th,

together with the two intermediate expressions of the page. 3. Uncorrelated coordinates (proof, p. 21): $\mathbb E[Z_{t,i}Z_{t,j}]=0$ for $i\ne j$ . 4. The predictable variance (proof, p. 21): $\sum_{t=1}^n\mathbb E[Z_t^2]=\sum_ic_i^2\,n\,\gamma_i$ . 5. Corollary B.1 (p. 26), Bernstein's inequality for bounded martingale differences with random predictable variance $V_n$ : for $n\ge96$ , $\delta\in(0,1)$ , with probability greater than $1-\delta$ ,

|M_n|\le2\sqrt{V_n\ln(n/\delta)}+3K\ln(n/\delta).

Significance

The result. Proposition 5.2 is the concentration half of the optimism step of the paper (Lemma 5.3): combined with an anti-concentration bound for Dirichlet samples along the same direction (Proposition 5.1), it shows that some posterior sample is optimistic along $h$ with constant probability. Because the bound is stated along a single direction and is weighted by the variance of $h$ rather than by $D$ alone, it avoids the $\sqrt S$ loss that an $\ell_1$ bound would incur, which is part of how the paper's regret bound improves on UCRL2's $\tilde O(DS\sqrt{AT})$ . The stick-breaking form of the variance is what lets the same quantity appear on both sides of the optimism argument, in the Dirichlet bound and in the empirical bound.

Formalizing it. The proposition and its proof steps are proved on paper; none of them has a machine-checked proof. The regret theorem of the paper (Theorem 1) is not posed: its constants are hidden in $O(\cdot)$ and its algorithm's parameters are given as $\Theta(\cdot)$ . Proposition 5.2, by contrast, is fully explicit. Corollary B.1 is a reusable martingale inequality with explicit constants. The predictable-variance identity and Fact 1 are exact identities about stick-breaking coordinates that recur in analyses of Dirichlet and categorical models.

Difficulty

Two steps resist the obvious approach. First, the statement carries the variance in stick-breaking form, not as $\mathrm{Var}_p(h)$ ; linking the two needs the decomposition of Fact 1 and the identity for the predictable variance, which are exact algebraic identities whose bookkeeping of tails and empty tails is error-prone. Second, the paper's own route goes through Corollary B.1, a martingale Bernstein inequality with a random variance, which rests on a peeling argument over a grid of variance levels (Seldin et al., 2012); Mathlib has neither this inequality nor a Bernstein inequality with explicit constants for bounded variables.

A known subtlety: the paper's proof, through Corollary B.1, yields the second term $3D\log(n/\rho)/n$ , while the statement prints the smaller $3D\log(2/\rho)/n$ . The printed statement is still true for $n$ iid trials (the classical Bernstein inequality gives a bound below it), so the goal is posed as printed. The paper's own proof therefore does not establish the printed constant.

Formalization scope

States are Fin S with its natural order, 0-based; the paper's range $i<S$ is every state but the last (belowLast S). Fact 1 holds for every ordering; the natural order covers this since states are labels.
Probability vectors are p : Fin S → ℝ with IsProbVec p (nonnegative, summing to one). Zero entries are allowed. A ratio whose denominator is zero evaluates to $0$ (Lean's convention), which gives the values the identities need; no positivity of $p$ is assumed.
One trial has law cat p $=\sum_ip_i\delta_i$ ; $n$ trials have the product law trialsLaw n p $=$ Measure.pi. The empirical vector phat ω is computed from the sample ω : Fin n → Fin S. "With probability $1-\rho$ " is ENNReal.ofReal (1 - ρ) ≤ trialsLaw n p {good event}; Corollary B.1's "greater than $1-\delta$ " is strict. $\log$ is Real.log.
The proof displays (milestones 2–4) are stated in the iid reading of the proposition: the paper writes them for transitions of an MDP out of a fixed $(s,a)$ , with an indicator $\mathbb 1(s_{t-1}=s,a_{t-1}=a)$ and a random count $\tau$ ; here the indicator is one and $\tau=n$ , and the conditional expectations are expectations under one draw of law $p$ . Milestone 2 assumes every drawn state has positive probability (true almost surely), which the page's intermediate sum over $i\le S-1$ needs.
Corollary B.1 is posed for a general filtered probability space, with $Z_i$ $\mathcal F_i$ -measurable, $|Z_i|\le K$ almost surely and $\mathbb E[Z_i\mid\mathcal F_{i-1}]=0$ .

The goal cannot be satisfied by a degenerate reading: $\hat p$ is built from the sample, the measure is the $n$ -fold product of the categorical law $p$ , the event is the good event itself (not a complement bound), and the variance term is not identically zero (for $S=2$ , $p=(\tfrac12,\tfrac12)$ it equals $(h_1-h_2)^2/4$ ).

Needed infrastructure: finite-sum manipulations over tails of Fin S; a Bernstein or Freedman inequality with explicit constants (for iid bounded variables for the goal, for martingale differences for Corollary B.1). Contributions of either inequality are reusable well beyond this mission and are welcome, as are alternative proofs of the goal that bypass Corollary B.1.

Selected references

S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
Y. Seldin, F. Laviolette, N. Cesa-Bianchi, J. Shawe-Taylor and P. Auer, PAC-Bayesian inequalities for martingales, IEEE Transactions on Information Theory 58(12), 2012. https://doi.org/10.1109/TIT.2012.2211334

7 thms3 active usersReviewed

Complexity Theory Quantum Information·Captain: mikedeng1

Fixed-Point Quantum Search with an Optimal Number of Queries: The Phases of Eq. (11) Give Success Probability 1 − δ²T_L(T_{1/L}(1/δ)√(1−λ))²Research Paper

Motivation

Quantum search starts with a state that has some overlap with a desired target. Standard Grover iterations can increase that overlap quickly, but their success probability oscillates with the number of iterations. If the initial overlap is unknown, a sequence chosen for one value can pass the target and perform poorly at another. Earlier fixed-point constructions avoided this oscillation but lost the quadratic improvement in query count. Yoder, Low, and Chuang gave a sequence of adjustable phase reflections with both a specified failure tolerance and a query count proportional to the inverse square root of the initial target probability Yoder, Low, and Chuang (2014).

The result concerns amplitude amplification, a reusable procedure in which a quantum algorithm prepares a state, a target test identifies the useful component, and repeated operations increase the chance of measuring that component. The paper's exact success formula is useful because it says what happens at every initial overlap, rather than only at a single guessed overlap or in an asymptotic regime. Its polynomial form also explains why the interval with a guaranteed error bound grows as the sequence becomes longer Yoder, Low, and Chuang (2014), pp. 1–2.

Setting

Let $|s\rangle$ and $|T\rangle$ be unit vectors in a finite-dimensional complex state space. The target overlap is $\lambda=|\langle T|s\rangle|^2>0$ . The parameter $\delta$ sets the desired upper bound $\delta^2$ on failure probability. A generalized reflection about a unit state changes its phase while leaving the orthogonal directions unchanged. The two reflections used here are

S_s(\alpha)=I-(1-e^{-i\alpha})|s\rangle\langle s|, \qquad S_T(\beta)=I-(1-e^{i\beta})|T\rangle\langle T|.

Their Grover iterate is $G(\alpha,\beta)=-S_s(\alpha)S_T(\beta)$ . For $L=2l+1$ , the sequence is $\mathcal S_L=G(\alpha_l,\beta_l)\cdots G(\alpha_1,\beta_1)$ , so the iterate with index $1$ acts first. The phases are those in Eq. (11) of the paper: $\alpha_j=-\beta_{l-j+1}=2\cot^{-1}(\tan(2\pi j/L)\sqrt{1-\gamma^2})$ , where $\gamma^{-1}=T_{1/L}(1/\delta)$ Yoder, Low, and Chuang (2014), pp. 2–3.

Here $T_L$ is the degree- $L$ Chebyshev polynomial of the first kind. For the fractional order at an argument at least one, $T_{1/L}(1/\delta)$ means the positive real continuation $\cosh(\operatorname{arcosh}(1/\delta)/L)$ . This convention gives $T_L(\gamma^{-1})=1/\delta$ . The paper also uses a two-dimensional coordinate system spanned by the prepared state and target state, with basis order $|\bar t\rangle,|t\rangle$ and $|s\rangle=(\sqrt{1-\lambda},\sqrt\lambda)$ Yoder, Low, and Chuang (2014), Eqs. (4), (6)–(7).

Formalization targets

Exact success probability

The goal is the paper's Eq. (1), for the phase sequence of Eq. (11):

|\langle T|\mathcal S_L|s\rangle|^2 =1-\delta^2T_L\!\left(T_{1/L}(1/\delta)\sqrt{1-\lambda}\right)^2, \qquad L=2l+1.

This equality determines the entire response curve, including the one-step case $l=0$ . It is stated for arbitrary finite dimension, rather than only after fixing two coordinates. The milestones cover the paper's two-dimensional reduction, the reflection and rotation formulas, the equatorial-rotation sequence, its amplitude recurrence, and the Chebyshev identity used to finish the calculation Yoder, Low, and Chuang (2014), Eqs. (1), (4), (6)–(15).

Consequences

The same exact formula gives a fixed-point interval. With $w=1-T_{1/L}(1/\delta)^{-2}$ , the desired success bound holds whenever $\lambda\ge w$ :

\lambda\ge w\quad\Longrightarrow\quad |\langle T|\mathcal S_L|s\rangle|^2\ge1-\delta^2.

The draft also states that $w$ decreases as the odd length increases, the sufficient length bound $L\ge\log(2/\delta)/\sqrt\lambda$ of Eq. (3), and the nesting identity for success-probability functions in Eq. (18) Yoder, Low, and Chuang (2014), pp. 2, 4.

Significance

The exact formula gives a sequence that can be selected from a lower bound on the target overlap and a chosen failure tolerance. Increasing its length extends the interval on which the tolerance is met; an already adequate state therefore stays within the bounded-error regime at greater odd lengths. The sufficient length bound records the quadratic query scaling in the overlap parameter. The nesting identity shows that the same family of probability functions is closed under the paper's specified composition of tolerances Yoder, Low, and Chuang (2014), pp. 2, 4.

The mathematical result is proved in the 2014 paper. This mission asks for machine-checked proofs of its exact operator-level equality and the cited intermediate identities; the statements here are currently draft targets, not already machine-checked results. A completed development would leave reusable finite-dimensional phase-reflection and Chebyshev tools for subsequent amplitude-amplification arguments. The paper's oracle implementation is separate from these operator identities Yoder, Low, and Chuang (2014), Fig. 2.

Difficulty

The obvious idea of repeating a fixed phase pair produces the familiar Grover oscillation. Adjusting phases removes that simple repeated-power description, while the target amplitude must still be controlled exactly across all allowed overlaps. A proof must keep the complex phase conventions and multiplication order aligned with the Chebyshev expression. The fractional-order parameter also lies outside the usual cosine formula's interval when $\delta<1$ ; replacing the polynomial by a clamped arccosine expression changes the target formula. The unnumbered Chebyshev-amplitude assertion after Eq. (15) is the central algebraic gap left for formalization Yoder, Low, and Chuang (2014), p. 3.

Formalization scope

States are functions Fin N → ℂ, and operators are complex N × N matrices. Inner products conjugate the first vector. The theorem binds $\lambda$ to the squared target overlap and requires both states to have norm one; it does not take an unrelated free success parameter. The goal permits every $N$ for which its hypotheses can hold, and every $l\ge0$ . The rotation milestones use Fin 2 with index $0$ for $|\bar t\rangle$ and index $1$ for $|t\rangle$ . The operator $S_T$ has the same rank-one projector as the paper's phase-adjusted $S_t$ . Matrix exponentials define the rotations, and $T_L$ is Mathlib's polynomial, evaluated even outside $[-1,1]$ .

The scope assumes $0<\delta\le1$ . At $\delta=0$ , the displayed expression involves division by zero and the paper treats its $\pi/3$ limit separately. The inverse cotangent is $\pi/2-\arctan$ , a branch whose changes by $\pi$ leave the reflection phases unchanged. The product order is fixed by the recursion defining $\mathcal S_L$ . The mission formalizes Eqs. (6)–(7) as operators; the ancilla and oracle gates of Fig. 2 are outside this mission. The goal retains the full equality and cannot be reduced to the easier lower bound $P_L\ge1-\delta^2$ .

The milestone for printed Eq. (12) uses a free output $Z$ rotation and a unit global phase. The printed outer rotations do not give the claimed state for the stated phases; this corrected form preserves the coordinate magnitudes needed for Eq. (1). The milestone for Eq. (15) states the displayed amplitude recurrence but does not restate the page's incompatible intermediate $b'_h$ sentence. These corrections are identified in the item descriptions and moderation notes. Contributions proving the reduction, phase identities, amplitude recurrence, Chebyshev relation, or the final equality are all within scope Yoder, Low, and Chuang (2014), p. 3.

Selected references

Theodore J. Yoder, Guang Hao Low, and Isaac L. Chuang, Fixed-point quantum search with an optimal number of queries, Physical Review Letters 113, 210501 (2014). arXiv:1409.3305v2. This mission cites the pinned preprint's page and equation numbers.

10 thms3 active usersReviewed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures: The Optimal Maintenance Frontier Has Six Possible StructuresResearch Paper

Motivation

Machines in production lines deteriorate in ways that are only partly visible. A machine may run in a degraded state that raises costs without announcing itself, and eventually fail in a way that cannot be missed. The decision maker must choose between continuing production, paying for an inspection that reveals the hidden state, and replacing the machine preventively. Models of this kind are partially observable Markov decision processes (POMDPs), and for POMDPs closed-form optimal policies are rare: the value function lives on the space of beliefs and is usually only computed numerically.

H. Zhang and W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures (Management Science, 2022; read here as SSRN 2945049, version of 2022-08-21), solve the classical two-state version of this problem completely. Working in the dual "efficient frontier" framework of Zhang (2010), they show that the optimal solution has exactly six possible structures and give each in closed form, with explicit or implicitly characterized thresholds on the replacement and inspection costs.

Setting

A machine is in a hidden state $x\in\{0,1\}$ (good or bad) or in the observable failure state $F$ . Each period, if the machine has failed it is replaced correctively at cost $c^F$ ; otherwise one of three actions is chosen:

production $P$ costs $0$ in state 0 and $c^P$ in state 1;
inspection $I$ costs $c^I$ and reveals the current state;
preventive replacement $R$ costs $c^R$ and resets the machine to state 0.

Production always takes place. From state 0 the machine moves to state 1 with probability $\gamma_0$ ; from state 1 it fails with probability $\gamma_1$ . Write $\bar\gamma_x=1-\gamma_x$ , $\mathbf p_0=(\bar\gamma_0,\gamma_0)'$ , $\mathbf p_1=(0,\bar\gamma_1)'$ , $\mathbf g^P(u_F)=(0,c^P+\beta\gamma_1u_F)'$ , $\mathbf g^I(u_F)=(c^I,c^I+\beta\gamma_1u_F)'$ and $\mathbf P^P\mathbf u=(\mathbf p_0'\mathbf u,\mathbf p_1'\mathbf u)'$ . Costs are discounted by $\beta$ over an infinite horizon.

A continuation-cost vector $\mathbf u=(u_0,u_1)'$ records the cost of a continuation policy from each hidden state, and $u_F$ the cost after a failure. The expected optimal cost at an (unnormalized) belief $\boldsymbol\pi=(\pi_0,\pi_1)'\ge0$ is $V(\boldsymbol\pi)=\min_{\mathbf u\in U^*}\boldsymbol\pi'\mathbf u$ , where $U^*$ is the set of extreme points of the efficient frontier. The pair $(U^*,u^*_F)$ is the fixed point of the dual value iteration (12)–(16). In support-function form, a pair $(W,w_F)$ is mapped to

W'(\boldsymbol\pi)=\min\Big\{\boldsymbol\pi'\mathbf g^P(w_F)+\beta W\big((\mathbf P^P)'\boldsymbol\pi\big),\ (\pi_0+\pi_1)\big(c^R+\beta W(\mathbf p_0)\big),\ \boldsymbol\pi'\mathbf g^I(w_F)+\beta\big(\pi_0W(\mathbf p_0)+\pi_1W(\mathbf p_1)\big)\Big\},

w_F'=c^F+\beta W(\mathbf p_0),

the three terms being $P$ , $R$ and $I$ . A finite set $U$ with a number $u_F$ is the optimal solution for an action set if value iteration from zero terminal costs converges to $\min_{\mathbf u\in U}\boldsymbol\pi'\mathbf u$ for every $\boldsymbol\pi\ge0$ and to $u_F$ after a failure.

The structures are built from two point sequences. The production sequence is $\mathbf u_{i+1}=\mathbf g^P(u_F)+\beta\mathbf P^P\mathbf u_i$ . Started on the diagonal at $(u^R,u^R)'$ with $u_F=u^R+c^F-c^R$ , the self-consistency equation $u^R=c^R+\beta\mathbf p_0'\mathbf u_m$ has a unique solution $u^R=f(m)$ (31). Started instead at the inspection point (35), it gives $g(m)$ (40).

Formalization targets

Goal: Theorem 2 (pp. 27–28, Table 1)

Let $\theta=\dfrac{c^P+\beta\gamma_1c^F}{1-\beta+\beta(\gamma_0+\gamma_1)}$ and $\hat c=(1+\beta\gamma_0)c^P-\beta\bar\gamma_1(1-\beta+\beta\gamma_0+\beta\gamma_1)c^R+\beta^2\gamma_1\bar\gamma_1c^F$ . Under $\{P,I,R\}$ :

c^R\ge\theta\ \Rightarrow\ [P];\qquad \tfrac{\gamma_0}{\gamma_1}\theta\le c^R<\theta\ \Rightarrow\ R[P],\ IR[P]\ \text{or}\ [PIR]\ \text{by explicit thresholds on }c^I;

c^R<\min\{\tfrac{\gamma_0}{\gamma_1}\theta,\theta\}\ \Rightarrow\ \exists\,0<\hat c_1\le\hat c_2<c^R:\ [PR],\ I[PR]\ \text{or}\ [PIR]\ \text{as}\ c^I\ge\hat c_2,\ \hat c_1\le c^I<\hat c_2,\ c^I<\hat c_1,

with every structure an explicit pair $(U^*,u^*_F)$ from Table 1, and the thresholds characterized implicitly ( $\mathbf u^{I\dagger}$ on the frontier of $U^\dagger$ at $c^I=\hat c_2$ ; $\min f=\min g$ at $c^I=\hat c_1$ ).

Milestones

Proposition 2 (the fixed-point equations), Proposition 3 (the cost of producing forever), Lemma 1 and Lemma 6 (the two sequences in closed form), Lemma 3 and Lemma 7 (the anchors $f$ and $g$ ), Proposition 4 (unimodality of $f$ ), Theorem 1 (the two-action solution: $[P]$ , $R[P]$ , $[PR]$ , with extreme-point exactness) and Lemma 5 (when inspection enters).

Significance

The result. The theorem turns a POMDP into a finite list of explicit policies. Each structure is a periodic plan that needs no belief updating: produce for $m^\dagger$ periods and replace; or inspect every $m^*$ periods and replace only if the machine is found bad. The thresholds tell when inspection is worth its cost, and the comparative statics of $m^\dagger$ and $m^*$ follow from the closed forms. The authors use the solution to justify common maintenance practices.

Formalizing it. The result is proved in the paper (main text §4, proofs in its e-companion, App. A); no part is machine-checked. The proofs of Theorems 1 and 2 argue geometrically from figures of convex curves in the plane ("the curve bends back", "all the points are still extreme points"). A formal development has to turn these into inequalities between piecewise-linear concave functions, and has to prove convergence of value iteration to the stated sets. The implicit thresholds of part (3) were not checked numerically when this mission was planned. Parts (1) and (2) and Theorem 1 were.

Difficulty

Verifying that a candidate set $U$ is a fixed point is not enough: the goal asserts that value iteration from zero converges to it, so uniqueness of the bounded fixed point must be proved (a contraction argument in the supremum norm over the simplex). More importantly, finding the frontier requires knowing which points of the infinite production sequence are extreme, which depends on the location of the anchor relative to the curve $\{\mathbf u_i:i\ge0\}$ (Fig. 5 of the paper, five subcases). The natural induction on $m$ fails because $f$ is not monotone: its least minimizer $m^\dagger$ must be located through the unimodality of the real extension (Proposition 4). In part (3) the thresholds $\hat c_1,\hat c_2$ are defined implicitly, and showing that the three regimes are ordered in $c^I$ requires monotonicity of the whole frontier in $c^I$ .

Formalization scope

Everything is defined in the namespace MaintPOMDP.Frontier. Vectors and beliefs are Fin 2 → ℝ (index 0 = good state); beliefs are unnormalized, $\boldsymbol\pi\ge0$ . The optimal solution is the limit of the support-function value iteration started from $W\equiv0$ , $w_F=0$ ; "the structure is X" means that this limit equals $\min$ over the points of row X of Table 1, with the failure cost of that row.

Standing assumptions: $0<\beta<1$ , $0<c^P<c^I<c^R<c^F$ (p. 14), and $0<\gamma_0<1$ , $0<\gamma_1<1$ , which the paper never states and which are added (the thresholds divide by $\gamma_1$ ). The hypothesis $\gamma_0\ne\gamma_1$ is added only to Lemmas 1, 3, 6, 7 and Proposition 4, whose printed formulas divide by $\gamma_1-\gamma_0$ ; $f$ and $g$ themselves are defined as solutions of the affine anchor equations, so Theorems 1 and 2 cover $\gamma_0=\gamma_1$ . Proposition 4 also carries the range of $c^R$ that its proof uses. " $m^\dagger=\arg\min f$ " is the least minimizer, and its existence is part of the conclusion. In Theorem 2, the indices $n_R,n_I$ of Table 1 are existential and extreme-point exactness is not asserted for the $I[PR]$ and $[PIR]$ rows (Table 1's $I[PR]$ row conflicts with the paper's Proposition 8). It is asserted in Theorem 1. In part (3) the thresholds are chosen before $c^I$ and the claims hold for every $c^I\in(c^P,c^R)$ .

Trivializing readings are ruled out: the value function is the limit of the iterates, not an arbitrary fixed point or a junk limit; identities hold for every belief $\boldsymbol\pi\ge0$ , not only at vertices; every frontier set is given by formulas, so no extra points can be slipped in; minimizers are asserted, not assumed; and thresholds involving $\gamma_0/\gamma_1$ are evaluated with $\gamma_1>0$ .

A complete development needs convergence of value iteration for a monotone contraction on bounded functions over the cone $\boldsymbol\pi\ge0$ , explicit solutions of two-dimensional linear recurrences, and lemmas on lower envelopes of finitely many linear functions in two variables. These are reusable beyond this mission, for other two-state POMDPs. Contributions of any milestone, of the γ0 = γ1 closed forms (App. B), or of a proof of Theorem 1 alone are welcome.

Selected references

H. Zhang, W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4547 (read as SSRN 2945049, https://ssrn.com/abstract=2945049)
H. Zhang, Partially Observable Markov Decision Processes: A Geometric Technique and Analysis, Operations Research 58(1), 2010. https://doi.org/10.1287/opre.1090.0697
R. D. Smallwood, E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5), 1973. https://doi.org/10.1287/opre.21.5.1071
S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), 1971. https://doi.org/10.1287/mnsc.17.9.587

19 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Privacy Rights and Data Security: GDPR and Personal Data Markets 1: With Privacy Rights the Monopoly Equilibrium Has Four Breach-Cost Regimes Separated by c = δσ/2, δσ/√2 and δσResearch Paper

Motivation

The European Union's General Data Protection Regulation (GDPR, 2018) and the California Consumer Privacy Act give consumers privacy rights over the personal data that firms collect: data may be collected only with explicit consent (opt-in), consent is separated from the purchase itself, and a consumer may later have her data deleted (erasure, the "right to be forgotten"). The same regulations carry a data security mandate, because data held by a firm is exposed to breaches. Regulators, firms and economists want to know how these rights change what data is collected, what prices are charged, and who gains.

Ke and Sudhir (SSRN 3643979; published in Management Science, 2022, doi:10.1287/mnsc.2022.4614) build a two-period model in which a firm sells a basic good, may collect a consumer's data with her consent, and uses the data to sell a personalized good in the second period. Consumers trade off the personalization benefit against the expected cost of a data breach. This mission formalizes the paper's first main result, Proposition 1: the equilibrium of the monopoly market with privacy rights. The companion mission (number 2 of this series) formalizes the benchmark without privacy rights.

Setting

A monopolist faces a unit mass of consumers whose valuation $v$ of the basic good is uniform on $[0,1]$ . A consumer values the personalized good at $(1+\kappa)v$ , where $\kappa\in\{\kappa_L,\kappa_H\}$ with probability $1/2$ each and $\kappa_H>\kappa_L>0$ . Write

\mu=\frac{\kappa_H+\kappa_L}{2},\qquad \sigma=\frac{\kappa_H-\kappa_L}{2}.

A consumer learns her $\kappa$ only after the first period, and the firm never learns it. Both sides discount the second period by $\delta\in(0,1]$ . Each period in which the firm holds a consumer's data costs her an expected breach cost $c\ge0$ .

Period 1. The firm posts a price $p_1$ . Each consumer chooses among not buying, buying without opting in, and buying and opting in. Opting in reveals $v$ to the firm and costs $c$ .

Period 2. The firm posts a basic price $p_2$ and offers each opted-in consumer a personalized price $r(v)$ . A consumer who did not opt in buys the basic good iff $v\ge p_2$ ; she never opts in in the last period. An opted-in consumer either keeps her data and buys the personalized good, with utility $(1+\kappa)v-r(v)-c$ , or erases her data and takes $\max\{v-p_2,0\}$ .

An equilibrium is a profile $(p_1,\ p_2(\cdot),\ r(\cdot,\cdot),\ \text{choice}(\cdot,\cdot))$ in which every personalized price $r(v,q)$ maximizes the expected revenue from consumer $v$ at basic price $q$ ; after every first-period price $p_1$ , the basic price $p_2(p_1)$ maximizes the firm's second-period profit; after every $p_1$ , every consumer's first-period action is optimal; and $p_1$ maximizes the firm's total profit over all real prices. The paper also imposes Assumption 1:

\mu\ \ge\ \max\Big\{(3+\delta)\sigma,\ \tfrac12+(2+\delta)\sigma\Big\}.

Formalization targets

Goal: Proposition 1

Under Assumption 1, an equilibrium exists with the following outcome in each regime. The constants $v_1^*$ and $P_1^*$ are those of the paper's appendix.

A. $0\le c\le\delta\sigma/2$ : $p^*_{1M}=P_1^*$ and $p^*_{2M}=1$ . Consumers with $v\ge v_1^*$ opt in and then buy the personalized good at $(1+\mu-\sigma)v-c$ . Consumers with $v<v_1^*$ never buy.
B. $\delta\sigma/2<c\le\delta\sigma/\sqrt2$ : $p^*_{1M}=1/2$ and $p^*_{2M}=1$ . Consumers with $v\ge c/(\delta\sigma)$ opt in and pay $(1+\mu-\sigma)v-c$ . Those with $1/2\le v<c/(\delta\sigma)$ buy only in period 1. The rest never buy.
C. $\delta\sigma/\sqrt2<c<\delta\sigma$ : $p^*_{1M}=p^*_{2M}=1/2$ . Consumers with $v\ge c/(\delta\sigma)$ opt in and pay $(\mu-\sigma)v+1/2-c$ . Those with $1/2\le v<c/(\delta\sigma)$ buy the basic good in both periods. The rest never buy.
D. $c\ge\delta\sigma$ : no one opts in, $p^*_{1M}=p^*_{2M}=1/2$ , and a consumer buys in each period iff $v\ge1/2$ .

Milestones

The equilibrium personalized price, eqs. (1)–(2):

r^*_M(v,p_2)=(\mu-\sigma)v+\min\{v,p_2\}-c,

which is optimal whenever $2(\kappa_Lv-c)\ge\kappa_Hv-c\ge0$ , a condition Assumption 1 guarantees above the opt-in threshold.

The opt-in threshold, eq. (4):

v^*_M(p_1)=\max\Big\{\frac{c}{\delta\sigma},\frac{p_1+c}{1+\delta\sigma}\Big\}.

The second-period basic price, eq. (3): $p^*_{2M}(p_1)=1/2$ if $v^*_M(p_1)\ge1/\sqrt2$ , and $1$ otherwise.

The remaining milestones are the identification of the firm's profit with the reduced first-period profit of p. 15, and the three cases of the appendix proof that locate its maximizer.

Significance

Proposition 1 is the basis of the paper's comparative statics and policy conclusions. The comparison with the benchmark (Proposition 2) shows when privacy rights raise or lower opt-in, profits and consumer surplus. Corollary 3 shows that under privacy rights, opt-in and profit fall strictly with the breach cost. In the paper's interpretation, the result explains how data-security investment and the rights themselves interact: privacy rights let consumers avoid the hold-up problem of sharing data before knowing its value to them.

The result is proved on paper in the appendix, by reducing the game to a piecewise-quadratic maximization. It has not been machine-checked. A formal proof adds a fully specified equilibrium concept with optimality at every history and an explicit treatment of tie-breaking and knife-edge regimes. It also corrects one misprint in the SSRN text (the price in case B(i)). This is the platform's first two-period data-market game with opt-in and erasure; existing privacy items are one-shot models.

Difficulty

The difficulty is that the goal is a statement about a game, not about the closed forms. A solver must exhibit strategies at every history, including first-period prices far from equilibrium and arbitrary basic prices. They must then show that the consumers' choices form a threshold set whose measure and integrals are the ones the reduced profit assumes.

The tempting shortcut is to read eq. (2) as the firm's personalized price everywhere. Eq. (1) shows it is optimal only in case (i); for small $v$ the firm prefers to price only to the high type or to let both types erase. The equilibrium survives because no such consumer opts in, which must be shown from the consumers' side. The global maximization of the first-period profit over all real $p_1$ involves a function with kinks at $p_1=c/(\delta\sigma)$ , at the price where $v^*_M(p_1)=1/\sqrt2$ , and where $v^*_M(p_1)$ reaches $1$ . Both halves of Assumption 1 are used in comparing its pieces.

Formalization scope

Parameters are a structure Params with fields kL, kH, d ( $\delta$ ) and c; $\mu$ , $\sigma$ , the standing assumptions ( $0<\kappa_L<\kappa_H$ , $0<\delta\le1$ , $0\le c$ ) and Assumption 1 are definitions, and every theorem carries both predicates as hypotheses. Consumers are $v\in[0,1]$ with Lebesgue measure. Expectations over $\kappa$ are averages of the two types. All quantities are real numbers, and prices range over all of $\mathbb R$ .

Committed conventions:

An indifferent consumer buys.
An opted-in consumer keeps her data on a tie.
"No basic good is offered" is the basic price $1$ .
The goal asserts existence of an equilibrium with the stated outcome, not uniqueness, which the paper does not claim.
The knife-edge $c=\delta\sigma/\sqrt2$ belongs to B, as in the proposition.
In B(i) the formal statement uses the price $(1+\mu-\sigma)v-c$ that eq. (2) gives when no basic good is sold; the SSRN text prints C's price there.

Profits are integrals over the sets of consumers defined by the profile's own choices. A formalization that defined profits by the paper's closed forms would be trivial and is excluded. So are optimality checked only on the equilibrium path, a dropped Assumption 1, a missing bullet of the proposition, and a uniqueness claim. A sorry-free check confirms that the hypotheses are satisfiable at the paper's figure point $\kappa_L=4$ , $\kappa_H=6$ , $\delta=0.8$ .

The development needs interval integrals and Lebesgue measure of intervals on $\mathbb R$ , and elementary real inequalities with square roots. The reduced-profit identity (consumers' optimal choices form threshold sets up to null sets) is the reusable core and would serve the benchmark mission too. Proofs of individual milestones are welcome independently.

Selected references

T. Tony Ke and K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, SSRN working paper 3643979 (pdfTeX build 2022-09-14). https://ssrn.com/abstract=3643979
T. Tony Ke and K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4614
Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

12 thms3 active usersReviewed

Linear algebra Quantum Information Theoretical Computer Science·Captain: mikedeng1

Learning Stabilizer States by Bell Sampling: Algorithm 1 Identifies an n-Qubit Stabilizer State from 5n+2 Copies, Failing with Probability at Most 2⁻ⁿResearch Paper

Motivation

Determining an unknown quantum state of $n$ qubits to good accuracy requires, in general, a number of copies of the state exponential in $n$ ; this follows from Holevo's theorem. One way around this barrier is to restrict the class of states. Stabilizer states are the natural candidate: they are the states produced from $|0^n\rangle$ by Clifford circuits, they underlie quantum error-correcting codes, measurement-based computation and randomized benchmarking, and there are $2^{\Theta(n^2)}$ of them, so $\Omega(n)$ copies are necessary to identify one.

Timeline.

Aaronson and Gottesman (2008, Identifying stabilizer states, talk, http://pirsa.org/08080052/) described a procedure identifying an unknown stabilizer state from $O(n^2)$ copies with single-copy measurements, and a variant using $O(n)$ copies with measurements collective across all copies.
Low (2009, arXiv:0907.2833) showed that a Clifford unitary can be identified from $O(n^2)$ uses, or $O(n)$ with access to its inverse.
Rocchetto (2017, arXiv:1705.00345) showed that stabilizer states are PAC-learnable efficiently.
Montanaro (2017, arXiv:1707.04012) gave the algorithm of this mission: $O(n)$ copies, collective measurements on at most two copies at a time, failure probability exponentially small in $n$ . Zhao, Pérez-Delgado and Fitzsimons obtained a related $O(n)$ -copy algorithm for graph states independently (arXiv:1510.03742).

Bell sampling became a standard tool after this paper, for instance in stabilizer testing (Gross, Nezami and Walter, arXiv:1712.08628), so a machine-checked version of its analysis is a reusable base.

Setting

A state of $n$ qubits is a vector $\psi:\{0,1\}^n\to\mathbb C$ ; its complex conjugate $\psi^*$ is taken entrywise in the computational basis. The paper uses the four $2\times2$ matrices

\sigma_{00}=\begin{pmatrix}1&0\\0&1\end{pmatrix},\ \sigma_{01}=\begin{pmatrix}0&1\\1&0\end{pmatrix},\ \sigma_{10}=\begin{pmatrix}1&0\\0&-1\end{pmatrix},\ \sigma_{11}=\sigma_{10}\sigma_{01}=\begin{pmatrix}0&1\\-1&0\end{pmatrix},

which are the Pauli matrices up to the factor $-i$ on $\sigma_{11}$ . For a string $s\in\{0,1\}^{2n}$ , $\sigma_s=\sigma_{s_1s_2}\otimes\cdots\otimes\sigma_{s_{2n-1}s_{2n}}$ ; strings are added bitwise, $s\oplus t$ .

The Bell basis of $\mathbb C^4$ is $|\sigma_{00}\rangle=\frac1{\sqrt2}(|00\rangle+|11\rangle)$ , $|\sigma_{01}\rangle=\frac1{\sqrt2}(|01\rangle+|10\rangle)$ , $|\sigma_{10}\rangle=\frac1{\sqrt2}(|00\rangle-|11\rangle)$ , $|\sigma_{11}\rangle=\frac1{\sqrt2}(|01\rangle-|10\rangle)$ . Bell sampling on $2n$ qubits $A_1,\dots,A_n,B_1,\dots,B_n$ measures each pair $A_iB_i$ in the Bell basis and returns a string $r\in\{0,1\}^{2n}$ . On two copies $|\psi\rangle|\psi\rangle$ (first copy on the $A$ 's) the outcome $r$ has probability $p_\psi(r)=|\langle\sigma_r|\,\psi\otimes\psi\rangle|^2$ .

A stabilizer state is $\psi=U|0^n\rangle$ for a Clifford unitary $U$ (a unitary normalising the Pauli group). Its stabilizer set $T(\psi)\subseteq\mathbb F_2^{2n}$ is the set of strings $t$ for which $\psi$ is an eigenvector of $\sigma_t$ , i.e. those $\sigma_t$ that lie in the stabilizer group of $\psi$ up to a phase.

Algorithm 1. Bell-sample two fresh copies to get $r_0$ ; repeat $2n$ times to get $r_1,\dots,r_{2n}$ ; find a basis $B$ of $\operatorname{span}\{r_i\oplus r_0\}$ ; for each element of $B$ measure one copy of $\psi$ in the eigenbasis of the corresponding (Hermitian) Pauli matrix $M$ to learn whether $M|\psi\rangle=+|\psi\rangle$ or $-|\psi\rangle$ . It uses $5n+2$ copies.

Formalization targets

Goal: Theorem 1, explicit form

For every $n$ and every $n$ -qubit stabilizer state $\psi$ , with the $2n+1$ Bell samples independent,

\Pr\bigl[\operatorname{span}\{r_i\oplus r_0:1\le i\le 2n\}=T(\psi)\bigr]\ \ge\ 1-2^{-n},

and for every basis $b_1,\dots,b_n$ of $T(\psi)$ with Hermitian Paulis $M_j$ , each $M_j\psi=\pm\psi$ and every vector with the same eigenvalues under all $M_j$ is a scalar multiple of $\psi$ . Together: Algorithm 1 identifies $\psi$ except with probability at most $2^{-n}$ .

Milestones

$\sigma_s\sigma_t=\pm\sigma_{s\oplus t}$ .
Lemma 2: $p_\psi(r)=|\langle\psi|\sigma_r|\psi^*\rangle|^2/2^n$ .
The Bell-sampling probabilities of a unit vector sum to $1$ .
For a stabilizer state, $|\psi^*\rangle=c\,\sigma_{10}^{\otimes S}|\psi\rangle$ with $|c|=1$ .
Eqn (1): $p_\psi(r)=|\langle\psi|\sigma_r\sigma_{10}^{\otimes S}|\psi\rangle|^2/2^n$ .
$T(\psi)$ is an $n$ -dimensional subspace of $\mathbb F_2^{2n}$ .
$\langle\psi|\sigma_t|\psi\rangle=0$ for $t\notin T(\psi)$ .
$p_\psi$ is uniform on a coset $\{t\oplus s:t\in T\}$ .
For two independent outcomes, $r_1\oplus r_2$ is uniform on $T$ .
$T$ and the signs on a basis of $T$ determine $\psi$ up to a scalar.
$2n$ uniform samples of an $n$ -dimensional $\mathbb F_2$ -space fail to span it with probability at most $2^{-n}$ .

Significance

The theorem gives a learning algorithm whose copy complexity $O(n)$ is optimal and whose measurements are simple: one Bell measurement on corresponding qubits of two copies. Its analysis isolates a structural fact about stabilizer states, that Bell sampling on two copies produces a uniformly random element of a coset of the stabilizer subspace, which is the engine of later work on stabilizer testing and on learning states with few non-Clifford gates.

The result is proved in the paper; no machine-checked proof of it is known. A complete formalization adds: the stabilizer formalism in a form usable from the definition " $U|0^n\rangle$ for a Clifford $U$ " (the subspace $T$ , its dimension, vanishing expectations off $T$ , determination by signs); the conjugation identity, which the paper takes from a normal form cited from the literature; and the probabilistic bookkeeping of the algorithm with its exact constants.

Difficulty

The probability calculations (Lemma 2, eqn (1), the union bound) are finite sums. The difficulty lies in the stabilizer structure. The platform's definition of a stabilizer state is the image of $|0^n\rangle$ under a Clifford unitary; from it one must derive that the strings whose $\sigma_t$ fixes $\psi$ up to phase form an $n$ -dimensional subspace, that all other Pauli expectations vanish, and that $\psi^*$ differs from $\psi$ by a diagonal Pauli. The paper obtains the last fact from the Dehaene–De Moor normal form $\psi\propto\sum_{x\in A}i^{\ell(x)}(-1)^{q(x)}|x\rangle$ , a cited theorem whose proof is not on the page; formalizing either that normal form or a direct substitute is the central step. The natural shortcut, treating $T$ as given with "uniform outcomes on $T$ " as a hypothesis, proves only the counting lemma and is ruled out below.

Formalization scope

States are StabilizerRank.QState n = (Fin n → Bool) → ℂ and stabilizer states are StabilizerRank.IsStabilizerState (published platform definition, referenced). Qubit $i$ is coordinate $i$ , false $=0$ .
Strings $\{0,1\}^{2n}$ are encoded as Fin n → ZMod 2 × ZMod 2, coordinate $i$ the pair $(s_{2i-1},s_{2i})$ of qubit $i$ ; $\oplus$ is +.
$\sigma_{11}$ is the page's $\begin{pmatrix}0&1\\-1&0\end{pmatrix}$ , not the Pauli $Y$ . The "corresponding Pauli matrix" of step 5 is the Hermitian $(-i)^{\#\{i:t_i=11\}}\sigma_t$ ; the page does not fix this phase.
The Bell outcome law is the Born rule with $\psi(x)\psi(y)$ the amplitude of $|\psi\rangle|\psi\rangle$ at $|x\rangle_A|y\rangle_B$ .
Algorithm 1 is modelled by its outcome law: the $2n+1$ samples are independent (fresh copies), and an event has probability $\sum \mathbf 1_E\,p_\psi(r_0)\prod_i p_\psi(r_i)$ . Step 5 is deterministic once a basis of $T$ is known, and is stated as a property of every such basis.
The explicit constants of p. 2 replace " $O(n)$ " and "exponentially small": $2n+1$ Bell samples, success probability at least $1-2^{-n}$ (the page's "fails with probability at most $2^{-n}$ ", in a form that a mis-normalised outcome law cannot satisfy). The count $5n+2$ and "at most two copies at a time" are properties of the model, not separate clauses. The running time $O(n^3)$ is not formalized.
Lemma 2 is stated for every vector, not only unit vectors (the identity is homogeneous). The conjugation identity carries a unit phase $c$ , which the page omits. " $\langle\psi|M|\psi\rangle=0$ for $M\notin G$ " is stated for strings outside $T$ .
Ruled out: $T$ as a hypothesis (it is always computed from $\psi$ ), dropping the reference sample $r_0$ or the independence of the samples, a degenerate outcome law, and reading "identifies" as "the samples span $T$ " without the sign step.

Needed infrastructure: Kronecker-product manipulations of $\sigma_s$ indexed by bit strings, the Bell basis as an orthonormal basis of $(\mathbb C^2\otimes\mathbb C^2)^{\otimes n}$ , the stabilizer formalism over $\mathbb F_2^{2n}$ , and counting hyperplanes of finite $\mathbb F_2$ -spaces. The stabilizer-formalism layer and the union bound are reusable beyond this mission. Contributions to any milestone are welcome, in particular direct proofs of milestones 4, 6 and 7 from the Clifford definition.

Selected references

A. S. Holevo, Bounds for the quantity of information transmitted by a quantum communication channel, Problems of Information Transmission 9:177–183, 1973.
D. Gross, S. Nezami and M. Walter, Schur–Weyl duality for the Clifford group with applications: property testing, a robust Hudson theorem, and de Finetti representations, Comm. Math. Phys. 385:1325–1393, 2021. https://arxiv.org/abs/1712.08628
A. Montanaro, Learning stabilizer states by Bell sampling, arXiv preprint, 2017. https://arxiv.org/abs/1707.04012
S. Aaronson and D. Gottesman, Identifying stabilizer states, PIRSA talk, 2008. http://pirsa.org/08080052/
R. Low, Learning and testing algorithms for the Clifford group, Phys. Rev. A 80:052314, 2009. https://arxiv.org/abs/0907.2833
A. Rocchetto, Stabiliser states are efficiently PAC-learnable, arXiv preprint, 2017. https://arxiv.org/abs/1705.00345
L. Zhao, C. Pérez-Delgado and J. Fitzsimons, Fast graph operations in quantum computation, Phys. Rev. A 93:032314, 2016. https://arxiv.org/abs/1510.03742
J. Dehaene and B. De Moor, Clifford group, stabilizer states, and linear and quadratic operations over GF(2), Phys. Rev. A 68:042318, 2003. https://arxiv.org/abs/quant-ph/0304125
M. Van den Nest, Classical simulation of quantum computation, the Gottesman–Knill theorem, and slightly beyond, Quantum Inf. Comput. 10:258, 2010. https://arxiv.org/abs/0811.0898
S. Aaronson, The learnability of quantum states, Proc. R. Soc. A 463:3089, 2007. https://arxiv.org/abs/quant-ph/0608142

14 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization I: The Largest-Coordinate Strategy Keeps the Stochastic Chasing 0 Game within 2(c+R)log(4mk²/p)Research Paper

Motivation

Cutting plane methods minimize a convex function, or find a point in a convex set, using only a separation oracle: a routine that, given a query point, either certifies it is good or returns a halfspace containing the target. Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) gave a cutting plane method for a convex set in $\mathbb R^n$ inside a box of radius $R$ that uses an expected $O(n\log(nR/\epsilon))$ oracle calls and $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time, improving on the $O(n^{\omega+1}\log(nR/\epsilon))$ additional time of Vaidya's method from over 25 years earlier, and derived from it faster algorithms for submodular function minimization, matroid intersection and submodular flow.

The speed-up depends on not recomputing the leverage scores of the current constraint matrix from scratch at every step. The algorithm maintains approximations and refreshes a few of them per step. Section 7.2 of the paper isolates the bookkeeping question this raises as a two-player game, the stochastic chasing $\vec 0$ game, and shows that a simple greedy strategy keeps the accumulated error small. The game is self-contained and has nothing to do with convexity: it is a statement about a random walk in $\mathbb R^m$ that is partially reset at every step.

Setting

Fix a dimension $m\ge1$ and constants $c>0$ , $R>0$ . For $\vec v\in\mathbb R^m$ , $\|\vec v\|_\infty=\max_i|v_i|$ and $\|\vec v\|_2=(\sum_iv_i^2)^{1/2}$ .

A point starts at $\vec x^{(1)}=\vec 0$ . Each round $k=1,2,\dots$ runs as follows (Algorithm 4).

A stochastic adversary chooses a probability distribution $\mathcal D^{(k)}$ on $\mathbb R^m$ with mean $\vec 0$ and $\|\vec\Delta\|_2\le c$ for every $\vec\Delta$ in its support.
The adversary chooses an observation $\vec y^{(k)}$ with $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$ .
The player chooses a coordinate $i^{(k)}$ , knowing only $\vec y^{(k)}$ : neither $\vec x^{(k)}$ , nor $\mathcal D^{(k)}$ , nor the step.
A step $\vec\Delta^{(k)}$ is drawn from $\mathcal D^{(k)}$ and the point moves to

x^{(k+1)}_{i^{(k)}}=0,\qquad x^{(k+1)}_j=x^{(k)}_j+\Delta^{(k)}_j\quad(j\ne i^{(k)}).

The adversary may use everything that has happened so far to make its choices. The player wants to keep $\vec x^{(k)}$ near $\vec 0$ in $\|\cdot\|_\infty$ ; the adversary wants to push it away. The largest-coordinate strategy is $i^{(k)}=\operatorname{argmax}_i|y^{(k)}_i|$ : reset the coordinate that looks largest.

Formalization targets

Goal: Theorem 34

If the player uses the largest-coordinate strategy, then for every $p\in(0,1]$ , with probability at least $1-p$ ,

\|\vec x^{(k)}\|_\infty\le2(c+R)\log\big(4mk^2/p\big)\qquad\text{for all }k\ge1.

The bound holds simultaneously for all rounds, against every adaptive adversary, and grows only logarithmically in $k$ , in $m$ and in $1/p$ .

Milestones

The milestones are the steps that the paper's proof of Theorem 34 (pp. 43–44) displays:

the exponential inequality $e^x\le1+x+\tfrac{x^2}{2}e^{|x|}$ and its consequence $e^{\alpha x+\alpha\delta}\le e^{\alpha x}+\alpha\delta e^{\alpha x}+\tfrac12\alpha^2\delta^2e^{\alpha x+|\alpha|c}$ for $|\delta|\le c$ ;
the one-step drift bound for the potential $\Phi(\vec x)=\sum_ie^{\alpha x_i}+\sum_ie^{-\alpha x_i}$ :

\mathbb E_{\vec\Delta\sim\mathcal D}\,\Phi(\vec x+\vec\Delta)\le\Phi(\vec x)+\alpha^2e^{\alpha c}c^2\eta,\qquad\eta=\max\big(\max_ie^{\alpha x_i},\max_ie^{-\alpha x_i}\big);

the choice $\alpha=1/(2(c+R))$ , for which $e^{2\alpha(c+R)}(\alpha(c+R))^2\le1$ and $\alpha^2e^{\alpha c}c^2\le e^{-\alpha(R+c)}$ ;
the union-bound arithmetic $1-\sum_{k\ge1}2m/\lambda_k=1-\sum_{k\ge1}p/(2k^2)\ge1-p$ for $\lambda_k=4mk^2/p$ .

Significance

Within the paper, Theorem 34 is what lets the cutting plane method keep its leverage-score estimates within a bounded multiplicative error while refreshing only one estimate per step; this is one of the ingredients behind the $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time. The game reappears whenever an algorithm tracks many slowly drifting quantities with noisy observations and can afford to recompute only a few of them exactly per step, which makes the statement useful beyond this paper.

None of the statements in this mission has a machine-checked proof. The theorem is published with a proof. The mission asks for a formal proof of the statement exactly as published, with the constant $4$ inside the logarithm. A formal proof of the milestones alone would already give a reusable exponential-potential toolkit for adaptive random processes in $\mathbb R^m$ .

Difficulty

The point process is not a martingale: the player's resets depend on a noisy observation, the adversary is adaptive, and the reset can hit a coordinate that is up to $2R$ smaller in absolute value than the largest one. Per-coordinate tail bounds do not suffice, because the adversary may concentrate its moves on whichever coordinates the player is not resetting. A bound that holds for all $k$ at once, with only logarithmic dependence on $k$ , has to control all coordinates jointly. Establishing such joint control, with the specific constant $4$ inside the logarithm, against the most adversarial interaction between the observation error $R$ and the step size $c$ , is where the work lies.

Formalization scope

Probability model. The randomness is a probability space $(\Omega,\mu)$ with a filtration $(\mathcal F_k)_{k\ge0}$ . The adversary's adaptive choice of $\mathcal D^{(k)}$ is modelled by the conditional law of the step: each coordinate of the step has conditional mean $0$ given the past, the step is measurable with respect to the next $\sigma$ -algebra, and $\sum_i\Delta_i^2\le c^2$ holds everywhere. The observation $\vec y^{(k)}$ is measurable with respect to the current $\sigma$ -algebra, so it is fixed before the step is drawn, and $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$ holds on the actual trajectory.
Indexing. Coordinates are Fin m (0-based), with $m\ge1$ . Lean round $k\in\mathbb N$ is the paper's round $k+1$ , so the goal's bound reads $\log(4m(k+1)^2/p)$ ; at Lean round $0$ the point is $\vec 0$ .
Norms. $\|\cdot\|_\infty$ is Lean's sup norm on Fin m → ℝ. The step bound $\|\vec\Delta\|_2\le c$ is written as $\sum_i\Delta_i^2\le c^2$ , never as a sup-norm bound. The paper's prose once writes $\|\vec\Delta\|_2^2\le c$ ; Algorithm 4 and the proof use $\|\vec\Delta\|_2\le c$ , which is what is formalized.
Tie rule. $\operatorname{argmax}_i|y_i|$ breaks ties by the least index; the paper's theorem is claimed for any tie rule.
Constants. $c>0$ , $R>0$ (Algorithm 4), $0<p\le1$ , natural logarithm. The drift milestone adds $\alpha\ge0$ .
Not trivial by construction. The hypotheses are satisfiable by genuinely random adversaries (a fair-coin step of size $c$ is one), and the conclusion is a probability lower bound on an event, not a statement that holds vacuously; a formalization in which the observation could depend on the step, or in which the step bound were a sup-norm bound, would not be the paper's theorem.
Out of scope. Running time, the leverage-score application (Section 7.1, Theorem 31) and the rest of the cutting plane method.
Infrastructure. Conditional expectation with respect to a filtration, Markov's inequality and countable union bounds are in Mathlib. Supermartingale lemmas for nonnegative adapted processes, and the passage from a per-step drift inequality to a bound on the expected potential, are reusable well beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

Y. T. Lee, A. Sidford, S. C. Wong, A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization, FOCS 2015; arXiv:1508.04874v2, 2015. https://arxiv.org/abs/1508.04874
P. M. Vaidya, A new algorithm for minimizing convex functions over convex sets, FOCS 1989; Mathematical Programming 73 (1996) 291–341. https://doi.org/10.1007/BF02592216

6 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Privacy Rights and Data Security: GDPR and Personal Data Markets 2: Without Privacy Rights the Monopoly Equilibrium Has Three Breach-Cost Regimes and No Trade Once c ≥ 1 + δμ/(1 + δ)Research Paper

Motivation

Personal data lets a firm tailor its product to each customer, and the same data exposes the customer to the risk of a breach. The EU's General Data Protection Regulation (GDPR, 2018) and the California Consumer Privacy Act give consumers rights over that data. Data collection must be opted into separately from the purchase, and stored data must be erased on request. Ke and Sudhir (SSRN 3643979; Management Science 2022, doi:10.1287/mnsc.2022.4614) build a two-period model of a data-driven market to ask what these rights do to prices, purchases, profits and consumer surplus.

To isolate the effect of privacy rights, the paper needs the equilibrium of the same market without them. That equilibrium is its Proposition 2, the benchmark of §3.2. Every comparison in §3.3 (segmentation, prices, profit, consumer surplus, Corollaries 1–3) contrasts it with the equilibrium under privacy rights (Proposition 1, the companion mission of this series).

Setting

A monopolist sells a basic good over two periods. A unit mass of consumers has valuations $v$ uniform on $[0,1]$ , and the outside option is worth $0$ in each period. Firm and consumers discount the second period by $\delta\in(0,1]$ . A consumer values a personalized good at $(1+\kappa)v$ , where $\kappa$ equals $\kappa_L$ or $\kappa_H$ with probability $1/2$ each, $\kappa_H>\kappa_L>0$ . She learns her $\kappa$ only at the start of period 2, and the firm never observes it. Write

\mu=\frac{\kappa_H+\kappa_L}{2},\qquad \sigma=\frac{\kappa_H-\kappa_L}{2}.

The paper keeps Assumption 1, $\mu\ge\max\{(3+\delta)\sigma,\ \tfrac12+(2+\delta)\sigma\}$ , throughout.

No privacy rights. A first-period purchase reveals $v$ to the firm, and the consumer bears an expected breach cost $c\ge0$ in every period the firm holds her data. The data cannot be erased, so a first-period buyer bears $c$ in period 2 as well, whatever she does then. In period 2 the firm offers each past buyer the personalized good at a price $r(v)$ tailored to her valuation, and offers the basic good at a price $p_2$ to those who did not buy in period 1. A non-buyer who buys the basic good in period 2 also bears $c$ .

The firm chooses $p_1$ , then $p_2$ as a function of $p_1$ , and $r(v)$ . Consumers choose whether to buy in period 1, anticipating the second-period prices. An equilibrium satisfies four conditions:

$r(v)$ maximizes the expected revenue from a past buyer of valuation $v$ ;
after every first-period price, $p_2$ maximizes second-period profit given who bought in period 1;
after every first-period price, each consumer's first-period choice is optimal;
$p_1$ maximizes the firm's discounted profit over all real prices.

Formalization targets

Goal: Proposition 2

Let

T_1=\frac{2-\delta+2\delta\sigma}{2-\delta+2\delta\mu+2\delta\sigma},\qquad T_2=1+\frac{\delta}{1+\delta}\,\mu .

Under the standing assumptions and Assumption 1 there is an equilibrium with the following outcome in each regime.

A, $0\le c\le T_1$ : $p_1=P_1^B$ . Consumers with $v\ge\overline v_1^B$ buy in period 1 and then buy the personalized good at $r^B_M(v)=(1+\mu-\sigma)v$ . Those with $\overline v_1^B>v\ge\underline v_1^B$ buy only the basic good in period 2, at $p^B_{2M}=[P_1^B+\delta(1-\sigma)c]/(2-\delta+2\delta\sigma)$ . The rest never buy.
B, $T_1<c<T_2$ : $p_1=P_2^B$ . Consumers with $v\ge v_2^B$ buy in period 1 and then buy the personalized good at $(1+\mu-\sigma)v$ . Nobody else ever buys.
C, $c\ge T_2$ : nobody buys in either period.

The closed forms $P_1^B$ , $\overline v_1^B$ , $\underline v_1^B$ , $P_2^B$ , $v_2^B$ are the paper's (pp. 49–51).

Milestones

The appendix proof (pp. 48–51) supplies the steps, in order:

the optimal personalized price $r^B_M(v)=(1+\kappa_L)v$ ;
the second-period basic price (5), $p^B_{2M}(p_1)=(v^B_M(p_1)-c)/2$ ;
the first-period threshold (6) and its fixed point with (5);
the first-period price (7);
the regime without second-period sales and its price (8);
the conditions separating the regimes;
the corner regime at $p_1=\delta(\sigma-1)c$ , which merges with (8) into $P_2^B$ , $v_2^B$ .

Significance

Proposition 2 describes how a data market behaves when the firm owns the data. A consumer who buys is locked in: the firm extracts the low type's full valuation of personalization, and both types keep buying. Consumers anticipate this hold-up, so first-period demand shrinks. Once $c>T_1$ , the firm no longer sells the basic good in period 2, and the market becomes "now or never". Once $c\ge T_2$ it closes. The paper's comparisons of segmentation, prices, profit and consumer surplus with and without GDPR rights all start from these regimes.

Formalizing it gives the platform a two-period equilibrium with data lock-in. That equilibrium has its own fixed point: the consumers' threshold depends on the second-period price, and that price depends on the threshold. The result is proved in the paper, partly by first-order conditions ("It is easy to verify that the second-order optimality condition is satisfied"). It has not been machine-checked. Formalizing it also fixes a typo in eq. (7), which prints a stray $\kappa$ in the numerator of $P_1^B$ .

Difficulty

The obvious argument is the paper's: guess threshold strategies, solve the first-order conditions, read off the regimes. Each step is calculus, but an equilibrium must hold at every history, not only along the guessed path. The solver must exhibit $p_2$ and the consumers' choices after every first-period price, including prices at which nobody or everybody buys. It must show that the consumers' threshold and the firm's $p_2$ are a fixed point at each such price. It must then prove that the firm's first-period price is a global maximizer of a piecewise objective with a kink at $p_1=\delta(\sigma-1)c$ . On each side of the kink the objective is a different quadratic, and on the far sides the threshold leaves $[0,1]$ . The first-order conditions alone show none of this.

Formalization scope

The Lean development lives in the namespace GDPRDataMarkets.Benchmark. Its conventions:

Parameters. All quantities are real. The standing assumptions $0<\kappa_L<\kappa_H$ , $0<\delta\le1$ and $c\ge0$ are Params.Standing, and Assumption 1 is Params.Assumption1. The goal carries both as hypotheses.
Consumers and κ. Masses are the Lebesgue measure of subsets of $[0,1]$ . Expectations over $\kappa$ are averages of the two types.
Ties. An indifferent consumer buys: the personalized good iff $r(v)\le(1+\kappa)v$ , the basic good iff $v-p_2-c\ge0$ , and in period 1 the profile may choose either side at the single indifferent valuation.
Profits. The firm's profits are integrals and Lebesgue measures over the consumers' own choices. The paper's reduced closed forms appear only in the milestones.
Strategies. The firm's second-period price is a function of $p_1$ .
Existence only. Proposition 2 asserts existence of an equilibrium with the stated outcome, as the paper does; uniqueness is not posed.

A formalization in which the profits are the paper's closed forms rather than integrals over the consumers' optimal choices would make the goal calculus. So would one in which the second-period price or the consumers' choices are optimal only on the equilibrium path, or one that drops Assumption 1 or a bullet of the proposition. The statements here do none of these.

Assumption 1 enters the proof only through $\mu\ge3\sigma-1$ (p. 49), which makes $(1+\kappa_L)v$ the optimal personalized price. The milestone for that step assumes exactly this weaker condition.

Infrastructure needed: interval integrals of linear functions, Lebesgue measure of intervals, and maximization of concave quadratics. The equilibrium predicate is reusable for variants of this model, such as other breach-cost structures. Proofs of the milestones in any order are welcome.

Selected references

T. Tony Ke, K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, SSRN working paper 3643979 (pdfTeX build 2022-09-14). https://ssrn.com/abstract=3643979
T. Tony Ke, K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4614
Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Economics of Permissioned Blockchain Adoption I: Blockchain Adoption Raises Total Welfare for Large Horizontal Differentiation Yet Is Not an EquilibriumResearch Paper

Why blockchain adoption in supply chains is an economic question

A permissioned blockchain is a shared ledger that only invited parties may write to. In supply chains it is promoted as a way to make the provenance and quality of goods verifiable by the end consumer: a manufacturer who joins records how a good was produced, and consumers can read that record. Joining is costly, and the parties who pay the cost are not the parties who benefit most from the information. Whether such a technology is adopted at all is therefore a question about incentives, not engineering.

G. Iyengar, F. Saleh, J. Sethuraman and W. Wang, Economics of Permissioned Blockchain Adoption (SSRN 3602376; Management Science, 2023, DOI 10.1287/mnsc.2022.4532), build a stylised supply chain with vendors, price-competing manufacturers and consumers with an outside option, and show that welfare-improving adoption can fail to arise in equilibrium. This mission formalizes the first of the paper's two main results, Proposition 4.8, together with the welfare comparisons it rests on. A companion mission formalizes the second, the self-financing transfers of Proposition 4.9.

The supply chain

There are two vendors, of high and low quality $h > l \ge 0$ , and a set $M$ of $4m$ manufacturers, $m \ge 2$ of each type $(q_i,\xi_i) \in \{A,B\}\times\{h,l\}$ . A consumer of horizontal type $t_k$ obtains utility $H$ from a good with $q_i = t_k$ and $L$ otherwise, plus the vertical utility $\xi_i$ ; here $0 \le L < H$ , and $\Delta := H - L > 0$ measures horizontal differentiation. Consumers can always take an outside option $\varphi_k$ , drawn from a continuous distribution $G$ supported on $[0,\infty)$ . The high type vendor produces at cost $c_h(x) = \gamma x$ , $\gamma > 0$ ; the low type vendor at a strictly increasing convex cost $c_l$ with $c_l(0)=0$ and strictly increasing derivative $c_l'$ (Assumption 1, items 1–2).

Manufacturer $i$ may join the blockchain at cost $\chi_i > 0$ ( $a_i = 1$ ) or not ( $a_i = 0$ ). Three scenarios are compared: full adoption $F$ (all adopt), partial adoption $P$ (exactly the high type manufacturers adopt) and non-adoption $N$ . The paper's Proposition A.1 gives each scenario's equilibrium in closed form: every consumer's best manufacturer offers utility

u^F = u^P = H + h - \gamma,\qquad u^N = \tfrac{H+L+h+l}{2} - \gamma,

the low type vendor price is $\Psi^F_l = \max\{\gamma-(h-l),0\}$ , $\Psi^P_l = \max\{\gamma-(h-l)-\frac{H-L}{2},0\}$ , $\Psi^N_l = \gamma$ (the high type price is always $\gamma$ ), the low type market shares are $s^F_l = (c_l')^{-1}(\gamma-(h-l))$ , $s^P_l = (c_l')^{-1}(\gamma-(h-l)-\frac{H-L}{2})$ , $s^N_l = (c_l')^{-1}(\gamma)$ , and $s^X_h = G(u^X) - s^X_l$ . Manufacturers earn zero gross profit $\Pi$ in every scenario because of price competition.

Welfare in scenario $X$ is the sum $W^X = W^X_V + W^X_M + W^X_C$ of vendor welfare $W^X_V$ (revenue minus production cost of both vendors, (10)), manufacturer welfare $W^X_M = \sum_{i}(\Pi - \chi_i a^X_i)$ and consumer welfare $W^X_C = \mathbb E[\max\{u^X,\varphi\}]$ ((12)). The adoption game (8) lets each manufacturer choose $a_i$ to maximise $\Pi(a_i,a_{-i}) - \chi_i a_i$ . An adoption failure is a situation in which full adoption raises total welfare, $W^F > W^N$ , but is not an equilibrium of the adoption game.

Formalization targets

Goal: Proposition 4.8 (p. 19)

With $L$ fixed and $H = L + \Delta$ ,

\exists\,\underline\Delta\ \ \forall\,\Delta > \underline\Delta:\quad W^F(\Delta) > W^N(\Delta)\ \text{ and full adoption is not an equilibrium},

at every such $\Delta$ at which Assumption 1 holds. The threshold $\underline\Delta$ is left unspecified, as in the paper.

Milestones

Proposition 4.1 (pp. 15–16): $W^F_C \ge W^P_C > W^N_C$ .
Proposition 4.3 (p. 17): $W^F_M < W^P_M < W^N_M$ .
Proposition 4.4 (p. 17): $W^F_V,\ W^P_V < W^N_V$ .
Proposition 4.6 (p. 18): $W^F, W^P > W^N$ for all sufficiently large $\Delta$ ; at fixed $\Delta$ , $W^F < W^N$ once $\sum_{i\in M}\chi_i$ is large and $W^P < W^N$ once $\sum_{i:\xi_i=h}\chi_i$ is large.
Proposition 4.7 (p. 19): neither full nor partial adoption is an equilibrium.

What the result gives

The proposition isolates a mechanism: blockchain information raises consumer surplus, which grows without bound in $\Delta$ , while Bertrand competition prevents the manufacturers who pay for adoption from capturing any of it. The conclusion is a market failure that persists however valuable the information is, and it motivates the paper's transfer scheme (Proposition 4.9), in which a consumer access fee finances the adopters. The welfare comparisons of Propositions 4.1–4.6 are reusable on their own: they quantify who gains and who loses from information disclosure in a vertically and horizontally differentiated market.

The results are proved in the paper (App. A.2, pp. 33–36). None is machine-checked. This mission produces a checked version of the welfare comparisons and of the failure result in the reduced form described below; the proofs as printed use a density for $G$ and a second derivative of $c_l$ , neither of which the model assumes, so a formal proof has to avoid both.

Where the difficulty lies

The equilibrium part is light once the gross profit is zero. The substance is in the welfare comparisons. Consumer welfare is an expectation $\mathbb E[\max\{u,\varphi\}]$ of an outside option with an arbitrary continuous law: strict monotonicity in $u$ needs positive mass of $\varphi$ below $u^N$ , which is a consequence of Assumption 1 rather than an assumption, and the growth in $\Delta$ of $W^F - W^N$ has to be bounded below without a density. Vendor welfare involves the generalised inverse $(c_l')^{-1}$ , which is $0$ below $c_l'(0)$ : the comparison $W^F_V < W^N_V$ must handle the regime where the low type vendor's share collapses to zero and the regime where it is interior, and must obtain continuity of $c_l'$ from convexity rather than from a second derivative.

Formalization scope

The paper describes a signalling and pricing game but does not define its equilibrium concept precisely; Proposition A.1 states the outcomes and every proof in App. A.2 uses only those closed forms. The mission adopts the same reduced form, disclosed in every item: welfare is evaluated at Proposition A.1's prices, shares and utilities; the manufacturers' gross profit $\Pi$ is the constant $0$ for every adoption profile (the paper's statement in the proof of Proposition 4.3, p. 34); an equilibrium of the adoption stage is a pure Nash equilibrium of (8) with that payoff, expressed with AGT.IsPureNash from the published agt_games vocabulary. The signal accuracy is fixed at $\alpha = 1/2$ , as in the paper's main text.

Conventions: manufacturers are Fin 2 × Bool × Fin m (the Boolean records $\xi_i = h$ ), adoption profiles are Boolean functions, $G$ is ProbabilityTheory.cdf μ for a probability measure $\mu$ on $\mathbb R$ , $\Delta$ is an argument of every statement with $H = L + \Delta$ , and $(c_l')^{-1}(x) = \sup\{s \ge 0 : c_l'(s) \le x\}$ . The standing assumptions are bundled in Model.Standing: $m \ge 2$ , $0 \le L$ , $0 \le l < h$ , $\gamma > 0$ , $\chi_i > 0$ , $\mu$ an atomless probability measure with $\mu((-\infty,0)) = 0$ and positive mass on every interval $(a,b) \subseteq [0,\infty)$ , $c_l$ strictly increasing and convex on $[0,\infty)$ with $c_l(0) = 0$ and a strictly increasing derivative there. One hypothesis is added to the paper's: $\varphi$ has a finite mean, which the paper uses (its proof of Proposition 4.1 integrates $v\,p(v)$ ) without stating it. Assumption 1, item 3, depends on $\Delta$ through $H$ and is a hypothesis at each $\Delta$ ; it is satisfiable (for instance with $c_l(x) = x^2$ , $\varphi \sim \mathrm{Exp}(1)$ , $\gamma = 1/2$ , $h=1$ , $L=l=0$ , $\Delta = 4$ ) and monotone in $\Delta$ .

The formalization rules out the trivializing readings: the equilibrium predicate is concrete, not an abstract hypothesis; the integrals are of integrable functions, so no junk value $0$ enters; the inverse of $c_l'$ is the explicit supremum, not Function.invFun; and $L$ , not $H$ , is held fixed as $\Delta$ grows.

Needed infrastructure: expectations of $\max\{c,\varphi\}$ as a function of $c$ (monotonicity, growth), and the generalised inverse of a strictly increasing derivative of a convex function. Both are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the density and the second derivative of the printed proofs.

Selected references

G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, SSRN 3602376, version of 2022-08-19. https://ssrn.com/abstract=3602376
G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4532
N. Nisan, T. Roughgarden, É. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Ch. 1 (pure Nash equilibrium). https://doi.org/10.1017/CBO9780511800481

8 thms3 active usersReviewed

Completed

Economics Operations Research Optimization+1·Captain: mikedeng1

Gathering Information before Negotiation I: The Buyer's Optimal Information Acquisition Increases with Its Bargaining Power and First Increases, Then Decreases with the Seller's CostResearch Paper

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

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$ .
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.
Proof of Proposition 1, p. 30. Integration by parts: $U_b(\alpha)=\theta_b\int_c^{\infty}[1-G(v,\alpha)]\,dv-k(\alpha)$ .
Proof of Proposition 1, p. 30. $U_b$ has increasing differences in $(\alpha,\theta_b)$ .
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$ .
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

10 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Stall Economy: The Value of Mobility in Retail on Wheels II: Closed-Form Mean and Variance of the Within-Radius Repositioning Trip Length, Increasing in R and Decreasing in rResearch Paper

Motivation

Mobile retail stalls (self-driving or driver-operated vending vehicles that move to customers who order through a phone app) are studied by Cao and Qi in Stall Economy: The Value of Mobility in Retail on Wheels (Operations Research, 2022; the mission cites the authors' SSRN manuscript 3711896). A retailer partitions a city into service zones, one stall per zone, and must decide how densely to deploy stalls. That decision is made by continuous approximation: each zone is modelled as a small queueing system whose service time includes the stall's travel to the next customer. The mean and variance of that travel distance enter the Pollaczek–Khinchine waiting-time formula of an M/G/1 queue (the paper's equations (1a)–(2), p. 18), so closed forms for them are the input of the paper's whole deployment and pricing analysis (§4).

The paper considers two on-demand modes. In the door-to-door mode the stall drives to each customer's doorstep. In the within-radius mode each customer walks up to a distance $r$ toward the stall, and the stall only moves until the two are $r$ apart. This mission formalizes the travel-distance moments of both modes: Proposition 1 (door-to-door, p. 11) and Proposition 3 (within-radius, p. 18), whose proofs are in the paper's Appendix B (pp. 44–45 and 49–51).

Setting

All distances are Manhattan ( $\ell_1$ ) distances (p. 9): $|A-B| = |a_1-b_1| + |a_2-b_2|$ . A service zone is a square rotated by $45^\circ$ , a diamond, of Euclidean edge length $R>0$ ; the paper sets $R = R(\rho) = 1/\sqrt\rho$ for a stall density $\rho$ (p. 11). In Manhattan coordinates centred at the zone's centre,

\mathcal Z_R = \{(x,y) : |x|+|y| \le R/\sqrt2\},

which has area $R^2$ . Customers arrive uniformly on $\mathcal Z_R$ .

Fix a walking radius $0\le r\le R/\sqrt2$ . The inner diamond $\mathcal I_{R,r} = \{|x|+|y|\le R/\sqrt2-r\}$ lies $r$ inward from the boundary and has edge length $R-\sqrt2 r$ . The paper's model for the stall's position when a new customer arrives (proof of Proposition 3, p. 49) is: the stall $A$ is uniform on $\mathcal I_{R,r}$ , the customer $B$ is uniform on $\mathcal Z_R$ , and the two are independent. The repositioning trip length is

L_r = \max\{|A-B| - r,\ 0\},

and $L_0' = |A-B|$ denotes the untruncated distance. In the door-to-door case $r=0$ , both points are uniform on the zone and $L_0 = |A-B|$ . The variance is $\operatorname{Var}(L_r) = \mathbb E[L_r^2]-\mathbb E[L_r]^2$ .

The uniform law of the stall is the paper's Theorem 1 (the subject of the companion mission I), read in a continuum limit that the paper states informally (p. 17). This mission takes the uniform law as its model and does not depend on that limit.

Formalization targets

Goal: Proposition 3 (p. 18)

For all $R>0$ and $0\le r\le R/\sqrt2$ ,

\mathbb E[L_r] = \frac{7\sqrt2R^3-22R^2r+2\sqrt2Rr^2+12r^3}{15R^2},

\operatorname{Var}(L_r) = \frac{22R^6-22\sqrt2R^5r-140\sqrt2R^3r^3+400R^2r^4-48\sqrt2Rr^5-144r^6}{225R^4},

and both are non-decreasing in $R$ (on $\{R : r\le R/\sqrt2\}$ ) and non-increasing in $r$ (on $[0,R/\sqrt2]$ ).

Milestones, in the order of the proof

Proposition 1 (p. 11): $\mathbb E[L_0] = 7\sqrt2R/15$ and $\operatorname{Var}(L_0) = 22R^2/225$ .
$\mathbb E[L_0'] = \tfrac{7\sqrt2R}{15}-\tfrac{7r}{15}+\tfrac{2\sqrt2r^2}{15R}+\tfrac{2r^3}{15R^2}$ (p. 49).
$\mathbb P(L_0'\le r) = 2r^2/R^2$ and $\mathbb E[L_0'\,\mathbf 1\{L_0'\le r\}] = \tfrac23r\cdot 2r^2/R^2$ (p. 50).
$\mathbb E[X^2] = (R^2-\sqrt2Rr+r^2)/6$ for the horizontal component $X$ of $|A-B|$ (p. 50).
$\mathbb E[(L_0')^2] = (8R^4-8\sqrt2R^3r+7R^2r^2+r^4)/(15R^2)$ (p. 51).
$\mathbb E[(L_0')^2\,\mathbf 1\{L_0'\le r\}] = \tfrac12r^2\cdot 2r^2/R^2$ (p. 51).
Proposition 3(I) and 8. Proposition 3(II) on their own.

A supporting theorem, $\mathbb E[XY] = (3R^4-3\sqrt2R^3r+2R^2r^2+r^4)/(30R^2)$ (p. 50), is posed as well.

Significance

The result. With Proposition 3 the service time of the within-radius mode has explicit first and second moments, so the M/G/1 waiting time, the stall's daily travel, and the profit density of §4 are explicit functions of $(\rho, r)$ . Part (III) is the qualitative content the paper calls the first effect of avoiding the "last 100 meters": a longer customer walk shortens the stall's repositioning, and a larger zone lengthens it. Proposition 1 is the $r=0$ benchmark against which that saving is measured.

Formalizing it. The results are proved in the paper by direct integration; none is machine-checked. The proofs split the domain into several regions by the signs of coordinate differences and assert the values of the resulting polynomial integrals "by calculation". A formal proof checks every one of those integrals, the use of conditional expectations given the event $\{L_0'\le r\}$ , and the derivative signs behind part (III), which the paper states without verification on the whole range. The intermediate moments are useful on their own for other models with uniform demand on diamonds under the Manhattan metric.

Difficulty

The obvious route rotates the diamond by $45^\circ$ , where the $\ell_1$ distance becomes an $\ell_\infty$ distance and the zone a square, and then integrates. For $r=0$ this works cleanly. For $r>0$ the stall's square is smaller than the customer's, and $\max\{\cdot\}$ of two coordinate differences over two squares of different sizes splits into many polynomial pieces. The paper instead stays in the original coordinates and splits into six regions for $\mathbb E[XY]$ . Either way, the truncation at $r$ is the delicate step: it requires that the whole $\ell_1$ ball of radius $r$ around the stall lies in the zone, which is exactly why the stall is confined to the inner diamond. Part (III) is not a consequence of (I) and (II) by inspection: the derivative in $R$ of the mean vanishes at the boundary $r = R/\sqrt2$ , so the sign argument must be done on the closed range.

Formalization scope

Points are elements of ℝ × ℝ with Lebesgue measure. The definition StallEconomy.TripLength.Setting provides zone R, innerZone R r, the scale factor shrink R r = 1 − √2 r / R, the Manhattan distance l1, the trip length Lr r, the expectation E R r F, meanL R r and varL R r. The stall's uniform law is realised as $A = s\,U$ with $s = 1-\sqrt2r/R \in [0,1]$ and $U$ uniform on $\mathcal Z_R$ , which is the uniform law on $\mathcal I_{R,r}$ ; it covers the endpoint $r=R/\sqrt2$ , where the inner diamond is a single point, without dividing by $(R-\sqrt2r)^2$ . Thus

\mathbb E[F(A,B)] = R^{-4}\int_{\mathcal Z_R}\int_{\mathcal Z_R} F(s\,u, b)\,db\,du.

Standing conventions and deviations from the page:

every statement assumes $R>0$ , and the within-radius statements $0\le r\le R/\sqrt2$ , the paper's range;
$R$ is the edge length itself, not $1/\sqrt\rho$ ;
the conditional expectations given $\{L_0'\le r\}$ of pp. 50–51 are stated as truncated expectations $\mathbb E[\,\cdot\,\mathbf 1\{L_0'\le r\}]$ , since the conditioning event has probability $0$ at $r=0$ ;
the printed slips " $\mathbb P(L_0>r)$ " (p. 50, $L_0'$ meant) and the conditioning event " $L_0'^2\le r$ " (p. 51, $L_0'\le r$ meant) are corrected;
"increasing/decreasing" in part (III) is weak monotonicity.

Formalizations that would trivialize the goal are ruled out: meanL and varL are integrals, not the closed forms; part (III) is stated about those integrals, not about the polynomials; and nothing is restricted to $r=0$ or to a fixed $R$ .

A complete development needs iterated set integrals of piecewise polynomials over diamonds in ℝ × ℝ (Fubini on zone R, the change of variables $u\mapsto su$ ), and elementary calculus for part (III). Contributions of any of the moments, of a reusable lemma computing integrals of polynomials over diamonds, and of the monotonicity of the closed forms are all welcome. Proposition 2 of the paper, which is false as printed, is not claimed here.

Selected references

J. Cao and W. Qi, Stall Economy: The Value of Mobility in Retail on Wheels, Operations Research, 2022 (articles in advance). https://doi.org/10.1287/opre.2022.2404 ; manuscript: SSRN 3711896, https://ssrn.com/abstract=3711896
G. F. Newell, Dispatching policies for a transportation route, Transportation Science 5(1) 91–105, 1971 (origin of continuous approximation). https://doi.org/10.1287/trsc.5.1.91

10 thms3 active usersReviewed

Completed

Combinatorics Markov Chain Operations Research+1·Captain: mikedeng1

Stall Economy: The Value of Mobility in Retail on Wheels I: The Magnet Rule Makes the Rendezvous Chain Doubly Stochastic, and Its Stationary Distribution Is Uniform on the Inner DiamondResearch Paper

Motivation

A mobile retail stall can travel toward its next customer while that customer walks toward the stall. The customer's walking allowance changes where the stall stops, so it also changes the location from which the next trip begins. A useful trip-length calculation therefore needs a distribution for successive meeting points, not just a rule for one meeting. Cao and Qi study this question in a service zone assigned to one stall and give a particular magnet rule whose rendezvous chain has a simple stationary law Cao and Qi, §3.3. The result supplies the location model used in their analysis of repositioning distances.

The rule matters because different choices of a meeting point can produce different chains even when each choice lets the customer walk the same maximum distance. The paper's Theorem 1 establishes a distributional property of the specified rule, for every admissible finite grid. Its proof is in Appendix B, pp. 46–49 of the cited SSRN manuscript.

Setting

The service zone is a square drawn as a diamond in ordinary horizontal and vertical coordinates. Its edge length is $R$ in Euclidean distance, while stall and customer travel is measured in Manhattan distance. For the chain, use the paper's two edge coordinates, aligned with the lower edges of the zone. The full customer grid is $G_k=\{0,\ldots,k\}^2$ , so it contains $(k+1)^2$ points. A customer is uniform on this full grid.

Write $h=\phi k$ , where $\phi=r/(\sqrt2R)$ and $r$ is the customer's maximum walking distance. The paper chooses $k$ so that $h$ is an integer and assumes $2h\le k$ . The stall docks only at points of the inner diamond

\mathcal I_0=[h,k-h]^2\cap\mathbb Z^2.

The name “diamond” refers to its appearance in ordinary coordinates; in edge coordinates it is an axis-aligned square. A type-1 origin lies in $\mathcal I_1=[2h,k-2h]^2\cap\mathbb Z^2$ . The other origins in $\mathcal I_0$ are type 2. The closed small diamond around an origin $z_o=(x_o,y_o)$ is $\mathcal I(z_o)=[x_o-h,x_o+h]\times[y_o-h,y_o+h]\cap\mathbb Z^2$ .

The magnet rule maps the origin $z_o$ and next customer location $z_c$ to a rendezvous $z_d$ . The stall stays at $z_o$ when $z_c\in\mathcal I(z_o)$ . Otherwise, the location of $z_c$ in one of eight surrounding regions selects one of eight customer movement arrows. At a type-1 origin the head of that arrow is the rendezvous. At a type-2 origin the rule changes an arrow whose head would leave $\mathcal I_0$ , keeping the rendezvous inside it while preserving the customer's allowed walking distance. These are Definitions 1 and 2 of the paper pp. 14–16.

For $z_o,z_d\in\mathcal I_0$ , let $\mathcal A(z_o,z_d)$ be the customer grid locations sent from $z_o$ to $z_d$ . The transition probability is

\mathbb P(z_o,z_d)=\frac{|\mathcal A(z_o,z_d)|}{(k+1)^2}.

Thus the denominator is the number of possible customers, not the number of stall locations. Repeated independent customer locations produce a finite Markov chain on $\mathcal I_0$ .

Formalization targets

The goal is Theorem 1 p. 17. For every $k,h\in\mathbb N$ with $2h\le k$ , its first part says that $\mathbb P$ is doubly stochastic:

\sum_{z_d\in\mathcal I_0}\mathbb P(z_o,z_d)=1 \quad\text{and}\quad \sum_{z_o\in\mathcal I_0}\mathbb P(z_o,z_d)=1.

Its second part says that the stationary distribution is uniform on $\mathcal I_0$ . The formal target states existence and uniqueness: a probability vector $\pi$ is stationary for $\mathbb P$ if and only if $\pi(z)=1/|\mathcal I_0|$ for every state $z$ .

The milestones follow the source's intermediate assertions: the rule keeps the rendezvous in $\mathcal I_0$ at the prescribed customer distance; each row counts $(k+1)^2$ customers; the type-1 self-transition counts $(2h+1)^2$ customers; type-1 and type-2 columns each count $(k+1)^2$ incoming customer events; and every transition entry is positive. The last assertion supports the uniqueness clause.

Significance

A uniform stationary law replaces an unknown, history-dependent location distribution with one specified directly by the inner diamond. In the paper, that distribution is the location input for later within-radius repositioning calculations Cao and Qi, §§3.2–3.3. The result is specific to the magnet rule. It does not say that every reasonable meeting rule has a uniform stationary law.

The paper proves the finite-grid theorem in Appendix B. This mission asks for a machine-checked account of its exact finite combinatorial statement. The development will provide reusable definitions of the grid rule and its transition counts, while using an existing formal library interface for finite Markov chains. The theorem statements are open proof targets; a successful local compilation of their statements alone is not a proof.

Difficulty

Unit row sums follow from assigning each customer location to one next rendezvous. Unit column sums are subtler: fixing a destination and varying the origin gives overlapping sets of customer locations. Interior destinations and boundary destinations have different counts because a type-2 origin can redirect an arrow that would otherwise leave the allowed stall region. The source treats these as Case I and Case II on pp. 46–49. An interior-only count cannot establish the theorem for all of $\mathcal I_0$ , and positivity of every transition is a separate requirement for identifying the unique stationary law.

Formalization scope

Lean uses integer coordinate pairs for grid points and finite sets for $G_k$ , $\mathcal I_0$ , $\mathcal I_1$ , and $\mathcal I(z_o)$ . The region boundaries use the paper's strict or inclusive inequalities exactly. The permitted parameters are all natural numbers $k,h$ satisfying $2h\le k$ , including $h=0$ , $k=0$ , and $2h=k$ . In physical units $h=\phi k$ ; no division by $k$ occurs in the formal statements. When $k=0$ , there is one customer point and one state.

The matrix is computed from the paper's two-part magnet rule and uniform demand on the full grid. Defining it as a uniform matrix, using a nearest-point rule, dropping the type-2 correction, fixing one grid size, or proving only column sums would miss the target. The definition of $\mathcal A$ counts customer locations that induce a transition. This includes customers already inside $\mathcal I(z_o)$ in a self-transition, as required by the paper's Case I(IX) and row-count formula. The paper's separate Proposition 2 is not a claim of this mission because it is false as printed; none of these targets assumes it. The finite-grid theorem does not formalize the subsequent informal $k\to\infty$ statement.

The complete development needs finite-set counting, integer interval bounds, real-valued stochastic matrices, and the stationary-distribution interface of the published MarkovChain definition. Contributions proving any of the stated counting milestones or strengthening the finite-chain consequences are welcome. The paper's own proof is in Appendix B, pp. 46–49.

Selected references

J. Cao and W. Qi, Stall Economy: The Value of Mobility in Retail on Wheels, SSRN manuscript 3711896, 2022, §§3.2–3.3 and Appendix B, pp. 46–49. Manuscript.

11 thms3 active usersReviewed

Completed

Economics Operations Research Optimization+1·Captain: mikedeng1

Gathering Information before Negotiation II: Under a Uniform Prior and Linear Information Cost, the Seller's Expected Payoff Jumps Down at θs = 1 − θ̃, Up at c = c_l and Down at c = c_hResearch Paper

Motivation

In many trades the buyer does not know how much the good is worth to it, and can find out before negotiating: a firm commissions due diligence before an acquisition, a hospital pilots a device before negotiating its price, a household inspects a house before making an offer. Such information has two effects. It makes the trade decision better informed, which enlarges the total surplus, and it is paid for by the buyer alone, while the surplus it creates is shared through bargaining.

L. Guo, Gathering Information before Negotiation (SSRN 3930651; Management Science, doi:10.1287/mnsc.2022.4360), studies how this interaction shapes the seller's payoff. Its headline is a reversal: a seller with more bargaining power, or with a more valuable outside option, can be worse off, and a seller with a higher production cost can be better off. The reason is that the buyer's information choice reacts to these parameters, and the reaction can outweigh their direct effect. This mission formalizes that reversal for the paper's worked example, the uniform prior with a linear information cost.

Setting

A seller and a buyer negotiate over one unit of a good. The seller's cost is $c\in(0,1)$ . The buyer's value $u$ is unknown to both parties; the common prior is the uniform distribution $F(u)=u$ on $[0,1]$ , with mean $\hat u=1/2$ . The bargaining powers are $\theta_b\in(0,1)$ for the buyer and $\theta_s=1-\theta_b$ for the seller.

Before negotiating, the buyer chooses an informativeness $\alpha\in[\underline\alpha,\bar\alpha]$ , with $0<\underline\alpha<\bar\alpha<1$ . It then observes a truth-or-noise signal $w$ : with probability $\alpha$ it equals $u$ , and otherwise it is an independent draw from the prior. The buyer's posterior mean is $v=\alpha w+(1-\alpha)\hat u$ . The information cost is linear,

k(\alpha)=\bar k\,\frac{\alpha-\underline\alpha}{\bar\alpha-\underline\alpha},\qquad \bar k>0 .

If $v>c$ the parties trade and split the net surplus $v-c$ in the proportions $\theta_s:\theta_b$ ; otherwise they do not trade. The total ex ante surplus is

A(\alpha,c)=\mathbb E\big[(v-c)^+\big]=\int_0^1\max\Big\{\alpha w+\frac{1-\alpha}{2}-c,\;0\Big\}\,dw ,

and the buyer chooses $\alpha$ to maximise

U_b(\alpha)=\theta_b\,A(\alpha,c)-k(\alpha).

The optimal set $\alpha^*$ is the set of maximisers of $U_b$ on $[\underline\alpha,\bar\alpha]$ . The seller's equilibrium expected payoff is

U_s^*=\theta_s\,A(\alpha^*,c)\quad\text{(material cost)},\qquad V_s^*=c+\theta_s\,A(\alpha^*,c)\quad\text{(opportunity cost)}.

Write $\Delta(c)=A(\bar\alpha,c)-A(\underline\alpha,c)$ for the surplus gain of maximal information, and $\tilde\theta=\bar k/\Delta(c)$ when $\Delta(c)>\bar k$ , $\tilde\theta=1$ otherwise. For fixed $\theta_b$ , the cost thresholds $c_l\le 1/2\le c_h$ are the endpoints of the set of costs at which $\theta_b\Delta(c)>\bar k$ .

Formalization targets

Goal: Proposition 2 (p. 14), uniform prior

For every selection of optimal information levels:

$\theta_s\mapsto U_s^*$ and $\theta_s\mapsto V_s^*$ are nondecreasing on $(0,1-\tilde\theta)$ and on $(1-\tilde\theta,1)$ , and, if $\tilde\theta<1$ , drop strictly at $\theta_s=1-\tilde\theta$ ;
$c\mapsto U_s^*$ is nonincreasing on $(0,c_l)$ and on $(c_l,1)$ , and, if $c_l<c_h$ , jumps up strictly at $c=c_l$ ;
$c\mapsto V_s^*$ is nondecreasing on $(0,c_h)$ and on $(c_h,1)$ , and, if $c_l<c_h$ , drops strictly at $c=c_h$ .

A drop at $t_0$ means: for some $\varepsilon>0$ , every value just to the right of $t_0$ is strictly below every value just to the left.

Milestones

A(\alpha,c)=\begin{cases}\max\{1/2-c,0\},&\alpha\le|1-2c|,\\ [(1+\alpha)/2-c]^2/(2\alpha),&\alpha\ge|1-2c|,\end{cases}

the uniform display of p. 13. The proof of Corollary 1 (p. 30) then contributes three steps: $A(\cdot,c)$ is constant and then increasing, and convex; the optimum is a corner, $\alpha^*\in\{\underline\alpha,\bar\alpha\}$ ; and $\Delta$ vanishes for extreme costs, rises and then falls in $c$ , and peaks at $\Delta(1/2)=(\bar\alpha-\underline\alpha)/8$ . Corollary 1 (p. 13) gives the two threshold rules: (i) $\alpha^*=\underline\alpha$ for $\theta_b\le\tilde\theta$ and $\alpha^*=\bar\alpha$ for $\theta_b>\tilde\theta$ ; (ii) $\alpha^*=\bar\alpha$ exactly for $c_l<c<c_h$ .

Significance

The result. Without information acquisition, the seller's payoff is increasing in its bargaining power and in its outside option and decreasing in its material cost: these are the direct effects. Proposition 2 shows that each of them can be reversed by a discontinuous jump. The mechanism is that the buyer stops gathering information when its own share of the surplus becomes too small (high $\theta_s$ ) or the trade decision becomes clear-cut (extreme $c$ ). The result bears on when a seller should prefer to commit to a weaker bargaining position, and on why cost increases need not hurt a seller facing an uninformed buyer.

Formalizing it. The paper calls Proposition 2 an immediate consequence of Corollary 1. That corollary rests on a short appendix argument whose printed version contains slips: the peak of $\Delta$ is printed as $\theta_b(\bar\alpha-\underline\alpha)/8$ , strictness is claimed on a closed interval at whose endpoints $\Delta=0$ , and " $\alpha^*\in\{\underline\alpha,\bar\alpha\}$ " fails at $c=1/2$ when the two corners tie. A machine-checked development settles exactly which form of each claim is true. The result has been proved informally in the paper; it has not been formalized before.

Difficulty

The obvious argument treats $\alpha^*$ as a function and differentiates $U_s^*$ . That does not work here. At the thresholds $\alpha^*$ is not single-valued, and between them it is constant, so the whole content lies in the jumps. A jump statement must hold whichever optimal level is selected at each parameter, and it must compare values on both sides of a threshold whose location depends on $\Delta$ . Showing that the thresholds are well placed requires the inverted-U shape of $\Delta$ , which comes from an explicit but piecewise integral. The corner property needs convexity of $A$ across the kink at $\alpha=|1-2c|$ , where the two branches of the closed form meet.

Formalization scope

All quantities are real numbers. $A$ is the interval integral over the uniform prior after the change of variables $v=\alpha w+(1-\alpha)\hat u$ ; no density is assumed. The bargaining stage is not modelled; the payoffs are the paper's reduced forms (6) and $\theta_sA(\alpha^*,c)$ . Conventions: $c\in(0,1)$ (the paper's $c\in(\underline u,\bar u)$ ); $\theta_b,\theta_s\in(0,1)$ with $\theta_s=1-\theta_b$ ; $[\underline\alpha,\bar\alpha]$ non-degenerate; $\tilde\theta=1$ when $\Delta(c)\le\bar k$ , which avoids $\bar k/0$ and keeps $\tilde\theta\in(0,1]$ . Monotonicity is claimed on each side of the jump point, open at that point (and across the other cost threshold), and the jump whenever the threshold is interior. In (ii) and (iii), $c_l\le1/2\le c_h$ are assumed to satisfy " $c_l<c<c_h$ iff $\theta_b\Delta(c)>\bar k$ " for all $c\in(0,1)$ , which determines them; when the buyer never gathers information this forces $c_l=c_h=1/2$ .

The paper states Corollary 1 and Proposition 2 for four focal priors (uniform, exponential, logistic, modified Pareto) but works out only the uniform one. This mission is pinned to the uniform prior and the linear cost.

A trivializing formalization is ruled out: $A$ is not defined by its closed form (that closed form is a milestone), $\alpha^*$ is the set of maximisers of $U_b$ and not a threshold rule, and the goal quantifies over every selection from that set, so neither Corollary 1 nor Proposition 2 holds by definition.

A complete development needs piecewise interval integrals of $\max\{\cdot,0\}$ , convexity of a function with a $C^1$ junction, and the fact that a convex function on a segment attains its maximum at an endpoint. All of these are general facts, reusable beyond this mission. Proofs of the milestones in any order are welcome; Proposition 3 and the other priors are not posed here.

Selected references

L. Guo, Gathering Information before Negotiation, SSRN 3930651, manuscript of 15 Feb 2022. https://ssrn.com/abstract=3930651
L. Guo, Gathering Information before Negotiation, Management Science (journal version of the manuscript above; its theorem numbering is not used here). https://doi.org/10.1287/mnsc.2022.4360

8 thms3 active usersReviewed

Completed

Theoretical Computer Science·Captain: Chutong

CLRS — Chapter 6, §§6.1–6.2, 6.5: Indexed-Heap Sorting — Correctness and Running TimeTextbook

Category: Textbook

Review status: This is a private draft revision for the owner's review. The existing published SortIndicesAnalysis.call is marked Proved on Prove2Me. The new headline theorem is a separate draft derived from that contract; its proof remains local. The reused proof library and the new correctness-and-runtime wrapper compile locally with Lean 4.33.1; their axiom checks contain no sorryAx. The new proof has not been submitted to Prove2Me. No public submission or publication is authorized by this revision.

CLRS scope and implementation

This mission belongs to the CLRS fourth-edition formalization series. It presents sorting through an indexed binary min-priority queue, using the heap representation and heap-order ideas of Chapter 6, §§6.1–6.2, and priority-queue operations of §6.5.

It reuses Lunjia Hu's published .algo implementation, definitions, and correctness-and-cost call contract unchanged. The program inserts identifiers $0,\ldots,n-1$ with their keys and then repeatedly extracts the minimum. The result is a fresh sequence of sorted identifiers; the original keys remain unchanged. Equal keys may occur in either order.

This implementation differs from the in-place max-heap HEAPSORT of §6.4: it allocates auxiliary sequences and constructs the heap by repeated insertion. Accordingly, this draft targets an $O(n\log(n+1))$ sorting bound. Constant extra space, linear-time bottom-up construction, stability, and a matching worst-case lower bound are outside this theorem's claims.

Correctness

For every initial heap, every allocated key-sequence reference, and every natural length $n$ , the source-facing sort_indices.Call terminates with a final heap and a fresh allocated result reference. Its first $n$ entries are a permutation of $0,\ldots,n-1$ , ordered by the corresponding original keys. Previously allocated caller sequences and objects, and all collections, are preserved. The output outside this prefix is unspecified.

Negative integer keys, duplicate keys, and $n=0$ are included. The key reference must be allocated even for the empty case. The sequence model is total on integer indices; $n$ specifies the finite input prefix. Integers are mathematical, unbounded integers.

Running time

The headline theorem retains the existing per-clock Budget n (2n) for the same completed call and adds a uniform asymptotic statement. There is a positive natural constant $C$ , chosen independently of the heap, keys, length, and initial counters, such that

T\le C\bigl(1+n(1+\lfloor\log_2(n+1)\rfloor)\bigr).

Here $T$ is the sum of the increments of sort_steps, heap_comparisons, and heap_swaps. Each clock may start at an arbitrary value. If $d=\lfloor\log_2(n+1)\rfloor$ , the existing contract bounds these increments by $2n$ , $4nd$ , and $2n(d+1)$ respectively. It therefore retains the reusable explicit bound

T\le 2n\bigl(3\lfloor\log_2(n+1)\rfloor+2\bigr).

The clocks count the source's marked sorting-loop iterations, heap comparisons, and heap swaps. They do not count every arithmetic operation, array access, allocation, or compiler transition, and do not measure integer bit complexity, Lean checking time, or elapsed machine time. For the empty input the named event count can be zero although initialization and allocation still occur.

Reusable results and milestone

The single supporting milestone is the existing, proved SortIndicesAnalysis.call. It combines termination, sorted-permutation correctness, preservation, freshness, and per-clock budgets. Its implementation reuses the published indexed-heap insertion and minimum-extraction contracts.

The new headline is CLRS.HeapSortIndices.correctness_and_running_time. It imports that established call theorem and derives a uniform asymptotic consequence without repeating the heap correctness proof. Clients can apply the same call contract with their actual initial heap and counters, obtain sorted identifiers, and continue with the resulting heap. No new copy of the heap or runtime definitions is required.

The checked proof of the new headline is retained locally for review. A draft theorem statement may display a sorry placeholder; that placeholder is not an accepted proof or a Prove2Me verification result. An independent read-back of the formal statement is included in the local review package.

Algorithm source

The following files are reproduced unchanged from Lunjia Hu's public v0.1.4 source. Project import root: examples/kruskal. Entry file: sort_indices.algo.

`indexed_heap.algo`

# An indexed binary min-heap for Dijkstra's priority queue.
# vertices[position] and positions[vertex] are inverse on the active prefix.
# keys is indexed by vertex; position -1 means the vertex is not in the heap.
# Clients use nonnegative vertex identifiers, so pop_min can use -1 for empty.

class MinHeap:
    vertices: Seq
    positions: Seq
    keys: Seq
    size: Int

    def __init__(self) -> None:
        self.vertices = const(0)
        self.positions = const(-1)
        self.keys = const(0)
        self.size = 0

    def swap(self, i: Int, j: Int) -> None:
        a = self.vertices[i]
        b = self.vertices[j]
        # @exchange
        self.vertices[i] = b
        self.vertices[j] = a
        self.positions[a] = j
        self.positions[b] = i
        tick("heap_swaps")

    def sift_up(self, i: Int) -> None:
        # @up_loop
        while i > 0:
            parent = (i - 1) // 2
            tick("heap_comparisons")
            if self.keys[self.vertices[parent]] <= self.keys[self.vertices[i]]:
                return
            self.swap(i, parent)
            i = parent

    def sift_down(self, i: Int) -> None:
        # @down_loop
        while 2 * i + 1 < self.size:
            child = 2 * i + 1
            right = child + 1
            if right < self.size:
                tick("heap_comparisons")
                if self.keys[self.vertices[right]] < self.keys[self.vertices[child]]:
                    child = right
            # @compare_child
            tick("heap_comparisons")
            if self.keys[self.vertices[i]] <= self.keys[self.vertices[child]]:
                return
            self.swap(i, child)
            i = child

    def push_or_decrease(self, vertex: Int, key: Int) -> None:
        i = self.positions[vertex]
        if i < 0:
            self.keys[vertex] = key
            i = self.size
            self.vertices[i] = vertex
            self.positions[vertex] = i
            self.size += 1
            self.sift_up(i)
        else:
            tick("heap_comparisons")
            if key < self.keys[vertex]:
                self.keys[vertex] = key
                self.sift_up(i)

    def pop_min(self) -> Int:
        if self.size <= 0:
            return -1
        vertex = self.vertices[0]
        last = self.size - 1
        self.swap(0, last)
        self.size = last
        self.positions[vertex] = -1
        if last > 0:
            self.sift_down(0)
        return vertex

    def is_empty(self) -> Bool:
        return self.size <= 0

`sort_indices.algo`

# Order the identifiers [0, count) by their keys using a reusable binary heap.
# This supplies Kruskal's sort-by-weight step: insert every identifier, then
# extract minima. It is not the in-place HEAPSORT procedure from CLRS Chapter 6.
# Only identifiers are reordered; keys are unchanged. Equal-key identifiers
# may appear in either order.
from indexed_heap import MinHeap


def sort_indices(keys: Seq, count: Int) -> Seq:
    queue = MinHeap()
    result = const(0)
    index = 0
    # @insert
    while index < count:
        tick("sort_steps")
        queue.push_or_decrease(index, keys[index])
        index += 1
    index = 0
    # @extract
    while index < count:
        tick("sort_steps")
        result[index] = queue.pop_min()
        index += 1
    return result

Compiler provenance and validation

The compiler is Algo2Lean, numbered release v0.1.4, public source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, with Lean 4.33.1. Generation uses project mode, the two source files above, entry sort_indices.algo, generated namespace Algo.«sort_indices», and standalone=false.

The hosted compiler archive was downloaded and verified against its release manifest and checksums. All 196 payload files agree with the pinned public source. Generation under that archive's native Python bridge and its released Pyodide 314.0.7 runtime produces identical bytes for all six generated modules and two shared libraries. The release archive and source identities were recorded separately.

The corresponding Prove2Me modules match those raw outputs after two recorded packaging adaptations: rewriting project/runtime imports to Definitions.Def_*, and adding the platform's autoImplicit/backward-definitional-equality option prelude. All remaining bytes, including declaration bodies, are unchanged. The compiler archive SHA-256 is 52b3978479b4f4cc473e11471d839c6c96aafe0ffc73bbeeea4e785228f4fdf0.

Separately, all 18 modules in the published proof dependency closure have been checked locally with Lean 4.33.1 using the accepted proof bodies. To combine separately submitted proof files locally, non-target helper declarations are made private and final solution declarations receive unique audit names; theorem statements and proof bodies are retained, and the named targets are checked against their published types. This local proof packaging is distinct from the generated-code import adaptation above. The axiom audit found only propext, Classical.choice, and Quot.sound, with no sorryAx in the reused results.

These reproduction checks establish generation and packaging correspondence. Lean proof checking is a separate check; neither establishes a proof of compiler correctness.

Attribution and references

Algorithm implementation and reused heap/sorting proofs: Lunjia Hu. This draft presents their reusable sorting contract in the CLRS series and adds the uniform-bound wrapper. The source and proof attribution are retained.

CLRS, fourth edition, Chapter 6, §§6.1–6.2 and §6.5.
Published sorting call contract.
Pinned source and analysis.
Numbered compiler release.

2 thms3 active usersReviewed

Completed

Combinatorics Information Theory·Captain: chaikon

Essential Coding Theory I: Generalized Hamming BoundTextbook

Motivation

An error-correcting code stores or transmits messages as words over a finite alphabet, adding redundancy so that the original word can be recovered after some symbols are corrupted. The basic question of coding theory is the trade-off between the amount of redundancy and the number of errors that can be corrected. The Hamming bound (also called the sphere-packing bound) is the first and most widely taught upper limit on this trade-off. It is due to R. W. Hamming (1950), who introduced the Hamming distance and the Hamming codes in the same paper (Hamming 1950).

This mission formalizes the bound as it is stated in Theorem 1.7.2 of the textbook Essential Coding Theory by V. Guruswami, A. Rudra and M. Sudan (web draft, §1.7, p. 21). It is the first mission of a series following that book. The result is used throughout the book to define perfect codes (Definition 1.7.3) and as the baseline against which later bounds (Singleton, Plotkin, Elias–Bassalygo, the linear-programming bound) are compared.

Setting

Let $\alpha$ be a finite alphabet with $q = |\alpha|$ symbols, and let $n \ge 0$ . A word of length $n$ is a function $\{0, \dots, n-1\} \to \alpha$ , and $\alpha^n$ is the set of all $q^n$ words. A code of block length $n$ is a subset $C \subseteq \alpha^n$ ; its elements are codewords.

The Hamming distance $\Delta(u, v)$ between two words is the number of coordinates in which they differ. The dimension of $C$ is the real number $k = \log_q |C|$ (Definition 1.2.3 of the book). The book calls $C$ an $(n, k, d)_q$ code when its minimum distance $\min_{c_1 \ne c_2 \in C} \Delta(c_1, c_2)$ equals $d$ (Definitions 1.4.1 and 1.7.1).

The Hamming ball of radius $e$ around a word $x$ is $B(x, e) = \{ y \in \alpha^n : \Delta(x, y) \le e \}$ (Definition 1.6.1).

Formalization targets

Milestone: volume of a Hamming ball

For every word $x \in \alpha^n$ and every radius $e \ge 0$ ,

|B(x, e)| = \sum_{i=0}^{e} \binom{n}{i} (q-1)^i.

This is equation (1.18) in the book.

Goal: the generalized Hamming bound

If any two distinct codewords of $C \subseteq \alpha^n$ are at Hamming distance at least $d$ , then

\log_q |C| \;\le\; n - \log_q \Bigl( \sum_{i=0}^{\lfloor (d-1)/2 \rfloor} \binom{n}{i} (q-1)^i \Bigr).

The hypothesis is "minimum distance at least $d$ " rather than "exactly $d$ ". Every $(n, k, d)_q$ code satisfies it, so the goal contains the book's Theorem 1.7.2 as stated.

Significance

The result itself. The bound says that a code correcting $\lfloor (d-1)/2 \rfloor$ errors can have at most $q^n / \mathrm{Vol}_q(\lfloor (d-1)/2 \rfloor, n)$ codewords, so its rate is at most $1 - \log_q \mathrm{Vol}_q / n$ . Codes meeting it with equality are the perfect codes: the Hamming codes, the binary repetition codes of odd length, and the two Golay codes. The bound's asymptotic form, $R \le 1 - H_q(\delta/2)$ , is one of the standard upper bounds on the rate–distance trade-off and is the reference point for the stronger bounds later in the book.

Formalizing it. The theorem has been proved since 1950 and appears in every coding theory text. Mathlib has the Hamming distance (hammingDist) but no notion of a code's distance, no Hamming-ball cardinality formula, and no sphere-packing bound. This mission supplies those, with the dimension stated through the real logarithm exactly as in the book, so later missions in the series can cite it.

Difficulty

The mathematics is elementary. The work lies in the counting step: showing that exactly $\binom{n}{i}(q-1)^i$ words lie at distance exactly $i$ from a fixed word. This identity has no ready-made counterpart in Mathlib, and the alphabet carries no algebraic structure, so translating every ball to a ball around a fixed word is not available. The final step, taking $\log_q$ of both sides, must also handle the conventions of the real logarithm on degenerate inputs.

Formalization scope

The alphabet is an arbitrary type α with [Fintype α] [DecidableEq α], and $q$ is Fintype.card α. Words are functions Fin n → α, and $\Delta$ is Mathlib's hammingDist.
A code is a Finset (Fin n → α). The distance hypothesis quantifies over pairs of distinct codewords.
The dimension is Real.logb q |C|, a real number. The ball volume is the natural-number sum $\sum_{i=0}^{\lfloor (d-1)/2 \rfloor} \binom{n}{i}(q-1)^i$ , cast to $\mathbb{R}$ , where $\lfloor (d-1)/2 \rfloor$ is computed in $\mathbb{N}$ as (d - 1) / 2.
No hypotheses $q \ge 2$ or $C \ne \emptyset$ are imposed. The book assumes them tacitly. Under Lean's conventions $\log_q x = 0$ when $q \le 1$ or $x = 0$ , and the statement remains true in those cases. It is therefore at least as strong as the book's version, and these degenerate cases are not a trivialization: for $q \ge 2$ and $C \ne \emptyset$ the goal is equivalent to the sphere-packing inequality $|C| \cdot \mathrm{Vol} \le q^n$ .
No custom definitions are needed. The ball-volume formula is reusable for any later bound that counts Hamming balls (Gilbert–Varshamov, Elias–Bassalygo). Contributions of alternative counting proofs are welcome.

Selected references

V. Guruswami, A. Rudra and M. Sudan, Essential Coding Theory, draft textbook, §1.6–1.7, Theorem 1.7.2, p. 21. https://cse.buffalo.edu/faculty/atri/courses/coding-theory/book/web-coding-book.pdf
R. W. Hamming, Error detecting and error correcting codes, Bell System Technical Journal 29(2), 147–160, 1950. https://doi.org/10.1002/j.1538-7305.1950.tb00463.x
The Mathlib Community, hammingDist, Mathlib.InformationTheory.Hamming. https://leanprover-community.github.io/mathlib4_docs/Mathlib/InformationTheory/Hamming.html

2 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Platform Competition and Interoperability: The Net Fee Model III: Stronger Interoperability Lowers the Symmetric Equilibrium Net Fee, Except in Duopoly Without an Outside OptionResearch Paper

Motivation

A recurring proposal in the policy debate on dominant digital platforms is to make competing platforms interoperable, so that users of one service can interact with users of another; the EU Digital Markets Act (Regulation (EU) 2022/1925, Article 7) imposes such an obligation on gatekeepers' messaging services. The economic case is that users then enjoy network effects across platforms, not only within their own. The counter-argument is that a network shared with rivals is a weaker competitive weapon, so platforms may compete less hard and users may lose through higher fees.

Ekmekci, White and Wu, Platform Competition and Interoperability: The Net Fee Model (Management Science, 2025), resolve this trade-off in a tractable model of platform competition with strong network effects. Their device is the net fee: the membership fee net of the interaction charges a platform extracts once users have joined. Competition in net fees turns platform demand into an ordinary discrete-choice demand, so equilibria can be characterized by pricing formulas. This mission formalizes their Proposition 7(b): with symmetric platforms, more interoperability lowers the equilibrium net fee, except in a duopoly without an outside option, where it has no effect.

Setting

There are $J \ge 2$ ex ante identical platforms, indexed by $j$ , and one side of users. Platform $j$ charges a net fee $t^j \in \mathbb R$ . A user either joins one platform or takes an outside option whose weight is $w = e^{z} \ge 0$ ; $w = 0$ means there is no outside option. Under Logit demand (13), platform $j$ 's user mass at the profile $t = (t^1,\dots,t^J)$ is

n^j(t) = \frac{e^{-t^j}}{w + \sum_{k} e^{-t^k}}.

Every platform has marginal cost $c$ , and each user values each other user on the same platform at $\gamma$ (the network effect). The degree of interoperability $\lambda \in [0,1]$ lets a user value each user of every other platform at $\lambda\gamma$ (19). Platform $j$ extracts all interaction utility through its total price, so its profit is

\pi^j(t) = \Big(t^j + \gamma n^j + \lambda\gamma \sum_{k\ne j} n^k - c\Big)\, n^j .

A profile $t$ is a Nash equilibrium in net fees if no platform can raise its profit by changing its own net fee to any other real number. A symmetric equilibrium is an equilibrium in which every platform charges the same net fee. The diversion ratio $\varphi^j = \sum_{k\ne j} n^k/(1-n^j)$ (32) is the share of the users a platform gains by a small fee cut that come from rival platforms rather than from the outside option.

When all platforms charge $\tau$ , each has share $n(\tau) = e^{-\tau}/(w + J e^{-\tau})$ and diversion ratio $\varphi(\tau) = (J-1)n(\tau)/(1-n(\tau))$ . The proof of Proposition 7 introduces

\xi(\tau;\lambda) = -\tau + c + \frac{1}{1-n(\tau)} - 2\gamma n(\tau) - \gamma\lambda\big(J-1-\varphi(\tau)\big) n(\tau).

Formalization targets

Goal: Proposition 7(b), Logit case

Let $0 < \gamma \le 27/8$ and $0 \le \underline\lambda < \overline\lambda \le 1$ , and suppose the constant profile $\underline t$ is a Nash equilibrium under $\underline\lambda$ . Then

J \ge 3 \text{ or } w > 0 \;\Longrightarrow\; \exists\, \overline t < \underline t:\ (\overline t,\dots,\overline t) \text{ is a Nash equilibrium under } \overline\lambda,

J = 2 \text{ and } w = 0 \;\Longrightarrow\; (\underline t,\underline t) \text{ is a Nash equilibrium under } \overline\lambda.

Milestones

The Logit diversion ratio (32) is independent of the platform's own fee, and equals the ratio of rival-demand to own-demand derivatives.
Proposition 7(a): at a symmetric equilibrium, $\tau = c + \frac{1}{1-n} - \big(2 + \lambda(J-1-\varphi)\big)\gamma n$ , the Logit form of (21).
For $\gamma \le 27/8$ , the first-order condition (33) gives a global best response (Appendix E.1.3 with (36)).
Symmetric equilibria are the zeros of $\xi(\cdot;\lambda)$ , the converse direction under $\gamma \le 27/8$ .
$\xi(\tau;\overline\lambda) = \xi(\tau;\underline\lambda) - \gamma(\overline\lambda-\underline\lambda)(J-1-\varphi)n$ , with $J - 1 - \varphi > 0$ unless $J = 2$ and $w = 0$ .
$\xi(\tau;\lambda) > 0$ for every $\tau < c - 2\gamma - \gamma\lambda(J-1)$ .

Significance

The result separates two forces that interoperability sets off. Platforms extract the new off-network utility of the users they add, which pushes them to compete harder for users; and part of the users they add are diverted from rivals, which erodes the off-network revenue they draw from existing users. Proposition 7(b) says the first force wins whenever there is an outside option or at least three platforms, so users gain twice from interoperability: wider network effects and lower net fees. In the knife-edge duopoly without an outside option the forces cancel exactly. The authors read the result, together with their Proposition 6 on dominance, as "reason for optimism about the effects of increasing interoperability" (p. 23) and as an encouraging view of interoperability regulation (p. 3).

The paper proves the result on pp. 52–53. No machine-checked version of it, or of any result of the paper, exists. The formalization adds three things: a fully specified equilibrium notion (global Nash, not a first-order condition); an explicit verification that first-order conditions are sufficient in the parameter range used; and a precise statement of the case split, which the paper phrases through $\varphi^j = 1$ and here is stated through the primitives $J$ and $w$ .

Difficulty

The proof reduces the comparison of equilibria to the zeros of the one-variable function $\xi$ , and then applies the intermediate value theorem. Two steps carry the substance. First, every symmetric equilibrium must satisfy $\xi = 0$ : this needs the first-order condition for a maximum of a profit function that depends on the deviating platform's fee through every platform's share. Second, every zero of $\xi$ must be a Nash equilibrium: this is false for large network effects, since profit can then fail to be concave and a platform can profit from a large deviation. The paper establishes sufficiency through concavity of profit in the platform's own share, which needs $2\gamma(1-\lambda\varphi^j) \le 1/(n(1-n)^2)$ for all shares and the independence of $\varphi^j$ from the platform's own fee. Identifying equilibria with solutions of the pricing formula, without this argument, proves a statement about stationary points, not about equilibria.

Formalization scope

Logit, one side, symmetric primitives. Proposition 7 is stated in the paper for general demand. This mission formalizes the Logit case (13), the specification of the paper's §5–6, with one side, common $c$ and common $\gamma$ . The proof of 7(b) writes the Logit markup $1/(1-n^j)$ , and its general-demand sufficiency argument is a sketch (Appendix E.1.3). General demand with Assumptions A1–A2, several sides, platform-specific parameters and the microfoundation of Appendix A are out of scope.
Outside option. $w = e^{z} \ge 0$ is a real parameter; "no outside option" is $w = 0$ , not a limit.
Added hypotheses. $\gamma > 0$ (the paper's "as long as network effects are positive", p. 25; with $\gamma < 0$ the comparison reverses) and $\gamma \le 27/8$ (the bound (36), Proposition 2′'s 3.375, under which the paper's first-order sufficiency holds). The interoperability levels lie in $[0,1]$ as in part (a).
Equilibrium. IsEquilibrium is the global Nash condition over every deviation $s \in \mathbb R$ . A formalization in which equilibrium means "the pricing formula holds", or in which the interoperability term $\lambda\gamma\sum_{k\ne j}n^k$ is dropped from profit (so that $\lambda$ affects nothing), would make the goal trivial and is not this theorem.
Lean conventions. Platforms are indexed by Fin J; $\lambda$ is called lam; $J$ is cast to $\mathbb R$ in the symmetric closed forms nSym, phiSym, xi.
Infrastructure. The proofs need the Logit derivatives, a one-variable concavity argument through the change of variables $t \mapsto n^j$ (a strictly decreasing bijection $\mathbb R \to (0,1)$ ), the bound $\min_{n\in(0,1)} 1/(n(1-n)^2) = 27/4$ , continuity of $\xi$ and Mathlib's intermediate value theorem. The Logit and concavity lemmas are shared with the other two missions of this series and are reusable for any Logit oligopoly with network effects. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

M. Ekmekci, A. White, L. Wu, Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025; accepted working-paper version of December 12, 2024. https://doi.org/10.1287/mnsc.2023.02810
S. P. Anderson, N. Erkal, D. Piccinin, Aggregative Games and Oligopoly Theory: Short-run and Long-run Analysis, The RAND Journal of Economics 51(2), 470–495, 2020.
A. Caplin, B. Nalebuff, Aggregation and Imperfect Competition: On the Existence of Equilibrium, Econometrica 59(1), 25–59, 1991. https://doi.org/10.2307/2938238
Regulation (EU) 2022/1925 (Digital Markets Act), Article 7. https://eur-lex.europa.eu/eli/reg/2022/1925/oj

9 thms3 active usersReviewed

Probability Random Matrix Theory Statistics·Captain: mikedeng1

Change-Point Detection in Dynamic Networks with Missing Links III: The Dyadic-Grid Matrix CUSUM Test Detects an Unknown Change Time Above Energy 4(1+ϵ)(6ω_n/T)^{1/2} + C log(4n log₂T/(α∧β))/√TResearch Paper

Detecting a change in a partially observed network

Many networks are recorded as a sequence of snapshots: contact networks in epidemiology, communication graphs, brain connectivity measured over time, trade or transport links. A basic statistical question is whether the law generating the snapshots changed at some point. Two features make the question hard in practice. The networks are often sparse, so each snapshot carries little information. And links are missing: a pair of vertices is observed only with some probability, so an absent edge may mean "no link" or "not sampled".

Enikeeva and Klopp (arXiv:2106.14470, Operations Research, 2025) give minimax bounds for this testing problem. They treat both a known change time (Theorems 1 and 2) and an unknown change time (Theorem 3). This mission formalizes the unknown-time case, where the test scans a dyadic grid of candidate times. Two companion missions formalize the known-time upper bound (Theorem 1) and the lower bound (Theorem 2).

Setting

There are $n$ vertices and $T$ time points. At time $t$ the statistician observes a symmetric matrix $Y^t\in\{0,1\}^{n\times n}$ with zero diagonal, $Y^t_{ij}=\Omega^t_{ij}A^t_{ij}$ . Here $A^t$ is the adjacency matrix of the network and $\Omega^t$ records which pairs were sampled. The entries $Y^t_{ij}$ , $i<j$ , are independent over pairs and times, and

Y^t_{ij}\sim\mathrm{Bernoulli}\big((\Pi\odot\Theta^t)_{ij}\big),

where $\Theta^t\in[0,1]^{n\times n}$ is the connection-probability matrix (symmetric, zero diagonal), $\Pi$ is the sampling matrix (symmetric, entries in $(0,1]$ , unit diagonal), and $\odot$ is the entrywise product.

The sparsity level $\omega_n$ bounds the expected observed degree: $(\Theta,\Pi)\in\mathcal S_n(\omega_n)$ when $\|\Pi\odot\Theta\|_{1,\infty}=\max_j\sum_i|(\Pi\odot\Theta)_{ij}|\le\omega_n$ .

Under the null hypothesis $\Theta^t=\Theta^0$ for all $t$ . Under the alternative there is $\tau\in\mathcal D_T=\{1,\dots,T-1\}$ with $\Theta^t=\Theta^0$ for $t\le\tau$ and $\Theta^t=\Theta^0+\Delta\Theta^\tau$ for $t>\tau$ . Both parameter pairs lie in $\mathcal S_n(\omega_n)$ , and the jump has energy at least $R$ :

q(\tau/T)\,\|\Pi\odot\Delta\Theta^\tau\|_{2\to2}\ge R,\qquad q(x)=\sqrt{x(1-x)},

where $\|\cdot\|_{2\to2}$ is the spectral norm. A test $\psi$ maps the data to $\{0,1\}$ . Its type I error $\alpha(\psi)$ is the largest rejection probability over the null class. Its type II error $\beta(\psi,R)$ is the largest acceptance probability over all $\tau\in\mathcal D_T$ and all alternatives of energy at least $R$ .

The Matrix CUSUM at time $t$ contrasts the averages before and after $t$ :

Z_T(t)=\sqrt{\frac{t(T-t)}{T}}\Big(\frac1t\sum_{s=1}^tY^s-\frac1{T-t}\sum_{s=t+1}^TY^s\Big),\qquad1\le t\le T-1.

The dyadic grid is $\mathcal T=\{2^k\}\cup\{T-2^k\}$ , $0\le k\le\lfloor\log_2(T/2)\rfloor$ . Fix $\epsilon\in(0,1/2]$ . The test (14) of the paper rejects when

\max_{t\in\mathcal T}\|Z_T(t)\|_{2\to2}>H_{\alpha,n,T}=2\sqrt2(1+\epsilon)\sqrt{\omega_n}+C_\epsilon\log\frac{4n\log_2(T)}{\alpha}.

Formalization targets

Goal: Theorem 3

For every $\epsilon\in(0,1/2]$ there are constants $C_\epsilon>0$ and $C$ , depending only on $\epsilon$ , such that for all $n\ge1$ , $T\ge2$ , $\omega_n\ge0$ and $\alpha,\beta\in(0,1)$ : if

R\ \ge\ 4(1+\epsilon)\Big(\frac{6\omega_n}{T}\Big)^{1/2}+\frac{C}{\sqrt T}\log\Big(\frac{4n\log_2(T)}{\alpha\wedge\beta}\Big),

then the grid test with threshold $H_{\alpha,n,T}$ has $\alpha(\psi_{n,T})\le\alpha$ and $\beta(\psi_{n,T},R)\le\beta$ .

Milestones

the signal-plus-noise decomposition $Z_T(t)=-\mu^\tau_T(t)\,\Pi\odot\Delta\Theta^\tau+\xi(t)$ and the maximum $\mu^\tau_T(\tau)=\sqrt T\,q(\tau/T)$ , display (7);
the grid facts $\mathcal T\subseteq\mathcal D_T$ and $|\mathcal T|\le2\log_2T$ ;
the grid captures signal: for every $\tau\in\mathcal D_T$ some $t\in\mathcal T$ has $\mu^\tau_T(t)\ge\sqrt T\,q(\tau/T)/\sqrt3$ ;
Proposition 11, the Bandeira–van Handel bound for symmetric random matrices with independent bounded entries;
Lemma 12, the noise bound for the CUSUM at a fixed time;
Lemma 5 (level) and Lemma 6 (power above $4\sqrt6(1+\epsilon)(\omega_n/T)^{1/2}+\frac{\sqrt3C_\epsilon}{\sqrt T}(\log\frac{4n\log_2T}\alpha+\log\frac{2n}\beta)$ ).

Significance

Theorem 3 shows that not knowing the change time costs at most a constant factor and a $\log\log T$ term in the detection energy. Together with the lower bound of Theorem 2, which is of order $(\omega_n/T)^{1/2}$ , this makes the grid test rate-optimal when $\omega_n$ grows at least polylogarithmically in $n$ (Remark 3 of the paper). The statistic depends on the data only through spectral norms of $O(\log T)$ CUSUM matrices, so it is cheap to compute. The threshold needs only the degree bound $\omega_n$ , which can be estimated from the observed degrees.

The paper's proof is complete on paper apart from one step noted below. No part of it is machine-checked. Formalizing it produces a checked finite model of Bernoulli network data with missing links, a reusable Matrix CUSUM, and a precise statement of a Bandeira–van Handel type bound for symmetric matrices with independent bounded entries. That bound is a standard tool in random-matrix statistics and is not yet available in Mathlib or on the platform.

Difficulty

The level of the test is a union bound over the grid combined with a high-probability bound on $\|\xi(t)\|_{2\to2}$ at a fixed time. The hard part is that bound, Lemma 12. A matrix Bernstein inequality gives a leading term $\sigma\sqrt{\log(n/\delta)}$ , which is too large. The statement needs the sharp form $2\sqrt2(1+\epsilon)\sigma+C_\epsilon\log(2n/\delta)$ , where the variance proxy $\sigma$ enters without a logarithmic factor. Proposition 11 supplies this only for matrices whose entries are bounded by $\sigma_*$ . The entries of $\xi(t)$ are sums over time and are only bounded by about $\sqrt{\log(n/\delta)}$ with high probability. The paper applies Proposition 11 "given the event" $\{\|\xi(t)\|_\infty\le\sigma_*\}$ , but conditioning on that event destroys centring and independence, so a truncation argument is missing there.

The power analysis is elementary once Lemma 12 is available. Its one subtlety is that the change time ranges over all of $\mathcal D_T$ , while the test inspects only the grid.

Formalization scope

Data and probability. Only $Y$ is modelled; the latent $A^t,\Omega^t$ are integrated out. An observation is a Boolean function of a 0-based time index and of a pair $i<j$ . Probabilities are finite sums of products of Bernoulli weights, so every test is measurable and no measure theory enters the model. Proposition 11 is the only measure-theoretic statement.
Classes. The sampling class carries the paper's standing assumptions $\Pi_{ii}=1$ , $\Pi_{ij}>0$ . The errors are real suprema of sets of probabilities; an empty alternative has type II error $0$ .
Spectral norm. $\|\cdot\|_{2\to2}$ is the published HighDimProb.RandomMatrices.matrixOpNorm.
Grid and test. $\lfloor\log_2(T/2)\rfloor$ is Nat.log 2 (T / 2). " $\max_{t\in\mathcal T}\|Z_T(t)\|>H$ " is " $\exists t\in\mathcal T$ , $\|Z_T(t)\|>H$ ". The threshold uses the real $\log_2T$ .
Constants. $C_\epsilon$ and $C$ are quantified existentially before $n,T,\omega_n,\alpha,\beta,R$ . A version with the constants chosen after $n$ or $T$ would be trivial, because huge constants silence the test or empty the alternative. The goal does not assume Lemma 12's conclusion. Lemmas 5 and 6 take it as a hypothesis, and Lemma 12 states that it is satisfiable. The test ranges over all functions of the data, and the alternative over all $\tau\in\mathcal D_T$ .
Disclosed additions and corrections. The theorems assume $n\ge1$ , $T\ge2$ and $\omega_n\ge0$ , which the paper leaves implicit. Proposition 11 assumes $m\ge1$ and $c_\epsilon>0$ . Independence in Proposition 11 and Lemma 12 refers to the entries with $i\le j$ ( $i<j$ ) of a symmetric matrix. The grid statement is the inequality $|\mathcal T|\le2\log_2T$ : the printed equality $|\mathcal T|=2+2\lfloor\log_2(T/2)\rfloor$ fails when the two halves overlap, as at $T=4$ . Lemma 5 is stated with " $\le\alpha$ ", as its proof concludes, rather than the printed "less than $\alpha$ ". The grid-signal milestone is stated as an existence claim, because the printed choice $\tau/2\le t^*<\tau$ has no solution at $\tau=1$ .

Welcome contributions: a proof of Proposition 11, or of any sharp spectral-norm bound that implies it; a rigorous proof of Lemma 12, repairing the conditioning step; and the elementary grid lemmas.

Selected references

F. Enikeeva and O. Klopp, Change-point detection in dynamic networks with missing links, Operations Research, 2025; arXiv:2106.14470v2. https://arxiv.org/abs/2106.14470
A. S. Bandeira and R. van Handel, Sharp nonasymptotic bounds on the norm of random matrices with independent entries, Annals of Probability 44(4), 2016. https://doi.org/10.1214/15-AOP1025
H. Liu, C. Gao and R. J. Samworth, Minimax rates in sparse, high-dimensional change point detection, Annals of Statistics 49(2), 2021. https://doi.org/10.1214/20-AOS1994

12 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Opinion Dynamics on Directed Complex Networks 3: On a Galton-Watson Limit, the Stationary Opinion with Memory Has Variance at Most That of the Proportional No-Memory RecursionResearch Paper

Motivation

Linear opinion models describe how individuals in a social network revise their views by averaging what their neighbours think, what external media tell them, and what they themselves believed a moment ago. The last ingredient, an autoregressive or memory term, appears in the Friedkin–Johnsen family of models and in its stochastic variants. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969, Mathematics of Operations Research, 2025) study such a model on large directed random graphs with vertex attributes and random media signals. They show that the opinion of a typical vertex has a stationary law that is described, in the large-graph limit, by a recursion on a marked Galton–Watson tree.

A natural question is what the memory term does to that stationary law. Simulations in the paper (Section 5.4, Figures 6–7) suggest that memory smooths individual trajectories and makes the stationary opinion less dispersed. Proposition 6 turns this into a theorem: on a Galton–Watson limit, the stationary opinion with memory has variance at most that of a no-memory recursion that keeps the same relative weights of neighbours and media.

Setting

Nodes of the limiting tree are labelled by finite words $\mathbf i=(i_1,\dots,i_k)$ , the root being $\varnothing$ ; $(\mathbf i,j)$ is the $j$ -th child of $\mathbf i$ . Each node carries a mark $\mathcal X_{\mathbf i}$ , from which the model reads an in-degree $\mathcal N_{\mathbf i}$ , weights $\mathcal C_{(\mathbf i,1)},\mathcal C_{(\mathbf i,2)},\dots\in[0,1]$ summing to $c$ when $\mathcal N_{\mathbf i}\ge1$ , and an internal opinion $\mathcal Q_{\mathbf i}\in[-1,1]$ . Parameters satisfy $c\in[0,1)$ , $d\in(0,1]$ , $c+d\le1$ . The tree is a delayed marked Galton–Watson tree: marks are independent, and all non-root marks have the same law.

Each node receives media signals $\mathcal Z_{\mathbf i}^{(k)}\in[-1,1]$ , $k\ge0$ , conditionally i.i.d. given its mark and conditionally independent across nodes, and the external signal

\mathcal W_{\mathbf i}^{(k)}=d\,\mathcal Z_{\mathbf i}^{(k)}+\mathcal Q_{\mathbf i}\Big(c-\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\Big).

The general recursion (8) and the no-memory recursion (9) are

\mathcal M_{\mathbf i}^{(k+1)}=\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\mathcal M_{(\mathbf i,j)}^{(k)}+\mathcal W_{\mathbf i}^{(k)}+(1-c-d)\mathcal M_{\mathbf i}^{(k)},\qquad \mathcal R_{\mathbf i}^{(k+1)}=\sum_{j=1}^{\mathcal N_{\mathbf i}}\frac{\mathcal C_{(\mathbf i,j)}}{c+d}\mathcal R_{(\mathbf i,j)}^{(k)}+\frac{\mathcal W_{\mathbf i}^{(k)}}{c+d}.

Writing $\Delta$ for the linear map on the right-hand side without the signal, the limiting root opinion is the series $\sum_{s\ge0}(\Delta^s\mathcal W^{(s)})(\varnothing)$ ; it is $\mathcal M^*$ for (8) and $\mathcal R^*$ for (9). The moments

\rho_1^*=E\Big[\sum_{i=1}^{\mathcal N_\varnothing}\mathcal C_i\Big],\quad \rho_1=E\Big[\sum_{i=1}^{\mathcal N_1}\mathcal C_{(1,i)}\Big],\quad \rho_2^*=E\Big[\sum_{i=1}^{\mathcal N_\varnothing}\mathcal C_i^2\Big],\quad \rho_2=E\Big[\sum_{i=1}^{\mathcal N_1}\mathcal C_{(1,i)}^2\Big]

and the series $p_m=\sum_{s\ge0}\binom{s+m}{s}^2(1-c-d)^{2s}(c+d)^{2(m+1)}$ enter every formula below.

Formalization targets

Goal: Proposition 6

If $c,d>0$ , $c+d<1$ and $P(\mathcal N_\varnothing>0)=P(\mathcal N_1>0)=1$ , then

\mathrm{Var}(\mathcal M^*)\le\mathrm{Var}(\mathcal R^*).

The goal asserts the comparison only, not the closed forms, so it is the weakest statement the paper's computation supports.

Milestones

Theorem 8 (pp. 32–33): closed forms for $E$ and $\mathrm{Var}$ of the limiting opinions of the root and of a neighbour, in terms of $\rho_1^*,\rho_1,\rho_2^*,\rho_2$ , $\mathcal Y_{\mathbf i}=E[\mathcal W_{\mathbf i}\mid\mathcal X_{\mathbf i}]$ , $\mathcal V_{\mathbf i}=\mathrm{Var}(\mathcal W_{\mathbf i}\mid\mathcal X_{\mathbf i})$ and a Geometric expectation of $p_T$ .
Remark 10.2 (pp. 33–34): the specialisation to the Section 5.1 signals with $\mathcal N_\varnothing,\mathcal N_1>0$ a.s.; it expresses $\mathrm{Var}(\mathcal M^*)$ through $\mathrm{Var}(\mathcal Z)$ and $E[\mathrm{Var}(\mathcal Z\mid\mathcal X)]$ .
(15) (p. 31): $\mathrm{Var}(\mathcal R^*)=\frac{d^2}{(c+d)^2}\mathrm{Var}(\mathcal Z_\varnothing)+\frac{\rho_2^*d^2}{(c+d)^2((c+d)^2-\rho_2)}\mathrm{Var}(\mathcal Z_1)$ .
Coefficient bound (pp. 31–32): $p_m\in(0,1)$ and $\frac{1}{1-\rho_2}E[(c+d)^{-2(T+2)}p_{T+1}]\le\frac{1}{(c+d)^2((c+d)^2-\rho_2)}$ , $T$ Geometric with success probability $1-\rho_2$ .

Additional item (not a milestone): Lemma 9 (p. 34), the mean and variance of $\mathcal R^{(k+1)}$ for the general recursion with general signals, started from $0$ , at the root and at non-root nodes; it is the finite-time step behind Theorem 8.

Significance

The proposition isolates the effect of memory on dispersion: with the same proportional influence of neighbours and media, adding inertia never increases the variance of the stationary opinion of a typical individual. In the paper's interpretation, slower updating produces less polarised stationary opinions, which matters when the model is used to compare network interventions or media exposure. Theorem 8 and Lemma 9 go further and give exact first and second moments of the stationary opinion on Galton–Watson limits with possibly stubborn (in-degree zero) vertices and arbitrary mark-dependent signals; such closed forms are rare for models of this kind.

The results are proved in the paper. None of them has a machine-checked proof. Formalizing them produces a Lean development of moment computations for linear recursions on marked Galton–Watson trees (conditioning on independent subtrees, laws of total variance along generations, and negative-binomial series), which is reusable for other smoothing-transform and branching-recursion problems. Two printed slips are corrected along the way (see Formalization scope).

Difficulty

The difficulty is not the comparison itself but the exact variance of $\mathcal M^*$ . With memory, a signal emitted at time $s$ by a node at depth $l$ reaches the root with coefficient $\binom{s}{l}(1-c-d)^{s-l}$ times the product of weights along the path, so its contributions spread over all later times. The variance then involves the squared coefficients $\sum_s\binom{s}{l}^2(1-c-d)^{2(s-l)}$ , which do not factor as the coefficients do in the no-memory case. The obvious route, comparing the two recursions pathwise or coupling them, fails: the two root opinions are not ordered, and only their variances are. The comparison emerges only after the conditional variances of the media signals are separated from the variance of their conditional means, and after the Geometric average of $p_{T+1}$ is bounded.

Formalization scope

Model. The tree is encoded with Ulam–Harris labels List ℕ (0-based children; the paper's node $1$ is [0]), and marks are read through measurable maps $\mathcal N$ , $\mathcal C$ , $\mathcal Q$ on a measurable space $M$ . The media signals are $\zeta(\mathcal X_{\mathbf i},U_{\mathbf i}^{(k)})$ with i.i.d. uniforms independent of the marks. This quantile representation is equivalent in law to the paper's conditional i.i.d. assumption and is the paper's own device (p. 25). The general signals of Theorem 8 and Lemma 9 are $\xi(\mathcal X_{\mathbf i},U_{\mathbf i}^{(k)})$ with $|\xi|\le d+c-\sum_j\mathcal C_{(\mathbf i,j)}$ .
Limit tree, not graph sequence. The paper's statements assume "the assumptions of Theorem 2" with the Galton–Watson tree as local limit. Those assumptions only identify the tree's root opinion with the large-graph typical opinion; every claim here is about the tree. All statements are made on the tree under the Section 5 standing assumptions, which is a generalization.
Conventions. Limiting opinions are the absolutely summable series $\sum_s(\Delta^s\mathcal W^{(s)})(\mathbf i)$ ; $E$ is the Bochner integral, Var/Cov are Mathlib's variance/covariance, conditional moments are condExp/condVar given $\sigma(\mathcal X_{\mathbf i})$ ; the Geometric expectation is the explicit series $\sum_k\rho^k(1-\rho)g(k)$ .
Corrections. Remark 10.2's printed mean lacks a factor $d$ ; the corrected mean is stated. Lemma 9's root variance is stated for $k\ge1$ (it fails at $k=0$ ) and its root mean under $\rho_1>0$ . Equation (15) is Proposition 4 applied to recursion (9) after rescaling.
No trivialization. Every random variable involved is bounded, so no variance, integral or series takes a junk value; the denominators $c+d-\rho_1$ , $(c+d)^2-\rho_2$ , $1-\rho_2$ are positive under the standing assumptions, and the goal's hypotheses are satisfied by, e.g., the path tree ( $\mathcal N\equiv1$ , $\mathcal C\equiv c$ ), where both variances are positive.
Infrastructure. Useful contributions include: summability and boundedness of the opinion series; independence of subtrees in Ulam–Harris encodings; the law of total variance (integral_condVar_add_variance_condExp in Mathlib); the identities $\sum_s\binom{s}{l}x^{s-l}=(1-x)^{-(l+1)}$ and the negative-binomial bound $p_m<1$ .

Selected references

N. Fraiman, T.-C. Lin, M. Olvera-Cravioto, Opinion dynamics on directed complex networks, arXiv:2209.00969v2, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2209.00969
N. E. Friedkin, E. C. Johnsen, Social influence and opinions, Journal of Mathematical Sociology 15(3–4), 1990. https://doi.org/10.1080/0022250X.1990.9990069
M. H. DeGroot, Reaching a consensus, Journal of the American Statistical Association 69(345), 1974. https://doi.org/10.1080/01621459.1974.10480137

8 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+2·Captain: mikedeng1

Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes III: Bipartite, Unit-Patience Side: Rounding Then Probing by Weight Earns ≥ (1 − 1/e)·Σ w_e p_e y_eResearch Paper

Motivation

Stochastic matching with patience models kidney exchange, online dating and labour platforms: every edge of a graph is present only with some probability, the only way to learn whether it is present is to probe it, and a probed edge that turns out to be present must be added to the matching. Each vertex $v$ also has a patience $t_v$ , a limit on how many of its edges may be probed. The goal is a probing strategy whose expected matched weight is a large fraction of what the best adaptive strategy obtains. Since the best strategy is hard to compute, algorithms are compared with the value of a linear program (LP (3) below), which upper-bounds every probing strategy (Bansal, Gupta, Li, Mestre, Nagarajan, Rudra, Algorithmica 2012).

Bansal et al. gave a $1/3$ -approximation for stochastic bipartite matching. Brubach, Grammel, Ma, MacRury and Srinivasan (Mathematics of Operations Research, 2025; arXiv:2106.06892v3) single out the case in which one side of the bipartition has unit patience, $t_u=1$ for every $u\in V_1$ . This case contains "Problem A" of Hikima et al. (AAAI 2021), whose approximation ratio transfers to their integrated two-stage problem ISPCB; Hikima et al. obtained $1/3$ from the bound of Bansal et al. For the special case in which one side has arbitrary patience and the other unlimited patience, Borodin and MacRury had already obtained the same $(1-1/e)$ guarantee through an online problem.

Setting

Let $G=(V_1\cup V_2,E)$ be a finite bipartite graph; $\delta(x)$ denotes the set of edges at a vertex $x$ . Each edge $e$ has a weight $w_e\ge 0$ and an activation probability $p_e\in[0,1]$ , independently across edges. Every $u\in V_1$ has patience $1$ ; every $v\in V_2$ has a patience $t_v\in\mathbb N\cup\{\infty\}$ .

LP (3). A vector $(y_e)_{e\in E}$ is feasible when $0\le y_e\le 1$ and, for every vertex $x$ ,

\sum_{e\in\delta(x)}y_ep_e\le 1,\qquad \sum_{e\in\delta(x)}y_e\le t_x .

Write $z_e=y_ep_e$ and $\mathsf{OPT}(v)=\sum_{e\in\delta(v)}w_ez_e$ .

The algorithm. A dependent rounding (Gandhi, Khuller, Parthasarathy, Srinivasan, J. ACM 2006) turns $y$ into a random set $\hat E=\{e:Y_e=1\}$ of rounded edges with $\Pr[Y_e=1]=y_e$ , at most one rounded edge at each $u\in V_1$ , at most $t_v$ at each $v\in V_2$ , and the negative correlation property (2): for $v\in V_2$ , $S\subseteq\delta(v)$ and $b\in\{0,1\}$ ,

\Pr\Big[\bigcap_{e\in S}(Y_e=b)\Big]\le\prod_{e\in S}\Pr[Y_e=b].

In the rounded graph every $v\in V_2$ is the centre of a star. Each $v$ probes its rounded edges in decreasing order of weight and is matched to the first active one; $W(v)$ is the weight of that edge ( $0$ if none), and $\mathbb E[\mathsf{ALG}]=\mathbb E[\sum_{v\in V_2}W(v)]$ .

Formalization targets

Goal: Theorem 2 (p. 18)

For every feasible $y$ , every rounding with the properties above and every decreasing-weight probing order,

\mathbb E[\mathsf{ALG}]\ \ge\ \Big(1-\frac1e\Big)\sum_{v\in V_2}\sum_{e\in\delta(v)}w_ep_ey_e .

Milestones

The proof of Lemma 7 (p. 17) expresses $W(v)$ as $\mathbb E[\sum_i w_iY_iP_i\prod_{j<i}(1-Y_jP_j)]$ and bounds $\mathbb E[\prod_{j\le i}(1-Y_jP_j)]\le\prod_{j\le i}(1-y_jp_j)$ using (2).
Lemma 7 (p. 16): $\mathbb E[W(v)]\ge\sum_{i=1}^k w_iz_i\prod_{j=1}^{i-1}(1-z_j)$ for the edges of $\delta(v)$ labelled by decreasing weight.
Eq. (29) (p. 18): the bound $F(i)\ge1-e^{-F^*(i)}\ge(1-1/e)F^*(i)$ . The summation-by-parts identity (27) on the same page is included as a supporting lemma.
Lemma 8 (p. 17): $\sum_i w_iz_i\prod_{j<i}(1-z_j)\ge(1-1/e)\sum_iw_iz_i$ when $z_i\in[0,1]$ , $\sum_iz_i\le1$ and $w_1\ge\cdots\ge w_k\ge0$ .
Lemma 9 (p. 18): $\mathbb E[W(v)]\ge(1-1/e)\,\mathsf{OPT}(v)$ for every $v\in V_2$ .

The paper's proofs are in §4, pp. 16–19.

Significance

Combined with the LP upper bound (Lemma 1 of the paper, from Bansal et al.), Theorem 2 is a $(1-1/e)$ -approximation for stochastic matching on bipartite graphs with a unit-patience side, improving and generalizing the $1/3$ guarantee of Hikima et al. for Problem A and, through their reduction, for ISPCB. By the paper's account (§1.1, p. 4), the guarantee rests on a new ingredient, a $(1-1/e)$ -balanced ordered contention resolution scheme for rank-1 matroids under negative correlation, in which the algorithm chooses the order: the per-star bound of Lemmas 7 and 9 holds for every rounding satisfying (2), not only for independent activations.

The result is proved in the paper; none of it has been machine-checked. This mission formalizes the per-star analysis and the theorem for an abstract rounding described by its properties, which is reusable for any algorithm that probes stars after a negatively correlated rounding.

Difficulty

If the rounded indicators $Y_e$ at a vertex were independent, Lemma 7 would be an equality and the remaining work would be the deterministic inequality of Lemma 8. They are not: the rounding is dependent, and Example 1 (p. 19) shows that this dependence can raise the probability that a particular edge is blocked to $1/2$ , so that no correlation-agnostic contention resolution scheme is better than $1/2$ -balanced. A per-edge guarantee, of the kind a contention resolution scheme that ignores correlation provides, is therefore unavailable: the bound of Theorem 2 holds only for the total weight collected at each $v$ , and the negative correlation property (2) is one-sided, so it can be used only in the direction in which it holds.

Formalization scope

All randomness is finite. The rounding is a probability vector $\mu$ on subsets of $E$ ; the activeness pattern $P:E\to\{0,1\}$ is independent with product weights. Every expectation is an explicit finite sum.
The rounding of Gandhi et al. is represented by its properties: $\mu\ge0$ , $\sum\mu=1$ , the marginals $\Pr[Y_e=1]=y_e$ , at most one rounded edge at each $u\in V_1$ , at most $t_v$ at each $v\in V_2$ , and (2) on the rounded indicators for every $v\in V_2$ , $S\subseteq\delta(v)$ , $b\in\{0,1\}$ . The goal holds for every such $\mu$ , so it covers the paper's rounding; formalizing the rounding procedure itself is a separate project.
$W(v)$ is defined from the run (the first active edge in $v$ 's probe list), not by the formula of Lemma 7; the identity between the two is a milestone.
Standing assumptions, disclosed: $w_e\ge0$ (with a negative weight the bound fails), $p_e\in[0,1]$ , patience $\infty$ is allowed on $V_2$ , and parallel edges are allowed. The goal is stated for every feasible $y$ , a stronger statement than the paper's "optimal" $y$ , since the proof never uses optimality. The phrase "yielding a $(1-1/e)$ -approximation" is not formalized: it needs Lemma 1 of Bansal et al.
Ruled out: defining $W(v)$ as $\sum_iw_iY_iP_i\prod_{j<i}(1-Y_jP_j)$ , as the best active edge regardless of the rounding, or stating the goal for one specific (independent) rounding or "for some rounding" would each be a different, weaker theorem.
Useful infrastructure: finite expectations over product measures, a negative-correlation inequality for products, Abel summation (Finset.sum_range_by_parts), and $1-x\le e^{-x}$ . Proofs of any milestone, and of the theorem from the milestones, are welcome.

Selected references

B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025. arXiv:2106.06892v3. https://arxiv.org/abs/2106.06892
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3):324–360, 2006. https://doi.org/10.1145/1147954.1147956
N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP is the cure for your matching woes: improved bounds for stochastic matchings, Algorithmica 63(4):733–762, 2012. https://doi.org/10.1007/s00453-011-9511-8
Y. Hikima, Y. Akagi, H. Kim, M. Kohjima, T. Kurashima, H. Toda, Integrated optimization of bipartite matching and its stochastic behavior: new formulation and approximation algorithm via min-cost flow optimization, The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI 2021) (reference [28] of the paper; no link).
A. Borodin, C. MacRury, Online bipartite matching in the probe-commit model, Mathematical Programming, 2025, pp. 1–54 (reference [9] of the paper; no link).

10 thms3 active usersReviewed

Experimental Design Operations Research Probability+1·Captain: mikedeng1

Pigeonhole Design: Balancing Sequential Experiments from an Online Matching Perspective 3: For p ≥ 2 Continuous Covariates, Expected Discrepancy O(T^(1−φ) + T^((p−1)φ)), with (log T)^(3/2) at p = 2Research Paper

Motivation

Online platforms run randomized experiments on subjects (users, sessions, orders) that arrive one at a time and must be assigned to a control or a treatment group on arrival, before later subjects are seen. The precision of a treatment-effect estimate depends on how similar the two groups are in their observed covariates. When the groups are badly balanced, the estimator's variance grows, and a large literature on covariate balancing (blocking, rerandomization, matched pairs) addresses this for offline experiments, where all covariates are known in advance.

J. Zhao and Z. Zhou (arXiv:2201.12936, Management Science, 2025) cast the online problem as an online matching problem. The cost of an assignment is the discrepancy, the weight of a minimum-cost perfect matching between the two groups, and they compare three designs against an oblivious adversary that fixes the covariate sequence in advance:

the clairvoyant matched-pair design;
the completely randomized design;
their online pigeonhole design.

For one continuous covariate the pigeonhole design attains $O(T^{1/4}(\log T)^{1/2})$ against $\Theta(T^{1/2})$ for complete randomization. This mission concerns the multi-dimensional result, Theorem 9.

Setting

$T$ subjects arrive in order; $T$ is even. Subject $t$ carries a covariate vector $x_t$ with $q$ discrete coordinates, the $i$ -th in a finite set $S_i\subseteq[0,1]$ of size $m_i$ , and $p\ge2$ continuous coordinates in $[0,1]$ . Distances are Euclidean in $\mathbb R^{q+p}$ . An assignment puts each subject in control ( $A$ ) or treatment ( $B$ ).

The discrepancy of a split with $|A|=|B|$ is

d_{A,B}=\min_{\sigma:A\to B\text{ bijective}}\ \sum_{t\in A}\lVert x_t-x_{\sigma(t)}\rVert_2 ,

the value of the assignment problem (1) of the paper.

The completely randomized design picks $A$ uniformly among the $\binom{T}{T/2}$ subsets of size $T/2$ ; $\mathrm{ALG}^C(x)$ is the mean of $d_{A,B}$ .

A pigeonhole design fixes a partition of the covariate space into pigeonholes. When subject $t$ arrives:

if one group already has $T/2$ subjects, $t$ joins the other group;
otherwise $t$ joins the group that has fewer subjects in its own pigeonhole, and on a tie a fair coin decides.

Theorem 9 uses the pigeonholes

\mathcal P(\mathcal S)=S_1\times\cdots\times S_q\times\Big\{[0,c^{1/p}T^{-\varphi}),\ \dots,\ [1-c^{1/p}T^{-\varphi},1]\Big\}^p ,

uniform cells of edge $c^{1/p}T^{-\varphi}$ on each continuous axis, for parameters $\varphi\in(0,1)$ and $c>1$ . The expected discrepancy is the mean of $d_{A,B}$ over the design's coins.

Formalization targets

Goal: Theorem 9 (p. 26)

There are $C>0$ and $T_0$ , depending only on $p,q,S_1,\dots,S_q,\varphi,c$ , such that for every even $T\ge T_0$ and every admissible arrival sequence,

\mathbb E[d_{A,B}]\le C\Big(T^{1-\varphi}+T^{(p-1)\varphi}\,\lambda_p(T)\Big),\qquad \lambda_2(T)=(\log T)^{3/2},\quad \lambda_p(T)=1\ (p\ge3).

Milestones

Lemma EC.1: Hoeffding for a binomial, $\Pr(|H(n)-pn|\le\sqrt{n\log n})\ge1-2/n^2$ .
Lemma 5, $p=2$ : if $T=m^2$ and the subjects occupy each cell of the $m\times m$ grid exactly once, then $\mathrm{ALG}^C(x)=O(T^{1/2}\log T)$ .
Lemma 5, $p\ge3$ : on the full grid of $T=m^p$ cells, $\mathrm{ALG}^C(x)=O(T^{(p-1)/p})$ .
Balance: every run of a pigeonhole design has $|A|=|B|=T/2$ .
Component 1: the subjects paired within their pigeonhole before the stopping time $\tau$ contribute at most $\tfrac12c^{1/p}\sqrt p\,T^{1-\varphi}$ , on every run.
Unmatched subjects: at most one unmatched subject per pigeonhole, $H^0_\tau+H^1_\tau$ at most the number of pigeonholes, and $|H^0_\tau-H^1_\tau|=T-\tau$ .
Component 2: the remaining subjects contribute $O(T^{(p-1)\varphi}\lambda_p(T))$ in expectation.

Corollary 2 (the case $\varphi=1/p$ ) is an extra theorem after the goal.

Significance

At $\varphi=1/p$ Theorem 9 gives $O(T^{(p-1)/p})$ for $p\ge3$ . This is the order $\Theta(T^{(p-1)/p})$ of the matched-pair design (Theorem 7), which sees all covariates in advance. An online design that commits to each assignment on arrival therefore loses at most a constant factor in dimension $p\ge3$ , and at most a $(\log T)^{3/2}$ factor at $p=2$ . For the completely randomized design no comparable upper bound is known for general sequences (p. 21). Lemma 5 is the paper's bound for complete randomization on the special family of full grids, and is of independent interest as a random-labelling matching estimate.

The results are proved on paper; none of them has a machine-checked proof, and the platform holds no item on them. A formalization would close the gaps of the printed argument:

Lemma 5's induction for $p=2$ ends at $\sqrt T(\log T)^{3/2}$ rather than the stated $\sqrt T\log T$ .
Component 2 applies Lemma 5 to unmatched subjects, which occupy distinct cells but do not fill the grid.
The case $q\ge1$ is argued per discrete support, although the balancing rule acts across supports.

Every statement in the mission is believed true.

Difficulty

The matched part (Component 1) is deterministic: paired subjects share a pigeonhole of diameter $O(T^{-\varphi})$ . The difficulty lies in the subjects left over: the unmatched ones and the subjects after $\tau$ . Their labels come from coins, but which subjects end up unmatched, and when $\tau$ occurs, depend on the same coins. So the leftover set is not a fixed set with independent fair labels, and the conditional binomial law used on p. ec22 does not hold literally.

A second obstacle is the random-matching estimate itself. Bounding the expected optimal matching between randomly labelled points of a grid at the rates $T^{1/2}\log T$ ( $p=2$ ) and $T^{(p-1)/p}$ ( $p\ge3$ ) is a multi-scale problem of Ajtai–Komlós–Tusnády type. A single-scale count of imbalances per cell gives only $T^{1/2}$ times a power of $T$ that is too large.

Formalization scope

Subjects are indexed $0,\dots,T-1$ ; an assignment is a map to Bool (false = control). The covariate space is EuclideanSpace ℝ (Fin q ⊕ Fin p). Admissible sequences have discrete coordinates in $S_i$ and continuous ones in $[0,1]$ , with $S_i\subseteq[0,1]$ (the paper's normalisation).
Discrepancy: an infimum over bijections between the groups. An unbalanced split has the junk value $0$ . The designs, the matched set and its complement are balanced on every run, so the junk is never reached.
Cells: the printed edge $c^{1/p}T^{-\varphi}$ gives a partition only when $c^{-1/p}T^{\varphi}$ is an integer. The formalization uses $m=\lceil c^{-1/p}T^{\varphi}\rceil$ cells per axis of edge $1/m\le c^{1/p}T^{-\varphi}$ , with the last cell closed. A pigeonhole is keyed by the exact discrete values and the cell index on each axis. The partition is the printed one, not a quantified family.
Randomness: the pigeonhole design uses one coin per subject, consulted only on a tie. Its expected discrepancy is the average over all $2^T$ coin vectors, which is exactly the paper's law. The completely randomized design averages over all $\binom{T}{T/2}$ control sets.
Asymptotics: $O(f(T))$ means $\exists C>0,\exists T_0,\forall T\ge T_0$ even, $\forall x$ admissible. $C$ and $T_0$ are chosen before $T$ and $x$ and depend only on the fixed parameters. $\log$ is the natural logarithm.
Lemma 5's family $\mathcal X$ : $T=m^p$ subjects in $[0,1]^p$ , one per cell, stated as injectivity of the cell map.
Stopping objects: $\tau$ is the first $n$ at which a group holds $T/2$ subjects. Within a pigeonhole the subjects before $\tau$ are paired in arrival order, and the last one is unmatched when their number is odd.
Corrections to the page: the second cell printed as $[T^{-\varphi},2c^{1/p}T^{-\varphi})$ on p. ec21 is read as $[c^{1/p}T^{-\varphi},2c^{1/p}T^{-\varphi})$ . The family's $x'_t\notin\mathbb X$ is read as $x_{t'}\notin\mathbb X$ . The bound $H\le\frac1cT^{p\varphi}$ becomes $H\le(\prod_i m_i)\,m^p$ under the ceiling and the discrete supports.

The following formalizations would trivialize the mission and are ruled out:

a bound on the discrepancy of one run, or of the best run, instead of the average over all coin vectors;
constants that depend on $T$ or $x$ ;
an unbalanced design that exploits the junk value $0$ ;
an arbitrary partition in place of the printed grid.

A complete development needs a binomial Hoeffding bound and an exact analysis of the design's recursion (balance, alternation within a pigeonhole before $\tau$ ). It also needs a multi-scale bound on random bichromatic matchings of grid points. That bound is reusable for Lemma 5 and for matching estimators generally. Contributions on any milestone are welcome, as are proofs of Lemma 5 for arbitrary subsets of grid points, which is what Component 2 needs.

Selected references

J. Zhao and Z. Zhou, Pigeonhole Design: Balancing Sequential Experiments from an Online Matching Perspective, Management Science, 2025; arXiv:2201.12936v6, 2024. https://arxiv.org/abs/2201.12936
M. Ajtai, J. Komlós and G. Tusnády, On optimal matchings, Combinatorica 4 (1984) 259–264. https://doi.org/10.1007/BF02579135
N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015) 707–738. https://doi.org/10.1007/s00440-014-0583-7
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Bandit Algorithms Machine Learning+1·Captain: mikedeng1

Optimal No-regret Learning in Repeated First-price Auctions 2: The ML-IS-UCB Bidding Policy Achieves Expected Regret at Most C√T log³ T for Every Oblivious Private-Value SequenceResearch Paper

Learning to bid in first-price auctions

Display advertising has been moving from second-price to first-price auctions: several exchanges began rolling them out in 2017, and Google Ad Manager completed its move at the end of 2019 (Davies 2019). In a second-price auction bidding one's value is a dominant strategy; in a first-price auction the optimal bid depends on the distribution of the competing bids, which a bidder does not know and must learn from repeated play. Most of the learning literature on auctions takes the seller's side of the second-price auction (reserve prices, e.g. Cesa-Bianchi, Gentile, Mansour 2015); on the bidder's side of the first-price auction, the main prior approach is the cross-learning framework of Balseiro et al. 2019.

Han, Zhou and Weissman (arXiv:2003.09795) study the bidder's problem with the feedback that ad exchanges actually provide, where only the winning price is announced, and with no assumption on the distribution of the competing bids. Their two upper bounds are $\widetilde O(\sqrt T)$ regret: Theorem 1 for iid private values and Theorem 2, the subject of this mission, for values chosen by an oblivious adversary. A matching $\Omega(\sqrt T)$ lower bound holds even under full information (Theorem 9).

Setting

A single bidder plays $T$ rounds. In round $t$ she observes a private value $v_t\in[0,1]$ , bids $b_t\in[0,1]$ , and wins if $b_t\ge m_t$ , where $m_t\in[0,1]$ is the highest other bid (HOB). Her payoff is (1)

r(v_t,b_t;m_t)=(v_t-b_t)\,\mathbb 1(b_t\ge m_t).

The HOBs are iid with an unknown cumulative distribution function $G(x)=\mathbb P(m_t\le x)$ on $[0,1]$ ; $G$ may be discrete, continuous or mixed. Feedback is censored: after round $t$ only $\max\{b_t,m_t\}$ is revealed, so $m_t$ is observed only when the bidder loses. The expected reward is $R(v,b)=(v-b)G(b)$ , and the regret of a policy $\pi$ against the value sequence $v=(v_1,\dots,v_T)$ is (3)

R_T(\pi;v)=\sum_{t=1}^T\Big(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Big),

the shortfall against an oracle that knows $G$ . A policy bids in round $t$ as a (possibly randomized) function of $v_1,\dots,v_t$ and of the feedback of rounds $1,\dots,t-1$ . An oblivious adversary fixes the whole value sequence in advance, independently of the bids and the HOBs.

The policy analysed is ML-IS-UCB (Algorithm 4). It restricts bids to the grid $b^i=(i-1)/K$ , $i\in[K]$ , with $K=\lceil\sqrt T\rceil$ ; it splits time into $L=\lceil\log_2T\rceil$ levels after an initialization phase of $T_0=(L+1)\lceil\sqrt T\rceil$ zero bids; and at each level it computes a width $w^\ell_{i,t}$ , an interval-splitting reward estimate $\hat r^\ell_{i,t}$ and a candidate set $\mathcal B^\ell_t$ by the displays (12)–(16).

Formalization targets

Goal: Theorem 2

There is an absolute constant $C>0$ such that for every $T\ge2$ some policy $\pi$ satisfies, for every value sequence $v\in[0,1]^T$ and every $G$ on $[0,1]$ ,

\mathbb E\big[R_T(\pi;v)\big]\le C\sqrt T\log^3T .

The constant is unspecified, so the goal survives any improvement of the constants below.

The explicit bound: Theorem 7

For every $\gamma\ge3$ , the ML-IS-UCB policy satisfies

\mathbb E\big[R_T(\pi^{\mathrm{ML\text{-}IS\text{-}UCB}};v)\big]\le4+(L+4)\lceil\sqrt T\rceil+80\gamma^{3/2}\log(LKT)(1+\log T)\,L\sqrt T .

Milestones

In the order of the proof (Section 4.3 and Appendix C):

Lemma 7: with probability at least $1-4T^{-3}$ , $|\hat r^\ell_{i,t}-r_{i,t}|\le w^\ell_{i,t}$ for all $i,\ell$ and $T_0<t\le T$ , and $w^\ell_{i,t}$ is bounded by (18) in terms of the true interval probabilities $p_j=G(b^{j+1})-G(b^j)$ .
Lemma 8: on that event the best grid bid is never eliminated, and a round assigned to level $\ell$ has regret at most $8\cdot2^{-\ell}$ against the grid.
Display (19): the grid regret is at most $T_0+8\sum_\ell2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|$ .
Lemma 16: a deterministic counting bound for the sums $\sum_t\sum_{j\ge i(t)}v_j/n^\ell_{j,t}$ .
Lemma 9: $2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|\le10\gamma^{3/2}\log(LKT)(1+\log T)\sqrt T$ .
Theorem 7.

A supporting item, not a milestone, states the quantization step $\max_{b\in[0,1]}R(v,b)\le\max_iR(v,b^i)+1/K$ for the grid of Algorithm 4.

Significance

The result shows that adversarial values cost at most a logarithmic factor relative to iid values in repeated first-price auctions with censored feedback, and that no regularity of $G$ is needed. ML-IS-UCB is also an algorithmic template: its widths are computed before the data of the current level is used, which makes the estimates at each level independent of the bids that select them, and its interval-splitting estimator uses the variance of each interval rather than a uniform bound. Remark 3 notes that replacing the interval probabilities by $1$ gives only $\widetilde O(\sqrt{KT})$ .

All results of the paper are proved in the preprint; none of them is machine-checked. A complete development formalizes a multi-level elimination algorithm with data-dependent level assignment, a Bernstein-type concentration argument for estimates indexed by random sets, and the counting lemma behind the logarithmic factors. Each of these is reusable for other elimination-based bandit algorithms.

Difficulty

The obvious route is a single UCB index per grid bid, (11) on p. 27, built from all past observations through the estimates $\hat p^t_j=\sum_{s\le t}\mathbb 1(b_s\le b^j)\mathbb 1(m_s\in(b^j,b^{j+1}])/\sum_{s\le t}\mathbb 1(b_s\le b^j)$ . It fails because $\hat p^t_j$ is not a normalized binomial variable: each bid depends on the earlier HOBs, so conditioned on the bids the HOBs are no longer independent and $\hat p^t_j$ is not even unbiased. Self-normalized martingale bounds control each $\hat p^t_j$ separately but not the sum $\sum_{j\ge i}\hat p^t_j$ that the reward estimate needs. Algorithm 4 restores conditional independence through its level structure, and Lemma 7 has to make that precise: the sets $\Phi^\ell(t)$ are random, and the bound must hold uniformly over all $(i,\ell,t)$ with a variance term estimated from a held-out sample. Lemma 9 then needs the variance-sensitive width (18); a crude width loses a factor $\sqrt K$ (Remark 3).

Formalization scope

Model. Rounds are Fin T; Lean round $t$ is paper time $t+1$ . The HOB law is a probability measure μG on ℝ with μG [0,1]ᶜ = 0, and $G(x)$ is (μG (Set.Iic x)).toReal; atoms are allowed. The maximum in (3) is a supremum over $[0,1]$ .
Policies. A policy has internal randomness $u\sim\mu_U$ and, for each $u$ , a bidding rule whose round- $t$ bid receives only the values of rounds $\le t$ and the feedback $\max\{b_s,m_s\}$ of rounds $<t$ , enforced by the argument types; bids lie in $[0,1]$ and are jointly measurable. The expectation is a Bochner integral over $u$ and $m\sim G^{\otimes T}$ , and Theorems 2 and 7 also assert integrability, so the integral cannot be a junk value.
Algorithm 4. Grid indices are 0-based ( $b^{i+1}=i/K$ , $b^{K+1}=1$ ); inside the algorithm times are the paper's $1,\dots,T$ . Every quantity $n,w,\hat p,\hat r,\mathcal B$ is defined by its formula for every $(i,\ell,t)$ . The estimators (14) and $\hat p^0$ are computed from the feedback, not from $m$ , and the algorithm recomputes its own past decisions, so it is a censored-feedback rule. "An arbitrary $i$ " is a selection rule depending on the time and the level only. If no level breaks (impossible for $\gamma\ge3$ , $T\ge2$ ) the round goes to level $L$ with bid $0$ .
Hypotheses added to the printed statements, each disclosed in its item: $T\ge2$ in Theorem 2 (the printed bound is $0$ at $T=1$ ); Lemmas 8, 9 and (19) are stated pathwise under the inequalities of Lemma 7 that their proofs use; Lemma 16 assumes that the set contains $\lceil\sqrt T\rceil$ initialization rounds with bid $0$ , which its proof uses; the quantization display is adapted from the grid of Lemma 4 to that of Algorithm 4.
Ruled out. A policy that reads $m_t$ , $G$ or future values, a constant $C$ chosen after $T$ , $v$ or $G$ , a policy chosen after $v$ or $G$ , and an expectation of a non-integrable function would each make the goal trivial; the statements exclude all four.
Needed and welcome. Bernstein and multiplicative Chernoff bounds for binomial variables (Lemmas 14, 15 of the paper are cited from the literature), measurability of the run of the algorithm, and the harmonic-sum bound $\sum_{k=a}^T1/k\le1+\log T$ . Contributions toward any milestone, or alternative proofs of the goal, are welcome.

Selected references

Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
N. Cesa-Bianchi, C. Gentile, Y. Mansour, Regret Minimization for Reserve Prices in Second-Price Auctions, IEEE Transactions on Information Theory 61(1), 2015. https://doi.org/10.1109/TIT.2014.2365772
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
J. Davies, What to know about Google's implementation of first-price ad auctions, Digiday, 2019. https://digiday.com/media/buyers-welcome-auction-standardization-as-google-finally-goes-all-in-on-first-price/

13 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Lightning Network Economics: Topology II: A Lightning Network with Average Degree Above 2g₊⁻¹(2·disc) Contains a Hermetizable SetResearch Paper

Why hubs appear in payment-channel networks

The Lightning Network (LN) is a layer-two payment system for Bitcoin. Two parties open a payment channel by locking funds on the blockchain and can then pay each other off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it has to carry. Guasoni, Huberman and Shikhelman (SSRN 4439190, version of February 3, 2023; published in Management Science, 2024) ask which network topologies support a given pattern of payments at least cost, using only qualitative properties of the channel cost derived in their earlier work on channel sizing (Guasoni, Huberman and Shikhelman, Lightning Network Economics: Channels, 2022, cited in the paper as [GHS22]).

One of the paper's central findings is that adding a new hub node, and routing the traffic of a group of nodes through it, reduces cost in a broad class of networks. This explains, from cost considerations alone, why hub-and-spoke structures emerge in deployed payment-channel networks. This mission formalizes the deterministic sufficient condition for that phenomenon (Theorem 3.8) and the chain of lemmas in Appendix B.1 that proves it.

Setting

Fix a finite set $V$ of nodes. A Lightning Network is an anti-symmetric real matrix $\Lambda=(\lambda_{i,j})_{i,j\in V}$ : $\lambda_{u,v}$ is the net flow from $u$ to $v$ in the channel between them, $\lambda_{u,v}=-\lambda_{v,u}$ , and $\lambda_{u,v}=0$ means there is no channel.

A channel cost is a function $c:\mathbb R\to\mathbb R_+$ that is strictly increasing on $[0,\infty)$ (MO), even (SY), zero at zero (CI), and strictly subadditive, $c(x+y)<c(x)+c(y)$ for $x,y>0$ (SA). It satisfies (SA+) with a nonnegative, strictly increasing $g_+$ on $[0,\infty)$ if $c(kx)<\tfrac{k}{g_+(k)}\,c(x)$ for all $k>1$ , $x>0$ : when the flow of a channel grows $k$ -fold, its cost grows by at most $k/g_+(k)$ . The cost of the network is $c(G)=\tfrac12\sum_{i,j}c(\lambda_{i,j})$ .

For a node $v$ and a set $U$ of nodes, $d_U(v)$ is the number of channels of $v$ into $U$ , $s_U(v)$ the smallest and $S_U(v)$ the largest absolute flow of these channels, $\delta(U)=\min_{v\in U}d_U(v)$ the minimum degree, and $\mathrm{disc}(U)=\max_v c(S_U(v))/c(s_U(v))$ the discrepancy, the maximum over nodes of $U$ with a channel in $U$ . For $U=V$ these are $d(v)$ , $s(v)$ , $S(v)$ , $\delta(G)$ , $\mathrm{disc}(G)$ , and $\bar d(G)=\sum_v d(v)/|V|$ is the average degree.

The hermetization of $U$ deletes all channels among nodes of $U$ , adds a new node $v_0$ , and joins each $i\in U$ to $v_0$ by a channel carrying $\sum_{j\in U}\lambda_{i,j}$ , its net flow towards $U$ ; every node keeps its net flow. $U$ is hermetizable if hermetization strictly reduces the cost, and the network is hermetizable if some $U$ is.

Formalization targets

Goal: Theorem 3.8 (existence part)

Under (MO)–(SA+), every network with at least one channel and

\bar d(G)\;>\;2\,g_+^{-1}\big(2\,\mathrm{disc}(G)\big)

is hermetizable. The cost function and $g_+$ are arbitrary subject to the axioms.

Milestones

Lemma B.1. A nonempty $U$ is hermetizable if $d_U(i)>g_+^{-1}\big(2c(S_U(i))/c(s_U(i))\big)$ for every $i\in U$ .
Lemma B.2. A nonempty $U$ is hermetizable if $\delta(U)\ge g_+^{-1}\big(2\,\mathrm{disc}(U)\big)$ .
Lemma B.4. A finite graph of average degree at least $2d$ , $d>0$ , has a nonempty induced subgraph $G'$ with $\delta(G')>d$ .
Lemma B.3 (the peeling procedure). Repeatedly deleting every vertex with at most $t$ neighbours among the remaining vertices returns the largest vertex set inducing minimum degree $>t$ ; it is empty exactly when no such set exists.

Significance

Theorem 3.8 turns a qualitative property of channel costs into a checkable topological criterion: if a network is dense relative to how unequal its channel flows are, a cost-reducing hub exists. The paper uses it to argue that such restructuring is profitable for an intermediary who charges part of the savings, and its probabilistic companion (Theorem 3.9) shows that random networks whose channel costs have light tails are hermetizable with high probability. The degree-to-subgraph Lemma B.4 is a standard tool of extremal graph theory (Diestel, Graph Theory, Prop. 1.2.2), and Lemma B.3 is the classical $k$ -core peeling.

Mathematically the result is proved in the paper. None of it is formalized: Lean's Mathlib has minimum degree and induced subgraphs but neither Lemma B.4 nor the correctness of $k$ -core peeling, and there is no formal model of payment-channel networks or of hermetization. The mission produces that model, machine-checked versions of the Appendix B.1 lemmas, and a statement of Theorem 3.8 under axioms that are actually satisfiable (see below).

Difficulty

The cost comparison in Lemma B.1 is node by node: the channels of a node inside $U$ are replaced by one channel to the hub carrying their sum. The obvious bound on the hub channel's cost uses only monotonicity and subadditivity, and that is too weak: a single channel carrying the sum of $d$ flows can cost almost as much as the $d$ channels it replaces, while the deleted channels are each shared by two nodes. The quantitative axiom (SA+) is what makes the comparison strict, and the discrepancy controls how unequal the replaced flows may be.

Passing from the average degree of the whole network to a subnetwork in which every node has high degree is the second step, and it must keep track of the fact that the discrepancy of an induced subnetwork can be smaller but never larger than that of the network. Lemma B.4 needs an argument that the deletion process cannot exhaust the graph; a counting argument that treats every deleted vertex alike loses exactly the margin needed.

Formalization scope

Nodes form an arbitrary finite type V; the network is Λ : V → V → ℝ with anti-symmetry IsLN. The hub is the extra element none of Option V. The cost is the $\tfrac12\sum_{i,j}$ form. In Lemmas B.1 and B.2 all degree data are those of the subnetwork induced on $U$ ; in Theorem 3.8 those of the whole network. $s(v)$ has the junk value $0$ for a node without channels, so every statement assumes the relevant nodes have a channel, and the discrepancy is a maximum over nodes having a channel.

Two axioms are corrected from the printed page and the correction is part of the statement. (SA) is printed for $x>y\ge0$ , which at $y=0$ reads $c(x)<c(x)$ ; it is stated for all $x,y>0$ , the form the paper's Appendix D verifies. (SA+) is printed for all $k\in\mathbb R_+$ , which fails at $x=0$ and, for the paper's own example cost, at every $k\le1$ ; it is stated for $k>1$ , $x>0$ . Under the printed axioms every theorem would hold vacuously.

$g_+$ is strictly increasing but not assumed onto, so $g_+^{-1}$ is replaced throughout by the equivalent $g_+$ -form: $d>g_+^{-1}(y)$ becomes $g_+(d)>y$ , as in the paper's own proof of Lemma B.1. Theorem 3.8 therefore assumes $g_+(\bar d(G)/2)>2\,\mathrm{disc}(G)$ and, explicitly, that the network has a channel (implied by the printed hypothesis). Lemma B.4 adds $d>0$ and reads "average degree $2d$ " as "at least $2d$ ", as its proof does. The polynomial-time clause of Theorem 3.8 and the $O(V+E)$ bound of Lemma B.3 are complexity claims and are not formalized; Lemma B.3 is posed as correctness of the procedure in its proof, which finds minimum degree $>t$ (the printed statement says $\ge t$ ).

Formalizations that would trivialize the mission are excluded: a specific cost such as $c(x)=2(B|x|/r)^{1/2}$ or a specific $g_+$ ; hermetizability defined by the per-node inequality instead of the cost comparison; Theorem 3.8 with the empty set allowed to witness hermetizability (the strict cost decrease rules it out); Lemma B.4 without nonemptiness; and Lemma B.3 as "there exists an algorithm".

The definitions (network, cost axioms, degree data, hermetization, peeling) are reusable by the companion missions on this paper. Proofs of any milestone are welcome, Lemma B.4 and Lemma B.3 being independent of the network model.

Selected references

P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Topology, SSRN working paper 4439190, version of February 3, 2023, https://ssrn.com/abstract=4439190; published in Management Science, 2024, https://doi.org/10.1287/mnsc.2023.03872 (theorem numbers here follow the SSRN version).
P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, 2022 (cited in the paper as [GHS22]; no stable link is given there).
R. Diestel, Graph Theory, 5th ed., Springer, 2017, Proposition 1.2.2. https://doi.org/10.1007/978-3-662-53622-3
J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, 2015. https://lightning.network/lightning-network-paper.pdf

10 thms3 active usersReviewed

Completed

Machine Learning Operations Research Optimization·Captain: mikedeng1

Contextual Inverse Optimization: Offline and Online Learning 2: The Greedy Circumcenter Policy Can Incur Regret Linear in the Horizon from a Pointed Knowledge SetResearch Paper

Learning a cost vector from optimal decisions

In inverse optimization, an observer sees decisions made by an expert who solves an optimization problem, and wants to recover the expert's unknown objective. Besbes, Fonseca and Lobel study a contextual version: in each period a feasible set and a context function are revealed, a learner must act before seeing the expert's choice, and then observes the expert's optimal action. The learner pays the expert's cost of its own action. This models, for example, a platform imitating a dispatcher's routing decisions or a recommender learning a user's trade-offs, where only optimal choices, not costs, are ever observed (Besbes, Fonseca, Lobel, arXiv:2106.14015).

For the one-period (offline) problem the paper shows that the circumcenter policy, which acts as if the unknown cost were the center of the smallest revolution cone containing the set of costs still consistent with the data, is minimax optimal (Theorem 1). The natural online policy is to apply it greedily in every period. This mission formalizes the paper's Theorem 2, which shows that this greedy policy can fail badly: its worst-case regret can grow linearly in the horizon, even when the initial uncertainty is small in a precise geometric sense.

Setting

Costs live in $\mathbb R^d$ and actions in $\mathbb R^n$ . The true cost $c^\star$ lies on the unit sphere $S^d$ . An action set $\mathcal X\in\mathfrak B$ is a nonempty compact subset of $\mathbb R^n$ of diameter at most $1$ ; a context function $f\in\mathfrak F$ is a $1$ -Lipschitz map $\mathbb R^n\to\mathbb R^d$ . The forward problem with cost $c$ has solution set

\psi(c,\mathcal X,f)=\arg\min_{x\in\mathcal X} f(x)'c .

The angle between nonzero vectors is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$ , set to $0$ if either vector is $0$ . The uncertainty angle of a set $C$ is

\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\theta(c,\hat c),

and a circumcenter $\hat c(C)$ is a unit vector attaining this infimum. A set is pointed when $\alpha(C)<\pi/2$ , i.e. it fits inside an open half-space cone.

Online protocol. In periods $t=1,\dots,T$ nature reveals $\mathcal X_t$ and $f_t$ , the learner picks $x^\pi_t\in\mathcal X_t$ , and then an optimal expert action $x^\star_t\in\psi(c^\star,\mathcal X_t,f_t)$ is revealed. Starting from a closed set $C_0\subseteq S^d$ , the knowledge set is

C(\mathcal I_t)=\{c\in C_0:\ c'f_s(x^\star_s)\le c'f_s(x)\ \ \forall x\in\mathcal X_s,\ s<t\},

the regret is $R^\pi_T=\sum_{t=1}^T\big(f_t(x^\pi_t)-f_t(x^\star_t)\big)'c^\star$ , and the worst-case regret $\mathcal{WCR}^\pi_T(C_0)$ is its supremum over $c^\star\in C_0$ and admissible instances. The greedy circumcenter policy chooses $x^\pi_t\in\psi\big(\hat c(C(\mathcal I_t)),\mathcal X_t,f_t\big)$ .

Formalization targets

Goal: Theorem 2 (pp. 13–14)

There is a closed, nonempty, pointed $C_0\subseteq S^3$ such that

\mathcal{WCR}^{\pi_{greedy}}_T(C_0)=\Omega(T).

Concretely: there are $C_0$ and $\kappa>0$ such that for every horizon $T\ge1$ some $c^\star\in C_0$ and admissible $(\mathcal X_t,f_t)$ admit a greedy run, and every greedy run (any circumcenter, any tie-break) has regret at least $\kappa T$ . The constant $\kappa$ is left existential, as the page claims only $\Omega(T)$ .

Milestones (the proof's displayed steps, App-9–App-11)

Lemma 2 (p. 12): a circumcenter exists for every nonempty set, and is unique when the set is pointed and not $\{0\}$ .
Step 1: for $0<\bar\alpha<\pi/2$ and $0\le\varepsilon\le\tan\bar\alpha/2$ , the set $C_{\varepsilon,\bar\alpha}$ , a polyhedral cone cut by three half-spaces and intersected with $S^3$ , has the unique circumcenter

\hat c(C_{\varepsilon,\bar\alpha})=\tfrac{1}{\sqrt{1+\varepsilon^2}}(1,\varepsilon,0).

Step 2: with $C_0=C_{0,\bar\alpha}$ , $f_t=\mathrm{id}$ , $\mathcal X_t=\{\bar x_t,0\}$ , $\varepsilon_t=t\tan\bar\alpha/(2T)$ , the greedy knowledge sets are $C(\mathcal I_t)=C_{\varepsilon_{t-1},\bar\alpha}$ .
Step 3: in that instance, with $\tan\bar\alpha\le 2$ , each period's regret is at least $\sin\bar\alpha/4$ .

Significance

The result separates offline from online learning in this model. Theorem 1 makes the circumcenter the best one-shot guess, yet Theorem 2 shows that one-shot optimality says nothing about information collection: a greedy learner can keep choosing actions that are wrong by a fixed margin while the revealed expert actions cut away only slivers of the knowledge set. This is the reason the paper introduces its EllipsoidalCones algorithm, which acts greedily on an enlarged ellipsoidal-cone superset and attains logarithmic regret for pointed initial sets. Theorem 2 is the lower bound that makes that design necessary.

On the formal side, the paper's proof is complete but compressed; it asserts the circumcenter of a three-generator spherical polygon "using Definition 2" and leaves the induction's geometric inclusions to the reader. A machine-checked version fixes the normalization of the circumcenter and the quantitative condition behind " $\varepsilon^2\le1$ ", and gives a reusable formal treatment of uncertainty angles and circumcenters, which the paper's other results (Theorem 1, Theorem 3, Lemma 10) all use. No result of the paper has a formal statement or proof on Prove2Me yet.

Difficulty

The arithmetic of Step 3 is elementary once the knowledge sets are known. The difficulty is in Steps 1 and 2. Identifying the circumcenter of $C_{\varepsilon,\bar\alpha}$ requires a minimax argument over the whole sphere: one must show that no other unit vector has a smaller maximal angle to the three extreme rays, and that the minimizer is unique, which rests on Lemma 2. The greedy policy is defined through this minimizer, so without uniqueness nothing can be said about its actions. Step 2 then needs an exact description of each knowledge set: showing that the new half-space makes the previous one redundant inside $C_0$ requires the sign information carried by the other constraints. A naive bound on the regret that ignores the knowledge-set dynamics fails, because a priori the policy might learn $c^\star$ after a few periods.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), so norms, diameters and Lipschitz constants are Euclidean. The angle uses the paper's convention $\theta(c,0)=\theta(0,\hat c)=0$ ; Mathlib's InnerProductGeometry.angle is not used. Action sets are required to be nonempty (otherwise no action exists). Periods are $0$ -based in Lean: Lean period $t$ is the paper's period $t+1$ , and Lean's knowledge set at $t$ is the paper's $C(\mathcal I_{t+1})$ . The construction and the goal are in dimension $d=3$ , as in the proof; the goal holds for every action dimension $n\ge1$ .

The worst-case regret is never written as a real supremum, whose junk values would decide the statement. The lower bound is stated by exhibiting the instance. A run of the greedy policy is a predicate quantifying over every circumcenter choice and every minimizer, and nature's sequences are arbitrary. Two pins relative to the page: the printed circumcenter $(1,\varepsilon,0)$ is normalized as in Step 3, and Step 3 assumes $\tan\bar\alpha\le2$ , which the page's " $\varepsilon^2\le1$ " needs (the goal uses $\bar\alpha=\pi/4$ ).

Two trivializations are ruled out. Without pointedness the claim holds for $C_0=S^3$ with antipodal costs, so $\alpha(C_0)<\pi/2$ is part of the goal. A bound over all runs would hold vacuously if no run existed, so the goal also asserts that a greedy run exists.

A complete development needs spherical geometry of polyhedral cones (extreme rays, angles to a cone), continuity of the uncertainty-angle objective for Lemma 2, and elementary trigonometry. The Geometry and Online definitions are shared with the other missions of this series and are reusable for any work on inverse optimization or learning from revealed preferences. Proofs of any milestone are welcome, as are alternative arguments for Lemma 2.

Selected references

O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023 (preprint used here; published in Operations Research, 2025). https://arxiv.org/abs/2106.14015
M. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485
R. K. Ahuja, J. B. Orlin, Inverse Optimization, Operations Research 49(5), 2001. https://doi.org/10.1287/opre.49.5.771.10607

9 thms3 active usersReviewed

Combinatorics Operations Research Optimization+2·Captain: mikedeng1

Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes I: With Patience at Least 2, Attenuated Random-Order Probing Gives Every Edge a(e)·Pr[e Is Free] ≥ β*Research Paper

Motivation

In offline stochastic matching a graph is given in which every edge is present only with some known probability, and the only way to find out is to probe it: a probed edge that turns out to be present must be added to the matching at once. Each vertex may also limit how many of its edges are probed (its patience). The model captures applications in which a proposed match may be refused and an accepted one is binding: organ (kidney) exchange, online dating, advertising, crowdsourcing and ride sharing are the examples the paper lists (pp. 1–2), following Chen, Immorlica, Karlin, Mahdian and Rudra (ICALP 2009) and Bansal, Gupta, Li, Mestre, Nagarajan and Rudra (Algorithmica 2012).

Finding the best probing strategy is computationally hard, so algorithms are compared with a linear-programming relaxation that upper-bounds every strategy (Lemma 1, from Bansal et al.).

Timeline (general graphs with patience, as recorded on p. 2 of the paper).

2012: Bansal et al., a $0.25$ -approximation.
2015: Adamczyk, Grandoni and Mukherjee, $0.269$ .
2018: Baveja, Chavan, Nikiforov, Srinivasan and Xu, $0.31$ .
2021–2026: Brubach, Grammel, Ma, MacRury and Srinivasan (arXiv:2106.06892v3; Mathematics of Operations Research, 2025), $0.382$ when every patience is at least $2$ . Their algorithm processes the edges in random order and attenuates each probe with an extra coin flip. Version 3 restricts the result to patience at least $2$ ; earlier versions claimed it for all patience values, and Remark 1 shows why patience $1$ fails.
Since then Pollner et al. have obtained $0.395$ for general graphs (reference [35] of the paper).

This mission formalizes the per-edge bound behind the $0.382$ result, Theorem 1 of the paper.

Setting

A finite graph $G = (V, E)$ is given. Each edge $e$ is active independently with probability $p_e \in [0,1]$ , and each vertex $v$ has a patience $t_v \in \{1, 2, \dots\} \cup \{\infty\}$ , the largest number of probes that may be made to edges incident to $v$ . Write $\delta(v)$ for the edges incident to $v$ .

LP (3). A vector $(y_e)_{e \in E}$ is feasible if

0 \le y_e \le 1, \qquad \sum_{e \in \delta(v)} y_e p_e \le 1, \qquad \sum_{e \in \delta(v)} y_e \le t_v \quad (e \in E,\ v \in V).

Here $y_e$ is the probability of probing $e$ .

Attenuation. An attenuation function $\tilde a : [0,1] \to [0,1]$ assigns to edge $e$ the probability $a(e) = \tilde a(p_e y_e)$ . It is effective (Definition 3) if $\tilde a(0) = 1$ and $z \mapsto \ln(1 - x z \tilde a(z))$ is convex on $[0,1]$ for every $x \in (0,1)$ . The two functions used here are $\tilde a_{\exp}(z) = e^{-z/2}$ and $\tilde a_{\mathrm{lin}}(z) = 1 - z/2$ (Definition 4 with $\alpha = 1/2$ ).

Algorithm 1. Draw independent coins $Y_e \sim \mathrm{Bernoulli}(y_e)$ and $A_e \sim \mathrm{Bernoulli}(a(e))$ for every edge, and process the edges in a uniformly random order. When $e$ is processed it is free if both endpoints are unmatched and have made fewer than their patience in probes. If $e$ is free and $Y_e = A_e = 1$ , probe $e$ ; if it is active (coin $P_e \sim \mathrm{Bernoulli}(p_e)$ ), match it and both endpoints. Finally

\beta^* = \int_0^1 \bigl(e^{-2x} + x e^{-2x}\bigr)^2\,dx \approx 0.38278.

Formalization targets

Goal: Theorem 1 (p. 9)

If every vertex has patience at least $2$ , $y$ is feasible for LP (3), and $\tilde a$ is $\tilde a_{\exp}$ or $\tilde a_{\mathrm{lin}}$ , then for every edge $e$

a(e) \cdot \Pr[e \text{ is free}] \;\ge\; \beta^*.

The probability is over the random order and the coins of Algorithm 1.

Milestones

The milestones are numbered results and displays of the paper, in the order its argument uses them:

$\tilde a_{\exp}$ and $\tilde a_{\mathrm{lin}}$ with $\alpha = 1/2$ are effective (Definition 4, p. 9).
(7), p. 10: a safe edge (one whose neighbourhood has neither a successful probe nor an exhausted patience before it arrives) is free, so $a(e)\Pr[e \text{ is free}] \ge \tilde a(p_e y_e)\Pr[e \text{ is safe}]$ .
Lemma 3, p. 11: $\prod_{f \in E_1(r)} (1 - x\,a(f) y_f) \ge e^{-x \sum_{f \in E_1(r)} y_f}$ for an effective attenuation, where $E_1(r)$ is the set of edges at $r$ other than $e$ with $p_f = 1$ .
Lemma 4, p. 12 (Baveja et al.): $\Pr[\sum_i B_i < t] \ge \Pr[\mathrm{Pois}(\mu) < t]$ for independent Bernoullis with mean sum $\mu < t - 1$ .
Lemma 5, p. 12: the Chernoff bound $\Pr[\sum_i B_i < (1+\varepsilon)\mu] \ge 1 - e^{-\varepsilon^2 \mu/(2+\varepsilon)}$ .
Proposition 1, p. 14: $\int_0^1 \lambda\varphi \ge \lambda(z^*)\int_0^1 \varphi$ for $\lambda \ge 0$ non-increasing and $\varphi$ changing sign once, from $+$ to $-$ , at $z^*$ .
(22), p. 15: $\tilde a(y_e)\int_0^1 (e^{-x(2-y_e)} + x e^{-x(2-y_e)})^2\,dx \ge \beta^*$ on $[0,1]$ , with equality at $y_e = 0$ .

Significance

The result. Equation (4) of the paper writes the expected weight of the algorithm's matching as $\sum_e w_e p_e y_e\, a(e)\Pr[e \text{ is free}]$ . Theorem 1 therefore gives at least $\beta^* \sum_e w_e p_e y_e$ , and with an optimal LP solution and the LP upper bound of Bansal et al. this is a $0.382$ -approximation for stochastic matching on general graphs with patience at least $2$ . The bound is per edge, which is the form a random-order contention resolution scheme needs: the same algorithm rounds fractional matchings edge by edge.

Formalizing it. The paper's proof combines a reduction (Lemma 2), the analytic bound of Lemma 3, the tail bounds of Lemmas 4–5, an exchange argument (Lemma 6) resting on a graph construction from another paper, and a case analysis in the patience values that is closed by numerical minimization of explicit integrals over two or three parameters ("we numerically minimize (12)", p. 13; "we numerically verify", p. 15). The margins are thin: the bound $0.3828$ in the last case exceeds $\beta^*$ by about $5 \cdot 10^{-5}$ . No part of this argument has a machine-checked proof. A formal proof would certify both the probabilistic reasoning and every numerical step, and would supply a reusable finite model of random-order probing algorithms with patience, of which the platform has none.

Difficulty

The obvious argument bounds $\Pr[e \text{ is free}]$ by a product over the two endpoints of $e$ and applies a Poisson approximation to the number of probes at each endpoint. For an endpoint of patience $2$ that approximation is only valid for arrival times $x < x_c$ , a threshold that can be $1/2$ , and the bound it gives, about $0.347$ (display (16)), falls below $\beta^*$ . Closing that case is what requires the exchange argument of Lemma 6. Beyond it, the remaining cases are optimization problems over the LP mass at each endpoint, which the paper settles by computer and a formal proof must settle by rigorous bounds.

Formalization scope

The graph is the platform's EdmondsMatching65.Polyhedron.Graph (loopless); the goal adds that the endpoint map is injective, since the paper's edges are pairs $\{u,v\}$ . Patience is ℕ∞, with $\infty$ allowed; "minimum patience $2$ " is $t_v \ge 2$ at every vertex.
Standing assumptions: $p_e \in [0,1]$ for every edge; $y$ feasible for LP (3) (which includes $y_e \in [0,1]$ ).
Every probability is a finite average: over the $|E|!$ orders of the edges and over the $2^{3|E|}$ outcomes of the coins $Y, A, P$ , each weighted by a product of Bernoulli weights. The paper's continuous arrival times induce exactly this uniform order. $\Pr[e \text{ is free}]$ is computed from the run of Algorithm 1 (matched vertices and probe counters, step by step), never from the product formulas of p. 11, which would assume the lemmas being proved.
The goal is stated for $\tilde a_{\exp}$ and $\tilde a_{\mathrm{lin}}$ with $\alpha = 1/2$ . Theorem 1 cites "Definition 3 where $\alpha = 1/2$ "; $\alpha$ belongs to Definition 4, and an arbitrary effective function would make the statement false. The third function of Definition 4 is not effective (its $\ln(1 - xz\tilde a(z))$ is concave near $z = 0$ for $x$ close to $1$ ), so neither the effectiveness milestone nor the goal covers it.
Lemma 4 prints $e^{-x\mu}$ in the Poisson sum; the statement uses $e^{-\mu}$ .
A formalization that defines "free" without the patience counters or the matched set, one that bounds $\Pr[e \text{ is safe}]$ or the integral (8) instead of $a(e)\Pr[e \text{ is free}]$ , or one stated for "some" attenuation function, is a different theorem and does not count.
Not stated: Lemma 2 (a without-loss-of-generality reduction), Lemma 6 (its hypothesis is a graph built in another paper, with property (18) asserted there), the conditional bounds (8)–(17) and (23)–(25), whose objects live inside the proof, and the numerical values of pp. 13–15. Solvers who need them are welcome to state them as their own lemmas. The paper's proofs are in §3.2, pp. 9–15.
Reusable beyond this mission: the finite model of Algorithm 1 and its events, Lemma 4 (Bernoulli versus Poisson lower tails), Lemma 5 (a Chernoff bound for independent Bernoullis), and Proposition 1.

Selected references

B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025; arXiv:2106.06892v3 (20 Apr 2026). https://arxiv.org/abs/2106.06892v3
N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP is the cure for your matching woes: improved bounds for stochastic matchings, Algorithmica 63(4):733–762, 2012 (reference [7] of the paper).
A. Baveja, A. Chavan, A. Nikiforov, A. Srinivasan, P. Xu, Improved bounds in stochastic matching and optimization, Algorithmica 80(11):3225–3252, 2018 (reference [8]; source of Lemma 4).
M. Adamczyk, F. Grandoni, J. Mukherjee, Improved approximation algorithms for stochastic matching, ESA 2015, 1–12 (reference [1]).
N. Chen, N. Immorlica, A. R. Karlin, M. Mahdian, A. Rudra, Approximating matches made in heaven, ICALP 2009, 266–278 (reference [15]).

11 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+2·Captain: mikedeng1

Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes II: With Infinite Patience, Attenuated Random-Order Probing Probes Each Edge w.p. ≥ (1 − e^(−2))y_e/2Research Paper

Motivation

In stochastic matching a platform knows, for every potential pair, the probability that the pair would succeed, but learns whether it does only by trying it, and a successful trial is binding. Kidney exchange, online dating and labour markets are the standard examples: a crossmatch test, a date or an interview is a probe whose outcome is random, and a positive outcome commits both sides. Each participant also tolerates only a limited number of attempts, its patience. The algorithmic question, studied since Chen, Immorlica, Karlin, Mahdian and Rudra (ICALP 2009), is how much of the optimal adaptive strategy's expected weight a simple, non-adaptive rule can secure.

The modern approach solves a linear programming relaxation and rounds its fractional solution online, through a contention resolution scheme: edges are examined one at a time, and an edge is used only when it does not conflict with earlier decisions. Bansal, Gupta, Li, Mestre, Nagarajan and Rudra (Algorithmica 2012) introduced the relaxation (LP (3) below) and showed that it bounds every adaptive probing algorithm. Baveja, Chavan, Nikiforov, Srinivasan and Xu (Algorithmica 2018) analysed processing edges in a uniformly random order. Brubach, Grammel, Ma, MacRury and Srinivasan (Mathematics of Operations Research, 2025; arXiv:2106.06892) add attenuation: an independent coin that sometimes skips an edge on purpose, so that edges likely to block others are probed less often. This mission formalizes their guarantee when patience is unlimited.

Setting

Let $G=(V,E)$ be a finite graph. Each edge $e$ is active independently with known probability $p_e\in[0,1]$ , and each vertex $v$ has a patience $t_v\in\mathbb N\cup\{\infty\}$ , the maximal number of edges at $v$ that may be probed. Write $\delta(v)$ for the edges incident to $v$ . A vector $(y_e)_{e\in E}$ is feasible for LP (3) when

0\le y_e\le 1,\qquad \sum_{e\in\delta(v)}y_ep_e\le 1,\qquad \sum_{e\in\delta(v)}y_e\le t_v\qquad(e\in E,\ v\in V);

$y_e$ is read as the probability of probing $e$ , and $z_e=y_ep_e$ as the probability that $e$ is matched.

An attenuation function is a map $\tilde a:[0,1]\to[0,1]$ , and the attenuation of an edge is $a(e)=\tilde a(p_ey_e)$ . The paper's examples (Definition 4) are $\tilde a_{\exp}(z)=e^{-\alpha z}$ , $\tilde a_{\rm lin}(z)=1-\alpha z$ , and $\tilde a(z)=\frac{1-z}{1-e^{-(1-z)}}(1-1/e)$ . A function is effective (Definition 3) when $\tilde a(0)=1$ and $z\mapsto\ln(1-xz\tilde a(z))$ is convex on $[0,1]$ for every $x\in(0,1)$ .

Algorithm 1 draws independent coins $Y_e\sim\mathrm{Bernoulli}(y_e)$ and $A_e\sim\mathrm{Bernoulli}(a(e))$ and processes the edges in a uniformly random order. When it reaches $e$ , it probes $e$ if $e$ is free (both endpoints unmatched and with remaining patience), $Y_e=1$ and $A_e=1$ . A probe uses one unit of patience at both endpoints and reveals the activeness $P_e\sim\mathrm{Bernoulli}(p_e)$ ; if $P_e=1$ , both endpoints are matched. The edge $e=\{u,v\}$ is safe when, before $e$ is processed, each endpoint $r$ has received at most $t_r-1$ probes and no earlier edge $f\neq e$ at $u$ or $v$ has $A_fP_fY_f=1$ .

Formalization targets

Goal: Corollary 5 (p. 16)

If every patience is $\infty$ , $(y_e)$ is feasible for LP (3), and $\tilde a$ is $\tilde a_{\exp}$ or $\tilde a_{\rm lin}$ with $\alpha=1/2$ , then for every edge $e$

\Pr[\text{Algorithm 1 probes }e]\ \ge\ \Bigl(\int_0^1e^{-2x}\,dx\Bigr)y_e=\tfrac12\bigl(1-e^{-2}\bigr)y_e\approx0.432\,y_e .

Milestones

The exponential and linear functions with $\alpha=1/2$ are effective (p. 9).
Equation (4) (p. 9): the expected matched weight is $\sum_ew_ep_e\Pr[e\text{ free}]\Pr[Y_e=1\cap A_e=1]=\sum_ew_ep_ey_ea(e)\Pr[e\text{ free}]$ .
Equation (7) (p. 10): $a(e)\Pr[e\text{ is free}]\ge\tilde a(p_ey_e)\Pr[e\text{ is safe}]$ .
Lemma 3 (p. 11): $\prod_{f\in E_1(r)}(1-xa(f)y_f)\ge e^{-x\sum_{f\in E_1(r)}y_f}$ for effective $\tilde a$ , where $E_1(r)$ is the set of edges $f\neq e$ at $r$ with $p_f=1$ .
§3.3 (p. 16): $z\mapsto\tilde a(z)\int_0^1e^{-2x(1-z)}dx$ is minimized on $[0,1]$ at $z=0$ .

Companion: Corollary 6 (p. 16)

On a star graph with infinite patience and the third attenuation function, $\Pr[e\text{ is probed}]\ge(1-1/e)\,y_e$ . It comes with the identity of p. 16 behind it: for the third function, $\tilde a(z)\int_0^1e^{-x(1-z)}dx=1-1/e$ for all $z\in[0,1]$ . Both are plain items of the mission, not milestones.

Significance

By (4), Corollary 5 bounds the expected weight of Algorithm 1 by $\frac12(1-e^{-2})\sum_ew_ep_ey_e$ , and with an optimal $y$ and the bound of Bansal et al. this is a $0.432$ -approximation for stochastic matching without patience constraints. Because the bound holds edge by edge and for every feasible $y$ , it also gives a random-order contention resolution scheme for the matching polytope, which is the form reused for other objectives and in online settings. Corollary 6 is the rank-one analogue with the constant $1-1/e$ .

None of this is formalized. Stochastic probing, patience, random-order processing and attenuation have no counterpart in Mathlib or on the platform. The mission produces a finite, executable model of a probing algorithm run on random coins and a random order, in which these probabilities are exact finite sums; that model is reusable for the other results of the paper and for related rounding schemes. The paper's results are proved in §3.2 (pp. 9–15) and §3.3 (p. 16); the milestones are the steps used there.

Difficulty

The obvious argument treats the edges at the two endpoints of $e$ as independent obstacles, each blocking $e$ with probability proportional to its LP value. That fails because being free is not a product event: whether an earlier edge $f$ blocks $e$ depends on whether $f$ was itself free, which depends on the whole run before $f$ . A second difficulty is uniformity. The bound must hold for every feasible $y$ , and the LP mass at an endpoint can be split among arbitrarily many edges of arbitrary sizes; the quantities involved are not monotone in how that mass is split, and the bound must survive the worst split, including the limit of many tiny edges. The choice of attenuation matters here: the third function of Definition 4 violates the convexity condition of Definition 3, which is why Corollary 6 is not covered by the paper's argument. Finally, the paper reasons with continuous arrival times, while the model has only permutations and finitely many coins.

Formalization scope

Model. The graph is the platform's EdmondsMatching65.Polyhedron.Graph (finite, loopless, parallel edges allowed). Probabilities $p$ , LP values $y$ , weights $w$ and attenuations are real; patience is in ℕ∞, with $\top=\infty$ . Every probability is a finite average over the $|E|!$ orders of $E$ and over all outcomes of the coins $Y$ , $A$ , $P$ , with product weights. The paper's independent uniform arrival times induce exactly this uniform order. The run of Algorithm 1 is computed step by step, with matched vertices and probe counters; free, probed and safe are events of that run.
Standing assumptions. $0\le p_e\le1$ for every edge (the meaning of "probability of being active"); LP (3) feasibility, which contains $0\le y_e\le1$ ; attenuations with values in $[0,1]$ on $[0,1]$ .
Disclosed choices. Corollary 5 is stated for $\tilde a_{\exp}$ and $\tilde a_{\rm lin}$ with $\alpha=1/2$ : the corollary says "the effective attenuation functions from Definition 4", its proof names these two, and the third function fails Definition 3 ( $g''(0)<0$ for $x$ near 1). The effectiveness milestone is stated for these two only. The third function is given its limit $1-1/e$ at $z=1$ , where the printed formula is $0/0$ . Corollary 6 is a companion item, not a milestone: the paper's argument for it passes through Lemma 3, which does not apply to the third function, so it is supported by numerical checks but its printed proof has a gap.
Not stated. The approximation-ratio and "balanced contention resolution scheme" sentences of Corollaries 5 and 6 need a model of all adaptive probing algorithms (Lemma 1 of the paper, from Bansal et al.) and are out of scope; the goals are the displayed probability bounds.
Ruled out. Defining $\Pr[e\text{ is free}]$ or $\Pr[e\text{ is probed}]$ by the product formula of p. 11 instead of from the run, or stating the goal for "some" attenuation function, would make the goal a different and easier theorem; neither is done.
Welcome contributions. Proofs of the milestones; a general lemma that an event depending only on the edges before $e$ is independent of $e$ 's coins; a conditioning-on-arrival-time lemma for uniform permutations; a proof (or a counterexample) for Corollary 6.

Selected references

B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025; arXiv:2106.06892v3. https://arxiv.org/abs/2106.06892
N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP Is the Cure for Your Matching Woes: Improved Bounds for Stochastic Matchings, Algorithmica 63(4):733–762, 2012. https://link.springer.com/journal/453/volumes-and-issues/63-4
A. Baveja, A. Chavan, A. Nikiforov, A. Srinivasan, P. Xu, Improved Bounds in Stochastic Matching and Optimization, Algorithmica 80(11):3225–3252, 2018. https://link.springer.com/journal/453/volumes-and-issues/80-11
N. Chen, N. Immorlica, A. R. Karlin, M. Mahdian, A. Rudra, Approximating Matches Made in Heaven, ICALP 2009, LNCS 5555. https://doi.org/10.1007/978-3-642-02927-1

8 thms3 active usersReviewed

All missions

Persuading Risk-Conscious Agents: A Geometric Approach II: In Binary Persuasion with a Convex Non-Adoption Region the Convex Program Reduces to a Linear Program over Ω ∪ K₀₁Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Further results on the same objects

Significance

Difficulty

Formalization scope

Selected references

Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds II: Along Any h, the Empirical Transition Vector Is within 2√(log(n/ρ)Σγᵢcᵢ²/n) + 3D log(2/ρ)/n of the TruthResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5.2 (p. 9)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fixed-Point Quantum Search with an Optimal Number of Queries: The Phases of Eq. (11) Give Success Probability 1 − δ²T_L(T_{1/L}(1/δ)√(1−λ))²Research Paper

Motivation

Setting

Formalization targets

Exact success probability

Consequences

Significance

Difficulty

Formalization scope

Selected references

Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures: The Optimal Maintenance Frontier Has Six Possible StructuresResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (pp. 27–28, Table 1)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Privacy Rights and Data Security: GDPR and Personal Data Markets 1: With Privacy Rights the Monopoly Equilibrium Has Four Breach-Cost Regimes Separated by c = δσ/2, δσ/√2 and δσResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Learning Stabilizer States by Bell Sampling: Algorithm 1 Identifies an n-Qubit Stabilizer State from 5n+2 Copies, Failing with Probability at Most 2⁻ⁿResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1, explicit form

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization I: The Largest-Coordinate Strategy Keeps the Stochastic Chasing 0 Game within 2(c+R)log(4mk²/p)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 34

Milestones

Significance

Difficulty

Formalization scope

Selected references

Privacy Rights and Data Security: GDPR and Personal Data Markets 2: Without Privacy Rights the Monopoly Equilibrium Has Three Breach-Cost Regimes and No Trade Once c ≥ 1 + δμ/(1 + δ)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2

Milestones

Significance

Difficulty

`indexed_heap.algo`

`sort_indices.algo`