Lemma 2(i), p. 11 — c^OR ≥ 0 if and only if α ≤ 1/2 and θ ≤ (1 − 2α)/(2(1 − α))

Proved

YieldPostpone.Pricing.lemma_2_i

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1random-yieldsupply-chainthreshold

For $a, b > 0$ and $\alpha, \theta \in (0,1)$ , the threshold

c^{OR} = \frac ab\,\alpha(1-\theta)\Big((1-\alpha) - \sqrt{\alpha^2 + \tfrac{\theta}{1-\theta}}\Big)

satisfies

c^{OR} \ge 0 \iff 0 < \alpha \le \tfrac12 \ \text{ and } \ 0 < \theta \le \frac{1-2\alpha}{2(1-\alpha)} .

So scenario OR has a low-cost piece, in which the retailer inflates its order, only when yield loss is both severe and likely. This is what makes the (W, L, W) case of Proposition 5(O)(iii) possible.

Preamble

import Mathlib
import Definitions.Def_YieldPostpone_Pricing_Setting

Formal statement

namespace YieldPostpone.Pricing

theorem lemma_2_i (P : Params) (hP : P.Valid) :
    0 ≤ cOR P ↔ P.α ≤ 1 / 2 ∧ P.θ ≤ (1 - 2 * P.α) / (2 * (1 - P.α)) := by sorry

end YieldPostpone.Pricing

Source

Geng, Guo, Xiao, Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, SSRN 3546872 (author version), p. 11, Lemma 2(i); App. B.2, PDF p. 35

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph