All missions

Motivation

A firm that needs outside money to start a project knows more about the project than its investors do, and it can usually choose how much of that knowledge to reveal before raising funds: which audits to commission, which metrics to report, how informative an analyst's report will be. The security-design literature studies the security side of this problem, meaning what claim to sell given the information the investors have (Innes, 1990; Nachman and Noe, RFS 1994). The Bayesian persuasion literature (Kamenica and Gentzkow, Bayesian Persuasion, AER 2011) studies the information side, meaning what to reveal when a sender can commit to a signal in advance.

M. Szydlowski, Optimal Financing and Disclosure (Management Science 2021; working paper of March 2017), puts the two together. An entrepreneur who cannot finance a project on the prior alone commits to a disclosure policy so as to maximize her expected payoff, subject to the investors' competitive pricing. The main answer is simple and testable: the optimal policy is a pass/fail test, and the passing standard is set exactly where investors break even. This mission formalizes that answer and the chain of lemmas the paper's appendix uses to reach it.

Setting

The project pays $s \in [0,1]$. The investment cost is $I \in (0,1)$. The entrepreneur sells a security with payoff $c(s)$ to competitive investors. $c$ is continuous, $0 \le c(s) \le s$, and both $c(s)$ and the residual $s - c(s)$ are weakly increasing (equity, debt $\min(s,R)$ and options all qualify). The common prior over $s$ has a continuous density $\mu_0$ with support $[0,1]$.

A posterior is a probability measure $\mu$ on $[0,1]$. At posterior $\mu$ the security sells for $p(\mu) = \mathbb E_\mu c(s)$ (1), and the project is financed iff $p(\mu) \ge I$ (2). If it is financed, the entrepreneur receives the residual, a private benefit $B > 0$, and a share $\lambda \in [0,1]$ of the excess cash, so her payoff (3) is

$$V(\mu) = \mathbb E_\mu[s - c(s) + B] + \lambda\big(\mathbb E_\mu c(s) - I\big) \ \text{ if } \mathbb E_\mu c(s) \ge I, \qquad V(\mu) = 0 \text{ otherwise}.$$

A disclosure policy induces a distribution $\tau$ over posteriors. By Kamenica and Gentzkow's equivalence, the feasible $\tau$ are exactly the Bayes-plausible ones, those whose mean posterior is the prior, $\mathbb E_\tau \mu = \mu_0$ (5). The entrepreneur's problem (6) is to maximize $\mathbb E_\tau V(\mu)$ over Bayes-plausible $\tau$. The threshold policy with cutoff $t$ reveals only whether $s \ge t$. With probability $q = \int_t^1 \mu_0$ it produces the posterior $\mu_h = \mu_0 / q$ on $[t,1]$, and otherwise the posterior $\mu_l = \mu_0/(1-q)$ on $[0,t)$; this is (17).

Throughout, the project cannot be financed without disclosure: $\mathbb E_{\mu_0} c(s) < I$ (§4).

Formalization targets

Goal: Proposition 1 (p. 18)

There is a threshold $\hat s \in (0,1]$ at which the financing constraint (20) binds,

$$\int_{\hat s}^1 \big(c(s) - I\big)\,\mu_0(s)\,ds = 0,$$

such that the threshold policy with cutoff $\hat s$ is Bayes plausible and attains the maximum of $\mathbb E_\tau V(\mu)$ over every Bayes-plausible $\tau$. The hypothesis $\lambda I \le B$ is added, as explained under Formalization scope.

Milestones (proof of Proposition 1, Appendix A)

1. Lemma 1 (p. 15): every Bayes-plausible $\tau$ can be replaced, at the same value, by one with two posteriors $\mu_h, \mu_l$ with densities and $\mathbb E_{\mu_l} c < \mathbb E_{\mu_0} c < I \le \mathbb E_{\mu_h} c$.
2. Lemma 3 (p. 35): at an optimum of the relaxed fixed-$q$ problem (31), the mass constraint and the financing constraint cannot both be slack.
3. Lemma 4 (p. 36): the states with nonnegative marginal contribution form an interval $\hat S = [\hat s, 1]$.
4. Proposition 7 (p. 33): for fixed $q \in (0,1)$, the threshold density (17) solves problem (30).
5. Lemma 5 (p. 38, monotonicity part): the fixed-$q$ value $V(q)$ is strictly increasing in $q$.
6. Lemma 6 (p. 38): there is a maximal feasible $\bar q \in (0,1)$, and $\hat s(\bar q)$ makes (20) bind.
7. Proposition 8 (p. 37, first case): the optimal two-posterior value is $V^* = \int_{\hat s}^1 (s - c(s) + B)\,\mu_0(s)\,ds$ (37), attained by (17) with the binding $\hat s$.

Significance

Proposition 1 gives disclosure a concrete shape: certify whether cash flows clear a bar, and say nothing more. The bar is the lowest one at which investors still break even, so the entrepreneur maximizes the probability of financing. The paper's later results build on it: the choice of the optimal security (Proposition 4), extensions to general utility (Proposition 5), and comparative statics of the threshold in the security's information sensitivity (Propositions 2–3).

The result is proved on paper but has not been machine-checked. A formalization adds three things. It checks a proof whose central step goes through an infinite-dimensional linear-programming duality (Levinson, 1966). It pins down hypotheses the printed statement omits, notably $\lambda I \le B$. And it provides a reusable Lean account of Bayesian persuasion over a continuum of states, with distributions over posteriors as measures on the space of measures.

Difficulty

The obvious argument is a bang-bang argument. Fix the probability $q$ of financing, put as much high-posterior mass as possible on the best states, then optimize over $q$. Each step hides a gap. The reduction to two posteriors (Lemma 1) needs barycentres of a measure on the space of measures. The fixed-$q$ problem is a linear program over densities with a pointwise cap $\mu_h \le \mu_0/q$, so finite-dimensional LP duality does not apply. The paper uses an infinite-dimensional duality theorem plus a compactness lemma under an extra equicontinuity restriction (32).

Monotonicity of the value in $q$ is where the printed argument fails in general. The marginal contribution $s - c(s) + B + \lambda(c(s) - I)$ can be negative near the cutoff when $\lambda I > B$. In that case a slack threshold beats the binding one, and the binding threshold is not optimal. A second trap is that the binding root of (20) need not be unique: for debt, every cutoff above the face value can solve (20) with equality. "$\hat s$ solves (20)" therefore cannot by itself be the content of the theorem.

Formalization scope

The state space is $\mathbb R$, and $c$ and $\mu_0$ are read only on $[0,1]$. The prior is Lebesgue measure on $[0,1]$ with density $\mu_0$. Support $[0,1]$ is encoded as positive prior mass on every nondegenerate subinterval. Posteriors are arbitrary measures on $\mathbb R$, and a distribution over posteriors is a measure on the space of measures with Mathlib's Giry σ-algebra. Bayes plausibility is: $\tau$ is a probability measure, almost every posterior is a probability measure, and $\tau$'s monadic join is the prior. Posterior expectations are integrals over $[0,1]$, written through positive and negative parts so that they are measurable in the posterior. As a result $\mathbb E_\tau V(\mu)$ is never a junk value. Ties in the financing rule go to financing ($\ge$). "Increasing" means weakly increasing. The fixed-$q$ problems range over integrable densities with $0 \le \mu_h \le \mu_0/q$ pointwise, which encodes $\mu_l \ge 0$. The equicontinuity restriction (32) is dropped; it serves only the compactness Lemma 2, which is not formalized.

Two hypotheses are added, each disclosed in the items that carry it:

• $\lambda I \le B$, on the goal and on Lemma 3, Lemma 5 and Proposition 8. Without it the printed results are false. For $\mu_0 = 1$, $c(s) = s$, $I = 0.6$, $B = 0.1$ and $\lambda = 1$, the binding threshold $\hat s = 0.2$ earns $0.08$, while revealing whether $s \ge 0.5$ earns $0.125$. The hypothesis covers $\lambda = 0$, the case §5 uses.
• $I < c(1)$, on Lemma 6 and Proposition 8, where $\bar q \in (0,1)$ requires that something can be financed.

