Proposition 4 — Comparison of the two cost bounds

Proved

CappedBaseStock.two_branch

by StellaXin · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximationcapped-base-stockinventorylost-salesoperations-research

Fix an integer $L\ge1$ , put $\rho=L/(L+1)$ and $\kappa_L=1+4L^2/((L+1)(3L-1))$ , and let $\lambda>0$ and $C_h,C_p\ge0$ be arbitrary real numbers. Then

\min\left\{(1+1/\lambda)C_h+(1+\rho)C_p,\ 2C_h+(1+\rho+\lambda\rho)C_p\right\}\le\kappa_L(C_h+C_p).

This purely algebraic statement includes the cases $C_h=0$ and $C_p=0$ . There is no division by their sum and no positivity assumption on either component beyond nonnegativity. All divisions in the coefficients are real division; $L\ge1$ keeps their lead-time denominators positive.

Preamble

import Mathlib

Formal statement

namespace CappedBaseStock


theorem two_branch
    (L : ℕ) (hL : 1 ≤ L)
    (lambda C_h C_p : ℝ)
    (hlambda : 0 < lambda) (hC_h : 0 ≤ C_h) (hC_p : 0 ≤ C_p) :
    min
      ((1 + 1 / lambda) * C_h + (1 + (L : ℝ) / ((L : ℝ) + 1)) * C_p)
      (2 * C_h +
        (1 + (L : ℝ) / ((L : ℝ) + 1) +
          lambda * ((L : ℝ) / ((L : ℝ) + 1))) * C_p) ≤
      (1 + 4 * (L : ℝ) ^ 2 / (((L : ℝ) + 1) * (3 * (L : ℝ) - 1))) *
        (C_h + C_p) := by sorry

end CappedBaseStock

Source

Linwei Xin, Capped Base-Stock Policies: A 2.33-Approximation, author-supplied LaTeX manuscript (756 lines); public paper listing https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538 . Author-supplied source SHA-256: f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a. Proposition 4 (`lem-two-branch`), lines 651–667.

Read-back

What the Lean code literally says, in plain math · GPT-6 (independent Codex sub-agent)

For every natural number $L$ with $1\le L$ , and every three real numbers $\lambda,C_h,C_p$ satisfying $\lambda>0$ , $C_h\ge0$ , and $C_p\ge0$ , the following inequality holds, with every occurrence of $L$ in the displayed arithmetic interpreted as a real number: $\min\!\left\{\left(1+\frac1\lambda\right)C_h+\left(1+\frac{L}{L+1}\right)C_p,\;2C_h+\left(1+\frac{L}{L+1}+\lambda\frac{L}{L+1}\right)C_p\right\}\le\left(1+\frac{4L^2}{(L+1)(3L-1)}\right)(C_h+C_p)$ . The minimum is the smaller of exactly the two displayed real quantities. The hypotheses exclude $L=0$ and $\lambda=0$ ; in particular $L+1>0$ and $3L-1>0$ , so all denominators are nonzero. They include $L=1$ , all positive real values of $\lambda$ , and cases where either or both of $C_h,C_p$ vanish; if both vanish, the asserted inequality is $0\le0$ .

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by StellaXin · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph