All missions

Motivation

A Nash equilibrium of a two-player game is a pair of choices from which neither player can improve by changing their own choice alone. Computing one equilibrium is a central task in algorithmic game theory. For unrestricted bimatrix games, their payoff tables may encode difficult equilibrium computations. The structure of a rank-one bimatrix game gives a more specific question: can one equilibrium be found in time polynomial in the binary description of the game, even when equilibria are not isolated? Adsul, Garg, Mehta, Sohoni and von Stengel answer this with their BINSEARCH algorithm in Fast Algorithms for Rank-1 Bimatrix Games, Theorem 19. Their analysis explicitly includes degenerate games, which can have continua of equilibria (p. 5).

The paper develops a geometric account of rank reduction, parameterized linear programs, the connected set of equilibria of the auxiliary games, and the binary search procedure. The present mission targets the algorithmic result. The separately stated results on enumeration, exponentially many equilibria, and a structure theorem are outside this mission (Adsul et al., §§6–9).

Setting

An $m\times n$ bimatrix game has payoff matrices $A,B\in\mathbb R^{m\times n}$. Player 1 chooses a row and player 2 chooses a column. A mixed strategy assigns nonnegative weights summing to one to a player's pure strategies. Write $X\subseteq\mathbb R^m$ and $Y\subseteq\mathbb R^n$ for the two simplices. Against mixed strategies $x\in X$ and $y\in Y$, the payoffs are $x^\top Ay$ and $x^\top By$. The pair is a Nash equilibrium when each strategy maximizes its owner's payoff against the other. These are the paper's definitions on pp. 4–5.

The games studied here have the form

$$(A,B)=(A,-A+ab^\top),\qquad a\in\mathbb R^m,\ b\in\mathbb R^n.$$

The sum of the two payoff matrices is $ab^\top$, so its rank is at most one. Zero vectors are allowed; the zero-sum case is included. A real parameter $\lambda$ defines an auxiliary game $(A,-A+\mathbf1\lambda b^\top)$. The set $\mathcal N$ consists of triples $(\lambda,x,y)$ for which $(x,y)$ is an equilibrium of that auxiliary game. The desired equilibria are the triples in $\mathcal N$ that also satisfy $x^\top a=\lambda$ (equations (10)–(12)).

For each $\lambda$, a primal linear program $P_\lambda$ minimizes $v$ subject to $A^\top x+\mathbf1v-s=b\lambda$, $x\in X$, and $s\ge0$. Its dual $D_\lambda$ maximizes $\lambda b^\top y+t$ subject to $Ay+\mathbf1t\le0$ and $y\in Y$. Their optimal solutions describe the auxiliary equilibria. The sets $M(\lambda)$ and $N(\lambda)$ identify the inequalities that can be slack or the coordinates that can be positive on the dual optimal face. They define a face $P(M,N)$ of the parameterized primal polyhedron (equations (17)–(29)).

Formalization targets

The goal is Theorem 19: for rational $A,a,b$ of combined binary length $L$, and polynomial-time LP solvers returning extreme optimal solutions, Figure 2's BINSEARCH finds a Nash equilibrium of $(A,-A+ab^\top)$ in polynomial time in $L$. In the formal statement, a polynomial $p$ is chosen before the dimensions, game data, and admissible LP-selection oracle. It bounds the number of main-loop iterations, the bit length of every midpoint parameter passed to $P_\lambda$, and the bit length of every returned $\lambda^*$, including the parameter passed to the final $D_{\lambda^*}$:

$$\exists p\in\mathbb N[T]\;\forall A,a,b,O\;\exists k\le p(L):\quad x_k^{*\top}a=\lambda_k^*,\quad (x_k^*,y)\text{ is an equilibrium of }(A,-A+ab^\top)$$

for every optimal $y$ returned by the final dual LP, with the stated bound on each intermediate parameter. The ordered milestones cover best responses (Lemma 1), rank reduction (Lemma 6 and Theorem 7), primal-dual optimality (Lemma 9), preservation of the bracket (Lemma 17), the segment test (Lemma 18), and separation of distinct breakpoints (proof of Theorem 19).

Significance

The theorem gives an algorithm whose performance guarantee depends on the input's bit length, not on the number of equilibria. This matters for degenerate games: a continuum of equilibria does not by itself supply an algorithm to find one. The auxiliary LPs also connect game-theoretic best responses to ordinary finite-dimensional optimization. These claims and their precise scope are in §§4–5 of the paper.

The paper proves the theorem on paper. This mission asks for a machine-checked version of its formal statements and, ultimately, the proof. The definitions of best responses, primal and dual feasible sets, optimal faces, breakpoints, and a rational-input LP oracle are reusable in other formalizations of parametric games. The draft theorem declarations contain proof placeholders; they are targets rather than completed machine-checked proofs.

Difficulty

Ordinary bisection finds an interval containing an equilibrium parameter, but it can continue indefinitely when the equilibrium lies at a breakpoint: the two bounds can remain in neighboring segments. Repeated midpoints also create parameters whose bit descriptions grow with the number of iterations. Figure 2 therefore uses additional LPs that search the current optimal face and, in a strict branch, replace the answer by a breakpoint. A correctness proof must cover every permitted extreme optimal answer from these LPs, including degenerate faces, and must bound the separation of rational breakpoints (pp. 17–22).

Formalization scope

Lean represents pure strategies by zero-based Fin m and Fin n, mixed strategies by real standard simplices, and payoffs by real matrices and vectors. The goal's input entries are rational and cast to reals for the LPs. It assumes $m,n>0$: the paper leaves this implicit, while its minimum over the entries of $a$ and both mixed-strategy simplices require nonempty index sets. The game may be degenerate and may have rank zero.

LP optima are members of feasible sets whose objective is least or greatest on the full feasible objective image. An extreme LP solution also lies in the feasible set's extreme-point set. A selection oracle is constrained whenever an optimal extreme solution exists, and the goal asserts that every LP actually called during the run has such an answer. This excludes arbitrary values from an oracle at an infeasible or unbounded call. The initial bracket is the minimum and maximum entry of $a$; every branch and BR replacement follows Figure 2. The breakpoint endpoint symbols $\lambda_0=-\infty$ and $\lambda_{K+1}=+\infty$ are represented by absent optional finite endpoints in Lemma 18.

The running-time clause is an iteration bound together with a bound on the binary size of the midpoint and returned LP parameters; it does not formalize a machine model or the assumed polynomial-time LP solver. The goal is about the specified BINSEARCH run for every admissible selection oracle. Existence of some Nash equilibrium or termination for one hand-picked oracle would not express Theorem 19. Lemma 6 uses $\lambda=x^\top a$, the condition used in its printed proof; with a freely fixed $\lambda$, its printed implication (a) to (b) is false. A full development needs finite-dimensional LP duality, extreme-point and rational-vertex bounds, convex optimal-face geometry, and control of the run invariant. Contributions proving these components are welcome.

Selected references

• B. Adsul, J. Garg, R. Mehta, M. Sohoni and B. von Stengel, Fast Algorithms for Rank-1 Bimatrix Games, Operations Research, 2021; arXiv:1812.04611v4, the pinned source for this mission.

Motivation

A bilevel program is an optimization problem in which one of the constraints is itself an optimization problem. An upper-level decision maker (a leader) chooses $x$; a lower-level decision maker (a follower) responds with an optimal solution $y$ of a problem parameterized by $x$; the leader's cost $F(x,y)$ depends on both. Stackelberg games, toll setting on transportation networks, hyperparameter selection in machine learning, and many pricing and network design problems in operations research have this form. See Dempe, Foundations of Bilevel Programming (Kluwer, 2002), and Dempe and Zemkoho (eds.), Bilevel Optimization (Springer, 2020).

Necessary optimality conditions for bilevel programs are hard to obtain because the follower's optimality is not a standard constraint. The value function approach of Outrata (1990) replaces "$y$ is optimal for the lower level" by the single inequality $f(x,y)-V(x)\le0$, where $V$ is the optimal value of the lower level. This gives an equivalent single-level problem, but a well-known obstacle follows: Ye and Zhu (1995) showed that the standard nonsmooth constraint qualifications (nonsmooth MFCQ, equivalently NNAMCQ) fail at every feasible point of this reformulation. KKT-type conditions have therefore relied on calmness (Clarke 1983) or on partial calmness (Ye and Zhu 1995), both of which are strong.

