Optimization

Motivation

Blood platelets, fresh produce and many pharmaceuticals have a fixed lifetime: a unit not used within $m$ periods of its arrival must be discarded. Optimal ordering for such products depends on the whole age profile of the stock, and the dynamic program that describes it has an $(m-1)$-dimensional state. It is intractable beyond small $m$ (Nahmias, 1982; Nandakumar & Morton, 1993), so practice relies on base-stock policies, which raise the total stock to a fixed level $S$ every period.

Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first performance guarantees for base-stock policies in this system. Under first-in-first-out (FIFO) issuance a heuristic base-stock level is asymptotically optimal in the lifetime, the demand population, the penalty cost and the outdating cost (missions 1–4 of this series). Under last-in-first-out (LIFO) issuance, which models a customer who picks the freshest unit from the shelf, a simple base-stock level is asymptotically optimal in the penalty cost and, when demand can be arbitrarily small, in the outdating cost (Theorem 5, mission 5). This mission formalizes the complementary negative result: when the demand is bounded away from zero, no base-stock policy is asymptotically optimal under LIFO as the outdating cost grows.

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0 < \mathbb E[D] < \infty$ and distribution function $F$. The lower support is $\underline D = \inf\{x : F(x) > 0\}$, and the newsvendor level is $S^{NP} = F^{-1}(p/(p+h))$ with $F^{-1}(x) = \inf\{y : F(y) \ge x\}$.

The product has lifetime $m \ge 1$. At the start of period $t$ the state is $x_t = (x_{t,1}, \dots, x_{t,m-1})$, where $x_{t,i}$ is the stock with remaining lifetime at most $i$; the system starts empty. The firm orders $q_t \ge 0$, which arrives at once, raising the total stock to $x_{t,m} = x_{t,m-1} + q_t$. Demand $D_t$ is served youngest stock first, unmet demand is lost, and stock reaching the end of its lifetime outdates. Under LIFO the outdated amount and the next state are

$$o_t = \min\{(x_{t,m} - D_t)^+, x_{t,1}\}, \qquad x_{t+1,i} = \min\{(x_{t,m} - D_t)^+, x_{t,i+1}\} - o_t .$$

Each period costs $C^\pi_t = h(x_{t,m} - D_t)^+ + p(D_t - x_{t,m})^+ + \theta o_t$ with $h, p > 0$ and $\theta \ge 0$. A policy is admissible if its order in period $t$ is a nonnegative measurable function of the current state. Its long-run average cost is $C^\pi = \limsup_T \frac1T \sum_{t=1}^T \mathbb E[C^\pi_t]$, and $\mathrm{OPT}^{LIFO} = \inf_\pi C^\pi$. The base-stock policy $\pi_S$ orders $(S - x_{t,m-1})^+$, with cost $C^{LIFO}(S)$. The subscript $\theta$ marks the outdating cost; $h$, $p$, $m$ and the demand law are fixed.

Formalization targets

Goal: Proposition 1 (p. 17)

If $m \ge 2$ and $S^{NP} > \underline D > 0$, then

$$\lim_{\theta\to\infty}\big(C^{LIFO}_\theta(S^{LIFO,*}_\theta) - \mathrm{OPT}^{LIFO}_\theta\big) > 0,$$

where $C^{LIFO}_\theta(S^{LIFO,*}_\theta) = \inf_{S \ge 0} C^{LIFO}_\theta(S)$ is the best base-stock cost. The goal asserts that both costs are finite, and that the limit exists and is strictly positive.

Milestones (Appendix C.3, pp. ec8–ec9)

1. Under $m\ge2$ and $S^{NP}>\underline D>0$, $\lim_{\theta\to\infty} \min_{S\ge0} \hat C_{L,\theta}(S) = p(\mathbb E[D] - \underline D)$, where $\hat C_L(S) = h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+] + \frac{\theta}{m}\mathbb E[(S - \max\{D_1,\dots,D_m\})^+]$ is the lower bound (11).
2. Under the same hypotheses, $\lim_{\theta\to\infty} C_\theta(S^{LIFO,*}_\theta) = p(\mathbb E[D] - \underline D)$.
3. Under the same hypotheses, $h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+] \le p(\mathbb E[D] - \underline D)$ for all $S \in [\underline D, \min\{S^{NP}, m\underline D\}]$.
4. The policy that orders $\min\{S^{NP}, m\underline D\}$ units in periods $1, m+1, 2m+1, \dots$ and uses base-stock level $\underline D$ otherwise is admissible, and its long-run average cost is strictly less than $p(\mathbb E[D] - \underline D)$ and independent of $\theta$.
5. $\lim_{\theta\to\infty} \mathrm{OPT}^{LIFO}_\theta < p(\mathbb E[D] - \underline D)$.

The proof also uses Lemma 3 ($\hat C_L \le C^{LIFO} \le \hat C_U$, p. 16) and inequality (EC.22) (p. ec8). Both are milestones of mission 5 of this series and are not restated here.

Significance

Proposition 1 marks the boundary of Theorem 5(c). Together they show that under LIFO, with a large outdating cost, base-stock policies are asymptotically optimal exactly in the trivial cases $m = 1$ or $S^{NP} \le \underline D$, and when $\underline D = 0$. In the remaining case some optimality gap persists however large $\theta$ is. Under FIFO the heuristic level is asymptotically optimal in $\theta$ without conditions (Theorem 4), so the result separates the two issuance rules: a manager facing fresh-first customers and costly waste should look beyond base-stock policies.

The result is proved in the paper; nothing in it is machine-checked. A formal proof would give the first verified statement about the long-run cost of a perishable inventory system. It would also produce reusable pieces: the LIFO recursion, the base-stock cost under LIFO, and a time-dependent policy whose cost can be computed exactly.

Difficulty

The obvious argument compares two limits. The limit of the best base-stock cost needs a lower bound valid for every base-stock level at once, and that bound must be uniform as $\theta$ changes. The lower bound $\hat C_L$ of Lemma 3 controls the outdating only through $\mathbb E[(S - \max_i D_i)^+]$, so the limit of its minimum has to be computed separately. The upper side cannot use a base-stock policy at all. It needs an explicit policy that is not stationary. That policy must be shown never to outdate along every demand path, and its periodic cost has to be bounded strictly below $p(\mathbb E[D]-\underline D)$. The strictness needs the facts that $S^{NP} > \underline D$ and that $m\underline D > \underline D$, which is where $m \ge 2$ and $\underline D > 0$ enter. A long-run average over a non-stationary policy is a $\limsup$ of Cesàro means, and the step from per-period bounds to the average has to be made explicitly.