The goal quantifies over all Bayes-plausible distributions over posteriors, and its threshold is pinned by optimality, not only by solving (20). A version restricted to threshold or two-point policies, or one whose $\hat s$ is any root of (20), would be a different and weaker theorem. Optimality is stated as "an optimal policy", since the optimum is not unique.

Not formalized: Lemma 2 (compactness); the continuity and differentiability parts of Lemma 5; the second case of Proposition 8 ($\mathbb E_{\mu_0} c \ge I$); and the paper's later Propositions 2–6, 9 and 10. The general definitions of Bayes plausibility and of the reveal-a-cell policy are stated for an arbitrary measurable state space and are reusable for other persuasion missions. Contributions are welcome on any milestone. A barycentre construction for measures on the space of measures (Lemma 1) and a bathtub principle for densities under a pointwise cap (Proposition 7) are of independent use.

Selected references

• M. Szydlowski, Optimal Financing and Disclosure, working paper, version of March 2017; published in Management Science 67(1), 2021. https://doi.org/10.1287/mnsc.2019.3462
• E. Kamenica and M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• N. Levinson, A class of continuous linear programming problems, Journal of Mathematical Analysis and Applications 16(1), 73–83, 1966.
• R. D. Innes, Limited liability and incentive contracting with ex-ante action choices, Journal of Economic Theory 52(1), 45–67, 1990.
• D. C. Nachman and T. H. Noe, Optimal design of securities under asymmetric information, Review of Financial Studies 7(1), 1–44, 1994. https://doi.org/10.1093/rfs/7.1.1

Motivation

Wind and solar generation have near-zero marginal cost. In a wholesale electricity market where prices are set by the marginal producer, adding such capacity displaces expensive conventional generation and lowers the spot price: the merit-order effect. Regulators and system planners rely on this effect when projecting the price impact of renewable expansion, and empirical studies of European markets report it.

Most electricity, however, is not traded only in the spot market. Producers and retailers hedge in forward markets before demand and wind output are known, and forward trading changes how producers with market power behave in the spot market (Allaz and Vila, 1993). Peura and Bunn (Management Science, 2021) ask what happens to the merit-order effect once this channel is included. Their answer is that, when wind output is variable and positively skewed, additional wind capacity eventually raises the expected spot price and the forward price. This mission formalizes that statement, Proposition 2 of the paper, together with the equilibrium characterization it rests on.

Setting

There are two conventional producers with constant marginal cost $c$, a set of price-taking wind producers with total capacity $k_W \ge 0$ and zero cost, $N_R \ge 1$ price-taking retailers who resell at a fixed retail price $p_R$, and an elastic industrial demand $D_I = a - p_s$, where $p_s$ is the spot price.

Two random quantities are drawn on a probability space: the total retail demand $\theta$, bounded, and the wind yield $\xi \in [0, 1]$, so that available wind output is $\xi k_W$. They are independent and both have positive variance. Write $\mu_\theta, \sigma_\theta^2, \tau_\theta$ for the mean, variance and third central moment of $\theta$, and $\mu_\xi, \sigma_\xi^2, \tau_\xi$ for those of $\xi$. The coefficient of variation of the yield is $CV_\xi = \sigma_\xi/\mu_\xi$ and its normalized skewness is $\tau^N_\xi = \tau_\xi/\sigma_\xi^3$.

Trading has two stages.

1. Forward stage. Before $(\theta, \xi)$ is known, each producer sells a forward quantity $f_{Pi}$ and each retailer buys $f_{Ri}$ at a common forward price $p_f$. The market clears at zero net supply, $f_P = f_R$. Every participant maximizes the mean-variance utility $U(\pi) = E[\pi] - \frac{\lambda}{2}V(\pi)$ of its profit, with risk aversion $\lambda > 0$. Retailers take $p_f$ and the spot-price distribution as given. Producers have market power in the forward market: a producer evaluates each alternative forward position at the forward price that would clear the market.
2. Spot stage. After $(\theta, \xi)$ is revealed, the producers compete à la Cournot on the inverse residual demand $p_s = a + \theta - \xi k_W - q_P$, each maximizing $p_s(q_{Pi} - f_{Pi}) - c\,q_{Pi}$.

With $q_0 = a - c + \theta - \xi k_W$ and $p_0 = a + 2c + \theta - \xi k_W$, the spot equilibrium is $q^*_{Pi} = (q_0 + 2f_{Pi} - f_{Pj})/3$ and $p_s = (p_0 - f_P)/3$ (Lemma 1). The forward-spot equilibrium is $f^*_{Pi} = \omega/\nu$ and $p_f = a_f - 2b_f\omega/\nu$ for explicit expressions $\omega, \nu, a_f, b_f$ in the parameters, the moments, and $k_W$ (Theorem 1).

Formalization targets

Goal: Proposition 2

If

$$CV_\xi\,\tau^N_\xi \ge \zeta := \frac{27}{4N_R},$$

then an equilibrium exists at every capacity $k_W \ge 0$, and there are thresholds $\bar k^s_W > 0$ and $\bar k^f_W \ge 0$ such that along every equilibrium selection

$$k_W \mapsto E[p_s] \text{ is strictly decreasing on } [0, \bar k^s_W] \text{ and strictly increasing on } [\bar k^s_W, \infty),$$ $$k_W \mapsto p_f \text{ is strictly increasing on } [\bar k^f_W, \infty).$$

The value of $\zeta$ comes from the paper's proof; the proposition itself only asserts that some $\zeta > 0$ works.

Milestones

1. Lemma 1 (p. 12): the spot Cournot equilibrium given forward positions.
2. Lemma 2 (p. 13): the retailers' optimal forward positions, a basis term plus a hedging term, and the resulting clearing condition.
3. Theorem 1 (p. 14): existence, uniqueness and closed form of the forward-spot equilibrium.
4. Derivative of $E[p_s]$ (proof of Proposition 2, p. 37): $\partial E[p_s]/\partial k_W = s_{p_s}(k_W)/(9N_R^2\nu^2)$, where $s_{p_s}(k_W) = \alpha_0 + \alpha_1 k_W + \alpha_2 k_W^2 + \alpha_4 k_W^4$ is a quartic with no cubic term and explicit coefficients.
5. Sign of the quartic (p. 37): under the $\zeta$ condition, $\alpha_4 \ge 0$, $\alpha_2 > 0$ and $\alpha_0 < 0$, and $s_{p_s}$ changes sign exactly once on $[0, \infty)$, from negative to positive.
6. Forward price (p. 37): the derivative of the closed-form forward price is eventually positive.

Significance

The result. Proposition 2 isolates a mechanism by which two pro-competitive forces, low-cost capacity and forward trading, can combine to raise prices. Variable and skewed wind output increases the risk that a producer is caught with a large forward position when wind is high and the spot price is low. Producers therefore sell less forward, which by Lemma 1 lowers their spot output and raises the spot price. For large enough capacity this forward effect outweighs the merit-order effect. The condition for the reversal involves only $CV_\xi$ and $\tau^N_\xi$.

Formalizing it. The result is proved in the paper but has no machine-checked proof. In a formal development the equilibrium has to be defined through the participants' optimization problems, not through the closed forms. Theorem 1 then has to show that this optimization-defined equilibrium exists, is unique, and equals the closed form. The polynomial coefficients have to be checked: the printed $\alpha_1$ has a misplaced parenthesis, and the printed $s_{p_s}$ is off by a factor of $3N_R^2$. Both are corrected and disclosed in the milestone statements. Neither affects the conclusion.

Difficulty

The goal combines three layers. The probabilistic layer computes means, variances and covariances of products of independent bounded random variables. These computations produce the third central moments $\tau_\theta, \tau_\xi$ and justify replacing the utility of each participant by an explicit quadratic in its own position. The game-theoretic layer has to show that each first-order condition gives a global optimum, which needs strict concavity, and that the producers' best responses, each computed against a clearing price that itself depends on the deviation, meet at a unique point. The analytic layer studies the rational function $E[p_0]/3 - 2\omega/(3\nu)$ of $k_W$, whose derivative's numerator is a quartic with coefficients that are themselves polynomials in eleven quantities.

