Algorithmic Game Theory

Motivation

In reward-based crowdfunding, a seller asks customers to pay before the product's quality is known to them. A high-quality seller can try to communicate private quality through the prices he posts. That signal is costly because a price that deters imitation may also reduce the seller's own expected revenue. Bolandifar, Chen, Kouvelis and Zhou study this tradeoff when a campaign must meet a financing target and a successful campaign leads to a later retail period (SSRN manuscript, §§3–5). Their model asks whether a high-quality seller can separate himself from a low-quality seller by committing in advance to both the crowdfunding price and the later retail price.

The manuscript treats price commitment separately from the case in which the seller chooses the retail price after the campaign. This mission concerns the commitment case, specifically Proposition 2 and the lemmas that support it. The theorem describes a separating equilibrium after applying the intuitive criterion: the high-quality seller chooses a lower crowdfunding price and a higher retail price than he would under full information. The cited artifact is the authors' SSRN manuscript dated 2022-05-30; its proofs are in Appendix A (manuscript, pp. 38–43).

Setting

There are two privately known product qualities, $0<q_L<q_H$. A seller commits to a price pair $x=(P_1,P_2)$, where $P_1$ is paid by crowdfunding backers and $P_2$ is charged in the regular selling period. The project needs a financing target $T>0$, so a feasible pair satisfies $P_1\ge T$ and $P_2>0$. Both period market sizes are normalized to one; production and salvage costs are zero, and future revenue is not discounted (manuscript, pp. 9–13).

All funding customers have the same taste $\theta_c$, uniformly distributed on $[0,1]$ and unknown to the seller. They believe quality is $q_j$ and back the campaign when $\theta_c q_j\ge P_1$. Thus success has probability $\max\{0,1-P_1/q_j\}$. After a successful campaign, true quality $q_i$ becomes known. A fraction $\alpha\in(0,1)$ of regular customers have the same taste as the funding customers; success updates their conditional taste distribution. The remaining fraction has independent uniform tastes. A customer in the regular period buys if taste times $q_i$ is at least $P_2$ (manuscript, pp. 10–11).

Write $\Pi^{ij}(P_1,P_2)$ for the seller's expected total profit when true quality is $q_i$ and customers believe $q_j$. The expressions $V^{ij}$ and $W^{ij}$ distinguish the regions in which returning customers buy for sure or with a conditional probability. Write $\Pi^{ij*}$ for the maximum of $\Pi^{ij}$ over feasible pairs. In particular, $\Pi^{L*}=\Pi^{LL*}$ is the low type's full-information payoff. These are outcomes of optimization, not inserted formulas (manuscript, pp. 22–24, (7)–(11)).

In a separating equilibrium, the two seller types choose different feasible pairs $x_H$ and $x_L$. Funding customers believe the product is high quality exactly at $x_H$ and low quality at every other pair, including off-path pairs. Neither seller type can gain by deviating under those beliefs. The intuitive criterion then checks whether an off-path pair would be profitable to the high type if believed high while being unattractive to the low type (manuscript, pp. 13, 19).

Formalization targets

Lemma 4 identifies an attained full-information optimum for any choice of true and believed quality in $\{q_L,q_H\}$. Its crowdfunding price is

$$P_1^{ij*}=\max\left\{\frac{4q_j-(1-\alpha)q_i}{8},T\right\},$$

and its retail price follows the three cases of equation (11), depending on whether $T$ lies below $q_j/2$, between that threshold and $q_j/[2(1-\alpha)]$, or above the second threshold (manuscript, p. 23, Lemma 4).

The goal is Proposition 2 in the small-quality-gap regime $q_L<q_H\le(\alpha^2+6\alpha+25)q_L/16$. Define $(\dot P_1,\dot P_2)$ by its equations, requiring $\dot P_2>q_H/2$:

$$4\dot P_1+(1-\alpha)\dot P_2=2q_H,\qquad W^{LH}(\dot P_1,\dot P_2)=\Pi^{L*}.$$

When $T\le\dot P_1$, the goal states that the unique separating equilibrium surviving the intuitive criterion has $x_H=(\dot P_1,\dot P_2)$ and the low type at his full-information optimum. Relative to every full-information optimum $(P^H_{1f},P^H_{2f})$ of the high type, it also states

$$\dot P_1<P^H_{1f},\qquad \dot P_2>P^H_{2f}.$$

The mission separately targets uniqueness of the dotted pair, the first claim of Lemma 6 concerning profitable imitation of the high type's full-information pair, and the constrained optimum in equations (A.13)–(A.14) (manuscript, pp. 26–27, 41).

Significance

The result identifies how a commitment to the later price changes the signal available during crowdfunding. The high type's retail price is raised while his crowdfunding price is lowered, so the signal is encoded in the pair, rather than in a single crowdfunding price. The theorem also determines which separating outcome survives a refinement intended to remove equilibria supported only by arbitrary off-path beliefs (manuscript, pp. 26–27).

The mathematical result is already proved in the manuscript. The remaining formalization work is to give the economic model an exact Lean meaning, prove the optimization and equilibrium assertions, and make the boundary conventions explicit. The five open Lean theorems in this proposal are statements to be proved; their sorry bodies are not machine-checked proofs.

Difficulty

The seller's payoff changes expression when the regular price crosses a threshold determined by the funding price and the two qualities. The low type can mimic a pair whose regular price exceeds $q_L$, in which case regular sales vanish but the crowdfunding payoff can still rise. This makes a direct comparison of the printed $W^{LH}$ expression with the actual mimicking payoff invalid outside its demand region. The intuitive criterion adds a second layer: it tests deviations under a different belief from the default off-path belief. These regime changes and belief-dependent deviations are the central obstacles to a concise, faithful Lean statement (manuscript, pp. 23, 26–27, 41–43).

Formalization scope

Lean represents qualities, prices, probabilities and payoffs as real numbers. Its parameter structure contains $q_L,q_H,\alpha,T$, with $0<q_L<q_H$, $0<\alpha<1$ and $T>0$. The prior high-quality belief is omitted because the separating statements use beliefs fixed by the observed pair. Market sizes, zero costs, salvage value and discount rate are incorporated into the payoff. The funding success probability and purchase probabilities are clipped at zero outside their printed domains. The printed $V^{ij}$ and $W^{ij}$ remain available for the page 41 equations; $W^{ij}$ is only used away from its zero denominator. Suprema range over all feasible pairs $P_1\ge T$, $P_2>0$, and “optimal” means the displayed pair attains that supremum.

The manuscript's Proposition 2 needs the additional bound $T\le(3+\alpha)q_L/8$. Without it, the low type's constrained full-information payoff can be too small and he can profitably mimic a dotted pair with $\dot P_2>q_L$; a numerical counterexample and the discrepancy are recorded in the local moderation notes. This proposal states that bound openly rather than treating the printed proposition as valid for all $T\le\dot P_1$. Lemma 4 also records its displayed domain $T\le q_j$. The goal does not define the optimum by a formula, the equilibrium by the paper's necessary conditions (13)–(14), or the dotted pair by an arbitrary choice.

