Operations Research

Motivation

Patrolling protects a border or facility perimeter against an intruder who needs uninterrupted time to complete an attack. The defender controls when patrollers pass; the attacker controls when to strike. In a patrol game, the question is how to time patrols when the attacker can observe them (Lin, Optimal Patrol of a Perimeter).

An observing attacker can wait until a patroller has passed before starting. Lin's result shows that a randomised schedule still gives the defender the same optimal detection probability as against a blind attacker, in closed form.

Setting

Fix three parameters: a dispatch rate $\lambda > 0$, an attack duration $t > 0$ and a detection probability $p \in (0, 1]$.

Defender. A pure strategy is a nondecreasing sequence of times $s_1 \le s_2 \le \cdots$ in $[0, \infty)$ at which patrollers pass a fixed location. With $N(T) = \#\{n : s_n \le T\}$ the number of patrollers dispatched by time $T$, the sequence is feasible if it satisfies condition (1) of the paper,

$$\lim_{T \to \infty} \frac{N(T)}{T} = \lambda .$$

A mixed strategy is a probability measure $\mu$ on sequences under which almost every sequence is feasible.

Attacker. The attacker chooses an operating window $[y, z]$ with $0 < y < z$, watches the patrollers go by, and at a time $\tau$ of his choosing starts an attack that occupies $(\tau, \tau + t]$ and must end by $z$. The choice of $\tau$ may depend on everything observed up to and including time $\tau$: it is a stopping time of the arrival process.

Payoff. Each patroller passing during the attack detects it independently with probability $p$. If the attack meets $N$ patrollers it escapes with probability $(1 - p)^N$, so the detection probability of $\tau$ against $\mu$ is

$$P_{\mathrm{det}}(\mu, \tau) = E_\mu\bigl[1 - (1 - p)^{N(\tau, \tau + t]}\bigr].$$

The defender moves first and maximises; the attacker responds and minimises. This Stackelberg game is $\Gamma(\lambda, t, p)$. Its value is (2):

$$V(\lambda, t, p) = 1 - (\lambda t - \lfloor \lambda t \rfloor)(1 - p)^{\lceil \lambda t \rceil} - (1 - \lambda t + \lfloor \lambda t \rfloor)(1 - p)^{\lfloor \lambda t \rfloor}.$$

The claimed optimal schedule $\mu^*$ puts blue patrollers deterministically at $jt + k\Delta$, with $\Delta = t / \lceil \lambda t \rceil$, $j = 0, 1, 2, \dots$ and $k = 1, \dots, \lfloor \lambda t \rfloor$. It puts a red patroller at each $jt$ independently with probability $\lambda t - \lfloor \lambda t \rfloor$. When $\lambda t$ is an integer there are no red patrollers, and the blue ones pass at fixed intervals of $1/\lambda$.

Formalization targets

Goal: Theorem 2

For all $\lambda > 0$, $t > 0$, $p \in (0, 1]$:

1. $\mu^*$ is a feasible mixed strategy;
2. $\displaystyle \inf_{\tau} P_{\mathrm{det}}(\mu^*, \tau) \ge V(\lambda, t, p)$ over all attacks $\tau$;
3. for every feasible mixed strategy $\mu$ and $\varepsilon > 0$ there is an attack $\tau$ with $P_{\mathrm{det}}(\mu, \tau) < V(\lambda, t, p) + \varepsilon$;
4. $V$ is nondecreasing in $\lambda$, in $t$ and in $p$.

Items 2 and 3 state $\sup_\mu \inf_\tau P_{\mathrm{det}}(\mu, \tau) = V(\lambda, t, p)$, attained at $\mu^*$.

Milestones

• Lemma 1 (p. 5). Among laws on $\{0, 1, 2, \dots\}$ with mean $c > 0$, the detection probability $1 - E[(1 - p)^N]$ is at most $V$ with $\lambda t$ replaced by $c$, and the least-variance law on $\{\lfloor c \rfloor, \lceil c \rceil\}$ attains it.
• Window counting (p. 7). Every window $(a, a + t]$ with $a \ge 0$ contains exactly $\lfloor \lambda t \rfloor$ blue time points and exactly one red slot.
• Feasibility (p. 7, with (1)). $\mu^*$ is a feasible mixed strategy.
• Guarantee (p. 7). $P_{\mathrm{det}}(\mu^*, \tau) = V(\lambda, t, p)$ for every attack $\tau$.
• Converse (pp. 7–8). For every feasible $\mu$ and $\varepsilon > 0$ some deterministic start time $y > 0$ has $P_{\mathrm{det}}(\mu, y) < V(\lambda, t, p) + \varepsilon$.
• Monotonicity (p. 8). $V$ is nondecreasing in each argument.

Significance

The result. Watching the patrollers gives the attacker no improvement in the game value. The value interpolates $n \mapsto 1 - (1 - p)^n$ at $n = \lambda t$, giving a closed-form trade-off between patrol rate, attack duration and detection reliability. The same schedule supports the paper's Theorem 3 (invisible patrollers) and Theorem 4 (a whole perimeter).

Formalizing it. The paper proves the result; this mission seeks a machine-checked proof. The development must specify the attacker's information, almost-sure feasibility of the random schedule, and the converse. It also supplies a reusable model of continuous-time patrol games with adaptive attackers.

Difficulty

For a fixed window, the blue count is fixed and its red slot is independent. An observing attacker instead chooses a stopping time from past arrivals. The proof must account for which red slots he has seen. The half-open window matters: with $[\tau, \tau + t)$, an attacker starting at an empty red slot meets only $\lfloor \lambda t \rfloor$ patrollers.

The converse is harder because a feasible mixed strategy may have infinite expected count in every window even when each path has rate $\lambda$. An argument based only on the expected count therefore fails.

Formalization scope

Lean namespace PerimeterPatrol.Visible. Schedules are maps $s : \mathbb N \to \mathbb R$ (patroller $n + 1$ passes at $s(n)$) with the product $\sigma$-algebra. Feasibility requires Monotone s, $0 \le s(0)$, and the limit (1) along atTop, with counts given by Nat.card. A mixed strategy is an IsProbabilityMeasure that is almost surely feasible. The attacker's information up to time $u$ is the $\sigma$-algebra generated by the counts $N(v)$, $v \le u$. An attack is a start-time rule $\tau$ with a fixed window $[y, z]$, $0 < y$, such that $\{\tau \le u\}$ is measurable for that $\sigma$-algebra for every $u$. The detection probability is a Bochner integral of a $[0,1]$-valued function. $\mu^*$ is the pushforward of i.i.d. uniform draws on $[0, 1]$, with the red patroller at $jt$ present iff the $j$-th draw is below $\lambda t - \lfloor \lambda t \rfloor$.

Conventions committed to:

• the attack window is $(\tau, \tau + t]$, with information up to and including $\tau$;
• the attacker may observe from time $0$ rather than from $y$, which enlarges the attacker class, so the guarantee is at least as strong as the paper's;
• "increasing" sequences may have ties;
• floors and ceilings are Nat.floor and Nat.ceil, exact for positive arguments;
• "increases" in (2) means nondecreasing, because $V \equiv 1$ when $p = 1$ and $\lambda t \ge 1$;
• Lemma 1's least-variance law is claimed to be a maximiser, not the unique one (uniqueness fails at $p = 1$).

The attacker class includes measurable adaptive stopping times; the optimal schedule must be a probability measure; and the value is characterized through the two game inequalities rather than an unrestricted real supremum or infimum.

Needed infrastructure: counting functions of nondecreasing sequences, the stopping-time and independence argument for the red slots, the strong law of large numbers (Mathlib's ProbabilityTheory.strong_law_ae) for the long-run rate of $\mu^*$, and an averaging argument over start times for the converse. The counting and stopping-time lemmas for point processes on $[0, \infty)$ are reusable beyond this mission. Proofs of any milestone, and alternative routes to the converse, are welcome.

Not formalized here: Theorem 3 (p. 9) as a separate item, Theorem 4 (the perimeter game, p. 10), Theorem 5 (the finite-horizon simultaneous game, p. 11) and the remarks of §2.1 and §5.

Selected references

• K. Y. Lin, Optimal Patrol of a Perimeter, Operations Research, 2022, Technical Note; preprint arXiv:1905.03600v3, 2020. https://arxiv.org/abs/1905.03600v3 , https://doi.org/10.1287/opre.2021.2117

Who to discharge from a congested ward

Every day a hospital ward with a fixed number of beds decides which patients go home. Sending a patient home early frees a bed for the next admission, which matters when the ward is congested and arrivals board in the emergency department or elective surgeries are cancelled. Sending a patient home too early raises the chance that the patient is readmitted, which is costly for the patient and, under the U.S. Hospital Readmissions Reduction Program, for the hospital. Shi, Helm, Deglise-Hawkinson and Pan (SSRN 3202975; Operations Research 2021, doi:10.1287/opre.2020.2044) model this trade-off as a Markov decision process over a census of patients indexed by class and length of stay (LOS), fit personalized readmission-risk curves to hospital data, and implement the resulting discharge policy at a partner hospital.

The structural question behind their policy is who to discharge first. Hospitals usually rank patients by their current, absolute readmission risk. The paper's Theorem 2 (p. 15) instead ranks types by how fast that risk falls with a further day of stay: a type whose risk curve is flatter from now on should be discharged before a type whose risk is still dropping quickly. This mission formalizes that ranking result, in a corrected form.

Setting

There are $M$ patient classes and a maximum length of stay $J$. A type is a pair $(m,j)$ of a class and a LOS $j\in\{0,\dots,J\}$. A state $X=(X^{m,j})$ counts the patients of each type, and the census is $S=\sum_m\sum_j X^{m,j}$. A discharge action $D=(D^{m,j})$ counts the patients of each type sent home. Class $m$ has a minimum LOS $\underline L_m\in[0,J]$, and an action is feasible at $X$ when $0\le D^{m,j}\le X^{m,j}$ (3), $D^{m,j}=0$ for $j<\underline L_m$ (4), and every patient at LOS $J$ leaves.

Between two daily decision epochs $k$ and $k+1$, new patients and readmitted patients arrive at LOS $0$, and every patient who was not discharged ages by one day: $X^{m,0}_{k+1}=A^{m,0}_k+A'^{m,0}_k$ (5) and $X^{m,j}_{k+1}=X^{m,j-1}_k-D^{m,j-1}_k$ (6). Each epoch costs the holding cost $c_h(X)=C\,(S-N)^+$ for $N$ beds (7), plus the discharge cost $c_d(D)=\sum_{m,j}D^{m,j}\,R\,r(m,j)$ (8), where $r(m,t)$ is the readmission risk of a class-$m$ patient discharged at LOS $t$ and $R\ge0$ is the readmission penalty. Each risk curve $r(m,\cdot)$ is continuously differentiable and nonincreasing in the LOS.

Strong dominance (Definition 1, p. 14): $(m_1,t_1)\succ(m_2,t_2)$ iff

$$\Bigl|\frac{\partial r(m_1,t_1+t)}{\partial t}\Bigr|\le\Bigl|\frac{\partial r(m_2,t_2+t)}{\partial t}\Bigr|\qquad\forall t\ge0.\tag{15}$$

Writing $e_{(m,t)}$ for one discharge of type $(m,t)$, a schedule $(D_k)$ with trajectory $(X_k)$ over a horizon $H$ has total cost $V(D)=\sum_{k<H}[c_h(X_k)+c_d(D_k)]+c_h(X_H)+c_d(X_H)$.

Formalization targets

Goal: Theorem 2, corrected

For an initial state, an arrival path and a horizon $H$, let $(m_1,t_1)\ne(m_2,t_2)$ with $(m_1,t_1)\succ(m_2,t_2)$, $t_2\le t_1$ and $\underline L_{m_1}\le t_1$. Then every feasible schedule $D$ has a feasible schedule $D'$ with $V(D')\le V(D)$ such that, for all $k<H$,

$$D'_k\cdot e_{(m_2,t_2)}>0\ \Longrightarrow\ D'_k\cdot e_{(m_1,t_1)}=X'_k\cdot e_{(m_1,t_1)}.$$

Since the feasible schedules are finitely many, some optimal schedule discharges a $(m_2,t_2)$ patient only after all $(m_1,t_1)$ patients.

Milestones

1. Proposition 2 (p. 15): for $k'>k$, $c_d(D_k+e_{(m_1,t_1)})-c_d(D_{k'}+e_{(m_1,t_1+k'-k)})\le c_d(D_k+e_{(m_2,t_2)})-c_d(D_{k'}+e_{(m_2,t_2+k'-k)})$.
2. Census invariance (proof of Theorem 2, p. 16): swapping the discharge epochs of one $(m_1,t_1)$ patient and one $(m_2,t_2)$ patient leaves the census unchanged at every epoch.
3. Cost identity and inequality (proof of Theorem 2, p. 16): the swapped schedule is feasible, its total-cost difference equals the four discharge-cost terms displayed in the proof, and $V^{\pi_2}-V^{\pi_1}\le0$.

Significance

Theorem 2 is the paper's main structural result. It turns a high-dimensional MDP, whose state is a census over $M(J+1)$ types, into a ranking problem: once types are ordered by strong dominance, the remaining decision is how many patients to discharge (Corollary 1, p. 16), which the paper then approximates with a univariate linear-quadratic heuristic (§5). The ranking also has a direct operational reading: discharge by marginal, not absolute, readmission risk.

No machine-checked version of this result exists. Formalizing it settles exactly which hypotheses the interchange argument needs. Doing so already exposed that the statement as printed is false (see Difficulty), so the mission's output is the corrected theorem with a checked proof, together with a reusable finite-horizon, pathwise model of class-by-LOS patient flow.

Difficulty

The obvious argument is a single interchange: if a $(m_2,t_2)$ patient is discharged at epoch $k$ while a $(m_1,t_1)$ patient stays until a later epoch $k'$, swap their discharge epochs. The census path does not change, and Proposition 2 shows the discharge cost does not increase. The step that fails is the one the paper defers to Appendix B.3: the dominated patient, kept from $k$ to $k'$, may pass the maximum LOS $J$ before $k'$, and then the swap is not available. The appendix's repair does not close the gap. With $J=3$, $N=1$, $C=1000$, $R=1$, no arrivals, $r(1,j)=10-j$, $r(2,j)=10-2j$ and one $(1,0)$ and one $(2,2)$ patient on day $0$, we have $(1,0)\succ(2,2)$, yet the unique optimum discharges the $(2,2)$ patient alone (cost 1013), and every schedule that obeys the rule costs at least 1014. The added hypothesis $t_2\le t_1$ guarantees that the dominated patient can wait as long as the dominating one, so the swap always exists.

The remaining difficulty is bookkeeping: the interchange changes two cohorts by $\pm1$ over an interval of epochs, and feasibility (counts, minimum LOS, forced exit at $J$) must be checked along the new trajectory. Repeated interchanges must also be ordered so that fixing one epoch does not break an earlier one.

Formalization scope

• Model. Classes are Fin M, LOS indices Fin (J+1), counts natural numbers, costs real numbers. Epochs start at $0$. Arrivals, new and readmitted, form one exogenous deterministic path, as Remark 4 (p. 12) prescribes for §4. Every statement is pathwise on a finite horizon $H$, the setting of the paper's interchange argument. The long-run average cost (9) is not used, since a finite interchange cannot change it.
• Conventions added. Patients at LOS $J$ must leave, since (6) has no LOS $J+1$. The total cost charges every patient present at the horizon as if discharged at their current LOS, so that holding a patient to the end is not free. The risk curves are $C^1$ and nonincreasing on $[0,\infty)$ (p. 15), and $R\ge0$. Strong dominance uses Mathlib's deriv with the absolute values of (15).
• Correction to Theorem 2. The goal adds $t_2\le t_1$ (the printed statement is false, as shown above), $(m_1,t_1)\ne(m_2,t_2)$ (strong dominance is reflexive, so the rule would otherwise demand every type be fully discharged once any is), and $\underline L_{m_1}\le t_1$ (otherwise $(m_1,t_1)$ patients can never be discharged). "The optimal action" becomes "some no-costlier feasible schedule obeys the rule": with ties an optimal schedule may break it.
• Ruling out trivial readings. The goal quantifies over feasible schedules with the real costs (7)–(8), and the rule is required at every epoch $k<H$ along $D'$'s own trajectory. Taking $D'=D$ does not suffice in general, and a schedule that avoids discharging $(m_2,t_2)$ by letting patients vanish is excluded by the forced exit and the terminal valuation.
• Infrastructure. One definitions file holds the model, strong dominance, unit actions and the interchange. Mathlib's fundamental theorem of calculus (intervalIntegral.integral_eq_sub_of_hasDerivAt) and monotonicity of integrals are the analytic substrate for Proposition 2. The trajectory and interchange lemmas about class-by-age cohorts are reusable for other census models. Proofs of any milestone are welcome independently.

Not formalized: Theorem 1 (existence of an average-cost optimal policy), Corollary 1 (threshold form), Propositions 1 and 3, and Lemma 1.

Selected references

• P. Shi, J. E. Helm, J. Deglise-Hawkinson, J. Pan, Timing it right: balancing inpatient congestion versus readmission risk at discharge, SSRN working paper 3202975, version of 2019-08-26. https://ssrn.com/abstract=3202975
• P. Shi, J. E. Helm, J. Deglise-Hawkinson, J. Pan, same title, Operations Research, 2021 (published version; not the citation basis of this mission). https://doi.org/10.1287/opre.2020.2044

Motivation

Flow networks model the movement of material, traffic, electricity, or gas through connected systems. In many such models, the required net flow at each vertex varies with a parameter, so the object of interest is a whole family of optimal flows rather than one solution. When edge costs are nonlinear, solving a new optimization problem for every parameter value gives no finite description of that family. Joachims, Klimm and Warode study two approximations of this parametric problem: one approximates each edge's marginal cost, and the other interpolates selected optimal flows. This mission concerns their marginal cost approximation result, Theorem 5.

The paper builds on an exact method for piecewise quadratic edge costs by Klimm and Warode. A piecewise linear approximation of each marginal cost has a piecewise quadratic integral, so it brings general convex costs into the class handled by that method. The question is how fine the linear interpolation mesh must be for the resulting flows to be close to optimal under the original costs. The paper gives local step size bounds involving the second derivative of each marginal cost. The target here is a corrected version of that guarantee, with the precise corrections stated below.

Setting

A network consists of finite sets of vertices $V$ and edges $E$. Every edge has a tail and a head. The graph is strongly connected and has neither self loops nor parallel directed edges. For an edge flow $x\in\mathbb R^E$, its net inflow at a vertex is the sum of flows entering that vertex minus the sum leaving it. Two balanced demand vectors $b^0,b\in\mathbb R^V$ determine a demand $b^0+\lambda b$ for $\lambda\in[0,\lambda^{\max}]$. A flow is feasible when its net inflow equals that demand. In the directed case all edge flows are nonnegative; in the undirected case their signs are unrestricted.

Each edge $e$ has a marginal cost $f_e:\mathbb R\to\mathbb R$ that is strictly increasing, differentiable, nonpositive on negative arguments, and nonnegative on positive arguments. Its edge cost is $F_e(x)=\int_0^x f_e(s)\,ds$. The total cost is the sum of edge costs, and $C(\lambda)$ is the minimum total cost of a feasible flow at parameter $\lambda$. These sign conditions make the edge costs nonnegative. The paper calls them homogeneous marginal costs, although this is a sign condition rather than algebraic homogeneity. Section 5.2 gives the model and its approximation criterion.

For each edge, choose a strictly increasing mesh from $-x^{\max}$ to $x^{\max}$, where

$$x^{\max}=\max_{0\le\lambda\le\lambda^{\max}}\frac12\sum_{v\in V}|b_v^0+\lambda b_v|.$$

The linear spline $s_{f_e}$ joins the values of $f_e$ at adjacent mesh points by straight chords. The minimum cost flow function $\widetilde x(\lambda)$ for these spline marginal costs is tested under the original costs: $\widetilde C(\lambda)=\sum_e F_e(\widetilde x_e(\lambda))$. This convention is essential because a small optimal cost for the spline instance alone says nothing about the cost under $f_e$.

Formalization targets

The milestones follow the paper's argument in order.

1. Edge-flow bound (§5.2.1, p. 16): every optimal edge flow satisfies $|x_e(\lambda)|\le x^{\max}$.
2. Equation (17) (proof of Lemma 4, p. 16): the closeness condition (15) of marginal costs on $[-x^{\max},x^{\max}]$ gives

$$\frac{2}{1+\alpha}F_e(x)-\frac{\beta}{(1+\alpha)m}\le\widetilde F_e(x)\le\frac{2\alpha}{1+\alpha}F_e(x)+\frac{\beta}{(1+\alpha)m}.$$

3. The (16) case (proof of Lemma 4, p. 17): $|\widetilde f_e|\ge|f_e|$ and (16) give $F_e\le\widetilde F_e\le\alpha F_e+\beta/m$.
4. Lemma 4 (p. 16): uniform control of $|\widetilde f_e-f_e|$ on $[-x^{\max},x^{\max}]$ in the sense (15) or (16) makes the minimum-cost flow function of the $\widetilde f$ instance an $(\alpha,\beta)$-approximation.
5. Equation (18) (p. 17): the interpolation estimate

$$|f(x)-s_f(x)|\le\frac18\delta_i^2\max_{\xi\in[x_i,x_{i+1}]}|f''(\xi)|.$$

6. Spline domination under (ii) (proof of Theorem 5, p. 18): $|s_{f_e}(x)|\ge|f_e(x)|$ on $[-x^{\max},x^{\max}]$.
7. Endpoint maximum under (ii) (proof of Theorem 5, p. 18): $\max_{[x_i,x_{i+1}]}|f_e''|=\max\{|f_e''(x_i)|,|f_e''(x_{i+1})|\}$.

The goal is the corrected Theorem 5. It states that either of the paper's two explicit step size regimes, involving $\alpha>1$, $\beta\ge0$, $m=|E|$, and $x^{\max}$, makes the spline instance's minimum cost flow function satisfy

$$\widetilde C(\lambda)\le\alpha C(\lambda)+\beta\qquad(0\le\lambda\le\lambda^{\max}).$$

The first regime bounds each step by a local maximum of $|f_e''|$ and the magnitude of $f_e$ at a mesh endpoint. The second adds monotonicity and sign conditions on $f_e''$ and uses its endpoint values. The formal theorem retains the constants $2\sqrt2$, the factor $1/8$ in (18), and both distinct denominators in Theorem 5. Theorem 5, pp. 17–18 is the source for the exact formulas.

Significance

The guarantee applies to an entire interval of demand parameters. It converts local numerical accuracy of the marginal cost splines into a bound on the original total cost at every parameter value, while preserving feasibility. The edge flow bound explains why it suffices to approximate marginal costs on a finite interval even when edge flows are otherwise real valued.

The paper proves the intended result by a paper argument, but its printed Theorem 5 has a counterexample when a mesh crosses zero without including zero: the spline can lose the marginal cost sign condition, and at zero demand the spline optimum can have positive original cost while the true optimum has cost zero. The corrected goal records a valid target for machine checked proof. Formalizing it also yields reusable definitions of finite flow networks, convex separable edge costs, parametric approximation, and chord splines. No machine checked proof of this theorem is claimed by this mission.

Difficulty

Pointwise closeness of marginal costs does not directly compare the two optimized flows, which may differ on every edge. A direct comparison at the spline optimum must also account for the original optimum and for how the edge costs accumulate across the network. The interpolation estimate alone does not settle this: a mesh interval crossing zero can change the sign of its chord at zero, even when every step size bound in the printed theorem holds. The shape condition in Theorem 5(ii), read literally with the third differentiability assumption, also forces the second derivative to vanish on the negative half line. The mission keeps that condition as printed rather than silently replacing it with a more symmetric one.

Formalization scope

Lean represents vertices and edges by finite types, net inflow by finite sums, and each edge cost by a real interval integral based at zero. A Boolean flag selects the directed case with $x_e\ge0$ or the undirected case with no sign constraint. The general finite lower and upper bounds of problem (14) are outside this mission. The optimal cost is the real infimum of feasible costs; the graph and balanced demand assumptions give feasible flows, and the sign assumptions bound their costs below. The spline is computed from its mesh values, with its end chords extended linearly outside $[-x^{\max},x^{\max}]$. Meshes are indexed from zero in Lean, regardless of the paper's two indexing styles.

The corrected Theorem 5 requires zero to be a mesh point on every edge. In regime (i), it replaces $|f_e(x_i)|$ by $\min\{|f_e(x_i)|,|f_e(x_{i+1})|\}$. In regime (ii), both entries of the factor $B$ are square roots of $|f_e''|$; this matches the equality $B^2=\max\{|f_e''(x_i)|,|f_e''(x_{i+1})|\}$ used in the printed proof. Lemma 4 and Theorem 5 explicitly require $x^{\max}>0$, since both step-size bounds and (15), (16) divide by it (with zero demands, a one-point mesh and $\beta=0$, Theorem 5 would otherwise fail), and its second marginal cost family is continuous, strictly increasing, and sign preserving. These conventions and corrections are recorded in the source analysis for Theorem 5.

A proof must use the chord spline determined by $f_e$ and the mesh; replacing it by an arbitrary close function would discard the numerical claim. Likewise, the bound $|\widetilde x_e(\lambda)|\le x^{\max}$ is never a hypothesis of Lemma 4 or of the goal: it is milestone 1, and assuming it would remove the combinatorial half of the argument. Milestone 6 is stated on $[-x^{\max},x^{\max}]$ rather than on all of $\mathbb R$ as printed, because the linearly extended end chord of a convex function lies below it. Contributions to the flow bound, Lemma 4, the spline estimate, or the final connection between them are all within scope. The flow and spline definitions can also support other approximation results beyond this theorem.

Selected references

• Per Joachims, Max Klimm and Philipp Warode, Approximate Parametric Computation of Minimum-Cost Flows with Convex Costs, arXiv preprint, 2022. arXiv:2203.13146v1.
• Max Klimm and Philipp Warode, Parametric Computation of Minimum-Cost Flows with Piecewise Quadratic Costs, Mathematics of Operations Research, articles in advance, 2021. DOI:10.1287/moor.2021.1151.

Motivation

Prices of staple vegetables in India, onions above all, rise sharply at irregular intervals. When they do, governments respond with cash transfers, subsidized sales and import programmes. A recurring explanation for these price spikes is artificial shortage: traders who control a large share of the stock withhold supply early in a season, and consumers who observe the scarcity raise the amount they are willing to spend on the commodity, so the traders sell more later at a higher price. Levi, Singhvi and Zheng (SSRN 3332493; Manufacturing & Service Operations Management) give a stylized model of this mechanism. It shows that a monopolist trader facing budget-adjusting consumers creates an artificial shortage. It then asks how three common government interventions change the shortage. This mission formalizes the paper's answer for the first intervention, a cash subsidy (CS) to the poorest consumers. The question matters for policy: the paper argues that a well-intended transfer can make the hoarding worse.

Setting

A unit mass of consumers have Period-1 budgets $b_c$ distributed uniformly on $[0,1]$. A monopolist trader sells over two periods.

• Period 1. The trader releases $q_1\in[0,1]$, which clears at price $p_1=1-q_1$. Consumers interpret $q_1<1$ as a shortage and scale their budgets by the updated-budget multiplier

$$B(q_1)=1+g(1-q_1),$$

where $g>0$ is the budget adjustment factor.

• Period 2, no intervention. A consumer buys at price $p_2$ iff $b_cB(q_1)\ge p_2$. The trader's total revenue is $q_1(1-q_1)+B(q_1)q_2(1-q_2)$.
• Artificial shortage (Definition 1): $q_1<q_2$ and $p_1<p_2$, i.e. less is sold early and the later price is still higher.

Under a cash subsidy $(c,f)$, the government gives cash $c\ge0$ to the fraction $f\in[0,1]$ of consumers with the lowest budgets, within a budget $cf\le b$. At price $p$:

• a non-subsidized consumer ($b_c\ge f$) buys iff $b_c\ge p/B(q_1)$;
• a subsidized consumer ($b_c<f$) buys iff $b_c\ge(p-c)/B(q_1)$.

The game is solved by backward induction:

1. the trader sets the Period-2 price, maximizing revenue;
2. the government, after observing $q_1$, chooses $(c,f)$ to maximize Period-2 consumer welfare $CW_2$ (eq. (5)) at the trader's response. $CW_2$ measures the buyers' original budgets against the price they pay, adds the cash they receive, and counts a utility $\lambda$ per buyer and $-\lambda$ per non-buyer, with $1+g<\lambda$;
3. the trader chooses $q_1$, anticipating both.

The set of equilibrium Period-1 quantities is $\mathrm{EqQ1}(b)$. An element is written $q^1_{CS}$, and $q^1_\phi$ is the no-intervention quantity.

Formalization targets

Goal: Proposition 3 (p. 22)

With $\bar b=(8+4g+g^2)/32$, there is a threshold $t_1\in(0,\bar b)$ such that

$$q^1_{CS}=q^1_\phi\ (b<t_1),\qquad q^1_{CS}\ge q^1_\phi\ (t_1<b\le\bar b),\qquad q^1_{CS}<q^1_\phi\ (b>\bar b),$$

and $q^1_{CS}$ is non-increasing in $b$ for $b>t_1$. The equilibrium set is also nonempty for every $b\ge0$.

Milestones

• Proposition 1 (p. 10): without intervention the unique optimum is $(q_1^*,q_2^*)=(1/2-g/8,\,1/2)$, with $p_1^*=1/2+g/8$ and $p_2^*=1/2+g/4+g^2/16$.
• Remark after Proposition 1 (p. 10): for $g>0$ this optimum is an artificial shortage.
• Theorem 1 (p. 16): the government's optimal subsidy is $f^*=\min(1,b/c^*)$, with $c^*$ given by four closed forms on four budget ranges.
• Theorem 2(i)–(iii) (p. 17): $q_1^*=1/2-g/8$ for $b<t_1$, and the roots of two explicit first-order conditions on $[t_1,\bar b)$ and $[\bar b,(4+2g+g^2)/4)$.
• Theorem 2(iv), corrected (p. 17): for $b>(4+2g+g^2)/4$,

$$q_1^*=\max\{0,(1-g)/2,1-(b-1)/g\}.$$

Significance

Proposition 3 is the paper's verdict on cash subsidies. A small budget is absorbed without effect on the trader's behaviour, because the trader's Period-2 revenue equals its no-intervention value. A moderate budget induces a larger Period-1 release and so mitigates the shortage. A budget above $\bar b$ makes the trader withhold more than without intervention, because subsidized consumers can pay more in Period 2. The non-monotone dependence on $b$ is the basis of the paper's policy advice against "oversubsidizing" and of its comparison with supply-allocation schemes (Proposition 4, not in this mission).

The paper prints no proofs; they are "available from the authors upon request" (p. 10). The threshold $t_1$ and the online appendix (Lemma O.1) are not in the published text. A machine-checked development would therefore be the first complete public proof of these statements. It would also settle Theorem 2(iv), whose printed form is false on a band of budgets and is posed here in corrected form. None of these results has a formal proof anywhere.

Difficulty

Every stage of the backward induction is a non-smooth optimization.

• Period 2. The demand is piecewise linear with up to three pieces, so the trader's revenue is bimodal. One mode sells only to non-subsidized consumers, the other also reaches subsidized ones.
• Government. It optimizes over a two-dimensional policy against this discontinuous best response. The optimum sits at the trader's point of indifference between the two modes (Theorem 1(i)), which is attained only through the trader's tie-break toward the larger quantity.
• Period 1. The trader's objective inherits the bimodality and a kink at $b=B(q_1)$. The equilibrium therefore jumps at $t_1$, and the printed closed form fails near the kink.

The tempting route is to differentiate the Period-1 objective and solve the first-order condition. It fails twice. It misses the jump at $t_1$, where the global maximizer switches modes, and it misses the kink above $(4+2g+g^2)/4$, where the maximizer is not a stationary point.

Formalization scope

All quantities are real numbers. The trader's Period-2 decision is a price $p\ge0$ with quantity equal to the explicit demand, which is equivalent to the paper's quantity form. Purchases at equality count as purchases, as in the text. The commitments are:

• Standing assumptions: $0<g$ and $1+g<\lambda$ (pp. 10, 13), and the added $g<4$, which keeps $1/2-g/8$ in $[0,1]$.
• Tie-breaks: the trader picks the larger quantity among revenue maximizers (footnote 10). The government picks the least outlay $cf$ among welfare maximizers. Without the second rule, Theorem 1(iv) and Proposition 3(i)(c) are false, because for $b>B(q_1)$ every $c\in[B(q_1),b]$ ties.
• Equilibrium: $\mathrm{EqQ1}(b)$ is the set of $q_1\in[0,1]$ that maximize total revenue against some selection of government choices and Period-2 best responses. Every claim about $q^1_{CS}$ is made for every element.
• Existential constants: $t_1$, $b^{CS}_1$ and $b^{CS}_2$, whose formulas are not in the paper. Each is pinned by the clauses around it.

The goal is stated about $\mathrm{EqQ1}$ itself. A version that substituted Theorem 2's closed forms or first-order roots for $q^1_{CS}$ would assume the content of the theorem, and is ruled out.

The development needs the Period-2 best response of a piecewise-linear demand, the government's two-variable welfare problem (eq. (5) is a polynomial in the breakpoints), and a comparison of the two modes of the Period-1 objective. Lemmas on maximizers of piecewise-quadratic functions are reusable beyond this mission. Proofs of any milestone, and sanity lemmas on the tie-breaks, are welcome.

Selected references

• R. Levi, S. Singhvi, Y. Zheng, Artificial Shortage in Agricultural Supply Chains, Manufacturing & Service Operations Management (forthcoming; SSRN version of 2021-04-14), 2021. https://ssrn.com/abstract=3332493 — DOI of the journal version: https://doi.org/10.1287/msom.2021.1010

Motivation

A seller whose customers influence one another faces a choice between two pricing policies. It can collect information about the social network and charge each customer a personalised price that reflects their position in it, or it can ignore the network and charge everyone one uniform price. Personalised pricing is never worse for the seller, but collecting network data is costly and raises privacy concerns. The question is how much profit the network information is worth.

For a fixed network the answer depends on its fine structure. Candogan, Bimpikis and Ozdaglar (Operations Research 2012) showed that with linear-quadratic utilities the optimal personalised prices are expressed through Bonacich centralities, so the gain from discrimination is a difference of discounted walk counts. Huang, Mani and Wang (SSRN 3368458; published in Management Science, 2021) study this gain, the value of price discrimination, in large random networks. Their main result for random networks, Theorem 5.1, says that in directed Erdős–Rényi networks the seller who prices uniformly loses only a vanishing fraction of the optimal profit, whatever the density of the network. This mission formalizes that theorem and the results its proof rests on.

Setting

There are $n$ consumers. The network is an $n\times n$ matrix $G$ with non-negative entries, where $G_{ij}$ is the influence of consumer $j$ on consumer $i$. For a square matrix $A$, $\|A\|$ is its spectral norm (the $\ell^2$ operator norm); $\mathbf 1$ is the all-ones vector, and $\mathbf 1^{\mathsf T}A^k\mathbf 1$ is the total weight of walks of length $k$ in $A$.

Consumer $i$ facing price $p_i$ chooses a consumption level $x_i$ to maximise

$$u_i=ax_i-x_i^2+4\rho x_i\sum_{j\ne i}\frac{G_{ij}}{\|G+G^{\mathsf T}\|}x_j-p_ix_i,$$

with a stand-alone utility $a>0$ and a network coefficient $\rho\in(0,1)$. The resulting consumption equilibrium is (eq. (1))

$$x^*(p)=\tfrac12\Big(I-\tfrac{2\rho}{\|G+G^{\mathsf T}\|}G\Big)^{-1}(a\mathbf 1-p).$$

The seller has marginal cost $c<a$ and profit $\pi(p)=(p-c\mathbf 1)^{\mathsf T}x^*(p)$. The optimal profit is $\pi^*=\max_{p\in\mathbb R^n}\pi(p)$; the optimal uniform price is $p_0=\frac{a+c}{2}\mathbf 1$. The regret and fractional regret of uniform pricing are

$$R(p_0)=\pi^*-\pi(p_0),\qquad R_F(p_0)=1-\frac{\pi(p_0)}{\pi^*}.$$

A directed Erdős–Rényi network $G(n,p)$ is the random $0/1$ matrix whose off-diagonal entries are independent with $\Pr[G_{ij}=1]=p$, and whose diagonal is zero. $\mathbb E_G$ denotes expectation over it. The constants $a,c,\rho$ are the same for every $n$.

Formalization targets

Goal: Theorem 5.1

For every sequence of densities $(p(n))_{n\in\mathbb N}$ with values in $[0,1]$,

$$\mathbb E_{G(n,p(n))}[R(p_0)]=o(n)\qquad\text{and}\qquad\mathbb E_{G(n,p(n))}[R_F(p_0)]=o(1).$$

Both parts are stated. The goal fixes no rate and no density regime; the paper's Theorems 5.2–5.4 give exact rates in three regimes and are not part of this mission.

Milestones

1. Eq. (3): $\pi^*$ is attained and equals $\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{\rho}{\|G+G^{\mathsf T}\|}(G+G^{\mathsf T}))^{-1}\mathbf 1$, with its walk series.
2. Eq. (4): $p_0$ is the optimal uniform price, and $\pi(p_0)=\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{2\rho}{\|G+G^{\mathsf T}\|}G)^{-1}\mathbf 1$.
3. Lemma 5.3 (for even $t$): $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1\le\|G+G^{\mathsf T}\|^{k-t}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^t\mathbf 1$ for $k\ge t$.
4. Eq. (29): $\mathbb E_G[R(p_0)]\le\frac12(\frac{a-c}{2})^2\,\mathbb E_G[\frac{\rho^2}{1-\rho}\|G+G^{\mathsf T}\|^{-2}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]$.
5. Appendix D.1, Case 1, and footnote 6: a non-empty binary network has $\|G+G^{\mathsf T}\|\ge1$. In the footnote's words, "Therefore a non-empty network (with at lease one link) has spectral norm greater than or equal to 1."
6. Lemma 5.2: $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]=2n(n-1)p(1-3p+2np)$.
7. Lemma 5.5 (i): $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1]\ge2^k\mathbb E_G[\mathbf 1^{\mathsf T}G^k\mathbf 1]$ for all $k\ge0$.
8. Lemma 5.5 (ii): for $1\le k<n$ and $\frac1{n-k+1}\le p<1$, the gap in (i) is at most $(k-1)2^{k-1}P(n,k)p^{k-1}+(k-1)^k2^kP(n,k-1)p^{k-2}$, with $P(n,k)=n!/(n-k)!$.
9. Eq. (12), Rayleigh step: $\|G+G^{\mathsf T}\|\ge\mathbf 1^{\mathsf T}(G+G^{\mathsf T})\mathbf 1/\mathbf 1^{\mathsf T}\mathbf 1$.
10. Eq. (9): for non-empty $G$ and $k>0$, $0<\mathbf 1^{\mathsf T}\big((G+G^{\mathsf T})/\|G+G^{\mathsf T}\|\big)^k\mathbf 1\le n$.
11. Eq. (14): $\frac n2(\frac{a-c}2)^2\le\pi^*\le\frac12(\frac{a-c}2)^2\frac n{1-\rho}$.

The paper calls the optimal uniform price $p_0$ "under the assumption that $c<a$, according to [12]" (p. 7); milestone 2 states that optimality as part of eq. (4).

Significance

Theorem 5.1 says that in large random networks the network information has asymptotically no value to a monopolist: the uniform price $p_0$ does not depend on the network, yet earns a fraction of the optimal profit tending to one, for sparse, critical and dense networks alike. This separates the deterministic picture, where some networks have a large value of discrimination (Theorem 4.1 of the paper characterises those with none), from the typical random one. It supplies a benchmark against which network-based pricing, and the cost of collecting network data, can be judged.

The paper proves the theorem by hand. No part of it, and no part of the model, has been machine-checked; the platform has no network pricing model and no walk-count results for directed random graphs. A complete development would make the closed forms (3) and (4), the spectral inequalities and the Erdős–Rényi walk moments reusable. The printed proof of Theorem 5.1 bounds expectations of ratios by almost-sure statements and splits the density sequence into "maximal subsequences"; a formal proof must replace these steps by quantitative ones. The printed proof of Lemma 5.5 (i) relies on a per-walk claim that fails (a closed walk $0\to1\to2\to0\to1$ in $G+G^{\mathsf T}$ can use four arcs of $G$ while it visits three ordered pairs), although the statement itself was checked by exhaustive enumeration for small $n$; that lemma needs a new argument.

