All missions

Motivation

Classical mechanism design assumes that agents are perfect optimizers: a mechanism is incentive compatible if no buyer gains anything, however small, by misreporting. In practice buyers face cognitive and computational costs, and a buyer may not bother to deviate for a gain below some threshold $\varepsilon$. Balseiro, Besbes and Castro, Mechanism Design under Approximate Incentive Compatibility (arXiv:2103.03403v2, 2022; Operations Research, 2024), ask how much additional revenue a seller can extract when the incentive constraints only need to hold up to $\varepsilon$.

A known benchmark answers this at order $\sqrt\varepsilon$. It comes from a rounding argument attributed to Noam Nisan, used in mechanism design to transform an approximately incentive compatible mechanism into an exactly incentive compatible one (see e.g. Balcan, Blum, Hartline and Mansour, FOCS 2005). The paper states this benchmark as its Proposition 1 and proves it in its online appendix "for completeness". This mission formalizes that benchmark; the paper's sharper, instance-dependent rates are the subject of the other missions of this series.

Setting

A seller sells a single item to one buyer. The buyer's value $v$ is drawn from a distribution $F$ with a density $f\ge 0$ supported in $S=[0,\bar v]$, $\bar v>0$, with $\int_0^{\bar v} f=1$.

A direct mechanism $m=(x,t)$ assigns to each reported value $v\in S$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$ (payments may be negative). Given $\varepsilon\ge 0$, the mechanism is

• individually rational (IR) if $v\cdot x(v)-t(v)\ge 0$ for all $v\in S$;
• $\varepsilon$-incentive compatible (IC$_\varepsilon$) if $v\cdot x(v)-t(v)\ge v\cdot x(v')-t(v')-\varepsilon$ for all $v,v'\in S$.

$\mathcal M(\varepsilon)$ denotes the set of mechanisms satisfying IR and IC$_\varepsilon$ (problem $(\mathcal P_\varepsilon)$ of the paper). For $\varepsilon=0$ this is the classical feasible set, and $\mathcal M(0)\subset\mathcal M(\varepsilon)$. The revenue of $m$ is $\Pi(m)=\mathbb E_v[t(v)]=\int_0^{\bar v}t(v)f(v)\,dv$, and the optimal revenue under $\varepsilon$-IC is

$$\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m).$$

The quantity of interest is the revenue gain $\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))$.

In the Lean development the model is ApproxIC.Rounding.Model (fields vbar, f) with the predicate Model.Standing; mechanisms are Mech (fields x, t); the sets and values are Mset M ε, revenue M m and optRev M ε.

Formalization targets

Goal: Proposition 1 (p. 15)

$$\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))=\mathcal O(\varepsilon^{1/2}),$$

in the paper's notation (p. 13): there are $C>0$ and $\varepsilon_0>0$, which may depend on the distribution, such that for every $\varepsilon\in(0,\varepsilon_0]$ and every $m\in\mathcal M(\varepsilon)$,

$$\Pi(m)-\Pi^\star(\mathcal M(0))\le C\sqrt\varepsilon .$$

Milestones (Appendix A, proof of Proposition 1, p. 38)

Fix $m=(x,t)\in\mathcal M(\varepsilon)$ and $\delta\in(0,1)$, and let $v^\star_\delta(v)\in\arg\max_{w\in S}\{v\cdot x(w)-(1-\delta)t(w)\}$.

1. The rounded mechanism $\tilde m=(x(v^\star_\delta(\cdot)),(1-\delta)t(v^\star_\delta(\cdot)))$ lies in $\mathcal M(0)$.
2. For $v'=v^\star_\delta(v)$: $t(v')\ge t(v)-\varepsilon/\delta$.
3. The non-asymptotic bound

$$\Pi(m)-\Pi^\star(\mathcal M(0))\le\frac{\delta}{1-\delta}\Pi^\star(\mathcal M(0))+\frac{\varepsilon}{\delta}\le 2\delta\,\Pi^\star(\mathcal M(0))+\frac{\varepsilon}{\delta}\qquad(\delta\le 1/2).$$

Significance

The result. Proposition 1 gives a distribution-free shape for the value of relaxing incentive compatibility: an $\varepsilon$-optimizing buyer can be exploited for at most order $\sqrt\varepsilon$ extra revenue. It is the starting point against which the paper measures its main contributions: an instance-dependent upper bound of order $\tilde{\mathcal O}(\varepsilon^{\alpha/(2\alpha-1)})$ (Theorem 1) and a matching lower bound (Theorem 3) for distributions whose revenue curve has local $\alpha$-power envelopes around the optimal price, and the $\Theta(\varepsilon)$ rate for deterministic mechanisms (Theorem 2). Since $\alpha/(2\alpha-1)>1/2$ for every $\alpha>1$, these show that the $\sqrt\varepsilon$ benchmark is not tight for such distributions. The rounding step itself (milestone 1) is the standard device for converting approximately incentive compatible mechanisms into exactly incentive compatible ones, and is reused across mechanism design.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal single-buyer model with $\varepsilon$-IC mechanisms that the other missions of the series share, and a formal version of Nisan's rounding argument for a continuum of types.

Difficulty

The paper's proof is short, but it is written for an argmax that is attained and a rounded mechanism that is tacitly measurable. In a formal treatment, the selection $v^\star_\delta$ must be chosen so that $\tilde m$ is measurable and its expected payment is defined. Exact incentive compatibility forces $\tilde x$ to be nondecreasing on $S$, and that monotonicity has to be established and then turned into measurability. The revenue comparison $\mathbb E_v[\tilde t(v)]\ge(1-\delta)(\mathbb E_v[t(v)]-\varepsilon/\delta)$ needs the integrability of $t\cdot f$, which comes from IR and IC$_\varepsilon$ bounding $t$ on $S$, not from an assumption. The milestone-3 bound carries no attainment hypothesis, so a proof must also handle the case in which the maximum over $S$ is not attained. Finally, $\Pi^\star(\mathcal M(0))$ is a supremum, and its nonnegativity (used in $\delta/(1-\delta)\le 2\delta$) and its finiteness must be derived from the feasible set.

Formalization scope

