All missions

Shortest paths in an unweighted graph

Breadth-first search computes which vertices can be reached from a source and the fewest edges needed to reach each one. Its predecessor information also records a shortest route. This mission belongs to the CLRS fourth-edition formalization series and targets Chapter 20, §20.2, including the algorithm's linear running-time guarantee. The section placement is given in the publisher's table of contents.

Graph, source, and outputs

A directed graph consists of vertices numbered $0,\ldots,n-1$ and outgoing adjacency rows. The field adj[u] is an integer sequence, and degree[u] determines its meaningful prefix. Every entry in that prefix must name a valid vertex. Let $m$ be the sum of these row lengths: parallel arcs count separately, and self-loops are permitted. An undirected graph is represented by symmetric directed entries, with both directions counted in $m$.

The caller supplies a valid source $s$, with $0\le s<n$. Consequently, the source contract excludes the empty graph. The distance output uses $-1$ for an unreachable vertex; otherwise it records a nonnegative number of edges. The parent output uses $-1$ at the source and unreachable vertices. Other reached vertices have a predecessor. No particular choice between equally short routes is required.

Formalization targets

The headline CLRS.BFS.correctness_and_running_time asks for one actual terminating bfs.Call whose result satisfies correctness, preservation, allocation, and running time together. Write $D$ and $P$ for its output arrays and $s\leadsto v$ for a finite directed walk in the initial graph. For every vertex $v$,

$$D[v]=-1\iff\neg(s\leadsto v).$$

When $D[v]\ge0$, the returned distance is attained and minimal:

$$\exists\text{ a walk }s\leadsto v\text{ of length }D[v],\qquad D[v]\le\text{length}(p)\text{ for every walk }p:s\leadsto v.$$

Moreover, $D[s]=0$, $P[s]=-1$, and each reached $v\ne s$ satisfies

$$P[v]\to v,\qquad D[P[v]]+1=D[v].$$

The running-time target is uniform over inputs, heaps, adjacency order, and initial counters:

$$\exists C\in\mathbb N,\ C>0:\quad T\le C(1+n+m).$$

Here $T$ is the increment of graph_work for that same call. The supporting milestone correctness_and_explicit_running_time retains the stronger numerical target

$$T\le 6n+2m+5$$

with the identical correctness and storage contract. Both statements are open; the numerical bound is a requested obligation, not an established result.

A reusable shortest-path contract

The result allows a later caller to read shortest distances and predecessor edges while continuing with the returned heap. The caller-facing predicate CLRS.BFS.Post before after result g source includes both the mathematical result and caller-storage preservation. It requires a fresh result object and two distinct fresh arrays, and preserves every previously allocated sequence, object, and collection. The goals combine that postcondition with the same terminating Call and its cost. Input graph storage therefore remains available for further traversals.

The textbook supplies the mathematical algorithm and analysis; the work here is their formal verification against a mutable source program. The finite-prefix specification gives callers useful facts without prescribing irrelevant sequence entries outside the vertex range. The source's discovery state is encoded by distance $-1$, and its queue is a fresh sequence with head and tail indices. These are implementation choices within the stated BFS contract. The familiar correctness and complexity claims are discussed in CLRS, fourth edition, §20.2.

What must be justified

Returning a reachable predecessor alone does not establish shortestness. The contract also requires minimum distance and a correct unreachable sentinel. Cycles, repeated adjacency entries, and edges to vertices already discovered must not produce repeated queue insertion or invalidate the cost bound. An execution theorem must establish termination and the result together; reasoning only about executions that happen to return leaves a missing obligation.

Formalization scope

CLRS.GraphTraversal.GraphRep connects the input heap to a finite mathematical graph. Adjacency rows may share references, because traversal only reads them. Validity includes allocated rows and nonnegative degrees. The explicit initialization loop is counted even though the result constructor already gives the same default values. Outputs are fresh, so their mutation cannot change aliased input storage.

The shared prerequisites are the published Algo2Lean runtime, module-call support, and unweighted graph representation and specifications. All three missions reuse these same definitions by reference, without introducing duplicate prerequisite bundles. The existing Dijkstra graph definition uses weighted, object-linked adjacency lists; the shared unweighted module supplies the arrays-of-arrays storage contract used here.

The definitions use Algo2Lean v0.1.4, source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, in project mode with standalone=false. The source root contains the explicitly named modules below; the entry file is identified for each mission. Raw generated definitions and platform import-path adaptations are recorded separately in the reproduction manifest. Stable generated definitions supply the public Call relations; optional named-line interfaces are not part of the goal statements.

The clock graph_work counts the marked source blocks, function entries, and evaluated loop guards, including final false guards. Each marked block contains a fixed amount of source work. Costs are differences between the caller's actual initial and final counters; other clocks are preserved. This model uses mathematical integer sequences and unbounded integers. It does not assert machine wall-clock time, integer bit complexity, stack-space bounds, or Lean proof-checking time. Construction of the caller's input graph is outside the traversal entry point.

All theorem bodies are open contributor tasks. Supplied definitions and well-formed goal statements are not correctness, termination, or running-time proofs. The requested results concern the displayed program's actual executions, not an assumed-correct replacement algorithm or a hypothesis containing its conclusion.

The complete source entry is bfs.algo; its shared dependency is graph_input.algo. Contributors may add proof lemmas or named observations while retaining the main source-facing contract.

graph_input.algo

# Unweighted directed graph: vertices are 0, ..., size-1.
# Row adj[u][0:degree[u]] lists outgoing targets, with one slot per arc.
# Traversals require nonnegative degrees and in-range targets. Duplicate arcs
# and self-loops are allowed. The constructor stores the supplied references.

class UnweightedGraph:
    size: Int
    adj: Seq[Seq]
    degree: Seq

    def __init__(self, size: Int, adj: Seq[Seq], degree: Seq) -> None:
        self.size = size
        self.adj = adj
        self.degree = degree

bfs.algo

# CLRS, fourth edition, Chapter 20, Section 20.2: breadth-first search.
# Adjacency rows contain vertex identifiers; degree gives each finite row length.
# The graph is read-only. A valid source lies between 0 and graph.size - 1.

from graph_input import UnweightedGraph


class BFSResult:
    distance: Seq
    parent: Seq

    def __init__(self) -> None:
        tick("graph_work")
        self.distance = const(-1)
        self.parent = const(-1)


