All missions

Motivation

In a linear bandit problem, a learner chooses a vector and observes a noisy scalar response that carries information about an unknown parameter. Regret analyses often need to control the sum of the learner's uncertainty in the directions it chooses. The familiar elliptical potential lemma does this when uncertainty is represented by the inverse of a deterministic, successively updated Gram matrix. Bayesian learning presents a different object: the posterior covariance of the unknown parameter given the observations. It changes with the realized data and can increase on an individual sample path. Hamidi and Bayati's technical note establishes a potential bound for this posterior object under general prior and noise distributions and uses it to analyze linear Thompson sampling.

The deterministic lemma and the posterior result answer related but distinct questions. In the deterministic setting, the update is fixed by the chosen vectors. Here, actions may depend on earlier observations and the next posterior covariance is itself random. The mission concerns the latter claim, including the observation model that gives the covariance its meaning.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with an increasing filtration $(\mathcal F_t)_{t\ge1}$. An unknown parameter $\Theta^\star\in\mathbb R^d$ obeys $\|\Theta^\star\|_2\le1$ almost surely. At time $t$, the learner chooses an $\mathcal F_t$-measurable action $A_t\in\mathbb R^d$ with $\|A_t\|_2\le1$ almost surely. An observation $Y_t$, measurable at time $t+1$, has conditional mean $\langle\Theta^\star,A_t\rangle$ and conditional variance at most $\sigma^2$ when both $\mathcal F_t$ and $\Theta^\star$ are known. No Gaussian law or independent noise model is part of these assumptions.

Write $\Gamma_t=\operatorname{Var}(\Theta^\star\mid\mathcal F_t)$ for the posterior covariance matrix. The quantity $A_t^\top\Gamma_t A_t$ is the remaining parameter uncertainty in the chosen direction. The matrix function used to measure accumulated uncertainty is

$$f(\Sigma,x)=\log\det(I+x\Sigma),\qquad \Sigma\succeq0,\quad x>0.$$

The matrix order $B\succeq A$ means that $B-A$ is positive semidefinite. Conditional expectations of matrices are taken entrywise. The filtration can contain information beyond the actions and observations; it need not be generated by them.

Formalization targets

The first target is the source's stochastic variance reduction inequality. For every $t\ge1$, almost surely,

$$\mathbb E[\Gamma_{t+1}\mid\mathcal F_t]\preceq\Gamma_t-\frac{\Gamma_t^\top A_tA_t^\top\Gamma_t}{\sigma^2+A_t^\top\Gamma_t A_t}.$$

The matrix potential targets are the concavity of $f(\cdot,x)$ on the positive semidefinite cone and equation (2.2): if $\Sigma'=\Sigma-\Sigma VV^\top\Sigma/(1+V^\top\Sigma V)$, then