The foundational setting is a reusable two-type, two-price payoff and equilibrium model. A complete development must establish the payoff's agreement with the manuscript's regions, attainment and comparison of the full-information optima, uniqueness of the dotted pair, optimization on the relevant iso-profit curve, and the no-deviation and intuitive-criterion conclusions. Contributions proving these targets or reusable real optimization lemmas are within scope.

Selected references

• E. Bolandifar, Z. Chen, P. Kouvelis and W. Zhou, Quality Signaling through Crowdfunding Pricing, SSRN manuscript 3689946, 2022-05-30, SSRN. Published as Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1177.

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

Fundraising competition after a disaster

In the days after a sudden-onset disaster, several humanitarian organizations (HOs) appeal to the same pool of donors. Donors increasingly want to earmark their gifts (restrict them to a programme, region or item), and HOs can offer more or less of that control. Earmarked money is less useful in the response: renegotiating restrictions costs time and overhead, so each dollar delivers less immediate relief. HOs therefore face a trade-off between attracting donors and using donations well, and they face it while competing with each other for the same donors.

A. Aflaki and A. J. Pedraza-Martinez model this trade-off as a game among HOs whose donors choose by a multinomial logit (MNL) rule, and compare three regimes: competition, full collaboration and partial collaboration (SSRN 3705595, December 2022; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202). This mission formalizes the equilibrium result for the competition regime, Proposition 1 of the paper. The source is the SSRN version dated December 2022; its proofs are in the bound-in Online Supplement (§S3).

The competition game

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$. HO $i$ chooses two numbers:

• a base utility $s_i \in [a_i, b_i]$ that it offers donors (in the paper, a monotone reparametrization of its earmarking level, used from problem (6) on);
• a fundraising effort $x_i \in [0,1]$, the fraction of donors it contacts, at cost $C_i(x_i)$ with $C_i : [0,1] \to \mathbb R_+$ strictly increasing.

Each dollar HO $i$ receives produces $\delta_i(s_i)$ dollars of immediate relief, the unit performance. HO $i$ needs $B_i > 0$ dollars of effective funding. Donors have mean budget $z > 0$.

A donor contacted by the set $J$ of HOs gives HO $i \in J$ the MNL share

$$\theta^J_i(s) = \frac{e^{s_i}}{1 + \sum_{j\in J} e^{s_j}}, \tag{4}$$

the $1$ standing for not donating. Contacts are independent, so with $w^a_i = \prod_{j \ne i} x_j^{a_j}(1-x_j)^{1-a_j}$ for $a \in A_i = \{a \in \{0,1\}^n : a_i = 1\}$ and $J_a = \{j : a_j = 1\}$, HO $i$'s expected donations are

$$\mathbb E[D_i(s;x)] = z\, x_i \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s). \tag{5}$$

The unit performance per donor contacted is $PPD_i(s;x) = \delta_i(s_i)\, z \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s)$; it does not depend on $x_i$.

Each HO is lexicographic (problem (6)): given the others' strategies, it first minimizes its funding gap $(B_i - \delta_i(s_i)\mathbb E[D_i(s;x)])^+$ over $[a_i,b_i]\times[0,1]$, and among the minimizers it maximizes

$$U_i(s_i,x_i) = \min\big(\delta_i(s_i)\mathbb E[D_i(s;x)],\, B_i\big) - C_i(x_i).$$

A Nash equilibrium is a profile $(s;x) \in \prod_i [a_i,b_i]\times[0,1]^n$ in which every HO's strategy solves its problem (6).

Assumption 1 (p. 16) asks that $\log\delta_i$ be sufficiently concave: $\partial^2 \log\delta_i(s_i)/\partial s_i^2 \le -\tfrac14 + e^{s_i}/(1+e^{s_i})^2$ on $[a_i,b_i]$.

Formalization targets

Goal: Proposition 1 (p. 16)

Under the standing hypotheses and Assumption 1, a Nash equilibrium exists, and a profile in the strategy box is an equilibrium if and only if for every $i$

$$x_i = \min\Big(\frac{B_i}{PPD_i(s;x)},1\Big),\qquad \frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\sum_{a\in A_i} w^a_i\,\partial\theta^{J_a}_i(s)/\partial s_i}{\sum_{a\in A_i} w^a_i\,\theta^{J_a}_i(s)} + \lambda_{i1}-\lambda_{i2} = 0,$$

with $\lambda_{i1},\lambda_{i2}\ge 0$, $\lambda_{i1}(a_i-s_i) = 0$ and $\lambda_{i2}(s_i-b_i) = 0$ (system (7)).

Milestones

1. Lemma 2 (p. 15): $\mathbb E[D_i]$ is nondecreasing in $x_i$ and $s_i$ and nonincreasing in $x_j$, $s_j$ for $j\ne i$.
2. Claim (S5) (p. S10): HO $i$'s strategy solves (6) iff $s_i$ maximizes $PPD_i$ over $[a_i,b_i]$ and $x_i = \min(B_i/PPD_i,1)$.
3. (S8) (p. S12): $\partial^2 \log\big[\sum_{a} w^a_i\theta^{J_a}_i(s)\big]/\partial s_i^2 \le \tfrac14 - e^{s_i}/(1+e^{s_i})^2$ for efforts in $[0,1]$.
4. Log-concavity (p. S12): under Assumption 1, $s_i \mapsto PPD_i$ is log-concave on $[a_i,b_i]$.

Significance

Proposition 1 is the foundation of the paper's comparison of fundraising regimes: Propositions 2, 5, 6 and 7 compare equilibria characterized by (7) with the full- and partial-collaboration outcomes, and the numerical study of the Haiti response (§8) computes equilibria by solving (7). The proposition reduces a two-level game with a non-smooth objective to a per-HO KKT system plus a closed-form effort, and it shows that equilibrium earmarking balances the relative loss in unit performance against the relative gain in donor share.

The result is proved on paper, in the Online Supplement; no machine-checked version exists. Formalizing it would check the reduction from the lexicographic problem to (S5), which hinges on $B_i>0$ and strictly increasing costs, and supply a sound proof of the bound (S8), whose printed derivation is loose (see below). The log-mixture-of-logit bound (S8) and the lexicographic best-response reduction are reusable for other MNL competition models.

Difficulty

The central difficulty is (S8). Each single share $\theta^J_i$ is log-concave in $s_i$, but a mixture of log-concave functions is not log-concave in general, so concavity of $\log\sum_a w^a\theta^{J_a}$ fails and only the weaker, $s_i$-dependent bound (S8) holds. The printed argument passes through a quasi-concavity step and a termwise inequality that do not combine as written; a correct argument must control the variance-like term of the mixture uniformly in the weights. Numerical tests on random instances support (S8).

