Interoperability and dominant platforms

Digital markets with strong network effects (messaging, social networks, app stores) tend to concentrate: a platform with more users is worth more to each user. Interoperability, the ability of a platform's users to interact with the users of rival platforms, is a central remedy in current competition policy; the EU Digital Markets Act (2022) mandates it for messaging services offered by designated gatekeepers. Whether interoperability actually reduces the market share of a dominant platform is a question about equilibria of a pricing game.

Ekmekci, White and Wu (Management Science, 2025) answer it in a model of platform competition built on net fees. Their Proposition 6 shows, for a Logit duopoly, that lowering interoperability always admits an equilibrium with an even larger dominant platform; equivalently, interoperability may mitigate dominance. This mission formalizes that result and the steps of its proof.

Setting

There are two platforms $j\in\{1,2\}$ and one side of users. Platform $j$ chooses a net fee $t^j\in\mathbb R$: the price a user pays, net of the interaction value the platform extracts once the user has joined. With Logit demand and no outside option, platform $j$'s market share at the fee profile $t=(t^1,t^2)$ is

$$n^j(t)=\frac{e^{-t^j}}{e^{-t^1}+e^{-t^2}} .$$

Both platforms have marginal cost $c$, and each user values each other user of the same platform at $\gamma$, the network externality. The degree of interoperability $\lambda\in[0,1]$ lets a user of platform $j$ also enjoy $\lambda\gamma$ per user of the rival platform (the paper's (19)), and the platform extracts this value too. Platform $j$'s profit is

$$\pi^j(t)=\bigl(t^j+\gamma n^j+\lambda\gamma n^{-j}-c\bigr)\,n^j,\qquad n^{-j}=1-n^j .$$

A fee profile $t$ is a Nash equilibrium in net fees under $\lambda$ if no platform can raise its profit by changing its own fee to any other real number. In an equilibrium with $n^j(t)>1/2$, platform $j$ is the dominant platform.

The Lean development (namespace NetFeePlatform.InteropDominance) writes $n^j(t)$ as demand 0 t j (the 0 is the weight of the absent outside option), $\pi^j$ as profit 0 c γ lam t j, and equilibrium as IsEquilibrium 0 c γ lam t, with t : Fin 2 → ℝ.

Formalization targets

Goal: Proposition 6 (p. 23)

Let $\gamma>0$, $0\le\underline\lambda<\overline\lambda\le1$ and $\gamma(1-\underline\lambda)\le 27/8$. If $t$ is an equilibrium under $\overline\lambda$ and $n^j(t)>1/2$, then there is an equilibrium $t'$ under $\underline\lambda$ with

$$n^j(t')>n^j(t).$$

The equilibrium $t'$ is not unique in general, and the statement does not say which one; it asserts existence, exactly as the paper does.

Milestones

1. Logit derivative (p. 13): $\partial n^j/\partial t^j=-n^j(1-n^j)$.
2. First-order condition (20) (p. 23): every equilibrium satisfies $t^j=c+\frac1{1-n^j}-2\gamma n^j-\gamma\lambda(1-n^j)+\gamma\lambda n^j$.
3. Sufficiency (Appendix E.1.3 with (36)): if $\gamma(1-\lambda)\le 27/8$, a fee satisfying (20) is a best response.
4. Equivalence (p. 24): the market $(c,\gamma,\lambda)$ has the equilibria of the market $(c-\gamma\lambda,\ \gamma(1-\lambda),\ 0)$.
5. Characterization (p. 51): equilibrium shares are the zeros of $\zeta(n;\lambda)=\ln\frac{n}{1-n}+\frac1{1-n}-\frac1n-2\gamma(1-\lambda)(2n-1)$, and conversely under the bound of item 3.
6. Comparison (p. 52): $\zeta(n;\underline\lambda)-\zeta(n;\overline\lambda)=2\gamma(\underline\lambda-\overline\lambda)(2n-1)<0$ for $n>1/2$.
7. Boundary behaviour (p. 52): $\zeta(n;\lambda)\to\infty$ as $n\to1^-$.

Significance

The result. Proposition 6 is the paper's argument that interoperability mandates can reduce concentration without any change in the platforms' cost or quality: at a fixed network externality, every equilibrium with a dominant platform under a higher degree of interoperability is outsized by an equilibrium under a lower degree, so the largest dominant share an equilibrium can sustain does not increase as interoperability rises. The proof rests on the equivalence of item 4, under which interoperability acts as a reduction of the effective network externality from $\gamma$ to $\gamma(1-\lambda)$; Figure 2 of the paper plots the resulting largest equilibrium share as $\lambda$ varies at $\gamma=3.375$.

Formalizing it. The paper's proof is three paragraphs, and it identifies equilibria with zeros of $\zeta$. A formal proof has to supply what the text takes for granted: that the first-order condition is necessary at a global Nash equilibrium, that it is sufficient in the stated range, and that a zero of $\zeta$ can be turned back into a fee profile. No part of the result has been machine-checked before. A complete development also gives a reusable treatment of Logit demand and of best responses in one-variable concave games.

Difficulty

The algebra of $\zeta$ and the intermediate value step are short. The work lies in the equilibrium notion. A Nash equilibrium is a global condition over every unilateral deviation $s\in\mathbb R$, and profit is not concave in the platform's own fee. Measured against the platform's own share $n\in(0,1)$, profit has second derivative $-1/(n(1-n)^2)+2\gamma(1-\lambda)$; it is concave exactly when $2\gamma(1-\lambda)$ does not exceed the minimum $27/4$ of $1/(n(1-n)^2)$. Outside that range the first-order condition is not sufficient, and a zero of $\zeta$ need not be an equilibrium; the paper does not treat that case.

Formalization scope

• Model. One side ($S=1$), two platforms indexed by Fin 2, Logit demand with no outside option (outside weight $w=0$, literally), common $c$ and $\gamma$, interoperability $\lambda$ written lam. The Setting file states the general $J$-platform objects (demand with an outside-option weight $w\ge0$, profit with the interoperability term $\lambda\gamma\sum_{k\ne j}n^k$, equilibrium, the diversion ratio of (32)); this mission uses them at $J=2$, $w=0$.
• Hypotheses. The paper assumes $\gamma>0$ and $\lambda\in[0,1]$. The goal adds $\gamma(1-\underline\lambda)\le 27/8$, the range in which the paper proves that the first-order condition is sufficient (Appendix E.1.3 with (36), the $3.375$ of Proposition 2′); the paper's own proof stops at the first-order condition and is not complete without it.
• Correction. The paper prints $\zeta(\overline n^1;\underline\lambda)-\zeta(\overline n^1;\overline\lambda)=4(\underline\lambda-\overline\lambda)\gamma\overline n^1$; the correct value is $2\gamma(\underline\lambda-\overline\lambda)(2\overline n^1-1)$. Its sign is the same, and milestone 6 states the correct value.
• Ruled out. Equilibrium is never replaced by "the pricing formula (20) holds": that would reduce the goal to an intermediate value argument and remove its substance. Shares are always demand 0 t j at a fee profile, never free variables. Profit keeps the interoperability term; without it $\lambda$ would not enter the model at all.
• Out of scope. General (non-Logit) demand and Assumptions A1–A2, $S\ge2$ sides, $J\ge3$ platforms (Proposition 12), platform-specific $c^j,\gamma^j$, the microfoundation of Appendix A, and the numerical Figure 2.
• Welcome contributions. Proofs of the milestones, in particular the Logit change of variable from fees to shares and the concavity bound, which are reusable in the two companion missions of this series.

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 (the version cited here). https://doi.org/10.1287/mnsc.2023.02810
• J. Crémer, P. Rey, J. Tirole, Connectivity in the Commercial Internet, Journal of Industrial Economics 48(4), 2000. https://doi.org/10.1111/1467-6451.00129
• Regulation (EU) 2022/1925 (Digital Markets Act), Official Journal of the European Union L 265, 2022. https://eur-lex.europa.eu/eli/reg/2022/1925/oj

Motivation

Markets organized by platforms (social networks, marketplaces, messaging services) exhibit network effects: a user values a platform more when more users join it. A standing concern in competition policy is that such markets "tip" towards one dominant platform, and the usual remedy proposed is to foster entry. Ekmekci, White and Wu (Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025) develop a tractable model of platform oligopoly in which platforms compete in net fees, the price a user pays net of the interaction value the platform delivers, and use it to examine policy interventions. Their Proposition 4 shows that the intuition "more platforms, less dominance" can fail: with strong network effects, adding a third platform to a duopoly can produce an equilibrium whose leader is larger than any platform of any duopoly equilibrium.

The net-fee approach is the authors' alternative to the "insulated equilibrium" of White and Weyl (2016); the paper's §5 specializes it to Logit demand, where pricing formulas are explicit.

Setting

There are $J$ platforms and one side of users. Platform $j$ charges a net fee $t^j\in\mathbb R$; write $t=(t^1,\dots,t^J)$. Demand has the Logit form (13): with outside-option weight $w=e^{z}\ge0$,

$$n^j(t)=\frac{e^{-t^j}}{w+\sum_k e^{-t^k}},$$

and in this mission there is no outside option, $w=0$, so the shares sum to one. Platforms are ex ante identical: common marginal cost $c$ and common interaction value $\gamma$. Platform $j$'s profit ((8) with one side) is

$$\pi^j(t)=\big(t^j+\gamma\,n^j(t)-c\big)\,n^j(t),$$

the net fee plus the interaction value the platform extracts per user, less cost, times its share. A net-fee equilibrium is a pure-strategy Nash equilibrium: no platform $j$ can raise $\pi^j$ by changing its own net fee to any $s\in\mathbb R$. Duopoly is $J=2$, triopoly $J=3$.

At an equilibrium, each net fee satisfies the Logit pricing formula (14), $t^j=c+\frac{1}{1-n^j}-2\gamma n^j$. For equilibria with one dominant platform of share $1-n$ and $J-1$ equal small platforms of share $n/(J-1)$, the paper reduces the equilibrium conditions to a zero of the characterization function

$$g(n;J)=\ln n-\ln(J-1)-\ln(1-n)+\frac{1}{1-\frac{n}{J-1}}-2\gamma\frac{n}{J-1}-\Big(\frac1n-2\gamma(1-n)\Big),\qquad 0<n<1.$$

Formalization targets

Goal: Proposition 4 (competition may increase dominance)

For $2\ln2+\tfrac43<\gamma\le\tfrac{27}{8}$: duopoly has an equilibrium, and there exist a triopoly equilibrium $t_3$ and a platform $i$ with

$$n^k(t_2)<n^i(t_3)\quad\text{for every duopoly equilibrium }t_2\text{ and every platform }k.$$

The comparison is against every duopoly equilibrium and every platform in it, not against one selected equilibrium.

Milestones

1. The Logit derivative $\partial n^j/\partial t^j=-n^j(1-n^j)$ (p. 13).
2. Proposition 1 in Logit form (14): every equilibrium satisfies $t^j=c+\frac1{1-n^j}-2\gamma n^j$ (pp. 12–13).
3. The Logit concavity bound (36): for $\gamma\le27/8$, the pricing formula gives a global best response (p. 43).
4. The zeros of $g(\cdot;J)$ are exactly the equilibria with one dominant and $J-1$ equal small platforms (p. 49).
5. $\lim_{n\to0^+}g(n;J)=-\infty$ (p. 49).
6. $g(n;3)-g(n;2)=-\ln2+\frac1{1-n/2}-\frac1{1-n}+\gamma n$ (p. 50).
7. For $2\ln2+\tfrac43<\gamma\le\tfrac{27}{8}$, $g(n;3)>0$ at every zero $n\in(0,\tfrac12]$ of $g(\cdot;2)$ (p. 50).

Significance

The result. Proposition 4 is a counterexample to a policy presumption: entry need not reduce concentration in markets with network effects. With a third platform, the two small platforms can split the fringe so thinly that the leader's share rises above anything sustainable in a duopoly. The result identifies an explicit parameter window; together with the companion results on interoperability (Propositions 6 and 7 of the same paper), it frames which interventions reduce dominance in this model.

Formalizing it. The proposition is proved in the paper partly by a numerical check ("we can verify", p. 50), and its printed interval $(2.71,3.375]$ is slightly too wide at the bottom: at the symmetric duopoly equilibrium the paper's own criterion requires $\gamma>2\ln2+\tfrac43\approx2.7196$. A machine-checked proof would settle the corrected statement, replace the numerical step by an argument, and make the equilibrium characterization through $g(n;J)$ (including the step from first-order conditions to global Nash equilibrium) available for the other results of the series. None of these statements is formalized anywhere to our knowledge.

Difficulty

Three steps resist the obvious argument.

• First-order conditions are not equilibria. The pricing formula is necessary; that it is sufficient requires profit to be concave in the platform's own share, which holds only for $2\gamma\le 1/(n(1-n)^2)$, i.e. for $\gamma\le 27/8$. Without this, zeros of $g$ need not be equilibria.
• "Any duopoly equilibrium" is universal. Duopoly may have asymmetric equilibria for $\gamma$ near the top of the range, so the triopoly leader must beat the smallest zero of $g(\cdot;2)$ in $(0,\tfrac12]$, not only the symmetric one.
• The positivity of $g(n;3)$ at duopoly zeros is an inequality between transcendental functions of $n$ on a $\gamma$-dependent set; the paper checks it numerically. Its margin vanishes as $\gamma$ approaches $2\ln2+\tfrac43$ at $n=\tfrac12$, and the paper's rewriting $\gamma=f(n,J)$ is $0/0$ exactly there.

Formalization scope

• Lean namespace NetFeePlatform.Competition. The definitions file Setting declares the Logit demand demand w t j, the profit profit w c γ lam t j (with an interoperability term $\lambda\gamma\sum_{k\ne j}n^k$, set to $\lambda=0$ throughout this mission), the global Nash predicate IsEquilibrium, and the diversion ratio; GChar declares $g(n;J)$. Platforms are indexed by Fin J.
• Committed conventions: one side ($S=1$), Logit demand, common $c$ and $\gamma$, no outside option ($w=0$, literally, not a limit $z\to-\infty$), real-valued net fees with deviations over all of $\mathbb R$.
• The goal's lower bound is $2\ln2+\tfrac43$ instead of the printed $2.71$ (see Difficulty and the goal's Formalization Note); the upper bound $27/8=3.375$ is exact. The goal adds the conjunct "duopoly has an equilibrium", the existence claim of Proposition 2′ in this case, so that "any duopoly equilibrium" is not vacuous.
• Trivializing formalizations are ruled out: equilibrium is the global Nash condition, never the first-order condition; the comparison quantifies over all duopoly equilibria; the dominant platform's index is existential, not fixed.
• Out of scope: general (non-Logit) demand and Assumptions A1–A2, $S\ge2$ sides, platform-specific $\gamma^j$ and $c^j$, the microfoundation of Appendix A, Propositions 2, 2′, 3, 5 and 13.
• Infrastructure: one-variable calculus (derivatives, concavity, the intermediate value theorem, limits) from Mathlib. The Logit derivative and the concavity-based best-response lemma (milestones 1–3) are reusable for any Logit oligopoly with network effects. Contributions of alternative proofs of milestone 7 (interval arithmetic or monotonicity arguments) 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
• A. White, E. G. Weyl, Insulated Platform Competition, SSRN working paper, 2016. https://ssrn.com/abstract=1694317

Motivation

Video-game consoles, streaming services and messaging apps share two features: users value a platform more when more people use it (network effects), and some users buy access to more than one platform (multihoming). In the standard Hotelling model where every consumer buys exactly one good, network effects intensify competition: a stronger network effect makes demand more price-sensitive, and the equilibrium price $t-\mu$ and profit $(t-\mu)/2$ fall in $\mu$ (the paper's single-homing benchmark, §3.1). Foros, Kind and Stähler (SNF Working Paper 16/21, NHH Bergen, 2021; published in Management Science, 2025, doi:10.1287/mnsc.2022.00613) show that this intuition reverses when consumers can multihome: firms then price the incremental value of their good (Kim and Serfes, 2006; Anderson, Foros and Kind, 2017), and the network benefit of the rival's users feeds back into that incremental value.

This mission formalizes the paper's Proposition 3, which describes how the symmetric multihoming equilibrium price and profit respond to the strength of network effects over the whole admissible range. It is the third of three missions on the paper; the first treats weak network effects with asymmetric firms (Proposition 1) and the second the comparison with the no-network-effect benchmark (Proposition 2).

Setting

Two firms $i\in\{0,1\}$ sit at the ends of a Hotelling line of unit length, populated by a unit mass of consumers, uniformly distributed. A consumer at distance $d$ from firm $i$ pays a mismatch cost $t\,d$ with $t>0$. Each good carries $e$ exclusive features (the same number for both firms in this mission) plus features common to both goods, which cancel from every object below. Buying good $i$ gives a network benefit $\mu z_i$, where $\mu\ge0$ is the network-effect strength and $z_i$ the expected number of users of good $i$; the paper assumes $\mu<t$ (Assumption 1(i)).

A consumer buys a second good when its incremental value exceeds its price. Under fulfilled expectations ($z_i=x_i$), the multihoming demand for good $i$ at prices $(p_i,p_j)$ is (14)

$$x_i^M(p_i,p_j)=\frac{\mu}{t+\mu}+t\,\frac{e-p_i}{t^2-\mu^2}-\mu\,\frac{e-p_j}{t^2-\mu^2}.$$

Maximizing $p_i\,x_i^M$ gives the reaction function (15), $p_i^M(p_j)=\frac{t\mu-\mu^2+te}{2t}+\mu\frac{p_j-e}{2t}$, whose symmetric fixed point yields the price and profit (26)

$$p^M(\mu)=\frac{(t-\mu)(\mu+e)}{2t-\mu},\qquad \pi^M(\mu)=\frac{t\,(t-\mu)\,(e+\mu)^2}{(t+\mu)\,(2t-\mu)^2}.$$

In the Lean development these are demandM t μ e pi pj, reactM t μ e pj, pM t μ e and piM t μ e in the namespace Multihoming.Hump. Partial multihoming means that some consumers buy one good and some buy both.

Formalization targets

Goal: Proposition 3

Assume partial multihoming. Then $p^M$ and $\pi^M$ are hump-shaped in $\mu$ on $[0,t]$: there are peaks $\hat\mu_p,\hat\mu_\pi\in(0,t)$ with

$$p^M \nearrow \text{ strictly on } [0,\hat\mu_p],\quad p^M\searrow \text{ strictly on } [\hat\mu_p,t],\qquad \pi^M \nearrow \text{ strictly on } [0,\hat\mu_\pi],\quad \pi^M\searrow \text{ strictly on } [\hat\mu_\pi,t].$$

The goal leaves the peaks unnamed; that is the paper's statement.

Milestones

1. (15) maximizes $p\,x_i^M(p,p_j)$ over all prices; $p^M$ is a fixed point of (15), the demand at $(p^M,p^M)$ is (25), and $\pi^M=p^M x^M$.
2. The factorization $\frac{d\pi^M}{d\mu}=\frac{2t(e+\mu)(e+t)}{(t+\mu)^2(2t-\mu)^3}(r_1-\mu)(r_2+\mu)$ with explicit roots $r_1,r_2$; their positivity; the identity for $r_1-t$ and the positivity of its numerator; the signs of $d\pi^M/d\mu$ at $\mu=0$ and $\mu=t$.
3. The profit hump with the peak identified as $r_1$, and $\pi^M(0)>\pi^M(t)$.
4. The factorization $\frac{dp^M}{d\mu}=\frac{(2t+\sqrt{t(2t+e)}-\mu)(2t-\sqrt{t(2t+e)}-\mu)}{(2t-\mu)^2}$ and its signs at $\mu=0$ and $\mu=t$.

Significance

The result. Proposition 3 says that firms benefit from weak network effects and are harmed by strong ones. As $\mu\to t$ the goods become as if undifferentiated, competition for consumers becomes Bertrand-like, and $p^M\to0$; combined with $\pi^M(0)>\pi^M(t)$ this means firms would prefer a market without network effects once these are strong enough. This non-monotone response is the paper's main qualitative message on pricing under multihoming, and the comparison of Proposition 2 (where the profit curve crosses its $\mu=0$ level) depends on the same shape.

Formalizing it. The result is proved in the paper by sign analysis of explicit derivatives; it has no machine-checked proof. A formal proof certifies the two derivative factorizations, the location of each peak strictly inside $(0,t)$, and the passage from derivative signs to strict monotonicity on closed intervals that the appendix states in one sentence. It also makes explicit the parameter range on which the statement holds, which the printed proposition leaves to the phrase "partial multihoming".

Difficulty

The derivatives of $p^M$ and $\pi^M$ are rational functions whose numerators are quadratics in $\mu$ with square-root roots; showing that exactly one root lies in $(0,t)$ requires inequalities between square roots and polynomials in $t,e$ that hold only under $0\le e<2t$. The appendix asserts "it is straightforward" and "it can be shown" at these steps. A second obstacle is the passage from "the derivative vanishes at one point, is positive at $0$ and negative at $t$" to strict monotonicity on each closed piece: this needs the sign of the derivative on the whole open subinterval, not only at the endpoints. Showing only that a maximizer exists on $[0,t]$ is trivial for any continuous function and is not the claim.

Formalization scope

• All parameters are real numbers. Standing assumptions: $t>0$; $\mu\ge0$; for the demand and reaction function $\mu<t$ (Assumption 1(i)). Assumption 1(ii)–(iii) (market coverage, positive market shares) are not needed by any statement and are not added.
• "Assume partial multihoming" is pinned as $0\le e<2t$, the condition the paper's proof uses ("$2t-e>0$, which is a necessary condition for partial multihoming"). For $e\in(t,2t)$ the partial-multihoming range $e\le(2t^2-\mu^2)/t$ fails for $\mu$ near $t$; like the proof, the statement concerns the closed forms (26) on all of $\mu\in[0,t]$, closed at $t$ as the proof evaluates there. Since both functions are continuous at $t$, the statement on $[0,t)$ is equivalent.
• The profit $\pi^M$ is the printed closed form (26), because the demand (14) divides by $t^2-\mu^2=0$ at $\mu=t$; a milestone proves $\pi^M=p^M x^M$ on $[0,t)$.
• The two signs at $\mu=0$ involving $\pi^M$ need $e>0$ (at $e=0$ both $d\pi^M/d\mu|_0$ and $\pi^M(0)-\pi^M(t)$ vanish); those milestones carry $e>0$, the goal does not.
• "Hump-shaped" is strict increase on $[0,\hat\mu]$ and strict decrease on $[\hat\mu,t]$ with $\hat\mu$ in the open interval $(0,t)$. A peak at an endpoint, or the mere existence of a maximizer, would trivialize the claim and is ruled out by the statement.
• Derivatives are two-sided HasDerivAt; all functions are smooth near $[0,t]$ under the hypotheses, and every denominator ($t+\mu$, $2t-\mu$, $t^2-\mu^2$, $e+t$) is positive where it is used, so no statement relies on Lean's convention $x/0=0$ or $\sqrt{x}=0$ for $x<0$.
• The derivation of (14) from consumer utilities and the full pricing game (regimes, deviations, equilibrium selection) are not formalized. Proposition 4 of the paper, the equilibrium characterization, is not posed because it is false as printed: a profitable deviation to the single-homing demand branch exists inside the stated range.
• Only Mathlib calculus (HasDerivAt, strictMonoOn_of_deriv_pos) and real-closed-field arithmetic are needed. Contributions of any milestone, alternative proofs of the hump via the derivative factorizations, and proofs that identify the price peak $2t-\sqrt{t(2t+e)}$ explicitly are welcome.

Selected references

• Ø. Foros, H. J. Kind, F. Stähler, Endogenous Multihoming and Network Effects: PlayStation, Xbox, or Both?, SNF Working Paper No. 16/21, NHH Bergen, 2021; Management Science, 2025. https://doi.org/10.1287/mnsc.2022.00613
• H. Kim, K. Serfes, A Location Model with Preference for Variety, Journal of Industrial Economics 54(4), 569–595, 2006. https://doi.org/10.1111/j.1467-6451.2006.00300.x
• S. P. Anderson, Ø. Foros, H. J. Kind, Product Functionality, Competition, and Multipurchasing, International Economic Review 58(1), 183–210, 2017. https://doi.org/10.1111/iere.12213

Motivation

Admissions offices and employers that run affirmative action usually measure representation one identity dimension at a time: the share of women among those admitted, the share of Black applicants, and so on. Applicants, however, belong to intersectional groups (Black women, white men, …), and a policy that looks balanced along every dimension can still leave some intersectional group under-represented. The sociological literature calls this hidden inequality. Carvalho, Pradelski and Williams (hal-04788142v1; published in Management Science 71(5), 2025, doi:10.1287/mnsc.2023.03839) put the question into a threshold-admission model with score adjustments. Their Theorem 1 shows that, for generic score distributions, no nonintersectional policy (one that adjusts each dimension separately and composes the adjustments) makes every intersectional group's share among the accepted equal to its population share.

This mission formalizes the paper's positive counterpart, Proposition 3: for the weaker, per-dimension target that committees actually monitor, nonintersectional policies do succeed on a nonempty open set of distributions. Together the two results explain why reductive monitoring can report success while intersectional groups remain under-represented (the paper's Example 3).

Setting

A decision maker accepts a share $\alpha \in (0,1)$ of a unit-mass applicant pool. An applicant has a score $x$ in an interval $X \subset \mathbb{R}$ and an identity $g \in G = \{0,1\}^n$ with $n \ge 2$. Everyone with $g_i = 1$ belongs to category $i$. The joint law $p$ of (score, identity) lies in the space $P$ of probability measures on $X \times G$ whose conditional score laws $F_g = p(\cdot \mid g)$ are continuous and have full support on $X$. $P$ carries the relative weak topology. Write $p(g)$ for the mass of group $g$ and $p(g_i)$ for the mass of category $i$.

A policy assigns to each group a score adjustment $q_g : X \to X$ taken from a family $Q$ of strictly increasing bijections that is rich (for all $x, y \in X$ some $q \in Q$ has $q(x) = y$) and commutative ($q \circ q' = q' \circ q$). The additive shifts $x \mapsto x + \delta$ on $X = \mathbb{R}$ are the leading example. Given a threshold $x^* \in X$, an applicant from group $g$ is accepted when $q_g(x) \ge x^*$, subject to the capacity constraint

$$\sum_{g \in G} \Pr(q_g(x) \ge x^* \mid g)\, p(g) = \alpha .$$

The accepted share of group $g$ is $\hat p(g)$, and the accepted share of category $i$ is $\hat p(g_i) = \sum_{g : g_i = 1} \hat p(g)$.

• A policy is nonintersectional if $g = g' + g''$ (as integer vectors) implies $q_g = q_{g'} \circ q_{g''}$.
• An outcome is reductive representative if $\hat p(g_i) = p(g_i)$ for every dimension $i$ (Definition 7).