• Values, allocations and payments are total functions $\mathbb R\to\mathbb R$; every condition quantifies over $S=[0,\bar v]$ only, and the revenue integral is over $[0,\bar v]$.
• Standing assumptions (the density half of the paper's Assumption 1): $\bar v>0$, $f\ge 0$, $f=0$ off $[0,\bar v]$, $f$ integrable on $[0,\bar v]$ with integral $1$. The bounded-variation half of Assumption 1 is not used by Proposition 1 and is not assumed.
• Added hypothesis: mechanisms in $\mathcal M(\varepsilon)$ have measurable $x$ and $t$, so that $\mathbb E_v[t(v)]$ is meaningful.
• $\Pi^\star$ is the supremum (sSup) of the revenue image of $\mathcal M(\varepsilon)$, which is nonempty (the zero mechanism) and bounded above by $\bar v$; the goal and milestone 3 are stated for every $m\in\mathcal M(\varepsilon)$, which is equivalent to the bound on the supremum. $\Pi^\star(\mathcal M(0))$ is never replaced by the posted-price revenue.
• $\varepsilon^{1/2}$ is Real.sqrt ε. The constants $C$ and $\varepsilon_0$ are quantified after the distribution and before $\varepsilon$; quantifying them after $\varepsilon$ would make the goal trivial.
• Milestones 1 and 2 take the argmax selection $v^\star_\delta$ as a map vs with values in $S$ attaining the maximum, as the page assumes. The rounded mechanism is set to $0$ off $S$; its measurability is part of the conclusion, not a hypothesis.
• Restricting $\mathcal M(\varepsilon)$ to deterministic mechanisms, to nonnegative payments, or defining $\Pi^\star(\mathcal M(0))$ by the optimal posted-price revenue would change the statement and is ruled out.

Needed infrastructure: monotone functions are measurable, interval integrals of bounded measurable functions against an integrable density, and suprema of bounded real sets, all in Mathlib. Contributions of the rounding lemma in reusable form (for general type sets) are welcome.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS'05), pp. 605–614, 2005. https://doi.org/10.1109/SFCS.2005.50

Motivation

Centralized markets such as kidney exchanges, ride-sharing platforms and online labor markets match agents who arrive over time. Kerimov, Ashlagi and Gurvich (SSRN 3824407; Management Science, 2023, doi:10.1287/mnsc.2021.01215) study such a market with $n$ agent types and $d$ feasible multi-way matches. Their main result is that, when a fluid linear program called the static-planning problem (SPP) has a unique non-degenerate solution, a periodic resolving policy keeps the regret against the hindsight optimum bounded by a constant of order $1/\epsilon$ at all times, where the general position gap $\epsilon$ is the smallest positive basic variable of (SPP).

The constant $1/\epsilon$ is only informative if one can say what $\epsilon$ is. Section 5 of the paper does this for a class of networks it calls (SPP)-acyclic: there the optimal solution of (SPP) is an explicit signed sum of arrival rates, so $\epsilon$ is an imbalance between sums of arrival probabilities. This mission formalizes that structural result and the lemmas it rests on. It needs no probability: only the combinatorics of the network and linear programming.

Setting

A matching network has agent types $\mathcal A = \{1,\dots,n\}$ and matches $\mathcal M = \{1,\dots,d\}$. Match $m$ uses one agent of each type in a set $\mathcal A(m)$ with $|\mathcal A(m)| \ge 2$, every type belongs to some match, and the matching matrix $M \in \{0,1\}^{n\times d}$ has $M_{im} = 1$ iff $i \in \mathcal A(m)$. Arrival probabilities $\lambda$ satisfy $\lambda_i > 0$, $\sum_i \lambda_i = 1$, and match values satisfy $r_m > 0$.

The matching network graph $\mathcal G$ is the bipartite graph whose vertices are the types and the matches, with an edge between type $i$ and match $m$ iff $i \in \mathcal A(m)$.

For a right-hand side $b \in \mathbb R^n$, the static-planning problem is

$$\max\ r\cdot z\quad\text{s.t.}\quad Mz + s = b,\quad z \in \mathbb R^d_{\ge 0},\ s \in \mathbb R^n_{\ge 0},$$

and (SPP) is the case $b = \lambda$. For a solution $(z^*, s^*)$ write $\mathcal M_+ = \{m : z^*_m > 0\}$ (active matches), $\mathcal M_0 = \mathcal M \setminus \mathcal M_+$ (redundant matches), $\mathcal Q_+ = \{j : s^*_j > 0\}$ and $\mathcal Q_0 = \mathcal A \setminus \mathcal Q_+$.

The network satisfies the general position condition (GP) if (SPP) has a unique optimal solution $(z^*, s^*)$ and it is non-degenerate: $|\mathcal M_+| + |\mathcal Q_+| = n$. The optimal basis matrix $\mathcal B$ is formed by the columns of $M$ indexed by $\mathcal M_+$ and the unit vectors $e_j$, $j \in \mathcal Q_+$.

The (SPP)-residual graph is $\mathcal G$ with the redundant matches removed, and the network is (SPP)-acyclic if it satisfies GP and its (SPP)-residual graph has no cycle.

Formalization targets

Goal: Theorem 5.1 (p. 25)

Assume GP and (SPP)-acyclicity. Then there are vectors $y^l \in \{-1,0,1\}^n$, $l \in \mathcal M_+ \cup \mathcal Q_+$, with

$$z^*_m = y^m\lambda > 0\ (m \in \mathcal M_+),\qquad s^*_j = y^j\lambda > 0\ (j \in \mathcal Q_+),$$

and every right-hand side $\tilde\lambda > 0$ with $y^l\tilde\lambda > 0$ for all $l$ has, as its unique optimal solution, $z_m = y^m\tilde\lambda$ on $\mathcal M_+$, $s_j = y^j\tilde\lambda$ on $\mathcal Q_+$, and zero elsewhere.

Milestones

1. (4), p. 20. Under GP, $\mathcal B$ is invertible and $(z^*_{\mathcal M_+}, s^*_{\mathcal Q_+}) = \mathcal B^{-1}\lambda > 0$.
2. §4.2, p. 20. Under GP the same basis remains optimal for every $\tilde\lambda > 0$ with $\|\tilde\lambda - \lambda\|_\infty \le \zeta_0$, for some $\zeta_0 > 0$.
3. Lemma C.1, p. 44. A connected acyclic matching network graph has at least $n - d + 1$ leaves; under GP with $\mathcal M_0 = \emptyset$ and a connected acyclic residual graph, $|\mathcal Q_+| = n - d$ and some over-demanded queue takes part in exactly one match.

A further theorem item, Lemma 5.1 (p. 24), states that under GP a network with only two-way matches, in which every cycle contains an even number of matches, is (SPP)-acyclic.

Significance

Theorem 5.1 turns the regret constant of the paper's main theorem into a quantity one can read off the data: every positive basic variable, and therefore $\epsilon$, is $\sum_i y_i\lambda_i$ with coefficients in $\{-1,0,1\}$. Its second sentence describes the whole region of right-hand sides on which the same basis stays optimal, an open polyhedral cone cut out by the inequalities $y^l\tilde\lambda > 0$, which is how the paper relates GP to the arrival rates in §5.1.

On the formal side, the mission builds a reusable model of the matching network, its bipartite incidence graph and the static-planning linear program with a variable right-hand side. Prove2Me does not yet contain the structural theory of optimal bases of such programs. Theorem 5.1 and its milestones are proved in the paper (Appendix C and §4.2); none of them is machine-checked yet.

Difficulty

The representation $z^* = \mathcal B^{-1}\lambda$ holds for every network in general position, so the content of the theorem lies in two places.

• The entries of $\mathcal B^{-1}$. Inverses of $0/1$ matrices have arbitrary rational entries in general: the triangle network (three types, matches $\{1,2\},\{2,3\},\{1,3\}$) has an optimal basis whose inverse has entries $\pm\tfrac12$. The claim needs the acyclic structure of the residual graph in an essential way.
• The second sentence. Exhibiting numbers $y^l$ with $y^l\lambda = z^*_l$ is trivial and says nothing. The statement requires the same vectors to produce the unique optimal solution for a whole open set of right-hand sides, which forces them to be the rows of $\mathcal B^{-1}$. This step therefore also involves the optimality conditions of (SPP) and the uniqueness part of GP.

Formalization scope

Types are Fin n, matches Fin d, both 0-based. The topology is the structure MatchingNetwork with the fields $|\mathcal A(m)| \ge 2$ and "every type is in a match"; $\lambda$ and $r$ are separate vectors with the standing predicates $\lambda_i > 0$, $\sum_i\lambda_i = 1$ and $r_m > 0$, which are hypotheses of every theorem. The optimal solution $(z^*, s^*)$ is an argument together with the GP hypothesis, never a default or a choice. The graph is a SimpleGraph on Fin n ⊕ Fin d; the residual graph keeps redundant matches as isolated vertices, which affects neither acyclicity nor the degrees of type vertices. The column index type of $\mathcal B$ is $\mathcal M_+ \sqcup \mathcal Q_+$, and the inverse is a two-sided inverse over these index types, not Matrix.inv, which is $0$ on singular matrices.

Conventions the statements commit to:

• in Theorem 5.1, "induces the optimal solution" is read as the unique optimal solution, and $\tilde\lambda$ is any positive vector, not necessarily summing to one;
• "for all sufficiently small $\zeta_0$" in milestone 2 is the existence of one $\zeta_0 > 0$;
• Lemma C.1's count of $n - d + 1$ leaves is stated without natural-number subtraction;
• Lemma C.1's second half carries the standing reduction of Appendix C ($\mathcal M_0 = \emptyset$, one connected component) as hypotheses;
• "every cycle contains an even number of matches" in Lemma 5.1 is stated as "every cycle of the bipartite graph has length divisible by 4".

The paper's own text says "all entries of $Y$ are either $-1$, $0$, or $-1$" (p. 25); this is read as $-1$, $0$ or $1$, as in the theorem's statement.

A formalization that keeps only the first sentence of Theorem 5.1, or that lets the vectors $y^l$ be unrelated to the basis, is trivially satisfiable and is not the theorem.

Needed infrastructure: optimality conditions for linear programs in equality form (reduced costs, uniqueness of a non-degenerate optimum), Mathlib's acyclic graphs and trees (SimpleGraph.IsAcyclic, IsTree.card_edgeFinset), and degree counting on bipartite graphs. The paper proves Theorem 5.1 in Appendix C by an explicit construction along paths of the residual graph; any correct argument is welcome. Lemmas on the inverse of a basis matrix whose bipartite row–column graph is a forest would be reusable well beyond this mission.

Selected references

• S. Kerimov, I. Ashlagi, I. Gurvich, Dynamic Matching: Characterizing and Achieving Constant Regret, SSRN 3824407 (version of September 14, 2022); Management Science (2023). https://ssrn.com/abstract=3824407, https://doi.org/10.1287/mnsc.2021.01215
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.1 (sensitivity analysis of an optimal basis).

Motivation

Offline policy learning chooses a treatment rule from logged data: given $n$ observations of features $X_i$, the action $A_i$ taken and the reward obtained, pick a policy $\pi:\mathcal X\to\{1,\dots,d\}$ from a class $\Pi$ whose expected reward is close to the best in the class. Zhou, Athey and Wager (arXiv:1810.04778v2) bound the regret of their cross-fitted augmented inverse-propensity-weighted learner by a quantity of order $\kappa(\Pi)\sqrt{V_*/n}$, where $\kappa(\Pi)$ is an entropy integral built from Hamming covering numbers of $\Pi$. A bound of this kind is only useful for a concrete policy class if $\kappa(\Pi)$ is finite and explicit.

Decision trees are the class the paper uses in practice: they are interpretable, they are the standard object in personalized-treatment applications, and the paper's computational sections (a mixed-integer program and a tree-search algorithm) optimize over them. Lemma 4 of the paper is the bridge between the general regret theory and trees: it bounds the Hamming covering number of the class $\Pi_L$ of depth-$L$ trees, and hence $\kappa(\Pi_L)$. Covering and complexity bounds for trees in the 0–1 (two-action) setting go back to VC-dimension arguments; the multi-action Hamming-cover version here is the one this paper's regret bound consumes.

Setting

Features are points $x\in\mathbb R^p$ with components $x(1),\dots,x(p)$; there are $d$ actions, written $1,\dots,d$. A deterministic policy is a map $\pi:\mathbb R^p\to\{1,\dots,d\}$.

Hamming distance and covers. Fix points $x_1,\dots,x_n$ (repetitions allowed). For two policies,

$$H(\pi_1,\pi_2)=\frac1n\sum_{j=1}^n\mathbf 1\{\pi_1(x_j)\ne\pi_2(x_j)\}.$$

The $\varepsilon$-Hamming covering number $N_H(\varepsilon,\Pi,\{x_1,\dots,x_n\})$ is the least $K$ such that some $\pi_1,\dots,\pi_K\in\Pi$ have every $\pi\in\Pi$ within Hamming distance $\varepsilon$ of some $\pi_i$. The covering number of the class is the worst case over point sets,

$$N_H(\varepsilon,\Pi)=\sup\{N_H(\varepsilon,\Pi,\{x_1,\dots,x_m\}) : m\ge1\},$$

and the entropy integral is $\kappa(\Pi)=\int_0^1\sqrt{\log N_H(\varepsilon^2,\Pi)}\,d\varepsilon$.

Decision trees. A depth-$L$ tree has $L$ layers: $L-1$ layers of branch nodes and a final layer of leaves, so $2^{L-1}-1$ branch nodes and $2^{L-1}$ leaves; a depth-1 tree is a single leaf. A branch node carries a split variable $i\in\{1,\dots,p\}$ and a threshold $b\in\mathbb R$, and sends $x$ to its left child if $x(i)<b$ and to its right child otherwise. Each leaf carries an action. $\Pi_L$ is the set of policies computed by depth-$L$ trees. In the Lean development these are DTree p d L, DTree.eval and treePolicies p d L; the Hamming layer is hammingDist, hammingCoverNumOn, hammingCoverNum and entropyIntegral.

Formalization targets

Goal: Lemma 4, part 1 (p. 27)

For $p,d,L\ge1$ and $\varepsilon>0$, $N_H(\varepsilon,\Pi_L)$ is finite and

$$\log N_H(\varepsilon,\Pi_L)\le(2^L-1)\log p+2^L\log d+(2^L-1)\log\Big(\frac L\varepsilon+1\Big).$$

Milestones (App. F)

1. Display (66), p. 67: for any reals $r_1,\dots,r_m$ there are $\lceil L/\varepsilon\rceil$ thresholds $b_i$ such that every indicator $\mathbf 1_b(r)=\mathbf 1\{r<b\}$ is within Hamming distance $\varepsilon/L$ of some $\mathbf 1_{b_i}$ with respect to $r_1,\dots,r_m$.
2. App. F, Step 2, p. 69: for any $n\ge1$ points, $p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ depth-$L$ trees $\varepsilon$-cover $\Pi_L$, i.e. $N_H(\varepsilon,\Pi_L,\{x_1,\dots,x_n\})\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$.
3. App. F, Step 2, p. 69: $N_H(\varepsilon,\Pi_L)\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$.

Companion: Lemma 4, part 2 (p. 27)

$$\kappa(\Pi_L)\le\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1}.$$