Existence is a fixed-point argument, but Assumption 1 with "$\le$" yields only concavity, so best responses in $s_i$ can be intervals rather than points, and a single-valued map need not exist. The correspondence is convex-valued, which is where the obvious Brouwer argument needs adjustment.

The reduction (S5) requires handling both regimes of the lexicographic problem: the gap can be closed (effort $B_i/PPD_i$, minimal cost) or cannot (full effort).

Formalization scope

HOs are Fin n. The paper's sum over $a\in A_i$ is a sum over finite sets $J$ with $i\in J$; $w^a_i$ is the product of $x_j$ over $J\setminus\{i\}$ and of $1-x_j$ over $j\notin J$. All statements live in base-utility coordinates: $\delta_i:\mathbb R\to\mathbb R$ is a primitive function of $s_i$ (earmarking $e_i$ and the map $s_i(e_i,\delta_i(e_i))$ are not modelled), and expected donations are the formula (5) (Lemma 1's Gumbel derivation is not formalized).

The standing hypotheses, collected in one predicate, are: $n\ge1$; $a_i\le b_i$; $B_i>0$; $z>0$; $C_i\ge0$ and strictly increasing on $[0,1]$; $\delta_i$ twice continuously differentiable on $\mathbb R$ with $0<\delta_i\le1$ on $[a_i,b_i]$. The additions relative to the page are $B_i>0$ (without it every $s_i$ is a best response and the "only if" fails), $z>0$, $\delta_i>0$ (needed for $\log\delta_i$ and $B_i/PPD_i$), and smoothness on all of $\mathbb R$ rather than on $[a_i,b_i]$. Assumption 1 is a separate predicate, assumed only by the goal and the log-concavity milestone. Derivatives are Mathlib's deriv; $\partial\theta^{J}_i/\partial s_i$ is the derivative of $t\mapsto\theta^J_i(s_{-i},t)$.

The equilibrium is defined as the lexicographic best response of problem (6) over the full strategy box, never by (7), (S5) or an argmax of $PPD_i$; with any of those as the definition the goal would be trivial. Multipliers are existential. Uniqueness of the equilibrium is not claimed.

Welcome contributions: proofs of the milestones, a reusable lemma that the KKT conditions characterize maximizers of a concave differentiable function on a closed interval, and Kakutani-type existence for convex-valued best responses.

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
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, 1973.

Motivation

Electric-vehicle makers such as NIO sell cars without the battery and lease the battery separately, a business model called Battery as a Service (BaaS). The leased battery can be swapped at a station in minutes, so a customer is not tied to one battery size: a driver who leases a small battery for the daily commute can rent a large one for a long holiday trip, and a driver who leases a large battery can downgrade for a while and pay less. Shi and Hu (M&SOM 2024, doi:10.1287/msom.2022.0587) ask whether such flexible battery leasing is good for all three parties at once: the manufacturer (profit), the customers (total cost) and the environment (total battery capacity that has to be produced). A business-model innovation of this kind is adopted only if it improves profit; it is defensible publicly only if it does not raise customer cost or the number of batteries in circulation. The paper's answer is a "win-win-win" region of parameters, and that result is the goal of this mission.

Setting

A manufacturer serves a unit mass of customers with two batteries. The low-capacity battery has range $r_l=0$, lease rate $p_l=0$ and acquisition cost $c_l=0$ (normalizations). The high-capacity battery has range $r_h$, lease rate $p_h$ and incremental acquisition cost $c_h$. Driving a distance beyond the battery's range costs the customer the shortfall: a need $x$ served by range $r$ costs $(x-r)^+$ plus the lease rate.

Each customer has a regular need $d\sim\mathcal U[0,1]$, known when choosing a primary battery, and a peak need $D\sim\mathcal U[0,a]$ with $a>1$, independent of $d$ and learned later. A fraction $\rho$ of the time is regular usage, $1-\rho$ peak usage. The standing assumptions are $a>1$, $a/(2+a)<\rho<1$, $0<r_h\le a$ and $0\le c_h\le(1-\rho)a$.

Simple leasing. The manufacturer sets $p_h$; each customer leases low capacity iff $\rho d+(1-\rho)\mathbb E[D]\le p_h+\rho(d-r_h)^++(1-\rho)\mathbb E[(D-r_h)^+]$. With $\tau^b$ the low-capacity volume, the profit is $\Pi^b=(1-\tau^b)(p_h-c_h)$, the total customer cost $CT^b$ is the integral over $d$ of the cost each customer bears, and the total battery capacity is $BT^b=(1-\tau^b)r_h$.

Flexible leasing. A two-period game. The manufacturer sets $p_h$; customers choose primary batteries anticipating the peak period; the manufacturer then sets an upgrade rate $\bar p_h$ and a downgrade rate $\bar p_l$; customers learn $D$ and choose whether to swap according to Table 1 of the paper (a low lessee pays $(D-r_h)^++\bar p_h$ after upgrading, a high lessee pays $D+\bar p_l$ after downgrading). Upgrades $U$ in excess of downgrades $V$ must be met by buying $Q_h=[U-V]^+$ extra high-capacity batteries. The peak-period objective is (1): $(1-\tau)p_h+V(\bar p_l-p_h)+U\bar p_h-c_hQ_h/(1-\rho)$, and the total profit is (2): $\Pi^f=\rho(1-\tau)p_h+(1-\rho)\cdot(1)-(1-\tau)c_h$. A flexible equilibrium is a lease rate $p_h$ with optimal peak rates, a lease volume $\tau$ that customers rationally expect, and a profit no other lease rate and continuation can beat. $CT^f$ is the total expected cost of the customers' choices, and $BT^f=(1-\tau+Q_h)r_h$.

Formalization targets

Write $c_0=a(1-\rho)/2$; by Proposition 2 this is the cost at which the manufacturer stops buying extra batteries.

Goal: Proposition 6 (win-win-win)

For $a>1$, $a/(2+a)<\rho<1$:

1. if $\rho<7a/(8+7a)$, there is $\delta>0$ such that for each $c_h\in(c_0-\delta,c_0)$ there is $R<a$ such that for all $r_h\in(R,a]$, a benchmark optimum and a flexible equilibrium exist, and every pair of them satisfies

$$Q^f_h>0,\qquad \Pi^b<\Pi^f,\qquad CT^f<CT^b,\qquad BT^f<BT^b;$$

2. there is $\delta>0$ such that for each $c_h\in(c_0,c_0+\delta)$ there is $R<a$ such that for all $r_h\in(R,a]$, the same holds with $Q^f_h=0$.

Milestones

Lemma 1 and Proposition 1 (the benchmark), Lemma 2 (peak volumes), Lemma 3 (optimal peak rates), Lemma 4 (flexible lease volume), Proposition 2 in its first case (the flexible equilibrium for $c_h<c_0$), Proposition 4 near the corner $(r_h,c_h)=(a,c_0)$ (customer cost), and Proposition 5 in its first bullet (capacity is smaller iff $\rho<7a/(8+7a)$ and $c_h\le T(r_h)$ for an explicit $T$).

Significance

The result identifies conditions under which a pricing innovation helps the firm, its customers and the environment at the same time: a battery cost near $a(1-\rho)/2$ and a high-capacity range close to the largest peak need. Flexible leasing reallocates high-capacity batteries from customers who do not need them in the peak period to customers who do, so fewer batteries have to be produced. But the manufacturer prices the up/downgrade options to extract the efficiency gain and may buy extra batteries, so lower customer cost and lower capacity are not automatic. Proposition 6 states where all three improvements coexist.

The paper proves its results by calculus on closed forms. Nothing here is machine-checked yet. A formalization adds three things. First, it derives the closed forms from the model itself (customer choices from Table 1, volumes as measures of customer sets, equilibria as maximizers), where the paper states them. Second, it settles which reading of "sufficiently close" and "sufficiently large" is true. Third, it records the regimes in which the intermediate lemmas hold, which the printed statements leave implicit.

Difficulty

The closed forms of Lemmas 1–4 are routine integrals of piecewise-linear functions. The difficulty is global optimality and the corner analysis.

• Equilibrium is global. A flexible equilibrium must beat every lease rate together with every rationally expected continuation, including continuations in the regime where the manufacturer buys no extra batteries and at lease rates where customers all lease one type. A first-order condition on one regime does not establish this.
• The $Q^f_h=0$ side is not the printed one. For $c_h$ just above $c_0$ the equilibrium is a kink regime that the paper does not describe. The paper's second-case formulas in Proposition 2 are not the equilibrium there, so the goal's second branch cannot be obtained from them.
• Order of limits. At the corner $(r_h,c_h)=(a,c_0)$ the two capacities coincide. Profit and customer cost are strictly better under flexible leasing there, but capacity is only weakly better. The capacity comparison holds only when $r_h$ approaches $a$ after $c_h$ is fixed.

Formalization scope

The model is the paper's base model of §3–§4: flexible leasing introduced into an existing BaaS program with independent regular and peak needs. The extensions of §5 (correlated needs, range choice, launching with flexible leasing) and the numerical calibration (§4.1, Figures 2–5) are out of scope.

Representation. All parameters are real numbers. Expectations over $D\sim\mathcal U[0,a]$ are interval integrals divided by $a$; volumes of customers are Lebesgue measures of subsets of $[0,1]$. Every volume, expected cost and equilibrium is defined from the model; the paper's closed forms are theorems, never definitions. Customers lease low when indifferent, upgrade on $\le$ and downgrade on $>$, following the proofs. The lease rate ranges over all of $\mathbb R$; the paper's remark "we require $p_h<\min(1,r_h)$" is not imposed, because the benchmark optimum can exceed 1. The peak rates range over the set $\bar p_h\le a$, $p_h-a\le\bar p_l\le p_h$ that the paper requires (p. 13). An equilibrium is optimal against every continuation at every lease rate.

Readings and added hypotheses.

• Proposition 6 is posed as "$c_h$ sufficiently close to $c_0$, then $r_h$ sufficiently large". A single neighbourhood of $(a,c_0)$ in both variables is false on both sides. On the $Q^f_h>0$ side, Proposition 5's threshold $T(r_h)$ equals $c_0$ at $r_h=a$ and is below it for $r_h<a$. The point $c_h=c_0$ is excluded.
• Each branch of the goal asserts existence of a benchmark optimum and a flexible equilibrium, so it is not vacuous. A goal of the form "every equilibrium is win-win-win" without existence would be trivially true where no equilibrium exists, and is ruled out.
• Lemma 2's interior cases hold with $r_h$ in place of $a$ (and $\bar p_h\ge0$). The statement also gives the missing outer cases for rates below zero or beyond $r_h$, covering every real rate.
• Lemma 3 is posed in the regime $\tau>c_h/(a(1-\rho))$, the only one in which its acquisition quantity is nonnegative. Its rates are assumed to lie below $r_h$.
• Lemmas 1, 4 and Propositions 1, 2, 5 carry the proofs' interior conditions as explicit parameter inequalities: the indifferent customer lies below $r_h$, and Proposition 1's range for $c_h$ holds.
• Proposition 5(i) is the $\le$ form, as in its proof. Proposition 4 is posed in its corner-neighbourhood clauses only.
• Proposition 2's second case, Proposition 3 and the remaining clauses of Propositions 4–5 are not posed: the second case of Proposition 2 is false on part of its range, and Proposition 3's threshold is garbled in the manuscript.

What a complete development needs. Lebesgue measure of intervals, interval integrals of piecewise-linear functions, and maximization of concave quadratics with a kink. It also needs the kink-regime equilibrium on the $Q^f_h=0$ side and continuity arguments at the corner. Lemmas 1–4 are reusable for any variant of the model, and proofs of the milestones in any order are welcome.

Selected references

• L. Shi and B. Hu, Battery as a Service: Flexible Electric Vehicle Battery Leasing, Manufacturing & Service Operations Management, Frontiers in Operations, 2024. Read as the authors' manuscript of 13 January 2024. https://doi.org/10.1287/msom.2022.0587

Why continuum Fisher markets matter

A Fisher market divides a supply of goods among buyers with fixed budgets. In a finite market, each good is a separate coordinate. Fair division can instead involve a continuum of items, such as locations along an interval or points in a region, where a buyer's valuation varies measurably from point to point. Finite dimensional existence and duality arguments do not automatically apply: the allocation is now a function, and the feasible set need not be compact in its natural function space. Gao and Kroer formulate a market and two Eisenberg–Gale programs for this setting, then prove that their optima exist and characterize equilibrium Gao and Kroer, §3.

The result also connects market equilibrium to fair division. A pure allocation assigns measurable regions of the item space to buyers, allowing overlap only on null sets. Existence of a pure optimizer means that a market outcome can be represented by such a division, rather than by fractional shares at each item. The same paper derives Pareto optimality, budget weighted envy freeness, and proportionality for equilibrium allocations Gao and Kroer, Theorems 1 and 3.

Market, allocations, and programs

The item space $\Theta$ is a compact subset of $\mathbb R^d$ with restricted Lebesgue measure $\mu$. There are $n$ buyers. Buyer $i$ has a budget $B_i>0$ and a nonnegative integrable valuation density $v_i$ with $\int_\Theta v_i\,d\mu>0$. The utility of a bounded nonnegative bundle $x_i$ is $\langle v_i,x_i\rangle=\int_\Theta v_i x_i\,d\mu$. An allocation $x=(x_i)$ is feasible when $\sum_i x_i\le1$ almost everywhere. It is pure when each $x_i$ equals the indicator of a measurable set $\Theta_i\subseteq\Theta$, up to almost everywhere equality, and these sets are pairwise disjoint up to null sets. Leftover items are allowed.

