Operations Research

Motivation

New brand-name drugs, in particular biologics, are expensive. Their benefit is also uncertain: a given patient cannot know in advance whether the treatment will work for her. Outcome-based pricing (also called performance-based or risk-sharing agreements) responds to this. The manufacturer is paid only when the treatment reaches a pre-specified goal and rebates the price otherwise. Agreements of this kind between manufacturers and payers have been signed for cholesterol, diabetes and oncology drugs. Carlson et al. (2010) give a taxonomy. Whether such a contract actually helps the parties that must agree to it is a question about incentives. It cannot be settled by noting that the patient bears less risk.

E. Adida (Management Science, 2021; accepted manuscript at eScholarship) studies it in a three-stage game between a monopolist firm, a payer and risk-sensitive patients. The patients follow prospect theory (Kahneman and Tversky 1979; Tversky and Kahneman 1992). The paper's headline result is that, in the region where the payer covers the drug under both systems, the firm and the payer typically disagree about outcome-based pricing. A side payment from the firm to the payer can make both strictly better off, but only for high-risk drugs. This mission formalizes that result and the chain of equilibrium computations that leads to it.

Setting

There are $n > 0$ patients with values $V \sim \mathrm U[0,\bar v]$, $\bar v > 0$, a unit cost $c > 0$, a co-insurance rate $\beta \in (0, 1/2]$ and a success probability $q \in (0,1)$. On success the payer gains a fixed surplus $v' \ge 0$. The game has three stages.

1. The firm announces a price $p \ge 0$.
2. The payer decides whether to cover the drug. With coverage a buyer pays the share $\bar\beta = \beta$ of the price and the payer pays $1-\beta$; without coverage $\bar\beta = 1$.
3. Each patient observes her value $v$ and buys iff her expected prospect-theory welfare is non-negative. Her value function is $u(x) = x^\alpha$ for $x \ge 0$ and $u(x) = -\lambda(-x)^\alpha$ for $x < 0$, with $0 < \alpha < 1$ and $\lambda \ge 1$.

Under uniform pricing the price is paid on every purchase, and the buyer's welfare is $q\,u(v-\bar\beta p) + (1-q)\,u(-\bar\beta p)$. Under outcome-based pricing it is paid only on success, and the welfare is $q\,u(v-\bar\beta p)$. Demand is $n/\bar v$ times the measure of buyers in $[0,\bar v]$. The firm earns $p - c$ per buyer under uniform pricing and $qp - c$ under outcome-based pricing. The payer's objective $W_{\text{payer}}$ is its own expected payoff plus the patients' total expected (risk-neutral) payoff. It covers iff its objective with coverage is at least its objective without. An equilibrium price maximizes the firm's realized profit, with the payer's coverage response, over all $p \ge 0$.

Let

$$z = 1 + \Big(\lambda\frac{1-q}{q}\Big)^{1/\alpha},\qquad q_0 = \frac{1}{1+\lambda^{-1/(1-\alpha)}} .$$

A drug is high-risk if $q < q_0$ and low-risk if $q > q_0$; the risk premium $qz - 1$ is positive exactly for high-risk drugs. Assumption 1 is $\beta c/\bar v < \min\{q, 1/z\}$. Assumption 2 is

$$v' \ge \tilde p^*(1-\beta/2) - \bar v/2 \quad\text{and}\quad \big(q \le q_1 \ \text{or}\ v' \ge p^*(1/q - z\beta/2) - \bar v/2\big),$$

with $p^* = c/2 + \bar v/(2\beta z)$, $\tilde p^* = c/(2q) + \bar v/(2\beta)$, and $q_1$ the solution of $zq = 2/\beta$. It is the region of large payer benefit, in which both systems end in coverage. Finally,

$$M' = \frac{\bar v}{2}\Big(\frac{\bar v}{z\beta^2c} - 1\Big) + \frac{\beta c\,(2/\beta - 1 - zq)}{4q}.$$

Formalization targets

Goal: Proposition 4

Under Assumptions 1 and 2, let $p^U$ and $p^O$ be equilibrium prices, and write $\Delta\Pi = \Pi^O_{\text{firm}}(p^O) - \Pi^U_{\text{firm}}(p^U)$ and $\Delta W = W^O_{\text{payer}}(p^O) - W^U_{\text{payer}}(p^U)$. Then

$$v' > M' \ \Longrightarrow\ \big(\Delta\Pi > 0 \iff \Delta W > 0\big)\ \wedge\ \big(\Delta\Pi < 0 \iff \Delta W < 0\big),$$ $$v' < M' \ \Longrightarrow\ \Big(\exists\,\tau:\ \Pi^U_{\text{firm}} < \Pi^O_{\text{firm}} - \tau\ \wedge\ W^U_{\text{payer}} < W^O_{\text{payer}} + \tau\Big) \iff q < q_0,$$

and, if $v' < M'$ and $q < q_0$, $0 < -\Delta W < \Delta\Pi$: every transfer strictly between the two amounts, which runs from the firm to the payer, works.

Milestones

In attack order:

• the purchase rules ($v \ge \bar\beta pz$, resp. $v \ge \bar\beta p$) and the closed forms of demand and payer objective;
• Lemma 1 ($1/z > q \iff q > q_0$ away from $q_0$ and $1$) and the shape of $q \mapsto zq$;
• the coverage rules, Propositions 1 and 2;
• the equilibrium prices, Theorem 1 part 1 ($p^*$) and Theorem 2 part 1 ($\tilde p^*$), and their combination under Assumption 2;
• the firm and payer comparisons, Proposition 3 parts 3 and 6, with the identities $\Delta\Pi = \frac{n}{4\bar v\beta}(qz-1)\big(\frac{\bar v^2}{z} - \frac{c^2\beta^2}{q}\big)$ and $\Delta W = \frac{n\beta c}{2\bar v}(qz-1)(v'-M')$;
• the joint-surplus identity of the proof of Proposition 4 and the positivity of its bracket.

Significance

Proposition 4 says that for a high-risk drug outcome-based pricing raises total firm-plus-payer surplus, even where it hurts the payer. A negotiated side payment therefore always exists that makes both parties prefer it. For a low-risk drug no such payment exists, because the payer's gain is smaller than the firm's loss. The result locates where outcome-based contracts can be self-enforcing and identifies the risk premium $qz - 1$ as the quantity that decides it. In this model the patients' loss aversion $\lambda$ and risk sensitivity $1-\alpha$ act on the comparison only through $z$ and $q_0$.

The paper proves the result with explicit algebra once the equilibrium is pinned down. The formalization adds two things. First, the equilibrium layer is checked, not assumed: the statements quantify over the backward-induction equilibrium prices, with an explicit payer coverage rule and an integral model of demand. The closed forms and the unique optima $p^*$, $\tilde p^*$ become theorems. Second, the formalization makes the small hypotheses explicit (positivity of $c$, non-negativity of $v'$, strict versus weak improvement), which the published proof uses without listing. As far as is known, none of these results has a machine-checked proof.

Difficulty

The algebra of Propositions 3 and 4 is short once $p^U = p^*$ and $p^O = \tilde p^*$ with coverage are established. The work is in establishing them. The firm's realized profit is a discontinuous function of the price, because the payer's coverage decision switches at the thresholds $p_1$, $p_2$, $\bar p_1$, $\bar p_2$, which depend on the regime of $q$. Showing that $p^*$ is the unique global maximizer requires comparing the covered and uncovered profit curves on every piece. It uses Assumption 1, the bound $\beta \le 1/2$ (which places $p^*$ above $\bar v/z$ and $\tilde p^*$ above $\bar v$), and the monotonicity of $zq$ through the root $q_1$ of $zq = 2/\beta$. Reading the closed forms off the paper's formulas is not enough: they must be derived from the purchase rule, which itself rests on the prospect-theory inequality $(v - \bar\beta p)^\alpha \ge \lambda\frac{1-q}{q}(\bar\beta p)^\alpha$. A natural shortcut is to state Proposition 4 at $p^*$ and $\tilde p^*$ directly. That deletes the equilibrium content and is not the goal.

Formalization scope

All quantities are real numbers in one structure Params with a Standing predicate: $n, \bar v, c > 0$, $0 < \beta \le 1/2$, $0 < q < 1$, $0 < \alpha < 1$, $\lambda \ge 1$, $v' \ge 0$. Two of these are added to the page's assumptions: $c > 0$ ($M'$ divides by $c$) and $v' \ge 0$ (used in the proof of Theorem 1).

Powers are Real.rpow on non-negative bases only. The roots $q_1$ (of $zq = 2/\beta$), $\bar q_1$ (of $zq = 1/\beta$) and $q_2$ (of $zq = 2/(1+\beta)$) are passed as numbers together with their defining equation on $(0,1)$; uniqueness is a milestone. Demand and patient payoff are a Lebesgue measure and a set integral over the buyers in $[0,\bar v]$. Ties follow the paper: an indifferent patient buys, and an indifferent payer covers. "The firm prices at $p^*$" is read as "$p^*$ is the unique equilibrium price". "Better for both parties" is read as strict improvement, and the paper's closed range of transfers is replaced by the open range, because at its endpoints one party is only indifferent. The payer's side of every comparison is its objective $W_{\text{payer}}$.

A formalization that fixes $p^U = p^*$ and $p^O = \tilde p^*$ by hypothesis, or takes the closed forms as definitions, would make the goal an algebraic identity. The goal here quantifies over all equilibrium prices of the integral model.

A complete development needs elementary real analysis (convexity and monotonicity of $q \mapsto zq$, rpow manipulations), Lebesgue measure and integrals over intervals, and piecewise maximization of concave quadratics. The prospect-theory value function and the threshold purchase rule are reusable for other behavioral pricing models. Proofs of any milestone are welcome, as are proofs of the omitted parts of Theorems 1 and 2 (the constrained prices $p_1$, $p_2$, $\bar p_1$, $\bar p_2$).

Selected references

• E. Adida, Outcome-based pricing for new pharmaceuticals via rebates, Management Science 67(2), 2021. https://doi.org/10.1287/mnsc.2019.3574 (accepted manuscript: https://escholarship.org/uc/item/0702h9wp)
• D. Kahneman, A. Tversky, Prospect theory: An analysis of decision under risk, Econometrica 47(2), 1979. https://doi.org/10.2307/1914185
• A. Tversky, D. Kahneman, Advances in prospect theory: Cumulative representation of uncertainty, Journal of Risk and Uncertainty 5(4), 1992. https://doi.org/10.1007/BF00122574
• J.J. Carlson, S.D. Sullivan, L.P. Garrison, P.J. Neumann, D.L. Veenstra, Linking payment to health outcomes: A taxonomy and examination of performance-based reimbursement schemes between healthcare payers and manufacturers, Health Policy 96(3), 2010. https://doi.org/10.1016/j.healthpol.2010.02.005
• G.P. Cachon, M.A. Lariviere, Supply chain coordination with revenue-sharing contracts: Strengths and limitations, Management Science 51(1), 2005. https://doi.org/10.1287/mnsc.1040.0215

Motivation

The circular economy movement argues that manufacturers should keep control of their products after use (by leasing instead of selling) and design them so that worn parts can be replaced individually (a modular architecture). Each of the two levers has a long literature in operations management and economics. Leasing versus selling durable goods is studied in models of durable goods with secondary markets (Desai & Purohit 1998; Agrawal, Ferguson, Toktay & Thomas 2012), and modularity in the product-design literature, where its value lies in replacing modules independently. Agrawal, Atasu and Ülkü (Management Science) ask whether the two levers reinforce each other: when is leasing a modular product strictly the most profitable of the four combinations of business model and architecture? Their answer (Proposition 3) is a closed-form partition of the parameter space by cost thresholds, and it shows that the combination is optimal only under limited conditions.

Setting

A monopolist offers a durable product made of two modules, each with a useful life of two periods; module 1 is the more durable one. A customer of type $\theta$, uniform on $[0,1]$, values a new product at $\theta$ per period. Under selling, a used module $k$ retains a fraction $\delta_k$ of its value; under leasing, off-lease modules retain $\delta_{kl}=\gamma\delta_k$, where $\gamma>0$ is the relative return condition ($\gamma<1$: off-lease products are in worse shape than previously sold ones; $\gamma>1$: in better shape). Each module costs $c$ to produce. The standing assumptions are

$$0<\delta_2<\delta_1<1,\qquad \gamma\delta_1<1,\qquad 0<c<\tfrac{1-\delta_2}{2},\qquad c<\tfrac{1-\gamma\delta_2}{2}.$$

In steady state the firm solves one of four quadratic problems, each written in quantities through inverse demand functions derived from customer self-selection and secondary-market clearing:

• SI (sell integral): choose $S_n\ge0$ new products, profit $\Pi_{SI}=(p_n(S_n)-2c)S_n$.
• SM (sell modular): choose $0\le S_{n1}\le S_{n2}$ new first and second modules; $S_{n2}-S_{n1}$ is the UN segment of customers who keep a used first module and buy a new second one.
• LI (lease integral): choose $0\le L_u\le L_n$ used and new leases.
• LM (lease modular): choose $L_{nn},L_{un},L_{uu}\ge0$ new, blended and used leases, with the supply constraint $L_{uu}+L_{un}\le L_{nn}$.

The optimal profits $\Pi^*_{SI},\Pi^*_{SM},\Pi^*_{LI},\Pi^*_{LM}$ are the attained maxima of these problems. The paper's thresholds are explicit functions of $(\delta_1,\delta_2,\gamma)$:

$$C_{SM}=\frac{(1-\delta_2)(\delta_1+\delta_2)}{3\delta_1+5\delta_2},\qquad C_{LM2}=\frac{(1-\gamma\delta_2)(\delta_1+\delta_2)}{3\delta_1+5\delta_2},$$

together with $C_{LI}$, $C_{LM1}$, and the square-root expressions $C_I$, $C_M$ of the Appendix.

Formalization targets

Goal: Proposition 3

With ties between architectures broken towards the integral one (footnote 13 of the paper):

• if $\gamma\le1$: the firm leases a modular product for $c<C_M$, sells a modular product for $C_M\le c<C_{SM}$, and sells an integral product for $c\ge C_{SM}$;
• if $\gamma>1$: the firm leases a modular product for $c<C_{LM2}$ and leases an integral product otherwise.

In each region the chosen option's optimal profit strictly exceeds the others, except at exact ties of the model. These are $\Pi^*_{SM}=\Pi^*_{SI}$ for $c\ge C_{SM}$, $\Pi^*_{LM}=\Pi^*_{LI}$ for $\gamma>1$, $c\ge C_{LM2}$, and at $\gamma=1$ further ties between leasing and selling. The goal states these as equalities or weak inequalities and restores strictness for $\gamma<1$.

Milestones

1. The closed forms of $\Pi^*_{SI}$, $\Pi^*_{SM}$, $\Pi^*_{LI}$ and $\Pi^*_{LM}$, the last in three cost regimes.
2. Lemma 1: under selling, modularity strictly pays (and a UN segment is served) iff $c<C_{SM}$, equivalently $\delta_2<D_S(\delta_1,c)$.
3. Lemma 2: under leasing, modularity strictly pays (and blended products are leased) iff $c<C_{LM2}$, equivalently $\delta_2<D_L(\delta_1,\gamma,c)$; and $C_{LM1}<C_{LI}<C_{LM2}$.
4. Lemma 3 and its converse: under architecture $j\in\{I,M\}$, leasing beats selling if $\gamma>1$ or $c<C_j$, and for $\gamma<1$ selling beats leasing iff $c>C_j$.
5. Proposition 2, $C_M<C_I$ for $\gamma<1$, and the threshold ordering $C_M<C_I<C_{SM}\le C_{LM2}$ for $\gamma\le1$.
6. The comparative statics of Proposition 3: $C_M$ increases in $\gamma$; $C_{SM}$ and $C_{LM2}$ increase in $\delta_1$ and decrease in $\delta_2$; $C_{LM2}$ decreases in $\gamma$.

Significance

The result gives a complete description of the firm's joint choice in a standard durable-goods model with a secondary market, and it qualifies a common claim. Leasing a modular product is strictly optimal only at low production cost. For $\gamma<1$ modularity can even push a leasing firm to selling (Proposition 2), and for $\gamma>1$ the firm never sells. The thresholds feed the paper's later environmental and consumer-surplus comparisons.

The paper's proofs are pencil-and-paper KKT computations reported in compressed form, and nothing in the paper is machine-checked. A formalization would certify the four closed-form optima, every threshold comparison, and the case split of Proposition 3. It would also settle two printing errors found while preparing this mission (see below), one of which changes the statement of Lemma 2 and Proposition 3.

Difficulty

Each firm problem is a strictly concave quadratic program over a polyhedral cone, so existence of the optimum is routine. The difficulty is everything after that. The optimum changes face as $c$ moves: LM alone has four KKT cases, and each must be shown to be optimal exactly on its cost interval. The profit comparisons then reduce to sign conditions on rational functions of four parameters. Some involve the square roots in $C_I$ and $C_M$, which are only meaningful for $\gamma\le1$ and are defined as roots of quadratics in $c$, so the comparisons must be placed relative to them. The ordering $C_M<C_I<C_{SM}\le C_{LM2}$ is an inequality between such expressions on the whole parameter region. It is not a symbolic identity, and checking it at sample points proves nothing.

Formalization scope

• Parameters are a record $(\delta_1,\delta_2,\gamma,c)$ of reals with the standing assumptions as a predicate. The positivity of $c$ is made explicit: at $c=0$, $\Pi^*_{LM}=\Pi^*_{LI}$ and the lease-modular region degenerates. $\alpha=1/2$, $c_1=c_2=c$ and the discount factor $\rho=1$ are fixed, as in the paper's main model.
• The four problems use the inverse demand functions and feasible sets of §4 and the Appendix. The SM feasible set $0\le S_{n1}\le S_{n2}$ covers both regimes of the Appendix (on the diagonal the profit is the no-UN profit). The LM problem is the three-product problem of §4.4, with the NU product already excluded.
• An optimal profit is a value $v$ with IsGreatest (profit '' feasible) v, never a supremum without attainment. Statements about the optimizer ("the UN segment exists", "$L_{un}>0$") quantify over every optimal decision.
• Thresholds are the printed closed forms, with Real.sqrt for $C_I$, $C_M$, $D_S$, $D_L$. $C_I$ and $C_M$ are used only for $\gamma\le1$, where their radicands are nonnegative.
• Corrections. (i) The Appendix prints $C_{LM2}$ with an extra factor $\gamma$ in the denominator. The mission uses $(1-\gamma\delta_2)(\delta_1+\delta_2)/(3\delta_1+5\delta_2)$, which the paper's own Case 4 multiplier, its printed difference $C_{LI}-C_{LM2}$ and its $D_L$ all require. With the printed form Lemma 2 and Proposition 3 are false for $\gamma\ne1$. (ii) The SI inverse demand on p. 31 prints $-2S_n(1+\delta_1+\delta_2)$; the printed optimum belongs to $-2S_n(\delta_1+\delta_2)$, which is used. (iii) "if and only if $\gamma>1$" in the summary of the proof of Lemma 3 is read as $\gamma<1$, the case the proof treats.
• Defining the optimal profits as their closed forms, or the thresholds as the crossing points of the profits, would make the goal and the lemmas hold by definition. The mission rules out both: profits are optima of the stated problems, and thresholds are explicit formulas.
• Needed infrastructure: maximization of concave quadratics on polyhedral cones (KKT for linear constraints), and real-algebraic sign arguments with square roots. Lemmas for the four optima and for the threshold inequalities are reusable across the milestones and welcome as separate contributions.

Selected references

• V. V. Agrawal, A. Atasu, S. Ülkü, Leasing, Modularity, and the Circular Economy, Management Science, 2021 (author manuscript of 2020-08-23 used here). https://doi.org/10.1287/mnsc.2020.3829
• P. Desai, D. Purohit, Leasing and Selling: Optimal Marketing Strategies for a Durable Goods Firm, Management Science 44(11), S19–S34, 1998. https://doi.org/10.1287/mnsc.44.11.S19
• V. V. Agrawal, M. Ferguson, L. B. Toktay, V. M. Thomas, Is Leasing Greener Than Selling?, Management Science 58(3), 523–533, 2012. https://doi.org/10.1287/mnsc.1110.1428

Motivation

Manufacturers of products with fixed shelf lives must decide both how much to send from a warehouse to a store and which age cohorts to send. A shipment can reduce expiry at the warehouse while changing the age mix seen by shoppers at the store. In the two-echelon system studied by Akkaş and Honhon, the store does not control which items each shopper takes: some shoppers select older items first and the remainder select newer items first. The resulting waste at the warehouse and store can move in different directions when the manufacturer changes a shipment. The paper uses this setting to ask whether ship oldest first (SOF), a simple age-selection rule, minimizes waste over an infinite horizon. Akkaş and Honhon, SSRN manuscript.

The paper reports an inventory-age audit of a consumer packaged goods supplier and then studies the shipment decision analytically. Its Theorem 1 separates warehouse waste from the sum of warehouse and store waste. The former has a specified SOF policy that ships in full; the latter has an SOF age-selection rule but allows the shipped quantity to vary with the state. This mission formalizes those two claims, with a correction to one printed clause described below. Akkaş and Honhon, §3 and Theorem 1.

Setting

A unit remains saleable for $N$ periods, where $N\ge1$. At the start of a period the warehouse holds $x_i$ units of age $i$, and the store holds $y_i$ units of that age, for $i=1,\ldots,N-1$. Both age-zero entries are zero before replenishment. A plant then delivers fresh units so the warehouse's total post-replenishment stock reaches the exogenous order-up-to level $S^W$. Thus its age-zero stock is $x^{\mathrm{post}}_0=S^W-\sum_{i=1}^{N-1}x_i$. The manufacturer sends $q_i$ units of age $i$ from the warehouse to the store, subject to warehouse availability and the store's shelf capacity $L$. In particular, $q_i\le x^{\mathrm{post}}_i$ and $\sum_iq_i+\sum_i y_i\le L$. Akkaş and Honhon, §4.1, pp. 10–13, and §4.2, p. 15.

The period's shopper population is $\lambda$. A fraction $\gamma\in[0,1]$ selects inventory first in, first out (FIFO), meaning older units first; the remaining shoppers select it last in, first out (LIFO), meaning newer units first. The discrete FIFO population is $\lceil\gamma\lambda\rceil$. If $z_i=y_i+q_i$ is the store stock after delivery, the paper's age-specific demand is

$$D_i(z,\lambda;\gamma)=\left(\lceil\gamma\lambda\rceil-\sum_{j>i}z_j\right)^+ +\left(\lambda-\lceil\gamma\lambda\rceil-\sum_{j<i}z_j\right)^+.$$

Here $u^+=\max(u,0)$. Only units of age $N-1$ expire at the end of the period. Warehouse waste is $W^W=x^{\mathrm{post}}_{N-1}-q_{N-1}$, store waste is $W^R=(z_{N-1}-D_{N-1})^+$, and total waste is $W=W^W+W^R$. The remaining units advance one age before the next period. An SOF shipment uses a younger unit only when every older available unit has been shipped. An SOF shipment in full fills the remaining store space or ships the entire available warehouse stock. Akkaş and Honhon, §4.1, pp. 11–12, and §4.2.1, p. 15.

Formalization targets

Warehouse waste

Let $\overline W^{W,+}$ and $\overline W^{W,-}$ denote the upper and lower limits of expected Cesàro averages of warehouse waste. The first sentence of Theorem 1 is the mission's sole milestone:

$$\overline W^{W,+}(\mathrm{SOF\text{-}full};s_0) \le \overline W^{W,-}(\sigma;s_0) \quad\text{for every feasible initial state }s_0\text{ and every admissible policy }\sigma.$$

Total waste and mission goal

The full goal also asserts that one stationary, feasible SOF policy $f$ minimizes total waste from every feasible initial state:

$$\exists f\;\text{stationary and SOF},\qquad \overline W^+(f;s_0)\le\overline W^-(\sigma;s_0) \quad\text{for all feasible }s_0\text{ and admissible }\sigma.$$

The policy $f$ chooses its shipping quantity from the current state; the theorem does not prescribe shipping in full for this second objective. These are waste objectives, independent of the paper's separate revenue, labor, and expiration-cost parameters. Akkaş and Honhon, Theorem 1, p. 15.

Significance

The warehouse result identifies a fixed, implementable shipment rule for minimizing waste at that location across the paper's whole FIFO/LIFO range. The total-waste result says that optimal age selection can remain SOF even when the quantity decision must respond to the store inventory and shopper behavior. Together they distinguish the two decisions in a setting where moving an expiring unit out of the warehouse can merely move the expiry to the store. The paper later uses its waste comparison in the analysis of profit policies under additional cost assumptions. Akkaş and Honhon, Appendix A.2–A.3.

The theorem is a published paper result, but this mission starts with open Lean statements rather than a machine-checked proof. A complete development would provide a reusable formal model of age-structured two-echelon inventory, stochastic shopper depletion, feasible shipment policies, and long-run waste criteria. The general controlled-process and Cesàro-average definitions can also support other finite inventory models.

Difficulty

An age-selection decision changes the stock carried into future periods, and a quantity decision changes the next warehouse replenishment. A comparison of immediate waste therefore does not by itself compare long-run averages. In particular, simply reordering each shipment to send older units first while keeping its quantity fixed can increase later warehouse waste for some policies; it cannot serve as an unrestricted policy-level argument. The store's FIFO/LIFO mixture introduces another intertemporal effect because a shipped younger unit can be sold ahead of an older one. Akkaş and Honhon, Appendix A.1, Appendix p. 1.

Formalization scope

Lean uses finite age vectors indexed by Fin N, natural-number stocks and shipments, a real $\gamma$ constrained to $[0,1]$, and an arbitrary probability mass function for shopper population. The standing condition $N\ge1$ makes the final age cohort defined; $S^W=0$ and $L=0$ remain allowed. Demand samples are independent and identically distributed across periods, as in the stationary transition model of §4.2. Policies are time-dependent deterministic Markov rules: at period $t$ they choose a shipment from the current inventory state. This is the finite-state class used by the paper's dynamic program. The comparison includes every feasible rule in that class, every feasible initial state, and a common stationary SOF witness for total waste; it does not restrict competitors to SOF or full shipments. Standard finite-MDP results explain why stationary deterministic optimal policies suffice among broader history-dependent randomized classes. Puterman, Markov Decision Processes, Theorem 9.1.8.

Costs and expectations live in $[0,\infty]$, and long-run criteria use upper and lower limits of expected Cesàro averages. The paper prints a plain limit without specifying what happens when a policy's average fails to converge. The upper-versus-lower comparison states the stronger optimality claim without relying on that convergence. Lean time starts at zero. Natural-number subtraction implements the paper's positive-part operation, and the post-replenishment stock formula is used only for feasible states. The model follows the printed balance equations when discarding the final-age store stock, despite a tension with the narrative timing of expired-unit pickup.

Three transcription corrections are explicit. The demand formula's sums use $z_j$, the running index, where the page prints $z_i$; the action sum runs through age $N-1$; and the waste objectives are minimized despite a printed “max” in §4.2.1. More consequentially, Theorem 1's last clause says shipping is in full under pure FIFO. This is false and is omitted: for $\gamma=1$, $N=2$, $S^W=1$, $L=2$, and a Bernoulli$(1/2)$ shopper population, SOF in full has average total waste $1/2$ while an SOF policy that holds stock back attains $1/4$. The formal goal neither assumes this clause nor asserts its negation. Its feasible-policy and feasible-initial-state quantifiers rule out vacuous or artificially easy readings.

A complete proof may need finite-state inventory invariants, admissibility of the SOF-in-full rule, comparisons of age profiles over time, and results about average costs of controlled chains. Contributions establishing those reusable facts, or the stated warehouse and total-waste targets, are within scope. The separate profit theorems and numerical studies of the paper are outside this mission.

Selected references

• Akkaş, A., and D. Honhon. Shipment Policies for Products with Fixed Shelf Lives: Impact on Profits and Waste. Authors' SSRN manuscript 3247290, 2021; published in Manufacturing & Service Operations Management. SSRN manuscript; journal DOI.
• Puterman, M. L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994. DOI.

Why consumers read the posts that agree with them

Online platforms show a reader many short signals about the same question (posts, headlines, tweets), more than the reader can absorb. The reader screens the menu and consumes only a few items. Allon, Drakopoulos and Manshadi (Information Inundation on Platforms and Implications, SSRN 3385627; Operations Research, 2021, doi:10.1287/opre.2021.2119) ask what a purely information-seeking reader picks when the accuracy of each post is unknown. Their answer, Proposition 1, is that she picks the post closest to her current belief, the effect the paper calls screening bias. It is the mechanism behind the paper's later results on slow learning and polarization, and it explains a pattern resembling confirmation bias without assuming any bias in how beliefs are updated. Confirmation bias was documented empirically by Lord, Ross and Lepper (1979) and modelled through source reputation by Gentzkow and Shapiro (2006) and Suen (2004). In those models the bias comes from repeated interaction with strategic sources; here it comes from a single screening decision by a Bayesian reader.

The screening model

An unknown fact is a real number $\theta$. A post is a noisy observation

$$Z=\theta+\Sigma\,\epsilon,$$

where $\epsilon\sim\mathcal N(0,1)$ and the accuracy $\Sigma$ (a standard deviation) is drawn independently from a publicly known law $\mathbb G$. The paper assumes throughout (§3, p. 8) that $\mathbb G$ is a probability law whose support lies in an interval $[\underline\sigma,\overline\sigma]$ with $0<\underline\sigma\le\overline\sigma$.

A consumer holds a normal belief $\mathcal N(\mu,s^2)$ about $\theta$, with $s>0$. From her point of view, a post of accuracy $\sigma$ is distributed $\mathcal N(\mu,\sigma^2+s^2)$, so its likelihood is

$$P(Z\mid\sigma;\mu,s)=\psi\big((Z-\mu)^2,\sqrt{2(\sigma^2+s^2)}\big),\qquad\psi(x,y)=\frac{1}{\sqrt\pi\,y}e^{-x/y^2}.\tag{5}$$

By Bayes rule (4), her posterior on the accuracy after seeing the post value $Z$ has density proportional to $P(Z\mid\sigma;\mu,s)$ with respect to $\mathbb G$; write $\mathbb E[\,\cdot\mid Z;\mu,s]$ for the posterior expectation.

If she reads a post and learns its accuracy $\sigma$ (ex-post known accuracy), her belief becomes normal with standard deviation $s'(\sigma)=\sqrt{s^2\sigma^2/(s^2+\sigma^2)}$ (Belief Updating Equations). Before reading, she scores each post by the expected reduction of her uncertainty. The Screening Equation prints the score as

$$S_{\mathrm{sd}}(Z)=s-\mathbb E\big[s'(\Sigma)\mid Z;\mu,s\big],$$

while the text calls it the expected decrease in posterior variance, $S_{\mathrm{var}}(Z)=s^2-\mathbb E[s'(\Sigma)^2\mid Z;\mu,s]$. A menu is a finite list $Z_1,\dots,Z_K$ of post values, and she picks a post in the argmax of the score.

In Lean the model lives in InfoInundation.Screening.Model: AccuracyLaw G (the standing assumption), psi, likelihood, postExp (the Bayes ratio), nextSd, sdScore, varScore, argmaxMenu, closestPosts, and the auxiliary moments auxMoment/auxExp used in the proof.

Formalization targets

Goal: Proposition 1 (p. 10)

For every accuracy law $\mathbb G$ satisfying the standing assumption, every belief $(\mu,s)$ with $s>0$ and every menu $Z_1,\dots,Z_K$:

(a) if $\mathbb G$ is not a point mass,

$$\operatorname*{arg\,max}_{i}S(Z_i)=\operatorname*{arg\,min}_{i}(Z_i-\mu)^2\quad\text{for }S=S_{\mathrm{sd}}\text{ and for }S=S_{\mathrm{var}};$$

(b) if $\mathbb G=\delta_\sigma$ with $\sigma>0$, the argmax of both scores is the whole menu.

Milestones

The proof on pp. 10–11 has no numbered lemmas; the milestones are its labelled steps:

1. (5): given $\Sigma=\sigma$, the post is $\mathcal N(\mu,\sigma^2+s^2)$ and its density is the $\psi$ expression.
2. (4): in the joint model $(\theta,\Sigma,\epsilon)$, the Bayes ratio is a version of $\mathbb E[h(\Sigma)\mid Z]$.
3. (3): $S_{\mathrm{var}}(Z)=s^4\,\mathbb E[(s^2+\Sigma^2)^{-1}\mid Z]$.
4. Auxiliary density (p. 11): $\mathbb E[(\Sigma^2+s^2)^{-1}\mid Z]=\mathbb E_g[(\Sigma^2+s^2)^{-3/2}]/\mathbb E_g[(\Sigma^2+s^2)^{-1/2}]$, with $g\propto d\mathbb G(\sigma)\,e^{-(Z-\mu)^2/(2(\sigma^2+s^2))}$.
5. Cauchy–Schwarz (p. 11): $\mathbb E_g[w^{3/2}]^2\le\mathbb E_g[w^{5/2}]\,\mathbb E_g[w^{1/2}]$ with $w=(\Sigma^2+s^2)^{-1}$, strict when $\mathbb G$ is not a point mass.
6. Derivative display (p. 11): the derivative in $r=(Z-\mu)^2$ of the ratio in 4, and its sign.
7. Monotonicity (p. 10): $\mathbb E[(s^2+\Sigma^2)^{-1}\mid Z]$ is non-increasing in $(Z-\mu)^2$, strictly decreasing when $\mathbb G$ is not a point mass.
8. Part (b) (p. 10): for $\mathbb G=\delta_\sigma$ both scores are constant in $Z$.

Significance

Proposition 1 turns a modelling choice (each reader maximizes expected information) into a behavioural prediction (each reader consumes the post nearest her belief). Every later result of the paper is built on it: the slow-learning theorem, in which the speed of learning decreases with menu size, and the multimodal belief distribution, both come from feeding the closest post back into the belief dynamics. Part (b) is the benchmark: with known equal accuracy there is no screening bias, and learning is fast.

The result is proved in the paper; it has no machine-checked proof. The mission produces one, and with it a small reusable library on posteriors over a Gaussian scale mixture: the predictive density of a normal belief under a known noise scale (milestone 1), a measure-theoretic Bayes rule for the noise scale given one observation (milestone 2), and moment inequalities under exponentially tilted mixing laws (milestones 5–6). The formalization also settles two points that the printed proof leaves open (see Difficulty): which of the two scores the conclusion holds for, and why the conclusion is an equality of sets rather than an inclusion.

Difficulty

The proof covers the variance score. Reducing it to the monotonicity of $r\mapsto\mathbb E[(\Sigma^2+s^2)^{-1}\mid Z]$ in $r=(Z-\mu)^2$ is algebra. The monotonicity itself requires differentiating a ratio of $\mathbb G$-integrals under the integral sign, for an arbitrary law $\mathbb G$, which in turn needs the boundedness of the support to dominate the integrands.

Three places need more than the printed argument:

• Strictness. The page shows the derivative is $\le0$. That gives only "the closest posts are among the maximizers"; the claimed equality of argmax and argmin needs strict decrease, hence the equality case of Cauchy–Schwarz, which uses that the support of $\mathbb G$ lies in $(0,\infty)$. Without that standing bound, $\mathbb G=\tfrac12\delta_{-1}+\tfrac12\delta_1$ is not a point mass yet every post has the same score.
• The printed score. The standard-deviation score $S_{\mathrm{sd}}$ is not an affine function of $\mathbb E[(s^2+\Sigma^2)^{-1}\mid Z]$, so steps (3)–(7) do not cover it. It needs the posterior expectation of the increasing function $\sigma\mapsto s'(\sigma)$ to increase strictly in $(Z-\mu)^2$, a statement the paper does not prove.
• The derivative display omits a factor $\tfrac12$; the sign is unaffected.

Formalization scope

• All quantities are real; $\mathbb G$ is a Measure ℝ with AccuracyLaw G: a probability measure with $\mathbb G([\underline\sigma,\overline\sigma]^{\mathrm c})=0$ for some $0<\underline\sigma\le\overline\sigma$. "Supp($\mathbb G$) includes at least two distinct values" is ∀ σ, G ≠ Measure.dirac σ; "Supp($\mathbb G$) = {σ}" is G = Measure.dirac σ with $\sigma>0$.
• "For any consumer $x$ and time $t$" is any $\mu\in\mathbb R$ and $s>0$. Reachable states have $s\in(0,1]$, so this is a mild generalization.
• Accuracy is ex-post known ($\hat\sigma=\Sigma$ inside the expectation), which is the case the proof treats. The paper's remark that the conclusion also holds for ex-post unknown accuracy is not formalized.
• The menu is Z : Fin K → ℝ; argmax and argmin are Finset (Fin K), so posts of equal value are distinct posts, and "$=K_x(t)$" is Finset.univ.
• The goal states the conclusion for both $S_{\mathrm{sd}}$ (as printed) and $S_{\mathrm{var}}$ (as described and as proved).
• Added relative to the page, and disclosed in each item: the strict forms of milestones 5 and 7, and the factor $\tfrac12$ in milestone 6.
• No trivialization. The posterior is the Bayes ratio (4) with the Gaussian likelihood (5) for an arbitrary $\mathbb G$; neither score is defined through $(Z-\mu)^2$, and a statement in which the score is replaced by a closed form, the menu by two posts, or the set equality by an inclusion is not this goal.

Needed infrastructure: dominated differentiation of parameter-dependent integrals against a finite measure on a bounded set (Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le), the equality case of Cauchy–Schwarz in $L^2(g)$, Gaussian convolution (gaussianReal_add_gaussianReal_of_indepFun) and conditional expectation via densities for milestone 2. Contributions of a covariance or likelihood-ratio ordering lemma for the standard-deviation conjunct are welcome as supporting theorems.

Selected references

• G. Allon, K. Drakopoulos, V. Manshadi, Information Inundation on Platforms and Implications, SSRN 3385627, version of 2020-04-05. https://ssrn.com/abstract=3385627 ; Operations Research, 2021. https://doi.org/10.1287/opre.2021.2119
• M. Gentzkow, J. M. Shapiro, Media Bias and Reputation, Journal of Political Economy 114(2), 2006. https://doi.org/10.1086/499414
• W. Suen, The Self-Perpetuation of Biased Beliefs, The Economic Journal 114(495), 2004. https://doi.org/10.1111/j.1468-0297.2004.00213.x
• C. G. Lord, L. Ross, M. R. Lepper, Biased Assimilation and Attitude Polarization, Journal of Personality and Social Psychology 37(11), 1979. https://doi.org/10.1037/0022-3514.37.11.2098

Motivation

A new venture rarely knows two things at once: whether its core idea is worth anything, and whether the particular way it has chosen to bring the idea to market — its strategy — will work. A failed pilot, a disappointing A/B test or a lukewarm customer experiment can mean either, and the founder cannot tell which. Work on entrepreneurial experimentation (Kerr, Nanda and Rhodes-Kropf, Journal of Economic Perspectives, 2014, doi:10.1257/jep.28.3.25; Gans, Stern and Wu, Strategic Management Journal, 2019, doi:10.1002/smj.3010) treats testing as the main tool founders have to resolve uncertainty before they commit resources.

Agrawal, Gans and Stern (NBER Working Paper 27379, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2020.3920) give a two-period model in which a single test produces a conflated signal about the idea and the strategy together. Two consequences come out of it. A signal that the strategy is good can still lead the entrepreneur to abandon the venture. And when a mentor can sharpen a test, the better direction to sharpen it depends on the founder's prior beliefs. This mission formalizes the model and its two propositions.

Setting

The idea is worth $v>0$ (state $h$) with prior probability $p_0$, or $0$ (state $l$). Value is realized only if the strategy used is effective (state $g$, against ineffective $b$). Every strategy is effective with prior probability $e_0$, independently of every other strategy and of the idea, and there are several strategies to choose from. Implementing a strategy costs $C$ and testing one costs $c$. The standing assumptions are

$$0<p_0<1,\qquad 0<e_0<1,\qquad V_0 := e_0p_0v - C = 0,\qquad c<C,$$

where $V_0=0$ means that launching a randomly chosen strategy without testing exactly breaks even.

A test of the selected strategy has precisions $(\lambda_v,\lambda_s)\in[0,1]^2$ and emits one of four signals, $(H,G)$, $(H,B)$, $(L,G)$ or $(L,B)$:

	$h$	$l$
$g$	$(H,G)$ w.p. $1$	$(L,G)$ w.p. $\lambda_s$, $(H,B)$ w.p. $1-\lambda_s$
$b$	$(H,B)$ w.p. $\lambda_v$, $(L,G)$ w.p. $1-\lambda_v$	$(L,B)$ w.p. $1$

Write $p_1(\sigma)$ and $e_1(\sigma)$ for the posterior probabilities that the idea is high-value and that the tested strategy is effective, given signal $\sigma$. Assumption (A1), that tests are weakly informative, requires

$$p_1(H,B)\ge p_0,\quad p_1(L,G)\le p_0,\quad e_1(H,B)\le e_0,\quad e_1(L,G)\ge e_0 .$$

After the signal the entrepreneur picks one of three period-1 actions:

• implement the tested strategy, which pays $v-C$ in state $(h,g)$ and $-C$ otherwise;
• implement another randomly chosen strategy, which pays $e_0v-C$ in expectation when the idea is high-value and $-C$ when it is not;
• abandon the venture, which pays $0$.

$V_1(\sigma)$ is the best of these three conditional values. The value of testing is

$$V_0(\lambda_v,\lambda_s)=\sum_{\sigma}\Pr(\sigma)\,V_1(\sigma)-c .$$

The strategy-biased test is $(\lambda_v,1)$ and the idea-biased test is $(1,\lambda_s)$, where $(\lambda_v,\lambda_s)$ is the baseline test.

Formalization targets

Goal: Proposition 2 (p. 17)

For baseline precisions $\lambda_v,\lambda_s\in[0,1]$, if both precise tests satisfy (A1) and

$$(1-p_0)e_0(1-\lambda_s)C>(1-\lambda_v)p_0(1-e_0)(e_0v-C),$$

then

$$V_0(1,\lambda_s)<V_0(\lambda_v,1).$$

The statement leaves $p_0,e_0,v,c$ and the baseline precisions free, subject only to the standing assumptions.

Milestones

1. Bayes posteriors (§3.1, p. 9): closed forms of $p_1$ and $e_1$ after $(H,B)$ and $(L,G)$.
2. (A1) in ratio form (p. 9): for $0<\lambda_v,\lambda_s<1$, each posterior clause is equivalent to a ratio condition such as $\lambda_v/(1-\lambda_s)\ge e_0/(1-e_0)$.
3. Case 3 (p. 11): after $(H,B)$, switching to another strategy is optimal, and $V_1(H,B)=e_0p_1(H,B)v-C$.
4. Case 4 (p. 11): after $(L,G)$, abandoning is optimal and $V_1(L,G)=0$.
5. Proposition 1 (p. 12): the tested strategy is implemented only after $(H,G)$; after $(H,B)$ and $(L,G)$, switching beats implementing the tested strategy; after $(L,B)$, and after $(L,G)$ when $V_0=0$, the venture is abandoned.
6. The $V_0$ display, first line (p. 12): for every (A1) test,

$$V_0(\lambda_v,\lambda_s)=p_0e_0(v-C)+\bigl(p_0(1-e_0)\lambda_v+(1-p_0)e_0(1-\lambda_s)\bigr)V_1(H,B)-c .$$

Significance

Proposition 2 answers the question a mentor faces when it can make a test more precise in one direction only. A test with high $\lambda_s$ makes abandoning a poor idea more efficient. A test with high $\lambda_v$ makes it more efficient to continue the idea with a different strategy. The condition weighs these two benefits, and it shows that the choice is driven by the prior $(p_0,e_0)$. Proposition 1 shows why: the idea is the same in every test while the strategy can change, so switching strategies after an ambiguous signal is how the entrepreneur learns about the idea. The paper's later sections (differing priors between mentor and entrepreneur, §5.2) start from these two results.

The results are proved in the paper by hand-calculation, and Proposition 2 has no printed proof. No part of the model has been machine-checked before. The formalization produces an explicit, reusable encoding of a two-dimensional Bayesian test with a conflated signal, together with machine-checked versions of the case analysis that Proposition 1 summarizes. It also gives a checked replacement for the printed $V_0$ display: the second line of that display does not follow from the first.

Difficulty

The obvious argument reads the paper's prose, takes $V_1(L,G)=0$ and $V_1(H,B)=e_0p_1(H,B)v-C$ as given, and subtracts. In the formal model these values are optima over three actions, computed from the signal table, and each one needs an argument.

• The $(L,G)$ case is not what intuition suggests. The posterior on the tested strategy rises, yet implementing it is never profitable, because a good strategy produces $(L,G)$ only when the idea is worthless.
• At the precise tests some signals have probability zero. For example, $(H,B)$ never occurs at $(0,1)$, and the posterior $p_1(H,B)$ is undefined there. The comparison has to stay valid on that boundary.
• (A1) is weak, so several of the paper's strict inequalities hold only with equality allowed. The case analysis has to be done without them.

Formalization scope

The model lives in the namespace EntrepChoice.TestChoice. Params holds $p_0,e_0,v,C,c$. Standing collects the standing assumptions, with $V_0=0$ kept as the hypothesis $e_0p_0v-C=0$ rather than substituted. Test holds $(\lambda_v,\lambda_s)$, and Test.Valid bounds both in $[0,1]$. The states, signals and actions are small inductive types, and sums over them are written out explicitly.

Action values are unnormalized: $\Pr(\sigma)$ times the conditional expected payoff. With this choice $V_0(\lambda_v,\lambda_s)$ (testValue) needs no division. (A1) is stated cross-multiplied by $\Pr(\sigma)$. It agrees with the posterior form whenever $\Pr(\sigma)>0$ and is harmless when $\Pr(\sigma)=0$. The posteriors p1 and e1 are real quotients, equal to $0$ on a probability-zero signal.

Several conventions are disclosed readings of the paper:

• Proposition 1's second sentence is missing its verb; it is read as "is strictly better than".
• The strict inequalities that weak (A1) cannot support are stated weakly.
• Proposition 1 is posed for the baseline range $0<\lambda_v,\lambda_s<1$ of p. 7.
• The goal assumes (A1) for the two precise tests. (A1) at the baseline test implies this.
• The second printed line of the $V_0$ display is not stated.

testValue is the maximum over the three period-1 actions, built from the signal table. It is never defined by the closed form of milestone 6, and neither Standing nor A1 mentions it, so the goal cannot be closed by unfolding a definition.

Contributions are welcome on every milestone. Further results of the paper — testing order under irreversibility (§4.1), heterogeneous strategy priors (§4.2) and the mentor–entrepreneur game with differing priors (§5.2) — are natural follow-on missions on the same definitions.

Selected references

• A. K. Agrawal, J. S. Gans, S. Stern, Enabling Entrepreneurial Choice, NBER Working Paper 27379, June 2020. https://www.nber.org/papers/w27379 — published in Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3920
• J. S. Gans, S. Stern, J. Wu, Foundations of Entrepreneurial Strategy, Strategic Management Journal 40(5), 2019. https://doi.org/10.1002/smj.3010
• W. R. Kerr, R. Nanda, M. Rhodes-Kropf, Entrepreneurship as Experimentation, Journal of Economic Perspectives 28(3), 2014. https://doi.org/10.1257/jep.28.3.25

Motivation

A learner wants to locate an unknown number, the true value $v^* \in [0,1)$, by asking threshold questions of a database: each query $q$ is answered by the single bit $\mathbb I(v^* \ge q)$. Bisection finds $v^*$ to within $\epsilon/2$ with $\lceil \log_2(1/\epsilon) \rceil$ queries, and no strategy does better (Waeber, Frazier and Henderson, 2013). Bisection, however, reveals everything: each query is a function of the previous answers, so anyone who sees the queries can reconstruct the answers and hence $v^*$.

Tsitsiklis, Xu and Xu study a learner whose queries, but not the answers, are watched by an adversary. Their motivating examples (pp. 2–3) are a firm testing prices whose surveys a competitor can observe, a consumer browsing products on a platform that sees what is browsed, and an optimizer whose test points are visible to the database it queries. The question is how many queries the learner needs if she must find $v^*$ accurately while keeping the adversary uncertain about it.

The model is from the authors' COLT 2018 extended abstract and Z. Xu's master's thesis (MIT, 2017); the journal version appeared in Operations Research (2021). This mission formalizes arXiv version 3 (26 Feb 2020), and all page and theorem numbers refer to it.

Setting

The learner submits $N$ queries one at a time. A random seed $Y$, uniform on $\{1, \dots, \bar Y\}$, lets her randomize. A learner strategy $\phi$ of length $N$ consists of query maps $\phi_k$ and an estimation map $\phi^E$ (§2.1, p. 8): the $k$-th query is $q_k = \phi_k(r_1, \dots, r_{k-1}, Y) \in [0,1)$, where $r_i = \mathbb I(v^* \ge q_i)$ are the responses so far, and the estimate is $\hat x = \phi^E(r_1, \dots, r_N, Y) \in [0,1)$. The class $\Phi_N$ consists of the strategies of length $N$ that submit pairwise distinct queries. Write $\bar q(x,y)$ for the queries and $\hat x(x,y)$ for the estimate when $v^* = x$ and $Y = y$.

The adversary knows $\phi$ and sees $\bar q$. The set of query sequences that can occur when $v^* = x$ is $\mathcal Q(x) = \{\bar q(x,y) : y\}$ (eq. (1)), and the adversary's information set is

$$\mathcal I(\bar q) = \{x \in [0,1) : \bar q \in \mathcal Q(x)\} \qquad \text{(Definition 3.1, p. 9).}$$

Its size is measured by the $\delta$-cover number $C_\delta(E)$, the least number of closed intervals of length at most $\delta$ whose union contains $E$ (Definition 3.2, p. 10). A strategy is $(\epsilon, \delta, L)$-private (Definition 3.3, p. 10) if

1. it is accurate: $|\hat x(x,y) - x| \le \epsilon/2$ for every $x \in [0,1)$ and every seed $y$; and
2. it is private: $C_\delta(\mathcal I(\bar q)) \ge L$ for every $x \in [0,1)$ and every $\bar q \in \mathcal Q(x)$.

The query complexity is $N^*(\epsilon, \delta, L) = \min\{N : \Phi_N \text{ contains an } (\epsilon,\delta,L)\text{-private strategy}\}$ (eq. (5), p. 11). All logarithms are base 2 and are rounded up (footnote 1, p. 4).

Formalization targets

Goal: Theorem 4.1 (p. 12)

For $\epsilon > 0$, $\delta > 0$ and an integer $L \ge 2$ with $2\epsilon < \delta \le 1/L$,

$$\max\left\{ \left\lceil \log_2 \tfrac1\epsilon \right\rceil,\ \left\lceil \log_2 \tfrac\delta\epsilon \right\rceil + 2L - 4 \right\} \le N^*(\epsilon,\delta,L) \le \left\lceil \log_2 \tfrac{1}{L\epsilon} \right\rceil + 2L.$$

Upper bound (§6)

The Opportunistic Bisection (OB) strategy first places $L$ "guesses" $[i/L, i/L+\epsilon)$ with $2L$ fixed queries, and then runs a bisection of $\lceil \log_2(1/(\epsilon L)) \rceil$ steps in one of the gaps. The bisection is truthful if no guess caught $v^*$, and driven by the seed otherwise. The milestones are: OB is accurate; the union of guesses $\mathcal G$ has $C_\delta(\mathcal G) \ge L$ (Claim 6.3); $\mathcal G \subseteq \mathcal I(\bar q)$ for every observable $\bar q$ (Claim 6.4); the cover number is monotone; and OB is $(\epsilon,\delta,L)$-private (Proposition 6.2).

Lower bound (§7)

For an accurate strategy, the final interval between consecutive sorted queries (with $q_0 = 0$, $q_{N+1} = 1$) has length at most $\epsilon$ (§7.1), so $\mathcal I(\bar q) \subseteq \bar{\mathcal I}(\bar q)$, the union of special intervals (display (20)). Lemma 7.1 puts $\lceil \log_2(\delta/\epsilon) \rceil$ queries in $(0,\delta)$ for some true value, and accuracy alone gives $N \ge \lceil \log_2(1/\epsilon) \rceil$. A covering bound gives $C_\delta(\bar{\mathcal I}(\bar q)) \le (K+3)/2$, with $K$ the number of special queries in $[\delta, 1]$ (p. 21). Together these give $N \ge \lceil \log_2(\delta/\epsilon) \rceil + 2L - 4$ for every private strategy.

Corollary 4.2 (the case $\delta = 1/L$) is Theorem 4.1 specialized and is not posed separately.

Significance

The result. The theorem gives the cost of privacy in this model up to an additive constant. At $\delta = 1/L$ the two bounds differ by at most 4 (Corollary 4.2), and the extra cost over plain bisection is at most an additive $2L$. That is much less than the non-adaptive $\epsilon$-dense strategy, which is always private but needs about $1/\epsilon$ queries (§5). The lower bound also shows that the $2L$ obfuscating queries cannot be shared with the queries that locate $v^*$ (§7, p. 19).

Formalizing it. The result is proved on paper, but Lemma 7.1 is given only an intuitive argument: the paper calls its proof "fairly standard" and omits it (p. 20). The covering step on p. 21 is argued component by component, with an exceptional component straddling $\delta$. A formal development supplies both and checks the bookkeeping behind the constants $-4$, $+3$ and $2L - 3$. To our knowledge, no machine-checked proof of this theorem or of the bisection lower bound in this form exists.

Difficulty

The upper bound is a construction. Its delicate point is Claim 6.4. For every point $g$ of every guess one must exhibit a seed under which $g$ produces exactly the observed queries, and that seed differs according to whether the observed run was truthful or fictitious.

The lower bound is harder. Counting queries is not enough by itself, because the obvious argument conflates query values with query indices. Lemma 7.1 counts indices along a single run (a fixed true value and seed). The covering bound counts distinct values in $[\delta,1]$, one of which may be the artificial point $1$. The natural first idea, a direct counting bound on $N^*$, is unavailable: $N^*$ is a minimum, so a lower bound must be proved for every private strategy of every length. Only the goal speaks about $N^*$, where the upper bound shows the set being minimized is nonempty.

Formalization scope

Everything lives in the namespace PrivSeqLearn.QueryComplexity, built on Mathlib with no measure theory in any statement. Conventions:

• The seed space is Fin Ybar with 0 < Ybar. "Positive probability" is read as "for some seed" and "probability one" as "for every seed", which is exact for a uniform seed on a finite set.
• Response histories are List Bool, and the response to $q$ at true value $x$ is decide (q ≤ x). Queries are 0-indexed (Fin N).
• $\Phi_N$ (InPhi) requires query values on every history of length $< N$ and estimate values on every history of length $N$ to lie in $[0,1)$, and the queries to be pairwise distinct for every $x \in [0,1)$ and seed.
• Covers are Fin L-indexed families of closed intervals Set.Icc. $C_\delta$ and $N^*$ are sInf over $\mathbb N$, which equals the minimum when the set is nonempty.
• Every logarithm term is ⌈Real.logb 2 ·⌉ computed in $\mathbb Z$, so $2L - 4$ never truncates. In the regime, all log arguments exceed 1.
• The OB seed is $\{0, \dots, L \cdot 2^M - 1\}$, decoded as the gap $\tilde{\mathcal J}$ and the bits $Z_1, \dots, Z_M$. The OB estimate, specified in the paper only inside the proof of Proposition 6.2, is the guess mid-point or the mid-point of the final bisection interval.
• Disclosed deviations from the page:
  • Lemma 7.1 assumes $\delta \le 1$.
  • The lower-bound milestones do not assume distinct queries, which is a strengthening.
  • The OB-only milestones use $2\epsilon < 1/L$ in place of $2\epsilon < \delta \le 1/L$.
  • Cover-number monotonicity assumes a bounded superset.

Trivializing encodings are ruled out:

• an empty seed space is excluded by 0 < Ybar;
• information sets range over $[0,1)$ only;
• privacy is required for every true value and every observable query sequence;
• OB is the constructed strategy, not "some strategy".

Contributions are welcome on any milestone. The bisection lower bounds (Lemma 7.1 and the $\log_2(1/\epsilon)$ bound) and the interval-covering facts are reusable beyond this mission.

Selected references

• J. N. Tsitsiklis, K. Xu, Z. Xu, Private Sequential Learning, arXiv:1805.02136v3, 2020; Operations Research, 2021. https://arxiv.org/abs/1805.02136
• R. Waeber, P. I. Frazier, S. G. Henderson, Bisection search with noisy responses, SIAM Journal on Control and Optimization 51(3):2261–2279, 2013. https://doi.org/10.1137/120861898
• M. Horstein, Sequential transmission using noiseless feedback, IEEE Transactions on Information Theory 9(3):136–143, 1963. https://doi.org/10.1109/TIT.1963.1057832
• Z. Xu, Private sequential search and optimization, Master's thesis, MIT, 2017. http://hdl.handle.net/1721.1/112054