Formalization scope

• Demand is the published CappedBaseStock.DemandLaw: a probability law on $[0,\infty)$ with finite positive mean. The demand path carries the i.i.d. product law. The newsvendor cost $h\mathbb E[(S-D)^+] + p\mathbb E[(D-S)^+]$ and $S^{NP}$ are backorderCost and newsvendorLevel of the published LostSalesOrderUpTo.Asymptotic.Backorder.
• Time is zero-based: Lean period $t$ is the paper's period $t+1$, and the cyclic policy's periods $1, m+1, \dots$ are Lean periods with $t \bmod m = 0$.
• The state is a vector of cumulative levels Fin (m - 1) → ℝ with $x_{t,0} := 0$, so $m = 1$ is allowed. Levels $S$ range over $[0,\infty)$.
• Period costs are in $[0,\infty]$, and expectations are lower Lebesgue integrals over the path law. $C^\pi$ is the $\limsup$ of Cesàro averages.
• $\Pi$ is the paper's class: time-dependent, deterministic, measurable functions of the current state. $\mathrm{OPT}^{LIFO}$ is the infimum over all of $\Pi$, not over base-stock policies.
• $C(S)$ is the simulated long-run average cost of $\pi_S$, not a formula. The best base-stock cost is $\inf_{S\ge0} C(S)$, because existence of a minimizer under LIFO is not shown. "min" in milestone 1 is likewise an infimum of a nonnegative real function.
• Limits in $\theta$ are along $\theta \in [0,\infty)$ with the other parameters fixed. The goal subtracts real values only after asserting finiteness, so neither $\infty - \infty$ nor a truncated subtraction can make it true. A formalization that fixes $\theta$, sets $m = 1$, restricts $\mathrm{OPT}$ to base-stock policies or defines $C(S)$ by the bound of Lemma 3 would trivialize or falsify the statement, and is ruled out.

The work needs a Cesàro-limit toolkit for $[0,\infty]$-valued sequences, the LIFO sample-path recursion, and convexity facts for the newsvendor cost. Proofs of the milestones, and of the definitional sanity facts ($\pi_S \in \Pi$, $C(S) < \infty$), are welcome.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, SSRN 3724966, 2022. https://ssrn.com/abstract=3724966 (version of record: Management Science, 2022, doi:10.1287/mnsc.2022.4400).
• S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 680–708, 1982. https://doi.org/10.1287/opre.30.4.680
• P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1490–1498, 1993. https://doi.org/10.1287/mnsc.39.12.1490

Motivation

A manufacturer can sell directly to consumers and also supply an independent retailer. The retailer reaches consumers for whom its distribution service is more valuable, but its presence can also force the manufacturer to lower direct-channel prices. Jullien, Reisinger and Rey study when the additional sales justify dual distribution under different abilities to personalize retail prices (Jullien, Reisinger and Rey, 2023). This mission isolates their Proposition 4: the manufacturer can personalize its own prices, and the retailer may either personalize or charge one uniform price. The source used here is the authors' March 2022 manuscript; the formal claims follow its Proposition 4 and Online Appendix A.

The question matters for vertical channel design because a retailer's reach and the competition it creates pull industry profit in different directions. The manufacturer and retailer negotiate a wholesale contract before retail pricing. A fixed fee can divide their combined profit, so the distribution decision depends on whether both channels together earn more than the manufacturer's direct channel alone. The model makes that comparison exact for a continuum of consumers rather than treating the retailer's contribution as a general benefit (Jullien, Reisinger and Rey, 2023).

Setting

Consumers have types $x\in[0,X]$, with one unit of consumer mass per unit of $x$. A monopoly manufacturer A offers a direct channel, and retailer B offers a differentiated service. Their consumer values are $u_A(x)=\max\{1-x,0\}$ and $u_B(x)=\max\{v-sx,0\}$. The market parameters satisfy $0<s<v<1$ and $X\ge v/s$. Thus both valuations fall as the consumer index rises, B's valuation falls more slowly, and the market extends beyond the last consumer with positive value for B. The two values cross at $\hat x=(1-v)/(1-s)$, with common value $\hat u=(v-s)/(1-s)$.

The channel contributions measure valuation advantages. A's contribution is $\alpha=\int_0^{\hat x}(u_A(x)-u_B(x))\,dx$; B's is $\beta=\int_{\hat x}^{X}(u_B(x)-u_A(x))\,dx$. They are defined by the integrals. The closed forms in the Online Appendix, $\alpha=(1-v)^2/[2(1-s)]$ and $\beta=(v-s)^2/[2s(1-s)]$, are milestone results, not substitutions into the definitions.

The manufacturer can instead use mono distribution, selling only through A and charging each consumer the full direct-channel value. Its profit is $\Pi_P^m=\int_0^X u_A(x)\,dx=1/2$. Under dual distribution, a two-part tariff has wholesale price $w\ge0$ and a fixed fee. The fee allocates the proceeds between firms; industry profit is the total price paid by consumers. Dual distribution is selected only when its industry profit strictly exceeds $\Pi_P^m$, as specified in the manuscript's footnote 17.

Two retail continuations are relevant. In PP, both firms personalize prices, and the manuscript selects the Bertrand equilibrium where the lower-valued offering prices at its opportunity cost. In PU, B first announces one price $p_B$, and A then tailors its prices to consumer types. B chooses a globally profit-maximizing price after allowing for A's response. These rules determine each consumer's payment and hence industry profit; they are represented directly in the Lean definitions.

Formalization targets

The central target is Proposition 4. It asserts the existence of functions $\beta_{PP}$ and $\beta_{PU}$ of $\alpha$ alone, valid uniformly across all admissible $(v,s,X)$, with

$$\text{dual distribution in PP}\iff\beta>\beta_{PP}(\alpha),\qquad \text{dual distribution in PU}\iff\beta>\beta_{PU}(\alpha),\qquad \beta_{PP}(\alpha)<\beta_{PU}(\alpha).$$

The valuation-space milestones identify the underlying cutoffs $\tilde v(s)=s(2+\sqrt{1-s})/(1+s)$ in PP and $\check v(s)=s[2+\sqrt{(1-s)(2+5s+s^2)/(1+2s)}]/(1+s)$ in PU. They say dual distribution is strictly better exactly when $v$ exceeds the respective cutoff. Other milestones give the mono benchmark, the formulas for $\alpha$ and $\beta$, the existence of the two contribution thresholds, and the strict ordering $\tilde v(s)<\check v(s)$ (Jullien, Reisinger and Rey, 2023, Proposition 4 and Online Appendix A).

