Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 2 — a coordinating target rebate helps the retailer, and the manufacturer iff ρC≥2ρD\rho^C \ge 2\rho^DρC≥2ρD

Proved
FalseFailureReturns.TargetRebate.target_rebate_pareto

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

contractsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1principal-agentsupply-chain

Consider one manufacturer and one retailer. Let a>0a > 0a>0 be the marginal effort cost, β>0\beta > 0β>0 the expected number of false failures at the minimum effort level, and Mm=m+δm(w−c)>0M_m = m + \delta_m(w - c) > 0Mm​=m+δm​(w−c)>0, Rr=r+δr(p−w)>0R_r = r + \delta_r(p - w) > 0Rr​=r+δr​(p−w)>0 the manufacturer's and the retailer's profits of avoiding one false failure return, in the interesting case (Mm+Rr)β>a(M_m + R_r)\beta > a(Mm​+Rr​)β>a. Suppose that at effort ρ\rhoρ the number of false failures is X(ρ)∼Uniform(0,2β/ρ)X(\rho) \sim \mathrm{Uniform}(0, 2\beta/\rho)X(ρ)∼Uniform(0,2β/ρ). Write

ρC=[Mm+Rra β]1/3,ρD=max⁡{(Rrβa)1/3, 1}\rho^C = \Big[\frac{M_m + R_r}{a}\,\beta\Big]^{1/3}, \qquad \rho^D = \max\Big\{\Big(\frac{R_r\beta}{a}\Big)^{1/3},\,1\Big\}ρC=[aMm​+Rr​​β]1/3,ρD=max{(aRr​β​)1/3,1}

for the coordinated and the decentralized effort.

Let (u,T)(u, T)(u,T) be a target rebate contract (the retailer receives uuu for every false failure below the target TTT) with u>0u > 0u>0, T>0T > 0T>0 and T<2β/ρCT < 2\beta/\rho^CT<2β/ρC, which coordinates the supply chain: ρC\rho^CρC maximizes the retailer's expected profit πR(ρ∣T,u)\pi_R(\rho \mid T, u)πR​(ρ∣T,u) of Eq. (6) over efforts ρ≥1\rho \ge 1ρ≥1. Then

  1. the contract makes the retailer better off:
πR(ρC∣T,u)≥πR(ρD);\pi_R(\rho^C \mid T, u) \ge \pi_R(\rho^D);πR​(ρC∣T,u)≥πR​(ρD);
  1. the contract makes the manufacturer better off if and only if the coordinated effort is at least twice the decentralized effort:
πM(ρC∣T,u)≥πM(ρD)  ⟺  ρC≥2ρD.\pi_M(\rho^C \mid T, u) \ge \pi_M(\rho^D) \iff \rho^C \ge 2\rho^D.πM​(ρC∣T,u)≥πM​(ρD)⟺ρC≥2ρD.

Here πR(ρD)\pi_R(\rho^D)πR​(ρD) and πM(ρD)\pi_M(\rho^D)πM​(ρD) are the no-contract profits (3) and (5), and πM(ρ∣T,u)\pi_M(\rho \mid T, u)πM​(ρ∣T,u) is the manufacturer's profit (7) under the contract. The result says that a coordinating target rebate is a Pareto improvement over no contract exactly when the retailer's own incentive to exert effort is weak relative to the supply chain's.

Formalization Note The paper's interesting case is printed as (m+r)β>a(m + r)\beta > a(m+r)β>a; the condition equivalent to ρC>1\rho^C > 1ρC>1, which the proof uses, is (Mm+Rr)β>a(M_m + R_r)\beta > a(Mm​+Rr​)β>a, and that is the hypothesis here. The side condition T<2β/ρCT < 2\beta/\rho^CT<2β/ρC is the paper's §3.1 requirement T<2β/ρT < 2\beta/\rhoT<2β/ρ at the coordinated effort. The expectation in (6)–(7) is the true uniform expectation for every effort.

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

theorem target_rebate_pareto (P : Params) (T u : ℝ)
    (ha : 0 < P.a) (hβ : 0 < P.β) (hM : 0 < P.Mm) (hR : 0 < P.Rr)
    (hint : P.a < (P.Mm + P.Rr) * P.β) (hu : 0 < u) (hT : 0 < T)
    (hTlt : T < 2 * P.β / coordEffort P) (hcoord : Coordinates P T u) :
    retailerProfit P (decentrEffort P) ≤ rebateRetailerProfit P T u (coordEffort P) ∧
      (manufProfit P (decentrEffort P) ≤ rebateManufProfit P T u (coordEffort P) ↔
        2 * 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. 383, Proposition 2 (proof: Appendix, pp. 392–393)
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

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