The milestones use the paper's parameterization (Appendix D). Fix $x_0 \in X$, let $r(\cdot \mid \theta)$ be the map in $Q$ sending $x_0$ to $\theta$, and for $\theta \in X^n$ let $r_g(\cdot \mid \theta)$ compose $r(\cdot \mid \theta_i)$ over the coordinates with $g_i = 1$. Let $R_i(\theta, x^*)$ be the resulting acceptance rate of category $i$ and $S(\theta, x^*)$ the total acceptance rate, and let $t(\theta)$ solve $S(\theta, t(\theta)) = \alpha$. For $a, b \in X^n$, condition (5) reads

$$R_i(a_i, \theta_{-i}, t(a_i, \theta_{-i})) < \alpha < R_i(b_i, \theta_{-i}, t(b_i, \theta_{-i})) \quad \text{for all } i,\ \theta_{-i} \in \textstyle\times_{j \ne i}[a_j, b_j].$$

Formalization targets

Goal: Proposition 3

$$\exists\, U \subseteq P \text{ open},\ U \ne \emptyset,\ \forall p \in U\ \exists\, q \text{ nonintersectional},\ q_g \in Q,\ \exists\, x^* \in X:\ \textstyle\sum_g A_g = \alpha \text{ and } \hat p(g_i) = p(g_i)\ \forall i,$$

