Finite ε-horizon from a geometric all-contested bound

Given any sequence $\mathrm{allContested}$ of all-contested-round probabilities bounded geometrically, $\mathrm{allContested}\, K \leq b^K$ with $0 \leq b < 1$, for every $\varepsilon > 0$ there is a round count $K$ with $\mathrm{allContested}\, K < \varepsilon$. This is the finite form of probabilistic liveness: it turns a geometric bound into an explicit $\varepsilon$-horizon without claiming a deterministic bound, and it does not itself prove the geometric bound.