Establish a separation exponent of at least $2.0635$ between block sensitivity and sensitivity of total Boolean functions.

For every $\varepsilon>0$ and integer $S\ge2$, construct $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0635-\varepsilon}$.

Multiple-Life Survival, Joint-and-Survivor Annuities and Contingent Assurances

Motivation

A multiple-life contract has payments depending on the survival of more than one individual. A joint-life pension might stop at the first death, while a last-survivor annuity continues until both lives have died. A retirement pension may continue in a smaller amount to a surviving spouse, and a policy may instead pay one capital sum on the first or second death. These arrangements arise in pension schemes, life insurance and the valuation of dependent beneficiaries. They have different claim events, beneficiaries and settlement dates. The distinction matters in actual valuation, especially when both deaths occur between scheduled pension dates.

The basic mathematical objects are laid out in Promislow's Fundamentals of Actuarial Mathematics, third edition (2015, Chapter 10), and Dickson, Hardy and Waters' Actuarial Mathematics for Life Contingent Risks, third edition (2020, Chapter 10). Both discuss joint and last-survivor states. The latter also treats dependent future lifetimes and common shocks. The mission develops event-consistent formulas from a shared joint mortality law, rather than selecting unrelated survival probabilities for different contract components.

Setting

Let two future lifetimes be represented by death-time states $K_x$ and $K_y$ on a finite grid with right-censoring horizon $h$. For $i<h$, state $K_x=i$ means the first life dies in the interval after anniversary $i$ and its death benefit is payable at tick $i+1$ under the annual settlement convention. The terminal state $K_x=h$ means that this death has not been observed before the horizon. The same convention applies to the second life. More finely spaced ticks can represent payment and death dates within a year, so ordering is retained when the two deaths fall in different subannual intervals.

The joint probability mass function is $p_{ij}=\Pr(K_x=i,K_y=j)$, with $p_{ij}\geq0$ and $\sum_{i=0}^{h}\sum_{j=0}^{h}p_{ij}=1$. It determines both one-life margins and their dependence. In particular, the probability that both lives are alive at tick $t$ is $\sum_{i,j}p_{ij}\mathbf{1}_{\{t\leq i\}}\mathbf{1}_{\{t\leq j\}}$. Products of the two marginal survival probabilities are valid only under an explicit independence assumption.

At a scheduled payment anniversary there are four disjoint in-force states: both alive, member only, spouse only and neither alive. The joint-life status is the both-alive state. The last-survivor status consists of all states except neither alive. The reversionary spouse status is specifically member dead and spouse alive. A reversionary pension starts once member death makes the spouse entitled and pays only when the spouse is alive at the relevant instalment date. This is contractually distinct from an unqualified joint-and-survivor pension, whose original member and survivor amounts may follow a different schedule.

Write $d_t$ for a discount factor taking a payment at tick $t$ to commencement, and $b_t$ for its gross benefit amount. A member pension may pay $b_t$ while the member is alive and $\rho b_t$ when the member is dead but the spouse remains alive. The ratio $\rho$ is the spouse continuation factor. Unless stated otherwise, the status is tested at each scheduled payment date, so a spouse who dies before the first eligible instalment receives no instalment. Death lump sums use the tick immediately after their death-year state and are distinct from these scheduled pension payments.

Formalization targets

Joint-law occupation states

The first group constructs the joint law, marginal survivals and four exclusive occupation states. Their probability sums and event identities must agree without assuming independent lives. Strict order events $K_x<K_y$ and $K_y<K_x$ are accompanied by the tie event $K_x=K_y$; both terminal states are right-censored and must not cause a fictitious death claim. Equal grid times are treated as genuine ties in the grid model. Physical simultaneous death in continuous time requires a separate law assigning it positive mass.

Annuity and reversionary values

The second group gives realised annuity cashflows and expected present values for joint-life, last-survivor, member-only and reversionary spouse statuses. A key identity for identical payment dates and discounting is

$$a_{\text{last}}=a_x+a_y-a_{xy},\qquad a_{y\mid x}=a_y-a_{xy}.$$

The first term values any surviving life, and the second values the spouse-only reversion. These identities are valid under general dependence because all terms come from the same joint distribution. For a member pension with a separately contractual spouse continuation of $\rho$, its expected value is

$$V=a_x+\rho a_{y\mid x} =(1-\rho)a_x+\rho a_{\text{last}}.$$

This formula presumes the member payment and spouse payment are evaluated at the same dates with no overlapping guarantee or independent payment entitlement. Guarantee cashflows require separate contractual events.

Order-sensitive death claims

The third group models a unit claim on the first death, a unit claim on the second death, the member dying first, the spouse dying first and simultaneous-grid death. It also models a later death of the survivor and pure endowments contingent on joint or last-survivor survival. Payment at death and payment on a pension anniversary can differ even when the same person eventually receives a benefit. Both deaths within a year are represented with a sufficiently fine tick grid; annual year-end states alone do not identify their physical order.

Integrated capstone

The capstone values a combined pension and assurance from the realised cashflow across all death-time pairs. It then reconciles the expected value independently against single-life, reversionary and last-survivor annuity factors, together with the disjoint first- and second-death assurance values. The event partition is incorporated in the total cashflow rather than appended as an unrelated identity.

Significance

The identities provide actuarially auditable bridges between benefits administered by member and spouse status and factors calculated by conventional life-contingency methods. In Dickson, Hardy and Waters (2020, Chapter 11), pension mathematics supplies further context. They can be used to check spouse continuation calculations in defined benefit pension administration, premium valuations of first- and second-death assurances, and mortality stress tests where lives in a household may be dependent. A dependent joint law can change the joint annuity and first-death insurance values while preserving each single-life margin.

The formalisation keeps payment timing, benefit entitlement, event order and valuation date visible in the mathematics. In the published sources the classical factor relations are known results, while the present finite-grid cashflow definitions and their combined capstone are original derived formulations. Each proposed theorem remains an open formal target until independently verified by Prove2Me's authoritative remote Lean compiler and, separately, proved.

Difficulty

Marginal survivals do not determine joint survival or within-year death order. A spouse may become entitled before the first payable instalment, and may die between those events. Death settlement, grid ties and terminal censoring therefore require careful treatment. The capstone reconciles expected realised cashflows with independently calculated factors, preserving the same joint law, dates and entitlement rules in both valuations.

Formalization scope

The Lean kernel uses finite double sums over one right-censored joint law. Due, arrears, subannual, deferred and guaranteed member/spouse cashflows are defined. Death timing is represented on an integer grid; periods can be made subannual by changing the tick size. Scheduled pension payments are due at their specified ticks. Lump sums are settled at the following death tick. Discount factors and benefit amounts are parameterised as schedules; no particular flat interest rate is built into the definitions.

In the guarantee kernel, $g$ is an absolute expiry tick and $a$ starts the payment window. Guaranteed member payments do not require survival to $a$: they model an already vested obligation, not a pension conditional on reaching retirement. A guarantee lasting $G$ periods from $a$ would expire at $a+G$ and require a separate retirement-eligibility condition. UK defined benefit death-in-deferment and dependant entitlements are scheme-specific and outside this kernel.

The main decomposition identities do not need independence, and explicit independent/dependent finite counterexamples are staged for remote theorem proofs. Equal-tick ties are explicit. A smooth continuous-time law, arbitrary within-tick death times, integrals for immediate death settlement, changing spouse eligibility and other pension guarantee arrangements require further declarations and remote verification before the complete mission can be released. The finite model does not imply those continuous-time results. Annuity-certain or single-life results from other unpublished owner Drafts are not assumed to be importable.

Formal contributors must preserve the same probability law and the same discount and settlement conventions across all components of any identity. A vacuous statement established by assuming its intended conclusion, using inconsistent marginals or suppressing the tie event does not meet the mission's mathematical contract.

Selected references

• S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, Chapter 10, Sections 10.2–10.8, publisher-linked contents.

• D. C. M. Dickson, M. R. Hardy and H. R. Waters, Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, 2020, Chapter 10, book DOI.

Improve the separation exponent between block sensitivity and sensitivity of total Boolean functions. This mission targets $\alpha\ge2.0391$; higher is better.

For every $\varepsilon>0$ and every integer $S\ge2$, the goal asks for a function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0391-\varepsilon}$. The shared definition SensitivityCampaign.AchievesExponent expresses exactly this requirement.

Using a finite certificate. Choose a total Boolean function $f$, an input $x$, and integers $A,B>1$. Prove $s(f)\le A$, $B\le bs(f,x)$, and $A^{2.0391}\le B$, then apply SensitivityCampaign.finite_certificate. Here $bs(f,x)$ means block sensitivity at the chosen input. The shared theorem handles normalization and passage to arbitrarily large sensitivity. Its proof is a foundation milestone; a proof depending on an open milestone remains conditional until that milestone is proved.

Direct proofs of the asymptotic goal are equally welcome. Keep the shared definitions, replace the target value, and give your theorem a unique name. Use exact certified bounds; numerical estimates alone do not establish a record.

Background: the campaign proposal.

Motivation

In industries built on a key component sold by one dominant supplier, such as smartphone chipsets, the supplier's contract terms shape how much its downstream customers innovate. Some suppliers require their customers to cross-license their own patents to each other as a condition of buying the component, so that each manufacturer's innovation also improves its rival's product. Wang, Huang and Lee (SSRN 3053682; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2019.0477) ask when a supplier facing two manufacturers of unequal innovation ability benefits from imposing cross-licensing. Their answer runs through the equilibrium of the manufacturers' innovation game, which is the subject of this mission: Proposition 2 describes how much each manufacturer innovates and shows that the supplier never ends up selling to a single manufacturer.

Setting

A supplier sells a component at wholesale price $r \ge 0$ to manufacturers $M_1$ and $M_2$. Manufacturer $M_i$ chooses a quality improvement $T_i \ge 0$ at cost $k_iT_i^2$. With cross-licensing of effectiveness $\beta \in [0, 1]$, the quality improvement of $M_i$ is $T_i + \beta T_j$ ($j \ne i$), and its inverse demand is $p_i = 1 + T_i + \beta T_j - q_i - q_j$. The standing assumptions are

$$0 \le \beta \le 1, \qquad \tfrac{49}{144} < k_2 < k_1,$$

so $M_2$ is the superior manufacturer. The game has three stages.

1. Quantities. Given $(T_1, T_2)$ and $r$, each $M_i$ chooses $q_i \ge 0$ to maximize $\Pi_i = (1 + T_i + \beta T_j - q_i - q_j - r)q_i$ (display (1)). The equilibrium quantities, display (2), are a duopoly when $r$ is low and a monopoly of the manufacturer with the higher quality when $r$ is higher.
2. Price. The supplier chooses $r \ge 0$ to maximize $r(q_1 + q_2)$. Its price $r^*(T_1, T_2)$ is the least maximizer. Lemma 1 computes it: the supplier induces a duopoly exactly when $\beta \ge \sqrt3 - 1$ or $T_2 \le \hat T_2(T_1\mid\beta)$, where

$$\hat T_2(T_1\mid\beta) = \frac{2 - \sqrt3 + T_1(1 - \beta(\sqrt3 - 1))}{\sqrt3 - 1 - \beta}.$$

3. Innovation. Each $M_i$ chooses $T_i \ge 0$ to maximize $\Pi^*_i(T_1, T_2\mid\beta) - k_iT_i^2$, where $\Pi^*_i$ is its Cournot profit at the supplier's price. An innovation equilibrium is a pure Nash equilibrium of this game.

The proof of Proposition 2 defines two candidate profiles in closed form: the interior candidate $T^I = (T^I_1, T^I_2)$, which solves both manufacturers' first-order conditions, and the boundary candidate $T^B = (T^B_1, T^B_2)$, where $M_2$ invests exactly up to $\hat T_2$. A threshold $\hat k_2(k_1\mid\beta)$ separates them, and $T^*(\beta) = T^B$ if $k_2 < \hat k_2(k_1\mid\beta)$, $T^*(\beta) = T^I$ otherwise.

Formalization targets

Goal: Proposition 2 (p. 12)

Under the standing assumptions:

1. every innovation equilibrium is a duopoly, meaning both manufacturers sell a positive quantity at the supplier's price;
2. $T^*(\beta)$ is an innovation equilibrium and a duopoly;
3. if $k_2 < \hat k_2(k_1\mid\beta)$, then $\beta < \sqrt3 - 1$ and $M_2$ is on the boundary:

$$T^*_2 = \hat T_2(T^*_1\mid\beta);$$

4. if $k_2 \ge \hat k_2(k_1\mid\beta)$, then $T^*(\beta) = T^I$ and both duopoly first-order conditions hold at $T^*(\beta)$.

Milestones

• display (2): the Cournot quantities are the unique equilibrium of the quantity game;
• Lemma 1: the supplier's price, the regime, its optimal profit, and the gross profits $\Pi^*_1, \Pi^*_2$;
• monopoly infeasibility at $T_1 = 0$, from the proof (p. A.1): $M_2$'s monopoly optimum $1/(16k_2 - 1)$ lies below $\hat T_2(0\mid\beta)$;
• $T^I$ is the unique solution of the two first-order conditions (p. A.1);
• $T^B_2 = \hat T_2(T^B_1\mid\beta)$, and $T^B_1$ is $M_1$'s best response to $T^B_2$ (p. A.1);
• $\hat k_2$ is where $T^I_2 = T^B_2$, and above it $T^I$ lies in the duopoly region (p. A.2);
• $\hat k_2(k_1\mid\beta)$ is strictly decreasing in $\beta$ with $\hat k_2(k_1\mid 1) = 0$ (p. A.2), so the boundary region shrinks to empty as $\beta$ grows.

Significance

Proposition 2 is the paper's equilibrium characterization. Proposition 3 is its instance $\beta = 0$ (no cross-licensing), and Proposition 4 compares the supplier's equilibrium profits with and without cross-licensing on the closed forms $T^B$, $T^I$ and $\hat k_2$ established here. The economic content is that, under cross-licensing, the supplier always ends up selling to both manufacturers. When the superior manufacturer's cost advantage is large it caps its own innovation exactly where the supplier stops preferring a monopoly.

The paper's proof states the closed forms and asserts the checks ("one can obtain", "we verify"). This mission produces a machine-checked version: a complete definition of the three-stage game, with the supplier's price defined as an optimization rather than by its solution, and the equilibrium claims stated against that game. To our knowledge no part of this result has been formalized before.

Difficulty

The innovation payoff of the superior manufacturer is discontinuous. When $T_2$ moves just above $\hat T_2(T_1\mid\beta)$, the supplier switches from a duopoly price to a monopoly price, and $M_2$'s gross profit jumps down. A first-order argument therefore does not show that $T^*$ is an equilibrium. One must also show that $M_2$ never gains by moving into the monopoly region, and that $M_1$ never gains by deviating above $T_2$, where $M_1$ itself becomes the potential monopolist. The boundary candidate is an equilibrium only because the supplier breaks its indifference at the boundary toward the duopoly.

Part 1 quantifies over every equilibrium, not only $T^*$. The paper checks monopoly infeasibility only at $T_1 = 0$, so the general case needs its own argument. The equilibrium is not unique: for some parameters a mirrored profile with $M_1$ at its own boundary is also an equilibrium. Uniqueness is therefore not claimed. The remaining steps are polynomial and rational inequalities in $(k_1, k_2, \beta)$ involving $\sqrt3$.

Formalization scope

• Parameters $\beta, k_1, k_2$ are real numbers. The standing assumptions $0 \le \beta \le 1$ and $49/144 < k_2 < k_1$ are bundled as Standing β k1 k2.
• Quantities and innovation levels range over $\mathbb R_{\ge 0}$ (NNReal). Equilibria use the published two-player predicate CompetingChains.Cournot.IsPureNash.
• Wholesale prices range over $[0, \infty)$. The paper leaves this implicit, so it is a disclosed addition.
• Display (2) is encoded in symmetric form, with the manufacturer of larger quality as the possible monopolist. The paper prints it for $T_2 \ge T_1$, but deviations in the innovation game reach $T_1 > T_2$.
• The supplier's price is the least maximizer of $r(q_1 + q_2)$ over $r \ge 0$. This is the tie-break Lemma 1 uses at $T_2 = \hat T_2$.
• First-order conditions are stated as derivatives (HasDerivAt … 0) of Lemma 1's duopoly polynomials, because the game payoff is not differentiable at the boundary.
• All closed forms are transcribed as printed, with $\sqrt3$ as Real.sqrt 3. Every denominator is proved nonzero in its regime, never assumed.

Two trivializing formalizations are ruled out. Equilibria are never defined by first-order conditions or by the closed forms, and the supplier's price is never defined by Lemma 1's case rule. Both are theorems here.

The source is the authors' SSRN manuscript (abstract 3053682, version of 2023-04-27); its proofs are in the appendix, pp. A.1–A.9. The paper's equivalent threshold $\hat\beta(k_1, k_2)$ is not formalized. Proofs of any milestone are welcome. Lemma 1 and display (2) are self-contained, and the closed-form milestones need only real-algebraic inequalities with $\sqrt3$.

Selected references

• J. Wang, T. Huang, H. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN 3053682, version of 2023-04-27. https://ssrn.com/abstract=3053682
• J. Wang, T. Huang, H. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2019.0477

Motivation

A rare disease affects few patients, so a drug for it has a small market and its research and development (R&D) cost is spread over few sales. Governments respond with two kinds of subsidy: cost subsidies that pay part of the manufacturer's R&D bill (orphan drug programmes), and price subsidies that pay part of what each patient is charged. At the same time two practices change how drugs are priced and paid for. In some markets an independent consortium negotiates the price instead of the manufacturer, and some manufacturers offer outcome-based payment ("No Cure No Pay", as in a programme of Bristol-Myers Squibb), under which the patient pays only if the drug works.

W. Olsder, T. Martagan and C. S. Tang ask how a government with a fixed budget should divide it between the manufacturer and the patients under each pricing and payment regime. This mission formalizes their analysis of the regime with a consortium price and outcome-based payment, Setting (2B) of the paper, where the answer depends on the price: for a high price only patients should be subsidized, and for a low price only the manufacturer. The source is the SSRN working paper 3481150 (version of 2019-11-13); the article later appeared in Management Science (2023) with possibly different numbering, which is not used here.

Setting

The market has size one. A patient's valuation $V$ of an efficacious drug is uniform on $[0,1]$. The model has three positive primitives: the R&D cost scale $k$, the government's budget $B$, and the unit price $p$, which the consortium fixes and which lies in $(0,1)$.

• A subsidy policy is a pair $(\alpha,\beta)$ with $\alpha\in[0,1)$ and $\beta\in[0,1)$. The government pays the share $\alpha$ of the R&D cost and the share $\beta$ of the unit price.
• The manufacturer chooses a target efficacy $e>0$, the probability that the drug works, at R&D cost $ke^2$. Under outcome-based payment it is paid $p$ per patient only when the drug works, and the demand is $1-(1-\beta)p$. Its profit, the bracket of the paper's (9), is

$$\pi_m(e)=e\,p\,[1-(1-\beta)p]-(1-\alpha)ke^2 .$$

A best response to $(\alpha,\beta)$ is a maximizer of $\pi_m$ over $e>0$.

• At efficacy $e$ the patient welfare (7) and the government spending, the left-hand side of the budget constraint in (10), are

$$W=\tfrac12\,e\,(1-(1-\beta)p)^2,\qquad M=\alpha k e^2+e\,\beta p\,[1-(1-\beta)p].$$

• A policy is optimal when it has a best response at which $M\le B$ and its welfare there is at least the welfare of every other policy at each of that policy's best responses with $M\le B$.
• $\alpha_{\max}$ is the largest $\alpha\in[0,1)$ for which the policy $(\alpha,0)$ is affordable at the manufacturer's best response.

The Lean development names these objects IsPolicy, profit, BR, welfare, spend, IsOptimal and IsAlphaMax, in the namespace RareDisease.ExogOutcome.

Formalization targets

Goal: Proposition 3, parts 1 and 3

For $k>0$, $B>0$, $0<p<1$ and $\alpha_{\max}$ as above:

1. At every optimal policy the budget constraint binds: $M=B$ at the best response.
2. If

$$p\ \ge\ \frac{2}{5-\alpha_{\max}}\quad\text{and}\quad B<\frac{p^2}{2k},$$

then there is a $\beta_1$ such that $(0,\beta_1)$ is optimal and every optimal policy equals $(0,\beta_1)$. Only patients are subsidized. 3. If

$$p\ \le\ \frac{2(1-\alpha_{\max})}{5},$$

then $(\alpha_{\max},0)$ is optimal, every optimal policy equals it, and

$$\alpha_{\max}=\frac{8Bk+p^4-2p^3+p^2-(p-p^2)\sqrt{16Bk+p^4-2p^3+p^2}}{8Bk}.$$

Only the manufacturer is subsidized.

The thresholds are the printed ones. They are not the sharpest possible (see Formalization scope), but they are what the paper states.

Milestones

In attack order: the best response (19), $e^*=p(1-(1-\beta)p)/(2(1-\alpha)k)$; the reduced problem (20), giving welfare and spending at the best response; the fact that both expressions of (20) are increasing in $\alpha$ and in $\beta$; and the marginal-rate identity from the proof of Proposition 3 (Appendix C, p. 37), whose sign is that of $(5-\alpha)p-2(1-\alpha)$.

Significance

The result splits the decision between subsidizing patients and subsidizing the manufacturer by a single comparison of the consortium's price with thresholds that depend only on the budget and the cost scale. For a policy maker the consequence is concrete. A high negotiated price already gives the manufacturer enough incentive to develop an efficacious drug, so every unit of budget should lower what patients pay. A low price leaves the manufacturer short of incentive, so every unit should go to R&D. Splitting the budget is never optimal in either regime.

The formalization adds three things. First, it checks a statement whose printed form has errors. Part 2 of the proposition, "subsidize both" for intermediate prices, is false as printed: $B=0.05$, $k=0.3$, $p=0.2$ lies in the printed middle range, yet the unique optimum is manufacturer-only. The printed closed form for the patient subsidy in part 1 does not satisfy the binding budget constraint. Second, the proof in the paper is a marginal argument along the binding curve, and its extremal step takes a maximum over $\alpha$ at the wrong end; the parts posed here stay true because their thresholds are stronger than needed, which a machine-checked proof makes explicit. Third, the game is stated as a game: the government's problem is posed over the manufacturer's best-response set, not over the reduced formulas, so the reduction (19)–(20) is itself a theorem. None of these results has a machine-checked proof yet.

Difficulty

The reduced problem (20) is a two-variable optimization with a nonlinear constraint, and its feasible region has no simple shape. The obvious first idea is to solve the first-order conditions of the Lagrangian, but the optimum of parts 1 and 3 is on the boundary of the policy square ($\alpha=0$ or $\beta=0$), so stationarity says nothing there. What has to be shown instead is a global sign property along the whole binding curve: trading manufacturer subsidy for patient subsidy changes welfare per unit of spending with the sign of $(5-\alpha)p-2(1-\alpha)$, and this sign must be controlled for every $\alpha$ the curve passes through. That requires knowing that the curve stays in $\alpha\le\alpha_{\max}$, which comes from the monotonicity of spending. Two existence and uniqueness questions also arise. In part 1 a patient-only policy must exhaust the budget with $\beta<1$, which is where $B<p^2/(2k)$ enters. In both parts no other policy may tie the optimum.

Formalization scope

All quantities are real numbers. The standing assumptions $k>0$, $B>0$ and $0<p<1$ are hypotheses of every theorem. The paper uses them without stating them: with $p\ge1$ and $\beta=0$ the demand $1-p$ is not positive and the manufacturer has no best response with $e>0$; the closed form of $\alpha_{\max}$ divides by $8Bk$. As in the paper, the efficacy $e$ ranges over all positive reals and is not bounded by $1$. Policies satisfy $\alpha,\beta\in[0,1)$, a half-open interval.

The added hypothesis $B<p^2/(2k)$ in part 1 is necessary. With $\alpha=0$ the spending tends to $p^2/(2k)$ as $\beta\uparrow1$, so for larger budgets no patient-only policy exhausts the budget. The thresholds $2/(5-\alpha_{\max})$ and $2(1-\alpha_{\max})/5$ are posed as printed; replacing them by the sharper values $2/5$ and $2(1-\alpha_{\max})/(5-\alpha_{\max})$ would be a different theorem. Part 2 and the printed closed form of part 1 are not posed, because both are false as printed.

The formalization cannot be trivialized by defining the government's problem through the reduced forms (20), because welfare and spending in IsOptimal are evaluated at members of the best-response set BR. "Optimal" means attained and compared against every policy at every best response, not a supremum. $\alpha_{\max}$ is defined as the greatest affordable manufacturer-only subsidy, not by its closed form, which is part of the goal.

A complete development needs only real analysis from Mathlib: maximization of a concave quadratic, monotonicity of rational functions, one-variable derivatives for the marginal-rate milestone, and Real.sqrt for the closed form. Proofs of any milestone are welcome.

Selected references

• W. Olsder, T. Martagan, C. S. Tang, Improving Access to Rare Disease Treatments: Optimal Subsidies, Pricing, and Payment, SSRN working paper 3481150, version of 2019-11-13. https://ssrn.com/abstract=3481150
• W. Olsder, T. Martagan, C. S. Tang, Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4634

Why liquidity can explain persistent private equity returns

Private equity funds are organized as limited partnerships. Limited partners (LPs: pension funds, endowments, insurers) commit capital, and a general partner (GP) manages the fund and calls the committed capital over several years. A well-documented empirical regularity is that some LPs earn persistently higher returns than others, and that fund returns persist across a GP's successive funds (Kaplan and Schoar, 2005; Lerner, Schoar and Wongsunwai, 2007). The usual explanation is differences in skill.

Maurin, Robinson and Strömberg propose a different channel. Because capital is called gradually, an LP hit by a liquidity shock may default on the remaining commitment. GPs who raise money from LPs that tolerate illiquidity can invest efficiently. GPs who raise money from LPs that do not must call capital early to protect themselves against default, which distorts investment. When illiquidity-tolerant capital is scarce, GPs compete for it and pay its owners a premium. This mission formalizes the paper's main equilibrium result without a secondary market: that premium exists exactly when both kinds of funds are raised.

Setting

An investment pays $R$ per unit on success and $0$ on failure. It succeeds with probability $p$ if the GP exerts effort and with probability $q<p$ if the GP shirks, in which case the GP enjoys a private benefit $B$ per unit invested. Each GP has wealth $A$ and runs one fund of total size $I>A$. A share $x\in[0,1]$ of the fund is invested in period 0 and the rest, $1-x$, in period 1; both investments succeed or fail independently.

A fee schedule $f$ pays the GP a fee per unit of investment that depends on which investments succeeded. It must satisfy limited liability, $0\le f\le$ the fund's cash flow, and incentive compatibility: effort on both investments must be at least as profitable for the GP as shirking on either or both. Write $\bar f$ for the expected fee under effort. LPs who receive the promised expected return $\bar R$ per unit contributed supply $I-A$, which ties the fund size to the fee through

$$(pR-\bar f)\,I=\bar R\,(I-A).\qquad(3)$$

LPs consume in periods 1 and 2. With probability $\lambda\in(0,1)$ an aggregate liquidity shock hits in period 1. After the shock an LP discounts period-2 consumption by $\delta\in(0,1)$. There are two types, $L$ and $H$, with $\delta_L<\delta_H$, holding the shares $1-\mu_H$ and $\mu_H$ of the LPs' total capital $K$. Without a secondary market an LP honours the second capital call only if the claim is worth at least its cost:

$$1-x\le\delta\,\bar R.\qquad(4)$$

A GP chooses $(x,I,f)$ to maximize the profit $\Pi_{GP}=\bar f I$ subject to (3) and (4). LPs invest in private equity when its value $(1-\lambda)\bar R+\lambda\delta\bar R$ exceeds the value $1$ of cash. An equilibrium (Definition 2) consists of the fractions $\alpha_L,\alpha_H$ of GPs raising each fund type, the returns $\bar R^*_{PE,L},\bar R^*_{PE,H}$, and optimal contracts such that GPs raise only profit-maximizing fund types and each primary market clears.

The key quantities are the LPs' break-even return $1+r(\lambda,\delta)=1/(1-\lambda(1-\delta))$, the minimal safe early call $\hat x(\lambda,\delta)=1-\delta/(1-\lambda(1-\delta))$, and the tolerance threshold $\hat\delta(\lambda)=1-p/(p+(1-\lambda)q)$. The Lean development uses the namespace PELiquidity.Primary, with grossReturn, xHat, deltaHat, xLow, xBar, IsFeasibleContract, IsOptimalContract, IsCapitalSupply and IsEquilibrium.

Formalization targets

Goal: Proposition 2

There are thresholds

$$0<\underline\mu_H<\bar\mu_H<1$$

such that for every $\mu_H\in(0,1)$ an equilibrium exists, and every equilibrium satisfies the following:

• if $\mu_H<\underline\mu_H$, both fund types are raised and $\bar R^*_{PE,H}>\bar R^*_{PE,L}=1+r(\lambda,\delta_L)$;
• if $\mu_H\ge\underline\mu_H$, then $\alpha^*_L=0$;
• $\bar R^*_{PE,H}$ is strictly decreasing in $\mu_H$ on $[\underline\mu_H,\bar\mu_H]$;
• if $\mu_H\ge\bar\mu_H$, then $\bar R^*_{PE,H}=1+r(\lambda,\delta_H)$.

The thresholds are existential, as in the paper. A variant pinning $\bar\mu_H$ by (C.3) is a welcome strengthening.

Milestones

1. (11): the break-even return $1+r(\lambda,\delta)$, decreasing in $\delta$.
2. Lemma 1 with (12): $\Pi_{GP}=pRI-\bar R(I-A)$, so an optimal contract minimizes $\bar f$.
3. Lemma 2: the minimal incentive-compatible fee is (15), minimized exactly on $x\in[q/(p+q),p/(p+q)]$.
4. Proposition 1: under (4) the optimal early call is $[\max\{\underline x,\hat x\},\bar x]$ if $\delta\ge\hat\delta(\lambda)$, and $\hat x(\lambda,\delta)$ with a strictly higher fee if $\delta<\hat\delta(\lambda)$.
5. (C.4): when only H-funds are raised above the H-LPs' break-even rate, $\mu_HK=I_H-A=(pR-\bar f_H)A/(\bar R_H-(pR-\bar f_H))$; for fixed fee, the contribution decreases with $\bar R_H$.
6. (18): the indifference rate $\bar R^{max}_{PE,H}\in(1+r(\lambda,\delta_L),pR)$.
7. Lemma C.1: $\alpha^*_L>0$ implies $\bar R^*_{PE,L}=1+r(\lambda,\delta_L)$.

Significance

The result shows that heterogeneous liquidity needs alone, without any difference in skill, produce a cross-section of LP returns: when capital from liquidity-tolerant LPs is scarce, those LPs earn strictly more than other LPs investing in otherwise identical funds. When it is abundant, they earn only their fair liquidity premium. This separates a liquidity explanation of return persistence from a skill explanation, and it is the benchmark against which the paper's second main result, the effect of a secondary market (Proposition 3, a separate mission), is measured.

The paper proves the result by hand. No part of it has a machine-checked proof. A formalization would check the three-case equilibrium argument, including uniqueness, which the paper treats briefly. It would also fix the readings of Definition 2 that the printed statement leaves open (see below) and record the hypotheses the proofs use without stating. The fee-design lemma (Lemma 2) is a small linear program of independent interest for moral-hazard models with several projects.

Difficulty

The equilibrium statements quantify over every equilibrium, and an equilibrium includes an optimal contract for each fund type, optimal against all fee schedules, call shares and fund sizes. The obvious approach, substituting the closed-form fee (15) and the optimal call (17) into the profit function, does not suffice. Uniqueness requires showing that no other combination of returns, fund fractions and contracts clears both markets. That includes returns at which a fund type is not raised. It also includes returns above the break-even rate, where the no-default constraint loosens and the fee falls. Ruling these out needs the GP's optimal profit to be decreasing in the promised return even when the no-default constraint binds. The boundary at $\underline\mu_H$, where the $H$-market just clears with every GP raising an $H$-fund, has to be placed correctly.

Formalization scope

• Parameters. The parameter structure records $0<q<p\le 1$, $B,A,K>0$, $\lambda,\delta_L,\delta_H\in(0,1)$, and Assumptions 1, 2, 3 and 6 as printed. Two hypotheses are added and disclosed:
  • Assumption 5 is required strictly for $\delta_L$, $1+r(\lambda,\delta_L)<pR$. With equality the GP's profit does not depend on the fee, and the strict ranking of returns fails.
  • $B\le p(p-q)R$ makes limited liability compatible with incentive compatibility at every call share. The paper's Claim A.1 assumes the stronger $R\ge B/(p-q)^2$.
• Fee schedules are indexed by the four success outcomes rather than the four cash-flow values. These differ only at $x=1/2$, and the minimal fee is the same.
• Equation (3) is stated multiplied out with $I>A$, never as a quotient. A return at which the GP's profit is unbounded therefore admits no optimal contract and cannot be an equilibrium price. Contract optimality is global over $(x,I,f)$.
• Definition 2 is read with $\alpha_L+\alpha_H=1$, which the proof uses. GP fund choice is read as "a raised fund type is profit-maximizing", the only-if direction of the printed biconditional. The literal biconditional admits no equilibrium at $\mu_H=\underline\mu_H$.
• Two printed boundaries are corrected. Proposition 2 i) is stated for $\mu_H<\underline\mu_H$, which resolves the overlap of its two cases as the proof does. "Decreasing" is read as strict.
• Out of scope. Assumption 4 and capital-call relief (Appendix C.1) are not formalized, since the no-default constraint (4) is imposed directly. The GP takes $\bar R$ as given, so raising the promised return (C.2) is not modelled. Appendix A's alternative contracts and the "no fund" option are also out of scope.
• Trivializations ruled out. The goal asserts existence of an equilibrium for every $\mu_H\in(0,1)$, so its "every equilibrium" clauses are not vacuous. The strict chain $0<\underline\mu_H<\bar\mu_H<1$ excludes degenerate thresholds.

Everything is built from Mathlib's real numbers and finite sums. The fee-schedule linear program (Lemma 2), the contract problem (Proposition 1) and the equilibrium predicate are reusable for the secondary-market mission of the same paper. Proofs of any milestone, and the pinned-threshold variant of the goal, are welcome.

Selected references

• V. Maurin, D. T. Robinson and P. Strömberg, A Theory of Liquidity in Private Equity, working paper, draft of December 2020; published in Management Science 69(10), 2023. https://doi.org/10.1287/mnsc.2022.4612
• S. N. Kaplan and A. Schoar, Private Equity Performance: Returns, Persistence, and Capital Flows, Journal of Finance 60(4), 1791–1823, 2005. https://doi.org/10.1111/j.1540-6261.2005.00775.x
• J. Lerner, A. Schoar and W. Wongsunwai, Smart Institutions, Foolish Choices: The Limited Partner Performance Puzzle, Journal of Finance 62(2), 731–764, 2007. https://doi.org/10.1111/j.1540-6261.2007.01220.x

Motivation

Many service platforms set a price paid by customers and a wage paid to the providers who serve them. A platform may instead announce how much of each transaction's price it will pass to providers, then choose prices after both platforms have announced their shares. These are different games: a price change in the second game changes both customer demand and provider pay. Hu and Liu's study of precommitments in two-sided competition asks which timing gives platforms a more favorable equilibrium. This mission isolates their comparison between a commission precommitment and no commitment, Proposition 3(b) of the submitted manuscript. The authors' Online Appendix, included in that manuscript, contains the proofs.

The comparison is useful where a platform must choose a contract with providers before it can adjust customer prices. It is not enough to know that either side of the market is competitive: the answer changes as demand-side and supply-side competition intensities move relative to each other. The mission makes the claimed parameter regions precise and ties them to equilibria of the two games.

Setting

