Proof of Proposition 1, p. 10 — unique equilibrium outside the threshold prices

Proved

NetExtDominance.Introspective.unique_equilibrium_outside

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

fixed-pointsnetwork-externalitiesp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1unique-equilibrium

In a market with In/Out inverse demand, suppose the relative price lies outside the interval of multiple equilibria, so $p>p_{\max}$ or $p<p_{\min}$ . Then there is exactly one feasible equilibrium quantity:

\exists!q\in[0,1],\quad D(p,q)=q.

This supplies the unique equilibrium named in the second part of Proposition 1.

Formalization Note An equilibrium is a fixed point of aggregate demand, including at $q=0$ or $q=1$ . At prices beyond $P(0)$ or $P(1)$ there need not be a solution to $P(q)=p$ ; the proof paragraph's claim about an inverse-demand intersection is read as the stated fixed-point claim.

Preamble

import Mathlib
import Definitions.Def_NetExtDominance_Introspective_Setting

Formal statement

namespace NetExtDominance.Introspective

/-- Proof of Proposition 1, second paragraph: outside the threshold prices
there is a unique feasible fixed point of aggregate demand. -/
theorem unique_equilibrium_outside
    (M : Market) (QL QH : ℝ) (hIO : IsInOut M.P QL QH)
    (p : ℝ) (hp : pmax M.P QH < p ∨ p < pmin M.P QL) :
    ∃! q, IsEquilibriumQty M p q := by sorry

end NetExtDominance.Introspective

Source

Akerlof, Holden & Rayo, Network Externalities and Market Dominance, author's accepted manuscript (WRAP 178238, dated September 16, 2022), p. 10, proof of Proposition 1, second paragraph; http://wrap.warwick.ac.uk/178238

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