The exact worst-case ratio of iterative rounding for the two-size Gasoline problem

We prove the positive-integer two-size conjecture stated by Lucas Lorieau (2024, Conjecture 3.1.1), and determine the exact worst-case approximation ratio under original-index tie breaking.

For deliveries in {1, K}, positive integer demands of equal total, and position-first iterative rounding with exact assignment-LP scores, we show

For every integer K ≥ 3, an explicit instance with 2K − 3 days attains L_init = OPT = K and C_IR = 2K − 2. Consequently the exact worst-case ratio is 2 − 2/K; its supremum over K is 2. The algorithm is optimal for K = 2. The upper bound permits every exact tie choice. The lower family is realized by the original-index rule.

Method and verification

Subtracting one from every delivery and demand reduces the model to supplies 0 and K − 1. We derive an exact formula for the remaining fractional LP. Its two integral choices cannot both cross the additive bound. A parameterized construction attains the bound.

The Lean proof covers the fractional assignment reduction, real-valued reachability, the integer rounding invariant, arbitrary integral comparison schedules, and the entire sharpness family. The executable scripts reproduce examples using an independent cycle-path LP oracle. Detailed audit status and pinned tools accompany the source package.

Practical contribution

The proof also yields an O(n)-arithmetic implementation of the same decisions without repeated LP solves. In replenishment or buffer scheduling systems that match the model, the theorem bounds the extra capacity required by this heuristic. The interactive laboratory shows the effect of tie handling; success of another tie rule on this family is not a universal guarantee.

Sources and scope

The target statement appears on printed page 21 of Lorieau’s thesis. The broader one-dimensional guarantee is described as unresolved in section 2.2.4 of Nikoleit et al. (2026). Our result covers the full two-size positive-integer Conjecture 3.1.1; the broader unrestricted conjecture remains open to this work. We found no verified earlier resolution in the searches performed; priority has not been established.

LP correspondence update

The new run_iff_algorithm1 theorem connects the complete LP-based execution to the score-based proof. All 11 current modules pass Lean; 24 target axiom lists contain only standard axioms. The new bridge is not covered by the historical Nanoda export. The model correspondence explicitly records the source’s conflicting row/column notation and our doubly stochastic interpretation.

AI contribution

OpenAI Codex (GPT-6 Astra) assisted with the literature search, experiments, proof development, Lean formalization, verification tooling and interactive explanation. MathIsEvenEasier directed the work and reviewed the publication materials.

Research inspired by @xamualexander, Dr. Samuel Allen Alexander. Still there.

Source: MathIsEvenEasier/gasoline-two-sizes. VibeMathed lists this result as Candidate / Lean-checked. Independent review of the new bridge is pending.