Proof of Proposition 1, p. 10 — convergence to the unique equilibrium from every impulse

Proved

NetExtDominance.Introspective.converge_outside

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

equilibrium-selectionmonotone-dynamicsnetwork-externalitiesp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

In a market with In/Out inverse demand, suppose $p>p_{\max}$ or $p<p_{\min}$ , and let $q\in[0,1]$ be an equilibrium quantity, $D(p,q)=q$ . Every impulse $I_0\in[0,1]$ produces level- $k$ consumption converging to $q$ :

D(p,\cdot)^{\circ k}(I_0)\longrightarrow q\qquad(k\to\infty).

With uniqueness of the equilibrium quantity, this establishes impulse independence outside the threshold interval.

Formalization Note The equilibrium hypothesis refers to aggregate demand, including saturated quantities at $0$ and $1$ .

Preamble

import Mathlib
import Definitions.Def_NetExtDominance_Introspective_Setting

Formal statement

namespace NetExtDominance.Introspective

/-- Proof of Proposition 1, second paragraph: every admissible impulse
converges to the unique equilibrium outside the threshold prices. -/
theorem converge_outside
    (M : Market) (QL QH : ℝ) (hIO : IsInOut M.P QL QH)
    (p : ℝ) (hp : pmax M.P QH < p ∨ p < pmin M.P QL)
    (q : ℝ) (hq : IsEquilibriumQty M p q)
    (I0 : ℝ) (hI0 : I0 ∈ Set.Icc (0 : ℝ) 1) :
    IsIntrospectiveEq M p I0 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