The hybrid event locator returns sound certificates or explicit failure within its budget

There are finitely many active guards. Each trial step processes at most $B_{\mathrm{r}\mathrm{o}\mathrm{o}\mathrm{t}}$ boxes per guard, and the entire run processes at most $B_{\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{p}}$ trial steps and $B_{\mathrm{e}\mathrm{v}\mathrm{e}\mathrm{n}\mathrm{t}}$ accepted events. The smooth isolator terminates at its finite box budget by [F3]. Hence every loop is finite and the procedure terminates.

Suppose the procedure accepts a no event step. For each active guard, [F1] requires a complete root-isolation result and either no certified roots or derivative enclosures that put every certified root strictly on the nontriggering side. By [F3], every exact root is in a certified or unresolved box; completeness removes the unresolved case, and [F5] makes each certified opposite-direction crossing nontriggering.

Suppose an event box is returned. By [F3] it contains exactly one root of its exact guard, and [F1] certifies that the derivative has the declared crossing sign with positive margin. Every earlier enabled root in any active guard would also have to appear in a certified or unresolved box by [F3]. The procedure either separates all candidate intervals and chooses the earliest, applies the fixed priority from [F5] to an exactly certified simultaneous tie, or returns inconclusive when order remains ambiguous. Therefore every successful event record is the first enabled event.

For a successful event result, [F1] reports the upper endpoint of the selected box mapped from local time to physical time; that mapped box contains the unique exact reference-guard root by [F3]. The admissible data in [F2] supply a valid total reference-mode error bound, a dense-guard enclosure at the reported endpoint, and the transverse derivative margin; in the finite-rational branch, [F6] justifies the local dense error and the provider's ledger must also include prior aligned reset-state errors. Thus the event record supplies the state error, guard residual, and positive margin required by [F4]. Applying [F4] gives the stated event-time bound.

Each remaining failure branch in [F1] returns inconclusive, domain-failure, or budget-exhausted with only the already certified prefix. By the procedure's stated output convention it asserts no absence of an event after the failed branch. Thus every successful certificate is sound and every incomplete branch makes no negative claim.

At each accepted event, [F1], [F3], and step 1.4 give a unique exact root $\tau$ and reported upper endpoint $\widehat{\tau }$ with $0\le \mathrm{\ell }:=\widehat{\tau }-\tau \le \mathrm{\Delta }<\delta \mathrm{/}3$. Separation by $\delta$ excludes another selected exact event before $\widehat{\tau }$, so the reference follows the outgoing mode throughout this lag. For $\mathrm{\ell }>0$, [F7] and [F8] bound the incoming continuation displacement by $M^{-}\mathrm{\ell }$ and the reference outgoing displacement by $M^{+}\mathrm{\ell }$; for $\mathrm{\ell }=0$ both vanish. Thus [F2] gives $\mathrm{\parallel }U(\widehat{\tau })-y^{-}(\tau ){\mathrm{\parallel }}_2\le {\eta }_{\mathrm{r}\mathrm{e}\mathrm{f}}+M^{-}\mathrm{\ell }$. The reset's Lipschitz bounds on the supplied coordinate segments give reset-state discrepancy at most $L_R{\eta }_{\mathrm{r}\mathrm{e}\mathrm{f}}+(L_R{M}^{-}+L_{R,t})\mathrm{\ell }$. Adding the outgoing displacement and certified reset-evaluation error gives aligned error at most $L_R{\eta }_{\mathrm{r}\mathrm{e}\mathrm{f}}+(L_R{M}^{-}+L_{R,t}+M^{+})\mathrm{\Delta }+{\epsilon }_R$, exactly the restart ledger in [F1]. This argument needs only the pathwise field bounds supplied by [F2]. Starting from the assumed valid $E=E_0$, induction proves every restart bound. Before processing a later trial, [F1] requires [F2]'s certified total reference-error bound on the whole enlarged prefix, including this aligned-start discrepancy or another sound justification; missing or unjustified data return inconclusive.