Prove2Me

(18), p. 8872 — the pooling threshold d₁ is strictly below the separating threshold d₂

Proved
FakeAccounts.Platform.d1_lt_d2

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

fake-accountsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1signalingthresholds

Under the standing parameter ranges of the model, the antifake-effort threshold up to which pooling is sustainable lies strictly below the threshold up to which costly separation is sustainable:

d1=(1−τ)(η1−p0)  <  (1−τ)(η2−p0)=d2,d_1=(1-\tau)(\eta_1-p_0)\;<\;(1-\tau)(\eta_2-p_0)=d_2,

with η1=λiμ(1−l)[qH(E[q]−qL)/(lE[q](qH−qL))+ρ]\eta_1=\lambda_i\mu(1-l)\big[q_H(E[q]-q_L)/(lE[q](q_H-q_L))+\rho\big] and η2=1lλiμ(1−l2)\eta_2=\frac1l\lambda_i\mu(1-l^2).

This ordering makes the three regions of Proposition 1 (pooling, costly separating, naturally separating) appear in that order as dd grows.

Preamble
import Mathlib
import Definitions.Def_FakeAccounts_Platform_Setting
Formal statement
namespace FakeAccounts.Platform

/-- (18), p. 8872: the pooling threshold d₁ lies strictly below the separating threshold d₂. -/
theorem d1_lt_d2 (P : Params) (hP : Standing P) : d1 P < d2 P := by sorry

end FakeAccounts.Platform
Source
Huang and Liu, Economics of Social Media Fake Accounts, Management Science 71(10), 2025, p. 8872, (13), (16), (18)
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