A nonnegative integrable price density $p$ defines a buyer's affordable bundles by $\langle p,x_i\rangle\le B_i$. A market equilibrium $(x,p)$ is a feasible allocation and price at which every buyer maximizes utility among affordable bundles and $\langle p,1-\sum_i x_i\rangle=0$. Thus unallocated supply may remain only where it has zero price. The paper's primal Eisenberg–Gale program, $\mathcal P_{EG}$, maximizes weighted log utility over feasible allocations. Its dual program, $\mathcal D_{EG}$, minimizes total price minus weighted log multipliers subject to $p\ge\beta_i v_i$ almost everywhere Gao and Kroer, pp. 6–8.

Formalization targets

The goal is the three part Theorem 1. In the notation above, it asserts attainment of the primal objective at a pure allocation, attainment of the dual objective with a unique multiplier vector $\beta^*$ and price $p^*=\max_i\beta_i^*v_i$ almost everywhere, and the equivalence

$$(x,p)\text{ is a market equilibrium} \quad\Longleftrightarrow\quad x\text{ optimizes }\mathcal P_{EG}\ \text{and}\ (p,\beta^*)\text{ optimizes }\mathcal D_{EG}.$$

The milestone list follows the results the paper uses to reach that goal. Lemma A.1 gives a convex, compact range for utility matrices and, under atomlessness, identifies mixed and partition based ranges. Lemma 1 specializes this to the market's feasible utility set $U$, proving that $U$ is compact and convex and equals the pure utility set $U'$. Lemma 2 establishes attainment and uniqueness in the finite dimensional reduction of the dual problem. Lemma 3 gives weak duality with the paper's constant $C=\sum_i B_i-\sum_i B_i\log B_i$ and its three optimality conditions. Theorem 2 expands the equivalence between optimality and equilibrium, including budget exhaustion and the utility formula $\langle v_i,x_i\rangle=B_i/\beta_i$. These are the paper's numbered results on pp. 8–10 and a1 Gao and Kroer, §3 and Appendix A.1.

The proposal also states Theorem 3, Lemma 4, and Corollaries 1–3 as companion results. They record the resulting fairness properties, normalized equilibrium bounds, winning sets, a construction of dual prices from a pure optimum, and a test for a pure equilibrium Gao and Kroer, pp. 10–11.

What the result provides

Theorem 1 shows that the two programs give actual allocations and prices in the continuum market, not merely limiting objective values. The pure optimizer provides measurable regions for buyers. The dual multipliers give a unique utility price for each buyer, while the price density is determined almost everywhere. Theorem 2 makes these program outputs economically interpretable: each buyer exhausts its budget at equilibrium. Theorem 3 then supplies efficiency and fairness guarantees for those allocations Gao and Kroer, Theorems 1–3.

These results are proved in the cited paper. This mission asks for machine checked Lean proofs of those mathematical statements. Its definitions of allocations, demand, equilibrium, the two programs, and feasible utilities could also support formalization of the paper's later geometric and quasilinear results. The draft declarations compile as open statements; compilation does not establish the theorems.

Why the proof is difficult

The feasible allocations are bounded in an infinite dimensional function space, but that does not make the set compact in the topology used for the optimization problem. The paper instead needs compactness of the finite dimensional set of achievable utility vectors. The range result in Lemma A.1 is therefore central, and its atomless conclusion must be strong enough to replace fractional allocations by measurable partitions Gao and Kroer, Lemma 1 and Appendix A.1.

Standard constraint qualification arguments also do not supply the required duality theorem here: the positive cone in $L^1(\Theta)$ has empty interior. The proposal consequently asks for the paper's specific weak duality inequality, attainment, and optimality characterization rather than assuming a general finite dimensional duality theorem applies Gao and Kroer, Remark 1.

Formalization scope

Lean uses real valued measurable functions on the ambient Euclidean space with measure $\mu=\mathrm{volume}|_\Theta$. It identifies prices and allocations up to $\mu$ almost everywhere equality, as the paper identifies $L^1$ and $L^\infty$ equivalence classes. Bundles must belong to $L^\infty(\mu)$ and prices and valuations must be integrable; these conditions prevent a nonintegrable product from receiving Lean's default integral value of zero. The number of buyers may be zero, consistent with the finite index formulation, while the standing positivity hypotheses apply to every buyer present.

The real logarithm in Lean returns zero at zero. The optimization predicates instead require positive utility or positive dual multipliers and compare only with other positive points, matching the paper's $\log 0=-\infty$ objective convention. The maximization over buyers is the finite supremum $\sup_i\beta_i v_i$. Price and allocation uniqueness is stated almost everywhere; multiplier uniqueness is exact. Lemma A.1 uses the paper's divisible measure condition for atomlessness and fixes its unnamed almost everywhere partition convention by requiring $\sum_jx_j=1$ everywhere. Corollary 3 explicitly requires each denominator $v_i(\Theta_i)$ to be positive. Lemma 4 alone assumes the normalizations $v_i(\Theta)=1$ and $\sum_iB_i=1$, which the paper recalls before its statement.

The goal remains the full three part theorem. It does not assume the range theorem, duality equality, or optimality conditions it is meant to establish. Contributions to the measure range theorem, utility set compactness, the dual reduction, and the equilibrium characterization are all within scope.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, Operations Research, 2023; formalization follows arXiv:2010.03025v5, 2021, §§2–3 and Appendix A.1.

Motivation

In reward based crowdfunding, customers must decide whether to back a product before its quality is known to them. The entrepreneur knows that quality and chooses a funding price. A high quality entrepreneur may therefore use price to convey information, but the same price is available to a low quality entrepreneur. The choice also changes the chance that the campaign meets its financing target. Bolandifar, Chen, Kouvelis, and Zhou study how these effects interact when the entrepreneur chooses a second, regular selling price after the campaign succeeds. The one price mechanism in this mission concerns the case in which only the funding price is posted in advance.

The question matters to the design and interpretation of crowdfunding campaigns. A lower funding price can be a credible quality signal even though it forgoes immediate revenue. Whether that signal is sustainable depends on the later selling opportunity, the financing target, and the different incentives of the two quality types. The paper gives a precise threshold for the financing target below which one separating outcome survives a refinement of the equilibrium concept.

Setting

The entrepreneur's product has privately known quality $q_i$, either low $q_L$ or high $q_H$, with $0<q_L<q_H$. The financing target is $T>0$. The entrepreneur posts a funding price $p_1\ge T$. Funding period customers all share a taste $\theta_c$ uniformly distributed on $[0,1]$ and evaluate the product using believed quality $q_j$. They back it when $\theta_cq_j\ge p_1$. The funding market has size one, so a successful campaign raises at least $T$ and occurs with probability $1-p_1/q_j$ for $T\le p_1\le q_j$. The formal definition extends this probability by zero for larger prices.

After success, true quality is revealed and the entrepreneur sets a regular selling price $p_2\in(0,q_i]$. A fraction $\alpha\in(0,1)$ of regular period customers have the same taste as the funding customers. Their taste distribution is therefore updated after success. The other regular customers have a fresh, independent uniform taste. The regular market also has size one. Production cost, salvage value, and discounting contribute no additional terms. Conditional regular period profit is $\pi^{ij}_2(p_2\mid p_1)$, the two branch function in equation (2) of the manuscript. Its optimal value $\pi^{ij*}_2(p_1)$ is the supremum over feasible $p_2$. The total expected profit $\pi^{ij}(p_1)$ is the success probability times $p_1+\pi^{ij*}_2(p_1)$.

A separating equilibrium assigns different feasible funding prices $p_H$ and $p_L$ to the two entrepreneur types. Customers believe quality is high at $p_H$ and low at every other price, including off path prices. Under those beliefs, neither type benefits from a feasible deviation. The intuitive criterion removes an equilibrium if an off path price would strictly improve the high type's profit while strictly reducing the low type's profit, were customers to interpret that deviation as a high quality signal. This is the paper's stated test, with the strict low type comparison used in its appendix.

Formalization targets

The separating equilibrium

Define the price threshold

$$\bar p_1=\frac{4q_H-(1-\alpha)q_L-\sqrt{(q_H-q_L)\bigl(16q_H-(1-\alpha)^2q_L\bigr)}}{8}.$$

The goal is Proposition 1 of the manuscript. If $T\le\bar p_1$, there is a separating equilibrium surviving the intuitive criterion, and every surviving separating equilibrium has exactly the prices

$$p_H=\bar p_1,\qquad p_L=\frac{3+\alpha}{8}q_L.$$

The formal goal also says that no separating equilibrium exists when $\bar p_1<T<q_L$. Its scope on this side of the threshold follows the manuscript's proof and the nondegenerate funding market; the printed “otherwise” sentence does not hold literally when $T\ge q_L$.

Supporting targets

Lemma 1 identifies the optimal regular price and its attained profit in each of three funding price ranges, split at $q_j/2$ and $\min\{q_j/[2(1-\alpha)],q_j\}$. Lemma 2 identifies the funding profit's single peak and the maximizing price $\max\{[4q_j-(1-\alpha)q_i]/8,T\}$. The three parts of Lemma 3 characterize the low type's mimicking indifference prices, the high type's upper indifference price, and the ordering of these thresholds. These are the milestones leading to Proposition 1.

Significance

The proposition gives both types' prices and shows why the high type's credible signal is a lower funding price than the low type's. It also identifies a financing target above which this separation disappears within the paper's nondegenerate range. The result relates a platform design parameter, the target, to equilibrium information revealed by price.

The result is proved in the cited manuscript, with proofs in Appendix A. The remaining work in this mission is a machine checked proof of the model's price optimization and equilibrium claims. The definition of the two period payoff, the treatment of the later optimal price, and the explicit deviation predicates may be reusable for other crowdfunding signaling mechanisms. The draft statements are open proof targets; the present mission does not claim those proofs are already formalized.

Difficulty

The later optimal price changes form as the funding price crosses two thresholds. That makes total expected profit a piecewise function, even before the two types' incentives are compared. Maximizing either type's full information payoff alone does not determine a separating equilibrium: the low type might imitate the high type, while the high type might deviate to a price customers would interpret as low quality. The intuitive criterion imposes a further comparison at prices outside the equilibrium path. The claim requires all of these comparisons with the same underlying payoff definition.

Formalization scope

Lean uses one tuple of real parameters $q_L,q_H,\alpha,T$ and the standing restrictions $0<q_L<q_H$, $0<\alpha<1$, and $T>0$. The prior probability of high quality does not occur in the separating price statements. The regular profit is the printed equation (2), with a positive regular price at most true quality. Campaign success probability is clipped at zero for funding prices above believed quality. Funding prices range over all reals at least $T$; the maximum profits are defined as suprema over those feasible prices. Milestones assert attainment, so those suprema cannot be replaced by convenient formula values.

The model uses the paper's market size, cost, salvage, and discount normalizations. Lemma 1 excludes $p_1=q_j$: at that endpoint the printed third case can specify an infeasible regular price. Lemma 2 assumes $T<q_j$ and quantifies only over the four true and believed quality combinations. Lemma 3 is stated for $T\le\bar p_1$ to avoid its circular printed preamble, and one threshold comparison is expressed as a strict profit inequality because the lower crossing can lie below $T$. Proposition 1 does not assert pooling existence, which would require the omitted prior; its no separation clause is restricted to $T<q_L$.

Contributions toward the piecewise optimization lemmas, the threshold characterization, and the equilibrium theorem are welcome. The separating equilibrium is defined by incentive comparisons over all feasible deviations, and its refinement is defined by the off path deviation test. The optimal profits are supremum values of the model payoffs. These choices keep the goal from collapsing into a restatement of a closed form or of the paper's derived necessary and sufficient conditions.

Selected references

• E. Bolandifar, Z. Chen, P. Kouvelis, and W. Zhou, Quality Signaling through Crowdfunding Pricing, SSRN manuscript 3689946, revision of 2022-05-30, §§3–4 and Appendix A. SSRN. Published as Manufacturing & Service Operations Management, DOI 10.1287/msom.2022.1177; the cited artifact here is the SSRN manuscript.

Why distribution and pricing interact

A manufacturer that already sells directly to consumers may also supply an independent retailer. Adding the retailer can reach consumers who prefer its service, but the two channels then compete for some of the same buyers. A wholesale price affects both the retailer's ability to serve consumers and its retail pricing. The manufacturer's choice of distribution channel therefore depends on the pricing tools available to each firm. Jullien, Reisinger, and Rey study this choice when either or both firms can charge prices tailored to individual consumers in Personalized Pricing and Distribution Strategies. The source used here is their authors' manuscript of March 2022, whose proof of Proposition 3 appears in Online Appendix A.

This mission addresses a particular case of that analysis: the manufacturer charges a single retail price, while the retailer may charge either a single price or a price tailored to each buyer. The consumers' valuations for both channels move in the same direction with their type. Under those conditions, the paper claims that opening the retailer channel raises total industry profit under either retailer pricing policy. This is a question about the distribution decision, with the downstream retail game determining the profit achieved by each decision.

The market and its two retail games

A consumer type is a real number $x$ in $[0,X]$, with unit density. Firm A is the manufacturer and direct seller; firm B is an independent retailer that obtains each unit from A. Their values to a consumer are

$$u_A(x)=\max\{1-x,0\},\qquad u_B(x)=\max\{v-sx,0\}.$$