It is posed as printed, as a second theorem of the mission rather than a milestone of the goal.

Significance

The result. Lemma 4 makes the abstract regret theory of the paper concrete: with part 2 it gives Theorem 4, the regret bound $O_p\big((\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1})\sqrt{V_*/n}\big)$ for learning depth-$L$ trees, which for fixed $L,p,d$ is $O_p(\sqrt{V_*/n})$. The covering bound grows only logarithmically in $1/\varepsilon$, which is the property the paper's Assumption 3 asks of a policy class. The same counting gives covering bounds for any class of piecewise-constant rules on axis-aligned partitions of bounded depth.

Formalizing it. The result is proved in the paper (App. F) but, as far as known, has no machine-checked proof. The paper omits the induction that combines per-node threshold grids into a cover of whole trees ("a straightforward but lengthy induction (omitted)"), and its appendix counts $2^L-1$ branch nodes where §6.1's trees have $2^{L-1}-1$. A formal proof fixes both: it supplies the omitted induction and confirms that the printed bound holds for the class actually defined in §6.1. The milestones are reusable statements about threshold indicators and tree covers. The companion part 2 is posed with the printed constant $4/3$, although the printed derivation evaluates $\int_0^1(L/\varepsilon^2)^{1/4}d\varepsilon$ as $\frac43L^{1/4}$ where the integral equals $2L^{1/4}$; whether the printed bound holds is part of what the mission settles.

Difficulty

The one-dimensional step (66) is elementary once the Hamming distance between two threshold indicators is identified with a count of points between the thresholds. The difficulty is in passing from single thresholds to whole trees. Replacing each branch node's threshold independently by its nearest grid threshold, with grids built on all $n$ points, does not give an $\varepsilon$ cover: the errors at different nodes of the same layer add up, and the naive bound is $(2^{L-1}-1)\varepsilon/L$ rather than $\varepsilon$. The points that reach a node depend on the thresholds above it, so the approximation has to respect the tree structure, while the number of candidate trees must still be counted as a product over nodes. The passage from finite point sets to $N_H(\varepsilon,\Pi_L)$, which is a supremum over all point sets in $\mathbb N\cup\{\infty\}$, and the arithmetic with $\lceil L/\varepsilon\rceil$ and real logarithms are routine but must be done in the stated types.

Formalization scope

• Features range over all of $\mathbb R^p$ (Fin p → ℝ); the paper's $\mathcal X$ is a bounded subset of $\mathbb R^p$, and a bound over $\mathbb R^p$ implies the bound over every $\mathcal X\subseteq\mathbb R^p$. Actions are Fin d, split variables Fin p (0-based); policies are deterministic.
• Point sets are sequences Fin m → (Fin p → ℝ) with repetitions allowed, $m\ge1$; covers are proper (centres in $\Pi_L$). $N_H(\varepsilon,\Pi)$ is in ℕ∞, $\kappa(\Pi)$ a lower Lebesgue integral in ℝ≥0∞ over $(0,1]$.
• Depth follows §6.1: DTree p d 1 are leaves, DTree p d 0 is empty. The bounds are the printed ones, which over-count for this convention; the Lean was not switched to the appendix's convention, which would change $\Pi_L$.
• Standing hypotheses: $p\ge1$, $d\ge1$, $L\ge1$ ("Let $L$ be any fixed positive integer"), $\varepsilon>0$ (needed for $\lceil L/\varepsilon\rceil$).
• The goal asserts finiteness of $N_H(\varepsilon,\Pi_L)$ explicitly. Without it the inequality would be trivially true for an infinite covering number, because Lean's toNat ⊤ = 0 and Real.log 0 = 0. The covering number is an infimum that is $0$ only for an empty class, and $\Pi_L$ is nonempty under the hypotheses, so the cover is not trivialized either.
• Not posed: the $O(\log 1/\varepsilon)$ remark of Lemma 4.1 (a remark on the right-hand side); Theorem 4 (p. 28, the combination with the regret theorem, which belongs to the companion mission on regret); the mixed-integer program and tree search of §6.2–6.3 and App. G (computational).

