Operations Research

Why changing environments matter

A reinforcement-learning agent chooses actions while learning how those actions affect future states. In a stationary model, observations collected long ago remain relevant to the current transition law. In a nonstationary Markov decision process, rewards and transition probabilities may change at each round. Old observations can then bias an estimate even when the agent has collected many samples. The challenge is to keep learning from recent observations without becoming blind to actions that the agent has not tried recently. Cheung, Simchi-Levi and Zhu study this tension for finite-state average-reward learning and introduce confidence widening in their SWUCRL2-CW algorithm Cheung et al., §4.

The paper's broad regret theorems suppress constants inside asymptotic notation. Proposition 2 gives an explicit one-round inequality that exposes the roles of estimation error, temporal variation, confidence widening, and the diameter of a plausible transition model. This mission targets that proposition and the stated auxiliary results used around it Cheung et al., pp. 14, 38–41.

The finite changing MDP

Let $\mathcal S$ be a finite state set. Each state $s$ has a nonempty finite set $\mathcal A_s$ of permitted actions. At round $t$, taking action $a\in\mathcal A_s$ in state $s$ gives expected reward $r_t(s,a)\in[0,1]$ and moves to state $s'$ with probability $p_t(s'\mid s,a)$. The one-step variation $B_{r,t}$ is the greatest change $|r_{t+1}(s,a)-r_t(s,a)|$ over permitted pairs; $B_{p,t}$ is the corresponding greatest $\ell_1$ distance between transition rows. These definitions make no stationarity assumption Cheung et al., pp. 6, 33.

At the start $\tau(m)$ of an episode, the algorithm counts visits to each pair in a recent window of length $W$. It divides empirical sums by $N^+=\max\{1,N\}$, where $N$ is the visit count. Thus an unvisited pair has estimated reward and transition vector equal to zero. Reward confidence sets lie in $[0,1]$; transition confidence sets lie in the probability simplex and use an $\ell_1$ radius enlarged by a nonnegative parameter $\eta$. Write $\operatorname{rad}_{r,\tau(m)}(s,a)$ and $\operatorname{rad}_{p,\tau(m)}(s,a)$ for their respective radii. The algorithm chooses a stationary policy $\tilde\pi_{\tau(m)}$ and an optimistic model, gain $\tilde\rho_{\tau(m)}$, and bias $\tilde\gamma_{\tau(m)}$ from extended value iteration Cheung et al., pp. 11–13.

The diameter of a transition model is the largest, over ordered source and target states, of the smallest expected number of transitions needed to reach the target under a stationary policy. Source equal to target means a return time after at least one transition. The round-$t$ optimal gain $\rho_t^*$ is the value of the stationary occupancy-measure linear program for $(r_t,p_t)$ with only permitted actions. From the window's first round through the round before $t$, let $\operatorname{var}_{r,t}$ and $\operatorname{var}_{p,t}$ be the sums of the corresponding one-step variations Cheung et al., pp. 8, 14, 33.

Formalization targets

The main target is Proposition 2. Condition on the local reward and transition estimation events at $\tau(m)$. Assume that the widened transition confidence sets contain every permitted row of an MDP of diameter at most $D$. For a round in which $a_t=\tilde\pi_{\tau(m)}(s_t)$, the target is