Gfrerer (2013) introduced directional versions of regularity conditions, required only along one critical direction. Bai and Ye (arXiv:2004.01783, Mathematics of Operations Research 2022) carry this idea to the value function approach. They define calmness in a direction, prove a directional KKT condition for a general inequality-constrained problem under it, and apply this to the value-function reformulation of a bilevel program. This mission formalizes that chain, up to the paper's Theorem 5.1.

Setting

Let $F,f:\mathbb R^n\times\mathbb R^m\to\mathbb R$, $g:\mathbb R^n\times\mathbb R^m\to\mathbb R^p$ and $G:\mathbb R^n\times\mathbb R^m\to\mathbb R^q$ be continuously differentiable. For each $x$, $S(x)$ is the solution set of the lower level program $(P_x)$: $\min_y f(x,y)$ subject to $g(x,y)\le0$. The bilevel program is

$$\text{(BP)}\qquad \min_{x,y}\ F(x,y)\quad\text{s.t.}\quad y\in S(x),\ \ G(x,y)\le0.$$

The value function is $V(x)=\inf_y\{f(x,y)\mid g(x,y)\le0\}\in[-\infty,+\infty]$, and the value-function reformulation is

$$\text{(VP)}\qquad \min_{x,y}\ F(x,y)\quad\text{s.t.}\quad f(x,y)-V(x)\le0,\ \ g(x,y)\le0,\ \ G(x,y)\le0.$$

All norms are Euclidean, and $\mathbb B$ is the open unit ball. For a direction $d$ and $\varepsilon,\delta>0$, the directional neighbourhood is

$$\mathcal V_{\varepsilon,\delta}(d)=\{z\in\varepsilon\mathbb B\mid \big\|\|d\|z-\|z\|d\big\|\le\delta\|z\|\|d\|\}.$$

It is a cone of half-angle governed by $\delta$ around the ray through $d$, cut at radius $\varepsilon$; for $d=0$ it is the whole ball $\varepsilon\mathbb B$.

(VP) is calm at $(\bar x,\bar y)$ in direction $d$ if there are $\varepsilon,\delta,\rho>0$ such that $F(x,y)-F(\bar x,\bar y)+\rho\|\alpha\|\ge0$ for every perturbation $\alpha\in\varepsilon\mathbb B$ of the right-hand sides and every $(x,y)\in(\bar x,\bar y)+\mathcal V_{\varepsilon,\delta}(d)$ that satisfies the perturbed constraints. The same definition (Definition 3.1) applies to a general problem (P): $\min\varphi(z)$ s.t. $\phi(z)\le0$.

A map $h$ is directionally Lipschitz at $\bar x$ in direction $u$ if it is Lipschitz on $\bar x+\mathcal V_{\varepsilon,\delta}(u)$ for some $\varepsilon,\delta>0$. Its directional derivative is $h'(\bar x;u)=\lim_{t\downarrow0}(h(\bar x+tu)-h(\bar x))/t$.

The directional limiting subdifferential $\partial\varphi(\bar x;u)$ collects the limits of Fréchet subgradients $\xi^k\in\widehat\partial\varphi(\bar x+t_ku^k)$ with $t_k\downarrow0$, $u^k\to u$ and $\varphi(\bar x+t_ku^k)\to\varphi(\bar x)$.

The critical cone $C(\bar x,\bar y)$ of (VP) consists of the $(u,v)$ with

• $\nabla f(\bar x,\bar y)(u,v)\le V'(\bar x;u)$;
• $\nabla g_i(\bar x,\bar y)(u,v)\le0$ and $\nabla G_j(\bar x,\bar y)(u,v)\le0$ on the active indices;
• $\nabla F(\bar x,\bar y)(u,v)\le0$.

Formalization targets

Goal: Theorem 5.1 (p. 22)

Let $(\bar x,\bar y)$ be a local minimizer of (BP). Suppose $V$ is directionally Lipschitz and directionally differentiable at $\bar x$ in direction $u$, that $(u,v)\in C(\bar x,\bar y)$, and that (VP) is calm at $(\bar x,\bar y)$ in direction $(u,v)$. Then there exist $\lambda_V\ge0$, $\lambda_g\in\mathbb R^p$ and $\lambda_G\in\mathbb R^q$ with

$$0\in\nabla F(\bar x,\bar y)+\lambda_V\nabla f(\bar x,\bar y)+\lambda_V\,\partial(-V)(\bar x;u)\times\{0\}+\nabla g(\bar x,\bar y)^T\lambda_g+\nabla G(\bar x,\bar y)^T\lambda_G,$$ $$0\le\lambda_g\perp g(\bar x,\bar y),\quad \lambda_g\perp\nabla g(\bar x,\bar y)(u,v),\quad 0\le\lambda_G\perp G(\bar x,\bar y),\quad \lambda_G\perp\nabla G(\bar x,\bar y)(u,v).$$

Milestones

1. (BP) and (VP) have the same feasible points (§1, p. 2).
2. Along $u\in C(\bar z)$, $\|\phi_+(\bar z+tu)\|/t\to0$ (proof of Theorem 3.1, p. 10).
3. Equation (7): $\lim_{t\downarrow0}\big(\varphi(\bar z+tu)+\rho\|\phi_+(\bar z+tu)\|-\varphi(\bar z)\big)/t=0$ (p. 10).
4. $N_{\mathbb R^q_-}(a;d)=\{\xi\mid0\le\xi\perp a,\ \xi\perp d\}$ for tangent $d$ (p. 11, with eq. (1), p. 5).
5. Theorem 3.1 (p. 9): under directional calmness of (P), a local minimizer satisfies $0\le\lambda\perp\phi(\bar z)$, $\lambda\perp\phi'(\bar z;u)$ and $0\in\nabla\varphi(\bar z)+\partial\langle\lambda,\phi\rangle(\bar z;u)$.
6. The directional sum rule $\partial(f-V)((\bar x,\bar y);(u,v))=\nabla f(\bar x,\bar y)+\partial(-V)(\bar x;u)\times\{0\}$ (proof of Theorem 5.2, p. 25).
7. A directionally Lipschitz function has $\partial\varphi(\bar x;u)\ne\emptyset$ (proof of Theorem 4.2(i), p. 20).

Significance

Theorem 5.1 gives a KKT condition for bilevel programs under a regularity assumption checked in one critical direction only. Directional calmness is weaker than classical calmness, because the neighbourhood $\mathcal V_{\varepsilon,\delta}(u,v)$ is smaller than a ball. The conclusion is also sharper than the nondirectional KKT condition: the subdifferential of $-V$ is the directional one, and the multipliers satisfy the extra orthogonality conditions with $\nabla g(\bar x,\bar y)(u,v)$ and $\nabla G(\bar x,\bar y)(u,v)$. Example 3.1 of the paper is a bilevel program in which partial calmness and calmness fail but calmness in a nonzero critical direction holds. Theorem 5.1 applies there, and the classical results do not. Section 5 of the paper derives verifiable sufficient conditions (directional quasi-normality, Theorems 5.2–5.3) from it.

The result is proved in the paper; nothing here is open mathematically. To our knowledge none of it has been machine-checked. A formal proof would check a chain that passes through Ekeland's variational principle, a Fermat rule and a chain rule for limiting subdifferentials, and a limiting argument with directional sequences. The general Theorem 3.1 is reusable for any inequality-constrained program with directionally Lipschitz constraints.

Difficulty

The obvious route is "calmness gives exact penalization, then Fermat's rule". For directional calmness this only says that $(\bar x,\bar y)$ minimizes the penalized function on the directional neighbourhood, which is not a neighbourhood of $(\bar x,\bar y)$. Fermat's rule cannot be applied at $(\bar x,\bar y)$ itself, so the stationarity must be produced at points inside the cone that approach $(\bar x,\bar y)$ along the direction, and then passed to the limit. That passage needs the multipliers to be bounded and the limiting subgradients to be directional ones.

The bilevel step adds two obstacles. The constraint $f-V$ is nonsmooth and extended-valued, so its subdifferential has to be split exactly into $\nabla f$ and the $x$-part of $\partial(-V)$. And when $\lambda_V=0$ the conclusion still requires an element of $\partial(-V)(\bar x;u)$, which exists only because $V$ is directionally Lipschitz.

Formalization scope