Difficulty

The regret is a difference of two discounted walk series. Bound (29) controls it by walks of length two and the spectral norm, which suffices when the network is very sparse, but in dense networks, where $\|G+G^{\mathsf T}\|\approx2np$ and $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1\approx4n^3p^2$, it only gives $O(n)$. The dense case needs the cancellation between $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1$ and $2^k\mathbf 1^{\mathsf T}G^k\mathbf 1$ for each $k$ up to a slowly growing cutoff (Lemma 5.5), together with a lower bound on the spectral norm that holds with high probability. In the critical regime $np=\Theta(1)$, neither bound applies directly, and one needs that $\|G+G^{\mathsf T}\|$ grows with $n$ in probability. The goal quantifies over all density sequences, so the argument must be uniform across these regimes; a proof for one regime does not suffice.

Formalization scope

All objects live in the namespace NetPriceDisc.Random and are defined in one file. Networks are Matrix (Fin n) (Fin n) ℝ; the spectral norm is Mathlib's $\ell^2$ operator norm (Matrix.Norms.L2Operator). The consumption equilibrium is formula (1) for every price vector, with no non-negativity constraint on consumption, as in the paper's definition of $\pi(p)$. $\pi^*$ is defined as the supremum of $\pi$ over $\mathbb R^n$, and $R$, $R_F$ from $\pi^*$ and $\pi(p_0)$; the closed forms (3) and (4) are theorems, not definitions, so the goal cannot be discharged by unfolding formulas. Lean's convention $x/0=0$ gives the empty network no externality, hence zero regret, which is the paper's own reading of the empty network (p. 12); the empty network keeps its probability $(1-p)^{n(n-1)}$. The Erdős–Rényi expectation is the finite sum over arc sets $S$ of off-diagonal pairs with weight $p^{|S|}(1-p)^{n(n-1)-|S|}$; no measure theory is used. The fractional regret's expectation is the expectation of the ratio. "Any sequence of densities" is a function $\mathbb N\to[0,1]$, with no further restriction.

