All missions

Why customized returns matter

Many sellers accept returns of standard goods but restrict returns of customized goods. A customized item is more likely to fit its buyer, yet it may be harder for the seller to recover value when it comes back. Choosing a return policy therefore changes both what customers buy and how many units they return. Esenduran, Letizia, and Ovchinnikov study this tradeoff in a two-product market and show that permitting customized-product returns can, for some parameters, raise the firm's profit while reducing its total return volume (accepted manuscript, Proposition 2, p. 11). The result is an existence statement about a firm's optimal policy, not a claim that permissive returns always have this effect.

Consumers, products, and the firm's policy

A unit mass of consumers has taste $t$ uniformly distributed over $[0,1]$. The standard product is located at $t=1$ and has baseline willingness to pay $\mathrm{WTP}_s(t)=t$. The customized product changes both a direct-value attribute and a taste-related attribute; its baseline willingness to pay is $\mathrm{WTP}_c(t)=1+\alpha_c-(1-\beta_c)(1-t)$. Here $\alpha_c$ may have either sign, while $0<\beta_c\le1$ measures the taste improvement. These are the paper's normalized expressions, with the reservation value set to one (§2.2, pp. 5–6).

Product $i\in\{c,s\}$ matches a consumer's needs with probability $m_i$; after a mismatch, the consumer values it at only $\theta\mathrm{WTP}_i(t)$, where $0\le\theta<1$. The firm chooses a nonnegative price $p_i$ and a nonnegative return fee $f_i$ for each product. A buyer learns whether the product matches after buying and keeps it exactly when keeping gives at least the payoff $-f_i$ from returning it. Before purchase, the consumer compares the two expected utilities, including this return option, and buys only if the best one is positive. A tie between products goes to the standard product. These rules determine the buyer volumes $Q_i$, the mismatch-return segments $Q_i^R$, and the keep segments $Q_i^K$. The expected number of returns is $R_i=(1-m_i)Q_i^R$ (§2.3, p. 7; problem (3), p. 10).

With production cost $k_i$ and recovered value $r_i$ on a returned unit, the firm's expected profit and total return volume are

$$\Pi(p,f)=\sum_{i\in\{c,s\}}\bigl[Q_i(p_i-k_i)+R_i(f_i+r_i-p_i)\bigr], \qquad R_{\mathrm{tot}}=R_c+R_s.$$

An optimal policy maximizes this profit over all nonnegative prices and fees. In the paper's disallow counterfactual, the standard product's price and fee remain at the original optimal policy's values, while the customized price and fee are chosen to maximize profit subject to $R_c=0$. The proof writes this as problem (5) in the Solution 2 region (Online Appendix pp. 14–15).

Formalization targets

The goal is Proposition 2. There exist admissible parameters and an original optimum such that customized returns occur, and for every original optimum and every associated disallow-counterfactual optimum,

$$R_c^*>0,\qquad \Pi^*>\Pi_{\mathrm{no\ }c\mathrm{\ returns}}^*,\qquad R_{\mathrm{tot}}^*<R_{\mathrm{tot,no\ }c\mathrm{\ returns}}^*.$$

Both optimization problems must attain their maxima. The quantified claim is what “can increase profits and reduce total returns” means in this model; it does not replace an optimum by a preselected formula.

Three milestones trace the part of the paper used for this existence result. Solution 2 characterizes an original optimum with positive customized-return and standard-return segments, a positive standard-keep segment, and no customized-keep segment. Solution 2b characterizes the corresponding optimum when customized returns are disallowed and the standard terms stay fixed. Their returns identity expresses the difference in total return volumes as a factor containing $W=m_s(1-m_c)-m_c(1-m_s)(1-\beta_c)$; away from the boundary $r_s=r_s^{SB2}(r_c)$, that difference is negative exactly when $W<0$ (Online Appendix pp. 4–5, 15).

What the result establishes

The paper's claim separates the total number of returns from the permissiveness of one product's return policy. A permissive customized policy may induce some consumers to switch away from standard goods. Since customized goods match preferences more often, those switches can outweigh returns from newly served buyers; profit can rise at the same time. Thus a firm cannot infer total return volume by looking only at the customized product's own returns (§3.2, p. 11).

The paper proves the result analytically. This mission records its model, optimization comparison, and three central statements in Lean; the theorem proofs are open formalization work. A completed development would certify the global optimum comparison, including existence and all admissible nonnegative policies, as well as the algebraic segment identity. The definitions of consumer choice, return volumes, and the constrained counterfactual can also support formalizations of the paper's other solution regions and robustness results.

Where the formalization is difficult

The return option makes each consumer's expected utility piecewise linear in taste. Which product a consumer buys depends on the upper envelope of two such functions and zero, so the volumes change formula when thresholds cross. The firm's objective is consequently piecewise rather than one differentiable expression on the full policy space. A stationary formula for one segment ordering is insufficient to establish a global optimum; the proof must account for policies on other orderings and their boundaries. The paper's displayed Solution 2 region also includes parameter points where a fee becomes negative or a segment leaves $[0,1]$, so those expressions alone do not characterize the intended interior policy (Online Appendix A.2, pp. 3–5).

Formalization scope

Lean represents every parameter, price, fee, threshold, profit, and segment size as a real number. Consumer volumes are Lebesgue measures of subsets of $[0,1]$; a consumer purchases only when expected utility is strictly positive. The latter convention follows the proof of Proposition B1 and Table 2, which exclude a buyer with nonpositive expected utility. The paper's p. 7 prose uses a weak inequality; at a zero fee that choice could create a positive-volume tie incompatible with its return accounting. The standard product wins ties between products. The standard product has $\alpha_s=\beta_s=0$ in the definitions (Table 1, p. 7; Online Appendix p. 11).

The standing assumptions include Table 1's parameter ranges, the ordering condition $m_s>\mu_c(1-\beta_c)$, $\mu_i>k_i$, and $m_i+r_i(1-m_i)>k_i$. The lower bounds $m_s\ge0$ and $k_s\ge0$ are made explicit. Milestone formulas that divide by $\theta$ or $1-\beta_c$ assume $\theta>0$ and $\beta_c<1$. The Solution 2 and 2b milestones additionally require an interior feasible region: positive return segments, a positive standard-keep segment, nonnegative standard fee, and less than full market coverage. These added conditions select the solution described in the appendix. The displayed customized price of Solution 2 is not used: at the rational consistency witness it conflicts with the displayed segment sizes. The statements retain those segment sizes and the standard terms, which are the quantities needed for Proposition 2.

The goal quantifies over the firm's actual feasible policies and asserts that both optima exist. Defining “optimal” through a closed-form candidate, omitting the disallow maximum, or using a zero-volume population would erase the comparison. Contributions may address global optimality, the consumer threshold and measure calculations, the counterfactual optimum, or the returns identity. The measure and piecewise optimization results would be reusable for other product-line models.

Selected references

• Esenduran, G., P. Letizia, and A. Ovchinnikov, Customization and Returns, accepted manuscript, Management Science, accepted December 13, 2021. SSRN 3444244. This mission cites the manuscript's printed pages and its Online Appendix.
• Esenduran, G., P. Letizia, and A. Ovchinnikov, Customization and Returns, Management Science, 2022. DOI: 10.1287/mnsc.2022.4305. The typeset pagination is not used for the formal statements.

Motivation

A seller choosing a simple way to sell several items faces a problem when one buyer values both individual items and combinations. Pricing each item or offering the entire set as one bundle is easy to describe; an optimal lottery menu can use many more options. The question is how much revenue this simplicity can cost. Eden, Feldman, Friedler, Talgam-Cohen and Weinberg give a guarantee controlled by how many potentially valuable combinations contain any one item. Their result applies to valuations with complements and feasibility constraints that also create substitutes. The preprint used here is arXiv:1612.04746v2; its theorem and page numbers are the source for this mission.

The paper's lower-bound examples show that dependence on the complementarity degree is needed, up to constants, for the mechanisms under study (§6, pp. 13–15). The mission targets the upper bound, including its stated constant. It does not claim that the stronger lower-bound examples have already been formalized.

Setting

Let $M$ be a finite set of items. A hyperedge $T\subseteq M$ represents a combination with a nonnegative bonus $w(T)$. A fixed feasible family $C\subseteq 2^M$ is downward closed and contains the empty set. A buyer receiving bundle $S$ can obtain the bonuses of a feasible subset $T\subseteq S$, so the induced valuation is

$$v_w(S)=\max_{T\subseteq S,\ T\in C}\sum_{U\subseteq T}w(U).$$

