Correctness of QSP phase synthesis

First verify the interval check. In efficient-numerical mode [F16] proves exact acceptance of the interval promise on the original unrounded target. For the complete modes the existing critical-point argument applies as follows. If the formal derivative is zero, write $p={\sum }_{k=0}^n{a}_k{x}^k$. By [F3] and [F11], $k{a}_k=0$ for each $k\ge 1$. In the ordered field [F12], $k\cdot 1>0$ for each positive integer $k$, by repeated addition of $1>0$; therefore $k\cdot 1$ is nonzero and invertible, so every $a_k=0$ for $k\ge 1$ and $p$ is constant. Its endpoint value is then its value everywhere, so the algorithm's single endpoint check is sufficient. Otherwise $p$ is nonconstant. If $p(x)>1$ somewhere, its maximum on $[-1,1]$ is greater than $1$ by [F4]. Since both endpoints were checked and are at most $1$, this maximum is attained at an interior point $c$. By [F5], $p^{\mathrm{\prime }}(c)=0$, and by [F3] this is a root of the formal derivative used by the algorithm. The complete list from [F2] therefore includes $c$, where the algorithm would detect $p(c)>1$, contrary to a successful check. The same argument applied to a value $p(x)<-1$ and the attained minimum detects every lower-bound violation. Conversely, when $\mathrm{\mid }p\mathrm{\mid }\le 1$ on the interval, every endpoint and critical-point comparison passes. Thus the validation branch accepts exactly the promised interval-bounded inputs.

On a valid input, the generated or checked complement identity and the degree/parity checks make $P=p_0+iB,Q=C$ admissible by [F6] and [F10]. In the supplied-complement branch the same conclusion follows from the exact identity and parity certificate, which is checked before use.

By [F7], that admissible pair has an exact phase list whose sequence matrix has upper-left entry $P$. Its real part is $p_0$, since $B$ has real coefficients. Hence exact mode gives $\mathrm{Re}P=p$; complete-numerical mode gives $\mathrm{\mid }\mathrm{Re}P-p\mathrm{\mid }=\mathrm{\mid }(1-{\delta }_0\mathrm{/}8)p-p\mathrm{\mid }\le {\delta }_0\mathrm{/}8$ because $\mathrm{\mid }p\mathrm{\mid }\le 1$. In efficient-numerical mode [F17] gives $\mathrm{\mid }\mathrm{Re}P-p\mathrm{\mid }=\mathrm{\mid }{p}_0-p\mathrm{\mid }\le 5{\delta }_0\mathrm{/}64<{\delta }_0\mathrm{/}8$. Thus the stated ideal error holds in either numerical mode. The explicit alternative square root in its peel has square $r$ and unit modulus by [F18], so the cancellation and factorization in [F7] apply unchanged.

In numerical mode the angle approximation contributes at most ${\delta }_0\mathrm{/}(16(d+1))$ per phase by [F8], and a supplied compiler contributes at most the same amount by its checked output certificate. Their sum is therefore at most ${\delta }_0\mathrm{/}(8(d+1))$ per phase. With exact signal calls, [F9] bounds the full unitary error by $(d+1){\delta }_0\mathrm{/}(8(d+1))={\delta }_0\mathrm{/}8$. Let $A=\tilde{U}-U$ and write $A{e}_0=A_{00}{e}_0+A_{10}{e}_1$ in the orthonormal signal basis of [F13]. Then [F14] gives $\mathrm{\parallel }A{e}_0{\mathrm{\parallel }}^2=\mathrm{\mid }{A}_{00}{\mathrm{\mid }}^2+\mathrm{\mid }{A}_{10}{\mathrm{\mid }}^2\ge \mathrm{\mid }{A}_{00}{\mathrm{\mid }}^2$, while [F15] and $\mathrm{\parallel }{e}_0\mathrm{\parallel }=1$ give $\mathrm{\parallel }A{e}_0\mathrm{\parallel }\le \mathrm{\parallel }A{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}$. Thus the upper-left entry error satisfies $\mathrm{\mid }{A}_{00}\mathrm{\mid }\le \mathrm{\parallel }A{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}$, and its real-part error is no larger. It differs from $p$ by at most the shrink error ${\delta }_0\mathrm{/}8$ plus phase error ${\delta }_0\mathrm{/}8$, at most ${\delta }_0\mathrm{/}4\le \delta$. Exact mode has zero shrink error. This identifies a matrix entry only and asserts no physical scalar-extraction procedure.

ROOTS and REALROOTS terminate by [F2], and their efficient-mode replacement terminates by [F17]. Root classification and multiplication process finite lists, the phase peel decreases nominal degree at every nonconstant step, and each phase approximation terminates by [F8], including for ideal-real coordinates: its rational buffered comparisons use the declared interface and contract every bracket by at least one half independently of equality. The supplied-complement path never invokes ROOTS on its coefficients; it checks its finite identity before any zero-complement branch and proceeds directly to the admissible pair. For its positive-root nodes, a positive real radicand has a finite rational upper bound, so doubling eventually succeeds; bisection then halves the width to the requested positive tolerance, with equality returning a singleton. In a unit peel ratio $r=x+iy$, $x=-1$ gives square root $i$; otherwise $s^2=(1+x)\mathrm{/}2>0$, $\omega =s+iy\mathrm{/}(2s)$ has imaginary-square contribution $y^2\mathrm{/}(4s^2)=(1-x)\mathrm{/}2$, so $\mathrm{\mid }\omega \mathrm{\mid }=1$ and ${\omega }^2=x+iy$. Thus these nodes give the same valid cancellation over real coefficients. No algebraic encoding of the real parameters is assumed. The optional compiler either returns a certificate or its declared failure. Consequently every promised execution terminates or returns the explicit IMPLEMENTATION_ERROR branch, and no failed certificate is reported as SUCCESS.

Put $S=d+1+{\log }_{+}(1\mathrm{/}\delta )$. Degree/parity validation scans at most $d+1$ coefficients on promised input. [F16] bounds its exact interval decision by $O((d+1{)}^4)$ operations, independent of original coefficient heights. [F17] bounds rounding by polynomially many charged coefficient operations/comparisons, gives a rounded rational target of polynomial coefficient height in $S$, and bounds its complete bounded-grid complement-root list at fixed isolator precision by $\mathrm{poly}(S)$ rational operations. Root classification, multiplicity grouping, descriptor sorting and symmetry checks use polynomially many exact equality/order tests on that finite list. No complete-mode root isolation of the original target or its critical points occurs in this branch.

[F18] bounds every positive-root descriptor in completion by a polynomial number of exact comparisons and rational operations using root-bound-based upper endpoints. In particular the norm-product leading coefficient has absolute value one, so the final scale has a known polynomial-height upper bound. Polynomial-array multiplication and full identity checks take polynomially many operations. Phase peeling, its identity checks, fixed convention conversion and padding require polynomially many field operations and at most $O(d+1)$ quadratic tower descriptors; no generic algebraic-coefficient ROOTS call occurs. The explicit half-angle formula divides only after checking that its positive root is nonzero. Its possible tiny numerical value does not alter a charged exact-field operation count.

There are $d+1$ phases, each requested to precision $\eta ={\delta }_0\mathrm{/}[16(d+1)]$. [F8] gives $O((1+\log (1\mathrm{/}\min (\eta ,1)){)}^2)$ rational operations and linear-in-that-log exact algebraic comparisons per phase, polynomial in $S$. Buffered comparisons contract the angular bracket in every case, including equality, so no hidden input-conditioned coordinate refinement is used. Each returned dyadic angle has polynomially many bits. Root isolators and their rational defining polynomials have polynomial height by [F17]; each completion/peel intermediate is a referenced field-operation or quadratic-extension node rather than an expanded minimal polynomial. The polynomial operation count thus gives polynomially many tower/DAG nodes and index bits. Angular bracket endpoints are obtained by fixed dyadic affine operations for polynomially many steps; Machin partial-sum denominators have polynomial bit length in the number of terms (multiplying their polynomially many integer denominators suffices as a common denominator). Their phase certificates also have polynomial size. The root, completion identity and peel certificates can reference these same nodes without duplicating expanded expressions. Together these bounds prove the resource assertion, while leaving the separately named encoding, implementation, conversion and optional compiler coordinates unclaimed.