Proposition 2 — a coordinating target rebate helps the retailer, and the manufacturer iff
ProvedFalseFailureReturns.TargetRebate.target_rebate_paretoConsider one manufacturer and one retailer. Let be the marginal effort cost, the expected number of false failures at the minimum effort level, and , the manufacturer's and the retailer's profits of avoiding one false failure return, in the interesting case . Suppose that at effort the number of false failures is . Write
for the coordinated and the decentralized effort.
Let be a target rebate contract (the retailer receives for every false failure below the target ) with , and , which coordinates the supply chain: maximizes the retailer's expected profit of Eq. (6) over efforts . Then
- the contract makes the retailer better off:
- the contract makes the manufacturer better off if and only if the coordinated effort is at least twice the decentralized effort:
Here and are the no-contract profits (3) and (5), and 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 ; the condition equivalent to , which the proof uses, is , and that is the hypothesis here. The side condition is the paper's §3.1 requirement at the coordinated effort. The expectation in (6)–(7) is the true uniform expectation for every effort.
import Mathlib import Definitions.Def_FalseFailureReturns_TargetRebate_Model import Definitions.Def_FalseFailureReturns_TargetRebate_UniformRebate
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.