proposition. A reliable acquisition bound [ftip-00OF]
✍️source

    The protocol in Definition [ftip-00OE] has hard additive cost at most \(U=S+kc\) and attains

    \[Q_{\rm acq}=\mathbb E Z\geq \beta \bigl (1-(1-q)^k\bigr ).\]

    Proof. 

      Let \(F_j\) denote failure of the first \(j\) attempts, with \(F_0\) certain. Conditional certification gives \(\Pr (F_j)\leq (1-q)\Pr (F_{j-1})\), hence \(\Pr (F_k)\leq (1-q)^k\). Conditional soundness at the first selected certificate and nonnegativity on failure imply \(\mathbb E Z\geq \beta \Pr (F_k^c)\). Summing the preparation and attempt caps proves the cost claim, including early stopping.

      If \(0<q<1\) and \(0<\tau <\beta \), the choice

      \[k=\left \lceil \frac {\log (1-\frac {\tau }{\beta })}{\log (1-q)}\right \rceil \]

      ensures \(Q_{\rm acq}\geq \tau \). If \(q=1\), one attempt suffices for \(\tau \leq \beta \). For example, \(q=1/4\), \(\beta =0.9\) and \(k=8\) give \(Q_{\rm acq}\geq 0.9(1-(3/4)^8)>0.8\); this is an illustration of the assumptions, not an empirical estimate.

      Together with an actual economically viable schedule for this protocol and an independent autonomous hard-work lower bound \(L>U\), this supplies the assisted construction needed in proposition [ftip-00O3], whenever the autonomous economic envelope is below \(L\). Here \(U\), \(L\) and that envelope must use the same counted resource unit, with any conversion explicitly justified. A low scalar cost does not establish the schedule or the lower bound.