The decision at this day
A candidate score is the smallest capacity of a fractional completion after that choice. It is a lower bound on its best integral completion.
A tight bound for iterative rounding
A local choice.
A bigger tank.
Reorder deliveries of size 1 or K to meet a fixed sequence of demands. This LP-based heuristic can use almost twice the minimum capacity. Here is exactly how it happens.
CIR ≤ OPT + K − 2Exact worst-case ratio: 2 − 2/K
Positive integer demands, equal supply and demand totals, and a delivery before each consumption. The upper bound allows every tie choice; sharpness uses original input index.
01 / Explore the example
Same deliveries. Different decisions.
Algorithm capacity8
Optimal capacity5Certified by a matching schedule
Proved upper bound8
Inventory after each event
AlgorithmOptimal schedule
Each delivery raises the level; consumption lowers it. Each trace is shifted so its minimum is zero. Required capacity is its full vertical range.
Why rounding has a cost
Fractional freedom, two actual choices
See deliveries, demands and the returned order
- Input deliveries X
- Fixed demands Y
- Returned deliveries
Try your own input
Use positive integers separated by commas or spaces. Deliveries must be 1 or K, with equal list lengths and equal totals. The laboratory accepts up to 200 entries.
For custom input we show a certified lower bound, not a claimed optimum. Browser arithmetic is exact for the permitted integer range; the general theorem is checked separately in Lean.
02 / Why the guarantee holds
The two choices cannot both be too expensive.
Subtract 1 from every delivery and demand. Deliveries become 0 or h = K − 1; the capacity drops by exactly 1. After any prefix, the next fractional LP score has the shape
f(z) = max(F, u − z, v + z), 0 ≤ z ≤ h.
Let L₀ be the initial normalized LP value and H = L₀ + h − 1. If both integral choices exceeded H, integer scores would force the two conflicting inequalities below.
If both choices failedu + v + h ≥ 2H + 2
Choosing 0 would force u ≥ H + 1; choosing h would force v + h ≥ H + 1.
But the LP structure givesu + v + h ≤ 2H + 1
The current LP is at most H, and every future demand-interval obstruction is at most L₀.
Those inequalities are incompatible. At least one choice stays inside the bound, and the algorithm takes a minimum-score choice. If only one supply size remains, fixing it leaves the LP value unchanged.
Why the examples matter
For every K ≥ 3, a family with 2K − 3 days has OPT = K and algorithm cost 2K − 2. The loss reaches K − 2 exactly. No constant below 2 works uniformly over K for this tie rule.
From the LP to the proved algorithm
Why the score really is the LP value.
Each link below does a different job: simplify the units, preserve the feasible assignments, identify the optimum, preserve the choices, and finally transfer the guarantee.
- Normalize the deliveries and demands. Subtract 1 from each. Deliveries become 0 or h = K − 1, and demands become d = y − 1 ≥ 0. Inventory after consumption stays unchanged; every delivery peak falls by 1. Original capacity is therefore normalized capacity plus 1, so candidate comparisons are preserved.
- Write the residual assignment LP. After fixing a prefix, assign each remaining item to the remaining days using a nonnegative matrix whose rows and columns sum to one. Constrain every inventory peak and trough, including the fixed prefix, and minimize the difference between the upper and lower bounds. This defines the optimization problem independently of our score formula.
- Replace the matrix with delivery fractions, in both directions. Let pj be the total weight of large items assigned to day j. Then 0 ≤ pj ≤ 1, the fractions sum to the number m of remaining large items, and that day’s original delivery is 1 + hpj. Conversely, any such fractions can be spread across the large and small rows to construct an assignment matrix. Thus this simplification neither loses nor invents feasible delivery vectors.
- Characterize which inventory bounds are feasible. A normalized delivery z lies between 0 and h. From current inventory s and next demand d, it must satisfy s + z ≤ b and a ≤ s + z − d; the same conditions then apply to the remaining days. The reachability theorem solves these conditions exactly, including the required total supply and terminal inventory zero.
- Prove that the formula is the optimum. First, every feasible completion has capacity at least the proposed value. Second, construct a feasible completion attaining that value and turn its fractions back into an assignment matrix. Both directions are needed: a lower bound alone would not justify replacing an LP solve. Restoring original units gives LP value = normalized score + 1.
- Compare actual candidate choices. Fixing a small delivery and fixing a large delivery produce two residual LPs. Their exact minima are their respective scores plus the same 1, so the ordering and all ties agree. If one size is exhausted, only the other is available. Identical items of the same size need no separate score comparison.
- Extend the correspondence through the whole execution. After each chosen delivery, update the remaining counts, current inventory and prefix extrema. The validity conditions are preserved, so the candidate argument applies again. Induction gives
run_iff_algorithm1: the LP-based and score-based execution predicates are equivalent. The bound covers every minimum tie choice, including the paper’s first-index rule. - Transfer the bound and its matching examples. The existing rounding invariant now applies to the LP algorithm: capacity ≤ initial LP + K − 2 ≤ OPT + K − 2. When a large item is present, OPT ≥ K gives the ratio 2 − 2/K; with only small items, the delivery sequence is unique and optimal. The extremal family is also an LP-based run, so the upper bound is attained for each K ≥ 3.
Read the bridge theorem ↗ · Read the model correspondence ↗
Why the source LP convention matters
In Figure 1.1 (printed page 4), row and column sums are written as ≤ 1. The discussion before Proposition 3.1.2 (printed page 16) calls the matrices doubly stochastic, meaning that both sums equal 1. Our formalization uses equality, consistently with using every delivery in a permutation.
The difference can change a candidate LP value. Take deliveries 1 and 3, demands 2 and 2, and fix delivery 1 first. If we weaken just the row and column equalities to ≤ 1, without requiring all supply to be used, the remaining delivery of size 3 can be used only to extent 2/3. The delivered amounts then become 1 and 2. With initial stock 1:
| Event | All supply used | Partial use allowed |
|---|---|---|
| Initial stock | 1 | 1 |
| First delivery: +1 | 2 | 2 |
| First consumption: −2 | 0 | 0 |
| Second delivery | +3 → 3 | +2 → 2 |
| Second consumption: −2 | 1 | 0 |
| Required capacity | 3 | 2 |
The smaller value omits one unit of supply and ends below the initial stock. Equal totals in the input do not prevent this: available supply is 4, but this fractional assignment uses only 3. A separate condition requiring all supply to be used would exclude it.
The problem’s permutation definition and the later doubly stochastic description support our interpretation. We regard the displayed inequality as a likely transcription error, but have no confirmation from the author. Lean checks our explicitly stated equality model; it does not determine the author’s intended reading of the inconsistent figure.
03 / What this can help with
A bound you can use before committing capacity.
Inventory and buffers
If a cyclic replenishment or processing schedule matches this model, the theorem bounds the extra storage used by the heuristic: at most K − 2 units over optimum.
Faster scheduling
The exact same LP decisions can be computed in O(n) arithmetic operations. The implementation replaces repeated LP solves with suffix summaries and integer comparisons.
A test for tie handling
Equivalent LP scores can lead to very different final schedules. Switch the tie rule above to see the effect. An improvement on this family does not establish a better universal guarantee.
Here the small-first rule needs capacity 7, while a certified schedule needs only 5. Found in a bounded Azure experiment of 10,000 random trials; no improved universal factor is claimed.
This model permits reordering deliveries, keeps demand order fixed and assumes a freely chosen initial stock. Lead times, reorder costs, losses and several resource types require additional analysis.
04 / Inspect the evidence
Proof, code and independent checks.
The updated Azure build compiled all 11 Lean modules and checked axiom dependencies for 24 targets, including the LP bridge. Only propext, Classical.choice and Quot.sound occur. Lean rejected a deliberately false control. The earlier Nanoda audit checked 9,451 declarations for the original 12 targets; that export does not include the new bridge.
Main Lean statements ↗Mathematical proof ↗Exact algorithm ↗LP bridge audit ↗Original audit ↗Prior-art review ↗Tie-rule experiment ↗Research announcement ↗
Target: Conjecture 3.1.1 in Lucas Lorieau’s 2024 thesis. This resolves the full two-size, positive-integer conjecture stated there, under the assignment convention above. The broader one-dimensional conjecture remains outside this result. A search without a matching result does not establish priority.
Prepared by MathIsEvenEasier with OpenAI Codex (GPT-6 Astra). VibeMathed: Candidate / Lean-checked · independent review of the new bridge pending.