There are two platforms, indexed by $i=1,2$, with rival $j\ne i$. Platform $i$ posts a consumer price $p_i$ and a provider wage $w_i$. Fix a potential market size $\Omega>0$. The demand substitution factor $\gamma\in[0,1)$ measures how a rival's price raises demand for platform $i$. The supply substitution factor $\beta\in[0,1)$ measures how a rival's wage draws providers away. The paper uses the positive part $[x]^+=\max\{x,0\}$:

$$d_i(p)=[\Omega-p_i+\gamma p_j]^+,\qquad s_i(w)=[w_i-\beta w_j]^+.$$

The number of completed matches is $z_i=\min\{d_i(p),s_i(w)\}$. Profit is $\pi_i=(p_i-w_i)z_i$. Unmatched consumers or providers generate no revenue. Keeping the positive parts matters when a platform chooses a price or wage that leaves one side of the market empty.

In mode P, both platforms choose their prices and wages simultaneously, and each can change its own price and wage together while its rival's choices stay fixed. In mode C, each platform first commits to a pay-out ratio $\alpha_i\in(0,1)$. The provider then receives $w_i=\alpha_i p_i$ per match and the platform keeps $1-\alpha_i$ of its price. After observing both ratios, the platforms choose prices. Their profit in this second stage is

$$\pi_i(\alpha,p)=(1-\alpha_i)p_i\min\{d_i(p),s_i(\alpha p)\}.$$

A subgame-perfect equilibrium in mode C specifies a price equilibrium after every admissible pair of ratios and an initial pair of ratios that resists unilateral deviation when prices are chosen again. The mission compares symmetric commission equilibria to the positive-profit equilibrium of mode P. In the paper's platform preference ranking, $X\succeq Y$ means that mode $X$ gives each platform a weakly higher price and profit, and a weakly lower wage and matching quantity, than mode $Y$.

Formalization targets

No commitment and commission outcomes

Lemma 1 gives the simultaneous price-and-wage outcome. Writing $D=4-3\beta-3\gamma+2\beta\gamma$, its price, wage, matching quantity, and profit are

$$p_P^*=\frac{3-2\beta}{D}\Omega,\quad w_P^*=\frac{\Omega}{D},\quad z_P^*=\frac{1-\beta}{D}\Omega,\quad \pi_P^*=\frac{2(1-\beta)^2}{D^2}\Omega^2.$$

Lemma F.2 says that second-stage commission prices equate demand and supply. Lemma 4 characterizes the symmetric commission equilibrium by the radical $\alpha^*$ in equation (7), its price $p_C^*=\Omega/[1-\gamma+(1-\beta)\alpha^*]$, and its profit in equation (9). These are the three milestones. The radical is transcribed exactly in the Lean definition associated with equation (7).

Proposition 3(b)

The goal compares the two equilibrium outcomes using all four components of the platform preference ranking:

$$\gamma\geq\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\ll\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\leq\beta\text{ and sufficiently close to }\beta\ \Longrightarrow\ P\succeq C.$$

The two informal proximity phrases are expressed by the existence of positive thresholds, with the threshold allowed to depend on $\beta$. At $\gamma=\beta$, both rankings can hold because the outcomes coincide. The goal also asserts that the equilibria being compared exist for every admissible parameter pair.

Significance

The result identifies when committing to a provider share yields a platform outcome that is preferable to choosing price and wage together. Its four-way comparison is stronger than a profit-only ranking: the associated prices, wages, and match counts all move in specified directions. It makes clear that the relative competition intensities on the two sides determine whether the timing of the provider contract helps or hurts platforms. Without the comparison, the closed-form equilibrium results for modes P and C would not say which contract timing platforms prefer.

The result is proved in the cited manuscript, with derivations in Online Appendix §F; it is not an open mathematical conjecture. The remaining work in this mission is a machine-checked Lean proof of the equilibrium statements and the parameter-region comparison. The development will also provide a reusable formal model of simultaneous and two-stage decisions in a two-sided market. No existing machine-checked proof of this particular comparison is identified in the local Prove2Me index.

Difficulty

A change in a commission ratio changes the wage at any given price, while the subsequent price decision changes both demand and the wage again. That coupling makes the comparison more delicate than ordering two prices by inspection. The commission equilibrium ratio contains a square root, and the ranking must establish the directions of four outcome quantities in several parameter regions. The apparent shortcut of comparing profits alone would leave three of Definition 1's required inequalities unresolved. The positive-part demand and supply functions also admit zero-match equilibria that complicate an unqualified uniqueness statement.

Formalization scope

The Lean development uses real-valued prices and wages, two platforms indexed by Fin 2, and all unilateral deviations in the stated strategy sets. Market size is positive, both substitution factors lie in $[0,1)$, and pay-out ratios lie in $(0,1)$. The paper does not spell out the strategy sets; these choices preserve the derivations in §3 and Appendix §F. The no-commitment uniqueness statement is restricted to equilibria where both platforms profit, because the literal unrestricted claim has zero-profit counterexamples. A second-stage strategy in mode C selects an equilibrium with positive profits for both platforms whenever one exists. This condition prevents off-path zero-profit punishments from making the printed symmetric SPE claim false.

The goal quantifies over equilibria derived from the demand, supply, match, and profit functions. It does not define an outcome to equal the paper's closed form, and it asserts equilibrium existence so that its universal comparisons have content. The radical for $\alpha^*$ is a named expression; Lemma 4, rather than its definition, establishes its equilibrium role. A full proof needs reasoning about unilateral deviations, positive-part functions, equilibrium existence and uniqueness, the radical expression, and real inequalities. The general Nash condition and the paper's market primitives are intended for reuse in other two-player platform games. Contributions addressing these foundations and any of the three cited milestones are within scope. Wage- and price-precommitment modes are outside this mission.

Selected references

• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, submitted manuscript with Online Appendix associated with the 2023 publication, SSRN 3734828. Manuscript.
• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, Manufacturing & Service Operations Management 25(2), 704–718, 2023. DOI.

Motivation

Reinforcement learning in a changing environment has a difficulty that is absent from a fixed Markov decision process: transition data gathered earlier may describe a different system from the one the decision maker currently faces. A learning algorithm therefore estimates transitions from a recent window of observations. The estimate comes with a confidence region, a set of transition laws consistent with the data at a chosen statistical radius. In the general nonstationary setting studied by Cheung, Simchi-Levi and Zhu, their algorithm widens this region to ensure that it can contain a model whose states remain readily reachable. Such a model is needed for the paper's dynamic regret analysis. Section 7 isolates a structural condition under which widening is unnecessary: every destination is reachable from every state with a uniformly positive one-step probability under a suitable action. Cheung, Simchi-Levi and Zhu, §7.

This mission formalizes Proposition 4 of that paper, the precise claim that the original, unwidened transition region contains a model with a controlled diameter. It is one of three separate missions for the paper. The result supports the paper's no-widening variant of its learning algorithm; it is not a claim that every model in the confidence region has small diameter. Cheung, Simchi-Levi and Zhu, Proposition 4.

Setting

There are finitely many states $\mathcal S$ and, for each state $s$, a nonempty finite set $\mathcal A_s$ of permitted actions. At each time $t\in[T]$, the system has a reward $r_t(s,a)\in[0,1]$ and a probability distribution $p_t(\cdot\mid s,a)$ for the next state. The distribution may change with $t$. A trajectory records the observed state $s_q$, chosen action $a_q$, and successor state $s_{q+1}$ at each time $q$. These are the model primitives in §2.2. Cheung, Simchi-Levi and Zhu, pp. 6–7.

