The 50% latency-reduction ceiling for breadth speculation

Declaration latency_reduction_le_half (namespace SpecActions).

The statement is about three real numbers, all of them explicit arguments: $\alpha$, $\beta$, and a third real number written $p_k$ (the identifier pk, a single real variable, not a function of an index $k$). Four hypotheses are assumed:

• $\alpha > 0$;
• $\beta > 0$;
• $p_k \ge 0$;
• $p_k \le 1$.

There are no other binders, no implicit arguments, no typeclass assumptions beyond the three variables being real numbers, and no quantification over any natural number, index, horizon, or sequence.

Under exactly those four hypotheses, the assertion is the strict inequality

where all operations are the real-number ones and $\tfrac12$ is the real number one-half. The claim is $<$, not $\le$, and it is a one-directional inequality (no equivalence, no matching lower bound, and no claim about when equality or near-equality occurs).

Concerning the degenerate cases the hypotheses permit: since $p_k \ge 0$ we have $1 + p_k \ge 1 > 0$, and since $\alpha, \beta > 0$ we have $\alpha + \beta > 0$, so neither division is by zero and no total-division junk value arises. The endpoints of the allowed range for $p_k$ are included: at $p_k = 0$ the left-hand side is $0$, and at $p_k = 1$ it is $\dfrac{\alpha}{2(\alpha+\beta)}$. Nothing relates $\alpha$ and $\beta$ to each other — the statement covers $\alpha < \beta$, $\alpha = \beta$, and $\alpha > \beta$ alike, and neither is bounded above. The hypotheses are jointly satisfiable (for instance $\alpha = \beta = 1$, $p_k = \tfrac12$), so the claim is not vacuous.

None of the definitions of the imported bundle occur in the statement: there is no reference to $\text{phit}$, to the hit-count recursion $S_n$ or its closed form, to $\text{seqTime}$, $\text{specTime}$, $\text{seqCost}$, $\text{specCost}$, to any of the depth-focused quantities, or to $q(m)$, $\delta q(m)$, and the per-window objective. In particular the statement mentions no step horizon $T$, no latency, no cost, and no algorithm; it is a purely arithmetic inequality among three real parameters.

The declaration is stated with its proof omitted.