A tempting shortcut is to define the equilibrium by its closed form, which reduces the goal to a sign argument on a polynomial. That shortcut removes Theorem 1 entirely and is excluded here. A second tempting reading treats the forward price as fixed when a producer deviates. That makes producers price takers in the forward market, which is a different game whose equilibrium is not $\omega/\nu$.

Formalization scope

The market parameters are a structure with fields a, c, pR, lam ($\lambda$, a Lean keyword) and NR : ℕ; the retailers are indexed by Fin NR. The demand $\theta$ and the yield $\xi$ are real functions on a probability space $(\Omega, P)$, and the capacity $k_W$ is a separate real argument, so the joint law stays fixed as $k_W$ varies. The standing assumptions, a hypothesis of every model theorem, are: $\theta$ and $\xi$ are measurable and independent; $\theta$ is bounded and $0 \le \xi \le 1$ at every sample point; $\lambda > 0$; $N_R \ge 1$; $V(\theta) > 0$ and $V(\xi) > 0$. The last two come from the paper's statement that demand and supply are uncertain in the forward market. Third moments are central. The footnoted conditions $N_R > 6$ and $c \le \min\{p_R, a\}$ are not assumed, since the goal holds without them.

The spot inverse demand is the interior branch of the paper's $p_s = \max\{a + \theta - \xi k_W - q_P, 0\}$, used for all $k_W \ge 0$ and all realizations, with quantities ranging over the reals. This is what Assumption 1 (no blackouts or curtailment) licenses and what the paper's proof differentiates. The statement is therefore about the model with linear inverse demand. At realistic parameter values the turning point $\bar k^s_W$ can lie where Assumption 1 fails for some realizations, so its economic reading inside the no-curtailment region is the paper's interpretation, not part of the theorem.

The forward-spot equilibrium is a predicate built from optimization alone: retailer optimality over all real positions, clearing, and each producer's optimality against every deviation evaluated at that deviation's own clearing price. The closed forms (13)–(16) and the quartic's coefficients live in a separate definition file used only in milestone conclusions. The goal imports only the model. The goal also contains an existence conjunct, so the statement about equilibrium selections is not vacuous.

A complete development needs moment calculus for bounded independent random variables (variance and covariance of products, third central moments), maximization of concave quadratics, and single-crossing arguments for real polynomials. The moment computations and the mean-variance optimization of an affine position are reusable beyond this mission. Contributions are welcome at every milestone, including partial results.

Selected references

• H. Peura, D. W. Bunn, Renewable power and electricity prices: The impact of forward markets, Management Science 67(8), 4772–4788, 2021. https://doi.org/10.1287/mnsc.2020.3710 (read as the author-accepted manuscript, LBS Research Online eprint 1432, https://lbsresearch.london.edu/id/eprint/1432/).
• B. Allaz, J.-L. Vila, Cournot competition, futures markets and efficiency, Journal of Economic Theory 59(1), 1–16, 1993. https://doi.org/10.1006/jeth.1993.1001
• H. Bessembinder, M. L. Lemmon, Equilibrium pricing and optimal hedging in electricity forward markets, Journal of Finance 57(3), 1347–1382, 2002. https://doi.org/10.1111/1540-6261.00463

Motivation

Networks of autonomous sensors — machines on a factory floor, vehicles, devices in the Internet of Things — each measure a common environment with their own noise and can improve their estimates by asking other sensors for theirs. Communication capacity is limited, so each sensor must decide whom to ask, and the answer it receives is useful only to the extent that it understands how the other sensor turns measurements into estimates. Saghafian, Tomlin and Biller (SSRN 3124417, version of October 16, 2020; published in Manufacturing & Service Operations Management, 2021) model this as a dynamic target-selection problem and ask which communication network forms in the long run. Their abstract leads with the answer: each sensor eventually settles on a constant target set, which is sample-path dependent. With known, pairwise distinct qualities this target set is a single sensor (Proposition 4, p. 21). This mission formalizes that result.

Setting

There are $n$ sensors $N = \{1, \dots, n\}$. Sensor $i$ has a quality $q_i > 0$: its measurement of the state has noise variance $1/q_i^2$. Sensor $i$ starts with initial familiarities $v_{ij0}, w_{ij0} > 0$ with each other sensor $j$, the precisions of its initial Gaussian beliefs about $j$'s inference parameters. A sample path $S_\infty = (s_0, s_1, s_2, \dots)$ is the sequence of realized states, an arbitrary sequence of reals.

The familiarity function of $i$ with $j$ in period $t$ is a function $\psi_{ijt} : \mathbb R \to \mathbb R$. It starts at

$$\psi_{ij1}(s) = \frac{v_{ij0}^2 w_{ij0}^2}{w_{ij0}^2 + v_{ij0}^2 s^2} \qquad (12)$$

In period $t$, after $s_{t-1}$ is revealed, sensor $i$ targets the sensor of least signal variance

$$j^*_{it} = \arg\min_{j \in N\setminus\{i\}} \frac{q_j^2 + 1/\psi_{ijt}(s_{t-1})}{q_j^4}, \qquad (10)\text{–}(11)$$

with ties broken toward the lower index (footnote 11). Writing $a_{ijt} = 1$ if $j^*_{it} = j$ and $0$ otherwise, the familiarity grows by the stickiness factor:

$$\psi_{ij,t+1}(s) = \psi_{ijt}(s) + f(q_i,q_j)\,a_{ijt}, \qquad f(q_i,q_j) = \frac{1+q_i^2}{q_j^2(1+q_i^2+q_j^2)}. \qquad (14)$$

The long-run contacts of $i$ along $S_\infty$ are (Definition 2)

$$T_i(S_\infty) = \{\, j \in N\setminus\{i\} : \lim_{t\to\infty} \psi_{ijt}(s_{t-1}) = \infty \,\}. \qquad (20)$$

In Lean these are Instance (q, v, w), psi1, sigma2, stick, lowArgmin, the joint recursion fam/target, count and longRunContacts in IoTFusion.KnownQuality.

Formalization targets

Goal: Proposition 4 (p. 21)

