Range and monotonicity of the $k$-branch hit probability $p(k)$

Read-back of SpecActions.phit_bounds.

Fix a natural number $k$ (the quantifier ranges over all of $\mathbb{N}$, so $k = 0$ is included) and a real number $p$. Assume the two hypotheses

The quantity named $\mathrm{phit}(k,p)$ is not a standard notion; it is the definition supplied by the imported bundle, namely

where the exponent is a natural-number power (so $(1-p)^0 = 1$ by the usual convention that the empty product is $1$, including in the case $1 - p = 0$, i.e. $0^0 = 1$). No probabilistic interpretation is asserted by the statement; $\mathrm{phit}(k,p)$ is simply this real-valued expression.

Under those hypotheses the theorem asserts the conjunction of the following three claims, all for the same $k$ and $p$:

1. $0 \le 1 - (1-p)^{k}$;
2. $1 - (1-p)^{k} \le 1$;
3. $1 - (1-p)^{k} \;\le\; 1 - (1-p)^{k+1}$, i.e. the single-step comparison between $\mathrm{phit}(k,p)$ and $\mathrm{phit}(k+1,p)$.

All three inequalities are non-strict ($\le$, not $<$), and claim 3 compares only consecutive exponents $k$ and $k+1$; no statement is made about $\mathrm{phit}(j,p) \le \mathrm{phit}(k,p)$ for general $j \le k$, about strict increase, about any limiting value as $k \to \infty$, or about behaviour when $p$ lies outside $[0,1]$.

Degenerate cases that the quantifiers silently include:

• $k = 0$: here $\mathrm{phit}(0,p) = 1 - (1-p)^0 = 1 - 1 = 0$, so claims 1 and 2 read $0 \le 0$ and $0 \le 1$, and claim 3 reduces to $0 \le p$.
• $p = 0$: $\mathrm{phit}(k,0) = 1 - 1^{k} = 0$ for every $k$, so claims 1 and 3 hold with equality.
• $p = 1$: $1 - p = 0$, so $\mathrm{phit}(0,1) = 1 - 0^0 = 0$ while $\mathrm{phit}(k,1) = 1 - 0 = 1$ for every $k \ge 1$; claim 3 is then $0 \le 1$ at $k = 0$ and $1 \le 1$ afterwards.

The hypothesis set is satisfiable (any $p$ in the closed unit interval, e.g. $p = \tfrac12$, together with any $k$), so the statement is not vacuous. Nothing else from the surrounding bundle — the recursion $S$, the runtime and cost expressions, the confidence-aware quantities — enters this statement; it involves only $\mathrm{phit}$, the two order hypotheses on $p$, and the three inequalities above.