Proposition 7(a), p. 21 — Cournot: (S,S) unique below k_N, (S,S) and (N,N) with (S,S) Pareto-better between, (N,N) unique above k_S
ProvedCompetingChains.Cournot.proposition_7aFix the competition intensity , the signal accuracy and the prior variance . There exist thresholds with
such that, for all satisfying the standing assumptions , , , the set of pure-strategy equilibria of the stage-one information-sharing game between the two manufacturers (Table 1) is:
- if : ;
- if : , and each manufacturer's payoff at is strictly larger than at ;
- if : .
Here manufacturer chooses whether chain shares () or not (), pays the retailer the side payment needed to induce sharing, and earns if it shares and otherwise.
This is the main result of the Cournot half of the paper: information sharing is the unique outcome when cost reduction is efficient, a coordination problem with a Pareto-better sharing equilibrium at intermediate efficiency, and absent when cost reduction is inefficient.
Formalization Note The thresholds depend only on and are chosen before ; their bounds are those of Proposition 6(a)(2), and they make all three cases nonempty. The page's "otherwise" is stated as : at and both and are equilibria, so the boundary points are left out. Only pure-strategy equilibria are counted, as in the paper (the middle region also has a mixed equilibrium). "Pareto optimal" is the strict inequality of the payoffs at over , stated for manufacturer 1; by symmetry it is the same for manufacturer 2. The hypothesis is added (at the middle region is empty).
import Mathlib import Definitions.Def_CompetingChains_Cournot_Setting
namespace CompetingChains.Cournot
theorem proposition_7a (γ t σsq : ℝ) (hγ0 : 0 < γ) (hγ1 : γ < 1) (ht : 0 < t) (hσ : 0 < σsq) :
∃ kN kS : ℝ, 1 / 2 < kN ∧ kN < kS ∧ kS < (3 + Real.sqrt 5) / 4 ∧
∀ a c k : ℝ, Standing a c k γ t σsq →
(k < kN → equilibria a c k γ t σsq = {(.S, .S)}) ∧
(kN < k → k < kS →
equilibria a c k γ t σsq = {(.S, .S), (.N, .N)} ∧
payoff a c k γ t σsq .N .N < payoff a c k γ t σsq .S .S) ∧
(kS < k → equilibria a c k γ t σsq = {(.N, .N)}) := by sorry
end CompetingChains.Cournot
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.