Operations Research

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6.5

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

The stochastic block model (SBM), introduced by Holland, Laskey and Leinhardt (1983), is the standard random model for networks with community structure, and the basic benchmark for community-detection algorithms (Abbe 2018). In its two-community form the nodes are split into two equal halves, edges inside a half appear with probability $p$, and edges across with probability $q<p$. The task of exact recovery is to identify the hidden halves from the graph alone.

The maximum a posteriori estimator for this model is the minimum bisection problem (find a balanced cut with the fewest crossing edges), which is NP-hard in general. Abbe, Bandeira and Hall (2016) determined when it recovers the planted bisection, and showed that a semidefinite relaxation is as good as the integer program. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research 2023) ask the same question for the cheapest standard relaxation: the metric linear programming relaxation, defined by triangle inequalities. This mission is their positive result in the very dense regime.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\cup V_2$ with $|V_1|=|V_2|=n/2$. For a graph $G=(V,E)$ let $a_{ij}=1$ if $(i,j)\in E$ and $0$ otherwise. The metric relaxation (LP-P) is

$$\min_{x\in\mathbb R^{\binom n2}}\ \sum_{i<j}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk},\quad x_{ij}+x_{ik}+x_{jk}\le 2,\quad \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first constraint for all distinct $i,j,k$ with $i<j$, the second for all $i<j<k$, and $x_{ji}:=x_{ij}$. The cut vector $\bar x$ of a bisection has $\bar x_{ij}=0$ for $i,j$ on the same side and $\bar x_{ij}=1$ otherwise. (LP-P) recovers the planted bisection when $\bar x$ is its unique optimal solution.

In the Erdős–Rényi model $\mathcal G_{n,p}$ every pair of nodes is an edge independently with probability $p$. In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first chosen uniformly at random; then pairs inside $V_1$ or inside $V_2$ are edges with probability $p$, pairs between them with probability $q$, all independently. $\mathcal G_{n,0,q}$ is the random bipartite graph across a random bisection. An event occurs with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$. The graph is very dense when $p$ and $q$ are constants.

For a finite graph $G=(V,E)$ and $b\in\mathbb Z_{\ge0}^V$, a $b$-factor (or $f$-factor) is a set $F\subseteq E$ with exactly $b_v$ edges of $F$ at each node $v$; $N(U,U')$ counts edges with one endpoint in $U$ and one in $U'$; $d_{\min}$, $d_{\max}$ are the minimum and maximum degrees; and the node connectivity $\kappa(G)$ is the minimum number of nodes whose deletion disconnects $G$ (the number of nodes, for a complete graph).

Formalization targets

Goal: Theorem 6 (p. 15)

For constants $0<q<p<1$,

$$p-q>\tfrac12\ \Longrightarrow\ \mathbb P_{G\sim\mathcal G_{n,p,q}}\big[\text{(LP-P) recovers the planted bisection}\big]\xrightarrow[n\to\infty]{}1 .$$

Milestones

1. Proposition 6 (p. 20): for $G\sim\mathcal G_{2m,0,q}$ there is $C>0$ with $d_{\max}\le qm+C\sqrt{m\log m}$ w.h.p.
2. Proposition 5 (p. 20; Schrijver, Cor. 21.4a): a bipartite graph has a $b$-factor iff $N(U,U)\ge b(U)-\frac12 b(V)$ for every $U\subseteq V$.
3. Proposition 3 (p. 14): there is $C_{\mathrm{reg},2}>0$ such that for every $q\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,0,q}$ is a subgraph of a regular bipartite graph with the same bipartition, of degree $d_{\mathrm{reg}}=\frac{qn}2+C_{\mathrm{reg},2}\sqrt{\frac n2\log\frac n2}$ (rounded down).
4. Proposition 8 (p. 24): for $G\sim\mathcal G_{n,p}$ there is $C>0$ with $d_{\min}\ge pn-C\sqrt{n\log n}$ w.h.p.
5. Proposition 9 (p. 24; Bollobás–Thomason): for $G\sim\mathcal G_{n,p}$, $\kappa(G)=d_{\min}$ w.h.p.
6. Proposition 7 (p. 24; Tutte's $f$-factor theorem).
7. Proposition 4 (p. 14): there is $C_{\mathrm{reg},1}>0$ such that for every $p\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,p}$ contains a spanning regular subgraph of degree $d_{\mathrm{reg}}=pn-C_{\mathrm{reg},1}\sqrt{n\log n}$ (rounded up to an even integer).

The deterministic recovery criterion that the goal also depends on, Theorem 4 of the paper (regular sandwiching with $d_{\mathrm{in}}-d_{\mathrm{out}}\ge n/4$), is the goal of mission 3 of this series and is not restated here.

Significance

The result. Theorem 6 is the only positive recovery guarantee for the metric LP in the random setting of the paper. Together with the failure results of Theorems 7 and 8 (missions 6 and 7), it locates the LP strictly between trivial and information-theoretically optimal: it recovers in a region of constant $p,q$, but not up to the threshold $p>q$ that the minimum bisection problem and its SDP relaxation reach. Propositions 3 and 4, that dense random graphs sit inside, and contain, regular graphs of nearly their average degree, are of independent interest in random graph theory, as the authors note.

Formalizing it. The result is proved in the paper; none of it is machine-checked. The mission also requires three classical theorems that are not in Mathlib: the $b$-factor criterion for bipartite graphs, Tutte's $f$-factor theorem (Mathlib has only the perfect-matching case $f\equiv 1$), and the Bollobás–Thomason theorem $\kappa=d_{\min}$ for random graphs, together with degree concentration for $\mathcal G_{n,p}$ and the bipartite SBM. Each is reusable well beyond this paper.

Difficulty

The obvious argument for recovery is to exhibit a dual certificate for (LP-P), which needs regularity of the communities and of the cross edges; a random graph is not regular. The paper bridges the gap by sandwiching the random graph between regular graphs of nearly equal degree, and that step is where the difficulty lies: the existence of a regular sub- or supergraph is a global combinatorial property, characterized by factor theorems with exponentially many conditions, each of which must hold simultaneously with high probability. Degree concentration alone, the first idea, controls only the singleton conditions. Tutte's $f$-factor theorem and the bipartite $b$-factor criterion are themselves substantial combinatorial theorems, and the connectivity statement of Bollobás and Thomason is a deep result on random graphs.

Formalization scope

Nodes are Fin n (0-based). A bisection is a Finset $V_1$ with $2|V_1|=n$. Points of $\mathbb R^{\binom n2}$ are symmetric arrays with zero diagonal; (LP-P) has no box constraints $0\le x\le1$ (they are implied by the constraints and adding them would change the LP). Recovery means: $\bar x$ is optimal and every optimal solution equals $\bar x$.

The random-graph laws are finite: a probability is a weighted sum over all graphs on Fin n, with independent edge weights, and for the SBM an average over all bisections; the event may depend on the drawn bisection. Edge probabilities are clamped into $[0,1]$, which is the identity on the parameters used here. "With high probability" is Tendsto … atTop (𝓝 1), along $n=2m$ for the SBM. The standing assumption $p>q$ is not built into the law, so that $\mathcal G_{n,0,q}$ is the case $p=0$.

Disclosed readings: the printed $d_{\mathrm{reg}}$ of Propositions 3 and 4 is not an integer; Proposition 3 is posed with degree $\lfloor d_{\mathrm{reg}}\rfloor$ and Proposition 4 with $2\lceil d_{\mathrm{reg}}/2\rceil$, the least even integer $\ge d_{\mathrm{reg}}$ (the proof assumes $d_{\mathrm{reg}}$ even). $\kappa(K_n)=n$ as on p. 24. Quantifier order follows each page: in Propositions 3 and 4 the constant precedes the probability parameter, in Propositions 6 and 8 it follows it; no constant depends on $n$.

A statement in which "with high probability" is replaced by a positive probability or an eventual bound, in which the bisection is fixed rather than random, or in which the regular degree is compared with an irrational real (an empty event) is not this mission's target.

Infrastructure needed: the finite random-graph laws, Hoeffding-type concentration over them, the two factor theorems, and node connectivity. Proofs of any milestone, and of the classical results as general graph theory, are welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62(1), 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18, 2018. https://arxiv.org/abs/1703.10146
• P. W. Holland, K. B. Laskey, S. Leinhardt, Stochastic Blockmodels: First Steps, Social Networks 5(2), 1983. https://doi.org/10.1016/0378-8733(83)90021-7
• W. T. Tutte, The Factors of Graphs, Canadian Journal of Mathematics 4, 1952. https://doi.org/10.4153/CJM-1952-028-2
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003 (Corollary 21.4a).
• B. Bollobás, A. Thomason, Random Graphs of Small Order, in Random Graphs '83, North-Holland Mathematics Studies 118, 1985 (Theorem 1).
• A. Frieze, M. Karoński, Introduction to Random Graphs, Cambridge University Press, 2016 (Chapter 3). https://doi.org/10.1017/CBO9781316339831

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 5

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Large-scale computing systems route incoming tasks to servers through dispatchers, one per task type. A task can only run on a server that holds the data or software it needs, so the set of admissible pairs forms a bipartite compatibility graph between task types and servers. Full flexibility (every server can serve every type) gives the best load balancing but requires each server to store everything. A central question is how sparse the compatibility graph can be while keeping the performance of the fully flexible system.

For the power-of-$d$ policy JSQ($d$) (an arriving task samples $d$ compatible servers and joins the shortest of their queues), Rutten and Mukherjee (arXiv:2008.07562v2, Math. Oper. Res. 2023) identify two deterministic graph conditions, proportional sparsity and subcriticality, under which the occupancy process has the same mean-field limit and the same steady-state limit as in the fully flexible system (their Theorem 3.4). They then show that natural random designs satisfy both conditions almost surely. This mission covers the second random design: task types with inhomogeneous levels of flexibility, where each edge incident to task type $w$ is present independently with its own probability $p_w(N)$ (Theorem 3.6 of the paper).

Earlier work on JSQ-type policies with constrained compatibility includes the stability analyses of Bramson (Ann. Appl. Probab. 2011) and of Cardinaels, Borst and van Leeuwaarden (Queueing Syst. 2019), to which subcriticality is equivalent for a fixed system (Remark 3 of the paper), and the mean-field analysis of the supermarket model on graphs by Budhiraja, Mukherjee and Wu (Ann. Appl. Probab. 2019), whose load condition is stronger than the condition (A.19) used here (Remark 11 of the paper).

Setting

For each $N \ge 1$ there are a set $V_N$ of $N$ servers and a set $W_N$ of $M(N) \ge 1$ dispatchers. A compatibility graph is $G_N = (V_N, W_N, E_N)$ with $E_N \subseteq V_N \times W_N$, and the neighbourhood of $w$ is $N_w = \{v : (v, w) \in E_N\}$.

Proportional sparsity (Definition 3.1). For every $\varepsilon > 0$,

$$\sup_{U \subseteq V_N} \frac{1}{M(N)} \Bigl| \Bigl\{ w \in W_N : \Bigl| \frac{|N_w \cap U|}{|N_w|} - \frac{|U|}{N} \Bigr| \ge \varepsilon \Bigr\} \Bigr| \to 0 .$$

Every set $U$ of servers is seen by all but a vanishing fraction of dispatchers in roughly its global proportion.

Subcriticality (Definition 3.3). For each $N$, $w$ and nonempty $U \subseteq V_N$ there is a probability distribution $\gamma^U_w$ on $U$ such that, with $k_w = \min(d, |N_w|)$,

$$\limsup_{N \to \infty} \max_{v \in V_N} \frac{N}{M(N)} \sum_{w \in W_N} \binom{|N_w|}{k_w}^{-1} \sum_{U \subseteq N_w,\ |U| = k_w} \gamma^U_w(v) \le 1 .$$

Some static routing of sampled sets loads no server asymptotically beyond its capacity.

The random graph. Given edge probabilities $p_w(N) \in (0, 1]$, the graph $G_N$ contains each pair $(v, w)$ independently with probability $p_w(N)$. Write $\bar p(N) = \min_{w} p_w(N)$ and $\|p(N)^{-1}\|_2^{-2} = (\sum_w p_w(N)^{-2})^{-1}$. Only the law of each $G_N$ is prescribed; the graphs for different $N$ may be coupled arbitrarily, and "almost surely" refers to any such coupling.

Formalization targets

Goal: Theorem 3.6 (graph part)

If, as $N \to \infty$,

$$\frac{N}{\ln M(N) + \ln N}\, \bar p(N) \to \infty, \qquad M(N)\, \bar p(N) \to \infty, \qquad \frac{\ln N}{M(N)^2} \sum_{w \in W_N} \frac{1}{p_w(N)^2} \to 0, \qquad (3.5)$$

then almost surely $\{G_N\}$ is proportionally sparse and satisfies the subcriticality condition.

Milestones

1. Lemma B.1. If $\bar p(N) = \omega(1/N)$ and $\bar p(N) = \omega(1/M(N))$, then $\{G_N\}$ is proportionally sparse almost surely.
2. The (A.19) reduction. For any graph sequence and $d \ge 1$,

$$\limsup_{N \to \infty} \max_{v \in V_N} \frac{N}{M(N)} \sum_{w \in W_N} \frac{\mathbb 1\{(v, w) \in E_N\}}{|N_w|} \le 1 \qquad \text{(A.19)}$$

implies subcriticality. 3. Lemma B.2. If $\bar p(N) = \omega((\ln M(N) + \ln N)/N)$ and $\|p(N)^{-1}\|_2^{-2} = \omega(\ln N / M(N)^2)$, then $\{G_N\}$ satisfies the subcriticality condition almost surely.

The goal is the conjunction of Lemmas B.1 and B.2 under (3.5).

Significance

Combined with Theorem 3.4 of the paper, the goal says that JSQ($d$) on a random compatibility graph with dispatcher-dependent flexibility behaves, in the large-system limit and in steady state, like JSQ($d$) on the complete bipartite graph. Condition (3.5) allows the least flexible task type to be compatible with only about $\ln(M(N)N)$ times a diverging factor of servers in expectation, far below $N$, and allows strongly heterogeneous flexibility levels as long as the spread measured by $\sum_w p_w(N)^{-2}$ is controlled. Remark 8 of the paper notes that for $M(N) = N$ and equal probabilities, $p(N) = o(\ln N / N)$ leaves a dispatcher isolated with probability tending to one, so the growth conditions are close to necessary.

The result is proved in the paper (Appendix B). As far as is known, none of it has been machine-checked. A formal proof requires a quantitative Chernoff bound for binomial tails, a bounded-differences (Azuma–Hoeffding) inequality for functions of independent Bernoulli variables, a union bound over all $2^N$ subsets of servers, and the first Borel–Cantelli lemma in a setting where only per-$N$ marginal laws are fixed.

Difficulty

Proportional sparsity quantifies over every subset $U$ of the $N$ servers. A concentration estimate for one fixed $U$, or one fixed dispatcher, is not enough: whatever bound is used must survive a union over $2^N$ subsets, so a merely vanishing failure probability per dispatcher does not suffice.

Subcriticality is a maximum over all servers of a sum whose terms $\mathbb 1\{(v, w) \in E_N\}/|N_w|$ are not independent: $|N_w|$ depends on the edge $(v, w)$ itself, and a term is unbounded in the regime where $|N_w|$ is small. A direct concentration inequality for this sum therefore does not apply, and the logarithmic factors in (3.5) reflect the need to control all $M(N)$ neighbourhood sizes and all $N$ servers at once.

Independence across $N$ is not available, so almost-sure statements cannot use the second Borel–Cantelli lemma or any law of large numbers along $N$; every bound must be summable in $N$.

Formalization scope

• Servers are Fin N, dispatchers Fin (M N) with 0 < M N assumed, and a graph is a Finset (Fin N × Fin (M N)).
• Edge probabilities are reals with $0 < p_w(N) \le 1$ (implicit in the paper). The random graph is a family of measurable maps $X_N : \Omega \to \{0,1\}^{V_N \times W_N}$ on one probability space whose image law is the product of Bernoulli$(p_w(N))$ laws. No assumption links different $N$.
• Every "$\limsup \le 1$" is stated as "for every $\varepsilon > 0$, eventually, for every server, $\le 1 + \varepsilon$"; the supremum over $U$ in (3.1) as "for all $\varepsilon, \delta > 0$, eventually, for every $U$, at most $\delta M(N)$ bad dispatchers". Both are exact equivalents.
• Ratios use real division; $|N_w| = 0$ gives ratio $0$, harmless for a limit condition. At $N = 1$ the logarithms in (3.5) and Lemma B.2 can make a denominator $0$; this affects finitely many $N$.
• Proportional sparsity does not include connectivity: these graphs are disconnected with positive probability for every $N$, so requiring connectivity would make the goal false.
• Subcriticality is Definition 3.3 with two repairs: distributions are required only for nonempty $U$, and the normalisation is $\binom{|N_w|}{\min(d, |N_w|)}$ instead of the printed $\binom{|N_w|}{d}$, which is $0$ when $|N_w| < d$, an event of positive probability here. The two agree when $|N_w| \ge d$.
• $d \ge 2$ as in the model. Under $d = 0$ the subcriticality predicate would be trivially true; the statements exclude it.
• Only the graph part of Theorem 3.6 is posed; "Consequently, the conclusions of Theorem 3.4 hold" belongs to the mean-field mission of this series.

A complete development needs binomial Chernoff bounds, a bounded-differences inequality and Borel–Cantelli for summable bounds; these are reusable for other random-graph statements. Proofs of the deterministic (A.19) reduction and of either lemma are welcome independently.

Selected references

• M. Rutten, D. Mukherjee, Load Balancing Under Strict Compatibility Constraints, arXiv:2008.07562v2, 2020; Math. Oper. Res. 48 (2023). https://arxiv.org/abs/2008.07562
• M. Bramson, Stability of join the shortest queue networks, Ann. Appl. Probab. 21(4):1568–1625, 2011. https://doi.org/10.1214/10-AAP726
• A. Budhiraja, D. Mukherjee, R. Wu, Supermarket model on graphs, Ann. Appl. Probab. 29(3):1740–1777, 2019. https://arxiv.org/abs/1712.07607
• E. Cardinaels, S. C. Borst, J. S. H. van Leeuwaarden, Job assignment in large-scale service systems with affinity relations, Queueing Syst. 93(3–4):227–268, 2019.
• S. Janson, T. Łuczak, A. Ruciński, Random Graphs, Wiley, 2000. https://doi.org/10.1002/9781118032718

Motivation

