Equation (2), p. 10 — the downstream Cournot equilibrium

Proved

CrossLicensing.ExPost.equation_2

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

cournotcross-licensingnash-equilibriump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Fix $0\le\beta\le1$ , $0\le T_1\le T_2$ , and $r\ge0$ . Let $r_1=1+T_1(2-\beta)-T_2(1-2\beta)$ and $r_2=1+\beta T_1+T_2$ . A quantity profile is a Nash equilibrium of the manufacturers' nonnegative-quantity game (1) exactly when it equals

(q_1,q_2)=\begin{cases} \left(\dfrac{1-r+T_1(2-\beta)+T_2(-1+2\beta)}{3},\dfrac{1-r+T_1(-1+2\beta)+T_2(2-\beta)}{3}\right),&r\le r_1,\\ \left(0,\dfrac{1-r+\beta T_1+T_2}{2}\right),&r_1<r\le r_2,\\ (0,0),&r>r_2. \end{cases}

Thus the displayed outcome exists and is the unique quantity equilibrium, including both regime boundaries. Formalization Note The paper's first line of (2) has an unclosed parenthesis; the intended first quantity is the fraction shown above. The nonnegative wholesale-price domain is explicit.

Preamble

import Mathlib
import Definitions.Def_CrossLicensing_ExPost_Model

Formal statement

namespace CrossLicensing.ExPost

/-- Equation (2), read as an exact characterization of the quantity-game equilibrium. -/
theorem equation_2 (β T₁ T₂ r : ℝ) (h : Standing β T₁ T₂ r) (q : ℝ × ℝ) :
    IsQuantityNE β T₁ T₂ r q ↔ q = quantityFormula β T₁ T₂ r := by sorry

end CrossLicensing.ExPost

Source

Wang, Huang, Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN 3053682 (version of 2023-04-27), p. 10, equation (2)

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph