p. 15 — under a ban the seller prefers the high-price option iff f > (1 − (2 − q)η)qv/(1 − η) − c

Proved

MarketplaceLeakage.Communication.s_option_choice

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

communication-banleakagep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1platforms

Under a ban on buyer–seller communication, the seller compares two on-platform prices. At $p_m=v$ it sells to the fraction $\eta q$ of buyers who learn that they value the product at $v$ , earning $\eta q\,(v-c-f)$ ; at $p_m=qv$ it also sells to the $1-\eta$ uninformed buyers, earning $(1-\eta+\eta q)(qv-c-f)$ .

Let $c<v$ , $0<q<1$ and $0\le\eta<1$ . For every fee $f$ , the high-price option pays strictly more than the low-price option if and only if

f>\frac{(1-(2-q)\eta)\,qv}{1-\eta}-c .

Otherwise the seller chooses the low-price option.

This threshold determines which option the marketplace induces with its fee, and is the basis of the computation of the marketplace's profit under a ban.

Formalization Note. The statement excludes $\eta=1$ , where the threshold divides by zero; there the comparison does not depend on $f$ .

Preamble

import Mathlib
import Definitions.Def_MarketplaceLeakage_Communication_Setting

Formal statement

namespace MarketplaceLeakage.Communication

theorem s_option_choice (v c : ℝ) (hvc : c < v) (q η f : ℝ) (hq0 : 0 < q) (hq1 : q < 1)
    (hη0 : 0 ≤ η) (hη1 : η < 1) :
    lowPay v c q η f < highPay v c q η f ↔ (1 - (2 - q) * η) * q * v / (1 - η) - c < f := by sorry

end MarketplaceLeakage.Communication

Source

Hagiu, Wright, Marketplace Leakage, authors' manuscript dated March 2023 (sha256 cb89c…98a6; published in Management Science, doi:10.1287/mnsc.2023.4757), p. 15, §5.2, display after "Thus, S prefers the first (high-price) option"

Human review

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

View graph