Optimization

Why payment timing matters

A retailer can pay a supplier when it places an order or after the supplier delivers it. When production yield is uncertain, the choice changes who bears the cost of missing units. It can also change the supplier's production decision and, through the amount available for sale, the surplus received by consumers. Geng, Guo, Xiao and Yang study these effects in a decentralized supply chain and show that payment postponement can help all three parties, hurt all three, or benefit some while hurting others, depending on production cost and the retailer's pricing rule. Their Proposition 4 gives the precise cost intervals for these outcomes in the SSRN author version, pp. 19–20.

The result matters to contract design in supply chains where realized output can be below planned production. Paying for units ordered and paying for units delivered allocate that shortage differently. A comparison based only on the retailer's expected profit would miss the effects on the upstream supplier and final consumers. Proposition 4 keeps all three outcomes visible while holding the retailer's pricing policy fixed.

The supply-chain game

There is one supplier and one retailer. The supplier chooses a wholesale price $w$ and plans production $Q$ at cost $cQ$. The retailer orders $q$ and sells to a market with linear demand $d(p)=a-bp$, where $a,b>0$ and $p$ is the retail price. The yield factor $Y$ equals $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$, with $0<\alpha,\theta<1$. Thus $\mu=\mathbb E Y=\alpha(1-\theta)+\theta$. The retailer receives $\widehat q=\min\{YQ,q\}$ units; the production cost applies to planned $Q$, including units lost to yield risk §3.1–3.2.

Under pay-by-order, the retailer transfers $wq$ to the supplier and the supplier produces $Q=q$. Under pay-by-delivery, the transfer is $w\widehat q$ and the supplier can choose a larger production quantity. Under ex ante pricing, the retailer fixes $p$ before yield is known. Under responsive pricing, the retailer sets $p$ after observing delivery. Combining payment and pricing gives OA (order, ex ante), OR (order, responsive), DA (delivery, ex ante), and DR (delivery, responsive). The supplier first sets $w$, the retailer next orders and possibly fixes a price, the supplier chooses production, yield is realized, and responsive pricing occurs last Table 1, p. 9.

Both firms maximize expected profit at every stage. A subgame-perfect equilibrium is a complete plan of choices after every history in which each choice is optimal at that history. For scenario $k$, write $\pi_R^k$ and $\pi_S^k$ for equilibrium retailer and supplier profit. The consumer surplus $CS^k$ is expected surplus from sales: for delivered stock $X$ and market price $p$, the model integrates inverse demand less $p$ from zero to $\min\{d(p),X\}$. This is the paper's priority allocation convention for consumers with the highest willingness to pay p. 10.

Formalization targets

The main target is Proposition 4, which compares OA with DA and OR with DR. Let $\Delta(\pi_R,\pi_S,CS)$ mean the delivery-payment outcome minus its order-payment counterpart. A plus sign below means a strict increase, a minus sign a strict decrease, and zero equality. The admissible cost range is $0<c<a\mu/b$.

For ex ante pricing, with no restriction $\alpha\ge9/16$, the paper gives a threshold $0<\overline C<c^{DA}$ and the following pattern:

$$\begin{array}{c|c} \text{cost interval}&\operatorname{sign}\Delta(\pi_R,\pi_S,CS)\\ (\max\{0,c^{OA}_2\},\max\{\overline C,c^{OA}_2\}) &(+,+,+)\\ (\max\{\overline C,c^{OA}_2\},c^{DA}) &(+,+,-)\\ (0,\max\{0,c^{OA}_1\})\text{ or }(c^{DA},a\mu/b)&(0,0,0). \end{array}$$

For responsive pricing, assuming $\alpha\ge9/16$, the pattern is $(+,+,+)$ on $(0,\widetilde C)$, $(-,-,-)$ on $(\widetilde C,c^{DR}_1)$, $(+,-,+)$ on $(c^{DR}_1,c^{DR}_2)$, and $(0,0,0)$ on $(c^{DR}_2,a\mu/b)$. The thresholds are those specified in the paper: $\widetilde C$ is equation (6), $\overline C$ is equation (8), and the scenario cost thresholds come from Appendix B. The first ex ante interval can be empty for some parameters; its printed endpoints are retained. The milestones establish the supplier's production and responsive pricing rules, the four scenario outcomes, and the threshold ordering used in the comparison Appendices B–C.

What the result provides

The theorem separates the effect of changing the payment contract from the effect of changing the pricing rule. For advance pricing it identifies an interval where payment postponement helps both firms and consumers, then an interval where consumers lose despite both firms gaining. For responsive pricing the direction of every effect can reverse as cost passes successive thresholds. At high cost the change in payment timing leaves all three equilibrium outcomes unchanged Proposition 4, pp. 19–20.

The paper derives the equilibrium formulas in Appendix B and proves the comparisons in Appendix C. The result is therefore a known mathematical claim, while this mission asks for a machine-checked development from the sequential game through the cost-dependent equilibrium outcomes and final comparisons. The definitions of a two-point yield game and its complete contingent strategies can support other formal studies of payment or pricing postponement. There is no claim that Proposition 4 already has a machine-checked proof.

Where the formal work is difficult

The supplier's production payoff has kinks at $Q=q$ and $Q=q/\alpha$. The retailer's best order changes when those production choices change, and responsive pricing adds another kink when delivered stock crosses $a/2$. As wholesale price varies, the supplier must compare outcomes on both sides of these changes. Consequently a single first-order condition for a smooth objective does not characterize the equilibrium. The cost thresholds also depend on square roots and comparisons among several formula pieces, including the larger root chosen for $c^{OA}_2$ Appendix B, pp. 33–37.

Formalization scope

Lean represents expectation by the two weighted yield outcomes. Production cost $c$ is a separate argument, so thresholds depend only on $(a,b,\alpha,\theta)$. Parameters satisfy $a,b>0$, $0<\alpha,\theta<1$, and $0<c<a\mu/b$. Wholesale and retail prices obey the strict admissibility bounds of equation (3). Orders are nonnegative; pay-by-delivery production is nonnegative; pay-by-order production equals the order. Consumer surplus is a real interval integral. Every comparison quantifies over actual subgame-perfect equilibria, and the goal separately asserts that the compared equilibria exist at every admissible cost. Equilibrium profits are computed from strategies and transfers, rather than defined to equal the Appendix B formulas.

The paper's statements require care at ties. The model selects $Q=q$ when that is a profit-maximizing pay-by-delivery production choice, including the indifferent DR regime. The printed middle DR consumer-surplus expression combines outcomes from different production choices; the equilibrium-consistent expression is used here, and Proposition 4(R)'s comparison remains valid under either expression. Equation (2) swaps the scenario labels of committed and responsive prices, so consumer surplus uses the actual ex ante price in OA and DA and the price after delivery in OR and DR. The printed $[x]^+$ in Appendix B.1 is read as $\max\{0,x\}$, as in Lemma 1. Outcome claims use open cost intervals because uniqueness at exact thresholds fails; equilibrium existence remains part of the targets there. The threshold $c^{OA}_2$ is the larger root of the relevant quadratic factor, and $\overline C$ and $\widetilde C$ use the paper's explicit formulas. These conventions are recorded in the local moderation notes.

The development calls for real inequality reasoning, optimization of piecewise objectives, and careful handling of interval integrals. Contributions that prove the production and price best responses, establish the four equilibrium lemmas, or verify the threshold order each advance the final comparison.

Selected references

• X. Geng, X. Guo, G. Xiao and N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. SSRN author version 3546872; DOI: 10.1287/msom.2022.0198.

Motivation

