Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 16Formalized record≤ 2Open frontier

7 provers on it13 of 14 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 23Formalized record≤ 5Open frontier

39 provers on it15 of 17 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 16Formalized record≤ 2Open frontier

7 provers on it13 of 14 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 23Formalized record≤ 5Open frontier

39 provers on it15 of 17 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Evaluating Stochastic Seeding Strategies in Networks: The Hájek Estimator of the Difference Between Two Seeding Strategies Is Consistent and Asymptotically NormalResearch Paper

Motivation

An experiment may compare two ways to select initial participants in a social network. Each selected seed set can lead to a different outcome, and the experiment observes only the outcome for the seed set actually selected. Chin, Eckles and Ugander study how known selection probabilities let observations from one experimental design estimate the outcomes of two other seeding strategies. Their setting includes one hop targeting and random targeting, but their statistical results apply to any two stochastic strategies with known probabilities. The central result here is their Proposition 2: the Hájek estimator, which normalizes the observed importance weights separately for the two strategies, is consistent and asymptotically normal. These properties are needed to interpret a large experiment's estimated difference and its uncertainty. Chin, Eckles and Ugander, §§2–3.3 and Proposition 2.

Setting

Let $\Omega$ be a countable space of possible seed sets, including any network information that varies across the superpopulation. Strategies $A$ and $B$ give probability mass functions $p_A$ and $p_B$ on $\Omega$ . An experimental design distribution $p_\Delta$ gives the law of each observed seed set. A fixed function $y:\Omega\to\mathbb R$ records the potential outcome for each possible seed set. For a draw $S$ , the observed outcome is $Y=y(S)$ . The design supplies independent draws $S_0,S_1,\ldots$ with common law $p_\Delta$ ; the outcome is a deterministic function of each draw. The paper allows outcomes such as counts and fractions and does not require a finite seed space. Chin, Eckles and Ugander, pp. 8–9.

The strategy means are $\mu_A=\mathbb E_A[Y]$ and $\mu_B=\mathbb E_B[Y]$ . Their difference is the superpopulation contrast $\tau_{\mathrm{sp}}=\mu_A-\mu_B$ . For a seed set $s$ with positive design probability, its importance weights are $w_A(s)=p_A(s)/p_\Delta(s)$ and $w_B(s)=p_B(s)/p_\Delta(s)$ . Write $\bar w_{A,N}=N^{-1}\sum_{i<N}w_A(S_i)$ , with analogous notation for $B$ . The paper's estimator in equation (7) separately normalizes the two sets of weights:

\widetilde\tau_N=\frac1N\sum_{i<N}\left(\frac{w_A(S_i)}{\bar w_{A,N}}-\frac{w_B(S_i)}{\bar w_{B,N}}\right)y(S_i).

The design can be a mixture of $p_A$ and $p_B$ , but the proposition also addresses other designs. The formal statement therefore leaves $p_\Delta$ general. Chin, Eckles and Ugander, equations (2), (4), (5), (7), pp. 9–10.

Formalization targets

The first targets are the weight moment identities, the limits of the four sample averages, and almost sure consistency of $\widetilde\tau_N$ . The joint central limit theorem for those averages and the variance identity connect these to the goal. These targets follow the displays and sentences in the proof of Proposition 2, Appendix A.2. Chin, Eckles and Ugander, pp. 39–40.

The goal is the corrected full strength of Proposition 2. Under full support of the design on the support of either strategy and finite second moments for the four weighted coordinates,

\widetilde\tau_N\longrightarrow\tau_{\mathrm{sp}}\quad\text{almost surely},\qquad \sqrt N(\widetilde\tau_N-\tau_{\mathrm{sp}})\Rightarrow\mathcal N(0,V_{\widetilde\tau}),

where the variance is the value specified by the paper's equation (15),

V_{\widetilde\tau}=\mathbb E_\Delta\!\left[ \left(\frac{\mu_Ap_A(S)-\mu_Bp_B(S)-y(S)(p_A(S)-p_B(S))}{p_\Delta(S)}\right)^2 \right].

The variance is determined by the two strategies, the design, and the outcomes; it is not a free variance parameter. The almost sure limit records the strong form supplied by the sample average law. Chin, Eckles and Ugander, Proposition 2 and equation (15), p. 14.

Significance

The result identifies both the value approached by the normalized estimator and its leading large sample variance. The two normalized terms are correlated because a single observed seed set contributes information about both strategies. Equation (15) retains that dependence, so the uncertainty of their difference is not obtained by adding two separate variance formulas. The paper uses this result to motivate inference for a superpopulation contrast rather than a finite collection of villages, for which a single observation per village does not identify each village's variance. Chin, Eckles and Ugander, §3.3, p. 14.

The mathematical result is published in the cited preprint. This mission asks for a machine checked statement and proof of its corrected version, plus reusable facts about weighted moments, strong laws for transformed samples, and a four coordinate central limit theorem. The proof infrastructure can serve other comparisons of two policies under a common sampling design. The Horvitz–Thompson result in Proposition 1 is related but is a separate theorem and is outside this mission. No proof of Proposition 2 is currently included in the mission's local formalization.

Difficulty

The estimator is a difference of two random ratios. At small sample sizes, either normalizing sum can vanish, and the two ratios are dependent. Applying a variance formula for one self normalized estimate twice would discard their covariance. There is also a source level obstacle: the printed positivity assumption permits the design to omit a seed set on which both strategies assign equal positive probability. Such a set does not affect the strategy contrast pointwise, but it changes the separate means and the normalizing weight expectations. The printed hypothesis therefore does not imply the moment identity used in Appendix A.2. Chin, Eckles and Ugander, Assumption 1, p. 11, and proof of Proposition 2, p. 40.

For example, take three seed sets with $p_A=(1/2,0,1/2)$ , $p_B=(0,1/2,1/2)$ , $p_\Delta=(1/2,1/2,0)$ and $y=(1,0,0)$ . The paper's Assumption 1 holds, but $\tau_{\mathrm{sp}}=1/2$ and the Hájek estimator approaches $1$ . This mission labels the replacement support condition as a correction. The printed intermediate expansion of the delta method variance also has a sign error in a cross term; equation (15) itself is retained. Chin, Eckles and Ugander, pp. 11, 14, 40.

Formalization scope

Lean represents $\Omega$ by an arbitrary countable type with measurable singletons, $p_A,p_B,p_\Delta$ by PMF, and the sample by measurable independent maps from one probability space, each with law $p_\Delta$ . The natural number $N$ is the number of sampled villages: Lean uses draws $S_0,\ldots,S_{N-1}$ in place of the paper's $S_1,\ldots,S_N$ . Probabilities enter real arithmetic through ENNReal.toReal; a PMF assigns finite mass to each point. Full positivity says $p_\Delta(s)>0$ whenever $p_A(s)>0$ or $p_B(s)>0$ . It is stronger than the paper's contrastive Assumption 1 and is needed for the separate means and normalization identities.

The four second moment conditions apply to $w_A$ , $w_B$ , $w_Ay$ , and $w_By$ under $p_\Delta$ . They make the joint covariance finite even when $y$ is unbounded. The consistency milestone uses only the first moments it needs. The variance is the real integral from equation (15), then converted to a nonnegative real variance for Mathlib's Gaussian law. Lean's total division assigns zero weight when $p_\Delta(s)=0$ ; such a seed set is not observed under the design. The estimator is zero at $N=0$ , and a finite sample with a zero normalizing sum uses Lean's division by zero value. The almost sure and distributional limits address the paper's asymptotic claim.

The intended statement includes every countable seed space and every qualifying independent sample. Restricting to a finite seed space, assuming the estimator's limit or a central limit theorem, or selecting an arbitrary Gaussian variance would change the claim. The development needs Mathlib's probability measures, integration, strong law, Gaussian laws, distributional convergence, and moment theory. Contributions that establish the listed milestones or develop the general joint limit and ratio tools are in scope.

Selected references

Chin, Alex, Dean Eckles, and Johan Ugander. Evaluating Stochastic Seeding Strategies in Networks. arXiv:1809.09561v3, 2020. Preprint.

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Graph Theory Operations Research·Captain: mikedeng1

Atomic Dynamic Flow Games: Adaptive vs. Nonadaptive Agents: Every Game of Nonadaptive Agents Admits an Iteratively Dominant Nash EquilibriumResearch Paper

Motivation

Traffic, packet and evacuation networks are often studied with atomic dynamic flows: individual agents move through a network over time, queue at congested links, and each wants to reach its destination as early as possible. The deterministic queuing (Vickrey) model makes the queue at every link explicit: a link has a capacity, and agents beyond it wait in a queue. In the atomic, discrete-time version, simultaneous arrivals at a queue must be ordered by some tie-breaking rule, and that rule decides whether the resulting routing game has an equilibrium.

Hoefer, Mirrokni, Röglin and Teng (2009, 2011) and Werth, Holzhauser and Krumke (2014) studied atomic routing over time in deterministic queuing models, and found non-existence of equilibria and computational hardness in several variants; Harks, Peis, Schmand, Tauer and Vargas Koch (2018) studied competitive packet routing with priority lists. Scarsini, Schröder and Tomala (Operations Research, 2018) proved that a Nash equilibrium exists when priorities are placed on agents, in single-origin, single-destination networks. Cao, Chen, Chen and Wang (Operations Research 2021) showed that with agent priorities and several origins an equilibrium can fail to exist (their Example 3, a rock–paper–scissors cycle). They proposed instead to break ties by edge priorities at each vertex, and proved that equilibria then always exist. This mission formalizes that existence theorem.

Setting

A network instance consists of the following data.

A finite acyclic directed multigraph $G=(V,E)$ with a destination $d$ ; every vertex has a path to $d$ . Every edge has unit capacity and unit length.
At each vertex $v$ , a complete priority order $\prec_v$ on the edges entering $v$ .
At time $0$ , an initial ranked queue $Q^0_e$ on each edge $e$ .
At each time $r\ge1$ and vertex $v$ , a finite ranked set $\Delta_{r,v}$ of agents entering at origin $v$ .

The agent set $\Delta$ is the disjoint union of all these, and may be infinite.

Each agent $i$ chooses at time $0$ a path $P_i$ from his starting vertex to $d$ . For $i\in Q^0_e$ the path must begin with $e$ ; this is his strategy set $\mathcal P_i$ . At every time unit only the head of the queue on an edge leaves it, and it reaches the head of the edge one unit later. Agents entering an edge are ranked by the edge-priority DQ rule, applied in this order:

(R0) initial-queue order;
(R1) an earlier entry ranks higher;
(R2) among simultaneous entries through different edges, higher priority under $\prec_{u_e}$ ranks higher;
(R3) an agent starting at $u_e$ ranks above through-traffic entering at the same time;
(R4) agents with the same origin keep their original ranks.

$t^v_i(p)$ denotes the time agent $i$ reaches vertex $v$ under the profile $p$ , and is $\infty$ if he never does.