Each weight $w(T)$ is sampled independently from a distribution $D'_T$ with finite support; together they induce a population $D$ of valuations. As in §2, pp. 4–5, weights outside $C$ are zero, and $w(\varnothing)=0$ normalizes the empty bundle's value. The population has complementarity degree at most $d$ when every item belongs to at most $d$ hyperedges for which a positive weight is possible.

A mechanism gives each reported valuation in the finite type space $V$ a lottery over bundles and a payment. The buyer evaluates a lottery by expected value. The mission uses incentive compatibility and individual rationality for truthful mechanisms: a buyer prefers their own report, and participating gives nonnegative utility. Let $\operatorname{Rev}(m)$ be such a mechanism's expected payment.

BREV is the best expected revenue from a single price $p$ for the grand bundle, namely $\sup_p p\Pr[v_w(M)\ge p]$. SREV* is a conservative separate-price benchmark. At item prices $\vec p$, item $i$ contributes its price only when some bundle containing $i$ has strictly positive surplus and every bundle omitting $i$ has nonpositive surplus. The supremum is over all real price vectors; it is the paper's $\operatorname{SREV}^{*}$, rather than a favorable tie-breaking convention for an ordinary item-pricing menu (§2, p. 5).

Formalization targets

The goal is Theorem 3.2, p. 6. For every population of degree at most $d$ and every truthful mechanism $m$,

$$\operatorname{Rev}(m)\le(4d+16)\max\{\operatorname{BREV}(D),\operatorname{SREV}^{*}(D)\}.$$

The milestones follow the paper's two benchmark terms. Corollary 3.1, p. 6 bounds revenue by NON-FAVORITE plus SINGLE. Theorem 4.6, pp. 9–10 specifies a partition of hyperedges returned by Partition-Edges, and Proposition 4.1, p. 7 bounds SINGLE by $4d\operatorname{SREV}^{*}+4\operatorname{BREV}$. For NON-FAVORITE, Lemma 5.1, p. 10 introduces the CORE and TAIL terms at a cutoff $t$; Propositions 5.5 and 5.7, pp. 12–13 bound those terms; and Proposition 5.10, p. 13 gives $\operatorname{NON\text{-}FAVORITE}\le12\operatorname{BREV}$. These seven statements are the mission's intermediate targets.

Significance

The theorem gives a concrete revenue guarantee for two simple selling formats even though the valuation can contain overlapping complementary bonuses and feasibility constraints. It says that, within the stated finite-support model, the better simple benchmark captures at least a $1/(4d+16)$ fraction of the revenue of any truthful, individually rational lottery mechanism. The paper also establishes lower bounds showing that a factor growing with $d$ is inherent for its simple-mechanism comparison (§6).

The mathematical result is proved in the paper. The Lean goal and milestones here are statements awaiting proofs; compilation checks their types and definitions, not their truth. Completing them would create a reusable finite product model for mechanism-design arguments, an explicit version of the strict separate-sale benchmark, and a machine-checked combinatorial partition theorem. Those pieces can support later work on revenue bounds with constrained bundles.

Difficulty

The first apparent shortcut is to compare revenue directly with the best bundle price. It cannot account for instances where value is spread among item prices, while item pricing alone cannot account for large complementary bonuses. The paper therefore has to control two different contributions to its revenue benchmark. In the favorite-hyperedge contribution, overlapping edges make independently chosen bundle prices interact. In the nonfavorite contribution, large weights require a different estimate from bounded weights. The duality benchmark also uses ironed virtual values for discrete distributions; replacing them by un-ironed slopes can change SINGLE. These are specific obstacles to closing the Lean goal, beyond the routine finite-sum bookkeeping (§§3–5).

Formalization scope

The Lean model uses Finset bundles, a downward-closed finite family $C$, and positive masses on finite supports for each hyperedge law. A finite product support gives the expectation and probability operators. The valuation is computed from a realized hypergraph; mechanisms operate on the resulting finite valuation type space. The goal quantifies over each valid mechanism. It does not use a real supremum over mechanism revenues, whose default value on an unbounded set would make the statement misleading. BREV and SREV* do use real suprema over all real prices, matching the paper's price domains.

Favorite regions compare nonempty hyperedges, with an injective rank resolving ties. The paper specifies a lexicographic tie rule; quantifying over ranks includes that choice. SINGLE uses the slope of the least concave majorant of the finite revenue curve, the discrete ironed virtual value implicit in the paper. Figure 1 is represented by its actual sweep and loop, and Theorem 4.6 excludes the empty hyperedge because that input prevents the stated procedure from terminating. Proposition 5.5 specifies $t\ge0$, the domain on which its printed inequality holds. These conventions and the explicit individual-rationality requirement prevent zero-valued or arbitrary-payment cases from trivializing the target.

Contributions toward the published milestones are welcome, including the duality and ironing argument behind Corollary 3.1, the combinatorial theorem for Figure 1, and the finite-support estimates for CORE and TAIL. The listed milestones do not include every supporting lemma from the paper; the remaining posted-price, concentration, and independent-event results may be developed as reusable lemmas where needed. No milestone is weakened to make its proof fit the current library.

Selected references

• A. Eden, M. Feldman, O. Friedler, I. Talgam-Cohen and S. M. Weinberg, A Simple and Approximately Optimal Mechanism for a Buyer with Complements, arXiv:1612.04746v2, 2017; published in Operations Research, 2021. Preprint.

Motivation

Optimal stopping asks when to halt a stochastic process so as to maximize an expected reward. Examples are exercising an American option, selling an asset, or ending a clinical trial. The optimal policy is the solution of a dynamic program over the whole state space. In high dimension it cannot be computed exactly, and the usual approximations (regression on basis functions, as in Longstaff–Schwartz) produce policies that are hard to read: a decision maker cannot see why the policy stops in a given state.

Ciocan and Mišić (Interpretable Optimal Stopping, Management Science 2022; arXiv:1812.07211) propose to restrict the search to tree policies. These are binary decision trees whose split nodes compare one state variable with a threshold and whose leaves say stop or go. The tree is fitted by maximizing the average reward over a finite set of simulated trajectories, which is a sample average approximation (SAA) of the true problem. This mission formalizes the consistency guarantee that justifies the method: as the number of trajectories grows, the optimal SAA value over trees of bounded depth converges almost surely to the optimal true value over the same trees.

Setting

The state of the system is a vector $\mathbf x\in\mathcal X=\mathcal X_1\times\cdots\times\mathcal X_n\subseteq\mathbb R^n$. The process $\mathbf x(1),\dots,\mathbf x(T)$ runs for $T$ periods and starts at a fixed state $\mathbf x(1)=\bar{\mathbf x}$. Stopping in period $t$ in state $\mathbf x$ pays $g(t,\mathbf x)$, and rewards are discounted by a factor $\beta\in[0,1]$ per period.

A stationary policy is a map $\pi:\mathcal X\to\{\mathbf{stop},\mathbf{go}\}$. Its stopping time on a path is $\tau_\pi=\min\{t:\pi(\mathbf x(t))=\mathbf{stop}\}$, and $\tau_\pi=+\infty$ if the policy never stops. Its value is

$$J^\pi(\bar{\mathbf x})=\mathbb E\big[\beta^{\tau_\pi-1}g(\tau_\pi,\mathbf x(\tau_\pi))\big],$$

where a path on which $\pi$ never stops earns $0$. Given trajectories $\mathbf x(\omega,\cdot)$ for $\omega=1,\dots,\Omega$, the sample-average value $\hat J^\pi(\bar{\mathbf x})$ is the average of the same discounted reward over the $\Omega$ trajectories.

A tree policy $\pi(\cdot;\mathcal T,\mathbf v,\boldsymbol\theta,\mathbf a)$ is given by four things:

• a binary tree topology $\mathcal T$;
• for each split node $s$, a split variable index $v(s)$;
• for each split node $s$, a real split point $\theta_s$;
• for each leaf $\ell$, an action $a(\ell)$.

A state descends to the left child of $s$ when $x_{v(s)}\le\theta_s$ and to the right child otherwise, and receives the action of the leaf it reaches. $\Pi_{\mathrm{tree}}(d)$ is the class of tree policies of depth at most $d$. Once $d$ is fixed, the skeletons $(\mathcal T,\mathbf v,\mathbf a)$ form a finite set, but the split points $\boldsymbol\theta\in\mathbb R^{\mathbf{splits}}$ range over a continuum.

The paper's standing assumptions are:

1. Assumption 1: $\mathcal X$ is totally bounded and $\|\mathbf x-\mathbf y\|_\infty\le1$ on $\mathcal X$.
2. Assumption 2: $0\le g(t,\mathbf x)\le G$ for all $t$ and $\mathbf x\in\mathcal X$.
3. Assumption 3: there is a function $f$, strictly increasing and continuous with $f(0)=0$, such that $\Pr[\mathbf x(t)\in A]\le f(\lambda(A))$ for every period $1<t\le T$, where $\lambda$ is Lebesgue measure.

Formalization targets

Goal: Corollary 1 (p. 10)

Fix a depth $d$ and $\epsilon>0$. With probability one there is a finite $\Omega_0$ such that for all $\Omega\ge\Omega_0$,

$$\Big|\sup_{\pi\in\Pi_{\mathrm{tree}}(d)}J^\pi(\bar{\mathbf x})-\sup_{\pi\in\Pi_{\mathrm{tree}}(d)}\hat J^\pi(\bar{\mathbf x})\Big|\le\epsilon.$$

This is the paper's headline consistency result: the optimal SAA value converges almost surely to the optimal tree-policy value.

Milestones

1. Slab bound (proof of Lemma EC.2, p. ec3): $\Pr[x_{v(s)}(t)\in[\min\{\theta_{1s},\theta_{2s}\},\max\{\theta_{1s},\theta_{2s}\}]]\le f(|\theta_{1s}-\theta_{2s}|)$ for $t>1$.
2. Lemma EC.2: if two split-point vectors give the same skeleton and both continue at $\bar{\mathbf x}$, then $|J^{\pi_{\boldsymbol\theta_1}}-J^{\pi_{\boldsymbol\theta_2}}|\le GT\sum_{s}f(|\theta_{1,s}-\theta_{2,s}|)$.
3. Lemma EC.3: the deterministic sample analogue, $|\hat J^{\pi_{\boldsymbol\theta_1}}-\hat J^{\pi_{\boldsymbol\theta_2}}|\le\frac G\Omega\sum_\omega\sum_{t\ne1}\sum_s\mathbb I\{x_{v(s)}(\omega,t)\in\text{slab}_s\}$.
4. Fixed-policy strong law (EC.1.1, p. ec1): for one tree policy, $\hat J^\pi\to J^\pi$ almost surely.
5. Lemma EC.1: for one skeleton, almost surely $\sup_{\boldsymbol\theta}|J^{\pi_{\boldsymbol\theta}}-\hat J^{\pi_{\boldsymbol\theta}}|\le\epsilon$ for all large $\Omega$.
6. Theorem 1 (p. 10): the same, uniformly over all of $\Pi_{\mathrm{tree}}(d)$.

Significance

Corollary 1 is what makes the SAA tree-fitting procedure a consistent estimator of the best interpretable policy. A decision maker who optimizes a depth-$d$ tree on enough simulated trajectories obtains an in-sample value that approximates, to any precision, the true value achievable by depth-$d$ trees. The paper also shows (Section EC.1.2) that the conclusion fails when the depth is unbounded, so the depth restriction is part of the result and not a convenience. Theorem 1, the uniform law behind it, has its own uses: it also controls the out-of-sample value of the SAA-optimal tree.

The results are proved in the paper's electronic companion. To our knowledge they have no machine-checked proof. Formalizing them yields a reusable model of finite-horizon stopping with stationary policies and decision-tree policies, and a uniform strong law for a class of indicator-type functionals that is discontinuous in its parameters. The latter is a pattern that recurs in empirical-risk results for trees and threshold rules.

Difficulty

The strong law gives convergence for one policy at a time, outside a null set that depends on the policy. Uncountably many split points mean uncountably many null sets, so the pointwise law does not yield Theorem 1. The usual fix, a Lipschitz or continuity argument in the parameter, fails because $\hat J^\pi$ is a step function of $\boldsymbol\theta$: moving one threshold past a sampled state changes a decision and the sample value jumps. The jumps of the true value must instead be controlled by the probability that the process visits the thin slab between two thresholds, which is where Assumption 3 enters. The jumps of the sample value must be controlled by the empirical frequency of such visits, uniformly in the thresholds. The first period is excluded throughout, because $\mathbf x(1)=\bar{\mathbf x}$ is deterministic and Assumption 3 does not apply to it.

Formalization scope

• States and paths. States are Fin n → ℝ, whose Mathlib norm is the sup norm $\|\cdot\|_\infty$. Paths are Fin T → (Fin n → ℝ), and periods are 0-indexed (k : Fin T is period $t=k+1$, so $\beta^{\tau-1}$ is β ^ k).
• The process. The process is its path law μ, a probability measure, with $\mathbf x(1)=\bar{\mathbf x}$ and $\mathbf x(t)\in\mathcal X$ almost surely.
• Rewards. $\beta\in[0,1]$ and the rewards g k are measurable. Both are readings of "discounted" and of the expectation on the page.
• The sample. The sample is an i.i.d. sequence of random paths with law μ, measurable and mutually independent (iIndepFun). The page says only "trajectories of the process" and its proofs use the strong law. $\hat J$ averages the first m samples, and "with probability one" is ∀ᵐ.
• Assumption 3. It is imposed on measurable sets of finite Lebesgue measure. The printed codomain $f:[0,\infty)\to[0,1]$ is dropped. As printed, the assumption cannot hold for $n\ge1$, $T\ge2$: a box containing $\mathcal X$ has probability $1$, which forces $f\equiv1$ on a half-line. Dropping the codomain costs nothing, because $r\mapsto f(r)+r$ converts any admissible $[0,1]$-valued $f$.
• Trees. A tree is an inductive skeleton with split variables Fin n and leaf actions. Split points are a function of the node address. A split sends ties left ($x_i\le\theta$). A leaf has depth $0$. $\Pi_{\mathrm{tree}}(d)$ is the type of (skeleton of depth $\le d$, split points), and the suprema in Corollary 1 are real suprema over it. They are genuine suprema because the type is nonempty and the values are bounded in $[0,G]$ (for $\hat J$, almost surely).
• Readings of the lemmas. Lemma EC.2 carries Assumption 1, which its proof uses, although its statement names only Assumptions 2 and 3. The page's "$\boldsymbol\theta\in\mathcal X$" in Lemmas EC.1–EC.3 is read as $\boldsymbol\theta\in\mathbb R^{\mathbf{splits}}$, the stronger statement.

The statements cannot be met by a degenerate policy class or a junk value. $J$ is the expectation under the true law, $\hat J$ the average over i.i.d. trajectories, and the suprema range over every tree of depth at most $d$ with arbitrary real split points. The hypotheses are jointly satisfiable with a nonconstant reward and a split that changes the action. One example is $n=1$, $T=2$, $\mathcal X=[0,1]$, $\mathbf x(2)$ uniform, $g(t,x)=x$ and $f(r)=r$.

A complete development needs:

• measurability of the reward of a tree policy;
• integrability from boundedness;
• the Lebesgue measure of product boxes;
• finiteness of the set of skeletons of bounded depth;
• a covering argument for the bounded range of split points;
• Mathlib's strong_law_ae.

Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 1 through Glivenko–Cantelli or VC-type arguments.

Selected references

• D. F. Ciocan and V. V. Mišić, Interpretable Optimal Stopping, Management Science, 2022. Preprint arXiv:1812.07211v2. https://arxiv.org/abs/1812.07211
• F. A. Longstaff and E. S. Schwartz, Valuing American Options by Simulation: A Simple Least-Squares Approach, Review of Financial Studies 14(1), 2001. https://doi.org/10.1093/rfs/14.1.113
• A. J. Kleywegt, A. Shapiro and T. Homem-de-Mello, The Sample Average Approximation Method for Stochastic Discrete Optimization, SIAM Journal on Optimization 12(2), 2002. https://doi.org/10.1137/S1052623499363220

Motivation

When a bank or firm in a network of mutual obligations cannot meet its liabilities, some rule must decide how much each debtor pays each creditor. The rule used almost universally in the systemic-risk literature is the proportional rule of Eisenberg and Noe (2001): every agent pays its liabilities in full if it can, and otherwise distributes its whole asset value over its creditors in proportion to their claims. Central banks and regulators use it to measure contagion in interbank markets; Elsinger, Lehar and Summer (2006) apply it to the 881 banks reporting to the Austrian Central Bank, and Upper (2011) surveys fifteen such studies.

The rule is usually taken as given. Csóka and Herings (2021) ask which properties of a bankruptcy rule single it out, without assuming in advance that payments depend only on an agent's asset value and liabilities. Their answer is an axiomatization: five basic axioms together with one axiom on splitting an agent into identical copies.

