§3, p. 382: $\rho^C \ge \rho^D$

Proved

FalseFailureReturns.TargetRebate.decentr_le_coord

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

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

Let $a > 0$ , $\beta > 0$ , $M_m > 0$ , $R_r > 0$ , and assume the interesting case $(M_m + R_r)\beta > a$ . Then the decentralized effort does not exceed the coordinated effort:

\rho^D = \max\Big\{\Big(\frac{R_r\beta}{a}\Big)^{1/3},\,1\Big\} \;\le\; \rho^C = \Big[\frac{M_m + R_r}{a}\,\beta\Big]^{1/3}.

Without a contract the retailer under-invests in effort; the comparison is used in the appendix proof of Proposition 2.

Preamble

import Mathlib
import Definitions.Def_FalseFailureReturns_TargetRebate_Model

Formal statement

namespace FalseFailureReturns.TargetRebate

theorem decentr_le_coord (P : Params)
    (ha : 0 < P.a) (hβ : 0 < P.β) (hM : 0 < P.Mm) (hR : 0 < P.Rr)
    (hint : P.a < (P.Mm + P.Rr) * P.β) :
    decentrEffort P ≤ coordEffort P := by sorry

end FalseFailureReturns.TargetRebate

Source

Ferguson, Guide & Souza, Supply Chain Coordination for False Failure Returns, MSOM 8(4) 2006, p. 382, §3

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

§3, p. 382: ρC≥ρD\rho^C \ge \rho^DρC≥ρD

§3, p. 382: $\rho^C \ge \rho^D$