Corollary of Theorem 2.3 — $\lim_k R^\alpha_{FF}(k)=\lim_k R^\alpha_{BF}(k)=1+\lfloor\alpha^{-1}\rfloor^{-1}$

Proved

BinPacking.BoundedItems.ratio_limit_eq

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

approximation-algorithmsasymptotic-ratiobin-packingp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For a real $\alpha$ with $0<\alpha\le\tfrac12$ , let $R^\alpha_{FF}(k)$ and $R^\alpha_{BF}(k)$ be the largest values of $FF(L)/L^*$ and $BF(L)/L^*$ over all lists $L$ with every element in $(0,\alpha]$ and optimum $L^*=k$ . Then

\lim_{k\to\infty}R^\alpha_{FF}(k)\;=\;\lim_{k\to\infty}R^\alpha_{BF}(k)\;=\;1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.

For example, if no item exceeds $\tfrac12$ both algorithms are asymptotically within a factor $\tfrac32$ of optimal, and within $\tfrac43$ if no item exceeds $\tfrac13$ . The bound interpolates between the unrestricted ratio $\tfrac{17}{10}$ (Section 2 of the paper) and $1$ as the largest item size tends to $0$ .

Formalization Note The ratios are suprema in $[0,\infty]$ (ℝ≥0∞), so the statement asserts in particular that they are finite for all large $k$ . $\lfloor\alpha^{-1}\rfloor$ is Nat.floor α⁻¹, cast to ℝ≥0∞ before inverting; it is at least $2$ under the hypotheses.

Preamble

import Mathlib
import Definitions.Def_BinPacking_BoundedItems_Model

Formal statement

namespace BinPacking.BoundedItems

open Filter Topology
open scoped ENNReal

/-- Corollary of Theorem 2.3 (Johnson et al. 1974, p. 308): for any positive `α ≤ 1/2`,
`lim_{k→∞} R^α_FF(k) = lim_{k→∞} R^α_BF(k) = 1 + ⌊α⁻¹⌋⁻¹`. -/
theorem ratio_limit_eq (α : ℝ) (hα : 0 < α) (hα2 : α ≤ 1 / 2) :
    Tendsto (ratioFF α) atTop (𝓝 (1 + ((⌊α⁻¹⌋₊ : ℕ) : ℝ≥0∞)⁻¹)) ∧
      Tendsto (ratioBF α) atTop (𝓝 (1 + ((⌊α⁻¹⌋₊ : ℕ) : ℝ≥0∞)⁻¹)) := by sorry

end BinPacking.BoundedItems

Source

Johnson, Demers, Ullman, Garey, Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3(4) (1974), p. 308, Corollary of Theorem 2.3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The statement has one real-number parameter, $\alpha$ , and two hypotheses:

0 < \alpha \le \tfrac{1}{2}.

From these, set

m \;=\; \big\lfloor \alpha^{-1} \big\rfloor \in \mathbb{N},

the largest natural number not exceeding $1/\alpha$ . Read $m$ in the extended non-negative reals $[0,\infty]$ , and let

L \;=\; 1 + \frac{1}{m} \in [0,\infty],

where the reciprocal and the sum are also taken in $[0,\infty]$ .

The statement uses two objects, $R^{\alpha}_{\mathrm{FF}}$ (written ratioFF α) and $R^{\alpha}_{\mathrm{BF}}$ (written ratioBF α). Both are defined in the imported file Definitions.Def_BinPacking_BoundedItems_Model, which is not shown here. So this read-back cannot say what they compute. Their names suggest worst-case performance ratios of the First Fit and Best Fit bin-packing rules for items bounded by $\alpha$ . That meaning comes from the names only, not from any definition I have seen.

The statement also fixes their types. Each is a function into $[0,\infty]$ , defined on some ordered index type that is not shown. That type has an "eventually, as the argument grows without bound" filter. Call its argument $k$ .

The theorem asserts that both of the following hold:

$R^{\alpha}_{\mathrm{FF}}(k) \to L$ as $k \to \infty$ .
$R^{\alpha}_{\mathrm{BF}}(k) \to L$ as $k \to \infty$ .

Convergence is in the usual order topology of $[0,\infty]$ . Because $L$ is finite (see below), convergence to $L$ has two parts:

for all sufficiently large $k$ , both functions take finite values;
those finite values converge to $L$ in the ordinary real sense.

There are no other hypotheses. In particular, nothing constrains the internal parameters of the imported definitions beyond what those definitions themselves contain.

Degenerate and edge cases.

The hypotheses can be satisfied, for example by $\alpha = \tfrac{1}{2}$ , so the statement is not vacuous.

Because $\alpha \le \tfrac12$ , we have $1/\alpha \ge 2$ , so $m \ge 2$ . The case $m = 0$ never arises, so the reciprocal in $[0,\infty]$ is never the junk value $1/0 = \infty$ .

The limit $L$ therefore always lies in $\left(1, \tfrac32\right]$ :

$L = \tfrac32$ for every $\alpha \in \left(\tfrac13, \tfrac12\right]$ ;
in general, $L = 1 + \tfrac1m$ for every $\alpha \in \left(\tfrac{1}{m+1}, \tfrac1m\right]$ , so it is constant on each such interval.

At $\alpha = 1/m$ exactly, the floor gives $m$ itself, not $m-1$ . As $\alpha \to 0^+$ , $m$ grows without bound and $L$ approaches $1$ , but $L$ never equals $1$ .

The statement says nothing about finitely many initial values of $R^{\alpha}_{\mathrm{FF}}$ and $R^{\alpha}_{\mathrm{BF}}$ ; those values may even equal $\infty$ .

This read-back cannot cover any degenerate behaviour inside the two ratio functions, such as:

junk values from division by zero in their definitions;
suprema over empty or unbounded sets;
how they treat an empty list of items or $k = 0$ .

Those all live in the unshown definitions file.

Human review

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

View graph

Corollary of Theorem 2.3 — lim⁡kRFFα(k)=lim⁡kRBFα(k)=1+⌊α−1⌋−1\lim_k R^\alpha_{FF}(k)=\lim_k R^\alpha_{BF}(k)=1+\lfloor\alpha^{-1}\rfloor^{-1}limk​RFFα​(k)=limk​RBFα​(k)=1+⌊α−1⌋−1

Corollary of Theorem 2.3 — $\lim_k R^\alpha_{FF}(k)=\lim_k R^\alpha_{BF}(k)=1+\lfloor\alpha^{-1}\rfloor^{-1}$