Operations Research

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

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

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

Regret bounds for reinforcement learning in a single, non-episodic Markov decision process (MDP) are stated in terms of the diameter $D$ of the MDP: the worst expected time needed to travel between two states when the travel policy is chosen well. UCRL2 (Jaksch, Ortner and Auer, 2010) achieves regret $\tilde O(DS\sqrt{AT})$, against a lower bound of $\Omega(\sqrt{DSAT})$, by planning in an extended MDP, whose action set lets the planner also pick a transition law from a confidence set. Posterior-sampling methods replace the confidence set with random samples from a posterior. Agrawal and Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023) show that such a method attains a high-probability worst-case regret bound of $\tilde O(DS\sqrt{AT})$ for every communicating MDP (their Theorem 1).

Their analysis plans in an extended MDP built from finitely many sampled transition vectors. Optimal-gain policies of that MDP are only useful if it is itself communicating with a diameter comparable to $D$, so the paper needs a deterministic statement: if every state-action pair has a sample that is optimistic about travel times, the diameter of the extended MDP is at most $D/(1-\delta)$. This mission formalizes that statement, Lemma 5.6 of the paper (p. 12), together with three claims from its proof.

Setting

A finite MDP $\mathcal M$ has a finite state set $\mathcal S$ of size $S$, a finite action set $\mathcal A$ of size $A$, a probability vector $P_{s,a}\in\Delta^{S}$ for each state $s$ and action $a$, and rewards $r_{s,a}\in[0,1]$. A deterministic policy is a map $\pi:\mathcal S\to\mathcal A$; under $\pi$ the state process is the Markov chain with transition rows $P_{s,\pi(s)}$.

For states $s'$ and $s$, $T^{\pi}_{s'\to s}\in[0,\infty]$ is the expected number of steps to reach $s$ when starting at $s'$ and following $\pi$. It is $0$ when $s'=s$. The diameter is

$$D(\mathcal M)=\max_{s\neq s'}\ \min_{\pi:\mathcal S\to\mathcal A} T^{\pi}_{s\to s'},$$

and $\mathcal M$ is communicating when $D(\mathcal M)<\infty$ (Definitions 1–3, p. 3). For a target $s$, the vector $E^{s}$ collects the minimum expected times, $E^{s}_{s'}=\min_{\pi}T^{\pi}_{s'\to s}$, so $E^{s}_{s}=0$.

The extended MDP (§3, p. 5) starts from $\psi$ probability vectors $Q^{1}_{s,a},\dots,Q^{\psi}_{s,a}$ for every pair $(s,a)$. In the algorithm these are posterior samples, but here they are arbitrary. The extended MDP $\tilde{\mathcal M}$ has the same states and, for every action $a$, the actions $a^{1},\dots,a^{\psi}$. Taking $a^{j}$ in $s$ gives reward $r_{s,a}$, and the next state is drawn from $Q^{j}_{s,a}$. Its diameter $D(\tilde{\mathcal M})$ is defined as above, minimizing over policies $\tilde\pi:\mathcal S\to\{a^{j}\}$.

Formalization targets

Goal: Lemma 5.6

Let $\delta\in[0,1)$. Suppose that for every target state $s$, every state $s'$ and every action $a$ there is a sample index $j$ with

$$Q^{j}_{s',a}\cdot E^{s}\ \le\ P_{s',a}\cdot E^{s}+\delta. \tag{16}$$

Then

$$D(\tilde{\mathcal M})\ \le\ \frac{D(\mathcal M)}{1-\delta}.$$

Milestones (claims of the proof, p. 13)

1. In a communicating MDP with at least one action, for every target $s_2$ there is one deterministic policy $\pi$ with $T^{\pi}_{s'\to s_2}=E^{s_2}_{s'}$ for every $s'$.
2. First-step analysis: for every policy $\pi$ and $s\neq s_2$,