For claims problems (one estate, several claimants) the proportional rule has classical characterizations through nonmanipulability by merging and splitting claims (O'Neill 1982, de Frutos 1999, Moreno-Ternero 2006, Ju, Miyagawa and Sakai 2007). Csóka and Herings show that the network analogue of nonmanipulability is too strong (no rule satisfies it together with the basic axioms) and replace it by invariance to mitosis.

Setting

Agents are natural numbers. A financial network $F = (N, z, L)$ consists of a nonempty finite set $N \subseteq \mathbb N$ of agents, endowments $z_i > 0$ for $i \in N$, and a nonnegative liability matrix $L$ on $N \times N$ with $L_{ii} = 0$; $L_{ij}$ is what $i$ owes $j$. The class of all financial networks is $\mathfrak F$. The relative liability matrix is $\Pi_{ij} = 0$ if $L_{ij} = 0$ and $\Pi_{ij} = L_{ij}/\sum_{k \in N} L_{ik}$ otherwise.

A payment matrix is an element of $\mathcal M(N)$, the nonnegative $N \times N$ matrices with zero diagonal; $P_{ij}$ is the amount $i$ pays $j$. Agent $i$'s asset value is $a_i(N,z,P) = z_i + \sum_{j \in N} P_{ji}$ and its equity is $e_i(N,z,P) = a_i(N,z,P) - \sum_{j \in N} P_{ij}$. For rows, $P_i < L_i$ means $P_{ij} \le L_{ij}$ for all $j$ with strict inequality for some $j$.

A bankruptcy rule $b$ assigns to each $F \in \mathfrak F$ a payment matrix $b(F) \in \mathcal M(N)$ (Definition 2.1). The proportional rule $p$ assigns the solution of

$$P_{ij} = \min\Big\{\Pi_{ij}\Big(z_i + \sum_{k \in N} P_{ki}\Big),\ L_{ij}\Big\}, \qquad i, j \in N. \tag{2.1}$$

The axioms, in the order of the paper:

• claims boundedness: $b(F) \le L$;
• limited liability: $e_i(N,z,b(F)) \ge 0$;
• priority of creditors: $b_i(F) < L_i$ implies $e_i(N,z,b(F)) = 0$;
• continuity: $b(F^n) \to b(F)$ whenever $F^n \to F$, where convergence means that the populations eventually coincide and endowments and liabilities converge;
• impartiality: $L_{ij} = L_{ik}$ implies $b_{ij}(F) = b_{ik}(F)$;
• invariance to mitosis: if agent $j$ is split into $|K|+1$ identical agents $\{j\} \cup K$, each receiving the fraction $1/(|K|+1)$ of $j$'s endowment, liabilities and claims and none toward each other, then the total payments of the copies to, and from, each other agent equal $j$'s original payments, and payments among the other agents do not change.

Formalization targets

Goal: Theorem 4.2

$$\text{(a)}\quad \forall F \in \mathfrak F,\ \exists!\, P \text{ solving (2.1) for } F,$$ $$\text{(b)}\quad b \text{ satisfies the six axioms} \iff \forall F,\ b(F) \text{ solves (2.1) for } F .$$

Part (a) makes $p$ a well-defined bankruptcy rule; part (b) says that $p$ satisfies the axioms and that every rule satisfying them is $p$.

Milestones

1. Uniqueness and existence of the solution of (2.1) (Eisenberg–Noe, Theorem 2, cited on p. 2801).
2. Every solution of (2.1) gives nonnegative equities, and zero equity to any agent not paying in full (Part (I), p. 2808).
3. A limit of solutions of (2.1) along converging networks solves (2.1) for the limit network (Part (I), p. 2808).
4. The split payment matrix (A.1) solves (2.1) for the split network (Part (I), pp. 2808–2809).
5. Part (I): the proportional rule satisfies the six axioms.
6. Lemma A.1: under impartiality and invariance to mitosis, $L_{ij} = (q/r) L_{ik}$ implies $b_{ij}(F) = (q/r) b_{ik}(F)$.
7. Part II for rational liabilities, without continuity; then Part II in general.

Significance

The theorem justifies the proportional rule by properties rather than by convention. Because the axioms make no assumption on the form of the rule, consequences such as the absence of pairwise netting are derived, not assumed. Together with the paper's Theorem 5.3 (no rule satisfies the basic axioms and full nonmanipulability), it shows that invariance to mitosis is the strongest splitting requirement compatible with the basic axioms.

The result is proved on paper; no part of it, and no part of the Eisenberg–Noe clearing theory, has a machine-checked proof on this platform. A formalization contributes a reusable layer for clearing payments in financial networks: the system (2.1), its existence and uniqueness under strictly positive endowments, nonnegativity and zero-equity properties of clearing vectors, and their continuity in the data. These are the objects every stress-testing model on top of Eisenberg–Noe starts from.

Difficulty

Existence and uniqueness of a solution of (2.1) is a fixed-point statement about a nonlinear, non-contracting map; uniqueness holds only because every endowment is strictly positive, and fails without it (two agents owing each other one unit with no endowments admit both $P = 0$ and $P = L$).

In the characterization direction, impartiality only equalizes payments to equal claims, and invariance to mitosis only relates networks that differ by splitting one agent into identical copies. Neither axiom speaks directly about payments to unequal claims, and splitting reaches only ratios of positive integers. Passing from rational to real liabilities needs continuity of the rule and continuity of $p$, and the latter rests on uniqueness of the clearing vector, so the two halves of the theorem are not independent.

Formalization scope

• Model. Agents are natural numbers and populations are nonempty Finset ℕ; a fixed finite type cannot express mitosis, which creates fresh agents. Endowments, liabilities and payment matrices are functions on $\mathbb N$ (resp. $\mathbb N \times \mathbb N$) that vanish outside the population, as part of the network structure and of $\mathcal M(N)$. All quantities are real.
• Conventions. $\Pi$ is written with the page's case split. Continuity is sequential, exactly in the paper's convergence criterion (eventual equality of populations, coordinatewise convergence of endowments, liabilities and payments); the paper's topology is first countable, so this is continuity. The split network of Axiom 4.1 is a predicate fixing every coordinate of the new network; $K$ is a finite set of fresh agents and may be empty. The divisor $|K|+1$ is real.
• Added hypothesis. In Lemma A.1, $q$ and $r$ are required to be positive integers; the page writes $q, r \in \mathbb N$ and its proof splits agents into $q$ and $r$ copies.
• Goal shape. "$b = p$" is expressed as "$b(F)$ solves (2.1) for every $F$", and the goal also asserts that (2.1) has a unique solution. Without part (a) the iff would be compatible with an empty class of rules satisfying (2.1); a formalization that drops it, or that defines $p$ by choice from an unproved existence claim, is not the theorem.
• Out of scope. Nonmanipulability (Axiom 5.1, Theorem 5.3), the independence examples of Section 6 and Appendix B, and the linear-programming characterization (2.2).
• Welcome contributions. A general Knaster–Tarski proof of existence for (2.1) via Mathlib's OrderHom.lfp, the uniqueness argument under positive endowments, and lemmas on the split network (sums over the copies, the relative liabilities of copies) that serve both Part (I) and Lemma A.1.

Selected references

• P. Csóka, P. J.-J. Herings, An Axiomatization of the Proportional Rule in Financial Networks, Management Science 67(5):2799–2812, 2021. https://doi.org/10.1287/mnsc.2020.3700
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2):236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• H. Elsinger, A. Lehar, M. Summer, Risk Assessment for Banking Systems, Management Science 52(9):1301–1314, 2006. https://doi.org/10.1287/mnsc.1060.0531
• C. Upper, Simulation Methods to Assess the Danger of Contagion in Interbank Markets, Journal of Financial Stability 7(3):111–125, 2011. https://doi.org/10.1016/j.jfs.2010.12.001
• B. O'Neill, A Problem of Rights Arbitration from the Talmud, Mathematical Social Sciences 2(4):345–371, 1982. https://doi.org/10.1016/0165-4896(82)90029-4
• B. Moreno-Ternero, Proportionality and Non-Manipulability in Bankruptcy Problems, International Game Theory Review 8(1):127–139, 2006. https://doi.org/10.1142/S0219198906000825

Motivation

Emergency departments (EDs) are crowded in part by patients whose condition could have been treated by a primary care provider (PCP), while other patients first visit a PCP, are found to be critical, and are sent on to the ED, paying for two visits. Teletriage — a nurse telephone line that assesses symptoms and recommends where to seek care — is widely offered by health systems and insurers as a remedy for both. It is not error-free: a nurse can undertriage a critical patient (advise primary care) or overtriage a sick one (advise the ED). Whether such an imperfect advisor reduces ED usage, or merely sends more worried-but-well patients to the ED, is the question this mission formalizes.

Çakıcı and Mills (M&SOM, 2020; accepted manuscript at SSRN 2849635) model a patient who does not know whether she is merely sick or critical, chooses between the PCP, the ED and a teletriage call, and updates her belief after the call. Their Proposition 3 answers the question in closed form when every patient calls: teletriage reduces ED usage exactly when the overtriage rate is below an explicit threshold, and reduces double-dipping exactly when the undertriage rate is below another.