Contributions welcome: proofs of the milestones, the omitted per-node induction as a stand-alone lemma, and the companion part 2.

Selected references

• Z. Zhou, S. Athey, S. Wager, Offline Multi-Action Policy Learning: Generalization and Optimization, arXiv preprint, 2018 (v2). https://arxiv.org/abs/1810.04778
• L. Breiman, J. Friedman, R. Olshen, C. Stone, Classification and Regression Trees, Wadsworth, 1984. https://doi.org/10.1201/9781315139470
• D. Bertsimas, J. Dunn, Optimal classification trees, Machine Learning 106, 1039–1082, 2017. https://doi.org/10.1007/s10994-017-5633-9
• S. Athey, S. Wager, Policy Learning With Observational Data, Econometrica 89(1), 133–161, 2021. https://doi.org/10.3982/ECTA15732

Prize money in rank-order competitions

Tournaments, races, poker finals and sports leagues end with a ranking of the participants and a sum of prize money to be split among them. The split is usually fixed by a published schedule, and different events use very different schedules: some pay almost everything to the winner, some pay many places, some decay geometrically from one place to the next. Dietzenbacher and Kondratev (arXiv:2008.08985, published in Management Science, 2023) treat the choice of schedule axiomatically: they state fairness, solidarity and consistency properties that a prize allocation rule may satisfy and characterize the families of rules that satisfy them. Their paper has three characterization theorems. Theorem 1 (interval rules) is the subject of a companion mission; this mission formalizes Theorem 2, the characterization of single-parametric rules under local consistency.

Axiomatic characterizations of allocation rules through consistency have a long history in fair division: bankruptcy problems (Aumann and Maschler, 1985), taxation (Young, 1987), bargaining (Lensberg, 1987) and cooperative games (Peleg, 1986; Hart and Mas-Colell, 1989); the paper's §1 surveys this literature. The paper is, by its own account, the first to apply this approach to prize allocation in rank-order competitions.

Setting

Fix a countable set $U$ of at least three potential competitors. A competition $(N,\mathcal R,E)$ consists of a finite set $N\subseteq U$, a ranking $\mathcal R:N\to\{1,\dots,|N|\}$ (a bijection; $i$ is ranked above $j$ when $\mathcal R(i)<\mathcal R(j)$) and a prize endowment $E\ge0$. For $S\subseteq N$ the subranking $\mathcal R_S$ lists $S$ in the order of $\mathcal R$. A prize allocation rule $\varphi$ assigns to each competition nonnegative prizes $\varphi_i(N,\mathcal R,E)$, $i\in N$, with $\sum_{i\in N}\varphi_i(N,\mathcal R,E)=E$.

The axioms of Theorem 2 are:

• anonymity: the prize depends only on $|N|$, the position and $E$, not on who the competitors are;
• order preservation: a higher-ranked competitor never receives less than a lower-ranked one;
• winner strict endowment monotonicity: when $E$ increases, nobody receives less, and the winner receives strictly more;
• local consistency: if a block $S$ of consecutively ranked competitors (the condition $|\mathcal R(i)-\mathcal R(j)|\le|S|-1$ for all $i,j\in S$) re-divides the total prize it received, using the rule on the reduced competition $(S,\mathcal R_S,\sum_{j\in S}\varphi_j(N,\mathcal R,E))$, each member gets the same prize as before.

A representation is a continuous, non-decreasing $f:\mathbb R_+\to\mathbb R_+$ with $f(x)\le x$. The single-parametric rule with representation $f$ pays $x$ to the winner, $f(x)$ to the runner-up, $f(f(x))$ to the third, and in general

$$\varphi_i(N,\mathcal R,E)=f^{(\mathcal R(i)-1)}(x),\qquad\text{where } x\ge0 \text{ solves } \sum_{k=1}^{|N|}f^{(k-1)}(x)=E .$$

Equal Division ($f(x)=x$), Winner-Takes-All ($f=0$), Winner-Takes-Surplus ($f(x)=\min\{a,x\}$) and the arithmetic rule $f(x)=\max\{0,x-1\}$ are examples.

Formalization targets

Goal: Theorem 2 (p. 18)

$$\varphi \text{ satisfies anonymity, order preservation, winner strict endowment monotonicity and local consistency} \iff \varphi \text{ is a single-parametric rule.}$$

Both directions are part of the goal.

Milestones, in the order the proof on pp. 31–32 uses them

1. Converse (p. 31): every single-parametric rule satisfies the four axioms.
2. The representation (p. 31): on a two-competitor competition, the allocation path $E\mapsto(\varphi_1,\varphi_2)$ is the graph $\{(x,f(x))\}$ of a well-defined representation $f$.
3. Two-competitor form (p. 31): by anonymity, the rule is the single-parametric rule with representation $f$ on every competition with two competitors.
4. Propagation (pp. 31–32): if the single-parametric rule $\varphi'$ with representation $f$ first exceeds $\varphi$ at position $i$, then $\varphi'_j\ge\varphi_j$ for every $j>i$.
5. Uniqueness (p. 32): a locally consistent rule that follows $f$ on two competitors coincides with $\varphi'$ everywhere.

The paper's Lemma 1 (endowment monotonicity implies endowment continuity, p. 10) is used at the start of the proof; it is formalized in the companion mission on interval rules, and the milestones here take endowment continuity as a hypothesis.

Companions

• Existence and uniqueness of $x$ (p. 18): for every representation $f$, $|N|\ge1$ and $E\ge0$ the equation $\sum_{k=1}^{|N|}f^{(k-1)}(x)=E$ has exactly one solution $x\ge0$.
• Corollary 5 (p. 19): a single-parametric rule satisfies winner-loser strict order preservation iff $f(x)<x$ for $x>0$; strict order preservation iff $0<f(x)<x$ for $x>0$; strict endowment monotonicity iff $f$ is increasing.
• Corollary 6 (p. 20): anonymity, order preservation, endowment additivity and local consistency characterize the geometric rules $\varphi_i=\lambda^{\mathcal R(i)-1}E/\sum_{k=1}^{|N|}\lambda^{k-1}$, $\lambda\in[0,1]$.

Significance

Theorem 2 reduces an infinite family of allocation schedules, one for every number of competitors and every endowment, to one function of one real variable. A designer who accepts the four axioms only has to choose how the prize of one position determines the prize of the next; the schedule for every field size and every endowment then follows. Corollaries 5 and 6 translate further axioms into shape conditions on that function, and identify the geometric schedules used in practice (the paper fits one to a poker final, p. 20) as the scale-invariant case. Local consistency is the property that a league split into consecutive divisions pays every division the same as the whole league would.

