All missions

Motivation

In linear regression with a budget, an experimenter holds $n$ candidate experiments, each described by a vector $v_i\in\mathbb R^d$, and may run only $k$ of them. If the experiments in $S\subseteq[n]$ are run and the unknown parameter is estimated by least squares, the covariance of the estimate is proportional to $\big(\sum_{i\in S}v_iv_i^\top\big)^{-1}$. A-optimal design chooses $S$ to minimise the trace of that matrix, which is the mean squared error of the estimator. The criterion is one of the classical optimality criteria of experimental design (Pukelsheim, Optimal Design of Experiments, SIAM 2006) and appears in feature selection, sensor placement and matrix sparsification.

Selecting the best $k$-set exactly is NP-hard (the paper proves this in its Theorem 1.7), so the question is approximation. Avron and Boutsidis (SIAM J. Matrix Anal. Appl. 2013) connected A-optimal design to volume sampling (Deshpande–Rademacher, FOCS 2010), which samples a set with probability proportional to $\det(V_SV_S^\top)$, and obtained the approximation ratio $\frac{n-d+1}{k-d+1}$. Nikolov, Singh and Tantipongpipat (arXiv:1802.08318; Mathematics of Operations Research, 2022) reweight volume sampling by a second measure $\mu$ that can depend on a solution of the natural convex relaxation. Their first result, Theorem 1.3, shows that the approximation ratio of this scheme is controlled by a single combinatorial property of $\mu$, approximate $(d-1,d)$-wise independence. Their later theorems obtain ratios $d$ (when $k=d$) and $1+\epsilon$ (when $k$ is large) by exhibiting such measures.

Setting

Let $V=[v_1,\dots,v_n]$ be a real $d\times n$ matrix and $d\le k\le n$. For $S\subseteq[n]$, $V_S$ is the $d\times|S|$ submatrix of the columns indexed by $S$, so $V_SV_S^\top=\sum_{i\in S}v_iv_i^\top$. The A-optimal design problem is

$$\mathrm{OPT}=\min_{S\subseteq[n],\,|S|=k}\operatorname{tr}\big(V_SV_S^\top\big)^{-1},$$

with the value $+\infty$ for sets whose Gram matrix is singular.

The convex relaxation (1)–(3) replaces the indicator of $S$ by $x\in\mathbb R^n$:

$$\mathrm{CP}=\min\ \operatorname{tr}\Big(\sum_{i=1}^n x_iv_iv_i^\top\Big)^{-1}\quad\text{s.t.}\quad\sum_{i=1}^n x_i=k,\quad 0\le x_i\le 1.$$

Write $V_S(x)$ for the matrix with columns $\sqrt{x_i}\,v_i$, $i\in S$, so that $V(x)V(x)^\top=\sum_ix_iv_iv_i^\top$, and $x^L=\prod_{i\in L}x_i$.

Let $\mathcal U_k$ ($\mathcal U_{\le k}$) be the subsets of $[n]$ of size exactly (at most) $k$, and $\mu$ a probability measure on them. Proportional volume sampling with measure $\mu$ (Definition 1.1) is the distribution $\mu'$ with

