§3, p. 382: in the interesting case,
ProvedFalseFailureReturns.TargetRebate.coord_effort_gt_onep2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chain
Let , , and be as in the model. Suppose the total potential saving of avoiding false failures exceeds the marginal cost of the minimum effort level,
Then the coordinated effort exceeds the minimum effort level:
This is the "interesting case" of the paper, in which the coordinated supply chain exerts more than the minimum effort; every later result about coordinating contracts is stated in it.
Formalization Note The paper writes the condition as . That condition does not imply when ; the condition the conclusion rests on is , which is used here.
Preamble
import Mathlib import Definitions.Def_FalseFailureReturns_TargetRebate_Model
Formal statement
namespace FalseFailureReturns.TargetRebate
theorem coord_effort_gt_one (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.β) :
1 < 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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.