All missions

Round-Robin as a game

Round-Robin is the simplest allocation procedure for indivisible goods: agents take turns, in a fixed order, and at each turn the active agent takes her favourite good among those still available. Run on truthful preferences with additive valuations it returns an allocation that is envy-free up to one good (EF1), which is why it is the default baseline of discrete fair division. The procedure, however, only asks each agent for a ranking of the goods, and an agent may gain by misreporting: taking a good that others want early, and a good nobody else wants later, can improve her bundle. Round-Robin is therefore a game whose strategies are rankings, and the natural questions are whether it has pure Nash equilibria and whether the allocations at equilibrium are still fair.

For additive valuations the answer to the first question is known: an exact equilibrium exists, given by a profile now called the bluff profile, with a proof fragmented over Aziz, Goldberg and Walsh (2017), Bouveret and Lemaître (2016) and Amanatidis et al. (2021), as recalled on p. 7 of the paper below. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research, 2025) move beyond additive agents, to valuations for which the goods already held change the value of the remaining ones. This mission formalizes their first result: for cancelable valuations, the bluff profile is an exact pure Nash equilibrium.

Setting

There are $n \ge 1$ agents $N = [n]$ and a finite set $M$ of $m$ goods. Agent $i$ has a valuation function $v_i : 2^M \to \mathbb R$ that is normalized ($v_i(\emptyset) = 0$) and non-decreasing. A valuation $v$ is cancelable if for all $S, T \subseteq M$ and every good $g \notin S \cup T$,

$$v(S \cup \{g\}) > v(T \cup \{g\}) \;\Longrightarrow\; v(S) > v(T).$$

Cancelability says that adding a common good never reverses a strict comparison. Additive valuations are cancelable; the paper notes (p. 3) that cancelable functions also generalize budget-additive, unit-demand and multiplicative valuations, and (p. 5) that neither the cancelable nor the submodular class contains the other.

A ranking $\succ_i$ is a total order on $M$. Given a profile $\boldsymbol\succ = (\succ_1, \dots, \succ_n)$, Round-Robin (Mechanism 1) runs $m/n$ rounds; in each round agents $1, \dots, n$ in turn receive $\mathrm{top}(\succ_i, S)$, the $\succ_i$-largest good of the set $S$ of goods still available. The bundle of agent $i$ is $A_i(\boldsymbol\succ)$. The profile $\boldsymbol\succ$ is an exact pure Nash equilibrium (PNE) if for every agent $i$ and every ranking $\succ_i'$,

$$v_i\big(A_i(\succ_i', \boldsymbol\succ_{-i})\big) \le v_i\big(A_i(\boldsymbol\succ)\big).$$

A strict truthful profile $\boldsymbol\succ^*$ has every agent rank the goods by non-increasing singleton value $v_i(\{g\})$, with ties broken in any fixed way. Let $h_1, \dots, h_m$ be the goods in the order Round-Robin$(\boldsymbol\succ^*)$ allocates them. The bluff profile $\boldsymbol\succ^{\mathrm b}$ has every agent report the same ranking $h_1 \succ h_2 \succ \cdots \succ h_m$.

Formalization targets

Goal: Theorem 3.2

For cancelable valuations and every strict truthful profile $\boldsymbol\succ^*$, the bluff profile is an exact PNE of Round-Robin:

$$\forall i \in N,\ \forall \succ_i' :\quad v_i\big(A_i(\succ_i', \boldsymbol\succ^{\mathrm b}_{-i})\big) \le v_i\big(A_i(\boldsymbol\succ^{\mathrm b})\big).$$

Milestones

1. Lemma 2.2. If $v$ is cancelable and $R \cap (S \cup T) = \emptyset$, then $v(S \cup R) > v(T \cup R) \Rightarrow v(S) > v(T)$, $v(S) \ge v(T) \Rightarrow v(S \cup R) \ge v(T \cup R)$, and $v(S) = v(T) \Rightarrow v(S \cup R) = v(T \cup R)$.
2. Lemma 3.3. For a cancelable valuation and $k$-element sets $X = \{x_1, \dots, x_k\}$, $Y = \{y_1, \dots, y_k\}$: if $v(\{x_j\}) \ge v(\{y_j\})$ for every $j$, then $v(X) \ge v(Y)$.
3. Fact 3.1. Round-Robin$(\boldsymbol\succ^{\mathrm b})$ and Round-Robin$(\boldsymbol\succ^*)$ return the same allocation.
4. The ordering $Y^*$ (proof of Theorem 3.2). If agent $i$ deviates to any ranking and receives $A_i$, then $A_i$ has an ordering $(y^*_1, \dots, y^*_k)$ with $v_i(\{y^*_r\}) \le v_i(\{h_{(r-1)n+i}\})$ for every round $r$.

