The fractional algorithm's dual solution is feasible

Proved

PrimalDualOnline.SkiRental.alg_dual_feasible

by moutei · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

competitive-analysislinear-programmingonline-algorithmsprimal-dualski-rental

Let $B \ge 1$ be the purchase price and $k \ge 0$ the number of ski days. The dual solution $y_0, \dots, y_{k-1}$ produced by the fractional algorithm is feasible for the dual packing program of Figure 3.1:

0 \le y_j \le 1 \ \ (0 \le j < k), \qquad \sum_{j=0}^{k-1} y_j \;\le\; B .

The box constraints are settled by the shape of the variable, which is $1$ on an active day and $0$ afterwards. The budget constraint is the substantive half. Since each $y_j$ is $0$ or $1$ , the sum counts the days on which the buy variable is still below $1$ , so the claim is a counting bound:

\#\bigl\{\, j < k \;:\; x_j < 1 \,\bigr\} \;\le\; B .

Dual feasibility is what licenses comparing the algorithm against the offline optimum at all: a feasible dual solution has objective value at most that of every feasible primal solution, hence at most the optimum. Without the budget constraint the accumulated dual objective would be an arbitrary number rather than a certified lower bound.

Source correspondence.

What the thesis states (p. 19): "to show feasibility of the dual solution, we need to show $\sum_{j=1}^{k} y_j \le B$ . We prove $x \ge 1$ after at most $B$ days of ski." The dual constraints themselves are those printed in Figure 3.1 (p. 18).
What this Lean theorem states: the two-clause dual-feasibility predicate for the algorithm's dual solution, at every horizon $k$ .
Introduced by the formalization: nothing beyond making the quantification over $k$ explicit.

Formalization Note. For $k \le B$ the budget constraint follows from counting alone, so the content of the statement lies in the regime $k > B$ , where it amounts to the assertion that the buy variable has reached $1$ by day $B$ . Each dual variable consults the trajectory at its own index; the value $x_k$ is never consulted.

Preamble

import Definitions.Def_PrimalDualOnline_SkiRentalLP
import Definitions.Def_PrimalDualOnline_SkiRentalAlg
import Mathlib.Tactic

open PrimalDualOnline.SkiRental

Formal statement

theorem PrimalDualOnline.SkiRental.alg_dual_feasible
    (B : ℕ) (hB : 0 < B) (k : ℕ) :
    DualFeasible (B : ℝ) k (fun j : Fin k => algY B (cOpt B) (j : ℕ)) := by sorry

Source

Niv Buchbinder, "Designing Competitive Online Algorithms via a Primal-Dual Approach", PhD thesis, Tel Aviv University, 2008, https://www.tau.ac.il/~nivb/download/phd-thsis.pdf, Chapter 3, p. 19 (PDF p. 35): the dual half of claim (i) ("to show feasibility of the dual solution, we need to show sum_j y_j <= B. We prove x >= 1 after at most B days of ski"). Dual constraints from Figure 3.1, p. 18.

Read-back

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

The declaration takes three inputs: a natural number $B$ , a proof $h_B$ that $0 < B$ , and a natural number $k$ . There is no hypothesis relating $k$ to $B$ , no hypothesis on the sign or nonvanishing of any other quantity, and no typeclass assumption; the conclusion is asserted for every $B \ge 1$ and every $k \ge 0$ simultaneously.

First, for a real parameter $c$ the trajectory is defined by recursion over all of $\mathbb{N}$ :

x_0 = 0, \qquad x_{j+1} = \begin{cases} x_j\left(1 + \dfrac{1}{B}\right) + \dfrac{1}{cB}, & \text{if } x_j < 1,\\[2mm] x_j, & \text{if } x_j \ge 1.\end{cases}

$B$ appears as a real via the cast; the divisions are total, so $1/B$ would be $0$ if $B$ were $0$ (excluded by $h_B$ ) and $1/(cB)$ would be $0$ if $cB$ were $0$ . The second branch returns $x_j$ unchanged, so once an index has value $\ge 1$ every later index has that same value.

Second, the dual variable at index $j$ is the $0/1$ indicator $y_j = 1$ if $x_j < 1$ and $0$ if $x_j \ge 1$ , i.e. it consults the trajectory at index $j$ itself — not $j+1$ , not $j-1$ . In particular $y_0$ consults $x_0 = 0$ , so $y_0 = 1$ unconditionally; the last dual variable in the statement, $y_{k-1}$ , consults $x_{k-1}$ . The value $x_k$ is never consulted.

Third, the parameter is fixed to $c_{\mathrm{opt}}(B) = \left(1 + \frac{1}{B}\right)^{B} - 1$ . The statement carries no hypothesis and makes no claim about the value, positivity, or optimality of this constant.

The conclusion unfolds to the conjunction of two clauses: (1) for every $j < k$ , $0 \le y_j$ and $y_j \le 1$ , both non-strict; (2) $\sum_{j<k} y_j \le B$ , non-strict, with the budget taken to be the real cast of the same natural $B$ that parameterizes the trajectory.

Clause 1 is a statement about numbers that are already either $0$ or $1$ , so it is settled by the definition alone and involves no property of the trajectory. Clause 2, given $0/1$ summands, is exactly a counting bound: the sum equals the number of indices in $\{0,\dots,k-1\}$ whose trajectory value lies strictly below $1$ , and the claim is that this count is at most $B$ :

\#\bigl\{\, j < k \;:\; x_j < 1 \,\bigr\} \;\le\; B .

Degenerate and boundary cases: $k = 0$ — the index type is empty, clause 1 is vacuous, the sum is $0$ , so clause 2 reads $0 \le B$ , true with no reference to the trajectory. $k \le B$ — the count is at most $k$ by cardinality alone, hence at most $B$ ; these instances hold for any $0/1$ -valued family and say nothing about the recursion. The only instances in which the trajectory matters are $k > B$ . $B = 1$ — $c_{\mathrm{opt}}(1) = 1$ , the recursion reads $x_{j+1} = 2x_j + 1$ while $x_j < 1$ , and the budget is $1$ ; the claim is that at most one index has $x_j < 1$ , for every $k$ . $h_B$ rules out $B = 0$ , where both $1/B$ and the budget would be $0$ .

Not asserted. Nothing about the trajectory values themselves — no bound such as $0 \le x_j$ or $x_j \le 1$ , no monotonicity, no claim about which index first reaches $1$ . No lower bound on the sum, no exactness or tightness of clause 2, no complementary-slackness or binding-constraint claim. No primal object: no primal feasibility, cost, objective value, weak- or strong-duality inequality, and no relation between $\sum_j y_j$ and anything computed from $x$ . No optimality or competitive-ratio property of $c_{\mathrm{opt}}(B)$ , and no claim that it is nonzero. No claim for parameters other than $c_{\mathrm{opt}}(B)$ . Nothing about indices $\ge k$ or any limit over all of $\mathbb{N}$ — only the finite initial segment of length $k$ is constrained. No interpretation of $y$ as the dual of a linear program: "dual feasible" is here nothing more than the two-clause conjunction. No algorithmic, online, or problem-specific property.

Human review

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

View graph