Significance

Proposition 4 turns a distribution choice involving wholesale and retail prices into a comparison of two channel contributions. It identifies precisely how large B's contribution must be to make a second channel profitable, and it says that B's ability to personalize prices lowers that required contribution. A price policy restriction on B therefore changes the region of market parameters in which the retailer is brought into the channel. The strict threshold statement also distinguishes an actual gain from a tie with mono distribution.

The result is proved in the authors' manuscript, with detailed arguments in Online Appendix A. This mission asks for a machine-checked version of the market definitions, its integral and cutoff identities, and the passage from $(v,s)$ to $(\alpha,\beta)$. The proposed Lean theorem files contain open proof obligations; compilation of their statements does not supply those proofs. A completed development would give reusable formal definitions of the consumer outcomes and a checked statement of the channel comparison.

Difficulty

The industry profit changes formula as the wholesale price changes which consumers can be served by B. In PP, the profit derivative has different expressions on either side of $w=v-s$, and the curvature of one region changes with $s$. In PU, B's uniform price can leave some consumers buying directly from A both before and after B's customer interval. A single interior first-order calculation therefore does not settle the global distribution choice. The contribution thresholds add another step: each cutoff in $(v,s)$ must correspond to a threshold depending only on $\alpha$, and the two resulting thresholds must retain a strict order along every admissible iso-$\alpha$ curve (Jullien, Reisinger and Rey, 2023, Online Appendix A).

Formalization scope

Lean uses real numbers for $v,s,X,w,p_B$, interval integrals against Lebesgue measure for profits and contributions, and the Lebesgue volume of B's buyer set for its PU demand. The standing assumptions are exactly $0<s<v<1$ and $v/s\le X$. Retail prices in B's maximization range over all real numbers; wholesale prices satisfy $w\ge0$. The continuation fixes an assignment of indifferent consumers. Positive-valuation tie boundaries have measure zero; at $w=0$, an interval of zero-valuation consumers pays zero in PP. Consumers with $u_B(x)=0$ are assigned to A in PU and are excluded from B's demand. If several uniform prices maximize B's profit, a strict industry gain at one maximizing price suffices in the dual-distribution predicate.

The setting defines industry profits from consumer payments and defines dual distribution by a strict profit comparison. It never defines them from $\tilde v$, $\check v$, or the desired threshold functions. The real-valued integrals are well behaved here because the consumer interval is bounded and the integrands are piecewise affine. The cutoff expressions use positive denominators under the standing assumptions. The PU price maximum is global; neither a stationary point nor the first market configuration is built into the definition.

A complete proof needs interval integration of piecewise affine functions, global optimization across the PP and PU price regions, and a comparison of the induced contribution-space thresholds. The integration and market-outcome lemmas can be reused for related channel games. Contributions establishing the stated milestones, or reusable lemmas about these bounded price regions, fit the mission's scope.

Selected references

• Bruno Jullien, Markus Reisinger and Patrick Rey, Personalized Pricing and Distribution Strategies, Management Science, 2023. DOI 10.1287/mnsc.2022.4437. Formalization source: authors' manuscript of March 2022, PDF SHA-256 25a6c84ac0c48c6720f6a9e1f9b1f1ec516412c31dac044ac84c1d4c72dfc253, Proposition 4 and Online Appendix A.

Perishable inventory with backlogging and lead times

Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that is not used within $m$ periods of its arrival must be discarded. Managing such products is a classical problem of inventory theory (Nahmias 1982, Operations Research 30(4), doi:10.1287/opre.30.4.680). The optimal ordering policy depends on the entire age profile of the stock, so it is computationally intractable beyond very short lifetimes, and practitioners use base-stock policies, which raise a single aggregate quantity to a fixed level $S$ every period.

Bu, Gong and Chao (SSRN 3724966, accepted manuscript, 2022; Management Science) give the first theoretical performance guarantees for base-stock policies in perishable systems. This mission covers §5 of the paper: the backlogging system with a positive replenishment lead time $L$, where unmet demand waits and orders arrive $L$ periods after they are placed. Earlier missions of this series treat the zero-lead-time lost-sales system under FIFO issuance (missions 1–4) and under LIFO issuance (missions 5–6).

Setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$. The product has lifetime $m\ge1$, the lead time is $L$, and the unit costs are $h>0$ (holding, per unit left over), $b>0$ (backlogging, per unit per period) and $\theta$ (outdating, in addition to holding). Throughout, $\theta\ge hL$.

In period $t$ the order placed in period $t-L$ arrives and serves backorders first. The firm then observes the state $\mathbf x_t=(x_{t,1},\dots,x_{t,m+L-1})$: for $i\le m$, $x_{t,i}$ is the on-hand stock with remaining lifetime at most $i$ minus the backorders, and for $m<i<m+L$ it adds the pipeline orders that arrive by period $t+i-m$. The firm orders $q_t\ge0$, which raises the inventory position to $x_{t,m+L}=x_{t,m+L-1}+q_t$. Demand $D_t$ is served oldest-first (FIFO), the shortfall is backlogged, and with the outdated quantity $o_t=(x_{t,1}-D_t)^+$ the state moves by

$$x_{t+1,i}=x_{t,i+1}-D_t-o_t,\qquad i=1,\dots,m+L-1 .$$

The system starts empty. The cost of period $t$ is $C^\pi_t=h(x_{t,m}-D_t)^++b(D_t-x_{t,m})^++\theta o_t$, where $x_{t,m}$ is the net on-hand inventory.

An admissible policy $\pi\in\Pi$ orders $\varphi^\pi_t(\mathbf x_t)\ge0$ with each $\varphi^\pi_t$ measurable. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$, and $\mathrm{OPT}^L=\inf_{\pi\in\Pi}C^\pi$. The base-stock policy $\pi_S$ orders $(S-x_{t,m+L-1})^+$; its cost is $C^L(S)$. The heuristic level $\widetilde S^L$ is any minimizer over $[0,\infty)$ of

$$\widetilde C^L(S)=h\mathbb E\Big[\Big(S-\sum_{i=1}^{L+1}D_i\Big)^+\Big]+b\mathbb E\Big[\Big(\sum_{i=1}^{L+1}D_i-S\Big)^+\Big]+\frac{\theta-hL}{m+L}\mathbb E\Big[\Big(S-\sum_{i=1}^{m+L}D_i\Big)^+\Big].$$

