Prove2Me

Appendix, Eq. (25): the manufacturer's profit under a coordinating rebate is Mmβ(ρC−2)/ρCM_m\beta(\rho^C-2)/\rho^C

Proved
FalseFailureReturns.TargetRebate.manuf_profit_at_coord

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

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

Let a>0a > 0, β>0\beta > 0, Mm>0M_m > 0, Rr>0R_r > 0 with (Mm+Rr)β>a(M_m + R_r)\beta > a, and let X(ρ)∼Uniform(0,2β/ρ)X(\rho) \sim \mathrm{Uniform}(0, 2\beta/\rho). Let (u,T)(u, T) with u>0u > 0, T>0T > 0 and T<2β/ρCT < 2\beta/\rho^C coordinate the supply chain. Then the manufacturer's expected profit (7) at the coordinated effort is

πM(ρC∣T,u)=Mm β ρC−2ρC.\pi_M(\rho^C \mid T, u) = M_m\,\beta\,\frac{\rho^C - 2}{\rho^C}.

Comparing this with the no-contract profit πM(ρD)=Mmβ(1−1/ρD)\pi_M(\rho^D) = M_m\beta(1 - 1/\rho^D) gives the manufacturer half of Proposition 2.

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

theorem manuf_profit_at_coord (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) :
    rebateManufProfit P T u (coordEffort P) =
      P.Mm * P.β * ((coordEffort P - 2) / coordEffort P) := by sorry

end FalseFailureReturns.TargetRebate
Source
Ferguson, Guide & Souza, Supply Chain Coordination for False Failure Returns, MSOM 8(4) 2006, p. 392, Appendix, Eq. (25)
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