Prove2Me

(G.51), OA p. 42 — separation of two production-cost cutoffs

Proved
RightRepair.Equilibrium.G51_cprime_sub_c2

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

cutoff-comparisonp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1right-to-repair

For the cutoffs c‾′\underline c' and c2c_2 defined on OA p. 40, the paper's identity is

c‾′−c2=(2−f)(cM−(2cI−δ)).\underline c'-c_2=(2-f)\bigl(c_M-(2c_I-\delta)\bigr).

If cI<(δ+cM)/2c_I<(\delta+c_M)/2, this difference is positive. The identity orders the first two cost regimes used in the low independent-repair-cost part of Table 1.

Formalization Note The standing assumptions include the disclosed c,cM≥0c,c_M\ge0 pins; 0<f<10<f<1 and 0<δ<10<\delta<1 ensure the cutoff formulas' denominators are nonzero.

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

theorem G51_cprime_sub_c2 (P : Params) (hP : Standing P) :
    cPrimeLow P - c2 P =
      (2 - P.f) * (P.cM - (2 * P.cI - P.δ)) ∧
    (P.cI < (P.δ + P.cM) / 2 → 0 < cPrimeLow P - c2 P) := 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. 42, (G.51) (PDF 75); definitions OA p. 40 (PDF 73)
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