• Spaces. Constraint values live in EuclideanSpace ℝ (Fin q) (E q). The pair $(x,y)$ lives in WithLp 2 (E n × E m), the Euclidean product; the bare product type would carry the sup norm. Theorem 3.1 and its milestones are stated on any finite-dimensional real inner product space, which is linearly isometric to $\mathbb R^N$; this lets the goal apply Theorem 3.1 on the product.
• Value function. $V$ is an EReal-valued infimum: $+\infty$ when the lower level is infeasible, $-\infty$ when it is unbounded. The constraint $f-V\le0$ of (VP) is evaluated in EReal. "$V$ directionally Lipschitz" includes finiteness of $V$ on $\bar x+\mathcal V_{\varepsilon,\delta}(u)$, which Definition 2.4 leaves implicit because it is written for real-valued maps. Directional differentiability is that of $V$ as a real function on that set, and its value $V'(\bar x;u)$ is passed explicitly and enters the critical cone.
• Encodings. $t_k\downarrow0$ is $t_k>0$, $t_k\to0$. The Fréchet subgradient is the published NonconvexSplitting.Shared.IsRegularSubgrad, and the directional normal cone is the published SetConstrSOC.Directional.dirLimNormal. Each $\perp$ is an inner product, and $\nabla g^T\lambda_g$ is $\sum_i(\lambda_g)_i\nabla g_i$. "$0\in\ldots+\lambda_V\partial(-V)(\bar x;u)\times\{0\}+\ldots$" is stated as the existence of one $\xi\in\partial(-V)(\bar x;u)$ that makes the sum zero, including when $\lambda_V=0$.
• Printed slips. The critical cone of (VP) on p. 22 prints "$F(\bar x,\bar y)(u,v)\le0$", read as $\nabla F(\bar x,\bar y)(u,v)\le0$ (as in Example 3.1). The critical cone on p. 8 prints $C(z)$ and $\nabla\varphi(z)$, read as $C(\bar z)$ and $\nabla\varphi(\bar z)$.
• Generalizations. Milestone 6 assumes only that $V(\bar x)$ is finite, and milestone 7 is stated for every directionally Lipschitz function.
• Ruled out. Dropping the direction from the subdifferential, dropping the value convergence $\varphi(\bar x+t_ku^k)\to\varphi(\bar x)$, restricting the calmness perturbation $\alpha$ to $0$, or allowing $\lambda_V=0$ without an element of $\partial(-V)(\bar x;u)$ would each give a different, weaker or vacuous statement. The definitions here keep all four.

A complete development needs Ekeland's variational principle (on the platform as EkelandVP.General.ekeland_variational_principle) and the Fréchet and limiting subdifferential calculus: the Fermat rule, the sum rule with a smooth function, and the chain rule for a Lipschitz composition. It also needs the fact that Lipschitz functions have bounded subgradients. These are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the subdifferential calculus lemmas as separate theorems.

Selected references

• K. Bai, J. J. Ye, Directional necessary optimality conditions for bilevel programs, arXiv:2004.01783v3; Mathematics of Operations Research 47 (2022). https://arxiv.org/abs/2004.01783
• H. Gfrerer, On directional metric regularity, subregularity and optimality conditions for nonsmooth mathematical programs, Set-Valued and Variational Analysis 21 (2013) 151–176. https://doi.org/10.1007/s11228-012-0220-5
• J. J. Ye, D. L. Zhu, Optimality conditions for bilevel programming problems, Optimization 33 (1995) 9–27. https://doi.org/10.1080/02331939508844060
• J. V. Outrata, On the numerical solution of a class of Stackelberg problems, Zeitschrift für Operations Research 34 (1990) 255–277. https://doi.org/10.1007/BF01416737
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• S. Dempe, Foundations of Bilevel Programming, Kluwer, 2002. https://doi.org/10.1007/b101970

Group buying with sign-up thresholds

In a group-buying event a retailer offers a product at a discount that materializes only if enough customers sign up before a deadline. Platforms such as Taobao and JD run such events with several deal levels: the more customers join, the lower the final price. Each arriving customer must decide whether to join without knowing how many others will follow, so the sign-up decisions form a dynamic game among customers who arrive one at a time.

Much of the theory of group buying works with batch sign-ups, where all customers decide simultaneously (Anand and Aron 2003; Jing and Xie 2011), or compares simultaneous and sequential mechanisms (Hu, Shi and Wu 2013). Ming and Tunca (SSRN 3352047; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1083) model the event in continuous time with a deposit and two deal thresholds, as on Taobao. They characterize the customers' equilibrium sign-up behaviour as a function of elapsed time and the current sign-up count, and use that characterization for structural estimation on Taobao data. This mission formalizes the theoretical part: Lemma 1 and Proposition 1 of §3.

The model

The event runs on a time window $[0,T]$, $T>0$. Customers arrive according to a Poisson process with rate $\lambda_g>0$. Each customer has unit demand and a reservation utility $u$ drawn from a probability law $\mu$ on $\mathbb R$ with c.d.f. $F$; the outside option is worth $0$.

A customer who joins pays a non-refundable deposit $d>0$. The platform fixes two sign-up thresholds $M_1\le M_2$, natural numbers with $M_1>0$. The retailer announces a base price $p_0$ and a deal discount $\delta$, which give the deal prices

$$p_1=p_0-\delta,\qquad p_2=p_1-\delta,\qquad p_2\ge d.$$

If the total number $N$ of sign-ups by time $T$ is below $M_1$ the price is $p_0$, if $M_1\le N<M_2$ it is $p_1$, and if $N\ge M_2$ it is $p_2$. After the event, a customer who joined either pays the balance or walks away and loses the deposit, so his surplus is $\max\{u-p,-d\}$.

A customer arriving at time $t$ sees the number $N_t=k$ of earlier sign-ups. Write $\pi^1_k(t)$ for the probability that only the first deal happens, and $\pi^2_k(t)$ for the probability that the second deal happens, given $N^+_t=k$ sign-ups on $[0,t]$. Joining moves the count to $k+1$, so the expected utility of signing up is

$$V_k(u,t)=\pi^1_{k+1}(t)\max\{u-p_1,-d\}+\pi^2_{k+1}(t)\max\{u-p_2,-d\}+\big(1-\pi^1_{k+1}(t)-\pi^2_{k+1}(t)\big)\max\{u-p_0,-d\}. \tag{1}$$

The customer signs up if and only if $V_k(u,t)\ge0$, and the sign-up probability is $H_k(t)=\mu\{u: V_k(u,t)\ge0\}$ (2).

Conditioning on the arrival time $t+x$ of the next customer, which is exponential with rate $\lambda_g$, gives the conditioning equations: for $k<M_2$,

$$\pi^2_k(t)=\int_0^{T-t}\big(H_k(t+x)\pi^2_{k+1}(t+x)+(1-H_k(t+x))\pi^2_k(t+x)\big)\lambda_g e^{-\lambda_g x}\,dx, \tag{4}$$

and the same equation (5) for $\pi^1_k$ when $k<M_1$. The boundary conditions are $\pi^1_k=0$, $\pi^2_k=1$ for $k\ge M_2$, and $\pi^1_k=1-\pi^2_k$ for $M_1\le k<M_2$. A dynamic consumer equilibrium is a family $(\pi^1_k,\pi^2_k)_{k\ge0}$ of $[0,1]$-valued measurable functions satisfying (2), (4), (5) and these boundary conditions on $[0,T]$.

Formalization targets

Goal: Proposition 1

For $d>0$ and $0<\delta<p_0/2$:

1. a dynamic consumer equilibrium exists, and any two agree on $[0,T]$;
2. in equilibrium a customer signs up if and only if $u\ge\bar u_{k,t}$, where $\bar u_{k,t}$ is the explicit threshold (3) evaluated at $(\pi^1_{k+1}(t),\pi^2_{k+1}(t))$;
3. $H_k(t)=1-F(\bar u_{k,t})$ (7), and for $0\le k<M_i$, $i=1,2$,

$$\pi^i_k(t)=\lambda_g\int_t^T e^{-\lambda_g\int_t^s H_k(v)\,dv}\,H_k(s)\,\pi^i_{k+1}(s)\,ds. \tag{6}$$

Milestones

• Lemma 1 (p. 9): for probabilities $a,b\ge0$ with $a+b\le1$, $V\ge0$ if and only if $u\ge\bar u(a,b)$, and $\bar u(a,b)\in[p_2,p_0]$.
• Boundary condition (i) (p. 8): $\pi^1_k(T)=0$ for $k<M_1$ and $\pi^2_k(T)=0$ for $k<M_2$.
• (4) ⇔ (A.14) (proof of Proposition 1): the conditioning equation and the closed form (6) have the same bounded solutions.
• (7) (proof of Proposition 1): $\mu\{u:V\ge0\}=1-F(\bar u)$.
• $H_k(t)=1-F(p_2)$ for $k\ge M_2-1$ (p. 9).