A companion item, Proposition 2.5, states that Round-Robin$(\boldsymbol\succ^*)$ is EF1 for cancelable valuations; with Fact 3.1 and Theorem 3.2 it exhibits an exact PNE whose allocation is EF1.

Significance

The theorem gives an explicit equilibrium of Round-Robin, computable by one run of the mechanism on truthful singleton rankings, for a valuation class strictly larger than the additive one. Combined with Proposition 2.5 it shows that Round-Robin with cancelable agents always has an exact equilibrium that is EF1, so strategic behaviour need not cost fairness. The same paper shows that this fails for submodular valuations, where the best one can guarantee is a $1/2$-approximate equilibrium (the second mission of this series), and that every approximate equilibrium remains approximately EF1 (the third and fourth missions).

The result is proved in the paper; nothing about its truth is open. As far as is known, no part of it, and no part of the Round-Robin mechanism, the EF1 notion or the class of cancelable valuations, has been machine-checked. This mission formalizes the known proof and, on the way, builds a reusable model of Round-Robin as a function of reported rankings.

Difficulty

The proof compares two executions of Round-Robin: one in which everybody reports the bluff order, and one in which agent $i$ reports a different ranking. A deviation changes which goods are available at every later step, and so changes what every other agent takes; the obvious attempt, comparing agent $i$'s $r$-th good in the two runs directly, fails because her $r$-th good under the deviation may be a good that was already gone in round $r$ of the bluff run. The argument needs a reordering of the deviation bundle under which the round-by-round comparison holds, and then a set-level inequality that cancelable (not additive) valuations still support. In Lean, the main work is in the bookkeeping of the two executions: which goods are allocated before a given step, and how a change of one report propagates.

Formalization scope

Agents are Fin n with $n \ge 1$, numbered from $0$; goods form a finite type $M$ with decidable equality. Valuations are real-valued functions on Finset M, normalized and non-decreasing, hence nonnegative. A ranking is a list of all goods without repetition, most preferred first. Round-Robin is defined by recursion on steps: step $t$ (from $0$) belongs to agent $t \bmod n$, and agent $i$'s bundle collects the goods picked at her steps among the first $m$; the paper's step $(r-1)n + i$ is step $(r-1)n + (i-1)$. The bluff profile is computed from the strict truthful profile, and the theorem quantifies over every strict truthful profile, i.e. every tie-breaking. Deviations range over rankings only, as in Definition 2.4.

The paper assumes $m = kn$ "for simplicity", noting that dummy goods reduce the general case to it. Every statement that uses the round structure carries the hypothesis $|M| = kn$; the dummy-goods reduction is not formalized. Lemma 2.2 is stated for any real-valued cancelable function, which the page's proof covers. A bluff profile defined as an arbitrary equilibrium, deviations over arbitrary lists, or an EF1 computed from reports instead of true valuations would each trivialize or change the statement; none is used.

Definitions needed: valuations, cancelability, rankings and top, Round-Robin with its step bookkeeping, approximate PNE and EF1, strict truthful profiles and the bluff profile. All are in one definitions file, written to be shared with the other missions of the series. Proofs of the milestones, and lemmas about Round-Robin executions (one good per step, bundles of size $k$, the effect of changing one report), are welcome contributions.

Selected references

• G. Amanatidis, G. Birmpas, P. Lazos, S. Leonardi, R. Reiffenhäuser, Round-Robin Beyond Additive Agents: Existence and Fairness of Approximate Equilibria, arXiv:2301.13652v1, 2023; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2301.13652
• G. Amanatidis, G. Birmpas, F. Fusco, P. Lazos, S. Leonardi, R. Reiffenhäuser, Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness, WINE 2021, LNCS 13112, pp. 149–166.
• H. Aziz, P. Goldberg, T. Walsh, Equilibria in Sequential Allocation, ADT 2017, LNCS 10576, pp. 270–283.
• S. Bouveret, M. Lemaître, Characterizing Conflicts in Fair Division of Indivisible Goods Using a Scale of Criteria, Autonomous Agents and Multi-Agent Systems 30(2):259–290, 2016.
• R. J. Lipton, E. Markakis, E. Mossel, A. Saberi, On Approximately Fair Allocations of Indivisible Goods, EC 2004, pp. 125–131.

