All missions

Motivation

A central planner holds a single pool of $Q$ units of a product and must supply $N$ customers whose demands $\tilde d_1, \dots, \tilde d_N$ are random. Each customer $i$ asks to be fully served, i.e. to receive her entire demand, with probability at least a target $\alpha_i$. This Type-I service level (the persistency value of the stochastic knapsack) is the standard requirement in supply-chain allocation and in humanitarian logistics. The planner's question is how much capacity the targets require.

The answer depends on when the planner learns the demands. Lyu, Chou, Teo, Zheng and Zhong (SSRN 3674463, 2021) compare three information regimes:

• a responsive policy sees every demand before allocating;
• an adaptive policy learns a customer's demand only once it has decided to serve her, and may choose the next customer in light of what it has seen (Dean, Goemans and Vondrák, 2008);
• an anticipative policy fixes a priority order before any demand is realized (Alptekinoğlu, Banerjee, Paul and Jain, M&SOM 15(1), 2013).

Anticipative rules are the ones used in practice, because they are simple to announce and to audit. The paper's main result quantifies what they cost in capacity compared with adaptive rules.

Timeline. Alptekinoğlu et al. (2013) introduced capacity pooling with differentiated service probabilities under anticipative priority rules. Dean, Goemans and Vondrák (2008) bounded the adaptivity gap of the stochastic knapsack for revenue maximization by a constant factor. Zhong, Zheng, Chou and Teo (Management Science 64(4), 2018) treated the Type-II (fill-rate) version, in which partial service counts in proportion. They showed that its achievable region is a polymatroid $\Gamma(Q)$ and that anticipative policies are optimal there. Lyu et al. (2021) use this Type-II system to compare the Type-I classes.

Setting

Customers are $i \in \{1, \dots, N\}$. The demands are random variables on a probability space $(\Omega, \mathcal F, \mathbf P)$. An allocation run with capacity $Q \ge 0$ serves customers one at a time. A chosen customer is fully served if her demand does not exceed the remaining capacity, and her demand is then deducted. Otherwise she is not fully served, and the run stops.

• A deterministic adaptive policy chooses the next customer as a function of the customers chosen so far and their realized demands.
• A deterministic anticipative policy is a priority order $\sigma$, fixed in advance.
• A randomized policy in either class is a finite mixture $\sum_k w_k A_k$ of deterministic ones, drawn independently of the demands.

The optimal Type-I capacities are

$$Q^{\mathrm{Adap}}_I = \inf\{Q \ge 0 : \text{some randomized adaptive policy has } \mathbf P(i \text{ fully served}) \ge \alpha_i\ \forall i\},$$

and $Q^{\mathrm{Anti}}_I$ is defined in the same way with anticipative policies. These are the optimal values of problem (CPP-A) of the paper.

On the Type-II side, $\Gamma(Q)$ is the set of $\alpha$ with $\sum_{i \in U} \alpha_i \mathbf E[\tilde d_i] \le \mathbf E[\min(Q, \sum_{i\in U} \tilde d_i)]$ for every $U \subseteq \{1,\dots,N\}$. $Q_{II}$ is the least $Q \ge 0$ with $\alpha \in \Gamma(Q)$. For a priority order $\sigma$, the greedy fill $x^*_i(\sigma, \tilde d, Q) = \min\{\tilde d_i, \max(0, Q - \sum_{j \text{ ahead of } i} \tilde d_j)\}$ solves the fractional knapsack (CPP-F).

Standing assumptions (§3.3): the demands are independent and positive, and almost surely $\max_i \tilde d_i \le \Delta$ for a constant $\Delta > 0$. The targets satisfy $0 \le \alpha_i \le 1$.

Formalization targets

Goal: Theorem 5

$$Q^{\mathrm{Anti}}_I - Q^{\mathrm{Adap}}_I \le 2\Delta.$$

The bound is uniform in $N$ and in the joint law of the demands, subject only to the standing assumptions.

The two halves: Theorems 3 and 4

$$Q^{\mathrm{Anti}}_I \le Q_{II} + \Delta, \qquad Q^{\mathrm{Adap}}_I \ge Q_{II} - \Delta.$$

Milestones inside the proofs

1. Achievability of $\Gamma(Q)$ in fill rate by randomized priority orders (p. 21, from Zhong et al. 2018).
2. Structure of the greedy fill: it is fractional for at most one customer, and positive exactly when the demand ahead is below $Q$ (p. 17).
3. $\mathbf E[x^*_i]/\mathbf E[\tilde d_i] \le \mathbf P(x^*_i > 0)$ (p. 17).
4. Theorem 3.
5. The rounded adaptive policy $A'$, which also serves the one customer the run turns away, satisfies $\mathbf E[\sum_{k\in U}\tilde d_k y^{A'}_k] \ge \sum_{k \in U} \mathbf E[\tilde d_k]\alpha_k$ (p. 37).
6. Adaptive feasibility of $Q$ implies $\alpha \in \Gamma(Q + \Delta)$ (p. 37). The page writes $Q^{\mathrm{Adpt}}_I$, a misprint for $Q^{\mathrm{Adap}}_I$.
7. Theorem 4.