Significance

Proposition 1 turns an equilibrium of a continuous-time game, defined implicitly by the conditioning equations, into a backward recursion over the sign-up count that can be computed. The structural estimation of §4 uses this recursion: the likelihood of the observed sign-up times is built from the equilibrium intensities $\lambda_g H_k(t)$, so without the proposition the estimator has no well-defined object. The threshold structure of Lemma 1 also underlies the paper's discussion of drop-outs after the event.

The result is proved on paper; nothing in this model has been formalized. The paper's proof differentiates (4) without stating any regularity of $\pi$ or $H$, and leaves implicit the facts that the beliefs stay in the probability simplex along the induction and that $H_k$ is measurable in $t$. A machine-checked proof settles these points. Printed slips in (6) and (A.14) are corrected in the statements (see Formalization scope).

Difficulty

The obvious argument is the paper's: differentiate (4), solve the resulting linear ODE with an integrating factor, and induct backwards from $k=M_2$. This argument assumes that $\pi^2_k$ is differentiable, which is not known a priori. Only measurability and boundedness are available, so the equivalence of (4) and (6) has to be proved at the level of integral equations: uniqueness through a Volterra-type estimate for bounded measurable solutions, and existence by checking that the closed form solves (4). The induction also has to carry two invariants that the paper does not mention. The beliefs $(\pi^1_{k+1},\pi^2_{k+1})$ must stay in the simplex so that Lemma 1 applies at the next step, and $H_k$ must be measurable so that the integrals in (4)–(6) mean anything. Lemma 1 itself is a three-branch case analysis with divisions by $\pi^2_{k+1}$ and $\pi^1_{k+1}+\pi^2_{k+1}$.

Formalization scope

Everything lives in the namespace GroupBuyEq.Signup; one definitions file, GroupBuyEq.Signup.Model, holds the objects.

• Parameters. A structure Params holds $T$, $\lambda_g$ (lam), $M_1,M_2\in\mathbb N$, $p_0$, $\delta$ and $d$. $p_1,p_2$ are derived. Standing bundles $0<T$, $0<\lambda_g$, $0<M_1\le M_2$, $d>0$, $0<\delta<p_0/2$ and $d\le p_2$. $T>0$ and $\lambda_g>0$ are implicit on the page.
• Utility law. $\mu$ is a probability measure on $\mathbb R$ without atoms (NullSingletonClass). This is weaker than the paper's density assumption. $F$ is Mathlib's ProbabilityTheory.cdf μ.
• Equilibrium. It is the solution of the conditioning equations (2), (4), (5) with boundary conditions (ii)–(iii), with all quantities in $\mathbb R$. The Poisson process is not modelled, and neither is the identification of $\pi^i_k$ as its conditional probabilities. (4) is imposed only for $k<M_2$ and (5) only for $k<M_1$: at $k\ge M_2$ the boundary value $\pi^2=1$ contradicts (4). The beliefs must be measurable and $[0,1]$-valued on $[0,T]$, so that the integrals are genuine. $\pi^1+\pi^2\le1$ is not imposed; it follows. Uniqueness means agreement on $[0,T]$.
• Corrected slips. (6) is stated with $H_k$ where the page prints $H_{k+1}$: the next arrival after $N_t=k$ joins with probability $H_k$, as in (4), (A.10) and (A.14). (A.14) is stated with one factor $\lambda_g$ instead of the printed two.
• Lemma 1 is stated for $d>0$: at $d=0$, which the printed branch "$0\le d$" allows, every customer has $V\ge0$ and the equivalence fails.

Not trivializations. The equilibrium is not defined by (6), which would make existence definitional, and $H_k$ is not defined by (7), which would bypass Lemma 1: $H_k$ is the $\mu$-measure of $\{u:V_k(u,t)\ge0\}$.

A complete development needs:

• interval integrals with a parametric inner integral;
• a Gronwall or Volterra uniqueness lemma for bounded measurable solutions;
• measurability of $t\mapsto\mu\{u:V(a(t),b(t),u)\ge0\}$;
• the case analysis of Lemma 1.

The equivalence (4) ⇔ (6) is a generic statement about linear integral equations with an exponential kernel and is reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• L. Ming and T. I. Tunca, Consumer Equilibrium, Demand Effects, and Efficiency in Group Buying, SSRN working paper 3352047, version of 2020-05-15. https://ssrn.com/abstract=3352047 (published in Manufacturing & Service Operations Management, https://doi.org/10.1287/msom.2022.1083).
• K. S. Anand and R. Aron, Group buying on the web: A comparison of price-discovery mechanisms, Management Science 49(11), 1546–1562, 2003. https://doi.org/10.1287/mnsc.49.11.1546.20582
• X. Jing and J. Xie, Group buying: a new mechanism for selling through social interactions, Management Science 57(8), 1354–1372, 2011. https://doi.org/10.1287/mnsc.1110.1366
• M. Hu, M. Shi and J. Wu, Simultaneous vs. sequential group-buying mechanisms, Management Science 59(12), 2805–2822, 2013. https://doi.org/10.1287/mnsc.2013.1740

Motivation

Load balancing asks for an assignment of $n$ jobs to $m$ machines that keeps the largest machine load, the makespan, small. On unrelated machines the processing time of a job may depend arbitrarily on the machine; the deterministic problem has the classical $2$-approximation of Lenstra, Shmoys and Tardos (1990). In many applications (virtual-circuit routing, assigning customers to warehouses, cloud jobs) the processing times are not known when the assignment is made, only their distributions are. The assignment is fixed up front, the sizes are then revealed, and the quantity to control is the expected makespan.

Timeline:

• Kleinberg, Rabani and Tardos (1997/2000) gave the first constant-factor approximation for the expected makespan on identical machines, introducing truncated and exceptional parts and an effective size measured at the parameter $k=m$.
• Gupta, Kumar, Nagarajan and Shen (SODA 2018; arXiv:1904.07271) gave the first $O(1)$-approximation on unrelated machines (Theorem 1), the result formalized here, together with a budgeted variant and an $O(q/\log q)$-approximation for $q$-norms.
• Molinaro (2019) obtained an $O(1)$-approximation for the expected $q$-norm for all $q\ge1$, combining the techniques of this paper with a different notion of effective size (the L-function method).

Setting

There are machines $[m]$ and jobs $[n]$. On a probability space, the random variable $X_{ij}\ge 0$ is the size of job $j$ on machine $i$. Jobs are independent: the vectors $(X_{ij})_{i\in[m]}$ for different $j$ are independent, while the sizes of one job on different machines may be correlated. An assignment $\sigma:[n]\to[m]$ puts the jobs $J_i=\sigma^{-1}(i)$ on machine $i$, and its expected makespan is

$$\mathbb E\Big[\max_{i\in[m]}\sum_{j\in J_i}X_{ij}\Big].$$

Every size splits into a truncated part $X'_{ij}=X_{ij}\mathbf 1(X_{ij}\le 1)$ and an exceptional part $X''_{ij}=X_{ij}\mathbf 1(X_{ij}>1)$. The effective size of a random variable $Y$ at an integer $k\ge2$ is

$$\beta_k(Y)=\frac{1}{\log k}\log\mathbb E\big[e^{(\log k)Y}\big],\qquad \beta_1(Y)=\mathbb E[Y].$$