def bfs(graph: UnweightedGraph, source: Int) -> BFSResult:
    tick("graph_work")
    result = BFSResult()
    vertex: Int = 0

    tick("graph_work")
    while vertex < graph.size:
        tick("graph_work")
        result.distance[vertex] = -1
        result.parent[vertex] = -1
        vertex += 1
        tick("graph_work")

    tick("graph_work")
    queue: Seq = const(-1)
    head: Int = 0
    tail: Int = 1
    queue[0] = source
    result.distance[source] = 0

    tick("graph_work")
    while head < tail:
        tick("graph_work")
        vertex = queue[head]
        head += 1
        index: Int = 0

        tick("graph_work")
        while index < graph.degree[vertex]:
            tick("graph_work")
            neighbor: Int = graph.adj[vertex][index]
            if result.distance[neighbor] == -1:
                tick("graph_work")
                result.distance[neighbor] = result.distance[vertex] + 1
                result.parent[neighbor] = vertex
                queue[tail] = neighbor
                tail += 1
            index += 1
            tick("graph_work")

        tick("graph_work")

    tick("graph_work")
    return result

Selected references

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022. Publisher; fourth-edition table of contents.
• Lunjia Hu and Chutong Yang, Algo2Lean, software release v0.1.4. Lunjia Hu is the project creator. Hosted compiler; fixed release source.

Motivation

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

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

Setting

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

Three assumptions restrict $\mathbb Y$:

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

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

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

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

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

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

Formalization targets

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

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

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

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

Milestones

In attack order:

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

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

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

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

attained only at $\mathbb T^*$.

Companion statements

These are not milestones:

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

Committed conventions:

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

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

Added hypotheses.

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

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

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

Selected references

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

Motivation

Platform markets often feature a Superstar: a single complement whose presence moves consumers, such as a blockbuster game on a console or a star streamer on a video platform. Whether such a Superstar signs an exclusive deal with one platform or stays available on both is a recurring question for competition authorities and for platform managers. Empirical work documents both sides of the effect. Exclusive titles help small consoles challenge incumbents (Lee 2013). Superstar apps generate demand-discovery spillovers for small developers (Ershov 2020, NET Institute working paper). When a star streamer switched platforms, viewers followed and other content producers repositioned (Förderer & Gutt 2021, working paper).

Carroni, Madio & Shekhar (Management Science, 2024) build a two-sided Hotelling model with three groups of agents: consumers, a fringe of small complementors, and the Superstar. The model asks how Superstar exclusivity changes prices, participation and welfare. This mission formalizes the paper's analysis of the complementor side under vertical separation. The analysis runs through the equilibrium prices (Lemmas 1–3) and the sorting of complementors into multihomers, singlehomers and inactive firms (Proposition 1). It ends in the welfare result that exclusivity raises complementors' total surplus (Proposition 3).

Setting

Two platforms $1$ and $2$ sit at the ends of a Hotelling line. A unit mass of consumers has types $m\in[-\bar m,\bar m]$, distributed with cumulative distribution function $F$ and density $f$. The type $m$ measures the preference for platform $2$ over platform $1$. The Superstar is worth $\phi$ to a consumer of a platform that hosts it, and $g_i\in\{0,1\}$ records its presence on platform $i$. A consumer of type $m$ joins platform $1$ rather than $2$ when

$$m\le \tilde m=\phi(g_1-g_2)-(p_1-p_2)+\theta(N_1-N_2),$$

where $p_i$ are the consumer prices, $N_i$ the masses of complementors on the platforms, and $\theta>0$ the value of a unit mass of complementors to a consumer. Platform $1$'s consumer share is $D=F(\tilde m)$ and platform $2$'s is $1-D$.

Complementors have an opportunity cost $k\ge0$ of joining each platform, distributed with mass function $\Lambda$ and density $\lambda$. A complementor receives $\gamma>0$ per unit mass of consumers, so it joins platform $i$ if and only if $k\le\gamma D_i$, and $N_i=\Lambda(\gamma D_i)$. A complementor that joins both platforms pays $k$ twice.

Expectations are fulfilled: the share $D$ solves the fixed-point equation

$$D=F\bigl(\phi(g_1-g_2)-(p_1-p_2)+\theta[\Lambda(\gamma D)-\Lambda(\gamma(1-D))]\bigr).$$

Platforms choose prices simultaneously to maximise gross profit $p_iD_i$. Under exclusivity the Superstar is on platform $1$ only ($g=(1,0)$); under non-exclusivity it is on both ($g=(1,1)$). The paper's standing assumptions are smoothness and symmetry of $F$, a positive nondecreasing density $\lambda$, and Assumption 3: $f\gamma\theta[\lambda(\gamma F)+\lambda(\gamma(1-F))]<1$, which keeps cross-group externalities below the differentiation parameter. The complementors' total surplus at shares $(D_1,D_2)$ is

$$FS(D_1,D_2)=\int_0^{\gamma D_1}(\gamma D_1-k)\lambda(k)\,dk+\int_0^{\gamma D_2}(\gamma D_2-k)\lambda(k)\,dk .$$

Formalization targets

Goal: Proposition 3

For $\phi>0$, let $D(\phi)$ be platform $1$'s share in the selected exclusivity equilibrium and $E$ the share in the symmetric non-exclusive equilibrium. Then

$$FS\bigl(E,1-E\bigr)<FS\bigl(D(\phi),1-D(\phi)\bigr).$$

The statement fixes no functional forms and no constants. It holds for every model satisfying the assumptions and every $\phi>0$.

Milestones

1. Lemma 1. At every interior equilibrium, $p_1=F(m^\star)\{1/f(m^\star)-\gamma\theta[\lambda(\gamma D_1)+\lambda(\gamma D_2)]\}$, and $p_2$ is the same expression with $1-F(m^\star)$ in place of $F(m^\star)$.
2. Lemma 2. Under non-exclusivity at equal prices, $D=\tfrac12$, $m^\star=0$ and $p=1/(2f(0))-\gamma\theta\lambda(\gamma/2)$. All active complementors multihome.
3. Lemma 3 (demand and complementor part). Under exclusivity, $D^\star_1(1,0)>D^\star_2(0,1)$ and $\Lambda(\gamma D^\star_1)>\Lambda(\gamma D^\star_2)$.
4. Proposition 1. Under exclusivity, complementors with $k\in(0,\gamma D^\star_2]$ multihome, those with $k\in(\gamma D^\star_2,\gamma D^\star_1]$ singlehome on platform $1$, and the rest are inactive. More complementors are active than under non-exclusivity.
5. Decomposition of $\Delta FS$ (Section 4.3) into the contributions of multihomers, of switchers from multihoming to singlehoming, and of entrants.