Two printed statements are corrected and disclosed: Lemma 5.3 is stated for even $t$ (as printed it fails for odd $t$; for the star $K_{1,3}$ with $t=1$, $k=2$ one gets $12>6\sqrt3$), and Lemma 5.5 (ii) for $k\ge1$ (at $k=0$ it involves the undefined $P(n,-1)$). Only the deterministic Rayleigh-quotient part of eq. (12) is stated.

Useful infrastructure includes Neumann series and Rayleigh-quotient bounds for symmetric non-negative matrices, walk moments of directed Erdős–Rényi graphs, and maximum-degree or spectral lower bounds in probability. Proofs of any milestone, and alternative routes to the goal that avoid Lemma 5.5, are welcome.

Selected references

• J. Huang, A. Mani, Z. Wang, The Value of Price Discrimination in Large Random Networks, SSRN 3368458 (EC '19 submission version); published as The Value of Price Discrimination in Large Social Networks, Management Science, 2021. https://ssrn.com/abstract=3368458, https://doi.org/10.1287/mnsc.2021.4108
• O. Candogan, K. Bimpikis, A. Ozdaglar, Optimal Pricing in Networks with Externalities, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1066
• P. Bonacich, Power and Centrality: A Family of Measures, American Journal of Sociology 92(5), 1987. https://doi.org/10.1086/228631
• M. Krivelevich, B. Sudakov, The Largest Eigenvalue of Sparse Random Graphs, Combinatorics, Probability and Computing 12(1), 2003. https://doi.org/10.1017/S0963548302005424

Motivation

Asset managers increasingly buy alternative data: satellite images, credit-card panels, web traffic. Raw data of this kind is worthless until someone has the skills to process it, and those skills are costly and uncertain to acquire. A fund can hire data scientists and still find that its models extract little. Huang, Xiong and Yang (Management Science, 2022) build an equilibrium model of a data seller who sells to investors who must first acquire such skills. They ask how the cost of acquiring skills feeds through the data market into the financial market: into how much the price reveals, the cost of capital and return volatility.

The model joins two lines of work. One is the classical noisy rational-expectations market of Grossman and Stiglitz (1980), in which prices partly reveal private information. The other is the literature on selling information started by Admati and Pfleiderer (1986, 1990), in which a monopolist seller degrades the information it sells to limit what the price leaks. The new feature is the "gold rush" of skill acquisition: an investor who pays the cost learns only afterwards whether her skill is high or low.

Setting

A risky asset pays $\tilde\theta\sim N(0,\tau_\theta^{-1})$ and there is noise demand $\tilde u\sim N(0,\tau_u^{-1})$. A data seller observes $\tilde\theta+\tilde\eta$ with $\tilde\eta\sim N(0,\tau_\eta^{-1})$; the precision $\tau_\eta$ is the data accuracy. The seller chooses a clarity $x\in(0,\infty]$ and passes the data with personalized noise, so that a buyer of skill $z$ receives a signal of precision $xz$ about $\tilde\theta+\tilde\eta$. The value $x=\infty$ means the data are sold "as is".

A continuum of CARA investors with risk aversion $\gamma$ is indexed by $i\in[0,1]$. Investor $i$ can acquire data-processing skills at cost $C(c,i)$, where $c>0$ is a cost parameter. The cost is continuous and strictly increasing in $i$, with $C(c,0)=0$ and $C(c,i)\to\infty$ as $i\to1$, and it is strictly increasing in $c$. A skilled investor turns out high-skilled ($Z_H$) or low-skilled ($Z_L$) with probability $\tfrac12$ each, with $0<Z_L<Z_H$. A mass $\lambda$ of investors becomes skilled.

In the asset market, the price reveals $\tilde\theta+\tilde\eta$ with precision $\alpha^2\tau_u$, and $\alpha$ is pinned down by the market-clearing equation (14). Skilled investors buy the data at a Nash-bargained price $q=\beta G$, where $G(x,\alpha)$ is the certainty-equivalent trading gain (15) and $\beta\in(0,1)$ is the seller's bargaining power. Investors acquire skills until the marginal investor is indifferent, $(1-\beta)G(x,\alpha)=C(c,\lambda)$ (19). The seller chooses $x$ to maximize the profit $\lambda q$. An equilibrium is a clarity $x^*$ with its $(\lambda^*,\alpha^*)$ such that no other feasible clarity gives more profit.

The market outcomes are:

• the data price $q^*$;
• price informativeness $1/\operatorname{Var}(\tilde\theta\mid\tilde p)$;
• the cost of capital $E(\tilde\theta-\tilde p)$;
• return volatility $\sigma(\tilde\theta-\tilde p)$;
• skilled investors' performance, the average certainty-equivalent advantage (21) of a skilled over an unskilled investor.

Formalization targets

Goal: Proposition 5

Fix $0<c_1<c_2$. There is a threshold $T$ such that, for every data accuracy $\tau_\eta\ge T$ and every pair of equilibria at $c_1$ and $c_2$, both clarities are finite and

$$\lambda^*_2<\lambda^*_1,\quad x^*_1<x^*_2,\quad q^*_1<q^*_2,\quad \frac{1}{\operatorname{Var}_1(\tilde\theta\mid\tilde p)}<\frac{1}{\operatorname{Var}_2(\tilde\theta\mid\tilde p)},$$ $$E_2(\tilde\theta-\tilde p)<E_1(\tilde\theta-\tilde p),\quad \sigma_2(\tilde\theta-\tilde p)<\sigma_1(\tilde\theta-\tilde p),\quad \mathrm{Performance}_1<\mathrm{Performance}_2 .$$

The paper writes these as signs of derivatives in $c$. The goal states them as comparisons between two cost levels, which is what the prose of the proposition asserts.

Milestones

1. Proposition 1: for given $(\lambda,x)$, equation (14) has a unique positive root $\alpha$.
2. Proof of Proposition 2: for each finite clarity $x$, a unique $(\lambda,\alpha)$ solves (14) and (19).
3. Proposition 2 (1): an equilibrium exists.
4. (C5): on feasible tuples the profit equals $\beta\lambda C(c,\lambda)/(1-\beta)$.
5. Proposition 3: in equilibrium, $x^*<\infty$ if $\lambda^*\tau_\eta>\alpha^*\gamma$ and $x^*=\infty$ otherwise.
6. The clarity limit: as $\tau_\eta\to\infty$, every solution $x$ of (14) tends to $2\alpha\gamma/(\lambda(Z_H+Z_L))$.
7. The α limit: the equilibrium $\alpha^*$ tends to $\sqrt{\tau_\theta/\tau_u}$.
8. (C18): the equilibrium $\lambda^*$ tends to a root of (C18).

Significance

The result. Proposition 5 is the paper's headline. When skills are uncertain, a rise in skill-acquisition costs makes prices more informative and lowers the cost of capital and return volatility. When skills are certain, these outcomes stay unchanged (Proposition 4). The mechanism is that the seller cannot tailor one clarity to buyers of unknown skill. To keep buyers interested as costs rise, she provides clearer data, and more information leaks into the price. The result separates the data market from a pure cost shock to information production. It gives empirical predictions for markets where skill acquisition is costlier, such as private or international equities.

Formalizing it. The proposition is proved in the paper by expansion in $w=1/\tau_\eta$ around $w=0$. A machine-checked version must make "sufficiently high $\tau_\eta$" precise, with a threshold that holds uniformly over all equilibria. It must also control the exact finite-$\tau_\eta$ equilibrium rather than its limit. The mission also contributes the first noisy rational-expectations model with a strategic data seller on the platform: posterior variances, the equilibrium equation (14), the certainty-equivalent gain, and the seller's choice between finite clarity and selling "as is". No part of the paper has been formalized before.

Difficulty

Several comparisons follow at leading order in $1/\tau_\eta$. As $\tau_\eta\to\infty$ the equilibrium mass converges to the root of (C18), which is decreasing in $c$, and the clarity, the data price and performance are, to first order, functions of that mass. The price-informativeness, cost-of-capital and volatility comparisons do not follow at leading order. At $\tau_\eta=\infty$ the ratio $\alpha^*$ tends to $\sqrt{\tau_\theta/\tau_u}$ whatever the cost, so these three outcomes are flat in $c$ to leading order. Their signs come from the $O(1/\tau_\eta)$ correction to $\alpha^*$, and the correction must be controlled jointly with the seller's optimal clarity. A newcomer's first idea is to set $\tau_\eta=\infty$ in the equilibrium conditions and differentiate. That loses exactly the term that carries the result. A further difficulty is that the seller's optimum is defined by comparison with every feasible clarity, including selling "as is", not by a first-order condition.

Formalization scope

All quantities are real numbers. The parameters satisfy $\tau_\theta,\tau_u,\gamma>0$, $0<\beta<1$, $0<Z_L<Z_H$ and $\tau_\eta>0$. Two of these go beyond the paper's §2 domains, and both are needed:

• $\beta>0$: with $\beta=0$ the profit is identically zero and every clarity is optimal;
• $Z_L>0$: this is the paper's own condition on p. 23.

The cost family is any admissible $C(c,i)$: continuous and strictly increasing in $i$ on $[0,1)$, $C(c,0)=0$, $C(c,i)\to\infty$ as $i\to1^-$, and strictly increasing in $c$ on $(0,1)$. "Increasing" in the paper is read as strictly increasing. Clarity is either a finite $x>0$ or "as is". At "as is", (14) becomes $\gamma\alpha=\lambda\tau_\eta$ and both conditional variances given a signal equal $1/(\tau_\theta+\tau_\eta)$. These are the $x\to\infty$ limits of the finite-clarity formulas. The value $x=0$ is excluded from the choice set because it gives no positive root of (14).

The posterior variances (8), (10), (12), the gain (15), the price coefficients (C1)–(C4), the cost of capital (C12), volatility (C13) and performance (21) are taken as closed-form definitions. Their CARA-normal derivation (Bayes' rule, market clearing, certainty equivalents) is not formalized. Equilibria are defined relationally: a feasible tuple whose profit is at least that of every feasible tuple, with no choice functions.

The goal concludes, rather than assumes, that the equilibrium clarities are finite. It quantifies over every equilibrium at each cost level. It does not define the equilibrium through the $\tau_\eta=\infty$ economy or through the paper's expansions, which would replace the theorem by its heuristic.

A complete development needs real analysis only: the intermediate value theorem, monotonicity, compactness on $(0,\infty]$, and asymptotics in $1/\tau_\eta$. Contributions are welcome on any milestone, on an independent proof of Proposition 4's $\Delta=0$ counterpart, and on a formal derivation of the closed forms from Gaussian conditioning and CARA utility, which would be reusable for other rational-expectations models.

Selected references

• S. Huang, Y. Xiong, L. Yang, Skill Acquisition and Data Sales, Management Science 68(8), 2022; working paper version of July 2019. https://doi.org/10.1287/mnsc.2021.4117
• S. J. Grossman, J. E. Stiglitz, On the Impossibility of Informationally Efficient Markets, American Economic Review 70(3), 1980. https://www.jstor.org/stable/1805228
• A. R. Admati, P. Pfleiderer, A Monopolistic Market for Information, Journal of Economic Theory 39(2), 1986. https://doi.org/10.1016/0022-0531(86)90049-3
• A. R. Admati, P. Pfleiderer, Direct and Indirect Sale of Information, Econometrica 58(4), 1990. https://doi.org/10.2307/2938330
• N. Gârleanu, L. H. Pedersen, Efficiently Inefficient Markets for Assets and Asset Management, Journal of Finance 73(4), 2018. https://doi.org/10.1111/jofi.12696