An episode begins at $\tau(m)$ and uses a window of length $W$. At time $t$ in that episode, $N_t(s,a)$ counts how often the pair $(s,a)$ appears between $(\tau(m)-W)\vee1$ and $t-1$; $N_t^+(s,a)=\max\{1,N_t(s,a)\}$. The empirical row $\hat p_t(\cdot\mid s,a)$ counts observed successors and divides by $N_t^+(s,a)$. The corresponding average true row $\bar p_t$ averages the time-varying transition probabilities over the same visits. Both are zero vectors when there are no visits. Cheung, Simchi-Levi and Zhu, equations (3) and (5).

Write $SA=\sum_s|\mathcal A_s|$, so this is the number of allowed state-action pairs. At confidence level $\delta$, the transition radius is $\operatorname{rad}_{p,t}(s,a)=2\sqrt{2S\log(SAT/\delta)/N_t^+(s,a)}$. The region $H_{p,t}(s,a;\eta)$ consists of probability vectors within $\ell_1$ distance $\operatorname{rad}_{p,t}(s,a)+\eta$ of $\hat p_t$. Here $\eta=0$ means no widening. The estimation event $E_p$ bounds the $\ell_1$ distance between $\bar p_t$ and $\hat p_t$ by that radius for each allowed pair. Cheung, Simchi-Levi and Zhu, pp. 12, 14.