Why the price of borrowing a stock matters

To sell a stock short, an investor must first borrow it, and the owner who lends it charges a lending fee. Securities lending is a large market, and the fee varies across stocks: D'Avolio (2002) documents that shorting costs are positively related to the dispersion of investors' beliefs. Short-sale constraints have a long history in asset pricing (Miller 1977; Harrison and Kreps 1978; Jones and Lamont 2002), but most models either forbid short sales outright or take the fee as an exogenous parameter. Neither explains where the fee comes from, nor when a lending market is active at all.

Evgeniou, Hugonnier and Prieto build a dynamic general equilibrium model in which the fee is endogenous: two investors with logarithmic utility disagree about the expected return of a risky asset, and a lending agent, acting for the asset owners, sets the fee charged to short sellers to maximize the owners' fee revenue. Their §3 derives the equilibrium shorting cost in closed form at every state of the economy. This mission formalizes that derivation.

Setting

The economy has a riskless asset and two risky assets with strictly positive volatilities $\sigma_1,\sigma_2$. Asset 1 can be shorted at a cost; asset 2 cannot be shorted at all. There are two investors, an optimist $o$ and a pessimist $p$, with wealths $W^{(o)},W^{(p)}>0$. Each investor $a$ perceives market prices of risk (Sharpe ratios) $\theta^{(a)}_1,\theta^{(a)}_2$, and the optimist is more optimistic about asset 1: $\theta^{(p)}_1\le\theta^{(o)}_1$, the disagreement $\Delta\ge0$.

A short position in asset 1 pays a shorting cost $\Phi$ per dollar shorted, and a long position earns a lending yield $\Gamma$. Both are measured per unit of volatility of asset 1: $\phi=\Phi/\sigma_1$ and $\gamma=\Gamma/\sigma_1$. A position $m$ in asset 1 earns fees at the rate

$$\Lambda(m;\Phi,\Gamma)=m^+\Gamma-m^-\Phi ,$$

with $m^+=\max\{m,0\}$ and $m^-=\max\{-m,0\}$. Investor $a$ chooses wealth fractions $p=(p_1,p_2)$ with $p_2\ge0$ to solve the mean-variance problem

$$\max_{p\in\mathbb R\times\mathbb R_+}\Big\{\Lambda(p_1;\Phi,\Gamma)+p_1\sigma_1\theta^{(a)}_1+p_2\sigma_2\theta^{(a)}_2-\tfrac12(p_1\sigma_1+p_2\sigma_2)^2\Big\},$$

which is what logarithmic utility reduces to at each instant. The lending agent's revenue per unit of volatility at fee $y$ is

$$R(y)=\sum_a y\,\big(\theta^{(a)}_1+y\big)^-\,W^{(a)} .$$

An equilibrium at a state consists of these quantities such that: the no-dominance condition $\theta^{(a)}_2=\theta^{(a)}_1+\gamma$ holds for both investors (equation (7)); each investor's portfolio is optimal; asset 1, in positive supply $S_1>0$, clears; the lending market clears (fees paid by short sellers equal fees received by long holders); and $\phi$ is the least maximizer of $R$ over $y\ge\gamma$. The inactive set is $\mathcal L=\{\gamma=0\}$ and the active set $\mathcal S$ is its complement.

Formalization targets

Goal: equations (15)–(17)

At every equilibrium state,

$$\gamma=0\iff\theta^{(p)}_2\ge0,\qquad \phi=-\tfrac12\,\theta^{(p)}_1\,\mathbb 1_{\{\theta^{(p)}_2<0\}} .$$

Lending is active exactly where the pessimist perceives a strictly negative net Sharpe ratio on long positions, and there the lending agent charges half the Sharpe ratio $-\theta^{(p)}_1$ the pessimist could earn by shorting absent frictions.

Milestones, in attack order