In large data centres, an incoming task often cannot run on every server: its data, software or licences sit on only some of the machines. Such strict compatibility constraints are modelled by a bipartite graph between task types (dispatchers) and servers. For the fully flexible system, in which every task can go to every server, the JSQ($d$) policy (sample $d$ servers at random and join the shortest queue) is described in the large-system limit by the mean-field ODE of Vvedenskaya, Dobrushin and Karpelevich (1996) and Mitzenmacher (1996). Rutten and Mukherjee (arXiv:2008.07562, Math. Oper. Res. 2023) identify two graph conditions, proportional sparsity and subcriticality, under which JSQ($d$) on a sparse compatibility graph has the same mean-field limit and the same steady state as the fully flexible system (their Theorem 3.4).

The two conditions are useful in system design only if there are natural graph families that satisfy them. A storage designer controls the server degree: the number of task types a server can process is roughly proportional to the data it must store. Theorem 3.5 of the paper answers this design question for random graphs. If every server stores data for $c(N)$ task types chosen uniformly at random, then $c(N)\to\infty$ together with a mild density condition suffices, even when $c(N)$ is negligible compared with the number $M(N)$ of task types. This mission formalizes Theorem 3.5's graph-theoretic content and the chain of lemmas in Appendix A that proves it.

Setting

A system with $N$ servers $V_N=\{1,\dots,N\}$ and $M(N)$ dispatchers $W_N=\{1,\dots,M(N)\}$ has a compatibility graph $G_N=(V_N,W_N,E_N)$ with $E_N\subseteq V_N\times W_N$. The neighbourhood of a dispatcher $w$ is $\mathcal N_w=\{v:(v,w)\in E_N\}$; that of a server $v$ is $\mathcal N_v=\{w:(v,w)\in E_N\}$.

Proportional sparsity (Definition 3.1): for every $\varepsilon>0$,

$$\sup_{U\subseteq V_N}\Big|\Big\{w\in W_N:\Big|\tfrac{|\mathcal N_w\cap U|}{|\mathcal N_w|}-\tfrac{|U|}{N}\Big|\ge\varepsilon\Big\}\Big|\Big/M(N)\to0 .$$

In words, for every set $U$ of servers, all but a vanishing fraction of the dispatchers see $U$ in roughly the proportion $|U|/N$.

Subcriticality (Definition 3.3) with sample size $d\ge2$: there are probability distributions $\gamma^U_w$ on the sets $U\subseteq V_N$ such that

$$\limsup_{N\to\infty}\max_{v\in V_N}\frac{N}{M(N)}\sum_{w\in W_N}\binom{|\mathcal N_w|}{k_w}^{-1}\sum_{U\subseteq\mathcal N_w,\ |U|=k_w}\gamma^U_w(v)\le1,\qquad k_w=\min(d,|\mathcal N_w|).$$

Think of a static policy that routes a task arriving at $w$ to a server in a sampled set $U$ according to $\gamma^U_w$. The condition says that no server receives more than its fair share of load. Its uniform-weight special case is condition (A.19):

$$\limsup_{N\to\infty}\max_{v\in V_N}\frac{N}{M(N)}\sum_{w\in W_N}\frac{\mathbb 1\{(v,w)\in E_N\}}{|\mathcal N_w|}\le1 .$$

The random graph. Let $1\le c(N)\le M(N)$. For each $N$, each server independently chooses its neighbourhood $\mathcal N_v$ uniformly among the $c(N)$-subsets of $W_N$, so every server has degree exactly $c(N)$. All graphs live on one probability space, but only the law of each $G_N$ is prescribed; the joint law across different $N$ is arbitrary.

Formalization targets

Goal: Theorem 3.5 (graph part)

If $c(N)\to\infty$ and $Nc(N)/(M(N)\ln N)\to\infty$, then almost surely

$$\{G_N\}_{N\ge1}\ \text{is proportionally sparse}\quad\text{and}\quad\{G_N\}_{N\ge1}\ \text{satisfies the subcriticality condition.}$$

Milestones, in the order of the proof in Appendix A

1. Lemma A.1. If $X_N\sim\mathrm{Bin}(N,p(N))$ and $p(N)\to0$, then for each $\delta\in(0,1/2)$ there are $N_0\ge1$ and $a>0$ with $\mathbb P(X_N\ge\delta N)\le(a\,p(N)^\delta)^N$ for $N\ge N_0$.
2. Lemma A.2. Let $B_N(X)$ be the set of servers whose number of neighbours in $X$ deviates from $c(N)|X|/M(N)$ by at least $\varepsilon c(N)|X|/M(N)$. If $c(N)\to\infty$ and $Nc(N)/M(N)\to\infty$, then for $0<\varepsilon\le3/2$, $0<\delta<1/2$ and $\eta>0$, almost surely eventually $|B_N(X)|\le\delta N$ for all $X$ with $|X|\ge\eta M(N)$.
3. Lemma A.3. Under the same growth conditions, almost surely eventually at most $\delta M(N)$ dispatchers have $|\mathcal N_w|\le(1-\varepsilon)Nc(N)/M(N)$.
4. Proposition A.4. Under the same growth conditions, $\{G_N\}$ is proportionally sparse almost surely.
5. (A.19) reduction (p. 34). For any graph sequence, (A.19) implies subcriticality.
6. Lemma A.5. If $Nc(N)/(M(N)\ln N)\to\infty$, then $\{G_N\}$ satisfies (A.19) almost surely.