Significance

The result says that a Superstar's exclusive contract, usually discussed as a tool of foreclosure against the rival platform, benefits the fringe of complementors taken as a whole. Some complementors stop paying for a second platform. Others, inactive without exclusivity, enter on the favoured platform. The comparison feeds into the paper's welfare analysis (consumer surplus, Proposition 4) and into its account of when the Superstar chooses exclusivity (Proposition 5). It supplies a theoretical counterpart to the empirical spillover findings cited above.

The paper's proofs are informal in places that matter. Equilibrium selection under fulfilled expectations is described in words only, and the derivative argument for Lemma 3 tracks an equilibrium as a function of $\phi$ without saying which one. A formal development has to fix these choices, and this mission fixes them explicitly (see Formalization scope). None of these results has been machine-checked before. The fixed-point and first-order machinery for two-sided fulfilled-expectations demand would also serve other platform-competition models in the Armstrong (2006) tradition.

Difficulty

The surplus comparison itself is elementary once the equilibrium shares are known. The work lies in the equilibrium shares. Fulfilled-expectations demand is defined by a fixed point that can have several solutions, so neither the share at a deviation price nor the equilibrium share is a priori a function of prices. The obvious first step, "impose symmetry", does not prove that the non-exclusive share is $\tfrac12$. One must show that $\tfrac12$ is the only interior fixed point at equal prices. Likewise, the exclusive share exceeds $\tfrac12$ only for the equilibrium reached continuously from the symmetric one. Coordination on the disfavoured platform is a fulfilled-expectations outcome the model does not exclude. Lemma 1 needs a differentiable local branch of the fixed point at a deviation, which is where Assumption 3 enters.

Formalization scope

Everything is real-valued. The model is a structure with $\bar m,\gamma,\theta>0$, functions $F,f,\Lambda,\lambda:\mathbb R\to\mathbb R$, and the following hypotheses:

• $F$ is continuous and monotone, $0$ left of $-\bar m$ and $1$ right of $\bar m$, $C^2$ with $F'=f>0$ on $(-\bar m,\bar m)$, and symmetric, $F(-x)=1-F(x)$;
• $\Lambda(0)=0$, $\Lambda$ is $C^2$ with $\Lambda'=\lambda$, and $\lambda>0$ is nondecreasing on $[0,\gamma]$;
• Assumption 3 holds on $(-\bar m,\bar m)$.

Several conventions depart from the paper's wording:

• The paper asks for $\lambda>0$, $\lambda'\ge0$ on all of $[0,\infty)$ for a distribution function $\Lambda$, which no distribution satisfies. These conditions are imposed on $[0,\gamma]$, the only range on which $\Lambda$ is evaluated.
• The bounds on $f'$ in Assumption 2 are dropped, which only strengthens the statements.
• "$\bar m$ large enough" is replaced by interiority ($0<D<1$) of every equilibrium considered.
• The standalone value $v$ cancels and is omitted.

Fulfilled-expectations demand is a relation, not a chosen function. A price equilibrium is a Nash equilibrium in prices in which no deviation is profitable for any fulfilled-expectations share it induces. Lemma 1's formulas are a theorem about this equilibrium, not its definition. The symmetric non-exclusive outcome is the interior equilibrium at equal prices. The exclusive outcome is the end point, at value $\phi$, of a continuous path of interior equilibria of the games with Superstar value $t\in[0,\phi]$, starting from equal prices at $t=0$. Platform $2$'s share is always $1-D$.

The goal must not be posed with $D(\phi)>\tfrac12$, $D(\phi)\ne\tfrac12$ or $E=\tfrac12$ as a hypothesis: since $D\mapsto FS(D,1-D)$ is strictly convex and symmetric about $\tfrac12$, any of these would reduce it to a calculus exercise. The price ranking in Lemma 3 is not part of the mission. Its proof rests on bounds on $f'$ that the paper states only as functions of unspecified equilibrium arguments.

The needed infrastructure is the implicit function theorem in one variable, interval integrals of continuous functions, and the intermediate value theorem. Contributions are welcome on any milestone, on alternative proofs of the goal, and on reusable lemmas about uniqueness of fulfilled-expectations fixed points.

Selected references

• Carroni, E., Madio, L., Shekhar, S., Superstar Exclusivity in Two-Sided Markets, Management Science 70(2):991–1011, 2024; accepted manuscript at IRIS Bologna. https://doi.org/10.1287/mnsc.2023.4720, http://hdl.handle.net/11585/922035
• Armstrong, M., Competition in Two-Sided Markets, RAND Journal of Economics 37(3):668–691, 2006. https://doi.org/10.1111/j.1756-2171.2006.tb00037.x
• Fudenberg, D., Tirole, J., Customer Poaching and Brand Switching, RAND Journal of Economics 31(4):634–657, 2000. https://doi.org/10.2307/2696352
• Lee, R. S., Vertical Integration and Exclusivity in Platform and Two-Sided Markets, American Economic Review 103(7):2960–3000, 2013. https://doi.org/10.1257/aer.103.7.2960
• Ershov, D., Competing with Superstars in the Mobile App Market, NET Institute Working Paper, 2020.
• Förderer, J., Gutt, D., The Effects of Platform Superstars on Content Production: Evidence from Ninja, working paper, 2021.

Motivation

Sports leagues, tournaments, esports events and research competitions all end with a ranking of the participants and a sum of prize money to divide among them. How the money is split according to the ranking is a design choice with visible consequences: Winner-Takes-All schemes reward only the top, equal division ignores the ranking, and most real prize schedules sit in between. The economics of tournaments has studied prize structures as incentive devices, but it has not asked which schedules follow from principles of fairness and coherence.

Dietzenbacher and Kondratev (arXiv:2008.08985, Management Science 2023) take the axiomatic approach of fair allocation theory to this question. The central axiom is consistency, the variable-population principle that has characterized solutions in bankruptcy, taxation, bargaining and cooperative games (Aumann and Maschler 1985; Young 1987; Lensberg 1988; Thomson 1988; Hart and Mas-Colell 1989): if any subgroup of competitors pools its prizes and re-divides them among themselves by the same rule, nobody's prize changes. This mission formalizes the paper's first main result, which identifies exactly the rules that are consistent, weakly respect the ranking, and never take money away when the endowment grows.