1. Proposition 1 (p. 17): the optimal portfolios of the mean-variance problem under (7) and $\phi\ge\gamma$.
2. (11) (p. 18): the optimist is long, $\theta^{(o)}_2=\theta^{(o)}_1+\gamma>0$.
3. (14) (p. 18): $\gamma\sigma_1S_1=(\phi-\gamma)(\theta^{(p)}_1+\phi)^-W^{(p)}$.
4. (12)–(13) (p. 18): the maximizers of the revenue over $y\ge\gamma$, and their least element $\max\{\gamma,-\tfrac12\theta^{(p)}_1\}$.

Two companion statements are also included: (18) (p. 20), that the pessimist is strictly short on $\mathcal S$, and the fee flow $(\pi^{(p)}_1)^-\Phi=\tfrac14(\theta^{(p)}_1)^2W^{(p)}\mathbb 1_{\mathcal S}$ (p. 19).

Significance

The goal is the paper's description of the short market. It identifies the active set by a condition on one observable-in-principle quantity, the pessimist's net Sharpe ratio, and it gives the fee as a fixed fraction of the pessimist's frictionless Sharpe ratio. The rest of the paper rests on it: the one-asset closed forms of §4.1, the trading regions of §3.3, and the pricing results of Proposition 2 all start from (15)–(16). The fee-flow identity shows that the optimist captures a quarter of the pessimist's frictionless excess return, which is the upper bound Remark 1 attributes to any alternative fee-setting mechanism.

The result is proved in the paper, partly in the text and partly in Appendix A. Some steps are argued informally: (11) rests on the sentence "agents cannot be short simultaneously in equilibrium", and (14) on "substituting the optimal portfolios of Proposition 1 into the market clearing conditions". As far as is known, none of it has been machine-checked. A formalization makes each step explicit, including the degenerate states the text passes over. In checking the statements against each other, three printed slips were found and are corrected here (see Formalization scope).

Difficulty

The goal combines optimality, clearing and revenue maximization, and the obvious argument fails at its degenerate edge. On the inactive set the shorting cost equals the lending yield ($\phi=\gamma=0$). There Proposition 1's characterization of optimal portfolios no longer holds: portfolios that short asset 1 to buy asset 2 are also optimal. So the step "substitute the optimal portfolios" is not available, and (14) must be obtained from the clearing conditions directly in that case. Similarly the revenue maximizer is not unique on the inactive set; the shorting cost is pinned down only by the paper's selection of the least maximizer, and (16) is false for any other selection. Finally, (11) requires an argument that the two investors cannot both be short while asset 1 is in positive supply. This uses optimality of both portfolios, not just of one.

Formalization scope

Everything is stated at one state $(\omega,t)$ of the paper's continuous-time economy, about real numbers. The continuous-time economy of §2 (Brownian filtrations, consumption streams, the dynamics of wealth) is the paper's motivation and is not formalized; the formalized statements are its instantaneous equilibrium conditions. The time index is dropped throughout, and the paper's "arbitrary process $x_t$" in Proposition 1 becomes an arbitrary real number.

Conventions:

• Rates are per unit of volatility; the dollar rates are $\Phi=\phi\sigma_1$ and $\Gamma=\gamma\sigma_1$, never obtained by division.
• $m^+$ and $m^-$ are written as $\max\{m,0\}$ and $\max\{-m,0\}$; indicators are if … then … else 0.
• Dollar positions are $\pi^{(a)}_1=W^{(a)}p^{(a)}_1$.
• The standing assumptions are hypotheses of every equilibrium statement: $\sigma_1,\sigma_2>0$ (the standing assumption of §3), $S_1>0$, $W^{(o)},W^{(p)}>0$, and $\theta^{(p)}_1\le\theta^{(o)}_1$.
• The shorting-cost condition (4) is stated in its per-volatility form (10), over $y\ge\gamma$, with the least maximizer selected as in (13). A single lending agent is built in.
• Consumption clearing and asset-2 clearing are not part of the equilibrium predicate; no statement uses them, so leaving them out makes every statement more general.

Corrected slips of the page, each disclosed in the item concerned:

1. Proposition 1's "the optimal portfolio satisfies (9)" fails when $\phi=\gamma$; the converse direction is stated under $\phi>\gamma$, and the constraint $0\le x\le\theta_2$ only where $\theta_2\ge0$.
2. The indicator in (12) should be $\mathbb 1_{\{\theta^{(p)}_1+\gamma\ge0\}}$, not $\mathbb 1_{\{\theta^{(p)}_1\ge0\}}$; the least maximizer (13) is unaffected.
3. (18) prints "$\neq\emptyset$"; its proof shows the set is empty, which is what is stated.