A retailer that buys from a supplier with unreliable production has two contractual levers against supply risk, and both postpone a decision until after the yield is known. Payment postponement means paying only for the units actually delivered (pay-by-delivery) instead of the units ordered (pay-by-order). This moves the yield risk upstream. Pricing postponement means setting the retail price after the delivery is observed (responsive pricing) instead of committing to it in advance (ex ante pricing). This moves the risk downstream to consumers. Both practices are common in procurement, and the natural intuition is that two ways of shedding the same risk should be substitutes: once one lever is in use, the other should be worth less.

Geng, Guo, Xiao and Yang (MSOM 25(3), 2023; author version SSRN 3546872) compute the subgame-perfect equilibria of all four combinations of the two levers in a stylized supplier–retailer game. Their Proposition 3 shows that the intuition fails at intermediate production cost. When full yield is likely and yield loss is mild, the two postponements are complements there: postponing payment is worth more when pricing is also postponed. This mission formalizes that result together with the four equilibrium characterizations it rests on.

Setting

A supplier sells one product to a retailer, who sells it in a market with linear demand $d(p)=a-bp$, $a,b>0$. The supplier plans production $Q$ at unit cost $c$ and realizes the fraction $Y$ of it, where

$$Y=1 \text{ with probability } \theta,\qquad Y=\alpha \text{ with probability } 1-\theta,\qquad 0<\alpha,\theta<1,$$

and $\mu=\alpha(1-\theta)+\theta$ is the mean yield. The retailer orders $q$ and receives $\hat q=\min\{YQ,q\}$.

The four scenarios are OA, OR, DA and DR. The first letter is the payment rule: by order (O, the transfer is $wq$) or by delivery (D, the transfer is $w\hat q$). The second letter is the pricing rule: ex ante (A, the price is fixed before the yield) or responsive (R, the price is set after $\hat q$ is observed). Each scenario is a sequential game. The supplier posts a wholesale price $w$. The retailer orders $q$, and also commits to a price $p$ in the ex ante scenarios. The supplier then chooses $Q$; under pay-by-order it produces exactly $q$. The yield realizes, and under responsive pricing the retailer then sets $p$. The retailer earns $p\min\{d(p),\hat q\}$ minus the transfer, and the supplier earns the transfer minus $cQ$. Both are risk neutral. Admissible actions follow the paper's standing ranges: $0<c<a\mu/b$, $0<p<a/b$, and $w$ between $c$ (or $c/\mu$ under pay-by-delivery) and $a/b$.

Write $\pi^k_R$ for the retailer's expected profit in a subgame-perfect equilibrium of scenario $k$. The paper's Definition 1 measures the interaction of the two postponements by

$$V=\big(\pi^{DR}_R-\pi^{OR}_R\big)-\big(\pi^{DA}_R-\pi^{OA}_R\big):$$

the value of payment postponement under responsive pricing, minus its value under ex ante pricing. The postponements are substitutes if $V<0$ and complements if $V>0$.

The parameter region of the result is $\alpha\ge 9/16$ together with $\mathcal H_3=\{\theta_2(\alpha)<\theta<1\}$, where $\theta_2(\alpha)$ is the largest real root of the cubic $-\alpha^3+\alpha^2(5+\alpha)x+(16-19\alpha-6\alpha^2)x^2-25(1-\alpha)x^3$. The cost thresholds $c^{DR}_1<c^{DR}_2$ (scenario DR) and $c^{DA}$ (scenario DA) are explicit algebraic functions of $(a,b,\alpha,\theta)$ given in the paper's Appendix B.

Formalization targets

Goal: Proposition 3

For $\alpha\ge9/16$ and $(\alpha,\theta)\in\mathcal H_3$, every scenario has an equilibrium at every cost $0<c<a\mu/b$, and there is a cost $0<\hat C<a\mu/b$ such that, at every choice of the four equilibria,

$$V<0 \text{ on } (0,c^{DR}_1)\cup(\hat C,c^{DA}),\qquad V>0 \text{ on } (c^{DR}_1,\hat C),\qquad V=0 \text{ on } (c^{DA},a\mu/b).$$

$\hat C$ is existential, as in the paper, and depends only on the parameters.

Milestones

• the supplier's production response (4) under pay-by-delivery and the ex post price (5);
• Lemmas 1–4: existence of the equilibrium of each scenario, and its outcome $(\pi_R,\pi_S,CS)$ in closed form on each cost interval;
• Lemma 1(i): on $\mathcal H_3$ the threshold $c^{OA}_2$ is nonpositive, so scenario OA has one regime;
• the threshold claims of Appendix C: $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$ for $\alpha\ge9/16$.

Significance