There are no fixed costs of opening a channel and no variable production or distribution costs. The market parameters satisfy $0<s<v<1$ and $X\ge v/s$. These conditions express the positively correlated case in §5 and keep the market large enough that its upper boundary does not limit B's demand. The two values cross at $\hat x=(1-v)/(1-s)$, with common value $\hat u=(v-s)/(1-s)>0$. Types below $\hat x$ value A's offer more; types above it value B's offer more, until valuations fall to zero.

A two-part tariff has a fixed fee $F$ and a wholesale price $w$ per unit B buys from A. The fee divides profit between the firms. Total industry profit is what consumers pay, so $F$ cancels from that total. The wholesale price is nonnegative. At the wholesale stage, the firms compare the total industry profit attainable with both channels against the profit from A selling alone. As on p. 9 of the manuscript, a tie is resolved in favor of mono distribution; a strictly greater profit is required for dual distribution.

When A sells alone and charges a uniform price $p$, its profit is $p$ times the measure of types for whom $u_A(x)\ge p$. If both firms charge uniform prices, denoted UU, they set $p_A$ and $p_B$ simultaneously. A consumer buys the product with highest nonnegative net utility. A earns $p_A$ on each of its retail sales and $w$ on each B sale. B earns $p_B-w$ on each of its sales. A downstream Nash equilibrium requires each price to maximize its firm's variable profit against the other price, including deviations into market regions where demand is zero or the identity of the preferred firm changes.

If A charges a uniform price and B tailors its price, denoted UP, A announces $p_A$ first. B then responds separately to each consumer. Under the continuation selected in the manuscript, B serves a type $x$ when $u_B(x)-w$ exceeds both zero and A's nonnegative consumer surplus. Its price is $u_B(x)-\max\{u_A(x)-p_A,0\}$. Otherwise, A sells if its price does not exceed the consumer's value. A chooses its uniform price to maximize its retail receipts plus wholesale receipts. Industry profit is the integral over $[0,X]$ of the price actually paid by each consumer.

Formalization targets

The mono-distribution benchmark is

$$\Pi_U^m=\max_p\Pi_U^m(p)=\Pi_U^m(1/2)=\frac14.$$

The paper derives a wholesale price $w^*_{UU}$ and retail prices $p_A(w^*_{UU}),p_B(w^*_{UU})$ for the UU game, together with a profit $\Pi^*_{UU}$ satisfying

$$\Pi^*_{UU}-\Pi_U^m=\frac{(1+s)(v-s)^2}{s(4+5s)(1-s)}>0.$$

For UP it derives $w^*_{UP}$, A's leader price $p_A(w^*_{UP})$, and a profit $\Pi^*_{UP}$. Equation (15) gives $\Pi^*_{UP}>\Pi^*_{UU}$. The milestone list follows these source results, including the consumer demands and the two profit identities. Its last comparison completes the UP side after the UU gain is established.

The goal is Proposition 3: for each of UU and UP, some nonnegative wholesale price admits a downstream equilibrium and every equilibrium at that price yields industry profit strictly greater than A could earn with any uniform price in mono distribution. The goal leaves the wholesale price existential, as the proposition does. It does not assume the paper's calculated candidates are the only possible wholesale prices that work.

What the result establishes

Proposition 3 identifies a robust distribution choice within the positively correlated case: while A uses uniform pricing, permitting the retailer channel raises joint profit whether B uses uniform or personalized retail prices. The conclusion separates the effect of B's pricing technology from the effect of A's own pricing technology; the latter changes the distribution comparison in Proposition 4 of the same manuscript. The result also supplies a precise instance in which additional downstream competition and additional market coverage must be assessed together.

The paper proves Proposition 3 in its Online Appendix A. The remaining work for this mission is a machine-checked derivation of the downstream equilibrium conditions, the demand and payment integrals, and the strict profit comparisons. The Lean statements here are open proof obligations. A complete development would make the consumer-choice and profit model reusable for related distribution games, while the rational formulas and equilibrium calculations are specific to this paper's linear valuations.

Where the formalization is difficult

The paper writes simple linear demand expressions in the region where both firms have positive sales. Actual demands are measures of consumer choice sets and change formula at market boundaries, when a price excludes a product, or when all consumers refuse to buy. A first-order condition within one region does not by itself establish a global best response in the full retail game. The UU equilibrium milestone consequently states global Nash optimality and uniqueness at the selected wholesale price. In UP, A's leader price must likewise maximize its variable profit over every real uniform price after B's per-consumer response. The integral of actual payments must then be shown to equal the paper's closed form.

Formalization scope

Lean represents consumer types by real numbers in $[0,X]$ and their mass by Lebesgue volume. The Model fields are $v,s,X$; Model.Standing records exactly $0<s<v<1$ and $X\ge v/s$. The valuations and crossing point are defined from these fields. Retail demand is clipped to the consumer interval, and profit is calculated from demand or actual payments. The expressions printed as (12) and (14) are theorem conclusions, not definitions of industry profit. A real supremum is unnecessary for mono distribution: the theorem bounds profit at every price and proves attainment at $1/2$.

The UP response uses the manuscript's selected personalized-pricing continuation. At indifference, the choice rules assign UU ties between the firms to A and give B a sale in UP only with a strict margin. Ties occur only at isolated types at the candidate equilibrium prices; zero-price deviations can create ties across the flat zero-valuation tail, and the rules specify their outcome. Global best responses quantify over all real retail prices, including zero and negative deviations. The goal restricts wholesale prices to $w\ge0$, the range used in the manuscript's analysis. The fixed fee is omitted from the model because it transfers profit between firms without changing industry profit. The goal includes existence of a continuation equilibrium, so a vacuous universal statement over an empty equilibrium set cannot establish dual distribution.

The development needs elementary properties of Lebesgue measure on real intervals, measurable piecewise choice sets, interval integration, and algebraic inequalities for the rational candidate prices. Proofs of the equilibrium and integral milestones, or reusable lemmas about volumes of intervals cut by affine utility comparisons, are welcome contributions. The shared primitives are duplicated in the companion mission on personalized pricing by A because unpublished draft definitions cannot be imported across proposals.

Selected references

• B. Jullien, M. Reisinger, and P. Rey, Personalized Pricing and Distribution Strategies, authors' manuscript of March 2022; published in Management Science (2023). DOI: 10.1287/mnsc.2022.4437. Source artifact in this repository: source.pdf, SHA-256 25a6c84ac0c48c6720f6a9e1f9b1f1ec516412c31dac044ac84c1d4c72dfc253, printed pp. 5–14 and Online Appendix A, pp. 1–4.

Motivation

A firm can learn a customer's preference before choosing a customized product, or it can let the customer choose a requested design. The two approaches assign the design decision to different parties. That matters when design changes both the value of a sale and a cost the seller must incur before the price is negotiated. Guo's study of customer voice in customization compares these approaches in a model where a buyer has private information about how much it values quality. The payoff comparison asks who gains from holding the design right and whether the answer survives a modest fixed cost of using that approach.