Setting

Let $U$ be a countable set of at least three potential competitors. A competition is a triple $(N, \mathcal R, E)$: a nonempty finite set $N \subseteq U$, a ranking $\mathcal R : N \to \{1, \dots, |N|\}$ (a bijection; $i$ is ranked above $j$ if $\mathcal R(i) < \mathcal R(j)$), and a prize endowment $E \ge 0$. For a nonempty $S \subseteq N$, the subranking $\mathcal R_S$ lists $S$ in the order of $\mathcal R$.

A prize allocation rule $\varphi$ assigns to every competition an allocation $\varphi(N, \mathcal R, E) \in \mathbb R^N_+$ with $\sum_{i \in N} \varphi_i(N, \mathcal R, E) = E$. Two basic rules are Equal Division, $\mathrm{ED}_i = E/|N|$, and Winner-Takes-All, $\mathrm{WTA}_i = E$ if $\mathcal R(i) = 1$ and $0$ otherwise.

The axioms of the main theorem are, for every competition and $i, j \in N$:

• order preservation: $\mathcal R(i) < \mathcal R(j) \Rightarrow \varphi_i(N, \mathcal R, E) \ge \varphi_j(N, \mathcal R, E)$;
• endowment monotonicity: $E < E' \Rightarrow \varphi_i(N, \mathcal R, E) \le \varphi_i(N, \mathcal R, E')$;
• consistency: for every nonempty $S \subseteq N$ and $i \in S$,

$$\varphi_i(N, \mathcal R, E) = \varphi_i\Big(S, \mathcal R_S, \sum_{j \in S} \varphi_j(N, \mathcal R, E)\Big).$$

Anonymity (prizes depend only on $|N|$, the position and $E$) and endowment continuity are auxiliary properties.

An interval rule is given by pairwise disjoint open intervals $(a_k, b_k)$, $k = 1, 2, \dots$, with $a_k \in \mathbb R_+$ and $b_k \in \mathbb R_+ \cup \{+\infty\}$. With $n = |N|$ and $r = \mathcal R(i)$,

$$\varphi_i(N, \mathcal R, E) = \begin{cases} a_k & \text{if } n a_k \le E \le (n - r + 1) a_k + (r - 1) b_k; \\ E - (n - r) a_k - (r - 1) b_k & \text{if } (n - r + 1) a_k + (r - 1) b_k \le E \le (n - r) a_k + r b_k; \\ b_k & \text{if } (n - r) a_k + r b_k \le E \le n b_k; \\ E / n & \text{otherwise.} \end{cases}$$

At endowment $n a_k$ everyone receives $a_k$; as $E$ grows, prizes are raised to $b_k$ one competitor at a time from the top; when $E/n$ lies in no $[a_k, b_k]$ the endowment is divided equally. ED has $a_k = b_k = 0$; WTA has $a_1 = 0$, $b_1 = +\infty$.

Formalization targets

Goal: Theorem 1 (p. 13)

$$\varphi \text{ satisfies order preservation, endowment monotonicity and consistency} \iff \varphi \text{ is an interval rule.}$$

Both directions are part of the goal.

Milestones, in the order the proof uses them

1. Lemma 1 (p. 10): endowment monotonicity implies endowment continuity.
2. Lemma 2 (p. 11): order preservation, endowment monotonicity and consistency imply anonymity.
3. Lemma 3 (p. 11): two endowment monotonic, consistent rules that agree on all two-competitor competitions agree on all competitions.
4. The "if" direction (p. 28): every interval rule satisfies the three axioms.
5. Step 1 (p. 28): for two competitors, if $\varphi(N, \mathcal R, x_1 + x_2) = (x_1, x_2)$ then $\varphi(N, \mathcal R, 2x_1) = (x_1, x_1)$ or $\varphi(N, \mathcal R, 2x_2) = (x_2, x_2)$.
6. Step 2 (p. 29): the two-competitor restriction has the interval form (9),

$$\varphi(N, \mathcal R, E) = (E - a_k, a_k) \text{ on } [2a_k, a_k + b_k], \quad (b_k, E - b_k) \text{ on } [a_k + b_k, 2b_k], \quad (E/2, E/2) \text{ otherwise.}$$

Further statements of §2.3

Lemma 4 (endowment additivity ⇔ scale invariance) and Corollaries 1–4, which single out WTA (winner-loser strict order preservation), ED (strict endowment monotonicity), the Winner-Takes-Surplus rules (winner strict endowment monotonicity) and the pair {ED, WTA} (additivity) inside the family of Theorem 1, are included as supporting theorems.

Significance

Theorem 1 replaces three qualitative requirements by an explicit, countably parametrized family. The family is broad (Equal Division, Winner-Takes-All, the "dollar at a time" rule of Example 1, and their concatenations along the endowment axis), so the theorem is the starting point for every sharper characterization in the paper: strengthening one axiom at a time selects WTA, ED or a Winner-Takes-Surplus rule (Corollaries 1–4), and the second and third missions of this series replace consistency by its local and top variants to obtain the single-parametric and parametric rules. Lemma 3 also isolates a general principle: a monotone consistent rule is determined by its behaviour on pairs.

On the formal side, Mathlib and the platform have no model of variable-population allocation with rankings. This mission provides one (competitions over a universe, subrankings, prize allocation rules and the consistency family of axioms) together with the first machine-checkable statement of a characterization theorem in this area. The paper's proofs are complete; nothing here is open mathematics, and none of it has been formalized before.

Difficulty

Consistency only constrains the rule across competitions; on its own it says nothing about how two competitors share a given endowment. The obvious plan, to read the intervals off the two-competitor allocation path and extend by Lemma 3, fails at the first step: an order preserving, monotone two-competitor path need not be a staircase of horizontal and vertical segments, and nothing about two competitors alone forces it to be. The staircase shape (Step 1) is a genuinely multi-competitor phenomenon that also relies on anonymity, which is not assumed and must be derived (Lemma 2, a six-case analysis over how two competitions share competitors). The countable family of intervals then has to be extracted from the path (Step 2), including endpoints at $+\infty$ and the gaps where the rule is equal division.

Formalization scope