Formalization targets

Goal: Theorem 7 (p. 20)

For $L\ge1$ and every minimizer $\widetilde S^L$, the gap $C^L(\widetilde S^L)-\mathrm{OPT}^L$

(a) is at most $K_1e^{-K_2m}$ for all lifetimes $m\ge1$, with $K_1,K_2>0$ independent of $m$;

(b) if the one-period demand has the population form $D(n)=\sum_{j=1}^{N(n)}\hat D_j$ of (7), with $N(n)=\sup\{N:\sum_{k=1}^NX_k/n\le1\}$ and the moment assumptions of Theorem 2, is at most $K_1e^{-K_2n}$ for all large $n$, for every fixed lifetime $m\ge2$;

(c) tends to $0$ as $\theta\to\infty$, for every choice $\theta\mapsto\widetilde S^L_\theta$ of minimizers.

Milestones

$$x^\pi_{t+L,m}=x^\pi_{t,m+L}-\sum_{i=t}^{t+L-1}D_i-\sum_{i=t}^{t+L-1}o^\pi_i,\qquad \sum_{i=t}^{t+m+L-1}o^\pi_i\ge\Big(x^\pi_{t,m+L}-\sum_{i=t}^{t+m+L-1}D_i\Big)^+ \quad\text{(EC.29), (EC.30)}$$

Lemma 5 (p. 19): for $L\ge0$ and $S\ge0$, $C^L(S)\ge\widetilde C^L(S)$, and $C^L(S)$ is at most the same expression with $\frac{\theta-hL}{m+L}$ replaced by $\theta+bL$. Proposition 4 (p. 23): $\mathrm{OPT}^L\ge\widetilde C^L(\widetilde S^L)$ for $L\ge1$. Inequality (28) (p. 24):

$$C^L(\widetilde S^L)-\mathrm{OPT}^L\le\frac{(m-1)\theta+(b(m+L)+h+\theta)L}{m+L}\,\mathbb E\Big[\Big(\widetilde S^L-\sum_{i=1}^{m+L}D_i\Big)^+\Big].$$

Significance

Theorem 7 says that a policy computed from one convex function of one variable is nearly optimal for a control problem whose state has dimension $m+L-1$, in three practically relevant regimes: long shelf life, high-volume demand, and expensive waste. The bound (28) is explicit and computable from the demand distribution, so it also certifies, for any given instance, how far $\pi_{\widetilde S^L}$ can be from optimal. Lemma 5 gives two-sided bounds on the cost of every base-stock policy without solving for a stationary distribution of the age profile.

The paper proves Theorem 7 by sketch (§6.2: "We omit the details for brevity"), relying on the arguments for the zero-lead-time Theorems 1, 2 and 4. None of these results has a machine-checked proof. The mission's work is therefore to formalize the lead-time bookkeeping (EC.29)–(EC.33), the lower bound of Proposition 4 with its conditional-Jensen step, the convergence argument in each regime, and the omitted details of the sketch.

Difficulty

The lower bound on $\mathrm{OPT}^L$ must hold for every admissible policy, including those that use the full age profile and the pipeline, whose optimal form is unknown. The obvious route, comparing with the non-perishable backlogging system where a base-stock policy is optimal (Karlin–Scarf), gives a lower bound that ignores outdating entirely and is too weak to make the gap vanish; outdating costs incurred by an arbitrary policy have to be accounted for, and the lead time means that units outdate up to $m+L$ periods after the order that created them. The standing assumption $\theta\ge hL$ is exactly what keeps the coefficient of the outdating term in $\widetilde C^L$ nonnegative. The upper bound requires the long-run cost of $\pi_S$ although the age-profile chain need not have a stationary law that is easy to describe.