The result separates the first-order question (which lever the retailer prefers, the subject of the paper's Proposition 2) from the second-order one (whether one lever raises the value of the other). It shows that two risk-shifting instruments can reinforce each other. On $(c^{DR}_1,\hat C)$, adopting one postponement raises the value of the other. So whenever the retailer gains from adopting either lever alone, it gains even more from adopting both. Below $c^{DR}_1$ and above $\hat C$ the reverse holds. Above $c^{DA}$, payment postponement is irrelevant, because the supplier never inflates production there.

The paper proves Lemmas 1–4 by backward induction in Appendix B and the proposition by comparing closed forms in Appendix C. None of it is machine-checked. A formal proof requires the four backward inductions with every kink and tie handled, and the polynomial inequalities between the thresholds over the parameter region. The formalization also corrects the record: the paper's explicit formula (7) for $\hat C$ does not locate the sign change of $V$ (at $(\alpha,\theta)=(0.6,0.75)$ it exceeds $c^{DA}$), while the existential statement of Proposition 3 holds at every sampled point.

Difficulty

Once Lemmas 1–4 are available, $V$ is a difference of explicit piecewise functions of $c$. The difficulty lies in those lemmas and in the thresholds. Each lemma is a three-stage optimization. The supplier's profit is piecewise linear in $Q$, with kinks at $q$ and $q/\alpha$. The retailer's profit is piecewise in $(q,p)$, with kinks where it becomes worth inflating the order. The supplier's value function in $w$ is piecewise quadratic, and its maximum can sit at a kink. In scenario DR it sits exactly at the price where the supplier is indifferent to inflating production. A naive reading of the paper's tie rule removes the equilibrium there altogether. On the middle DR interval the sign of $V$ changes inside the interval, at a root of a polynomial with nested square roots. On the other pieces, the signs of $V$ and the ordering $c^{DR}_1<c^{DR}_2<c^{DA}$ are polynomial inequalities in $(\alpha,\theta)$, with $\theta_2(\alpha)$ defined implicitly as a cubic root.

Formalization scope

• Parameters and cost. The parameters $(a,b,\alpha,\theta)$ form a structure. The cost $c$ is a separate argument, and every threshold depends on the parameters only.
• Expectation. The expectation over the yield is the explicit two-point sum $\theta f(1)+(1-\theta)f(\alpha)$.
• Equilibrium. Strategies are functions of all earlier moves, and optimality is required at every node over the full admissible action sets.
• Production ties. Under pay-by-delivery the supplier's production is a best response. When producing exactly $q$ is optimal, it produces $q$. The paper's display (4) assigns that tie to inflation, but under that rule scenario DR has no equilibrium for intermediate cost. The convention reproduces the paper's DR profits.
• Consumer surplus. It is the integral $\int_0^{\min\{d(p),\hat q\}}(p(t)-p)\,dt$. It uses the ex post price in the responsive scenarios and the committed price in the ex ante ones; the labels of the paper's display (2) are swapped.
• Closed forms. Two printed consumer-surplus values are corrected to the equilibrium values: the middle piece of OA ($8b\alpha^2$ for $8b\alpha^3$) and the middle piece of DR (one factor $\alpha^2(1-\theta)+\theta$ fewer).
• Cost intervals. Every statement is on open cost intervals, because at a threshold the outcome is not unique.
• Thresholds. $c^{OA}_2$, "the second root" of a quartic, is the larger root of the quadratic factor that defines it. $\theta_2$ is the supremum of the cubic's real roots, a finite nonempty set.

The equilibrium profits are outcomes of the equilibrium predicate. They are never defined by their closed forms, and the goal carries the existence of an equilibrium in each scenario. Without that, the comparison would be vacuous whenever the predicate is unsatisfiable.

Every object is elementary: real arithmetic, square roots, min/max, one interval integral and one sSup. The equilibrium predicate and the four lemmas are shared with the three companion missions of this paper (Propositions 2, 4 and 5). Proofs of the lemmas, of the threshold inequalities and of the goal are all welcome.

Selected references

• X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. https://doi.org/10.1287/msom.2022.0198 ; author version SSRN 3546872, https://ssrn.com/abstract=3546872

Motivation

When a supplier's production is subject to random yield, only part of a planned production run turns into usable output. A retailer sourcing from such a supplier bears the resulting shortage risk unless the contract or the selling strategy moves it elsewhere. Random yield is a classical topic in production planning (Yano and Lee, 1995), and postponing a decision until uncertainty resolves is a classical risk-mitigation tool (Van Mieghem and Dada, 1999).

Geng, Guo, Xiao and Yang study two postponements available to a retailer facing an unreliable supplier. Payment postponement replaces payment for the ordered quantity by payment for the delivered quantity, which shifts the yield risk to the supplier. Pricing postponement (responsive pricing) sets the retail price after the delivery is known, which shifts the risk to consumers. Their Proposition 2 answers which of the four combinations the retailer prefers, as a function of the production cost, when the yield loss is not too severe. This mission formalizes that proposition and the equilibrium results it rests on.

Setting

A supplier sells to a retailer, who sells to a market with linear demand $d(p)=a-bp$, $a,b>0$. The supplier's yield factor $Y$ takes the value $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$, with $\alpha,\theta\in(0,1)$, and has mean $\mu=\alpha(1-\theta)+\theta$. The supplier plans production $Q$, pays $c$ per planned unit, and delivers $\hat q=\min\{YQ,q\}$ against an order $q$. Throughout, $0<c<a\mu/b$.

There are four scenarios, written $k\in\{OA,OR,DA,DR\}$:

• O (pay-by-order): the retailer pays $wq$, and the supplier produces exactly $Q=q$;
• D (pay-by-delivery): the retailer pays $w\hat q$, and the supplier chooses $Q$ and may inflate production above $q$;
• A (ex ante pricing): the retailer commits to the retail price $p$ when it orders;
• R (responsive pricing): the retailer sets $p$ after seeing $\hat q$, maximizing $p\min\{d(p),\hat q\}$.

Each scenario is a Stackelberg game. The supplier sets the wholesale price $w$, the retailer orders (and, ex ante, prices), the supplier produces, the yield realizes, and under responsive pricing the retailer prices. Both firms are risk neutral. The solution concept is subgame-perfect equilibrium, and $\pi^k_R$ denotes the retailer's expected equilibrium profit in scenario $k$. Admissible prices are those of the paper's standing assumption (3): $0<p<a/b$, and $c<w<a/b$ under pay-by-order or $c/\mu<w<a/b$ under pay-by-delivery.

The cost thresholds of the comparison are

$$\tilde C=\frac{a\alpha\big(1-\sqrt{\alpha^2(1-\theta)+\theta}\big)}{b(1+\alpha)},\qquad c^{DR}_2=\frac{a\alpha\mu(1-\theta)}{b(\mu+\theta)},$$ $$c^{DR}_1=\frac{a\alpha(1-\theta)\big(\mu^2+\theta-2\theta\sqrt{\alpha\mu(1-\alpha)(1-\theta)}\big)}{b\big(\alpha^2(1-\theta)^3+4\alpha\theta(1-\theta)+\theta(1+\theta)^2\big)}.$$

Formalization targets

Goal: Proposition 2 (p. 16)

For $9/16\le\alpha<1$ and every $0<c<a\mu/b$, equilibria of OR, DA and DR exist, and every choice of equilibria satisfies

$$\begin{aligned} &\pi^{OR}_R<\pi^{DR}_R=\pi^{DA}_R && 0<c<\tilde C,\\ &\pi^{DA}_R=\pi^{DR}_R<\pi^{OR}_R && \tilde C<c<c^{DR}_1,\\ &\pi^{DA}_R<\pi^{OR}_R<\pi^{DR}_R && c^{DR}_1<c<c^{DR}_2,\\ &\pi^{DA}_R<\pi^{DR}_R=\pi^{OR}_R && c^{DR}_2<c<a\mu/b. \end{aligned}$$

Milestones

1. (4): the supplier's production under pay-by-delivery is $q$ below the wholesale price $c/(\alpha(1-\theta))$ and $q/\alpha$ above it.
2. (5): the responsive price is $(a-\hat q)/b$ for $\hat q<a/2$ and $a/(2b)$ otherwise.
3. Lemmas 2, 3, 4: existence of equilibria of OR, DA and DR, and their outcomes $(\pi_R,\pi_S,CS)$ in closed form on each open cost interval (Lemma 4 for $\alpha\ge 9/16$).
4. Threshold order (proof of Propositions 1–2): for $\alpha\ge 9/16$, $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$.
5. Position of $\tilde C$ (proof of Proposition 4): for $\alpha\ge 9/16$, $0<\tilde C<c^{DR}_1$.

Significance

The proposition describes a preference cycle. Payment postponement (DA) is best when production is cheap, because the supplier then absorbs yield risk by inflating production. Pricing postponement (OR) is best at intermediate cost. Using both (DR) is strictly best on $(c^{DR}_1,c^{DR}_2)$, where the two postponements are worth more together than either alone. Above $c^{DR}_2$ the supplier stops inflating, DR and OR coincide, and pricing postponement suffices. These are the paper's managerial conclusions on contract and pricing choice under supply risk, and the other three missions of the series (strategic complementarity, and the effect of each postponement on the whole chain) rest on the same equilibria.

The paper derives the four equilibria in its Appendix B and proves the propositions in Appendix C as direct comparisons of closed forms. None of this has been machine-checked. The mission produces a formal model of the four games and a verified link from the game to the closed forms. Lemmas 2–4 are reusable by every statement about this model.

Difficulty

Once the closed forms are known, the comparison is polynomial algebra in $(\alpha,\theta,c)$ with square roots. The work lies upstream. Each equilibrium requires a backward induction over piecewise-linear objectives in $Q$ and $q$ and piecewise-quadratic objectives in $p$ and $w$. Optima occur at kinks such as the inflation threshold $w_0=c/(\alpha(1-\theta))$, and the supplier's value function is discontinuous there, so the maximum can sit at a boundary rather than at the center of a piece. In scenario DR the equilibrium wholesale price on $(c^{DR}_1,c^{DR}_2)$ sits exactly at $w_0$, where the supplier is indifferent among all productions in $[q,q/\alpha]$, so existence depends on how that tie is resolved. Uniqueness of outcomes, which the comparison needs, holds only on open cost intervals, because at each threshold two wholesale prices tie with different outcomes. The threshold inequalities for $\alpha\ge 9/16$ are not visible from the formulas and need careful estimates of the radicals.

Formalization scope

Parameters are a structure $(a,b,\alpha,\theta)$ with validity predicate $a,b>0$, $\alpha,\theta\in(0,1)$; the cost $c$ is a separate real argument. The expectation over $Y$ is the two-term sum $\theta f(1)+(1-\theta)f(\alpha)$, with no measure theory. A strategy profile consists of a wholesale price and rules for production $Q(w,q)$, the order $q(w)$, the ex ante price $p(w)$ and the ex post price $p^{\mathrm r}(w,q,\hat q)$. Equilibrium requires optimality at every admissible history over the admissible sets of (3). Consumer surplus is the integral $\int_0^{\min\{d(p),X\}}(p(t)-p)\,dt$, evaluated at the ex post price under responsive pricing and at the committed price under ex ante pricing.

Conventions and disclosed departures from the page:

• Tie rule. Under pay-by-delivery, when producing exactly $q$ is optimal, the supplier produces $q$. Display (4) assigns the tie at $w_0$ to inflation, under which DR has no equilibrium on $(c^{DR}_1,c^{DR}_2)$. Lemma 4's printed profits there are those of the convention.
• $CS^{DR}$ on the middle piece is stated with denominator $8b\alpha^2(1-\theta)^2(\alpha^2(1-\theta)+\theta)$; the page prints the last factor squared, which is the surplus of no single equilibrium. Proposition 2 does not involve $CS$.
• Open intervals. Lemmas are stated on open cost intervals; at the thresholds outcomes are not unique.
• $\tilde C$ is instantiated by (6), as Appendix C does; the page introduces it through Proposition 1's existential.
• Display (2) prints the scenario labels of $CS$ swapped; the Appendix B reading is used.

$\pi^k_R$ is the retailer's profit along an equilibrium of the game, never its closed form; a formalization that defines the profits by the Appendix B formulas, or an equilibrium predicate that no profile satisfies, would make the goal trivial. The goal therefore also asserts existence of equilibria of the three scenarios.

Contributions welcome: proofs of the milestones; general lemmas on maximizing piecewise-linear and piecewise-quadratic functions with kinks; the threshold inequalities. Proposition 1 (OA versus the others) is not part of this mission.

Selected references

• X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, SSRN 3546872 (author version), 2022; published in Manufacturing & Service Operations Management 25(3), 2023. https://ssrn.com/abstract=3546872, https://doi.org/10.1287/msom.2022.0198
• C. A. Yano, H. L. Lee, Lot Sizing with Random Yields: A Review, Operations Research 43(2), 1995. https://doi.org/10.1287/opre.43.2.311
• J. A. Van Mieghem, M. Dada, Price Versus Production Postponement: Capacity and Competition, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1631

Motivation

Payment channels let two parties make repeated transfers while using an on-chain transaction only when a channel needs resetting. They require funds to be committed in advance. The economic choice is therefore between the transaction fees saved by using a channel and the opportunity cost of funds tied up in it. Guasoni, Huberman, and Shikhelman give a stochastic cost model in which this tradeoff can be compared for one-way and two-way payment streams (Guasoni et al., 2023, §§1 and 3). Their small-discount-rate result makes the difference between the two arrangements quantitative: the optimal one-way cost grows like $r^{-1/2}$, while the optimal symmetric two-way cost grows like $r^{-1/3}$.

The paper was published online in Management Science on November 6, 2023. This mission concerns Theorem 3(i)–(ii) in that published version, especially the cost expansion (8). The paper proves these asymptotic claims; the task here is to state them precisely in Lean and develop machine-checked proofs of the stated cost laws.

Setting

Two nodes exchange unit payments. Payments from node 1 to node 2 arrive at rate $\lambda_1$, and payments in the reverse direction arrive at rate $\lambda_2$. Each payment stream is a Poisson process, and the streams are independent. The continuously compounded discount rate $r>0$ measures the opportunity cost of committed capital. A channel reset costs $B>0$, while an on-chain payment costs $C$. Node 1 commits $l_1$ and node 2 commits $l_2$. The channel balance moves by one unit at each payment; at a boundary, a reset replenishes it (Guasoni et al., 2023, §§1.1, 3.1 and 5).

The paper's closed-form bidirectional cost $c^{l_1,l_2}(\lambda_1,\lambda_2)$ is given in equations (3)–(4). It uses two characteristic roots $\alpha_-$ and $\alpha_+$, determined by the payment rates and $r$. This mission uses the formula at equal rates $\lambda_1=\lambda_2=\lambda>0$. A separate unidirectional cost $c^{0,m}(0,\lambda)$ from equation (1) describes a stream in only one direction. Its optimizing size is denoted $m$ below. The exact channel model has integer balance states; the paper optimizes the closed forms over positive real channel sizes in its asymptotic analysis.

Write $c^{\mathrm{opt}}(0,\lambda)$ for the infimum of the unidirectional cost over $m>0$, and $c^{\mathrm{opt}}(\lambda,\lambda)$ for the infimum of the symmetric bidirectional cost over $l_1,l_2>0$. These are functions of $r$ and $B$ as well as of $\lambda$; the compact paper notation suppresses those arguments. The term $O(r^a)$ has its usual uniform meaning as $r\downarrow0$ with $B$ and $\lambda$ fixed: its absolute value is at most a constant times $r^a$ for all sufficiently small positive $r$.

Formalization targets

Unidirectional benchmark

Theorem 3(i), equation (7), states

$$c^{\mathrm{opt}}(0,\lambda) =2\left(\frac{B\lambda}{r}\right)^{1/2}-\frac B2+O(r^{1/2}).$$

The same part states that an optimal size is $(B\lambda/r)^{1/2}+O(r^{1/2})$. The mission records that size claim using the explicit optimizer displayed after equation (2) (Guasoni et al., 2023, pp. 6–7).

Symmetric bidirectional goal

The mission's goal is the cost clause of Theorem 3(ii), equation (8):

$$c^{\mathrm{opt}}(\lambda,\lambda) =3\left(\frac{2B\lambda}{r}\right)^{1/3}-\frac B6+O(r^{1/3}).$$

This includes the constant correction $-B/6$ and a two-sided error estimate of order $r^{1/3}$. The theorem also states that optimal commitments are equal and each has size $(2B\lambda/r)^{1/3}+O(r^{1/3})$. That separate size clause is outside this proposal; the goal does not assert the existence or location of a minimizing pair (Guasoni et al., 2023, p. 7).

Significance

The different exponents distinguish the two designs even when both can make frequent off-chain payments. At small $r$, the model's optimal symmetric bidirectional cost grows more slowly than its optimal unidirectional cost. The formulas also retain the next constant term, allowing a comparison beyond the leading growth rates. The paper relates this difference to the amount of capital that must be committed by the participants (Guasoni et al., 2023, p. 7).

A formal proof would connect the exact channel-cost formulas, a two-variable infimum, the diagonal specialization, bounds on the hyperbolic cosecant, and real asymptotics in one reusable development. The supporting statements are useful separately: the root expansion concerns a quadratic characteristic equation, and the diagonal reduction concerns a symmetric optimization problem. The paper supplies proofs of the mathematical results; the remaining work is their faithful machine-checked formalization.

Difficulty

The cost depends on $r$ and on sizes that grow without bound as $r$ approaches zero. An expansion valid for each fixed size does not by itself justify substituting a size that varies with $r$. The target asks for a uniform remainder at the infimum, including its constant term. The cost must be controlled from both sides over every admissible positive size; evaluating one promising size supplies only one side of that comparison. The paper's proof of Theorem 3 uses formal small-$r$ expansions of the cost and first-order conditions, and the stated error rate calls for care when these are applied to moving optimizers (Guasoni et al., 2023, pp. 11–12).

Formalization scope

The Lean definitions reproduce equations (1), (3), and (4). The one-way and two-way costs are separate functions, matching the paper's separate treatment of the unidirectional boundary case. Real powers are used for the real-size optimization; the balance lattice in the exact stochastic model uses integer sizes. Both optimal costs are infima over strictly positive real sizes. The symmetric infimum is not defined by choosing a particular size or by assuming that the minimum is attained. All rates in the asymptotic theorems satisfy $\lambda>0$, the reset cost satisfies $B>0$, and the filter sends $r$ to zero through positive values. Consequently a Big-O constant may depend on $B$ and $\lambda$ but cannot depend on $r$.

The on-chain costs $C\lambda/r$ for one stream and $2C\lambda/r$ for two equal streams supply the paper's economic comparison, although $C$ does not occur in this mission's cost goal. The diagonal milestone omits that on-chain term because it is constant in the channel sizes; it states a midpoint cost inequality so no minimizer is assumed. The proof's root expansion is recorded for both $\alpha_+$ and $\alpha_-$. The paper's assertion that the symmetric minimizing sizes equal $(2B\lambda/r)^{1/3}+O(r^{1/3})$ is explicitly omitted. The development does not fix a numerical value of $r$, permit an $r$-dependent Big-O constant, drop the $-B/6$ term, or replace the infimum by cost at a chosen size.

The mission needs real-power identities, properties of $\sinh$ and $\cosh$, nonempty bounded-below cost sets, infimum estimates, and Mathlib's Asymptotics.IsBigO on the positive-side neighborhood of zero. Results about real asymptotics and symmetric minimization can be reused beyond this channel model. Contributions proving the cost milestones, the root expansion, the diagonal inequality, and the goal are all within scope.

Selected references

• Guasoni, P., Huberman, G., and Shikhelman, Y., Lightning Network Economics: Channels, Management Science, Articles in Advance, November 6, 2023, pp. 1–14. DOI: 10.1287/mnsc.2022.01664.

Linear programs as zero-sum games

Linear programming and two-player zero-sum matrix games are two faces of one theory. Von Neumann's minimax theorem is a statement of LP duality, and conversely, since Dantzig's 1951 note, every linear program can be rewritten as a zero-sum game. The equivalence matters in practice whenever an algorithm is much better at one of the two problems. Game solvers based on multiplicative weights and sampling, such as the randomized algorithm of Grigoriadis and Khachiyan (GK95), approximate the value of an $n\times m$ game in time sublinear in the size of the matrix. Carmon, Duchi, Sidford and Tian (arXiv:1903.02675) and van Apeldoorn and Gilyén (arXiv:1904.03180) use such game solvers, classical or quantum, as linear-programming solvers. For that to work, the reduction from a linear program to a game must be explicit, with the exact error budget that the game solver has to meet.

This mission formalizes that reduction as it is stated in §4 of van Apeldoorn and Gilyén (2019), Lemma 12 (p. 14). The paper uses it to turn its quantum zero-sum game solvers into quantum LP solvers with cubic dependence on $R(r+1)/\varepsilon$ (Theorem 13, p. 15).

Setting

The linear program. Let $A \in \mathbb R^{n\times m}$, $b \in \mathbb R^m$ and $c \in \mathbb R^n$. The primal LP (4) and its dual (5) are

$$\max_{y \in \mathbb R^m}\ \{\, b^{\mathsf T}y : Ay \le c,\ y \ge 0 \,\}, \qquad \min_{x \in \mathbb R^n}\ \{\, c^{\mathsf T}x : A^{\mathsf T}x \ge b,\ x \ge 0 \,\}.$$

The paper's standing assumptions (p. 12) are:

• every entry of $A$, $b$ and $c$ lies in $[-1,1]$;
• a constant $R > 0$ is known such that adding $\sum_j y_j \le R$ to the primal does not change its optimal value, and $|c_i| \le R$ for every $i$;
• a constant $r$ is known such that adding $\sum_i x_i \le r$ to the dual does not change its optimal value. The two optimal values coincide, and $\mathrm{OPT}$ denotes the common value.

The game. In a zero-sum game with payoff matrix $M$, the column player picks a mixed strategy $y$ in the standard simplex $\Delta = \{y \ge 0 : \sum_k y_k = 1\}$, and the row player picks the row with the largest payoff. The value of the game (LP (1), p. 2) is

$$\lambda^*(M) = \min_{y \in \Delta}\ \max_i\ (My)_i .$$

The reduction. Fix a threshold $\alpha$. With $e$ the all-ones vector of length $m$, the game matrix (6) acts on the variables $(y, z, h)$ (the original variables, one slack variable and one homogenizing variable):

$$A''' = \begin{pmatrix} e^{\mathsf T} & 1 & -1 \\ -e^{\mathsf T} & -1 & 1 \\ -b^{\mathsf T} & 0 & \alpha/R \\ A & 0 & -c/R \end{pmatrix}.$$

Write $\lambda^* = \lambda^*(A''')$ for its value, and set the error level $\varepsilon''' = \varepsilon/(6R(r+1))$.

Formalization targets

Goal: Lemma 12

For every $\varepsilon > 0$, every threshold $\alpha$ with $|\alpha| \le R$, and every estimate $\tilde\lambda$ with $|\tilde\lambda - \lambda^*| \le \varepsilon'''$,