The algorithm works at a scale $M>0$ on the sizes $X_{ij}/M$. With $z_i(k)=\sum_j\beta_k(X'_{ij})y_{ij}$, the LP with parameter $b$ asks for $y\ge0$ with

$$\sum_i y_{ij}=1\ (5),\qquad \sum_{i,j}\mathbb E[X''_{ij}]y_{ij}\le2\ (7),\qquad \sum_{i\in K}z_i(|K|)\le b\,|K|\ \ \forall K\ne\emptyset\ (8).$$

The class loop starts with $L=[m]$; while $L\neq\emptyset$ it gives the machines $\{i\in L: z_i(|L|)\le b\}$ the class $\ell=|L|$ and removes them. The class $\ell_i$ defines a generalized assignment instance with processing times $p_{ij}=\beta_{\ell_i}(X'_{ij})$ and costs $c_{ij}=\mathbb E[X''_{ij}]$, which the Shmoys–Tardos algorithm rounds to an assignment with

$$\sum_{i}\sum_{j\in J_i}\mathbb E[X''_{ij}]\le 2\ \ (13),\qquad \sum_{j\in J_i}\beta_{\ell_i}(X'_{ij})\le b+1\ \ \forall i\ \ (14).$$

Formalization targets

Goal: Theorem 1, pinned to the procedure

There is an absolute constant $c_0>0$ such that for every instance and every $M>0$:

$$\text{(A)}\quad \exists\,\sigma:\ \mathbb E[\text{makespan}(\sigma)]\le c_0M\ \Longrightarrow\ \text{the LP for } X/M \text{ with } b=17 \text{ is feasible};$$ $$\text{(B)}\quad b\ge0,\ y \text{ feasible for } X/M \ \Longrightarrow\ \text{some } \sigma \text{ satisfies (13)–(14)};$$ $$\text{(C)}\quad \sigma \text{ satisfies (13)–(14)}\ \Longrightarrow\ \mathbb E\Big[\max_i\sum_{j\in J_i}X_{ij}\Big]\le(4b+10)\,M.$$

For $\mathrm{OPT}>0$, taking $M=\mathrm{OPT}/c_0$, (A)–(C) give an assignment of expected makespan at most $78\,\mathrm{OPT}/c_0$; a binary search over $M$ loses a factor $2$. The constant $c_0$ is left unspecified so that the goal survives any improvement of the lower-bound constants.

Milestones

In attack order: Lemma 1 (exceptional items lower bound) and Lemma 4 (truncated items lower bound); Lemma 5 (valid inequalities) and Proposition 1 (LP lower bound), which give (A); Observation 1 (the class loop terminates; at most $\ell$ machines of class $\le\ell$) and Observation 2 (the GAP rounding), which give (B); Lemma 2 (effective-size Chernoff bound), the effective-size facts $0\le\beta_k(Y)\le1$ and $\beta_k(Y)\ge\mathbb E[Y]$, Observation 3 (tail $\ell_i^{-\alpha}$), Lemma 7 (union bound over classes) and Lemma 6 (expected makespan $\le 4b+10$), which give (C).

Significance

Theorem 1 shows that the expected makespan on unrelated machines, a quantity that is #P-hard even to evaluate for a fixed assignment (Theorem 4 of the paper), can be approximated within a constant factor by a polynomial-size certificate: an LP with one effective-size constraint per subset of machines, measured at the parameter $|K|$. The same LP technique underlies the budgeted variant in the same paper and enters the later $q$-norm results (Molinaro 2019). Lemma 6 is a converse of the valid inequalities that needs only one constraint per machine, which is what makes the rounding through the generalized assignment problem possible.

All results here are proved on paper; none is formalized. A formalization produces a reusable effective-size calculus (Lemma 2, Jensen-type bounds) in Mathlib's probability library, an expected-maximum lower bound for independent variables (Lemma 1), and a Lean version of the Shmoys–Tardos rounding with costs. It also records two corrections found while pinning the statements: Lemma 5's inequality (3) fails under the threshold $1$ as printed (a $1000$-machine instance with expected makespan $\approx0.989$ has $\sum\mathbb E[X'']\approx3.57$), so the threshold is an absolute constant $c_0$; and Lemma 1 requires independence, which the page omits.

Difficulty

The obvious approach maps every random size to one deterministic number and balances those. The paper shows (p. 7) that every such approach loses a factor $\Omega(\log m/\log\log m)$ on unrelated machines: the right effective size of a job depends on how many machines it competes for, which is not known in advance. The LP sidesteps this with exponentially many constraints, one per subset of machines, and the rounding cannot satisfy them all. The upper bound therefore rests on the class loop picking, for each machine, one parameter $\ell_i$ such that few machines have small classes and machines of large class have tails decaying like $\ell_i^{-\alpha}$. On the lower-bound side, Lemma 4 rests on the Kleinberg–Rabani–Tardos analysis of Bernoulli variables, which the paper only cites, and Observation 2 rests on the Shmoys–Tardos rounding, also only cited.

Formalization scope

Machines are Fin m with $m\ge1$ and jobs Fin n, both 0-based. The probability space is (Ω, P) with Ω : Type and IsProbabilityMeasure P; sizes are X : Fin m → Fin n → Ω → ℝ, each measurable, nonnegative and integrable (integrability keeps $\mathbb E[X''_{ij}]$ and the expected makespan from collapsing to the Bochner junk value $0$). Job independence is iIndepFun (fun j ω i => X i j ω) P, independence of the per-job vectors, not of all $mn$ variables. Logarithms are natural. The makespan is the supremum over the finite set Fin m. Truncation keeps $X\le1$, the exceptional part keeps $X>1$. $\beta_0$ is a junk value $0$, never used.

The LP's $z_i(k)$ are functions of $y$, fixed by (6). The class loop is a recursion with fuel $m$ that recomputes $\ell=|L|$ each round; an unclassified machine gets the junk class $0$, which Observation 1 rules out for feasible $y$. The Shmoys–Tardos algorithm is represented by its guarantee: an output of the rounding is any assignment satisfying (13)–(14). The goal bounds every such assignment, which is stronger than bounding the one the algorithm returns, and (B) asserts that one exists. Running time, the ellipsoid separation oracle and the binary search over $M$ are not modelled.

None of the definitions mentions an optimal assignment or its value. A goal of the form "there exists $\sigma$ with expected makespan at most $C\cdot\mathrm{OPT}$" is ruled out: it is true with $C=1$, because a minimizer exists among the $m^n$ assignments.

Corrected statements: Lemma 1 adds independence (and drops "discrete"); Lemma 5 and Proposition 1 replace the threshold $1$ by an absolute constant $c_0$, with the $O(1)$ of (4) equal to $17$; Lemma 4's $\Omega(1)$ is an absolute constant $c_1$. Welcome contributions: the effective-size Chernoff bound, the Jensen facts, Observation 1 (pure combinatorics of the class loop), the union-bound and tail-integral steps of Lemmas 6–7, and a cost-preserving Shmoys–Tardos rounding.

Related platform results: UnrelatedSched.TwoApprox.rounding_load_bound and MatousekLP.Scheduling.rounding_makespan_le (Proved) carry out the Lenstra–Shmoys–Tardos rounding for deterministic sizes without costs; WilliamsonShmoys.generalized_assignment_cost_preserving_rounding (Open) is a cost-preserving GAP rounding with load at most $2T$. None of them states Observation 2.

Selected references

• A. Gupta, A. Kumar, V. Nagarajan, X. Shen, Stochastic Load Balancing on Unrelated Machines, SODA 2018; arXiv:1904.07271v1, 2019. https://arxiv.org/abs/1904.07271
• J. Kleinberg, Y. Rabani, É. Tardos, Allocating Bandwidth for Bursty Connections, SIAM J. Comput. 30(1), 2000. https://doi.org/10.1137/S0097539797329142
• D. B. Shmoys, É. Tardos, An Approximation Algorithm for the Generalized Assignment Problem, Math. Program. 62, 1993. https://doi.org/10.1007/BF01585178
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation Algorithms for Scheduling Unrelated Parallel Machines, Math. Program. 46, 1990. https://doi.org/10.1007/BF01585745
• M. Molinaro, Stochastic ℓp Load Balancing and Moment Problems via the L-Function Method, SODA 2019 (reference [21] of arXiv:1904.07271).

Why hidden hedging changes a contract

A manager can influence a project's output through effort, but the owner observes output rather than effort. When the manager can also trade privately in a financial market, a contract based on output and market returns changes both effort incentives and the manager's ability to hedge risk. The owner must decide what the contract pays, how sensitive it is to output, and how much market exposure it gives the manager. Huang, Ju and Xing formulate these choices as a continuous-time control problem in Optimal Contracting with Unobservable Managerial Hedging, the November 2017 working paper underlying the later Management Science article. This mission uses the working paper's equations and numbering.

The question is operational: given an initial promise to the manager, which admissible contract maximizes the owner's discounted cash flow? The paper's Proposition 2.3 answers with a payment boundary, a liquidation boundary, and sensitivities chosen from a two-dimensional control box. Formalizing that proposition requires the value to come from the control problem itself. The free-boundary equation alone does not identify a contract or prove its optimality.

The reduced control problem

The state $Y_t$ is the manager's contract value, with initial promise $\hat y\ge0$. The owner controls the contract sensitivity $Z_t$, gross market exposure $\zeta_t$, and a nondecreasing cumulative payment process $I_t$. The two shocks $B$ and $B^\perp$ are independent standard Brownian motions. The project is liquidated at $\tau=\inf\{t\ge0:Y_t\le0\}$. Time-zero payment is permitted and is charged to the owner.

Effort lies in $[\underline A,\overline A]$ and costs $h(A)=\kappa A^2/2+bA$. The manager's effort response $A^*(Z)$ is the minimizer of $h(A)-ZA$ over that interval. The regular controls lie in $\mathcal Z=[\underline Z,\overline Z]$ and $\Gamma=[\underline\Gamma,\overline\Gamma]$. With $g(Z,\zeta)=r\gamma\psi^2(1-\rho^2)Z^2/2+h(A^*(Z))+(m-r)\zeta$ and $\Sigma(Z,\zeta)=(1-\rho^2)\psi^2Z^2+\sigma^2\zeta^2$, the state dynamics of equation (21) are

$$dY_t=(rY_t+g(Z_t,\zeta_t))\,dt-dI_t+\sigma\zeta_t\,dB_t+\psi\sqrt{1-\rho^2}\,Z_t\,dB_t^\perp.$$

The principal's value $W(y)$ is the least upper bound of expected payoffs over admissible contracts from $y$. Equation (24) includes the discounted output and effort flow, the discounted payment measure, and the liquidation payoff $\Phi$, all scaled by $\delta$. Admissibility includes the paper's transversality condition (57). The value is a control value, not an arbitrary solution of a differential equation.

Formalization targets

The first target is the value characterization of Proposition 6.4. On the continuation interval $(0,\bar y)$, $W$ is twice continuously differentiable and satisfies

$$\delta W(y)=\sup_{(Z,\zeta)\in\mathcal Z\times\Gamma} \left\{\delta(\mu+A^*(Z))+(ry+g(Z,\zeta))W'(y) +\tfrac12\Sigma(Z,\zeta)W''(y)\right\}.$$

Here $\widetilde W(y)=\mu-ry+\sup(A^*-g)$ and $\bar y=\sup\{y\ge0:W(y)<\widetilde W(y)\}$. At and above $\bar y$, $W'=-\delta$; at the boundary, $W(0)=\delta\Phi$ and $W''(\bar y)=0$. Proposition 6.4 also states concavity on $[0,\infty)$ and strict concavity on $[0,\bar y)$.

The mission goal is the stronger Proposition 2.3: for each initial promise, a reflected contract attains $W$. It pays $(\hat y-\bar y)^+$ immediately, makes further payments only when the contract value is at $\bar y$, and liquidates when the value reaches zero. Before liquidation its sensitivities come from maximizers of the displayed Hamiltonian's control-dependent terms. The market sensitivity $U^*(y)$ is recovered from $Z^*(y)$ and $\zeta^*(y)$ by $U^*=\zeta^*-(\rho\psi/\sigma)Z^*$.

What the result establishes

Proposition 2.3 connects a value function to an implementable payment and risk-sharing rule. The upper boundary describes when the owner returns part of the manager's contract value as cash; the lower boundary describes termination. Concavity records the owner's endogenous aversion to leaving value exposed to the manager's future actions. Without the attainment statement, a smooth solution of the HJB could remain only a candidate and would not determine an optimal contract.

The working paper gives an argument for these conclusions; the statements here are open Lean targets. A complete development would check the stochastic control value, the regularity and comparison steps, and the existence of the reflected contract against the same definitions. The finite-horizon Itô integral and independent Brownian coordinates come from the published Peng1990.SMP.Stochastic definition. The effort clamp and the model-specific contract are new definitions for this mission.

Mathematical difficulty

The control has both regular choices $(Z,\zeta)$ and a singular payment process $I$. If one optimizes an unconstrained payment rate as though it were an ordinary bounded control, the Hamiltonian is unbounded whenever $W'<-\delta$. The correct value therefore has a gradient constraint and a free payment boundary. Showing that the resulting boundary rule actually attains the value also requires a reflected stochastic equation up to the liquidation time. The two Brownian shocks must remain separate: merging them changes the information available to the controls.

Formalization scope

Lean represents $Y,Z,\zeta,I$ as time-indexed real processes on an underlying probability space. Brownian coordinate zero is the market shock; coordinate one is the idiosyncratic shock. The filtration is the Brownian filtration supplied by Peng1990.SMP.Stochastic, and Itô integral conditions hold on every finite horizon. This is the reduced principal's problem (24). The manager's separate optimization in Lemma 2.2 and the original output and market processes are outside the model; incentive compatibility enters through $A^*(Z)$.

The formalization uses real-valued payoffs and an explicit least-upper-bound condition for every $y\ge0$, so empty or unbounded feasible payoff sets cannot silently produce Lean's default real supremum. The control box is compact under the standing interval assumptions. Its Hamiltonian and net-contribution suprema are therefore genuine finite suprema. The convention for an empty set in the definition of $\bar y$ is $\bar y=0$, matching the degenerate zero-continuation case. Derivatives at zero use one-sided, within-set derivatives.

The paper's formulas use $\sqrt{1-\rho^2}$ and the proof uses a diffusion coefficient bounded away from zero. The model explicitly assumes $\sigma,\psi,\gamma,\delta>0$ and $-1<\rho<1$ in addition to the paper's stated interval and cost bounds. Admissible contracts have integrable drift and payoff and finite expected discounted payments, so a nonintegrable real integral cannot become zero by Lean's total-function convention. Payments use the Stieltjes measure of $I$, extended by zero before time zero; this charges an immediate lump sum. The transversality limit is taken along deterministic times as in the proof of Lemma 6.3. The value is the supremum of admissible contract payoffs, not a function postulated to solve the HJB. Contributions formalizing the comparison theorem, the singular-control dynamic programming step, or the reflected equation are directly useful to the goal.

Selected references

• Yu Huang, Nengjiu Ju and Hao Xing, Optimal Contracting with Unobservable Managerial Hedging, working paper, November 14, 2017, §§2 and 6.6; later published as Performance Evaluation, Managerial Hedging, and Contract Termination, Management Science, 2023. Published article DOI. The theorem and page numbers in this mission are those of the working paper held in the repository.

Why the credit limit is endogenous

A household can borrow against expected future income only while repayment remains preferable to default. In the baseline model of Choi, Koo, Lim and Yoo, this choice is imposed through a participation condition at every date: the household's remaining utility from its planned consumption must be at least its remaining utility after default. The constraint changes the borrowing limit from the present value of income to a smaller level that depends on the default penalty. Determining that level is useful for understanding which debts are sustainable when income fluctuates and contracts cannot force repayment. The paper gives a closed form for the limit and for optimal financial wealth in its baseline continuous-time model (Proposition 3.2, p. 11).

The result is known mathematically: it is stated and proved by the authors, with the proofs placed in an Online Appendix. This mission targets a machine-checked formalization of the baseline result. It also identifies smaller claims about the constants and the optimal multiplier that are useful independently of the stochastic verification theorem.

Household, income, and participation

The household receives income $I_t$ with initial level $\bar I>0$. Its growth is a geometric Brownian motion driven by two independent standard Brownian motions $B_1$ and $B_2$. The first is the source of risk priced by the traded stock; the second is the remaining income risk, which the paper assumes can be hedged. The state-price density $H_t$ prices future consumption. In the formal model both processes are given explicitly:

$$H_t=\exp\!\left[-\left(r+\frac{\theta^2}{2}\right)t-\theta B_{1,t}\right],\qquad I_t=\bar I\exp\!\left[\left(\mu_I-\frac{\sigma_I^2}{2}\right)t+\sigma_I\left(\rho_I B_{1,t}+\sqrt{1-\rho_I^2}B_{2,t}\right)\right],$$

where $\theta=(\mu-r)/\sigma$. The rate $r_I=r-\mu_I+\theta\sigma_I\rho_I>0$ gives the present-value benchmark $I_t/r_I$ for income. These are the paper's mortality-adjusted $r$, $\mu$, and discount rate $\beta$; the mortality intensity has already been absorbed into them (§2.1, pp. 4–6 of the preprint).

For risk aversion $\gamma>0$, $\gamma\ne1$, utility is $u(c)=c^{1-\gamma}/(1-\gamma)$. A consumption plan is a positive process measurable as information arrives. It is feasible from wealth $x$ when its discounted net cost satisfies $\mathbb E\int_0^\infty H_s(c_s-I_s)\,ds\le x$ and, at every $t\ge0$, it meets the conditional participation constraint

$$\mathbb E\!\left[\int_t^\infty e^{-\beta s}u(c_s)\,ds\mid\mathcal F_t\right]\ge \mathbb E\!\left[\int_t^\infty e^{-\beta s}u(\delta I_s)\,ds\mid\mathcal F_t\right].$$

Here $\mathcal F_t$ is the information generated by the two Brownian motions through time $t$, and $\delta I_s$ is consumption after default. A larger $\delta$ means a less severe default penalty. The paper restricts $0<\delta\le\bar\delta$ and defines $\bar\delta$ from its other parameters in (2.7) (pp. 6–7 of the preprint).

Formalization targets

The endogenous credit-limit coefficient is

$$m^*=\frac1{r_I}-\frac{1-\gamma+\alpha_+\gamma}{\gamma K(\alpha_+-1)}Q,$$

where $K$, $Q$, and the positive quadratic root $\alpha_+$ have exactly the formulas in (2.7) and Proposition 3.1. The first targets establish $\alpha_+>1$, $0<Q<1$, and $0\le m^*<1/r_I$. Proposition 3.4 then gives the dependence on the default fraction:

$$m^*(\delta)=\frac{1-\delta/\bar\delta}{r_I}\quad(0\le\delta\le\bar\delta),\qquad m^*(\bar\delta)=0.$$

The central target is Proposition 3.2. For $x\ge-m^*\bar I$, the candidate consumption plan is feasible and maximizes expected utility among all feasible plans. Its optimal wealth $X_t^*$, defined as the conditional present value of future net consumption, satisfies the closed form (3.10) and the bound

$$X_t^*\ge-m^*I_t\qquad(t\ge0).$$

For $x<-m^*\bar I$, the feasible set is empty: the household defaults immediately. On the way, the mission states the two duality results of §3.1 that the paper's argument rests on. With a Lagrange multiplier $\lambda>0$ for the budget and a non-decreasing shadow-price process $D_t$, $D_0=0$, for the participation constraints, the dual objective (3.4) is minimized by the running maximum

$$D^*_t=\max\Big(0,\max_{0\le s\le t}Q^\gamma y_s-1\Big),\qquad y_s=\lambda e^{\beta s}H_sI_s^\gamma$$

(Proposition 3.1, for multipliers with $D^*_0=0$), and the primal value satisfies the duality relation $V(x,\bar I)=\min_{\lambda>0}\{J(\lambda,\bar I)+\lambda x\}$ (Theorem 3.1). The algebraic milestones also identify the binding level $Q^{-\gamma}$ and the unique admissible initial multiplier solving Proposition 3.3's equation. These targets follow §§3.1–3.2, pp. 8–12 of the preprint.

What the result supplies

The coefficient $m^*$ turns a family of conditional participation conditions into a usable state-dependent debt bound. Its comparison with $1/r_I$ quantifies the difference between a limit based on priced income alone and one that lenders can sustain when the household can default. Proposition 3.4 states precisely how that bound shrinks as default becomes more attractive; at $\delta=\bar\delta$ it reaches zero. The wealth formula also says where the optimal policy sits relative to the boundary at every time, rather than only at the initial date (Propositions 3.2 and 3.4 of the preprint).

Formalizing the result supplies reusable definitions for a continuous-time consumption problem with conditional participation constraints and a stochastic income stream. The constants, multiplier equation, and binding-level facts are separate theorem targets; the final theorem must additionally verify feasibility, optimality, and the conditional wealth identity. The present proposal contains open Lean statements, not verified Lean proofs.

Main difficulty

The natural-limit calculation prices future income, but it does not establish an incentive-compatible borrowing limit: a plan can meet its time-zero budget and still violate participation at a later date. The candidate shadow price depends on the running maximum of an income-adjusted dual process, so the wealth identity involves an infinite-horizon conditional expectation of a path-dependent consumption process. The same candidate must satisfy every conditional participation condition and outperform every feasible plan. Checking only the closed formula for $m^*$ or defining wealth by the right side of (3.10) would leave these claims unproved. The paper places its detailed proofs in an Online Appendix unavailable with the pinned preprint.

Formalization scope

Lean uses time $\mathbb R_{\ge0}$, real-valued wealth and utility, and a natural uncompleted filtration generated by two Brownian coordinates. Infinite time integrals are over the real interval $(t,\infty)$. Each participation condition holds almost surely for each fixed $t$, matching conditional expectations' almost-sure meaning. The running maximum defining the shadow price ranges over $[0,t]$; continuous Brownian paths make that range compact. Its initial value is zero almost surely, as is the Brownian starting value, and it is nonnegative on every path. The optimization statement uses a greatest element of the feasible utility values, avoiding a real supremum with a default value on an empty or unbounded set.

The printed Problem 2.2 mentions a default time $\tau$ but does not define it. The formalization uses the static martingale budget that §3 prices in its Lagrangian; it represents consumption rather than the stock and futures positions. This is the form of the problem for which the goal states optimality. Plans carry the integrability needed for their budget, utility, and conditional expectations. The source leaves $\hat\beta>0$ and a positive leading coefficient of the $\alpha_+$ quadratic unstated; both are explicit because the reservation value and closed-form real powers otherwise become ill posed. Plans are strictly positive, so that utility is never evaluated at zero. The dual value $J(\lambda,\bar I)$ is not defined as a real infimum: the duality relation is stated with least elements of the explicit set of values of the dual objective, and the integrability conditions (3.2) on shadow prices are genuine finiteness requirements, never default values. The optimal-stopping representation of the dual (Lemma 3.1) is not formalized. The initial multiplier is restricted to $0<y_0\le Q^{-\gamma}$, the branch that makes the shadow price start at zero. The endpoint $\delta=0$ appears only in the comparative-statics result for $m^*$, whose formula remains defined there.

The shared Brownian and Euclidean-state definitions are reused from the platform. The new model, candidate process, real-power calculus, conditional integrability, and stochastic verification are available as distinct contributions. The goal cannot be discharged by assuming optimality or by defining $X_t^*$ to equal (3.10): it identifies wealth through a conditional present value and proves the displayed formula separately.

Selected references

• K. J. Choi, H. K. Koo, B. H. Lim and J. Yoo, Endogenous Credit, Business Cycle, and Portfolio Selection, SSRN preprint 2560607, version of October 25, 2023; published in Operations Research (2023). Preprint; journal DOI.

Motivation

Unit commitment (UC) decides, period by period, which thermal generators of a power system are switched on and how much power each produces. It is solved daily by system operators and in the bidding tools of producers, usually as a mixed-integer program, and its size makes the strength of the formulation the main computational lever. A formulation whose continuous relaxation already equals the convex hull of the feasible set closes the integrality gap of each single-unit block. Such single-unit descriptions are then combined into tighter multi-unit models.

For the single-unit problem (1UC) with linear costs, several convex-hull descriptions are known. With ramping limits and a convex, nonlinear generation cost, the question is harder, because the power output is semi-continuous: either $0$ or between the minimum and maximum output. Bacci, Frangioni, Gentile and Tavlaridis-Gyparakis (Operations Research, 2024) give a formulation built on the state-space graph of a dynamic-programming algorithm for 1UC (Frangioni and Gentile, 2006), combined with perspective reformulations (Frangioni and Gentile, 2006) of the dispatch subproblems, and prove that it describes the (closed) convex hull. The paper notes that an earlier formulation claimed to have this property was later shown false by a counterexample.

Setting

A single unit is scheduled over the periods $T=\{1,\dots,n\}$; $T(t',t'')$ denotes the periods from $t'$ to $t''$, empty if $t'>t''$. Its data are:

• minimum up and down times $\tau^+,\tau^-\ge 1$ (numbers of consecutive periods);
• an initial state $\tau^0\neq 0$: on for $\tau^0$ periods if $\tau^0>0$, off for $-\tau^0$ periods if $\tau^0<0$;
• output limits $l\le u$, start-up and shut-down limits $\bar l,\bar u$ with $l\le\bar l\le u$ and $l\le\bar u\le u$;
• ramp limits $0\le\Delta^+,\Delta^-\le u-l$;
• a convex generation cost $f:\mathbb R\to\mathbb R$.

The state-space graph $G=(N,A)$ has a source $s$, a sink $d$, and nodes $ON_t$, $OFF_t$ for $t\in T$. Its arcs are:

• ON arcs $(OFF_h,ON_k)$ with $k\ge h+\tau^+-1$ (the unit starts at $h$ and stays on through $k$), whose pairs form $A_{ON}$;
• OFF arcs $(ON_k,OFF_r)$ with $r\ge k+\tau^-+1$;
• source arcs fixed by $\tau^0$: $(s,ON_k)$ with $k+\tau^0\ge\tau^+$ if $\tau^0>0$, and $(s,OFF_h)$ with $h-\tau^0-1\ge\tau^-$ if $\tau^0<0$;
• the arcs $(ON_t,d)$, $(OFF_t,d)$ and $(s,d)$.

Formulation (26) has a flow variable on every arc subject to the flow system (18), $Ey=\delta$, $y\ge 0$, where $E$ is the node–arc incidence matrix and $\delta$ sends one unit from $s$ to $d$. For every $(h,k)\in A_{ON}$ it adds a private dispatch block in variables $y^{hk}_+$ (the arc flow), $p^{hk}_t$ for $t\in T(h,k)$, and $z^{hk}$:

$$\begin{aligned} &l\,y^{hk}_+\le p^{hk}_h\le\bar l\,y^{hk}_+,\qquad l\,y^{hk}_+\le p^{hk}_t\le u\,y^{hk}_+\ (t\in T(h{+}1,k{-}1)),\qquad l\,y^{hk}_+\le p^{hk}_k\le\bar u\,y^{hk}_+,\\ &p^{hk}_{t+1}\le p^{hk}_t+y^{hk}_+\Delta^+,\qquad p^{hk}_t\le p^{hk}_{t+1}+y^{hk}_+\Delta^-\quad(t\in T(h,k{-}1)),\qquad y^{hk}_+\in[0,1],\\ &z^{hk}\ \ge\ \sum_{t\in T(h,k)} y^{hk}_+\,f\!\left(p^{hk}_t/y^{hk}_+\right). \end{aligned}$$

The last line is the epigraph of the perspective of the dispatch cost. Write $R$ for this constraint set and $S$ for its mixed-integer points, those with every arc variable in $\{0,1\}$.

Two general objects enter the milestones. The 1-sum of $S^1\subseteq\mathbb R^{n_1}\times\mathbb R$ and $S^2\subseteq\mathbb R^{n_2}\times\mathbb R$ is $S^1\oplus S^2=\{(x^1,x^2,y):(x^h,y)\in S^h,\ h=1,2\}$. For a constraint map $f$ with $C=\{z: f(z)\le 0\}$, the support function of a set $S$ is $\sigma_S(c)=\inf\{cz : z\in S\}$, and the Lagrangian dual of $C$ is $D(c)=\sup_{\lambda\ge 0}\inf_z\{cz+\lambda f(z)\}$. $\overline{\operatorname{conv}}$ denotes the closure of the convex hull.

Formalization targets

Goal: Theorem 1 (pp. 18–19)

$$R=\overline{\operatorname{conv}}(S).$$

The continuous relaxation of (26) is the closed convex hull of its own mixed-integer points, for every unit satisfying the standing assumptions and every convex cost.

Milestones

1. Proposition 1 (pp. 16–17): if $C=\{f\le 0\}$ is closed and convex and its mixed-integer restriction $S$ satisfies $\sigma_S(c)=D(c)$ for all $c$, then $C=\overline{\operatorname{conv}}(S)$.
2. Remark after Definition 1 (p. 17): 1-sums preserve convexity and closedness.
3. Lemma 1 (p. 18): if $C^h=\overline{\operatorname{conv}}(S^h)$, the last coordinate of $S^h$ is binary and takes both values, for $h=1,2$, then $C^1\oplus C^2=\overline{\operatorname{conv}}(S^1\oplus S^2)$.
4. Integrality of (18) (p. 16): $\{Ey=\delta,\ y\ge 0\}=\operatorname{conv}\{Ey=\delta,\ y\in\{0,1\}^A\}$.
5. The perspective block ((21), p. 16): each dispatch block is the closed convex hull of its points with $y^{hk}_+\in\{0,1\}$.
6. The composition (proof of Theorem 1, p. 19): (18) with the blocks of any subset $J\subseteq A_{ON}$ is the closed convex hull of its mixed-integer points.

Significance

The result. Theorem 1 gives an exact convex description of 1UC with minimum up and down times, initial conditions, start-up and shut-down limits, ramping limits and a convex cost. Minimizing a linear function over $R$ solves 1UC, and the single-unit blocks of a multi-unit UC model built from (26) carry no integrality gap of their own. Lemma 1 is a composition rule for mixed-integer convex sets glued along a binary variable, which the paper presents as the nonlinear analogue of a classical composition approach for polyhedra; it applies beyond unit commitment.

Formalizing it. The result is proved on paper but not machine-checked, and no part of it is formalized on the platform. A formal proof would certify the exactness claim, which matters in a literature where a published exactness claim was refuted. The paper's proof of Lemma 1 (Appendix A) assumes that a linear objective attains its minimum over a closed convex set, which is false for non-polyhedral sets; the set identity remains true, and a formal proof has to establish it without that step. The paper's remark that Lemma 1 "clearly holds in general" without hypothesis (iv) is also false, so the formal statements keep (iv).

Difficulty

The inclusion $\overline{\operatorname{conv}}(S)\subseteq R$ is routine; the content is $R\subseteq\overline{\operatorname{conv}}(S)$. The obvious attempt treats each dispatch block separately and concatenates the convex combinations. This fails because the blocks share no variables with one another but all depend on the one flow vector $y$: the convex combination that represents one block must be compatible with those representing every other block and the flow system at once. Points of $R$ with some $y^{hk}_+=0$ need care too: there the perspective term is defined by continuity, the epigraph variable is unbounded above, and the closure is genuinely needed in the general lemmas. The duality route of the paper (Proposition 1 with KKT conditions) requires a strong-duality argument for every objective, which is where the printed proof has its gap.

Formalization scope

All values are real. Periods are natural numbers $1,\dots,n$, so the paper's indices are kept; the rule $k\ge h+\tau^+-1$ is written without natural-number subtraction, and the source rules are evaluated in the integers. The ambient space of (26) is finite-dimensional: arc flows indexed by the arcs of $G$; for each $(h,k)\in A_{ON}$ a power vector indexed by $\{0,\dots,n\}$ whose coordinates outside $T(h,k)$ are fixed at $0$; and one epigraph variable. The convex hull is closed, as in the paper's own $\overline{\operatorname{conv}}$.

Committed conventions:

• dispatch blocks are attached to the pairs of $A_{ON}$ only, as printed in (26); the ON-type source and sink arcs carry no power variables;
• one aggregated epigraph variable $z^{hk}$ per ON arc in the goal (26), and one per-period variable $z^{hk}_t$ in the (21) milestone;
• $y\,f(p/y)$ at $y=0$ is read as $0$, which is the perspective's value there because the scaled bounds force $p=0$;
• added hypotheses: $\tau^\pm\ge 1$ (minimum numbers of periods; they make $G$ acyclic) and $f$ convex on $\mathbb R$;
• Lemma 1's hypothesis (ii), a KKT condition on the representing functions of $C^h$, is dropped. It constrains only how $C^h$ is written, so dropping it strengthens the lemma;
• arc costs are not modelled: the theorems are identities between constraint sets.

The mixed-integer set is defined as the relaxation intersected with binary arc variables, and the relaxation is defined directly from the constraints; neither is defined through a convex hull, so the goal cannot hold by unfolding definitions. The correspondence between $s$–$d$ paths and feasible schedules of the paper's 3-bin model (§4, p. 14) is asserted there without proof and is not formalized: Theorem 1 is stated in the extended space of (26).

A complete development needs convex-analysis infrastructure that is reusable beyond this mission:

• closed convex hulls of sets glued along a binary coordinate (Lemma 1);
• the support-function characterization of closed convex sets (Proposition 1);
• flow decomposition and integrality of flow polytopes on acyclic graphs (milestone 4);
• the closed perspective of a convex function (milestone 5).

Contributions to any of these are welcome, as are proofs of individual milestones.

Selected references

• T. Bacci, A. Frangioni, C. Gentile, K. Tavlaridis-Gyparakis, New Mixed-Integer Nonlinear Programming Formulations for the Unit Commitment Problems with Ramping Constraints, Operations Research, 2024. https://doi.org/10.1287/opre.2023.2435 (the statements here follow the submitted manuscript).
• A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106, 2006. https://doi.org/10.1007/s10107-005-0594-3
• A. Frangioni, C. Gentile, Solving nonlinear single-unit commitment problems with ramping constraints, Operations Research 54(4), 2006. https://doi.org/10.1287/opre.1060.0309
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173