A ranked set $(N, \mathcal R)$ is a duplicate-free nonempty List U, best first; $|N|$ is its length and $\mathcal R(i)$ = pos l i, the 1-based index. The subranking is the sublist of members of $S$. A rule is a function φ : List U → ℝ → U → ℝ; its values on non-rankings, negative endowments and non-members are irrelevant, and every axiom and the interval-rule definition quantify only over rankings, $E \ge 0$ and $i \in N$. The standing assumption on $U$ is carried as [Countable U] plus three distinct elements on every statement whose proof needs a third competitor (Lemma 2, Steps 1–2, Theorem 1, Corollaries 1–4); it is unnecessary for Lemmas 1, 3, 4 and for the "if" direction. Interval endpoints $b_k$ are extended reals (EReal), the intervals are indexed by $\mathbb N$ (finitely many intervals are padded with $a_k = b_k = 0$), $a_k \le b_k$, and disjointness is of the open intervals. The four cases are implications; "otherwise" means $E \notin [n a_k, n b_k]$ for every $k$.

The following formalizations would trivialize or change the theorem and are ruled out: a fixed competitor set or a finite $U$ of size two (consistency then has no reduced competitions to act on, and Corollary 1(i) fails); consistency restricted to two-element subsets or to some subsets only; a one-directional goal; interval rules without $+\infty$ endpoints (which excludes WTA and makes the "only if" direction false); and anonymity as an extra hypothesis.

The definitions are reusable by the two companion missions of this series (local and top consistency), which use the same model. Contributions welcome: proofs of the milestones, a general lemma that consistent monotone rules are determined by pairs, and proofs that ED, WTA and the Example 1 rule are interval rules.

Selected references

• B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science 69 (2023). https://arxiv.org/abs/2008.08985, https://doi.org/10.1287/mnsc.2022.4520
• R. J. Aumann and M. Maschler, Game theoretic analysis of a bankruptcy problem from the Talmud, Journal of Economic Theory 36 (1985), 195–213. https://doi.org/10.1016/0022-0531(85)90102-4
• W. Thomson, A study of choice correspondences in economies with a variable number of agents, Journal of Economic Theory 46 (1988), 237–254. https://doi.org/10.1016/0022-0531(88)90131-7
• T. Lensberg, Stability and the Nash solution, Journal of Economic Theory 45 (1988), 330–341. https://doi.org/10.1016/0022-0531(88)90274-8
• S. Hart and A. Mas-Colell, Potential, value, and consistency, Econometrica 57 (1989), 589–614. https://doi.org/10.2307/1911054

Why digital businesses choose how much data to keep and how well to guard it

Platforms that earn money from their users' activity make two linked decisions about the data that activity generates: how much of it to record and store, and how much to spend protecting what they store. Stored data lets a business tailor its services and sell data-driven products, but it also attracts adversaries (hackers, data brokers, unauthorized third parties) whose access harms users, who then use the service less. Fainmesser, Galeotti and Momot, Digital Privacy (Management Science 69(6), 2023, doi:10.1287/mnsc.2022.4513; author manuscript SSRN 3459274), build a tractable model of this trade-off and solve it in closed form. Their first main result, Theorem 1, gives the profit-maximizing data strategy explicitly and shows that a business whose revenue depends more on data both collects more and protects more. The result is the basis for the paper's policy analysis (data protection standards, Pigouvian taxes on stored data) and for its comparison with the social optimum, which is the subject of a companion mission.

Setting

A unit mass of identical users each choose an activity level $a \ge 0$. The business stores a fraction $\xi \in [0,1]$ of every user's activity and protects it at level $C \ge 0$, at cost $\psi C$. With average activity $\bar a$ and a mass $\omega$ of active adversaries, a user's utility is (display (1))

$$U(a, \bar a) = a - \tfrac12 a^2 + \beta a\bar a + (\rho - \omega) a\xi ,$$

where $\beta \in [0,1)$ measures network effects and $\rho \in [0,1)$ the users' benefit from tailored services built on stored data. Adversaries have access costs $\gamma C$ with $\gamma$ uniform on $[0, M]$ and gain $\bar a\xi$; letting $M \to \infty$, the mass of active adversaries is $\omega = \xi\bar a/C$. Proposition 1 shows that for every data strategy $(\xi, C)$ with $C > 0$ this users–adversaries subgame has a unique equilibrium,

$$\bar a^*(\xi, C) = \frac{C(1+\rho\xi)}{C(1-\beta)+\xi^2}, \qquad \omega^*(\xi, C) = \frac{\xi\bar a^*(\xi, C)}{C},$$

with consumer surplus $\mathrm{CS}(\xi, C) = \tfrac12\bar a^*(\xi, C)^2$; when nothing is stored, $\bar a^*(0, C) = 1/(1-\beta)$. The business's profit is (display (2))

$$\Pi(\xi, C) = (1-P)\,\bar a^*(\xi, C) + P\,\xi\bar a^*(\xi, C) - \psi C ,$$

where the revenue model $P \in [0,1]$ is the share of revenue that is data-driven: $P = 0$ is a purely usage-driven business, $P = 1$ a purely data-driven one. A business optimum is a strategy $(\xi, C) \in [0,1] \times [0,\infty)$ that maximizes $\Pi$ over $[0,1] \times [0,\infty)$.

The Lean development uses the same names: abar, omegaStar, CS, profit, Feasible, IsBusinessOpt, the best-response quantities Ch ($C_h$), kappa ($\kappa$), Cl ($C_l$), xiBR, the threshold psiL ($\psi_L$), the interior root xiI ($\xi_i$), and the closed forms xiStar ($\xi^\star$) and CStar ($C^\star$).

Formalization targets

Goal: Theorem 1

For fixed $0 \le \beta < 1$, $0 < \rho < 1$, $\psi > 0$ and every $P \in (0,1]$, let

$$\xi^\star = \max\Big\{0, \min\Big\{1, \frac{1}{2P\rho}\Big(-(1-P)\rho - P + |P-(1-P)\rho|\sqrt{\frac{\psi}{\max\{0,\psi-P\rho\}}}\Big)\Big\}\Big\},$$ $$C^\star = \frac{\xi^\star}{1-\beta}\Big(-\xi^\star + \sqrt{\tfrac1\psi(1+\rho\xi^\star)(1-P(1-\xi^\star))}\Big).$$

Then $(\xi^\star, C^\star)$ is a business optimum, and both $P \mapsto \xi^\star$ and $P \mapsto C^\star$ are weakly increasing on $(0,1]$.

Milestones