$$\begin{aligned} \rho_t^*-r_t(s_t,a_t)\le{}&\sum_{s'}p_t(s'\mid s_t,a_t)\tilde\gamma_{\tau(m)}(s')-\tilde\gamma_{\tau(m)}(s_t)+\frac1{\sqrt{\tau(m)}}\\ &+2\operatorname{var}_{r,t}+4D(\operatorname{var}_{p,t}+\eta)\\ &+2\operatorname{rad}_{r,\tau(m)}(s_t,a_t)+4D\operatorname{rad}_{p,\tau(m)}(s_t,a_t). \end{aligned}$$

The five milestones are the paper's Lemmas 2–5 and displayed inequality (32): a dual-bias span bound, a drift estimate for window averages, bounded optimistic bias, optimism under drift, and a transition-value error bound. Their exact constants are part of the targets Cheung et al., pp. 33, 38–39.

What the result supplies

Proposition 2 separates the per-round change in optimal gain from the cost of the current action. Its first term tracks changes in the optimistic bias along transitions; the other terms identify window drift, reward and transition estimation, and widening. This decomposition can be summed across episodes when analyzing the algorithm. The result has a concrete role even though the later horizon-wide theorem is given in asymptotic notation Cheung et al., pp. 14, 41.

The paper proves these claims mathematically. The mission asks for machine-checked proofs of the explicit statements and for reusable definitions of finite nonstationary MDP variation, window estimators, confidence sets, occupancy gain, and hitting-time diameter. The source's Theorems 1–4 are not posed here: their displayed bounds hide constants in $\widetilde O(\cdot)$ and, in one case, use an unspecified $O(\delta)$ failure probability Cheung et al., pp. 14–25. This proposal supplies statements for solvers; it does not claim that these new statements already have machine-checked proofs.

Where the difficulty lies

The current model need not resemble the model that generated every observation in the window. A direct stationary confidence argument cannot control the resulting temporal error. The challenge is especially visible at a pair with no recent visits: its comparison transition vector is zero, although a genuine transition row has total mass one. The paper's Lemma 3, read literally for every pair, fails in that case. The mission states its positive-count condition explicitly while keeping the proposition and the later optimism and transition milestones valid at unvisited pairs Cheung et al., pp. 12, 38–40.

There is a separate issue with the printed dual-bias lemma. Feasibility alone permits an arbitrarily large dual gain and does not force the asserted $2D$ span bound. The mission adds $\rho\le2$ to Lemma 2 and records the change for audit. The EVI output is represented by its selected-model membership, bias normalization, optimism, and near-optimality properties; this is the contract stated for the algorithm's output, rather than a formal execution of extended value iteration Cheung et al., pp. 13, 33, 35–36.

Formalization scope

States and ambient actions are Fin S and Fin A; permitted actions are state-dependent finite subsets. The setup has $S>1$, $0<\delta<1$, $\eta\ge0$, and a nonempty action set at each state. Time is zero-based in Lean, while the paper's rounds are one-based; in particular its $1/\sqrt{\tau(m)}$ is represented by $1/\sqrt{\tau_m+1}$. Counts and confidence sets are evaluated at the episode start. Variations continue up to the target round. The estimation events are assumed at the episode start, which is the only time used by these statements.

Hitting times and diameter take values in extended nonnegative reals, so an unreachable target does not acquire a false finite diameter. The diameter includes return times and minimizes over deterministic stationary policies. The confidence-radius product $SA$ counts actual permitted pairs. At an unvisited pair, the comparison averages remain zero and $N^+=1$; the large confidence radii under the stated bounds are essential. The local transition event uses the $\ell_1$ error condition: literal membership of the zero comparison vector in a simplex would make the paper's event fail. The printed coordinatewise maxima in Property 1 imply the standard joint-distribution optimism condition used here. The free $(s,a)$ printed in the last radius of Proposition 2 means $(s_t,a_t)$, as the proof's context confirms Cheung et al., pp. 12, 14, 36, 40–41.

Two milestones carry a pinned hypothesis because the printed statement is false without it: Lemma 2 assumes the dual gain satisfies $\rho\le 2$ (an arbitrary feasible $\rho$ can make the bias span exceed $2D$), and Lemma 3 assumes the pair was visited in the episode-start window (at an unvisited pair the comparison averages are zero). Proposition 2 is stated for every round $t\ge\tau(m)$ before the horizon at which the action is the episode policy's choice, which covers the rounds of episode $m$; the coefficient $4D$ of $\eta$ is kept as printed.

The witness MDP has genuine probability rows in the widened sets and a diameter bound. The EVI tuple obeys both stated properties, and the chosen action obeys its policy. These conditions prevent an unconstrained bias, a spurious zero diameter, a confidence event at the wrong time, or a reward bound for an unrelated action. The published FiniteMDPLearning model supplies probability rows and rewards in $[0,1]$; its different travel-time convention is not substituted for the paper's diameter. Contributions to the MDP linear program, finite-state hitting times, window-average inequalities, and confidence-region geometry are all useful beyond this mission.

Selected references

• W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. Preprint; journal DOI.
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. Article.

Motivation

Reinforcement learning in a changing environment needs a benchmark that remains meaningful when the transition law and rewards vary from round to round. For a stationary Markov decision process (MDP), the optimal long-run average reward is a standard benchmark. In a nonstationary MDP, summing those stationary optima across rounds is convenient, but it need not equal the best expected reward achievable over the whole horizon: today's action changes tomorrow's state. Cheung, Simchi-Levi and Zhu use Proposition 1 to quantify this gap in their analysis of nonstationary reinforcement learning (preprint, pp. 7–8). This mission formalizes that proposition and the explicit estimates in its proof.

The paper develops algorithms for MDPs with drifting rewards and transitions. Its oracle comparison is useful before any algorithm is chosen: it relates a sum of local, stationary benchmarks to the reward of every non-anticipatory policy, including policies that adapt to the observed trajectory. This separates a property of the environment from the performance of a learning rule. The paper was published in Management Science in 2023; this mission follows the numbered statements and pages of the authors' pinned arXiv preprint (Cheung et al., 2020, pp. 6–8).

Setting

A finite nonstationary MDP has a finite state set $\mathcal S$, a nonempty available-action set $\mathcal A_s$ at each state $s$, and a horizon of $T$ rounds. At round $t$, taking action $a\in\mathcal A_s$ in state $s$ gives a stochastic reward with mean $r_t(s,a)\in[0,1]$ and moves to a new state according to the probability distribution $p_t(\cdot\mid s,a)$. A non-anticipatory policy selects an allowed action using the current state and observations from previous rounds. The target concerns expected sums of the mean rewards, so the distributional shape of the reward noise does not enter its formula (preprint, §2.2, pp. 6–7).

The one-step reward variation $B_{r,t}$ is the largest value of $|r_{t+1}(s,a)-r_t(s,a)|$ over allowed state–action pairs. The transition variation $B_{p,t}$ is the largest $\ell_1$ distance between the corresponding transition distributions. Their variation budgets are $B_r=\sum_{t=1}^{T-1}B_{r,t}$ and $B_p=\sum_{t=1}^{T-1}B_{p,t}$, exactly as in equation (1). The budgets are computed from the MDP sequence; they are not independent inputs to the theorem (preprint, p. 6, (1)).

For the stationary MDP at round $t$, $\rho_t^*$ is its optimal long-run average reward. The mission represents it as the optimum of the paper's occupancy linear program (15), whose variables are nonnegative state–action occupancies, satisfy flow balance, and sum to one. A diameter $D_t$ bounds the least expected hitting time between any two states under an allowed stationary policy. The paper's Definition 1 includes equal initial and target states, so this includes a return time. Assumption 1 requires a finite diameter at every round; $D_{\max}$ is a common bound on those diameters (preprint, pp. 7–8, Definition 1 and Assumption 1; p. 33, (15)).

Formalization targets

Proposition 1: the oracle gap

Write $B=B_r+2D_{\max}B_p$. For $0<B\le T$ and the necessary small-budget condition $BT\ge1$, the target is

$$\sum_{t=1}^{T}\rho_t^*\ge \mathbb E^{\Pi}\!\left[\sum_{t=1}^{T}r_t(s_t,a_t)\right] -4(D_{\max}+1)\sqrt{BT}$$

for every initial state and every allowed non-anticipatory policy $\Pi$. Quantifying over every policy expresses the paper's maximum over policies without introducing a supremum over an unbounded real-valued function space. The first five targets follow Appendix A.2: a bounded optimal dual potential, the gain-drift inequality (18), the pathwise dual inequality (19), the window inequality (23), and the full-horizon inequality (24). Their constants and index ranges are part of the targets (preprint, pp. 8, 33–34).

Significance

The result gives a finite-horizon comparison between two different benchmarks. The sum of stationary gains is additive over time, while the best expected cumulative reward accounts for how actions alter later states. Proposition 1 says that their difference is controlled by variation and diameter under its hypotheses. This is the paper's justification for using the additive oracle in its dynamic-regret definition; the authors note that the later algorithmic bounds are larger than this comparison term (preprint, p. 8, text after Proposition 1).

The mathematical result is already claimed in the paper. This mission asks for a machine-checked version with explicit finite-horizon distributions, the occupancy LP, the diameter convention, and the drift sums. The new Lean statements currently have placeholders for their proofs; the imported finite-MDP definitions are already published. A completed development would provide reusable code for time-dependent MDP trajectory laws and for comparing stationary LP values as a model drifts. It would also make the precise domain of the square-root bound reviewable independently of the algorithms in the remainder of the paper.

Difficulty

The stationary gain $\rho_t^*$ is not a per-round reward guarantee. An action can collect reward now and put the process in a state whose future reward is poor, so summing stationary optima does not directly bound a nonstationary trajectory. Conversely, treating each round as an independent stationary experiment discards the state dependence that the policy exploits. The diameter controls the cost of that dependence, and variation controls changes between the stationary problems. The proof must connect these objects while preserving the exact factors $2D_{\max}$, $2W$, and $4TD_{\max}/W$ in Appendix A.2 (preprint, pp. 33–35).

There is also a small-budget obstruction in the printed Proposition 1. Its stated $0<B\le T$ permits $BT<1$, where the displayed inequality is false: a two-state, one-action example with a slowly returning state, $T=2$, and reward drift $10^{-12}$ has an oracle sum near $2/11$ while the proposed lower bound on that sum is near $1$. The mission therefore adds $BT\ge1$ and records the difference from the page. Inequality (24), posed separately, retains the paper's every-integer-window form and needs no such pin.

Formalization scope

States and actions are Fin S and Fin A; available actions form a nonempty Finset at each state, and $S>0$. The imported FiniteMDPLearning structure supplies reward rows in $[0,1]$ and transition probability rows. It has rows for actions unavailable at a particular state; all mathematical maxima, LP constraints, policy restrictions, and drift formulas use only allowed pairs. The source's time $t\in\{1,\ldots,T\}$ is stored at Lean index $t-1$. No value of the MDP sequence after the horizon enters a stated budget or reward sum.

The occupancy LP has a nonempty bounded feasible-value set under the standing MDP assumptions; its real supremum denotes $\rho^*$. Hitting times and diameters use extended nonnegative reals to retain infinity, rather than silently converting an infinite hitting time to zero. The diameter includes same-state return times and minimizes over deterministic stationary policies; such policies attain the hitting-time minimum. The policy used for cumulative reward is a history-dependent randomized kernel on state–action histories. Conditioning an action rule that also observes past rewards on that history yields the same state–action trajectory law. The nonstationary measure samples the next state with the current round's transition law and is a probability measure.

The fixed $D_{\max}$ is constrained to bound every round's diameter; it is not an unrelated parameter. The stated $BT\ge1$ pin rules out the false small-budget case. In (23), the paper's last-window drift sum includes $B_{\cdot,T}$, which equation (1) does not define; the formal sum retains all defined terms through $T-1$. The goal and milestones do not weaken $\rho_t^*$, restrict the policy class to a convenient subclass, or omit a time step. Contributions on LP duality, finite-horizon trajectory expectations, hitting-time bounds, and drift inequalities are useful beyond this proposition. The paper's headline Theorems 1–4 are not posed here because their $\widetilde O$ notation hides constants (preprint, p. 6, §2.1).

Selected references

• W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. Preprint; published article.
• T. Jaksch, R. Ortner and P. Auer, Near-Optimal Regret Bounds for Reinforcement Learning, Journal of Machine Learning Research 11, 2010. Article. The source paper cites its diameter and bias-span results in Definition 1 and Appendix A.1.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. Book. The source paper cites it for the average-reward occupancy LP on p. 33.

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