Significance

The result. Theorem 5 says that the information an adaptive planner gains costs at most two maximal demands of capacity, independently of the number of customers. Anticipative priority rules are therefore near-optimal for Type-I service whenever individual demands are small relative to the pool. This contrasts with the responsive regime: Example 1 of the paper shows that $Q^{\mathrm{Adap}}_I$ can exceed $Q^{\mathrm{Resp}}_I$ by an unbounded factor. In Theorems 3–4 the Type-II capacity $Q_{II}$ serves as a common yardstick, so each policy class is compared with an explicitly computable polymatroid quantity.

Formalizing it. The theorem is proved on paper. To our knowledge none of it is machine-checked. A formal development has to make precise what the paper leaves informal: what a randomized adaptive policy is, why the event "customer $i$ is reached" is independent of $\tilde d_i$, and why the infima defining the optimal capacities are over non-empty sets. The milestones on the greedy fill and the polymatroid $\Gamma(Q)$ can be reused for other fill-rate and persistency problems.

Difficulty

The obvious comparison fails because the two classes face different constraints. A Type-I requirement is an all-or-nothing event, so a deterministic priority order cannot hedge. With three identical unit-demand customers and targets $1/3$, any fixed order needs $Q = 3$, while $Q_{II} = 1$. Randomization over orders is therefore essential on the anticipative side, and the link between a Type-I requirement and the Type-II region $\Gamma(Q)$ is not a statement about any single order. On the adaptive side, the decisions depend on revealed demands. Whether customer $k$ is fully served is correlated with $\tilde d_k$, so a Type-I service probability does not translate directly into a bound on the expected demand served, which is what $\Gamma(Q)$ constrains. Conditioning arguments that ignore this correlation give false inequalities.

Formalization scope

• Demands are a vector d : Fin N → Ω → ℝ on a probability space. Probabilities are μ.real, expectations are Bochner integrals. The standing assumptions are bundled in Standing μ d Δ α: measurable, iIndepFun, almost surely positive, almost surely ≤ Δ, 0 < Δ, and α i ∈ [0, 1].
• A run has at most $N$ steps. A demand equal to the remaining capacity is served. Every run, anticipative ones included, stops at the first customer not fully served.
• Adaptive policies are functions of the chosen list and the demand vector that depend only on the chosen customers' demands, with measurable decision events. Anticipative policies are permutations, embedded as adaptive policies that ignore the demands.
• Randomized policies are finite mixtures. Service levels are probabilities, not the long-run scenario frequencies of p. 11.
• $Q^{\mathrm{Adap}}_I$, $Q^{\mathrm{Anti}}_I$ and $Q_{II}$ are real infima. Under the standing assumptions every feasible set is non-empty ($Q = N\Delta$ works) and bounded below by $0$, so no value is a junk default. $Q_{II}$ uses the subset form $\Gamma(Q)$, which p. 17 shows equals the Type-II problem (CPP-B).
• The greedy fill is stated for a priority order $\sigma$ rather than for weights $\theta'$. It equals $x^*(\theta', \tilde d, Q)$ for every $\theta'$ whose decreasing order, ties broken by index, is $\sigma$.
• Two encodings would trivialize the goal, and both are excluded. Restricting to deterministic priority orders makes Theorem 3 false. Letting adaptive runs skip an oversized customer and continue enlarges the adaptive class beyond the paper's.

The infrastructure the proofs need: measurability of runs, independence of functions of disjoint coordinates, continuity of $Q \mapsto \mathbf E[\min(Q, S)]$ (so that $Q_{II}$ is attained), and the greedy description of a polymatroid's base polytope. Proofs of any milestone are welcome. So are alternative proofs of milestone 1 that avoid the general polymatroid theorem.

Selected references

• G. Lyu, M. C. Chou, C.-P. Teo, Z. Zheng, Y. Zhong, Stochastic Knapsack Revisited: The Service Level Perspective, SSRN working paper 3674463, 2021. https://ssrn.com/abstract=3674463
• Y. Zhong, Z. Zheng, M. C. Chou, C.-P. Teo, Resource Pooling and Allocation Policies to Deliver Differentiated Service, Management Science 64(4), 1555–1573, 2018.
• A. Alptekinoğlu, A. Banerjee, A. Paul, N. Jain, Inventory Pooling to Deliver Differentiated Service, Manufacturing & Service Operations Management 15(1), 33–44, 2013.
• B. C. Dean, M. X. Goemans, J. Vondrák, Approximating the Stochastic Knapsack Problem: The Benefit of Adaptivity, Mathematics of Operations Research 33(4), 945–964, 2008. https://doi.org/10.1287/moor.1080.0330

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

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

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

1. 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]$.
2. 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)$.
3. Proposition A.6 (p. 36): $V$, $p$ and $E$ are nondecreasing in $x$.
4. Corollary A.4 (p. 35): the fictitious default algorithm stops at $V(x)$, and every matrix it inverts is nonsingular.
5. §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.