$$T^{\pi}_{s\to s_2}=1+\sum_{s'\neq s_2}P_{s,\pi(s)}(s')\,T^{\pi}_{s'\to s_2}.$$

3. Comparison (display (17)): if $E\in[0,\infty]^{\mathcal S}$ satisfies $1+\sum_{s'\neq s_2}Q_{s,\tilde\pi(s)}(s')E_{s'}\le E_s+\delta$ for all $s\neq s_2$, then $(1-\delta)\,T^{\tilde\pi}_{s\to s_2}\le E_s$ for all $s\neq s_2$.

Significance

The result. Lemma 5.6 turns a per-pair, one-sided condition on samples into a global bound on the diameter. Agrawal and Jia combine it with their Lemma 5.7, which shows that (16) holds with $\delta\le 1/2$ with high probability for their posterior samples. Together these give $D(\tilde{\mathcal M}^{k})\le 2D$ in every epoch, which is what lets the bias span of the sampled MDP enter their regret analysis. The lemma is deterministic and makes no use of how the samples were drawn, so it applies to any optimistic-sampling or perturbation scheme that produces vectors satisfying (16).

Formalizing it. The lemma is proved in the paper; no machine-checked version exists. The paper's proof assumes that every sampled entry is strictly positive ("drawn from Dirichlet distribution") so that the absorbing chain and its fundamental matrix are well defined. That assumption fails for the simple optimistic samples of the same algorithm, which can have zero entries. The statements here drop it, so a formal proof also settles the general case. Milestones 1 and 2 are standard facts about minimum expected hitting times (stochastic shortest paths) that the platform's finite-MDP library does not yet contain. They are reusable for any diameter-based regret analysis.

The main regret bound (Theorem 1) is not posed. Its constants are hidden in $O(\cdot)$, and the algorithm's parameters are given only up to $\Theta(\cdot)$.

Difficulty

The paper's argument inverts $I-Q^{\dagger}_{\tilde\pi}$ and uses the nonnegativity of the fundamental matrix of an absorbing chain. Without positive entries the policy $\tilde\pi$ can have closed classes that avoid the target, so $I-Q^{\dagger}_{\tilde\pi}$ can be singular and the matrix argument does not apply as written. The comparison has to be made with expected travel times that may be infinite.

A second obstacle is that (16) constrains only the minimizing vectors $E^{s}$ of the true MDP. The bound therefore needs a policy of $\mathcal M$ whose travel times equal $E^{s_2}$ from every state at once, not merely from the starting state $s_1$. The existence of such a uniformly optimal deterministic policy is not immediate from the definition of the diameter, which minimizes separately for each pair of states.

Finally, the platform's expected travel time is defined through finite-horizon trajectory laws, so first-step analysis is a Markov-property computation on those measures. It does not follow from the definition by unfolding alone.

Formalization scope

• Library. The mission reuses the published definitions FiniteMDPLearning (namespace BanditAlgorithm): FiniteMDP S A, mdpTravelTime M f src tgt (the expected hitting time minus one, valued in $[0,\infty]$, equal to $T^{f}_{src\to tgt}$), and mdpDiameterENN M (Definition 2 verbatim, valued in $[0,\infty]$). The mission's own definitions file adds extendedMDP, extendedAction and minTravel (the vector $E^{s}$).
• Indexing. States, actions and samples are 0-based (Fin S, Fin A, Fin ψ). The action $a^{j}$ of the extended MDP is finProdFinEquiv (a, j) : Fin (A * ψ). The epoch index $k$ plays no role and is dropped.
• Extended values. Travel times, diameters, the vectors $E^{s}$ and the inner products $Q\cdot E^{s}$ are computed in $[0,\infty]$ with $0\cdot\infty=0$. The bound $D/(1-\delta)$ is division in $[0,\infty]$ by the positive real $1-\delta$, with $\delta\in[0,1)$ as δ : ℝ≥0, δ < 1.
• Quantifiers of (16). The printed (16) uses the letter $s$ both for the target of $E^{s}$ and for the state in $P_{s,a}$. The proof applies it at the current state with a different target, so the goal quantifies the target separately: for every target, state and action there is a sample.
• Pinned hypotheses. Milestone 1 assumes $D(\mathcal M)<\infty$ (the paper's "$\mathcal M$ has diameter $D$") and $A\ge1$. The goal assumes neither: if $D(\mathcal M)=\infty$ its bound is trivially true, so it generalizes the paper's statement. No statement assumes positivity of the sampled entries or any distribution of the samples.
• Ruled-out trivializations. An extended MDP whose transitions ignore $j$ or $Q$, an $E^{s}$ that is not the infimum over policies, a hypothesis comparing $Q$ and $P$ against different vectors, and a real-valued conclusion through a truncation with junk value $0$ for non-communicating MDPs would each make the goal vacuous or different. None is used.
• Useful existing result. The platform has the proved drift criterion BanditAlgorithm.mdp_travel_time_le_of_lyapunov_drift (a real-valued nonnegative $V$ with $\sum_{s'}P_{s,f(s)}(s')V(s')+1\le V(s)$ off the target bounds the travel time by $V$), which covers the case $\delta=0$ of milestone 3 for finite $E$.
• Welcome contributions. Proofs of the three milestones and of the goal; a general first-step (Markov property) lemma for mdpMeasure; an existence theorem for uniformly optimal deterministic policies of minimum expected hitting time.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic posterior sampling for reinforcement learning: worst-case regret bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• D. P. Bertsekas and J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Mathematics of Operations Research 16(3), 1991. https://doi.org/10.1287/moor.16.3.580
• C. M. Grinstead and J. L. Snell, Introduction to Probability, American Mathematical Society, 2nd revised edition, 1997 (Chapter 11, absorbing Markov chains). https://math.dartmouth.edu/~prob/prob/prob.pdf
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (Chapter 38, MDPs and the diameter). https://tor-lattimore.com/downloads/book/book.pdf

Why blockchain adoption in supply chains is an economic question

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

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

The supply chain

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

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

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

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

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

Formalization targets

Goal: Proposition 4.8 (p. 19)

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

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

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

Milestones

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

What the result gives

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

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

Where the difficulty lies

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

Formalization scope

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

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

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

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

Selected references

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