Appendix A1, PDF p. 28 (printed p. 22) — r₁ − t = −t(e + 4t − √(3(4t² − e²)))/(2(e + t)), and the numerator is positive

Proved

Multihoming.Hump.r1_sub_t

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

comparative-staticshotellingnetwork-effectsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $t>0$ and $0\le e<2t$ , and let $r_1$ be the root of Appendix A1. Then

r_1-t=-t\,\frac{e+4t-\sqrt{3(4t^2-e^2)}}{2(e+t)},

and $e+4t-\sqrt{3(4t^2-e^2)}>0$ . In particular $r_1<t$ .

This locates the profit's peak $r_1$ strictly inside $[0,t)$ at its right end.

Preamble

import Mathlib
import Definitions.Def_Multihoming_Hump_Model

Formal statement

namespace Multihoming.Hump

/-- Appendix A1, PDF p. 28: r₁ − t = −t (e + 4t − √(3(4t² − e²)))/(2(e + t)), and
e + 4t − √(3(4t² − e²)) is positive. -/
theorem r1_sub_t (t e : ℝ) (ht : 0 < t) (he0 : 0 ≤ e) (he : e < 2 * t) :
    r1 t e - t = -t * ((e + 4 * t - Real.sqrt (3 * (4 * t ^ 2 - e ^ 2))) / (2 * (e + t))) ∧
    0 < e + 4 * t - Real.sqrt (3 * (4 * t ^ 2 - e ^ 2)) := by sorry

end Multihoming.Hump

Source

Foros, Kind & Stähler, Endogenous multihoming and network effects: PlayStation, Xbox, or both?, SNF Working Paper No. 16/21 (NHH Bergen, December 2021; Management Science DOI 10.1287/mnsc.2022.00613), PDF p. 28 (printed p. 22), Appendix A1, display r₁ − t

Human review

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

View graph