If the qualities are asymmetric ($q_j \neq q_{j'}$ for $j \ne j'$, Definition 3), then for every sample path

$$|T_i(S_\infty)| = 1 \qquad \text{for all } i \in N.$$

No hypothesis on the state process is involved: the statement holds path by path.

Milestones

1. Proposition 2 (p. 15): the closed form $\psi_{ij,t+1}(s) = \psi_{ij1}(s) + f(q_i,q_j)\sum_{l=1}^{t} a_{ijl}$ (15).
2. Remark 1 (p. 20): $j \in T_i(S_\infty)$ iff $i$ targets $j$ infinitely often.
3. Lemma 2 (p. 21): for every $\epsilon > 0$ there is a fixed threshold $\bar\psi_\epsilon$ such that $\psi_{ijt}(s_{t-1}) > \bar\psi_\epsilon$ and $q_j/q_{j'} > 1+\epsilon$ imply $j^*_{it} \ne j'$.

Supporting items: $T_i(S_\infty) \ne \emptyset$ for $n \ge 2$ (long_run_contacts_nonempty); each sensor eventually targets one fixed sensor (eventually_constant_target, the wording of p. 5); and the rank-one precision identity (EC.66).

Significance

Proposition 4 says that, with known and distinct qualities, the long-run communication network is a functional graph — every sensor has out-degree one — although which graph forms depends on the realized states, and a sensor's eventual partner need not be the highest-quality sensor available. The paper builds on it its description of the long-run network as a random directed graph (Propositions 5–6) and its managerial discussion of early-period "momentum" in familiarity.

The result is proved in the paper; nothing in it is machine-checked. The work here is a formal proof of the deterministic core, including the existence half $T_i \neq \emptyset$, which the printed proof (p. ec22) does not give: it shows only $|T_i| \le 1$.

Difficulty

Every statement is elementary in isolation; the difficulty is that the target sequence is defined by a feedback loop. The target of period $t$ depends on familiarities, which depend on all earlier targets, which depend on earlier states. Statements about "infinitely often" therefore cannot be reduced to the behavior of any single function of $t$ fixed in advance.

The tempting argument "the highest-quality sensor eventually wins" is false: a sensor that becomes familiar early with a lower-quality partner can keep choosing it forever, so no fixed candidate for the unique contact exists. The uniqueness argument must instead compare two putative long-run contacts with each other, using a familiarity threshold that does not depend on the familiarity with the worse one (Lemma 2), and the existence half needs a separate counting argument over the finitely many possible targets.

Formalization scope

• Sensors are Fin n (0-based) with $n \ge 2$ on the existence statements; for $n = 1$ there is no other sensor and $T_i = \emptyset$.
• Periods are 0-based: Lean step $k$ is the paper's period $k+1$, the target at step $k$ uses the state $s_k$, and fam P i s k is $\psi_{ij,k+1}$.
• $q_i > 0$, and $v_{ij0}, w_{ij0}$ finite and positive, are theorem hypotheses (the paper's standing assumptions; its limiting case "fully knows", $v = w = \infty$, is not posed).
• Ties go to the lower index; "$\lim = \infty$" is Filter.Tendsto … atTop atTop; $|T_i|$ is Set.ncard; asymmetry is Function.Injective q.
• The familiarity function is defined by (12) and (14), the paper's familiarity dynamics. The paper derives (14) by Bayesian updating of the scalar $\hat\alpha_j + \hat\beta_j s_{t-1}$. Under the joint Gaussian beliefs, the update is exact for the precision at the realized state $s_{t-1}$ (the item (EC.66)), but at other states $s$ the posterior precision grows by less than $f$. Proposition 2(i) "for any $s$" is therefore a modelling choice. Every later result of the paper is derived from (15), so the dynamics (12) + (14) is the paper's operative model. Whether Proposition 4 survives under the exact bivariate posterior is open and not posed.
• Not posed: Propositions 5–6. Proposition 5's step "(EC.87): at $t^*$ the sets $T_i(S_\infty)$ are all determined" does not follow. Even with Gaussian innovations, a continuation of the path through a state near $0$ after any $t^*$ can make a never-targeted higher-quality sensor the unique long-run contact, so the printed claim fails without further assumptions on the state process. Lemma 1, Proposition 3 and Proposition 7 (unknown qualities) are outside this mission.
• Lemma 2's threshold depends on the pair $(j, j')$ in the paper's proof; the statement fixes the instance first and asks for one threshold per $\epsilon$, uniform over paths, sensors and periods (the maximum over the finitely many pairs).
• Trivializations ruled out: the target ranges over $j \neq i$ only, with a specified tie-break; familiarity and target form one trajectory determined by the instance, the sensor and the path, with no free history argument; $T_i$ is defined by divergence of $\psi_{ijt}(s_{t-1})$, not by target counts; the goal is $|T_i| = 1$, not $\le 1$; and it quantifies over every real path, with no AR(1) or typicality hypothesis.
• Infrastructure: none beyond Mathlib (finite sets, filters, $2\times2$ matrices for (EC.66)). Proofs of the milestones, of the existence half and of the goal are welcome in any order. A general lemma that "a sequence in a finite set takes some value infinitely often" with the matching Set.ncard bookkeeping would be reusable.

Selected references

• S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, SSRN 3124417, version of October 16, 2020. https://ssrn.com/abstract=3124417
• S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2020.0958

Motivation

Firms increasingly delegate the generation of new concepts (product designs, advertising campaigns, engineering prototypes) to outside providers such as design agencies and engineering consultancies. The client cannot dictate how hard the provider works; it can only decide when to stop asking for new solutions. Two practices are common. Under a flexible stopping policy the client keeps the right to stop or continue after each submitted solution. Under a committed stopping policy the client commits in advance to stop, and pay, as soon as a feasible solution arrives. Classical search theory says that keeping options open is never harmful, so flexibility should dominate. Yet committed contracts are widespread in practice.

Rahmani and Ramachandran (2021) explain this by two features that the classical benchmarks omit: a deadline on the number of rounds, and a provider who adjusts its effort from round to round in response to the client's policy. In two benchmark settings, an unlimited number of rounds or a fixed provider effort, flexibility (weakly) dominates (their Lemmas 1 and 2). With a deadline and strategic effort, commitment can be strictly better, and the paper characterizes exactly when.

Setting

A client delegates a project of $T = 2$ rounds to a provider. In each round $t$ in which the client asks for a solution, the provider chooses an effort $\mu_t \in \{\mu_l, \mu_h\}$, at cost $c_l$ or $c_h$, and submits a solution of quality $v_t \ge 0$. The client pays an evaluation cost $c_I$ for each submitted solution. When the project stops with a feasible solution ($v > 0$), the client implements the best solution received and pays the provider a fixed payment $p$; if no feasible solution is found by the deadline, nothing is paid.

Quality under effort $\mu$ has distribution function

$$\Phi_\mu(x) = 1 - \mu e^{-x/k}, \qquad x \ge 0,$$

where $k > 0$ is the provider's capability: with probability $1-\mu$ the solution is infeasible ($v = 0$), and otherwise it has density $\frac{\mu}{k}e^{-v/k}$ on $(0,\infty)$. The expected quality is $k\mu$. The standing assumptions are

$$0 < \mu_l < \mu_h < 1, \qquad 0 \le c_l < c_h, \qquad c_h/\mu_h \ge c_l/\mu_l .$$

Under the committed policy, the project stops after round 1 if $v_1 > 0$. Under the flexible policy, after a feasible $v_1$ the client compares $v_1 - p$ with the expected value of a second round and stops when stopping is at least as good. The provider anticipates this and chooses its efforts by backward induction: round-2 efforts $\mu^C_2$, $\mu^{F+}_2$ (after a feasible first solution), $\mu^{F-}_2$ (after an infeasible one), then round-1 efforts $\mu^C_1$, $\mu^F_1$. Write $\Pi^C_1$ and $\Pi^F_1$ for the client's equilibrium expected profits under the two policies.

Formalization targets

Goal: Proposition 4 (a)

Fix $\mu_l,\mu_h,c_l,c_h$ satisfying the standing assumptions and a payment $p > 0$. There exist thresholds $\hat c_I(k)$ and $\bar c_I(k)$ such that for all $k > 0$ and $c_I > 0$,

$$\Pi^F_1 < \Pi^C_1 \iff \hat c_I(k) < c_I < \bar c_I(k) \ \text{ and } \ p \ge \frac{c_h - c_l}{\mu_h - \mu_l}.$$

Commitment is strictly better exactly for an intermediate range of evaluation costs, and never when the payment is below $(c_h - c_l)/(\mu_h - \mu_l)$. The thresholds are left existential, as in the paper.

Milestones

1. §3.2, property (2): the expected quality under effort $\mu$ is $k\mu$.
2. Proposition 2 (a)–(b): the flexible client stops after a feasible $v_1$ if and only if $v_1 \ge v^F_s$, for a unique threshold $v^F_s \ge 0$.
3. Proposition 3 (a): under commitment, $(\mu^C_1,\mu^C_2)$ is $(\mu_l,\mu_l)$, $(\mu_l,\mu_h)$, $(\mu_h,\mu_h)$ as $p$ crosses thresholds $\underline p \le \bar p^C$.
4. Proposition 3 (b): under flexibility, $\mu^{F+}_2 = \mu_l$, and $(\mu^F_1,\mu^{F-}_2)$ switches at $\underline p$ and $\bar p^F$.
5. Proposition 3 (c): $\bar p^C \le \bar p^F$, and $\bar p^F - \bar p^C$ is nondecreasing in $k$ and nonincreasing in $c_I$.
6. Proposition 2 (c): $v^F_s$ is nondecreasing in $k$ and nonincreasing in $c_I$.
7. Lemma 2 at $T = 2$: with the same effort in every round, $\Pi^C_1 \le \Pi^F_1$.

Significance

Proposition 4 reverses the conventional wisdom that retaining decision rights cannot hurt the decision maker. The mechanism is strategic: flexible stopping lowers the provider's expected reward for a good first solution, because the client may continue the search instead of accepting it, and so it weakens the provider's first-round effort (Proposition 3). When the payment is in $[\bar p^C, \bar p^F)$, commitment induces high first-round effort that flexibility does not, and whether this outweighs the option value of a second round depends on the evaluation cost. The result gives contract designers in innovation procurement a concrete criterion in terms of evaluation cost, capability and payment.

The paper's proofs are in an online appendix. No machine-checked version of any result in this model exists. The mission produces a formal model of a dynamic principal–agent stopping game with an atom-plus-density quality law, a verified threshold structure for the client's stopping rule, and the full equilibrium effort characterization, all of which carry over to related delegation and contest models.

Difficulty

The goal compares two equilibrium profits, each determined by a nested backward induction in which the provider's round-1 effort depends on the client's stop rule, which in turn depends on the provider's round-2 effort. The obvious approach, comparing the two policies at the same efforts, proves only Lemma 2 and points the wrong way. The comparison must instead track which of the effort regimes of Proposition 3 each policy induces, as a function of $p$ and $c_I$. The profits are piecewise in $c_I$ (the stopping threshold is zero for large $c_I$), and the claim that the strict-improvement set in $c_I$ is a single open interval requires a monotonicity argument across these pieces, uniformly in $k$. The case $p < (c_h-c_l)/(\mu_h-\mu_l)$ must be shown to give no improvement at all.

Formalization scope

The Lean development models exactly the two-round game ($T = 2$), the case the paper analyzes in §4. Effort levels form a two-element inductive type; parameters $(\mu_l,\mu_h,c_l,c_h,k)$ form a record, with $c_I$ and $p$ separate arguments. The standing assumption $c_h/\mu_h \ge c_l/\mu_l$ is written cross-multiplied; $c_l \ge 0$ is the reading that costs are non-negative. The paper's Stieltjes integrals $\int_a^\infty g\,d\Phi_\mu$ are Bochner integrals of $g$ against the density over the open ray $(a,\infty)$; the atom at $0$ appears in the separate $\Phi_\mu(a)$ terms, so no payment is charged on infeasible solutions. Ties are broken as on the page: the provider takes high effort, and the flexible client stops. The paper's restriction to payments "neither too high nor too small" (Lemma A-1 of its online appendix) is not available; every statement is posed for all $p > 0$, for which it remains true. Evaluation costs satisfy $c_I > 0$.

The model defines no stopping threshold and no effort in closed form: the stopping threshold $v^F_s$ is a theorem (Proposition 2), $\mu^{F+}_2$ is computed from the provider's objective, and the goal compares profits at the efforts the model computes, not at efforts supplied as arguments. A formalization that defined $v^F_s = k\log(k\mu_l/c_I)$, fixed $\mu^{F+}_2 = \mu_l$, or compared the policies at exogenous efforts would make the milestones trivial or prove a different theorem, and is ruled out.

A complete development needs integrals of polynomial-times-exponential functions on rays, the closed forms of the round-2 values, and finite case analysis over effort profiles. Contributions to the comparative statics (Propositions 2 (c), 3 (c)) are welcome independently of the goal.

Not formalized: Proposition 4 (b) (its $\hat c_I$ half fails under the main-text model, e.g. at $\mu_l = 1/2$, $\mu_h = 4/5$, $c_l = 1/2$, $c_h = 1$, $p = 7/2$, $c_I = 9/10$, $k \in \{6, 8\}$); Lemma 1 (infinite horizon); Proposition 1 (general finite $T$); Proposition 5 (dependent solutions); Propositions 6–8 (endogenous payments); the numerical study.

Selected references

• M. Rahmani and K. Ramachandran, Delegating Innovation Projects with Deadline: Committed vs. Flexible Stopping, Management Science 67(10):6317–6332, 2021. https://doi.org/10.1287/mnsc.2020.3800
• C. Terwiesch and C. Loch, Collaborative prototyping and pricing of custom-designed products, Management Science 50(2):145–158, 2004 (cited by the paper as the source of the infinite-round and fixed-effort benchmarks).

Why platforms share demand information

Online retail platforms such as Amazon, Alibaba's Tmall and JD.com host thousands of third-party sellers and observe every customer interaction with each of them. From these interactions the platform learns about market demand far better than any single seller can, and it sells or gives away part of that knowledge through analytics tools (Alibaba's Business Advisor is the example in the source paper). The platform earns a commission on every seller's revenue, so it cares about the sellers' total profit, and it has to decide what each seller is told.

The classic literature on information sharing in oligopoly points the other way. Gal-Or (1985) showed that Cournot competitors facing a common demand shock never voluntarily pool their private demand signals: shared information makes their strategies more correlated, and the resulting competition destroys more value than the better forecasts create. Li (2002) and others refined the conditions. Liu, Zhang and Zhang (Manufacturing & Service Operations Management, 2023; SSRN 3258109) change who decides: the signals belong to the platform, which chooses what each seller learns in order to maximize its commission. Their headline result for the unconstrained ("asymmetric full sharing") format is that the platform shares everything it knows, without any added noise, but only with a limited number of sellers, and that number is determined by the substitution between products alone.

The model

There are $N \ge 1$ sellers of substitutable products. Given quantities $q_1, \dots, q_N$, seller $i$'s price is

$$p_i = a - q_i - b\sum_{d \ne i} q_d + u, \qquad 0 < b \le 1,$$

where $u \sim N(0, \sigma)$ is a common demand shock with prior variance $\sigma > 0$. The platform observes, for each seller $i$, a signal $x_i = u + e_i$ with $e_i \sim N(0, t)$, $t > 0$, independent of everything else.

A noise matrix $M = (m_{ij})$ with entries in $[0, +\infty]$ is the platform's sharing strategy. Seller $j$ receives the noisy copy $\hat x_{ij} = x_i + \epsilon_{ij}$, $\epsilon_{ij} \sim N(0, m_{ij})$ independent, for every $i$ with $m_{ij} < +\infty$; $m_{ij} = 0$ is truthful sharing and $m_{ij} = +\infty$ means $x_i$ is withheld from seller $j$. Seller $j$'s information $y_j(M)$ is the $\sigma$-algebra generated by what he receives.

Each seller chooses a quantity measurable with respect to his information to maximize his expected profit $\pi_i = E[(1 - \alpha) q_i p_i]$, where $\alpha \in (0,1)$ is the platform's commission rate. A Bayesian equilibrium under $M$ is a profile of such strategies from which no seller gains by deviating. The platform's expected profit is $\Pi = E[\alpha \sum_i q_i p_i]$, and it chooses $M$ before the signals are realized.

Under Asymmetric Full Sharing (AFS) each seller $j$ receives all $N$ signals with one common noise level $\eta_j = m_{ij}$ (for all $i$), and the levels may differ across sellers. The benchmark is no sharing, $m_{ij} = +\infty$ for all $i, j$, with platform profit $\Pi_{NS} = \alpha N a^2/[2 + b(N-1)]^2$.

Formalization targets

Goal: Proposition 2 (optimal asymmetric full sharing)

Let $m = \min\{2/b - 1, N\}$. Among all AFS noise matrices in $[0,+\infty]^{N \times N}$ and all equilibria, an optimal strategy is to share $\{x_1, \dots, x_N\}$ truthfully with sellers $1, \dots, K^*$ and nothing with the others, where

$$K^*_{AFS} \in \big\{\lfloor m \rfloor, \lceil m \rceil\big\}, \qquad \Pi^*_{AFS} = \frac{\alpha N a^2}{[2 + b(N-1)]^2} + \frac{\alpha K^*_{AFS}\,\sigma^2}{[2 + b(K^*_{AFS} - 1)]^2\,(\sigma + t/N)}.$$

The platform and every seller do weakly better than without sharing, and every optimal truthful group has size $\lfloor m \rfloor$ or $\lceil m \rceil$.

Milestones

1. Eq. (5): under full sharing with noise $\eta$, $E[u \mid y_j] = \frac{\sigma}{\sigma + (t + \eta)/N}\cdot\frac1N\sum_i \hat x_{ij}$.
2. Eq. (4): a profile is an equilibrium iff $q_i = \frac12\big(a - b\sum_{d\ne i}E[q_d \mid y_i] + E[u \mid y_i]\big)$ for all $i$.
3. Lemma 1: the no-sharing equilibrium quantities $a/(2 + b(N-1))$ and profit $\Pi_{NS}$.
4. A seller who receives nothing earns exactly his no-sharing profit (p. 13).
5. Under AFS, an interior noise level for one seller is strictly beaten by $0$ or $+\infty$ (p. 16).
6. Proposition 1 (AFS half): optimal AFS matrices have $m^*_{ij} \in \{0, +\infty\}$.
7. Eq. (8) at every group size $K \le N$.
8. The integer maximizers of $K \mapsto K/[2 + b(K-1)]^2$ on $\{0,\dots,N\}$ lie in $\{\lfloor m \rfloor, \lceil m \rceil\}$ (p. 18).
9. Informed sellers strictly gain and the others earn the benchmark (p. 19).

Significance

The result separates two levers of information design, precision and audience, and shows that in this linear-Gaussian Cournot setting only the audience matters: the platform never degrades a signal, it only chooses how many sellers see it. The optimal audience size $\min\{2/b - 1, N\}$ depends only on the substitution parameter once the market is large, and equals one seller when products are perfect substitutes. This reverses the Gal-Or no-sharing result by changing who decides, and it explains why a commission-earning platform may rationally treat its sellers asymmetrically, which is the tension the paper's later sections on fairness and privacy constraints study.

The paper's proofs are in an online appendix. No part of this model has a machine-checked proof. The mission produces a reusable Lean layer for Bayesian games with designed Gaussian signals: information $\sigma$-algebras generated by noisy copies of shared signals, Bayesian Nash equilibrium over square-integrable strategies, and its characterization by first-order conditions in conditional expectations. Mathlib has Gaussian measures, conditional expectation and independence, but not the projection formula for jointly Gaussian vectors that eq. (5) needs.

Difficulty

The closed forms are routine once one assumes that equilibria are linear in the received average signal. The difficulty lies in what that assumption skips. First, eq. (5) is a statement about conditional expectation with respect to a $\sigma$-algebra generated by $N$ correlated Gaussian variables; it needs the Gaussian conditioning (projection) theorem, not a computation with densities. Second, the goal quantifies over all equilibria, so existence and uniqueness of the equilibrium must be proved for every noise matrix, including those with infinite entries; the paper solves the first-order condition and never discusses uniqueness. Third, Proposition 1 is an optimization over $[0,+\infty]^N$: the platform's profit is not concave in the noise levels, and the endpoint property for one seller (with the others fixed at arbitrary levels) is the step that rules out partial sharing. Restricting attention to truthful groups from the outset assumes away exactly this step.

Formalization scope

All declarations live in the namespace RetailInfoShare.AFS, with one definitions file RetailInfoShare.AFS.Model. Conventions:

• $\sigma$, $t$ and $m_{ij}$ are variances (gaussianReal 0 σ), as eq. (3) of the paper requires.
• The primitives $u$, $e_i$ and standard normals $\xi_{ij}$ are measurable and mutually independent on one probability space; the added noise is $\epsilon_{ij} = \sqrt{m_{ij}}\,\xi_{ij}$. The paper's "cov = 0" is read as independence, as its text says.
• Noise levels are in ℝ≥0∞; a signal with $m_{ij} = \top$ never enters the receiving seller's information $\sigma$-algebra.
• Equilibrium is the ex-ante best-response property over square-integrable strategies measurable for the seller's information; this is equivalent a.e. to the interim maximization of eq. (2).
• The platform's profit is the unconditional expectation (the matrix is chosen before the signals).
• Added standing hypotheses: $0 < \alpha < 1$ (never stated in the paper), and $\sigma > 0$, $t > 0$, $N \ge 1$ made explicit. Sellers are Fin N, so the paper's sellers $1,\dots,K$ are indices $0,\dots,K-1$.
• Profits and equilibria are defined from the model, never by the closed forms (4) or (8); a formalization that defined $\Pi$ by eq. (8) or optimized only over truthful groups would reduce the goal to milestone 8 and is ruled out.

Out of scope: the AIS half of Proposition 1, Proposition 3 and Lemma 2 (privacy-constrained sharing), the symmetric formats of §5, the pricing mechanism of §6, and the appendix extensions. Contributions of general infrastructure are welcome: the Gaussian conditioning theorem in Mathlib form, and existence and uniqueness of equilibria in linear-quadratic Bayesian games with Gaussian information.

Selected references

• Z. Liu, D. J. Zhang, F. Zhang, Information Sharing on Retail Platforms, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2020.0915 (preprint: SSRN 3258109, https://ssrn.com/abstract=3258109)
• E. Gal-Or, Information Sharing in Oligopoly, Econometrica 53(2), 1985. https://doi.org/10.2307/1911241
• L. Li, Information Sharing in a Supply Chain with Horizontal Competition, Management Science 48(9), 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
• L. Li, Cournot Oligopoly with Information Sharing, RAND Journal of Economics 16(4), 1985. https://doi.org/10.2307/2555502

Motivation

A manufacturer selling through several retailers rarely publishes the terms it gives each of them. Wholesale prices, slotting fees and rebates are negotiated bilaterally, and a retailer usually sees its own contract but not its rival's. Much of the supply-chain contracting literature nevertheless assumes observable contracts, and under that assumption a well-known ranking holds: the manufacturer, the channel and social welfare do better with two-part tariffs (a fixed fee plus a marginal wholesale price), while the retailers do better with plain wholesale-price contracts.

The industrial-organization literature has long known that secrecy changes the manufacturer's problem. Hart and Tirole (1990), O'Brien and Shaffer (1992) and McAfee and Schwartz (1994) showed that a manufacturer that cannot commit publicly to the terms it offers each retailer is tempted to undercut itself bilaterally: it offers one retailer a better deal, at the expense of the others, and the retailers anticipate this. Li and Liu (Manufacturing & Service Operations Management, SSRN 3339702) ask what this does to the ranking of contract types in a simple model of price competition. Their answer, Proposition 3, is that the ranking reverses when competition is intense: the manufacturer prefers wholesale prices once the competition parameter reaches $2\sqrt2$, the retailers always prefer them, and the whole industry prefers them once the parameter reaches $\sqrt3 - 1$.

Setting

A manufacturer with zero unit cost sells one product through two retailers $i \in \{1,2\}$. Retailer $i$ charges price $p_i$ and faces demand

$$D_i = 1 - p_i + \theta\,(p_j - p_i), \qquad j \ne i,$$

where $\theta \ge 0$ measures how intensely the retailers compete.

The manufacturer offers each retailer a contract $C_i = (K_i, w_i)$, a fixed fee $K_i$ and a marginal wholesale price $w_i$. In the two-part tariff game contracts range over $\{(K,w): w \ge 0\}$; in the wholesale-price game over $\{(0,w): w \ge 0\}$. The contract type is common knowledge, but retailer $j$ does not observe the terms offered to retailer $i$.

Each retailer, seeing only its own contract, accepts or rejects and chooses a price $p_i \ge 0$ and an order $Q_i \ge 0$. A retailer holding the belief $\tilde p_j$ about its rival's price conjectures the profit

$$\tilde\pi_i = p_i \min\bigl(Q_i,\ 1 - p_i + \theta(\tilde p_j - p_i)\bigr) - w_i Q_i - K_i ,$$

and $0$ if it rejects. The manufacturer earns $w_i Q_i + K_i$ from each retailer that accepts.

Because no proper subgame exists, the solution concept is the contract equilibrium with passive beliefs: a pair of contracts $(C_1^*, C_2^*)$ and, for each retailer, a strategy $\sigma_i$ giving an action at every contract of the class, such that

1. at every contract $C$, $\sigma_i(C)$ maximizes $\tilde\pi_i$ for the belief $\tilde p_j$ equal to the rival's equilibrium price, the price in $\sigma_j(C_j^*)$, so an unexpected offer does not change the belief;
2. no pair of contracts gives the manufacturer more total profit when each retailer responds to its own contract through $\sigma_i$.

The equilibrium profits are the manufacturer's $\Pi$, retailer $i$'s $\pi_i$ (computed with the actual prices), and the industry's $\Pi + \pi_1 + \pi_2$.

Formalization targets

Goal: Proposition 3

For every $\theta \ge 0$, both games have a passive-belief equilibrium, and for every equilibrium $E^T$ of the tariff game and $E^W$ of the wholesale-price game,

$$\Pi(E^T) \le \Pi(E^W) \iff \theta \ge 2\sqrt2, \qquad \pi_i(E^T) < \pi_i(E^W)\ (i = 1,2), \qquad \Pi_{\mathrm{ind}}(E^T) \le \Pi_{\mathrm{ind}}(E^W) \iff \theta \ge \sqrt3 - 1,$$

together with the strict versions of the two equivalences ($<$ iff $>$). At the thresholds the two profits coincide.

Milestones

1. Equation (2), p. 13: an accepting retailer with belief $\tilde p$ and contract $(K,w)$ charges $p = \frac{1+\theta\tilde p}{2+2\theta} + \frac w2$ and orders its conjectured demand.
2. Two-part tariffs, bilateral optimum, p. 14: against a retailer with a fixed belief, the manufacturer's best tariff is $\bigl(\frac{(1+\theta\tilde p)^2}{4(1+\theta)}, 0\bigr)$.
3. Wholesale prices, bilateral optimum, p. 17: the best wholesale price is $\frac{1+\theta\tilde p}{2(1+\theta)}$.
4. Proposition 1, p. 14: under unobservable two-part tariffs every equilibrium has $(K_i,w_i) = \bigl(\frac{1+\theta}{(2+\theta)^2}, 0\bigr)$, $p_i = \frac1{2+\theta}$, $\Pi = \frac{2(1+\theta)}{(2+\theta)^2}$, $\pi_i = 0$.
5. Proposition 2, p. 16: under unobservable wholesale prices every equilibrium has $w_i = \frac2{4+\theta}$, $p_i = \frac3{4+\theta}$, $\Pi = \frac{4(1+\theta)}{(4+\theta)^2}$, $\pi_i = \frac{1+\theta}{(4+\theta)^2}$.

Significance

Proposition 3 shows that the textbook ranking of supply-chain contracts depends on an observability assumption that is often false in practice. Under secret contracts the fixed fee loses its usual advantage: a manufacturer offering two-part tariffs cuts marginal wholesale prices to zero, retail competition becomes as fierce as possible, and all profit has to be collected through fees out of a shrinking pie. A wholesale price keeps marginal costs, and therefore retail prices, high. For $\theta \ge 2\sqrt2$ this "win-win" makes both the manufacturer and the retailers better off; as $\theta \to \infty$ the manufacturer's gain approaches 100 percent and the industry's 200 percent (p. 18).

The proposition is proved in the paper's Online Appendix. No machine-checked proof of it, or of the underlying equilibria, is known. A formalization would fix the solution concept precisely (quantification over off-path contracts, the tie-break at zero conjectured profit, the domain of contracts), establish uniqueness of the equilibria, which the page asserts only implicitly, and provide a reusable encoding of contract equilibria with passive beliefs for later missions on vertical contracting.

Difficulty

The closed forms of Propositions 1 and 2 make Proposition 3 a comparison of rational functions. The work is in the equilibrium layer. The retailers' strategies must be optimal at every contract, including contracts never offered, and the manufacturer's deviation is evaluated against those off-path responses while the rival's action is held fixed. Each retailer's belief is pinned to the rival's equilibrium price, so the equilibrium is a fixed point of a belief map composed with two optimization problems, the retailer's and the manufacturer's bilateral one. Uniqueness of the equilibrium is part of the claim, and the retailer's problem is non-smooth because of the $\min$ in sales and the accept/reject choice. At a zero marginal price the optimal order is not unique, so order quantities cannot be pinned down.

Formalization scope

Everything lives in the namespace ContractUnobs.Compare, with one definitions module, ContractUnobs.Compare.Model. Retailers are indexed by Fin 2 with rival 1 - i; all quantities are real. A contract is a structure with fields K and w; a retailer's action records accept : Bool, a price p and an order Q. IsPassiveEq θ cls E is the equilibrium condition above for a contract class cls (tariffClass or wholesaleClass); mfrProfit, retProfit and industryProfit are the realized profits.

Conventions committed to, each disclosed in the item statements:

• wholesale prices are nonnegative in both classes ($w < 0$ makes the retailer's order problem unbounded);
• retail prices are nonnegative (the paper assumes prices induce nonnegative demand, p. 11), and sales are $\min(Q, \max(0, D))$;
• a retailer whose best conjectured profit is exactly $0$ accepts (as on p. 13);
• the manufacturer is paid for quantities ordered;
• "in equilibrium" is read as a statement about every equilibrium, together with existence;
• in Proposition 3, "higher when $\theta \ge 2\sqrt2$" is read as an equivalence (weak at the threshold, strict beyond it), with the converse shown in the paper's figures.

Stating Proposition 3 with the closed-form values of Propositions 1 and 2 substituted for the equilibria is a different, nearly trivial theorem and is not the goal; the goal quantifies over equilibrium profiles, and its existence conjuncts exclude a vacuous reading.

The observable benchmark (Lemmas 1–3), the corollaries, and the extensions of §6 (buyback contracts, asymmetric retailers, downstream merger) are not part of this mission. Contributions welcome: proofs of the milestones, a general lemma on maximizing $(p-w)(A-Bp)$ over $p \ge 0$, and a reusable treatment of passive-belief contract equilibria.

Selected references

• X. Li and Q. Liu, Contract Unobservability and Downstream Competition, Manufacturing & Service Operations Management; SSRN preprint 3339702. https://ssrn.com/abstract=3339702 (published version: https://doi.org/10.1287/msom.2020.0905)
• O. Hart and J. Tirole, Vertical Integration and Market Foreclosure, Brookings Papers on Economic Activity: Microeconomics, 1990, 205–286. https://doi.org/10.2307/2534783
• D. P. O'Brien and G. Shaffer, Vertical Control with Bilateral Contracts, RAND Journal of Economics 23(3), 1992, 299–308. https://doi.org/10.2307/2555895
• R. P. McAfee and M. Schwartz, Opportunism in Multilateral Vertical Contracting: Nondiscrimination, Exclusivity, and Uniformity, American Economic Review 84(1), 1994, 210–230. https://www.jstor.org/stable/2117980

Motivation

Firms carry risks they cannot insure directly. A farmer's revenue depends on local yield and on local price; an airline's cost depends on jet fuel at a specific airport; an energy retailer's margin depends on load and on weather. Exchange-traded derivatives are written on standardized indices, so the exposure that matters is only partly claimable. Guiotto and Roncoroni (Operations Research 2022) study the design of a combined custom hedge: one over-the-counter claim written on the claimable part $X$ of the firm's risk, plus a second claim written on a side index $I$ that is correlated with the unclaimable part. The question is when such a pair is well defined, that is, when the firm's mean–variance hedging problem has one and only one optimal pair of claims.

Single-claim custom hedging goes back to Chowdhry and Howe (1999) and Caldentey and Haugh (2006; 2009, Operations Research 57(1)), whose framework prices claims through a pricing kernel $dQ/dP$ known to the firm; that framework is adopted here. With two claims on two different random elements the optimal pair is coupled, and existence and uniqueness are no longer automatic.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying three random elements, valued in arbitrary measurable spaces: the claimable term $X$, the nonclaimable term $Y$ and the side index $I$. Write $\mathcal F_X=\sigma(X)$ and $\mathcal F_I=\sigma(I)$. The firm's business position is $\pi=\pi(X,Y)$ for a Borel revenue function $\pi$, assumed square-integrable.

A claim on $X$ is a random variable $H$ that is $\mathcal F_X$-measurable and has finite variance; the set of such claims is $\mathcal H_X$, and $\mathcal H_I$ is defined likewise. The centered subspace $\mathbb H_X\subseteq\mathcal H_X$ consists of claims with $\mathbb E[H]=0$.

Claims are priced by a pricing kernel $dQ/dP$, the density of an equivalent martingale measure $Q$: it is positive almost surely, has mean one and is square-integrable, and $\mathbb E_Q[Z]=\mathbb E[Z\,dQ/dP]$. The firm ranks positions by the mean–variance criterion

$$\mathcal U(Z)=\varrho\,\mathbb E[Z]-\tfrac a2\operatorname{Var}[Z],\qquad \varrho\ge 0,\ a>0 .$$

The value-centered design problem is

$$\max\Big\{\mathcal U\big(\pi+[H+G]\big)\ :\ H\in\mathcal H_X,\ G\in\mathcal H_I,\ \mathbb E_Q[H]=\mathbb E_Q[G]=0\Big\}.\qquad(4)$$

A maximizer $(H^*,G^*)$ is an optimal combined claim pair. The dependence between $X$ and $I$ is measured by the maximal correlation

$$r_{XI}=\sup\big\{\rho(\phi,\psi)\ :\ \phi\in\mathbb H_X,\ \psi\in\mathbb H_I\big\}\in[0,1],\qquad(6)$$

with $\rho$ the Pearson correlation. Finally $\mathcal K=\pi+(\varrho/a)\,dQ/dP$ is the optimal hedging kernel, $\Pi^X_0=-\mathbb E\big[\mathcal K-\mathbb E[\mathcal K\mid\mathcal F_I]\mid\mathcal F_X\big]$, and $T[Z]=\mathbb E\big[\mathbb E[Z\mid\mathcal F_I]\mid\mathcal F_X\big]$.

Formalization targets

Goal: Theorem 1 (p. 11)

If $r_{XI}<1$, then

1. an optimal combined claim pair $(H^*,G^*)$ of (4) exists;
2. it is unique up to $P$-null sets, and so is the hedge $H^*+G^*$;
3. the value-centered optimal claim $H^*_0=H^*-\mathbb E[H^*]$ solves

$$H^*_0=\Pi^X_0+\mathbb E\big[\mathbb E[H^*_0\mid\mathcal F_I]\mid\mathcal F_X\big].\qquad(7)$$

Milestones

• Proposition 1 (p. 9): every optimal pair is $H^*=H^*_0-\mathbb E_Q[H^*_0]$, $G^*=G^*_0-\mathbb E_Q[G^*_0]$ with $P$-centered $(H^*_0,G^*_0)$ solving the first-order system (5).
• (EC.25)–(EC.26) (p. ec24): a centered solution of (5) satisfies $H_0=\Pi_0+T[H_0]$.
• $T$ on $\mathbb H_X$ (p. ec24): $\mathbb E[T[Z]]=\mathbb E[Z]$, $T(\mathbb H_X)\subseteq\mathbb H_X$, and $\Pi_0\in\mathbb H_X$.
• Inner-product bound (p. ec25): $\langle\mathbb E[\phi\mid\mathcal F_I],\psi\rangle\le r_{XI}\|\phi\|_2\|\psi\|_2$ for $\phi\in\mathbb H_X$, $\psi\in\mathbb H_I$.
• (EC.28) (p. ec25): $\|\mathbb E[\phi\mid\mathcal F_I]\|_2\le r_{XI}\|\phi\|_2$.
• $\|T\|\le r_{XI}$ (p. ec25) on $\mathbb H_X$.
• (EC.27) (p. ec25): if $r_{XI}<1$, $H_0=\Pi_0+T[H_0]$ has a unique solution in $\mathbb H_X$.

Significance

The result. Theorem 1 makes the combined hedge an object: without it the optimal pair may fail to exist or may be non-unique (the paper points to Appendix EC.1(F) for non-uniqueness), and the paper's later results, the design integral equation (Theorem 2) and the value of combining claims (Theorem 3 and Definitions 1–3), are stated for the optimal pair whose existence and uniqueness Theorem 1 provides. Equation (7) separates the optimal claim into a part determined by the kernel $\mathcal K$ alone and a cross-claim feedback through $I$. The condition $r_{XI}<1$ is checkable: for jointly lognormal $(X,I)$ it reduces to $|\rho_{Z,W}|<1$ for the underlying normals (Example 4).

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof needs a Hilbert-space treatment of conditional expectations onto two σ-algebras, a formal maximal-correlation index, and an existence argument for the maximization problem itself, which the paper's proof leaves implicit (see below). The intermediate statements are general facts about pairs of σ-algebras with maximal correlation below one and are reusable outside hedging.

Difficulty

The optimal pair is coupled: the claim on $X$ depends on the conditional expectation of the claim on $I$ given $X$ and conversely, so neither can be computed first. When $X$ and $I$ share information, the two claim spaces overlap and the sum $\mathcal H_X+\mathcal H_I$ need not be closed in $L^2$; a maximizing sequence can then escape, and two different pairs can produce the same hedge. The condition $r_{XI}<1$ excludes this, and the work lies in turning it into a quantitative bound on the alternating conditional-expectation operator.

A second difficulty is a gap in the printed argument. The paper derives the first-order system (5) as a necessary condition and then proves that the resulting fixed-point equation has a unique solution. It does not show that the pair built from that solution is optimal for (4), so existence of a maximizer needs a separate argument that the first-order condition is also sufficient or that the maximum is attained. The goal is stated for maximizers of (4), so this step cannot be skipped.

Formalization scope

Everything lives in the namespace CustomHedge.Exist. A Market bundles $P$, $X$, $Y$, $I$, the revenue function, the kernel D $=dQ/dP$, rho $=\varrho$ and a; Standing collects the assumptions above. Conventions:

• Claims are random variables $\Omega\to\mathbb R$, strongly measurable for $\sigma(X)$ (resp. $\sigma(I)$) and in $L^2(P)$, not payoff functions $x\mapsto H(x)$.
• Optimality is maximization of U over all feasible pairs; uniqueness and the equations (5), (7), (EC.25), (EC.27) hold $P$-almost surely.
• $\mathbb E_Q$ centers the budget constraint; $\mathbb E=\mathbb E_P$ centers $H^*_0$, $\mathbb H_X$ and the maximal correlation.
• The paper allows $a\ge0$; the formalization requires $a>0$, because $\mathcal K$ divides by $a$ and with $a=0$ problem (4) generally has no maximizer. $\varrho=0$ is allowed.
• The maximal correlation is a real supremum over pairs with positive variances (where $\rho$ is defined), with $\sup\emptyset=0$; the set is bounded by one.
• $\|Z\|_2=(\mathbb E[Z^2])^{1/2}$; conditional expectation is Mathlib's condExp.

A trivializing formalization is ruled out: the goal quantifies over maximizers of (4), not over solutions of the first-order system or of (EC.27), which are separate milestones. A sorry-free check confirms the standing assumptions and $r_{XI}<1$ hold together with a non-trivial $\sigma(X)$.

Needed infrastructure: $L^2$ conditional expectation as an orthogonal projection, the identity $\mathbb E[\mathbb E[\phi\mid\mathcal G]\psi]=\mathbb E[\phi\psi]$ for $\mathcal G$-measurable $\psi$, Banach's fixed-point theorem on a closed subspace of $L^2$, and concave maximization over a closed affine subspace. The maximal-correlation file is reusable beyond this mission. Proofs of individual milestones, and a proof of the goal by any route, are welcome.

Selected references

• P. Guiotto and A. Roncoroni, Combined custom hedging: optimal design, noninsurable exposure, and operational risk management, Operations Research 70(3), 2022. https://doi.org/10.1287/opre.2021.2133 (cited from manuscript OPRE-2019-01-058.R3)
• R. Caldentey and M. Haugh, Optimal control and hedging of operations in the presence of financial markets, Mathematics of Operations Research 31(2), 2006. https://doi.org/10.1287/moor.1060.0193
• B. Chowdhry and J. T. B. Howe, Corporate risk management for multinational corporations: financial and operational hedging policies, European Finance Review 2, 229–246, 1999 (as cited in the paper; no link verified).
• A. Rényi, On measures of dependence, Acta Mathematica Academiae Scientiarum Hungarica 10, 1959. https://doi.org/10.1007/BF02024507
• B. Schweizer and E. F. Wolff, On nonparametric measures of dependence for random variables, Annals of Statistics 9(4), 1981. https://doi.org/10.1214/aos/1176345528