$$\Pr_{\mu'}[\mathcal S=S]=\frac{\mu(S)\det(V_SV_S^\top)}{\sum_{S'}\mu(S')\det(V_{S'}V_{S'}^\top)}.$$

The measure $\mu$ is $\alpha$-approximate $(d-1,d)$-wise independent with respect to a feasible $x$ (Definition 1.2) if for all $T,R\subseteq[n]$ with $|T|=d-1$ and $|R|=d$,

$$\frac{\Pr_{\mathcal S\sim\mu}[T\subseteq\mathcal S]}{\Pr_{\mathcal S\sim\mu}[R\subseteq\mathcal S]}\le\alpha\,\frac{x^T}{x^R}.$$

For a square matrix $M$ with eigenvalues $\lambda_1,\dots,\lambda_m$, $E_k(M)$ is the $k$-th elementary symmetric polynomial $e_k(\lambda_1,\dots,\lambda_m)$; $E_m(M)=\det M$.

Algorithm 1 (p. 8) solves the relaxation for $x$, samples $\mathcal S\sim\mu'$, and pads $\mathcal S$ with arbitrary indices to size $k$ if it is smaller.

Formalization targets

Goal: Theorem 1.3

If $x$ is an optimal solution of (1)–(3) and $\mu$ is $\alpha$-approximate $(d-1,d)$-wise independent with respect to $x$, then the output $\operatorname{pad}(\mathcal S)$ of Algorithm 1 satisfies, for every $k$-set $S^{\mathrm{opt}}$,

$$\mathbb E_{\mathcal S\sim\mu'}\Big[\operatorname{tr}\big(V_{\operatorname{pad}(\mathcal S)}V_{\operatorname{pad}(\mathcal S)}^\top\big)^{-1}\Big]\le\alpha\operatorname{tr}\big(V_{S^{\mathrm{opt}}}V_{S^{\mathrm{opt}}}^\top\big)^{-1},$$

so the algorithm is an $\alpha$-approximation in expectation, and some $k$-set has objective at most $\alpha\,\mathrm{CP}$ (the integrality gap is at most $\alpha$). The constant $\alpha$ is a parameter: the goal fixes no value of it, so later constructions of better measures plug into it unchanged.

Milestones

1. Lemma 2.1: $\det(V_T(x)^\top V_T(x))=x^T\det(V_T^\top V_T)$ for $|T|\le d$.
2. Identity (4): $E_k(VV^\top)=E_k(V^\top V)=\sum_{S\in\mathcal U_k}\det(V_S^\top V_S)$.
3. Identity (6): $\operatorname{tr}M^{-1}=E_{d-1}(M)/\det M$ for a $d\times d$ matrix of rank $d$.
4. The expected objective under $\mu'$ is at most $\sum_{|T|=d-1}\det(V_T^\top V_T)\Pr_\mu[\mathcal S\supseteq T]\big/\sum_{|R|=d}\det(V_R^\top V_R)\Pr_\mu[\mathcal S\supseteq R]$ (p. 9).
5. $\operatorname{tr}(V(x)V(x)^\top)^{-1}=\sum_{|T|=d-1}\det(V_T^\top V_T)x^T\big/\sum_{|R|=d}\det(V_R^\top V_R)x^R$ (p. 9).
6. Inequality (5): $\mathbb E_{\mathcal S\sim\mu'}[\operatorname{tr}(\sum_{i\in\mathcal S}v_iv_i^\top)^{-1}]\le\alpha\operatorname{tr}(\sum_ix_iv_iv_i^\top)^{-1}$.
7. $\mathrm{CP}\le\mathrm{OPT}$ (p. 7).
8. Padding a set with further vectors does not increase $\operatorname{tr}(V_SV_S^\top)^{-1}$ (p. 8).

Significance

Theorem 1.3 turns an approximation question about a continuous, spectral objective into a question about the marginals of a distribution on sets: any measure with approximately independent $(d-1)$- and $d$-marginals relative to the relaxation's solution yields an approximation algorithm with the same ratio, and simultaneously bounds the integrality gap of the relaxation. The paper's Theorems 1.4 and 1.5 are proved by applying it to hard-core distributions, giving a $d$-approximation for $k=d$ and a $(1+\epsilon)$-approximation for $k=\Omega\big(\frac d\epsilon+\frac{\log(1/\epsilon)}{\epsilon^2}\big)$.

The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. The formalization produces, beyond the theorem itself, a reusable linear-algebra layer that the pinned Mathlib lacks: the Cauchy–Binet formula for Gram matrices, its extension (4) to all elementary symmetric functions of the spectrum, and the identity $\operatorname{tr}M^{-1}=E_{d-1}(M)/\det M$. These are standard tools for determinantal point processes and volume sampling, and a later formalization of the hard-core constructions (Theorems 1.4, 1.5) would build directly on this mission's goal.

Difficulty

The reduction itself is a short calculation once both sides of (5) are written as ratios of sums over $(d-1)$- and $d$-subsets; the difficulty is in the linear algebra that produces those ratios. Identity (4) needs Cauchy–Binet for non-square matrices together with the relation between the coefficients of the characteristic polynomial, its roots and sums of principal minors; none of this is in Mathlib in the required form, and the eigenvalue side requires that the characteristic polynomial of a real symmetric matrix splits over $\mathbb R$. Applying (4) to every $V_S$ separately and exchanging the order of summation is bookkeeping between index sets of different sizes, which is where informal proofs are quietest. The expectation also has to be handled honestly at sets $S$ with singular $V_SV_S^\top$: they are never sampled, but the paper's displayed equality on p. 9 counts them, so the first display holds only as an inequality.

Formalization scope

Everything is over $\mathbb R$, with index sets Finset (Fin n) and $V$ a Matrix (Fin d) (Fin n) ℝ. A probability measure on $\mathcal U_{\le k}$ is a nonnegative function on subsets of $[n]$ with total mass $1$ vanishing on sets larger than $k$; this covers $\mathcal U_k$ as a special case. $E_k$ is the elementary symmetric function of the real roots of the characteristic polynomial, applied only to symmetric matrices. Lean's matrix inverse is $0$ on singular matrices, so every comparison of objectives assumes positive definiteness of the inverted matrix, and OPT is expressed by quantifying over $k$-sets with positive definite Gram matrix rather than by an infimum.

The statements add the following, each disclosed in the item's Formalization Note: $1\le d$ (for the natural-number subtraction $d-1$); a positive normaliser $\sum_S\mu(S)\det(V_SV_S^\top)>0$, which Definition 1.1 presupposes; positive definiteness of $\sum_ix_iv_iv_i^\top$, which is what a finite CP means; Definition 1.2 in cross-multiplied form; and "$\le$" in place of the printed "$=$" in the first display of p. 9. Theorem 1.3 assumes a suitable $\mu$ only for the optimal $x$, as the remark after the theorem says; this implies the printed form. The padding of Algorithm 1 is an arbitrary map $\operatorname{pad}$ with $S\subseteq\operatorname{pad}(S)$ and $|\operatorname{pad}(S)|=k$ on the support of $\mu$.

The goal is not inequality (5) alone and $E_k$ is not defined as a sum of minors, and the expectation is not defined as the ratio of p. 9; any of those would make milestones true by definition. A sorry-free sanity file shows that all hypotheses of the goal are simultaneously satisfiable ($d=k=n=2$, $V=I$, $x=(1,1)$, $\mu$ the point mass at $[2]$, $\alpha=1$).

Contributions are welcome at every milestone; the Cauchy–Binet layer (milestones 2 and 3) is reusable well beyond this mission and is the natural place to start.

Selected references

• A. Nikolov, M. Singh, U. Tantipongpipat, Proportional Volume Sampling and Approximation Algorithms for A-Optimal Design, arXiv:1802.08318v5, 2018; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1802.08318
• H. Avron, C. Boutsidis, Faster Subset Selection for Matrices and Applications, SIAM Journal on Matrix Analysis and Applications 34(4):1464–1499, 2013. https://arxiv.org/abs/1201.0127
• A. Deshpande, L. Rademacher, Efficient Volume Sampling for Row/Column Subset Selection, FOCS 2010, 329–338. https://doi.org/10.1109/FOCS.2010.38
• Z. Mariet, S. Sra, Elementary Symmetric Polynomials for Optimal Experimental Design, NeurIPS 2017. https://arxiv.org/abs/1705.09677
• F. Pukelsheim, Optimal Design of Experiments, SIAM Classics in Applied Mathematics, 2006. https://doi.org/10.1137/1.9780898719109

Why truthful reports fail in strategy-proof mechanisms

Deferred acceptance and top trading cycles are strategy-proof: submitting one's true preference ranking is optimal whatever the other participants do (Roth, 1982). School-choice and residency-match systems around the world use them for this reason. Yet laboratory and field data show participants misreporting systematically, most often by leaving popular options out of their list or by ranking options with high admission chances above options they prefer (Chen and Sönmez, 2006; Hassidim, Marciano, Romm and Shorrer, 2017; Chen and Pereyra, 2019; survey by Hakimov and Kübler, 2021). One line of explanation treats these reports as mistakes; another looks for preferences under which they are optimal, such as expectation-based loss aversion (Dreyfuss, Heffetz and Rabin, 2022).

V. Meisner's paper Report-dependent utility and strategy-proofness proposes report-dependent utility: on top of the value of the option she is assigned, a participant cares about where that option sits in the list she submitted, enjoying acceptance by her reported top choice and disliking acceptance only at the bottom. The paper's Proposition 2 says exactly when truth-telling survives such preferences, for every strength of the report-dependent component. This mission formalizes Proposition 2 and the steps of its proof.

Setting

A participant ranks $n$ options, labelled $1,\dots,n$. She gets a report-independent payoff $v_s$ from being matched with option $s$, and the options are labelled so that

$$v_1\ \ge\ v_2\ \ge\ \cdots\ \ge\ v_n .$$

A rank-ordered list (ROL) is a bijection $\widetilde R$ from options to ranks $⟦1,n⟧=\{1,\dots,n\}$; its $r$-th ranked option is $\widetilde r=\widetilde R^{-1}(r)$. The true ROL $R=(1,2,\dots,n)$ ranks options by $v$. She also receives a report-dependent payoff $\rho(r)$ when matched with her $r$-th ranked option, where $\rho:⟦1,n⟧\to\mathbb R$ is decreasing.

The other participants' reports are fixed. An option $s$ is attainable ($A_s=1$) if the participant would be matched with it by ranking it first. The attainability distribution $P$ is a probability distribution on the $2^n$ states $(A_1,\dots,A_n)\in\{0,1\}^n$; the $A_s$ may be correlated in any way. In a strategy-proof mechanism she is matched with the highest-ranked attainable option of her list, so her match probability at rank $r$ under $\widetilde R$ is

$$\widetilde f_r = P\bigl(A_{\widetilde r}=1,\ A_{\widetilde t}=0\ \ \forall t<r\bigr),$$

and her expected payoff is

$$U(v\mid\widetilde R)=\sum_{r=1}^n \widetilde f_r\,\bigl(v_{\widetilde r}+\rho(r)\bigr). \tag{1}$$

Under the truth these are $f_r$ and $U(v\mid R)$. The true ROL is optimal if $U(v\mid R)\ge U(v\mid\widetilde R)$ for every $\widetilde R\ne R$.

In Lean, options and ranks are Fin n, a ROL is Rt : Equiv.Perm (Fin n) (option ↦ rank), the truth is 1, $P$ is a function (Fin n → Bool) → ℝ, and $\widetilde f_r$, $U(v\mid\widetilde R)$ are matchProb P Rt r, payoff v ρ P Rt.

Formalization targets

Goal: Proposition 2 (p. 7)

For every non-truthful ROL $\widetilde R$: $U(v\mid R)\ge U(v\mid\widetilde R)$ for all decreasing $\rho$ if and only if

$$\sum_{r=1}^{\bar r}\bigl(f_r-\widetilde f_r\bigr)\ \ge\ 0\qquad\forall\,\bar r\in⟦1,n⟧. \tag{3}$$

Hence the true ROL is optimal for every decreasing $\rho$ if and only if (3) holds against all non-truthful ROLs.

Milestones (steps of the proof, pp. 12–13)

1. First-order stochastic dominance: $\sum_{s\le k}\widetilde f_{\widetilde R(s)}\le\sum_{s\le k}f_s$ for every $k$.
2. $\Delta_v\ge 0$ for decreasing $v$.
3. If (3) fails at some $\bar r$, some strictly decreasing $\rho$ gives $U(v\mid R)<U(v\mid\widetilde R)$.
4. If (3) holds, $U(v\mid R)\ge U(v\mid\widetilde R)$ for every decreasing $\rho$.

Supporting statements (the displays of the proof)

• The decomposition $U(v\mid R)-U(v\mid\widetilde R)=\Delta_v+\Delta_\rho$ with $\Delta_v=\sum_s v_s(f_s-\widetilde f_{\widetilde R(s)})$ and $\Delta_\rho=\sum_r\rho(r)(f_r-\widetilde f_r)$.
• All ROLs have the same total match probability $\sum_r\widetilde f_r$.
• $\Delta_\rho=\sum_{r=1}^{n-1}(\rho(r)-\rho(r+1))\bigl(\sum_{i\le r}f_i-\sum_{i\le r}\widetilde f_i\bigr)$.

Significance

Proposition 2 gives a testable condition, stated only in terms of beliefs about admission, under which no report-dependent taste of any size can break truth-telling: no alternative list may raise the probability of being matched with one of the top $\bar r$ ranked options, for any $\bar r$. Conversely, when an alternative list does raise such a probability, as ranking a safe option first does, a strong enough report-dependent payoff makes that list strictly better than the truth even though the mechanism is strategy-proof. The paper uses this to separate settings in which truthful reports are predicted from those in which self-selection is predicted, and contrasts it with Proposition 1, under which every list is optimal for some beliefs.

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission provides one, together with a reusable finite model of matching under correlated attainability (match probabilities of the highest-ranked attainable option, the expected payoff (1)) and the stochastic-dominance property of the truthful lottery, which other results about rank-ordered lists in strategy-proof mechanisms can import.

Difficulty

The two directions are elementary in spirit but need care. The "only if" direction in the paper takes a limit of decreasing functions $\rho$; a formal proof has to exhibit an actual strictly decreasing $\rho$ and control the report-independent term $\Delta_v$ uniformly. The "if" direction rests on two facts the paper asserts briefly: that the true lottery stochastically dominates every other (which is a statement about the match rule under arbitrarily correlated attainability, not an assumption), and a summation-by-parts rewriting of $\Delta_\rho$ that uses the equality of total match probabilities across lists. The paper's inequalities "$\Delta_v>0$" and the final "$>0$" are strict as printed but hold only weakly, so the formal statements use $\ge$.

Formalization scope

• Model. Options and ranks are Fin n, 0-indexed (Lean index $i$ is the page's $i+1$). A ROL is Equiv.Perm (Fin n) mapping options to ranks; the $r$-th ranked option is R.symm r; the truth is 1. States are Fin n → Bool; $P$ is a real weight function and IsAttainabilityDist P says it is nonnegative with total mass one. Probabilities are finite sums; there is no measure theory.
• Match rule. matchProb P R r is the weight of the states in which the rank-r option is attainable and every option ranked above it is not: the highest-ranked attainable option is matched, as on p. 5. The distribution $P$ does not depend on the submitted list.
• Conventions in the goal. "Decreasing $\rho$" is StrictAnti ρ, the model's standing assumption; the equivalence also holds for weakly decreasing $\rho$. The order $v_1\ge\dots\ge v_n$ is a hypothesis (Antitone v). The normalizations $v_n=0$ and $\rho(1)>0>\rho(n)$ are not imposed: all lists have the same total match probability, so adding a constant to $v$ or $\rho$ leaves $U(v\mid R)-U(v\mid\widetilde R)$ unchanged, and the statement with them is equivalent. "Non-truthful" is Rt ≠ 1. Condition (3) is Condition3 P Rt, with rbar : Fin n the page's $\bar r$ shifted by one and Iic rbar the ranks $1,\dots,\bar r$.
• Not trivial. $P$ is an arbitrary correlated distribution and the match probability is the highest-ranked-attainable rule, so neither side of the equivalence can hold by a degenerate model: for two options with independent fair-coin attainability both sides hold, and for a point mass on "only option 2 attainable" both fail against the swapped list.
• Infrastructure. Only finite sums over Fin n and Fin n → Bool, permutations of Fin n and Mathlib's summation by parts. Proofs of any milestone are welcome, as are alternative proofs of the goal that bypass the decomposition.

Selected references

• V. Meisner, Report-dependent utility and strategy-proofness, CRC TRR 190 Discussion Paper No. 289, 2021; Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4504
• A. E. Roth, The economics of matching: stability and incentives, Mathematics of Operations Research 7(4), 1982. https://doi.org/10.1287/moor.7.4.617
• Y. Chen, T. Sönmez, School choice: an experimental study, Journal of Economic Theory 127(1), 2006. https://doi.org/10.1016/j.jet.2004.10.006
• A. Hassidim, D. Marciano, A. Romm, R. I. Shorrer, The mechanism is truthful, why aren't you?, American Economic Review 107(5), 2017. https://doi.org/10.1257/aer.p20171027
• L. Chen, J. S. Pereyra, Self-selection in school choice, Games and Economic Behavior 117, 2019. https://doi.org/10.1016/j.geb.2019.06.004
• R. Hakimov, D. Kübler, Experiments on centralized school choice and college admissions: a survey, Experimental Economics 24(2), 2021. https://doi.org/10.1007/s10683-020-09667-7
• B. Dreyfuss, O. Heffetz, M. Rabin, Expectations-based loss aversion may help explain seemingly dominated choices in strategy-proof mechanisms, American Economic Journal: Microeconomics, 2022. https://doi.org/10.1257/mic.20200259

Why support geometry matters

A probability distribution can spread its mass while remaining inside a set of limited diameter. A bound on the diameter alone does not specify its center, shape, or number of support points. Lim and McCann ask how large a recentered moment can become under this sparse geometric information. Their answer identifies a regular simplex as the extremal configuration: in dimension two it is an equilateral triangle, and in dimension three a regular tetrahedron. This gives an exact higher-dimensional analogue of the familiar one-dimensional observation that a distribution on an interval maximizes variance by placing equal mass at the endpoints. The paper frames the question in connection with systems of particles or organisms that prefer separation from one another, where a diameter constraint limits how far their spatial distribution can spread (Lim and McCann, 2020, pp. 5–7).

The mission follows the first arXiv version of the paper. The theorem is already proved in the source. The formalization task is to express its sharp bound and its equality case precisely in Lean, together with the geometric statements that distinguish the simplex from other diameter-constrained supports.

The objects being compared

Work in Euclidean space $E_n=\mathbb R^n$ with its ordinary distance. For a Borel probability measure $\mu$, its support $\operatorname{spt}\mu$ is the smallest closed set carrying all its mass. The diameter of the support is the supremum of the distances between its points. A bounded diameter places no restriction on where the support sits in space: translating the distribution leaves the diameter unchanged.

For a nonnegative convex function $V:E_n\to[0,\infty)$, the generalized variance allows the center to move:

$$\operatorname{Var}_V(\mu) =\inf_{z\in E_n}\int_{E_n}V(x-z)\,d\mu(x).$$

The center minimizing this integral can depend on $V$ and need not be the ordinary barycenter. For $V(x)=\|x\|^2$ it is the barycenter and the expression is classical variance. This mission focuses on radial functions $V(x)=v(\|x\|)$, where $v$ is convex and increasing on nonnegative radii. The paper's definition and the relation to classical variance appear in equation (1.8) and Remark 1.6 (pp. 4–5).

A regular $n$-simplex in $E_n$ has $n+1$ vertices, and every pair of distinct vertices has the same positive distance $d$. Its uniform vertex measure assigns mass $1/(n+1)$ to each vertex. Write

$$r_n=\sqrt{\frac{n}{2n+2}}.$$

This is the distance from the centroid to each vertex when the simplex has side length one. The paper defines regular and unit simplices in Definition 1.8 and identifies this radius in Proposition 3.1 (pp. 6, 13).

Formalization targets

Sharp diameter bound

For a Borel probability measure $\mu$ with $\operatorname{diam}(\operatorname{spt}\mu)\le d$, the target is

$$\operatorname{Var}_{v\circ\|\cdot\|}(\mu)\le v(r_nd).$$

Here $d\ge0$, so the argument $r_nd$ belongs to the domain on which $v$ is specified. The bound fixes the optimal constant in every dimension and for each eligible radial cost (Theorem 1.10, pp. 6–7).

Equality and its geometric milestones

When $d>0$ and $v$ is differentiable at $r_nd$, equality is characterized by a regular $n$-simplex with side length $d$:

$$\operatorname{Var}_{v\circ\|\cdot\|}(\mu)=v(r_nd) \quad\Longleftrightarrow\quad \mu=\frac{1}{n+1}\sum_{i=0}^{n}\delta_{x_i}, \qquad \|x_i-x_j\|=d\quad(i\ne j).$$

The source's proof uses a maximization principle for generalized variance (Theorem 1.7), a constraint placing a minimizing center inside the support's closed convex hull, the two parts of Proposition 3.1 on spherical sets, and the uniqueness of barycentric weights in Remark 3.2. Those statements are the five milestones. Their order follows the progression from the measure problem to the limiting geometry and finally to equal mass (pp. 5, 13, 15).

What the result gives

The bound controls every convex radial recentered moment allowed by the hypotheses using only the diameter and dimension. Its equality clause identifies the entire extremal distribution, rather than merely the value of the maximum. For squared distance, this recovers a sharp variance statement; for powers of the distance, it supplies corresponding recentered moment bounds (Example 1.11, p. 7). The geometric threshold $r_n$ also links the paper's result to Jung's enclosing-ball theorem, which the authors discuss separately (Theorem 1.12 and §3.1, pp. 7, 15–16).

A complete Lean proof would connect measure-theoretic optimization to finite-dimensional convex geometry. It would provide reusable formal statements for generalized variance, support-constrained probability measures, simplex geometry, and the equality mechanism. The source paper proves these results mathematically. In this mission, the Lean statements are drafted and compile with proof placeholders; they do not yet have machine-checked proofs.

Where the difficulty lies

The diameter restriction is imposed on the support, which need not be convex. Replacing it by a restriction on a convex set loses the particular geometry that makes the simplex extremal. The minimizing center is also part of the optimization: evaluating the integral at the barycenter would change the object for a general radial cost. In the equality case, knowing only that the support lies on a sphere is insufficient. The radius must reach exactly $r_n$, the spherical support must be precisely the $n+1$ simplex vertices, and the mass at those vertices must be equal. Proposition 3.1 and Remark 3.2 isolate these separate assertions (pp. 13–15).

Formalization scope

Lean represents $E_n$ as EuclideanSpace ℝ (Fin n), with the Euclidean norm and Borel measurable space. The support diameter in the goal is the extended metric diameter, which correctly excludes unbounded supports from a finite bound. The paper's $\operatorname{conv}(K)$ is its smallest closed convex hull, so the statements use closedConvexHull. Probability measures supported on $K$ carry the condition $\mu(K^c)=0$. The generalized variance is the infimum over all centers $z\in E_n$; restricting centers to the support hull or replacing the infimum by the integral at the mean would give a different and potentially easier claim.

The function $v$ is modeled on all real numbers because Lean functions are total, but every value used by the mathematical statements is at a nonnegative radius. The hypotheses require nonnegativity, convexity, and strict increase on $[0,\infty)$; the latter makes the paper's equality conclusion meaningful. The equality clause additionally assumes differentiability at $r_nd$. Without it, a kinked strictly increasing convex $v$, with a change of slope at that radius, can have unequal masses attaining the same optimum. The manuscript states the clause without this condition. Theorem 1.7 explicitly assumes $K$ nonempty, and the goal explicitly records $d\ge0$ and $d>0$ where they are needed. Theorem 1.7's support level set follows the sign proved on p. 12, $V(x-z_*)=\lambda$; the printed translated set has the opposite sign.

The definitions and theorem files contain no custom probability or simplex infrastructure beyond these source objects. Contributions proving the optimization principle, the center-in-hull claim, either part of the spherical geometry proposition, or the barycentric uniqueness statement are within scope. Theorem 1.1, the paper's separate convex-envelope result, and the deduction of Jung's theorem are outside this mission.

Selected references

• Tongseok Lim and Robert J. McCann, Geometrical bounds for the variance and recentered moments, arXiv:2001.11851v1, 2020; published in Mathematics of Operations Research, 2022. arXiv version.

Motivation

In many emerging economies, smallholder farmers decide each season how much of their land to give to an export crop, sold through a local processor at a price linked to the world market, and how much to keep for a traditional alternative crop. Yields are uncertain and often correlated across neighbouring regions because they share weather. Governments and development agencies frequently protect farmers with a minimum guaranteed price: no processor may pay less than $p_o$ per unit of harvest. Whether such a floor encourages too little, enough, or too much planting relative to the processing capacity of the region is a policy question with direct consequences for farm income and processor utilization.

Li, Kouvelis and Dada (SSRN 3531158; published in Manufacturing & Service Operations Management 26(2), 2024, doi:10.1287/msom.2022.0076) model this as a two-stage game between two farmers and two capacity-constrained processors, and characterize the land-allocation equilibria in closed form for all-or-nothing yields. This mission formalizes that characterization, together with the second-stage pricing results it is built on.

Setting

There are two regions $i\in\{1,2\}$, each with one farmer and one processor. The processed crop sells at the world price $p^e$. Processor $i$ has unit processing cost $c_i$ and capacity $K_i>0$, with $c_1\le c_2$, and the minimum guaranteed price satisfies $0\le p_o\le p^e-c_2$.

Second stage. Farmer $i$ has planted $x_i$ units of land and harvests $y_i=x_iY^e_i$, where $Y^e_i$ is the random yield. Both farmers sell first to the winning processor (Processor 1 on ties); a winner who cannot absorb the whole harvest first takes the harvest of its own region's farmer, and the residual goes to the losing processor up to its capacity (Theorem 1 of the paper). Processor $i$'s profit $g_i(p_1,p_2)$ is its margin $p^e-c_i-p_i$ times the amount it procures. Its willingness to pay $\bar p_i$ is the highest price $p\in[p_o,p^e-c_i]$ at which winning at $p$ is no worse than losing at $p_o$ (conditions (7)–(8)). The processors then settle as in a second-price auction (Theorem 3): if $\bar p_1\ge\bar p_2$, Processor 1 wins and the final prices are $(p^*_1,p^*_2)=(\bar p_2,p_o)$; otherwise Processor 2 wins and they are $(p_o,\bar p_1)$. Farmer $i$'s revenue $f_i$ is the sum of her sales to the two processors at the final prices.

First stage. Farmer $i$'s expected profit is

$$F_i(x_1,x_2)=E\big[f_i(x_1Y^e_1,x_2Y^e_2)\big]-x_iU_i+A_i ,$$

where $U_i$ is the per-unit cost of export-crop land, including the forgone alternative crop, and $A_i$ is a constant. An equilibrium is a pair $(x^*_1,x^*_2)\in[0,L_1]\times[0,L_2]$ in which each $x^*_i$ maximizes $F_i$ given the other farmer's choice.

All-or-nothing (AON) yields. Each $Y^e_i$ takes the value $H>0$ or $0$. In the symmetric IID chain the processors are identical ($c_1=c_2=c$, $K_1=K_2=K$), the farmers are identical ($U_1=U_2=U$, $A_1=A_2=A$), and the yields are independent with $P(Y^e_i=H)=h\in(0,1)$.

Formalization targets

Goal: Theorem 6, parts 1, 3, 4 (p. 20)

In the symmetric IID chain with $U>0$, $L_i\ge 2K/H$ and the participation condition $p^e-c>U/(hH)$:

$$p_o<\frac{U}{h^2H}-\frac{1-h}{h}(p^e-c)\ \Longrightarrow\ \text{all equilibria satisfy } x^*_1+x^*_2=\tfrac KH,\ \text{and a nondegenerate segment of that line consists of equilibria};$$ $$\frac{2h-1}{2h}(p^e-c)+\frac{U}{2h^2H}\le p_o<\frac12\Big[(p^e-c)+\frac{U}{h(1-h)H}\Big]\ \Longrightarrow\ \big(\tfrac KH,\tfrac KH\big)\ \text{is the unique equilibrium};$$ $$p_o>\frac12\Big[(p^e-c)+\frac{U}{h(1-h)H}\Big]\ \Longrightarrow\ \big(\tfrac{2K}H,\tfrac{2K}H\big)\ \text{is the unique equilibrium}.$$

Milestones

1. Theorem 2 (p. 14): the WTPs equal the closed forms (9)–(10) whenever the total harvest is positive.
2. Lemma 1 (p. 14): $\bar p_1-\bar p_2$ depends on the total harvest only, is continuous, and changes sign at most once, from $+$ to $-$.
3. Theorem 4, part 1 (p. 15): if $(p^e-c_1-p_o)/K_1\ge(p^e-c_2-p_o)/K_2$, Processor 1 wins at every harvest.
4. §3.1 (p. 19): in the symmetric chain $\bar p_1=\bar p_2$, and Processor 1 wins at prices $(\bar p_2,p_o)$.
5. §3 (p. 18): under AON yields, $F_1=h_{an}f_1(x_1H,0)+h_{aa}f_1(x_1H,x_2H)-x_1U_1+A_1$, and similarly for $F_2$.
6. §3.1 (p. 19): $F_i$ decreases at rate $U$ beyond $2K/H$, so every equilibrium has $x^*_i\le 2K/H$.
7. Lemma 2 (p. 19): if $p^e-c<U/(hH)$, then $(0,0)$ is the unique equilibrium. This is the no-production region, the complement of the goal's participation condition.

Significance

The theorem shows that the price floor is the decisive policy lever. A low floor leaves farmers with thin margins and produces under-planting together with a whole continuum of equilibria, so total production is pinned down but its split between regions is not. Intermediate floors coordinate both farmers on filling exactly the processing capacity. A high floor makes planting so attractive that both farmers plant enough to fill both processors on their own, and part of the harvest goes unsold whenever both crops succeed. These regimes underlie the paper's later comparisons of ownership structures and yield correlations (§4–§5).

The result is proved on paper; it has no machine-checked proof. Formalization adds a precise model of a second-stage protocol that is described partly in prose, and it pins down the boundary cases. Checking the printed statement already corrected three points: part 2 of Theorem 6 is false as printed, the participation condition must be strict for part 1, and the threshold of part 4 must be strict.

Difficulty

The profits $F_i$ are piecewise linear in $(x_1,x_2)$, but the pieces come from nested $\min$ and $(\cdot)^+$ operations in the allocation rule, multiplied by a WTP that is itself a ratio of such terms. Each farmer's best response is therefore discontinuous and has to be found region by region. The two farmers are not symmetric even in the symmetric chain, because Processor 1 wins every tie and so farmer 1's harvest is served first. Equilibrium claims are global: "unique equilibrium" requires excluding every other point of $[0,L_1]\times[0,L_2]$, including allocations above $2K/H$ and corners where a farmer plants nothing. The WTPs are defined as suprema, so identifying them with (9)–(10) is a separate optimization over all competing prices.

Formalization scope

All quantities are real numbers. The model is one definition, AgriChain.LandAlloc.Model: the chain, the allocation of Theorem 1 indexed by the winning processor, the profits (5)–(6), the WTP sets defined by (7)–(8) and the WTPs as their suprema, the final prices of Theorem 3 with ties going to Processor 1, the revenues (11)–(12), AON yield laws, the expected profits (13)–(14) as finite sums over the four yield outcomes, and the equilibrium. The equilibrium is the published generic pure-Nash predicate CarbonDoubleCount.Planner.IsPureNash, with feasible sets $[0,L_i]$. $U_i$ and $A_i$ are real parameters, as in the paper from (13) on.

Hypotheses added to the goal: $0<h<1$, $H>0$, $K>0$ and $U>0$ (the thresholds divide by $h$, $H$ and $h(1-h)$, and the bound $x^*_i\le 2K/H$ needs $U>0$); $L_i\ge 2K/H$ (the over-production equilibrium plants $2K/H$); the participation condition $p^e-c\ge U/(hH)$ of p. 19, made strict; and part 4's threshold, made strict. "Unique equilibrium" is an "if and only if", asserting existence. Part 2 of Theorem 6 is not posed: at $h=1/2$, $H=K=U=1$, $p^e-c=5$, $p_o=0$ its hypotheses hold, but the unique equilibrium is $(4/5,3/5)$, whose total $7/5$ is below $3K/(2H)$. Theorem 5 (p. 18) and part 2 of Theorem 4 are not posed either.

The goal is about the equilibria of the full model. Defining the WTPs by (9)–(10), defining $F_i$ by the two-term AON form, or stating Theorem 6 for a hand-simplified symmetric profit would make the milestones definitional and is ruled out. Contributions are welcome on every milestone. The WTP computation and the AON reduction are reusable for the paper's other correlation structures (§4–§5).

Selected references

• J. Li, P. Kouvelis, M. Dada, Agricultural Supply Chains in Emerging Markets: Competition and Cooperation under Correlated Yields, SSRN working paper 3531158, version of 2023-01-03. https://ssrn.com/abstract=3531158
• J. Li, P. Kouvelis, M. Dada, same title, Manufacturing & Service Operations Management 26(2):664–680, 2024. https://doi.org/10.1287/msom.2022.0076
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• R. P. McAfee, J. McMillan, Auctions and bidding, Journal of Economic Literature 25(2), 1987. https://www.jstor.org/stable/2726107

Why product-support contracts matter

A repair supplier can invest in capacity before a service contract begins, while the customer may know more about how often her equipment fails. The supplier must choose both an incentive to maintain uptime and a menu that gives customers reason to reveal their failure rates. Li, Mishra, and Netessine study this interaction for maintenance, repair, and overhaul services. Their model compares a price per repair with a performance-based contract (PBC), under which the supplier is paid for the product's uptime. The latter ties revenue to the outcome the customer values. The paper asks when that arrangement can preserve the full-information outcome despite asymmetric information about product reliability. Li, Mishra, and Netessine, SSRN author version, §§1, 3, 5.

The specific result targeted here is Proposition 5(i). The two customer types differ both in failure rate and in the value of their outside options. This creates countervailing incentives: the customer with the less reliable product need not always be the one seeking a better contract. The paper identifies a range of outside-option ratios in which a single separating PBC menu gives each type the same contract she would receive if the supplier knew her type. Li, Mishra, and Netessine, Proposition 5(i), p. 18.

The contracting setting

A contract period has length one. A product has failures at a rate $\lambda$, and the supplier sets a repair rate $\mu$ by investing in capacity. Each repair requires a random lead time. The product's uptime $A$ is one minus total downtime. The paper's expected-uptime expression is $E[A\mid\lambda,\mu]=1-\lambda/\mu$. It uses this expression to turn the stochastic model into the closed-form payoffs of its supplementary equation (B.39). Li, Mishra, and Netessine, §3, pp. 7–10, and supplement (B.39), p. 9.

There are two types, $L$ and $H$, with $0<\lambda_L<\lambda_H$. The probability of the low-failure type is $\beta\in(0,1)$. Type $\tau$ can decline the contract and obtain her reservation payoff $M_\tau$; the setting has $0<M_H<M_L$. The supplier receives $v_\tau$ per unit uptime from a customer choosing contract $\tau$ and incurs a capacity cost $c\mu_\tau$ plus expected material cost $c_r\lambda_\tau$. The customer's payoff, evaluated at her actual failure rate $\lambda$, is $(r-v_\tau)(1-\lambda/\mu_\tau)$, where $r$ is revenue per unit uptime. The supplier's corresponding payoff is $v_\tau(1-\lambda/\mu_\tau)-c_r\lambda-c\mu_\tau$. Li, Mishra, and Netessine, §§3–4 and supplement (B.39).

A menu contains one positive-price, positive-rate contract for each type. Individual rationality (IR) requires that each type's payoff from her designated contract reach her reservation payoff. Incentive compatibility (IC) requires that neither type prefer the other contract. In problem (9), the supplier maximizes her prior-weighted payoff over all menus satisfying both IR and both IC constraints. Under full information, the two types can be optimized separately; Proposition 1(ii) gives the first-best PBC repair rate $\mu_\tau^0=\sqrt{r\lambda_\tau/c}$ and the price $v_\tau^0=r-M_\tau\mu_\tau^0/(\mu_\tau^0-\lambda_\tau)$. Li, Mishra, and Netessine, Proposition 1, p. 12; problem (9), p. 18.

Formalization targets

The goal formalizes Proposition 5(i). Define the first-best menu by offering $(v_L^0,\mu_L^0)$ to type $L$ and $(v_H^0,\mu_H^0)$ to type $H$. Condition (10) is

$$\frac{\mu_H^0-\lambda_L}{\mu_H^0-\lambda_H} \leq \frac{M_L}{M_H} \leq \frac{\mu_L^0-\lambda_L}{\mu_L^0-\lambda_H}.$$

When this condition holds and both first-best prices are positive, the first-best menu is feasible for problem (9) and achieves at least the supplier payoff of every feasible menu. Both IR constraints bind, so each customer's information rent is zero; the two repair rates differ, so the menu separates the types. Li, Mishra, and Netessine, Proposition 5(i), p. 18.

The milestones follow the paper's stated calculations: the binding-IR price and reduced objective from (B.6)–(B.7); the PBC part of Proposition 1(ii)–(iii); the two IC slack formulas (B.41) and (B.42); and the first-best payoff bound used at the end of the proof of Proposition 5(i). The joint-profit benchmark is $\Pi_\tau^0=r-2\sqrt{cr\lambda_\tau}-c_r\lambda_\tau$. Li, Mishra, and Netessine, supplement pp. 3–4 and 9.

What the result provides

The result identifies a parameter region in which screening does not reduce productive efficiency or leave an information rent to either customer type. The supplier can offer the same repair capacities and prices as in the full-information problem while satisfying each type's participation and truthful-choice requirements. This makes the full-information outcome a concrete benchmark for the other regions of Proposition 5, where one or more constraints bind differently. Li, Mishra, and Netessine, Proposition 5, pp. 18–19.

The mathematical result is proved in the paper. This mission asks for machine-checked proofs of the model identities and the first region of its screening theorem. The reusable artifacts are the explicit PBC menu, the four feasibility constraints, the separation between supplier and joint profit, and a uniform upper bound over every feasible menu. No existing platform theorem found in the local prior-art index has this paper's contract space and payoffs.

Where the difficulty lies

The first-best solution optimizes a contract separately for each known type. With private failure rates, a customer can choose the contract intended for the other type; solving the two full-information problems alone therefore does not establish a feasible screening menu. The signs of both IC slacks must agree with the ratio interval in condition (10), and every denominator in the ratio and in the first-best prices must be nonzero. Feasibility still is not enough for the conclusion: optimality compares the candidate with all positive-price, positive-rate menus satisfying the four constraints, including menus with slack IR constraints. Li, Mishra, and Netessine, problem (9), p. 18, and supplement (B.39)–(B.43), p. 9.

Formalization scope

The Lean development uses real-valued prices, rates, costs, payoffs, and prior weights. It represents expected uptime and expected payoffs by the paper's closed form (B.39), $1-\lambda/\mu$; it does not encode the underlying Poisson failure process or random repair times in this first mission. The model keeps a separate customer payoff, supplier payoff, and joint-profit function, so $\pi_s^P$ is never confused with $\Pi^0$. The menu's feasibility predicate contains exactly the four constraints of problem (9), plus the strict positivity of both prices and both repair rates written under its maximization sign. The objective uses the prior weights $\beta$ and $1-\beta$. Li, Mishra, and Netessine, §§3–5.2 and supplement (B.39).

The standing predicate makes the parameter domain explicit: $r,c>0$, $c_r\geq0$, $0<\lambda_L<\lambda_H$, $0<\beta<1$, and $0<M_H<M_L$. The order of the two outside options is stated in the paper's setting; $M_H>0$ is needed for the ratio $M_L/M_H$ in (10). The goal also assumes $v_L^0,v_H^0>0$, because a first-best menu with a nonpositive price is not in problem (9)'s admissible set. The algebraic IC milestones explicitly exclude zero denominators, and the goal's ratio condition with the standing order rules out its degenerate denominator cases.

The candidate's optimality is stated against every feasible menu. Restricting competitors to first-best-form or binding-IR menus would make the main theorem weaker. Useful contributions include proofs of the source's algebraic identities, the first-best profit properties, the global upper bound, and Proposition 5(i) itself. The omitted stochastic expected-uptime identity and the remaining cases of Proposition 5 are separate formalization work; the present goal uses the closed form printed by the paper.

Selected references

• Li, D., N. Mishra, and S. Netessine, Contracting for Product Support under Information Asymmetry, Management Science, 2022, author version SSRN 2881356, doi:10.1287/mnsc.2022.4606.

Motivation

When a bank run forces asset sales, the sale price can reflect buyers’ beliefs about the condition of other banks as well as the assets being sold. In the two-bank model of Li and Ma, observing two runs makes buyers more pessimistic about the aggregate state than observing one. That change in beliefs lowers the market price precisely when both banks need liquidity. The paper studies whether a regulator can commit in advance to a purchase price that reduces joint failures while recovering its expected expenditure. Its Proposition 3 gives a specific break-even policy in a limiting version of the model.

The paper proves the policy result in its accepted manuscript, dated 28 October 2021, and was published in Management Science in 2022. The result is mathematically known. The work here is to state its price, payoff, and risk claims as machine-checkable theorems with the paper’s parameter restrictions visible.

Setting

There are two banks and two aggregate states, good $G$ and bad $B$. In state $s$, each bank’s asset portfolio produces a cash flow uniformly distributed between a state-dependent lower bound $\underline\theta_s$ and a common upper bound $\bar\theta$. The good state has the higher lower bound: $0<\underline\theta_B<\underline\theta_G$. Conditional on the state, the banks’ cash flows are independent. The prior probability of $G$ is $\alpha\in(0,1)$; the probability of $B$ is $1-\alpha$. These are the primitives of §2.1 of Li and Ma.

Each bank finances a unit portfolio using equity $E$, retail deposits $F$, and positive wholesale debt $1-E-F$. A wholesale creditor who withdraws early receives a gross factor $qr_D$, while one who waits receives $r_D$, where $r_D>1$ and $q<1$. The debt obligations used throughout are

$$D_1=(1-E-F)qr_D,\qquad D_2=(1-E-F)r_D+F.$$

Assumptions (1)–(3) say $D_2>\underline\theta_s$ in both states, $F>D_1$, and $q>\tfrac12+\underline\theta_G/(2D_2)$. The candidate market-price interval begins at $\underline P=(\underline\theta_B+D_2)/2$ and ends below $qD_2$. The upper-cash-flow condition in footnote 29 is $\bar\theta>F/(1-D_1/\underline P)$. It keeps the uniform probabilities within their intended range on this interval. Footnotes 25 and 27 explain why the interval is nonempty and $\underline P>D_1$; see pp. 13 and 15 of the accepted manuscript.

Buyers who observe $M\in\{1,2\}$ bank runs use a posterior probability $\omega_M^B$ of state $B$, with $\omega_M^G=1-\omega_M^B$. Their expected profit from buying one unit at price $P$ is $\Pi_M(P)$. A market break-even price $P_M^*$ solves $\Pi_M(P_M^*)=0$ in $[\underline P,qD_2)$. The two prices differ because the number of runs changes buyers’ posterior. In the paper’s $\epsilon,\eta\to0$ regime, a committed regulator price $P_A$ gives the critical cash flow

$$\theta^*(P_A)=\frac{D_2-D_1}{1-qD_1/P_A}.$$

The regulator’s expected payoff $V_A(P_A)$ averages purchase gains over the two states and the possibilities of one or two runs, exactly as in equation (22). The systemic-failure probability $\mathrm{SYS}(P_A)$ is the prior-weighted probability that both banks’ cash flows fall below $\theta^*(P_A)$, using the closed uniform formula on p. 26 of Li and Ma.

Formalization targets

The milestone path establishes the existence of the two market prices, their ordering, the payoff identity (23), the signs of $V_A$ at those prices, and the monotonicity of payoff and systemic risk. The main target is Proposition 3: a unique regulator price lies strictly between the market prices,

$$P_2^*<P_A^*<P_1^*,\qquad V_A(P_A^*)=0.$$

Both $V_A$ and $\mathrm{SYS}$ decrease strictly as the committed price rises through $[\underline P,qD_2)$. Among all prices in the regulator’s program (20)–(21),

$$P_A\ge P_2^*,\qquad V_A(P_A)\ge0,\qquad \theta^*(P_A)\ge D_2,$$

the price $P_A^*$ minimizes $\mathrm{SYS}$ and satisfies $\mathrm{SYS}(P_A^*)<\mathrm{SYS}(P_2^*)$. This is the limit interpretation of the comparison printed at the end of Proposition 3.

Significance

The theorem identifies a precommitted price at which the regulator breaks even across possible numbers of runs, while a buyer who acts after observing the run count must break even conditional on that count. The resulting interval between $P_2^*$ and $P_1^*$ is where liquidity support can lower joint failures without an expected transfer. The program also excludes saving banks whose cash flow is below $D_2$; the policy result meets that solvency restriction.

A checked formalization would make the paper’s assumptions and the links among posterior prices, regulator payoff, and systemic risk explicit. Proposition 3 is proved in the paper; its Lean proof and the supporting results in this mission remain to be completed. The definitions of the uniform two-state model, posterior weights, and payoff sums can support later formal work on related liquidity policies, while the paper-specific financial parameters remain tied to this model.

Difficulty

The regulator cannot choose a price from the simple interval between two fixed asset values. Each price changes the cash-flow threshold at which runs lead to failure, which changes the posterior beliefs used in $\Pi_M$ and the probabilities weighting $V_A$. A direct comparison of $P_A$ with either market price therefore does not determine the sign of the regulator’s total payoff. The proof must control both market-contingent profits and their state and run-count weights before the break-even price and its risk effect can be certified.

Formalization scope

Lean represents the aggregate state by a two-constructor type and the primitive bank data by one parameter structure. The standing predicate includes assumptions (1)–(3), $r_D>1$, $q<1$, $0<\underline\theta_B<\underline\theta_G$, $0<\alpha<1$, footnote 29, and positive wholesale debt. The last condition makes the model’s financing convention explicit. The formulation uses the paper’s closed forms in the $\epsilon,\eta\to0$ limit; it does not encode creditor signals or the full global game.

Uniform probabilities are not clipped, because the relevant threshold lies inside the cash-flow support on the stated price interval. The market prices are characterized by their break-even equations rather than chosen from a prior existence assumption: a milestone establishes their existence. $V_A$ is defined by equation (22), not the later identity (23), and the policy goal asserts existence and uniqueness of its zero. The feasible set is exactly program (20)–(21). Strict decrease means strict antitonicity on $[\underline P,qD_2)$. Lean’s real division is total at zero, so the critical-threshold formula has junk values at singular inputs; every claim uses the economically valid interval. Useful contributions include proofs of the market-price milestones, the payoff identity and signs, and the two monotonicity results.

Selected references

• Z. Li and K. Ma, Contagious Bank Runs and Committed Liquidity Support, author’s accepted manuscript, 28 October 2021, WRAP 165968; published in Management Science, 2022, doi:10.1287/mnsc.2021.4258.

Motivation

A firm can have valuable operations yet fail when a temporary cash shortfall leaves it unable to pay its bills. Cash reserves protect the firm, but holding them is costly. In Lee and Rivera’s study, the manager also doubts the probability model for future shocks. The manager evaluates a policy under the least favorable model within a prescribed set of plausible models. This makes the composition of pessimism a decision linked to the firm’s cash position. The paper’s central qualitative claim is that adverse beliefs respond to recent shocks in a way resembling extrapolation bias: a recent shock changes the manager’s assessment of future shocks of the same type.

The result belongs to the paper’s 2019 working version, Extrapolation Bias and Dynamic Liquidity Management. The later Management Science article has a different title. The theorem and equation numbers here refer to the working version, especially §2, §3.3, §4.1 and Appendix A.

Setting

The firm has a positive size δ and cash reserves M. Its cash ratio is m=M/δ. The manager chooses an investment rate i, which raises expected size growth but incurs an expenditure g(i)=i+θi²/2. The size process has a permanent shock with volatility σδ; operating cash flow has an independent temporary shock with volatility σY. The manager discounts at rate r. Cash earns r−λ, so λ is its carry cost. At cash exhaustion the firm either issues equity, paying proportional and fixed costs ρ₁ and ρ₀, or liquidates for a fraction ω of the ambiguity-only benchmark value δqᴬ. These objects and their cash-management interpretation follow the working paper’s model and HJB equations.

The manager allows drift changes h=(hᴾ,hᵀ) in an ambiguity ellipse,

$$H=\{h:(h^P/\kappa_P)^2+(h^T/\kappa_T)^2\leq1\}.$$

The superscripts P and T mean permanent and temporary. The two radii κP and κT limit how much each drift can be distorted. A distortion h changes expected size growth by σδhᴾ and expected cash flow by σYhᵀ. The manager chooses i against the least favorable h. On the ellipse boundary, the model writes hᴾ=−κP cos φ and hᵀ=−κT sin φ for an angle φ in [0,2π].

The paper uses a scaled value function F: firm value at size δ and cash M is δF(M/δ). In the no-payout region 0≤m≤m*, F satisfies the max-min Hamilton–Jacobi–Bellman equation (25), with payout boundary m*. The conditions at m=0 compare refinancing with liquidation, and the value is linear in cash above m*. The ambiguity-only benchmark qᴬ is determined by the paper’s equations (36)–(38). For an increasing concave F, the worst-case angle and distortions are defined by (26)–(27).

Formalization targets

Main claim: endogenous extrapolation bias

For every cash ratio in the no-payout region, the angle from (26) is the unique minimizer of the HJB expression among admissible angles. Its associated worst-case distortions satisfy four shock-response inequalities:

$$S_{PP}(m)\geq0,\qquad S_{PT}(m)\leq0,\qquad S_{TP}(m)\leq0,\qquad S_{TT}(m)\geq0 \quad(0\leq m\leq m^*).$$

Here the first subscript names the belief component and the second names the shock. The four coefficients are the derivatives in the display on p. 21, multiplied by the corresponding shock loading of the cash ratio. When F″(m)<0, the temporary-shock inequalities are strict. The permanent-shock inequalities are strict when also m>0. This states the paper’s §4.1 claim at the boundaries where its printed strict wording would otherwise fail.

Supporting results

The attack path follows four statements in the working paper: Lemma 4 equates minimization over the filled ellipse with minimization over its angle-parametrized boundary; Proposition 3 (19) gives the investment and belief-allocation conditions for the two-state HJB; equations (26)–(27) give their scaled counterparts; and §4.1 describes how beliefs change as the cash ratio rises. The milestone list retains the printed passages verbatim and identifies the necessary corrections in its titles.

Significance

The result identifies which adverse cash-flow model the manager uses at a given cash position. With little cash, temporary losses can force costly financing or liquidation, and the adverse model weighs them more heavily. With more cash, the adverse model shifts toward permanent shocks to firm size. The sign pattern translates that change in beliefs into responses to realized shocks. It supplies a precise meaning for the paper’s claim of endogenous extrapolation bias within this cash-management model.

The paper gives analytical HJB conditions and illustrates the time-varying beliefs in Figure 4.1. This mission asks for Lean proofs of the qualitative allocation and sensitivity statements for the paper’s stated variational system. The local formalization records three corrections to the working paper’s formulas and prose, so solvers have a single explicit target rather than relying on incompatible printed expressions.

Difficulty

The obvious appeal to worst-case beliefs does not by itself establish which point of the ellipse minimizes the HJB expression, whether that point is unique, or whether its angle remains in the required quadrant. The HJB also mixes investment and belief allocation, while the target concerns derivatives of the belief allocation with respect to the cash ratio. Finally, the printed strict signs fail at m=0 and at a smooth payout boundary where F″(m*)=0. The theorem must account for both endpoints while preserving the paper’s interior claim.

Formalization scope

Lean represents parameters in a structure, the ellipse as a subset of ℝ×ℝ, and F as a global C² real function restricted to nonnegative cash. The scaled solution predicate includes monotonicity, concavity, the attained max-min equation (25), and the boundary conditions (28)–(31). The HJB angle interval is the closed [0,2π] of (25). No real supremum of an empty or unbounded set is used. The benchmark predicate records (36)–(38) and the positive transversality gap r−µ−iᴬ.

The working paper has three relevant slips. Lemma 4’s h-form HJB omits the volatility multipliers present in (11)–(12), so the formal statement restores them and uses the paper’s γ=2 restriction. Proposition 3 (19) prints an extra δ in the investment condition; the formal statement uses the condition implied by (18). The last sentence of §4.1 p. 20 reverses the belief monotonicity directions implied by the preceding prose and the p. 21 sensitivity display; the formal statement follows the latter. Strictly positive κP, κT, σY, ω and qᴬ specify the nondegenerate regime in which the arctangent formula and liquidation value carry their intended meaning.

The scaled solution predicate prevents an arbitrary concave function from replacing the paper’s value function. The target requires the displayed angle to be the actual unique minimizer of (25), and its divisions have positive denominators under the model assumptions. Reusable work includes the ellipse minimization and real-analysis facts behind the angle’s monotonicity. Contributions proving these milestones or the final sensitivity theorem are within scope.

Selected references

• S. Lee and A. Rivera, Extrapolation Bias and Robust Dynamic Liquidity Management, Management Science, 2021. DOI: 10.1287/mnsc.2020.3765. This mission cites the authors’ working version, Extrapolation Bias and Dynamic Liquidity Management, dated May 24, 2019; its pagination and numbering govern every milestone.

Motivation

Business-interruption (BI) insurance reimburses a firm for the revenue it loses while a disruption (a flood, a fire, a supplier failure) keeps its capacity down. The 2011 Thailand floods and the Tōhoku earthquake made such losses large and visible for manufacturers, and BI cover is now a standard part of commercial property insurance. Two information problems make it hard to price. The insurer does not know how strong the firm's demand will be, and so how much revenue is really at stake (adverse selection); and once a disruption happens, the insurer does not observe how hard the firm works to restore capacity (moral hazard).

Kao, Keskin and Shang (SSRN 3184530, version of May 13, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2020.3776) model both problems at once for a firm with limited production capacity. Their headline is an ordering of the optimal contracts that runs against standard screening theory: the firm with the lower demand forecast is sold the contract with more coverage and a higher premium.

Setting

A firm has capacity $K>0$ and sells over periods $1,\dots,T$ at unit price $p$. Its early demand forecast $\mu\in\{\mu_H,\mu_L\}$, with $\mu_H>\mu_L>0$, is its private type, high with probability $\alpha$. A forecast update $\delta\in\{\delta_H,\delta_L\}$, with $\delta_H>0>\delta_L$, probability $\beta$ of $\delta_H$ and mean zero, arrives before selling starts. Demand in period $t$ is $D_t=\mu+\delta+\epsilon_t$ with i.i.d. logistic shocks $\epsilon_t$ of mean $0$ and scale $\gamma>0$. Expected sales from a capacity $x$ are $E[\min(D,x)]$.

In period $\tau$ a disruption occurs with probability $\rho$ and wipes out capacity. The firm then chooses a recovery effort $e\in[0,1]$ at cost $ceK$ and sells from capacity $eK$ for the remaining $T-\tau$ periods. It also pays a penalty $\lambda>0$ per unit of the net disruption loss.

An insurance contract $(y,s)$ has premium $y$ and coverage percentage $s\in[0,\bar s]$. From period $\tau+w$ on, the insurer reimburses the fraction $s$ of the expected revenue loss $p\,E[\min(D,K)-\min(D,eK)]$. Given the contract, the firm chooses the effort $e^*(s)$ that maximizes its profit under disruption, and $E_{\delta,Z}[\pi^I_i(K,y,s)]$ denotes its expected profit with insurance when $\mu=\mu_i$. Without insurance the effort is $\hat e$ and the expected profit is $E_{\delta,Z}[\pi^N_i(K)]$.

The insurer offers a menu $(y_H,s_H)$, $(y_L,s_L)$. It maximizes expected premiums minus expected claims, $\alpha\{y_H-\text{claims}_H(s_H)\}+(1-\alpha)\{y_L-\text{claims}_L(s_L)\}$, subject to four constraints:

• incentive compatibility, (IC-HL) and (IC-LH): each type prefers its own contract;
• individual rationality, (IR-H) and (IR-L): each type prefers its contract to no insurance.

This is program (5.1).

Formalization targets

Goal: Proposition 4

Under the paper's standing conditions,

$$K>\mu_H+\delta_H+\gamma\ln\frac{(T-\tau)p-c}{c}\qquad\text{and (5.5)},$$

program (5.1) has an optimal menu, and every optimal menu satisfies

$$s^*_L\ge s^*_H\qquad\text{and}\qquad y^*_L\ge y^*_H .$$

The goal asserts only the order of the two contracts, not their values: the optimal coverages have no closed form.

Milestones

1. Eq. (4.1): the closed form $E[\min(D,x)]=x+m-\gamma\ln[e^{x/\gamma}+e^{m/\gamma}]$ for logistic demand with location $m$.
2. Eq. (4.13)–(4.14): $e^*(s)$ is the unique optimal effort, and it is positive.
3. Proposition 1(i): $e^*(s)$ is non-increasing and concave in $s$, and $e^*(s)\le\hat e$.
4. Proposition 1(ii): $E_{\delta,Z}[\pi^I_i(K,y,s)]$ is non-decreasing and convex in $s$.
5. The marginal profit formula from the proof of Proposition 1(ii).
6. Proposition 2: the marginal profit in $s$ is non-increasing in $\mu$ (the reverse single-crossing property).
7. Eq. (5.2)–(5.4): (IC-HL) and (IR-L) are redundant, and (IC-LH) and (IR-H) bind at the optimum.
8. Lemma 1(i): the reduced objective $R(s_H,s_L)$ is quasi-concave in $s_L$.
9. Lemma 1(ii): under (5.5), $R(s_H,s_L)$ is quasi-concave in $s_H$.
10. Proposition 3: the optimal coverages are selected by the first-order conditions (5.6)–(5.7), with the cap and a zero-root boundary case handled explicitly.
11. The FOC comparison from the proof of Proposition 4.

Significance

In the classical screening model (Mussa–Rosen, Maskin–Riley), the type with the higher valuation receives the higher quality, and the lower type's participation constraint binds. Here the order is reversed. The high-demand firm restores more capacity on its own and is more often capacity-bound, so a unit of coverage is worth less to it than to the low-demand firm. Proposition 4 turns this into an operational recommendation: offer the low-demand firm the richer and dearer policy. The reduction of (5.1) to two binding constraints, and the resulting first-order conditions, support the paper's comparative statics (Table 1) and its capacity-investment results (Propositions 5–6).

The results are proved in the paper by calculus on explicit closed forms. None of them has been machine-checked, and the platform has no model of BI insurance, no logistic demand law and no two-type insurance-screening program. A complete development checks every step of a chain that mixes an expectation, an envelope argument, a reverse single crossing and a constrained optimization. It also produces reusable pieces: logistic expected sales, and a template for two-type screening problems in which the binding constraints are derived rather than assumed.

Difficulty

Each analytic step is elementary on its own; the difficulty is the length of the chain and the places where the obvious argument does not apply.

• The expected-sales formula. It is an improper integral against the logistic density, and the rest of the development rests on it.
• Differentiability at the effort cap. The optimal effort switches between an interior formula and the cap $e=1$ and is not differentiable in $s$ at the switch, while Propositions 1(ii) and 2 are statements about the derivative of the firm's profit there.
• Existence of an optimal menu. The paper presupposes it. The premiums range over all of $\mathbb R$, so (5.1) as posed is not an optimization over a compact set.
• The order of the premiums. It does not follow from the order of the coverages alone: it also needs the monotonicity of the firm's profit in coverage.

Formalization scope

All objects live in the namespace BIInsurance.Screening:

• Logistic: the logistic density and expected sales as a Lebesgue integral;
• Model: the parameters, the standing assumptions, the firm's profits, the efforts $\hat e$ and $e^*$, program (5.1), $g_H$, $g_L$, $R$, condition (5.5) and the left sides of (5.6)–(5.7).

The formalization commits to these conventions:

• Periods. $T,\tau,w$ are natural numbers cast to reals. The disruption period satisfies $\tau\ge1$, as it belongs to the selling season. One waiting period $w=w_H=w_L$ is used.
• Expectations. Expectations over $\delta$ and over the disruption indicator are finite weighted sums. Only the demand shock is integrated.
• Coverage set. It is $[0,\bar s]$, i.e. $\underline s=0$, as in all results of the paper.
• Added hypotheses. $\rho>0$ and $w<T-\tau$ are added to the page's assumptions. Without them insurance pays nothing and the goal is false.
• Standing conditions. The $K$-condition and (5.5) are explicit hypotheses wherever the paper assumes them "throughout the sequel" (p. 19).
• Effort. $e^*$ is defined by its formula (4.13), and its optimality is a milestone.
• General forecasts. Firm-level milestones are stated for every early forecast $\mu\ge\mu_L$, as the proofs show.
• Printed slip. Lemma 1(ii)'s "positive slope" is stated under strict (5.5), because a non-strict (5.5) gives only a non-negative slope.
• Boundary root. When (5.5) holds with equality, zero solves (5.6); Proposition 3 distinguishes when zero is optimal from when a positive root or the cap is optimal.

A trivializing encoding is ruled out. The optimal contract is a maximizer of (5.1) with all four constraints, never the closed form $\min\{s',\bar s\}$ of Proposition 3, and never a maximizer of the reduced objective $R$. Expected sales are an integral, not their closed form.

The development needs:

• improper integrals of logistic densities;
• one-variable derivatives of compositions with $\ln$ and $\exp$;
• quasi-concavity on intervals;
• an existence argument for the insurer's optimum.

The logistic expected-sales lemma and the redundancy argument for two-type screening are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• Y.-M. Kao, N. B. Keskin, K. Shang, Impact of Information Asymmetry and Limited Production Capacity on Business Interruption Insurance, SSRN working paper 3184530, version of May 13, 2020. https://ssrn.com/abstract=3184530
• Y.-M. Kao, N. B. Keskin, K. Shang, Impact of Information Asymmetry and Limited Production Capacity on Business Interruption Insurance, Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3776
• M. Mussa, S. Rosen, Monopoly and Product Quality, Journal of Economic Theory 18(2), 1978. https://doi.org/10.1016/0022-0531(78)90085-6
• E. Maskin, J. Riley, Monopoly with Incomplete Information, RAND Journal of Economics 15(2), 1984. https://doi.org/10.2307/2555675