Setting

A patient is in one of two states, sick ($S$) or critical ($C$), and holds a belief $b\in[0,1]$, the probability that she is critical. Three actions are available.

• PCP: copay $c_P$. A critical patient seen at the PCP is sent on to the ED, so she also pays $c_E$; this is double-dipping. The expected cost is $c_P+b\,c_E$.
• ED: copay $c_E$, which ends the episode.
• Teletriage (TT): copay $c_T$. The line predicts sick (PS) or critical (PC) with undertriage rate $\alpha=\Pr(PS\mid C)$ and overtriage rate $\beta=\Pr(PC\mid S)$. The patient updates her belief by Bayes' rule to $b_{PS}=\alpha b/(\alpha b+(1-\beta)(1-b))$ or $b_{PC}=(1-\alpha)b/((1-\alpha)b+\beta(1-b))$, and then takes the better of PCP and ED at her posterior. She cannot call twice.

Without teletriage the patient's cost is $V_0(b)=\min\{c_E,\,c_P+b\,c_E\}$, minimized by the ED exactly when $b\ge b_0=1-c_P/c_E$. With teletriage it is

$$\tilde V_0(b)=\min\bigl\{c_E,\;c_P+b\,c_E,\;c_T+(\alpha b+(1-\beta)(1-b))V_0(b_{PS})+((1-\alpha)b+\beta(1-b))V_0(b_{PC})\bigr\}.$$

Teletriage is informative when $\alpha+\beta<1$. Proposition 2 of the paper identifies an interval where calling is strictly optimal, bounded by two thresholds

$$\underline b_0=\frac{\beta b_0+\frac{c_T}{c_P}(1-b_0)}{\beta b_0+(1-\alpha)(1-b_0)},\qquad \bar b_0=\frac{(1-\beta)b_0-\frac{c_T}{c_P}(1-b_0)}{(1-\beta)b_0+\alpha(1-b_0)}.$$

Write $\pi^{ED}(b)$ and $\pi^{DD}(b)$ for the probabilities that a patient with belief $b$ who acts optimally ends up at the ED, resp. double-dips, without teletriage, and $\tilde\pi^{ED}(b)$, $\tilde\pi^{DD}(b)$ with it. When beliefs are uniform on $[l,u]$, the population rates are the averages $\pi^{ED}=\frac1{u-l}\int_l^u\pi^{ED}(s)\,ds$, and likewise for the others.

Formalization targets

Goal: Proposition 3

Assume informative teletriage, beliefs uniform on $[l,u]\subseteq[0,1]$, and $\underline b_0<l<b_0<u<\bar b_0$: with teletriage everyone calls, and without it some patients go to the PCP and some to the ED. Then

$$\pi^{ED}-\tilde\pi^{ED}>0\iff\beta<\beta^0=\frac{u-\frac{u^2}{2}-\bigl(b_0-\frac{b_0^2}{2}\bigr)}{u-\frac{u^2}{2}-\bigl(l-\frac{l^2}{2}\bigr)},\qquad \pi^{DD}-\tilde\pi^{DD}>0\iff\alpha<\alpha^0=\frac{b_0^2-l^2}{u^2-l^2}.$$

Milestones

1. The no-teletriage threshold at $b_0$ (§4.1).
2. Proposition 1, informative case: $b_{PS}<b<b_{PC}$ for $0<b<1$, $\alpha+\beta<1$.
3. Steps of the proof of Proposition 2: the auxiliary thresholds $\underline{\underline b}_0\le\underline b_0$, $\bar b_0\le\bar{\bar b}_0$ and where the posteriors fall; the cost of calling outside $(\underline{\underline b}_0,\bar{\bar b}_0)$; the two linear comparisons inside it.
4. Proposition 2.
5. The closed forms of $\pi^{ED},\pi^{DD}$ and $\tilde\pi^{ED},\tilde\pi^{DD}$ (display on p. 11).
6. The closed forms of $\pi^{ED}-\tilde\pi^{ED}$ and $\pi^{DD}-\tilde\pi^{DD}$ (proof of Proposition 3).

Significance

The result separates the two failure modes of a triage line. Overtriage alone governs whether ED visits fall, and undertriage alone governs whether double-dipping falls, with thresholds that depend only on the copays (through $b_0$) and the belief range. A health system can therefore read off, for a given patient population, the overtriage rate a teletriage service must achieve before it relieves the ED. In the paper's example ($c_E=5c_P$, beliefs uniform on $[0.15,0.85]$), $\beta^0=0.025$: with an overtriage rate of 2.5% or more, teletriage does not reduce ED usage even though every patient calls.

The result is proved in the paper; no machine-checked version exists. Formalizing it means checking the full chain from the patient's optimization to the population averages: that the argmin of $\tilde V_0$ produces the threshold structure of Proposition 2 with the stated thresholds, that the per-belief probabilities on p. 11 follow from the optimal actions (including the boundary cases the page leaves implicit), and that the integrals evaluate as claimed. Two printing slips in the proofs (a right-hand side $c_P+b_{PS}c_E$ for $c_P+b\,c_E$, and a denominator $u-l-(\frac{u^2}2+\frac{l^2}2)$ for $u-l-(\frac{u^2}2-\frac{l^2}2)$) are corrected in the milestone statements.

Difficulty

The final integrals are elementary once the integrands are known. The work is in the integrands. $\tilde\pi^{ED}(b)$ is not given; it comes from which of three costs is smallest at $b$, and, for a caller, which provider is chosen at each of two posteriors that are rational functions of $b$. On the calling range the patient must go to the PCP after the prediction sick and to the ED after critical, i.e. $b_{PS}<b_0<b_{PC}$, and this is what makes $\tilde\pi^{ED}(b)=b+\beta(1-b)$. That in turn needs the inequalities $\underline{\underline b}_0\le\underline b_0$ and $\bar b_0\le\bar{\bar b}_0$, which use $c_T\ge0$ and informativeness, and the linearization of the teletriage cost in the middle range. Reading $\tilde\pi^{ED}$ off the display on p. 11 skips exactly this argument.

Formalization scope

Everything lives in the namespace Teletriage.OneShot and in ℝ. A single definition file holds the parameters $(c_P,c_E,c_T,\alpha,\beta)$, the standing assumptions, the posteriors, the costs, the optimal actions, the probabilities, the uniform average and all thresholds.

Conventions:

• Standing assumptions $0<c_P<c_E$, $0\le c_T$, $\alpha,\beta\in[0,1]$. The first three are added. The thresholds divide by $c_P$; $c_P<c_E$ is stated only in passing (p. 12) and makes $b_0\in(0,1)$; $c_T$ is a copayment, and with $c_T<0$ the display of $\tilde\pi^{ED}$ is false. Informativeness $\alpha+\beta<1$ is a separate hypothesis, inherited by Proposition 3 from Proposition 2.
• Ties in the argmin are broken ED ≻ teletriage ≻ PCP (and ED over PCP without teletriage), matching the displays on p. 11. Proposition 2 is stated in its strict open-region reading: at $c_T=0$ teletriage ties the PCP at low beliefs, so the page's "if and only if" at the endpoints is false under any tie rule.
• Probabilities are computed from the optimal actions, never defined by the closed forms on p. 11. Defining $\tilde\pi^{ED}$ or $\tilde\pi^{DD}$ by those displays, or the teletriage cost by its middle-range linear form, would make the goal a calculus exercise and is ruled out.
• Averages are $\frac1{u-l}\int_l^u g$, the paper's $\int_0^1 g f$ with the Uniform$[l,u]$ density. No integrability hypotheses are added: the integrands are piecewise linear, and proving their integrability is part of the work.
• Lean's division returns $0$ on a zero denominator. The posteriors are only used multiplied by the probability of their prediction, so a junk value never enters a cost or a probability.

Not in scope: the traditional-access model (Propositions 4–5), the open- vs traditional-access comparisons (Propositions 6–7, Corollaries 1–2), the sequential POMDP (Lemma 1, Propositions 8–9), and the uninformative cases of Proposition 1.

Welcome contributions: proofs of the milestones in any order. The algebra of milestones 3–4 is self-contained and reusable for the traditional-access analogue (Proposition 4).

Selected references

• Ö. E. Çakıcı and A. F. Mills, On the Role of Teletriage in Healthcare Demand Management, Manufacturing & Service Operations Management, 2020. https://doi.org/10.1287/msom.2020.0908 (accepted manuscript: https://ssrn.com/abstract=2849635)
• T. Ayer, O. Alagoz and N. K. Stout, OR Forum—A POMDP Approach to Personalize Mammography Screening Decisions, Operations Research 60(5), 2012. https://doi.org/10.1287/opre.1110.1019

Motivation

Loot boxes are a selling format for virtual items in video games and digital collectibles: the customer pays a fixed price for a box whose content is a random item from a catalog. They generate a large share of revenue in the game industry and have drawn regulatory attention because the customer does not know what they are buying. From the seller's side they are a form of probabilistic selling, close to bundling: a box is a lottery over the catalog, and repeated purchases let a customer assemble a collection.

Chen, Elmachtoub, Hamilton and Lei (Loot Box Pricing and Design, Management Science 2021; the mission follows the authors' manuscript submitted in August 2019) compare two designs. A unique box never repeats an item the customer owns; a traditional box draws uniformly from the whole catalog, so duplicates occur. Their headline asymptotic results are that, as the catalog grows, the optimal unique box earns the mean valuation $\mu$ per item, as much as the grand bundle (Theorem 2), while the optimal traditional box earns exactly a fraction $1/e$ of it (Theorem 3). This mission formalizes the traditional-box result.

Setting

A monopolist sells $N \ge 1$ distinct virtual items. A customer's valuations $V_1, \dots, V_N$ are i.i.d. with a law $F$ on $[0,\infty)$ with mean $\mu$ and finite variance $\sigma^2$. A second copy of an item is worth nothing.

The seller offers a traditional box at a fixed price $p > 0$ in every period. Each box contains an item drawn uniformly at random from $[N]$, independently of the valuations and of earlier draws. Let $S_t$ be the set of distinct items owned before the $t$-th box, so $S_1 = \emptyset$. The expected utility of the $t$-th box is

$$U_t = \frac{1}{N}\sum_{i \in [N]\setminus S_t} V_i \;-\; p .$$

The customer is myopic: they buy the $t$-th box if and only if $U_t \ge 0$, and the first time $U_t < 0$ they leave for good. The normalized revenue at price $p$ and the optimal normalized revenue are

$$R_{TB}(p) = \frac{p \cdot \mathbb E[\#\text{ of traditional box purchases}]}{N}, \qquad R_{TB} = \sup_{p>0} R_{TB}(p).$$

The milestones use a random walk. For i.i.d. $w_0, w_1, \dots$ with law $F$, the first passage above a level $t$ is $r(t) = \inf\{j \ge 1 : t \le w_0 + \dots + w_{j-1}\}$; the paper's $r_N$ is $r(Np)$. Also $\zeta_N = \sum_{i=1}^N 1/i - \log N - \gamma$, where $\gamma$ is the Euler–Mascheroni constant.

Formalization targets

Goal: Theorem 3, the limit clause (p. 13)

$$\lim_{N\to\infty} R_{TB} = \frac{\mu}{e}.$$

It holds for every valuation law in the model, with no condition on the shape of $F$ beyond non-negativity and a finite variance.

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

1. Eq. (16), index corrected. The revenue identity $R_{TB}(p) = p\,\mathbb E\big[\sum_{k=r_N}^{N} 1/k\big]$.
2. Eq. (17). $\frac{Np}{\mu} \le \mathbb E[r_N] \le \frac{Np}{\mu} + 1 + \frac{\sigma^2}{\mu^2}$ when $\mu > 0$.
3. Eq. (21). $R_{TB}(\mu/e) \ge \frac{\mu}{e}\log\Big(1\big/\big(\frac1e + \frac{1+\sigma^2/\mu^2}{N}\big)\Big)$, the finite-$N$ lower bound of Theorem 3 at an explicit price.
4. Eq. (22). $\mathbb P\big(r_N \le (1-\epsilon)Np/\mu\big) \le \sigma^2\big/\big(\frac{\epsilon^2}{1-\epsilon}Np\mu\big)$ for $0<\epsilon<1$.
5. Eqs. (24)–(26), corrected. For $0 < \epsilon < 1$,

$$R_{TB} \le \frac{\mu e^{\zeta_N-1}}{1-\epsilon} + \frac{\mu}{(1-\epsilon)N} + \frac{(1-\epsilon)\sigma^2(1+\log N)}{\epsilon^2\mu N},$$

whose right-hand side tends to $\mu/e$ when $\epsilon = N^{-1/3}$.

Significance

The result. Theorem 3 quantifies the price of duplicates. A traditional box loses a factor $e$ against the unique box, the grand bundle and the upper bound $\mu$ of the paper's Proposition 1, for every valuation distribution, so in large catalogs the unique box earns about $0.63\mu$ more per item. The constant $1/e$ comes from the interplay between the coupon-collector waiting times $N/(N-j)$ and the price at which the myopic customer stops; the identity and the bounds expose that interplay as a statement about the first passage of a random walk.

Formalizing it. The result is proved on paper, not formalized. Two of the printed steps of the proof need repair: the harmonic-number rewriting in (16) drops one term, and the per-price upper bound (25) derived from it is false at small prices (for $V \equiv 1$, $N = 1000$, $p = 1/N$ the revenue is $\approx 0.007485$ while (25) gives $\approx 0.007014$); its maximization also ignores prices above $\mu/(1-\epsilon)$. The milestones state the corrected claims, and the limit survives. A machine-checked proof therefore settles the headline result independently of the printed argument.

Difficulty

The number of boxes a myopic customer buys depends on all valuations and on the random order in which distinct items arrive, and the index at which the customer stops is not a stopping time of the forward purchase process: whether the customer continues depends on valuations of items not yet collected. Applying Wald-type identities directly to the purchase sequence therefore fails. The revenue identity (16) also mixes two sources of randomness, the coupon-collector waiting times and the values in order of collection, whose independence must be established rather than assumed. On the upper side, the expected first-passage index needs an overshoot bound for renewal processes (Lorden's inequality), which Mathlib does not contain, and the limit needs an upper bound that is uniform over all prices, including prices far above $\mu$ where the per-price estimate of the paper breaks down.

Formalization scope

All declarations live in the namespace LootBox.TB. The valuation law is a probability measure F : Measure ℝ with F (Set.Iio 0) = 0 and MemLp id 2 F; $\mu$ is ∫ x, x ∂F and $\sigma^2$ the centred second moment. The sample space for $N$ items is valuations × draws, (Fin N → ℝ) × (ℕ → Fin N), with the product of Measure.pi of $F$ and Measure.infinitePi of the uniform law on Fin N; draw $t$ is the item of the $(t+1)$-th box. The purchase count is the first $t$ with $U_{t+1}<0$, valued in ℕ∞; expectations are lower Lebesgue integrals and revenues live in ℝ≥0∞, so no expectation is truncated by toReal. The paper's $\max_p$ is a supremum over $p > 0$. The goal is indexed by $N = n + 1$ so that the uniform law is defined. The page's backward walk $C_j$, extended by virtual i.i.d. variables, is represented by the partial sums of an i.i.d. sequence under walkLaw F = Measure.infinitePi (fun _ => F).

The hypothesis $\mu > 0$ appears in the milestones that divide by $\mu$, not in the goal: when $\mu = 0$ nothing is bought and both sides of the limit are $0$. A formalization in which revenue is a real number obtained by toReal, or in which prices may be $0$ (where a customer with zero valuations buys forever), could make bounds vacuous; neither is used here.

A complete development needs the coupon-collector decomposition of the purchase count, the exchangeability of the values in order of collection, Wald's identity and Lorden's overshoot bound for i.i.d. non-negative walks, Chebyshev's inequality (meas_ge_le_variance_div_sq), Jensen's inequality for $-\log$, and the bounds $\log(n+1) \le H_n \le 1 + \log n$ and $\zeta_N \to 0$ (Mathlib's NumberTheory/Harmonic). Wald's identity and Lorden's bound are reusable well beyond this mission. Proofs of individual milestones, and of the renewal-theoretic lemmas they need, are welcome.

Selected references

• N. Chen, A. N. Elmachtoub, M. L. Hamilton, X. Lei, Loot Box Pricing and Design, Management Science 67(8), 2021. https://doi.org/10.1287/mnsc.2020.3748
• G. Lorden, On excess over the boundary, Annals of Mathematical Statistics 41(2), 1970. https://doi.org/10.1214/aoms/1177697092
• Y. Bakos, E. Brynjolfsson, Bundling Information Goods: Pricing, Profits, and Efficiency, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1613
• A. Gut, Stopped Random Walks: Limit Theorems and Applications, 2nd ed., Springer, 2009. https://doi.org/10.1007/978-0-387-87835-5

Motivation

Convex optimization often minimizes a function obtained by applying one convex function to the output of another map. The inner map may be vector valued, and its components need not be linear. To understand sensitivity, optimality conditions, and dual formulations for such a convex composite, one needs its Fenchel conjugate. Standard formulas for an affine inner map do not directly describe a nonlinear, partially defined map. Burke, Hoheisel, and Nguyen treat this setting in finite-dimensional Euclidean spaces and identify conditions under which the conjugate has an exact, attained representation over a polar cone (Burke–Hoheisel–Nguyen, pp. 3, 10).

The paper distinguishes monotonicity of the outer function along the particular epigraph of the inner map from monotonicity throughout the entire cone order. This matters when the outer function behaves well on the points the inner map can reach but does not satisfy a stronger global condition. Its Theorem 12 gives a conjugacy formula under a point-based condition on relative interiors; subsequent results use it to describe subgradients and additive composites (Burke–Hoheisel–Nguyen, pp. 8, 10–13). The mission isolates the conjugacy theorem and the source results that support it.

Setting

Let $E_1$ and $E_2$ be finite-dimensional real inner-product spaces. A closed convex cone $K\subseteq E_2$ defines the relation $u\le_K v$ when $v-u\in K$. Its polar cone is $K^\circ=\{v:\langle v,k\rangle\le0\text{ for all }k\in K\}$. A possibly partial map $F:E_1\to E_2^\bullet$, where $E_2^\bullet$ adjoins one formal value $+\infty^\bullet$, has an effective domain $D=\operatorname{dom}F$ on which its values lie in $E_2$. Its $K$-epigraph is

$$K\text{-epi}F=\{(x,y)\in E_1\times E_2:x\in D,\ y-F(x)\in K\}.$$

The map $F$ is $K$-convex when this set is convex. The paper assumes throughout §4 that $D$ is nonempty (Burke–Hoheisel–Nguyen, pp. 6, 10).

The outer function $g:E_2\to\mathbb R\cup\{+\infty\}$ belongs to $\Gamma(E_2)$: it is proper and convex but need not be lower semicontinuous. The composite $g\circ F$ equals $g(F(x))$ on $D$ and $+\infty$ outside $D$. The key monotonicity condition, numbered (7), is $g(F(x))\le g(y)$ whenever $(x,y)\in K\text{-epi}F$. It is restricted to the epigraph of $F$, unlike global $K$-increasingness (Burke–Hoheisel–Nguyen, pp. 6, 8).

For an extended-real function $f$, the Fenchel conjugate is $f^*(p)=\sup_x\{\langle p,x\rangle-f(x)\}$. The scalarization $\langle v,F\rangle$ takes value $\langle v,F(x)\rangle$ on $D$ and $+\infty$ elsewhere. Its conjugate and the conjugate $g^*$ are combined in the dual function

$$\eta(p)=\inf_{v\in-K^\circ}\bigl\{g^*(v)+\langle v,F\rangle^*(p)\bigr\}.$$

Here $\operatorname{ri}$ means interior relative to the affine hull, and $\operatorname{dom}f$ means the set where $f$ is finite (Burke–Hoheisel–Nguyen, pp. 4, 6, 10).

Formalization targets

The goal is Theorem 12(c). Suppose $K$ is a closed convex cone, $F$ is proper and $K$-convex, $g\in\Gamma(E_2)$ satisfies (7), and the Slater-type condition (10) holds:

$$F(\operatorname{ri}D)\cap\operatorname{ri}(\operatorname{dom}g-K)\ne\varnothing.$$

Then the formula has an actual minimizer at every $p\in E_1$ and the effective domain has an exact description:

$$(g\circ F)^*(p)=\min_{v\in-K^\circ}\bigl\{g^*(v)+\langle v,F\rangle^*(p)\bigr\},$$ $$\operatorname{dom}(g\circ F)^*=\{p:\exists v\in\operatorname{dom}g^*\cap(-K^\circ),\ \langle v,F\rangle^*(p)<+\infty\}.$$

The milestones follow results stated in the paper: Theorem 2 on conjugacy and infimal convolution; Lemma 6 on support functions; Lemma 4 on the relative interior of a $K$-epigraph; and parts (a) and (b) of Theorem 12, which establish a closure bound and properness with attainment for $\eta$ (Burke–Hoheisel–Nguyen, pp. 5–7, 10).

Significance

The theorem turns the conjugate of a nonlinear composite into a minimization over the negative polar cone. It also identifies exactly which dual arguments give a finite value. Attainment matters because later subgradient formulas can use a specific minimizing multiplier rather than only an approximating sequence. In this paper, Theorem 12 is followed by a subdifferential formula for $g\circ F$ and a formula for the additive composite $f+g\circ F$ (Burke–Hoheisel–Nguyen, pp. 10–13).

The mathematical theorem is proved in the source paper. The formalization task is to give its statement a machine-checkable meaning and then prove that statement from a reusable collection of facts about extended-real conjugacy, support functions, cones, and relative interiors. The imported definitions of conjugacy and closed convex cones already have published formal interfaces; the paper-specific definitions and theorems in this mission are draft statements and do not yet have machine-checked proofs.

Difficulty

The main obstruction is the interaction between closure and conjugacy of a sum. A direct interchange of a supremum over primal points and an infimum over cone multipliers does not itself establish equality or the existence of a minimizing multiplier. Theorem 2 supplies a finite-dimensional conjugacy rule under a relative-interior qualification, while Lemma 4 identifies the relative interior of the relevant epigraph. The source then needs to account for the extended-real values of a partial map and for an outer function that is convex but may not be lower semicontinuous (Burke–Hoheisel–Nguyen, pp. 5–6, 10–11).

Formalization scope

The Lean model uses finite-dimensional real inner-product spaces and EReal for extended-real values. The partial map $F$ is a pair $(D,F)$: $D$ is its domain, and values of the total representative $F$ outside $D$ are ignored. Properness of $F$ is the explicit hypothesis $D\ne\varnothing$. The effective domain of an extended-real function excludes $+\infty$; this corrects a printed $\le+\infty$ in the paper's definition. Conjugacy, epigraph convexity, $\Gamma_0$, closed convex cones, and polar cones reuse published definitions. The lower semicontinuous hull follows the paper's sequential-limit definition, and $\operatorname{ri}$ is Mathlib's intrinsic interior. Pairings on $E_1\times E_2$ are sums of the two component inner products.

The theorem keeps the infimum and minimizer inside $-K^\circ$, uses relative rather than ordinary interior in (10), and retains the properness and finite-dimensional hypotheses. These conventions prevent a vacuous or weaker encoding. Attainment is a separate existential statement, including the case where the minimum is $+\infty$. The printed $\Gamma_0(E_2)$ in Theorem 12(a)'s scalarization clause is read as $\Gamma_0(E_1)$ because each scalarization has domain $E_1$; the paper's Lemma 10 uses that same space. Theorem 2's closure identity is stated under the added hypothesis $\operatorname{dom}(\operatorname{cl}f)\cap\operatorname{dom}(\operatorname{cl}g)\ne\varnothing$. With the paper's definition of $\operatorname{cl}$ as the lower semicontinuous hull, the unconditional identity fails when $\operatorname{cl}f+\operatorname{cl}g\equiv+\infty$. The cited source theorem uses a closure that is identically $-\infty$ for improper functions.

The mission develops the definitions of effective domain, closure, infimal convolution, indicators and support functions, $K$-epigraphs, scalarizations, condition (7), and $\eta$. Contributions proving the listed milestones or building general lemmas for those definitions are in scope. Corollaries 14 and 16, the other corollaries of §4, and the applications of §5 are outside this mission (Burke–Hoheisel–Nguyen, pp. 11–27).

Selected references

• J. V. Burke, T. Hoheisel, and Q. V. Nguyen, A Study of Convex Convex-Composite Functions via Infimal Convolution with Applications, Mathematics of Operations Research (2021), read as arXiv:1907.08318v2.

Motivation

Allocating divisible resources among agents with money-like budgets is the setting of Fisher markets. When agents report their preferences, a central planner can compute a market equilibrium, and by the Eisenberg–Gale convex program that equilibrium maximizes the Nash social welfare, the budget-weighted geometric mean of utilities. This objective is a standard compromise between efficiency and fairness, and is scale-free in each agent's utility.

The catch is that agents may misreport. Brânzei, Gkatzelis and Mehta (arXiv:1607.01569v3, published in Operations Research, 2022) ask how much Nash social welfare is lost when agents act strategically in simple market mechanisms, measured by the price of anarchy: the worst ratio between the optimal Nash social welfare and the welfare at a pure Nash equilibrium. One of the mechanisms they study is the Trading Post game of Shapley and Shubik (Shapley–Shubik 1977), in which each agent splits its budget into bids on the goods, and each good is shared in proportion to the bids it receives.

For agents with Leontief (perfect-complements) utilities, the plain Trading Post game may have no pure equilibrium at all (Example 4.4 of the paper). The paper repairs this with a small entrance fee $\Delta$: a bid below $\Delta$ buys nothing. This mission formalizes the main result of §4.2: with a small enough fee, every pure Nash equilibrium has Nash social welfare within a factor $1+\epsilon$ of the optimum.

Setting

There are $n$ agents and $m \ge 1$ divisible goods, one unit of each. Agent $i$ has a valuation vector $v_i \in \mathbb{R}^m_+$, a budget $B_i \ge 1$, and a demand set $D_i = \{j \mid v_{i,j} > 0\}$, assumed nonempty. Its Leontief utility for a bundle $y$ is

$$u_i(y) = \min_{j \in D_i} \frac{y_j}{v_{i,j}},$$

so the agent wants the goods in the fixed ratio $v_{i,1} : \dots : v_{i,m}$. An allocation $x$ is feasible if $x_{i,j} \ge 0$ and $\sum_i x_{i,j} = 1$ for every good. With $B = \sum_i B_i$, the Nash social welfare is

$$\mathrm{NSW}(x) = \Big(\prod_{i=1}^n u_i(x_i)^{B_i}\Big)^{1/B}.$$

In the Trading Post game with entrance fee $\Delta > 0$, $\mathcal{TP}(\Delta)$, agent $i$ chooses bids $b_i \in [0, B_i]^m$ with $\sum_j b_{i,j} = B_i$. A bid is effective, $\bar b_{i,j} = b_{i,j}$, if $b_{i,j} \ge \Delta$, and $\bar b_{i,j} = 0$ otherwise. Agent $i$ receives $x_{i,j} = \bar b_{i,j} / \sum_k \bar b_{k,j}$ of good $j$ when $\bar b_{i,j} > 0$, and nothing otherwise. A profile $b$ is a pure Nash equilibrium if no agent can raise its utility by switching unilaterally to another bid vector.

Throughout §4 the paper assumes perfect competition: each good is demanded by at least two distinct agents.

The proof passes through Fisher-market prices. Given prices $p \ge 0$, let $\phi_i(p) = \sum_j v_{i,j} p_j$ be the cost of one unit of utility for agent $i$. A pair $(p, x)$ is an $\epsilon$-market equilibrium (Definition 4.6) if goods with positive price are sold out, every agent spends exactly its budget, and no bundle $y \ge 0$ that agent $i$ can afford gives it more than $(1+\epsilon)\,u_i(x_i)$.

Formalization targets

Goal: Theorem 4.9

For every $\epsilon > 0$ and every entrance fee $0 < \Delta < \min\{\epsilon/m^2, 1/m\}$, every pure Nash equilibrium $b$ of $\mathcal{TP}(\Delta)$ satisfies

$$\mathrm{NSW}(y) \le (1+\epsilon)\,\mathrm{NSW}\big(x(b)\big) \qquad \text{for every feasible allocation } y,$$

for arbitrary budgets $B_i \ge 1$.

Milestones

The proof has two halves, and the milestones follow them.

1. Equilibrium structure (proof of Theorem 4.7, pp. 14–16). At a pure Nash equilibrium, every bid on a demanded good is positive; every bid is $0$ or at least $\Delta$; on the demanded goods outside the tight set $S_i$ (the goods received in the smallest fraction) the bid is exactly $\Delta$; hence at most $(m-1)\Delta$ is spent outside $S_i$.
2. Theorem 4.7. With $p_j = \sum_i b_{i,j}$ and $x$ the induced allocation, $(p, x)$ is an $\epsilon$-market equilibrium.
3. Fisher-market facts (proof of Theorem 4.8, p. 22). At an $\epsilon$-market equilibrium, $\sum_j p_j = \sum_i B_i$. The optimal affordable utility is $B_i/\phi_i(p)$ (equation (14)). For such prices every feasible $y$ has $\prod_i u_i(y_i)^{B_i} \le \prod_i (B_i/\phi_i(p))^{B_i}$ (inequality (13)).
4. Theorem 4.8. The Nash social welfare at an $\epsilon$-market equilibrium is at least a $1/(1+\epsilon)$ fraction of the optimum.

Significance

The result shows that a decentralized, prior-free mechanism, in which agents only place bids, implements the Nash social welfare objective for perfect complements up to an arbitrarily small loss. By contrast, the paper shows that the centralized Fisher market mechanism with strategic Leontief agents has price of anarchy $n$ (Theorem 3.9), so the bound here is a strong guarantee for a simple mechanism. Theorem 4.8, which the authors flag as of independent interest, says that approximate Leontief market equilibria are approximately optimal for Nash social welfare. That is a robustness statement about the Eisenberg–Gale optimum, useful independently of any game.

The result is proved on paper; nothing here is open mathematically. To our knowledge none of it has been machine-checked. A complete development produces a reusable formal model of Fisher markets with Leontief utilities, $\epsilon$-market equilibria and the Trading Post game, the first such model on the platform, and checks two printed slips that the formalization repairs (see the scope section).

Difficulty

Without the fee, equilibria need not exist, and the natural argument "an equilibrium is a market equilibrium" fails: agents can leave tiny bids on goods they barely need, and the induced prices then misrepresent demand. With the fee, an equilibrium is only an approximate market equilibrium. Each agent is forced to leave a bid of exactly $\Delta$ on its non-tight goods, and the money spent there must be shown to cost at most a factor $1+\epsilon$ in utility. That accounting is where the bound $\Delta < \min\{\epsilon/m^2, 1/m\}$ and the normalization $B_i \ge 1$ enter.

The second half needs a welfare comparison between an approximate equilibrium and the unknown optimum. The paper uses duality for the Eisenberg–Gale program, in the dual form due to Devanur (2009, manuscript). An exact-equilibrium argument does not transfer directly, because approximate optimality of each agent's bundle must be converted into a product bound over all agents with budget weights.

Formalization scope

Agents and goods are Fin n and Fin m; all quantities are real numbers. The standing assumptions are bundled in Standing: $0 < m$, $v_{i,j} \ge 0$, $B_i \ge 1$, and $D_i \ne \emptyset$ for every agent. Perfect competition is a separate predicate. It is a hypothesis of every Trading Post statement and not of the Fisher-market statements. The utility is a finite minimum over $D_i$. The Nash social welfare uses real powers of nonnegative bases. Prices are $p_j = \sum_i b_{i,j}$, as in the proof. Deviations in the game range over the whole strategy set, including bids below the fee.

Three encoding choices are disclosed in the statements:

1. The goal uses Theorem 4.7's fee bound $\min\{\epsilon/m^2, 1/m\}$ for every $\epsilon > 0$. Theorem 4.9 prints $\min\{\epsilon^2/m, 1/m\}$, but its proof applies Theorem 4.7. For $\epsilon \le 1/m$, $\epsilon^2/m \le \epsilon/m^2$, so every fee the printed bound allows is allowed by the corrected one and the goal implies the printed statement; the bounds coincide only at $\epsilon = 1/m$. The printed bound fails for large $\epsilon$.
2. Clause (iii) of Definition 4.6 quantifies over all bundles $y \ge 0$, not the printed $y \in [0,1]^m$. Under the printed reading Theorem 4.8 is false. The proof on p. 22 uses $y \ge 0$.
3. "Price of anarchy at most $1+\epsilon$" and "optimal Nash social welfare" are stated multiplicatively against every feasible allocation. There is no division and no supremum over a possibly empty set of equilibria.

The goal is not trivialized by an empty equilibrium set. A sorry-free sanity check exhibits, for two agents and two goods with $v \equiv 1$ and $B \equiv 1$, a pure Nash equilibrium of $\mathcal{TP}(\Delta)$ for every $0 < \Delta < 1/2$, and an $\epsilon$-market equilibrium for every $\epsilon > 0$.

A complete proof needs weighted AM–GM, which is in Mathlib as Real.geom_mean_le_arith_mean_weighted. It also needs elementary but careful reasoning about best responses in the Trading Post game. The Fisher-market milestones and Theorem 4.8 are reusable for any later work on Leontief markets. Contributions to either half are welcome independently.

Selected references

• S. Brânzei, V. Gkatzelis, R. Mehta, Nash Social Welfare Approximation for Strategic Agents, arXiv:1607.01569v3, 2017; journal version in Operations Research, 2022. https://arxiv.org/abs/1607.01569v3
• L. Shapley, M. Shubik, Trade Using One Commodity as a Means of Payment, Journal of Political Economy 85(5), 1977. https://doi.org/10.1086/260600
• E. Eisenberg, D. Gale, Consensus of Subjective Probabilities: The Pari-Mutuel Method, Annals of Mathematical Statistics 30(1), 1959. https://doi.org/10.1214/aoms/1177706369