The result is proved in the paper; nothing here is open. No part of it has been formalized before: the platform has no model of prize allocation rules or of consistency axioms over variable populations. The mission produces that model (competitions over a universe of competitors, subrankings, the axioms) and a machine-checked proof of the characterization, including the "readily checked" converse that the paper leaves to the reader.

Difficulty

The converse requires that the parameter $x$ be well defined: the map $x\mapsto\sum_{k}f^{(k-1)}(x)$ must be shown continuous, strictly increasing and onto $\mathbb R_+$, so that it can be inverted, and local consistency then requires identifying the parameter of a reduced competition with an iterate of the original one. In the forward direction the representation $f$ is defined only implicitly, as the second coordinate of the two-competitor allocation path; its continuity and monotonicity come from inverting the strictly increasing winner's prize $E\mapsto\varphi_1(N,\mathcal R,E)$, which needs both endowment continuity and the strict part of winner strict endowment monotonicity. Without the strict part the runner-up's prize is not a function of the winner's, and the paper's Example 5 shows that local consistency alone then does not determine the rule from its two-competitor restriction. The extension from two to many competitors is a comparison argument over positions that uses local consistency only on adjacent pairs.

Formalization scope

• Competitions. A ranking is a duplicate-free nonempty List U, best competitor first; $N$ is its set of entries and $\mathcal R(i)$ is the 1-based position pos l i. The subranking $\mathcal R_S$ is the sublist of entries in $S$. $U$ is any type with decidable equality; the goal and the corollaries carry the page's standing assumptions [Countable U] and the existence of three distinct elements. Milestones that do not need them omit them.
• Rules are functions List U → ℝ → U → ℝ. A prize allocation rule is nonnegative and exhausts $E$ on every ranking and every $E\ge0$; values elsewhere are irrelevant, and every axiom quantifies only over rankings, $E\ge0$ and competitors in $N$.
• Representations are functions on $\mathbb R$ constrained on $[0,\infty)$ only: ContinuousOn and MonotoneOn on Set.Ici 0, and $0\le f(x)\le x$ for $x\ge0$. Requiring global continuity or monotonicity on $\mathbb R$ would shrink the family and is not done. The sum $\sum_{k=1}^{|N|}f^{(k-1)}(x)$ uses the iterate f^[k] with the index shifted to $k=0,\dots,|N|-1$; "$x$ is chosen such that" is an existential, and uniqueness of $x$ is a separate item.
• Trivializing encodings ruled out. The rule is defined on every competition over $U$, not on a fixed competitor set; local consistency ranges over exactly the blocks of consecutive positions (using full consistency instead would make the "if" direction false for most $f$); the goal is a biconditional; the family requires continuity of $f$ and is not restricted to a closed form.
• Infrastructure. The model and the axioms shared with the companion missions on interval and parametric rules are one common set of definitions; this mission adds three: local consistency, single-parametric rules, and geometric rules. Lemma 1 and the facts about inverting a continuous strictly increasing function on $\mathbb R_+$ are reusable beyond this mission. Proofs of any item, and of the companions, are welcome.

Selected references

• B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science, 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. https://doi.org/10.1016/0022-0531(85)90102-4

Motivation

Rank-order competitions — sports tournaments, poker final tables, golf tours, crowdsourcing contests, sales leagues — end with a ranking of the participants and a pot of prize money that has to be split according to that ranking. Organisers publish prize tables that change with the number of entrants and with the size of the purse, and these tables are usually justified only by tradition. Dietzenbacher and Kondratev (arXiv:2008.08985v2, published in Management Science 2023, doi:10.1287/mnsc.2022.4520) take the axiomatic approach of fair-division theory and ask which prize allocation rules are characterised by natural requirements of fairness and coherence across competitions of different sizes.

Consistency — invariance of a rule under "re-running the allocation" for a subgroup with the money it collectively received — has a long history in axiomatic allocation: bankruptcy problems (Aumann and Maschler 1985), taxation (Young 1987), bargaining (Lensberg 1987, 1988) and cooperative games (Peleg 1986; Hart and Mas-Colell 1989). The paper applies it to competitions. Full consistency together with order preservation and endowment monotonicity yields the interval rules (Theorem 1); weakening consistency to local consistency yields the single-parametric rules (Theorem 2). This mission concerns the weakest version, top consistency, which only constrains the top segment of the ranking and describes real prize schemes such as the golf tournament of Table 1(b) of the paper. It is the third mission of a series on this paper; the first two treat Theorems 1 and 2.

Setting

Fix a countable set $U$ of at least three potential competitors. A competition $(N,\mathcal R,E)$ consists of a finite nonempty set $N\subseteq U$, a ranking $\mathcal R:N\to\{1,\dots,|N|\}$ (a bijection; competitor $i$ is ranked above $j$ when $\mathcal R(i)<\mathcal R(j)$), and a prize endowment $E\ge0$. For $S\subseteq N$ the subranking $\mathcal R_S:S\to\{1,\dots,|S|\}$ orders $S$ as $\mathcal R$ does.

A prize allocation rule $\varphi$ assigns to each competition a vector $\varphi(N,\mathcal R,E)\in\mathbb R_+^N$ with $\sum_{i\in N}\varphi_i(N,\mathcal R,E)=E$. The axioms are:

• anonymity: $\varphi_i(N,\mathcal R,E)=\varphi_j(N',\mathcal R',E)$ whenever $|N|=|N'|$ and $\mathcal R(i)=\mathcal R'(j)$;
• order preservation: $\mathcal R(i)<\mathcal R(j)$ implies $\varphi_i\ge\varphi_j$;
• winner strict endowment monotonicity: if $E<E'$ then $\varphi_i(N,\mathcal R,E)\le\varphi_i(N,\mathcal R,E')$ for all $i$, strictly for the winner $\mathcal R(i)=1$;
• top consistency: for each $S\subseteq N$ with $\mathcal R(i)\le|S|$ for every $i\in S$, and each $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).$$

A rule is parametric if there are continuous non-decreasing $f_1,f_2,\dots:\mathbb R_+\to\mathbb R_+$ with $f_1(x)=x$ and $f_{k+1}(x)\le f_k(x)$ such that $\varphi_i(N,\mathcal R,E)=f_{\mathcal R(i)}(x)$, where $x\ge0$ solves $\sum_{k=1}^{|N|}f_k(x)=E$. The winner gets $x$ and position $k$ gets $f_k(x)$. Equal Division ($f_k(x)=x$) and Winner-Takes-All ($f_k=0$ for $k\ge2$) are parametric.