with $A_g$ the accepted mass of group $g$. The policy may be any nonintersectional policy in $Q$. The set $U$ is not specified.

Milestones (in the order of Appendix D)

1. Lemma 1(b): the map in $Q$ sending $x$ to $y$ is unique.
2. Continuity of the parameterization: $\theta \mapsto r(x \mid \theta)$ is continuous.
3. The capacity threshold: for $p \in P$, $S(\theta, \cdot) = \alpha$ has exactly one solution $t(\theta)$.
4. The Poincaré–Miranda step: (5) with $a \le b$ yields $\theta^* \in [a, b]$ with $R_i(\theta^*, t(\theta^*)) = \alpha$ for all $i$, and the policy $r_g(\cdot \mid \theta^*)$ with threshold $t(\theta^*)$ is nonintersectional and reductive representative.
5. Lemma 3: (5) at $\bar p$ persists on a neighbourhood of $\bar p$ in $P$.
6. Lemma 4: some $\bar p \in P$ satisfies (5) with $a \le b$.

Significance

The result. Proposition 3 shows that the obstruction in Theorem 1 belongs to the intersectional target, not to nonintersectional policies as such. A committee that monitors only per-dimension shares can meet its target with a nonintersectional policy on an open set of distributions, and the paper's Example 3 shows that such a policy can at the same time lower the acceptance rate of an intersectional group (Black men) that receives affirmative action. Taken together, the two results make the case for monitoring representation at the intersectional level.

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs pieces that do not yet exist in Lean. One is the algebraic structure of rich commutative families (Lemma 1: such a $Q$ is an abelian group acting simply transitively on $X$). Another is weak-topology continuity of acceptance masses on $P$. A third is a continuity-of-argmax argument (Berge's maximum theorem) for $t(\theta, p)$ and for minima over boxes, and the last is the Poincaré–Miranda theorem. Mathlib has neither Poincaré–Miranda nor Brouwer's fixed-point theorem.

Difficulty

A first attempt is to solve $R_i(\theta, t(\theta)) = \alpha$ one coordinate at a time with the intermediate value theorem. This fails because the coordinates interact through the common threshold: raising $\theta_j$ admits more of category $j$, pushes $t(\theta)$ up, and lowers every other $R_i$. A genuinely $n$-dimensional fixed-point argument is needed, here Poincaré–Miranda on the box $[a, b]$, which in turn needs $R_i(\theta, t(\theta))$ to be continuous in $\theta$.

The open-set claim needs more than one good distribution: condition (5) must survive weak perturbations of $p$. That requires continuity of acceptance masses in $p$, which holds only because conditional laws in $P$ are atomless (so threshold boundaries carry no mass), and continuity of the implicitly defined threshold $t(\theta, p)$ jointly in $\theta$ and $p$. Exhibiting the distribution of Lemma 4 is the easy part.

Formalization scope

Scores live in the subtype of an order-connected $X \subseteq \mathbb{R}$ with at least two points. Identities are Fin n → Bool with 0-based indices, and $g = g' + g''$ is coordinatewise addition in $\mathbb{N}$. $P$ is a subtype of ProbabilityMeasure on $X \times G$ (product topology, Borel σ-algebra), with Mathlib's weak topology. Membership in $P$ asks, for every group with $p(g) > 0$, that the conditional law have no atoms and charge every nonempty open subinterval. Groups with $p(g) = 0$ are unconstrained (convention C1; the paper is silent, and Lemma 4's $\bar p$ has null groups). "Increasing" is read as strictly increasing, which is the same thing for bijections. Accepted masses are measures of sets, and $R_i$ divides by $p(g_i)$ (Lean returns $0$ when $p(g_i) = 0$). The objects $r(\cdot \mid \theta)$ and $t(\theta)$ are chosen elements, unique for rich commutative $Q$ and $p \in P$ respectively.

Disclosed additions to the page:

• $X$ has at least two points in the goal and in Lemma 4, since on a one-point $X$ the space $P$ is empty.
• $a \le b$ is a hypothesis of the Poincaré–Miranda step and part of the conclusion of Lemma 4, because with an empty box condition (5) holds vacuously.

Ruled out:

• trivial readings: an empty $P$ or an unsatisfiable $Q$ (the additive family satisfies the hypotheses), and a single distribution in place of an open set;
• a weaker notion of representation: dropping the capacity constraint, which would turn representation into equal acceptance rates at an arbitrary level;
• the wrong ambient space: openness taken in all of $\Delta(X \times G)$ rather than in $P$;
• unrestricted policies: policies are required to lie in $Q$ group by group.

Contributions welcome: the group structure of rich commutative families (shared with the companion mission on Theorem 1), weak continuity of threshold acceptance masses, a Poincaré–Miranda theorem for boxes in $\mathbb{R}^n$, which is reusable well beyond this paper, and Berge's maximum theorem.

Selected references

• J.-P. Carvalho, B. S. R. Pradelski, C. Williams, Intersectionality: Affirmative Action with Multidimensional Identities, Management Science 71(5), 2025; author manuscript hal-04788142v1. https://hal.science/hal-04788142v1, https://doi.org/10.1287/mnsc.2023.03839
• A. Fonda, P. Gidoni, Generalizing the Poincaré–Miranda theorem: the avoiding cones condition, Annali di Matematica Pura ed Applicata 195, 2016. https://doi.org/10.1007/s10231-015-0519-7
• C. D. Aliprantis, K. C. Border, Infinite Dimensional Analysis: A Hitchhiker's Guide, 3rd ed., Springer, 2006 (Theorem 17.31, Berge's maximum theorem). https://doi.org/10.1007/3-540-29587-9

Motivation

Ranking and selection (R&S) asks which of $k$ simulated systems has the largest mean performance when every observation is costly. It is a basic tool of simulation optimization: choosing a staffing level, an inventory policy or a network design from a large catalogue of candidates that can only be evaluated by noisy simulation. In the fixed-budget formulation a total of $B$ observations is spent sequentially and one alternative is selected at the end; procedures are compared by their probability of correct selection (PCS).

Cloud and parallel computing have made problems with thousands to millions of alternatives routine, and the relevant question is how the budget must grow with $k$. A procedure is sample optimal if a budget $B = ck$, linear in $k$, keeps its PCS bounded away from zero as $k \to \infty$; a total budget of order $k$ is clearly necessary. Li, Fan and Hong (arXiv:2303.02951) show that the simplest procedure of all, the greedy procedure, which always samples the alternative with the largest current sample mean, is sample optimal. They also show that its PCS limit is strictly below one under the slippage configuration, however large $c$ is: the greedy procedure is not consistent. This mission formalizes the remedy: an exploration phase of $n_0$ observations per alternative before the greedy phase makes the procedure consistent.

Setting

There are $k$ alternatives. Alternative $i$ produces independent observations $X_{i1}, X_{i2}, \dots \sim N(\mu_i, \sigma_i^2)$, independent across alternatives, and alternative 1 is the unique best. The running average after $n$ observations is $\bar X_i(n) = \frac1n\sum_{j=1}^n X_{ij}$.

Assumption 1 (p. 12). There are constants $\gamma > 0$ and $\bar\sigma^2 > 0$ such that $\mu_1 - \max_{i \ge 2}\mu_i \ge \gamma$ and $\max_i \sigma_i^2 \le \bar\sigma^2$, regardless of how large $k$ is.

The explore-first greedy (EFG) procedure (Procedure 2, p. 21) with exploration size $n_0$ and budget $B$:

1. take $n_0$ observations from every alternative, and set $n_i = n_0$;
2. while $\sum_i n_i < B$, take one more observation from $\arg\max_i \bar X_i(n_i)$;
3. select $\arg\max_i \bar X_i(n_i)$.

With $B = ck$ the exploration phase uses $n_0 k$ observations and the greedy phase $n_g k$, where $n_g = c - n_0$. The greedy procedure is the case $n_0 = 1$.

Crossing times. Let $Z_1, Z_2, \dots$ be iid standard normal, $\bar Z(n) = \frac1n\sum_{j=1}^n Z_j$, and

$$\tilde N(x; n_0) = \inf\{n \ge n_0 : \bar Z(n) < x\}, \qquad C(x; n_0) = \mathrm E\big[\tilde N(x; n_0)\big] \in [0, \infty],$$

with $\inf \emptyset = \infty$. $C(\cdot\,; n_0)$ is finite exactly on $(0, \infty)$, where it is strictly decreasing and continuous.

Consistency (Definition 2, p. 21): A sample-optimal fixed-budget R&S procedure is consistent if the PCS of the procedure satisfies that, for any $\alpha \in (0,1)$, there exists a constant $c>0$ such that $\liminf_{k\to\infty} \mathrm{PCS} \ge \alpha$, for $B = ck$.

Formalization targets

Goal: Theorem 4 (p. 24)

Suppose Assumption 1 holds. Let $\alpha \in (0,1)$ and $\gamma_0 \in (0, \gamma)$. Let $n_0 \ge 1$ satisfy

$$\Pr\Big\{\min_{n \ge n_0} \bar X_1(n) > \mu_1 - \gamma_0\Big\} \ge \alpha \tag{5.3}$$

and let $n_g \ge C\big(\tfrac{\gamma - \gamma_0}{\bar\sigma}; n_0\big) - n_0$. If $B = (n_0 + n_g)k$, then the PCS of the EFG procedure satisfies

$$\liminf_{k \to \infty} \mathrm{PCS} \ \ge\ \alpha .$$

Milestones

1. Lemma 3 (p. 22): $\bar Z(n)$, $n \ge n_0$, attains its minimum at a finite time almost surely.
2. (5.1) (p. 22): $\tilde N(x) \le \tilde N(x; n_0) \le n_0 \inf\{m \ge 1 : \bar Z(mn_0) < x\}$, and the last crossing time is distributed as $\tilde N(\sqrt{n_0}\,x)$ (scaling corrected, see below).
3. Lemma 4 (p. 22): $\tilde N(x;n_0)$ is a.s. finite with finite mean for $x > 0$; finite with probability strictly between 0 and 1, with infinite mean, for $x < 0$; a.s. finite with infinite mean for $x = 0$.
4. Lemma 7 (p. ec6): $C(x; n_0)$ is strictly decreasing and continuous on $(0, \infty)$.
5. (5.2) (p. 23): $\mathrm{PCS} \ge \Pr\big\{\sum_{i=2}^k N_i(\bar X_1^*(n_0); n_0) + N_1^*(n_0) \le B\big\}$, where $\bar X_1^*(n_0)$ and $N_1^*(n_0)$ are the minimum and argmin of $\bar X_1(n)$ over $n \ge n_0$, and $N_i(b; n_0)$ is the first $n \ge n_0$ with $\bar X_i(n) < b$.
6. Theorem 3 (p. 23, first sentence): if $B/k = n_0 + n_g$ and $n_g > C(\gamma/\bar\sigma; n_0) - n_0$, then $\liminf_k \mathrm{PCS} \ge \Pr\{\min_{n\ge n_0}\bar X_1(n) > \mu_1 - \gamma_0\}$, where $\gamma_0 \in (0, \gamma)$ solves $C\big(\tfrac{\gamma-\gamma_0}{\bar\sigma}; n_0\big) = n_g + n_0$.
7. Lemma 5 (p. 24): for every $\gamma_0 > 0$ and $\alpha \in (0,1)$ some finite $n_0 \ge 1$ satisfies (5.3).

Significance

The result. Theorem 4 shows that a one-line change to the greedy procedure, a fixed number of initial observations per alternative, turns a sample-optimal but inconsistent procedure into one that is both sample optimal and consistent. Any PCS target is reached with a budget that grows only linearly in the number of alternatives, without variance estimates, elimination rules or pairwise comparisons. Together with (5.4) (p. 24) it also gives a recipe for choosing $n_0$ and $n_g$ when $\gamma$ and $\bar\sigma^2$ are known, which converts the fixed-budget procedure into a fixed-precision one.

Formalizing it. The results are proved in the paper, but Lemma 4 and Theorem 4 have their proofs omitted ("straightforward"), and Theorem 3's proof refers to "almost the same analysis" as Theorem 1. A machine-checked development makes these steps explicit. It also corrects the scaling in (5.1), which is misprinted in the source. No part of it is formalized on the platform. The boundary-crossing inequality (5.2) and the crossing-time lemmas for the Gaussian running average are reusable in the companion missions of this series and for other greedy procedures.

Difficulty

The obvious approach is to bound each inferior alternative's sample size by the number of observations it needs to fall below alternative 1, and to sum. It fails because alternative 1's running average is itself random, may drop below its mean, and can lose the lead at any time before it reaches its minimum. The boundary must be the random minimum $\bar X_1^*(n_0)$, and the crossing times of the other alternatives are then dependent through it. The step from (5.2) to Theorem 3 needs crossing times dominated by iid copies of $\tilde N(\cdot\,; n_0)$ on the event that the minimum is high, a strong law over the growing array, and the continuity of $C(\cdot\,; n_0)$ (Lemma 7) to pass to the limit in the level. Lemma 4 needs fluctuation facts for the Gaussian random walk (finite expected crossing time for $x>0$, infinite mean at $x=0$) that are not in Mathlib.

Formalization scope

• Model. Observations form an array $X_{ij}$ indexed by $\mathbb N \times \mathbb N$ on a probability space, mutually independent, with $X_{ij} \sim N(\mu_i, \sigma_i^2)$ and $\sigma_i^2 > 0$. Problem $k$ uses alternatives $0, \dots, k-1$; Lean's alternative $0$ is the paper's alternative 1. One array serves every $k$, which does not change any PCS.

• Procedure. The EFG procedure is a deterministic map from the observation array to the selected index. Ties in every arg max go to the smallest index, which is a null event under the model. The greedy loop runs $B - n_0k$ times (none if $B \le n_0k$).

• Budget. $B = (n_0 + n_g)k$ is read as $\lfloor (n_0+n_g)k \rfloor$. Conditions involving $C(\cdot\,; n_0) - n_0$ are written additively in $[0, \infty]$.

• Crossing times, argmins and $C$. These take values in $\mathbb N \cup \{\infty\}$ and $[0, \infty]$. A path that never crosses has crossing time $\infty$, and $C(0; n_0) = \infty$ is literal. "$\min_{n \ge n_0} \bar X_1(n) > a$" means that the path is bounded below from $n_0$ on and its infimum exceeds $a$. The minimum is attained a.s. (Lemma 3).

• Probabilities and limits. These are extended nonnegative reals. The liminf is taken in $[0, \infty]$.

• (5.1) correction. The paper derives $\tilde N(x;n_0) \le n_0\tilde N(x/\sqrt{n_0})$ from "$\bar Z(mn_0) = \sqrt{n_0}\,\bar Z(m)$ statistically". In fact $\bar Z(mn_0) \overset{d}{=} \bar Z(m)/\sqrt{n_0}$, so the milestone states the bound with $\tilde N(\sqrt{n_0}\,x)$. The printed form is false for $x < 0$ and $n_0 \ge 2$.

• Theorem 3. The existence of $\gamma_0$, implicit in the paper, is a conclusion of the statement, so the lower bound cannot hold vacuously. The slippage-configuration limit in its second sentence is not stated.

• Ruled out. None of the following can make the statements trivial, because the encodings above exclude them:

  • an $\mathbb N$-valued crossing time with $\inf\emptyset = 0$;
  • a real infimum of an unbounded path read as $0$;
  • an unsolvable equation for $\gamma_0$.

• Infrastructure needed. A complete development needs the following, all reusable beyond this mission:

  • laws of crossing times of the Gaussian random walk;
  • the strong law for iid $\mathbb N\cup\{\infty\}$-valued variables;
  • a coupling of the crossing times with iid copies;
  • a pathwise induction over the run of the procedure for (5.2).

  Contributions to any milestone are welcome.

• Source. The source is the authors' arXiv preprint, version 3 (11 Dec 2023), and all numbering follows it.

Selected references

• Z. Li, W. Fan, L. J. Hong, The (Surprising) Sample Optimality of Greedy Procedures for Large-Scale Ranking and Selection, arXiv:2303.02951v3, 2023; Management Science, 2025. https://arxiv.org/abs/2303.02951
• R. E. Bechhofer, A single-sample multiple decision procedure for ranking means of normal populations with known variances, Annals of Mathematical Statistics 25(1):16–39, 1954. https://doi.org/10.1214/aoms/1177728845
• S.-H. Kim, B. L. Nelson, A fully sequential procedure for indifference-zone selection in simulation, ACM Transactions on Modeling and Computer Simulation 11(3):251–273, 2001. https://doi.org/10.1145/502109.502111

Motivation

Ranking and selection (R&S) asks how to spend a fixed budget of simulation runs on $k$ competing system designs so that the design with the largest mean performance is identified with high probability. When $k$ runs into the thousands or millions, the relevant question is how the total budget must grow with $k$. Li, Fan and Hong (arXiv:2303.02951v3, published in Management Science, 2025) showed that the simplest adaptive rule, the greedy procedure, is sample optimal: a budget linear in $k$ keeps the probability of correct selection (PCS) bounded away from zero (their Theorem 1, p. 15). This mission formalizes their second main result: under the least favorable configuration of means and variances, the PCS lower bound of Theorem 1 is exactly the limit, so it cannot be improved for the greedy procedure.

The result also explains the paper's later design choices. Corollary 1 (p. 18) deduces from it that the greedy procedure is not consistent: however large the constant $c$ in $B = ck$, its worst-case PCS stays below a constant less than one. This is why §5 of the paper introduces an explore-first variant.

Setting

There are $k$ alternatives. Alternative $i$ produces independent observations $X_{i1}, X_{i2}, \dots \sim N(\mu_i, \sigma_i^2)$, independent across alternatives, and alternative $1$ is the unique best. The running average of alternative $i$ after $n$ observations is $\bar X_i(n) = \frac1n \sum_{j=1}^n X_{ij}$.

The greedy procedure (Procedure 1, p. 10) takes one observation from each alternative, then repeatedly takes one more observation from the alternative with the largest current running average, until $B$ observations have been taken in total; it selects the alternative with the largest final running average. PCS is the probability that it selects alternative $1$, and PICS $= 1 -$ PCS.

The slippage configuration with a common variance (SC-CV, §4.3, p. 16) is

$$\mu_1 - \mu_i = \gamma > 0 \quad (i = 2, \dots, k), \qquad \sigma_i^2 = \sigma^2 > 0 \quad (i = 1, \dots, k):$$

the non-best alternatives share one mean and all alternatives share one variance.

The constant governing the analysis is

$$C(x) = \exp\Big( \sum_{n=1}^\infty \frac1n \Phi(-\sqrt n\, x) \Big), \qquad x > 0,$$

where $\Phi$ is the standard normal distribution function. By Lemma 2 of the paper, $C(x)$ is the expected first time $n$ at which the running average of iid $N(0,1)$ variables drops below $x$; it is continuous and strictly decreasing on $(0, \infty)$ and tends to $\infty$ as $x \to 0^+$.

Formalization targets

Goal: Theorem 2 (p. 16)

If $B = ck$ and $c > C(\gamma/\sigma)$, let $\gamma_0 \in (0, \gamma)$ solve $C((\gamma - \gamma_0)/\sigma) = c$. Under the SC-CV,

$$\lim_{k\to\infty} \mathrm{PCS} = \Pr\Big\{ \min_{n\ge1} \bar X_1(n) > \mu_1 - \gamma_0 \Big\} = \Big[C\Big(\frac{\gamma_0}{\sigma}\Big)\Big]^{-1}.$$

The goal asserts both that some such $\gamma_0$ exists and that the limit holds for every solution.

Milestones, in the order of the proof (EC.1.4, pp. ec3–ec5)

1. (EC.1.8), p. ec4: with $m_\epsilon$ the first time $\bar X_1$ drops below a level $\mu_1 - \gamma_\epsilon^+$, PICS is at least the probability that the budget suffices to reach $m_\epsilon$ but not to push every other alternative below the new minimum of $\bar X_1$.
2. (EC.1.11), p. ec5, with $\gamma_\epsilon^\pm$ from (EC.1.7): $\liminf_k \mathrm{PICS} \ge \Pr\{ m_\epsilon < \infty, \min_{1\le n\le m_\epsilon-1} \bar X_1(n) \ge \mu_1 - \gamma_\epsilon^- \}$.
3. (EC.1.6), p. ec3: $\liminf_k \mathrm{PICS} \ge \Pr\{\exists n \ge 1 \text{ s.t. } \bar X_1(n) < \mu_1 - \gamma_0\}$.
4. Theorem 1 under the SC-CV, p. 15: $\liminf_k \mathrm{PCS} \ge \Pr\{\min_{n\ge1} \bar X_1(n) > \mu_1 - \gamma_0\} = [C(\gamma_0/\sigma)]^{-1} > 0$.

Milestones 3 and 4 bound the PCS from above and below by the same quantity, up to the null event $\{\min_n \bar X_1(n) = \mu_1 - \gamma_0\}$. Corollary 1 (p. 18, $\lim \mathrm{PCS} \le [C(\gamma/\sigma)]^{-1} < 1$) is included as a separate theorem after the goal; it is not a milestone.

Significance

The result. Theorem 1 gives a lower bound on the asymptotic PCS that holds for every configuration satisfying a gap and a variance bound. Theorem 2 shows the bound is attained under the SC-CV, so it is the exact worst-case asymptotic PCS of the greedy procedure on a linear budget. It also identifies the slippage configuration as least favorable for this procedure. Corollary 1, which follows from it, shows that the greedy procedure is sample optimal without being consistent. The paper uses this to motivate the explore-first greedy procedure of §5, which is consistent.

Formalizing it. The theorem is proved in the paper; none of it is formalized. A formal proof requires a precise, total definition of the greedy procedure as a map from an observation array to a selected alternative, a pathwise analysis of that map (milestone 1), the strong law of large numbers for iid crossing times with values in $\mathbb N \cup \{\infty\}$, and a limiting argument in $\epsilon$ that uses the continuity and strict monotonicity of $C$. The identity $\Pr\{\min_n \bar X_1(n) > \mu_1 - \gamma_0\} = [C(\gamma_0/\sigma)]^{-1}$ is the Gaussian case of Spitzer's identity, which Mathlib does not have.

Difficulty

The lower half is Theorem 1. The upper half needs a different pathwise argument. Showing that the greedy procedure can succeed only requires bounding the budget the inferior alternatives consume. Showing that it must fail requires an event on which alternative 1 has fallen below a level and the remaining budget cannot lift it back. The paper conditions on such an event, $B_\epsilon$. On $B_\epsilon$, two families of crossing times, measured against two different random levels (the running minimum of $\bar X_1$ before and at $m_\epsilon$), are compared with deterministic multiples of $k$. Both comparisons need the strong law, and the event $B_\epsilon$ must survive the limit $\epsilon \to 0$. The obvious first idea is to copy the proof of Theorem 1 with the inequalities reversed. It fails because the inclusion (3.2) behind Theorem 1 is one-sided: a large budget forces a correct selection, but a small budget alone does not force an incorrect one.

Formalization scope

• Model. Alternatives are indexed from $0$ in Lean: Lean's alternative $0$ is the paper's alternative $1$. Observations form one infinite array $X_{ij}$ on a probability space, mutually independent over all pairs $(i, j)$, with $X_{ij} \sim N(\mu_i, v_i)$. The problem with $k$ alternatives reads rows $0, \dots, k-1$. PCS for $k$ alternatives depends only on the law of those rows, so this coupling changes no PCS.
• Procedure. The procedure is a deterministic function of the array. Ties in every arg max go to the smallest index; ties have probability zero under normality. With fewer than $k$ observations of budget, no greedy step is taken.
• Budget. "$B = ck$" is read as $B = \lfloor ck \rfloor$.
• Values. Probabilities, limits and liminfs are taken in $[0, \infty]$. Crossing times take values in $\mathbb N \cup \{\infty\}$, with $\infty$ when no crossing occurs. "$\min_{n\ge1} \bar X_1(n) > a$" means the running average is bounded below and its infimum exceeds $a$; the minimum is attained almost surely.
• The constant $C$. It is defined by the series above. Every statement evaluates it only at positive arguments ($\gamma/\sigma$, $(\gamma - \gamma_0)/\sigma$, $\gamma_0/\sigma$), where the series converges.
• Disclosed generalization. Milestone 1 is stated for an arbitrary level and for arbitrary means with positive variances, since the inclusion uses neither the SC-CV nor the event $B_\epsilon$.

Three trivializations are ruled out. Crossing times typed in $\mathbb N$ would be $0$ when no crossing occurs. Junk values of tsum or of the infimum on unbounded sets would make the statements meaningless. A $\gamma_0$ that no value can satisfy would make the goal vacuous, which is why the goal also asserts that $\gamma_0$ exists.

Infrastructure needed: the strong law for iid $\mathbb N \cup \{\infty\}$-valued variables with finite mean, Spitzer's identity for Gaussian random walks, and continuity of $C$. These would be reusable in any boundary-crossing analysis of sequential procedures. Contributions toward any milestone, or toward these general lemmas, are welcome. The source PDF is the arXiv v3 preprint (11 Dec 2023), and all page and equation numbers refer to it.

Selected references

• Z. Li, W. Fan, L. J. Hong, The (Surprising) Sample Optimality of Greedy Procedures for Large-Scale Ranking and Selection, arXiv:2303.02951v3, 2023; Management Science, 2025. https://arxiv.org/abs/2303.02951
• F. Spitzer, A combinatorial lemma and its application to probability theory, Trans. Amer. Math. Soc. 82 (1956), 323–339. https://doi.org/10.1090/S0002-9947-1956-0079851-X
• R. E. Bechhofer, A single-sample multiple decision procedure for ranking means of normal populations with known variances, Ann. Math. Statist. 25 (1954), 16–39. https://doi.org/10.1214/aoms/1177728845