The online buy trajectory is nondecreasing

Binders. The statement takes two arguments: a natural number $B$ (explicit), and a hypothesis $h_B : 0 < B$. There are no other variables, no implicit arguments, and no typeclass assumptions. In particular the real parameter $c$ of the underlying sequence is not quantified: it is fixed to the single value $c_{\mathrm{opt}}(B)$.

The objects involved. For a natural number $B$ and a real number $c$, the sequence $x^{B,c} : \mathbb{N} \to \mathbb{R}$ is defined by recursion on its index:

where $B$ is coerced from $\mathbb{N}$ into $\mathbb{R}$ in both occurrences, and the branch test is the strict inequality $x^{B,c}_j < 1$ (so the value exactly $1$ takes the second, stationary branch). The real constant is

with $B$ coerced to $\mathbb{R}$ inside the base and used as a natural-number exponent. Both are plain definitions with no side conditions; all divisions are total real division, so a zero denominator yields $0$ rather than being undefined.

What is asserted. For every natural number $B$ with $0 < B$, the function $j \mapsto x^{B,\,c_{\mathrm{opt}}(B)}_j$ is monotone in Mathlib's sense. For a function on $\mathbb{N}$ ordered by the usual $\le$, this unfolds to the universally quantified, non-strict implication

Both index quantifiers are universal, the antecedent is the weak order on naturals, and the conclusion is the weak order on reals. The case $a = b$ is included and holds trivially; the quantifiers range over all natural indices.

What is not asserted. The statement does not claim strict increase, nor strict increase at any particular step; consecutive values may be equal, and the second branch of the recursion makes the sequence stationary once a value $\ge 1$ is reached. It states no upper or lower bound on the values — nothing says they lie in $[0,1]$, nothing says they are nonnegative, nothing says they ever reach or stay below $1$. It states nothing about a limit, convergence, supremum, or eventual behaviour, and nothing about the number of steps needed for any event. There is no finite horizon, index range, or truncation anywhere: the function is defined on all of $\mathbb{N}$ and the claim is about all indices. Nothing is claimed about any other value of the parameter $c$, and nothing about $c_{\mathrm{opt}}(B)$ itself — no sign, no bound, no optimality or extremal property, no relation to any cost, ratio, or algorithm. There is no mention of any cost function, competitive ratio, adversary, primal or dual objective, or feasibility condition.

Degenerate cases. The hypothesis $0 < B$ excludes exactly $B = 0$. Given total division, $B = 0$ is not a meaningless instance but a concrete one: $1/0 = 0$, hence $c_{\mathrm{opt}}(0) = (1+0)^0 - 1 = 0$, hence the increment is $1/0 = 0$, so the recursion for $B = 0$ would read $x_{j+1} = x_j$ on the branch $x_j < 1$ — the constant zero sequence. The hypothesis removes that instance. At $B = 1$ one has $c_{\mathrm{opt}}(1) = 1$ and the recursion is $x_{j+1} = 2x_j + 1$ while $x_j < 1$, starting from $x_0 = 0$; so $x_1 = 1$, and from then on the guard fails and the sequence is constantly $1$ — a case where the asserted inequality holds with equality for all $a, b \ge 1$.