1. Proposition 1 (p. 10): the subgame equilibrium (3) is unique, and consumer surplus is (4).
2. Proposition 1 (a)–(b) with footnote 15: $\bar a^*$ and $\xi\bar a^*$ increase in $C$, and are single-peaked in $\xi$.
3. Lemma 1 (p. 29): for fixed $\xi$, the unique optimal protection is $\max\{C_h(\xi), 0\}$.
4. Lemma 2 (p. 29): for fixed $C > 0$, the unique optimal collection is $-\kappa(C) + \sqrt{\kappa(C)^2 + C(1-\beta)}$ if $C < C_l$ and $1$ if $C > C_l$.
5. App. A.2 summary (p. 31): with $P\rho \le \psi_L \le \psi_H$, the business optimum is $(1, C_h(1))$ for $\psi \le \psi_L$, $(\xi_i, C_h(\xi_i))$ with $\xi_i \in (0,1)$ for $\psi_L < \psi < \psi_H$, and $(0,0)$ for $\psi \ge \psi_H$.

Significance

Theorem 1 is the statement that a business's revenue model alone orders its data practices: holding users and costs fixed, moving toward data-driven revenue never lowers collection and never lowers protection. The paper uses it to explain why consumer surplus is maximized at an intermediate revenue model $P = \rho/(1+\rho)$ (Proposition 2), and as the benchmark against which it evaluates regulation in §6. The closed form also makes the regime structure explicit: no collection when protection is expensive, full collection when it is cheap, and an interior solution in between.

The result is proved in the paper (App. A.2–A.3, with the proofs of Lemmas 1–2 in Online App. B), but parts of that proof are informal: several steps are "easy to check" or "can be derived similarly", one case is treated and the other left to the reader, and the second-order conditions are referred to a general lemma in Online App. C.5. No machine-checked version exists. A formal proof certifies the closed form, including its boundary cases, which the printed formula handles through an infinite square root.

Difficulty

The profit is not jointly concave, so first-order conditions do not settle the problem. The argument intersects the two best responses (Lemmas 1–2), and two candidate strategies survive in the intermediate regime: $(0,0)$ and the interior point. Choosing between them requires comparing profits across all $\psi$ and showing the comparison flips exactly at $\psi_H$. Monotonicity in $P$ is harder still: as $P$ moves, so do both thresholds $\psi_L(P)$ and $\psi_H(P)$, so a fixed $\psi$ can cross from one regime to another, and $\xi^\star$ and $C^\star$ must be shown monotone within each regime and across the switches. Within the interior regime $C^\star = C_h(\xi^\star)$ depends on $P$ both directly and through $\xi^\star$, so differentiating the closed form does not by itself give the sign.

Formalization scope

All parameters are explicit real numbers; every optimum is taken over $\xi \in [0,1]$, $C \ge 0$, never over $\mathbb R^2$. The page's ranges are $0 \le \beta < 1$, $0 \le \rho < 1$, $\psi \ge 0$, $0 \le P \le 1$. The following are added and disclosed in each item: $\psi > 0$ everywhere (otherwise $C_h$ and (6) divide by zero and no maximizer exists); $P > 0$ and $\rho > 0$ in Theorem 1 and the App. A.2 summary (formula (5) divides by $2P\rho$); $C > 0$ in Proposition 1 and Lemma 2 (the adversary mass $\xi\bar a/C$); $\rho > 0$ in Lemma 2.

Three conventions are fixed. First, $\bar a^*(0, C) = 1/(1-\beta)$ for every $C$, the paper's value at $(0,0)$ where (3) is $0/0$. Second, $\xi^\star = 1$ whenever $\psi \le P\rho$, the page's own reading of the infinite square root in (5). Third, $\psi \ge \psi_H$ is written as $(P+(1-P)\rho)^2 \le 4(1-P)\psi$, so that $\psi_H = +\infty$ at $P = 1$. Using Lean's $0/0 = 0$ at either of the first two places makes Theorem 1 false, not trivial, and is ruled out by these definitions. Theorem 1 asserts that $(\xi^\star, C^\star)$ is a maximizer: uniqueness fails at $P = \rho/(1+\rho)$, $\psi = \rho^2/(1+\rho)$. Monotonicity is MonotoneOn on $(0,1]$ with $\beta, \rho, \psi$ fixed; a Monotone statement with junk values outside $(0,1]$ would not be the paper's claim.

A complete development needs only real analysis from Mathlib: one-variable calculus for the best responses, square-root and absolute-value manipulations for the closed form, and a profit comparison across regimes. The best-response lemmas are reusable for the companion mission on the social optimum. Contributions of proofs of any milestone, and of auxiliary lemmas such as $C^\star = C_h(\xi^\star)$, are welcome.

Selected references