In the limits, the heuristic level $\widetilde S^L$ moves with the varying parameter. For (a), a uniform bound on $\widetilde S^L_m$ in $m$ is needed; for (b), the newsvendor level of the compound demand grows with $n$ and concentration of $N(n)$ is required (Scarf's bound and a Bernstein inequality in the zero-lead-time case); for (c), $\theta\,\mathbb E[(\widetilde S^L_\theta-\sum_{i=1}^{m+L}D_i)^+]\to0$ must be shown although the coefficient of (28) grows linearly in $\theta$.

Formalization scope

• Namespace PerishBaseStock.Backlog. Demand laws, the i.i.d. path law, the lead-time sum law and the newsvendor expectations are imported from the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.
• Time is zero-based: Lean period $t$ is the paper's period $t+1$, and the demand d t is $D_{t+1}$.
• The state is a signed vector Fin (m + L - 1) → ℝ of cumulative levels; when $m+L=1$ it is empty and $x_{t,0}:=0$.
• Base-stock levels range over $[0,\infty)$ (ℝ≥0).
• Costs live in $[0,\infty]$; expectations are lower Lebesgue integrals over the demand path law. The long-run average is a limsup of Cesàro means. $\Pi$ is the paper's class: deterministic, time-dependent, measurable functions of the current state.
• $C^L(S)$ is the simulated long-run average cost of $\pi_S$, never the formula of Lemma 5.
• "$\widetilde S^L$ is a minimizer" is a predicate, and every statement quantifies over every minimizer (over every selection of minimizers in (c)).
• Gaps are stated as $C^L(\widetilde S^L)\le\mathrm{OPT}^L+B$; in (c) as a difference of real values together with finiteness of $C^L(\widetilde S^L_\theta)$.
• The standing assumptions $m\ge1$, $h,b>0$, $\theta\ge hL$ are the predicate Params.Standing; $L\ge1$ is an explicit hypothesis of Proposition 4, (28) and Theorem 7. Proposition 4 is formalized for FIFO issuance, the only issuance rule the paper specifies for this system.
• Part (b) is posed for lifetimes $m\ge2$. The page states it for every $m\ge1$, but at $m=1$ the bound (28) does not decay in $n$ (both $\widetilde S^L_n$ and $\sum_{i=1}^{1+L}D_i$ are of order $(L+1)n\,\mathbb E[\hat D_1]$), and the Theorem 2 argument the paper invokes needs $m\ge2$ (p. 12).
• In (b), the demand of form (7) is built on a product of two independent i.i.d. sequences; $N(n)$ is $\mathbb N\cup\{\infty\}$-valued and $D(n)$ is set to $0$ on the null event where it is infinite.

Trivializing formalizations are ruled out: $\mathrm{OPT}^L$ is an infimum over all measurable state-feedback policies, not over base-stock policies; $C^L(S)$ is the long-run average of the simulated cost; neither $m$, $L$, $\theta$ nor the demand law is fixed; and no gap is stated through a truncated subtraction or an infinite $\mathrm{OPT}^L$.

A complete development needs the long-run behaviour of the base-stock dynamics, conditional Jensen for policies adapted to past demand, exponential tail bounds for sums of i.i.d. demands, and, for (b), renewal-count moments and concentration. The sample-path lemmas (EC.29)–(EC.30) and Lemma 5 are reusable for other perishable models with lead times. Proofs of any milestone and of the individual parts (a), (b), (c) are welcome.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, SSRN 3724966, 2022; Management Science. https://ssrn.com/abstract=3724966
• S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680
• S. Karlin, H. Scarf, Inventory Models of the Arrow–Harris–Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• J. F. C. Kingman, Some Inequalities for the Queue GI/G/1, Biometrika 49(3/4):315–324, 1962. https://doi.org/10.2307/2333566

Motivation

Social platforms show news articles to their users without sending them to the publisher's site. Publishers argue that this diverts readers and advertising revenue, and so weakens their incentive to invest in journalism. Several regulators have responded by requiring dominant platforms to negotiate payments with news publishers: France transposed the EU neighbouring right for press publishers in 2019, and Australia adopted the News Media Bargaining Code in 2021. Whether such negotiated payments raise or lower the quality of news is not obvious, because the payment and the publisher's traffic both depend on the quality the publisher chooses.

de Cornière and Sarvary (TSE Working Paper n° 1152, August 2021; published in Management Science, 2023, doi:10.1287/mnsc.2022.4341) study a model in which a platform bundles a publisher's content with user-generated content. In their baseline (§3–§4) the platform bundles unilaterally; this is the subject of the companion mission Social Media and News: Content Bundling and News Quality I. Section 6 replaces unilateral bundling by a negotiated agreement, and Proposition 5 compares the resulting news quality with both the no-bundling benchmark and unilateral bundling. This mission formalizes Proposition 5.

Setting

Consumers. A consumer has one unit of time. She spends $T_1$ on the publisher's site and $T_0=1-T_1$ on the platform. On the platform a share $\lambda$ of what she sees is news and $1-\lambda$ is user-generated content, so she consumes $x_N=T_1+\lambda T_0$ units of news and $x_U=(1-\lambda)T_0$ units of other content, with utility

$$U(x_U,x_N)=x_U+(1+q)x_N-\frac{x_N^2}{2},$$

where $q$ is the quality of the publisher's news.

Baseline game (unilateral bundling). The publisher chooses $q\in[0,1]$ at cost $cq^2/2$; the platform chooses $\lambda\in[0,\Lambda]$; the consumer chooses $T_1\in[0,1]$. The platform earns $R_0=(1-\lambda+\lambda\varphi_0)T_0$ and the publisher earns $R_1=\beta T_1+\varphi_1\lambda T_0$. The standing assumptions (Table 1) are $\varphi_0,\varphi_1\in(0,1)$, $\beta>\varphi_1$, $c>2\beta$, $\Lambda\in(0,1/2)$. The benchmark is the same game with $\Lambda=0$. The unilateral threshold is

$$c^\dagger=\frac{\beta+\varphi_1(1-2\Lambda)}{2\Lambda(1-\Lambda)}.$$

Negotiated game (§6). The publisher chooses $q$. Publisher and platform then agree, by Nash bargaining with equal bargaining power, on a lump-sum payment $F$ to the publisher. The platform chooses $\lambda\le\Lambda$ and keeps all advertising revenue ($\varphi_0=1$, $\varphi_1=0$). Finally the consumer allocates her time. With an agreement the publisher receives $\beta T_1+F$ and the platform $T_0-F$; if bargaining fails the outcome is the benchmark, with payoffs $\beta q$ and $1-q$. The fee maximizes the Nash product

$$\bigl(\beta T_1+F-\beta q\bigr)\bigl(T_0-F-(1-q)\bigr).$$

Section 6 assumes $1/3<\beta\le1$ and keeps $c>2\beta$ and $\Lambda\in(0,1/2)$.

In each game a subgame-perfect equilibrium requires best responses after every history: the consumer at every $(q,\lambda)$, the platform at every $q$, the fee at every $q$, and the publisher's quality optimal over $[0,1]$. In the negotiated game, a platform that is indifferent between several values of $\lambda$ chooses the smallest one (p. 19). The equilibrium qualities are written $\hat q$ (benchmark), $q^*$ (unilateral) and $\tilde q$ (negotiated).

Formalization targets

Goal: Proposition 5

Under $1/3<\beta\le1$, $\varphi_0,\varphi_1\in(0,1)$, $\varphi_1<\beta$, $c>2\beta$, $\Lambda\in(0,1/2)$, all three games have subgame-perfect equilibria, and for any equilibria of the three games

$$\beta<1\ \Longrightarrow\ \bigl(\hat q<\tilde q\iff c>\beta/\Lambda\bigr),\qquad c\neq c^\dagger\ \Longrightarrow\ \bigl(q^*<\tilde q\iff c>c^\dagger\bigr).$$

Milestones

The negotiated equilibrium is solved by backward induction, as in §6:

• the platform's choice $\lambda=\min\{q,\Lambda\}$ (p. 19);
• the fees $F_1(q)=q(1+\beta)/2$ for $q\le\Lambda$, display (4), and $F_2(q)=(1-q)(1+\beta)\Lambda/(2(1-\Lambda))$ for $q>\Lambda$, display (6);
• the publisher's stage-1 profit, display (7);
• $q_1(c)<1$ and $q_2(c)<q_1(c)$, where $q_1(c)=(1+\beta)/(2c)$ and $q_2(c)=(\beta(2-\Lambda)-\Lambda)/(2(1-\Lambda)c)$ (proof of Lemma 5);
• Lemma 5: $\tilde q=q_2(c)$, $\Lambda$ or $q_1(c)$ according as $c$ is below, inside or above $\bigl[\tfrac{\beta(2-\Lambda)-\Lambda}{2(1-\Lambda)\Lambda},\tfrac{1+\beta}{2\Lambda}\bigr]$.

The comparison uses Lemma 1 ($\hat q=\beta/c$), Lemma 4 ($q^*=q_L(c)=\varphi_1/c$ above $c^\dagger$, $q_H(c)=(\beta-\Lambda\varphi_1)/(c(1-\Lambda))$ below), and the inequality $q_2(c)<\beta/c<q_1(c)$ of the proof of Proposition 5.

Significance

Proposition 5 reverses the conclusion of the unilateral analysis. Under unilateral bundling (Proposition 1, companion mission) quality rises only when quality is cheap ($c<c^\dagger$). Under a negotiated agreement quality rises over unilateral bundling exactly when quality is costly ($c>c^\dagger$), and over the benchmark exactly when $c>\beta/\Lambda$. A bargaining mandate therefore helps news quality for publishers whose content is mostly consumed through the platform, which is the case that motivates the Australian and French policies.

The result is proved in the paper; the proof of part 2 is a one-sentence case sketch over the position of $c^\dagger$ relative to the two thresholds of Lemma 5. No machine-checked version exists. A formal proof checks the case analysis, including the knife-edge cases $c=c^\dagger$ and $\beta=1$, which the printed statement does not treat, and produces a reusable formal model of Nash bargaining inside a multi-stage game.

Difficulty

The closed forms are elementary; the content lies in the equilibrium objects. Each equilibrium concept quantifies over strategies at every history, so every closed form must be derived, not assumed: the consumer's split from utility maximization, the platform's share from the revenue comparison and the tie-break, the fee from maximizing the Nash product, and the quality from a piecewise objective whose two pieces meet at $q=\Lambda$. The comparison in part 2 then crosses two different games, whose thresholds $c^\dagger$ and $\bigl[\tfrac{\beta(2-\Lambda)-\Lambda}{2(1-\Lambda)\Lambda},\tfrac{1+\beta}{2\Lambda}\bigr]$ can be ordered in several ways, and the equivalence must hold in every ordering. Reading the closed forms off the paper and comparing them does not prove anything about the games.

Formalization scope

All objects are real-valued. Quality ranges over $[0,1]$, since demand for news equals $q$ and the paper notes the profit expression is valid only for $q\le1$. A strategy profile is a record of functions: the consumer's time $T_1(q,\lambda)$, the platform's share $\lambda(q)$, in the negotiated game the fee $F(q)$, and a quality. The fee maximizes the Nash product over all $F\in\mathbb R$; the agreement and disagreement payoffs are those printed on p. 19. The negotiated platform minimizes $\lambda$ among its maximizers, as printed. The benchmark is the baseline game at $\Lambda=0$, and the unilateral game keeps Table 1's $\varphi_0,\varphi_1$; footnote 16's $\varphi_0=1$, $\varphi_1=0$ apply to the negotiated game only.

Two hypotheses are added to the printed statement, both disclosed in the goal's statement:

1. part 1 is posed for $\beta<1$, because at $\beta=1$ the negotiated quality equals the benchmark quality $\beta/c$ whenever $c>(1+\beta)/(2\Lambda)$;
2. part 2 is posed for $c\ne c^\dagger$, because at $c=c^\dagger$ the unilateral game has two equilibrium qualities and the negotiated quality lies strictly between them.

Trivializing formalizations are ruled out. Equilibrium strategies are never given by their closed forms. Best responses are required after every history, not only on the path. The fee is never defined as $F_1$ or $F_2$. The benchmark is an equilibrium of the game at $\Lambda=0$, not the number $\beta/c$. The goal and Lemma 5 assert existence of equilibria, so the "for every equilibrium" clauses are not vacuous.

The definitions (NewsBundling.Negotiated.Setting) import the baseline game from the shared module NewsBundling.Unilateral.Setting and define the negotiated game. A proof needs elementary real analysis: maxima of concave quadratics, piecewise functions on $[0,1]$, and the existence of maximizers. Proofs of any milestone are welcome, as are proofs of Lemmas 1 and 4 shared with the companion mission.

Selected references

• A. de Cornière and M. Sarvary, Social Media and News: Content Bundling and News Quality, Toulouse School of Economics Working Paper n° 1152, August 2021 (the version this mission cites); journal version below.
• A. de Cornière and M. Sarvary, Social Media and News: Content Bundling and News Quality, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4341
• J. F. Nash, The Bargaining Problem, Econometrica 18(2), 1950. https://doi.org/10.2307/1907266

Motivation

Blood platelets, fresh produce, bakery items and many pharmaceuticals have a fixed lifetime: a unit that is not used within $m$ periods of arrival must be discarded. Replenishing such a product is a classical problem of inventory theory (Nahmias 1982), and its optimal policy depends on the whole age profile of the stock, so it cannot be computed for realistic lifetimes. Practice therefore relies on base-stock policies, which raise total stock to a fixed level every period.

Bu, Gong and Chao give the first theoretical guarantees for such a policy. Under first-in-first-out (FIFO) issuance they choose the level $\widetilde S$ by minimizing an explicit surrogate of the long-run cost and show that its optimality gap vanishes in four regimes. This mission is the fourth: a large unit outdating cost $\theta$. The regime matters in practice because outdating is expensive. Slonim et al. (2014) put the component cost of a unit of blood sold to U.S. hospitals at about $570, and disposing of expired products often requires costly handling.

Setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a non-negative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F$. The product lives $m\ge1$ periods. At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$, where $x_{t,i}$ is the stock with remaining lifetime at most $i$. The firm orders $q_t\ge0$, raising the total stock to $x_{t,m}=x_{t,m-1}+q_t$ (lead time zero). Demand is served oldest first and unmet demand is lost. The quantity $o_t=(x_{t,1}-D_t)^+$ outdates, and the state evolves by

$$x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1.$$

The system starts empty. The period cost is

$$C^\pi_t=h(x^\pi_{t,m}-D_t)^+ + p(D_t-x^\pi_{t,m})^+ + \theta o^\pi_t,$$

with holding cost $h>0$, lost-sales penalty $p>0$ and outdating cost $\theta\ge0$.

A policy is admissible if each period's order is a non-negative measurable function of the current state. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$, and $\mathrm{OPT}_\theta$ is the infimum of $C^\pi$ over admissible policies. The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$, and $C_\theta(S)$ is its long-run average cost. The heuristic level $\widetilde S_\theta$ is any minimizer over $[0,\infty)$ of

$$\widetilde C_\theta(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac\theta m\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big].$$

The lower support of demand is $\underline D=\inf\{x:F(x)>0\}$.

Formalization targets

Goal: Theorem 4 (p. 14)

$$\lim_{\theta\to\infty}\big(C_\theta(\widetilde S_\theta)-\mathrm{OPT}_\theta\big)=0,$$

for every selection $\theta\mapsto\widetilde S_\theta$ of minimizers, with $h$, $p$, $m$ and the demand law fixed. The statement holds for every demand law, whether $\underline D$ is zero or positive.

Milestones (Appendix B.3 and §6.2)

1. (EC.16): for every $\theta\ge0$, $\widetilde C_\theta(\widetilde S_\theta)\le\min_{0\le S\le m\underline D}\widetilde C_\theta(S)=\min_{0\le S\le m\underline D}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]\}$.
2. $S^0=m\underline D$: $\sup\{S\ge0:\mathbb E[(S-\sum_{i=1}^mD_i)^+]=0\}=m\underline D$.
3. (EC.17): for the least minimizers, $\widetilde S_\infty=\lim_\theta\widetilde S_\theta$ exists, the newsvendor cost of $\widetilde S_\theta$ converges to that of $\widetilde S_\infty$, and the limit is at least $\min_{0\le S\le m\underline D}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]\}$.
4. (24): $\lim_{\theta\to\infty}\theta\,\mathbb E[(\widetilde S_\theta-\sum_{i=1}^mD_i)^+]=0$ for every selection of minimizers.