$$\tilde\lambda > \varepsilon''' \implies \mathrm{OPT} < \alpha, \qquad \tilde\lambda \le \varepsilon''' \implies \mathrm{OPT} \ge \alpha - \varepsilon .$$

This is the paper's "finding the optimal value $\lambda^*$ of the game (6) up to additive error $\varepsilon'''$ suffices to correctly conclude either $\mathrm{OPT} < \alpha$ or $\mathrm{OPT} \ge \alpha - \varepsilon$", with the decision rule its proof uses.

The two cases (milestones)

The goal splits into the two exact implications of the proof:

$$\lambda^* > 0 \implies \mathrm{OPT} < \alpha, \qquad\qquad \lambda^* \le 2\varepsilon''' \implies \mathrm{OPT} \ge \alpha - \varepsilon .$$

The milestones follow the printed proof, all on p. 14:

• the explicit strategy $\hat y$ built from a primal point with objective at least $\alpha$;
• the first case;
• the existence of a strategy that attains the value;
• the bound $|h - 1/2| \le \varepsilon'''$;
• the approximate feasibility and optimality bounds (7)–(8);
• weak duality with relaxed constraints;
• the second case.

Significance

The result. Lemma 12 is the bridge that makes any approximate zero-sum game solver an approximate LP solver. It turns the question "is $\mathrm{OPT} \ge \alpha$?" into a single approximate value computation, and binary search over $\alpha \in [-R, R]$ (p. 12) then locates $\mathrm{OPT}$ to additive error $\varepsilon$. The constant $6R(r+1)$ is the price of the reduction. It fixes how accurately the game must be solved, and therefore the $(R(r+1)/\varepsilon)^3$ and $(R(r+1)/\varepsilon)^{3.5}$ factors of Theorem 13. The same reduction appears, in other forms, in classical sublinear LP solvers.

Formalizing it. The lemma is proved in the paper; this mission produces a machine-checked version with every constant explicit. That is not a formality here. As printed, the second row of (6) is $(-e^{\mathsf T}, 1, 1)$, and with that row the lemma is false: for $n = m = 1$, $A = 1$, $c = 1$, $b = -1$, $R = 1$, $r = 0$ and $\alpha = 0$, one has $\mathrm{OPT} = 0 \ge \alpha$ but $\lambda^* > 0$. The derivation on p. 13 gives $(-e^{\mathsf T}, -1, 1)$, which the mission uses. Step (7) of the proof is written for $\alpha \ge 0$ and needs $|\alpha| \le R$ in general. The mission states the lemma with both repairs, so that later LP-solver formalizations can cite an exact statement. To our knowledge no machine-checked version of this reduction exists.

Difficulty

Each step is elementary, and the difficulty is bookkeeping. The game value is an infimum over the simplex, and the second case needs a strategy that actually attains it, or an approximation argument with slack. The homogenizing variable $h$ is pinned only approximately: an approximately optimal strategy satisfies $h \approx 1/2$ only up to $\varepsilon'''$. That error is multiplied by $\alpha/R$ and $c_i/R$, whose signs are arbitrary, so the inequalities that look natural for nonnegative data fail for negative $\alpha$ or $c_i$. The relaxed constraints then pass through weak duality, where the dual bound $r$ enters, and the errors have to add up to exactly $\varepsilon$. A reading with $\alpha \ge 0$ would cover only half of the binary search.

Formalization scope

• Data. $A$ is Matrix (Fin n) (Fin m) ℝ, $b$ is Fin m → ℝ and $c$ is Fin n → ℝ: constraints are indexed by Fin n and variables by Fin m, as in (4). The paper's index letters in §4 vary.

• Standing assumptions. A structure LPStanding A b c R r OPT collects them:

  • entries of $A$, $b$, $c$ in $[-1,1]$;
  • $R > 0$ and $|c_i| \le R$;
  • $\mathrm{OPT}$ bounds every primal feasible objective and is attained by a primal feasible $y$ with $\sum_j y_j \le R$;
  • $\mathrm{OPT}$ is attained by a dual feasible $x$ with $\sum_i x_i \le r$.

  The last item is the paper's assumption of strong duality, in the form its proof uses. It is a hypothesis, not a theorem to derive.

• The game. The matrix (6) has rows Fin 2 ⊕ (Unit ⊕ Fin n) and columns Fin m ⊕ Fin 2 (with $z$ = inr 0 and $h$ = inr 1), and its second row is the corrected $(-e^{\mathsf T}, -1, 1)$.

• The value. The value is sInf of the image of stdSimplex under $y \mapsto \max_i (My)_i$. It is not an infimum over a membership proposition, which in Lean would return $\min(0, \lambda^*)$ and make the first case vacuous. LP (1)'s side constraint $\lambda \in [-1, 1]$ is omitted because it is inactive for entries in $[-1, 1]$.

• Constants. $\varepsilon''' = \varepsilon/(6R(r+1))$ exactly, with $\varepsilon > 0$.

• Added hypothesis. $|\alpha| \le R$ is the one hypothesis not written in the lemma. §4 supplies it through the binary search range, and through the requirement that (6) be a game with entries in $[-1,1]$.

Trivializing formalizations are ruled out. LPStanding is satisfiable, the second row forces $\sum_j y_j + z = h$, the value is not junk on a positive game, and the goal is stated for every estimate within $\varepsilon'''$ rather than only at $\lambda^* = 0$. A sanity file checks the first three on small instances.

Infrastructure. Everything is built from Mathlib's stdSimplex, Matrix.mulVec and dotProduct. The attainment of the value of a finite matrix game (milestone exists_strategy_le) and weak duality with relaxed constraints are reusable beyond this mission. Proofs of any milestone are welcome, and so are alternative proofs of the second case that avoid attainment by a slack argument.

Selected references

• J. van Apeldoorn and A. Gilyén, Quantum algorithms for zero-sum games, arXiv:1904.03180v1, 2019. https://arxiv.org/abs/1904.03180
• M. D. Grigoriadis and L. G. Khachiyan, A sublinear-time randomized approximation algorithm for matrix games, Operations Research Letters 18(2):53–58, 1995. https://doi.org/10.1016/0167-6377(95)00032-0
• Y. Carmon, J. C. Duchi, A. Sidford and K. Tian, A rank-1 sketch for matrix multiplicative weights, arXiv:1903.02675, 2019. https://arxiv.org/abs/1903.02675
• G. B. Dantzig, A proof of the equivalence of the programming problem and the game problem, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, pp. 330–335.
• I. Adler, The equivalence of linear programs and zero-sum games, International Journal of Game Theory 42(1):165–177, 2013. https://doi.org/10.1007/s00182-012-0328-8

Motivation

On reward-based crowdfunding platforms such as Kickstarter, a project creator fixes two numbers before launch: the pledge level $p$, the amount a backer commits, and the campaign duration $T$. Both are set once and cannot be revised. A higher pledge earns more per backer but turns away backers whose valuation falls short, and a longer campaign reaches more backers but makes them wait longer for a project they value less the further away its delivery is. Zhang, Savin and Veeraraghavan (Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022; manuscript SSRN 3065267) model this trade-off with two kinds of backers. Independent backers decide on their own valuation. Herding backers arrive in proportion to the pledges already collected, so early success attracts more pledges. The paper asks when the creator should exploit herding and when it should ignore it.

This mission formalizes the paper's answer in the simplest setting it treats: every independent backer values the project at the same $v_i$, and every herding backer at the same $v_h$.

Setting

A campaign has a population $\hat I>0$ of independent backers, who arrive at rate $k>0$ times the number still to come. Every backer discounts the project's value at rate $r>0$: a backer arriving at time $t$ with valuation $v$ pledges if and only if $v e^{-r(T-t)}\ge p$. Herding backers arrive at time $t$ at rate $\Lambda_h q p$ times the number of pledges so far, where $\Lambda_h\ge0$ is an arrival rate and $q\ge0$ a propensity to pledge, and they pledge under the same discounted-value rule. Valuations lie in $[0,\bar v]$ and enter only through the survival functions $\bar F_i=1-F_i$ and $\bar F_h=1-F_h$ of the two valuation laws.

The paper solves the pledging dynamics in closed form (its Propositions 1 and 2). The numbers of pledging independent and herding backers at time $t$ are

$$n^p_i(t,p,T)=k\hat I\int_0^t e^{-kx}\bar F_i\big(pe^{r(T-x)}\big)\,dx,$$ $$n^p_h(t,p,T)=\Lambda_hqp\,k\hat I\int_0^t e^{\Lambda_hqp\int_\tau^t\bar F_h(pe^{r(T-u)})du}\,\bar F_h\big(pe^{r(T-\tau)}\big)\int_0^\tau e^{-kx}\bar F_i\big(pe^{r(T-x)}\big)dx\,d\tau .$$

The total number of pledges is $n(p,T)=n^p_i(T,p,T)+n^p_h(T,p,T)$, and the creator's problem (18) is

$$\max\ \pi(p,T)=p\,n(p,T)\quad\text{over}\quad 0<p\le\bar v,\ \ 0\le T\le\tfrac1r\ln(\bar v/p).$$

With identical valuations, $\bar F_i(y)=1$ for $y<v_i$ and $0$ for $y\ge v_i$, and likewise $\bar F_h$ with $v_h$, where $0<v_i,v_h\le\bar v$. Proposition 6 adds the constraint $T\le\frac1r\ln(v_i/p)$, under which every independent backer pledges from the start.

Formalization targets

Goal: Proposition 6(ii)

Let $\Lambda_h,q>0$, $v_i>v_h$, and set $\delta=\Lambda_hqv_h/r$, $a=k/(\Lambda_hq)$, $b=\Lambda_hq/r$ and

$$X=e^{bv_h/e}\frac1{4a}\Big(\frac kr v_he^{-2}+0.5\,bv_h^2e^{-3}+2a+v_h\Big)+\frac1a\Big(\frac kr(v_h+a)+a\Big).$$

If $\delta<1$ and $v_i/v_h>(X/(1-\delta))^{r/k}$, then on Proposition 6's feasible set the unique maximizer of $\pi$ is

$$p^*=v_i\Big(\frac r{k+r}\Big)^{r/k},\qquad T^*=\frac1r\ln\frac{v_i}{p^*}.$$

Milestones

1. Corollary 1. If $0<p\le\min(v_ie^{-rT},v_h)$, then for $t\in[0,T]$, $n^p_i(t,p,T)=\hat I(1-e^{-kt})$ and $n^p_h$ equals the explicit formula (15).
2. Proposition 3(b). If $\Lambda_hqv_h/r<1$ and $k/r>2$, then for every sufficiently long fixed duration $T$, the unique optimal pledge level on (18)'s range is $p^*(T)=v_ie^{-rT}$.
3. Proposition 6(i). If $v_i\le v_h$, an optimal campaign exists on Proposition 6's feasible set, and every optimum has $p^*\ge v_i/e$ and $T^*\le 1/r$.

Significance

Proposition 6 separates two regimes. When herding backers value the project at least as much as independent ones, the optimal campaign is short, $T^*\le1/r$, and its pledge is at least $v_i/e$. When herding is weak ($\delta<1$) and independent backers value the project enough more than herding ones, the creator's best response is to price herding backers out entirely and run the campaign that would be optimal if no herding backer existed. The threshold (33) quantifies "enough more". Together with Proposition 3(b), which fixes the duration and finds that the optimal pledge sits exactly at the highest level that keeps every independent backer in from the start, these results give a creator explicit rules rather than a numerical optimization.

The paper states that the proofs of Propositions 3 to 7 are in an online Technical Appendix, which is not part of the manuscript this mission cites; the manuscript's own Appendix proves only Propositions 1 and 2 and Corollaries 1 and 2. None of the results has a machine-checked proof. Formalizing Proposition 6(ii) would supply a verified proof of a result whose published proof is not in the source held here, and would check the threshold (33), whose grouping of terms is read off the typeset page.

Difficulty

The objective $\pi$ is defined through nested integrals of step functions, so it is not differentiable everywhere: the jumps of $\bar F_i$ and $\bar F_h$ put kinks in $\pi$ where $p=v_ie^{-rT}$ and where $p=v_he^{-rT}$ or $p=v_h$, at which a backer type starts or stops pledging during the campaign. Setting a gradient to zero does not identify the optimum. The obvious argument for the goal, that herding backers do not pledge at $p^*>v_h$ and so the no-herding optimum is optimal, compares only campaigns that exclude herding backers; it says nothing about the campaigns with a lower pledge level that do attract them. Those campaigns gain a herding term growing exponentially in $\Lambda_hqp$ times the time during which herding backers pledge, and the comparison must hold uniformly over the whole feasible region, which is what the threshold (33) is for. Uniqueness, not only optimality, must also be shown.

Formalization scope

All objects live in the namespace CrowdfundRM.Identical. Parameters form a structure Campaign with fields Ihat, k, r, Lh (for $\Lambda_h$), q, vbar, Fbi, Fbh. The standing assumptions, implicit in the paper, are $\hat I,k,r,\bar v>0$, $\Lambda_h,q\ge0$, and that each survival function is nonincreasing, takes values in $[0,1]$, equals $1$ below $0$ and $0$ from $\bar v$ on. Identical valuations set $\bar F_i$, $\bar F_h$ to the step functions above with $0<v_i,v_h\le\bar v$.

Conventions: real numbers throughout; the pledge counts are the closed forms (5) and (11); the feasible set of (18) adds $p>0$, which $\ln(\bar v/p)$ requires; "the optimal" is the unique maximizer over the stated feasible set, and Proposition 6(i), which does not claim uniqueness, asserts that a maximizer exists and bounds every maximizer; "sufficiently long" in Proposition 3(b) is an unspecified threshold $T_0>0$; $\Lambda_h,q>0$ is added in Proposition 6(ii) because $a$ and $b$ divide by $\Lambda_hq$. The paper's $T^*=\frac1r\ln(v_i/\bar p)$ has an undefined $\bar p$ and is read as $p^*$. In (33) the factors $e^{bv_h/e}$ and $1/(4a)$ multiply only the first bracket.

The following formalizations would trivialize the targets and are ruled out: defining $n(p,T)$ by the explicit formulas (14)–(15) or by the paper's single formula (17) instead of (5) and (11); stating optimality through sSup or a first-order condition; stating Proposition 6(i) for maximizers without asserting that one exists; and stating Proposition 3(b) with a chosen threshold or with Proposition 6's narrower feasible set. The pledging differential equations themselves and their solution (Propositions 1–2) are formalized in the companion mission on triangular valuations; this mission works from their closed forms.

Infrastructure needed: interval integrals of monotone step functions, the exponential, logarithm and real power from Mathlib. Explicit evaluation of the nested integrals under step laws (Corollary 1) is reusable for any proof in this model. Contributions are welcome on each milestone and on lemmas such as continuity of $\pi$ on the feasible set and the closed form of $\pi$ in each region of $(p,T)$.

Selected references

• J. Zhang, S. Savin, S. Veeraraghavan, Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1147. Cited from the authors' manuscript of May 26, 2021, SSRN 3065267: https://ssrn.com/abstract=3065267

Motivation

Many outpatient clinics offer two ways in: an appointment booked online, and walk-in hours on the day. Some patients have no choice (acute cases arrive as walk-ins), but many can pick either channel, and they pick the one that costs them less: a long appointment delay pushes them into the walk-in room, a crowded walk-in room pushes them to book or to give up. A clinic deciding how to split its daily capacity between the two channels therefore faces a game, not a forecasting problem.

Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science 2023, doi:10.1287/mnsc.2023.4676) model this game and compare three operational levers: the capacity split, how much delay information the booking system reveals, and triage, that is, reserving walk-in hours for acute patients only (as some practices do, e.g. Centre Pediatrics 2021). This mission formalizes the triage comparison, Proposition 6 of the paper: closing walk-in hours to patients who could book pays off exactly when lost demand is cheap relative to overtime.

Setting

Patients. Exogenous walk-ins arrive at rate $\lambda_E$ and are always served on the day, possibly in overtime. Strategic patients arrive as a Poisson process of rate $\lambda>0$. A served patient gains $R>0$.

Capacity. The clinic has total capacity $\mu>0$ per day, split into appointment hours $\mu_S$ and walk-in hours $\mu_W=\mu-\mu_S$, with $\mu_S\in[0,\mu)$.

The appointment queue. Appointments form a single-server queue with deterministic service time $1/\mu_S$. In the observable setting a patient sees the queue: with $k$ patients waiting, the delay is $(k+\tilde u)/\mu_S$, $\tilde u$ uniform on $[0,1]$. A patient schedules when this delay is at most a threshold $\delta$, and scheduling at delay $d$ is worth $u^2_S(d)=R-C_D d$. The fraction of strategic patients who do not schedule is the blocking probability $\pi(\delta,\mu_S)$ of this M/D/1/K−1+p queue, where $K=\lceil\delta\mu_S\rceil$ and $p=\delta\mu_S+1-K$. With $\rho=\lambda/\mu_S$ it has the closed form $\pi(\delta,\mu_S)=1-1/(q_0+\rho)$, where $q_0$ is built from the Poisson weights $\alpha_j=\rho^je^{-\rho}/j!$ by the Brun–Garcia recursion (Online Appendix C, (26)–(27), Corollary C.1). With no appointment hours, $\pi(\delta,0)=1$.

Walking in and balking. A patient who does not schedule walks in with probability proportional to $p_W$ or balks with probability proportional to $p_B$. Walking in is worth $u^2_W(p_W)=R-C_W\,w\big((\lambda_E+p_W\lambda)/\mu_W\big)$, with $w$ convex, strictly increasing and $w(0)=0$; balking is worth $0$. An observable equilibrium $(\delta,p_W,p_B)$ is a solution of conditions (6)–(10): the threshold $\delta$ makes scheduling at least as good as the walk-in/balk mixture up to $\delta$ and worse beyond it, $p_W+p_B=\pi(\delta,\mu_S)$, and patients walk in (balk) only if walking in is worth at least (at most) zero.

Costs. The provider pays $C_L$ per balking patient and $C_O\,o(\cdot)$ for overtime, with $o$ convex and strictly increasing. In the strategic model patients choose freely, and the cost at allocation $\mu_S$ and equilibrium $(\delta,p_W,p_B)$ is

$$Z^s=C_L\,p_B\lambda+C_O\,o\Big(\frac{p_W\lambda+\lambda_E}{\mu_W}\Big). \qquad\text{(Ob.P)}$$

In the triage model strategic patients may only schedule or balk, so they behave with threshold $R/C_D$ and

$$Z^t=C_L\,\pi(R/C_D,\mu_S)\,\lambda+C_O\,o\Big(\frac{\lambda_E}{\mu_W}\Big). \qquad\text{(T.Ob.P)}$$

Let $\underline\mu_W$ solve $R-C_W\,w(\lambda_E/\underline\mu_W)=0$ (15): below these walk-in hours the exogenous walk-ins alone make walking in worthless.

Formalization targets

Goal: Proposition 6

Suppose $\mu>\underline\mu_W$ and set

$$\underline\alpha=\frac{o'(\lambda_E/\mu)}{\mu},\qquad \overline\alpha=\frac{o'(\lambda_E/\underline\mu_W)}{\underline\mu_W}\max\Big\{\frac{\lambda_E}{\lambda\,\pi(R/C_D,\mu-\underline\mu_W)},1\Big\}.$$

Then

$$\frac{C_L}{C_O}\le\underline\alpha\ \Longrightarrow\ \inf Z^t\le\inf Z^s,\qquad \frac{C_L}{C_O}\ge\overline\alpha\ \Longrightarrow\ \inf Z^s\le\inf Z^t,$$

where the infima are over allocations $\mu_S\in[0,\mu)$ and, on the strategic side, over the equilibria at each allocation. The Lean statement says this without infima: every strategic configuration is matched by a triage allocation that costs no more, and every triage allocation is matched by a strategic allocation at which an equilibrium exists and every equilibrium costs no more.

Milestones

1. Proposition C.2 ($\mu_S$-part): $\mu_S\mapsto\pi(\delta,\mu_S)$ is continuous and strictly decreasing on $(0,\infty)$.
2. Proposition 1 (observable setting): an observable equilibrium exists at every allocation.
3. Proposition 2 (1): if $\mu_W\le\underline\mu_W$, every equilibrium is schedule-and-balk, $p_W=0$, $\delta=R/C_D$, $p_B=\pi(R/C_D,\mu_S)$.
4. From the proof of part 1: $\lambda\,(1-\pi(\delta,\mu_S))\le\lambda\,(1-\pi(R/C_D,\mu_S))$ at every equilibrium.
5. From the proof of part 2: if nobody balks, $(\lambda p_W+\lambda_E)/\mu_W\le\lambda_E/\underline\mu_W$.
6. From the proof of part 2: if patients mix between walking in and balking, $(\lambda p_W+\lambda_E)/\mu_W=\lambda_E/\underline\mu_W$.

Significance

Proposition 6 turns a qualitative trade-off into two explicit thresholds on the ratio of the lost-demand cost to the overtime cost. Free choice reduces balking but lets strategic patients crowd the walk-in hours; triage removes that crowding at the price of more balking. The thresholds $\underline\alpha$ and $\overline\alpha$ depend only on the overtime function, the capacity and the blocking probability, so a clinic can evaluate them from its own data. The paper also shows (Remark 4, Appendix D.8) that the same insight holds in the unobservable setting, with capacity playing an additional role; that variant is not part of this mission.

The result is proved in the paper (Online Appendix E.3, pp. 35–37) and has no machine-checked proof. The formalization adds three things. It fixes the equilibrium concept precisely, including the mixture weights and the endpoint conventions. It states the comparison of optimal costs without presupposing that the optima are attained; the paper's proof begins "denote the optimal capacity allocations" without proving existence. And it ties the blocking probability to the paper's closed form, so the monotonicity in $\mu_S$ that the proof invokes becomes a statement about an explicit function rather than about a queue described in words.

Difficulty

The comparison itself is a chain of convexity inequalities at a single allocation. The hard part is the blocking probability. The paper proves that $\pi(\delta,\mu_S)$ decreases in $\mu_S$ by a sample-path argument on the queue, but a formal development has only the closed form, in which $K=\lceil\delta\mu_S\rceil$ jumps at every $\mu_S$ where $\delta\mu_S$ is an integer, $p$ jumps from $1$ to $0$ there, and $\rho=\lambda/\mu_S$ moves continuously. Monotonicity and continuity must be shown across these seams, through alternating sums whose terms cancel heavily. The obvious route, differentiating the closed form for fixed $K$, does not give the sign without a further structural argument on the coefficients $a_j$.

Existence of an equilibrium (milestone 2) is an intermediate-value argument in $\delta$, which in turn needs continuity of $\pi$ in $\delta$ and positivity of $\pi$.

Formalization scope

Everything lives in the namespace OutpatientWalkIn.Triage. The definition Queue contains the closed-form blocking probability blockProb lam δ μS; the definition Setting contains the model, the standing assumptions, the utilities, the equilibrium IsObsEq, the costs obsCost and triageCost, and the thresholds alphaLow, alphaHigh.

Conventions:

• Standing assumptions, hypotheses of every theorem: $\lambda>0$, $\lambda_E\ge0$, $R,C_D,C_W>0$, $C_L,C_O\ge0$, $\mu>0$; $w$ convex and strictly increasing on $[0,\infty)$ with $w(0)=0$ (Assumption 1); $o$ convex and strictly increasing on $[0,\infty)$ (Assumption 2).
• Allocations range over $\mu_S\in[0,\mu)$ on both sides, so that $\mu_W>0$; the paper's $\mu_S=\mu$ leaves the exogenous walk-ins with no walk-in hours.
• $\pi(\delta,0)=1$; the observable setting is defined directly (the paper's $C_G=0$).
• The equilibrium carries the guard $p_W+p_B>0$, which by (8) is $\pi(\delta,\mu_S)>0$ and excludes no equilibrium of the paper.
• Added hypotheses of the goal: $C_O>0$, $\lambda_E>0$, $\underline\mu_W>0$ given by (15), and differentiability of $o$ at $\lambda_E/\mu$ and $\lambda_E/\underline\mu_W$ (where $o'$ is evaluated). Without them Lean's $C_L/0=0$ and the zero derivative of a non-differentiable function would make $\underline\alpha=0$ and turn part 1 into a different claim.
• "Costs less" is "costs no more" (p. 26).

A formalization that compares the two models at one fixed allocation only, that lets the prover choose a cheap equilibrium when several might exist, or that replaces $\pi$ by an arbitrary decreasing function, is not the paper's theorem; the statements here rule these out.

Contributions welcome: properties of the closed-form $\pi$ (positivity, $\pi\le1$, monotonicity and continuity in both arguments), the existence of equilibria, and the convexity estimates of the final comparison. The queue file is reusable for any M/D/1/K model with partial joining.

Selected references

• N. Liu, W. van Jaarsveld, S. Wang, G. Xiao, Managing Outpatient Service with Strategic Walk-ins, SSRN 3558209 (version of 2022-07-05); Management Science, 2023. https://ssrn.com/abstract=3558209, https://doi.org/10.1287/mnsc.2023.4676
• O. Brun, J.-M. Garcia, Analytical solution of finite capacity M/D/1 queues, Journal of Applied Probability 37(4), 2000 (the source of the $a_j$ recursion, cited in the paper's Online Appendix C).
• P. Naor, The regulation of queue size by levying tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200