Proof of Theorem 4.1, p. 17 — if $p_T\le p_S$ , $q_T>q_S$ and $g_S(\omega_S)>g_S(\omega_T)\ge0$ , then $\bar v_T<\bar v_S$

Proved

EngagementOpt.Misalign.thm_4_1_step_v

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

behavioral-economicsengagementp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1recommender-systems

This is the second step of the proof of Theorem 4.1.

Let $W>0$ and let $\omega_S=(p_S,q_S,\bar v_S)$ and $\omega_T=(p_T,q_T,\bar v_T)$ be two points of $\Omega=[0,1)\times[0,1)\times\mathbb R_+$ , with

g_S(\omega)=\frac{\bar v-W}{1-q}-\frac{pW}{1-p}.

Suppose that

$p_T\le p_S$ ;
$q_T>q_S$ ;
$g_S(\omega_S)>g_S(\omega_T)$ ;
$g_S(\omega_T)\ge 0$ .

Then

\bar v_T<\bar v_S.

Together with the first step, this shows that when the engagement maximizer is not more moreish, it has a longer span but a lower value.

Formalization Note Hypothesis 4 is the constraint of (4) satisfied by the engagement maximizer; the printed step marked " $(q_T>q_S)$ " uses it silently (it gives $\bar v_T\ge W$ ), and the statement is false without it. $W>0$ is added: the paper fixes $W=1$ (p. 5).

Preamble

import Mathlib
import Definitions.Def_EngagementOpt_Misalign_Model

Formal statement

namespace EngagementOpt.Misalign

/-- Proof of Theorem 4.1, p. 17: for `ω_S, ω_T ∈ Ω` and `W > 0`, if `p_T ≤ p_S`, `q_T > q_S`,
`g_S(ω_S) > g_S(ω_T)` and `g_S(ω_T) ≥ 0` (the constraint of (4), used implicitly in the step
marked "(q_T > q_S)"), then `v̄_T < v̄_S`. -/
theorem thm_4_1_step_v (W : ℝ) (hW : 0 < W) (ωS ωT : Params) (hS : InOmega ωS)
    (hT : InOmega ωT) (hp : ωT.p ≤ ωS.p) (hq : ωS.q < ωT.q) (hgS : gS W ωT < gS W ωS)
    (hpart : 0 ≤ gS W ωT) :
    ωT.v < ωS.v := by sorry

end EngagementOpt.Misalign

Source

Kleinberg, Mullainathan, Raghavan, The Challenge of Understanding What Users Want, arXiv:2202.11776v3, p. 17, proof of Theorem 4.1 (second display)

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

Proof of Theorem 4.1, p. 17 — if pT≤pSp_T\le p_SpT​≤pS​, qT>qSq_T>q_SqT​>qS​ and gS(ωS)>gS(ωT)≥0g_S(\omega_S)>g_S(\omega_T)\ge0gS​(ωS​)>gS​(ωT​)≥0, then vˉT<vˉS\bar v_T<\bar v_SvˉT​<vˉS​

Proof of Theorem 4.1, p. 17 — if $p_T\le p_S$ , $q_T>q_S$ and $g_S(\omega_S)>g_S(\omega_T)\ge0$ , then $\bar v_T<\bar v_S$