Formalization targets

Goal: Theorem 3 (p. 22)

$$\varphi \text{ is anonymous, order preserving, winner strictly endowment monotonic and top consistent}\iff\varphi\text{ is a parametric rule.}$$

Both directions are part of the goal.

Milestones (proof of Theorem 3, pp. 32–33)

1. Every parametric rule satisfies the four axioms (the "readily checked" direction).
2. Under order preservation, endowment continuity and winner strict endowment monotonicity, the winner's prize $E\mapsto\varphi_1(N,\mathcal R,E)$ is strictly increasing, continuous and unbounded on $\mathbb R_+$, so each $x\ge0$ is the winner's prize for exactly one $E$.
3. The induction step: a representation $f_1,\dots,f_n$ valid on all competitions with at most $n$ competitors extends, by a new continuous non-decreasing $f_{n+1}\le f_n$, to all competitions with $n+1$ competitors.

Lemma 1 of the paper (endowment monotonicity implies endowment continuity, p. 10) is used in the proof; it is formalized in the first mission of this series and will be referenced from there.

Companion: Corollary 8 (p. 22)

Replacing winner strict endowment monotonicity by endowment additivity (equivalently scale invariance) characterises the proportional rules $\varphi_i=\lambda_{\mathcal R(i)}E/\sum_{k\le|N|}\lambda_k$ with $\lambda_1>0$ and $\lambda_{k+1}\le\lambda_k$.

Significance

Theorem 3 says that the four axioms leave exactly one degree of freedom per position: a monotone function of the winner's prize. This gives organisers a complete menu of prize schemes that are fair in the anonymous, order-preserving sense and that keep the top of the table unchanged when lower-ranked entrants leave — the property that matters when competitors are eliminated one at a time and paid at the moment of elimination. It contains the single-parametric rules of Theorem 2, the Winner-Takes-Surplus rules, the geometric rules and the proportional rules (Corollary 8) as special cases, and the paper shows in a Remark (p. 33) that the four axioms are logically independent.

The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. The formalization adds a reusable layer for variable-population allocation problems — rankings of finite subsets of a fixed universe, subrankings, and consistency axioms restricted to families of subsets — that is not in Mathlib. Formal proofs of both directions, of the milestones, and of Corollary 8 are all welcome.

Difficulty

The "if" direction is a computation, but it requires showing that the parameter $x$ is well defined and moves monotonically with $E$, which uses $f_1(x)=x$ and the intermediate value theorem. The "only if" direction must construct the functions $f_k$ from an abstract rule. The natural first idea — define $f_k(x)$ as the prize of position $k$ when the winner receives $x$ — needs the winner's prize to be invertible as a function of $E$, which uses continuity (supplied by Lemma 1, not assumed), strict monotonicity only for the winner, and unboundedness, which comes from order preservation together with exhaustion of the endowment. Top consistency then has to transfer the representation from competitions of size $n$ to size $n+1$, and anonymity has to transfer it from one ranked set to every other one of the same size; the induction over the number of competitors must keep all smaller sizes, since top consistency reduces to every top segment.

Formalization scope

• A ranked set $(N,\mathcal R)$ is a duplicate-free nonempty List U, best competitor first; $\mathcal R(i)$ is the 1-based index pos l i, and $\mathcal R_S$ is the sublist of entries in $S$. $U$ is an arbitrary type with decidable equality; the paper's standing assumptions (countable, at least three elements) are hypotheses of the goal and of Corollary 8, and are omitted from milestones that do not use them.
• A rule is a function φ : List U → ℝ → U → ℝ; it is required to be a prize allocation rule (nonnegative prizes summing to $E$) on rankings and $E\ge0$, and every axiom quantifies only over that domain. Endowments are reals with $E\ge0$.
• The representation $f_1,f_2,\dots$ is f : ℕ → ℝ → ℝ, indexed from 1 as on the page ($f_0$ unused); continuity, monotonicity, nonnegativity and $f_1(x)=x$ are required on $[0,\infty)$. The parameter $x$ is given existentially; it is unique, so this is the page's "where $x\in\mathbb R_+$ is such that".
• Endowment continuity is coordinatewise continuity on $[0,\infty)$.

Trivializing formalizations are ruled out: rules act on every finite ranked subset of $U$, not on a fixed competitor set; top consistency quantifies over exactly the top segments (full or local consistency would change the theorem — the rule of Example 6 is parametric but not locally consistent); the goal is a biconditional; the parametric family includes $f_1=\mathrm{id}$, the decreasing chain $f_{k+1}\le f_k$, and continuity of every $f_k$.

Corollary 7 of the paper is not included: its "only if" parts ("for each $k$") fail as written when $U$ is finite, since $f_k$ for $k>|U|$ is not determined by the rule.

Selected references

• B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science, 2023. https://arxiv.org/abs/2008.08985v2, 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(2):195–213, 1985. https://doi.org/10.1016/0022-0531(85)90102-4
• S. Hart and A. Mas-Colell, Potential, value, and consistency, Econometrica 57(3):589–614, 1989. https://doi.org/10.2307/1911054

Motivation

Firms that outsource work to an agent whose effort they cannot observe often punish poor performance by suspending the relationship for a while, even though restarting costs money: a new set-up, re-training, re-mobilisation. Cao, Sun and Tian (Management Science, 2024) study this trade-off in a continuous-time principal–agent model with Poisson arrivals and a fixed switching cost paid every time work (re)starts. They characterise the optimal dynamic contract in three regimes: never hire the agent, hire and keep the agent working forever, or a control-band contract with suspension episodes of fixed length. The model extends the Poisson-arrival contracting framework of Sun and Tian (2018) by adding the switching cost.

The proof follows a guess-and-verify pattern. A stochastic verification theorem (Theorem 1 of the paper) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value. Propositions 2–7 then supply such a pair in each parameter region. This mission covers one region: the agent is much more impatient than the principal (Condition 2) and the switching cost is high.

Setting

