Buffered certified rational phase approximation

PHASEAPPROX(ω,η) takes a unit scalar $\omega =u+iv$ and positive rational tolerance $\eta$. Coordinates may be exact algebraic, or exact real expression-DAG nodes in the following explicitly selected ideal-real model. A finite input table labels real constants by their stipulated values; a constant is a parameter with an oracle interface, not a finite rational encoding of an arbitrary real. DAG nodes denote rational constants, those parameters, field operations (division only by a tested nonzero value), and uniquely specified nonnegative square roots. The interface supplies exact equality and order tests on all such expressions, including comparisons with rationals; each call and each field/node operation is charged, together with rational arithmetic and written descriptors. An implementation may additionally return certified rational enclosures, but no enclosure-based equality decision is presumed. This ideal interface is an explicit resource assumption; arbitrary Cauchy names alone do not supply it. Algebraic inputs retain the original exact-algebraic operation model. Implementation and parameter-oracle costs are separate, with no Turing-time claim. Put $h=\min (\eta ,1)$. Reject a failed unit promise as INVALID.

1. Compute a rational interval $I_{\pi }$ of width at most $h\mathrm{/}8$ for $\pi =16\arctan (1\mathrm{/}5)-4\arctan (1\mathrm{/}239)$. For each arctangent use consecutive partial sums of ${\sum }_{j\ge 0}(-1{)}^j{r}^{2j+1}\mathrm{/}(2j+1)$ as the enclosure. Increment $N\ge 1$ until $20\cdot 5^{-(2N+1)}\le h\mathrm{/}8$ and use sums through indices $N-1,N$. Combine the two intervals outward.
2. Check coordinates for exact zero. If $v=0,u>0$, set $J=[0,0]$; if $v=0,u<0$, set $J=I_{\pi }$; if $u=0,v>0$, set $J=I_{\pi }\mathrm{/}2$; if $u=0,v<0$, set $J=-I_{\pi }\mathrm{/}2$. In these axis branches proceed to instruction 5. The zero vector returns INVALID.
3. Set $a=\mathrm{\mid }u\mathrm{\mid },b=\mathrm{\mid }v\mathrm{\mid }$ and $[L,U]=[0,2]$. While $w=U-L>h\mathrm{/}8$, set $m=(L+U)\mathrm{/}2$ and $\epsilon =w\mathrm{/}96$. Compute rational Taylor sums $c,s$ for cosine and sine at $m$ with error at most $\epsilon$. Retain at least indices $0,1,2$; increment until twice the next absolute term is at most $\epsilon$. The successive-term ratios after this index are at most $1\mathrm{/}2$. Form the exact real expression $q=bc-as$. If $q>2\epsilon$, set $L=m$. Otherwise if $q<-2\epsilon$, set $U=m$. Otherwise set $[L,U]=[L,U]\cap [m-12\epsilon ,m+12\epsilon ]$. Equality takes this last branch.
4. If $u>0,v>0$, set $J=[L,U]$; if $u<0,v>0$, set $J=I_{\pi }-[L,U]$; if $u<0,v<0$, set $J=-I_{\pi }+[L,U]$; if $u>0,v<0$, set $J=-[L,U]$.
5. Set $t_0$ to the rational midpoint of $J$. Find $k\ge 0$ by repeated halving until $2^{-k}\le h\mathrm{/}16$. Round $t_0$ to a multiple of $2^{-k}$ within $2^{-k}$, obtaining $t$; this can be done by binary search among the dyadic grid points in $[-4,4]$, charging every comparison and written bit. Return $t$, $J$, and the rounding bound as the phase certificate.

Use the returned rational phase in $Z(t)$ from QSP signal matrix and ordered phase sequence. All branches and operation counts are explicit; no coordinate-isolator refinement or equality test involving a transcendental sine/cosine value is invoked. In the ideal-real variant all coordinate equality/order calls use the explicitly supplied interface. This definition makes no Turing-time or finite-basis compilation claim.