This mission concerns Proposition 8 of the SSRN author copy, printed page 23. The result is a comparative statement about two already specified separating equilibrium outcomes. Earlier results in the same paper characterize when the outcomes arise: Proposition 1 treats communication before seller design, and Proposition 3 treats a buyer's design request. Proposition 8 compares the parties' payoffs at the qualities associated with those outcomes. Its four clauses distinguish gross payoff rankings from net rankings after an incremental fixed cost. The paper states Proposition 8 without a separate proof; its surrounding discussion explains its interpretation. All page and result numbers here follow the SSRN version of 2023-11-29.

Setting

There is one seller and a unit mass of buyers. Each buyer has one-unit demand and a privately known quality preference $\theta_i$, with type $i\in\{H,L\}$ and $\theta_H>\theta_L>0$. The high type has population share $\alpha\in(0,1)$, while the low type has share $1-\alpha$. A product's quality is a nonnegative real number $q$. Producing a unit of quality $q$ costs $kq^2$, and offering that product incurs a selling cost $sq^2$, where $k,s>0$. The selling cost is incurred before the price is settled. The seller makes a take-it-or-leave-it offer with probability $\gamma\in(0,1)$; the buyer does so with probability $1-\gamma$. These primitives and the timing are specified in Section 2.

In A-Learning, the buyer sends a costless message about its preference and the seller chooses the design. In O-Learning, the buyer requests a quality and the seller decides whether to accept it. The paper compares separating outcomes, so each type is associated with its true preference when the equilibrium payoff is evaluated. The pricing stage is represented by the paper's payoff formulas. If the seller regards a buyer's preference as $\hat\theta$, its payoff from quality $q$ is

$$v(q,\hat\theta)=\gamma(\hat\theta q-kq^2)-sq^2.$$

The buyer's payoffs $u^A(\theta,\hat\theta,q)$ and $\mu(q,\theta,\hat\theta)$ retain the nonnegative parts in equations (5) and (9): each is $\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}$, with its arguments ordered as in the relevant equation. For type $i$, the paper's A-Learning and O-Learning equilibrium qualities are

$$q^A_i=\frac{\gamma\theta_i}{2s+2\gamma k},\qquad q^O_i=\min\left\{\frac{\gamma\theta_i}{s+\gamma k},\frac{\theta_i}{2k}\right\}.$$

Write $\alpha_H=\alpha$ and $\alpha_L=1-\alpha$. The seller's expected gross payoffs are $V^A=\sum_i\alpha_i v(q^A_i,\theta_i)$ and $V^O=\sum_i\alpha_i v(q^O_i,\theta_i)$. The buyer payoffs $U^A_i$ and $U^O_i$ evaluate $u^A$ and $\mu$ at type $i$'s quality and truthful preference. These are the payoffs defined around equations (8) and (13) of the paper.

Formalization targets

The first comparison says that the seller earns more from its own design, while each buyer type earns more from its requested design:

$$V^A>V^O,\qquad U^A_i<U^O_i\quad(i\in\{H,L\}).$$

The two fixed-cost clauses hold the preference levels, population share, bargaining weight, and production-cost coefficient fixed while the positive selling-cost coefficient $s$ varies. For every seller-side incremental fixed cost $F>0$, there is a positive threshold $\tilde s_F$ such that

$$0<s<\tilde s_F\quad\Longrightarrow\quad V^A(s)-F<V^O(s).$$

For every buyer-side incremental fixed cost $G>0$ and each type $i$, there is a positive threshold $\tilde s_{iG}$ such that

$$0<s<\tilde s_{iG}\quad\Longrightarrow\quad U^A_i(s)>U^O_i(s)-G.$$

The goal is the conjunction of these four clauses, exactly the payoff content of Proposition 8. The milestone list also includes the paper's strict quality comparison $q^A_i<q^O_i$ and its observation that the quality difference tends to zero as $s$ tends to zero. The printed statement and discussion are on pages 22–23.

Significance

The gross comparisons separate the seller's and buyers' preferences over who chooses quality. The fixed-cost clauses show why the party favored by the gross comparison need not favor that approach once its own extra effort or implementation expense is counted. The thresholds make this claim uniform over all sufficiently small positive selling costs, rather than treating the single case $s=0$. This distinction is relevant when comparing preference solicitation, which requires seller effort, with buyer-led design, which requires customer effort.

Formalizing the result gives a reusable two-type model of quadratic production and selling costs, the two reduced-form buyer payoffs, and a finite-population expected-payoff calculation. It also creates separate targets for each clause, so the gross-payoff and small-cost claims can be checked independently. The result is proved in the mathematical paper only to the extent of its stated Proposition 8 and accompanying discussion; the local Lean statements in this proposal compile with proof placeholders and do not yet constitute machine-checked proofs.

Difficulty

The two approaches select different quality formulas, and O-Learning uses a minimum of two expressions. As $s$ changes, that minimum can switch branches. The buyer payoff formulas also contain maxima with zero, so replacing them unconditionally with simplified quadratic expressions would change the model. A valid payoff comparison must account for the relevant branch and preserve the strict inequalities for both buyer types. For the fixed-cost clauses, pointwise closeness at $s=0$ does not itself state a uniform claim for every sufficiently small positive $s$; the threshold must be positive and chosen before $s$.

Formalization scope

The Lean model uses a two-constructor buyer type, real parameters $\theta_H,\theta_L,\alpha,\gamma,k,s$, and a Standing predicate carrying every displayed positivity and interval assumption. Qualities are real-valued, with the paper's intended domain $q\geq0$; the closed-form equilibrium qualities in this mission are nonnegative under those assumptions. Expected seller payoffs use a finite sum over exactly the high and low types, weighted by $\alpha$ and $1-\alpha$. Buyer payoffs use the original maxima with zero. The pricing stage is in reduced form through equations (4), (5), and (9). The model and payoff notation are local to CustomerVoice.Payoffs, because the other missions' definitions are unpublished drafts.

The statements compare the printed closed-form qualities without adding the separate inequalities that guarantee both separating equilibria exist. Thus their domain is all parameter choices satisfying Section 2's standing assumptions; this is the stronger reading identified in the paper's planning notes for Proposition 8. In the small-$s$ statements, withS changes only the selling-cost coefficient, and the quantified values of $s$ satisfy $0<s<\tilde s$. The proof targets cannot be reduced by deleting the nonnegative parts of the buyer payoffs, allowing a zero threshold, or checking only the limit at $s=0$. Contributions to the elementary quality comparisons, branch-sensitive payoff inequalities, and positive-side limits all support the goal. The finite weighted-payoff and limit infrastructure can be reused in other small-cost comparisons.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, version of 2023-11-29, §§2–3.4 and Proposition 8. SSRN record.
• Liang Guo, The Voice of Customers in Customization, Management Science, 2021. DOI:10.1287/mnsc.2021.04025. The mission's statement indices follow the SSRN copy above.