The results (11), (13) and (14) are not built into the equilibrium predicate. With them assumed, the goal would reduce to a four-line computation; they are separate items to be proved. The definitions are short and self-contained, needing only real arithmetic from Mathlib. Proofs of the milestones, and proofs of the goal that use the milestones, are welcome.

Selected references

• T. Evgeniou, J. Hugonnier, R. Prieto, Asset Pricing with Costly Short Sales, Swiss Finance Institute Research Paper N°22-21, version of September 22, 2022 — the source of this mission. Published as J. Hugonnier, R. Prieto, Asset Pricing with Costly Short Sales, Management Science (2024), https://doi.org/10.1287/mnsc.2023.01887, whose numbering is not used here.
• G. D'Avolio, The market for borrowing stock, Journal of Financial Economics 66 (2002), 271–306.
• C. Jones, O. Lamont, Short-sale constraints and stock returns, Journal of Financial Economics 66 (2002).
• R. Radner, Existence of equilibrium of plans, prices and price expectations in a sequence of markets, Econometrica 40 (2) (1972), 289–303.

Why bound the order-up-to level of a perishable product

Food, blood products, pharmaceuticals and many retail goods are perishable: a unit is usable for a fixed number of periods and is then discarded. A seller of such a product decides every period how much to order, what price to charge, and how much stock to deplete or dispose of. Because units of different ages coexist, the state of the system is a vector of inventory levels by remaining lifetime, and the exact dynamic program suffers from the curse of dimensionality in that vector. Nahmias's survey (Nahmias 1982) records this obstacle for the pure ordering problem; adding pricing makes it worse.

Chen, Pang and Pan (Operations Research 62(2), 2014) analyse the joint ordering, pricing and disposal problem with the tools of L♮-concavity (Murota's discrete convex analysis, extended to real vectors). Their §4 shows that the optimal profit-to-go is L♮-concave, which yields monotone policies with bounded sensitivity. Their §6.1 then shows that two one-dimensional, myopic problems bracket the optimal order-up-to level, which is the starting point of the heuristics of §6.2. This mission formalizes the backlogging case of that bracketing result, Theorem 3.

Setting

A single product has lifetime $l\ge 2$ periods; the replenishment lead time is zero, and unmet demand is backlogged. The unit costs are $c$ (ordering), $h^+$ (holding), $h^-$ (backlogging) and $\theta$ (disposal); $\gamma$ is the discount factor. The seller chooses the expected demand $d$ in an interval $\mathcal D=[\underline d,\bar d]$, which is equivalent to choosing the price $P(d)$, where $P$ is strictly decreasing. The expected revenue $P(d)\,d$ is continuous and concave on $\mathcal D$ (Assumption 1). Realized demand is $d_t=d+\varepsilon_t$, with independent, identically distributed, zero-mean noise supported in $[A,B]$, $A\le 0\le B$, and $\underline d+A\ge 0$.

The state $s=(s_1,\dots,s_{l-1})$ lies in $\mathcal S=\{s_1\le\dots\le s_{l-1}\}$: $s_i$ is the inventory with residual lifetime at most $i$ periods (negative values are backorders), and $s_{l-1}$ is the inventory position. Each period the seller picks an order-up-to level $s_l\ge s_{l-1}$, the demand level $d$, and, after demand is realized, a depletion $a$ with $s_1\vee d_t\le a\le s_l\vee d_t$. The next state is $\tilde s=(s_2-a,\dots,s_l-a)$. The one-period objective is

$$\varphi_t(s,s_l,d,a\mid\varepsilon_t)=\gamma c\,\tilde s_{l-1}-cs_l-\theta(a-d_t)-h^+(s_l-a)^+-h^-(a-s_l)^++\gamma f_{t+1}(\tilde s),$$

$g_t$ maximizes it over $a$, $G_t(s,s_l,d)=P(d)d+\mathbb E[g_t]$, and the profit-to-go is $f_t(s)=\max_{s_l\ge s_{l-1},\,d\in\mathcal D}G_t(s,s_l,d)$ with $f_{T+1}=0$.

Under $\theta\ge h^+/(1-\gamma)$ only expiring stock is disposed of (Proposition 1). With $\tilde\theta=\theta+\gamma c-h^+$ and $v_t(s_l,d_t)=-(1-\gamma)cs_l-\gamma cd_t-h^+(s_l-d_t)^+-h^-(d_t-s_l)^+$, the two myopic objectives are

$$\Pi_t(s_l,d)=P(d)d+\mathbb E[v_t(s_l,d_t)],\qquad \tilde\Pi_t(s_l,d)=\Pi_t(s_l,d)-\gamma cs_l-K\,\mathbb E[(s_l-d_t)^+],$$

with $K=\gamma h^++\dots+\gamma^{l-2}h^++\gamma^{l-1}\tilde\theta$. $\bar S_t(d)$ and $\underline S_t(d)$ are their largest maximizers over $s_l\ge0$.

Formalization targets

Goal: Theorem 3 (Bounds), backlogging case

For every period, every state $s\in\mathcal S$ and every $d\in\mathcal D$, the largest optimal order-up-to level $s_{lt}(s,d)$ satisfies

$$\underline S_t(d)\vee s_{l-1}\ \le\ s_{lt}(s,d)\ \le\ \bar S_t(d)\vee s_{l-1}.$$

Milestones, in attack order

1. Lemma 6 (p. 290): $f_t$ is nonincreasing in each coordinate of the state.
2. Proposition 1 (p. 292): if $\theta\ge h^+/(1-\gamma)$, depleting $d_t\vee s_1$ is optimal.
3. The p. 294 decomposition: $\varphi_t$ at $a=d_t\vee s_1$ equals $v_t(s_l,d_t)-\tilde\theta(s_1-d_t)^++\gamma f_{t+1}(\tilde s)$.
4. Theorem 1, first sentence (p. 291), at zero lead time: $f_t$, $g_t$, $\varphi_t$ are L♮-concave.
5. Concavity in $s_l$ (p. 295): $\Pi_t(\cdot,d)$ and $G_t(s,\cdot,d)$ are concave.
6. Upper step (p. 295): $G_t(s,s'_l,d)-G_t(s,s_l,d)\le\Pi_t(s'_l,d)-\Pi_t(s_l,d)$ for $s'_l>s_l\ge s_{l-1}$.

The proof's lower-bound display (p. 295) is not a milestone: as printed, for arbitrary $s'_l>s_l\ge s_{l-1}$, it is false when $h^+>\gamma c$ (see Formalization scope).

Significance

The result. The bounds reduce an $(l-1)$-dimensional optimization to two scalar newsvendor-type problems whose solutions do not depend on the period (Remark 6), and they give interpretable brackets: $\bar S_t(d)$ ignores the future cost of excess stock, while $\underline S_t(d)$ charges every excess unit holding until expiry and then disposal. They justify the one-dimensional heuristics of §6.2 and give a check on any computed policy.

Formalizing it. The paper's proof is short but compresses three steps that need care: the structural results of §4 at zero lead time, the minimal-disposal property, and a coupling argument for the lower bound whose printed display is not correct as stated (see below). A machine-checked development would make the whole chain from the recursion to the bounds explicit, including the existence conventions for optimal decisions. To the knowledge of this mission, none of these results has been formalized in any proof assistant.

Difficulty

The central obstacle is the concavity of $G_t(s,\cdot,d)$ in the order-up-to level. It is not visible from the one-period terms: it rests on L♮-concavity of the whole recursion (Theorem 1), and the depletion constraint $s_1\vee d_t\le a\le s_l\vee d_t$ is not an L♮-convex set, so the standard preservation lemma does not apply to (5) as written.

The lower bound needs a quantitative estimate of how much an extra unit of fresh stock can cost in the future. The printed estimate charges the expiring unit $\tilde\theta$ where an unused unit actually costs $\theta$, so it cannot hold for every pair of order-up-to levels; the lower bound must use that the comparison is only needed below $\underline S_t(d)$, where excess stock is not pushed past the next period's optimal order-up-to level.

Formalization scope

The Lean development lives in the namespace PerishablePricing.Bounds. Its conventions are:

• Carrier $\mathbb R$. The paper treats real and integer vectors at once; only the real case is formalized. L♮-convexity is defined on an explicit domain with real values, the paper's convention for "L♮-convex on a set".
• Indices. States are Fin L → ℝ with $L=l-1\ge1$, 0-based.
• Time. Time counts periods to go: f 0 = 0 is $f_{T+1}$, and $G_t$, $g_t$, $\varphi_t$ use the continuation f n.
• Maxima and expectations. The maxima in the recursion are suprema over nonempty sets whose values are bounded above, and expectations are Bochner integrals against the noise law.
• Optimal decisions. Every optimal decision is a largest maximizer, taken as a hypothesis at the points where it is used. With an arbitrary maximizer the upper bound fails when $\Pi_t(\cdot,d)$ is flat.

The standing assumptions are the hypotheses of every statement:

• nonnegative unit costs and $0\le\gamma\le1$;
• the noise conditions and the strictly decreasing inverse demand;
• Assumption 1;
• $(1-\gamma)c\le h^-$, the §4 assumption $c\le h^-/(1-\gamma)$;
• $h^+\le(1-\gamma)\theta$ with $\gamma<1$, the §6.1 assumption $\theta\ge h^+/(1-\gamma)$, which divides by $1-\gamma$.

Deviations from the page, all disclosed in the items:

• Only the backlogging case of Theorem 3 is stated. The lost-sales case rests on Theorem 2, which is not posed.
• The hypothesis "the starting inventory level of the planning horizon is zero" constrains no object of the statement, and the conclusion is stated for every state.
• $\tilde\Pi_t$'s printed term $-\gamma c\,\tilde s_{l-1}$ depends on the state and the noise. It is read as $-\gamma c\,s_l$, which leaves the maximizers unchanged.
• The objective missing from the printed definition of $\bar S_t(d)$ is $\Pi_t$.
• The upper step's "$G_t=\Pi_t+\gamma\mathbb E[f_{t+1}]$" omits a term constant in $s_l$.
• The lower-bound display of the proof of Theorem 3 is not stated. Its exponents $t+l-3$, $t+l-2$ should read $l-3$, $l-2$, and even then, for arbitrary $s'_l>s_l\ge s_{l-1}$, it fails when $h^+>\gamma c$. Example: $l=2$, deterministic demand, $c=1$, $\gamma=\tfrac12$, $h^+=h^-=1$, $\theta=2$, one period after the current one, $s_1=0$, $d=\tfrac12$, $s_l=100$, $s'_l=101$: the left side is $-3$ and the right side is $-2.75$. In that case an unused unit is disposed of at cost $\theta$, not $\tilde\theta$. Theorem 3 itself is stated as printed, with $\underline S_t(d)$ defined through $\tilde\Pi_t$.

The goal must not be trivialized. Its continuation, the concavity of $G_t$ and the monotonicity of $f_{t+1}$ are properties of the model's own recursion, never hypotheses on abstract functions. Likewise $s_{lt}(s,d)$ is defined through $G_t$, never through $\Pi_t$ or $\tilde\Pi_t$.

A complete development needs:

• L♮-concavity preservation under partial maximization over an L♮-convex set and under expectation;
• concavity of expectations of piecewise-linear functions of the noise;
• measurability and integrability of the stage value $g_t$ in the noise;
• the coupling arguments for Proposition 1 and the lower bound.

The L♮ preservation lemmas are reusable for other discrete-convexity models in inventory theory. Contributions toward any milestone, or toward that infrastructure, are welcome.

The source is the published Operations Research article. In the held scan, printed page = PDF page + 282.

Selected references

• X. Chen, Z. Pang, L. Pan, Coordinating Inventory Control and Pricing Strategies for Perishable Products, Operations Research 62(2):284–300, 2014. https://doi.org/10.1287/opre.2014.1261
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4):937–944, 2008. https://doi.org/10.1287/opre.1070.0482
• S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge62$, also holds for every real $p\ge50$. This is an open problem: no proof is known, and the technique that reached 62 cannot go further. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-62 mission already covers every $p\ge62$, the new work is the range from 50 to 62.