The normal-form game $\Gamma^N$ has players $\Delta$ , strategies $\mathcal P_i$ , and cost $t^d_i$ . A profile $p$ is a Nash equilibrium (NE) if $t^d_i(p)\le t^d_i(P'_i,p_{-i})$ for all $i$ and $P'_i\in\mathcal P_i$ . It is an iteratively dominant NE (IDNE) if the agents can be reindexed $1,2,\dots$ such that for every $k$ , every vertex $v$ on $P_k$ and every profile $q$ of the agents outside $[k]=\{1,\dots,k\}$ ,

t^v_k(p_{[k]},q)=\min\{t^v_j(p_{[k-1]},r): j\notin[k-1],\ r \text{ a profile of }\Delta\setminus[k-1]\}.

Formalization targets

Goal: Theorem 1 (p. 12)

\text{every } \Gamma^N \text{ admits a path profile } p \text{ that is an IDNE, and hence an NE.}

The goal makes no finiteness assumption on $\Delta$ and fixes no constants.

Milestones

Selection step (§4.1, p. 14). Given the first $k-1$ agents of the construction, the pruning (S1)–(S3) leaves exactly one candidate pair $(j,P_j)$ .
Lemma EC.2 (p. ec6). For the selected $(k,P_k)$ , any $S\subseteq\Delta\setminus[k-1]$ , $j\in S$ , $v\in P_k$ and any profile $q$ ,

t^v_k(p_{[k]},q_{S\setminus\{k\}})=\ell^v_k[\![k-1]\!]\le t^v_j(p_{[k-1]},q_S).

Reindexing (p. ec3). The selection can be iterated so that every agent receives an index.
Theorem EC.2 (p. ec8). The profile so constructed (a special IDNE) is an IDNE.
IDNE ⇒ NE (§4.1, p. 11).

Significance

The result. Theorem 1 gives an equilibrium for every network with edge priorities: multiple origins, initial queues and an unbounded stream of inflows are all allowed. With agent priorities, equilibrium can fail to exist in exactly this setting. The IDNE carries more structure than an NE. Arrival times along each agent's path are independent of later agents' choices, and no agent who enters later at the same origin overtakes an earlier one. The paper uses these properties in its study of subgame-perfect equilibria for adaptive agents (p. 12; §5).

Formalizing it. The result is proved in the paper; nothing here is open mathematically. To our knowledge no part of it is formalized in any proof assistant. The mission produces:

a reusable, executable model of discrete-time deterministic queuing with priority tie-breaking;
a formal proof of the constructive existence argument.

The paper proves Lemma EC.2 in a transformed game $\bar\Gamma^N$ on an infinite graph (Lemma EC.1). The mission instead states everything directly in $\Gamma^N$ , so a complete development must either carry out the transfer or reprove the lemma natively. For infinitely many agents, the claim that every agent is eventually indexed (milestone 3) is asserted in the paper without a separate argument; the formal proof has to supply one.

Difficulty

The obvious argument fails at the no speed-up property. Adding agents to a network can make some other agent arrive earlier. The paper's Example 4 (pp. 15–16) has such a chain effect: removing an agent delays another. So the claim that agent $k$ 's arrival times are unaffected by everyone after him is not monotonicity of congestion. It holds only for the specific order and paths produced by the selection procedure, and it must be proved by an induction that carries invariance (equality in (EC.2)) and domination (inequality in (EC.2)) together.

The tie-breaking is the second difficulty. The selection compares candidates backwards from $d$ : by arrival time, then by incoming-edge priority, then one edge further back. The argument has to show that this order matches the queue rule (R0)–(R4) at every vertex, including (R3) for agents starting mid-network.

Formalization scope

Everything lives in the namespace AtomicDynFlow.IDNE.

Network and agents. Instance V E A carries the graph as finite types V, E with tail, head, d, and the priorities as lists inc v of incoming edges, highest priority first. Initial queues Q0 e are listed head first, and inflows inflow r v highest original rank first. The standing hypotheses are fields:
- acyclicity, as a height function;
- reachability of $d$ ;
- no inflow at time $0$ ;
- every agent lies in exactly one source list.
The agent type A is arbitrary and may be infinite.
Dynamics. queue π s e is a computable, list-based simulation of the queue on each edge at each time, under a partial profile π : A → Option (List E), where none means the agent is absent. arrival π i v : ℕ∞ is $t^v_i$ , with ⊤ for $\infty$ (p. ec4). The starting-vertex time is $0$ for initial-queue agents and $r$ for $\Delta_{r,v}$ (Algorithm 1, Step 2).
Equilibria. The reindexing of Definition 2 is an injective $\sigma:\Delta\to\mathbb N$ whose range is an initial segment, with agent $a$ receiving index $\sigma(a)+1$ . Definition 2 quantifies over every vertex of the path, the starting vertex included.
Selection. The pruning (S1)–(S3) is a backward pairwise comparison of candidate pairs (Before, IsSelected). Milestones 2 and 4 are $\Gamma^N$ -native versions of the e-companion statements, and Lemma EC.1 is not formalized.

Ruled out. Three encodings would trivialize the goal, and none is used:

arrival times that ignore queuing, under which every profile would be an IDNE;
a profile in which removed agents are frozen rather than absent;
a reindexing that skips agents.

A sorry-free check of the paper's Example 2 shows that agent $i$ waits at $y_1$ and reaches $d$ at time $6$ , and that removing agent $g$ lets him arrive at $5$ .

Welcome contributions: proofs of the milestones in any order. Milestone 5 needs only the definitions. Milestones 1 and 2 are the technical core, and general lemmas about the queue simulation (FIFO within an edge, monotonicity in entry times) are reusable throughout.

Selected references

Z. Cao, B. Chen, X. Chen, C. Wang, Atomic dynamic flow games: adaptive versus nonadaptive agents, Operations Research, 2021; accepted manuscript Oct. 2020, WRAP 143835. https://doi.org/10.1287/opre.2021.2105
M. Scarsini, M. Schröder, T. Tomala, Dynamic atomic congestion games with seasonal flows, Operations Research 66(2):327–339, 2018.
T. Werth, M. Holzhauser, S. Krumke, Atomic routing in a deterministic queuing model, Operations Research Perspectives 1(1):18–41, 2014.
T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4, 2018.
M. Hoefer, V. S. Mirrokni, H. Röglin, S.-H. Teng, Competitive routing over time, Theoretical Computer Science 412(39):5420–5432, 2011.
W. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–260, 1969.

9 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Asymmetric Reporting Timeliness and Informational Feedback: Timely Loss Recognition Raises the Speculator's Gains from Selling on Bad News and Widens the Trading RegionResearch Paper

Motivation

A firm's accounting disclosure affects what traders know. The price produced by their orders can then affect the firm's own investment decision. In this setting, the timing of bad news changes both the speculator's incentive to trade and the information conveyed by market prices. Chen, Huang, Jiang, Zhang and Zhang study this interaction in a finite trading game, asking how timely loss recognition changes gross trading profits and the ranges of trading costs that support trading or no trading. Their result is Proposition 4 of the held working paper, later published under a different title in Management Science (published article).

The model builds on the feedback-effect framework of Edmans, Goldstein and Jiang (AER 2015), in which a firm learns from its own stock's order flow and, as a result, a speculator gains less from selling on bad news than from buying on good news; their firm has no private information of its own. The present paper adds a privately informed firm whose reporting system may disclose good and bad news with different timeliness, a theme of the accounting literature on conservatism. The paper relates its profit comparisons to the strategic-trading intuition of Kyle (Econometrica 1985).

The comparison matters because a disclosure rule that makes bad news public more often also changes what a null disclosure means. A null report can alter the market maker's valuation, while order flow can lead an uninformed firm to change investment. The question is therefore about prices and real decisions together, under the same reporting rule.

Setting

The underlying state is either good, $H$ , or bad, $L$ , each with prior probability $1/2$ . The firm may increase investment, decrease investment, or keep its current level. A correct change adds $x$ to terminal value and costs $c$ ; a wrong change loses $x$ and costs $c$ . Without a change, terminal value is $R_H$ or $R_L$ . The model assumes $0<c<x$ and $R_H-x>R_L+x$ .

The firm privately learns the state with probability $f$ ; otherwise it has a null signal. An informed firm discloses its state with probability $\beta_H$ in state $H$ and $\beta_L$ in state $L$ . Write $\beta=(\beta_H+\beta_L)/2$ and $\xi=(\beta_L-\beta_H)/2$ , so $\beta_H=\beta-\xi$ and $\beta_L=\beta+\xi$ . Positive $\xi$ means bad news is disclosed more promptly than good news. A feasible disclosure rule has $0\leq\beta\pm\xi\leq1$ .

After a null report, a speculator may buy one share, sell one share, or abstain. She learns the state with probability $\lambda$ ; otherwise her private signal is null. An independent noise trader submits an order of $-1$ , $0$ , or $1$ with equal probability. The market maker sees only the total order flow $X$ and prices the share at expected terminal firm value conditional on the report and $X$ . The firm also observes the order flow before its investment decision. When it has no private state signal, it invests only if its posterior exceeds $\bar\mu=1/2+c/(2x)$ , divests only if it falls below $\underline\mu=1/2-c/(2x)$ , and otherwise keeps its investment.

Two speculator strategies are compared. Under no trading (NT) she abstains; $\pi^{NT}_{buy}$ and $\pi^{NT}_{sell}$ are gross profits from deviating to a buy on good news or a sale on bad news. Under trading (T) she buys on good news and sells on bad news; $\pi^T_{buy}$ and $\pi^T_{sell}$ are the corresponding gross profits. Each profit averages over the three noise orders and uses the market maker's Bayesian price and the firm's response under that strategy. Let $\kappa^T=\min\{\pi^T_{buy},\pi^T_{sell}\}$ and $\kappa^{NT}=\max\{\pi^{NT}_{buy},\pi^{NT}_{sell}\}$ . These are the trading cost thresholds reported by Propositions 1 and 2 of the working paper.

Formalization targets

The goal is Proposition 4. For every feasible $\xi$ , selling on bad news becomes more profitable as $\xi$ rises, under both profiles:

\frac{d\pi^T_{sell}}{d\xi}>0,\qquad \frac{d\pi^{NT}_{sell}}{d\xi}>0.

In a neighborhood of neutral reporting, the trading threshold rises with $\xi$ :

\frac{d\kappa^T}{d\xi}>0\quad\text{near }\xi=0.

For every feasible $\widehat\xi>0$ , the no-trading threshold under timely loss recognition exceeds both the neutral threshold and the threshold under the mirrored timely gain policy:

\kappa^{NT}(\widehat\xi)>\kappa^{NT}(0),\qquad \kappa^{NT}(\widehat\xi)>\kappa^{NT}(-\widehat\xi).

The milestone chain establishes the firm's investment rule, the null-report posterior and the probability of an informed firm behind that report, the relevant trading-profile posteriors, the two profiles' gross profit formulas, and the neutral-policy comparisons. The target does not assert that $\kappa^T$ increases across the entire feasible range: the smaller of buying and selling profits can switch away from selling as $\xi$ grows.

Significance

The first claim identifies a strict incentive effect of asymmetric reporting on trading against bad news. The second concerns the trading threshold locally around symmetric reporting, and the third compares the no-trading threshold with neutral reporting and its mirror policy. Together they express how a reporting choice can change the regions of trading cost in which the two profiles are candidates for equilibrium (Chen et al.).

The result is proved in the held working paper. The formalization task is to connect it to an explicit finite Bayesian trading model in Lean. This includes the order-flow likelihoods, the market maker's posterior expected value, the firm's posterior investment rule, and the gross profits averaged over noise orders. Those definitions can support later work on the paper's other trading profiles and on disclosure choices. No machine-checked proof of this mission's goal is claimed here.

Difficulty

The reporting parameter changes more than the posterior probability of $H$ after a null report. It also changes the probability that a firm which made a null report privately knows the state, and hence the value traders expect after the firm's investment decision. The same order flow affects the market maker's price and an uninformed firm's investment. A direct comparison of null-report beliefs alone therefore does not establish the profit inequalities. The minimum defining $\kappa^T$ adds a local regime change: near $\xi=0$ selling is the smaller profit, but that need not remain true at a larger feasible $\xi$ .

Formalization scope

The Lean development uses two finite state constructors, three investment decisions, integer order flows, and real-valued probabilities, values and profits. Disclosure and order-flow posteriors are explicit Bayes ratios. Off-path order flows with zero Bayesian denominator receive the paper's belief convention: $H$ at positive $X$ , $L$ at negative $X$ . The firm's tie-break chooses the status quo at either investment threshold. The speculator's trading cost is excluded from gross profit, as in the paper.

Every theorem carries the paper's standing restrictions $0<c<x$ , $R_H-x>R_L+x$ , $0<\beta<1$ , and $\lambda>2c/(x+c)$ . The formalization also makes explicit $0<f<1$ and $\lambda<1$ : both are probabilities, and endpoint choices destroy strict conclusions used here. Claims about a given $\xi$ require $0\leq\beta\pm\xi\leq1$ . The neighborhood claim is stated as a positive derivative throughout some open interval about zero. In particular, the profits are calculated from the Bayesian prices and the firm's response; they are not defined to equal the closed forms that the milestones ask solvers to prove.

Reusable work includes finite likelihoods, posterior calculations, the optimal investment rule, and algebraic profit reductions. Contributions toward the source-labelled milestone statements and the full derivative comparison are welcome. The held source is the authors' 2018 working paper; its pages and numbering have not been reconciled with the retitled 2021 journal article.

Selected references

Q. Chen, Z. Huang, X. Jiang, G. Zhang and Y. Zhang, The Role of Asymmetric Disclosure When Price Efficiency Affects Real Efficiency, working paper, 2018, held PDF pp. 7–22 and 33–39; published as Asymmetric Reporting Timeliness and Informational Feedback, Management Science, 2021. DOI.
A. Edmans, I. Goldstein and W. Jiang, Feedback Effects, Asymmetric Trading, and the Limits to Arbitrage, American Economic Review 105(12), 3766–3797, 2015. DOI.
A. S. Kyle, Continuous Auctions and Insider Trading, Econometrica 53(6), 1315–1335, 1985. DOI.

10 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Operational Strategies for Distributing Durable Goods in the Base of the Pyramid: At Low Ability to Pay and High Risk Aversion the Profit-Maximizing Allocation Yields the Lowest Consumer SurplusResearch Paper

Motivation

Durable life-improving products such as solar lamps, water filters and clean cookstoves reach few households in the base of the pyramid (BOP), the low-income markets of developing economies. Two frictions explain much of the gap. Customers cannot afford the product (low ability to pay, ATP), and they are uncertain whether an unfamiliar product is worth its price; being poor, they are also risk averse. Distributors and the foundations that fund them must decide how to spend a fixed budget: on subsidies that make the product affordable, on marketing and demonstrations that inform customers, or on return policies that remove the risk of trying.

Calmon, Jue-Rajasingh, Romero and Stenson (M&SOM 24(4), 1887–1905, 2022; accepted manuscript SSRN 2882402) model this decision, motivated by the Indian distributor Essmart. Their headline finding concerns a funder's dilemma: in the BOP, the allocation that maximizes the distributor's profit is often the one that gives customers the lowest average consumer surplus, and the misalignment disappears when the ATP is high. This mission formalizes that finding and the chain of results the paper proves on the way.

Setting

A unit mass of customers values the product at $v_h$ with probability $\beta\in(0,1)$ , and lower otherwise. A fraction $\theta$ of customers is informed and knows its valuation. The rest know only the population distribution. Customers have CARA utility with risk aversion $\alpha>0$ , and all of them can pay at most $m$ , the homogeneous ATP. A distributor buys at wholesale cost $w$ , salvages returned units at $y$ , and values consumer surplus with weight $\gamma\in[0,1)$ .

The distributor has a budget $b$ per customer. It can raise the ATP by a subsidy $x\in[0,v_h-m]$ , and it can raise the education level from $\theta_0$ to $\theta\le1$ at marginal cost $c_\theta$ . A downstream retailer then sets prices and refunds. The resulting pricing outcome is given in closed form by the paper's Proposition B.1:

pricing strategy (a) sells only to informed high-value customers, without returns;
pricing strategy (b) sells to everyone and accepts returns, with the minimum refund

r_\alpha(m)=\max\Big(0,\ m-\tfrac1\alpha\ln\tfrac{1-\beta e^{-\alpha(v_h-m)}}{1-\beta}\Big).

Each strategy has its profit $\Pi^a_D,\Pi^b_D$ and consumer surplus $CS^a,CS^b$ . The budget constraint is $c_\theta(\theta-\theta_0)+xB\le b$ , where the demand $B$ is $\theta\beta$ under (a) and $\beta+(1-\theta)(1-\beta)$ under (b).

Theorem 1 reduces the allocation problem to four strategies:

F: subsidy first, pricing (a);
M: education first, pricing (a);
FR: subsidy first, pricing (b);
MR: education first, pricing (b).

Each strategy has an explicit allocation $(x^i,\theta^i)$ , profit $\Pi^i$ and consumer surplus $CS^i$ . The ATP thresholds are

m^F=\frac{c_\theta/\beta+w-\gamma v_h}{1-\gamma},\quad m^{MR}=v_h-\frac{(1-\beta)(w-y)-c_\theta}{(1-\gamma)\beta},\quad \bar m^{MR}=v_h-\frac{\beta v_h+(1-\beta)y-w}{(1-\gamma)\beta},

and the parameter bounds are $\bar w=\beta v_h+(1-\beta)y$ and $\bar c_\theta=(1-\beta)(w-y)$ .

Formalization targets

Goal: Corollary 1 with Proposition 2

There is a threshold $a^{cs}_F(m)\in[0,\infty]$ such that for every $\alpha>0$ , MR maximizes consumer surplus with $CS^{MR}\ge CS^M\ge CS^F$ , and

CS^F\le\min(CS^{MR},CS^M,CS^{FR})\iff\alpha\ge a^{cs}_F(m).

If $w\le\bar w$ and $c_\theta\le\bar c_\theta$ , then $m^F\le m^{MR},\bar m^{MR}\le v_h$ . There is also a threshold $a_F(m)$ such that

\Pi^F\ge\max(\Pi^M,\Pi^{FR},\Pi^{MR})\iff m\le m^F\ \text{and}\ \alpha\ge a_F(m),

and F is both profit-optimal and worst for consumers iff $m\le m^F$ and $\alpha\ge\max(a_F(m),a^{cs}_F(m))$ . Finally, MR is profit-optimal for all $\alpha$ when $m\ge\max(m^{MR},\bar m^{MR})$ .

Milestones

In attack order:

Theorem 1 in regime form: F/M solve the problem under pricing (a), and FR/MR under (b).
Monotonicity and range of the log term $\tfrac{1-\beta}{\alpha}\ln\tfrac{1-\beta e^{-\alpha(v_h-m)}}{1-\beta}$ .
Lemma B.1, $\theta^M=\theta^{MR}\ge\theta^F\ge\theta^{FR}$ .
Property 1, $\Pi^F\ge\Pi^M\iff m\le m^F$ .
Property 4, a risk-aversion threshold for $\Pi^F\ge\Pi^{FR}$ .
Property 6.
The second statement of Property 5.
The first bullet of Proposition 2.
The threshold for $CS^{FR}\ge CS^F$ .

Significance

The result separates two regimes:

BOP regime (low $m$ , high $\alpha$ ): a profit-maximizing distributor subsidizes customers and refuses returns. Once risk aversion also exceeds $a^{cs}_F(m)$ , this is the strategy with the lowest consumer surplus.
High-ATP regime: education with returns maximizes both profit and surplus.

For a funder whose grant the distributor allocates (p. 10), this means that profit-seeking allocation serves customers well only outside the BOP. The paper's §4.3 goes on to show that an operational commitment, free returns, reduces the misalignment; that extension is not part of this mission.

The results are proved in the paper by direct case analysis; none of them has a machine-checked proof. A complete formalization would make the hypotheses explicit. For example, the paper's list of ATP thresholds includes $w\le m^F$ , which fails for $\gamma>0$ . The proof also claims that $m\ge m^{MR}$ alone makes MR more profitable than F; a counterexample before $\bar m^{MR}$ is recorded in the moderation notes. Formalization would pin down the tie-breaking and degenerate cases that the prose leaves implicit, and provide a reusable model of CARA-refund pricing with budgeted subsidy and education.

Difficulty

Each strategy value is a composition of positive parts, minima, indicator tie-breaks and a log-exponential refund. The comparisons in the strategy map are therefore piecewise in $(m,\alpha)$ , and the obvious approach, writing the closed forms and comparing, breaks into many cases. The threshold statements are harder than inequalities. "F is optimal iff $\alpha\ge a_F(m)$ " asserts that the set of good $\alpha$ is a closed upward ray, so one needs monotonicity in $\alpha$ of every competing value. That includes $\Pi^{FR}$ , whose allocation jumps when the tie-break flips. One also needs closedness at the jump. The consumer-surplus threshold rests on $\theta^{FR}$ being non-decreasing in $\alpha$ , and on the refund term staying within $[0,\beta(v_h-m)]$ .

Formalization scope

Everything is real-valued, in the namespace BOPDistrib.Misalign, with the definitions in one file. The parameters are a structure Params with fields $v_h,\beta,w,y,c_\theta,b,\theta_0,\gamma$ ; $m$ and $\alpha$ are explicit arguments.

The formalization commits to the following conventions.

Pricing stage. It is Proposition B.1's outcome; the retailer game is not re-derived.
Refund. $r_\alpha(m)$ keeps its positive part, and $m-r_\alpha(m)$ stands wherever Proposition B.1 has it.
Strategy values. They are evaluated at the allocations of the proof of Theorem 1, never taken as the closed forms (16)–(17).
FR tie-break. FR's leftover budget is invested iff $y\le y_\theta$ with $y_\theta=w-(1-\gamma)(m-r_\alpha(m))-(v_h-m)$ . This is the proof's indicator; the theorem's text has " $<$ ".
Optimality. "Optimal" and "smallest" are weak inequalities.
Thresholds. The risk-aversion thresholds are existential in $[0,\infty]$ , with $\infty$ meaning never, and fixed before $\alpha$ . The ATP thresholds are pinned to the proof's formulas.

Added standing hypotheses relative to the page:

$\alpha>0$ , since the refund divides by $\alpha$ ;
$\gamma<1$ , since $m^F$ divides by $1-\gamma$ and the paper treats only $\gamma\le1$ ;
$0<\theta_0<1$ and $c_\theta>0$ , which are divisors;
$0\le m$ , since ATP is nonnegative and the refund cannot exceed the customer price;
$m<v_h$ , $b>0$ and the strict homogeneous Assumption 1, $b<c_\theta(1-\theta_0)+\beta(v_h-m)$ . At the boundary the F and M allocations coincide, and "F optimal only if $m\le m^F$ " fails.

A formalization in which the thresholds are chosen after $\alpha$ (so that $\exists a$ is trivial), or in which $\Pi^F$ is compared with closed forms that build in the conclusion, would be vacuous; both are excluded by the statement shapes. The heterogeneous-ATP model of §5, the free-returns setting of §4.3, and the regime $w>\bar w$ or $c_\theta>\bar c_\theta$ are out of scope.

The work needs elementary real analysis: monotonicity of $\tfrac1\alpha\ln(\cdot)$ in $\alpha$ , limits at $0^+$ and $\infty$ , and piecewise-linear optimization over a polygon. Contributions of proofs of any milestone are welcome, as are lemmas on the monotonicity of the refund in $\alpha$ , which every threshold uses.

Selected references

A. P. Calmon, D. Jue-Rajasingh, G. Romero, J. Stenson, Operational strategies for distributing durable goods in the base of the pyramid, Manufacturing & Service Operations Management 24(4), 2022. https://doi.org/10.1287/msom.2022.1106 ; accepted manuscript https://ssrn.com/abstract=2882402

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Bundling for Flexibility and Variety: An Economic Model for Multiproducer Value Aggregation: The Producers' Output Game Has a Unique Equilibrium, Solved in Closed FormResearch Paper

Motivation

Many digital goods are sold as bundles assembled from the output of many independent producers: a streaming service carries films from many studios, a music subscription carries many labels, a news or software aggregator carries many publishers. One retailer (the aggregator) prices the bundle and keeps a share of the revenue. The producers split the rest in proportion to how much content each contributes. Two questions follow. How much does each producer contribute when it competes with the others for the shared revenue? And how many producers can survive with positive output when their costs differ?

H. K. Bhargava's Bundling for Flexibility and Variety: An Economic Model for Multiproducer Value Aggregation (Management Science, 2021, doi:10.1287/mnsc.2020.3662) answers both questions in a stylized model with an explicit equilibrium. Its central result, Lemma 1, gives the retailer's price, the number $K$ of active producers, and every producer's output in closed form. The paper's propositions are then derived from these formulas: how outputs respond to costs, how participation responds to the bundle-size elasticity $\theta$ , and the effects of mergers and of the revenue share $\gamma$ . This mission formalizes Lemma 1 from the author's accepted manuscript (2020).

Setting

There are $I \ge 1$ producers, indexed in ascending order of unit cost, $0 < c_1 \le c_2 \le \dots \le c_I$ . Producer $i$ chooses an output $Q_i \ge 0$ , measured in value units. The bundle has size $Q = \sum_i Q_i$ .

Retailer. For a bundle of size $Q$ the retailer charges a price $P$ . Demand is

D(P,Q) = \sqrt{AQ^\theta - bP}, \qquad 0 < \theta < 2/3,\ b > 0,

with zero demand when $AQ^\theta < bP$ . The retailer's distribution cost per unit of demand is $w^R(Q) = wQ^\theta$ (the paper writes this coefficient as $c$ ). The retailer keeps a fraction $1 - \gamma$ of the surplus, so its profit is

\Pi_R(P,Q) = (1-\gamma)\,(P - wQ^\theta)\,D(P,Q), \qquad 0 < \gamma < 1 .

The sharable surplus $S(Q)$ is the largest value of $(P - wQ^\theta)D(P,Q)$ over all prices $P$ , which is the surplus at the retailer's optimal price. Throughout, $A - bw > 0$ .

Producers. Producer $i$ receives the share $\gamma\,(Q_i/Q)\,S(Q)$ of the surplus and pays $c_iQ_i$ , so its profit is

\pi_i = \gamma\,\frac{Q_i}{Q}\,S(Q) - c_iQ_i .

Producers choose their outputs simultaneously. A profile $(Q_1,\dots,Q_I)$ is a Nash equilibrium if no producer can increase its profit by changing its own output to any other $x \ge 0$ .

Formalization targets

Write $\alpha = 1 - 3\theta/2$ .

Goal: Lemma 1 (p. 14)

Let

K = \max\Bigl\{i : c_i \le \frac{c_1 + \dots + c_i}{i - \alpha}\Bigr\},\qquad Q^* = \Bigl[\frac{2\gamma}{b}\,\frac{K - \alpha}{c_1 + \dots + c_K}\Bigr]^{\frac{2}{2-3\theta}}\Bigl(\frac{A-bw}{3}\Bigr)^{\frac{3}{2-3\theta}},

Q^*_i = \Bigl[1 - c_i\,\frac{K-\alpha}{c_1 + \dots + c_K}\Bigr]\frac{2Q^*}{2-3\theta}\ (i \le K), \qquad Q^*_i = 0\ (i > K).

Then $1 \le K \le I$ . The retailer's unique optimal price is $P^*(Q) = \frac{2A+bw}{3b}Q^\theta$ . A profile is a Nash equilibrium if and only if it equals $(Q^*_1,\dots,Q^*_I)$ . Moreover, $\sum_i Q^*_i = Q^*$ , every $Q^*_i \ge 0$ , and the producers with positive output are exactly those $i \le K$ with $c_i < (c_1+\dots+c_K)/(K-\alpha)$ . When $K = 1$ , $Q^*_1 = (3\gamma\theta/(bc_1))^{2/(2-3\theta)}((A-bw)/3)^{3/(2-3\theta)}$ . When $I \ge 2$ , $K = 1$ holds exactly when $c_2 > 2c_1/(3\theta)$ .

Milestones

(3b)–(3e): the retailer's unique optimal price, demand, profit, and $S(Q) = \frac{2}{b}\bigl(\frac{A-bw}{3}Q^\theta\bigr)^{3/2}$ .
(4a)–(4c): a positive output is a best response if and only if it solves the first-order condition (4c).
(4e): (4c) yields a nonnegative output if and only if $c_i \le \gamma S(Q)/Q$ .
§3.3: in equilibrium, a producer is active if and only if $c_i < \gamma S(Q)/Q$ .
Proof step (i): the active producers form an initial segment of the cost order.
(5a)–(5c): summing (4c) over the first $k$ producers pins down the aggregate output in closed form.
Downward closedness: if $k \ge 2$ satisfies the condition of (2a), so does $k - 1$ , and $k = 1$ always does.
(6): at the aggregate (5c), the participation bound of the $k$ -th producer is condition (2a).
(2b): (2c) is (5c) at $k = K$ , and (4c) evaluated at $Q^*$ gives $Q^*_i$ .

Significance

Lemma 1 is the basis of the paper's comparative statics. Its formulas show that output falls with a producer's own cost and rises with the revenue share. They also show that the number of active producers is set by a single threshold condition rather than by an iterative entry process. Under proportional sharing, several producers with different costs can all remain active, and the condition $c_2 \le 2c_1/(3\theta)$ for at least two active producers is the paper's headline insight about variety.

The paper establishes the closed form by summing first-order conditions. It does not argue that the stationary points are maximizers, that no inactive producer gains by entering, or that the equilibrium is unique. A machine-checked proof of the full characterization, uniqueness included, makes the model a verified base for the paper's later propositions and for variants with other demand curves or sharing rules. No formalization of this model was found on the platform.

Difficulty

The first-order conditions give each active producer's output as a function of the aggregate $Q$ , and summing them over a guessed active set gives $Q$ . The obvious argument stops there. Turning that computation into an equilibrium characterization requires several further facts.

Each producer's profit, viewed as a function of its own output, must be shown concave, so that (4c) describes the best response exactly.
The all-zero profile must be ruled out separately, because there the revenue share is $0/0$ .
The active set of an arbitrary equilibrium must be shown to be an initial segment of the cost order.
The count $m$ of active producers in an arbitrary equilibrium must be matched with the $K$ of (2a). This step is delicate under ties: when $c_{m+1} = (c_1 + \dots + c_m)/(m - \alpha)$ , index $m+1$ also satisfies the weak condition (2a), so $K$ exceeds $m$ . Producer $m+1$ then has output $0$ by (2b), and the two descriptions must be shown to give the same profile.

Finally, $S$ is defined as a supremum over prices, so the closed form (3e) itself requires solving the retailer's problem, including prices above the choke price.

Formalization scope

Producers are Fin I with 0 < I, so Lean's producer i is the paper's producer $i+1$ . The paper's distribution-cost coefficient $c$ is named w, and every $A - bc$ of the paper is A - b * w. Costs are ordered by Monotone c and are positive. The standing hypotheses are $b > 0$ , $A - bw > 0$ , $0 < \theta < 2/3$ and $0 < \gamma < 1$ . The paper uses $c_i > 0$ , $b > 0$ and $A - bw > 0$ implicitly; they are needed for the formulas to be finite and well-defined. All powers are real powers. Demand uses Real.sqrt, which returns $0$ above the choke price. Outputs are arbitrary nonnegative reals with no upper bound. The Nash equilibrium is the published predicate CachonCoord.Proportional.IsNash (nonnegative real strategies, unilateral deviations) applied to the producers' payoffs. Because the retailer's optimal surplus is folded into $S$ , this is the subgame-perfect reading of the paper's backward solution. The share $Q_i/Q$ at $Q = 0$ evaluates to $0$ in Lean; the all-zero profile is still not an equilibrium.

Two readings of the page are fixed explicitly. "The equilibrium" means the unique Nash equilibrium. "The set of producers $1\dots K$ with positive output" is stated exactly, because with the weak inequality of (2a), a producer whose cost ties the threshold has output $0$ . Three slips of the page are corrected rather than copied. The page calls $\bar c_{(K)} = \sum_i c_i$ "the average"; the formalization uses the average $(c_1+\dots+c_K)/K$ . The share formula printed in the proof is wrong and is not formalized. The proof's " $LHS(i-1) < LHS(i)$ " holds only weakly under ties.

The producers' payoff uses the surplus at the retailer's optimal price for the realized bundle size, a supremum over prices. It is not the closed form (3e), so none of the closed forms holds by definition. $K$ , $Q^*$ , $Q^*_i$ and $P^*$ are fixed by the page's formulas and are not quantified as arbitrary objects satisfying (6).

Everything needed beyond Mathlib is in one definitions file in CoProdBundle.Equil. Contributions are welcome on every milestone. The retailer's square-root pricing problem (milestone 1) and the concavity of the proportional-share payoff behind milestone 2 can be reused in other aggregative games with proportional revenue sharing.

Selected references

H. K. Bhargava, Bundling for Flexibility and Variety: An Economic Model for Multiproducer Value Aggregation, Management Science, 2021 (author's accepted manuscript, 2020). doi:10.1287/mnsc.2020.3662
Y. Bakos, E. Brynjolfsson, Bundling and Competition on the Internet, Marketing Science 19(1), 2000. doi:10.1287/mksc.19.1.63.15182
G. P. Cachon, Supply Chain Coordination with Contracts, Handbooks in Operations Research and Management Science 11, 2003. doi:10.1016/S0927-0507(03)11006-7

12 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Risk, Ambiguity, and the Value of Diversification: Increasing or Constant Absolute Ambiguity Aversion Lowers the Smooth-Model Value of Diversification Below Its Ambiguity-Neutral LevelResearch Paper

Motivation

Diversification is the oldest prescription of decision theory. Bernoulli (1738) used the example of a merchant, Sempronius, who can send his goods on one ship or split them over two ships, and showed that an expected-utility maximizer with concave utility prefers to split. Portfolio choice, insurance and supply-chain sourcing all rest on the same principle: when the risk of loss is known, spreading exposure helps a risk-averse decision maker.

Most real diversification decisions are made without knowing the probability of loss. A common intuition in the ambiguity literature holds that ambiguity aversion, a dislike of not knowing the probabilities, should add a second motive to diversify on top of risk aversion. Epstein (2010) and Klibanoff, Marinacci and Mukerji (2012) debated whether the smooth ambiguity model of Klibanoff, Marinacci and Mukerji (2005) captures a preference for diversification at all.

Berger and Eeckhoudt (iRisk Working Paper 2021-iRisk-02; Management Science 67(3), 2021, doi:10.1287/mnsc.2020.3823) return to Bernoulli's two-ship problem with two experts who disagree about the probability that a ship perishes. They show that ambiguity can lower the value of diversification: under ambiguity neutrality it is below the value for the corresponding known risk (their Proposition 2), and in the smooth model, under constant or increasing absolute ambiguity aversion, it is below the ambiguity-neutral value (their Proposition 4.1). This mission formalizes the second result.

Setting

A decision maker has sure wealth $W_0\in\mathbb R$ and ships cargo of value $L>0$ . A ship perishes with probability $p$ . Her utility is $u:\mathbb R\to\mathbb R$ . Shipping everything on one ship, or splitting the cargo over two ships that perish independently, gives the expected utilities

EU^{ND}=p\,u(W_0-L)+(1-p)\,u(W_0),\qquad EU^{D}=p^2u(W_0-L)+2p(1-p)\,u\!\left(W_0-\tfrac L2\right)+(1-p)^2u(W_0).

The value of diversification under risk is $VD_{risk}=EU^D-EU^{ND}$ .

Under ambiguity, two experts $\theta\in\{1,2\}$ give probabilities $p_1,p_2\in[0,1]$ . The decision maker holds the prior $\mu(1)=\mu$ , $\mu(2)=1-\mu$ with $\mu\in[0,1]$ . Write $\Delta(\theta)=EU^D(p_\theta)-EU^{ND}(p_\theta)$ for the value of diversification according to expert $\theta$ . The ambiguity-neutral decision maker averages the experts' expected utilities, so that

VD_{AN}=\big[\mu EU^D(p_1)+(1-\mu)EU^D(p_2)\big]-\big[\mu EU^{ND}(p_1)+(1-\mu)EU^{ND}(p_2)\big].

The smooth ambiguity model aggregates them through an ambiguity function $\phi$ and takes the certainty equivalent:

EU^{j}_{smt}=\phi^{-1}\big(\mu\,\phi(EU^{j}(p_1))+(1-\mu)\,\phi(EU^{j}(p_2))\big),\qquad VD_{smt}=EU^D_{smt}-EU^{ND}_{smt}.

A concave $\phi$ expresses ambiguity aversion. A linear $\phi$ gives back $VD_{AN}$ . The coefficient of absolute ambiguity aversion is $\lambda(x)=-\phi''(x)/\phi'(x)$ . The decision maker exhibits DAAA, CAAA or IAAA (decreasing, constant or increasing absolute ambiguity aversion) when $\lambda$ is strictly decreasing, constant or strictly increasing.

Formalization targets

Goal: Proposition 4.1

Let $u$ be nondecreasing and concave, and let $\phi$ be $C^2$ , concave, with $\phi'>0$ . Suppose that (i) IAAA holds and $p_1=1-p_2$ , or (ii) CAAA or IAAA holds and $p_1,p_2\ge\tfrac12$ . Then

VD_{smt}\le VD_{AN}.

Milestones

The closed form $VD_{risk}=p(1-p)\big[2u(W_0-\tfrac L2)-u(W_0-L)-u(W_0)\big]$ , (A.1).
Proposition 1: for continuous $u$ , $VD_{risk}\ge0$ for all $W_0$ , $L>0$ , $p\in[0,1]$ if and only if $u$ is concave.
The closed form $VD_{AN}=\big[\mu p_1(1-p_1)+(1-\mu)p_2(1-p_2)\big]\big[2u(W_0-\tfrac L2)-u(W_0-L)-u(W_0)\big]$ , (A.2).
Lemma 1, for a two-point lottery: under DAAA, CAAA or IAAA, shifting both expert utilities by $z>0$ moves the certainty equivalent by more than, exactly, or less than $z$ .
If $p_1=1-p_2$ then $\Delta(1)=\Delta(2)$ .
If $\tfrac12\le p_2\le p_1\le1$ and $u$ is concave then $\Delta(1)\le\Delta(2)$ , strictly under strict concavity, $p_1>p_2$ and $L>0$ .
For concave $\phi$ , $x_1\le x_2$ and $d\ge0$ : $\phi^{-1}(\mu\phi(x_1)+(1-\mu)\phi(x_2+d))\le\phi^{-1}(\mu\phi(x_1)+(1-\mu)\phi(x_2))+(1-\mu)d$ .

Significance

Proposition 4.1 shows that the smooth model does not automatically turn ambiguity aversion into a stronger taste for diversification. Under CAAA, the exponential case $\phi(x)=-e^{-\lambda x}$ used throughout applied work, together with experts who both consider a loss at least as likely as not, the smooth value of diversification never exceeds the ambiguity-neutral one. Together with Proposition 2 this says that, in Bernoulli's own example, ambiguity weakly lowers the incentive to diversify. Applied models that use the smooth criterion to explain hedging or portfolio spreading by ambiguity aversion rely on the opposite comparison. The result marks the conditions on $\lambda$ and on the experts' beliefs under which that comparison fails.

The paper's proofs are short, but they compress several steps. Lemma 1 is Pratt's (1964) characterization of decreasing, constant and increasing absolute aversion through certainty equivalents, cited without proof. Case (ii) relies on the sentence "it is easy to show that, under the concavity of $\phi$ , inequality (A.8) is satisfied if $\Delta(2)>\Delta(1)$ ", and (A.6)–(A.8) are stated through an expectation over a random $\tilde\Delta$ whose law is never specified. A formal proof fixes the exact hypotheses: risk aversion and monotonicity of $u$ , the regularity of $\phi$ , and the weak form of the conclusion. The mission also yields a reusable Lean statement of Pratt's comparative-statics lemma for two-point lotteries. As far as is known, none of these results has a machine-checked proof.

Difficulty

The algebra (milestones 1, 3, 5, 6) is routine. Lemma 1 is not: its hypothesis is a pointwise condition on $\lambda=-\phi''/\phi'$ , a local quantity, while its conclusion compares certainty equivalents, which are global quantities involving $\phi^{-1}$ . Mathlib has no theory of absolute risk aversion or of Pratt's comparison for this to rest on.

The natural first attempt at the goal applies Lemma 1 directly, but this only works when every expert's utility rises by the same amount, which is case (i). In case (ii) the shifts $\Delta(1)\neq\Delta(2)$ differ, and comparing $VD_{smt}$ with the weighted average $\mu\Delta(1)+(1-\mu)\Delta(2)$ requires knowing which expert gains more. It also requires that this expert is the one with the higher no-diversification utility, and that is where $p_\theta\ge\tfrac12$ and the monotonicity of $u$ enter.

Formalization scope

All quantities are real. The utility $u$ and the ambiguity function $\phi$ are functions $\mathbb R\to\mathbb R$ , so outcomes $W_0-L<0$ are allowed and logarithmic utility is outside the model. The two experts are two real parameters $p_1,p_2$ with prior weights $\mu,1-\mu$ , exactly as the proofs write them. $\phi^{-1}$ is Function.invFun φ. Every argument it receives is a $\mu$ -mixture of two values of a continuous, strictly increasing $\phi$ , so it lies in the range of $\phi$ and the inverse is the true one.

The following hypotheses are added to the page and disclosed in each item:

$u$ nondecreasing and concave in the goal;
$u$ continuous in Proposition 1;
$\phi$ of class $C^2$ with $\phi'>0$ ;
$L>0$ ;
nondegeneracy ( $x_1\neq x_2$ , $0<\mu<1$ ) for the strict cases of Lemma 1.

IAAA, CAAA and DAAA are monotonicity of $\lambda$ , not a sign condition on $\lambda'$ . "Decreases the value of diversification" is the weak inequality $VD_{smt}\le VD_{AN}$ , the comparison (A.4) of the proof. The strict inequality is false at $p_1=p_2$ , at $\mu\in\{0,1\}$ , or for linear $u$ .

The values of diversification are defined as differences of expected utilities. The closed forms (A.1), (A.2) are milestones, so they cannot become definitions under which those milestones hold by rfl. IAAA is defined through $\lambda$ , never through certainty equivalents, which is the conclusion of Lemma 1. Milestone 7 is a repaired two-expert reading of the (A.8) step, not (A.8) as printed.

Not formalized: Proposition 2, the $\alpha$ -maxmin results (Propositions 3.1, 3.2), Proposition 4.2, the converse of Lemma 1 and its version for general random variables, and the numerical examples.

Welcome contributions: proofs of the milestones, a general Pratt comparison theorem for certainty equivalents in Lean, and the omitted companion results.

Selected references

L. Berger, L. Eeckhoudt, Risk, ambiguity, and the value of diversification, Management Science 67(3), 2021; iRisk Working Paper 2021-iRisk-02, IÉSEG School of Management, 2021. https://doi.org/10.1287/mnsc.2020.3823
D. Bernoulli, Specimen theoriae novae de mensura sortis, 1738; English translation Exposition of a new theory on the measurement of risk, Econometrica 22(1), 1954. https://doi.org/10.2307/1909829
P. Klibanoff, M. Marinacci, S. Mukerji, A smooth model of decision making under ambiguity, Econometrica 73(6), 2005. https://doi.org/10.1111/j.1468-0262.2005.00640.x
L. G. Epstein, A paradox for the "smooth ambiguity" model of preference, Econometrica 78(6), 2010. https://doi.org/10.3982/ECTA8689
P. Klibanoff, M. Marinacci, S. Mukerji, On the smooth ambiguity model: a reply, Econometrica 80(3), 2012. https://doi.org/10.3982/ECTA9775
J. W. Pratt, Risk aversion in the small and in the large, Econometrica 32(1/2), 1964. https://doi.org/10.2307/1913738

9 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Service Design for a Holistic Customer Experience: A Process Framework: Step Types and the Inverse Correlation Matrix Decide Whether Optimal Step Efforts Are Complementary or SubstitutableResearch Paper

Motivation

A medical visit, a hotel stay or a bank onboarding is not one transaction but a service process: a sequence of steps (check-in, waiting, examination, payment), each delivered by the provider and each experienced by the customer. Practitioners design such processes with descriptive tools such as customer-journey maps and service blueprints, which list the steps and their touchpoints but do not say how much effort each step deserves. Two features make this allocation non-obvious. First, customers judge the experience as a whole, and the experiences at different steps are correlated: a long wait colours the examination that follows. Second, effort changes not only the average quality of a step but also its variability, and the direction depends on the step: at a routine step (check-in) more effort makes the outcome more predictable, while at a non-routine step (a diagnostic procedure) it may make it less so.

Bellos and Kavadias (Management Science, 2020) give a model in which the optimal effort per step has a closed form, and characterise when the efforts at two steps move together (are complementary) or in opposite directions (are substitutable) in response to a change in one step's characteristics. The answer depends on the two step types and on one entry of the inverse of the correlation matrix, not on the correlation itself. This mission formalizes that characterisation.

Setting

There are $n$ steps $i \in \mathcal J = \{1,\dots,n\}$ . The provider chooses an effort $\delta_i \in [0,1]$ at every step and one price $\pi$ .

Functional value. Step $i$ delivers $V_i = \delta_i V^H_i + (1-\delta_i)V^L_i$ with $V^H_i > V^L_i \ge 0$ . Steps reinforce each other through technical couplings $\beta_{j,i} \in [0,1)$ ( $j \ne i$ ), $\beta_{i,i} = 1$ , $\sum_{i\ne j}\beta_{j,i} < 1$ , and the functional value at step $i$ is $\mathcal V_i = \sum_j \beta_{j,i}V_j$ .
Variability. The experiential value at step $i$ has standard deviation $\sigma_i = \delta_i\sigma^H_i + (1-\delta_i)\sigma^L_i$ with $\sigma^H_i, \sigma^L_i \ge 0$ . The step is routine if $\sigma^H_i < \sigma^L_i$ and non-routine if $\sigma^H_i > \sigma^L_i$ .
Correlation. The experiences at steps $i$ and $j$ have correlation $\rho_{i,j} \in (-1,1)$ , collected in a symmetric positive definite correlation matrix $\mathbf P$ with unit diagonal.
Utility. Customers with risk aversion $r > 0$ obtain the mean-variance net utility

\mathcal U(\delta,\pi) = \sum_{i=1}^n \mathcal V_i - \frac r2\Big(\sum_{i=1}^n\sigma_i^2 + 2\sum\sum_{i<j}\rho_{i,j}\sigma_i\sigma_j\Big) - \pi.

Design problem. With unit costs $c_i \in (\sum_{j\ne i}\beta_{j,i}, 1)$ and a reservation profit $\pi_0 \ge 0$ , the provider maximizes $\mathcal U(\delta,\pi)$ subject to $\pi - \sum_i V_ic_i \ge \pi_0$ and $0 \le \delta_i \le 1$ . An optimal effort $\delta^*$ is the effort of an optimal design.

The paper's analysis assumes that each $V^H_i - V^L_i$ lies in an explicit interval $(\underline{\Delta V}_i, \overline{\Delta V}_i)$ built from the other parameters, the cofactors of $\mathbf P$ and $|\mathbf P|$ (the interior condition), and for its comparative statics it sets the technical couplings between distinct steps to zero.

Formalization targets

Goal: Proposition 3

Fix a step $i$ . Under the interior condition and without technical coupling, the effort at step $i$ satisfies

\frac{\partial\delta^*_i}{\partial c_i} < 0,\qquad \frac{\partial\delta^*_i}{\partial V^H_i} > 0,\qquad \operatorname{sgn}\frac{\partial\delta^*_i}{\partial\sigma^H_i} = -\operatorname{sgn}(\sigma^H_i - \sigma^L_i),

and for every $j \ne i$ the effort at step $j$ responds to $c_i$ , $V^H_i$ and $\sigma^H_i$ in the same directions if and only if

\Big(\operatorname{sgn}[\sigma^H_i-\sigma^L_i] = \operatorname{sgn}[\sigma^H_j-\sigma^L_j] \text{ and } [\mathbf P^{-1}]_{i,j} > 0\Big) \text{ or } \Big(\operatorname{sgn}[\sigma^H_i-\sigma^L_i] \ne \operatorname{sgn}[\sigma^H_j-\sigma^L_j] \text{ and } [\mathbf P^{-1}]_{i,j} < 0\Big),

and in the opposite directions otherwise (when $[\mathbf P^{-1}]_{i,j} \ne 0$ ). The derivatives are of the optimizer of the design problem, in one parameter at a time.

Milestones

For a given effort the optimal price is $\tilde\pi(\delta) = \pi_0 + \sum_i V_ic_i$ , so the problem reduces to maximizing $\tilde{\mathcal U}(\delta) = \mathcal U(\delta,\tilde\pi(\delta))$ over $[0,1]^n$ .
The Hessian of $\tilde{\mathcal U}$ has entries $-r(\sigma^H_i-\sigma^L_i)(\sigma^H_j-\sigma^L_j)\rho_{i,j}$ and leading minors $|\boldsymbol H_k| = (-1)^kr^k\prod_{j\le k}(\sigma^H_j-\sigma^L_j)^2|\mathbf P[1:k;1:k]|$ ; $\tilde{\mathcal U}$ is strictly concave.
The gradient of $\tilde{\mathcal U}$ , and the unique solution $\hat\delta$ of the first-order conditions.
The slope $\partial\hat\delta_i/\partial(V^H_i-V^L_i) > 0$ and the thresholds: $\hat\delta_i \le 0$ iff $V^H_i - V^L_i \le \underline{\Delta V}_i$ , $\hat\delta_i \ge 1$ iff $V^H_i - V^L_i \ge \overline{\Delta V}_i$ .
Proposition 1: under the interior condition the optimal effort is unique and equals

\delta^*_i = \hat\delta_i = \sum_{j=1}^n\frac{\big(1-(c_j-\sum_{m\ne j}\beta_{j,m})\big)(V^H_j-V^L_j)}{r(\sigma^H_i-\sigma^L_i)(\sigma^H_j-\sigma^L_j)}[\mathbf P^{-1}]_{i,j} - \frac{\sigma^L_i}{\sigma^H_i-\sigma^L_i}.

The explicit partial derivatives of $\delta^*$ in $c_j$ , $V^H_j$ , $\sigma^H_j$ , own-step and cross-step, and the own-step half of Proposition 3.

Significance

The result. Proposition 3 says that a change at one step propagates to every other step through the inverse correlation matrix. An entry $[\mathbf P^{-1}]_{i,j}$ is, up to a negative factor, the partial correlation of steps $i$ and $j$ given all other steps. So two steps whose experiences are positively correlated can still have substitutable efforts once the rest of the process is accounted for, and two uncorrelated steps can have coupled efforts. Pairing a routine with a non-routine step reverses the direction. The paper's later results, on antedependent and autoregressive correlation structures and on the first versus the last step, use this characterisation as their starting point.

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. Formalizing it means: a verified closed form for the maximizer of a box-constrained concave quadratic with a correlation-matrix Hessian; the identification of the optimizer with that closed form near the base point, so that the optimizer is differentiable there; and the sign analysis. Along the way the formalization corrects two printed slips: the auxiliary quantities $A$ and $B$ in the proof of Proposition 3 (as printed, the displayed identity for $\delta^*_i$ fails), and the printed "Otherwise", which is false when $[\mathbf P^{-1}]_{i,j} = 0$ .

Difficulty

The sign algebra at the end is short. The work lies in the step before it: Proposition 3 differentiates the optimizer of a constrained problem, not a formula. To differentiate it one has to show that under the interior condition the optimizer exists, is unique, and coincides with $\hat\delta$ on a neighbourhood of the parameters in each direction of perturbation. This needs strict concavity from positive definiteness of $\mathbf P$ , the identification of the interior condition (stated through cofactors of $\mathbf P$ ) with $\hat\delta \in (0,1)^n$ , and the openness of that condition in the parameters. Differentiating $\hat\delta$ directly and reading off signs proves a statement about the closed form, not Proposition 3.

Formalization scope

Steps are Fin n, 0-based. All quantities are real. The utility $\mathcal U$ is defined by its mean-variance expression; no random variables appear. $\mathbf P$ is assumed symmetric, positive definite, with unit diagonal and off-diagonal entries in $(-1,1)$ . The cofactor $(-1)^{i+j}|\mathbf P[-j;-i]|$ is Matrix.adjugate P i j. Two hypotheses are added to the page and disclosed: $r > 0$ (the model allows $r \ge 0$ , but Proposition 1 divides by $r$ ) and $\sigma^H_i \ne \sigma^L_i$ (every step is routine or non-routine). Proposition 3 assumes $\beta_{j,i} = 0$ for $j \ne i$ , the paper's own simplification for §4. A partial derivative is Lean's deriv of the optimal effort along one parameter, the others fixed ( $V^L_i$ fixed when $V^H_i$ moves, $\sigma^L_i$ fixed when $\sigma^H_i$ moves). The optimal effort is a choice of maximizer of the §3.3 problem, with junk value $0$ when none exists.

Stating Proposition 3 for the closed form $\hat\delta$ instead of the optimizer of the design problem would trivialize it, and that formalization is ruled out. Likewise the interior condition is the page's interval on $V^H_i - V^L_i$ , not the assumption $\hat\delta \in (0,1)^n$ .

The development needs Mathlib's positive definite matrices, adjugates and determinants, strict concavity, and one-variable derivatives. Reusable by-products: strict concavity and the unique maximizer of a concave quadratic with Hessian $-rD\mathbf PD$ ; positivity of principal cofactors of a positive definite matrix. Contributions are welcome on any milestone, and alternative proofs of Proposition 1 by convex duality or KKT are welcome too.

Selected references

I. Bellos and S. Kavadias, Service design for a holistic customer experience: a process framework, Management Science, 2020 (authors' manuscript). https://doi.org/10.1287/mnsc.2020.3609
U. Karmarkar and R. Pitbladdo, Quality, class, and competition, Management Science 43(1), 27–39, 1997. https://doi.org/10.1287/mnsc.43.1.27
A. Raveh, On the use of the inverse of the correlation matrix in multivariate data analysis, The American Statistician 39(1), 39–42, 1985. https://doi.org/10.2307/2683904

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Bitcoin: A Natural Oligopoly: Under Economies of Scale Every Participating Miner's Equilibrium Market Share Is at Least 1 − (1/α)(c_i/c_j)Research Paper

Why mining shares matter

Proof-of-work mining allocates a fixed reward among miners whose investments determine their chances of receiving it. The resulting distribution of mining power matters for decentralization: if a few miners control most of the investment, the economic mechanism does not support a diffuse set of participants. Arnosti and Weinberg study this question in a contest model where miners have different unit costs and rewards may rise more than proportionally with investment. Their proportional model has an explicit equilibrium; the economies-of-scale model asks what can still be said about market shares when that explicit characterization is unavailable.

The authors' result is a bound for each miner who invests, measured against the cost of any other miner who invests. It applies even when unit costs are asymmetric. The claim is conditional on a pure equilibrium: for sufficiently strong economies of scale, such an equilibrium need not exist, as the paper observes. The mission concerns the quantitative restriction on every equilibrium that does exist, not an assertion that all parameter choices have one.

Contest and equilibrium

There are $n\ge2$ miners and a prize worth one. Miner $i$ chooses a nonnegative investment $q_i$ and pays $c_iq_i$ , where the unit cost $c_i$ is strictly positive. A parameter $\alpha\ge1$ determines how investment affects rewards. At an investment profile $q=(q_1,\ldots,q_n)$ , the market share of miner $i$ is

x_i(q)=\frac{q_i^\alpha}{\sum_{j=1}^n q_j^\alpha}

when some miner invests. When every investment is zero, the model assigns every miner share zero. The utility of miner $i$ is $U_i(q)=x_i(q)-c_iq_i$ . The prize value is fixed at one throughout; there is no extra reward parameter.

A pure Nash equilibrium is a nonnegative profile $q$ at which no miner can increase its own utility by replacing $q_i$ with another nonnegative investment while all other investments remain fixed. This global comparison matters because, with economies of scale, a local first-order condition alone does not characterize a best response. The paper's phrase “equilibrium in the EoS model” has this pure-strategy meaning. A miner participates when $q_i>0$ ; at the equilibrium profiles of interest this is equivalent to having positive market share.

The paper states the cost vector in increasing order without loss of generality in its earlier proportional-model section. The share bound is invariant under relabelling, so its formal statement permits any assignment of positive costs to the $n$ miners. No pair of miners has to be distinct.

Formalization targets

The goal is Theorem 2 of the arXiv preprint. For every pure equilibrium $q$ and every pair of participants $i,j$ , including $i=j$ , it states

x_i(q)\ge 1-\frac1\alpha\frac{c_i}{c_j}.

The bound depends on both the scale exponent and the relative costs. Setting $i=j$ gives the symmetric threshold $1-1/\alpha$ for each participant. The target therefore retains the exact cost ratio and the paper's quantifier over all participating pairs. It does not require a selected or unique equilibrium.

The milestone list follows the authors' named results and one explicit analytic statement in their proof. Lemma 3 gives the equilibrium identity $c_iq_i=\alpha x_i(q)(1-x_i(q))$ and a separate inequality that still applies to a nonparticipant. Corollary 4 gives $x_i(q)\ge1-1/\alpha$ when $x_i(q)>0$ . In the proof of Proposition 1, the function $f_\alpha(x)=x^{1-1/\alpha}(1-x)$ is decreasing on the open interval $(1-1/\alpha,1)$ ; the milestone states strict decrease, matching the negative derivative shown there. Proposition 1 then says that if $q_i\ge q_j>0$ , then $c_i\le c_j$ , with equality exactly when $q_i=q_j$ . These are the source's results that support Theorem 2, rather than substitutes with weaker conclusions.

What the bound gives

The theorem turns a claim about scale effects into a checkable limit on equilibrium concentration. When costs are equal, every participant has share at least $1-1/\alpha$ . Thus, as the paper notes, sufficiently strong scale effects limit the number of participants in any pure equilibrium. With unequal costs, the same result gives a pairwise share guarantee that accounts for each miner's cost relative to another participant's. A bound only in terms of $\alpha$ would lose that comparison.

The mathematical result is proved in the cited paper. This mission asks for machine-checked Lean proofs of the statement and its source milestones. The definitions and theorem statements here are local drafts; compilation of a statement confirms that Lean can parse it, not that a proof exists. The reusable global pure Nash predicate is imported from an existing formalization. The paper-specific layer consists of the contest success function, utility, equilibrium specialization, and share-shape function. Together they make it possible to compare formal proofs of the same economic claim without silently changing the game.

Main difficulty

For $\alpha>1$ , the utility from a unilateral investment change can have a shape that is not captured by a single local optimum test. An argument based solely on setting a derivative to zero can miss a better distant deviation or the boundary action $q_i=0$ . The first-order relations of Lemma 3 are consequences of global equilibrium, not its definition. The main share bound also compares two miners at once: knowing only a participant's own first-order identity gives an expression involving its own share and investment, while Theorem 2 asks for an exact ratio of two different costs. Proposition 1 supplies the ordering information needed by the authors' argument. At $\alpha=1$ , the model meets the proportional case, so formulas involving $q_i^{\alpha-1}$ must still make sense at zero investment.

Formalization scope

Lean indexes miners by Fin n; its zero-based labels correspond to the paper's miners $1,\ldots,n$ without changing any statement. The model uses real-valued investments and costs, with the strategy constraint $q_i\ge0$ , and real exponentiation for $q_i^\alpha$ . Standing assumptions are $n\ge2$ , $\alpha\ge1$ , and $c_i>0$ for every miner. The model explicitly assigns zero share at the all-zero profile, rather than relying on a convention for division by zero. The imported feasible-strategy Nash predicate is specialized to the set of nonnegative real numbers and therefore quantifies over every nonnegative unilateral deviation. No theorem adds positivity of the aggregate investment as a premise: that property must follow from equilibrium where it is needed.

These choices rule out a trivializing formalization in which equilibrium is defined by Lemma 3's first-order equations or the goal is weakened to the equal-cost case. The exact exponent, the unit prize, and the ratio $c_i/c_j$ are part of the target. The real-power convention gives $0^0=1$ at $\alpha=1$ in Lemma 3's inequality; the theorem's denominator is positive at equilibrium. Formal proofs will need finite-sum and real-power facts, unilateral-deviation reasoning, real analysis for the shape function, and inequalities linking investment, share, and costs. Proofs of the four milestones, alternative proofs of the goal, and reusable game-theoretic lemmas are within scope. The paper's separate proportional-equilibrium characterization and countably infinite-miner model are outside this mission.

Selected references

Nick Arnosti and S. Matthew Weinberg, Bitcoin: A Natural Oligopoly, arXiv:1811.08572v1, 2018; later published in Management Science, 2022. Pinned preprint.

7 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Capacity Expansions with Bundled Supplies of Attributes: An Application to Server Procurement in Cloud Computing: A Unique Fixed-Cost Threshold Decides Simultaneous Versus Sequential ReplenishmentResearch Paper

Motivation

A cloud provider buys servers in preset configurations, while its demand for processing and memory grows at different rates. Each server configuration supplies both resources, so adding capacity for one resource also changes the unused capacity of the other. Purchases incur a charge for the servers, a charge for making an expansion, and an ongoing cost for unused capacity. The choice between buying configurations together and staggering their purchases is therefore a cost decision even when demand is known. Arbabian, Chen, and Moinzadeh study this decision for two resources and two server configurations over a finite planning horizon. Their Proposition 1 identifies a threshold in the fixed cost of a joint expansion.

The result was stated in the authors' April 14, 2019 manuscript and published in Manufacturing & Service Operations Management in 2020. This mission uses the manuscript's theorem numbers and pages. The result is a known mathematical claim; the remaining work is to give its definitions and proof in Lean, with the source's policy classes and cost accounting represented explicitly.

Setting

There are two capacity attributes, indexed by $i\in\{1,2\}$ , and two cluster types, indexed by $j\in\{1,2\}$ . A unit of cluster $j$ supplies $a_{ij}>0$ units of attribute $i$ . Demand for attribute $i$ increases at a nonnegative rate $d_i(t)$ over $[0,T]$ , and $D_i(s,t)=\int_s^t d_i(u)\,du$ is its growth between $s$ and $t$ . The provider starts with both attributes at their minimum desired excess capacity, normalized to zero. It must meet demand at every time and return both excess capacities to zero at the end of the horizon. Replenishment takes effect immediately. These are the base-model conventions in §3 of the manuscript.

A capacity expansion cycle begins and ends when both attributes are leveled. In a sequential cycle, one cluster type leads: it is bought one or more times, followed by one purchase of the other type. Each expansion costs $A>0$ . In a simultaneous cycle, both types are bought at each expansion, whose fixed cost is $\beta A$ for $\beta\in[1,2]$ . Cluster $j$ has unit purchase cost $c_j$ , and unused attribute $i$ has holding rate $h_i>0$ . If $E_i(t)$ is the excess capacity after the expansions at time $t$ , total holding cost is $\sum_i h_i\int_0^T E_i(t)\,dt$ . Total cost also includes all fixed and purchase costs. Sequential policies may have any positive number of cycles, any positive number of leading expansions within each cycle, and either leading type. For joint policies, the intervals between consecutive joint expansions form a partition of $[0,T]$ .

Formalization targets

The main target is the unique fixed-cost threshold of Proposition 1. Write $V_{\mathrm{seq}}$ for the infimum of costs of all feasible sequential policies and $V_{\mathrm{sim}}(\beta)$ for the corresponding simultaneous infimum. The threshold $\bar\beta\in(1,2)$ satisfies, for every $\beta\in[1,2]$ ,

V_{\mathrm{sim}}(\beta)\le V_{\mathrm{seq}}\iff\beta\le\bar\beta, \qquad V_{\mathrm{sim}}(\beta)<V_{\mathrm{seq}}\iff\beta<\bar\beta.

This makes equality at $\bar\beta$ explicit, in line with the paragraph following Proposition 1. The milestone list records the source's sequential and simultaneous cost identities, the fixed-time holding comparison, the split comparison from the appendix, the two endpoint inequalities, and monotonicity in $\beta$ . Equation (8), which fixes the final sequential expansion time inside a cycle, is another milestone because the authors use its uniqueness in their analysis.

Significance

The threshold gives a precise decision rule for the model: a lower relative joint expansion charge favors buying both types together; a higher charge favors staggered purchases. It compares optimized policies, whose cycle boundaries and expansion times may differ, rather than only two schedules held at the same times. The result therefore captures the interaction of the fixed charge and the time spent holding unused capacity. The paper also analyzes specialized one-cycle schedules under exponential demand; those results are separate from this mission's general comparison.

A completed Lean development would make the policy definitions, cost identities, and threshold claim machine checked. It would also provide reusable definitions for finite-horizon bundled capacity expansion, including a time-dependent excess-capacity trajectory and its integral holding cost. The manuscript supplies a mathematical proof, but this proposal's theorem files currently contain open sorry proofs. The mission invites proofs of its listed statements and the analytic facts needed to connect them, including existence of optimal schedules.

Difficulty

The straightforward comparison uses identical expansion times. That comparison identifies a holding-cost difference, but it does not compare the two optimized classes: the least-cost sequential schedule and the least-cost joint schedule may choose different times and different numbers of expansions. The paper's endpoint arguments also rely on strict inequalities for optimal costs. A strict inequality for every fixed schedule does not automatically become strict after taking an infimum. Showing that the relevant optima are attained, or supplying an equivalent uniform argument, is part of the formalization burden. The fixed expansion charge bounds how many expansions a near-optimal policy can afford, but the interval lengths remain continuous variables.

Formalization scope

Lean represents the attributes and cluster types by Fin 2, with index 0 corresponding to the paper's 1 and index 1 to its 2. The matrix entry a i j is capacity of attribute $i$ per unit of cluster $j$ . Times, demand, quantities, and costs are real. Replenishment times are strictly increasing, and a purchase at time $t$ contributes to the right-continuous excess capacity at $t$ . Policy validity requires no shortage and balance at cycle endpoints. The positive determinant $\alpha=a_{11}a_{22}-a_{12}a_{21}$ records the nondegenerate, attribute-intensive cluster configurations needed by the paper's division formulas. The optimal costs are real infima over full policy classes, with no attainment built into their definitions. Holding cost is computed from the integral of actual excess capacity; defining it by the displayed closed forms would erase the content of Lemmas 1 and 2.

The theorem assumes continuous demand rates and the strict demand-ratio guard $a_{12}d_2(t)<a_{22}d_1(t)$ and $a_{21}d_1(t)<a_{11}d_2(t)$ throughout $[0,T]$ . The manuscript states Assumption 1 only for chosen leading intervals. Its Proposition 1 needs more: without the guard, taking $a=((2,1),(1,2))$ , $A=100$ , $c_j=0$ , $h_i=1$ , $d_2=1$ , and $d_1=90$ on $[0,0.01)$ then $10/99$ permits one joint expansion at $\beta=2$ for at most 202 while every feasible sequential policy costs at least 300. Demand continuity supports the cost integrals; the strict guard makes every subinterval satisfy Assumption 1 strictly and keeps the appendix's sequential split feasible. Neither regularity nor this guard is claimed as a printed hypothesis of Proposition 1.

The appendix prints an extra $h_1$ outside the sum in its Case 2 holding-cost difference; the Lean milestone uses $\sum_i h_i(y-s)a_{i2}Q_2$ , consistent with the preceding integrals. The paper also prints $[0,1]$ in its last monotonicity sentence, while its fixed-cost parameter is defined on $[1,2]$ ; the milestone uses the model's interval. Useful contributions include formal integration identities for these finite replenishment schedules, existence and finiteness of the policy optima, and the comparison claims in the milestones.

Selected references

M. E. Arbabian, S. Chen, and K. Moinzadeh, Capacity Expansions with Bundled Supplies of Attributes: An Application to Server Procurement in Cloud Computing, Manufacturing & Service Operations Management, 2020. SSRN manuscript, April 14, 2019; published DOI.

10 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

Asset Selling Under Debt Obligations: Under a Single Debt Payment Due Before the Horizon Ends, the Optimal First Sale Follows a Control Band of Two Critical PricesResearch Paper

Selling an asset bought with debt

Firms that hold a large, divisible asset (a commodity inventory, a block of shares, a stock of natural gas) often financed it with debt and must sell it over time to repay that debt. Without debt, the timing problem is classical: Karlin (1962) showed that a non-divisible asset facing independent prices should be sold the first time the price exceeds a reservation price. Debt changes the incentives in two opposite directions. Limited liability caps the shareholders' loss at zero, which rewards gambling on high future prices and delays selling. Bankruptcy also destroys the value of the unsold asset, an indirect bankruptcy cost, which rewards selling early to secure the debt payment. Ahn, Wang and Wu (SSRN 3472345, published in Operations Research 69(4), 2021, doi:10.1287/opre.2019.1961) solve the resulting dynamic program with Markov prices. This mission formalizes their central structural result: the optimal first sale under a single debt payment due before the end of the horizon.

Setting

A seller holds an amount $x_t \in [0,1]$ of a divisible asset at the beginning of period $t = 1, \dots, T$ , with $x_1 = 1$ . The selling price $P_t$ follows a Markov process: the law of $P_{t+1}$ given $P_t = p$ is a probability kernel $\kappa_t(p)$ , with finite conditional mean. Write $E_t$ for the expectation given the current price. The discount factor is $\rho \in (0,1)$ , the per-period selling capacity is $\ell \in (0,1]$ , and unsold asset is worthless after period $T$ .

The debt-free value $U_t(x,p)$ solves, with $U_{T+1} \equiv 0$ ,

U_t(x,p) = \max_{0 \le q \le \min(x,\ell)} \; p\,q + \rho\,E_t\,U_{t+1}(x-q, P_{t+1}).

The debt-free critical price is $R^o_t = \rho\,E[U_{t+1}(1,P_{t+1}) \mid P_t]$ .

Debt. A schedule $d = (d_t)_{t \le m}$ , $d_t \ge 0$ , is due at the end of periods $t = 1, \dots, m$ , with maturity $1 \le m \le T$ . The seller's working capital $w_t$ starts at $w_1 = 0$ and grows at rate $1/\rho$ . In period $t \le m$ , a quantity $q$ is feasible if $0 \le q \le \min(x_t,\ell)$ and $w_t + p_t q \ge d_t$ . If no quantity is feasible, the seller is bankrupt and the equity value $V_t(x,w,p;d)$ is $0$ . Otherwise

V_m(x,w,p;d) = \max_{q \text{ feasible}} \; p\,q + w - d_m + \rho\,E_m\,U_{m+1}(x-q,P_{m+1}),

V_t(x,w,p;d) = \max_{q \text{ feasible}} \; \rho\,E_t\,V_{t+1}\big(x-q,\ \rho^{-1}(w + p\,q - d_t),\ P_{t+1}; d\big), \quad t < m.

For a single payment $d_m = D$ (and $d_t = 0$ otherwise), write $\delta_t = \rho^{m-t}D$ and $C_t = \rho\,E_t V_{t+1}(1,0,P_{t+1};d)$ , with $V_{m+1} := 0$ . The net effect of debt is

\Delta_t = V_t(1,0,P_t;d) - \big(U_t(1,P_t) - \rho^{m-t}D\big).

It is the value of limited liability net of the bankruptcy cost. The two critical prices are

R^{(1)}_t = \min\Big\{\frac{\delta_t R^o_t}{R^o_t - C_t},\ C_t + \delta_t\Big\}, \qquad R^{(2)}_t = \max\{R^o_t,\ C_t + \delta_t\}.

Formalization targets

Goal: Proposition 4 (p. 14)

Assume $\ell = 1$ , a single payment $D > 0$ at $m < T$ , a period $t \le m$ before any sale ( $x = 1$ , $w = 0$ ), and a price $p > 0$ . Then $R^{(1)}_t \le R^{(2)}_t$ , and:

p < R^{(1)}_t \Rightarrow \text{sell nothing } (t<m) \text{ or bankruptcy } (t=m), \qquad R^{(1)}_t \le p < R^{(2)}_t \Rightarrow q = \delta_t/p \text{ is optimal}, \qquad p \ge R^{(2)}_t \Rightarrow q = 1 \text{ is optimal}.

After the debt-securing sale, the optimal quantities coincide with the debt-free ones. Moreover:

E_t\Delta_{t+1} < 0 \Rightarrow R^{(1)}_t < R^{(2)}_t = R^o_t, \qquad E_t\Delta_{t+1} \ge 0 \Rightarrow R^{(1)}_t = R^{(2)}_t \ge R^o_t.

When $E_t\Delta_{t+1} = 0$ , all three prices coincide.

Milestones

In attack order:

Lemma 1(i)–(ii) (p. 8). Enough working capital makes $V_t = U_t + w - \sum_{i\ge t}\rho^{i-t}d_i$ . With no asset left, $V_t = (w - \sum_{i \ge t}\rho^{i-t}d_i)^+$ .
Proposition 1 (p. 9) with (A.1). The debt-free rule is to sell everything once $P_t \ge R^o_t$ ; moreover $U_t(x,p) = \max\{p, R^o_t\}x$ and $R^o_t = \rho E_t\max\{P_{t+1}, R^o_{t+1}\}$ .
(A.6). The closed form of $V_m$ .
Lemma 3 (p. 13). Convexity, linearity and continuity of $V_t$ in $(x, w, d_m)$ .
(A.8). $V_t$ is a three-term maximum.
(A.9). Its specialization at $x = 1$ , $w = 0$ .
Footnote 4. $0 \le C_t < R^o_t$ .

Significance

Proposition 4 is the paper's headline. Under debt, the first sale follows a control band. Below $R^{(1)}_t$ the seller waits. Between the two critical prices, the seller sells exactly the quantity whose revenue covers the discounted debt; in that band a higher price means a smaller sale. Above $R^{(2)}_t$ the seller sells everything. Part (ii) separates the two economic forces by the sign of one number, $E_t\Delta_{t+1}$ . When the bankruptcy cost dominates, part of the asset is sold earlier than without debt. When limited liability dominates, selling is delayed and done all at once. The same structure underlies the paper's later results on threshold debt levels and general installment schedules.

The result is proved on paper but has not been formalized; the platform has no asset-selling, reservation-price or debt-constrained selling model. The mission contributes three things. The first is a finite-horizon Markov-price dynamic program with an explicit bankruptcy branch and limited liability, built on Mathlib's probability kernels. The second is Karlin-type debt-free stopping results for a divisible asset. The third is the full convexity argument behind the control band.

Difficulty

Part (ii) is signed algebra once footnote 4 is known; the work is in part (i). Because of the bankruptcy branch, $V_t$ is neither convex nor concave in general (Lemma 1(iii)). So the first-order reasoning that settles the debt-free problem, a linear objective in $q$ , does not carry over. Two facts reduce the optimum to three candidate quantities. The first is convexity of $V_t$ in $(x, w, d_m)$ below the debt-covering region, proved by backward induction together with the debt level. The second is linearity above that region. The induction must carry the debt level as a variable.

Every value function is integrated against a kernel. Before any identity between expectations can be used, $p' \mapsto U_{t+1}(x,p')$ and $p' \mapsto V_{t+1}(x,w,p')$ must be shown measurable and integrable, and both are suprema over a continuum of quantities. The strict inequality of footnote 4 is a separate induction: $V_{t+1}(1,0,\cdot) < U_{t+1}(1,\cdot)$ at every positive price.

Formalization scope

Everything lives in the namespace AssetDebt.ControlBand.

Representation.

Periods are natural numbers and values are real numbers.
κ t p is the law of $P_{t+1}$ given $P_t = p$ , a Mathlib Kernel ℝ ℝ.
$U$ and $V$ are defined by well-founded recursion as suprema of the objective over the feasible set. For $V$ , the bankruptcy test comes first, so the supremum is only taken over a nonempty interval.
$V_t := 0$ for $t > m$ , which is the paper's convention $V_{m+1} := 0$ .
Feasibility is written $0 \le q \le \min(x,\ell)$ , $d_t \le w + pq$ . This avoids dividing by $p$ .
"Optimal" means feasible and attaining the maximum; uniqueness is not claimed.
The critical prices $R^{(1)}_t, R^{(2)}_t$ are the explicit thresholds (A.10) from the paper's proof, not a free existential.
$E_t\Delta_{t+1}$ is the integral of $\Delta_{t+1}$ as defined in (5).

Added hypotheses.

Prices are almost surely strictly positive. The paper writes $P_t \ge 0$ but divides by $p_t$ .
The multi-step conditional means $E[P_s \mid p_t]$ , $t < s \le T$ , are finite. The paper treats $R^o_t$ as a real number, and the one-step assumption alone does not guarantee that.
Section 3's standing assumption $\ell = 1$ is a hypothesis of every statement except Lemma 1.

Excluded trivializations. $V$ is never defined by its closed forms (A.6), (A.8) or (A.9), which would make the goal an unfolding exercise. The critical prices are not existentially quantified: a price-dependent existential could be witnessed by thresholds read off the optimal action itself.

Infrastructure. A complete development needs measurability of suprema of kernel integrals, sup-shift lemmas for bounded intervals, and the backward-induction convexity argument. The debt-free results (Proposition 1) and the sup and measurability lemmas apply to other finite-horizon selling and stopping models. Contributions are welcome on any milestone, in particular on the measurability layer.

Selected references

H.-S. Ahn, D. D. Wang, O. Q. Wu, Asset Selling Under Debt Obligations, SSRN 3472345, version of May 7, 2019. https://ssrn.com/abstract=3472345 ; published in Operations Research 69(4), 2021. https://doi.org/10.1287/opre.2019.1961
S. Karlin, Stochastic models and optimal policy for selling an asset, in K. J. Arrow, S. Karlin, H. Scarf (eds.), Studies in Applied Probability and Management Science, Stanford University Press, 1962, pp. 148–158 (cited as in the paper’s reference list).
O. Besbes, D. A. Iancu, N. Trichakis, Dynamic pricing under debt: spiraling distortions and efficiency losses, Management Science 64(10), 2018, pp. 4572–4589 (cited as in the paper's reference list).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Quality Disclosure Under Consumer Loss Aversion: In a Duopoly with Costly Disclosure, Stronger Loss Aversion Lowers the Disclosure Threshold and Raises Each Firm's Ex Ante ProfitResearch Paper

Motivation

A seller can disclose privately known product quality, but credible disclosure costs money. In a market with competing sellers, disclosure changes both what consumers believe about a silent seller and how aggressively the sellers can price. Zhang and Li study this interaction when consumers are loss averse about quality: learning that a product falls below an expected standard hurts more than learning that it exceeds the standard helps. Their duopoly result says that stronger consumer loss aversion makes firms disclose more often and raises each firm's profit before quality is known, even though disclosure itself remains costly. The model and result appear in the SSRN preprint, §§3.1–3.3 and Proposition 2.

The paper first gives a monopoly benchmark and then analyzes two firms facing the same consumers. The duopoly question is distinct because a firm's disclosure affects the gap between its own product's perceived value and its rival's. The paper's Proposition 2 is a comparative statement about the equilibrium of this disclosure game, not a claim about a distribution chosen for a numerical example. The formalization targets the general quality distribution used in the paper.

Setting

Two symmetric firms, A and B, each have one product and a privately known quality $q_a,q_b\in[0,1]$ . Their qualities are independent draws from a common cumulative distribution $F$ with a continuous, strictly positive density $f$ and $F(1)=1$ . A firm may pay a common disclosure cost $c>0$ to reveal its quality truthfully. Otherwise, consumers infer quality from nondisclosure. With a common disclosure threshold $\hat q$ , firms reveal quality above $\hat q$ and remain silent at or below it. The inferred quality of a silent firm is the conditional mean $\bar q=E[q\mid q\le\hat q]$ .

When a product's quality is disclosed, a consumer values it at $q-p$ , where $p$ is its price. When quality is hidden, the consumer experiences a gain or loss relative to $\bar q$ . With gain sensitivity $g>0$ and loss sensitivity $l>0$ , equation (1) gives utility

u=q-p+g\max\{q-\bar q,0\}-l\max\{\bar q-q,0\}.

The degree of consumer loss aversion is $k=l-g$ . The paper assumes $k>0$ and also discusses the loss neutral benchmark $k=0$ . It uses two functions of the quality distribution,

G(x)=\frac{\int_0^x F(q)\,dq}{F(x)},\qquad H(x)=\frac{\int_0^{x-G(x)}F(q)\,dq}{F(x)},\qquad 0<x\le1.

They express the belief as $\bar q=\hat q-G(\hat q)$ and the expected gross utility of a silent product as $\bar q-kH(\hat q)$ , by equation (2). After disclosure decisions, firms set prices against homogeneous consumers. Under the paper's participation condition, the Bertrand outcome awards the firm with the higher gross consumer value the difference between the two values as revenue; the lower valued firm earns zero. Disclosure cost is then subtracted from the revealing firm's revenue. A symmetric equilibrium threshold means that both firms use the same $\hat q$ and each firm's disclosure choice is a best response at every quality.

Formalization targets

Proposition 2: threshold and profit

Fix $F,f,c,g$ and compare $l_1<l_2$ at fixed $g$ , with $0\le k_1=l_1-g<k_2=l_2-g$ . For the corresponding symmetric best response thresholds $\hat q_1,\hat q_2$ , Proposition 2 asks for both strict comparisons:

\hat q_2<\hat q_1,\qquad E(\pi^d_1)<E(\pi^d_2).

Here $E(\pi^d_i)$ is either firm's ex ante profit, averaged over its own quality before the draw. The result does not prescribe a numerical disclosure threshold or profit. The preprint's Proposition 2, p. 18, states the two directional claims; its proof on p. A7 gives strict signs.

The milestones preserve the paper's intermediate statements: the nondisclosure belief and expected utility, growth of $H$ , the two disclosure profits, the equilibrium equation (6) and its unique root in Claim 3, the ex ante profit identity (7), and the derivative of the integral $L$ . In particular, the game defined above determines the threshold and profit; equations (6) and (7) are claims to establish about those objects.

Significance

The result identifies a setting in which a consumer preference that lowers the perceived value of undisclosed goods can benefit competing firms. A stronger aversion to disappointed quality expectations changes firms' disclosure decisions and, through those decisions, the price differences available in competition. Proposition 2 gives a statement about each firm's expected profit, while the paper separately discusses cases in which an individual firm's realized profit can rise or fall. These distinctions are explicit in the preprint's §3.3, pp. 15–18.

The economic result is established in the paper; this mission seeks a machine checked Lean proof of its symmetric equilibrium claim and the paper's supporting identities. The statements here compile as open targets, and no proof is asserted to have been formalized. The work also develops reusable interval integral facts for conditional means and costed disclosure games with a general continuous quality density.

Difficulty

The central difficulty is the link between the original disclosure game and the integral expressions used in the paper's comparative statics. The profit of disclosing depends on the rival's random quality and its disclosure decision. The profit of silence depends on a belief formed from the same threshold that firms choose. A formula about a root of equation (6) alone does not establish that the root is a best response threshold in this game. Likewise, the compact profit expression (7) must agree with the profit obtained by integrating the game's conditional Bertrand margins and paying disclosure cost.

The general density also matters. A calculation for the uniform distribution in the paper's numerical footnote does not cover the paper's proposition. Establishing strictness requires keeping the positive density, the monotonicity assumption on $G$ , and the consumer participation domain visible throughout the development.

Formalization scope

Lean represents $F$ and $f$ as real valued functions relevant on $[0,1]$ , together with a proposition asserting that $f$ is continuous and positive there, that $F(x)=\int_0^x f(q)\,dq$ on the interval, and that $F(1)=1$ . Every expectation against $dF(q)$ is an interval integral against $f(q)\,dq$ . The firms' independent, identical draws are encoded by using that same density separately for own and rival quality; no probability space is introduced. The standing assumption that $G$ is increasing is expressed as strict monotonicity on $(0,1]$ . The threshold lies in that interval, so division by $F(0)=0$ cannot create a boundary statement about an undefined conditional mean.

Lean's utility function is gross of price. Its pricing layer represents the paper's homogeneous consumer Bertrand outcome by $\max\{u-v,0\}$ . The symmetric equilibrium predicate requires the silent product's gross utility to be nonnegative, and the strategic payoff identities carry the same condition. This is the bound in footnote 3 of §3.3, p. 15. The comparison fixes $g$ and increases $l$ ; it includes $k_1=0$ to cover the paper's loss neutral benchmark. The model's positive $g$ and $l$ assumptions are explicit in the economic statements. The milestone for $H$ exposes positivity on the full positive interval, beyond the page's explicit $H(1)>0$ .

The symmetric equilibrium is defined by best responses in disclosure and the participation condition, with consumers using the conditional belief and firms receiving Bertrand revenue less disclosure cost. Neither the equilibrium threshold nor ex ante profit is defined by the simplified equation it is supposed to satisfy. Claim 3 gives a unique root of the threshold equation; an admissible root must also satisfy participation to represent an equilibrium. The paper's Claim 2 about the absence of asymmetric equilibria is outside this mission: Proposition 2 is framed for the symmetric equilibrium, and the printed argument for Claim 2 has an unresolved monotonicity step. Contributions to the model identities, equilibrium characterization, integral calculus, and goal proof are all within scope.

Selected references

J. Zhang and K. J. Li, Quality Disclosure under Consumer Loss Aversion, SSRN preprint 3544738, version of 2020-01-20, §§3.1–3.3 and Appendix, 2020. SSRN.
J. Zhang and K. J. Li, Quality Disclosure under Consumer Loss Aversion, Management Science 67, 2021. DOI: 10.1287/mnsc.2020.3745. The mission's page and equation citations refer to the pinned preprint above.

10 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Trade Credit Insurance: Operational Value and Contract Choice: With an Attractive Outside Option, the Cancelable Contract δ = 0, p = f = c/θ₁ + β₁r Is Optimal and Recovers the Full Value of TCIResearch Paper

Motivation

Suppliers often let buyers pay after delivery. If the buyer defaults, the supplier loses the credit sale revenue and may also face a financing cost from the resulting cash shortfall. Trade credit insurance transfers part of this loss to an insurer, but the insurer may possess information about the buyer that the supplier cannot observe. The insurer can use that information by canceling coverage before shipment. Yang, Bakshi, and Chen study how this option changes both the insurer's incentive to gather information and the supplier's decision to ship. Their Proposition 3 identifies a regime in which a simple cancelable contract recovers the entire value available to a centralized decision maker. Yang, Bakshi, and Chen (2021)

The question matters for contract design because a policy's deductible and refund affect different decisions. A deductible changes the supplier's loss if the buyer defaults. A refund changes the insurer's cost of canceling coverage. With a sufficiently attractive alternative sales channel, these terms can induce the insurer to reveal adverse credit information through cancelation while leaving the supplier fully covered when she ships. This mission states that claim precisely for the three-signal model in the authors' accepted manuscript. Accepted manuscript, §§3 and 6

Setting

A supplier receives an order for one unit at credit price $r$ . She may ship on credit or sell through an outside channel for $r_0<r$ . When the buyer defaults, the supplier receives no payment from the buyer. Her financing cost depends on end-of-period net cash flow $x$ :

L(x)=l(T-x)^+=l\max\{T-x,0\}.

Here $T$ is a cash flow threshold and $l$ is the marginal cost of falling short. At the time of contracting, the buyer's default probability is $\bar\beta$ . An insurer can pay cost $c$ to monitor the buyer and observe one of three signals $i=1,2,3$ . Signal $i$ occurs with probability $\theta_i$ and has conditional default probability $\beta_i$ , where $\beta_1<\beta_2<\beta_3$ and $\bar\beta=\sum_i\theta_i\beta_i$ . The paper assumes the outside channel is initially less attractive than the credit sale: $r_0<(1-\bar\beta)r$ . Accepted manuscript, §3 and Table 1

A cancelable contract is $\kappa=(p,\delta,f)$ . The supplier pays premium $p$ ; if she ships while covered and the buyer defaults, the insurer pays the credit price minus deductible $\delta$ . Before shipment, the insurer can instead cancel coverage and refund $f$ . After this decision, the supplier chooses whether to ship. The contract must satisfy $0\le\delta\le r$ and $0\le f\le p$ . The insurer's monitoring decision compares its expected total cost with three alternatives: keep coverage without monitoring, cancel without monitoring, and decline the contract. The supplier's payoff includes her premium, any refund, default losses, and financing costs. Accepted manuscript, §§3 and 6, and Lemma B.1

The first-best payoff is the maximum available to a financially unconstrained planner who controls monitoring and, if monitoring occurs, can choose whether to ship at each signal. The paper's Proposition 1 identifies it as

\Pi^{FB}=(1-\bar\beta)r+(\phi-c)^+,\qquad \phi=\sum_{i=1}^{3}\theta_i[r_0-(1-\beta_i)r]^+.

The quantity $\phi$ is the value of using the signal to avoid credit shipments for which the outside sale is better. The supplier receives the full value of TCI when her payoff under a contract equals $\Pi^{FB}$ . Accepted manuscript, Proposition 1 and its proof

Formalization targets

Potential value and first-best

Proposition 1 gives the difference between the first-best and the no-insurance payoff:

\Pi^{FB}-\Pi^{NI} =\min\{\bar\beta L(0),(1-\bar\beta)r-r_0\}+(\phi-c)^+.

This benchmark makes the phrase “full value” testable against a separate maximization over planner policies, rather than against a formula chosen to fit the contract. Accepted manuscript, Proposition 1, p. 11

Cancelable contract with an attractive outside option

The goal is Proposition 3. Under Assumptions 1 and 2, the paper's efficient-monitoring regime $c\le\phi$ , and $r_0\ge(1-\beta_2)r$ , it identifies

\delta=0,\qquad p=f=\frac{c}{\theta_1}+\beta_1r.

The insurer monitors and cancels at signals 2 and 3; the supplier ships only at signal 1. Her payoff equals $\Pi^{FB}$ , and no other admissible cancelable contract gives her more. Milestones establish the monitoring conditions, the first-best formula, feasibility and resulting decisions, attainment of the payoff, and the upper bound over other contracts. Accepted manuscript, Proposition 3, p. 18, and proof, pp. xi–xii

Significance

Proposition 3 identifies a regime where cancelation transmits the insurer's private credit information into the supplier's shipment choice. It gives exact contract terms, the induced actions at each signal, and a payoff that meets the centralized benchmark. The result thus pins down when the option to cancel coverage eliminates the loss from the two parties controlling different decisions. Yang, Bakshi, and Chen (2021), §6.2

The result is proved in the paper. The remaining formalization work is to prove the Lean statements, beginning with the finite three-signal model and ending with the optimality inequality over every admissible cancelable contract. A local prior-art search found no published declaration with this model and these conclusions. The finite contract and policy definitions can also support formal statements about the paper's other regimes, provided their distinct assumptions and timing rules are introduced explicitly.

Difficulty

The contract sits on several decision boundaries. In particular, the insurer's cost of monitoring can equal the refund, so replacing a weak incentive comparison by a strict one would discard the proposed contract. The supplier can be indifferent about shipping at signal 2 after coverage is canceled when $r_0=(1-\beta_2)r$ . The paper's displayed threshold rule and its Proposition 3 proof make different tie choices there. The formal goal follows the proof's choice and records it in the model.

A second difficulty is showing global optimality. Computing the proposed contract's payoff alone does not compare it with contracts that generate different cancelation or shipping patterns. The upper-bound milestone covers all admissible cancelable contracts, while the first-best is defined from the planner's actual choices. The threshold $\mathbb B=(r-r_0)/[\delta+L(r-\delta-p)]$ cannot define shipping at the proposed contract, because its denominator is zero there. Accepted manuscript, equations (1), (6)–(9), and proof of Proposition 3

Formalization scope

Lean uses real-valued prices, costs, probabilities, and payoffs, and a finite signal type with three members. Lean indices $0,1,2$ correspond to the paper's signals $1,2,3$ . The prior $\bar\beta$ is defined by Table 1's weighted average $\sum_i\theta_i\beta_i$ . Standing hypotheses state nonnegative signal probabilities summing to one, ordered default probabilities in $[0,1]$ , $r_0<r$ , $r_0<(1-\bar\beta)r$ , and positive monitoring cost. The explicit additions $l\ge0$ and $\theta_1>0$ make financing cost nonnegative and $c/\theta_1$ meaningful. Assumption 1, Assumption 2, and $c\le\phi$ remain separate hypotheses.

Decisions are defined by payoff comparisons. Shipping under coverage uses the weak inequality in (1); cancelation and shipping after cancelation use the strict tie choices in the proof of Proposition 3, equations (64)–(66). The first-best is a maximum over no-monitoring choices and all shipping policies after monitoring. Optimality compares the supplier's payoff with every valid cancelable contract that induces monitoring and actual cancelation at some signal. Defining the first-best as the desired formula, restricting competitors to contracts with the proposed policy, or using division by a zero threshold denominator would empty the intended claim.

The development needs finite sums, real inequalities, maxima, and a representation of sequential contract decisions. Contributions proving the monitoring characterization, planner value, feasibility, payoff identity, and global upper bound are within scope. The model's finite signal and contract interfaces may be reused in further results of the paper.

Selected references

S. A. Yang, N. Bakshi, and C. J. Chen, Trade Credit Insurance: Operational Value and Contract Choice, Management Science 67(2), 2021. DOI.
S. A. Yang, N. Bakshi, and C. J. Chen, Trade Credit Insurance: Operational Value and Contract Choice, authors' accepted manuscript, LBS Research Online eprint 1343, current version December 2019. Repository record.

7 thms2 active usersReviewed

Completed

Economics Operations Research Probability·Captain: mikedeng1

Optimal Financing and Disclosure: Truthfully Revealing Whether Cash Flows Exceed the Threshold at Which the Financing Constraint Binds Is an Optimal Disclosure PolicyResearch Paper

Motivation

A firm that needs outside money to start a project knows more about the project than its investors do, and it can usually choose how much of that knowledge to reveal before raising funds: which audits to commission, which metrics to report, how informative an analyst's report will be. The security-design literature studies the security side of this problem, meaning what claim to sell given the information the investors have (Innes, 1990; Nachman and Noe, RFS 1994). The Bayesian persuasion literature (Kamenica and Gentzkow, Bayesian Persuasion, AER 2011) studies the information side, meaning what to reveal when a sender can commit to a signal in advance.

M. Szydlowski, Optimal Financing and Disclosure (Management Science 2021; working paper of March 2017), puts the two together. An entrepreneur who cannot finance a project on the prior alone commits to a disclosure policy so as to maximize her expected payoff, subject to the investors' competitive pricing. The main answer is simple and testable: the optimal policy is a pass/fail test, and the passing standard is set exactly where investors break even. This mission formalizes that answer and the chain of lemmas the paper's appendix uses to reach it.

Setting

The project pays $s \in [0,1]$ . The investment cost is $I \in (0,1)$ . The entrepreneur sells a security with payoff $c(s)$ to competitive investors. $c$ is continuous, $0 \le c(s) \le s$ , and both $c(s)$ and the residual $s - c(s)$ are weakly increasing (equity, debt $\min(s,R)$ and options all qualify). The common prior over $s$ has a continuous density $\mu_0$ with support $[0,1]$ .

A posterior is a probability measure $\mu$ on $[0,1]$ . At posterior $\mu$ the security sells for $p(\mu) = \mathbb E_\mu c(s)$ (1), and the project is financed iff $p(\mu) \ge I$ (2). If it is financed, the entrepreneur receives the residual, a private benefit $B > 0$ , and a share $\lambda \in [0,1]$ of the excess cash, so her payoff (3) is

V(\mu) = \mathbb E_\mu[s - c(s) + B] + \lambda\big(\mathbb E_\mu c(s) - I\big) \ \text{ if } \mathbb E_\mu c(s) \ge I, \qquad V(\mu) = 0 \text{ otherwise}.

A disclosure policy induces a distribution $\tau$ over posteriors. By Kamenica and Gentzkow's equivalence, the feasible $\tau$ are exactly the Bayes-plausible ones, those whose mean posterior is the prior, $\mathbb E_\tau \mu = \mu_0$ (5). The entrepreneur's problem (6) is to maximize $\mathbb E_\tau V(\mu)$ over Bayes-plausible $\tau$ . The threshold policy with cutoff $t$ reveals only whether $s \ge t$ . With probability $q = \int_t^1 \mu_0$ it produces the posterior $\mu_h = \mu_0 / q$ on $[t,1]$ , and otherwise the posterior $\mu_l = \mu_0/(1-q)$ on $[0,t)$ ; this is (17).

Throughout, the project cannot be financed without disclosure: $\mathbb E_{\mu_0} c(s) < I$ (§4).

Formalization targets

Goal: Proposition 1 (p. 18)

There is a threshold $\hat s \in (0,1]$ at which the financing constraint (20) binds,

\int_{\hat s}^1 \big(c(s) - I\big)\,\mu_0(s)\,ds = 0,

such that the threshold policy with cutoff $\hat s$ is Bayes plausible and attains the maximum of $\mathbb E_\tau V(\mu)$ over every Bayes-plausible $\tau$ . The hypothesis $\lambda I \le B$ is added, as explained under Formalization scope.

Milestones (proof of Proposition 1, Appendix A)

Lemma 1 (p. 15): every Bayes-plausible $\tau$ can be replaced, at the same value, by one with two posteriors $\mu_h, \mu_l$ with densities and $\mathbb E_{\mu_l} c < \mathbb E_{\mu_0} c < I \le \mathbb E_{\mu_h} c$ .
Lemma 3 (p. 35): at an optimum of the relaxed fixed- $q$ problem (31), the mass constraint and the financing constraint cannot both be slack.
Lemma 4 (p. 36): the states with nonnegative marginal contribution form an interval $\hat S = [\hat s, 1]$ .
Proposition 7 (p. 33): for fixed $q \in (0,1)$ , the threshold density (17) solves problem (30).
Lemma 5 (p. 38, monotonicity part): the fixed- $q$ value $V(q)$ is strictly increasing in $q$ .
Lemma 6 (p. 38): there is a maximal feasible $\bar q \in (0,1)$ , and $\hat s(\bar q)$ makes (20) bind.
Proposition 8 (p. 37, first case): the optimal two-posterior value is $V^* = \int_{\hat s}^1 (s - c(s) + B)\,\mu_0(s)\,ds$ (37), attained by (17) with the binding $\hat s$ .

Significance

Proposition 1 gives disclosure a concrete shape: certify whether cash flows clear a bar, and say nothing more. The bar is the lowest one at which investors still break even, so the entrepreneur maximizes the probability of financing. The paper's later results build on it: the choice of the optimal security (Proposition 4), extensions to general utility (Proposition 5), and comparative statics of the threshold in the security's information sensitivity (Propositions 2–3).

The result is proved on paper but has not been machine-checked. A formalization adds three things. It checks a proof whose central step goes through an infinite-dimensional linear-programming duality (Levinson, 1966). It pins down hypotheses the printed statement omits, notably $\lambda I \le B$ . And it provides a reusable Lean account of Bayesian persuasion over a continuum of states, with distributions over posteriors as measures on the space of measures.

Difficulty

The obvious argument is a bang-bang argument. Fix the probability $q$ of financing, put as much high-posterior mass as possible on the best states, then optimize over $q$ . Each step hides a gap. The reduction to two posteriors (Lemma 1) needs barycentres of a measure on the space of measures. The fixed- $q$ problem is a linear program over densities with a pointwise cap $\mu_h \le \mu_0/q$ , so finite-dimensional LP duality does not apply. The paper uses an infinite-dimensional duality theorem plus a compactness lemma under an extra equicontinuity restriction (32).

Monotonicity of the value in $q$ is where the printed argument fails in general. The marginal contribution $s - c(s) + B + \lambda(c(s) - I)$ can be negative near the cutoff when $\lambda I > B$ . In that case a slack threshold beats the binding one, and the binding threshold is not optimal. A second trap is that the binding root of (20) need not be unique: for debt, every cutoff above the face value can solve (20) with equality. " $\hat s$ solves (20)" therefore cannot by itself be the content of the theorem.

Formalization scope

The state space is $\mathbb R$ , and $c$ and $\mu_0$ are read only on $[0,1]$ . The prior is Lebesgue measure on $[0,1]$ with density $\mu_0$ . Support $[0,1]$ is encoded as positive prior mass on every nondegenerate subinterval. Posteriors are arbitrary measures on $\mathbb R$ , and a distribution over posteriors is a measure on the space of measures with Mathlib's Giry σ-algebra. Bayes plausibility is: $\tau$ is a probability measure, almost every posterior is a probability measure, and $\tau$ 's monadic join is the prior. Posterior expectations are integrals over $[0,1]$ , written through positive and negative parts so that they are measurable in the posterior. As a result $\mathbb E_\tau V(\mu)$ is never a junk value. Ties in the financing rule go to financing ( $\ge$ ). "Increasing" means weakly increasing. The fixed- $q$ problems range over integrable densities with $0 \le \mu_h \le \mu_0/q$ pointwise, which encodes $\mu_l \ge 0$ . The equicontinuity restriction (32) is dropped; it serves only the compactness Lemma 2, which is not formalized.

Two hypotheses are added, each disclosed in the items that carry it:

$\lambda I \le B$ , on the goal and on Lemma 3, Lemma 5 and Proposition 8. Without it the printed results are false. For $\mu_0 = 1$ , $c(s) = s$ , $I = 0.6$ , $B = 0.1$ and $\lambda = 1$ , the binding threshold $\hat s = 0.2$ earns $0.08$ , while revealing whether $s \ge 0.5$ earns $0.125$ . The hypothesis covers $\lambda = 0$ , the case §5 uses.
$I < c(1)$ , on Lemma 6 and Proposition 8, where $\bar q \in (0,1)$ requires that something can be financed.

The goal quantifies over all Bayes-plausible distributions over posteriors, and its threshold is pinned by optimality, not only by solving (20). A version restricted to threshold or two-point policies, or one whose $\hat s$ is any root of (20), would be a different and weaker theorem. Optimality is stated as "an optimal policy", since the optimum is not unique.

Not formalized: Lemma 2 (compactness); the continuity and differentiability parts of Lemma 5; the second case of Proposition 8 ( $\mathbb E_{\mu_0} c \ge I$ ); and the paper's later Propositions 2–6, 9 and 10. The general definitions of Bayes plausibility and of the reveal-a-cell policy are stated for an arbitrary measurable state space and are reusable for other persuasion missions. Contributions are welcome on any milestone. A barycentre construction for measures on the space of measures (Lemma 1) and a bathtub principle for densities under a pointwise cap (Proposition 7) are of independent use.

Selected references

M. Szydlowski, Optimal Financing and Disclosure, working paper, version of March 2017; published in Management Science 67(1), 2021. https://doi.org/10.1287/mnsc.2019.3462
E. Kamenica and M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
N. Levinson, A class of continuous linear programming problems, Journal of Mathematical Analysis and Applications 16(1), 73–83, 1966.
R. D. Innes, Limited liability and incentive contracting with ex-ante action choices, Journal of Economic Theory 52(1), 45–67, 1990.
D. C. Nachman and T. H. Noe, Optimal design of securities under asymmetric information, Review of Financial Studies 7(1), 1–44, 1994. https://doi.org/10.1093/rfs/7.1.1

10 thms2 active usersReviewed

Completed

Economics Operations Research Probability·Captain: mikedeng1

Renewable Power and Electricity Prices: The Impact of Forward Markets: With Skewed, Variable Wind Output the Expected Spot Price First Falls and Then Rises in Wind CapacityResearch Paper

Motivation

Wind and solar generation have near-zero marginal cost. In a wholesale electricity market where prices are set by the marginal producer, adding such capacity displaces expensive conventional generation and lowers the spot price: the merit-order effect. Regulators and system planners rely on this effect when projecting the price impact of renewable expansion, and empirical studies of European markets report it.

Most electricity, however, is not traded only in the spot market. Producers and retailers hedge in forward markets before demand and wind output are known, and forward trading changes how producers with market power behave in the spot market (Allaz and Vila, 1993). Peura and Bunn (Management Science, 2021) ask what happens to the merit-order effect once this channel is included. Their answer is that, when wind output is variable and positively skewed, additional wind capacity eventually raises the expected spot price and the forward price. This mission formalizes that statement, Proposition 2 of the paper, together with the equilibrium characterization it rests on.

Setting

There are two conventional producers with constant marginal cost $c$ , a set of price-taking wind producers with total capacity $k_W \ge 0$ and zero cost, $N_R \ge 1$ price-taking retailers who resell at a fixed retail price $p_R$ , and an elastic industrial demand $D_I = a - p_s$ , where $p_s$ is the spot price.

Two random quantities are drawn on a probability space: the total retail demand $\theta$ , bounded, and the wind yield $\xi \in [0, 1]$ , so that available wind output is $\xi k_W$ . They are independent and both have positive variance. Write $\mu_\theta, \sigma_\theta^2, \tau_\theta$ for the mean, variance and third central moment of $\theta$ , and $\mu_\xi, \sigma_\xi^2, \tau_\xi$ for those of $\xi$ . The coefficient of variation of the yield is $CV_\xi = \sigma_\xi/\mu_\xi$ and its normalized skewness is $\tau^N_\xi = \tau_\xi/\sigma_\xi^3$ .

Trading has two stages.

Forward stage. Before $(\theta, \xi)$ is known, each producer sells a forward quantity $f_{Pi}$ and each retailer buys $f_{Ri}$ at a common forward price $p_f$ . The market clears at zero net supply, $f_P = f_R$ . Every participant maximizes the mean-variance utility $U(\pi) = E[\pi] - \frac{\lambda}{2}V(\pi)$ of its profit, with risk aversion $\lambda > 0$ . Retailers take $p_f$ and the spot-price distribution as given. Producers have market power in the forward market: a producer evaluates each alternative forward position at the forward price that would clear the market.
Spot stage. After $(\theta, \xi)$ is revealed, the producers compete à la Cournot on the inverse residual demand $p_s = a + \theta - \xi k_W - q_P$ , each maximizing $p_s(q_{Pi} - f_{Pi}) - c\,q_{Pi}$ .

With $q_0 = a - c + \theta - \xi k_W$ and $p_0 = a + 2c + \theta - \xi k_W$ , the spot equilibrium is $q^*_{Pi} = (q_0 + 2f_{Pi} - f_{Pj})/3$ and $p_s = (p_0 - f_P)/3$ (Lemma 1). The forward-spot equilibrium is $f^*_{Pi} = \omega/\nu$ and $p_f = a_f - 2b_f\omega/\nu$ for explicit expressions $\omega, \nu, a_f, b_f$ in the parameters, the moments, and $k_W$ (Theorem 1).

Formalization targets

Goal: Proposition 2

CV_\xi\,\tau^N_\xi \ge \zeta := \frac{27}{4N_R},

then an equilibrium exists at every capacity $k_W \ge 0$ , and there are thresholds $\bar k^s_W > 0$ and $\bar k^f_W \ge 0$ such that along every equilibrium selection

k_W \mapsto E[p_s] \text{ is strictly decreasing on } [0, \bar k^s_W] \text{ and strictly increasing on } [\bar k^s_W, \infty),

k_W \mapsto p_f \text{ is strictly increasing on } [\bar k^f_W, \infty).

The value of $\zeta$ comes from the paper's proof; the proposition itself only asserts that some $\zeta > 0$ works.

Milestones

Lemma 1 (p. 12): the spot Cournot equilibrium given forward positions.
Lemma 2 (p. 13): the retailers' optimal forward positions, a basis term plus a hedging term, and the resulting clearing condition.
Theorem 1 (p. 14): existence, uniqueness and closed form of the forward-spot equilibrium.
Derivative of $E[p_s]$ (proof of Proposition 2, p. 37): $\partial E[p_s]/\partial k_W = s_{p_s}(k_W)/(9N_R^2\nu^2)$ , where $s_{p_s}(k_W) = \alpha_0 + \alpha_1 k_W + \alpha_2 k_W^2 + \alpha_4 k_W^4$ is a quartic with no cubic term and explicit coefficients.
Sign of the quartic (p. 37): under the $\zeta$ condition, $\alpha_4 \ge 0$ , $\alpha_2 > 0$ and $\alpha_0 < 0$ , and $s_{p_s}$ changes sign exactly once on $[0, \infty)$ , from negative to positive.
Forward price (p. 37): the derivative of the closed-form forward price is eventually positive.

Significance

The result. Proposition 2 isolates a mechanism by which two pro-competitive forces, low-cost capacity and forward trading, can combine to raise prices. Variable and skewed wind output increases the risk that a producer is caught with a large forward position when wind is high and the spot price is low. Producers therefore sell less forward, which by Lemma 1 lowers their spot output and raises the spot price. For large enough capacity this forward effect outweighs the merit-order effect. The condition for the reversal involves only $CV_\xi$ and $\tau^N_\xi$ .

Formalizing it. The result is proved in the paper but has no machine-checked proof. In a formal development the equilibrium has to be defined through the participants' optimization problems, not through the closed forms. Theorem 1 then has to show that this optimization-defined equilibrium exists, is unique, and equals the closed form. The polynomial coefficients have to be checked: the printed $\alpha_1$ has a misplaced parenthesis, and the printed $s_{p_s}$ is off by a factor of $3N_R^2$ . Both are corrected and disclosed in the milestone statements. Neither affects the conclusion.

Difficulty

The goal combines three layers. The probabilistic layer computes means, variances and covariances of products of independent bounded random variables. These computations produce the third central moments $\tau_\theta, \tau_\xi$ and justify replacing the utility of each participant by an explicit quadratic in its own position. The game-theoretic layer has to show that each first-order condition gives a global optimum, which needs strict concavity, and that the producers' best responses, each computed against a clearing price that itself depends on the deviation, meet at a unique point. The analytic layer studies the rational function $E[p_0]/3 - 2\omega/(3\nu)$ of $k_W$ , whose derivative's numerator is a quartic with coefficients that are themselves polynomials in eleven quantities.

A tempting shortcut is to define the equilibrium by its closed form, which reduces the goal to a sign argument on a polynomial. That shortcut removes Theorem 1 entirely and is excluded here. A second tempting reading treats the forward price as fixed when a producer deviates. That makes producers price takers in the forward market, which is a different game whose equilibrium is not $\omega/\nu$ .

Formalization scope

The market parameters are a structure with fields a, c, pR, lam ( $\lambda$ , a Lean keyword) and NR : ℕ; the retailers are indexed by Fin NR. The demand $\theta$ and the yield $\xi$ are real functions on a probability space $(\Omega, P)$ , and the capacity $k_W$ is a separate real argument, so the joint law stays fixed as $k_W$ varies. The standing assumptions, a hypothesis of every model theorem, are: $\theta$ and $\xi$ are measurable and independent; $\theta$ is bounded and $0 \le \xi \le 1$ at every sample point; $\lambda > 0$ ; $N_R \ge 1$ ; $V(\theta) > 0$ and $V(\xi) > 0$ . The last two come from the paper's statement that demand and supply are uncertain in the forward market. Third moments are central. The footnoted conditions $N_R > 6$ and $c \le \min\{p_R, a\}$ are not assumed, since the goal holds without them.

The spot inverse demand is the interior branch of the paper's $p_s = \max\{a + \theta - \xi k_W - q_P, 0\}$ , used for all $k_W \ge 0$ and all realizations, with quantities ranging over the reals. This is what Assumption 1 (no blackouts or curtailment) licenses and what the paper's proof differentiates. The statement is therefore about the model with linear inverse demand. At realistic parameter values the turning point $\bar k^s_W$ can lie where Assumption 1 fails for some realizations, so its economic reading inside the no-curtailment region is the paper's interpretation, not part of the theorem.

The forward-spot equilibrium is a predicate built from optimization alone: retailer optimality over all real positions, clearing, and each producer's optimality against every deviation evaluated at that deviation's own clearing price. The closed forms (13)–(16) and the quartic's coefficients live in a separate definition file used only in milestone conclusions. The goal imports only the model. The goal also contains an existence conjunct, so the statement about equilibrium selections is not vacuous.

A complete development needs moment calculus for bounded independent random variables (variance and covariance of products, third central moments), maximization of concave quadratics, and single-crossing arguments for real polynomials. The moment computations and the mean-variance optimization of an affine position are reusable beyond this mission. Contributions are welcome at every milestone, including partial results.

Selected references

H. Peura, D. W. Bunn, Renewable power and electricity prices: The impact of forward markets, Management Science 67(8), 4772–4788, 2021. https://doi.org/10.1287/mnsc.2020.3710 (read as the author-accepted manuscript, LBS Research Online eprint 1432, https://lbsresearch.london.edu/id/eprint/1432/).
B. Allaz, J.-L. Vila, Cournot competition, futures markets and efficiency, Journal of Economic Theory 59(1), 1–16, 1993. https://doi.org/10.1006/jeth.1993.1001
H. Bessembinder, M. L. Lemmon, Equilibrium pricing and optimal hedging in electricity forward markets, Journal of Finance 57(3), 1347–1382, 2002. https://doi.org/10.1111/1540-6261.00463

9 thms2 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

The Internet of Things and Information Fusion: Who Talks to Who?: With Known Asymmetric Qualities Each Sensor Has Exactly One Long-Run Contact on Every Sample PathResearch Paper

Motivation

Networks of autonomous sensors — machines on a factory floor, vehicles, devices in the Internet of Things — each measure a common environment with their own noise and can improve their estimates by asking other sensors for theirs. Communication capacity is limited, so each sensor must decide whom to ask, and the answer it receives is useful only to the extent that it understands how the other sensor turns measurements into estimates. Saghafian, Tomlin and Biller (SSRN 3124417, version of October 16, 2020; published in Manufacturing & Service Operations Management, 2021) model this as a dynamic target-selection problem and ask which communication network forms in the long run. Their abstract leads with the answer: each sensor eventually settles on a constant target set, which is sample-path dependent. With known, pairwise distinct qualities this target set is a single sensor (Proposition 4, p. 21). This mission formalizes that result.

Setting

There are $n$ sensors $N = \{1, \dots, n\}$ . Sensor $i$ has a quality $q_i > 0$ : its measurement of the state has noise variance $1/q_i^2$ . Sensor $i$ starts with initial familiarities $v_{ij0}, w_{ij0} > 0$ with each other sensor $j$ , the precisions of its initial Gaussian beliefs about $j$ 's inference parameters. A sample path $S_\infty = (s_0, s_1, s_2, \dots)$ is the sequence of realized states, an arbitrary sequence of reals.

The familiarity function of $i$ with $j$ in period $t$ is a function $\psi_{ijt} : \mathbb R \to \mathbb R$ . It starts at

\psi_{ij1}(s) = \frac{v_{ij0}^2 w_{ij0}^2}{w_{ij0}^2 + v_{ij0}^2 s^2} \qquad (12)

In period $t$ , after $s_{t-1}$ is revealed, sensor $i$ targets the sensor of least signal variance

j^*_{it} = \arg\min_{j \in N\setminus\{i\}} \frac{q_j^2 + 1/\psi_{ijt}(s_{t-1})}{q_j^4}, \qquad (10)\text{–}(11)

with ties broken toward the lower index (footnote 11). Writing $a_{ijt} = 1$ if $j^*_{it} = j$ and $0$ otherwise, the familiarity grows by the stickiness factor:

\psi_{ij,t+1}(s) = \psi_{ijt}(s) + f(q_i,q_j)\,a_{ijt}, \qquad f(q_i,q_j) = \frac{1+q_i^2}{q_j^2(1+q_i^2+q_j^2)}. \qquad (14)

The long-run contacts of $i$ along $S_\infty$ are (Definition 2)

T_i(S_\infty) = \{\, j \in N\setminus\{i\} : \lim_{t\to\infty} \psi_{ijt}(s_{t-1}) = \infty \,\}. \qquad (20)

In Lean these are Instance (q, v, w), psi1, sigma2, stick, lowArgmin, the joint recursion fam/target, count and longRunContacts in IoTFusion.KnownQuality.

Formalization targets

Goal: Proposition 4 (p. 21)

If the qualities are asymmetric ( $q_j \neq q_{j'}$ for $j \ne j'$ , Definition 3), then for every sample path

|T_i(S_\infty)| = 1 \qquad \text{for all } i \in N.

No hypothesis on the state process is involved: the statement holds path by path.

Milestones

Proposition 2 (p. 15): the closed form $\psi_{ij,t+1}(s) = \psi_{ij1}(s) + f(q_i,q_j)\sum_{l=1}^{t} a_{ijl}$ (15).
Remark 1 (p. 20): $j \in T_i(S_\infty)$ iff $i$ targets $j$ infinitely often.
Lemma 2 (p. 21): for every $\epsilon > 0$ there is a fixed threshold $\bar\psi_\epsilon$ such that $\psi_{ijt}(s_{t-1}) > \bar\psi_\epsilon$ and $q_j/q_{j'} > 1+\epsilon$ imply $j^*_{it} \ne j'$ .

Supporting items: $T_i(S_\infty) \ne \emptyset$ for $n \ge 2$ (long_run_contacts_nonempty); each sensor eventually targets one fixed sensor (eventually_constant_target, the wording of p. 5); and the rank-one precision identity (EC.66).

Significance

Proposition 4 says that, with known and distinct qualities, the long-run communication network is a functional graph — every sensor has out-degree one — although which graph forms depends on the realized states, and a sensor's eventual partner need not be the highest-quality sensor available. The paper builds on it its description of the long-run network as a random directed graph (Propositions 5–6) and its managerial discussion of early-period "momentum" in familiarity.

The result is proved in the paper; nothing in it is machine-checked. The work here is a formal proof of the deterministic core, including the existence half $T_i \neq \emptyset$ , which the printed proof (p. ec22) does not give: it shows only $|T_i| \le 1$ .

Difficulty

Every statement is elementary in isolation; the difficulty is that the target sequence is defined by a feedback loop. The target of period $t$ depends on familiarities, which depend on all earlier targets, which depend on earlier states. Statements about "infinitely often" therefore cannot be reduced to the behavior of any single function of $t$ fixed in advance.

The tempting argument "the highest-quality sensor eventually wins" is false: a sensor that becomes familiar early with a lower-quality partner can keep choosing it forever, so no fixed candidate for the unique contact exists. The uniqueness argument must instead compare two putative long-run contacts with each other, using a familiarity threshold that does not depend on the familiarity with the worse one (Lemma 2), and the existence half needs a separate counting argument over the finitely many possible targets.

Formalization scope

Sensors are Fin n (0-based) with $n \ge 2$ on the existence statements; for $n = 1$ there is no other sensor and $T_i = \emptyset$ .
Periods are 0-based: Lean step $k$ is the paper's period $k+1$ , the target at step $k$ uses the state $s_k$ , and fam P i s k is $\psi_{ij,k+1}$ .
$q_i > 0$ , and $v_{ij0}, w_{ij0}$ finite and positive, are theorem hypotheses (the paper's standing assumptions; its limiting case "fully knows", $v = w = \infty$ , is not posed).
Ties go to the lower index; " $\lim = \infty$ " is Filter.Tendsto … atTop atTop; $|T_i|$ is Set.ncard; asymmetry is Function.Injective q.
The familiarity function is defined by (12) and (14), the paper's familiarity dynamics. The paper derives (14) by Bayesian updating of the scalar $\hat\alpha_j + \hat\beta_j s_{t-1}$ . Under the joint Gaussian beliefs, the update is exact for the precision at the realized state $s_{t-1}$ (the item (EC.66)), but at other states $s$ the posterior precision grows by less than $f$ . Proposition 2(i) "for any $s$ " is therefore a modelling choice. Every later result of the paper is derived from (15), so the dynamics (12) + (14) is the paper's operative model. Whether Proposition 4 survives under the exact bivariate posterior is open and not posed.
Not posed: Propositions 5–6. Proposition 5's step "(EC.87): at $t^*$ the sets $T_i(S_\infty)$ are all determined" does not follow. Even with Gaussian innovations, a continuation of the path through a state near $0$ after any $t^*$ can make a never-targeted higher-quality sensor the unique long-run contact, so the printed claim fails without further assumptions on the state process. Lemma 1, Proposition 3 and Proposition 7 (unknown qualities) are outside this mission.
Lemma 2's threshold depends on the pair $(j, j')$ in the paper's proof; the statement fixes the instance first and asks for one threshold per $\epsilon$ , uniform over paths, sensors and periods (the maximum over the finitely many pairs).
Trivializations ruled out: the target ranges over $j \neq i$ only, with a specified tie-break; familiarity and target form one trajectory determined by the instance, the sensor and the path, with no free history argument; $T_i$ is defined by divergence of $\psi_{ijt}(s_{t-1})$ , not by target counts; the goal is $|T_i| = 1$ , not $\le 1$ ; and it quantifies over every real path, with no AR(1) or typicality hypothesis.
Infrastructure: none beyond Mathlib (finite sets, filters, $2\times2$ matrices for (EC.66)). Proofs of the milestones, of the existence half and of the goal are welcome in any order. A general lemma that "a sequence in a finite set takes some value infinitely often" with the matching Set.ncard bookkeeping would be reusable.

Selected references

S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, SSRN 3124417, version of October 16, 2020. https://ssrn.com/abstract=3124417
S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2020.0958

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Delegating Innovation Projects with Deadline: Committed vs. Flexible Stopping: Commitment Beats Flexibility Exactly When the Evaluation Cost Is Intermediate and p ≥ (c_h − c_l)/(μ_h − μ_l)Research Paper

Motivation

Firms increasingly delegate the generation of new concepts (product designs, advertising campaigns, engineering prototypes) to outside providers such as design agencies and engineering consultancies. The client cannot dictate how hard the provider works; it can only decide when to stop asking for new solutions. Two practices are common. Under a flexible stopping policy the client keeps the right to stop or continue after each submitted solution. Under a committed stopping policy the client commits in advance to stop, and pay, as soon as a feasible solution arrives. Classical search theory says that keeping options open is never harmful, so flexibility should dominate. Yet committed contracts are widespread in practice.

Rahmani and Ramachandran (2021) explain this by two features that the classical benchmarks omit: a deadline on the number of rounds, and a provider who adjusts its effort from round to round in response to the client's policy. In two benchmark settings, an unlimited number of rounds or a fixed provider effort, flexibility (weakly) dominates (their Lemmas 1 and 2). With a deadline and strategic effort, commitment can be strictly better, and the paper characterizes exactly when.

Setting

A client delegates a project of $T = 2$ rounds to a provider. In each round $t$ in which the client asks for a solution, the provider chooses an effort $\mu_t \in \{\mu_l, \mu_h\}$ , at cost $c_l$ or $c_h$ , and submits a solution of quality $v_t \ge 0$ . The client pays an evaluation cost $c_I$ for each submitted solution. When the project stops with a feasible solution ( $v > 0$ ), the client implements the best solution received and pays the provider a fixed payment $p$ ; if no feasible solution is found by the deadline, nothing is paid.

Quality under effort $\mu$ has distribution function

\Phi_\mu(x) = 1 - \mu e^{-x/k}, \qquad x \ge 0,

where $k > 0$ is the provider's capability: with probability $1-\mu$ the solution is infeasible ( $v = 0$ ), and otherwise it has density $\frac{\mu}{k}e^{-v/k}$ on $(0,\infty)$ . The expected quality is $k\mu$ . The standing assumptions are

0 < \mu_l < \mu_h < 1, \qquad 0 \le c_l < c_h, \qquad c_h/\mu_h \ge c_l/\mu_l .

Under the committed policy, the project stops after round 1 if $v_1 > 0$ . Under the flexible policy, after a feasible $v_1$ the client compares $v_1 - p$ with the expected value of a second round and stops when stopping is at least as good. The provider anticipates this and chooses its efforts by backward induction: round-2 efforts $\mu^C_2$ , $\mu^{F+}_2$ (after a feasible first solution), $\mu^{F-}_2$ (after an infeasible one), then round-1 efforts $\mu^C_1$ , $\mu^F_1$ . Write $\Pi^C_1$ and $\Pi^F_1$ for the client's equilibrium expected profits under the two policies.

Formalization targets

Goal: Proposition 4 (a)

Fix $\mu_l,\mu_h,c_l,c_h$ satisfying the standing assumptions and a payment $p > 0$ . There exist thresholds $\hat c_I(k)$ and $\bar c_I(k)$ such that for all $k > 0$ and $c_I > 0$ ,

\Pi^F_1 < \Pi^C_1 \iff \hat c_I(k) < c_I < \bar c_I(k) \ \text{ and } \ p \ge \frac{c_h - c_l}{\mu_h - \mu_l}.

Commitment is strictly better exactly for an intermediate range of evaluation costs, and never when the payment is below $(c_h - c_l)/(\mu_h - \mu_l)$ . The thresholds are left existential, as in the paper.

Milestones

§3.2, property (2): the expected quality under effort $\mu$ is $k\mu$ .
Proposition 2 (a)–(b): the flexible client stops after a feasible $v_1$ if and only if $v_1 \ge v^F_s$ , for a unique threshold $v^F_s \ge 0$ .
Proposition 3 (a): under commitment, $(\mu^C_1,\mu^C_2)$ is $(\mu_l,\mu_l)$ , $(\mu_l,\mu_h)$ , $(\mu_h,\mu_h)$ as $p$ crosses thresholds $\underline p \le \bar p^C$ .
Proposition 3 (b): under flexibility, $\mu^{F+}_2 = \mu_l$ , and $(\mu^F_1,\mu^{F-}_2)$ switches at $\underline p$ and $\bar p^F$ .
Proposition 3 (c): $\bar p^C \le \bar p^F$ , and $\bar p^F - \bar p^C$ is nondecreasing in $k$ and nonincreasing in $c_I$ .
Proposition 2 (c): $v^F_s$ is nondecreasing in $k$ and nonincreasing in $c_I$ .
Lemma 2 at $T = 2$ : with the same effort in every round, $\Pi^C_1 \le \Pi^F_1$ .

Significance

Proposition 4 reverses the conventional wisdom that retaining decision rights cannot hurt the decision maker. The mechanism is strategic: flexible stopping lowers the provider's expected reward for a good first solution, because the client may continue the search instead of accepting it, and so it weakens the provider's first-round effort (Proposition 3). When the payment is in $[\bar p^C, \bar p^F)$ , commitment induces high first-round effort that flexibility does not, and whether this outweighs the option value of a second round depends on the evaluation cost. The result gives contract designers in innovation procurement a concrete criterion in terms of evaluation cost, capability and payment.

The paper's proofs are in an online appendix. No machine-checked version of any result in this model exists. The mission produces a formal model of a dynamic principal–agent stopping game with an atom-plus-density quality law, a verified threshold structure for the client's stopping rule, and the full equilibrium effort characterization, all of which carry over to related delegation and contest models.

Difficulty

The goal compares two equilibrium profits, each determined by a nested backward induction in which the provider's round-1 effort depends on the client's stop rule, which in turn depends on the provider's round-2 effort. The obvious approach, comparing the two policies at the same efforts, proves only Lemma 2 and points the wrong way. The comparison must instead track which of the effort regimes of Proposition 3 each policy induces, as a function of $p$ and $c_I$ . The profits are piecewise in $c_I$ (the stopping threshold is zero for large $c_I$ ), and the claim that the strict-improvement set in $c_I$ is a single open interval requires a monotonicity argument across these pieces, uniformly in $k$ . The case $p < (c_h-c_l)/(\mu_h-\mu_l)$ must be shown to give no improvement at all.

Formalization scope

The Lean development models exactly the two-round game ( $T = 2$ ), the case the paper analyzes in §4. Effort levels form a two-element inductive type; parameters $(\mu_l,\mu_h,c_l,c_h,k)$ form a record, with $c_I$ and $p$ separate arguments. The standing assumption $c_h/\mu_h \ge c_l/\mu_l$ is written cross-multiplied; $c_l \ge 0$ is the reading that costs are non-negative. The paper's Stieltjes integrals $\int_a^\infty g\,d\Phi_\mu$ are Bochner integrals of $g$ against the density over the open ray $(a,\infty)$ ; the atom at $0$ appears in the separate $\Phi_\mu(a)$ terms, so no payment is charged on infeasible solutions. Ties are broken as on the page: the provider takes high effort, and the flexible client stops. The paper's restriction to payments "neither too high nor too small" (Lemma A-1 of its online appendix) is not available; every statement is posed for all $p > 0$ , for which it remains true. Evaluation costs satisfy $c_I > 0$ .

The model defines no stopping threshold and no effort in closed form: the stopping threshold $v^F_s$ is a theorem (Proposition 2), $\mu^{F+}_2$ is computed from the provider's objective, and the goal compares profits at the efforts the model computes, not at efforts supplied as arguments. A formalization that defined $v^F_s = k\log(k\mu_l/c_I)$ , fixed $\mu^{F+}_2 = \mu_l$ , or compared the policies at exogenous efforts would make the milestones trivial or prove a different theorem, and is ruled out.

A complete development needs integrals of polynomial-times-exponential functions on rays, the closed forms of the round-2 values, and finite case analysis over effort profiles. Contributions to the comparative statics (Propositions 2 (c), 3 (c)) are welcome independently of the goal.

Not formalized: Proposition 4 (b) (its $\hat c_I$ half fails under the main-text model, e.g. at $\mu_l = 1/2$ , $\mu_h = 4/5$ , $c_l = 1/2$ , $c_h = 1$ , $p = 7/2$ , $c_I = 9/10$ , $k \in \{6, 8\}$ ); Lemma 1 (infinite horizon); Proposition 1 (general finite $T$ ); Proposition 5 (dependent solutions); Propositions 6–8 (endogenous payments); the numerical study.

Selected references

M. Rahmani and K. Ramachandran, Delegating Innovation Projects with Deadline: Committed vs. Flexible Stopping, Management Science 67(10):6317–6332, 2021. https://doi.org/10.1287/mnsc.2020.3800
C. Terwiesch and C. Loch, Collaborative prototyping and pricing of custom-designed products, Management Science 50(2):145–158, 2004 (cited by the paper as the source of the infinite-round and fixed-effort benchmarks).

9 thms2 active usersReviewed

Completed

Economics Operations Research Probability·Captain: mikedeng1

Information Sharing on Retail Platforms: Under Asymmetric Full Sharing the Platform Optimally Shares All Signals Truthfully with Floor or Ceiling of min(2/b - 1, N) SellersResearch Paper

Why platforms share demand information

Online retail platforms such as Amazon, Alibaba's Tmall and JD.com host thousands of third-party sellers and observe every customer interaction with each of them. From these interactions the platform learns about market demand far better than any single seller can, and it sells or gives away part of that knowledge through analytics tools (Alibaba's Business Advisor is the example in the source paper). The platform earns a commission on every seller's revenue, so it cares about the sellers' total profit, and it has to decide what each seller is told.

The classic literature on information sharing in oligopoly points the other way. Gal-Or (1985) showed that Cournot competitors facing a common demand shock never voluntarily pool their private demand signals: shared information makes their strategies more correlated, and the resulting competition destroys more value than the better forecasts create. Li (2002) and others refined the conditions. Liu, Zhang and Zhang (Manufacturing & Service Operations Management, 2023; SSRN 3258109) change who decides: the signals belong to the platform, which chooses what each seller learns in order to maximize its commission. Their headline result for the unconstrained ("asymmetric full sharing") format is that the platform shares everything it knows, without any added noise, but only with a limited number of sellers, and that number is determined by the substitution between products alone.

The model

There are $N \ge 1$ sellers of substitutable products. Given quantities $q_1, \dots, q_N$ , seller $i$ 's price is

p_i = a - q_i - b\sum_{d \ne i} q_d + u, \qquad 0 < b \le 1,

where $u \sim N(0, \sigma)$ is a common demand shock with prior variance $\sigma > 0$ . The platform observes, for each seller $i$ , a signal $x_i = u + e_i$ with $e_i \sim N(0, t)$ , $t > 0$ , independent of everything else.

A noise matrix $M = (m_{ij})$ with entries in $[0, +\infty]$ is the platform's sharing strategy. Seller $j$ receives the noisy copy $\hat x_{ij} = x_i + \epsilon_{ij}$ , $\epsilon_{ij} \sim N(0, m_{ij})$ independent, for every $i$ with $m_{ij} < +\infty$ ; $m_{ij} = 0$ is truthful sharing and $m_{ij} = +\infty$ means $x_i$ is withheld from seller $j$ . Seller $j$ 's information $y_j(M)$ is the $\sigma$ -algebra generated by what he receives.

Each seller chooses a quantity measurable with respect to his information to maximize his expected profit $\pi_i = E[(1 - \alpha) q_i p_i]$ , where $\alpha \in (0,1)$ is the platform's commission rate. A Bayesian equilibrium under $M$ is a profile of such strategies from which no seller gains by deviating. The platform's expected profit is $\Pi = E[\alpha \sum_i q_i p_i]$ , and it chooses $M$ before the signals are realized.

Under Asymmetric Full Sharing (AFS) each seller $j$ receives all $N$ signals with one common noise level $\eta_j = m_{ij}$ (for all $i$ ), and the levels may differ across sellers. The benchmark is no sharing, $m_{ij} = +\infty$ for all $i, j$ , with platform profit $\Pi_{NS} = \alpha N a^2/[2 + b(N-1)]^2$ .

Formalization targets

Goal: Proposition 2 (optimal asymmetric full sharing)

Let $m = \min\{2/b - 1, N\}$ . Among all AFS noise matrices in $[0,+\infty]^{N \times N}$ and all equilibria, an optimal strategy is to share $\{x_1, \dots, x_N\}$ truthfully with sellers $1, \dots, K^*$ and nothing with the others, where

K^*_{AFS} \in \big\{\lfloor m \rfloor, \lceil m \rceil\big\}, \qquad \Pi^*_{AFS} = \frac{\alpha N a^2}{[2 + b(N-1)]^2} + \frac{\alpha K^*_{AFS}\,\sigma^2}{[2 + b(K^*_{AFS} - 1)]^2\,(\sigma + t/N)}.

The platform and every seller do weakly better than without sharing, and every optimal truthful group has size $\lfloor m \rfloor$ or $\lceil m \rceil$ .

Milestones

Eq. (5): under full sharing with noise $\eta$ , $E[u \mid y_j] = \frac{\sigma}{\sigma + (t + \eta)/N}\cdot\frac1N\sum_i \hat x_{ij}$ .
Eq. (4): a profile is an equilibrium iff $q_i = \frac12\big(a - b\sum_{d\ne i}E[q_d \mid y_i] + E[u \mid y_i]\big)$ for all $i$ .
Lemma 1: the no-sharing equilibrium quantities $a/(2 + b(N-1))$ and profit $\Pi_{NS}$ .
A seller who receives nothing earns exactly his no-sharing profit (p. 13).
Under AFS, an interior noise level for one seller is strictly beaten by $0$ or $+\infty$ (p. 16).
Proposition 1 (AFS half): optimal AFS matrices have $m^*_{ij} \in \{0, +\infty\}$ .
Eq. (8) at every group size $K \le N$ .
The integer maximizers of $K \mapsto K/[2 + b(K-1)]^2$ on $\{0,\dots,N\}$ lie in $\{\lfloor m \rfloor, \lceil m \rceil\}$ (p. 18).
Informed sellers strictly gain and the others earn the benchmark (p. 19).

Significance

The result separates two levers of information design, precision and audience, and shows that in this linear-Gaussian Cournot setting only the audience matters: the platform never degrades a signal, it only chooses how many sellers see it. The optimal audience size $\min\{2/b - 1, N\}$ depends only on the substitution parameter once the market is large, and equals one seller when products are perfect substitutes. This reverses the Gal-Or no-sharing result by changing who decides, and it explains why a commission-earning platform may rationally treat its sellers asymmetrically, which is the tension the paper's later sections on fairness and privacy constraints study.

The paper's proofs are in an online appendix. No part of this model has a machine-checked proof. The mission produces a reusable Lean layer for Bayesian games with designed Gaussian signals: information $\sigma$ -algebras generated by noisy copies of shared signals, Bayesian Nash equilibrium over square-integrable strategies, and its characterization by first-order conditions in conditional expectations. Mathlib has Gaussian measures, conditional expectation and independence, but not the projection formula for jointly Gaussian vectors that eq. (5) needs.

Difficulty

The closed forms are routine once one assumes that equilibria are linear in the received average signal. The difficulty lies in what that assumption skips. First, eq. (5) is a statement about conditional expectation with respect to a $\sigma$ -algebra generated by $N$ correlated Gaussian variables; it needs the Gaussian conditioning (projection) theorem, not a computation with densities. Second, the goal quantifies over all equilibria, so existence and uniqueness of the equilibrium must be proved for every noise matrix, including those with infinite entries; the paper solves the first-order condition and never discusses uniqueness. Third, Proposition 1 is an optimization over $[0,+\infty]^N$ : the platform's profit is not concave in the noise levels, and the endpoint property for one seller (with the others fixed at arbitrary levels) is the step that rules out partial sharing. Restricting attention to truthful groups from the outset assumes away exactly this step.

Formalization scope

All declarations live in the namespace RetailInfoShare.AFS, with one definitions file RetailInfoShare.AFS.Model. Conventions:

$\sigma$ , $t$ and $m_{ij}$ are variances (gaussianReal 0 σ), as eq. (3) of the paper requires.
The primitives $u$ , $e_i$ and standard normals $\xi_{ij}$ are measurable and mutually independent on one probability space; the added noise is $\epsilon_{ij} = \sqrt{m_{ij}}\,\xi_{ij}$ . The paper's "cov = 0" is read as independence, as its text says.
Noise levels are in ℝ≥0∞; a signal with $m_{ij} = \top$ never enters the receiving seller's information $\sigma$ -algebra.
Equilibrium is the ex-ante best-response property over square-integrable strategies measurable for the seller's information; this is equivalent a.e. to the interim maximization of eq. (2).
The platform's profit is the unconditional expectation (the matrix is chosen before the signals).
Added standing hypotheses: $0 < \alpha < 1$ (never stated in the paper), and $\sigma > 0$ , $t > 0$ , $N \ge 1$ made explicit. Sellers are Fin N, so the paper's sellers $1,\dots,K$ are indices $0,\dots,K-1$ .
Profits and equilibria are defined from the model, never by the closed forms (4) or (8); a formalization that defined $\Pi$ by eq. (8) or optimized only over truthful groups would reduce the goal to milestone 8 and is ruled out.

Out of scope: the AIS half of Proposition 1, Proposition 3 and Lemma 2 (privacy-constrained sharing), the symmetric formats of §5, the pricing mechanism of §6, and the appendix extensions. Contributions of general infrastructure are welcome: the Gaussian conditioning theorem in Mathlib form, and existence and uniqueness of equilibria in linear-quadratic Bayesian games with Gaussian information.

Selected references

Z. Liu, D. J. Zhang, F. Zhang, Information Sharing on Retail Platforms, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2020.0915 (preprint: SSRN 3258109, https://ssrn.com/abstract=3258109)
E. Gal-Or, Information Sharing in Oligopoly, Econometrica 53(2), 1985. https://doi.org/10.2307/1911241
L. Li, Information Sharing in a Supply Chain with Horizontal Competition, Management Science 48(9), 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
L. Li, Cournot Oligopoly with Information Sharing, RAND Journal of Economics 16(4), 1985. https://doi.org/10.2307/2555502

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Contract Unobservability and Downstream Competition: Under Unobservable Contracts and Passive Beliefs, Wholesale Prices Beat Two-Part Tariffs for the Manufacturer iff θ ≥ 2√2Research Paper

Motivation

A manufacturer selling through several retailers rarely publishes the terms it gives each of them. Wholesale prices, slotting fees and rebates are negotiated bilaterally, and a retailer usually sees its own contract but not its rival's. Much of the supply-chain contracting literature nevertheless assumes observable contracts, and under that assumption a well-known ranking holds: the manufacturer, the channel and social welfare do better with two-part tariffs (a fixed fee plus a marginal wholesale price), while the retailers do better with plain wholesale-price contracts.

The industrial-organization literature has long known that secrecy changes the manufacturer's problem. Hart and Tirole (1990), O'Brien and Shaffer (1992) and McAfee and Schwartz (1994) showed that a manufacturer that cannot commit publicly to the terms it offers each retailer is tempted to undercut itself bilaterally: it offers one retailer a better deal, at the expense of the others, and the retailers anticipate this. Li and Liu (Manufacturing & Service Operations Management, SSRN 3339702) ask what this does to the ranking of contract types in a simple model of price competition. Their answer, Proposition 3, is that the ranking reverses when competition is intense: the manufacturer prefers wholesale prices once the competition parameter reaches $2\sqrt2$ , the retailers always prefer them, and the whole industry prefers them once the parameter reaches $\sqrt3 - 1$ .

Setting

A manufacturer with zero unit cost sells one product through two retailers $i \in \{1,2\}$ . Retailer $i$ charges price $p_i$ and faces demand

D_i = 1 - p_i + \theta\,(p_j - p_i), \qquad j \ne i,

where $\theta \ge 0$ measures how intensely the retailers compete.

The manufacturer offers each retailer a contract $C_i = (K_i, w_i)$ , a fixed fee $K_i$ and a marginal wholesale price $w_i$ . In the two-part tariff game contracts range over $\{(K,w): w \ge 0\}$ ; in the wholesale-price game over $\{(0,w): w \ge 0\}$ . The contract type is common knowledge, but retailer $j$ does not observe the terms offered to retailer $i$ .

Each retailer, seeing only its own contract, accepts or rejects and chooses a price $p_i \ge 0$ and an order $Q_i \ge 0$ . A retailer holding the belief $\tilde p_j$ about its rival's price conjectures the profit

\tilde\pi_i = p_i \min\bigl(Q_i,\ 1 - p_i + \theta(\tilde p_j - p_i)\bigr) - w_i Q_i - K_i ,

and $0$ if it rejects. The manufacturer earns $w_i Q_i + K_i$ from each retailer that accepts.

Because no proper subgame exists, the solution concept is the contract equilibrium with passive beliefs: a pair of contracts $(C_1^*, C_2^*)$ and, for each retailer, a strategy $\sigma_i$ giving an action at every contract of the class, such that

at every contract $C$ , $\sigma_i(C)$ maximizes $\tilde\pi_i$ for the belief $\tilde p_j$ equal to the rival's equilibrium price, the price in $\sigma_j(C_j^*)$ , so an unexpected offer does not change the belief;
no pair of contracts gives the manufacturer more total profit when each retailer responds to its own contract through $\sigma_i$ .

The equilibrium profits are the manufacturer's $\Pi$ , retailer $i$ 's $\pi_i$ (computed with the actual prices), and the industry's $\Pi + \pi_1 + \pi_2$ .

Formalization targets

Goal: Proposition 3

For every $\theta \ge 0$ , both games have a passive-belief equilibrium, and for every equilibrium $E^T$ of the tariff game and $E^W$ of the wholesale-price game,

\Pi(E^T) \le \Pi(E^W) \iff \theta \ge 2\sqrt2, \qquad \pi_i(E^T) < \pi_i(E^W)\ (i = 1,2), \qquad \Pi_{\mathrm{ind}}(E^T) \le \Pi_{\mathrm{ind}}(E^W) \iff \theta \ge \sqrt3 - 1,

together with the strict versions of the two equivalences ( $<$ iff $>$ ). At the thresholds the two profits coincide.

Milestones

Equation (2), p. 13: an accepting retailer with belief $\tilde p$ and contract $(K,w)$ charges $p = \frac{1+\theta\tilde p}{2+2\theta} + \frac w2$ and orders its conjectured demand.
Two-part tariffs, bilateral optimum, p. 14: against a retailer with a fixed belief, the manufacturer's best tariff is $\bigl(\frac{(1+\theta\tilde p)^2}{4(1+\theta)}, 0\bigr)$ .
Wholesale prices, bilateral optimum, p. 17: the best wholesale price is $\frac{1+\theta\tilde p}{2(1+\theta)}$ .
Proposition 1, p. 14: under unobservable two-part tariffs every equilibrium has $(K_i,w_i) = \bigl(\frac{1+\theta}{(2+\theta)^2}, 0\bigr)$ , $p_i = \frac1{2+\theta}$ , $\Pi = \frac{2(1+\theta)}{(2+\theta)^2}$ , $\pi_i = 0$ .
Proposition 2, p. 16: under unobservable wholesale prices every equilibrium has $w_i = \frac2{4+\theta}$ , $p_i = \frac3{4+\theta}$ , $\Pi = \frac{4(1+\theta)}{(4+\theta)^2}$ , $\pi_i = \frac{1+\theta}{(4+\theta)^2}$ .

Significance

Proposition 3 shows that the textbook ranking of supply-chain contracts depends on an observability assumption that is often false in practice. Under secret contracts the fixed fee loses its usual advantage: a manufacturer offering two-part tariffs cuts marginal wholesale prices to zero, retail competition becomes as fierce as possible, and all profit has to be collected through fees out of a shrinking pie. A wholesale price keeps marginal costs, and therefore retail prices, high. For $\theta \ge 2\sqrt2$ this "win-win" makes both the manufacturer and the retailers better off; as $\theta \to \infty$ the manufacturer's gain approaches 100 percent and the industry's 200 percent (p. 18).

The proposition is proved in the paper's Online Appendix. No machine-checked proof of it, or of the underlying equilibria, is known. A formalization would fix the solution concept precisely (quantification over off-path contracts, the tie-break at zero conjectured profit, the domain of contracts), establish uniqueness of the equilibria, which the page asserts only implicitly, and provide a reusable encoding of contract equilibria with passive beliefs for later missions on vertical contracting.

Difficulty

The closed forms of Propositions 1 and 2 make Proposition 3 a comparison of rational functions. The work is in the equilibrium layer. The retailers' strategies must be optimal at every contract, including contracts never offered, and the manufacturer's deviation is evaluated against those off-path responses while the rival's action is held fixed. Each retailer's belief is pinned to the rival's equilibrium price, so the equilibrium is a fixed point of a belief map composed with two optimization problems, the retailer's and the manufacturer's bilateral one. Uniqueness of the equilibrium is part of the claim, and the retailer's problem is non-smooth because of the $\min$ in sales and the accept/reject choice. At a zero marginal price the optimal order is not unique, so order quantities cannot be pinned down.

Formalization scope

Everything lives in the namespace ContractUnobs.Compare, with one definitions module, ContractUnobs.Compare.Model. Retailers are indexed by Fin 2 with rival 1 - i; all quantities are real. A contract is a structure with fields K and w; a retailer's action records accept : Bool, a price p and an order Q. IsPassiveEq θ cls E is the equilibrium condition above for a contract class cls (tariffClass or wholesaleClass); mfrProfit, retProfit and industryProfit are the realized profits.

Conventions committed to, each disclosed in the item statements:

wholesale prices are nonnegative in both classes ( $w < 0$ makes the retailer's order problem unbounded);
retail prices are nonnegative (the paper assumes prices induce nonnegative demand, p. 11), and sales are $\min(Q, \max(0, D))$ ;
a retailer whose best conjectured profit is exactly $0$ accepts (as on p. 13);
the manufacturer is paid for quantities ordered;
"in equilibrium" is read as a statement about every equilibrium, together with existence;
in Proposition 3, "higher when $\theta \ge 2\sqrt2$ " is read as an equivalence (weak at the threshold, strict beyond it), with the converse shown in the paper's figures.

Stating Proposition 3 with the closed-form values of Propositions 1 and 2 substituted for the equilibria is a different, nearly trivial theorem and is not the goal; the goal quantifies over equilibrium profiles, and its existence conjuncts exclude a vacuous reading.

The observable benchmark (Lemmas 1–3), the corollaries, and the extensions of §6 (buyback contracts, asymmetric retailers, downstream merger) are not part of this mission. Contributions welcome: proofs of the milestones, a general lemma on maximizing $(p-w)(A-Bp)$ over $p \ge 0$ , and a reusable treatment of passive-belief contract equilibria.

Selected references

X. Li and Q. Liu, Contract Unobservability and Downstream Competition, Manufacturing & Service Operations Management; SSRN preprint 3339702. https://ssrn.com/abstract=3339702 (published version: https://doi.org/10.1287/msom.2020.0905)
O. Hart and J. Tirole, Vertical Integration and Market Foreclosure, Brookings Papers on Economic Activity: Microeconomics, 1990, 205–286. https://doi.org/10.2307/2534783
D. P. O'Brien and G. Shaffer, Vertical Control with Bilateral Contracts, RAND Journal of Economics 23(3), 1992, 299–308. https://doi.org/10.2307/2555895
R. P. McAfee and M. Schwartz, Opportunism in Multilateral Vertical Contracting: Nondiscrimination, Exclusivity, and Uniformity, American Economic Review 84(1), 1994, 210–230. https://www.jstor.org/stable/2117980

7 thms2 active usersReviewed

Completed

Functional Analysis Operations Research Probability·Captain: mikedeng1

Combined Custom Hedging: Optimal Design, Noninsurable Exposure, and Operational Risk Management: A Unique Optimal Combined Custom Hedge Exists When the Maximal Correlation Is Below OneResearch Paper

Motivation

Firms carry risks they cannot insure directly. A farmer's revenue depends on local yield and on local price; an airline's cost depends on jet fuel at a specific airport; an energy retailer's margin depends on load and on weather. Exchange-traded derivatives are written on standardized indices, so the exposure that matters is only partly claimable. Guiotto and Roncoroni (Operations Research 2022) study the design of a combined custom hedge: one over-the-counter claim written on the claimable part $X$ of the firm's risk, plus a second claim written on a side index $I$ that is correlated with the unclaimable part. The question is when such a pair is well defined, that is, when the firm's mean–variance hedging problem has one and only one optimal pair of claims.

Single-claim custom hedging goes back to Chowdhry and Howe (1999) and Caldentey and Haugh (2006; 2009, Operations Research 57(1)), whose framework prices claims through a pricing kernel $dQ/dP$ known to the firm; that framework is adopted here. With two claims on two different random elements the optimal pair is coupled, and existence and uniqueness are no longer automatic.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying three random elements, valued in arbitrary measurable spaces: the claimable term $X$ , the nonclaimable term $Y$ and the side index $I$ . Write $\mathcal F_X=\sigma(X)$ and $\mathcal F_I=\sigma(I)$ . The firm's business position is $\pi=\pi(X,Y)$ for a Borel revenue function $\pi$ , assumed square-integrable.

A claim on $X$ is a random variable $H$ that is $\mathcal F_X$ -measurable and has finite variance; the set of such claims is $\mathcal H_X$ , and $\mathcal H_I$ is defined likewise. The centered subspace $\mathbb H_X\subseteq\mathcal H_X$ consists of claims with $\mathbb E[H]=0$ .

Claims are priced by a pricing kernel $dQ/dP$ , the density of an equivalent martingale measure $Q$ : it is positive almost surely, has mean one and is square-integrable, and $\mathbb E_Q[Z]=\mathbb E[Z\,dQ/dP]$ . The firm ranks positions by the mean–variance criterion

\mathcal U(Z)=\varrho\,\mathbb E[Z]-\tfrac a2\operatorname{Var}[Z],\qquad \varrho\ge 0,\ a>0 .

The value-centered design problem is

\max\Big\{\mathcal U\big(\pi+[H+G]\big)\ :\ H\in\mathcal H_X,\ G\in\mathcal H_I,\ \mathbb E_Q[H]=\mathbb E_Q[G]=0\Big\}.\qquad(4)

A maximizer $(H^*,G^*)$ is an optimal combined claim pair. The dependence between $X$ and $I$ is measured by the maximal correlation

r_{XI}=\sup\big\{\rho(\phi,\psi)\ :\ \phi\in\mathbb H_X,\ \psi\in\mathbb H_I\big\}\in[0,1],\qquad(6)

with $\rho$ the Pearson correlation. Finally $\mathcal K=\pi+(\varrho/a)\,dQ/dP$ is the optimal hedging kernel, $\Pi^X_0=-\mathbb E\big[\mathcal K-\mathbb E[\mathcal K\mid\mathcal F_I]\mid\mathcal F_X\big]$ , and $T[Z]=\mathbb E\big[\mathbb E[Z\mid\mathcal F_I]\mid\mathcal F_X\big]$ .

Formalization targets

Goal: Theorem 1 (p. 11)

If $r_{XI}<1$ , then

an optimal combined claim pair $(H^*,G^*)$ of (4) exists;
it is unique up to $P$ -null sets, and so is the hedge $H^*+G^*$ ;
the value-centered optimal claim $H^*_0=H^*-\mathbb E[H^*]$ solves

H^*_0=\Pi^X_0+\mathbb E\big[\mathbb E[H^*_0\mid\mathcal F_I]\mid\mathcal F_X\big].\qquad(7)

Milestones

Proposition 1 (p. 9): every optimal pair is $H^*=H^*_0-\mathbb E_Q[H^*_0]$ , $G^*=G^*_0-\mathbb E_Q[G^*_0]$ with $P$ -centered $(H^*_0,G^*_0)$ solving the first-order system (5).
(EC.25)–(EC.26) (p. ec24): a centered solution of (5) satisfies $H_0=\Pi_0+T[H_0]$ .
$T$ on $\mathbb H_X$ (p. ec24): $\mathbb E[T[Z]]=\mathbb E[Z]$ , $T(\mathbb H_X)\subseteq\mathbb H_X$ , and $\Pi_0\in\mathbb H_X$ .
Inner-product bound (p. ec25): $\langle\mathbb E[\phi\mid\mathcal F_I],\psi\rangle\le r_{XI}\|\phi\|_2\|\psi\|_2$ for $\phi\in\mathbb H_X$ , $\psi\in\mathbb H_I$ .
(EC.28) (p. ec25): $\|\mathbb E[\phi\mid\mathcal F_I]\|_2\le r_{XI}\|\phi\|_2$ .
$\|T\|\le r_{XI}$ (p. ec25) on $\mathbb H_X$ .
(EC.27) (p. ec25): if $r_{XI}<1$ , $H_0=\Pi_0+T[H_0]$ has a unique solution in $\mathbb H_X$ .

Significance

The result. Theorem 1 makes the combined hedge an object: without it the optimal pair may fail to exist or may be non-unique (the paper points to Appendix EC.1(F) for non-uniqueness), and the paper's later results, the design integral equation (Theorem 2) and the value of combining claims (Theorem 3 and Definitions 1–3), are stated for the optimal pair whose existence and uniqueness Theorem 1 provides. Equation (7) separates the optimal claim into a part determined by the kernel $\mathcal K$ alone and a cross-claim feedback through $I$ . The condition $r_{XI}<1$ is checkable: for jointly lognormal $(X,I)$ it reduces to $|\rho_{Z,W}|<1$ for the underlying normals (Example 4).

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof needs a Hilbert-space treatment of conditional expectations onto two σ-algebras, a formal maximal-correlation index, and an existence argument for the maximization problem itself, which the paper's proof leaves implicit (see below). The intermediate statements are general facts about pairs of σ-algebras with maximal correlation below one and are reusable outside hedging.

Difficulty

The optimal pair is coupled: the claim on $X$ depends on the conditional expectation of the claim on $I$ given $X$ and conversely, so neither can be computed first. When $X$ and $I$ share information, the two claim spaces overlap and the sum $\mathcal H_X+\mathcal H_I$ need not be closed in $L^2$ ; a maximizing sequence can then escape, and two different pairs can produce the same hedge. The condition $r_{XI}<1$ excludes this, and the work lies in turning it into a quantitative bound on the alternating conditional-expectation operator.

A second difficulty is a gap in the printed argument. The paper derives the first-order system (5) as a necessary condition and then proves that the resulting fixed-point equation has a unique solution. It does not show that the pair built from that solution is optimal for (4), so existence of a maximizer needs a separate argument that the first-order condition is also sufficient or that the maximum is attained. The goal is stated for maximizers of (4), so this step cannot be skipped.

Formalization scope

Everything lives in the namespace CustomHedge.Exist. A Market bundles $P$ , $X$ , $Y$ , $I$ , the revenue function, the kernel D $=dQ/dP$ , rho $=\varrho$ and a; Standing collects the assumptions above. Conventions:

Claims are random variables $\Omega\to\mathbb R$ , strongly measurable for $\sigma(X)$ (resp. $\sigma(I)$ ) and in $L^2(P)$ , not payoff functions $x\mapsto H(x)$ .
Optimality is maximization of U over all feasible pairs; uniqueness and the equations (5), (7), (EC.25), (EC.27) hold $P$ -almost surely.
$\mathbb E_Q$ centers the budget constraint; $\mathbb E=\mathbb E_P$ centers $H^*_0$ , $\mathbb H_X$ and the maximal correlation.
The paper allows $a\ge0$ ; the formalization requires $a>0$ , because $\mathcal K$ divides by $a$ and with $a=0$ problem (4) generally has no maximizer. $\varrho=0$ is allowed.
The maximal correlation is a real supremum over pairs with positive variances (where $\rho$ is defined), with $\sup\emptyset=0$ ; the set is bounded by one.
$\|Z\|_2=(\mathbb E[Z^2])^{1/2}$ ; conditional expectation is Mathlib's condExp.

A trivializing formalization is ruled out: the goal quantifies over maximizers of (4), not over solutions of the first-order system or of (EC.27), which are separate milestones. A sorry-free check confirms the standing assumptions and $r_{XI}<1$ hold together with a non-trivial $\sigma(X)$ .

Needed infrastructure: $L^2$ conditional expectation as an orthogonal projection, the identity $\mathbb E[\mathbb E[\phi\mid\mathcal G]\psi]=\mathbb E[\phi\psi]$ for $\mathcal G$ -measurable $\psi$ , Banach's fixed-point theorem on a closed subspace of $L^2$ , and concave maximization over a closed affine subspace. The maximal-correlation file is reusable beyond this mission. Proofs of individual milestones, and a proof of the goal by any route, are welcome.

Selected references

P. Guiotto and A. Roncoroni, Combined custom hedging: optimal design, noninsurable exposure, and operational risk management, Operations Research 70(3), 2022. https://doi.org/10.1287/opre.2021.2133 (cited from manuscript OPRE-2019-01-058.R3)
R. Caldentey and M. Haugh, Optimal control and hedging of operations in the presence of financial markets, Mathematics of Operations Research 31(2), 2006. https://doi.org/10.1287/moor.1060.0193
B. Chowdhry and J. T. B. Howe, Corporate risk management for multinational corporations: financial and operational hedging policies, European Finance Review 2, 229–246, 1999 (as cited in the paper; no link verified).
A. Rényi, On measures of dependence, Acta Mathematica Academiae Scientiarum Hungarica 10, 1959. https://doi.org/10.1007/BF02024507
B. Schweizer and E. F. Wolff, On nonparametric measures of dependence for random variables, Annals of Statistics 9(4), 1981. https://doi.org/10.1214/aos/1176345528

10 thms2 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

Order Now, Pickup in 30 Minutes: Managing Queues with Static Delivery Guarantees: The Perfectly-Clairvoyant Cost of Any N Customers Lower-Bounds the Optimal Long-Run Average CostResearch Paper

Motivation

Restaurants that take orders online promise each customer a pickup time when the order is placed. A static quote promises every customer the same lead time $\delta$ , the form in common use. Once the promise is fixed, the kitchen still decides when to start each order. Starting too early means the food waits and cools (an earliness cost). Starting too late breaks the promise (a tardiness cost). Farahani, Dawande and Janakiraman (SSRN 3557605; published in Operations Research, 2022, doi:10.1287/opre.2021.2203) model this as a single-server queue and propose simple threshold policies. To judge those policies against the unknown optimum they need lower bounds on the optimal long-run average cost, and their first such bound is the subject of this mission.

The bound uses a clairvoyant relaxation: a decision maker who knows every future arrival and service time can do no worse than one who does not. Relaxations of this kind are standard for finite-horizon stochastic dynamic programs, where the relaxed problem is deterministic and its expected value can be estimated by Monte Carlo simulation (Brown, Smith and Sun, 2010, doi:10.1287/opre.1090.0796). Brown and Haugh (2017, doi:10.1287/opre.2017.1631) extended them to discounted infinite-horizon problems. The queue here is an undiscounted infinite-horizon problem: the clairvoyant problem involves an infinitely long sample path, which cannot be simulated directly. Theorem 4 of the paper resolves this by showing that the clairvoyant cost per customer over any finite number of customers is already a valid lower bound.

Setting

A probability space carries inter-arrival times $T_1, T_2, \dots$ and service times $x_1, x_2, \dots$ . The $T_n$ are identically distributed with mean $1/\lambda$ , the $x_n$ are identically distributed with mean $1/\mu$ , the whole family is mutually independent, and $\lambda < \mu$ (the queue is stable). Customer $n \ge 1$ arrives at

t_n = T_1 + \cdots + T_n

and is due at $d_n = t_n + \delta$ , where $\delta \ge 0$ is the quote time. The arrival rate is $\lambda = 1/\mathbb E[T_1]$ .

A schedule assigns to each customer $n$ a service start time $y_n$ , which may depend on the sample path. It is FCFS-feasible if on every sample path

y_n \ge t_n, \qquad y_{n+1} \ge y_n + x_n \qquad (n \ge 1).

Customer $n$ departs at $D_n = y_n + x_n$ and pays $g(D_n - d_n)$ , where

g(\xi) = c_e(-\xi)^+ + c_d(\xi)^+, \qquad c_e, c_d \ge 0.

The long-run average cost of a schedule is (the paper's form (4))

C(y) = \lambda \limsup_{N \to \infty} \mathbb E\Big[\frac1N \sum_{n=1}^N g(y_n + x_n - d_n)\Big].

The perfectly-clairvoyant cost of customers $i, \dots, j$ on a sample path $\omega$ (program (12)) is

\gamma_{i:j}(\omega) = \inf_y \sum_{n=i}^j g(y_n + x_n - d_n) \quad \text{s.t.} \quad y_n \ge t_n \ (i \le n \le j), \quad y_{n+1} \ge y_n + x_n \ (i \le n < j).

In Lean these are StaticQuote.Clairvoyant.Model with Standing, rate, arrival, due, g, IsFCFSSchedule, cost, IsSchedule and gamma.

Formalization targets

Goal: Theorem 4 (p. 18)

For every FCFS-feasible schedule $y$ and every $N \ge 1$ ,

C(y) \ \ge\ \lambda\, \mathbb E\Big[\frac{\gamma_{1:N}(\omega)}{N}\Big].

The paper writes the left side as $C^{\pi^*}$ , the optimal cost. The statement here holds for every schedule, so it covers the optimum whenever one exists.

Milestones (in the order of the printed proof, pp. 18–19)

Sample-path bound: $\gamma_{1:M}(\omega)/M \le \sum_{n=1}^M g(D_n - d_n)/M$ on every path.
(14): $\limsup_M \lambda\, \mathbb E[\gamma_{1:M}/M] \le C(y)$ .
Superadditivity: $\gamma_{1:2N}(\omega) \ge \gamma_{1:N}(\omega) + \gamma_{N+1:2N}(\omega)$ .
Block stationarity: $\mathbb E[\gamma_{1:N}] = \mathbb E[\gamma_{N+1:2N}]$ .
Doubling: $\mathbb E[\gamma_{1:2N}] \ge 2\,\mathbb E[\gamma_{1:N}]$ .
Dyadic bound: $k \mapsto \mathbb E[\gamma_{1:2^kN}/2^kN]$ is non-decreasing and $\mathbb E[\gamma_{1:N}/N] \le \limsup_k \mathbb E[\gamma_{1:2^kN}/2^kN]$ .
(15): $\mathbb E[\gamma_{1:N}/N] \le \limsup_M \mathbb E[\gamma_{1:M}/M]$ .

Significance

The result. Theorem 4 turns an infinite-horizon lower bound into a finite computation: for any $N$ , the deterministic clairvoyant problem over $N$ customers can be solved on simulated sample paths, and the sample mean, scaled by $\lambda$ , estimates a lower bound on the optimal long-run cost. The paper uses this bound, with its refinements (Theorems 5 and 6), to certify the numerical quality of its threshold policies (§7). Without it, the only available benchmark is the asymptotic clairvoyant cost, which cannot be computed.

Formalizing it. The paper proves the theorem with an informal argument. No machine-checked proof of this bound, or of the sample-path GI/G/1 objects it needs, is known to exist. The mission produces a sample-path model of a single-server queue with due dates, a clairvoyant value defined as an extended-real infimum, and the measure-theoretic step that the clairvoyant cost of a block of customers has the same expectation as that of the first block.

Difficulty

Most steps are monotonicity of integrals and of $\limsup$ . The substantive step is block stationarity (milestone 4). $\gamma_{N+1:2N}$ and $\gamma_{1:N}$ are not functions of the same random variables, and $\gamma_{N+1:2N}$ depends on the absolute arrival times $t_{N+1}, \dots, t_{2N}$ , which carry the whole history $T_1, \dots, T_N$ . The equality of expectations needs the clairvoyant value to be expressed as a function of relative arrival times and service times only. It also needs that function to be measurable (it is an infimum over uncountably many schedules) and the joint law of a block of an i.i.d. family to be invariant under shifting the block. The doubling argument then has to pass from horizons $2^kN$ to all horizons $M$ , which in the extended reals needs no integrability.

Formalization scope

Source. The statements follow the SSRN author version of 2021-08-05 (abstract 3557605), whose page and equation numbers are cited throughout; the published article's numbering is not used.
Indices start at $1$ : $t_n = T_1 + \cdots + T_n$ ; the coordinates $T_0, x_0$ are unused and carry no hypothesis. $N \ge 1$ in the goal, in the dyadic bound and in (15) (the paper's $\mathbb N$ starts at $1$ ; the ratios are $0/0$ at $N = 0$ ).
Sample paths. The outcome $\omega$ is the full sample path of inter-arrival and service times; the page calls it "a sample path of inter-arrival times" on p. 18 and "of inter-arrival and service times" on p. 19.
Policy class. The paper's admissible, FCFS and Loynes stable policy classes are not modelled. The Loynes class asks for $L^1$ convergence of the waiting times $W^\pi_n$ . For a nondegenerate GI/G/1 queue these converge only in law, so the class may be empty, and an infimum over it would be vacuous. Every statement instead quantifies over all schedules that are FCFS-feasible on every sample path. That class contains every policy the paper considers, so the statements imply the paper's. No measurability or adaptedness of $y$ is required: the bound holds without it.
Cost. $C(y)$ is defined by the per-customer form (4), not by the calendar-time form (1); the paper passes from (1) to (4) by citing Whitt (1991), and the proof of Theorem 4 uses (4) only.
Extended reals. $\gamma$ is an infimum in $[0, \infty]$ (the page writes $\min$ , which is attained but not proved to be). Costs, expectations (lower Lebesgue integrals) and $\limsup$ s are in $[0, \infty]$ . Each cost term is $\max(g, 0)$ , which is exact because $g \ge 0$ .
Standing assumptions. The paper leaves some conditions implicit; they are made explicit: durations are nonnegative almost surely, $\delta, c_e, c_d \ge 0$ , and "mean $1/\lambda$ , mean $1/\mu$ " means $0 < \mathbb E[T_1] < \infty$ and $0 < \mathbb E[x_1] < \infty$ . Stability $\lambda < \mu$ ( $\mathbb E[x_1] < \mathbb E[T_1]$ ) is kept as the paper's standing assumption although Theorem 4 does not use it. A one-point model ( $T \equiv 1$ , $x \equiv 1/2$ , $\delta = c_e = c_d = 1$ ) satisfies all of them and has finite $\gamma_{1:N}$ .
Ruled out. A real-valued $\gamma$ , cost, expectation or $\limsup$ (junk value $0$ on unbounded or non-integrable input); a policy class that may be empty; dropping the i.i.d. or independence hypotheses (milestone 4 and the goal fail without them); $N = 0$ ; and $\lambda$ as a free parameter (it is $1/\mathbb E[T_1]$ ).
Infrastructure. A complete development needs measurability of the clairvoyant value, invariance of block laws for i.i.d. families, and the comparison of a $\limsup$ along a subsequence with the full $\limsup$ in $[0, \infty]$ . The block-law invariance and the sample-path queue model can be reused in other missions. Proofs of any milestone, and lemmas towards milestone 4, are welcome.

Selected references

M. H. Farahani, M. Dawande, G. Janakiraman, Order Now, Pickup in 30 Minutes: Managing Queues with Static Delivery Guarantees, SSRN 3557605, version of 2021-08-05; published in Operations Research, 2022. https://ssrn.com/abstract=3557605, https://doi.org/10.1287/opre.2021.2203
D. B. Brown, J. E. Smith, P. Sun, Information relaxations and duality in stochastic dynamic programs, Operations Research 58(4), 785–801, 2010. https://doi.org/10.1287/opre.1090.0796
D. B. Brown, M. B. Haugh, Information relaxation bounds for infinite horizon Markov decision processes, Operations Research 65(5), 1355–1379, 2017. https://doi.org/10.1287/opre.2017.1631
R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036094
W. Whitt, A review of L = λW and extensions, Queueing Systems 9(3), 235–268, 1991. https://doi.org/10.1007/BF01158466

9 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Customization and Returns: Allowing Returns of Customized Products Can Increase Profits and Reduce Total ReturnsResearch Paper

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.

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

A Simple and Approximately Optimal Mechanism for a Buyer with Complements: With Complementarity d, the Better of Bundling and Selling Separately Earns a 1/(4d+16) Fraction of Optimal RevenueResearch Paper

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.

9 thms2 active usersReviewed

Completed

Machine Learning Operations Research Probability·Captain: mikedeng1

Interpretable Optimal Stopping: For Trees of Bounded Depth, the Optimal SAA Value of Tree Policies Converges Almost Surely to the Optimal Tree-Policy ValueResearch Paper

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:

Assumption 1: $\mathcal X$ is totally bounded and $\|\mathbf x-\mathbf y\|_\infty\le1$ on $\mathcal X$ .
Assumption 2: $0\le g(t,\mathbf x)\le G$ for all $t$ and $\mathbf x\in\mathcal X$ .
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

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$ .
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}|)$ .
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\}$ .
Fixed-policy strong law (EC.1.1, p. ec1): for one tree policy, $\hat J^\pi\to J^\pi$ almost surely.
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$ .
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

9 thms2 active usersReviewed

Completed

Economics Mechanism Design Operations Research·Captain: mikedeng1

An Axiomatization of the Proportional Rule in Financial Networks: The Proportional Rule Is the Unique Bankruptcy Rule Satisfying the Five Basic Axioms and Invariance to MitosisResearch Paper

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

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

11 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

On the Role of Teletriage in Healthcare Demand Management: When Every Patient Calls, Teletriage Reduces ED Usage iff Overtriage Is Below β⁰ and Double-Dipping iff Undertriage Is Below α⁰Research Paper

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

The no-teletriage threshold at $b_0$ (§4.1).
Proposition 1, informative case: $b_{PS}<b<b_{PC}$ for $0<b<1$ , $\alpha+\beta<1$ .
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.
Proposition 2.
The closed forms of $\pi^{ED},\pi^{DD}$ and $\tilde\pi^{ED},\tilde\pi^{DD}$ (display on p. 11).
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

12 thms2 active usersReviewed