The goal's proof also uses inequality (21), $C(\widetilde S)-\mathrm{OPT}\le\frac{(m-1)\theta}{m}\mathbb E[(\widetilde S-\sum_{i=1}^mD_i)^+]$. That inequality, together with Lemmas 1–2 and Proposition 2 behind it, is posed in mission 1 of this series and is not restated here.

Significance

Theorem 4 says that when outdating is expensive, a policy computed from a one-dimensional convex function is as good as the optimal age-dependent policy. A base-stock policy does not need to track the age distribution, and its level can be found by simulation and golden-section search between explicit bounds. Together with Theorems 1–3 it shows that $\widetilde S$ is asymptotically optimal in all four regimes of the paper. Remark 2 of the paper notes that the plain newsvendor level $S^{NP}$ fails in this regime.

The result is proved in the paper (Management Science, 2022). It has not been formalized. This mission adds a machine-checked model of the FIFO perishable system with lost sales: the age-structured dynamics, admissible policies, long-run average costs and the optimal cost over all policies. The model is reusable for the other missions of the series and for the wider perishable-inventory literature. The paper's proof leaves several steps to the reader: the monotonicity of $\widetilde S_\theta$, the identity $S^0=m\underline D$, and continuity of the newsvendor cost. Each of these becomes an explicit statement.

