Prove2Me

Proof of Proposition 5, p. 33 — for β < 1, q₂(c) < q̂(c) = β/c < q₁(c)

Proved
NewsBundling.Negotiated.prop5_preamble

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

content-bundlingnash-bargainingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Assume 13<β≤1\tfrac13<\beta\le1, c>2βc>2\beta and 0<Λ<120<\Lambda<\tfrac12. If β<1\beta<1, then

q2(c)=β(2−Λ)−Λ2(1−Λ)c<q^(c)=βc<q1(c)=1+β2c.q_2(c)=\frac{\beta(2-\Lambda)-\Lambda}{2(1-\Lambda)c}<\hat q(c)=\frac{\beta}{c}<q_1(c)=\frac{1+\beta}{2c}.

The benchmark quality therefore lies strictly between the two interior qualities of Lemma 5.

Formalization Note At β=1\beta=1 all three quantities equal 1/c1/c, so the page's strict inequalities need β<1\beta<1, which is added as a hypothesis.

Preamble
import Mathlib
import Definitions.Def_NewsBundling_Negotiated_Setting
Formal statement
namespace NewsBundling.Negotiated

theorem prop5_preamble (β c Λ : ℝ) (hN : NegAssumptions β c Λ) :
    β < 1 → q2 β c Λ < β / c ∧ β / c < q1 β c := by sorry

end NewsBundling.Negotiated
Source
de Cornière & Sarvary, Social Media and News: Content Bundling and News Quality, TSE Working Paper n° 1152 (August 2021), App. A, proof of Proposition 5, p. 33, first sentence
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