The cutoff came down from 256 to 62 across nine missions. The step from 90 to 80 used a weighted pair-curvature and confinement estimate introduced by moona3k, and further refinement pushed it from 80 through 70 to 62. The confinement method is now exhausted: at $p=61$, every confinement radius whose tangent model stays positive already makes the budget-7 box factor larger than 1. Reaching 50 requires a fundamentally new idea. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 50 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh's Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 62.
• The accepted real coordinate bound for every real p ≥ 62.
• The accepted diagonal Schatten norm identity.

Motivation

Quantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space $\mathcal H$ and its observables by self-adjoint operators on $\mathcal H$. The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of $\mathcal H$, and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.

This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on $L^2(\mathbb R)$.

Setting

Let $\mathcal H$ be a complex Hilbert space. A (partially defined) linear operator $A$ has a domain $D(A)\subseteq\mathcal H$; it is bounded if there is $k\in\mathbb R$ with $\|A\psi\|\le k\|\psi\|$ for all $\psi\in D(A)$, and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, $A=A^*$, which includes $D(A)=D(A^*)$.

On $\mathcal H=L^2(\mathbb R)$:

1. The position operator acts by $(Q\psi)(x)=x\,\psi(x)$ on

$$D(Q)=\Big\{\psi\in L^2(\mathbb R): \int_{\mathbb R}x^2|\psi(x)|^2\,dx<\infty\Big\}\qquad\text{(eq. (3))}.$$