$$\log(1+V^\top\Sigma V)+f(\Sigma',x)\le f(\Sigma,x+V^\top V).$$

Two scalar and covariance bounds from the proof complete the milestone list: $x\le2\log(1+x)$ on $[0,1]$, and $A_t^\top\Gamma_t A_t\le1$ almost surely. The main target, a conditional formulation of Theorem 2.1, is

$$\mathbb E\!\left[\sum_{t=1}^{T}A_t^\top\Gamma_t A_t\,\middle|\,\mathcal F_1\right]\le 2\max(\sigma^2,1)\log\det(I+T\Gamma_1)\quad\text{almost surely}.$$

The source prints an unconditional expectation on the left although $\Gamma_1$ can be random. Conditioning on $\mathcal F_1$ supplies a coherent general statement; it becomes the printed display when the initial information is trivial. The goal retains the explicit factor $2\max(\sigma^2,1)$ and the horizon $T$ inside the log determinant.

Significance

The result controls a cumulative, adaptively selected posterior quadratic form using only the initial posterior covariance, the horizon and the conditional noise bound. It permits a regret analysis of linear Thompson sampling without replacing the prior by a Gaussian model. In the source, this bound feeds the Bayesian regret theorem for that algorithm; that later theorem is outside this mission's scope. Its proof would also require formalizing the sampling policy and its action-selection law.

The formal development fixes a reusable interface for finite-dimensional posterior covariance under a filtration: a parameter, adapted actions, conditional moments of observations, and an entrywise matrix covariance. It also states the matrix potential claims separately from the probability model, so those claims can serve other analyses of covariance updates. The statements compile locally as open Lean theorems; this mission does not claim machine-checked proofs of them. The deterministic elliptical potential statement already available elsewhere uses a Gram-matrix update and does not establish this posterior result.

Difficulty

Posterior covariance is not pathwise decreasing. The paper's Section 2 example has an observation after which $\Gamma_2>\Gamma_1$. A bound that assumes $\Gamma_{t+1}\preceq\Gamma_t$ for every outcome therefore fails at the first stochastic step. The issue matters especially when actions are adapted: later actions can point toward directions whose posterior variance became large after earlier data. Conditional covariance reduction is a matrix inequality, while the target is a scalar sum of quadratic forms; its potential must remain valid across those different objects.

Formalization scope

Lean uses vectors Fin d → ℝ and the Euclidean dot product, so the unit-ball assumptions mean $v^\top v\le1$. The posterior covariance is the conditional expectation of centered coordinate products. The expectation of a covariance matrix is defined entrywise; matrix order is positive semidefiniteness of the difference. The conditioning sigma-algebra for $Y_t$ is $\mathcal F_t\vee\sigma(\Theta^\star)$, not merely $\mathcal F_t$. Every observation is explicitly square-integrable, so Lean's totalized conditional variance cannot silently return zero for a non-square-integrable input. The source's bound on the parameter already supplies its integrability.

Rounds start at $1$; the finite sum uses $1\le t\le T$. At $T=0$ it is empty and both sides of the goal are zero. No positivity assumption on $\sigma$ is imposed, since the statements use $\sigma^2$ and the zero-denominator covariance correction has zero numerator. The log determinant is used on positive semidefinite covariance matrices with nonnegative scalar argument, where its determinant is positive. The paper's square-root factorization of $\Sigma'$ is represented by its equal direct matrix formula. A deterministic Gram matrix in place of $\Gamma_t$, an independent-observation construction in place of the conditional-moment model, or a supremum-norm ball would change the theorem. The separate matrix and probability lemmas, conditional expectation infrastructure, and finite-dimensional matrix order are the principal reusable components.

Selected references

• Nima Hamidi and Mohsen Bayati, The Elliptical Potential Lemma for General Distributions with an Application to Linear Thompson Sampling, technical note, Operations Research, 2023; formalization source: arXiv:2102.07987v3, 2022, §2 and Appendix A.

Motivation

Capacitated vehicle routing asks how to serve clients from a depot with vehicles that can carry only a limited load. In the unsplittable version, one vehicle must deliver each client's entire demand. This makes the choice of routes interact with bin packing: a short tour can fail because its total demand exceeds the vehicle's capacity. Approximation algorithms are therefore useful when exact optimization is impractical, and their guarantees must account for both travel distance and capacity. Friggstad et al., arXiv:2111.08138v1, pp. 1–2.

The paper distinguishes unit-demand, splittable-demand and unsplittable-demand CVRP. Earlier tour-partitioning methods gave constant-factor guarantees, while the paper's first main result is a combinatorial algorithm with ratio $\alpha+1.75$, where $\alpha$ is an approximation ratio for metric traveling salesman tours. Taking $\alpha=1.5$ gives the paper's stated $3.25$ ratio. The paper also gives a separate linear-programming-based improvement, which is outside this mission. These are results already proved mathematically; the mission concerns their precise Lean statements and a machine-checked proof of the combinatorial result. Friggstad et al., arXiv:2111.08138v1, pp. 2–3.

Setting

An instance consists of a finite set $V$ of clients, a separate depot $r$, a symmetric nonnegative metric cost $c(u,v)$, and a demand $d_v\in(0,1]$ for each client. A vehicle has capacity $1$. A route starts and ends at $r$, visits a sequence of clients, and carries at most one unit of total demand. A feasible solution is a collection of routes in which every client appears exactly once. Its cost is the sum of its routes' travel costs, and $\mathrm{opt}$ is the least such cost. The normalization to unit capacity and the positivity of every demand are standing assumptions of §2. Friggstad et al., arXiv:2111.08138v1, p. 4, Definitions 3–4.

For a threshold $\delta\in[0,1/2]$, a client is small when $d_v\le\delta$ and big when $d_v>\delta$. The radial sums are

$$\mathcal D=\sum_{v\in V}2d_vc(r,v),\qquad \mathcal D_{\rm small}=\sum_{v\text{ small}}2d_vc(r,v),\qquad \mathcal D_{\rm big}=\sum_{v\text{ big}}2d_vc(r,v),\qquad \mathcal D'_{\rm big}=\sum_{v\text{ big}}2c(r,v).$$

The last sum is the cost of giving each big client its own depot route. Lemma 6 says $\mathcal D\le\mathrm{opt}$. Friggstad et al., arXiv:2111.08138v1, pp. 4–5.

Algorithm 1 fixes $\delta=1/3$. It obtains one traveling-salesman tour $A_s$ through the small clients and another $A_a$ through all clients. A consecutive split partitions the visiting order of a tour into capacity-feasible routes; $\operatorname{Split}(A)$ is the minimum cost of such a partition. The algorithm also finds a minimum-cost matching with loops on the big clients, whose one- or two-client routes cost $\operatorname{Match}(V_{\rm big})$. It returns the cheaper of a matching plus a split of $A_s$, and a split of $A_a$. Friggstad et al., arXiv:2111.08138v1, pp. 7–8, Algorithm 1.

Formalization targets

The first targets are the paper's intermediate bounds: Lemma 6's radial lower bound; the TSP lower bound used in §3.1; Claims 8–9 on the probabilities of the tank events; Lemma 7's $\delta$-tank cost guarantee; Lemmas 10–11 on the matching; and the two branch estimates (4)–(5). These are the mission's milestones in the order in which their results are needed. Friggstad et al., arXiv:2111.08138v1, pp. 4–8.

The goal is Theorem 1. Let $\operatorname{TSP}(S)$ be the minimum depot tour length through exactly the client set $S$, and suppose

$$c(A_s)\le\alpha\operatorname{TSP}(V_{\rm small}),\qquad c(A_a)\le\alpha\operatorname{TSP}(V),\qquad \alpha\ge1.$$

For the specific cost

$$C_{\rm alg}:=\min\{\operatorname{Match}(V_{\rm big})+\operatorname{Split}(A_s), \operatorname{Split}(A_a)\},$$

the goal says that a feasible solution attains $C_{\rm alg}$ and, for every feasible solution $\mathcal T$,

$$C_{\rm alg}\le(\alpha+1.75)c(\mathcal T).$$

Quantifying over every feasible solution expresses the ratio against $\mathrm{opt}$ without relying on a default value of a real infimum. Friggstad et al., arXiv:2111.08138v1, p. 2, Theorem 1; pp. 7–8, Algorithm 1.

Significance

The theorem supplies a cost guarantee for a concrete routing algorithm with a fixed threshold and two prescribed branches. It applies to unequal, indivisible client demands, while a unit-demand model cannot express the main capacity issue. The $3.25$ instance obtained from a $1.5$-approximate TSP routine is a directly interpretable guarantee. The stronger LP-based theorem in §4 is a separate result and is not needed to establish this one. Friggstad et al., arXiv:2111.08138v1, pp. 2, 7–9.

A completed formalization would connect the paper's demand-aware CVRP model to a reusable published metric-route module, add definitions for optimal consecutive tour splitting and loop-allowed matching, and certify the stated branch and radial inequalities. Related platform results cover unit-demand VRP and TSP bounds, but their capacity and demand conventions differ. This mission introduces the unsplittable-demand statements rather than treating those unit-demand results as interchangeable.

Difficulty

The direct shortcut from a TSP tour to CVRP routes does not control capacity: a segment cheap in distance may carry too much demand. The big clients are especially restrictive at $\delta=1/3$, since no feasible route can contain three of them. The tank lemma has to relate a partition of a fixed visiting order to the four radial terms with the exact coefficients shown above. The final ratio depends on comparing the two algorithm branches, including both matching bounds; an arbitrary feasible solution with a small cost would not establish a guarantee for Algorithm 1. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.

Formalization scope

Lean represents the nodes by Fin (n+1), with depot $0$ and all other nodes as clients. A route is a nonempty list of clients, and a solution is a list of routes whose concatenation contains each required client once. The metric and route-cost functions come from the published SupplyChainTheory_vrp definition module; its unit-demand feasibility predicate is not used. The number of clients may be zero. Costs and demands are real, capacity is exactly $1$, and every client demand lies in $(0,1]$. The value at the depot is unused.

Each optimum in the statement is a real infimum over a finite, nonempty, nonnegative cost set for a valid instance. Singleton routes make the split and matching candidate sets nonempty; an ordering exists for every finite client set. The TSP inputs list exactly their intended client sets, and their $\alpha$ guarantees refer to the corresponding TSP optima. The explicit $\alpha\ge1$ condition records what the paper means by an approximation ratio. Lemma 7 is stated for any client subset because Algorithm 1 applies it both to the small-client tour and the all-client tour. Display (5) is an upper bound: the printed equality replaces the tour cost by upper bounds. The running-time assertions are outside this cost formalization. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.

The goal bounds the cost of the specified algorithm, including attainment by a feasible solution. Merely asserting that some feasible solution has cost at most $(\alpha+1.75)\mathrm{opt}$ would be trivial, since an optimal solution already does. Contributions to the finite-tour, consecutive-split, radial, matching and tank-event lemmas are useful beyond the final ratio.

Selected references

• Z. Friggstad, R. Mousavi, M. Rahgoshay, and M. R. Salavatipour, Improved Approximations for CVRP with Unsplittable Demands, arXiv:2111.08138v1, 2021; published in Mathematics of Operations Research, 2025. arXiv

Motivation

Firms that disclose a product carbon footprint can lower it in two ways: by cutting the emissions they control (better materials, cleaner processes), which costs money up front, or by buying carbon offsets from a third party at a constant price per tonne. Offsets have become cheap and widely available, and the business press has repeatedly argued that cheaper offsets let firms substitute away from costly abatement (The Wall Street Journal 2008, Forbes 2020 and The Washington Post 2020, as cited by Gao and Souza, p. 14). Whether that substitution actually happens matters for climate policy: if a lower offset price always raises a firm's own emissions, cheap offsets undercut real abatement.

Gao and Souza, Carbon Offsetting with Eco-Conscious Consumers (Management Science, 2022, doi:10.1287/mnsc.2021.4293), study this question in a model where demand responds to the disclosed footprint. Their Proposition 1 shows that the conventional intuition can fail in both directions of preference correlation: a cheaper offset can make the firm cut its controllable emissions. This mission formalizes that proposition together with the lemmas of its proof.

Setting

A firm sells to $m>0$ consumers. It chooses a controllable emission level $e\in[0,\bar e]$ per unit, which determines a unit cost $c(e)$ and a fixed cost $f(e)$, with $c'<0$, $c''>0$, $f'<0$, $f''>0$ on $[0,\bar e]$ and $f(\bar e)=0$. Each unit also carries uncontrollable emissions $e_o\ge0$. At the offset price $g>0$ the firm offsets $t\in[0,e+e_o]$ units, and discloses the footprint $\mathcal E=e+e_o-t$.

A consumer with valuation $V\ge0$ and environmental disutility $\Xi$ gets utility $u=V-\Xi\mathcal E-p$ at the price $p$, and buys if and only if $u\ge0$. A share $\alpha\in[0,1]$ of consumers is eco-conscious ($\Xi=\xi>0$); the rest are eco-unconscious ($\Xi=0$). A share $\beta_c$ of eco-conscious and $\beta_u$ of eco-unconscious consumers have the high valuation $v_h$; the others have $v_l$, with $0\le v_l$, $c(\bar e)<v_l<v_h$. The demand is the sum of the four segment masses whose utility is nonnegative, and the firm's profit is

$$\pi(p,e,t\mid g)=(p-c(e)-gt)\,d(p,e,t)-f(e).$$

A best response to $g$ is a feasible $(p,e,t)$ maximizing $\pi(\cdot\mid g)$.

Two special cases carry the analysis: Case N ($\beta_u=1$, negative correlation between caring about function and caring about the environment) and Case P ($\beta_c=1$, positive correlation). For $x\ge0$, the segment-optimal emission $e_{x,a}$ is the maximizer over $[0,\bar e]$ of $-(c(e)+xe)\,a\,m-f(e)$: the abatement level a firm chooses when it serves a segment of size $a$ and pays $x$ per unit of footprint. The proof compares the profit of covering the whole market at $v_l$ with that of serving only high-value consumers at $v_h$; their difference $h(g)$ has a least zero $X$, the offset price at which the firm switches.

Formalization targets

Goal: Proposition 1

In Case N, with $\alpha>0$, $\beta_c<B_2=\big(\frac{v_l-c(\bar e)}{v_h-c(\bar e)}-1+\alpha\big)/\alpha$, a sign change of $h$ at its least zero $X<\xi$, and condition (1) of the proof at $X$, there are offset prices

$$0<g_1<g_2\quad\text{with}\quad t^*(g_i)>0,\quad e^*(g_1)\le e^*(g_2),\quad d_u^*(g_1)=d_u^*(g_2),\quad d_c^*(g_1)>d_c^*(g_2),$$

for every pair of best responses (which exist), with strict emissions inequality when $e_{X,1}<\bar e$ and $e_{X,a}>0$. In Case P the analogue holds with $v_h-v_l<\xi e_o$, $\beta_u<\tilde B_2$, $d_c^*(g_1)=d_c^*(g_2)$ and $d_u^*(g_1)>d_u^*(g_2)$.

Milestones

1. $e_{x,a}$ exists, is unique and solves the first-order condition when it is interior (Online Supplement p. 1).
2. Lemma VI1: $e_{x,a}$ is weakly decreasing in $x$ and in $a$, plus its strict version for $a<1$.
3. In each case, the reduction of the firm's problem to two candidate profiles when offsets are bought.
4. $h(0)>0\iff\beta_c<B_2$, and existence of $X$ (Case N); $\beta_u<\tilde B_2\Rightarrow h(0)>0$ and existence of $X$ (Case P).
5. The switch of best responses across $X$, in each case.
6. Condition (1) is an upper set in $\beta_c$ (Case N) and in $\beta_u$ (Case P): the thresholds $B_1$, $\tilde B_1$.

Significance

Proposition 1 identifies a mechanism by which cheaper offsets complement, rather than substitute for, controllable abatement. In Case N a lower offset price lets the firm lower its footprint enough to attract low-value eco-conscious consumers; in Case P it lets the firm price down to the low-value eco-unconscious consumers while keeping eco-conscious buyers. In both cases the served volume grows, and because abatement is a fixed cost, the larger volume makes deeper abatement worthwhile (economies of scale). The paper builds its NGO-pricing results (Propositions 2 and 4) on this subgame analysis.

The result is proved in the paper by a case analysis and derivative arguments; it has no machine-checked proof. Formalizing it produces a complete, checked treatment of a discontinuous best response in a pricing model with threshold demand, and it makes several steps of the published proof precise: where the paper asserts $\partial h/\partial g|_{g=X}<0$ and "$X<G$" without proof, the formal statements carry them as disclosed hypotheses, and the formalization of "$\beta_c\in(B_1,B_2)$ for some $B_1,B_2$" pins both thresholds down.

Difficulty

The best response is not a continuous function of $g$: demand is a step function of price and footprint, so the firm's problem splits into six regimes (Online Supplement I1), and the optimal price jumps between $v_l$, $v_h$ and the footprint-adjusted prices. Comparative statics by differentiating first-order conditions, the method of the paper's lemmas, applies only within a regime. The obvious argument, "$e^*$ is decreasing in $g$ by Lemma VI1", is wrong across the switch at $X$: there the served segment shrinks, and Lemma VI1's monotonicity in the segment size works against its monotonicity in the price. Showing that the jump in segment size dominates requires controlling the best response on both sides of $X$, including uniqueness of the best response and the behaviour of $e_{x,a}$ at the ends of $[0,\bar e]$ where the first-order condition fails.

Formalization scope

All quantities are real. The model is one definition file, EcoOffset.Subgame.Model, with a structure Params of primitives and a predicate Params.Standing bundling the standing assumptions of §3: $m,\bar e,\xi>0$, $e_o\ge0$, $\alpha,\beta_c,\beta_u\in[0,1]$, $0\le v_l$, $c(\bar e)<v_l<v_h$, $c,f$ of class $C^2$ on $\mathbb R$ with the sign conditions on $c',c'',f',f''$ on the closed interval $[0,\bar e]$, and $f(\bar e)=0$. Prices range over all of $\mathbb R$; consumers buy at zero utility. A best response is a predicate, never a chosen function, and the goal quantifies over every best response at $g_1$ and $g_2$ and asserts that one exists. $e_{x,a}$ is defined as the maximizer, not through the paper's root of the first-order condition (which does not exist at $x=0$). The switching price $X$ is a variable pinned by $h(X)=0$ and $h>0$ on $[0,X)$.

Added hypotheses relative to the page, all disclosed in the statements: $X<\xi$ (the proof's unproved "$X<G$"; numerical Case N instances violate it); a sign change of $h$ at $X$ (the proof's unproved $\partial h/\partial g|_{g=X}<0$); $\alpha>0$ in Case N and $\alpha<1$ in Case P (divisions in $B_2$, $\tilde B_2$); $e_o>0$ for the existence of $X$ in Case N; explicit interiority conditions in place of "if $\bar e$ is large enough".

Stating the goal about the two named profiles (for example $e_{g_1,1}\le e_{g_2,a}$) would reduce it to Lemma VI1 plus algebra and is ruled out: the goal is about best responses of the full profit maximization. The paper's "for some $B_1,B_2\ge0$" is likewise not used, since $B_1=B_2$ would make it vacuous.

A complete development needs: existence, uniqueness and continuity in $x$ of the maximizer of a strictly concave function on an interval (Berge's maximum theorem in one dimension); monotone comparative statics for $e_{x,a}$; the case analysis of the step-function demand; and intermediate-value arguments for $X$. The first two are reusable for any one-dimensional parametric optimization. Proofs of individual milestones, and of the goal from the milestones, are welcome.

Selected references

• F. Gao and G. C. Souza, Carbon Offsetting with Eco-Conscious Consumers, Management Science, 2022. https://doi.org/10.1287/mnsc.2021.4293
• F. Gao and G. C. Souza, Carbon Offsetting with Eco-Conscious Consumers, preprint with Online Supplement (the version formalized here; all page numbers refer to it), SSRN 3440652. https://ssrn.com/abstract=3440652

Risk aversion, markets and planning

Electricity systems with hydro storage, and many other resource systems, are operated over time under uncertain inflows. In a centrally planned system a single risk-averse planner chooses releases and storage to minimize a nested (time-consistent) coherent risk measure of total cost. In a deregulated system the same decisions are taken by many agents, each with its own risk attitude, who trade the product, stored resources and financial instruments at market prices. A classical question of welfare economics is when the two coincide.

For risk-neutral agents the answer is the standard welfare theorems. Ferris and Philpott, Dynamic risked equilibrium (Operations Research, 2022), extend them to a multistage setting in which each agent evaluates risk with its own polyhedral coherent risk measure on a scenario tree and can trade Arrow–Debreu securities between each node and its children. Their First Welfare Theorem (Theorem 3) says that every such risk-trading equilibrium solves a social planning problem whose risk set is the intersection of the agents' risk sets. The converse direction, that a risk-averse social planning solution can be supported as a competitive equilibrium with risk trading (a Second Welfare Theorem), was shown for multistage hydro-thermal electricity markets by Philpott, Ferris and Wets (Mathematical Programming B, 2016). The forward direction is described in the 2022 paper as newly established there.

Setting

A finite scenario tree has nodes $\mathcal N$, root $0$, leaves $\mathcal L$; $n_-$ is the parent of $n\neq 0$ and $n_+$ its set of children. A finite set $\mathcal A$ of agents acts on it. At node $n$, agent $a$ chooses releases $u_a(n)\in\mathcal U_a\subseteq\mathbb R^{d_U(a)}$ and storage $x_a(n)\in\mathcal X_a\subseteq\mathbb R^{d_X(a)}$; it has a cost $C_a(u_a)$, a production $g_a(u_a)$, a terminal storage value $V_a(x_a)$, and its storage evolves as $x_a(n)\le x_a(n_-)+\sum_bT_{ab}u_b(n)+\omega_a(n)$ with random supply $\omega_a(n)$.

Each agent's risk attitude is a polyhedral risk set at every non-leaf node,

$$\mathcal D_a(n)=\operatorname{conv}\{[p^k_a]_{n_+}: k\in\mathcal K_a(n)\},$$

a polytope of probability vectors on the children $n_+$; the one-step risk of a cost $Z$ on $n_+$ is $\max_{\mu\in\mathcal D_a(n)}\sum_{m\in n_+}\mu(m)Z(m)$. The social planning risk set is $\mathcal D_s(n)=\bigcap_a\mathcal D_a(n)$ (Definition 1), assumed nonempty (Assumption 3).

Prices are $\pi(n)$ for the product, $\alpha_a(n)$ for agent $a$'s storage, and $\mu(m)$ for an Arrow–Debreu security bought at $n$ that pays $1$ in child $m$. Agent $a$ buys $W_a(m)$ of them. Its one-node disbenefit is

$$Z_a(n)=C_a(u_a(n))-\pi(n)g_a(u_a(n))+\alpha_a(n)^\top\big(x_a(n)-x_a(n_-)-\omega_a(n)\big)-\sum_b\alpha_b(n)^\top T_{ba}u_a(n)+\sum_{m\in n_+}\mu(m)W_a(m),$$

and its problem in complementarity form is the system $\mathrm{AE}_a(\pi,\alpha,\mu,\mathcal D_a)$, (20a)–(20g). A multistage risk-trading equilibrium RTE (Definition 3) is a set of prices and actions such that every agent solves $\mathrm{AE}_a$ and the product, storage and security markets clear, (21)–(23). The social planning system $\mathrm{SE}(\mathcal D)$ (p. 10) is the analogous eight-line complementarity system for a single planner with stage cost $\sum_aC_a$ and risk set $\mathcal D$.

Formalization targets

Goal: Theorem 3

Every RTE with prices $(\bar\pi,\bar\alpha,\bar\mu)$ and actions $(\bar u,\bar x,\bar W,\bar\theta_a)$ satisfies, with $\bar\theta=\sum_a\bar\theta_a$:

1. $[\bar\mu]_{n_+}\in\mathcal D_a(n)$ for every agent, hence $[\bar\mu]_{n_+}\in\mathcal D_s(n)$;

$$\bar\theta(n)=\sum_{m\in n_+}\bar\mu(m)\Big(\sum_aC_a(\bar u_a(m))+\bar\theta(m)\Big),\qquad n\notin\mathcal L;\tag{24}$$

3. $(\bar u,\bar x,\bar\theta,\gamma,\bar\pi,\bar\alpha)$ solves $\mathrm{SE}(\{\bar\mu\})$ for some $\gamma$;
4. $(\bar u,\bar x,\bar\theta,\gamma,\bar\pi,\bar\alpha)$ solves $\mathrm{SE}(\mathcal D_s)$ for some $\gamma$ with $\bar\mu(m)=\sum_k\gamma^k(n)p^k_s(m)$ on $n_+$.

Milestones

• Lemma 1 (p. 3): $\theta=\sup_{\mu\in\mathcal D}\sum_m\mu(m)Z(m)$ iff complementary multipliers $\gamma$ exist, and $\sum_k\gamma^kp^k$ attains the supremum.
• Theorem 2(i), value identity (p. 13): a solution of $\mathrm{AE}_a$ has $\theta_a(n)=\max_{\mu\in\mathcal D_a(n)}\sum_{m\in n_+}\mu(m)(Z_a(m)-W_a(m)+\theta_a(m))$, attained at $\sum_k\gamma^k(n)p^k_a$.
• Theorem 3(i) and Theorem 3(ii) = (24) (p. 15).
• The maximizer step of the proof of (iv) (p. 16): $[\bar\mu]_{n_+}$ maximizes $\sum_{m\in n_+}\mu(m)(\sum_aC_a(\bar u_a(m))+\bar\theta(m))$ over $\mathcal D_s(n)$.

Significance

Theorem 3 says that competitive trading of risk, through a complete set of one-step Arrow–Debreu securities, leads risk-averse agents with different risk attitudes to the outcome a risk-averse planner would choose if the planner used the intersection of their risk sets. The equilibrium security prices are the planner's worst-case probability measure. The paper uses the welfare theorems to indicate how social welfare might be compromised when risk markets are incomplete or illiquid, even if agents behave as price takers; its motivating example is a cascade of hydroelectric reservoirs operated by different agents.

The result is proved on paper. As far as a search of the Prove2Me catalog shows, no risk-trading equilibrium, nested polyhedral risk measure on a tree, or welfare theorem with coherent risk measures has been formalized. The mission produces a machine-checked statement of the multistage model (the agent problem, equilibrium and planning system, written out line by line) and of the welfare theorem. It also fixes the readings of a garbled clause of the printed statement and of one gap in the printed proof (see below).

Difficulty

Each step of the argument is elementary, but the bookkeeping is heavy. The model is indexed by agents, nodes, children, risk-set generators and storage components, and every condition is a finite sum over children. The proof of (24) has to show that, summed over agents, all payments cancel by the complementarity conditions (21)–(23), and this cancellation uses the agents' disbenefits at the grandchildren as well. Part (iv) is the substantive step. The natural first attempt, taking the multipliers of $\mathrm{SE}(\mathcal D_s)$ from Lemma 1 as the printed proof does, puts all weight on one maximizing generator. That reproduces the equilibrium price only when $\bar\mu$ is itself a generator, and the fifth line of $\mathrm{SE}(\mathcal D_s)$ needs the multipliers to reproduce $\bar\mu$ exactly.

Formalization scope

The tree is the platform's StochasticProg.Multistage.Tree ($n_+$ = children n, $n_-$ = anc n); a leaf is a node with no children. The normal cone is the platform's FirstOrderOpt.ConvexTheory.normalCone. The definition file DynRiskEq.Welfare.Model holds the market data, the risk sets, $Z_a$ (18), $\mathrm{AE}_a$ (20a)–(20g), RTE (Definition 3), $\mathcal D_s$ (Definition 1) and $\mathrm{SE}(\mathcal D)$ (p. 10). These are the model.

Committed conventions:

• vectors are EuclideanSpace ℝ (Fin d);
• a risk set is the convex hull of a finite generating family restricted to $n_+$. It need not consist of extreme points, and every generator is a probability vector;
• prices $\mu$ and holdings $W_a$ are functions on all nodes, read only at non-root nodes;
• "$0\in\nabla f(v)+N_S(v)$" requires $v\in S$ and a gradient of $f$ at $v$ (HasGradientAt), and every normal-cone condition includes membership in its set;
• vector complementarity is componentwise;
• $x_a(0_-)$ is given initial storage;
• in (20d) the gradient is taken in $u_a(n)$ alone.

The hypotheses of the goal are:

• probability-vector generators;
• Assumption 3;
• a social generating family whose hull is $\mathcal D_s(n)$;
• the RTE.

Convexity of $C_a$, Assumptions 1, 2 and 4 and equal leaf depth are not assumed: Theorem 3 does not use them. The closing clause of Theorem 3 is read as the link $\bar\mu(m)=\sum_k\gamma^k(n)p^k_s(m)$ and is part of the conclusion of (iv). Without it, (iv) would not say that the equilibrium price is the social worst-case measure.

The equilibrium does not contain $\mathrm{SE}$ or the conclusion $\bar\mu\in\mathcal D_s$, $\bar\theta$ is not defined by (24), and $\mathrm{SE}$ keeps all eight lines of p. 10. A formalization that took any of these shortcuts would make the goal trivial.

Not formalized here:

• Theorem 4 (the converse) and Corollaries 5–6;
• Theorem 1;
• the KKT halves of Theorem 2 (they rest on an unspecified constraint qualification);
• Lemmas 2–4.

Theorem 4 is the natural follow-up mission. General lemmas about maxima of linear functions over convex hulls of finite families are reusable beyond this mission, and contributions of them are welcome.

Selected references

• M. C. Ferris, A. B. Philpott, Dynamic risked equilibrium, Operations Research, 2022 (author's manuscript of April 16, 2018 used here). https://doi.org/10.1287/opre.2019.1958
• A. B. Philpott, M. C. Ferris, R. J.-B. Wets, Equilibrium, uncertainty and risk in hydro-thermal electricity systems, Mathematical Programming B 157(2):483–513, 2016 (reference [5] of the paper).
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068

Motivation

Platforms that estimate a population quantity from individual data, such as a health service estimating the mean response to a treatment, must compensate users for the privacy they give up. Users differ in how much they value privacy, and that value is private information. Differential privacy (Dwork, McSherry, Nissim, Smith, 2006) supplies a quantitative unit of privacy loss, so the platform can trade estimation accuracy against privacy at a price. Fallah, Makhdoumi, Malekian and Ozdaglar (arXiv:2201.03968v2, Operations Research, 2024) design the cost-minimizing mechanism that elicits users' privacy sensitivities, chooses a privacy level for each user, and pays them, when the platform's estimator is a weighted mean with Laplace noise. This mission formalizes their characterization of that mechanism in the central privacy setting (Theorem 3, p. 18).

Buying privacy at auction was studied by Ghosh and Roth (2011, arXiv:1011.1375); the paper's contribution is a Bayesian mechanism in which each user receives an individual privacy level and the estimator is chosen jointly with the payments.

Setting

There are $n \ge 1$ users. User $i$ holds a data point $X_i = \theta + Z_i$, where the $Z_i$ are i.i.d. with mean $0$, variance $\mathrm{VAR} > 0$ and $|Z_i| \le 1/2$. A randomized algorithm on datasets is $\varepsilon$-centrally differentially private for $\varepsilon = (\varepsilon_i)_i$ if changing user $i$'s entry changes the probability of any measurable output event by at most a factor $e^{\varepsilon_i}$ (Definition 1, p. 8).

The platform uses an estimator of the central class (22):

$$\hat\theta(x) = \sum_{i=1}^n w_i(c)\,x_i + \mathrm{Laplace}\big(1/\eta(c)\big), \qquad \sum_i w_i(c) = 1, \quad \eta(c)\,w_i(c) \le \varepsilon_i(c),$$

which is $(w_i\eta)_i$-centrally private (Lemma 2) and has mean square error $\mathrm{MSE}(c) = 2/\eta(c)^2 + \sum_i w_i(c)^2\,\mathrm{VAR}$.

Each user has a privacy sensitivity $c_i$, drawn independently with density $f_i$ and distribution function $F_i$. A direct mechanism maps the reported profile $c$ to weights $w(c)$, a noise parameter $\eta(c)$, privacy losses $\varepsilon(c)$ and payments $t(c)$. A user of type $c_i$ who reports $r$ bears the expected cost

$$\mathrm{cost}_i(r, c_i) = \mathbb E_{c_{-i}}\big[\mathrm{MSE}(r, c_{-i}) + c_i\,\varepsilon_i(r, c_{-i}) - t_i(r, c_{-i})\big],$$

and a non-participant's cost is $\mathrm{VAR}$. The platform minimizes $\mathbb E_c[\mathrm{MSE}(c) + \sum_i t_i(c)]$ subject to incentive compatibility (truthful reporting is optimal) and individual rationality (truthful participation costs at most $\mathrm{VAR}$). The virtual cost is $\psi_i(c) = c + F_i(c)/f_i(c)$, and Assumption 1 asks that each $\psi_i$ be increasing.

Formalization targets

Goal: Theorem 3 (p. 18)

Under Assumption 1, let $y^*(c)$ be an optimal solution of

$$\min_{y \ge 0}\; \frac{n+1}{\big(\sum_j y_j\big)^2}\Big(2 + \sum_i y_i^2\,\mathrm{VAR}\Big) + \sum_i \psi_i(c_i)\,y_i . \tag{23}$$

The mechanism with $\varepsilon^*_i(c) = y^*_i(c)$, weights $w^*_i(c) = y^*_i/\sum_j y^*_j$, $\eta^* = \sum_j y^*_j$ and the payments of Proposition 1 is incentive compatible, individually rational, and minimizes the platform's expected cost among all such mechanisms of class (22). The statement holds for every measurable selection of minimizers.

Milestones

1. Lemma 1 (p. 9): Laplace noise of parameter $1/\varepsilon$ yields per-user privacy $\varepsilon L_i(f)$.
2. Lemma 2 (p. 10): the linear estimator is $(w_i\eta)_i$-centrally private.
3. The MSE formula $2/\eta^2 + \sum_i w_i^2\mathrm{VAR}$ (p. 18).
4. Proposition 1 (p. 16): the payment identity characterizing incentive compatibility and individual rationality.
5. Proposition 2 (p. 17): reduction of the platform's problem to minimizing $\mathbb E_c[(n+1)\mathrm{MSE} + \sum_i \varepsilon_i\psi_i(c_i)] - n\,\mathrm{VAR}$ subject to monotone interim privacy losses.
6. The constraints $\eta w_i \le \varepsilon_i$ bind, so the pointwise problem (24) is (23) (proof of Theorem 3, pp. 44–45).
7. Under Assumption 1, minimizers of (23) are weakly decreasing in the own privacy cost (p. 45).

Significance

Theorem 3 turns a mechanism design problem over function spaces into a finite-dimensional program solved separately at each type profile. Its consequences are that users with higher virtual cost receive less weight and less privacy loss (Corollary 1), that the optimal privacy level is a continuous function of the sensitivity rather than a threshold rule, and that the program can be solved in $O(n\log n)$ time (Proposition 3). The same reduction underlies the paper's comparison of central and local privacy.

The result is proved in the paper; no machine-checked version exists. The mission produces a verified payment identity for a setting where the allocation enters every user's cost through a shared externality (the MSE), a verified reduction to virtual costs that does not rely on differentiability of the mechanism, and the per-user Laplace mechanism on top of Mathlib's measure theory.

Difficulty

The classical Myerson argument assumes a linear objective and a single-dimensional allocation. Here the objective is non-linear and non-convex in the privacy losses, the MSE couples all users, and the minimizer of (23) has kinks where a coordinate reaches zero, so the paper's first-order derivation of the payment identity, which differentiates the interim cost, does not apply to the optimal mechanism, and the identity has to hold without any differentiability. A second obstacle is monotonicity: (23) is not convex and its minimizer need not be unique, so the monotonicity required by the payment identity cannot be read off from a unique smooth solution map; it has to hold for an arbitrary measurable selection of minimizers. Finally, the comparison is over all incentive compatible, individually rational mechanisms, not over a parametric family, so the measure-theoretic bookkeeping (interim expectations, exchanges of integrals over the type law) is part of the statement's content.

Formalization scope

All quantities are real. Users are Fin n with 0 < n. Types live in compact intervals $[a_i, b_i]$ with $0 < a_i < b_i$, and $f_i$ is continuous, positive and integrates to one there; the paper's $c_i \in \mathbb R_+$ and integrals to $\infty$ become integrals to $b_i$. The type law is the product of the laws with densities $f_i$, and interim expectations over $c_{-i}$ are integrals of $g(\mathrm{update}(c,i,r))$ against the type law. Incentive compatibility and individual rationality quantify over types and reports in $[a_i,b_i]$. Class (22) makes $\eta > 0$ and $w \ge 0$ explicit. Mechanisms are required to be measurable, with bounded privacy losses and integrable MSE and payments; differentiability (Definition 3) and nonnegative payments are not required, since the optimal mechanism has kinks and may pay negative amounts. Assumption 1 is strict monotonicity. The feasible set of (23) adds $\sum_j y_j > 0$, because at $y = 0$ Lean's $1/0 = 0$ would make the objective vanish. Laplace noise is the published PrivLearn.Generic.laplace.

Stating Theorem 3 as "$y^*$ minimizes (23)", or comparing the mechanism only with mechanisms that already use the payment rule (19), would be a trivialization; the goal compares against every admissible, incentive compatible, individually rational mechanism of class (22).

Reusable infrastructure includes heterogeneous differential privacy, the per-coordinate Laplace mechanism, the variance of Laplace noise, and a payment identity under concavity without differentiability. Proofs of any milestone, and alternative arguments for the monotonicity of the minimizer, are welcome.

Selected references

• A. Fallah, A. Makhdoumi, A. Malekian, A. Ozdaglar, Optimal and Differentially Private Data Acquisition: Central and Local Mechanisms, Operations Research, 2024. arXiv:2201.03968v2
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. doi:10.1007/11681878_14
• C. Dwork, A. Roth, The Algorithmic Foundations of Differential Privacy, Foundations and Trends in Theoretical Computer Science, 2014. doi:10.1561/0400000042
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research, 1981. doi:10.1287/moor.6.1.58
• A. Ghosh, A. Roth, Selling Privacy at Auction, EC 2011. arXiv:1011.1375

Motivation

A financial transaction tax (FTT) charges a fixed fraction of the value of each securities trade. The idea goes back to Keynes (1936) and to Tobin's proposal of 1972, and it became policy after 2008: France (August 2012) and Italy (March 2013) introduced taxes on equity purchases, and the European Commission has proposed a common FTT (see the introduction of the paper below, pp. 2–3). The standard objection is that such a tax reduces trading volume and market liquidity, and therefore welfare.

Dieler, Biswas, Calzolari and Castiglionesi (Management Science 69(4), 2023; accepted manuscript of January 24, 2022, SSRN 2739357) identify a channel through which a transaction tax can raise welfare. Stock prices are read by firm managers when they decide on real investment. A market can be liquid but uninformative: trade then takes place at a price that does not reveal what informed traders know, and investment is inefficient. A tax that makes this liquid equilibrium impossible can move ("tilt") the market to an equilibrium in which prices are informative. The paper's headline result, Proposition 6, says when such a tilt is optimal and identifies the optimal tax.

Setting

There are two states, $\omega\in\{L,H\}$, with $\Pr(H)=\beta\in(0,1)$. A single informed trader with discount factor $\delta_I$ observes $\omega$ and buys a quantity $T\in[0,1]$ of the firm's stock from a unit mass of competitive uninformed traders with discount factor $\delta_U$, where $0<\delta_U<\delta_I$. The buyer pays a tax $\tau\ge 0$ proportional to the purchase value $P\cdot T$. After observing the trade, the uninformed traders set the price, and the firm's manager observes the price and invests.

Firm values are $F_\omega$ when the manager invests knowing $\omega$, $\bar F_\omega$ when she invests on the prior, and $F^{-\omega}_\omega$ when she invests as if the state were the other one. They satisfy $F_\omega\ge\bar F_\omega\ge F^{-\omega}_\omega$ (1), $F^L_H>F_L$ and $F^H_L>0$ (3), $F_H>F_L$ and $\bar F_H>\bar F_L$. Write $\bar F=\beta\bar F_H+(1-\beta)\bar F_L$. In §5 the paper specifies $F_\omega=V_\omega+v$, $\bar F_\omega=V_\omega$, $F^{-\omega}_\omega=V_\omega-v$ with $V_H>V_L>0$ (23); the parameter $v$ is the value of information.

A separating equilibrium is a pair of trades $T_H\neq T_L$ that reveals the state, so the price is $P_\omega=\delta_UF_\omega$ and the firm is worth $F_\omega$. A pooling equilibrium is a common trade $T_P\in(0,1]$ at the price $P_P=\delta_U\bar F$, and the firm is worth $\bar F_\omega$. Both must satisfy the informed trader's participation and incentive constraints, including deviations to any other quantity $T'\in[0,1]$, which the paper's off-path beliefs price as the $H$-state. Welfare is the expected sum of traders' payoffs and tax revenue, (8). In the Pareto-optimal pooling equilibrium ($T_P=1$) it is $W_P=W^*-\delta_Iv$. In the Pareto-optimal separating equilibrium ($T_H=1$, $T_L=\bar T_L(\tau)$) it is $W_S(\tau)=W^*-(1-\beta)(\delta_I-\delta_U)(1-\bar T_L(\tau))F_L$, where $W^*=\delta_I(\beta F_H+(1-\beta)F_L)$.

Formalization targets

Goal: Proposition 6 (Efficient FTT)

Suppose that without a tax both a pooling and a separating equilibrium exist (Proposition 4 (ii) at $\tau=0$, with strict participation of the low type), that $v>0$, and that

$$\tau^*=\frac{\delta_I}{\delta_U}\frac{\bar F_L}{\bar F}-1\ <\ \tau_0,$$

where $\tau_0$ is the tax at which $W_S=W_P$. Then $0<\tau^*<\tau_{FB}=\delta_I/\delta_U-1$. Moreover:

• the pooling equilibrium with $T_P=1$ survives every tax $\tau\in[0,\tau^*]$, and no pooling equilibrium exists for $\tau>\tau^*$;
• for $\tau\in(\tau^*,\tau_{FB}]$, $W_S(\tau)$ is the best welfare of any separating equilibrium;
• $W_S$ is strictly decreasing, and $W_P<W_S(\tau^*)$;
• $W_P<W_S(\tau)$ exactly when $\tau<\tau_0$;
• above $\tau_{FB}$ there is no equilibrium with trade.

Together these say that the smallest tilting tax $\tau^*$ is the optimal FTT and that it is strictly positive.

Milestones

Proposition 2 (separating equilibria and the bounds $\underline T_L\le T_L\le\bar T_L$); the monotonicity $\partial\bar T_L/\partial\tau<0$; Proposition 3 (pooling equilibria exist iff (22)); Proposition 4 (which equilibria coexist); the welfare formulas (24)–(25); Corollary 1 (ii) (a high enough tax rules out pooling); the $\tau_0$ step and the $\tau^*$ step of the proof of Proposition 6; and the existence of parameters satisfying all hypotheses of the goal.

Significance

The result turns a qualitative policy argument into a formula. When information is valuable relative to the liquidity gains from trade, the welfare-maximizing tax is the threshold $\tau^*$. This threshold is determined only by the discount-factor ratio and the information gap $\bar F/\bar F_L$, and it is strictly positive. It does not depend on the level of pooling trade. A tax larger than $\tau^*$ only destroys more trade in the separating equilibrium. A tax at or below $\tau^*$ changes nothing.

The paper's proofs are explicit algebra. A formal development checks them, and the drafting already found several places where the printed statements are wrong at a boundary:

• Proposition 2 (i) fails when $\delta_I=(1+\tau)\delta_U$;
• Proposition 4 (i) fails at equality with $\bar F/\bar F_L$;
• the pooling equilibrium still exists at $\tau^*$ itself, so the claimed range "$[\tau^*,\bar\tau)$" of welfare-improving taxes is wrong at its left end;
• the printed sufficient condition $v>\frac{V_H-V_L}{V_H+V_L}V_L$ for $\tau^*<\tau_0$ is false.

The mission states the corrected versions. None of these results has a machine-checked proof.

Difficulty

Each step is elementary real algebra, but there are many of them, and they all depend on the deviation constraint. The informed trader may deviate to any quantity $T'\in[0,1]$, so every equilibrium condition quantifies over a continuum. In the pooling case the binding deviation is $T'\to 1$, which is excluded when $T_P=1$. Characterizing the equilibria therefore needs a supremum argument over a punctured interval, not a finite check. The goal combines both characterizations with a sign analysis of the linear-fractional function $\tau\mapsto W_S(\tau)-W_P$ and the order of $\tau^*$, $\tau_0$ and $\tau_{FB}$. A tempting shortcut is to identify equilibria with the closed-form conditions (17) and (22). That assumes Propositions 2 and 3, which are themselves milestones.

Formalization scope

All objects are real numbers. There is no probability space: expectations over the two states are written out as $\beta(\cdot)+(1-\beta)(\cdot)$. The parameters form a structure Firm. The hypotheses are named predicates: Standing for (1), (3), $F_H>F_L$, $\bar F_H>\bar F_L$, $\delta_U<\delta_I$, together with the disclosed readings $\delta_U>0$ and $0<\beta<1$; Spec23 for (23); and Coexist for Proposition 4 (ii). Every ratio condition is cross-multiplied, so division by zero never decides a statement. The bounds $\bar T_L$, $\underline T_L$, $\underline T_P$ and the taxes $\tau^*$, $\tau_0$, $\tau_{FB}$ are the printed closed forms. They are used only where their denominators are positive.

The equilibrium predicates IsSeparatingEq and IsPoolingEq encode the paper's participation and incentive constraints (14), (16), (31) and (20), (21) directly, with the deviation $T'$ ranging over all of $[0,1]$ except the equilibrium trades. They are not defined through the existence conditions (17) or (22). Welfare is the bracket of (8), evaluated at the realized firm values, not the closed forms (24)–(25). These choices rule out the trivializing formalization in which the propositions hold by definition.

Not formalized:

• Proposition 1 (benchmark);
• Proposition 5 (the cut-off $\bar v$, which the goal replaces by its consequence $W_P<W_S(0)$);
• the $\bar\tau=\tau_1$ variant of Proposition 6;
• Proposition 7 and Corollary 2;
• Corollary 1 (i);
• the extensions of §6.

Only Mathlib's ordered-field and calculus libraries are needed. Proofs of any milestone are welcome. The supremum lemma for punctured intervals is reusable in other signaling models with a continuum of deviations.

Selected references

• T. Dieler, S. Biswas, G. Calzolari, F. Castiglionesi, Asset Trade, Real Investment and a Tilting Financial Transaction Tax, Management Science 69(4), 2023. https://doi.org/10.1287/mnsc.2022.4417 (accepted manuscript, January 24, 2022: https://ssrn.com/abstract=2739357)

Motivation

Dividing indivisible goods fairly is a central problem of fair division, with applications from inheritance and course allocation to the division of computing resources. Since envy-free allocations of indivisible goods need not exist (one good, two agents), the field studies relaxations. The most prominent is envy-freeness up to any good (EFX): no agent prefers another agent's bundle after removing any single good from it. Whether EFX allocations always exist for additive valuations is one of the main open questions of the area; Plaut and Roughgarden (arXiv:1707.04769) suspected that they may not exist for general valuations.

Two lines of relaxation have been pursued: weakening the envy condition by a factor $\alpha<1$, and leaving some goods unallocated ("charity").

• 2004: Lipton, Markakis, Mossel and Saberi introduce envy-cycle elimination (doi:10.1145/988772.988792).
• 2018: Plaut and Roughgarden show that $\tfrac12$-EFX allocations exist (arXiv:1707.04769).
• 2019: Caragiannis, Gravin and Huang show that a partial EFX allocation with high Nash welfare exists (arXiv:1902.04319).
• 2020: Amanatidis, Markakis and Ntokos obtain $0.618$-EFX allocations (arXiv:1909.07650).
• 2020: Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that a partial EFX allocation exists with at most $n-1$ unallocated goods, none of which anybody envies (arXiv:1907.04596).
• 2020–2021: EFX allocations exist for three additive agents (Chaudhury, Garg, Mehlhorn, arXiv:2002.05119); Berger, Cohen, Feldman and Fiat reduce the charity to $n-2$ goods (arXiv:2102.10654).
• 2021: Chaudhury, Garg, Mehlhorn, Mehta and Misra (arXiv:2103.01628; Mathematics of Operations Research, 2024) combine both relaxations and obtain a number of unallocated goods sublinear in $n$. This mission formalizes that result.

Setting

There are $n$ agents $[n]$ and a finite set $M$ of $m$ goods. Agent $i$ has an additive valuation: $v_i(S)=\sum_{g\in S}v_i(\{g\})$ with $v_i(\{g\})\ge 0$. A partial allocation $X=\langle X_1,\dots,X_n\rangle$ consists of pairwise disjoint bundles $X_i\subseteq M$; the goods in none of them form the pool $P$ of unallocated goods.

For $\alpha\in(0,1]$, $X$ is $\alpha$-EFX if

$$v_i(X_i)\ \ge\ \alpha\cdot v_i(X_j\setminus\{g\})\qquad\text{for all agents } i,j \text{ and every } g\in X_j .$$

Fix $\varepsilon\in(0,1)$. Agent $i$ heavily envies a set $S$ if $v_i(X_i)<(1-\varepsilon)v_i(S)$ and strongly envies $S$ if it heavily envies a proper subset of $S$. The envy graph $E_X$ has an edge $i\to j$ when $v_i(X_i)<v_i(X_j)$; a source is an agent nobody envies.

The rainbow cycle number $R(d)$ (Definition 2) is the largest $k$ for which there is a directed graph whose vertex set is split into $k$ parts, each of size at most $d$, such that every vertex has an incoming edge from every other part, but no directed cycle visits each part at most once. In the paper the parts of such a graph are indexed by low-demand unallocated goods, and the graph records which agents are "champions" for which bundles (the group champion graph).

Formalization targets

Goal: Theorem 1

For all $n\ge1$, all additive valuations and all $\varepsilon\in(0,1/2]$ there is a partial allocation $X$ that is $(1-\varepsilon)$-EFX and leaves a pool $P$ with

$$|P|\ \le\ 64\,(n/\varepsilon)^{4/5}.$$

The combinatorial bound: Theorem 3

For every $d\ge1$, $R(d)$ is finite and

$$R(d)\le d^4+d ;$$

equivalently, every digraph with more than $d^4+d$ parts of size at most $d$ in which every vertex has an incoming edge from every other part contains a cycle visiting each part at most once.

The reduction

The milestones follow the paper's proof: the update rules U1, U2, U3 (Lemmas 8–10) and envy-cycle elimination (Lemma 6); the high-demand bound $|H_X|<2n/(\varepsilon d)$ under the standing assumption (*) (Observation 12); the in-edge property of the group champion graph (Observation 13); the conversion of a rainbow cycle into a strictly Pareto-improving allocation (Lemma 14, Lemma 16); and the final count with $d=\lceil (n/\varepsilon)^{1/5}\rceil$.

Significance

The result. Theorem 1 is the first guarantee for EFX-type allocations in which the number of unallocated goods grows sublinearly in the number of agents. It shows that the relaxation by a factor $1-\varepsilon$ can be traded for a large reduction in charity, and it isolates a purely graph-theoretic quantity, $R(d)$, whose improvement directly improves the bound: $R(d)=\mathcal O(d)$ would give $\mathcal O(\sqrt{n/\varepsilon})$ unallocated goods. For $n\le 64^5\varepsilon^{-4}$ (about $10^9$ at $\varepsilon=1/2$) the goal already follows from the $n-1$ bound of Chaudhury et al. 2020, which is posed on the platform but unproved; the content of the goal is the sublinear regime of large $n$.

Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formalization produces a reusable account of approximate EFX, most envious agents and the update rules, and a standalone combinatorial theorem on cycles in multipartite digraphs that can be reused independently of fair division. Sharper bounds on $R(d)$, or the paper's existence bound in terms of $h(d)=d\cdot R(d)$, are natural follow-ups.

Difficulty

The fair-division part is a potential argument: as long as one of the update rules applies, the allocation strictly improves, and the work is to show that a rule applies whenever too many goods are unallocated. The high-demand goods are counted directly. The low-demand goods are the hard part: a rule applies to them only if the group champion graph has a cycle that uses each good at most once, and nothing about a single good or a single pair of goods forces such a cycle. A Ramsey argument on the configurations between pairs of parts shows that $R(d)$ is finite, but only with a bound exponential in $d$, which does not give a sublinear count. The polynomial bound $R(d)\le d^4+d$ requires a different construction.

Formalization scope

Agents are Fin n and goods Fin m, with all of Fin m as the set of goods; valuations are Fin n → Finset (Fin m) → ℝ with the published predicate LittleCharity.MMS.IsAdditive. Allocations, the pool, the envy graph, sources and reachability come from the published LittleCharity.EFX.Setting. The mission's own definitions are in RainbowEFX.Sublinear.Setting.

Conventions committed to:

• Polynomial time is not formalized. Every "in polynomial time, we can determine $X'$" is stated as "there exists $X'$". An existential "there is an algorithm" over a finite search space would be trivial; the paper itself separates existence from the algorithm (Theorem 17).
• $n\ge1$ is assumed in Theorem 1, Observation 12, Lemma 16 and the final count. With no agents the bound $64(n/\varepsilon)^{4/5}$ is $0$.
• The approximation factor is $1-\varepsilon$ with $\varepsilon\in(0,1/2]$, fixed in the goal; §3 statements are stated for all $\varepsilon\in(0,1)$.
• Strong Pareto domination $X'>_{PD}X$ requires $(1-\varepsilon)v_{i'}(X'_{i'})>v_{i'}(X_{i'})$ strictly for some $i'$; the printed non-strict inequality would be satisfied with no improvement.
• The champion of a set is read as any most envious agent of it.
• $R(d)$ counts graphs whose parts have between $1$ and $d$ vertices; with empty parts allowed $R(d)$ would be infinite. It is a natural-number supremum, so Theorem 3 also asserts boundedness, and states the cycle-existence form directly; a bare rainbowCycleNumber d ≤ d^4 + d would hold vacuously for an unbounded set.
• Lemma 16 and the count carry the §4 standing assumption (*): $E_X$ acyclic and neither U1 nor U2 applicable.

A formalization in which the pool is an independent variable, the factor $1-\varepsilon$ is replaced by a weaker one, or $R(d)$ is computed as a junk supremum would trivialize the targets; the statements rule these out. The development needs basic finite combinatorics of digraphs and finite sets, and finite sums of real valuations; no measure theory or probability. Proofs of the update rules, of Theorem 3, and of any milestone independently are welcome.

Selected references

• B. R. Chaudhury, J. Garg, K. Mehlhorn, R. Mehta, P. Misra, Improving EFX Guarantees through Rainbow Cycle Number, arXiv:2103.01628v1, 2021; published as Improving Envy Freeness up to Any Good Guarantees Through Rainbow Cycle Number, Mathematics of Operations Research, 2024. https://arxiv.org/abs/2103.01628
• B. R. Chaudhury, T. Kavitha, K. Mehlhorn, A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, SODA 2020. https://arxiv.org/abs/1907.04596
• R. J. Lipton, E. Markakis, E. Mossel, A. Saberi, On Approximately Fair Allocations of Indivisible Goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
• B. Plaut, T. Roughgarden, Almost Envy-Freeness with General Valuations, SODA 2018. https://arxiv.org/abs/1707.04769
• G. Amanatidis, E. Markakis, A. Ntokos, Multiple Birds with One Stone: Beating 1/2 for EFX and GMMS via Envy Cycle Elimination, Theoretical Computer Science 841, 2020. https://arxiv.org/abs/1909.07650
• I. Caragiannis, N. Gravin, X. Huang, Envy-Freeness up to Any Item with High Nash Welfare: The Virtue of Donating Items, ACM EC 2019. https://arxiv.org/abs/1902.04319
• B. R. Chaudhury, J. Garg, K. Mehlhorn, EFX Exists for Three Agents, ACM EC 2020. https://arxiv.org/abs/2002.05119
• B. Berger, A. Cohen, M. Feldman, A. Fiat, (Almost Full) EFX Exists for Four Agents (and Beyond), arXiv:2102.10654, 2021. https://arxiv.org/abs/2102.10654