Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Table G.1, OA p. 24 — optimal prices when independent repair costs at least δ

Proved
RightRepair.Equilibrium.table_G1

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

equilibriump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1repair-pricingright-to-repair

Suppose cI≥δc_I\ge\deltacI​≥δ and the standing assumptions hold. Table G.1 gives three optimal outcomes as production cost ccc rises: no repair for c<c‾c<\underline cc<c​, partial repair for c‾≤c<cˉ\underline c\le c<\bar cc​≤c<cˉ, and full repair for cˉ≤c\bar c\le ccˉ≤c. The new and used prices and repair probabilities in each case are exactly the Table G.1 formulas, and each outcome attains at least the profit of every admissible competing equilibrium.

In the partial-repair interval, pn=(c+1+δ(1−f))/2p_n=(c+1+\delta(1-f))/2pn​=(c+1+δ(1−f))/2, pr=pu=(δ+cM)/2p_r=p_u=(\delta+c_M)/2pr​=pu​=(δ+cM​)/2, and α=α^(pn,pr)\alpha=\hat\alpha(p_n,p_r)α=α^(pn​,pr​). Its repair probability is strictly between zero and one when c‾<c<cˉ\underline c<c<\bar cc​<c<cˉ.

Formalization Note At the printed left endpoint c=c‾c=\underline cc=c​, α^=0\hat\alpha=0α^=0, so the strict claim in Table G.1 is made only in the open interval. The statement still asserts optimality at that endpoint. Assumption 1 excludes the table's cM≥δc_M\ge\deltacM​≥δ row. The nonnegative unit-cost pins, the zero-price excess-supply equilibrium corner, and the none encoding of pr=∞p_r=\inftypr​=∞ are part of the shared model.

Preamble
import Mathlib
import Definitions.Def_RightRepair_Equilibrium_Setting
Formal statement
namespace RightRepair.Equilibrium

theorem table_G1 (P : Params) (hP : Standing P)
    (hI : P.δ ≤ P.cI) :
    (P.c < cLow P →
      OptimalOutcome P (pnNo P) none (puNo P) 0) ∧
    (cLow P ≤ P.c → P.c < cBar P →
      OptimalOutcome P (pnNo P) (some ((P.δ + P.cM) / 2))
        ((P.δ + P.cM) / 2)
        (alphaHat P (pnNo P) ((P.δ + P.cM) / 2))) ∧
    (cLow P < P.c → P.c < cBar P →
      0 < alphaHat P (pnNo P) ((P.δ + P.cM) / 2) ∧
      alphaHat P (pnNo P) ((P.δ + P.cM) / 2) < 1) ∧
    (cBar P ≤ P.c →
      OptimalOutcome P (pnFull P) (some 0) (puFull P) 1) := by sorry

end RightRepair.Equilibrium
Source
Jin, Yang & Zhu, Right to Repair: Pricing, Welfare, and Environmental Implications, authors' manuscript of Management Science (2022), doi:10.1287/mnsc.2022.4401 (PDF sha256 b869b33a…1763), OA p. 24, Table G.1 (PDF 57)
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me