Missions · Prove2Me

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Discrete Dividend Payments in Continuous Time: The Value Function Is the Unique Fixed Point of the One-Period Dividend-and-Issuance OperatorResearch Paper

Why periodic dividends matter

A firm can return cash to shareholders by paying dividends, but a payment reduces the reserves available to survive future losses. If cash can be distributed only at scheduled dates while equity can be raised between those dates, the firm must coordinate a discrete dividend decision with a continuous-time financing decision. Keppo, Reppen and Soner study this combination for a firm whose cash flow is a Brownian motion with drift. Their preprint identifies the firm's optimal value through an operator that first solves the financing problem between dividend dates and then chooses the next dividend. The mission concerns that characterization, Theorem 3.4, together with the regularity results on which it depends.

The cash reserve model

Let $x\ge0$ be the initial reserve and let $C_t=\mu t+\sigma W_t$ , where $W$ is a one-dimensional Brownian motion, $\mu>0$ is profitability, and $\sigma>0$ is volatility. Dividends of amounts $\ell_n\ge0$ may be paid at dates $nT$ , with $T>0$ . Equity issues have sizes $\zeta_k\ge0$ and occur at stopping times $\tau_k$ ; the issue times are locally finite. A positive issue costs

c(\zeta)=\lambda_f+(1+\lambda_p)\zeta,\qquad \lambda_f,\lambda_p>0,

while no issue costs zero. The cash reserve after actions at time $t$ is $X_t=x+C_t-L_t+I_t$ . The ruin time $\theta$ is the first strictly positive time that $X_t<0$ . A dividend cannot exceed the reserve immediately before its date, and no action is taken after ruin. These conditions define the admissible controls $\mathcal A_x$ .

The firm's value function is the supremum, over admissible controls, of expected discounted dividends less expected discounted issue costs:

V(x)=\sup_{(L,I)\in\mathcal A_x}\mathbb E_x\left[\sum_{n\ge0}e^{-\rho nT}\ell_n-\sum_k e^{-\rho\tau_k}c(\zeta_k)\right],\qquad \rho>0.

The first sum includes a possible dividend at time zero, following the displayed objective in §3.1 of the preprint. An issue at time $T$ belongs to the next period. Thus the one-period financing operator $\mathcal L\phi$ charges issues on $[0,T)$ and evaluates its continuation reward $\phi$ at the reserve immediately before $T$ . The dividend operator is

\mathcal D\phi(x)=\sup_{0\le\ell\le x}\{\phi(x-\ell)+\ell\},\qquad \mathcal T=\mathcal D\circ\mathcal L.

The continuation class $\mathcal C_A$ consists of the continuous, nondecreasing functions $\phi:[0,\infty)\to[0,\infty)$ that satisfy the issuance boundary condition of Definition 3.2, are bounded above by $x+A$ , and have $\phi(x)-x$ nondecreasing and bounded in absolute value by $A$ . Its larger class $\widehat{\mathcal C}_A$ omits the last condition. The intervention value in the boundary condition is $\mathcal I\phi(x)=\sup_{\zeta>0}\{\phi(x+\zeta)-c(\zeta)\}$ .

Formalization targets

The first target is the mapping statement in Theorem 3.3: $\mathcal D:\widehat{\mathcal C}_A\to\mathcal C_A$ for $A\ge0$ . With

A^*=\frac{\mu T}{e^{\rho T}-1},

the next targets are the one-period bound $0\le\mathcal L\phi(x)\le e^{-\rho T}x+A$ for $A\ge A^*$ , the classical one-period characterization of Theorem 3.6, and the remaining mapping and contraction assertions of Theorem 3.3. In particular, $\mathcal T$ contracts the uniform distance between functions in $\mathcal C_A$ by the factor $e^{-\rho T}$ .

The goal is Theorem 3.4:

V\in\mathcal C_{A^*},\qquad \mathcal T V=V,\qquad \phi\in\mathcal C_{A^*}\ \text{and}\ \mathcal T\phi=\phi\ \Longrightarrow\ \phi=V.

This identifies the fixed point with the value defined from admissible controls. It also asserts that the value is finite at every nonnegative initial reserve.

What the characterization gives

Theorem 3.4 turns an infinite-horizon control problem into repeated one-period calculations. Since Theorem 3.3 makes $\mathcal T$ a strict contraction on $\mathcal C_{A^*}$ , iterating it determines the value in that class. The source connects this characterization to a numerical method when the one-period financing problem can be computed efficiently. A proof in Lean would also provide reusable statements about locally finite impulse controls, periodic actions, ruin, and discounted extended-real objectives. The preprint proves the mathematical results; this mission records their statements as open Lean theorems for machine-checked proofs.

Where the difficulty lies

The dividend operator is an elementary supremum over one payment, but the financing operator ranges over adapted impulses before ruin. Its regularity is central: the paper invokes Theorem 3.6 to show that $\mathcal L\phi$ is continuous and satisfies the issuance boundary condition. That theorem characterizes the arbitrary-maturity issuance value as the unique classical solution of a parabolic equation with a nonlocal boundary condition. The fixed-point conclusion alone would leave an additional gap: Theorem 3.4 must identify that fixed point with the original control supremum, including the limit over dividend periods and its terminal reward.

Formalization scope

Lean represents nonnegative reserves by $\mathbb R_{\ge0}$ and the discount, costs and function values by real numbers. Control values and one-period rewards are suprema in extended real numbers, with dividends and issue costs integrated separately as nonnegative quantities. The $\mathcal L$ bound proves the finiteness needed before converting to real values. An expression with both expected dividends and expected costs infinite takes the extended-real value $-\infty$ and cannot improve a supremum with a finite admissible alternative.

The paper's cumulative processes are represented by nonnegative dividend amounts and a locally finite impulse sequence of nonnegative issues. This makes explicit that equity cannot be supplied by an uncharged continuous component. Simultaneous impulses are allowed; merging them cannot increase the cost. The Brownian cash flow uses the published AtaBarjesteh23.Workload.IsDriftBM definition. The model requires a probability measure, adaptation to a filtration, and positive $\rho,\mu,\sigma,\lambda_f,\lambda_p,T$ . The filtration is right-continuous and its initial σ-algebra contains all subsets of ambient null measurable sets, as required by the usual conditions. A dividend at time zero follows the objective's sum. In $\mathcal L$ , the continuation value uses $X_{T-}$ , resolving the free-issue-at- $T$ ambiguity in the printed formula. The arbitrary-maturity problem retains its separately printed non-strict survival indicator.

The value $V$ is defined solely from admissible controls, never from $\mathcal T$ or its iterates. Theorem 3.6 uses time to maturity and states smoothness only on the interior rectangle; uniqueness is restricted to the closed nonnegative time-state rectangle. Reusable work includes stopping-time measurability, impulse summation and parabolic regularity. Contributions proving the goal or the four listed milestones are within scope; §4's random-profitability model and §3.4's numerical experiments are outside this mission.

Selected references

J. Keppo, A. M. Reppen and H. M. Soner, Discrete Dividend Payments in Continuous Time, Mathematics of Operations Research, 2021; preprint arXiv:1805.05077v2, 2019. https://arxiv.org/abs/1805.05077v2

9 thms2 active usersReviewed

Completed

Machine Learning Operations Research Optimization·Captain: mikedeng1

Risk Guarantees for End-to-End Prediction and Optimization Processes: The Excess Squared-Loss Risk Bounds the Squared Excess Optimality-Gap Risk, Scaled by the Squared Diameter of the Feasible SetResearch Paper

Motivation

Many operational decisions are optimization problems whose cost vector is unknown when the decision is made but can be predicted from observed features: shortest paths under predicted travel times, portfolios under predicted returns, production plans under predicted prices. The common practice, predict-then-optimize, first fits a regression model $g$ mapping features $w$ to a cost estimate $g(w)$ and then solves the optimization problem with $g(w)$ in place of the true cost $c$ . What the decision maker cares about is not the prediction error but the optimality gap of the resulting decision under the true cost. Elmachtoub and Grigas (arXiv:1710.08005, Management Science 2022) introduced the SPO+ surrogate to train predictors against that gap directly, and established its Fisher consistency.

Ho-Nguyen and Kılınç-Karzan (arXiv:2012.15046, Management Science 2022) ask which surrogate losses give quantitative guarantees: when does a small excess surrogate risk force a small excess optimality-gap risk, uniformly over a class of data distributions? Their answer adapts the calibration theory of Steinwart (Constructive Approximation 26, 2007) to the end-to-end setting, and its most striking consequence concerns the ordinary squared loss.

Setting

Let $X \subset \mathbb R^m$ be a non-empty convex compact set and $f$ a convex function, continuous on $X$ . For a cost vector $c$ the decision maker solves

\min_{x \in X}\ \{ f(x) + c^\top x \}.

An argmin selection is a fixed map $x^* : \mathbb R^m \to X$ with $x^*(d)$ a minimizer of $f(x) + d^\top x$ over $X$ for every $d$ . Using a prediction $d$ instead of the true cost $c$ incurs the true loss

L(d,c) = f(x^*(d)) + c^\top x^*(d) - \min_{x \in X}\{f(x) + c^\top x\} \ \ge 0 .

Features and costs form a random pair $(w,c) \in W \times \mathbb R^m$ with joint law $\mathbb P$ . For a loss $\ell$ and a measurable predictor $g : W \to \mathbb R^m$ , the risk is $R_\ell(g,\mathbb P) = \mathbb E[\ell(g(w),c)]$ and the Bayes risk is $R_\ell(\mathbb P) = \inf_g R_\ell(g,\mathbb P)$ over measurable $g$ ; for $\ell = L$ these are written $R(g,\mathbb P)$ and $R(\mathbb P)$ . The squared loss is $\ell_{LS}(d,c) = \|d - c\|_2^2$ .

Given a set $C \subset \mathbb R^m$ , the class $\mathcal P$ consists of the laws for which every conditional law $\mathbb P[\cdot \mid w]$ is concentrated on $C$ , is square integrable, and has mean $\mathbb E[c \mid w] \in \mathrm{Conv}(C)$ . Assumption 2 asks that $C$ be bounded. The constants are $B_X = \max_{x,x' \in X}\|x - x'\|_2$ , $B_f = \max_{x,x' \in X}\{f(x) - f(x')\}$ and $B_C = \max_{c \in C}\|c\|_2$ .

A loss $\ell$ is $\mathcal P$ -uniformly calibrated if for every $\epsilon > 0$ there is $\delta > 0$ such that, for every law in $\mathcal P$ , every $w$ and every $d$ , a conditional excess $\ell$ -risk $\mathbb E[\ell(d,c)\mid w] - \inf_{d'}\mathbb E[\ell(d',c)\mid w]$ below $\delta$ forces a conditional excess true risk below $\epsilon$ . The largest such $\delta$ is the calibration function $\delta_\ell(\epsilon;\mathcal P)$ .

Formalization targets

Goal: Corollary 3 (p. 22)

For every law $\mathbb P \in \mathcal P$ with $\mathbb E\|c\|_2^2 < \infty$ and every measurable predictor $g$ ,

\big(R(g,\mathbb P) - R(\mathbb P)\big)^2 \ \le\ B_X^2\,\big(R_{\ell_{LS}}(g,\mathbb P) - R_{\ell_{LS}}(\mathbb P)\big).

Milestones

Lemma 2 (p. 10): $g^*(w) = \mathbb E[c \mid w]$ attains $R(\mathbb P)$ , and $R(\mathbb P) = \mathbb E[\min_{d'}\mathbb E[L(d',c)\mid w]]$ .
Remark 5 (p. 19): the conditional excess true risk equals $f(x^*(d)) - f(x^*(\bar c)) + \bar c^\top(x^*(d) - x^*(\bar c))$ with $\bar c = \mathbb E[c\mid w]$ , and is at most $B_f + B_C B_X$ .
Lemma 3 (p. 20): uniform calibration holds iff $\delta_\ell(\epsilon;\mathcal P) > 0$ for all $\epsilon > 0$ .
Lemma 4 (p. 21): the alternative form (14) of $\delta_\ell$ .
Lemma 5 (p. 21): $\|d - \bar c\|_2 \ge \max\{0, f(x) - f(x') + \bar c^\top(x - x')\}/\|x - x'\|_2$ when $x^*(d) = x \ne x' = x^*(\bar c)$ .
Lemma 6 (p. 22): $\delta_{\ell_{LS}}(\epsilon;\mathcal P)$ is the purely geometric infimum of $\|d - \bar c\|_2^2$ .
Theorem 4 (p. 22): $\ell_{LS}$ is $\mathcal P$ -uniformly calibrated, with $\delta_{\ell_{LS}}(\epsilon;\mathcal P) \ge \epsilon^2/B_X^2 > 0$ .
Theorem 3 (p. 20): for any uniformly calibrated $\ell$ , $\delta^{**}_\ell(R(g,\mathbb P) - R(\mathbb P)) \le R_\ell(g,\mathbb P) - R_\ell(\mathbb P)$ , with $\delta^{**}_\ell$ the convex minorant of $\delta_\ell$ on $(0, B_f + B_C B_X]$ .

The goal is stated with the constant $B_X^2$ and no other problem data: it is independent of $f$ , of $C$ beyond boundedness, and of the law of the data.

Significance

The corollary says that a predictor trained by ordinary least squares, without any information about $f$ or $X$ , has excess optimality-gap risk at most $B_X\sqrt{R_{\ell_{LS}}(g,\mathbb P) - R_{\ell_{LS}}(\mathbb P)}$ . Since the excess squared-loss risk separates over coordinates, coordinate-wise regression bounds suffice for end-to-end guarantees (Remark 7). Any learning-theoretic rate for least-squares regression therefore transfers to a rate for the decision problem, up to a square root. Theorem 3 gives the same transfer for any uniformly calibrated surrogate, and is the template for the paper's further results on separable symmetric losses.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires a measure-theoretic treatment of conditional risks through kernels, a Lean version of Steinwart's convexified calibration inequality in this setting, and the geometric bound of Lemma 5. Each milestone is a self-contained target.

Difficulty

