Proposition 1 — finite-horizon latency ratio (goal theorem)

Read-back — SpecActions.prop1_finite_horizon.

The declaration is a universally quantified statement about a natural number $T$ and three real numbers $\alpha$, $\beta$, $p_k$, under the five hypotheses

$$1 \le T,\qquad \alpha > 0,\qquad \beta > 0,\qquad 0 \le p_k,\qquad p_k \le 1 .$$

No other assumption is imposed: in particular no ordering between $\alpha$ and $\beta$ is required, $p_k$ is allowed to be exactly $0$ or exactly $1$, and $T$ may be arbitrarily large. All five hypotheses are simultaneously satisfiable (e.g. $T = 1$, $\alpha = \beta = 1$, $p_k = 0$), so the statement is not vacuous.

Two quantities from the imported bundle occur in the claim, and both must be unfolded. First,

$$\mathrm{seqTime}(T,\beta) \;=\; \frac{T}{\beta},$$

with the natural number $T$ cast to a real. Second,

$$\mathrm{specTime}(T,\alpha,\beta,p_k) \;=\; \frac{T}{\beta} \;-\; S_{\,T-1}(p_k)\cdot\frac{\alpha}{\beta\,(\alpha+\beta)},$$

where $S_n(p)$ is the recursively defined sequence of the bundle (not the separately supplied closed-form expression hitsClosed), given by

$$S_0(p) = 0,\qquad S_1(p) = p,\qquad S_{n+2}(p) = p\bigl(1 + S_n(p)\bigr) + (1-p)\,S_{n+1}(p).$$

The index $T-1$ is truncated subtraction on natural numbers; under the hypothesis $T \ge 1$ it is the ordinary $T-1$ (had $T = 0$ been allowed it would evaluate to $S_0 = 0$).

The assertion is the exact equality of the ratio $\mathrm{specTime}/\mathrm{seqTime}$ with an explicit closed-form expression:

$$\frac{\dfrac{T}{\beta} - S_{\,T-1}(p_k)\cdot\dfrac{\alpha}{\beta(\alpha+\beta)}}{\dfrac{T}{\beta}} \;=\; 1 \;-\; \frac{1}{T}\cdot\frac{\alpha}{\alpha+\beta}\left[\,(T-1)\,\frac{p_k}{1+p_k} \;+\; \frac{p_k^{2}}{(1+p_k)^{2}} \;-\; \frac{p_k^{2}}{(1+p_k)^{2}}\,(-p_k)^{\,T-1}\,\right].$$

Two occurrences of "$T-1$" on the right-hand side are of different kinds: the factor $(T-1)$ multiplying $p_k/(1+p_k)$ is real subtraction applied to the cast of $T$, whereas the exponent in $(-p_k)^{T-1}$ is a natural-number exponent formed by truncated subtraction. Under $T \ge 1$ the two agree numerically. The power $(-p_k)^{T-1}$ is a natural power of a non-positive real, so it alternates in sign with the parity of $T-1$.

On well-definedness and degenerate cases: because $T \ge 1$ and $\beta > 0$, the divisor $\mathrm{seqTime}(T,\beta) = T/\beta$ is strictly positive, so the quotient on the left is an honest division and not a division by zero; likewise $1/T$ is well defined and $1 + p_k \ge 1 > 0$, so neither $p_k/(1+p_k)$ nor $p_k^{2}/(1+p_k)^{2}$ can degenerate. In the boundary case $T = 1$ the left-hand side is $1$ (since $S_0(p_k) = 0$) and the bracket on the right is $0 \cdot \frac{p_k}{1+p_k} + \frac{p_k^{2}}{(1+p_k)^{2}} - \frac{p_k^{2}}{(1+p_k)^{2}}\cdot(-p_k)^{0} = 0$, so both sides equal $1$. In the case $p_k = 0$ the recursion gives $S_n(0) = 0$ for every $n$ and the bracket vanishes, again making both sides equal to $1$. Since $\alpha > 0$ and $\beta > 0$ force $\alpha/(\alpha+\beta) \ne 0$, and $T \ne 0$, the asserted identity is equivalent to the plain statement that

$$S_{\,T-1}(p_k) \;=\; (T-1)\,\frac{p_k}{1+p_k} + \frac{p_k^{2}}{(1+p_k)^{2}}\bigl(1 - (-p_k)^{\,T-1}\bigr),$$

i.e. the equality of the recursively defined sequence with that explicit formula at index $T-1$; the parameters $\alpha$ and $\beta$ cancel entirely from the content of the claim and enter only through the requirement that they be positive.

The declaration carries no proof (its body is left as an unproved placeholder).