2. The momentum operator $P\psi=\hbar i^{-1}\,d\psi/dx$ has, in the paper's description, domain $D(P)$ consisting of the absolutely continuous functions in $L^2(\mathbb R)$.
3. Heathcote's wave function (eq. (4)) is

$$\psi(x)=\begin{cases}x^{-1}, & x\ge 1,\\ 0, & x<1.\end{cases}$$

Formalization targets

Goal

There is a unit vector of $L^2(\mathbb R)$, namely the class of $\psi$, lying in neither domain:

$$\exists\,\varphi\in L^2(\mathbb R):\quad \varphi=\psi\ \text{a.e.},\qquad \|\varphi\|=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P).$$

Milestones

1. Hellinger–Toeplitz (p. 2, footnote 1): a symmetric operator defined on all of a Hilbert space is bounded (an existing platform theorem).
2. Unbounded self-adjoint operators (p. 2, footnote 2): if $A=A^*$ is unbounded then $D(A)$ is dense and $D(A)\neq\mathcal H$.
3. Normalization (p. 5): $\psi\in L^2(\mathbb R)$ and $\int|\psi|^2=\int_1^\infty x^{-2}dx=1$.
4. Not in $D(Q)$ (p. 5): $\int x^2|\psi(x)|^2dx=\infty$.
5. Not in $D(P)$ (pp. 5–6): no a.e.-representative of $\psi$ is absolutely continuous on every compact interval.
6. Infinite position expectation (p. 9): $\int|x|\,|\psi(x)|^2dx=\int_1^\infty x^{-1}dx=\infty$.

Significance

The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of $\psi\in D(Q)$ is not explained by $\psi$ being "sharp in momentum", because $\psi$ is not even in $D(P)$. Milestone 6 records the physical reading: the mean position of this normalized state is infinite.

Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual $L^2$ space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.

Difficulty

The calculus is easy; the subtleties are in the bookkeeping. Elements of $L^2(\mathbb R)$ are almost-everywhere classes, so "$\psi$ is discontinuous at $1$" does not by itself show $\psi\notin D(P)$: one must rule out every a.e.-modification of $\psi$ being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives $D(A)\neq\mathcal H$ but not density, which comes from the adjoint being a genuine operator.

Formalization scope

• Operators are Mathlib's partially defined linear maps H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.
• $L^2(\mathbb R)$ is Lp ℂ 2 volume on ℝ; $D(Q)$ and $D(P)$ are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in $[0,\infty]$, so "$=\infty$" is literal and not a junk value.
• $D(P)$ follows the paper (absolutely continuous elements, i.e. having a representative absolutely continuous on every $[a,b]$) and omits the standard requirement $\psi'\in L^2$. This set contains the standard domain, so non-membership is a stronger statement.
• The paper's further claim that $\psi\notin D(H)$ for a Hamiltonian $H=P^2/2m+V$ is stated there without proof and for an unspecified potential $V$, and is not included.
• Trivialization is excluded: the goal pins $\varphi$ to the explicit function $\psi$ and requires $\|\varphi\|=1$.

Selected references

• A. Heathcote, Unbounded Operators and the Incompleteness of Quantum Mechanics, Philosophy of Science 57 (1990), 523–534.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press, 1980.