A principal earns revenue $R$ per arrival of a Poisson process. Without the agent's effort the arrival rate is $\underline\mu\ge0$; with effort it is $\mu>\underline\mu$, and effort costs the agent $b>0$ per unit of time. While the agent works, the principal's total cost rate is $c\ge b$. Each time work starts or restarts, the principal pays a switching cost $K>0$. The principal discounts at rate $r$ and the agent at rate $\rho$, with $0<r\le\rho$. Write $\Delta\mu=\mu-\underline\mu$. Assumption 1 is $R\Delta\mu>c$.

The derived constants are

$$\beta=\frac{b}{\Delta\mu},\qquad \bar w=\frac{\beta\mu}{\rho},\qquad \underline v=\frac{\underline\mu R}{r},\qquad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\qquad \bar K_2=\bar V-\underline v-\bar w .$$

The variable $w\ge0$ is the agent's promised utility. The revenue threshold is

$$\hat R=\Big[\frac cb+\frac{(\rho-r)\mu}{\Delta\mu(\rho-r-\mu)}\cdot\frac{\rho-\mu}{\rho}\Big]\beta .$$

Condition 2 is: $\mu<\rho-r$ and $R\ge\hat R$.

For a function $f$ on $\mathbb R_+$ with left derivative $f'$, the working-state operator and the suspension-state operator are

$$(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,$$ $$(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu .$$

The first is a delay-differential operator: it evaluates $f$ at $w+\beta$. A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if

$$(\mathcal A_IV_I)(w)\ge0,\quad(\mathcal A_\emptyset V_\emptyset)(w)\ge0,\qquad 0\le V_I(w)-V_\emptyset(w)\le K,\qquad V_I(0)\ge\underline v,\ V_\emptyset(0)\ge\underline v .$$

Formalization targets

Goal: Proposition 4

Under Condition 2, let $V_I$ be the line from $\underline v$ at $w=0$ to $\bar V$ at $w=\bar w$, and let $V_I$ be constant $\bar V$ beyond $\bar w$ (display (31)). Then

$$K>\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset\equiv\underline v)\ \text{satisfies (20)–(22)},$$ $$\bar K_2<K\le\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset)\ \text{satisfies (20)–(22)},$$

where in the second case $V_\emptyset$ is the line from $\underline v$ to $\bar V-K$ on $[0,\bar w]$, constant $\bar V-K$ beyond (display (32)).

Milestones

1. Lemma EC.2(vi), second claim: if $\rho>r+\mu$, then $\bar V-\frac{\rho-r}{\rho-r-\mu}\bar w\ge\underline v$ if and only if $R\ge\hat R$.
2. Proposition 4, first part: the case $K>\bar V-\underline v$.
3. Proposition 4, second part: the case $\bar K_2<K\le\bar V-\underline v$.

Significance

Through the paper's verification theorem, Proposition 4 yields the "not hiring" half of the main Theorem 2 in the Condition 2 regime. If $K\ge\bar K_2$, the principal's value is at most $\underline v$, so it is optimal never to engage the agent (Theorem 3). The threshold $\bar K_2=\bar V-\underline v-\bar w$ is the switching cost above which the value of hiring, net of the set-up cost and of the agent's promised rent, falls below the outside value. Together with the companion missions of this series (Condition 1 with high cost, Condition 2 with medium cost, and the low-cost control-band regime), this result completes the partition of the parameter space behind Theorem 2.

The result is proved in the paper and has no machine-checked proof yet. This mission states the analytic certificate of the guess-and-verify argument, not the contract-optimality theorem. The contribution it asks for is a formal proof that these explicit functions satisfy the quasi-variational inequalities, including the left-derivative behaviour at the kink $w=\bar w$ and the algebra that links Condition 2 to the sign of $\mathcal A_IV_I$.

Difficulty

The functions are piecewise linear, so the difficulty is not analytic depth but bookkeeping that is easy to get wrong:

• The operator $\mathcal A_I$ is non-local. It evaluates $V_I$ at $w+\beta$, and which branch of (31) applies there depends on how $\bar w$ compares with $\beta$, which Condition 2 settles.
• At the kink $w=\bar w$ the functions are not differentiable, so the left-derivative convention must be used explicitly.
• The sign of $\mathcal A_IV_I$ on $[0,\bar w]$ reduces to an inequality between $\bar V$, $\underline v$ and $\bar w$, and showing that this inequality is the revenue condition $R\ge\hat R$ requires unfolding (8)–(10) and (28).

The naive check, that $\mathcal A_IV_I$ vanishes or is positive because $V_I$ is "close to" a solution of the delay equation, does not work: $V_I$ is not a solution of (25), and the inequality is strict in general.

Formalization scope

All parameters are real numbers in one structure Params. Its predicate Standing collects the paper's standing assumptions: $0\le\underline\mu<\mu$, $0<b\le c$, $K>0$, $0<r\le\rho$ and $R\Delta\mu>c$. Two of these are added to the page and disclosed: $\underline\mu\ge0$, since it is an arrival rate, and $b>0$, since (31)–(32) divide by $\bar w=\beta\mu/\rho$.

Functions are ℝ → ℝ, and every condition is quantified over $w\ge0$ only. The derivative in $\mathcal A_I$ and $\mathcal A_\emptyset$ is the left derivative derivWithin f (Set.Iic w) w, as the paper prescribes on p. 15. Inequality (20) is required for $w>0$: on $\mathbb R_+$ the left derivative at $0$ does not exist. Inequalities (21) and (22) are required exactly as printed. "Satisfy the optimality condition (20)–(22)" means exactly these three conditions; the paper's Theorem 1 additionally asks for monotonicity and concavity, but Proposition 4 does not claim them and they are not added.

The threshold $\hat R$ is the printed formula. Its denominator $\rho-r-\mu$ is positive under Condition 2, so Lean's convention $x/0=0$ never applies there.

None of the conditions is weakened: (21) keeps both bounds, (22) is kept, and the operators are not pre-simplified with the closed form of $\bar V$. A formal proof therefore has to carry out the sign computation itself. The stochastic contract model (Poisson point processes, promise keeping, incentive compatibility), the verification Theorem 1 and the optimality Theorems 2–3 are not formalized.

Two hat symbols elsewhere in the paper are distinct objects from those used here: $\hat{\mathrm w}$ of Lemma 3 and the bold $\hat{\mathbf w}$ of Proposition 6. Neither appears in this mission. Proofs of the milestones, and proofs of the goal that use them, are welcome.

Selected references

• P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
• P. Sun, F. Tian, Optimal Contract to Induce Continued Effort, Management Science 64(9), 4193–4217, 2018. https://doi.org/10.1287/mnsc.2017.2795