• I. P. Fainmesser, A. Galeotti, R. Momot, Digital Privacy, Management Science 69(6):3157–3173, 2023. doi:10.1287/mnsc.2022.4513; author manuscript (This Draft: April 2022), SSRN 3459274.
• E. L. Glaeser, J. A. Scheinkman, Non-Market Interactions, NBER Working Paper 8053, 2000 (existence and uniqueness of the users' response, used in App. A.1). doi:10.3386/w8053

Motivation

A secretary problem asks a decision maker to choose one candidate from a sequence, without being able to recall a rejected candidate. Each arrival reveals how the candidate compares with those seen earlier, but the decision maker does not know the candidate's final rank. A classifier can provide an additional Yes or No signal about whether the current candidate is the best overall. The natural performance question is how much this signal improves the chance of selecting the best candidate when the number of arrivals grows. Dütting, Lattanzi, Paes Leme and Vassilvitskii give an exact finite linear program for this setting and an explicit asymptotic value. This mission makes the limit and its finite prerequisites precise.

The classifier's quality has two parameters with different meanings. Recall $p$ is the probability of a Yes signal for the top candidate. Specificity $p'$ is the probability of a No signal for any other candidate. Both lie in $[1/2,1]$, as in Example 5 of the paper. At $p=p'=1/2$ the signal conveys no information, while $p=p'=1$ is perfect advice. These endpoints matter to the statement rather than being omitted as special cases. Example 5, pp. 7–8.

Setting

There are $n\ge1$ arrivals, indexed by $i=1,\ldots,n$. Their ranks form a uniformly random permutation; the maximum rank is the candidate to select. At each arrival, the observer sees the relative ranking of candidates already seen and a signal $s\in\{Y,N\}$ from the classifier. An admissible decision can depend on this observed history and may use a stopping probability. It cannot inspect a candidate's hidden final rank. The paper shows that, for this signal model, the optimal stopping probability is characterized by a finite primal linear program. Sections 2 and 6.

For each round and signal, $z_i^s\in[0,1]$ is a primal variable. Put $\bar z_j=(1-p')z_j^Y+p'z_j^N$. The program has constraints $z_i^s\le1-\sum_{j<i}\bar z_j/j$, and its objective is $\sum_{i=1}^n[pz_i^Y+(1-p)z_i^N]/n$. Write $\operatorname{Opt}(n,p,p')$ for its optimal value. The constraints account for the chance that an earlier candidate has already been selected; the objective weights winning selections by the signal probabilities of the top candidate. This is the $\operatorname{Opt}$ of Section 6, rather than a value defined by an asymptotic formula. Section 6, p. 20.

The paper also considers a rescaled dual with variables $w_i^Y,w_i^N$ and an associated pair of thresholds $t_Y,t_N$. The thresholds are the first rounds at which the corresponding greedy dual coordinate is positive. In the finite formalization, $n+1$ records a signal whose coordinate is never positive. Proof of Theorem 20, p. 21.

Formalization targets

The main target is the limiting primal optimum for every $p,p'\in[1/2,1]$:

$$\lim_{n\to\infty}\operatorname{Opt}(n,p,p') =\left(\frac{1-p'}p\right)^{(1-p')/p'} \exp\left(\frac{p-1}{p'}\right).$$

The finite milestones identify the primal optimum with the greedy dual objective, give the exact late dual coordinates and the exact range of the early $Y$ recursion, and establish $t_Y\le t_N$. The asymptotic milestones state

$$\frac{t_N}{n}\longrightarrow \exp\left(\frac{p-1}{p'}\right),\qquad \frac{t_Y}{n}\longrightarrow \left(\frac{1-p'}p\right)^{1/p'}\exp\left(\frac{p-1}{p'}\right).$$

A separate companion target gives the finite lower bound $\operatorname{Opt}(n,p,p')\ge L(p,p')$, where $L$ denotes the displayed limit. Theorem 20 states the corresponding infimum inequality but does not separately prove it. Theorem 20 and its proof, pp. 20–22.

Significance

The limit quantifies the benefit of advice across the whole parameter square, including asymmetric classifiers. It recovers the classical value $e^{-1}$ when $p=p'=1/2$, and gives value $1$ for perfect advice. The two threshold limits say when each signal begins to justify stopping as the horizon grows. Thus the result specifies both the achievable success probability and the scale of the optimal decisions. Theorem 20, p. 20.

The paper already proves threshold optimality through its linear program and presents the limit calculation. The formalization work here is to establish a full Lean limit theorem from an exact finite LP, including the two endpoint regimes and a finite dual characterization. The nearby classical secretary threshold limit on Prove2Me uses a different rank-based model; it does not state this classifier result. Definitions of the primal feasible set and the backward dual sequence can support later results about other advice distributions.

Difficulty

The source uses approximations throughout its asymptotic argument and explicitly omits terms that vanish as $n$ grows. Those omissions cannot be carried into an exact finite statement: the $Y$ recursion, for example, fails at the round immediately before the $N$ threshold because the next $N$ dual coordinate is then present. A complete argument has to keep the discrete threshold boundaries and the harmonic sums under control while passing to a limit. The source's displayed theorem also contains an exponent inconsistent with the last equation of its proof; the corrected expression must be checked uniformly, including zero base at $p'=1$. Proof of Theorem 20, pp. 21–22.

Formalization scope

Lean represents time by natural numbers $1,\ldots,n$, matching the paper's displayed LP, and signals by Bool, with true meaning $Y$. The primal optimum is the real supremum of objective values over exactly the feasible LP variables. For $n\ge1$ and $p,p'\in[1/2,1]$, the zero assignment is feasible and the objective is bounded, so this supremum has its ordinary optimization meaning. Values of a variable array outside $1,\ldots,n$ are ignored. The greedy dual is a backward finite recursion, not the definition of $\operatorname{Opt}$; otherwise the central LP-to-dual milestone would disappear.

The formal thresholds are first positive greedy dual coordinates. If there is no positive $N$ coordinate, $t_N=n+1$; this occurs when $p=1$ and has the same normalized limit as the paper's informal $t_N=n$ convention at perfect advice. Real powers use Lean's $0^0=1$, yielding the correct $p'=1$ endpoint. All theorems quantify explicitly over $n\ge1$ where finite rounds are used, and over $p,p'\in[1/2,1]$. The limit uses Filter.Tendsto at infinity. The chapter does not formalize the algorithmic running time, Figures 3 and 7, or the policy-level threshold optimality addressed by the series' preceding mission. Contributions to finite LP duality, harmonic asymptotics, and endpoint analysis are within scope. Sections 6 and Appendix C.

Selected references

• Paul Dütting, Silvio Lattanzi, Renato Paes Leme and Sergei Vassilvitskii, Secretaries with Advice, arXiv:2011.06726v1, 2020; published in Mathematics of Operations Research, 2024. Preprint.

Motivation

In the secretary problem $n$ candidates arrive one at a time in uniformly random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones and must accept or reject irrevocably, aiming to accept the best candidate overall. Dütting, Lattanzi, Paes Leme and Vassilvitskii, Secretaries with Advice (arXiv:2011.06726), study a family of variants in which each candidate also carries a signal about its quality, and show that for many of them the optimal stopping rule is the solution of a finite factor-revealing linear program whose dual can be solved greedily by backward induction.

One of their main examples is the secretary problem with samples: before the $n$ candidates arrive, $k$ further elements of the same random order are revealed as a sample, and a candidate's signal is the number of sample elements smaller than it. This model interpolates between the classical problem ($k=0$, optimal success probability tending to $1/e$) and, as $k\to\infty$, the full-information problem of Gilbert and Mosteller (1966). The paper's Theorem 17 gives the optimal dual solution of this LP in closed form.

Setting

Fix natural numbers $n\ge 1$ (secretaries) and $k\ge 0$ (samples). Rounds are $i=1,\dots,n$; signals are $s\in\{0,1,\dots,k\}$. The dual LP of §5 has the coefficients

$$a(i,s)=\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{s+t}{k+t+1},\qquad c(j,s',i,s)=\frac{1}{s'+1}\prod_{t=1}^{i-1}\frac{s+t}{s'+t+1}\ \ (s'\ge s),$$

with $c(j,s',i,s)=0$ for $s'<s$, and reads

$$\min\sum_{i}\sum_{s}u(i,s)\quad\text{s.t.}\quad u(i,s)+\sum_{j>i}\sum_{s'\ge s}u(j,s')\,c(j,s',i,s)\ge a(i,s),\quad u(i,s)\ge 0 .$$

The greedy solution (equation (8) of the paper) sets $u(n,s)=a(n,s)$ and, going backwards,

$$u(i,s)=\max\Bigl\{0,\ a(i,s)-\sum_{j>i}\sum_{s'}u(j,s')\,c(j,s',i,s)\Bigr\}\qquad(i<n).$$

The un-clipped recursion $v(i,s)$ is the same backward induction with the $\max\{0,\cdot\}$ removed. In Lean, the generic recursion (8) is greedyDual (and unclippedDual) over an arbitrary finite signal type, and the samples instance is samplesGreedy n k i s (resp. samplesUnclipped) with s : Fin (k + 1). Products $\prod_{t=a}^{b}$ with $b<a$ equal $1$.

Formalization targets

Goal: Theorem 17

For every $1\le i\le n$ and $0\le s\le k$: $u(n,s)=a(n,s)$, and for $i<n$

$$u(i,s)=\max\left\{0,\frac{1}{k+1}\prod_{t=1}^{i-1}\frac{s+t}{k+t+1}\left(\prod_{t=i}^{n-1}\frac{s+t}{k+t+1}-\frac{\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{\ell=1}^{n-i-j}(s+i-1+\ell)}{\prod_{t=i}^{n-1}(k+t+1)}\right)\right\}.$$

Milestones (the steps of the paper's proof)

1. Reduction (p. 17): if $v(i',\cdot)$ has the closed form for all $i'>i$, then $v(i,s)=a(n,s)-\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{1}{k+t+1}\prod_{t=1}^{i-1}(s+t)\sum_{s'=s}^{k}T(i,s')$, with $T(i,s')$ an explicit double sum.
2. Two forms of $T$ (pp. 17–18): the double sum collapses to $\sum_{j=1}^{n-i-1}(n-i)\binom{n-i-1}{j}\frac{1}{j(j+1)}\prod_{\ell\le j}(k-s'+\ell)\prod_{t=i+1}^{n-j-1}(s'+t)$.
3. Key identity (p. 18): $\sum_{s'=s}^{k}T(i,s')=\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{t=i}^{n-j-1}(s+t)$.
4. Base case $s=k$ (p. 18) and 5. inductive step $s+1\to s$ (Appendix B, pp. 26–28) of the key identity.
5. Un-clipped closed form (pp. 17–19): $v(i,s)$ equals the expression inside the max, for all $1\le i\le n$.

Significance

Theorem 16 of the paper shows that the greedy dual solution is optimal and that the optimal policy for secretaries with samples is a threshold policy in the signal: accept a best-so-far candidate in round $i$ iff its signal is large enough. Theorem 17 makes this solution explicit, so the optimal thresholds can be read off from the sign of a closed-form expression rather than computed by running the backward recursion, and it is the discrete precursor of the paper's Corollary 18, which recovers the Gilbert–Mosteller full-information thresholds in the limit $k\to\infty$.

The identities are proved in the paper by explicit manipulation of finite sums and products of binomials. No machine-checked version exists. A formal proof checks the long index computations of the proof and of Appendix B, and closes a gap: the paper proves the identity for the un-clipped recursion only ("for the proof we can ignore the $\max\{0,\cdot\}$") and does not argue why the clipped greedy solution has the same form. The goal as stated here, with the maximum, is the statement the paper asserts.

Difficulty

The identities are rational-function identities in $s$, $k$ and the round indices, with sums whose ranges depend on the summation variables and products whose ranges may be empty. The natural first idea, induction on $n-i$ directly on the formula, requires the key identity for $\sum_{s'=s}^{k}T(i,s')$, a double sum over $s'$ and $j$ of products of rising factorials; the paper handles it by a second backward induction over $s$, and both the base case and the step re-index sums with shifted bounds and boundary terms such as $(n-i-1)!$ and $\frac{1}{n-i}\prod_{\ell=1}^{n-i}(k-s+\ell)$.

The passage from the un-clipped to the clipped recursion is a separate difficulty: once $u(j,s')$ is clipped to $0$ at a later round, the sums used at earlier rounds differ from those of the un-clipped recursion, and the closed form survives only because the clipped entries do not affect the relevant sums. That argument is not in the paper.

Formalization scope

• Rounds are natural numbers $1\le i\le n$ (1-based, as printed); signals are Fin (k + 1) in the recursion and naturals $s\le k$ in the formulas. All arithmetic is in $\mathbb R$; naturals are cast before $k-s$, and the natural differences $n-i$, $n-i-j$, $n-j-1$ appear only where the ranges keep them non-truncated.
• Products and sums are over Finset.Icc a b, empty when $b<a$, matching the paper's convention.
• The recursion is defined by well-founded recursion on $n-i$ and sums over all later rounds $j\in\{i+1,\dots,n\}$ and all signals; $c=0$ for $s'<s$ encodes the paper's $\sum_{s'\ge s}$.
• The goal keeps the $\max\{0,\cdot\}$. Stating instead the identity for the un-clipped recursion would be a different (weaker-content) theorem; it is milestone 6.
• No probability model appears: the coefficients are taken as given by their formulas on p. 15. Their probabilistic derivation, the optimality of the greedy solution (Theorem 16), the running time of the LP algorithm, the "natural interpretation" paragraph, Corollary 18 and the plots are out of scope.
• The generic recursion greedyDual is reusable for any instance of the paper's factor-revealing LP (the binary-classifier model of §6 included). General lemmas about sums of rising factorials (ascPochhammer) and binomial re-indexing developed for the milestones are welcome contributions.

Selected references

• P. Dütting, S. Lattanzi, R. Paes Leme, S. Vassilvitskii, Secretaries with Advice, arXiv:2011.06726v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2011.06726
• J. P. Gilbert, F. Mosteller, Recognizing the Maximum of a Sequence, Journal of the American Statistical Association 61(313), 1966. https://doi.org/10.1080/01621459.1966.10502008
• T. S. Ferguson, Who Solved the Secretary Problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493