Significance

The result. Theorem 3.5 shows that the performance of the fully flexible JSQ($d$) system, in the mean-field limit and in steady state, can be achieved with a server degree $c(N)$ that grows arbitrarily slowly. The only requirement is that each dispatcher's mean degree $Nc(N)/M(N)$ grow faster than $\ln N$. Each server then needs to store data for only $c(N)$ task types, a vanishing fraction of the $M(N)$ types. The $\ln N$ threshold matches the scale below which some dispatchers have too few neighbours to share the load evenly.

Formalizing it. The result is proved in the paper, and no part of it has been machine-checked. The mission produces reusable statements about random bipartite graphs with fixed left degree: hypergeometric concentration over all large dispatcher sets, the degree lower tail, and a Borel–Cantelli argument without independence across $N$. It also produces a deterministic reduction from subcriticality to (A.19). That reduction is shared with Theorem 3.6 of the same paper (inhomogeneous random graphs). The printed proof of Lemma A.5 has a gap: (A.23) bounds the probability that some dispatcher has low degree by $N^{1-a^2/2}$, but the union over $M(N)$ dispatchers gives $M(N)N^{-a^2/2}$. This is not summable when $M(N)$ grows faster than every polynomial, which the hypotheses allow. A complete formal proof must close this gap or show that low-degree dispatchers contribute too little to matter.

Difficulty

Every statement is almost sure along the whole sequence, but the graphs for different $N$ may be coupled arbitrarily, so no strong law over $N$ is available. Each a.s. claim needs a failure probability that is summable in $N$, followed by the first Borel–Cantelli lemma. Proportional sparsity quantifies over all $2^N$ server sets $U$, and Lemma A.2 over all $2^{M(N)}$ dispatcher sets $X$. The obvious argument would concentrate each $|\mathcal N_w\cap U|$ separately and take a union bound. It fails because $|\mathcal N_w|$ is only of order $Nc(N)/M(N)$, which may be far smaller than $N$ and $M(N)$, so per-dispatcher tails cannot absorb an $e^{N}$ or $e^{M(N)}$ union. Uniform control over all large sets $X$ (Lemma A.2) is therefore the crux. For subcriticality, the difficulty is that the maximum over $v$ runs over $N$ servers while the minimum degree runs over $M(N)$ dispatchers.

Formalization scope

• Servers are Fin N, dispatchers Fin (M N); a graph is a Finset (Fin N × Fin (M N)), and a random graph is a measurable random adjacency matrix Fin N → Fin (M N) → Bool (the space $\{0,1\}^{N\times M(N)}$ of p. 13).
• The law of each random matrix is prescribed pointwise: every matrix with all row sums equal to $c(N)$ has probability $\binom{M(N)}{c(N)}^{-N}$. This is the uniform, independent-over-servers choice. No independence across $N$ is assumed. A formalization that assumes independent graphs for different $N$ proves a weaker theorem.
• Hypotheses $1\le c(N)\le M(N)$ for every $N$, $d\ge2$, and the growth conditions as real limits (Tendsto … atTop atTop). $\ln N$ is Real.log, so the ratio is $0$ at $N=1$, which does not affect a limit.
• Proportional sparsity is the limit condition (3.1) as "for every $\varepsilon,\delta>0$, eventually, for every $U$, at most $\delta M(N)$ bad dispatchers". The connectivity in Definition 3.1 is not included, because the random graphs are disconnected for small $N$. A dispatcher with $|\mathcal N_w|=0$ gives the ratio $0/0=0$ in Lean.
• Subcriticality constrains $\gamma^U_w$ only for nonempty $U$ and normalises by $\binom{|\mathcal N_w|}{\min(d,|\mathcal N_w|)}$. The paper's $\binom{|\mathcal N_w|}{d}$ is $1/0$ when $|\mathcal N_w|<d$, and the empty $U$ admits no distribution. With the literal definition the goal would be false. Both "$\limsup\le1$" conditions are written as "for every $\varepsilon>0$, eventually at most $1+\varepsilon$".
• Not formalized: the sentence "Consequently, the conclusions of Theorem 3.4 hold", which composes this mission's goal with the mean-field mission of this series.
• Infrastructure that is welcome and reusable: hypergeometric and binomial Chernoff bounds in a form usable with Finset.powersetCard, and Borel–Cantelli for eventually-uniform statements over families of finite sets.

Selected references

