Closed form for the expected hit count $S_n$

Proved

SpecActions.hits_closed_form

by naimengye · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

machine-learningprobabilitytheoretical-computer-science

Let $S_n$ be the expected number of speculation hits by round $n$ . Because a correct guess leaves the next call already cached, that round opens no speculation window, which gives the two-term recursion

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

For every $p\ge 0$ and every $n$ ,

S_n=\frac{p}{1+p}\,n+\frac{p^2}{(1+p)^2}\bigl(1-(-p)^n\bigr).

The characteristic polynomial $r^2-(1-p)r-p$ has roots $1$ and $-p$ ; since $r=1$ is a root, a constant particular solution collides with the homogeneous family and the particular solution is linear in $n$ .

Preamble

import Definitions.Def_SpecActions_model

Formal statement

import Definitions.Def_SpecActions_model

namespace SpecActions
theorem hits_closed_form (p : ℝ) (hp : 0 ≤ p) (n : ℕ) :
    hits p n = p / (1 + p) * n + p ^ 2 / (1 + p) ^ 2 * (1 - (-p) ^ n) := by sorry
end SpecActions

Source

Ye, Ahuja, Liargkovas, Lu, Kaffes, Peng, "Speculative Actions: A Lossless Framework for Faster Agentic Systems", ICLR 2026, arXiv:2510.04371, https://arxiv.org/abs/2510.04371, Appendix A (pp. 13–14), the recursion

S_n=p(k)(1+S_{n-2})+(1-p(k))S_{n-1}

and its closed-form solution

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back — SpecActions.hits_closed_form

The declaration is an equational claim about one real-valued sequence. Fix a real number $p$ subject to the single hypothesis $0 \le p$ (no upper bound is imposed: $p$ may be $0$ , may equal $1$ , and may be arbitrarily large; nothing in the statement asserts that $p$ is a probability), and fix an arbitrary natural number $n$ (the quantifier includes $n = 0$ ).

The symbol $S_p(n)$ — written hits p n in the code under audit — is not a standard notion; it is the sequence introduced in the imported bundle by the two-step recursion

S_p(0) = 0, \qquad S_p(1) = p, \qquad S_p(n+2) \;=\; p\bigl(1 + S_p(n)\bigr) \;+\; (1 - p)\,S_p(n+1),

i.e. each term two steps ahead is a fixed real combination of the two preceding terms, with the coefficients $p$ and $1-p$ taken as literal real numbers built from the same $p$ (they are not assumed to lie in $[0,1]$ or to sum to a probability weighting beyond the algebraic fact that they sum to $1$ ). The recursion is total: it defines a real number for every natural $n$ and every real $p$ , whatever the sign or size of $p$ .

For every such $p$ and $n$ , the theorem asserts the exact real-number identity

S_p(n) \;=\; \frac{p}{1+p}\cdot n \;+\; \frac{p^{2}}{(1+p)^{2}}\Bigl(1 - (-p)^{n}\Bigr).

Points of literal reading:

The two coefficients are written exactly as displayed: a first-power quotient $\dfrac{p}{1+p}$ multiplying $n$ , and a quotient of squares $\dfrac{p^{2}}{(1+p)^{2}}$ multiplying the bracket. The factor $n$ is the natural number $n$ regarded as a real number, and $(-p)^{n}$ is the $n$ -th natural-number power of the negated quantity $-p$ (so it alternates in sign with the parity of $n$ when $p > 0$ ).
The claim is an exact equality of real numbers for each individual $n$ , not an approximation, a bound, an asymptotic statement, or a limit.
Because $0 \le p$ forces $1 + p \ge 1 > 0$ , both denominators are nonzero under the hypothesis, so no degenerate division arises anywhere in the right-hand side; the hypothesis $0 \le p$ is exactly what rules out the one value $p = -1$ at which the displayed expression would divide by zero, and it additionally excludes all other negative $p$ .
The hypothesis $0 \le p$ is satisfiable (e.g. $p = 0$ ), so the statement is not vacuous.
Degenerate instances are included by the quantifier over $n$ . At $n = 0$ both sides are $0$ : the left side by the base case, the right side because $0 \cdot \frac{p}{1+p} = 0$ and $(-p)^{0} = 1$ makes the bracket $1 - 1 = 0$ — this uses the convention that the zeroth power is $1$ even when $p = 0$ . At $n = 1$ both sides equal $p$ . At $p = 0$ the recursion gives $S_0(n) = 0$ for all $n$ and the right-hand side is $0$ as well.
The statement mentions only the recursively defined $S_p$ and the arithmetic expression above; it makes no reference to the separately defined closed-form function hitsClosed of the bundle, nor to any of the runtime or token-cost quantities defined there, even though the right-hand side is written with the same symbols as that definition's body.

No proof is supplied in the declaration; the proof position is occupied by a placeholder, so the file asserts the identity without establishing it.

Human review

Endorsed by Shuze Chen · Sep 12, 2026
Endorsed by naimengye · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Closed form for the expected hit count SnS_nSn​

Closed form for the expected hit count $S_n$