The true loss $L(d,c)$ is neither convex nor continuous in $d$ (Lemma 1): the decision $x^*(d)$ jumps between faces of $X$ . A pointwise comparison between $\|d - c\|_2^2$ and $L(d,c)$ fails, since a prediction close to $c$ can still select a far-away vertex when $c$ lies near a tie. The comparison only holds after conditioning on $w$ and averaging over $c$ , and it must hold uniformly over all conditional laws in $\mathcal P$ , not for a fixed distribution. The step from conditional comparisons to the integrated risks is where the uniform bound $B_f + B_C B_X$ on the conditional excess true risk and the convention at $\epsilon = 0$ in $\delta^{**}$ matter; Bayes risks are infima over predictors, so this step also needs the conditional minimizers to assemble into a measurable predictor.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m). The standing setting (Standing X f) bundles convexity, compactness and non-emptiness of $X$ , convexity of $f$ on $X$ and continuity of $f$ on $X$ ; IsArgminSelection X f xstar is the selection property. A joint law is μ ⊗ₘ κ, with μ the law of $w$ and κ a Markov kernel giving $\mathbb P[\cdot \mid w]$ ; $\mathbb E[c \mid w]$ is the Bochner integral against κ w. Risks are $[0,\infty]$ -valued lower integrals of ENNReal.ofReal of the non-negative losses, Bayes risks are infima over measurable predictors, and excess risks are truncated differences. The class $\mathcal P$ is lsClass C, a set of conditional laws concentrated on $C`; the calibration function `deltaL` and `UniformlyCalibrated` range over such a set, which matches the page's "for all$ \mathbb P \in \mathcal P $,$ w \in W $" whenever$ W $is non-empty.$ B_X$ is Metric.diam X.

Added or pinned conventions:

measurability of xstar (the paper uses Lebesgue measurability, Lemma EC.4) and of predictors;
$\mathbb E\|c\|_2^2 < \infty$ in the goal, explicit though implied by support on bounded $C$ , to make the extended-real Bayes-risk subtraction finite;
$1/B_X^2$ multiplied out in the goal; Theorem 4 carries $B_X>0$ for its printed quotient;
the conclusion of (12) read conditionally on $w$ ;
$\delta^{**}$ constrained by $h'(0) \le 0$ (the convention $\delta_\ell(0) = 0$ of p. 19);
in Theorem 3, the identity $R_\ell(\mathbb P) = \mathbb E[\inf_{d'}\mathbb E[\ell(d',c)\mid w]]$ and finiteness of $R_\ell(\mathbb P)$ .

The Bayes risks are genuine infima over measurable predictors and the conditional excess risks are defined generically. Neither is defined by the closed form that Lemma 2 or Lemma 6 establishes, so neither lemma holds by definition.

Needed infrastructure: lower integrals against μ ⊗ₘ κ and their disintegration, measurability of the conditional mean and of the optimal value $c \mapsto \min_x\{f(x) + c^\top x\}$ , Jensen's inequality for real convex functions on a bounded interval, and the distance from a point to a half-space. The bias–variance decomposition for laws on $\mathbb R^m$ and the half-space distance formula are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal that bypass Theorem 3.

Selected references

N. Ho-Nguyen and F. Kılınç-Karzan, Risk guarantees for end-to-end prediction and optimization processes, Management Science 68(12), 2022. arXiv:2012.15046v1. https://arxiv.org/abs/2012.15046
A. N. Elmachtoub and P. Grigas, Smart "predict, then optimize", Management Science 68(1), 2022. https://arxiv.org/abs/1710.08005
I. Steinwart, How to compare different loss functions and their risks, Constructive Approximation 26, 2007. https://doi.org/10.1007/s00365-006-0662-3

10 thms2 active usersReviewed

Algebraic Geometry Convex Optimization Operations Research+1·Captain: mikedeng1

On Computing the Nonlinearity Interval in Parametric Semidefinite Optimization: The Set of Transition Points of the Optimal Partition Is FiniteResearch Paper

Motivation

Sensitivity analysis asks how the solution of an optimization problem changes when its data move. For linear optimization the answer has been known since the 1990s: as the objective is perturbed along a fixed direction, the optimal partition (which variables can be positive at an optimum and which slacks can) stays constant on open intervals and changes only at finitely many breakpoints, and the optimal value is piecewise linear with breakpoints exactly there (Adler and Monteiro, Algorithmica 8, 1992; Jansen, Roos and Terlaky, 1993). Semidefinite optimization (SDO) is used throughout control, combinatorial relaxations and polynomial optimization, and its parametric behaviour is less regular. The optimal partition can stay constant while the optimal sets move (a nonlinearity interval), and the optimal value need not be piecewise linear.

Mohammad-Nezhad and Terlaky (Optimization 69, 2020) defined invariancy intervals, nonlinearity intervals and transition points for parametric SDO. Hauenstein, Mohammad-Nezhad, Tang and Terlaky (arXiv:1908.10499v3; Mathematics of Operations Research, 2022) prove that there are only finitely many transition points (Theorem 1, p. 8) and then compute nonlinearity intervals with numerical algebraic geometry. Finiteness is what makes a computational description possible: without it, the interior of the domain need not decompose into finitely many intervals of each kind.

Timeline:

1992–1993: Adler and Monteiro, and Jansen, Roos and Terlaky, start the optimal partition approach to parametric linear optimization.
1999: Goldfarb and Scheinberg extend the optimal partition approach to parametric SDO (Applied Numerical Mathematics 29).
2020: Mohammad-Nezhad and Terlaky introduce the optimal partition approach to parametric SDO (Definitions 3–5 of the present paper are taken from there).
2019–2022: Hauenstein, Mohammad-Nezhad, Tang and Terlaky prove that the transition points are finite (Theorem 1) and give the nonlinearity-interval algorithm.

Setting

Let $\mathbb S^n$ be the real symmetric $n\times n$ matrices with $\langle M,X\rangle=\operatorname{tr}(MX)$ . Data: $A^1,\dots,A^m,C,\bar C\in\mathbb S^n$ and $b\in\mathbb R^m$ . For a real parameter $\epsilon$ consider

(\mathrm P_\epsilon)\ \inf_X\{\langle C+\epsilon\bar C,X\rangle:\ \langle A^i,X\rangle=b_i,\ X\succeq0\},\qquad (\mathrm D_\epsilon)\ \sup_{(y,S)}\Big\{b^Ty:\ \textstyle\sum_i y_iA^i+S=C+\epsilon\bar C,\ S\succeq0\Big\}.

The primal feasible set $\mathcal P$ does not depend on $\epsilon$ ; the dual one is $\mathcal D(\epsilon)$ . The optimal value function $v(\epsilon)\in\mathbb R\cup\{\pm\infty\}$ is the infimum of $(\mathrm P_\epsilon)$ , its domain is $\mathcal E=\{\epsilon:\ v(\epsilon)>-\infty\}$ , and the optimal sets are $\mathcal P^*(\epsilon)=\{X\in\mathcal P:\langle C+\epsilon\bar C,X\rangle=v(\epsilon)\}$ and $\mathcal D^*(\epsilon)=\{(y,S)\in\mathcal D(\epsilon):b^Ty=v(\epsilon)\}$ .

Standing assumptions (p. 2): Assumption 1, the $A^i$ are linearly independent; Assumption 2, there are $X^\circ\in\mathcal P$ , $(y^\circ,S^\circ)\in\mathcal D(0)$ with $X^\circ,S^\circ\succ0$ .

For $\epsilon\in\operatorname{int}(\mathcal E)$ , a maximally complementary optimal solution $(X^*(\epsilon),y^*(\epsilon),S^*(\epsilon))$ has $X^*(\epsilon)\in\operatorname{ri}\mathcal P^*(\epsilon)$ and $(y^*(\epsilon),S^*(\epsilon))\in\operatorname{ri}\mathcal D^*(\epsilon)$ (Definition 1). A point $\bar\epsilon\in\operatorname{int}(\mathcal E)$ is a transition point if every interval $(\bar\epsilon-\delta,\bar\epsilon+\delta)\cap\operatorname{int}(\mathcal E)$ contains an $\epsilon$ with $\operatorname{rank}X^*(\epsilon)\ne\operatorname{rank}X^*(\bar\epsilon)$ or $\operatorname{rank}S^*(\epsilon)\ne\operatorname{rank}S^*(\bar\epsilon)$ (Definition 5).

Formalization targets

Goal: Theorem 1 (p. 8)

\{\bar\epsilon\in\mathbb R:\ \bar\epsilon\ \text{is a transition point}\}\ \text{is finite.}

The statement names no bound on the number of transition points; it asserts finiteness only.

Milestones, in the order of the paper's argument

Remark 1 (p. 2): strictly feasible primal and dual solutions exist at every $\epsilon\in\operatorname{int}(\mathcal E)$ .
p. 2: $\mathcal E$ is an interval with at least two points; $v$ is finite and concave on $\mathcal E$ and continuous on $\operatorname{int}(\mathcal E)$ .
p. 2: for $\epsilon\in\operatorname{int}(\mathcal E)$ , $\mathcal P^*(\epsilon)$ and $\mathcal D^*(\epsilon)$ are nonempty and compact (strong duality).
(1), p. 2: on $\operatorname{int}(\mathcal E)$ , a primal–dual triple is optimal iff it is feasible and $XS=0$ .
Appendix, p. 22: the ranks at relative-interior optimal points are maximal on the optimal sets.
(19), p. 22: $\operatorname{int}(\mathcal E)=\bigcup_{\theta+\sigma\le n}\mathcal S_{(\theta,\sigma)}$ , where $\mathcal S_{(\theta,\sigma)}$ is the set of $\epsilon\in\operatorname{int}(\mathcal E)$ at which some $(X,y,S)\in\operatorname{ri}(\mathcal P^*(\epsilon)\times\mathcal D^*(\epsilon))$ has ranks $(\theta,\sigma)$ .
p. 22: $\bar\epsilon$ is a transition point iff $\bar\epsilon\in\operatorname{bd}(\mathcal S_{(\theta,\sigma)})\cap\operatorname{int}(\mathcal E)$ for some $\theta+\sigma\le n$ .
p. 23: every $\mathcal S_{(\theta,\sigma)}$ is a semi-algebraic subset of $\mathbb R$ .
[Basu–Pollack–Roy, Theorem 5.22], cited p. 22: a semi-algebraic subset of $\mathbb R$ has finitely many boundary points.

Significance

The result. Theorem 1 implies that $\operatorname{int}(\mathcal E)$ is a finite union of invariancy intervals, nonlinearity intervals and transition points (p. 8). This is the structural fact behind the paper's algorithm, which follows the optimal solution along a nonlinearity interval and detects its end points, and it extends to SDO the finite-breakpoint picture of parametric linear optimization. Without finiteness, a sensitivity report would have no finite description.

Formalizing it. The theorem is proved in the paper; nothing here is open. It has no machine-checked proof that we know of. A complete development would bring parametric conic duality into Lean (the interior point condition moving along a direction, strong duality with attainment, compactness of optimal sets), and it would connect convex analysis to semi-algebraic geometry: relative interiors, ranks of positive semidefinite matrices, and the one-dimensional case of Tarski–Seidenberg. Each of these is useful beyond this paper.

Difficulty

The obvious argument says that ranks are integers between $0$ and $n$ , so they can change only finitely often. That is false for arbitrary integer-valued functions on an interval: a rank pair could alternate on a sequence accumulating at a point, producing infinitely many transition points. Finiteness needs a structural reason why each level set $\mathcal S_{(\theta,\sigma)}$ is a finite union of points and intervals. That reason is semi-algebraicity. Proving it requires showing that the relative interior of the optimal set, and the parameter values where a rank is attained there, can be described by a first-order formula over the reals, and then eliminating the quantifiers. Mathlib has no Tarski–Seidenberg theorem, and the one-variable structure theorem for semi-algebraic sets (milestone 9) is itself missing.

A second difficulty is the parametric duality: strict feasibility is assumed only at $\epsilon=0$ , and propagating it to all of $\operatorname{int}(\mathcal E)$ (Remark 1) uses a theorem of the alternative for SDO.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; $X\succeq0$ is PosSemidef (which includes symmetry) and $X\succ0$ is PosDef. Symmetry of $A^i$ , $C$ , $\bar C$ is a hypothesis of every theorem, as are Assumptions 1–2. The optimal value $v$ is an EReal infimum over $\mathcal P$ , so $v=-\infty$ is represented faithfully and $\mathcal E$ is not a junk set. $\mathcal D^*(\epsilon)$ compares $b^Ty$ with the primal value $v(\epsilon)$ , as printed. The relative interior is Mathlib's intrinsicInterior. Definition 1 lets $X^*(\epsilon)$ be any maximally complementary solution. The formalization removes this choice by taking the supremum of ranks over relative-interior points, and milestone 5 shows that every such point has that rank. $\mathcal S_{(\theta,\sigma)}$ uses the relative interior of the product, as printed. A subset of $\mathbb R$ is semi-algebraic when its copy in $\mathbb R^1$ is a finite union of sets $\{p=0,\ g<0\}$ with real polynomials.

Trivializing formalizations are excluded:

ranks are taken at relative-interior points only, never at arbitrary optimal points;
$v$ is an extended-real infimum, never a real sInf (which would make an unbounded problem look finite with value $0$ );
transition points are defined by Definition 5 itself, not as boundary points of $\mathcal S_{(\theta,\sigma)}$ .

The paper also states that $\mathcal E$ is closed. Under Assumptions 1–2 this is false: $n=2$ , $m=1$ , $A^1=\operatorname{diag}(1,0)$ , $b=1$ , $C=\begin{pmatrix}0&1\\1&1\end{pmatrix}$ , $\bar C=\operatorname{diag}(0,1)$ gives $\mathcal E=(-1,\infty)$ . Milestone 2 omits closedness. The paper's proof of Theorem 1 does not use it.

Contributions welcome: proofs of any milestone; a semi-algebraic toolkit in Lean (closure under Boolean operations, projections from $\mathbb R^{N+1}$ to $\mathbb R$ , the one-dimensional structure theorem); conic duality for standard-form SDO.

Selected references

J. D. Hauenstein, A. Mohammad-Nezhad, T. Tang, T. Terlaky, On computing the nonlinearity interval in parametric semidefinite optimization, Mathematics of Operations Research, 2022. arXiv:1908.10499v3
A. Mohammad-Nezhad, T. Terlaky, Parametric analysis of semidefinite optimization, Optimization 69 (2020), 187–216.
I. Adler, R. D. C. Monteiro, A geometric view of parametric linear programming, Algorithmica 8 (1992), 161–176.
D. Goldfarb, K. Scheinberg, On parametric semidefinite programming, Applied Numerical Mathematics 29 (1999), 361–377.
S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, Springer, 2006.
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.

11 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Optimal Use and Replenishment of Two Substitutable Raw Materials in a Stochastic Capacitated Make-to-Order Production System: A Use-Down-To/Balancing Production Policy Is OptimalResearch Paper

Motivation

Make-to-order manufacturers may use two substitutable raw materials to satisfy demand when production capacity and material deliveries are uncertain. A cheaper material may yield less finished product per unit, and the firm must decide how much of each material to preserve for later periods. A production rule based only on current unit costs can be wrong because using one material changes the inventory state from which future orders and production will be chosen. Chen, Duenyas, and Jasin study this coupled replenishment and production problem and characterize the form of an optimal production decision. Their result gives a state-dependent rule described by four curves, rather than requiring a separate optimization for every inventory state. This mission formalizes that production result from the 2016 working-paper version of their study.

Setting

There are $T\ge1$ periods and two substitutable materials. A unit of finished product requires $a^j>0$ units of type- $j$ material, with $a^1<a^2$ . Before production in period $t$ , the available material is a vector $y_t=(y_t^1,y_t^2)\in\mathbb R_+^2$ . Demand $D_t$ and production capacity $R_t$ are nonnegative random quantities with finite support. A unit of satisfied demand earns revenue $e_t$ ; a unit of lost demand incurs penalty $\sigma_t>0$ . Holding costs are $h_t^j$ and material purchasing costs are $c_t^j$ . Ordered amounts are limited by random availabilities $q_t^j$ , whose finite supports may include $+\infty$ .

The production decision is the remaining inventory $w_t$ after material use. The feasible set $E_2(y_t,D_t,R_t)$ contains vectors satisfying $0\le w_t\le y_t$ , the demand limit, and the capacity limit:

a^1w_t^1+a^2w_t^2\ge a^1y_t^1+a^2y_t^2-D_t,\qquad w_t^1+w_t^2\ge y_t^1+y_t^2-R_t.

The objective $J_t(w_t)$ adds the current cost coefficients $(a^jp_t+h_t^j-c_{t+1}^j)w_t^j$ , where $p_t=e_t+\sigma_t$ , to the next-period value $V_{t+1}(w_t)$ . The value functions are determined backward from $V_{T+1}(x)=c_{T+1}^1x^1+c_{T+1}^2x^2$ by the production and replenishment equations (1)–(5). Thus $J_t$ is an object computed from the model data and the dynamic program. These definitions follow §3 of the working paper.

Formalization targets

Optimal production rule

The goal is Theorem 1, pp. 15–16. There are two nonincreasing switching curves $\gamma_t^1,\gamma_t^2$ and two balancing curves $\alpha_t,\beta_t$ meeting at $\bar w_t$ . Together they define the use-down-to and balancing (UB) rule of Definition 1. For every nonnegative $D,R$ and every $y\in\mathbb R_+^2$ , the prescribed decision is feasible and optimal:

w_t^*(y,D,R)\in\operatorname*{arg\,min}_{w\in E_2(y,D,R)}J_t(w).

The goal also includes the theorem's four minimization characterizations: $\bar w_t$ minimizes $J_t$ on the whole nonnegative orthant; each $\gamma_t^j$ minimizes a one-coordinate section; $\alpha_t(x)$ minimizes on $a^1w^1+a^2w^2=x$ ; and $\beta_t(x)$ minimizes on $w^1+w^2=x$ , for every $x\ge0$ . The milestones retain Lemma 3(a), Lemma 3(d), the backward-induction claim for $H_t$ , Proposition 1 for the strictly convex perturbation, and Proposition 2 for the limiting policy.

Significance

The theorem identifies which material-use rule solves the production stage for any observed demand, capacity, and inventory. Its curves are independent of that period's realized $D$ and $R$ ; those realizations enter the region boundaries and the rule's arguments. This structure supports the paper's later ordering-policy and computational work without replacing the original dynamic program with an unrelated one. The same formal definitions of feasible production, finite-support expectations, and coordinatewise value-function structure can be reused in other two-resource inventory models.

The working paper proves the result mathematically; the requested machine-checked work is to prove the Lean statements. The present proposal supplies definitions and theorem targets with sorry proof bodies. It does not claim that Theorem 1 or its milestones already have Lean proofs. A completed development would connect the backward dynamic program to the curve characterization and then prove that the region-specific action is optimal.

Difficulty

The replenishment-stage objective $G_t$ is generally neither convex nor supermodular even when the subsequent value function has those properties, as the paper notes after Lemma 3. Consequently, taking a minimum in the replenishment recursion does not preserve the desired shape by an immediate standard argument. At the production stage, demand and capacity impose different coupled linear constraints on the two materials. Minimizing each material coordinate separately therefore does not produce a feasible or optimal decision in general. The source's region boundaries must account for which of these constraints binds and for their changes at $D=a^1R$ and $D=a^2R$ .

Formalization scope

Lean uses $\mathbb R\times\mathbb R$ with componentwise order for two-material vectors. Each random quantity is a finite support with nonnegative real weights summing to one; expectations are finite sums. The two availability laws are multiplied as independent laws at each period, and $+\infty$ availability is represented by WithTop ℝ. The joint law of $(D_t,R_t)$ need not factor. The dynamic program has periods $1,\ldots,T$ , and the terminal value is set at $T+1$ . Its minima are defined as infima of feasible objective images; attainment is content of the results, not part of the definitions. Lower-growth claims use eventual real inequalities for every positive error, with the other inventory coordinate fixed and nonnegative.

The paper describes revenues and costs as monetary amounts and uses sign conditions in its proof of Lemma 3. The Lean standing predicate makes explicit $e_t,h_t^j,c_t^j\ge0$ , $c_t^j+h_t^j>0$ , $a^j>0$ , and $T>0$ , in addition to the paper's $\sigma_t>0$ and $a^1<a^2$ . These assumptions are disclosed because without them the stated coercivity and attainment claims may fail. The objective in the goal is precisely $J_t$ produced by the full backward recursion; allowing an arbitrary objective with assumed structural properties would omit the dynamic-programming content.

Definition 1 calls its six regions a partition. At $D\le a^1R$ , two printed regions can overlap; a concrete Lean check is included locally. The formal policy follows the page's displayed order when more than one region matches. Region coverage is asserted for all nonnegative $D,R$ , and pairwise disjointness is asserted only when $a^1R<D$ . The first-match convention and corrected partition claim are documented with the counterexample for review. The piecewise formulas for $K^j$ , $L^j$ , and $\bar\gamma^j$ retain their source inequalities. Contributions establishing feasibility, curve existence, uniqueness for the perturbed problem, and the induction step are all useful to the mission.

Selected references

Q. Chen, I. Duenyas, and S. Jasin, Optimal Use and Replenishment of Two Substitutable Raw Materials in a Nonstationary Capacitated Make-to-Order Production System, SSRN working paper 2801786, version of 2016-06-28. SSRN.

11 thms2 active usersReviewed

Algorithmic Game Theory Linear Optimization Operations Research·Captain: mikedeng1

Consensus Halving for Sets of Items: For n Agents with Additive Utilities a Consensus Halving That Cuts at Most min{n, m} of the m Items Always ExistsResearch Paper

Motivation

Consensus halving asks for a division of a resource into two parts that every one of $n$ agents values equally, so that a group with heterogeneous preferences can agree that the two parts are of the same worth. The classical setting is a divisible interval (a cake or a necklace), where Simmons and Su (2003), building on Hobby and Rice (1965), showed that $n$ cuts always suffice. The question has a direct application to fair division: once a consensus halving is found, two parties can each take a part without either side of a group of stakeholders preferring the other part. Since Filos-Ratsikas and Goldberg (2018) proved that approximate consensus halving on an interval is PPA-complete, the problem has also become a central example in the complexity theory of total search problems.

Goldberg, Hollender, Igarashi, Manurangsi and Suksompong (arXiv:2007.06754, Mathematics of Operations Research, 2022) study the same question for a set of items with no spatial order: houses, children's custody days, or a portfolio of assets, where an item may be shared fractionally but each shared item is a cost. Their first result, for additive utilities, is the subject of this mission.

Setting

There is a set of $n$ agents and a set of $m$ items. Agent $i$ values item $j$ at $u_i(j)$ , and §2 of the paper assumes $u_i(j)\ge 0$ .

A fractional set of items holds a fraction $x_j\in[0,1]$ of each item $j$ ; it is written as the vector $x=(x_1,\dots,x_m)$ .
Utilities are additive: agent $i$ values the fractional set $x$ at $u_i(x)=\sum_j x_j\,u_i(j)$ .
A partition into two fractional sets $M_1,M_2$ gives every item fractions summing to exactly $1$ , so it is determined by $M_1=x$ : the set $M_2$ holds $1-x_j$ of item $j$ .
A consensus halving (Definition 2.1) is such a partition with $u_i(M_1)=u_i(M_2)$ for every agent $i$ , that is,

\sum_j x_j\,u_i(j)=\sum_j (1-x_j)\,u_i(j)\qquad\text{for all } i .

Equivalently (display (1) of the paper), $\sum_j x_j\,u_i(j)=\tfrac12\sum_j u_i(j)$ for all $i$ .

Item $j$ is cut if a positive fraction of it lies in each part, i.e. $0<x_j<1$ .

In the Lean development these are util, IsFractional, IsConsensusHalving, IsCut and numCuts in the namespace ConsHalving.Additive.

Formalization targets

Goal: Theorem 2.2 (existence form)

For $n$ agents with nonnegative additive utilities over $m$ items there is a consensus halving with at most $\min\{n,m\}$ cut items:

\exists\,x\in[0,1]^m:\quad \sum_j x_j\,u_i(j)=\sum_j(1-x_j)\,u_i(j)\ \ \forall i,\qquad \#\{j:0<x_j<1\}\le\min\{n,m\}.

The paper states:

Theorem 2.2. For n agents with additive utilities, there exists a polynomial-time algorithm that computes a consensus halving with at most min{n, m} cuts.

The mission formalizes the existence of the algorithm's output. The polynomial-time clause is not formalized: the paper fixes no machine model, and its complexity argument is a reference to Gaussian elimination.

Milestones

The milestones follow the steps of the paper's proof (p. 5), which runs an iterative procedure starting from $x\equiv\tfrac12$ :

display (1): the equal-value condition is the linear system $\sum_j x_j u_i(j)=\tfrac12\sum_j u_i(j)$ ;
the case $n\ge m$ : halving every item gives a consensus halving with $m=\min\{n,m\}$ cuts;
the combination $(1-\gamma)x+\gamma y$ of two solutions of (1) solves (1);
the bounds of Step 3(c): the new point stays in $[0,1]^m$ and the minimizing item $j^*$ becomes uncut;
one pass of Step 3 preserves the invariants (consensus halving, every frozen item uncut) and freezes a new item;
if the current point is the unique solution of the system $S\cup T$ , then $|T|\ge m-n$ .

Significance

The result. Splitting every item in half is always a consensus halving, but it cuts all $m$ items. Theorem 2.2 shows that, however many items there are, sharing at most as many items as there are agents is enough. This matches the $n$ -cut bound of Hobby–Rice and Simmons–Su for the interval, and the paper shows it is tight: Theorem 2.5 proves that when the utilities are drawn independently from non-atomic distributions, almost surely every consensus halving cuts at least $\min\{n,m\}$ items. The paper generalizes it to consensus $k$ -splitting (Theorem 5.3, at most $(k-1)\min\{n,m\}$ cuts).

Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. The mission produces a checked consensus-halving model for additive utilities over unordered items and a checked proof of the $\min\{n,m\}$ bound, together with a reusable fact about linear systems: a system of $n+|T|$ equations in $m$ unknowns with a unique solution has $n+|T|\ge m$ .

Difficulty

The obvious approach is to note that the consensus halvings form a polytope in $[0,1]^m$ cut out by $n$ equations, and that a vertex of that polytope has at most $n$ fractional coordinates. The difficulty is to make "vertex" precise and nonempty in Lean: one must show that the polytope (nonempty, since it contains $x\equiv\tfrac12$ ) has a point where enough box constraints are tight, which needs either an extreme-point argument for compact convex sets or the paper's explicit procedure. The procedure in turn needs a termination argument: each pass freezes one new coordinate at $0$ or $1$ , and when no further move exists, a dimension count on the solution set of $S\cup T$ is required. The step coefficient $\gamma_{j^*}$ may exceed $1$ , so the "convex combination" of the paper is an affine one, and the bound $s\in[0,1]^m$ comes from the minimality of $\gamma_{j^*}$ , not from convexity.

Formalization scope

Agents are Fin n, items Fin m (the paper's $[n]$ , $[m]$ , indexed from $0$ ). The bounds $n,m\ge1$ are not assumed; every statement remains true for $n=0$ or $m=0$ .
Utilities are u : Fin n → Fin m → ℝ. Nonnegativity, a standing assumption of §2, is a hypothesis of the goal only; the milestones hold for real utilities of any sign, as the paper remarks on p. 6 for combinations of goods and chores.
A partition is encoded by $x$ alone, with $M_2$ holding $1-x_j$ ; IsConsensusHalving includes $x\in[0,1]^m$ . Without that bound every solution of (1) would count, and the cut count would be meaningless, so a formalization dropping it is ruled out.
A cut is $0<x_j\wedge 0<1-x_j$ , not $x_j\ne0$ . numCuts is the cardinality of the set of cut items.
gamma x y j is the $\gamma_j$ of Step 3(a). At $y_j=x_j$ it takes the junk value $0$ , and every statement using it quantifies over $y_j\ne x_j$ only and assumes $y_{j^*}\ne x_{j^*}$ , so the junk value never enters.
In the termination milestone the current point is assumed to solve $S$ , so that the uniqueness hypothesis cannot hold vacuously for an infeasible system. The inequality $|T|\ge m-n$ is written $m\le n+|T|$ .
Mathlib supplies the needed linear algebra (finite-dimensional kernels, rank–nullity). The step lemmas carry the loop invariants as explicit hypotheses rather than formalizing the while loop itself. Solvers may close the goal along the paper's procedure, through the milestones, or by any other argument, such as an extreme-point argument.

Selected references

P. W. Goldberg, A. Hollender, A. Igarashi, P. Manurangsi, W. Suksompong, Consensus Halving for Sets of Items, Mathematics of Operations Research, 2022; preprint arXiv:2007.06754v1, 2020. https://arxiv.org/abs/2007.06754
C. R. Hobby, J. R. Rice, A moment problem in L1 approximation, Proceedings of the American Mathematical Society 16(4):665–670, 1965. https://doi.org/10.2307/2033900
F. W. Simmons, F. E. Su, Consensus-halving via theorems of Borsuk–Ulam and Tucker, Mathematical Social Sciences 45(1), 2003. https://doi.org/10.1016/S0165-4896(02)00087-2
A. Filos-Ratsikas, P. W. Goldberg, Consensus halving is PPA-complete, Proceedings of the 50th ACM Symposium on Theory of Computing (STOC), 51–64, 2018. https://doi.org/10.1145/3188745.3188880

18 thms2 active users

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Hypergraph k-Cut for Fixed k in Deterministic Polynomial Time: A Maximal Minimum k-Partition's First Part Is the Source-Maximal Minimum (S, T)-Terminal Cut for Some |S| = 2k − 2Research Paper

Why this question matters

The hypergraph k-cut problem asks for a least-cost way to split the vertices of a hypergraph into $k$ nonempty groups. An edge of a hypergraph may contain more than two vertices, so the graph version does not capture the behavior of every input. For fixed $k$ , randomized polynomial-time algorithms for hypergraph k-cut were known before the deterministic result of Chandrasekaran and Chekuri. Their paper identifies a structural property of optimal partitions that makes one of their deterministic approaches possible. This mission isolates that property as a mathematical theorem about finite hypergraphs.

The same paper explains why the distinction between hypergraph k-cut and partitioning by a general symmetric submodular set function matters. The hypergraph cut function is symmetric and submodular, but the cost of a k-partition counts each crossing hyperedge once; it is generally different from the sum of the cut values of the parts. The paper also gives a counterexample to a proposed extension of its uncrossing theorem to general submodular functions. The target here therefore uses the actual hyperedge crossing cost throughout. Chandrasekaran and Chekuri, §§1.1 and 3.

Finite hypergraphs and terminal cuts

Let $G=(V,E)$ be a finite unit-cost hypergraph. A hyperedge is a subset of the vertex set $V$ , and $E$ may contain parallel copies. For a vertex set $A$ , its cut value $d(A)$ is the number of edge copies meeting both $A$ and its complement $\overline A=V\setminus A$ . Thus empty edges, singleton edges, and edges lying entirely on one side contribute zero. This is the paper's convention after it reduces to unit costs in §1.1. Source, pp. 3 and 7.

An ordered k-partition $P=(V_1,\ldots,V_k)$ has $k$ nonempty, pairwise disjoint parts whose union is $V$ . Its cost counts each hyperedge once if that edge meets at least two distinct parts. A minimum k-partition has least cost among all such ordered partitions. It is maximal minimum when there is no other minimum k-partition whose first part strictly contains $V_1$ . The order matters because the theorem singles out $V_1$ . Source, p. 4.

For disjoint vertex sets $(S,T)$ , an $(S,T)$ -terminal cut is a source set $U$ with $S\subseteq U\subseteq V\setminus T$ . A minimum terminal cut has the smallest $d(U)$ among these sets. The source-maximal minimum terminal cut is the minimum cut whose source set contains the source set of every other minimum $(S,T)$ -terminal cut. This condition identifies one set, even when several minimum cuts have the same value. Source, p. 3.

Formalization targets

The structural theorem

For $k\ge 2$ , let $P=(V_1,\ldots,V_k)$ be a maximal minimum k-partition with $|V_1|\ge 2k-2$ . For every $T\subseteq\overline{V_1}$ that meets every $V_j$ with $j\ge 2$ , the goal is

\exists S\subseteq V_1,\quad |S|=2k-2 \quad\text{and}\quad V_1\text{ is the source-maximal minimum }(S,T)\text{-terminal cut}.

This is Theorem 1.2, p. 4. The size is an equality, and the set $S$ may depend on $T$ . Source maximality is part of the conclusion.

Supporting statements

The milestone list includes symmetry and submodularity of $d$ , uniqueness of the source-maximal minimum terminal cut, the counting statements of §3 (Proposition 3.1, the identity $d(Y_1\cup W)+d(Y_2\cup W)=\sigma(Y_1,Y_2,W,Z)$ ; Lemma 3.1, the one-step refinement bound on $\sigma$ ; Lemma 3.2, the $\sigma$ bound for uncrossed minimum terminal cuts; Lemma 3.3, the selection of $k-1$ parts), and the containment and extremal claims used in §4 (Lemma 4.1, Claims 4.1 and 4.2). The principal intermediate target is Theorem 3.1: under its specified family of minimum terminal cuts, it produces a k-partition $P$ whose last part strictly contains a given complement $\overline U$ , and whose cost is at most half of every pair sum $d(A_i)+d(A_j)$ . These are separate theorem statements with the same finite hypergraph model.

What the result provides

Theorem 1.2 says that a part of a suitably chosen optimum partition can be specified by a bounded-size source set and a sink set meeting the other parts. It gives a finite certificate for recovering that part via a minimum terminal-cut problem. Unlike a statement about one specially chosen low-cut-value part, it applies to the first part of any maximal minimum k-partition that meets the size condition. The paper uses this theorem to derive its first deterministic polynomial-time algorithm. Chandrasekaran and Chekuri, Theorem 2.1 and §2.

This mission formalizes the known structural result, not a new conjecture. The Lean statements are compiled with proof placeholders; the mathematical proofs remain work for solvers. A complete development would produce reusable definitions and lemmas for hypergraph cut values, minimum terminal cuts, uncrossing, and counting edges crossing a partition. These objects are also useful for checking related claims about graph cuts and constrained partitions.

Where the proof is difficult

For a graph edge, crossing a partition has only two endpoints to track. A hyperedge may meet several parts at once, and the relationship between the sum of part cut values and the cost of the whole partition changes with that pattern. A direct submodularity argument does not control all the needed costs. Section 3 introduces an auxiliary count $\sigma$ that distinguishes edge patterns, and Theorem 3.1 combines minimum terminal cuts with a partition cost bound. Section 4 then uses that bound to rule out a failed choice of the source set in Theorem 1.2. The paper explicitly shows that the corresponding uncrossing statement fails for arbitrary symmetric submodular functions. Source, §§3–4, especially Remark 3.2.

Formalization scope

Vertices have a finite Lean type, vertex subsets are Finset V, and hyperedges form a Multiset (Finset V). The multiset preserves parallel copies under unit costs. Partitions are functions Fin k → Finset V; their parts are required to be nonempty, disjoint, and exhaustive, with P 0 representing $V_1$ . Complements are relative to all vertices. All counts are natural numbers. The theorem assumes $k\ge2$ , so $2k-2$ is the ordinary nontruncated value. It counts a crossing edge when that edge meets at least two parts, following the explicit mathematical test in the paper's definition.

The source-maximal predicate requires both minimum cut value and containment of every other minimum terminal source set. Neither a merely minimum cut nor an arbitrary maximal minimum cut is accepted as the target. The cost and d functions count edge copies, including duplicate hyperedges, so replacing the multiset by a set would change the problem. The published predicates for symmetric and submodular real-valued set functions are reused after casting the cut counts to real numbers.

Theorem 1.1, the polynomial-time algorithm claim, is outside this mission. It would need a precise machine and running-time model; an unqualified existential algorithm claim would also be satisfied by exhaustive search. The algorithms and running-time theorems of §§2 and 6, and the distinct structural results of §§5–6, are not represented here. Contributions toward proofs of the source-maximal cut theorem, the §3 counting estimates, and the §4 containment argument are within scope.

Selected references

Karthekeyan Chandrasekaran and Chandra Chekuri, Hypergraph k-cut for fixed k in deterministic polynomial time, arXiv:2009.12442v1, 2020; published in Mathematics of Operations Research, 2022. arXiv.

15 thms2 active usersReviewed

Completed

Economics Mechanism Design Operations Research·Captain: mikedeng1

Mechanism Design for Managing Hidden Rebates and Inflated Quotes of a Procurement Service Provider: Paying a Fee Equal to the Hidden Rebate Is the Optimal Truthful Contract for Small RebatesResearch Paper

Motivation

Retailers that source apparel and other consumer goods from contract manufacturers in developing countries often work through a procurement service provider, an intermediary that solicits quotes, negotiates and manages production on the retailer's behalf. A documented problem in this industry is the hidden rebate: some manufacturers pay the intermediary a covert "referral commission" whenever they win an order. The intermediary then has a reason to favour those manufacturers, and, because the retailer sees quotes only through the intermediary, it can inflate the quotes of manufacturers that pay nothing. The retailer ends up buying from a more expensive source.

Fan, Chen and Tang (SSRN 3514358; Manufacturing & Service Operations Management, 2020) ask what a retailer can do about this with contracts alone, without audits or penalties, when it can verify a quote only with the manufacturer it finally selects. Their answer for the base model is an explicit contract: a selection rule that handicaps the rebate-paying manufacturer by the size of the rebate, together with a service fee equal to the rebate. The paper relates to the literature on middlemen and corruption in procurement (Burguet and Che 2004; Burguet and Perry 2007) and on mechanism design with partial verification, where Strausz (2016) showed that the revelation principle survives when only the selected party's report can be checked.

Setting

A retailer must buy one order from one of two manufacturers. Manufacturer $S$ is known to be ethical; manufacturer $W$ pays the intermediary a fixed hidden rebate $r \ge 0$ if and only if $W$ wins. The manufacturers' prices $x_S, x_W \ge 0$ are independent draws from a common distribution $\mu$ with density $g$ and survival function $\bar G(t) = \mu((t,\infty))$ . Because $W$ builds the rebate into its quote, the true quotes are

q = (q_S, q_W) = (x_S,\ x_W + r).

The intermediary observes $q$ and reports $z = (z_S, z_W)$ to the retailer. A deterministic contract $\langle A, F\rangle$ is a selection rule $A(z) \in \{S, W\}$ and a non-negative service fee $F(z)$ . After choosing $A(z)$ , the retailer checks the selected manufacturer's quote: if $z_{A(z)} = q_{A(z)}$ , the intermediary is paid $F(z)$ and, if $W$ was selected, also collects $r$ from $W$ ; otherwise it receives nothing. Its ex post payoff (1) is

\pi(z; \langle A,F\rangle) = \big(r\,\mathbf 1_{A(z)=W} + F(z)\big)\,\mathbf 1_{z_{A(z)} = q_{A(z)}}.

A contract is incentive compatible (13) when truthful reporting $z = q$ maximizes this payoff for every pair of true prices; ties are resolved in favour of truth-telling. Under truthful reporting the retailer pays $q_{A(q)} + F(q)$ , and its problem (14) is to minimize the expected value of this cost over incentive-compatible contracts.

The threshold of footnote 15 is

\bar r = \min\Big\{ \inf_{a>0,\,T\ge a} \frac{E\big((x_S-x_W)\mathbf 1_{x_S>x_W>T}\big) + E\big((x_W-x_S)\mathbf 1_{T>x_W>x_S>a}\big)}{\bar G(T)\,\bar G(a)},\ \inf_{T\ge 0} \Big[E\big(x_W \mathbf 1_{x_W<T}\big) + E(x_S)\,\bar G(T) - E\min\{x_S,x_W\}\Big] \Big\}.

In the Lean development these objects are quote, payoff, IsIC, Feasible, cost, contractStar, Gbar and rbar, in the namespace HiddenRebate.Fixed.

Formalization targets

Goal: Theorem 1 (p. 12)

Let $\langle A^*, F^*\rangle$ be the contract (15):

A^*(z) = \begin{cases} S & z_S \le z_W - r\\ W & z_S > z_W - r\end{cases},\qquad F^*(z) = \begin{cases} r & A^*(z) = S\\ 0 & \text{otherwise.}\end{cases}

If $0 \le r < \bar r$ , then $\langle A^*, F^*\rangle$ is incentive compatible, its expected cost is finite, and

E\,C(q;\langle A^*,F^*\rangle) \le E\,C(q;\langle A,F\rangle)

for every admissible incentive-compatible deterministic contract $\langle A,F\rangle$ .

Milestones

§5.1, p. 12. Under (15) the intermediary collects $r$ in every state, so (15) is incentive compatible.
§5.1, p. 12. In cost coordinates, $A^*(x_S, x_W + r) = S$ if and only if $x_S \le x_W$ .
(19), p. 13. $E\,C(q;\langle A^*,F^*\rangle) = E[\min\{x_S,x_W\} + r]$ .

Significance

Theorem 1 gives the retailer a contract that can be written down and implemented: it removes quote inflation entirely, selects the cheaper manufacturer in every state (no distortion), and lowers the retailer's expected cost from $E(x_W) + r$ under "lowest quote wins" to $E\min\{x_S, x_W\} + r$ (Corollaries 1 and 2 of the paper). The price of honesty is exactly the rebate, paid as a fee. The optimality half says that no other deterministic incentive-compatible contract does better as long as the rebate is below $\bar r$ .

The paper's proof of Theorem 1, including the characterization of incentive-compatible contracts and the optimal contract for $r > \bar r$ , is in an appendix that is not part of the preprint held for this mission. Formalizing the theorem therefore means reconstructing the optimality argument, not transcribing it. No machine-checked proof of this result, or of any result of the paper, is known.

Difficulty

Incentive compatibility of (15) is a short case check. The difficulty is optimality: the class of competitors is every pair of measurable maps on $\mathbb R^2$ satisfying (13), and the obvious comparison with the first-best cost $E\min\{x_S,x_W\}$ fails, because a competitor can pay less than $r$ in some states. One has to understand which contracts are incentive compatible under partial verification, where the intermediary can freely misreport the quote of the manufacturer that is not selected, and show that every such contract costs at least $E\min\{x_S,x_W\} + r$ when $r < \bar r$ . The threshold $\bar r$ is an infimum over a two-parameter family, so the comparison must hold uniformly over that family.

Formalization scope

Prices live in $\mathbb R$ with $\mu((-\infty,0)) = 0$ ; $\mu$ is a probability measure absolutely continuous with respect to Lebesgue measure (the density $g$ ); the joint law of $(x_S, x_W)$ is $\mu \otimes \mu$ . Reports range over all of $\mathbb R^2$ , and (13) is required for every pair $x_S, x_W \ge 0$ and every report, pointwise. A contract is a pair A : ℝ × ℝ → Supplier, F : ℝ × ℝ → ℝ with $F \ge 0$ , $\{A = S\}$ measurable and $F$ measurable. The cost (14) is the Bochner integral over $(x_S, x_W)$ of $q_{A(q)} + F(q)$ at $q = (x_S, x_W + r)$ .

Conventions and additions relative to the page, all disclosed in the item statements:

$E[x_S] < \infty$ and $r \ge 0$ are assumed;
competitors are required to have an integrable cost (a non-integrable non-negative cost is infinite and cannot beat (15)), and integrability of (15)'s cost is part of the conclusion;
each "min" in footnote 15 is an infimum, and pairs with $\bar G(T)\bar G(a) = 0$ are excluded from the first one;
footnote 15 is stated as printed: its second term is not divided by $\bar G(T)$ . This can only make $\bar r$ smaller, so the hypothesis is at least as strong as the evidently intended one;
the reduction from general mechanisms to deterministic direct ones (Strausz 2016) is cited by the paper and is not part of the statement.

The goal compares the cost of (15) with each competitor's cost directly; it is not stated with $E\min\{x_S, x_W\} + r$ substituted for the left side, and it is not reduced to incentive compatibility alone, which is milestone 1. For iid Exp(1) prices $\bar r = 1/2 - 1/e \approx 0.132$ , so the hypothesis $r < \bar r$ is satisfiable; for prices with bounded support $\bar r = 0$ and the theorem is vacuous, as on the page.

Needed infrastructure: product measures and Bochner integrals on $\mathbb R^2$ (in Mathlib), and a characterization of incentive-compatible contracts under partial verification, which would be reusable for other models in which only the selected agent is audited. Contributions of intermediate lemmas, such as lower bounds on the cost of incentive-compatible contracts, are welcome as linked theorems.

Selected references

X. Fan, Y.-J. Chen, C. S. Tang, Mechanism design for managing hidden rebates and inflated quotes of a procurement service provider, Manufacturing & Service Operations Management, 2020; preprint SSRN 3514358. https://ssrn.com/abstract=3514358
R. Strausz, Mechanism design with partially verifiable information, working paper, Humboldt University of Berlin, 2016 (as cited in the paper).
R. Burguet, Y.-K. Che, Competitive procurement with corruption, RAND Journal of Economics 35(1), 50–68, 2004.
R. Burguet, M. Perry, Bribery and favoritism by auctioneers in sealed-bid auctions, The B.E. Journal of Theoretical Economics 7(1), 1–27, 2007.

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Optimal Price/Advertising Menus for Two-Sided Media Platforms: In Duopoly with Multi-Item Menus the Unique Equilibrium Is a Symmetric Two-Item Menu on Which Both Consumer Types Multi-HomeResearch Paper

Motivation

Ad-supported media and digital services (streaming music and video, news sites, social platforms) sell to two sides at once. Consumers value the content, advertisers value the consumers' attention, and consumers usually regard advertising as a nuisance whose cost differs from one person to the next. Many such platforms answer this with menu pricing: a free tier with ads next to a paid tier with few or no ads, so that consumers sort themselves by how much they mind advertising.

DeValve and Pekeč (SSRN 2715531; Operations Research 70(3), 2022, doi:10.1287/opre.2021.2230) characterize revenue-maximizing price/advertising menus when the platform does not observe a consumer's advertising disutility, first for a monopoly and then for a duopoly in which consumers decide endogenously whether to use one platform (single-homing), both (multi-homing) or neither. Earlier models of competing ad-supported platforms either fix homing behaviour through Hotelling competition (Anderson and Coate 2005; Armstrong 2006) or allow multi-homing with homogeneous ad disutility (Ambrus, Calvano and Reisinger 2016). This mission targets the paper's duopoly result, Proposition 3: the equilibrium with menus exists, is unique, and is symmetric, with both consumer types multi-homing.

Setting

A representative consumer has base value $v$ for content and is of type $\theta\in\{L,H\}$ with advertising disutility $d^\theta$ , $0<d^L<d^H$ . Type $H$ occurs with probability $r\in(0,1)$ ; write $r^H=r$ , $r^L=1-r$ . Two platforms $i=1,2$ each offer a menu of two items $(s,a)$ , a subscription price $s\in\mathbb R$ (negative prices allowed) and an advertising quantity $a\ge 0$ ; the two items of a menu may coincide.

A consumer who single-homes on platform $i$ with item $(s_i,a_i)$ and consumes $x_i\ge0$ gets $v x_i-\tfrac12x_i^2-(d^\theta a_i+s_i)$ . A consumer who multi-homes with items $(s_1,a_1)$ , $(s_2,a_2)$ gets

\sum_{i=1}^2\big(vx_i-\tfrac12x_i^2-(d^\theta a_i+s_i)\big)-\gamma x_1x_2,

where $\gamma\in(0,1)$ measures substitutability between the platforms. The utility of a choice is the supremum over nonnegative consumption; abstaining gives $0$ . Write $c^\theta(s,a)=d^\theta a+s$ for the cost of an item to type $\theta$ .

Advertisers pay a per-type market-clearing price $p=w-\sum_i a_i$ , the sum over the platforms the consumer uses, and a platform used with item $(s_i,a_i)$ earns $s_i+p\,a_i$ . Each platform maximizes its expected revenue over the two types.

An equilibrium is a menu profile with consumer choices such that: each type maximizes utility; on ties she multi-homes if multi-homing is optimal and participates if participating is optimal; and no platform can raise its expected revenue by switching to another admissible menu, when the consumers respond optimally under the same tie rules, the deviator may select the response most favourable to it, and a type that uses the rival platform before and after the deviation keeps her item there. The paper uses this concept in its proofs without naming it. The mission writes it out.

Let $\rho=(1-\gamma)/(1+\gamma)$ and $\alpha=\big(w-d^H-(1-r)(d^H-d^L)/r\big)^+$ .

Formalization targets

Goal: Proposition 3

With

(s^L,a^L)=\Big(\tfrac{\rho v^2}{2}-d^La^L-(d^H-d^L)a^H,\ \tfrac{w-d^L}{3}\Big),\qquad(s^H,a^H)=\Big(\tfrac{\rho v^2}{2}-d^Ha^H,\ \tfrac{\alpha}{3}\Big),

the profile in which both platforms offer $\{(s^L,a^L),(s^H,a^H)\}$ and each type $\theta$ multi-homes on $(s^\theta,a^\theta)$ is an equilibrium; the two items are distinct; in every equilibrium each menu is exactly these two items and each type multi-homes on her item; and each platform's expected revenue is

\frac{\rho v^2}{2}+\frac{(1-r)(w-d^L)^2+r\alpha^2}{9}.

Milestones

Lemma 6 A–E (p. 45): the multi-homing utility $v^2/(1+\gamma)-\sum_i c^\theta_i$ , the single-homing utility $\tfrac12v^2-c^\theta_i$ , the participation threshold $(1-\gamma)v^2/(2(1+\gamma))$ for multi- and single-homing, and cost minimization within each platform's menu.
Lemma 8 (p. 47): in every equilibrium both types multi-home.
Consumer choices (pp. 52–53): at the stated menus, multi-homing on the designed items is an admissible response for each type.
Platform best response (pp. 53–56): against the stated menu, no deviation earns more than the stated revenue.
Best response (22)/(24) (pp. 56–58): in every equilibrium, each platform's chosen ad quantities and prices are the explicit best response to the rival's.
Fixed point (pp. 58–59): the best-response equations (22) have the unique solution $a^L_1=a^L_2=(w-d^L)/3$ , $a^H_1=a^H_2=\alpha/3$ .

Significance

The proposition describes how competition shapes menus. With two platforms, consumers of both types use both platforms, the menus are symmetric, and the low-disutility type is given a price discount while the high-disutility type gets an advertising discount. When $\alpha=0$ the menu is a "free use with ads / pay for no ads" menu. The paper builds on this characterization: Corollary 1 compares monopoly and duopoly prices by type, and Proposition 4 shows the value of offering a menu instead of a single item can exceed $2$ under competition.

No machine-checked version of these results exists. A formal proof checks a uniqueness argument that runs over every combination of homing behaviour and every admissible deviation, and it fixes an equilibrium concept that the paper uses without defining. The model file is reusable for the paper's other duopoly results (Lemma 3, Proposition 4, Corollary 1) and for related two-sided pricing models with quadratic utility.

Difficulty

The consumer has nine possible choices per type, and a platform's deviation changes which of them is optimal. A best response is therefore not one optimization problem but a family indexed by homing behaviour, and the ad price $w-\sum_ia_i$ couples the two platforms through every type that multi-homes. Reducing the deviation problem to a single program requires showing that no deviation profitably moves a type from multi-homing to single-homing, which uses the rival's menu and the tie rules. The uniqueness part needs every non-multi-homing configuration ruled out separately (Lemma 8) and then a fixed-point argument for a piecewise-linear best-response map with a pooling regime. Tie-breaking matters: without the multi-homing tie rule or the status-quo rule on the rival platform, the stated profile is not an equilibrium.

Formalization scope

Lean represents platforms and item slots by Fin 2 (the paper's platforms 1, 2 are 0, 1), menus by Fin 2 → ℝ × ℝ with entries (s, a), and all quantities in ℝ. A menu is admissible when every ad quantity is nonnegative; prices are unrestricted. Utilities are suprema over nonnegative consumption, which are finite because $\gamma<1$ . They are not defined by the closed forms of Lemma 6. The equilibrium predicate IsEquilibrium encodes the four rules above: consumer optimality, multi-homing and participation on ties, arbitrary admissible deviations with the deviator's most favourable admissible response, and the status-quo rule on the rival platform. The strategy space is two-item menus, as in the paper after Lemma 7. Uniqueness is uniqueness of the chosen items and of each menu as a set, up to which slot holds which item.

Two hypotheses are added to the paper's standing assumptions and disclosed: $v>0$ , and $w>d^L$ , without which the stated $a^L$ is negative. The condition $w>d^H$ is not assumed; the case $\alpha=0$ is part of the result.

The goal is not posed as "each menu solves the platform's program (21) given the other". That would assume the reduction from the game to the program, which is the content of Lemma 8 and of the platform-best-response step. The goal quantifies over all equilibria of the game itself. Existence is a conjunct of the goal, so the uniqueness and revenue clauses cannot hold vacuously.

Needed: the model file (provided), elementary calculus of concave quadratics for Lemma 6, and case analysis over finite choice sets. Welcome contributions are proofs of the Lemma 6 parts, the fixed-point algebra, the consumer-choice step, and the two platform best-response steps.

Selected references

L. DeValve, S. Pekeč, Optimal Price/Advertising Menus for Two-Sided Media Platforms, SSRN 2715531 (version of 2021-04-15); published in Operations Research 70(3), 2022. https://ssrn.com/abstract=2715531, https://doi.org/10.1287/opre.2021.2230
A. Ambrus, E. Calvano, M. Reisinger, Either or Both Competition: A "Two-Sided" Theory of Advertising with Overlapping Viewerships, American Economic Journal: Microeconomics 8(3), 2016. https://doi.org/10.1257/mic.20150019
S. P. Anderson, S. Coate, Market Provision of Broadcasting: A Welfare Analysis, Review of Economic Studies 72(4), 2005. https://doi.org/10.1111/0034-6527.00356
M. Armstrong, Competition in Two-Sided Markets, RAND Journal of Economics 37(3), 2006. https://doi.org/10.1111/j.1756-2171.2006.tb00037.x
J.-C. Rochet, J. Tirole, Platform Competition in Two-Sided Markets, Journal of the European Economic Association 1(4), 2003. https://doi.org/10.1162/154247603322493212

12 thms2 active usersReviewed

Machine Learning Optimization Random Matrix Theory+1·Captain: mikedeng1

Nonconvex Low-Rank Tensor Completion from Noisy Data: Spectrally Initialized Vanilla Gradient Descent Recovers the Tensor Factors at a Linear Rate to Near-Optimal ℓ2 and ℓ2,∞ AccuracyResearch Paper

Motivation

A partially observed array with three indices appears when data record relationships among triples of objects. If its entries have a low-rank structure, one can hope to recover the full array from far fewer than $d^3$ measurements. Cai, Li, Poor and Chen study this problem when the measurements are noisy and only a random subset of entries is seen. Their result gives a statistical error bound for a concrete two-stage method: spectral initialization followed by ordinary gradient descent on a nonconvex loss. It is a known theorem, proved in the pinned preprint, rather than an open conjecture.

Setting

The unknown symmetric order-three tensor is $T^\star\in\mathbb R^{d\times d\times d}$ . It has a CP decomposition $T^\star=\sum_{s=1}^r(u_s^\star)^{\otimes3}$ , where the nonzero columns $u_s^\star$ form $U^\star\in\mathbb R^{d\times r}$ . Each unordered triple of coordinates is sampled independently with probability $p$ ; its six permutations share one sampling decision. On a sampled triple the observation is $T^\star_{ijk}+E_{ijk}$ , with symmetric, centered, independent sub-Gaussian noise of variance at most $\sigma^2$ . The observed tensor $T$ vanishes outside the sampled set $\Omega$ .

For a candidate factor matrix $U=[u_1,\ldots,u_r]$ , the objective is

f(U)=\frac{1}{6p}\left\|P_\Omega\!\left(\sum_{s=1}^r u_s^{\otimes3}-T\right)\right\|_F^2.

Algorithm 2 obtains a leading $r$ -dimensional eigenspace from an off-diagonal Gram matrix of the mode-one unfolding of $p^{-1}T$ . Algorithm 3 uses Gaussian restarts, leading singular vectors, and greedy pruning to turn that subspace into a factor matrix $U^0$ . Algorithm 1 then applies the gradient step to $f$ . Eigenvalue ties, leading singular-vector choices, and pruning ties can produce several admissible executions; the result concerns every execution.

Incoherence $\mu$ measures how evenly the tensor and factors spread across coordinates and how nearly orthogonal distinct factors are. The condition number $\kappa$ is the ratio of the largest to smallest factor norm. Write $\lambda^\star_{\min}=\min_s\|u_s^\star\|_2^3$ and $\lambda^\star_{\max}=\max_s\|u_s^\star\|_2^3$ . Distances $\operatorname{dist}_F$ , $\operatorname{dist}_\infty$ , and $\operatorname{dist}_{2,\infty}$ minimize their respective matrix norms over permutations of the $r$ columns.

Formalization targets

The goal is Theorem 2.4, in the bounded-rank, bounded-incoherence, bounded-condition-number regime. Under its printed sampling, noise, restart, threshold and step-size conditions, for every $0\le t\le d^5$ it asserts, with probability at least $1-\delta$ ,

\operatorname{dist}_F(U^t,U^\star)\le\left(C_1\rho^t+C_2\frac{\sigma}{\lambda^\star_{\min}}\sqrt{\frac{d\log d}{p}}\right)\|U^\star\|_F,

\operatorname{dist}_\infty(U^t,U^\star)\le\operatorname{dist}_{2,\infty}(U^t,U^\star)\le\left(C_3\rho^t+C_4\frac{\sigma}{\lambda^\star_{\min}}\sqrt{\frac{d\log d}{p}}\right)\|U^\star\|_{2,\infty}.

The rate is fixed to $\rho=1-\lambda_{\min}^{\star,4/3}\eta/5$ , consistent with the paper's local-convergence lemmas. Milestones formalize the gradient identity (36), local Hessian bounds (Lemma 5.1), spectral-subspace recovery (Lemma 5.7), factor retrieval (Theorem 5.9), and the paper's general-parameter recovery theorem (Theorem 2.8). The latter makes the dependence on $\mu$ and $r$ explicit.

Significance

The inequalities give two guarantees at once: geometric reduction of initialization error and an explicit noise floor. The $2,\infty$ bound controls the error in each coordinate row, which a Frobenius estimate alone does not supply. Together with the tensor-entry corollaries in the paper, they explain the accuracy of this practical nonconvex method under random subsampling. The authors also specify how the sample probability, noise level, rank and incoherence interact, so the result can be compared to other tensor-completion methods.

This mission asks for a machine-checked version of the known result. Its published ψ₂ norm definition is reused; the paper-specific tensor model, spectral initialization relations, loss and gradient iteration are new. The theorem statements compile with sorry, so none of their proofs is claimed as machine checked here. Proofs of the listed milestones, the main theorem, and faithful auxiliary concentration results are welcome; the paper's numerical experiments are outside this formalization.

Difficulty

The gradient loss is nonconvex, so global convexity cannot justify the iteration bound. The local Hessian estimate applies only near $U^\star$ in both Frobenius and rowwise norm. A Frobenius estimate alone cannot establish the rowwise condition at every iteration. The spectral initializer must also select individual factors from a subspace despite nearly tied eigenvalues and noisy tensor contractions. These are the points where a direct appeal to standard smooth-gradient-descent theory stops short of the stated result.

Formalization scope

Coordinates are Fin d and Fin r, with zero-based indexing; the PDF uses one-based indices. All logarithms are natural. Tensor and matrix norms are explicit finite-coordinate Euclidean norms. Minima over permutations range over all permutations of Fin r, and maxima in the incoherence parameters range over the indices specified by Definition 2.1. Sampling is on sorted triples, then extended by symmetry. The probability model is a single probability space carrying the sampling indicators, noise variables and Gaussian restarts, jointly independent; the paper leaves some cross-family independence implicit. Noise has mean zero, variance at most $\sigma^2$ , and ψ₂ norm at most $\sigma$ using the published extended-nonnegative norm. The last bound makes the paper's sub-Gaussian scale explicit.

The statements use $d\ge d_0\ge2$ , $r\ge1$ , nonzero true factor columns, $0<p\le1$ , and $\sigma\ge0$ . Theorems 2.8 and 5.9 use $r\ge2$ and round their real-valued restart count up to a natural number; this handles the boundary where $\log r=0$ . Theorem 2.4 places its claimed absolute error constants before the rank and incoherence bounds and all instance data. Probability is expressed as the outer measure of the bad event, since admissible-execution predicates quantify over choices and need not be measurable. Each good event explicitly asserts that an admissible execution exists before requiring the bounds for every execution; otherwise a failed pruning run would make a universal claim vacuous.

The remaining reusable infrastructure includes concentration for symmetric sampled tensors, finite-dimensional spectral perturbation with ties, and derivative estimates for the cubic factor map. The paper's leave-one-out iteration lemmas and their auxiliary estimators are not included in this initial milestone list; they remain natural contributions toward the full proof.

Selected references

C. Cai, G. Li, H. V. Poor and Y. Chen, Nonconvex Low-Rank Tensor Completion from Noisy Data, arXiv:1911.04436v2, 2021; published in Operations Research 70(2), 2022. Preprint.
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Definition 2.5.6 for the ψ₂ norm. Publisher DOI.

8 thms2 active usersReviewed

Completed

Economics Operations Research Probability·Captain: mikedeng1

Pricing of Debt and Equity in a Financial Network with Comonotonic Endowments: Closed-Form Default Probabilities and Expected Wealth, Debt Payments and Equity under Bankruptcy CostsResearch Paper

Motivation

Banks hold claims on one another. When one bank cannot pay, its creditors receive less, which can push them into default in turn. Clearing models compute the payments and wealths that are consistent across the whole network. Regulators and researchers use them to measure systemic risk and to price interbank debt. The basic model is that of Eisenberg and Noe (2001), doi:10.1287/mnsc.47.2.236.9835. Rogers and Veraart (2013), doi:10.1287/mnsc.1120.1569, added bankruptcy costs: a defaulting bank recovers only part of its assets.

The value of a bank's debt or equity is an expectation over random endowments. For general endowments that expectation requires partitioning the endowment space into up to $2^n$ default regions (Gouriéroux, Héam and Monfort 2012), and with bankruptcy costs those regions need not be convex. Banerjee and Feinstein, Pricing of debt and equity in a financial network with comonotonic endowments (Operations Research 2022; arXiv:1810.01372), observe that when all endowments are driven by one factor (they are comonotonic), banks default in a fixed order as the factor falls. Default probabilities and the prices of debt and equity then have closed forms.

Setting

There are $n$ banks and an outside society node. Bank $i$ owes a total of $\bar p_i > 0$ ; the fraction $\pi_{ij} \ge 0$ of it is owed to bank $j$ ( $\pi_{ii} = 0$ ), and the fraction $1 - \sum_j \pi_{ij} > 0$ to society (Assumption 2.1). The matrix $\Pi = (\pi_{ij})$ is the relative liabilities matrix. Banks start with endowments $x \in \mathbb R^n_+$ . A bank with negative wealth $V_i < 0$ defaults and keeps a fraction $\alpha_x \in [0,1]$ of its external assets and $\alpha_L \in [0,1]$ of its interbank assets.

With $V^- = \max(-V, 0)$ componentwise, the clearing process is

\Psi^*_i(V) = \big(\mathbb I_{\{V_i\ge0\}} + \mathbb I_{\{V_i<0\}}\alpha_x\big)x_i + \big(\mathbb I_{\{V_i\ge0\}} + \mathbb I_{\{V_i<0\}}\alpha_L\big)\sum_{j}\pi_{ji}(\bar p_j - V_j^-) - \bar p_i ,

and a variant $\Psi$ , which replaces $\bar p_j - V_j^-$ by its positive part, is used in the appendix. The greatest clearing wealth $V(x)$ is the largest real solution of $V = \Psi^*(V)$ . Bank $i$ 's payment is $p_i(x) = \bar p_i - V_i(x)^-$ and its equity is $E_i(x) = V_i(x)^+$ .

If the set of defaulting banks has indicator $z \in \{0,1\}^n$ , the clearing equations are linear. With $\operatorname{diag}(z)$ the diagonal 0–1 matrix of $z$ ,

\Delta(z) = \big(I - (I - (1-\alpha_L)\operatorname{diag}(z))\Pi^\top\operatorname{diag}(z)\big)^{-1}\big(I - (1-\alpha_x)\operatorname{diag}(z)\big),

\delta(z) = \big(I - (I - (1-\alpha_L)\operatorname{diag}(z))\Pi^\top\operatorname{diag}(z)\big)^{-1}\big[I - (I - (1-\alpha_L)\operatorname{diag}(z))\Pi^\top\big]\bar p .

Comonotonic endowments are $X = f(q)$ for a nonnegative random factor $q$ and a nondecreasing map $f : \mathbb R_+ \to \mathbb R^n_+$ (Assumption 3.2). The solvency threshold of bank $i$ is $q^*_i = \inf\{q \ge 0 \mid V_i(f(q)) \ge 0\}$ (Definition 3.4). Banks are numbered so that $q^*_1 \ge \dots \ge q^*_n$ , with $q^*_0 = \infty$ and $q^*_{n+1} = 0$ (Assumption 3.5). On $q \in [q^*_{k+1}, q^*_k)$ exactly banks $1,\dots,k$ default; $\Delta_k$ and $\delta_k$ are $\Delta$ and $\delta$ at that default set, with $\Delta_0 = I$ and $\delta_0 = (I - \Pi^\top)\bar p$ .

Formalization targets

Goal: Theorem 3.6 (p. 13), with right-continuous $f$

With $T_k = \Delta_k\,\mathbb E[f(q)\mathbb I_{\{q\in[q^*_{k+1},q^*_k)\}}] - \delta_k\,\mathbb P(q\in[q^*_{k+1},q^*_k))$ , for every bank $i$ :

\mathbb P(V_i(X)<0) = \mathbb P(q<q^*_i), \qquad \mathbb E[V_i(X)] = e_i^\top\sum_{k=0}^n T_k,

\mathbb E[p_i(X)] = \bar p_i + e_i^\top\sum_{k=i}^n T_k, \qquad \mathbb E[E_i(X)] = e_i^\top\sum_{k=0}^{i-1}T_k .

The goal is the theorem as printed, with one added hypothesis (see Formalization scope).

Milestones

Proposition A.1 (p. 34): $V = \Psi(V)$ has a greatest and a least solution, and every solution lies in $[-\bar p,\; x + \Pi^\top\bar p - \bar p]$ .
Proposition A.3 (p. 34): the greatest solution of $V = \Psi(V)$ is the greatest real fixed point of $\Psi^*$ , so it is $V(x)$ .
Proposition A.6 (p. 36): $V$ , $p$ and $E$ are nondecreasing in $x$ .
Corollary A.4 (p. 35): the fictitious default algorithm stops at $V(x)$ , and every matrix it inverts is nonsingular.
§3.1 display (p. 11): $V(x) = \Delta(\mathbb I_{\{V(x)<0\}})x - \delta(\mathbb I_{\{V(x)<0\}})$ for every $x \in \mathbb R^n_+$ .

Significance

Theorem 3.6 turns the valuation of every bank's debt and equity in a network with bankruptcy costs into $n+1$ one-dimensional integrals of the factor, replacing the $2^n$ default regions of the general case. The default probabilities depend only on the thresholds $q^*$ , which in turn depend only on the map $f$ and not on the law of $q$ . The same formulas price debt and equity in the paper's numerical study of the European banking system, and they are the starting point for the comonotonic bounds of Lemma 4.1, which are not part of this mission.

The paper gives a one-sentence proof of Theorem 3.6 and proves its appendix results largely by citation (Tarski, Milgrom–Roberts, Rogers–Veraart, input–output theory). No part of it has been machine-checked. A formalization supplies the missing steps: the identification of the two clearing maps, the attainment of the thresholds, nonsingularity of the linear systems, and the decomposition of the expectations. It also produces, as a reusable by-product, the Rogers–Veraart clearing model with its greatest fixed point, which other financial-network results can build on.

Difficulty

The obvious argument is: banks default in order, on each interval of $q$ the wealth is affine in $f(q)$ , so integrate piece by piece. Two steps of it fail as stated.

First, the threshold $q^*_i$ is an infimum, and the paper treats it as attained ("the minimal value such that firm $i$ is solvent"). With bankruptcy costs the wealth $V(f(q))$ jumps when a bank defaults, even for continuous $f$ , so attainment needs an argument about the greatest fixed point under decreasing endowments. Without right-continuity of $f$ it is false.

Second, the greatest fixed point of $\Psi^*$ is not reached by Tarski's theorem on $[-\infty, \cdot]$ , because $\Psi^*$ is not monotone below $-\bar p$ . That every real fixed point lies above $-\bar p$ uses Assumption 2.1. Nonsingularity of $I - (I-(1-\alpha_L)\Lambda)\Pi^\top\Lambda$ also rests on Assumption 2.1. Matching the default set $\{1,\dots,k\}$ to the interval $[q^*_{k+1},q^*_k)$ then combines monotonicity (Proposition A.6) with the ordering of Assumption 3.5.

Formalization scope

Model. The theorem statements assume $n>0$ , as in §2 of the paper. Banks are Fin n; bank i is the paper's bank $i+1$ . The data are $\Pi$ , $\bar p$ , $\alpha_x$ , $\alpha_L$ (structure Network), with the standing assumptions bundled in Network.Standing. $V(x)$ is the supremum of the real fixed points of $\Psi^*$ in the lattice $\mathbb R^n$ ; payments and equity follow Definition 2.2. Default sets are finite sets of banks. Inverses are Matrix.inv.
Thresholds are valued in $[0,\infty]$ : a bank that is never solvent has $q^*_i = \infty$ (the paper writes $q^* \in \mathbb R^n_+$ , but its own convention $q^*_0 = \infty$ requires the extended value).
Added hypothesis: $f$ is right-continuous on $[0,\infty)$ . As printed, Theorem 3.6 fails: with $n=1$ , $\Pi=0$ , $\bar p=1$ , $f=0$ on $[0,1]$ and $f=2$ afterwards, and $q \in \{1,2\}$ with probability $\tfrac12$ each, $\mathbb P(V_1<0) = \tfrac12$ but $\mathbb P(q<q^*_1) = 0$ .
Typo: Corollary A.4 (iv) prints $\Pi^\top\Lambda V^{(k)}$ where $\alpha_L\Pi^\top\Lambda V^{(k)}$ is meant in the default bracket; the closed form on its second line is used.
Index shift: the paper's sums over $k = i,\dots,n$ and $k = 0,\dots,i-1$ become $k \in \{i+1,\dots,n\}$ and $k \in \{0,\dots,i\}$ for the 0-based bank i.
Endowments are $X = f(q)$ literally, with $q$ measurable, $q \ge 0$ almost surely, and each $f_j(q)$ integrable.
Ruled out. $V$ is never defined by the piecewise formula, and $q^*$ is never a free parameter. Both are computed from the clearing map, and only their ordering (Assumption 3.5) is assumed. Integrability and Assumption 2.1 are present wherever an integral or an inverse appears, so neither can collapse to Lean's junk value $0$ .
Infrastructure. The development needs Knaster–Tarski on boxes in $\mathbb R^n$ , monotone comparative statics of greatest fixed points, invertibility of $I - A$ for nonnegative $A$ with column sums below $1$ , and decomposition of Bochner integrals over finitely many disjoint events. The clearing model and the greatest-fixed-point lemmas are reusable for other network models. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

T. Banerjee, Z. Feinstein, Pricing of debt and equity in a financial network with comonotonic endowments, Operations Research, 2022; preprint arXiv:1810.01372v5. https://arxiv.org/abs/1810.01372
L. Eisenberg, T. H. Noe, Systemic risk in financial systems, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
L. C. G. Rogers, L. A. M. Veraart, Failure and rescue in an interbank network, Management Science 59(4), 2013. https://doi.org/10.1287/mnsc.1120.1569
C. Gouriéroux, J.-C. Héam, A. Monfort, Bilateral exposures and systemic solvency risk, Canadian Journal of Economics 45(4):1273–1309, 2012.
P. Milgrom, J. Roberts, Comparing equilibria, American Economic Review 84(3), 1994.

8 thms2 active usersReviewed

Completed

Linear algebra Operations Research Optimization·Captain: mikedeng1

Market Efficient Portfolios in a Systemic Economy: f-Efficient Bank Holdings Exist, Attain Mean Squared Deviation (bᵀv)²/(1ᵀG⁻¹1), and Are Unique if and only if There Are Exactly Two BanksResearch Paper

Motivation

When banks are hit by losses they sell assets to restore their leverage targets, and these fire sales depress prices for every other holder of the same assets. The resulting deviation of market capitalization from its fundamental value is a systemic externality: it depends not on any single bank's portfolio but on how the stock of each asset is distributed across banks. Awiszus, Capponi and Weber (arXiv:2003.10121, Operations Research 2022) ask which distribution of a fixed stock of assets among banks with fixed budgets minimizes this externality, as measured by the expected squared deviation of market capitalization from fundamentals. The question matters to macroprudential regulators, who can influence portfolio overlap among banks, and it connects to the literature on overlapping portfolios and price-mediated contagion (Greenwood, Landier and Thesmar, 2015; Capponi and Larsson, 2015).

The paper's answer is explicit: the optimal mean squared deviation has a closed form, the optimum is computed by a two-step "aggregate first, then allocate" procedure, and the optimal allocation is unique exactly when there are two banks.

Setting

There are $K$ assets and $N$ banks. A holding matrix $Q\in\mathbb R^{K\times N}$ records in entry $Q_{ki}$ the holding of asset $k$ by bank $i$ , so column $i$ is bank $i$ 's portfolio. Initial prices are normalized to $1$ .

The vector $q\in\mathbb R^K$ gives the total initial holdings of each asset in the banking sector, and $b\in\mathbb R^N$ gives the banks' budgets. The feasible holding matrices are

\mathscr D(q,b) = \{Q\in\mathbb R^{K\times N} \mid Q\mathbf 1_N = q,\ \mathbf 1_K^\top Q = b^\top\}.

Price shocks $Z_1,\dots,Z_K$ have means $\mu\in\mathbb R^K$ and are uncorrelated with variances $\sigma_k^2$ , $\sigma_k>0$ (Assumption 2). Their second-moment matrix is

G = \mu\mu^\top + \mathrm{Diag}(\sigma^2).

The systemic significance vector $v\in\mathbb R^N$ (the paper's (3.1)) summarizes each bank's leverage targeting, liquidation strategy and the assets' illiquidity. To first order, the deviation of market capitalization from fundamentals is $(Qv)^\top Z$ , and its second moment is the mean squared deviation

\mathrm{MSD}(Q) = (Qv)^\top G\,(Qv).

A holding matrix $Q^*\in\mathscr D(q,b)$ is f-efficient (Definition 1) if it minimizes $\mathrm{MSD}$ over $\mathscr D(q,b)$ .
Assumption 3: $v_i\neq v_j$ for some $i,j$ , and $b^\top v\neq 0$ .
The aggregate problem (4.3) minimizes $y^\top G y$ over $\mathscr D_y = \{y\in\mathbb R^K \mid \mathbf 1_K^\top y = b^\top v\}$ . With $z = G^{-1}\mathbf 1_K$ , put $y^* = \frac{b^\top v}{\mathbf 1_K^\top z}\,z$ .

Formalization targets

Goal: Theorem 4.1

Let $N,K\ge 2$ . Then

\exists\,Q^*\ \text{f-efficient with}\quad \mathrm{MSD}(Q^*) = \frac{(b^\top v)^2}{\mathbf 1_K^\top G^{-1}\mathbf 1_K},

the f-efficient holding matrix is unique if and only if $N=2$ , and in that case it equals

Q^{N=2} = \frac{1}{v_2-v_1}\big(\,v_2 q - y^*\;\;\; y^* - v_1 q\,\big)\in\mathbb R^{K\times 2}.

Milestones

$G$ is positive definite, $G^{-1}$ has the Sherman–Morrison form, and $\mathbf 1_K^\top G^{-1}\mathbf 1_K\neq 0$ (proof of Lemma 4.1).
Lemma 4.1: $y^*$ is the unique solution of the aggregate problem (4.3).
Proposition 4.2: for $N\ge2$ , $K\ge1$ there is $Q^*\in\mathscr D(q,b)$ with $Q^*v=y^*$ .
Proposition 4.1: $Q^*\in\mathscr D(q,b)$ is f-efficient if and only if $Q^*v$ solves (4.3).
Remark EC.1.1: $Q^*$ is f-efficient if and only if $F\,\mathrm{vec}(Q^*) = (b,q,y^*)$ for the $(2K+N)\times KN$ matrix $F$ of (EC.1.12).
The value computation $\mathrm{MSD}(Q^*) = (y^*)^\top G y^* = (b^\top v)^2/\mathbf 1_K^\top G^{-1}\mathbf 1_K$ (proof of Theorem 4.1 a).
$\mathrm{rank}(F) = 2K+N-2$ and $\mathrm{null}(F) = (N-2)(K-1)$ (proof of Theorem 4.1 b).

Significance

The result itself. Theorem 4.1 gives the smallest achievable mean squared deviation of market capitalization from fundamentals for a given asset supply, budget profile and systemic significance profile, as an explicit function of the shock moments. It is the benchmark against which the paper measures the inefficiency of observed and diversified holdings (Section 4.2 shows that full diversification is f-efficient only in a degenerate case) and drives the comparative statics of Section 5. Part b) says that with three or more banks efficiency leaves an affine family of optimal allocations of dimension $(N-2)(K-1)$ , so a regulator has residual freedom to pursue other objectives at no cost in market efficiency.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The formal development delivers the theorem together with a reusable treatment of minimizing a positive definite quadratic form over a hyperplane, the existence part of the transportation-type linear system $Q\mathbf 1_N=q$ , $\mathbf 1_K^\top Q=b^\top$ , $Qv=y$ , and an exact rank computation for the structured matrix $F$ . The uniqueness characterization in part b) depends on that rank computation, which the paper carries out by Gaussian elimination on block matrices.

Difficulty

The minimization over $\mathscr D(q,b)$ is a $KN$ -dimensional quadratic program whose objective is degenerate: it depends on $Q$ only through the $K$ -vector $Qv$ . Strict convexity therefore cannot give uniqueness, since the objective is constant along every direction in which $Qv$ and the constraints do not change, and the obvious argument for part b) fails. Existence is not automatic either: $\mathscr D(q,b)$ is unbounded, and one must show that every point of the hyperplane $\mathscr D_y$ is attained as $Qv$ by a feasible $Q$ , which fails when $v$ is constant. The uniqueness statement is a dimension count: it needs the exact rank of the $(2K+N)\times KN$ constraint matrix $F$ , whose rows carry exactly two linear dependencies under Assumption 3, so that the solution set has dimension $(N-2)(K-1)$ , which is positive as soon as $N\ge3$ and $K\ge2$ .

Formalization scope

Assets are Fin K, banks are Fin N, all quantities are real; holding matrices are Matrix (Fin K) (Fin N) ℝ. The paper's banks 1 and 2 are the indices 0 and 1.
$G^{-1}$ is Mathlib's Matrix.inv, which returns $0$ on singular matrices. Every statement that mentions $G^{-1}$ , $z$ or $y^*$ assumes $\sigma_k>0$ for all $k$ (Assumption 2), and every statement that divides by $\mathbf 1_K^\top z$ assumes $K\ge1$ .
The systemic significance $v$ is a free parameter in $\mathbb R^N$ subject to Assumption 3, not derived from the primitives by (3.1). Every result of Section 4 holds for each such $v$ , and $v$ does not depend on $Q$ .
Added hypothesis: $\sum_k q_k=\sum_i b_i$ appears on the statements that need $\mathscr D(q,b)\neq\emptyset$ (Proposition 4.2 and Theorem 4.1). The paper derives it from feasibility on p. 11; without it part a) is false.
Statements that use only the first half of Assumption 3 ( $v$ not constant) assume only that half. The goal carries Assumption 3 in full.
f-efficiency is an argmin. It is the minimization over $\mathscr D(q,b)$ of Definition 1, and $\mathrm{MSD}$ is the quadratic form $(Qv)^\top G(Qv)$ . Defining f-efficiency as $Qv=y^*$ , or defining $\mathrm{MSD}$ through $y^*$ , would remove the optimization from the goal and is ruled out.
$\mathrm{vec}(Q)$ is indexed by pairs (asset, bank) instead of stacked columns, and $\mathrm{null}(F)$ is the Module.finrank of the kernel of $x\mapsto Fx$ .
$Q^{N=2}$ is defined for $v\in\mathbb R^2$ ; the goal transports it along $N=2$ with Fin.cast.

The development needs the Sherman–Morrison identity for a diagonal-plus-rank-one matrix, the minimizer of a positive definite quadratic form under one linear constraint, explicit constructions in $\mathscr D(q,b)$ , and a rank computation. Contributions of reusable lemmas for these, and of proofs of the milestones in any order, are welcome.

Selected references

K. Awiszus, A. Capponi, S. Weber, Market Efficient Portfolios in a Systemic Economy, Operations Research 70(2), 2022. Preprint arXiv:2003.10121v3. https://arxiv.org/abs/2003.10121
R. Greenwood, A. Landier, D. Thesmar, Vulnerable Banks, Journal of Financial Economics 115(3), 2015. https://doi.org/10.1016/j.jfineco.2014.11.006
A. Capponi, M. Larsson, Price Contagion through Balance Sheet Linkages, Review of Asset Pricing Studies 5(2), 2015. https://doi.org/10.1093/rapstu/rav006
D. S. Bernstein, Matrix Mathematics, Princeton University Press, 2005.

9 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

A General Framework to Compare Announcement Accuracy: Static vs. LES-Based Announcement: The Static Announcement Has No Larger MSE if and only if the Correlation Is at Most 1/2Research Paper

Why delay announcements matter

A customer who is told that service will be delayed can use the announced wait to decide whether to stay, leave, or plan around the delay. A service operator needs to know whether a changing, customer-specific announcement actually predicts the eventual wait more accurately than a fixed announcement. Bassamboo and Ibrahim studied this question for the last-entered-service (LES) announcement, which reports the wait of the last customer to enter service, and for a static announcement based on the mean wait of delayed customers. Their empirical examples show that neither method wins uniformly across queueing regimes; the comparison depends on how the announcement and the eventual wait move together (Bassamboo and Ibrahim, 2021, §§3–4 of the submitted manuscript).

The mission isolates the paper's general comparison criterion. Its statement needs no particular arrival process, service discipline, or queue length. This makes the result a reusable mathematical test for predictors in other service systems as well as for LES. The paper itself notes that the criterion applies irrespective of the specific queueing model, subject to the moment conditions under which its mean-squared errors and correlations are defined (submitted manuscript, §4.2, p. 14).

Random waits and predictions

Let $W_D$ be the real-valued waiting time of a delayed customer in steady state. Operationally, the paper takes the virtual waiting time $W_\infty$ and conditions on $W_\infty>0$ : $W_D$ has the conditional distribution of a positive wait. Let $P$ be a real-valued predictor issued to that customer. To compare a prediction with the outcome, the pair $(P,W_D)$ must be jointly distributed; their separate marginal distributions cannot determine the correlation. Both are represented as functions on one probability space in Lean.

The static announcement, denoted $\operatorname{EA}$ , always reports $\mathbb E[W_D]$ . A changing predictor can instead respond to the system's current state. The paper's mean-squared error of $P$ is the expectation of its squared discrepancy from the outcome:

\operatorname{MSE}(P)=\mathbb E[(W_D-P)^2].

Write $\operatorname{Var}(X)$ and $\operatorname{Cov}(X,Y)$ for variance and covariance. When both variances are positive, the Pearson correlation is $r[X,Y]=\operatorname{Cov}(X,Y)/\sqrt{\operatorname{Var}(X)\operatorname{Var}(Y)}$ . The coefficient of variation of the delay is $C_{W_D}=\sqrt{\operatorname{Var}(W_D)}/\mathbb E[W_D]$ . These are the quantities in §4.2 and equation (3) of the submitted manuscript (published article; mission citations use the submitted manuscript's page and equation numbers).

Formalization targets

The first milestone establishes the error of the static predictor from its definition:

\operatorname{MSE}(\operatorname{EA})=\operatorname{Var}(W_D).

The next two milestones give the expanded error identity from the proof of Proposition 1 and its normalized form, equation (4). Suppose $\mathbb E[P]=\gamma\mathbb E[W_D]$ and $\operatorname{Var}(P)=\beta\operatorname{Var}(W_D)$ with $\gamma,\beta\ge0$ . Proposition 1 states

\operatorname{MSE}(P)=\operatorname{Var}(W_D) \left(\beta+1+\left(\frac{\gamma-1}{C_{W_D}}\right)^2 -2r[P,W_D]\sqrt\beta\right).

The goal is Corollary 1, equation (5). If $P$ has the same mean and variance as $W_D$ , it compares the two predictors at the exact threshold $1/2$ :

\operatorname{MSE}(\operatorname{EA})\le\operatorname{MSE}(P) \quad\Longleftrightarrow\quad r[P,W_D]\le\frac12.

Both inequalities are non-strict. The corollary is stated for a general predictor $P$ ; applying it to LES requires a separate analysis of the LES wait and its correlation with the arriving customer's wait. The submitted manuscript supplies that model-specific analysis later in §5 (Bassamboo and Ibrahim, 2021).

What the criterion gives

Under the corollary's equal-mean and equal-variance assumptions, the comparison of two expected squared errors reduces to one correlation. A predictor with correlation at most $1/2$ offers no mean-squared-error improvement over the static announcement; a predictor above that threshold does. The equality case is included. Proposition 1 also records how a mean shift or a variance change modifies this comparison, which is useful when a proposed announcement is biased or more variable than the delay.

The paper proves these identities. This mission asks for machine-checked proofs of their statements in Lean; the draft theorems themselves are open proof obligations. A completed development would provide reusable definitions of predictor MSE, the constant mean announcement, Pearson correlation, and coefficient of variation, together with exact interfaces for later queueing results. It does not assert that the paper's LES limit theorems are already formalized.

Where the proof work lies

The key mathematical work is passing from the expectation of a squared difference to the variance and covariance terms while keeping the two random variables on the same probability space. In Lean this requires the integrability consequences of square integrability, the relation between covariance and the centered product, and careful handling of the square-root normalization. Merely replacing MSE and correlation by unrelated real parameters would erase that work and yield an elementary numerical equivalence. The proposed definitions are therefore the expectations and covariance stated in the paper, and the goal quantifies over actual random variables.

The boundary $\beta=0$ also needs attention: the predictor has zero variance and ordinary Pearson correlation has a zero denominator. The term involving correlation is multiplied by $\sqrt\beta$ , so the displayed identity still has a meaningful value under the Lean convention described below. Proposition 1's other denominator, $C_{W_D}$ , requires a positive delay mean and variance in the intended setting.

Formalization scope

Lean uses an arbitrary measurable space with a probability measure and real-valued functions $W_D,P$ on that space. It does not construct the underlying queue; §4.2 makes the comparison at the level of the joint law of the delay and prediction. Each theorem explicitly assumes $W_D,P\in L^2$ where both appear. This supplies finite second moments for the paper's variances and MSE and avoids Lean's default value for a nonintegrable real integral. The EA identity only needs $W_D\in L^2$ .

Positive variance of $W_D$ is explicit in Proposition 1, its expansion, and the corollary. It gives the intended domain of correlation in the equal-variance corollary and prevents equation (4) from failing under division by zero. Proposition 1 additionally assumes $\mathbb E[W_D]>0$ , as expected for a positive conditional wait, so $C_{W_D}>0$ . No condition $\beta>0$ is imposed: at $\beta=0$ , Lean evaluates the zero-denominator correlation as zero and the entire correlation term vanishes. The error is defined with $(W_D-P)^2$ as in equation (3), although the proof writes the reversed difference. Contributions toward the integral identities, covariance normalization, and the final inequality are welcome; the four definitions may also serve other prediction-error formalizations.

Selected references

A. Bassamboo and R. Ibrahim, A General Framework to Compare Announcement Accuracy: Static vs. LES-Based Announcement, Management Science, 2021. DOI: 10.1287/mnsc.2020.3722. Mission theorem numbers and pages refer to the authors' submitted manuscript, §§3.1 and 4.2, pp. 7 and 12–14.

5 thms2 active usersReviewed

Algebraic Topology Algorithmic Game Theory Topology·Captain: mikedeng1

Equipartition of a Segment: Every Continuous Function on Subsegments of [0, 1] Vanishing on Degenerate Segments Takes Equal Values on Some Partition of [0, 1] into m SegmentsResearch Paper

Motivation

In fair division, a value may be assigned to each interval that a cut produces. If the value is continuous in the interval's endpoints, an equal-value partition is a natural target. Some valuations are nonnegative and additive, but a difference of competing measures or a signed utility need have neither property. Avvakumov and Karasev establish equal-value partitions even when the value changes sign and is not additive, provided it vanishes on degenerate intervals. Their result is used by Bogomolnaia and Moulin in work on guarantees for fair division. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The paper identifies earlier special cases: a nonnegative valuation follows from the Knaster–Kuratowski–Mazurkiewicz theorem; prime-power numbers of parts with a valuation of varying sign were known through degree-theoretic results; additive valuations admit an elementary argument. The remaining case permits a sign-changing, nonadditive valuation and an arbitrary positive number of parts. The authors distinguish this from an envy-free division problem with separate valuations for several players, which they state remains open outside prime-power cases. Avvakumov and Karasev, p. 2; Avvakumov and Karasev, Envy-free division using mapping degree; Meunier and Zerbib.

Setting

Write $\mathcal I$ for the set of all subsegments $I=[a,b]$ of $[0,1]$ with $0\le a\le b\le1$ . An interval may be degenerate, meaning $a=b$ . A real-valued function $f$ on $\mathcal I$ is continuous when its value varies continuously with the two endpoints. The required boundary condition is $f([a,a])=0$ for every $a\in[0,1]$ . No sign, monotonicity, or additivity condition is imposed. A partition into $m$ parts is a sequence $0=x_0\le x_1\le\cdots\le x_m=1$ , so its parts $[x_{j-1},x_j]$ may also be degenerate. Avvakumov and Karasev, Theorem 1.1, pp. 1–2.

The intermediate setting is a nice multivalued function. Its graph is a compact subset $Z$ of $\mathcal I\times(-1,1)$ . The graph separates the bottom $\mathcal I\times\{-1\}$ from the top $\mathcal I\times\{1\}$ inside the cylinder $C=\mathcal I\times[-1,1]$ : those two sides lie in different connected components of $C\setminus Z$ . A representation of a nice graph is a continuous real function $\varphi$ on $C$ that is negative on the bottom, positive on the top, and whose zero set is the graph. The paper passes between graphs and representations in Lemma 2.2. Avvakumov and Karasev, Definition 2.1 and Lemma 2.2, p. 2.

For a prime $p$ , a segment $I=[a,b]$ , and a value $y$ , a zero partition is a sequence $a=x_0\le\cdots\le x_p=b$ such that $\varphi([x_{j-1},x_j],y)=0$ for each $j=1,\ldots,p$ . The set $Z_p(\varphi)$ contains exactly those pairs $(I,y)$ that admit a zero partition. This is the projection to the cylinder of the paper's simultaneous-solution set $S$ for labeled partitions. Avvakumov and Karasev, equation (4.1) and Claim 4.4, pp. 7–9.

Formalization targets

The goal is Theorem 1.1: for every positive integer $m$ and every continuous $f$ satisfying the degenerate-interval condition, there are possibly repeated cut points with a common value:

0=x_0\le x_1\le\cdots\le x_m=1,\qquad f([x_0,x_1])=\cdots=f([x_{m-1},x_m]).

The theorem is already posed as the Open platform statement FairGuarantees.DivideChoose.theorem_of_4; this mission references that exact statement as its goal. It supplies the paper's supporting statements, including Lemma 2.2 on graph representations, Claim 4.4 on separation by projected zero partitions, and the prime-step Lemma 2.3. The latter asserts that, when $\varphi([a,a],y)=y$ , there is a represented nice graph with the same degenerate identity whose zeros each yield a zero partition for $\varphi$ . The milestone list includes the fixed-segment and continuous-family statements used to characterize $Z_p(\varphi)$ , and equation (4.2) describing its degenerate boundary. Avvakumov and Karasev, Lemmas 2.2–2.3, pp. 2–3; Claims 4.3–4.4 and equation (4.2), pp. 8–9.

Significance

The theorem guarantees equal values for any positive number of consecutive parts under only endpoint continuity and the zero-on-degenerates condition. It covers valuations for which nonnegative or additive special-case results give no conclusion. It also provides the theorem invoked in the fair-guarantee application cited by the authors. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The mathematical result was proved in the paper; the platform's theorem statement remains Open and lacks a machine-checked proof there. Formalizing the paper's intermediate claims makes its topological assumptions and its treatment of degenerate parts explicit. The definitions of a separating graph, its representation, and zero partitions can also be reused for related partition problems. The present mission states the paper's prime-step targets, leaving the proofs and the underlying equivariant topology as work for solvers.

Difficulty

For a fixed signed valuation, continuity alone does not select one common value that works across every piece of an arbitrary partition. The nonnegative case has a simplex-covering argument, but that argument does not directly control values of both signs. In the paper's general case, the difficult claim is that the projected simultaneous-zero set separates an entire cylinder, even as the segment varies. Its source proof requires a mod- $p$ statement for a space of labeled partitions and control of the resulting solution set. A further boundary issue arises on degenerate segments: a representation of the projected graph must satisfy $\psi([a,a],y)=y$ , not merely have the right zeros. Avvakumov and Karasev, pp. 2, 7–10.

Formalization scope

Lean represents $I=[a,b]$ by the endpoint pair $(a,b)$ with $0\le a\le b\le1$ . The cylinder uses the closed value range $[-1,1]$ ; a nice graph lies in its open interior $(-1,1)$ . Functions are total Lean functions, but only their values on this cylinder enter the definitions and results. Continuity is required on the cylinder. Separation uses connected components of its complement, as in Definition 2.1, and explicitly requires the bottom and top to avoid the graph. This prevents a graph containing a boundary side from satisfying separation vacuously.

Every prime-step claim assumes $p$ prime, the representation's strict boundary signs, and the degenerate identity. Zero partitions have exactly $p$ consecutive parts whose endpoints are pinned to the original segment; repeated cuts are allowed. The goal reference likewise permits degenerate parts and assumes $m\ge1$ . The projected set is defined through existence of an ordinary ordered partition, independent of how the paper labels partitions in its configuration space. The needed existing Lean notions include ContinuousOn, IsCompact, connectedComponentIn, finite index types, and Nat.Prime. A complete proof development also needs results about the paper's labeled-partition complex, equivariant cycles and transverse maps. Contributions establishing that reusable topology, as well as proofs of the stated milestones, are within scope. Avvakumov and Karasev, §§2–4.

Selected references

Sergey Avvakumov and Roman Karasev, Equipartition of a Segment, Mathematics of Operations Research, 2023. arXiv:2009.09862v4.
Anna Bogomolnaia and Hervé Moulin, Guarantees in Fair Division: General or Monotone Preferences, 2019. arXiv:1911.10009v3.
Sergey Avvakumov and Roman Karasev, Envy-Free Division Using Mapping Degree, Mathematika 67, 2021. arXiv:1907.11183.
Frédéric Meunier and Shira Zerbib, Envy-Free Cake Division Without Assuming the Players Prefer Nonempty Pieces, Israel Journal of Mathematics 234, 2019. arXiv:1804.00449.

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Multiregional Oligopoly with Capacity Constraints: The Capacity-Constrained Cournot Game Has a Unique Equilibrium, Implementing the Unique Fixed Point of the Marginal-Profit Best ResponseResearch Paper

Motivation

Firms that serve several geographic markets must decide both how much to produce and where to sell it. A capacity limit couples those regional decisions: an extra unit sent to one region cannot also be sent to another. Different transport costs and demand curves make a collection of independent single-region Cournot models inadequate. Alsabah, Bernard, Capponi, Iyengar and Sethuraman study whether this coupled quantity game has a determinate outcome. Their 2020 author version proves a unique equilibrium allocation and characterizes it through firms' marginal profits. This mission concerns that result, Theorem 4.5 on p. 12 of that version.

Setting

There are firms $i=1,\ldots,N$ and regions $r=1,\ldots,R$ . Firm $i$ sells quantity $q_r^i\ge0$ in region $r$ . Its total output is $q_{tot}^i=\sum_r q_r^i$ , constrained by capacity $\kappa^i$ . The total sales in region $r$ are $q_r^{tot}=\sum_i q_r^i$ . The inverse demand function $p_r(q)$ gives the price when total sales are $q$ . Firm $i$ pays production cost $a^i$ per unit and transport cost $t_r^i$ per unit sent to region $r$ . Its profit at allocation $Q=(q_r^i)$ is

\pi^i(Q)=\sum_r\bigl(p_r(q_r^{tot})-t_r^i\bigr)q_r^i-a^i q_{tot}^i.

A strategy for firm $i$ is any nonnegative regional allocation whose total is at most $\kappa^i$ . A Nash equilibrium is a feasible profile at which no firm can gain by changing its entire regional allocation while the others hold theirs fixed. This is the feasible unilateral-deviation definition in the paper's Definition 3.1, p. 8.

The marginal profit in region $r$ is

g_r^i(Q)=p'_r(q_r^{tot})q_r^i+p_r(q_r^{tot})-t_r^i-a^i.

For a vector $\rho=(\rho^i)$ of marginal-profit levels, condition (2) says $g_r^i(Q)\le\rho^i$ and $q_r^i(g_r^i(Q)-\rho^i)=0$ for every firm and region. Proposition 4.2 gives a unique nonnegative allocation satisfying these conditions, denoted $\hat Q(\rho)$ , when $\rho$ lies in the box $[0,\bar w]^N$ , where $w_r=p_r(0)$ and $\bar w=\max_r w_r$ . The reduced-form operator $\Phi$ assigns firm $i$ zero marginal profit if its output at $\rho^i=0$ is below capacity. Otherwise it assigns the marginal-profit level at which its output under $\hat Q$ equals $\kappa^i$ . This is the two-case definition on p. 11; it depends on the other firms' marginal-profit levels through $\hat Q$ .

Formalization targets

Fixed point of the reduced-form operator

Lemma 4.3 asserts that $\Phi$ has exactly one fixed point in the marginal-profit box:

\exists!\rho^*\in[0,\bar w]^N:\quad\Phi(\rho^*)=\rho^*.

Unique equilibrium allocation

Theorem 4.5 identifies every equilibrium of the original quantity game with the allocation at that fixed point:

Q\text{ is a Nash equilibrium}\quad\Longleftrightarrow\quad Q=\hat Q(\rho^*).

The goal includes existence of $\rho^*$ and the equivalence, so it asserts both existence and uniqueness of the equilibrium allocation. Its milestones follow the paper's supporting statements: existence of a pure equilibrium, marginal-profit conditions, existence and uniqueness of $\hat Q$ , continuity and comparative statics, fixed points of $\Phi$ , and the link from an equilibrium to a fixed point. The Algorithm 4.1 computation clause of Proposition 4.2 and the iteration-convergence clause of Lemma C.5 are identified as partial milestones; their full printed text is retained in the milestone provenance.

Significance

The result establishes that capacities, regional demand, and unequal shipping costs still lead to a single predicted sales allocation under the paper's regularity conditions. It also gives a common language for comparing the original game with a smaller game in marginal-profit vectors. Subsequent results in the paper analyze changes in costs, capacities, prices, and consumer surplus relative to this equilibrium Alsabah et al., §§5–6; those later comparative-statics claims are outside this mission.

The mathematical result is proved in the cited paper. The goal here is a machine-checked Lean development of its model, its fixed-point characterization, and the existence and uniqueness theorem. The current proposal contains definitions and theorem statements, with proofs open. The pure-Nash relation is a published reusable definition; the market model, complementarity allocation, and operator are new interfaces that could also support later formalizations of the paper's comparative-statics results.

Difficulty

An equilibrium of the quantity game satisfies the marginal-profit conditions, but those conditions alone describe candidate allocations and do not replace feasible unilateral deviations. Conversely, a fixed point of $\Phi$ does not become an equilibrium merely from the fixed-point equation: the capacity-constrained regional payoff problem still has to be connected to the allocation $\hat Q$ . Uniqueness also requires control of how all firms' regional sales respond when one marginal-profit coordinate changes. Lemma C.4 records weak and strict changes, including boundary cases where a firm stops selling in a region. The existence lemma invokes a general pure-strategy equilibrium argument; the statement is kept even though that infrastructure is substantial in Lean.

Formalization scope

Lean uses Fin N and Fin R for zero-based firm and region indices. An allocation has type Fin N → Fin R → ℝ, with the firm coordinate first, the transpose of the matrix orientation in the paper. Finite sums give firm and region totals. The inverse demands are $C^2$ on $\mathbb R$ , strictly decreasing and concave on nonnegative quantities; deriv is therefore the ordinary derivative at the quantities used here. The paper phrases Assumption 1 for direct demand $d_r$ on $[0,w_r]$ and then uses regularity of its inverse $p_r$ . The formal model makes that inverse-demand regularity an explicit assumption. It also states $w_r=p_r(0)\ge0$ , as implicit in the interval $[0,w_r]$ , positive capacities, and nonnegative production and transport costs. Those sign assumptions are needed for the box and the two branches of $\Phi$ to have the stated meaning. No positivity of prices at all quantities or finite choke quantity is assumed.

IsEquilibrium uses the published CarbonDoubleCount.Planner.IsPureNash relation, testing every feasible full strategy deviation. Qhat is chosen as the unique solution of condition (2), and Phi is computed from that allocation and the market capacities. On the stated box, the proposal's milestones establish that the selection and inverse branches denote the paper's objects. The intended theorem excludes encodings that choose an active set freely, pass $\Phi$ or $\rho^*$ as arbitrary parameters, or substitute first-order conditions or coordinatewise deviations for Nash equilibrium. The definition layer and results on continuity, monotonicity, and fixed points are reusable parts of the development. Contributions that prove these stated targets or provide supporting analysis of the firm's concave payoff problem are within scope.

Selected references

H. Alsabah, B. Bernard, A. Capponi, G. Iyengar and J. Sethuraman, Multiregional Oligopoly with Capacity Constraints, SSRN 3280688, author version dated June 6, 2020; published in Management Science, 2021. SSRN author version.

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Adversarial Patrolling in a Uniform: Attacking in the Second Period of the Patroller's Absence and Never Staying at a Location Are Optimal Strategies for Every Attack DurationResearch Paper

Why the attacker's timing matters

A visible patroller gives an attacker information: the attacker can observe when a location is vacant and wait for a favorable moment. This changes the patrolling problem from choosing how often to visit each location to choosing a movement rule that remains effective against an adversary who chooses the attack time. The preprint The Uniformed Patroller Game studies this setting on a star network, where the patroller moves between a central base and the locations she protects. Its main result characterizes a robust attack delay and a robust patroller reflection rule for every attack duration, as well as exactly when those choices are unique. The source here is arXiv:1908.07366v2, by Alpern, Chleboun, and Katsikas; the later journal article has a different title and author list.

The star and the two strategy sets

The network $S_n$ has a centre $C$ and $n$ end nodes. Each end node is a location to defend; the centre is a base and is not an attack location. A Markov patroller strategy is a pair $(p,s)$ . When at $C$ , the patroller goes to each specified end node with probability $p$ and stays at $C$ with probability $r=1-np$ . When at an end node, she returns to $C$ with probability $s$ and otherwise stays at that same end node. Thus $p>0$ , $np\leq 1$ , and $0<s\leq 1$ . The strategy does not depend on which node the attacker selects.

The attacker chooses an end node $A$ and an integer delay $d\geq1$ . After the patroller leaves $A$ , the attacker counts consecutive periods of her absence. If she returns before $d$ periods pass, the count resets. Otherwise the attack begins in the $d$ th period of absence. It lasts $m\geq2$ periods and is intercepted if the patroller visits $A$ during that interval. The paper requires $m\geq2$ because a one-period attack could always begin immediately after departure. This mission also takes $n\geq2$ , ensuring another end node exists and the conditional attack event has positive probability under the admissible strategies.

Let $T_A$ be the first positive step at which the patroller, having just left $A$ for $C$ , returns to $A$ . The starting state $X_0=C$ is already the first period of absence. The interception probability is the paper's equation (17):

Q_{n,m}(p,s;A,d) =1-\frac{\Pr_C(T_A\geq d+m-1)}{\Pr_C(T_A\geq d)}.

The patroller maximizes $Q$ and the attacker minimizes it. A saddle point is a pair of strategies for which neither can improve by changing alone, with comparisons over all admissible $(p,s)$ and all end-node-and-delay pairs $(A,d)$ . A strategy is called optimal if it occurs in a saddle point. The source analyzes pure strategies in these parametric sets; a pure saddle remains a saddle if independent randomization of these strategies is permitted.

Formalization targets

Main theorem

Theorem 1 asserts that some optimal patroller strategy has $s=1$ and pairs with an attack at any end node with $d=2$ . It also asserts two exact uniqueness regimes:

\begin{aligned} &d=2\text{ is the only optimal delay}\quad\Longleftrightarrow\quad m\text{ is even},\\ &s=1\text{ is the only reflection probability of an optimal patroller strategy} \quad\Longleftrightarrow\quad m\geq3. \end{aligned}

The patroller's centre-to-end probability $p$ is selected optimally; it is not fixed in the main statement. The attack node is immaterial by symmetry, but it remains an explicit part of every attacker strategy. The theorem is posed over the full strategy sets, so its uniqueness assertions cannot be satisfied by restricting those sets to the displayed choices.

Cases and supporting targets

The milestone list follows the source's symmetry reduction, Lemmas 1–3, equations (3) and (15), and Propositions 1–2. For $m=2$ , Proposition 1 identifies $\hat p=1-\sqrt{n(n-1)}/n$ and the value $V=(2n-1)-2\sqrt{n(n-1)}$ . It also identifies optimal reflection probabilities below one. For odd $m$ , Proposition 2 identifies the unique optimal patroller strategy $(1/n,1)$ , permits every attacker delay, and gives

V=1-\left(\frac{n-1}{n}\right)^{(m-1)/2}.

For general even $m$ , the statement that an optimum has $np<1$ is recorded separately. It is needed to support the delay-uniqueness clause, while the paper illustrates this interior maximum numerically in Figure 2 rather than proving it as a numbered result.

What the result settles

The theorem reduces the strategic choices in this game: regardless of attack duration, delay two is an optimal response, and full reflection is compatible with an optimal patrol. The uniqueness clauses explain when alternatives are possible. With odd duration, the zero-holding random walk makes all delays equally good for the attacker. With duration two, a range of reflection probabilities below one remains optimal for the patroller. Those facts distinguish a recommendation that is optimal from one that is forced by the game.

The paper gives arguments for its numbered results, but this mission's Lean theorems are open statements awaiting machine-checked proofs. A completed development would provide a reusable finite-path model of conditional hitting probabilities and a formal game-theoretic treatment of the full delay set. The even-duration interior-maximizer milestone also calls for an analytic proof of a property that the preprint supports with plots. The finite-path and generic saddle-point definitions can be reused outside this particular star network.

Where the difficulty lies

The apparently direct comparison of attack delays fails because the patroller's state at attack start depends on surviving the entire waiting period without a return to $A$ . The conditional distribution at that start time changes with $d$ . Likewise, increasing reflection probability can change both the trajectory and the event on which the payoff is conditioned. A comparison of one-step transition probabilities alone does not establish a comparison of $Q$ . Exact uniqueness is more delicate still: at $np=1$ the chain alternates between centre and end nodes, creating genuine ties between delays for odd durations. The even-duration argument needs an optimum away from this boundary.

Formalization scope

Lean represents the original star as Option (Fin n), with none denoting $C$ and some i denoting end node $i$ . It builds finite-step taboo path probabilities and defines $Q$ by the ratio above, rather than by a closed-form solution or by the three-state reduction. The two-player saddle predicate is a separate generic definition; the paper-specific model supplies its strategy types and payoff. The definitions use real probabilities. The conditions $n\geq2$ , $m\geq2$ , $p>0$ , $np\leq1$ , $0<s\leq1$ , and $d\geq1$ are explicit. They make the relevant conditioning event nonempty and ensure the natural-number indices $d-1$ and $d+m-2$ mean the intended periods.

Lemmas 1–2 count the attack start as $X_1$ and count interception by $T(X)\leq m$ ; the model instead uses $X_0=C$ at departure and $m-1$ later transitions from the attack-start state. Lemma 3's printed claim that odd $m$ makes delay two uniquely optimal conflicts with Proposition 2 at $np=1$ . The milestone states a corrected strict claim under $np<1$ , for all $m$ , and records the discrepancy. Contributions to the model's finite-path identities, the three-state symmetry reduction, the numbered lemmas, the case propositions, and the even-duration interior maximum are all within scope.

Selected references

S. Alpern, P. Chleboun, and S. Katsikas, The Uniformed Patroller Game, arXiv:1908.07366v2, 2020, §§1–2, especially Theorem 1, p. 10. arXiv
S. Alpern, P. Chleboun, S. Katsikas, and K. Y. Lin, Adversarial Patrolling in a Uniform, Operations Research 70(1), 2022. This is the later journal version; the mission's page and result indices follow the preprint. DOI

12 thms2 active usersReviewed

Graph Theory Operations Research Probability·Captain: mikedeng1

A Dynamic Contagion Risk Model with Recovery Features: Fluid Limit for the Final Fraction of Failed Nodes in Threshold Contagion with Growth on the Configuration ModelResearch Paper

Motivation

Financial networks, supply chains and contact networks share a failure mode: a node fails when enough of its counterparties have failed, and its failure in turn weakens its own counterparties. Threshold contagion on random graphs is the standard mathematical model of this. Amini, Cont and Minca (Resilience to contagion in financial networks, Mathematical Finance 2016) proved that on a configuration-model network the final fraction of failed nodes concentrates, as the network grows, around an explicit value determined by the smallest fixed point of a one-dimensional map.

In that model thresholds are fixed. In practice institutions recover while a crisis unfolds: capital is raised, earnings accrue, and a node that survives long enough can absorb more losses than at the start. Amini, Minca and Sulem (A Dynamic Contagion Risk Model with Recovery Features, Mathematics of Operations Research 2022; the mission follows the authors' preprint of February 2021) add this recovery feature: every surviving node's threshold grows linearly in calendar time, at a rate proportional to its connectivity. The main result, Theorem 5, identifies the scaling limit of the cascade with growth. It is the basis of the paper's analysis of equilibrium connectivity choice (§3), where agents trade off the rewards of links against contagion risk.

Setting

A network has $n$ nodes. Node $i$ has a connectivity $\lambda_i\in\mathbb N$ (in-degree and out-degree both equal $\lambda_i$ ) and an integer initial threshold $\theta_i\in\mathbb N$ . The empirical type distribution is $\mu^{(n)}_{\lambda,\theta}=\#\{i:\theta_i=\theta,\lambda_i=\lambda\}/n$ and the mean connectivity is $\bar\lambda^{(n)}=\sum_{\lambda,\theta}\lambda\mu^{(n)}_{\lambda,\theta}$ . Two regularity conditions are assumed: (C1) $\mu^{(n)}_{\lambda,\theta}\to\mu_{\lambda,\theta}$ for a probability distribution $\mu$ on $\mathbb N^2$ ; (C2) $\bar\lambda^{(n)}\to\bar\lambda=\sum\lambda\mu_{\lambda,\theta}\in(0,\infty)$ .

Each node owns $\lambda_i$ out-going and $\lambda_i$ in-coming half-edges. The directed configuration model matches out-half-edges to in-half-edges by a uniformly random bijection; self-loops and multiple links are allowed.

The cascade: at time $0$ the nodes with $\theta_i=0$ fail. Interactions happen at times $T^{(n)}_k$ whose gaps are i.i.d. exponential with rate $n$ . At each interaction one unrevealed out-link of a failed node, chosen uniformly, is revealed; its counterparty $j$ gains one failed link and fails if its count of failed links reaches its current threshold $\theta_j+\alpha\lambda_jT^{(n)}_k/\bar\lambda^{(n)}$ , where $0<\alpha<1$ is the growth rate. Only surviving nodes grow. The cascade stops at $k^{(n)}_{\rm stop}$ , when no unrevealed failed link remains; $|\mathcal D^{(n)}_f|$ is the number of failed nodes and $S^{(n)}_{\lambda,\theta}(k^{(n)}_{\rm stop})$ the number of survivors of type $(\lambda,\theta)$ .

The limit objects: $P_{\lambda,\theta,\ell}(\pi)$ is the probability that the order statistics of $\ell$ i.i.d. uniform variables on $[0,\pi]$ satisfy $U_{(u)}>(u-\theta)/(\alpha\lambda)$ for $u=\theta+1,\dots,\ell$ ; $B^\alpha_{\lambda,0}=1$ and, for $\theta\ge1$ ,

B^\alpha_{\lambda,\theta}(\pi)=1-\sum_{\ell=0}^{\min\{\lceil\theta+\alpha\lambda\pi\rceil-1,\lambda\}}\binom{\lambda}{\ell}\pi^\ell(1-\pi)^{\lambda-\ell}P_{\lambda,\theta,\ell}(\pi);

$J^\alpha(\pi)=\sum_{\lambda,\theta}\lambda\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(\pi)/\bar\lambda$ ; and the relaxed fixed point $\pi^*=\min\{\pi\in[0,1]:J^\alpha(\pi)\le\pi\}$ .

Formalization targets

Goal: Theorem 5 (corrected)

With $L=\sum_{\lambda,\theta}\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(\pi^*)$ : for every $\varepsilon>0$ , with high probability $|\mathcal D^{(n)}_f|/n\ge L-\varepsilon$ . (i) If $\pi^*=1$ and $\mu_{0,\theta}=0$ for $\theta\ge1$ , then $|\mathcal D^{(n)}_f|/n\to1$ in probability. (ii) If $\pi^*<1$ is a stable fixed point ( $J^\alpha(\pi)<\pi$ just to the right of $\pi^*$ ), then

\frac{|\mathcal D^{(n)}_f|}{n}\xrightarrow{p}L,\qquad\frac{S^{(n)}_{\lambda,\theta}(k^{(n)}_{\rm stop})}{n}\xrightarrow{p}\mu_{\lambda,\theta}\big(1-B^\alpha_{\lambda,\theta}(\pi^*)\big).

Milestones

Lemma 16: a recursion in $\ell$ for $P_{\lambda,\theta,\ell}(t)$ , for $0<\alpha<1$ and $\theta<\ell\le\lambda$ , valid for $t\ge\hat t_{\lambda,\theta,\ell}=(\ell-\theta)\bar\lambda/(\alpha\lambda)$ .
Lemma 15: for $0<\alpha<1$ and $0<\theta\le\lambda$ , the piecewise linear system (DE) for the rescaled numbers of surviving nodes with $\ell$ failed links has a unique continuous solution on $[0,\bar\lambda)$ , in closed form.
(24)–(25): the limiting failed fraction of a class is $\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(t/\bar\lambda)$ , and the limiting number of unrevealed failed links is $\bar\lambda(J^\alpha(t/\bar\lambda)-t/\bar\lambda)$ .
(27)–(28): for $k=\gamma\bar\lambda^{(n)}n+o(n)$ , $T^{(n)}_k\to\gamma\bar\lambda$ in probability.
Remark 6: the minimum defining $\pi^*$ is attained.

Significance

Theorem 5 gives the final size of a cascade with recovery as an explicit function of the type distribution and the growth rate. The paper uses it to define each agent's expected reward as a function of its connectivity and to study the equilibrium of the resulting connectivity game (§3). Without the theorem, the equilibrium analysis would rest on the heuristic of §2.3 alone.

On the formal side, the platform has no random graph model of configuration type, no network contagion process and no fluid limit of a random cascade. This mission introduces all three. The result is proved on paper (by Wormald's differential-equation method); none of it is machine-checked. The work is to formalize the proof, and the milestones are self-contained pieces of it: an order-statistic identity, an explicit ODE solution, an algebraic identification of the limit, a concentration bound for sums of exponentials, and a fixed-point existence result.

Difficulty

The obvious approach is to view the cascade as a Markov chain in the counts of surviving nodes by type and number of failed links, and to apply Wormald's theorem directly. Two things break. First, with growth a node's survival depends on the whole history of its failed-link count, not on its current value, so the state space grows with time: new states become relevant at each growth time $\hat t_{\lambda,\theta,\ell}$ , and the fluid limit has to be established inductively on successive time intervals. Second, the cascade stops at a random time, near the first zero of the limiting number of unrevealed failed links. Showing that the stopping time concentrates requires the stability condition on $\pi^*$ and a truncation of the type distribution in the degree, since $\mu$ may have infinite support. The fixed point need not be a crossing point of a smooth map, so the identification of the stopping time is delicate even when the drift is known.

Formalization scope

Network. Half-edges of node $i$ are pairs $(i,a)$ with $a<\lambda_i$ ; the matching is a uniformly random permutation of the half-edges. Each $n$ has its own probability space: the matching, $m=n\bar\lambda^{(n)}$ i.i.d. $\mathrm{Exp}(n)$ gaps, and $m$ i.i.d. uniform variables on $[0,1)$ that choose the revealed link (uniform among the available ones given the past). The probability of an event averages over permutations the product law of gaps and choices. "With high probability" and "in probability" are stated with explicit $\varepsilon$ and limits of these probabilities.
Cascade. Computed step by step from the randomness and run for $m$ steps; $|\mathcal D^{(n)}_f|$ and $S^{(n)}_{\lambda,\theta}(k_{\rm stop})$ are read off the final state. A node fails when its failed links reach (not exceed) its threshold, as in every formula of the paper. Initially failed nodes are those with $\theta_i=0$ .
Limit objects. Order statistics are encoded by counting ( $U_{(u)}>s$ iff fewer than $u$ variables are $\le s$ ), and probabilities as Lebesgue measures of subsets of $[0,\pi]^\ell$ . Sums over types are tsums with summability hypotheses; $\mu$ is nonnegative with total mass $1$ .
Corrections, all labelled. (a) $B^\alpha_{\lambda,0}:=1$ ; the printed formula gives a value below $1$ for $\pi>0$ , contradicting the paper's p. 9, and makes the theorem false. (b) Part (i) assumes no isolated nodes with a positive threshold. (c) Lemma 16 assumes $t\ge\hat t_{\lambda,\theta,\ell}$ . (d) Lemma 15 is stated for $0<\theta\le\lambda$ , with uniqueness among continuous solutions, and reads the printed $\bar\lambda-u$ as $\bar\lambda-t$ . (e) (24) ends in $\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(t/\bar\lambda)$ , not $\mu_{\lambda,\theta}(1-B^\alpha_{\lambda,\theta}(t/\bar\lambda))$ . "Stable fixed point" means $J^\alpha(\pi)<\pi$ on some interval $(\pi^*,\pi^*+\eta)$ .
No trivialization. $|\mathcal D^{(n)}_f|$ and $S^{(n)}_{\lambda,\theta}$ are computed from the random matching, the gaps and the revelation order, never from $B^\alpha$ or $J^\alpha$ ; $\pi^*$ is defined from $\mu$ and $\alpha$ , not taken as a parameter.
Not included. Theorem 3 (the case $\alpha=0$ , cited from earlier work), the equilibrium results of §3, Wormald's theorem (Lemma 17, an external result), the in/out-degree extension (Theorem 18) and the displays (32)–(41) of the inductive argument.
Infrastructure. A complete proof needs Wormald's differential-equation method for Markov chains with bounded increments, concentration of the configuration model, and the elementary facts in the milestones. A general Wormald theorem and the configuration model are reusable well beyond this mission; contributions of either, as separate theorems, are welcome.

Selected references

H. Amini, A. Minca, A. Sulem, A dynamic contagion risk model with recovery features, Mathematics of Operations Research, 2022 (preprint February 2021). https://doi.org/10.1287/moor.2021.1174
H. Amini, R. Cont, A. Minca, Resilience to contagion in financial networks, Mathematical Finance, 2016. https://doi.org/10.1111/mafi.12051
N. C. Wormald, Differential equations for random processes and random graphs, Annals of Applied Probability, 1995. https://doi.org/10.1214/aoap/1177004612
L. Warnke, On Wormald's differential equation method, arXiv:1905.08928, 2019. https://arxiv.org/abs/1905.08928
B. Bollobás, A probabilistic proof of an asymptotic formula for the number of labelled regular graphs, European Journal of Combinatorics, 1980. https://doi.org/10.1016/S0195-6698(80)80030-8

10 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Maximizing Sequence-Submodular Functions and Its Application to Online Advertising: Any α-Greedy Sequence Achieves 1 − 1/e^α of the Optimum of a Non-Decreasing Sequence-Submodular FunctionResearch Paper

Motivation

Many allocation problems in online advertising are decisions about order, not only about membership. A search engine that rewrites an incoming query into one of several ad-matching configurations, or a publisher that runs a sequence of ad allocations over a day, extracts revenue that depends on which configurations are used and on the order in which they are applied: advertisers' budgets are spent down along the way, so a configuration run early changes what a later one can earn. Classical submodular set functions cannot express this order dependence, and the guarantees developed for them do not apply directly.

Alaei, Makhdoumi and Malekian (arXiv:1009.4153v4; Management Science, 2021) introduce sequence functions, which assign a value to every finite sequence of actions, and identify a sequence analogue of monotonicity and submodularity under which a simple greedy rule is provably near-optimal. They apply the discrete version to query rewriting in sponsored search and a continuous version to online ad allocation with budgets.

Timeline:

1978: Nemhauser, Wolsey and Fisher prove that the greedy algorithm achieves a $1-1/e$ fraction of the optimum for maximizing a monotone submodular set function under a cardinality constraint (Math. Programming 14).
2010–2021: Alaei, Makhdoumi and Malekian state the discrete and continuous sequence-submodular framework and prove the $1-1/e^{\alpha}$ guarantee for $\alpha$ -approximate greedy choices (arXiv first version 2010, journal version 2021).

Setting

Let $\mathcal S$ be a finite set of actions. A discrete sequence is a tuple $A=(s_1,\dots,s_k)$ with $k\ge0$ and every $s_i\in\mathcal S$ ; for $k=0$ it is the empty sequence $\emptyset$ . Its length is $|A|=k$ , and $\mathbb H^D(\mathcal S)$ denotes the set of all discrete sequences. The concatenation $A\perp B$ lists the elements of $A$ followed by those of $B$ . For $H=(s_1,\dots,s_T)$ the refinement $H_{[1,i]}=(s_1,\dots,s_i)$ is its prefix of length $i$ , with $H_{[1,0]}=\emptyset$ .

A sequence $A$ is dominated by $B$ , written $A\prec B$ , if $A$ can be obtained from $B$ by removing some of its elements while keeping the order of the remaining ones. Thus $(a,c)\prec(a,b,c)$ but $(c,a)\not\prec(a,b,c)$ .

A discrete sequence function is any $u:\mathbb H^D(\mathcal S)\to\mathbb R$ . The marginal value of appending $B$ after $A$ is

u(B\mid A)=u(A\perp B)-u(A).

The function $u$ is sequence-non-decreasing if $u(A)\le u(B)$ whenever $A\prec B$ , and $u(\emptyset)=0$ (display (10)). It is sequence-submodular if

u(C\mid A)\ \ge\ u(C\mid B)\qquad\text{for all }A,B,C\text{ with }A\prec B

(display (11)): appending the same sequence $C$ gains less after a longer history. Assumption 2 requires both properties.

The optimization problem (12) is, for a length budget $T\in\mathbb N$ ,

\max_{H\in\mathbb H^D(\mathcal S)}u(H)\quad\text{subject to}\quad|H|\le T.

For $\alpha\in[0,1]$ , a sequence $H=(s_1,\dots,s_T)$ is $\alpha$ -greedy if at every step its choice is within a factor $\alpha$ of the best single-action marginal value (display (13)):

u\big(s_i\mid H_{[1,i-1]}\big)\ \ge\ \alpha\max_{s\in\mathcal S}u\big(s\mid H_{[1,i-1]}\big)\qquad(i=1,\dots,T).

Formalization targets

Goal: Theorem 3 (p. 17)

Under Assumption 2, for every $\alpha\in[0,1]$ , every $\alpha$ -greedy $H$ of length $T$ and every sequence $O$ with $|O|\le T$ ,

u(H)\ \ge\ \Big(1-\frac1{e^{\alpha}}\Big)u(O).

Applied to the optimum $O$ of (12), this is the paper's display (14), $u(H)/u(O)\ge1-1/e^{\alpha}$ .

Milestones

Lemma 10 (p. 26): if $u$ is sequence-submodular, then for every $A$ and every nonempty $B$ there is $s\in\mathcal S$ with

u(s\mid A)\ \ge\ \frac1{|B|}\,u(B\mid A).

Eq. (38) (p. 26): for an $\alpha$ -greedy $H$ of length $k$ , every $O$ with $|O|\le k$ and every $i$ ,

u\big(s_i\mid H_{[1,i-1]}\big)\ \ge\ \frac{\alpha}{k}\Big(u(O)-u\big(H_{[1,i-1]}\big)\Big).

Eq. (41) (p. 27): under the same hypotheses,

u(H)\ \ge\ \Big(1-\Big(1-\frac{\alpha}{k}\Big)^k\Big)u(O).

Significance

For sets, the $1-1/e$ bound of Nemhauser, Wolsey and Fisher is the reference guarantee for greedy selection. Theorem 3 transfers it to sequences: any objective that can be shown sequence-non-decreasing and sequence-submodular inherits a $1-e^{-\alpha}$ guarantee for a greedy rule, with no further analysis. The paper uses this for query rewriting (Theorem 4) and, through the continuous analogue, for budgeted online ad allocation (Theorem 2). The parameter $\alpha$ covers the common situation in which the best next action can only be found approximately, for instance by solving a subproblem with an approximation algorithm.

Theorem 3 is proved in the paper. As far as a search of the Prove2Me catalog shows, no sequence-function model and no sequence-submodular greedy bound has been formalized there; set-function greedy bounds exist on the platform only as separate, set-based statements. This mission produces a machine-checked version of the discrete model and of the guarantee, which later missions on sequence or string submodularity can import.

Difficulty

The set-function argument compares the greedy set with the optimum by adding the optimum's elements one at a time to the current greedy set and using that the union is at least as valuable as the optimum. For sequences the comparison object is $H_{[1,i-1]}\perp O$ , and two features of the order break the direct transcription. First, sequence-submodularity only compares marginal values after a dominated history, so each comparison has to be arranged so that the shorter history is a subsequence of the longer one, in the right order. Second, the averaging over the elements of $O$ produces a factor $1/|O|$ , while the recursion needs the uniform factor $1/k$ ; the replacement relies on feasibility $|O|\le k$ together with nonnegativity of $u(O\mid H_{[1,i-1]})$ , which comes from monotonicity. A formal proof also has to handle the indices of the refinement and the edge cases $|O|=0$ , $k=0$ and $\alpha=0$ that the printed argument passes over.

Formalization scope

All declarations live in the namespace SeqSubmod.Discrete.

Sequences are Lean lists List S over a type S with [Fintype S]; concatenation is ++, the empty sequence is [], and $|A|$ is A.length.
Domination $\prec$ is List.Sublist (A <+ B), the subsequence order. It is neither the prefix order nor the subset order of the underlying sets.
marginal u B A := u (A ++ B) - u A is $u(B\mid A)$ , with the arguments in the paper's order.
Sequence-non-decreasing keeps the normalization $u(\emptyset)=0$ , so $u\ge0$ ; sequence-submodularity has the paper's direction.
The $\alpha$ -greedy condition uses Lean's 0-based indexing: H[i] is the paper's $s_{i+1}$ and H.take i is $H_{[1,i]}$ . The maximum over $\mathcal S$ is Finset.univ.sup', which needs [Nonempty S]. This is added and harmless: with no actions the only sequence is empty.
The optimum of (12) is not defined: the goal quantifies over every $O$ with $|O|\le|H|$ . This is equivalent to the statement about the optimum, which exists because there are finitely many feasible sequences.
The ratio (14) is stated in multiplied form, $(1-e^{-\alpha})\,u(O)\le u(H)$ , because the ratio is $0/0$ when $u(O)=0$ .
Lemma 10 adds $B\neq\emptyset$ , since $1/|B|$ is undefined at $|B|=0$ .

A trivializing formalization is ruled out: a prefix or subset order, a reversed (11), a dropped $u(\emptyset)=0$ , or an existentially quantified $O$ would each change the theorem, and none is used.

A complete development needs telescoping sums of marginal values along a list, an averaging argument over a finite sum, the recursion (40), and the inequality $(1-\alpha/k)^k\le e^{-\alpha}$ , which Mathlib provides. The definitions file is reusable by any later work on sequence functions, including the continuous model of the paper's §3, which is not part of this mission. Proofs of the milestones, alternative proofs of the goal, and tightness examples are all welcome contributions.

Selected references

S. Alaei, A. Makhdoumi, A. Malekian, Maximizing Sequence-Submodular Functions and Its Application to Online Advertising, Management Science, 2021; preprint arXiv:1009.4153v4 (2019). https://arxiv.org/abs/1009.4153
G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14, 265–294, 1978. https://doi.org/10.1007/BF01588971

5 thms2 active usersReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics CIII: Pension Death-in-Service, Death-in-Deferment, Survivor Benefits and Payment GuaranteesTextbook

Motivation

A defined benefit pension promises payments whose form depends on a member's employment and retirement status at death, and on the existence and later survival of a qualifying dependent. The same member can generate very different death benefits while employed, after leaving with preserved rights, or after retirement. A scheme may specify a salary-related lump sum before exit, a revalued preserved-rights benefit in deferment, a spouse's continuing pension after death, and instalments under a fixed pension guarantee. Coordination rules determine which payments coincide.

This mission formalises a finite-horizon actuarial contract in which the payable cash amounts and their dates follow explicit benefit switches, rather than being inferred from names such as “spouse's pension” or “death benefit”. The pension and multiple-state foundations are described by Dickson, Hardy and Waters (2020), Chapters 8–11, https://doi.org/10.1017/9781108784184. The contractual rules here are independently defined examples.

Scheme rules and governing documents determine legal entitlement and tax treatment. No salary multiple, spouse percentage, contribution refund or guarantee is universal.

Setting

Time is measured in integer anniversary ticks, numbered from valuation time zero. Let $h$ be a finite mortality horizon, $e$ the employment exit tick and $r$ the pension commencement tick. The coherent contract satisfies $e\leq r\leq h$ . A member death-year index $i<h$ means death occurs during $(i,i+1]$ and a death-related lump sum is paid at tick $i+1$ . The terminal index $i=h$ denotes no death within the observable horizon. A dependent's corresponding death index is $j$ , with the same convention. A same-tick death is treated as non-qualifying; within-year ordering needs a finer model.

The joint mortality law has masses $p_{ij}\geq0$ summing to one. At member death $i$ , $q_i\in[0,1]$ is the probability of a qualifying spouse, conditionally independent of the hypothetical dependent death index $j$ given $i$ . A spouse qualifies only when $j>i$ , then receives payments while $t\leq j$ . Eligibility is fixed at death; later mortality is checked at each due date.

An active death has $i<e$ , a deferred death has $e\leq i<r$ , and a retired death has $r\leq i<h$ . Define benefit amounts $L_{\text{A}}(i+1)$ , $L_{\text{D}}(i+1)$ and $L_{\text{R}}(i+1)$ at settlement for these disjoint regimes. The active benefit can include an optional salary multiple, an accrued-service amount and a contractual refund. The deferred death lump uses preserved annual pension multiplied by revaluation and an explicit pension-to-capital factor measured in years; any contribution refund is a separate cash amount. The retired benefit is a distinct lump-sum rider if the scheme provides one. No component is automatically cumulative with another merely because both appear in the model.

Let $b_t$ be the original member pension payable at anniversary $t\geq r$ , conditional on the member surviving that date. Let $s_{\text{A}}(i+1)$ , $s_{\text{D}}(i+1)$ and $s_{\text{R}}(i+1)$ be survivor pensions fixed from the death regime, with survivor indexation multiplier $u_t$ . The amounts can reflect salary or service to death, preserved rights, or a fraction of a retirement pension. The main survivor contract pays for $t>i+1$ ; a separate immediate alternative allows $t=i+1$ . Amounts are per instalment, with consistent monthly units when required.

A retirement guarantee of $g$ ticks covers pension due dates $r,r+1,\ldots,r+g-1$ . After a retired member dies, remaining guaranteed member instalments continue to the contractual recipient. Under the parallel rule the surviving spouse also receives its separately payable pension. Under the replacement rule the survivor pension is suppressed while the guarantee remains payable, then resumes when eligible after its expiry. A separate commutation switch can replace all unpaid estate-guaranteed instalments with one lump sum at death settlement, priced using consistent forward discount factors. No guarantee or payment alternative is universal.

Formalization targets

Mutually exclusive death states

Existing joint-life mathematics provides basic survivor occupancy identities. This mission extends them to the three death regimes. For $i<h$ and $e\leq r$ :

I_{\text{A}}(i)+I_{\text{D}}(i)+I_{\text{R}}(i)=1.

The indicators are pairwise disjoint, preventing multiple death-regime claims.

Death and subsequent pension cashflows

The second family constructs the realised present value $Z(i,j)$ for a full benefit contract from the paid lump sum and the dated instalments. Write $v_t$ for the discount factor to time zero and $C_t(i,j;\eta)$ for the sum of original member pension, qualifying survivor instalment and remaining guaranteed payment under replacement switch $\eta$ . Then

Z(i,j;\eta)=v_{i+1}L(i)+\sum_{t=0}^{n-1}v_t C_t(i,j;\eta).

The death lump is zero for the censored member state. The instalment horizon obeys $n\leq h+1$ in the root: right-censored members and spouses remain alive at every priced tick. Extension beyond $h$ needs a new mortality model.

Main capstone: event valuation and overlap

The principal target establishes an equality between mortality-event valuation and the payment-date component EPVs, together with a second equality accounting for guarantee coordination. With $V_{\text{event}}$ for expectation over the actual member and dependent death cells, $V_{\text{dated}}$ for the separately priced death, member, spouse and guarantee payment streams, and $O$ for the qualifying retiree-survivor pension suppressed during the guarantee:

V_{\text{event}}(\eta)=V_{\text{dated}}(\eta), \qquad V_{\text{event}}(\text{parallel}) =V_{\text{event}}(\text{replacement})+O.

The overlap is separately priced using $q_i$ , survivor mortality, death regime and payment eligibility. It is not introduced as a residual defined by subtracting two values.

Significance

The event-based formulation follows member status and the amount payable at death. The payment-date formulation uses explicit mortality conditions at each cashflow date, as in the valuation models of Dickson, Hardy and Waters (2020), Chapter 11, https://doi.org/10.1017/9781108784184. Agreement provides an auditable reconciliation between those independently constructed views. Where the spouse receives income while guaranteed member payments continue to an estate, valuing the two promises separately is appropriate. Where a contract suppresses that survivor pension, the overlap term quantifies the adjustment required to prevent charging for both.

Supporting targets cover exit, retirement and guarantee endpoints, and frozen survivor entitlement. Further results mix dependent-age mortality scenarios and value child pensions with an explicit cessation age.

Difficulty

A death benefit calculated from salary or preserved rights at a member's death differs from a pension instalment conditional on living at a subsequent payment date. Moving from a double sum over member and dependent death times to a sum over payment dates must respect that distinction. In particular, multiplying an unconditional probability of marriage at every later instalment would introduce a new eligibility test absent from the contract. The overlap between an estate guarantee and a spouse pension creates a second risk of overvaluation when the intended rule replaces one stream with the other.

Boundary cases are sensitive to strict and weak inequalities. A guarantee ending at $r+g$ has no payment at that endpoint under the due-in-advance anniversary convention adopted here. Same-grid member and dependent death is not automatically resolved by a continuous-time assumption. The project therefore has to distinguish mathematical cashflow identities, genuine survival-law properties and scheme-specific premises throughout its theorem graph.

Formalization scope

Lean 4 represents joint death-year cell masses and real-valued finite sums with targeted Mathlib imports. It supports arbitrary dependent-life mortality associations and user-supplied discount factors, salary schedules, preserved rights, revaluation multipliers and survivor indexation. Salary multiples, contribution refunds, deferred benefit valuations and retirement lump sums are switches or amounts supplied by a contract. The retirement guarantee has zero, parallel and replacement regimes. Payment streams may be represented on a finer integer grid to accommodate monthly schedules, but no mathematical identity in the annual kernel asserts exact continuous-payment equivalence.

The principal theorem assumes a normalised joint mortality law, $e\leq r\leq h$ , $n\leq h+1$ and $0\leq q_i\leq1$ . The event-to-payment equality follows from explicit realised payments, not a vacuous equality hypothesis, independence assumption or constant-rate restriction. It relies on genuine death-year and survivor eligibility indicators, rather than stipulating valuation equality in the hypotheses. Continuous-time integration and stochastic marital-history transitions remain future extensions. Finite spouse age-difference mixtures and age-limited child payments are included as separate supporting results. Statutory GMP/excess floors and pension tax rules are outside the contractual core until a scheme type and applicable legal basis are separately verified.

Selected references

David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, 2020, Chapters 8 (multiple state models), 9 (multiple decrements), 10 (joint-life benefits) and 11 (pension mathematics). https://doi.org/10.1017/9781108784184
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, John Wiley & Sons, 2015: §13.3.1 (DB pension plans), §§10.6–10.8 (two-life contracts), §§11.2–11.3 (multiple-decrement valuation) and §§19.1–19.2 (multi-state pension cashflows). https://books.google.com/books?id=gZ3mBQAAQBAJ

173 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Transmitting algebras through quantum channelsResearch Paper

Motivation

We develop a theory of exact transmission of finite-dimensional $C^*$ -algebras through quantum channels. These algebras describe hybrid classical-quantum information, allowing the dimension of the quantum system to depend on the classical message. Allowing arbitrary encodings and decodings yields a transmission set of algebra types, ordered by embedding, that unifies zero-error information theory with operator-algebraic error correction. We ask if this set admits a dominating algebra into which every transmittable algebra embeds. Our central finding is that domination can fail even in small dimensions. In its absence, several incomparable maximal algebras can describe different optimal uses of the same channel, forcing the user to select one depending on the operational task and the type of information to be preserved. We introduce hybrid capacities that reconstruct the only possible dominating algebra type and present a complete finite characterization of domination using minimal forbidden algebra types. We identify dominating algebras for channels whose operator systems are graph-isomorphic to $*$ -algebras, including highly divisible channels, and for channels with zero one-shot zero-error quantum capacity. Under tensor products, we prove that joint coding can produce new algebra types, giving an algebraic analogue of superadditivity from Shannon theory. Domination can fail for the joint use of two channels, even when both channels separately admit dominating algebras. Finally, we construct a channel whose $n$ -fold tensor powers have doubly exponentially many maximal algebra types, attaining the largest possible growth scaling for finite-dimensional channels. Consequently, new transmittable algebra types appear at arbitrarily large block-lengths for this channel, so its full transmission structure cannot be generated from any finite collection of bounded-block-length codes. △ Less

This mission is the statement-level formalization of Transmitting algebras through quantum channels (arXiv:2609.40054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main nonexistence result; Example 4.2 and (4.3) (Main nonexistence result; Example 4.2 and (4.3), PDF p. 30). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 4.20 and Definition 2.13, p.17: Canonical peripheral spectral projection P_Phi; support H0perp=im P_Phi(I); restricted channel and its adjoint image Xstar(Phi) with ordinary multiplication. (hard)

Selected references

Transmitting algebras through quantum channels, arXiv:2609.40054v1, https://arxiv.org/abs/2609.40054v1

53 thms2 active usersReviewed

Machine Learning Markov Chain Operations Research+1·Captain: mikedeng1

Learning Markov Models Via Low-Rank Optimization: KL Error Bound for the Rank-Constrained Maximum Likelihood Estimator of a Low-Rank Markov ChainResearch Paper

Motivation

Many systems studied in operations research and reinforcement learning are modelled as finite Markov chains with a large number of states $p$ : the stops of a taxi in a city, a random walk on a network, the conformations of a molecule. Estimating the $p\times p$ transition matrix from one observed trajectory needs, in general, a trajectory long compared with the $p^2$ unknown entries. In many such systems the transition matrix has, at least approximately, a small rank $r\ll p$ : the observed chain is driven by a low-dimensional latent process, as in state aggregation, where $\mathbb P(s_{t+1}\mid s_t)=\sum_z\mathbb P(z_t=z\mid s_t)\,\mathbb P(s_{t+1}\mid z_t=z)$ (Zhu, Li, Wang & Zhang, arXiv:1907.00113, §1.1). Zhu, Li, Wang and Zhang show that a low-rank transition matrix can be estimated from a trajectory whose length is proportional to $p$ (up to logarithmic factors), and they give two maximum-likelihood estimators with explicit rates. This mission formalizes the rate of the second, rank-constrained, estimator in Kullback–Leibler divergence.

Setting

Let $X_0,X_1,\dots,X_n$ be a Markov chain on the states $[p]=\{s_1,\dots,s_p\}$ with transition matrix $P$ ( $P_{ij}\ge0$ , $\sum_jP_{ij}=1$ , $P_{ij}=\mathbb P(X_1=s_j\mid X_0=s_i)$ ) and stationary distribution $\pi$ ( $\pi^\top P=\pi^\top$ ). The chain is primitive (some power of $P$ has all entries positive), and $X_0$ is drawn from $\pi$ . Write $\pi_{\min}=\min_j\pi_j$ and $\pi_{\max}=\max_j\pi_j$ .

The right spectral gap is $1-\rho_+$ , where, with $\langle h_1,h_2\rangle_\pi=\sum_jh_{1j}h_{2j}\pi_j$ and the adjoint $P^*=\mathrm{Diag}(\pi)^{-1}P^\top\mathrm{Diag}(\pi)$ ,

\rho_+=\sup_{\langle h,1\rangle_\pi=0,\ \langle h,h\rangle_\pi=1}\tfrac12\langle(P+P^*)h,h\rangle_\pi .

The KL divergence of a transition matrix $Q$ from $P$ is $D_{\mathrm{KL}}(P,Q)=\sum_{i,j}\pi_iP_{ij}\log(P_{ij}/Q_{ij})1_{\{P_{ij}\ne0\}}$ . From the trajectory, $n_{ij}$ counts the transitions $s_i\to s_j$ , and the averaged negative log-likelihood is $\ell_n(Q)=-\frac1n\sum_{i,j}n_{ij}\log Q_{ij}$ . The empirical KL divergence is $\widetilde D_{\mathrm{KL}}(P,Q)=\ell_n(Q)-\ell_n(P)$ .

Assumption 1 of the paper: $\operatorname{rank}(P)=r$ , and $P_{jk}\in\{0\}\cup[\alpha/p,\beta/p]$ for constants $\alpha,\beta>0$ . The $(\alpha/p)$ -minoration (Remark 2) removes the $0$ : $\alpha/p\le P_{jk}\le\beta/p$ for all $j,k$ . The rank-constrained MLE (5) is any

\widehat P^r\in\arg\min\big\{\ell_n(Q):\ Q1_p=1_p,\ \alpha/p\le Q_{ij}\le\beta/p,\ \operatorname{rank}(Q)\le r\big\}.

In Lean these objects are IsStochastic, IsStationary, IsPrimitive, piMin, piMax, trajProb, rhoPlus, klDiv, negLogLik, empKL, Assumption1, Minorated, RankFeasible and IsRankMLE in the namespace LowRankMarkov.RankMLE.

Formalization targets

Goal: Theorem 2, KL display (p. 10)

There are universal constants $C_1,C_2>0$ such that, for $p\ge2$ , under minoration with $\operatorname{rank}P=r$ and $n\pi_{\max}(1-\rho_+)>\max(20\log p,\log n)$ , every rank-constrained MLE satisfies, for all $\xi>0$ ,

\mathbb P\Big\{D_{\mathrm{KL}}(P,\widehat P^r)\ge\max\Big(\frac{C_1r\pi_{\max}\beta^2p\log p}{\pi_{\min}\alpha^3n},\ \frac{\xi\pi_{\min}}{rp\pi_{\max}\log p}\Big)\Big\}\le C_2e^{-\xi}.

The constants are not fixed numerically, so a sharper analysis does not invalidate the goal.

Milestones

Lemma EC.1, both forms: $D_{\mathrm{KL}}(u,v)\ge\frac{p\alpha}{2\beta^2}\|u-v\|_2^2$ for distributions with $u_j\in\{0\}\cup[\alpha/p,\beta/p]$ , $v_j\in[\alpha/p,\beta/p]$ , and its matrix form $\|P-Q\|_F^2\le\frac{2\beta^2}{\alpha\pi_{\min}p}D_{\mathrm{KL}}(P,Q)$ .
The rank remark (p. 14): $\operatorname{rank}(\widehat P^r-P)\le2r$ and $\|\widehat P^r-P\|_*\le(2r)^{1/2}\|\widehat P^r-P\|_F$ .
(EC.14): on the shell $Q\in\mathcal C(\eta)$ , $l\ge1$ and $2^{l-1}\eta\le D_{\mathrm{KL}}(P,Q)\le2^l\eta$ , $\|Q-P\|_*\le2\beta(2^l\eta r/(p\alpha\pi_{\min}))^{1/2}$ .
(EC.15), (EC.17): Bernstein-type tails $p^{-(\xi-1)}$ for $W^{(1)}_n=\max_j\sum_{i\le n}P_{X_{i-1},j}$ and $W^{(2)}_n=\max_j\sum_{i\le n}1_{\{X_{i-1}=s_j\}}$ .
Lemma 3: with probability at least $1-C_2\exp(-\eta\pi_{\max}rp\log p/\pi_{\min})$ , $|\widetilde D_{\mathrm{KL}}(P,Q)-D_{\mathrm{KL}}(P,Q)|\le\frac12D_{\mathrm{KL}}(P,Q)+C_1\pi_{\max}\beta^2rp\log p/(\pi_{\min}\alpha^3n)$ for every $Q\in\mathcal C$ with $D_{\mathrm{KL}}(P,Q)\ge\eta$ .
(EC.3): $\widetilde D_{\mathrm{KL}}(P,\widehat P^r)\le0$ . Together with $D_{\mathrm{KL}}(P,\widehat P^r)=\mathcal L(\widehat P^r)-\mathcal L(P)$ it gives (EC.4), $D_{\mathrm{KL}}(P,\widehat P^r)\le D_{\mathrm{KL}}(P,\widehat P^r)-\widetilde D_{\mathrm{KL}}(P,\widehat P^r)$ .

Significance

The bound says that, with high probability, the KL error of $\widehat P^r$ is of order $rp\log p/n$ up to the factors $\pi_{\max}/\pi_{\min}$ and $\beta^2/\alpha^3$ , plus a term independent of $n$ controlled by $\xi$ . A trajectory of length of order $rp\log p$ , rather than $p^2$ , therefore suffices: the low rank is what makes the estimation problem sample-efficient. Lemma EC.1 converts the KL bound into a Frobenius-norm bound, and Lemma 3 is a uniform law for the empirical KL process of a dependent sequence over the paper’s cone class.

The result is proved in the paper; nothing in it has been machine-checked. The mission asks for a formal proof of the KL display. Two points need care beyond transcription: the printed hypotheses do not suffice (see Formalization scope), and the paper's proof of Lemma 3 symmetrizes the dependent summands as if they were independent (EC.8), so a formal proof must supply a valid argument for that step.

Difficulty

Comparing $\ell_n(\widehat P^r)$ with $\ell_n(P)$ is immediate; the difficulty is to control $\widetilde D_{\mathrm{KL}}-D_{\mathrm{KL}}$ uniformly over a non-convex set of matrices, from one dependent trajectory. A union bound over a net of the feasible set loses polynomial factors in $p$ , and i.i.d. empirical-process tools do not apply directly to a Markov chain. The printed Lemma 3 covers the cone class $\mathcal C$ , while the appendix proof restricts its shells to rank- $r$ matrices. This leaves a gap for matrices in $\mathcal C$ of higher rank and for the claimed application to $\widehat P^r$ when $r>16$ . The paper combines a tail inequality for suprema of empirical processes of Markov chains (Adamczak 2008), a contraction step, the matrix Freedman inequality (Tropp 2011) for a matrix martingale, and a Bernstein inequality for Markov chains with a spectral gap (Jiang, Fan & Sun 2018) for the quadratic variations $W^{(1)}_n,W^{(2)}_n$ . None of these is in Mathlib.

Formalization scope

States are Fin p, matrices Matrix (Fin p) (Fin p) ℝ, logarithms natural. A trajectory $x=(X_0,\dots,X_n)$ makes $n$ transitions, and its probability is $\pi(x_0)\prod_{k<n}P_{x_kx_{k+1}}$ ; probabilities of events are finite sums, so no measure theory is needed. $\rho_+$ is a real sSup; " $\rho_+<1$ " is not built into its definition. The nuclear and Frobenius norms come from the published definition CaiCandesShen.Convergence.Basic.

Hypotheses fixed relative to the page:

Minoration instead of Assumption 1(ii), in the goal and (EC.3). The printed Theorem 2 allows $P_{jk}=0$ , and it is false then. For even $p$ , let rows $1,\dots,p/2$ of $P$ equal $2/p$ on columns $p/2+1,\dots,p$ and $0$ elsewhere, and rows $p/2+1,\dots,p$ equal $1/p$ . Then $\operatorname{rank}P=2$ , $\alpha=1$ , $\beta=2$ , $\rho_+=0$ , $\pi$ puts mass $1/3$ on the first half and $\pi_{\max}/\pi_{\min}=2$ . Every feasible $Q$ has $Q_{ij}\ge1/p$ , so on each of the first $p/2$ rows $Q$ puts mass at most $1/2$ on the support of $P$ , and $D_{\mathrm{KL}}(P,Q)\ge\frac13\log2$ . With $\xi=0.9\,p\log p$ the threshold is below $\frac13\log2$ for all large $n$ , so the probability is $1$ , while $C_2e^{-\xi}<1$ for large $p$ . The broken step is (EC.3), which needs $P$ feasible for (5); minoration with $\operatorname{rank}P=r$ makes it feasible. Lemma EC.1, (EC.14), (EC.15), (EC.17) and Lemma 3 keep the printed Assumption 1.
$X_0\sim\pi$ , stated in Theorem 1 and used by the proof of Theorem 2 through Lemma 3.
Ergodic is read as primitive; $\pi_i>0$ is stated (it is implied); $p\ge2$ keeps $\log p>0$ in denominators.
Lemma 3's set is the printed $\mathcal C(\eta)$ , whose cone is $\|Q-P\|_*\le4\times2^{1/2}\|Q-P\|_F$ and which has no rank constraint. The appendix proof uses rank-restricted shells; for $r>16$ the rank remark alone does not place $\widehat P^r$ in $\mathcal C$ . This is a proof gap, while the formal statement retains the page's quantification.
Lemma EC.1's matrix form and (EC.14) include the printed cone condition. (EC.14) is stated pointwise for members of $\mathcal C_l$ .

The statements rule out trivializing readings: $C_1,C_2$ are quantified before all data; the goal holds for every selection of minimizers, not for one fixed estimator; $p\ge2$ and $\pi>0$ exclude the junk values $x/0=0$ and $\log1=0$ that would collapse the thresholds; a sorry-free check shows the goal's hypotheses are jointly satisfiable ( $p=2$ , uniform $P$ , $n=28$ ).

Not posed: Theorem 1 (nuclear-norm MLE), the Frobenius display of Theorem 2 (Lemma EC.1 turns the KL threshold into twice the printed Frobenius threshold, so the paper's one-line derivation gives $C_2e^{-\xi/2}$ ), Theorem 3 (lower bound), and the DC-programming results of §4. Useful reusable contributions: a Bernstein inequality for finite Markov chains with a spectral gap, the matrix Freedman inequality, and the reverse-Pinsker bound of Lemma EC.1.

Selected references

Z. Zhu, X. Li, M. Wang, A. R. Zhang, Learning Markov models via low-rank optimization, Operations Research, 2022; preprint arXiv:1907.00113v2, 2020. https://arxiv.org/abs/1907.00113
B. Jiang, J. Fan, Q. Sun, Bernstein's inequality for general Markov chains, arXiv:1805.10721, 2018. https://arxiv.org/abs/1805.10721
J. A. Tropp, Freedman's inequality for matrix martingales, Electronic Communications in Probability 16:262–270, 2011. https://arxiv.org/abs/1101.3039
R. Adamczak, A tail inequality for suprema of unbounded empirical processes with applications to Markov chains, Electronic Journal of Probability 13(34):1000–1034, 2008. https://arxiv.org/abs/0709.3110
J. A. Fill, Eigenvalue bounds on convergence to stationarity for nonreversible Markov chains, with an application to the exclusion process, The Annals of Applied Probability 1(1):62–87, 1991. https://doi.org/10.1214/aoap/1177005981

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

“Now or Later?” When to Deploy Qualification Screening in Open-Bid Auction for Re-Sourcing: The Incumbent's Optimal Drop-Out Price Is a Compete-or-Fold Threshold RuleResearch Paper

Motivation

Firms that already buy a service from an incumbent supplier regularly re-source the contract: they invite new suppliers, the entrants, to compete in a descending open-bid auction. Entrants may be cheaper but are unproven: before the contract can be awarded to an entrant, the buyer must pay for qualification screening (visits to the supplier's facility, purchasing and testing sample products), and an entrant passes only with some probability. Industry practice splits into screening every entrant before the auction (pre-qualification) and screening only the winner after it (post-qualification). Zhang, Chen and Katok, “Now or Later?” When to deploy qualification screening in open-bid auction for re-sourcing, Operations Research 69(6), 2021, compare the two formats in equilibrium.

In the post-qualification format (POST), the incumbent needs no screening, so he faces a genuine dynamic decision: as the clock price falls and entrants drop out, when should he quit? His drop-out price determines the buyer's procurement cost in POST, and Theorem 2 of the paper characterizes it completely. This mission formalizes that theorem.

Setting

Costs lie in an interval $[\underline R,\overline R]$ . The incumbent's cost is $x_0\in[\underline R,\overline R]$ . There are $N\ge2$ entrants with i.i.d. costs of density $f_e$ and c.d.f. $F_e$ , supported on $[\underline R,\overline R]$ . Screening one entrant costs the buyer $K>0$ , and an entrant passes with probability $\beta\in(0,1)$ . In POST, the clock descends from $\overline R$ ; when the incumbent drops out at price $b$ , the price jumps down by the decrement $\Delta:=K/\beta$ , and the incumbent ends up with the contract at price $b$ only if all remaining entrants fail screening. The paper assumes $\Delta<\overline R-\underline R$ and Assumption 1: $F_e/f_e$ is nondecreasing and convex.

Before the incumbent quits, an entrant with cost $x_j$ stays until the price reaches his effective cost $x_j+\Delta$ . With $m$ entrants left at price $p$ , the highest remaining entrant cost therefore has c.d.f. $G^m_e(z;p-\Delta)=[F_e(z)/F_e(p-\Delta)]^m$ and density $g^m_e$ . Writing $\ell(x_0)=\max\{\underline R+\Delta,x_0\}$ , the incumbent's value $V^m_0(x_0,p)$ solves the Bellman system (8)–(10):

\Pi^m_0(b;x_0,p)=\int_b^p V^{m-1}_0(x_0,z)\,g^m_e(z-\Delta;p-\Delta)\,dz+G^m_e(b-\Delta;p-\Delta)(1-\beta)^m(b-x_0),

V^m_0(x_0,p)=\max_{b\in[\ell(x_0),p]}\Pi^m_0(b;x_0,p),\qquad V^0_0(x_0,p)=p-x_0 .

Here $b$ is the planned drop-out price. The integral covers the event that an entrant drops out first, at price $z$ ; the second term covers the event that the incumbent quits at $b$ and all $m$ entrants then fail screening.

Theorem 2 introduces four objects. $m^\star(x_0)$ is the floor of the minimum over $b$ of $(1-\beta)F_e(b-\Delta)/(\beta(b-x_0)f_e(b-\Delta))$ . The compete threshold $b^\star_m(x_0)$ is the first price at which $H(b)=F_e(b-\Delta)/f_e(b-\Delta)$ falls below $L^m(b;x_0)=m\beta(b-x_0)/(1-\beta)$ . The switching price $p^\star_m(x_0)$ is the least price above $b^\star_m(x_0)$ at which quitting is worth as much as competing down to $b^\star_m(x_0)$ . The candidate drop-out rule is $s^\star_m(x_0;p)$ .

Formalization targets

Goal: Theorem 2

For all $x_0\in[\underline R,\overline R]$ , $1\le m\le N$ and $p\ge\ell(x_0)$ :

s^\star_m(x_0;p)=\begin{cases}b^\star_m(x_0)\wedge p,& m>m^\star(x_0),\ p\le p^\star_m(x_0),\\ p,&\text{otherwise}\end{cases}\quad\text{maximizes } b\mapsto\Pi^m_0(b;x_0,p)\text{ on }[\ell(x_0),p],

and $V^m_0(x_0,p)=\Pi^m_0(s^\star_m(x_0;p);x_0,p)$ . The goal also asserts that $m^\star,b^\star_m,p^\star_m$ are well defined and satisfy $p^\star_m>b^\star_m\ge x_0$ . It asserts the monotonicity of part (i): $m^\star$ and $b^\star_m$ are nondecreasing in $x_0$ , $b^\star_m$ is nonincreasing in $m$ , and $p^\star_m$ is nonincreasing in $x_0$ and nondecreasing in $m$ . Finally, $s^\star_m(x_0;p)$ is nondecreasing in $x_0$ and $p$ and nonincreasing in $m$ .

Milestones

The proof in the e-companion (pp. ec5–ec11) provides the milestones, in attack order:

the drop-now value $(1-\beta)^m(p-x_0)\le V^m_0(x_0,p)$ ;
the derivative formula (EC.7) with its bound $\zeta^m$ ;
the factorization (EC.8)–(EC.9) of $\zeta^m$ through $H-L^m$ ;
well-definedness of $b^\star_m$ and $p^\star_m$ ;
Lemma EC.1 (a)–(d);
Claim EC.1, the sign pattern of $\zeta^m$ ;
Lemma EC.2, the induction behind the monotonicity of $p^\star_m$ ;
the fold-only case $m\le m^\star(x_0)$ .

Significance

The theorem turns an infinite-horizon-looking stopping problem into a compete-or-fold rule. Either the incumbent stays in until the price falls to the threshold $b^\star_m(x_0)$ , or he drops out immediately. The choice depends only on how many entrants remain and on whether the price is above the curve $p^\star_m(x_0)$ . With Lemma 2 and Theorem 1 (the entrants' strategies), this completes the equilibrium of POST. The paper's comparison of POST and pre-qualification, and its closed form for the buyer's expected cost, both rest on this equilibrium.

The result is proved in the paper; it has not been machine-checked. A formal proof would check a long argument with an intricate induction: Lemma EC.2 interleaves the strict monotonicity of $\Pi^{m'}_0$ with the monotonicity of $p^\star_{m'}$ in $m'$ and $x_0$ . It would also check the treatment of the boundary case $x_0=\underline R+\Delta$ , where the proof appeals to the convexity in Assumption 1.

Difficulty

The obvious argument differentiates $\Pi^m_0$ in $b$ and reads off the sign. That fails because the derivative involves $V^{m-1}_0(x_0,b)$ , which is itself the value of an optimization. Its sign is controlled by the explicit function $\zeta^m$ only after an induction on $m$ shows that $V^{m-1}_0$ has the form $(1-\beta)^{m-1}(b-x_0)$ wherever it matters. The induction must carry the ordering of $b^\star$ , $b^{\star\star}$ and $p^\star$ across different $m$ and $x_0$ (Claim EC.1) at the same time. Another difficulty is that $\Pi^m_0$ must be evaluated beyond the current price: $p^\star_m(x_0)$ is defined at the reference price $\overline R+\Delta$ and may exceed $p$ .

Formalization scope

All prices and costs are real numbers, and $m$ is a natural number with $1\le m\le N$ . The standing assumptions (including Assumption 1) are hypotheses of every statement. One hypothesis is added to the page: $f_e$ is positive and continuous on $[\underline R,\overline R]$ . The page's own formulas divide by $f_e(b-\Delta)$ and differentiate (9) in $b$ . $\Delta$ is defined as $K/\beta$ , not taken as a parameter, and $F_e$ is the integral of $f_e$ .

The max in (8) is a real supremum over the compact feasible interval; that it is attained is part of the goal. The integral in (9) is a signed interval integral, so $\Pi^m_0(b;x_0,p)$ is given by (9) for $b>p$ as well. The minimum defining $m^\star$ is read as an infimum over $(\max\{x_0,\underline R+\Delta\},\overline R+\Delta]$ , because the ratio has a zero denominator at $b=x_0$ . The page's $(b^\star_m,\infty]$ is taken over the reals. "Optimal drop-out price" means a maximizer in (8): at $p=p^\star_m(x_0)$ two maximizers exist, so uniqueness would be false. The derivative (EC.7) is stated away from the kink $b=\overline R+\Delta$ . Milestones use the open price domain $p>\ell(x_0)$ the proof uses.

The game-theoretic layer is not modelled. The hypothesis "entrants follow Lemma 2 and Theorem 1" is how the page derives (8)–(10), and the statement is about (8)–(10). A formalization that states only the sign pattern of $\zeta^m$ or the inductive hypothesis $\mathbb H^m$ would be trivializing; the goal states optimality of $s^\star_m$ in (8) for every $m$ , $x_0$ , $p$ , together with part (i).

A development needs differentiation under a parametrized integral (the fundamental theorem of calculus for $\int_b^p$ ), continuity of $V^m_0$ in $p$ , and real-analysis facts about convex functions crossing a line. These are reusable for other auction and optimal-stopping models. Proofs of any milestone are welcome, as are proofs of the fold-only case independently of the compete case.

Selected references

W. Zhang, Q. (George) Chen, E. Katok, “Now or Later?” When to deploy qualification screening in open-bid auction for re-sourcing, Operations Research 69(6):1715–1733, 2021. https://doi.org/10.1287/opre.2021.2111 (accepted manuscript: LBS Research Online eprint 1542, https://lbsresearch.london.edu/id/eprint/1542/)

14 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Co-Opetition in Service Clusters with Waiting-Area Entertainment: With an Even Cost Split, Co-Opetition Is at Least as Profitable as Local Monopoly iff Price Competition Is Below a ThresholdResearch Paper

Motivation

Restaurants, clinics and amusement venues that announce a waiting-time standard compete not only on price but on how unpleasant the wait feels. Waiting-area entertainment (a piano player, a television, a play area) lowers the perceived cost of waiting, and when several providers sit in one service cluster, a food court, a mall, a strip of restaurants, a single entertainment option can serve all of their customers at once. Yuan, Dai, Chen and Gavirneni (MSOM 2021) model this choice and ask when providers that compete on price but jointly fund entertainment, a form of co-opetition, do better than a single provider serving the market alone.

The model builds on the waiting-time-standard and volume-based capacity framework of Allon and Federgruen (Operations Research 2007) and on linear cost-allocation schemes of the yardstick type. Its central comparison concerns the even cost split: does sharing the entertainment bill outweigh the margin lost to price competition?

Setting

Customers arrive at a provider as a Poisson stream and the service time is exponential. With service fee $p$ and entertainment level $\alpha\ge0$ , a local monopolist faces the arrival rate

\lambda(p,\alpha;w)=B-hw\,e^{-\delta\alpha}-\beta_0p ,

where $B>0$ is the maximum demand rate, $\beta_0>0$ the price sensitivity, $h>0$ the waiting cost per unit time, $w>0$ the announced waiting-time standard and $\delta>0$ the effectiveness of entertainment. Entertainment costs $C(\alpha)=\tfrac12c\alpha^2$ with $c>0$ . To keep the expected wait at $w$ the provider buys service rate $\mu=\lambda+1/w$ at marginal cost $\gamma\ge0$ , so its profit is

\Pi(p,\alpha)=p\,\lambda(p,\alpha;w)-C(\alpha)-\gamma\mu .

The monopoly profit $\Pi^M$ is the greatest value of $\Pi$ over $p\ge\gamma$ , $\alpha\ge0$ .

Under co-opetition two symmetric providers share one entertainment level. Write $A=B-\beta_0\gamma$ , $D(\alpha)=A-hw\,e^{-\delta\alpha}$ , margins $P_i=p_i-\gamma$ , a price-competition intensity $\theta\ge0$ and $\beta=\beta_0+\theta$ . Provider $i$ 's arrival rate is $\lambda_i=D(\alpha)-\beta P_i+\theta P_j$ . The cost is split by $\phi(\lambda_i,\lambda_j)=\tfrac12+t(\lambda_i-\lambda_j)$ with cost-sharing factor $t\ge0$ , and provider $i$ earns

\Pi_i=\pi(\alpha,P_i,P_j)=P_i\lambda_i-\phi(\lambda_i,\lambda_j)C(\alpha)-\gamma/w .

Providers first set margins simultaneously; then they jointly choose $\alpha\ge0$ to maximize $\Pi_1+\Pi_2$ . A symmetric equilibrium $(P^O,\alpha^O)$ has $P^O\ge0$ , $\alpha^O$ jointly optimal at $(P^O,P^O)$ , and no deviation $P'\ge0$ , followed by the joint optimum it induces, raises a provider's profit. The equilibrium profit is $\Pi^O=\pi(\alpha^O,P^O,P^O)$ . Throughout, the parameters satisfy $2\beta_0c-\delta^2(B-\beta_0\gamma)^2\ge0$ and $\beta_0\gamma<B-hw$ .

Formalization targets

Goal: Proposition 7(ii)

With an even split ( $t=0$ ) there is a threshold $\theta^c\ge0$ such that, for every $\theta\ge0$ and every symmetric equilibrium at $\theta$ ,

\theta\le\theta^c\ \Rightarrow\ \Pi^O(\theta)\ge\Pi^M,\qquad \theta>\theta^c\ \Rightarrow\ \Pi^O(\theta)<\Pi^M .

No value of $\theta^c$ is fixed: the goal asserts only the threshold shape of the comparison.

Milestones

Proposition 1. The monopoly optimum exists, is unique, and is given by the unique root $\alpha^M\ge0$ of

\delta hw\bigl(B-hw e^{-\delta\alpha}-\beta_0\gamma\bigr)-2\beta_0c\,\alpha e^{\delta\alpha}=0

and $p^M=(B-hw e^{-\delta\alpha^M}+\beta_0\gamma)/(2\beta_0)$ . 2. Proposition 3(i) at $t=0$ . A symmetric equilibrium exists, and every one satisfies

2D(\alpha^O)hw\delta-(2\beta_0+\theta)c\,\alpha^Oe^{\delta\alpha^O}=0,\qquad P^O=\frac{D(\alpha^O)}{2\beta_0+\theta}.

Proposition 3(ii) at $t=0$ . $\lambda^O=(\beta_0+\theta)D(\alpha^O)/(2\beta_0+\theta)$ , $\Pi^O=P^O\lambda^O-C(\alpha^O)/2-\gamma/w$ , $\rho^O=1-1/(w\lambda^O+1)$ , and each cost share is $\tfrac12$ .
Proposition 7(i). At $t=0$ , $\alpha^O$ , $p^O$ and $\Pi^O$ strictly decrease in $\theta$ .

Significance

The result separates two effects of clustering. Sharing one entertainment option halves each provider's cost, which supports a higher entertainment level and more demand; price competition erodes margins. Proposition 7(ii) says that, under an even split, the comparison with a local monopolist is decided by a single cut-off in the competition intensity, which is what lets the paper conclude that co-opetition can restore monopoly profit levels when competition is mild, and it is the reference point for the paper's analysis of unequal cost-sharing rules (Propositions 6 and 8) and of the design of cost allocation.

The paper's proofs sit in an online supplement; no machine-checked proof of any of these statements is known. Formalizing them produces a verified analysis of a two-stage game with a joint second stage, including the existence of the symmetric equilibrium, which the paper uses but which requires a global, not first-order, argument.

Difficulty

The co-opetition equilibrium is defined by a two-stage game: a price deviation changes the jointly chosen entertainment level, so a provider's payoff as a function of its own price is a composition with an argmax and need not be concave. Verifying that the first-order point of Proposition 3 is a global best response, and that every symmetric equilibrium satisfies the first-order conditions, is the step a direct first-order computation does not deliver. The threshold of Proposition 7(ii) then requires comparing an implicitly defined equilibrium profit, through its root equation in $\alpha$ , with the implicitly defined monopoly optimum, and showing that the difference changes sign exactly once in $\theta$ ; monotonicity of $\Pi^O$ alone does not give a sign change.

Formalization scope

Everything is real-valued. Prices are encoded by margins $P=p-\gamma\ge0$ , for the equilibrium and for every deviation, matching the page's domain $p\ge\gamma$ . The joint entertainment stage maximizes over $\alpha\ge0$ , and a deviation is evaluated at every joint optimum it induces. $\Pi^M$ is any greatest element of the set of monopoly profits over $p\ge\gamma$ , $\alpha\ge0$ . The goal and milestones fix $t=0$ ; Proposition 3 for $t>0$ is out of scope.

Disclosed conventions: the capacity bound is the strict $\beta_0\gamma<B-hw$ instead of the page's $\gamma\le(B-hw)/\beta_0$ (at equality a degenerate profile with zero margins and no entertainment makes both profits equal to $-\gamma/w$ and falsifies the strict clause); the demand is read as $D(\alpha)-\beta P_i+\theta P_j$ , as in §3 and Proposition 3(ii), since the §4 display double-counts $\theta$ ; the cost share is read as $\tfrac12+t(\lambda_i-\lambda_j)$ , the first of the page's two inconsistent forms (they agree at $t=0$ ); "decrease" is strict; "the opposite holds" is the strict $\Pi^O<\Pi^M$ .

The goal is stated about genuine equilibria of the game and the genuine monopoly optimum. Replacing $\Pi^O$ by the closed form of Proposition 3, or $\Pi^M$ by the formula of Proposition 1, would turn the goal into a one-variable real-analysis fact and is not the paper's statement.

A complete development needs: the monopoly first-order analysis (joint concavity on $p\ge\gamma$ , $\alpha\ge0$ ); strict concavity of the joint second stage for positive total margin; the envelope argument for a provider's deviation; existence of a symmetric equilibrium; implicit-function comparative statics in $\theta$ . Lemmas on implicitly defined roots of $x\mapsto a e^{-\delta x}-b x e^{\delta x}$ type equations are reusable. Contributions of intermediate lemmas, including the existence of the equilibrium, are welcome.

Selected references

X. Yuan, T. Dai, L. G. Chen, S. Gavirneni, Co-opetition in service clusters with waiting-area entertainment, Manufacturing & Service Operations Management 23(1):106–122, 2021. https://doi.org/10.1287/msom.2019.0815
G. Allon, A. Federgruen, Competition in service industries, Operations Research 55(1):37–55, 2007. https://doi.org/10.1287/opre.1060.0329
E. J. Friedman, H. Moulin, Three methods to share joint costs or surplus, Journal of Economic Theory 87(2):275–312, 1999. https://doi.org/10.1006/jeth.1999.2534

6 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Financial Intermediation Chains in an Over-the-Counter Market: For Search Costs Below the Threshold c*, There Is a Unique Steady-State Equilibrium with an Intermediary SectorResearch Paper

Motivation

Many financial assets (corporate and municipal bonds, swaps, asset-backed securities) trade over the counter (OTC): there is no central exchange, and a trade requires that a buyer and a seller find each other. Empirically, a large share of OTC volume passes through intermediation chains, in which an asset moves from the original seller to the final buyer through several dealers. Search-theoretic models explain how such chains form. Duffie, Gârleanu and Pedersen (2005) introduced continuous-time search and bargaining in OTC markets, and Hugonnier, Lester and Weill (2016) let investors' valuations take a continuum of values, so that dealers emerge endogenously as the investors with intermediate valuations.

Shen, Wei and Yan add a search cost: an investor who looks for a trading partner pays a flow cost $c$ . Investors with extreme valuations then prefer to stay out of the market, and participation becomes an equilibrium choice. The paper's Theorem 1 is the foundation of everything that follows in it: every proposition on chain length, trading volume, price dispersion and welfare is stated "in the equilibrium of Theorem 1".

Setting

Time is continuous. A continuum of investors of total mass $N$ trades an asset in supply $X$ , with $0 < X < N$ ; each investor holds $0$ or $1$ unit, and the asset pays a coupon of $1$ per unit of time. An investor of type $\Delta \in [0, \bar\Delta]$ values the coupon at $1 + \Delta$ . Types are redrawn independently at intensity $\kappa > 0$ from a probability density $f$ on $[0, \bar\Delta]$ with c.d.f. $F$ . Everyone discounts at rate $r > 0$ .

A non-owner either stays out or searches to buy; an owner either stays out or searches to sell. Searching costs $c \ge 0$ per unit of time. Write $\mu_b, \mu_s, \mu_n, \mu_h$ for the densities over types of buyers, sellers, inactive non-owners and inactive holders, and $N_b = \int_0^{\bar\Delta}\mu_b$ , $N_s = \int_0^{\bar\Delta}\mu_s$ . A buyer meets sellers at rate $\lambda N_s$ and a seller meets buyers at rate $\lambda N_b$ , with $\lambda > 0$ .

Let $V_h, V_s, V_n, V_b$ be the values of the four activities, $V(0,\Delta) = \max(V_n, V_b)$ and $V(1,\Delta) = \max(V_h, V_s)$ . When a type- $x$ buyer meets a type- $y$ seller, the surplus is

S(x,y) = [V(1,x) + V(0,y)] - [V(0,x) + V(1,y)],

they trade iff $S(x,y) > 0$ , and the buyer, with bargaining power $\eta \in (0,1)$ , pays $P(x,y) = V(1,x) - V(0,x) - \eta S(x,y)$ .

For cutoffs $\Delta_b$ , $\Delta_s$ , non-owners search to buy iff $\Delta > \Delta_b$ and owners search to sell iff $\Delta < \Delta_s$ . A steady-state intermediation equilibrium (Definition 1) consists of cutoffs $0 < \Delta_b < \Delta_s < \bar\Delta$ , densities satisfying the flow balances (12)–(18) and market clearing (19), and value functions solving the Bellman system (8)–(11) under which these cutoff rules are optimal. Types in $(\Delta_b, \Delta_s)$ are the intermediaries: they search to buy when they hold nothing and search to sell as soon as they hold the asset.

Formalization targets

Goal: Theorem 1

There is an explicit threshold $c^*$ , built from the right-hand sides of the cutoff equations

c = \frac{\lambda\kappa\eta X}{[\kappa + r + \lambda N_b(1-\eta)](\kappa + \lambda N_b)}\int_0^{\Delta_b}F(x)\,dx, \qquad (20)

c = \frac{\lambda\kappa(1-\eta)(N-X)}{(\kappa + r + \lambda\eta N_s)(\kappa + \lambda N_s)}\int_{\Delta_s}^{\bar\Delta}[1-F(x)]\,dx, \qquad (21)

with $N_b$ , $N_s$ the explicit functions (66), (64) of $F(\Delta_b)$ , $F(\Delta_s)$ , such that for

0 < c < c^*

a steady-state intermediation equilibrium exists, and every such equilibrium has cutoffs equal to the unique roots of (20) and (21), densities (55)–(63), value functions (79)–(82), and the trade rule "trade iff $x > y$ " with prices (6).

Milestones

The milestones follow the paper's proof. Step I solves the flow equations for given cutoffs: (55)–(57), (61)–(63), the populations (64) and (65)–(66), and the densities between the cutoffs (58)–(60), together with the existence of the steady state. Step II derives the slopes (77)–(78), the value functions (79)–(82), the trade rule (83)/(7), the cutoff equations (20), (21) with their unique roots, and the threshold (84). Step III shows that the cutoff rules are optimal for the closed-form values.

Significance

Theorem 1 gives a closed-form description of an OTC market with endogenous participation and an endogenous dealer sector. The search cost splits the population into three groups (passive low types, intermediaries, passive high types), and the length of intermediation chains, trading volumes and price dispersion are all computed from the explicit densities and value functions. Every comparative-statics result of the paper (for example, that a lower search cost lengthens chains) is a statement about the equilibrium this theorem constructs.

The result is proved in the paper, with gaps: the verification of the trade rule outside the dealer region is called "straightforward", Step III treats one of four cases, and uniqueness of the solution of the Bellman system is not argued. No part of it is machine-checked. The mission asks for a complete formal proof, and its definitions give a reusable Lean model of a continuous-time search-and-bargaining steady state with endogenous participation, which no existing formalization provides.

Difficulty

Step I is not just algebra. Between the cutoffs, the flow equation (18) couples each density with integrals of the others, and its solution comes from a Riccati-type equation for $\int_\Delta^{\bar\Delta}\mu_b$ . As printed, the densities (59)–(60) do not solve it. Step II differentiates parametric integrals of the positive part of the surplus, which needs the monotonicity of $V(1,\cdot) - V(0,\cdot)$ before that monotonicity is proved. That uniqueness is the main gap: the paper takes it for granted. Monotonicity of the right-hand sides of (20)–(21) in the cutoff rests on $N_b(F)$ decreasing and $N_s(F)$ increasing, which is asserted, not shown. The obvious approach, plugging the closed forms into Definition 1, gives only existence; uniqueness requires showing that every solution of the flow equations and of the Bellman system is the closed-form one.

Formalization scope

All quantities are real numbers; $\lambda$ is written lam and $\bar\Delta$ is Δbar. The standing assumptions are $0 < X < N$ , $\lambda, \kappa, r > 0$ , $\eta \in (0,1)$ , $c \ge 0$ , $\bar\Delta > 0$ and $f$ a probability density on $[0,\bar\Delta]$ (nonnegative, integrable, total mass $1$ ); $F(\Delta) = \int_0^\Delta f$ and $\mathbf E[g(\Delta')] = \int_0^{\bar\Delta} g f$ . The densities are required to be nonnegative and integrable, and the value functions bounded and measurable on $[0,\bar\Delta]$ , so that no integral takes Lean's default value $0$ .

The equilibrium predicate is Definition 1 itself: flow equations (12)–(19), Bellman system (8)–(11) multiplied through by $\kappa + r$ , and optimality of the cutoff rules ( $V_b \le V_n$ below $\Delta_b$ , $V_n \le V_b$ above, and likewise for owners). The closed forms are separate definitions, and $c^*$ is defined from (20)–(21) as the common value of their right-hand sides at the crossing point; it is never a parameter. A formalization that defined the equilibrium by its closed form, or took $c^*$ as a hypothesis, would make the goal trivial and is excluded.

Corrections and conventions, all disclosed in the items:

$c > 0$ is added. At $c = 0$ , (20) forces $\int_0^{\Delta_b}F = 0$ , which is incompatible with $\Delta_b > 0$ or gives a continuum of equilibria.
(59)–(60) are corrected: the printed densities lack the term $2\kappa(N-X)/(\lambda N)$ and violate (18).
(9) and (11) are read as the derivation on p. 39 uses them ( $1 + \Delta - c$ , and $\max\{V_b(\Delta'), V_n(\Delta')\}$ in the expectation).
The surplus enters (9) and (11) as $S^+$ integrated over all partner types, which is the trade rule of (5)–(6); the conjectured rule (7) is then a conclusion.
Uniqueness off the cutoffs. The flow equations leave the densities free at $\Delta_b$ and $\Delta_s$ , so density uniqueness is stated off these two points.
The pieces of (80) and (82) are read with (81): $V(1,\cdot) = V_s$ on $[0,\Delta_s]$ and $V_h$ on $[\Delta_s,\bar\Delta]$ .

The definitions are split into a model module (parameters, steady state, Bellman system, optimality, equilibrium, prices) and a closed-form module ( $N_b$ , $N_s$ , the cutoff equations, $c^*$ , densities, slopes, value functions). The model module is reusable for the paper's later results (trading volumes, chain length, comparative statics in $c$ , $\lambda$ , $\kappa$ , $X$ ) and for the non-intermediation equilibrium of its Theorem 2. Proofs of individual milestones, and lemmas on the monotonicity of $N_b$ , $N_s$ and of the cutoff equations, are welcome as separate contributions.

Selected references

J. Shen, B. Wei, H. Yan, Financial Intermediation Chains in an OTC Market, MPRA Paper No. 74925, 2016; published as Financial Intermediation Chains in an Over-the-Counter Market, Management Science 67(7), 2021. https://mpra.ub.uni-muenchen.de/74925/ , https://doi.org/10.1287/mnsc.2020.3687
D. Duffie, N. Gârleanu, L. H. Pedersen, Over-the-Counter Markets, Econometrica 73(6), 1815–1847, 2005. https://doi.org/10.1111/j.1468-0262.2005.00639.x
J. Hugonnier, B. Lester, P.-O. Weill, Frictional Intermediation in Over-the-Counter Markets, Review of Economic Studies 87(3), 1432–1469, 2020 (working paper versions from 2014). https://doi.org/10.1093/restud/rdz024

15 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Optimal Patrol of a Perimeter: Optimal Randomized Patrol Schedule and Value of the Patrol Game Against an Observing AttackerResearch Paper

Motivation

Patrolling protects a border or facility perimeter against an intruder who needs uninterrupted time to complete an attack. The defender controls when patrollers pass; the attacker controls when to strike. In a patrol game, the question is how to time patrols when the attacker can observe them (Lin, Optimal Patrol of a Perimeter).

An observing attacker can wait until a patroller has passed before starting. Lin's result shows that a randomised schedule still gives the defender the same optimal detection probability as against a blind attacker, in closed form.

Setting

Fix three parameters: a dispatch rate $\lambda > 0$ , an attack duration $t > 0$ and a detection probability $p \in (0, 1]$ .

Defender. A pure strategy is a nondecreasing sequence of times $s_1 \le s_2 \le \cdots$ in $[0, \infty)$ at which patrollers pass a fixed location. With $N(T) = \#\{n : s_n \le T\}$ the number of patrollers dispatched by time $T$ , the sequence is feasible if it satisfies condition (1) of the paper,

\lim_{T \to \infty} \frac{N(T)}{T} = \lambda .

A mixed strategy is a probability measure $\mu$ on sequences under which almost every sequence is feasible.

Attacker. The attacker chooses an operating window $[y, z]$ with $0 < y < z$ , watches the patrollers go by, and at a time $\tau$ of his choosing starts an attack that occupies $(\tau, \tau + t]$ and must end by $z$ . The choice of $\tau$ may depend on everything observed up to and including time $\tau$ : it is a stopping time of the arrival process.

Payoff. Each patroller passing during the attack detects it independently with probability $p$ . If the attack meets $N$ patrollers it escapes with probability $(1 - p)^N$ , so the detection probability of $\tau$ against $\mu$ is

P_{\mathrm{det}}(\mu, \tau) = E_\mu\bigl[1 - (1 - p)^{N(\tau, \tau + t]}\bigr].

The defender moves first and maximises; the attacker responds and minimises. This Stackelberg game is $\Gamma(\lambda, t, p)$ . Its value is (2):

V(\lambda, t, p) = 1 - (\lambda t - \lfloor \lambda t \rfloor)(1 - p)^{\lceil \lambda t \rceil} - (1 - \lambda t + \lfloor \lambda t \rfloor)(1 - p)^{\lfloor \lambda t \rfloor}.

The claimed optimal schedule $\mu^*$ puts blue patrollers deterministically at $jt + k\Delta$ , with $\Delta = t / \lceil \lambda t \rceil$ , $j = 0, 1, 2, \dots$ and $k = 1, \dots, \lfloor \lambda t \rfloor$ . It puts a red patroller at each $jt$ independently with probability $\lambda t - \lfloor \lambda t \rfloor$ . When $\lambda t$ is an integer there are no red patrollers, and the blue ones pass at fixed intervals of $1/\lambda$ .

Formalization targets

Goal: Theorem 2

For all $\lambda > 0$ , $t > 0$ , $p \in (0, 1]$ :

$\mu^*$ is a feasible mixed strategy;
$\displaystyle \inf_{\tau} P_{\mathrm{det}}(\mu^*, \tau) \ge V(\lambda, t, p)$ over all attacks $\tau$ ;
for every feasible mixed strategy $\mu$ and $\varepsilon > 0$ there is an attack $\tau$ with $P_{\mathrm{det}}(\mu, \tau) < V(\lambda, t, p) + \varepsilon$ ;
$V$ is nondecreasing in $\lambda$ , in $t$ and in $p$ .

Items 2 and 3 state $\sup_\mu \inf_\tau P_{\mathrm{det}}(\mu, \tau) = V(\lambda, t, p)$ , attained at $\mu^*$ .

Milestones

Lemma 1 (p. 5). Among laws on $\{0, 1, 2, \dots\}$ with mean $c > 0$ , the detection probability $1 - E[(1 - p)^N]$ is at most $V$ with $\lambda t$ replaced by $c$ , and the least-variance law on $\{\lfloor c \rfloor, \lceil c \rceil\}$ attains it.
Window counting (p. 7). Every window $(a, a + t]$ with $a \ge 0$ contains exactly $\lfloor \lambda t \rfloor$ blue time points and exactly one red slot.
Feasibility (p. 7, with (1)). $\mu^*$ is a feasible mixed strategy.
Guarantee (p. 7). $P_{\mathrm{det}}(\mu^*, \tau) = V(\lambda, t, p)$ for every attack $\tau$ .
Converse (pp. 7–8). For every feasible $\mu$ and $\varepsilon > 0$ some deterministic start time $y > 0$ has $P_{\mathrm{det}}(\mu, y) < V(\lambda, t, p) + \varepsilon$ .
Monotonicity (p. 8). $V$ is nondecreasing in each argument.

Significance

The result. Watching the patrollers gives the attacker no improvement in the game value. The value interpolates $n \mapsto 1 - (1 - p)^n$ at $n = \lambda t$ , giving a closed-form trade-off between patrol rate, attack duration and detection reliability. The same schedule supports the paper's Theorem 3 (invisible patrollers) and Theorem 4 (a whole perimeter).

Formalizing it. The paper proves the result; this mission seeks a machine-checked proof. The development must specify the attacker's information, almost-sure feasibility of the random schedule, and the converse. It also supplies a reusable model of continuous-time patrol games with adaptive attackers.

Difficulty

For a fixed window, the blue count is fixed and its red slot is independent. An observing attacker instead chooses a stopping time from past arrivals. The proof must account for which red slots he has seen. The half-open window matters: with $[\tau, \tau + t)$ , an attacker starting at an empty red slot meets only $\lfloor \lambda t \rfloor$ patrollers.

The converse is harder because a feasible mixed strategy may have infinite expected count in every window even when each path has rate $\lambda$ . An argument based only on the expected count therefore fails.

Formalization scope

Lean namespace PerimeterPatrol.Visible. Schedules are maps $s : \mathbb N \to \mathbb R$ (patroller $n + 1$ passes at $s(n)$ ) with the product $\sigma$ -algebra. Feasibility requires Monotone s, $0 \le s(0)$ , and the limit (1) along atTop, with counts given by Nat.card. A mixed strategy is an IsProbabilityMeasure that is almost surely feasible. The attacker's information up to time $u$ is the $\sigma$ -algebra generated by the counts $N(v)$ , $v \le u$ . An attack is a start-time rule $\tau$ with a fixed window $[y, z]$ , $0 < y$ , such that $\{\tau \le u\}$ is measurable for that $\sigma$ -algebra for every $u$ . The detection probability is a Bochner integral of a $[0,1]$ -valued function. $\mu^*$ is the pushforward of i.i.d. uniform draws on $[0, 1]$ , with the red patroller at $jt$ present iff the $j$ -th draw is below $\lambda t - \lfloor \lambda t \rfloor$ .

Conventions committed to:

the attack window is $(\tau, \tau + t]$ , with information up to and including $\tau$ ;
the attacker may observe from time $0$ rather than from $y$ , which enlarges the attacker class, so the guarantee is at least as strong as the paper's;
"increasing" sequences may have ties;
floors and ceilings are Nat.floor and Nat.ceil, exact for positive arguments;
"increases" in (2) means nondecreasing, because $V \equiv 1$ when $p = 1$ and $\lambda t \ge 1$ ;
Lemma 1's least-variance law is claimed to be a maximiser, not the unique one (uniqueness fails at $p = 1$ ).

The attacker class includes measurable adaptive stopping times; the optimal schedule must be a probability measure; and the value is characterized through the two game inequalities rather than an unrestricted real supremum or infimum.

Needed infrastructure: counting functions of nondecreasing sequences, the stopping-time and independence argument for the red slots, the strong law of large numbers (Mathlib's ProbabilityTheory.strong_law_ae) for the long-run rate of $\mu^*$ , and an averaging argument over start times for the converse. The counting and stopping-time lemmas for point processes on $[0, \infty)$ are reusable beyond this mission. Proofs of any milestone, and alternative routes to the converse, are welcome.

Not formalized here: Theorem 3 (p. 9) as a separate item, Theorem 4 (the perimeter game, p. 10), Theorem 5 (the finite-horizon simultaneous game, p. 11) and the remarks of §2.1 and §5.

Selected references

K. Y. Lin, Optimal Patrol of a Perimeter, Operations Research, 2022, Technical Note; preprint arXiv:1905.03600v3, 2020. https://arxiv.org/abs/1905.03600v3 , https://doi.org/10.1287/opre.2021.2117

9 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Timing It Right: Balancing Inpatient Congestion vs. Readmission Risk at Discharge: Discharge a Patient Type Only After Every Strongly Dominating Type of No Shorter StayResearch Paper

Who to discharge from a congested ward

Every day a hospital ward with a fixed number of beds decides which patients go home. Sending a patient home early frees a bed for the next admission, which matters when the ward is congested and arrivals board in the emergency department or elective surgeries are cancelled. Sending a patient home too early raises the chance that the patient is readmitted, which is costly for the patient and, under the U.S. Hospital Readmissions Reduction Program, for the hospital. Shi, Helm, Deglise-Hawkinson and Pan (SSRN 3202975; Operations Research 2021, doi:10.1287/opre.2020.2044) model this trade-off as a Markov decision process over a census of patients indexed by class and length of stay (LOS), fit personalized readmission-risk curves to hospital data, and implement the resulting discharge policy at a partner hospital.

The structural question behind their policy is who to discharge first. Hospitals usually rank patients by their current, absolute readmission risk. The paper's Theorem 2 (p. 15) instead ranks types by how fast that risk falls with a further day of stay: a type whose risk curve is flatter from now on should be discharged before a type whose risk is still dropping quickly. This mission formalizes that ranking result, in a corrected form.

Setting

There are $M$ patient classes and a maximum length of stay $J$ . A type is a pair $(m,j)$ of a class and a LOS $j\in\{0,\dots,J\}$ . A state $X=(X^{m,j})$ counts the patients of each type, and the census is $S=\sum_m\sum_j X^{m,j}$ . A discharge action $D=(D^{m,j})$ counts the patients of each type sent home. Class $m$ has a minimum LOS $\underline L_m\in[0,J]$ , and an action is feasible at $X$ when $0\le D^{m,j}\le X^{m,j}$ (3), $D^{m,j}=0$ for $j<\underline L_m$ (4), and every patient at LOS $J$ leaves.

Between two daily decision epochs $k$ and $k+1$ , new patients and readmitted patients arrive at LOS $0$ , and every patient who was not discharged ages by one day: $X^{m,0}_{k+1}=A^{m,0}_k+A'^{m,0}_k$ (5) and $X^{m,j}_{k+1}=X^{m,j-1}_k-D^{m,j-1}_k$ (6). Each epoch costs the holding cost $c_h(X)=C\,(S-N)^+$ for $N$ beds (7), plus the discharge cost $c_d(D)=\sum_{m,j}D^{m,j}\,R\,r(m,j)$ (8), where $r(m,t)$ is the readmission risk of a class- $m$ patient discharged at LOS $t$ and $R\ge0$ is the readmission penalty. Each risk curve $r(m,\cdot)$ is continuously differentiable and nonincreasing in the LOS.

Strong dominance (Definition 1, p. 14): $(m_1,t_1)\succ(m_2,t_2)$ iff

\Bigl|\frac{\partial r(m_1,t_1+t)}{\partial t}\Bigr|\le\Bigl|\frac{\partial r(m_2,t_2+t)}{\partial t}\Bigr|\qquad\forall t\ge0.\tag{15}

Writing $e_{(m,t)}$ for one discharge of type $(m,t)$ , a schedule $(D_k)$ with trajectory $(X_k)$ over a horizon $H$ has total cost $V(D)=\sum_{k<H}[c_h(X_k)+c_d(D_k)]+c_h(X_H)+c_d(X_H)$ .

Formalization targets

Goal: Theorem 2, corrected

For an initial state, an arrival path and a horizon $H$ , let $(m_1,t_1)\ne(m_2,t_2)$ with $(m_1,t_1)\succ(m_2,t_2)$ , $t_2\le t_1$ and $\underline L_{m_1}\le t_1$ . Then every feasible schedule $D$ has a feasible schedule $D'$ with $V(D')\le V(D)$ such that, for all $k<H$ ,

D'_k\cdot e_{(m_2,t_2)}>0\ \Longrightarrow\ D'_k\cdot e_{(m_1,t_1)}=X'_k\cdot e_{(m_1,t_1)}.

Since the feasible schedules are finitely many, some optimal schedule discharges a $(m_2,t_2)$ patient only after all $(m_1,t_1)$ patients.

Milestones

Proposition 2 (p. 15): for $k'>k$ , $c_d(D_k+e_{(m_1,t_1)})-c_d(D_{k'}+e_{(m_1,t_1+k'-k)})\le c_d(D_k+e_{(m_2,t_2)})-c_d(D_{k'}+e_{(m_2,t_2+k'-k)})$ .
Census invariance (proof of Theorem 2, p. 16): swapping the discharge epochs of one $(m_1,t_1)$ patient and one $(m_2,t_2)$ patient leaves the census unchanged at every epoch.
Cost identity and inequality (proof of Theorem 2, p. 16): the swapped schedule is feasible, its total-cost difference equals the four discharge-cost terms displayed in the proof, and $V^{\pi_2}-V^{\pi_1}\le0$ .

Significance

Theorem 2 is the paper's main structural result. It turns a high-dimensional MDP, whose state is a census over $M(J+1)$ types, into a ranking problem: once types are ordered by strong dominance, the remaining decision is how many patients to discharge (Corollary 1, p. 16), which the paper then approximates with a univariate linear-quadratic heuristic (§5). The ranking also has a direct operational reading: discharge by marginal, not absolute, readmission risk.

No machine-checked version of this result exists. Formalizing it settles exactly which hypotheses the interchange argument needs. Doing so already exposed that the statement as printed is false (see Difficulty), so the mission's output is the corrected theorem with a checked proof, together with a reusable finite-horizon, pathwise model of class-by-LOS patient flow.

Difficulty

The obvious argument is a single interchange: if a $(m_2,t_2)$ patient is discharged at epoch $k$ while a $(m_1,t_1)$ patient stays until a later epoch $k'$ , swap their discharge epochs. The census path does not change, and Proposition 2 shows the discharge cost does not increase. The step that fails is the one the paper defers to Appendix B.3: the dominated patient, kept from $k$ to $k'$ , may pass the maximum LOS $J$ before $k'$ , and then the swap is not available. The appendix's repair does not close the gap. With $J=3$ , $N=1$ , $C=1000$ , $R=1$ , no arrivals, $r(1,j)=10-j$ , $r(2,j)=10-2j$ and one $(1,0)$ and one $(2,2)$ patient on day $0$ , we have $(1,0)\succ(2,2)$ , yet the unique optimum discharges the $(2,2)$ patient alone (cost 1013), and every schedule that obeys the rule costs at least 1014. The added hypothesis $t_2\le t_1$ guarantees that the dominated patient can wait as long as the dominating one, so the swap always exists.

The remaining difficulty is bookkeeping: the interchange changes two cohorts by $\pm1$ over an interval of epochs, and feasibility (counts, minimum LOS, forced exit at $J$ ) must be checked along the new trajectory. Repeated interchanges must also be ordered so that fixing one epoch does not break an earlier one.

Formalization scope

Model. Classes are Fin M, LOS indices Fin (J+1), counts natural numbers, costs real numbers. Epochs start at $0$ . Arrivals, new and readmitted, form one exogenous deterministic path, as Remark 4 (p. 12) prescribes for §4. Every statement is pathwise on a finite horizon $H$ , the setting of the paper's interchange argument. The long-run average cost (9) is not used, since a finite interchange cannot change it.
Conventions added. Patients at LOS $J$ must leave, since (6) has no LOS $J+1$ . The total cost charges every patient present at the horizon as if discharged at their current LOS, so that holding a patient to the end is not free. The risk curves are $C^1$ and nonincreasing on $[0,\infty)$ (p. 15), and $R\ge0$ . Strong dominance uses Mathlib's deriv with the absolute values of (15).
Correction to Theorem 2. The goal adds $t_2\le t_1$ (the printed statement is false, as shown above), $(m_1,t_1)\ne(m_2,t_2)$ (strong dominance is reflexive, so the rule would otherwise demand every type be fully discharged once any is), and $\underline L_{m_1}\le t_1$ (otherwise $(m_1,t_1)$ patients can never be discharged). "The optimal action" becomes "some no-costlier feasible schedule obeys the rule": with ties an optimal schedule may break it.
Ruling out trivial readings. The goal quantifies over feasible schedules with the real costs (7)–(8), and the rule is required at every epoch $k<H$ along $D'$ 's own trajectory. Taking $D'=D$ does not suffice in general, and a schedule that avoids discharging $(m_2,t_2)$ by letting patients vanish is excluded by the forced exit and the terminal valuation.
Infrastructure. One definitions file holds the model, strong dominance, unit actions and the interchange. Mathlib's fundamental theorem of calculus (intervalIntegral.integral_eq_sub_of_hasDerivAt) and monotonicity of integrals are the analytic substrate for Proposition 2. The trajectory and interchange lemmas about class-by-age cohorts are reusable for other census models. Proofs of any milestone are welcome independently.

Not formalized: Theorem 1 (existence of an average-cost optimal policy), Corollary 1 (threshold form), Propositions 1 and 3, and Lemma 1.

Selected references

P. Shi, J. E. Helm, J. Deglise-Hawkinson, J. Pan, Timing it right: balancing inpatient congestion versus readmission risk at discharge, SSRN working paper 3202975, version of 2019-08-26. https://ssrn.com/abstract=3202975
P. Shi, J. E. Helm, J. Deglise-Hawkinson, J. Pan, same title, Operations Research, 2021 (published version; not the citation basis of this mission). https://doi.org/10.1287/opre.2020.2044

5 thms2 active usersReviewed

All missions

Discrete Dividend Payments in Continuous Time: The Value Function Is the Unique Fixed Point of the One-Period Dividend-and-Issuance OperatorResearch Paper

Why periodic dividends matter

The cash reserve model

Formalization targets

What the characterization gives

Where the difficulty lies

Formalization scope

Selected references

Risk Guarantees for End-to-End Prediction and Optimization Processes: The Excess Squared-Loss Risk Bounds the Squared Excess Optimality-Gap Risk, Scaled by the Squared Diameter of the Feasible SetResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 3 (p. 22)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Computing the Nonlinearity Interval in Parametric Semidefinite Optimization: The Set of Transition Points of the Optimal Partition Is FiniteResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 8)

Milestones, in the order of the paper's argument

Significance

Difficulty

Formalization scope

Selected references

Optimal Use and Replenishment of Two Substitutable Raw Materials in a Stochastic Capacitated Make-to-Order Production System: A Use-Down-To/Balancing Production Policy Is OptimalResearch Paper

Motivation

Setting

Formalization targets

Optimal production rule

Significance

Difficulty

Formalization scope

Selected references

Consensus Halving for Sets of Items: For n Agents with Additive Utilities a Consensus Halving That Cuts at Most min{n, m} of the m Items Always ExistsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.2 (existence form)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Hypergraph k-Cut for Fixed k in Deterministic Polynomial Time: A Maximal Minimum k-Partition's First Part Is the Source-Maximal Minimum (S, T)-Terminal Cut for Some |S| = 2k − 2Research Paper

Why this question matters

Finite hypergraphs and terminal cuts

Formalization targets

The structural theorem

Supporting statements

What the result provides

Where the proof is difficult

Formalization scope

Selected references

Mechanism Design for Managing Hidden Rebates and Inflated Quotes of a Procurement Service Provider: Paying a Fee Equal to the Hidden Rebate Is the Optimal Truthful Contract for Small RebatesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 12)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Price/Advertising Menus for Two-Sided Media Platforms: In Duopoly with Multi-Item Menus the Unique Equilibrium Is a Symmetric Two-Item Menu on Which Both Consumer Types Multi-HomeResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Nonconvex Low-Rank Tensor Completion from Noisy Data: Spectrally Initialized Vanilla Gradient Descent Recovers the Tensor Factors at a Linear Rate to Near-Optimal ℓ2 and ℓ2,∞ AccuracyResearch Paper

Motivation

Goal: Theorem 3.6 (p. 13), with right-continuous $f$