• D. Rutten and D. Mukherjee, Load Balancing Under Strict Compatibility Constraints, Math. Oper. Res., 2023; arXiv:2008.07562v2. https://arxiv.org/abs/2008.07562
• A. Budhiraja, D. Mukherjee and R. Wu, Supermarket model on graphs, Ann. Appl. Probab. 29(3):1740–1777, 2019. https://doi.org/10.1214/18-AAP1437
• M. Bramson, Stability of join the shortest queue networks, Ann. Appl. Probab. 21(4):1568–1625, 2011. https://doi.org/10.1214/10-AAP726
• S. Janson, T. Łuczak and A. Ruciński, Random Graphs, Wiley, 2000. https://doi.org/10.1002/9781118032718
• N. D. Vvedenskaya, R. L. Dobrushin and F. I. Karpelevich, Queueing system with selection of the shortest of two queues: an asymptotic approach, Probl. Inf. Transm. 32(1):15–27, 1996.
• M. Mitzenmacher, The power of two choices in randomized load balancing, IEEE Trans. Parallel Distrib. Syst. 12(10):1094–1104, 2001. https://doi.org/10.1109/71.963420

Motivation

On reward-based crowdfunding platforms such as Kickstarter, a project creator fixes two numbers before launch: the pledge level $p$, the amount a backer commits, and the campaign duration $T$. Both are set once and cannot be revised. A higher pledge earns more per backer but turns away backers whose valuation falls short, and a longer campaign reaches more backers but makes them wait longer for a project they value less the further away its delivery is. Zhang, Savin and Veeraraghavan (Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022; manuscript SSRN 3065267) model this trade-off with two kinds of backers. Independent backers decide on their own valuation. Herding backers arrive in proportion to the pledges already collected, so early success attracts more pledges. The paper asks when the creator should exploit herding and when it should ignore it.

This mission formalizes the paper's answer in the simplest setting it treats: every independent backer values the project at the same $v_i$, and every herding backer at the same $v_h$.

Setting

A campaign has a population $\hat I>0$ of independent backers, who arrive at rate $k>0$ times the number still to come. Every backer discounts the project's value at rate $r>0$: a backer arriving at time $t$ with valuation $v$ pledges if and only if $v e^{-r(T-t)}\ge p$. Herding backers arrive at time $t$ at rate $\Lambda_h q p$ times the number of pledges so far, where $\Lambda_h\ge0$ is an arrival rate and $q\ge0$ a propensity to pledge, and they pledge under the same discounted-value rule. Valuations lie in $[0,\bar v]$ and enter only through the survival functions $\bar F_i=1-F_i$ and $\bar F_h=1-F_h$ of the two valuation laws.

The paper solves the pledging dynamics in closed form (its Propositions 1 and 2). The numbers of pledging independent and herding backers at time $t$ are

$$n^p_i(t,p,T)=k\hat I\int_0^t e^{-kx}\bar F_i\big(pe^{r(T-x)}\big)\,dx,$$ $$n^p_h(t,p,T)=\Lambda_hqp\,k\hat I\int_0^t e^{\Lambda_hqp\int_\tau^t\bar F_h(pe^{r(T-u)})du}\,\bar F_h\big(pe^{r(T-\tau)}\big)\int_0^\tau e^{-kx}\bar F_i\big(pe^{r(T-x)}\big)dx\,d\tau .$$

The total number of pledges is $n(p,T)=n^p_i(T,p,T)+n^p_h(T,p,T)$, and the creator's problem (18) is

$$\max\ \pi(p,T)=p\,n(p,T)\quad\text{over}\quad 0<p\le\bar v,\ \ 0\le T\le\tfrac1r\ln(\bar v/p).$$

With identical valuations, $\bar F_i(y)=1$ for $y<v_i$ and $0$ for $y\ge v_i$, and likewise $\bar F_h$ with $v_h$, where $0<v_i,v_h\le\bar v$. Proposition 6 adds the constraint $T\le\frac1r\ln(v_i/p)$, under which every independent backer pledges from the start.

Formalization targets

Goal: Proposition 6(ii)

Let $\Lambda_h,q>0$, $v_i>v_h$, and set $\delta=\Lambda_hqv_h/r$, $a=k/(\Lambda_hq)$, $b=\Lambda_hq/r$ and

$$X=e^{bv_h/e}\frac1{4a}\Big(\frac kr v_he^{-2}+0.5\,bv_h^2e^{-3}+2a+v_h\Big)+\frac1a\Big(\frac kr(v_h+a)+a\Big).$$

If $\delta<1$ and $v_i/v_h>(X/(1-\delta))^{r/k}$, then on Proposition 6's feasible set the unique maximizer of $\pi$ is

$$p^*=v_i\Big(\frac r{k+r}\Big)^{r/k},\qquad T^*=\frac1r\ln\frac{v_i}{p^*}.$$

Milestones

1. Corollary 1. If $0<p\le\min(v_ie^{-rT},v_h)$, then for $t\in[0,T]$, $n^p_i(t,p,T)=\hat I(1-e^{-kt})$ and $n^p_h$ equals the explicit formula (15).
2. Proposition 3(b). If $\Lambda_hqv_h/r<1$ and $k/r>2$, then for every sufficiently long fixed duration $T$, the unique optimal pledge level on (18)'s range is $p^*(T)=v_ie^{-rT}$.
3. Proposition 6(i). If $v_i\le v_h$, an optimal campaign exists on Proposition 6's feasible set, and every optimum has $p^*\ge v_i/e$ and $T^*\le 1/r$.

Significance

Proposition 6 separates two regimes. When herding backers value the project at least as much as independent ones, the optimal campaign is short, $T^*\le1/r$, and its pledge is at least $v_i/e$. When herding is weak ($\delta<1$) and independent backers value the project enough more than herding ones, the creator's best response is to price herding backers out entirely and run the campaign that would be optimal if no herding backer existed. The threshold (33) quantifies "enough more". Together with Proposition 3(b), which fixes the duration and finds that the optimal pledge sits exactly at the highest level that keeps every independent backer in from the start, these results give a creator explicit rules rather than a numerical optimization.

The paper states that the proofs of Propositions 3 to 7 are in an online Technical Appendix, which is not part of the manuscript this mission cites; the manuscript's own Appendix proves only Propositions 1 and 2 and Corollaries 1 and 2. None of the results has a machine-checked proof. Formalizing Proposition 6(ii) would supply a verified proof of a result whose published proof is not in the source held here, and would check the threshold (33), whose grouping of terms is read off the typeset page.

Difficulty

The objective $\pi$ is defined through nested integrals of step functions, so it is not differentiable everywhere: the jumps of $\bar F_i$ and $\bar F_h$ put kinks in $\pi$ where $p=v_ie^{-rT}$ and where $p=v_he^{-rT}$ or $p=v_h$, at which a backer type starts or stops pledging during the campaign. Setting a gradient to zero does not identify the optimum. The obvious argument for the goal, that herding backers do not pledge at $p^*>v_h$ and so the no-herding optimum is optimal, compares only campaigns that exclude herding backers; it says nothing about the campaigns with a lower pledge level that do attract them. Those campaigns gain a herding term growing exponentially in $\Lambda_hqp$ times the time during which herding backers pledge, and the comparison must hold uniformly over the whole feasible region, which is what the threshold (33) is for. Uniqueness, not only optimality, must also be shown.

Formalization scope

All objects live in the namespace CrowdfundRM.Identical. Parameters form a structure Campaign with fields Ihat, k, r, Lh (for $\Lambda_h$), q, vbar, Fbi, Fbh. The standing assumptions, implicit in the paper, are $\hat I,k,r,\bar v>0$, $\Lambda_h,q\ge0$, and that each survival function is nonincreasing, takes values in $[0,1]$, equals $1$ below $0$ and $0$ from $\bar v$ on. Identical valuations set $\bar F_i$, $\bar F_h$ to the step functions above with $0<v_i,v_h\le\bar v$.

Conventions: real numbers throughout; the pledge counts are the closed forms (5) and (11); the feasible set of (18) adds $p>0$, which $\ln(\bar v/p)$ requires; "the optimal" is the unique maximizer over the stated feasible set, and Proposition 6(i), which does not claim uniqueness, asserts that a maximizer exists and bounds every maximizer; "sufficiently long" in Proposition 3(b) is an unspecified threshold $T_0>0$; $\Lambda_h,q>0$ is added in Proposition 6(ii) because $a$ and $b$ divide by $\Lambda_hq$. The paper's $T^*=\frac1r\ln(v_i/\bar p)$ has an undefined $\bar p$ and is read as $p^*$. In (33) the factors $e^{bv_h/e}$ and $1/(4a)$ multiply only the first bracket.

The following formalizations would trivialize the targets and are ruled out: defining $n(p,T)$ by the explicit formulas (14)–(15) or by the paper's single formula (17) instead of (5) and (11); stating optimality through sSup or a first-order condition; stating Proposition 6(i) for maximizers without asserting that one exists; and stating Proposition 3(b) with a chosen threshold or with Proposition 6's narrower feasible set. The pledging differential equations themselves and their solution (Propositions 1–2) are formalized in the companion mission on triangular valuations; this mission works from their closed forms.

Infrastructure needed: interval integrals of monotone step functions, the exponential, logarithm and real power from Mathlib. Explicit evaluation of the nested integrals under step laws (Corollary 1) is reusable for any proof in this model. Contributions are welcome on each milestone and on lemmas such as continuity of $\pi$ on the feasible set and the closed form of $\pi$ in each region of $(p,T)$.

Selected references

• J. Zhang, S. Savin, S. Veeraraghavan, Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1147. Cited from the authors' manuscript of May 26, 2021, SSRN 3065267: https://ssrn.com/abstract=3065267