Certified bracketed bisection for a continuous CDF

Input a continuous nondecreasing CDF $F$ on a finite interval $[a,b]$ with $a<b$, a target $u$, tolerance $\epsilon >0$, a nonnegative integer $N$, and a verified modulus certificate $\mathrm{\mid }x-y\mathrm{\mid }\le (b-a)2^{-N}⟹\mathrm{\mid }F(x)-F(y)\mathrm{\mid }\le \epsilon (x,y\in [a,b])\mathrm{.}$ An exact real-comparison oracle for $F$ and a budget of at least $N+2$ evaluations are also inputs. First evaluate and store $F(a)$ and $F(b)$, counting both against the budget; an evaluation failure returns inconclusive. If $u\mathrm{\notin }[F(a),F(b)]$, return status tail-unresolved. Otherwise set $\mathrm{\ell }=a$ and $r=b$. Repeat $N$ times: set $m=(\mathrm{\ell }+r)\mathrm{/}2$; if $F(m)\le u$, replace $\mathrm{\ell }$ by $m$, and otherwise replace $r$ by $m$. If an evaluation or the budget fails, return inconclusive. Return $\widehat{x}=(\mathrm{\ell }+r)\mathrm{/}2$ and the certificate $F(\mathrm{\ell })\le u\le F(r)$ and $\mathrm{\mid }F(\widehat{x})-u\mathrm{\mid }\le \epsilon$.

A caller that cannot supply a certified $N$, the required budget, or exact comparison returns inconclusive. The procedure resolves the central bracket only; any tails outside $[a,b]$ require a separately specified branch or sampler.

This is a real-arithmetic reference procedure. Endpoint queries and each midpoint query are counted against the input evaluation budget, with tail and precision failures explicit. It does not identify CDF residual with spatial error unless an additional positive lower density bound is supplied.