Prove2Me

Eqs. (3)–(4): the retailer's no-contract profit is maximized at ρD\rho^D

Proved
FalseFailureReturns.TargetRebate.decentr_effort_maximizes

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chain

Let a>0a > 0, β>0\beta > 0, Mm>0M_m > 0 and Rr>0R_r > 0 be as in the model. Without a contract the retailer's expected profit at effort ρ\rho is

πR(ρ)=−aρ22+Rr β(1−1ρ).\pi_R(\rho) = -\frac{a\rho^2}{2} + R_r\,\beta\Big(1 - \frac{1}{\rho}\Big).

Over the effort domain ρ≥1\rho \ge 1 it is maximized at

ρD=max⁡{(Rrβa)1/3, 1},\rho^D = \max\Big\{\Big(\frac{R_r\beta}{a}\Big)^{1/3},\,1\Big\},

that is, πR(ρ)≤πR(ρD)\pi_R(\rho) \le \pi_R(\rho^D) for every ρ≥1\rho \ge 1.

This identifies ρD\rho^D as the effort the retailer exerts in the absence of an incentive from the manufacturer, the benchmark of the paper's comparisons.

Preamble
import Mathlib
import Definitions.Def_FalseFailureReturns_TargetRebate_Model
Formal statement
namespace FalseFailureReturns.TargetRebate

theorem decentr_effort_maximizes (P : Params)
    (ha : 0 < P.a) (hβ : 0 < P.β) (hM : 0 < P.Mm) (hR : 0 < P.Rr) :
    IsMaxOn (retailerProfit P) (Set.Ici 1) (decentrEffort P) := by sorry

end FalseFailureReturns.TargetRebate
Source
Ferguson, Guide & Souza, Supply Chain Coordination for False Failure Returns, MSOM 8(4) 2006, p. 382, §3, Eqs. (3)–(4)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph