The fractional solution is primal feasible

Proved

PrimalDualOnline.SkiRental.alg_primal_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 solution the fractional algorithm holds after $k$ days — the buy level $x_k$ together with the rent variables $z_0, \dots, z_{k-1}$ of source days $1, \dots, k$ — is feasible for the canonical fractional primal program:

0 \le x_k \le 1, \qquad 0 \le z_j \le 1 \ \ (0 \le j < k), \qquad x_k + z_j \ge 1 \ \ (0 \le j < k).

Note which buy level appears in the covering constraints: the final one, $x_k$ , and not the value $x_j$ current on day $j+1$ . That is the correct reading of feasibility for an online algorithm whose primal variables only increase — the solution that must be feasible is the one the algorithm ends with, and an early day's constraint is satisfied a fortiori by the larger final value.

Source correspondence.

What the thesis states (p. 18): the primal half of claim (i), justified in one line — "since we set $z_j = 1 - x$ whenever $x < 1$ , the primal solution produced is feasible."
What this Lean theorem states: the three-part box-feasibility predicate, at every horizon $k$ .
Introduced by the formalization: two things. First, the upper bounds $x_k \le 1$ and $z_j \le 1$ are part of the claim, because the canonical program of this mission is the $[0,1]$ relaxation of the source's prose; the source's one-line justification addresses only the covering constraint. Second, because the statement is asserted at every $k$ and the recursion freezes the trajectory at the first value reaching $1$ , the conjunct $x_k \le 1$ taken over all $k$ has the effect of asserting that the frozen value is exactly $1$ — that is, that the last update does not overshoot. That no-overshoot consequence is genuine content of this formalization and is not something the source states.

Formalization Note. For $0 < k < B$ the bound $x_k \le 1$ holds strictly; at $k = B$ it holds with equality. The statement asserts nothing about monotonicity of the trajectory, nothing about the closed form, and nothing of the form $x_j + z_j \ge 1$ at a common index.

Preamble

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

open PrimalDualOnline.SkiRental

Formal statement

theorem PrimalDualOnline.SkiRental.alg_primal_feasible
    (B : ℕ) (hB : 0 < B) (k : ℕ) :
    PrimalFeasibleBox k (algX B (cOpt B) k)
      (fun j : Fin k => algZ 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, pp. 18-19 (PDF pp. 34-35): the primal half of claim (i) ("since we set z_j = 1 - x whenever x < 1, the primal solution produced is feasible"). Feasible region as relaxed on p. 17.

Read-back

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

Setting and notation. Two natural numbers are quantified over: a parameter $B$ , subject to the single hypothesis $B > 0$ , and an index $k$ , subject to no hypothesis at all. Write $c_B = \left(1 + \frac{1}{B}\right)^{B} - 1$ , where $B$ is cast to a real number (the hypothesis $B > 0$ is what makes $1/B$ an ordinary reciprocal rather than the value total division returns at $0$ ; for every $B \ge 1$ this gives $c_B \ge 1 > 0$ ).

With $c = c_B$ fixed, define a real sequence by

X_0 = 0, \qquad X_{j+1} = \begin{cases} X_j\left(1 + \dfrac{1}{B}\right) + \dfrac{1}{c_B\, B}, & \text{if } X_j < 1,\\[2mm] X_j, & \text{if } X_j \ge 1,\end{cases}

so the sequence grows by a geometric factor plus a fixed additive increment for as long as it is strictly below $1$ , and is frozen forever at its value from the first index onward at which that value is $\ge 1$ . Define a second sequence by $Z_j = 1 - X_j$ if $X_j < 1$ , and $Z_j = 0$ if $X_j \ge 1$ . Both are total functions on $\mathbb{N}$ ; the same $B$ and $c_B$ are used in both.

What the theorem asserts. For every $B > 0$ and every $k$ , the following five statements all hold. The first two concern the single real number $X_k$ ; the last three are universally quantified over the $k$ indices $j \in \{0, \dots, k-1\}$ :

$0 \le X_k$ ;
$X_k \le 1$ ;
$0 \le Z_j$ for every $j < k$ ;
$Z_j \le 1$ for every $j < k$ ;
$1 \le X_k + Z_j$ for every $j < k$ .

All five are conjoined; none is a hypothesis, and there is no implication in the conclusion. All inequalities are non-strict; the only strict comparison in the development is the internal test $X_j < 1$ inside the definitions.

The index mismatch. The scalar argument is $X$ evaluated at index $k$ , whereas the family argument supplies $Z$ at indices $0, \dots, k-1$ — index $k$ is never used for $Z$ , and indices $0,\dots,k-1$ are never used for $X$ . Consequently conjunct 5 does not assert $1 \le X_j + Z_j$ for matching indices. It asserts that the single value $X_k$ , together with each earlier $Z_j$ , sums to at least $1$ . Unfolding $Z$ : for every $j < k$ , if $X_j < 1$ then $X_j \le X_k$ ; and if $X_j \ge 1$ then $X_k \ge 1$ . So for each fixed $k$ the covering conjunct compares $X_k$ against all strictly earlier terms, not a per-index pairing. Because $k$ is universally quantified, the family of instances collectively yields $1 \le X_k + Z_j$ for all pairs $j < k$ ; the instance at $k+1$ pairs $Z_k$ with $X_{k+1}$ , but no instance ever pairs $Z_k$ with $X_k$ .

Degenerate cases.

$k = 0$ . The index type is empty, so conjuncts 3, 4, 5 are vacuously true. The entire content collapses to $0 \le X_0 \le 1$ , and $X_0 = 0$ , so this instance asserts $0 \le 0 \le 1$ and nothing else.
$k = 1$ . The only index is $j = 0$ , with $Z_0 = 1$ . Conjuncts 3 and 4 read $0 \le 1 \le 1$ ; conjunct 5 reads $1 \le X_1 + 1$ , i.e. $X_1 \ge 0$ , where $X_1 = 1/(c_B B)$ .
$B = 1$ . $c_1 = 1$ , the update is $X_{j+1} = 2X_j + 1$ , and $X_1 = 1$ ; the sequence is frozen at $1$ from index $1$ , with $Z_0 = 1$ and $Z_j = 0$ for $j \ge 1$ .
$k = B$ . The statement singles out no index; $k$ and $B$ are independent, and nothing in the conclusion changes form at $k = B$ . $B$ enters only through the recursion coefficients and $c_B$ .
$k$ much larger than $B$ . Since the recursion freezes $X$ at the first value $\ge 1$ , the sequence is eventually constant. Conjunct 2 is asserted at every $k$ , including all $k$ past that freezing point; combined with the freeze, asserting $X_k \le 1$ for all $k$ pins the frozen value to be exactly $1$ — i.e. the assertion covers the case of the recursion overshooting $1$ rather than excluding it by hypothesis.
$B = 0$ is excluded by the hypothesis, and nothing is asserted there.

What is not asserted. Nothing about any cost, objective value, competitive ratio, or performance guarantee; nothing about $c_B$ being optimal or extremal; nothing about any dual object, duality relation, or linear program; nothing about any online input sequence, request, or adversary. It does not assert monotonicity of $X$ , that $X_k$ reaches $1$ at any particular index (in particular nothing about $X_B$ ), that $X_k < 1$ for $k < B$ , or any closed form. It makes no claim about $Z_j$ or $X_j$ for indices $j \ge k$ within a given instance, and no claim of the form $1 \le X_j + Z_j$ at a common index. It gives no bounds on the increment, no telescoping identity, and no relation between $X$ and $Z$ beyond the five inequalities. It says nothing for $B = 0$ .

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