For a stationary transition model and policy $\pi$, the hitting time $\Lambda(s'\mid\pi,s)$ counts transitions until the first arrival at $s'$ after starting at $s$. This includes the first return time when $s=s'$. Its diameter is $D=\max_{s,s'}\min_\pi\mathbb E[\Lambda(s'\mid\pi,s)]$. Infinite expectations are possible in the definition. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization targets

Goal: Proposition 4

Assumption 2 supplies $\zeta>0$ and an allowed action $a_{(s,s')}$ for every ordered pair of states, fixed across time, such that $p_t(s'\mid s,a_{(s,s')})\ge\zeta$ for all $t\in[T]$. Conditional on $E_p$, Proposition 4 says that for every time in the horizon there exists a transition model $p$ whose every allowed row belongs to $H_{p,t}(s,a;0)$ and whose diameter obeys

$$D(\mathcal S,\mathcal A,p)\le\bar D:=\frac1\zeta.$$

The target is existential: the region need only contain one such model at each time. The milestone list follows the two cases in the proof of Lemma 13, the lemma's model existence claim, and the expected hitting-time bound in the proof of Proposition 4. Cheung, Simchi-Levi and Zhu, pp. 21, 49–50.

Significance

Proposition 4 identifies a condition under which the algorithm can use $\eta=0$ while retaining a uniform diameter guarantee for at least one plausible transition model. The paper uses this to analyze a no-widening version of its dynamic regret bound, and later applies that viewpoint to inventory control. Without a bounded-diameter model in the region, the diameter-dependent regret argument does not apply in the same form. Cheung, Simchi-Levi and Zhu, §7.

The proposition and its appendix proof are known results of the paper. This mission asks for a machine-checked account of the exact confidence region, its pathwise estimation event, Lemma 13, and the diameter claim. A general finite MDP with probability-valued transition rows is already available as the published FiniteMDPLearning definition; the paper-specific window estimators and its return-time diameter still need formal proofs. The paper's headline Theorems 1–4 are not posed here because their displayed bounds hide constants in $\widetilde O(\cdot)$ notation. Cheung, Simchi-Levi and Zhu, p. 6 and Theorems 1–4.

Difficulty

The obvious idea that the true transition law belongs to the confidence region can fail under drift: the region is centered on recent observations, while the law at the current time may differ from the laws that generated those observations. Even the average true row has a special case. At an unvisited pair, equation (5) sets it to the zero vector, which is not a probability distribution and therefore is not a member of the simplex-valued confidence region. The existence claim must cover visited and unvisited pairs while preserving one-step reachability for all targets under a single transition law. Cheung, Simchi-Levi and Zhu, pp. 12, 49–50.

The diameter also uses the paper's first-arrival-after-start convention. A library travel time that is zero when source equals target misses the return-time cases and would weaken the stated conclusion. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization scope

States and actions are Fin S and Fin A; permitted actions are state-dependent finite sets. Extra MDP rows for disallowed actions are never consulted. The finite MDP type supplies valid probability rows and bounded rewards. Hitting times and the diameter use extended nonnegative reals, so infinite values are represented without a default real value. The diameter ranges over allowed deterministic stationary policies and over all ordered state pairs, including equal pairs. Time is zero-based in Lean: paper time $t\in[T]$ is index $t-1<T$, and the paper's window becomes the half-open interval [τm-W,t). The paper's $N^+$ is at least one, so its estimators never divide by zero. A result at arbitrary $t$ with $\tau_m\le t<T$ covers every episode time without assuming any additional episode schedule property.

The Lean statement makes two domain conditions explicit: $S>1$ and $0<\delta<1$. These ensure the paper's claim that the radius at an unvisited pair is at least one; it can fail when $S=1$ and the confidence level is close to one. Assumption 2 is required for every time in the horizon, with $\zeta>0$. The event $E_p$ is the $\ell_1$ estimation inequality at the selected time. The paper writes it as membership of $\bar p_t$ in a simplex-valued region for every pair, but that literal wording is false at an unvisited pair because $\bar p_t=0$ there. At visited pairs, the inequality and membership agree. This convention is disclosed in the definition item and keeps the theorem meaningful on ordinary early trajectories.

The region is centered at the exact empirical $\hat p_t$, uses $\eta=0$, and constrains every allowed row of the constructed model. The diameter uses its full extended-real value, and $\zeta$ is strictly positive; dropping any of these clauses would change the claim. Reusable contributions include finite-state hitting-time estimates and windowed transition estimation identities. Proofs of the four milestones and the goal, as well as small lemmas connecting the published MDP measure to successive transition rows, are welcome.

Selected references

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

Motivation

After a sudden-onset disaster, humanitarian organizations (HOs) raise most of their response budget from private donors within days. Donors increasingly earmark their gifts, restricting them to a region, a program or a type of expense. Earmarking makes an appeal more attractive to a donor but lowers the share of each dollar that the HO can deploy immediately. Aflaki and Pedraza-Martinez (SSRN 3705595, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202) model how HOs set earmarking and fundraising effort under three institutional arrangements: competition, full collaboration (a coalition that fundraises and decides as one), and partial collaboration, in which HOs pool the cost of reaching donors on a common platform while each donor still chooses which HO to give to. Joint appeals such as the UK's Disasters Emergency Committee are of the last kind.

This mission formalizes the paper's equilibrium result for partial collaboration (Proposition 4): equilibria exist, equilibrium earmarking is determined by first-order conditions that do not involve the efforts, and only the HOs with the largest required funding relative to their unit performance pay for the platform, while the others free-ride.

Setting

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$. HO $i$ chooses a base utility $s_i \in [a_i, b_i]$, the attractiveness to donors that its earmarking level induces, and an effort $x_i \in [0, 1]$, the fraction of donors it pays to contact, at cost $C_i(x_i)$. Its unit performance $\delta_i(s_i) \in (0, 1]$ is the fraction of each donated dollar usable now, and $B_i > 0$ is its required funding. The mean donation is normalized to $1$.

Pooled effort reaches $\bar x = \min\left(\sum_{i \in I} x_i, 1\right)$ donors. A contacted donor gives to HO $i$ with the multinomial-logit probability

$$\theta^p_i(s) = \frac{e^{s_i}}{1 + \sum_{j \in I} e^{s_j}},$$

the $1$ being the option of not donating, so HO $i$ expects donations $\bar x\,\theta^p_i(s)$ and achieves total performance $\delta_i(s_i)\,\bar x\,\theta^p_i(s)$, of which only $\min(\cdot, B_i)$ is useful. HO $i$ is lexicographic (problem (10)): given the other HOs' strategies, it first minimizes its funding gap $\left(B_i - \delta_i(s_i)\bar x\theta^p_i(s)\right)^+$ over $[a_i, b_i] \times [0,1]$; among the gap minimizers it maximizes its utility $\min\left(\delta_i(s_i)\bar x\theta^p_i(s), B_i\right) - C_i(x_i)$; and an HO that is still indifferent picks a strategy maximizing its unconstrained total performance $\delta_i(s_i)\bar x\theta^p_i(s)$. A Nash equilibrium is a profile $(s, x)$ in the product of the boxes at which every HO's strategy is such a best response. Finally,

$$\alpha^p_i(s) = \min\left(\frac{B_i}{\delta_i(s_i)\,\theta^p_i(s)}, 1\right)$$

is the reach HO $i$ needs to close its own gap.

Formalization targets

Goal: Proposition 4

A pure Nash equilibrium exists. For every profile $(s, x)$ in the box, labelled so that $\alpha^p_1(s) \ge \dots \ge \alpha^p_n(s)$, with $\bar k = \#\{i : \alpha^p_i(s) = \alpha^p_1(s)\}$: $(s, x)$ is an equilibrium if and only if (i) for every $i$ there are $\lambda^p_{i1}, \lambda^p_{i2} \ge 0$ with

$$\frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\partial \theta^p_i(s)/\partial s_i}{\theta^p_i(s)} + \lambda^p_{i1} - \lambda^p_{i2} = 0, \quad \lambda^p_{i1}(a_i - s_i) = 0, \quad \lambda^p_{i2}(s_i - b_i) = 0, \tag{11}$$

and (ii) $\sum_{i=1}^{\bar k} x_i = \alpha^p_1(s)$ and $x_{\bar k+1} = \dots = x_n = 0$.

Milestones

1. (S11): $(s, x)$ is an equilibrium iff each $s_i$ maximizes $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ on $[a_i, b_i]$ and $x_i = \left(\alpha^p_i(s) - \sum_{j \ne i} x_j\right)^+$.
2. Log-concavity: $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ is log-concave on $[a_i, b_i]$.
3. Total effort: every solution of $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ with $\alpha$ sorted decreasingly has $\sum_i x_i \ge \alpha_1$.
4. Effort system: for $1 \ge \alpha_1 \ge \dots \ge \alpha_n \ge 0$ and $x \in [0,1]^n$, that system holds iff $\sum_{i \le \bar k} x_i = \alpha_1$ and $x_i = 0$ for $i > \bar k$.

Significance

The proposition separates the two decisions. Equilibrium earmarking solves each HO's own first-order condition (11) and does not depend on anyone's effort, because the pooled reach multiplies every HO's donations by the same factor. Equilibrium effort is a pure coordination outcome: the platform is funded exactly up to the largest required reach $\alpha^p_1$, and only the HOs attaining it contribute. The paper uses these facts to compare earmarking and performance across the three arrangements (its Propositions 5 and 7), and the free-riding structure is what drives the comparison of partial collaboration with competition.

The result is proved in the paper's Online Supplement (pp. S13–S14). No machine-checked version exists. The mission asks for a Lean proof of the proposition as stated, with the equilibrium defined from the HOs' lexicographic problem rather than from its characterization; the effort-system milestones are self-contained statements about a piecewise-linear fixed-point system and are reusable for other pooled-contribution games.

Difficulty

The obvious argument, "each HO maximizes $\delta_i\theta^p_i$, and the rest is bookkeeping", skips the case analysis behind (S11). Whether HO $i$'s gap can be closed depends on the others' efforts. When the others' pooled effort already covers HO $i$'s requirement, HO $i$'s gap and utility no longer depend on its base utility. Only the third, tie-breaking level of the best response then pins $s_i$ down, and without it (11) is false. The existence part needs a fixed point of the base-utility best-response map on $\prod_i [a_i, b_i]$; when HO $i$'s best response is not unique, that map is not even a function. In part (ii), the effort system $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ is not a contraction, and the paper's proof by successive elimination of indices is informal.

Formalization scope

HOs are Fin n with 0-based indices, so $\alpha^p_1$ is the value at index 0, and [NeZero n] is assumed. Strategies are in base-utility coordinates: $\delta_i : \mathbb R \to \mathbb R$ is a primitive function of $s_i$, as in the paper's problem (10). The earmarking coordinates are not modelled. All definitions live in one Setting structure with a Standing predicate, which every theorem assumes:

• $a_i \le b_i$ and $B_i > 0$;
• $C_i$ is nonnegative and strictly increasing on $[0,1]$;
• on an open interval containing $[a_i, b_i]$, $\delta_i$ is positive, differentiable and concave;
• $\delta_i \le 1$ on $[a_i, b_i]$.

$B_i > 0$ is implicit in the paper; with all $B_i = 0$ every base utility is an equilibrium strategy. Concavity of $\delta_i$ is used by the paper's proof. The HO problem (10) is printed with decision $(s_i, \bar x)$ and cost $C^p(\bar x)$. It is encoded with HO $i$'s own effort $x_i$ and own cost $C_i(x_i)$, the reading used by the paper's proof and by part (ii). The paper's "without loss of generality" ordering is the hypothesis that $\alpha^p(s)$ is antitone in the index, and $\bar k$ is the number of entries tied with the first; this gives $\bar k = n$ when all tie. Partial derivatives are Mathlib deriv of $t \mapsto \theta^p_i(s \text{ with } s_i := t)$. Every function differentiated is differentiable at the point by Standing. The pure-algebra milestones 3–4 use no game objects.

The equilibrium must not be defined by (S11) or (11); that would make the goal a tautology. The Setting defines it as the three-level lexicographic best response over the full strategy box, and (S11) is a milestone to be proved. A sorry-free check that the standing hypotheses hold for the paper's numerical primitives ($\delta_i(s) = 1 - s/4$, $C_i(x) = x/10$, $[a_i, b_i] = [0,1]$, $B = (0.2, 0.3)$) accompanies the draft.

A full development needs: KKT conditions for a differentiable concave function on a compact interval (including the degenerate interval $a_i = b_i$); log-concavity of the logistic share; a continuous-maximum (Berge-type) argument and Brouwer's fixed-point theorem on a product of intervals; and the algebra of the effort system. Contributions of the interval-KKT lemma and of the effort-system lemmas are welcome as separate theorems.

The source is the authors' SSRN version (abstract 3705595, dated December 2022); all proofs are in its Online Supplement, Section S3.

Selected references

• A. Aflaki, A. J. Pedraza-Martinez, Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance, SSRN 3705595, version of December 2022. https://ssrn.com/abstract=3705595
• A. Aflaki, A. J. Pedraza-Martinez, same title, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1202