Operations Research

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

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

1. Remark 1 (p. 2): strictly feasible primal and dual solutions exist at every $\epsilon\in\operatorname{int}(\mathcal E)$.
2. 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)$.
3. p. 2: for $\epsilon\in\operatorname{int}(\mathcal E)$, $\mathcal P^*(\epsilon)$ and $\mathcal D^*(\epsilon)$ are nonempty and compact (strong duality).
4. (1), p. 2: on $\operatorname{int}(\mathcal E)$, a primal–dual triple is optimal iff it is feasible and $XS=0$.
5. Appendix, p. 22: the ranks at relative-interior optimal points are maximal on the optimal sets.
6. (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)$.
7. 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$.
8. p. 23: every $\mathcal S_{(\theta,\sigma)}$ is a semi-algebraic subset of $\mathbb R$.
9. [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.

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.

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$:

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

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.

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

1. §5.1, p. 12. Under (15) the intermediary collects $r$ in every state, so (15) is incentive compatible.
2. §5.1, p. 12. In cost coordinates, $A^*(x_S, x_W + r) = S$ if and only if $x_S \le x_W$.
3. (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.

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

1. 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.
2. Lemma 8 (p. 47): in every equilibrium both types multi-home.
3. Consumer choices (pp. 52–53): at the stated menus, multi-homing on the designed items is an admissible response for each type.
4. Platform best response (pp. 53–56): against the stated menu, no deviation earns more than the stated revenue.
5. 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.
6. 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

Motivation

Many problems in convex optimization, variational inequalities, game theory and signal processing are systems of monotone inclusions coupled by linear operators: several unknowns $x_i$ in different Hilbert spaces, each subject to its own maximally monotone, cocoercive and Lipschitzian operators, and tied together through linear maps $L_{ki}$ and composite terms. Bùi and Combettes (arXiv:2002.06135, Mathematics of Operations Research, 2022) introduce a single model, Problem 1.1, that contains a large part of these formulations and design algorithms for it that are fully split (each operator is used separately, set-valued operators through their resolvents and single-valued ones through forward evaluations), block-iterative (only some blocks are updated at each iteration) and asynchronous (updates may use information computed up to $T$ iterations earlier).

The paper places itself after a line of primal-dual splitting methods: Briceño-Arias and Combettes (SIAM J. Optim. 2011, doi:10.1137/10081602x) for a two-operator monotone+skew model, Alotaibi, Combettes and Shahzad (SIAM J. Optim. 2014) for Fejér approximation of a Kuhn–Tucker set, Combettes and Eckstein (Math. Program. B168, 2018) for asynchronous block-iterative primal-dual decomposition, and the projective splitting methods of Johnstone and Eckstein (2020–2021). These earlier methods work in the primal-dual space $\mathcal H\oplus\mathcal G$. The new idea is to reformulate the problem as finding a zero of a saddle operator on a larger space and to approximate that zero set from outside by half-spaces.

Setting

Let $I$ and $K$ be finite index sets and let $(\mathcal H_i)_{i\in I}$, $(\mathcal G_k)_{k\in K}$ be real Hilbert spaces, with Hilbert direct sums $\mathcal H=\bigoplus_i\mathcal H_i$ and $\mathcal G=\bigoplus_k\mathcal G_k$. For every $i$ and $k$ the data are:

• $A_i:\mathcal H_i\to2^{\mathcal H_i}$ maximally monotone, $C_i$ cocoercive with constant $\alpha^c_i>0$, $Q_i$ monotone and $\alpha^\ell_i$-Lipschitzian, and $R_i:\mathcal H\to\mathcal H_i$ such that $R=(R_i)_i$ is monotone and $\chi$-Lipschitzian on $\mathcal H$;
• $B^m_k$, $D^m_k$ maximally monotone on $\mathcal G_k$, $B^c_k$, $D^c_k$ cocoercive with constants $\beta^c_k,\delta^c_k>0$, and $B^\ell_k$, $D^\ell_k$ monotone and Lipschitzian with constants $\beta^\ell_k,\delta^\ell_k$;
• bounded linear $L_{ki}:\mathcal H_i\to\mathcal G_k$, and vectors $s^*_i\in\mathcal H_i$, $r_k\in\mathcal G_k$.

The parallel sum of $B,D:\mathcal G_k\to2^{\mathcal G_k}$ is $B\,\square\,D=(B^{-1}+D^{-1})^{-1}$. Write $\mathsf B_k=B^m_k+B^c_k+B^\ell_k$ and $\mathsf D_k=D^m_k+D^c_k+D^\ell_k$. The primal problem (1.1) asks for $\overline x\in\mathcal H$ with

$$s^*_i\in A_i\overline x_i+C_i\overline x_i+Q_i\overline x_i+R_i\overline x+\sum_{k\in K}L^*_{ki}\Big((\mathsf B_k\,\square\,\mathsf D_k)\Big(\sum_{j\in I}L_{kj}\overline x_j-r_k\Big)\Big)\quad(\forall i\in I).$$

Its set of solutions is $\mathscr P$. The dual problem (1.2) asks for $\overline v^*\in\mathcal G$ such that some $x\in\mathcal H$ satisfies $s^*_i-\sum_jL^*_{ji}\overline v^*_j\in A_ix_i+C_ix_i+Q_ix_i+R_ix$ and $\overline v^*_k\in(\mathsf B_k\,\square\,\mathsf D_k)(\sum_jL_{kj}x_j-r_k)$; its set of solutions is $\mathscr D$. The Kuhn–Tucker set $\mathsf Z\subset\mathcal H\oplus\mathcal G$ (2.13) collects the pairs $(\overline x,\overline v^*)$ satisfying the first condition at $\overline x$ and $\sum_jL_{kj}\overline x_j-r_k\in\mathsf B_k^{-1}\overline v^*_k+\mathsf D_k^{-1}\overline v^*_k$.

On $\mathbf X=\mathcal H\oplus\mathcal G\oplus\mathcal G\oplus\mathcal G$ the saddle operator $\boldsymbol{\mathcal S}$ (2.11) maps $(x,y,z,v^*)$ to the product of the sets $-s^*_i+A_ix_i+C_ix_i+Q_ix_i+R_ix+\sum_kL^*_{ki}v^*_k$, $\ B^m_ky_k+B^c_ky_k+B^\ell_ky_k-v^*_k$, $\ D^m_kz_k+D^c_kz_k+D^\ell_kz_k-v^*_k$ and $\{r_k+y_k+z_k-\sum_iL_{ki}x_i\}$. It splits as $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$ (Definition 2.4), where $\mathbf C$ collects the cocoercive operators.

Algorithm 3.4 runs, at iteration $n$, over activated blocks $I_n\subset I$, $K_n\subset K$. For $i\in I_n$ it computes a resolvent step $a_{i,n}=J_{\gamma A_i}(\cdot)$ from the delayed iterate $x_{\pi_i(n)}$; for $k\in K_n$ it computes $b_{k,n}$, $d_{k,n}$ from resolvents of $B^m_k$, $D^m_k$ at the delayed iterate $\omega_k(n)$. Blocks that are not activated keep their previous values. From these quantities it forms a half-space containing $\operatorname{zer}\boldsymbol{\mathcal S}$, measured by a number $\Delta_n$ that involves $\alpha=\min\{\alpha^c_i,\beta^c_k,\delta^c_k\}$. If $\Delta_n>0$, it moves $(x_n,y_n,z_n,v^*_n)$ toward that half-space with relaxation $\lambda_n\in[\varepsilon,2-\varepsilon]$; otherwise the iterate stays put.

Formalization targets

Goal: Theorem 3.5

Under Assumptions 3.1–3.3 (step-size ranges tied to $\alpha$, $\sigma>1/(4\alpha)$ and $\varepsilon$ by (3.1); every block activated at least once in every $P+1$ consecutive iterations; delays at most $T$), if the dual problem has a solution, then every run of Algorithm 3.4 satisfies

$$\sum_n\|x_{i,n+1}-x_{i,n}\|^2<\infty,\qquad x_{i,n}-a_{i,n}\to0,\qquad v^*_{k,n}-e^*_{k,n}\to0,$$

together with the analogous statements for $y,z,v^*$ and $b,d$. There exist $\overline x\in\mathscr P$ and $\overline v^*\in\mathscr D$ with $(\overline x,\overline v^*)\in\mathsf Z$ such that

$$x_{i,n}\rightharpoonup\overline x_i,\qquad a_{i,n}\rightharpoonup\overline x_i,\qquad v^*_{k,n}\rightharpoonup\overline v^*_k.$$

Milestones

In attack order:

1. Proposition 2.2(i)–(ii): $\boldsymbol{\mathcal S}$ is maximally monotone and $\operatorname{zer}\boldsymbol{\mathcal S}$ is closed and convex.
2. Proposition 2.2(iii)–(iv): zeros of $\boldsymbol{\mathcal S}$ project into $\mathsf Z\subset\mathscr P\times\mathscr D$, and $\mathscr D\neq\varnothing\Leftrightarrow\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing\Leftrightarrow\mathsf Z\neq\varnothing\Rightarrow\mathscr P\neq\varnothing$.
3. Proposition 2.5: $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$, $\mathbf M$ maximally monotone, $\mathbf C$ $\alpha$-cocoercive, and the half-spaces containing $\operatorname{zer}\boldsymbol{\mathcal S}$.
4. Lemma A.4: the relaxed half-space outer-approximation iteration (A.3) is Fejér monotone and converges weakly when every weak sequential cluster point lies in $Z$.
5. Proposition 2.6: the iteration (2.32) on $\mathbf X$ converges weakly to a zero of $\boldsymbol{\mathcal S}$ when its three stated residual conditions hold.
6. Lemmas A.1, A.2 and A.3: boundedness of resolvent sequences, strong monotonicity of $\gamma^{-1}\mathrm{Id}-A$, and the vanishing of the delayed differences $x_{\vartheta_i(n)}-x_n$.

Significance

Theorem 3.5 gives weak convergence of a method that uses each operator of Problem 1.1 separately, needs no inversion of linear operators and no knowledge of $\|L\|$, and updates nonempty subsets of blocks subject to the coverage windows and bounded delays of Assumptions 3.2–3.3. It produces primal and dual solutions together. Section 4 of the paper derives from it algorithms for variational inequalities over sums of sets and for multivariate convex minimization with infimal convolutions. The hypothesis is dual solvability. Remark 2.3 shows that primal solvability alone is not enough: there are instances with $\mathscr P\neq\varnothing$ and $\mathsf Z=\varnothing$.

The theorem is proved in the paper. A formalization adds machine-checked foundations that later work in splitting methods can reuse: the saddle operator and its maximal monotonicity; the Fejér outer-approximation principle in Hilbert space (Lemma A.4, cited by the paper from an encyclopedia entry); and the asynchrony lemma (Lemma A.3). To our knowledge none of these results has been formalized before.

Difficulty

The obvious approach would be to show that Algorithm 3.4 is a Fejér-monotone iteration toward $\mathsf Z$ in $\mathcal H\oplus\mathcal G$. That approach fails: for the general Problem 1.1, no half-space separating the current point from $\mathsf Z$ can be computed from separate operator evaluations (Remark 2.3(iii)). The algorithm instead targets $\operatorname{zer}\boldsymbol{\mathcal S}$ in the larger space $\mathbf X$. The link back to $\mathscr P$, $\mathscr D$ and $\mathsf Z$ is Proposition 2.2.

The second difficulty is asynchrony. The half-space at iteration $n$ is built from points computed at earlier iterations, with stale step sizes. To show that the weak cluster points are zeros of $\boldsymbol{\mathcal S}$, one has to control these delays (Lemma A.3) and use the cocoercive and Lipschitzian terms uniformly over the step-size ranges (Lemmas A.1–A.2).

Formalization scope

• Spaces. Every space is a complete real inner product space. $\mathcal H$ and $\mathcal G$ are PiLp 2 over finite index types, and $\mathbf X$ is a nested WithLp 2 product, so all norms and inner products are the Hilbert ones (not sup norms).
• Operators. Set-valued operators are maps E → Set E. Monotonicity, maximal monotonicity, zer, cocoercivity, resolvents and weak convergence are the published ThreeOpSplitting.Convergence definitions; inverses and sums of set-valued maps are the published DouglasRachfordPPA.GenDR ones.
• Runs. A run of Algorithm 3.4 is a predicate on given sequences that pins every assignment of (3.3). This includes the delayed indices inside the step sizes, the carry-over of inactive blocks (stated at $n+1$), the recomputation of $e_{k,n}$ for every $k$, and $\Delta_n$ with the factor $(4\alpha)^{-1}$ at the current iterates. The resolvents are given maps constrained by the resolvent identity at every positive step.
• Constants and assumptions. $\alpha$ is pinned as the least cocoercivity constant. The delay bound $n-T\le\pi_i(n)\le n$ is written without natural-number subtraction. "$\varlimsup\Delta_n\le0$" in Proposition 2.6 is stated as "eventually $\Delta_n\le\delta$ for every $\delta>0$".
• Ruling out trivial readings. The run predicate determines every assignment of (3.3), so no free choice of outputs makes the theorem trivial. The hypothesis is dual solvability $\mathscr D\neq\varnothing$ exactly as in (1.2), not the stronger-looking $\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing$ (equivalent only by Proposition 2.2). The conclusion is weak convergence to a pair that is simultaneously primal, dual and Kuhn–Tucker. A sorry-free check shows that the goal's hypotheses are jointly satisfiable.
• Not included. Theorem 3.7 (strong convergence of a Haugazeau-type variant) with Proposition 2.7 and Lemma A.5, Proposition 2.2(v), and the applications of Section 4.
• Reusable parts. The saddle operator and its splitting, Lemma A.4, Lemma A.3, and Lemmas A.1–A.2 are stated in general form and can serve other splitting missions. Contributions of auxiliary results are welcome, for example demiclosedness of maximally monotone operators, Minty's theorem in the published encoding, and Fejér-monotone weak convergence (Opial).

Selected references

• M. N. Bùi and P. L. Combettes, Multivariate monotone inclusions in saddle form, Mathematics of Operations Research, 2022; preprint arXiv:2002.06135v3, 2021. https://arxiv.org/abs/2002.06135
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• L. M. Briceño-Arias and P. L. Combettes, A monotone+skew splitting model for composite monotone inclusions in duality, SIAM Journal on Optimization 21, 2011. https://doi.org/10.1137/10081602x
• P. L. Combettes and J. Eckstein, Asynchronous block-iterative primal-dual decomposition methods for monotone inclusions, Mathematical Programming B168, pp. 645–672, 2018 (reference [25] of arXiv:2002.06135).
• P. L. Combettes, Fejér-monotonicity in convex optimization, in: Encyclopedia of Optimization, vol. 2, pp. 106–114, Springer, 2001 (reference [22] of arXiv:2002.06135; source of Lemma A.4).