Difficulty

The obvious argument compares the heuristic with an optimal policy directly. That fails because the optimal policy has no tractable form. The proof instead goes through (21), a lower bound on $\mathrm{OPT}$ obtained by a sample-path argument, and then has to show that the outdating term of the heuristic level vanishes faster than $\theta$ grows. That needs uniform control of $\widetilde S_\theta$ as $\theta\to\infty$. The level must eventually fall into $[0,m\underline D]$, where no stock survives $m$ periods of demand, and the newsvendor cost there must match the restricted minimum. A naive reading of "$\widetilde S_\theta$ decreases in $\theta$" holds only for the least minimizer. For an arbitrary selection, the argument has to work through the bound (EC.16) alone.

Formalization scope

• Lean 4 with Mathlib. Everything sits in the namespace PerishBaseStock.Outdating and builds on the published demand layer CappedBaseStock_Model (i.i.d. demand path, demand law with $0<\mathbb E[D]<\infty$) and the newsvendor functions of LostSalesOrderUpTo.Asymptotic.Backorder.
• Time is zero-based: Lean period $t$ is the paper's period $t+1$. The state is Fin (m - 1) → ℝ≥0 of cumulative levels, with $x_{t,0}=0$. When $m=1$ the state is empty and everything left over outdates. Levels $S$ range over $\mathbb R_{\ge0}$.
• Costs take values in $[0,\infty]$. Expectations of costs are lower Lebesgue integrals over the demand-path law, and $C^\pi$ is the limsup of Cesàro averages. $\mathrm{OPT}_\theta$ is the infimum over all admissible policies: time-dependent measurable functions of the state, as in the paper.
• $C_\theta(S)$ is the limsup average of the simulated cost of $\pi_S$, never a closed form.
• $\theta$ ranges over $\mathbb R_{\ge0}$, and limits are taken along atTop there. The goal asserts that $C_\theta(\widetilde S_\theta)$ is finite and that the difference of real values tends to $0$, so no $\infty-\infty$ convention enters.
• "A minimizer" means every minimizer. (EC.17) is posed for the least minimizer, the selection for which the paper's monotonicity claim holds.
• $\underline D$, $S^0$ and the restricted minimum are real infima and suprema over nonempty, bounded sets, so Lean's default values never arise.
• The model must not be trivialized: a fixed $m$, $\theta=0$, a restriction of $\mathrm{OPT}$ to base-stock policies, or $\widetilde S_\theta$ replaced by a closed form would each change the theorem, and none is used.
• Welcome contributions: proofs of the milestones, continuity and coercivity of the newsvendor and heuristic costs, monotone comparative statics of $\arg\min$ in $\theta$, and the sample-path lemmas of mission 1.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022 (accepted manuscript, SSRN 3724966). https://ssrn.com/abstract=3724966
• S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 1982. https://doi.org/10.1287/opre.30.4.680
• W. L. Cooper, Pathwise properties and performance bounds for a perishable inventory system, Operations Research 49(3), 2001. https://doi.org/10.1287/opre.49.3.455.11214
• A. W. Chazan, S. Gal, A Markovian model for a perishable product inventory, Management Science 23(5), 1977. https://doi.org/10.1287/mnsc.23.5.512
• R. Slonim, C. Wang, E. Garbarino, The market for blood, Journal of Economic Perspectives 28(2), 2014. https://doi.org/10.1257/jep.28.2.177

Motivation

Carbon pricing changes both a manufacturer's production decisions and its incentive to invest in cleaner technology. A carbon tax fixes the price of emissions in advance. Cap-and-trade fixes an emissions quota while the price of permits changes with market conditions. The comparison is especially sensitive to whether high product demand tends to coincide with a high permit price. Fan, Chen, and Chen study that interaction for a firm that chooses its technology before learning demand and then adjusts production after uncertainty is resolved. Their preprint finds that the preferred policy can change as demand and permit prices become more correlated. This mission concerns the paper's base model and its comparisons of consumer surplus and emissions.

Setting

A monopolist sells quantity $q$ at the inverse demand price $a-bq$, where $b>0$ is demand sensitivity and the random variable $a$ is market potential. A unit of output emits $\gamma$ units of carbon. Before observing market conditions, the firm chooses $\gamma\in[0,\gamma^+]$ by paying the technology investment cost $\beta(\gamma^+-\gamma)^2$. After observing demand and, under cap-and-trade, the permit price $k$, it chooses $q$. The operating profit is

$$\pi(q;\gamma,a,k)=(a-bq)q-(\gamma q-w)k, \qquad q^*(\gamma,a,k)=\frac{a-\gamma k}{2b}.$$

Here $w$ is the assigned emissions quota. If emissions are below $w$, the permit term is a receipt from selling unused permits. The carbon tax sets the carbon price to the mean permit price $\bar k$. Its term $w\bar k$ is the paper's lump-sum green subsidy, so the same $w$ appears in both regimes. Under cap-and-trade, $k$ remains random. These definitions follow §3 and equations (1)–(3) of the source preprint.

Let $\bar a$ and $\bar k$ be the means of $a$ and $k$, let $\sigma_D$ and $\sigma$ be their standard deviations, and let $\rho$ be their correlation. The first-stage objectives $\Pi_T(\gamma)$ and $\Pi_C(\gamma)$ are expected operating profit under the tax and cap-and-trade, respectively, less the investment cost. Their maximizers on $[0,\gamma^+]$ are denoted $\gamma_T^*$ and $\gamma_C^*$. Expected consumer surplus is the expected value of $b(q^*)^2/2$ in each regime, denoted $CS_T$ and $CS_C$. Expected emissions are the expected values of $\gamma_T^*q_T^*$ and $\gamma_C^*q_C^*$, denoted $S_T$ and $S_C$. The welfare quantities are those of equations (8)–(9) in the preprint.

The paper's Assumption 1 requires sufficiently high investment cost, expressed by $4b\beta>\bar k^2+\sigma^2$ and $4b\beta\gamma^+>\max\{\bar a\bar k,\bar a\bar k+\rho\sigma_D\sigma\}$, together with $a>\gamma^+k$ for realized demand and permit price. The comparison uses thresholds $R_0=(\sigma/\sigma_D)\gamma_T^*$ and $R$, with $0<R<R_0$. The latter is specified by the piecewise formulas for $\rho_0$ and $\rho_1$ in Proposition 2(a) of the preprint.

Formalization targets

The target is Corollary 1(a)–(b), on pages 19–20 of the preprint. Its consumer-surplus part asserts the existence of two thresholds, $R_1<R<R_0<R_2$, such that

$$CS_T>CS_C\quad\Longleftrightarrow\quad R_1<\rho<R_2.$$

The thresholds depend on the fixed model parameters and moments, and the comparison holds for every admissible joint distribution with those moments. The emissions part compares $S_T$ and $S_C$ on each side of $R_0$. For $\rho<R_0$, it says $S_T<S_C$ when $\gamma_T^*+\gamma_C^*<\bar a/\bar k$, and $S_T\ge S_C$ otherwise. For $\rho>R_0$, the strict comparison reverses and the other case becomes $S_T\le S_C$. The printed corollary leaves $\rho=R_0$ outside these two cases.

The supporting targets follow the source's attack path: the second-stage quantity in equation (1), the expected-profit moment forms in the proofs of Lemmas 1–2, the unique optimal emission intensities in Lemmas 1–2, the investment and profit comparisons in Propositions 1(a) and 2(a), and the consumer-surplus and emissions identities in the proof of Corollary 1.

Significance

The corollary separates two outcomes that a carbon policy can affect in different ways. It specifies when the tax yields higher expected consumer surplus and when it yields lower expected emissions, rather than inferring either outcome from the firm's profit alone. In the interval between $R$ and $R_0$, the source also identifies stronger clean-technology investment and higher firm profit under the tax. Its policy comparison can therefore be applied only after identifying the relevant correlation and the position of the optimal intensities relative to $\bar a/\bar k$.

The paper proves the result analytically. This formalization records its base model, expectation identities, and threshold comparisons as Lean statements. The goal and milestone proofs remain to be machine checked. A completed development would make the probabilistic moment calculations and the piecewise threshold reasoning reusable for other two-stage production models with correlated prices and demand.

Difficulty

The correlation changes the cap-and-trade investment choice, and that choice can reach the boundary $\gamma^+$. Consequently, the consumer-surplus comparison changes algebraic form across the boundary. The proof of Corollary 1 describes the surplus difference as a quadratic in $\rho$; this description applies to the interior branch, while the boundary branch is linear. The formal target is the full interval assertion across both branches. The threshold $\rho_0$ also solves a quadratic equation with two roots; the relevant one is the smaller root in the domain allowed by Assumption 1.

Formalization scope

Lean represents $a$ and $k$ as real random variables on a probability space, with $L^2$ hypotheses so every quadratic expectation is integrable. Their means are integrals, their standard deviations are square roots of variance, and $\rho$ is covariance divided by $\sigma_D\sigma$. The standing conditions are $b>0$, $\gamma^+>0$, $\bar k>0$, $\sigma_D>0$, and $\sigma>0$; $w$ is unrestricted. The paper's realized-demand clause is interpreted almost surely. These conditions keep the divisions in the formulas meaningful and state the paper's positive-price and nondegenerate-uncertainty conventions. The parameter-level conditions in the uniform consumer-surplus claim include the correlation-free consequences of Assumption 1.

Optimal intensities are maximizers of the expectation-based objectives on $[0,\gamma^+]$. The comparison statements quantify over arbitrary maximizers; the closed forms are established separately. The surplus thresholds $R_1,R_2$ are selected before quantifying over probability models with the fixed moments. This prevents them from depending on a particular realized correlation. Lean names $\gamma^+$ as γp and defines $\rho_0$ using the smaller-root condition; its fallback value outside that condition is not used under the theorem hypotheses.

The scope is the base model with advance technology investment and full production flexibility in §§3–5. The case studies of §6 and the modified models of §7 and the Online Appendices A–B are outside this mission. Useful supporting work includes identities for expectations of products of $L^2$ variables, strict concavity and uniqueness of the first-stage maximizers, and the piecewise correlation thresholds.

Selected references

• X. Fan, K. Chen, and Y.-J. Chen, Is Price Commitment a Better Solution to Control Carbon Emissions and Promote Technology Investment?, SSRN preprint 3817235, version of November 15, 2021; published in Management Science, 2022. Preprint. DOI.