Efficient coherent amplitude-grid rounding

Put $a=\arctan (1\mathrm{/}5)$ and $b=\arctan (1\mathrm{/}239)$. Principal monotonicity and $\tan (\pi \mathrm{/}4)=1$ give $0<b<a<\pi \mathrm{/}4$. The tangent double-angle formula gives $\tan (2a)=5\mathrm{/}12<1$, so $2a<\pi \mathrm{/}4$ and $0<4a<\pi \mathrm{/}2$. A second doubling gives $\tan (4a)=120\mathrm{/}119>1$, hence $4a>\pi \mathrm{/}4>b$. The subtraction formula gives $\tan (4a-b)=\frac{120\mathrm{/}119-1\mathrm{/}239}{1+(120\mathrm{/}119)(1\mathrm{/}239)}=1.$ All denominators are positive, and $0<4a-b<4a<\pi \mathrm{/}2$. Injectivity of the principal tangent branch therefore proves $4a-b=\pi \mathrm{/}4$, or $\pi =16\arctan (1\mathrm{/}5)-4\arctan (1\mathrm{/}239)$. This is a local proof of the needed Machin identity.

For $0\le x<1$ and any integer $J\ge 1$, the exact finite geometric identity is $\frac{1}{1+t^2}={\sum }_{j=0}^{J-1}(-1{)}^j{t}^{2j}+\frac{(-1{)}^J{t}^{2J}}{1+t^2}\mathrm{.}$ Integrating from zero to $x$ and using the arctangent integral yields $\mid \arctan x-{\sum }_{j=0}^{J-1}\frac{(-1{)}^j{x}^{2j+1}}{2j+1}\mid \le \frac{x^{2J+1}}{2J+1}\mathrm{.}$ This is a finite bound, requiring no limit test during the algorithm. Set $J=k+8$ and form the exact rational $\widehat{\pi }=16{\sum }_{j=0}^{J-1}\frac{(-1{)}^j}{(2j+1)5^{2j+1}}-4{\sum }_{j=0}^{J-1}\frac{(-1{)}^j}{(2j+1){239}^{2j+1}}\mathrm{.}$ Step 1.1 and the finite integral estimate above give $\mathrm{\mid }\widehat{\pi }-\pi \mathrm{\mid }\le \frac{20}{5^{2J+1}}\le \frac{1}{1024M^2},$ because $5^{2k}\ge 2^{2k}=M^2$ and $20\cdot 1024<5^{17}$. In particular $0<\widehat{\pi }<4$: for the lower bound, $\pi \mathrm{/}4={\int }_0^1(1+t^2{)}^{-1}dt>1\mathrm{/}2$ gives $\pi >2$; for the upper bound, step 1.1 and $\arctan (1\mathrm{/}5)<1\mathrm{/}5$ give $\pi <16\mathrm{/}5$, and the displayed error is below $1\mathrm{/}1024$.

Set $x=\widehat{\pi }y\mathrm{/}M$, so $0\le x<4$, and set the even integer $n=16(k+4)$. Compute the exact rational sine polynomial $S(x)={\sum }_{j=0}^{n\mathrm{/}2-1}\frac{(-1{)}^j{x}^{2j+1}}{(2j+1)!}\mathrm{.}$ Every derivative of sine has absolute value at most one. The Taylor remainder bound at degree $n-1$ gives $\mathrm{\mid }S(x)-\sin x\mathrm{\mid }\le \frac{4^n}{n!}\le {\left(\frac{32}{n}\right)}^{n\mathrm{/}2}\le 2^{-n\mathrm{/}2}\le \frac{1}{4096M^2}\mathrm{.}$ Indeed the last $n\mathrm{/}2$ factors in $n!$ are at least $n\mathrm{/}2$, so $n!\ge (n\mathrm{/}2{)}^{n\mathrm{/}2}$, and $n\ge 96\ge 64$. Finally $n\mathrm{/}2=8(k+4)\ge 2k+12$ gives the stated precision.

All rational computations above have polynomial bit length in $k$. For the arctangent sum at $q\in \{5,239\}$, one may take as an unreduced common denominator $D_q={\prod }_{j=0}^{J-1}(2j+1)q^{2j+1}$, whose bit length is $O(J^2+J\log (J+1))=O(k^2)$. Obtain each numerator by exact division of this known multiple, then sum with the indicated signs. A common denominator for $\widehat{\pi }$ is $D_5{D}_{239}$, still of $O(k^2)$ bits; the same bound holds for its numerator. Therefore $x=P\mathrm{/}Q$ can be written with integer $P\ge 0$, $Q>0$ of $O(k^2)$ bits, without rational reduction.

The derivative bound for sine and the mean value theorem give $\mathrm{\mid }\sin x-\sin (\pi y\mathrm{/}M)\mathrm{\mid }\le \mathrm{\mid }\widehat{\pi }-\pi \mathrm{\mid }y\mathrm{/}M\le 1\mathrm{/}(1024M^2)$. Put $s=\sin (\pi y\mathrm{/}M)$ and $d=5\mathrm{/}(4096M^2)$. Step 3.1 implies $\mathrm{\mid }S(x)-s\mathrm{\mid }\le d<1$ and $\mathrm{\mid }s\mathrm{\mid }\le 1$. Consequently $\mathrm{\mid }S(x{)}^2-s^2\mathrm{\mid }\le d(2+d)\le 3d=\frac{15}{4096M^2}<\frac{1}{4M^2}\mathrm{.}$ Thus the exact rational square $r=S(x{)}^2$ approximates the desired probability with absolute error strictly below $1\mathrm{/}(4M^2)$.

If $y=0$, set $a_M(y)=0$ explicitly. Otherwise write the exact rational $r=U\mathrm{/}V$ with integers $U\ge 0$ and $V>0$, without requiring cancellation to lowest terms. Use integer division to compute $q=\lfloor \frac{2M^{2}U+V}{2V}\rfloor ,a_M(y)=\min (M^2,\max (0,q))\mathrm{.}$ The floor rule is deterministic nearest-grid rounding, breaking rational half-grid ties upward. Hence $\mathrm{\mid }q\mathrm{/}{M}^2-r\mathrm{\mid }\le 1\mathrm{/}(2M^2)$. Clipping to $[0,1]$ cannot increase distance from the true probability $s^2\in [0,1]$. Step 4.1 therefore gives $\mid a_M(y)\mathrm{/}{M}^2-s^2\mid <\frac{1}{4M^2}+\frac{1}{2M^2}=\frac{3}{4M^2}\mathrm{.}$ For $y=0$, the exact target is zero, so the bound also holds. Every comparison in this procedure compares finite integers, including any tie; there is no comparison against an exact transcendental number.

A common denominator for the sine polynomial is $D=Q^{n-1}(n-1)!$. Its $j$th integer numerator term is $(-1{)}^j{P}^{2j+1}{Q}^{n-2j-2}\frac{(n-1)!}{(2j+1)!}\mathrm{.}$ All exponents are nonnegative and every indicated division is exact. The powers, factorials, terms, common denominator, and signed partial sums have $O(k^3)$ bits: $n=O(k)$, $\log P,\log Q=O(k^2)$, and $\log ((n-1)!)=O(k\log (k+1))$. Summing $O(k)$ terms adds only $O(\log (k+1))$ extra bits. Thus $S=A\mathrm{/}D$ can be computed with $O(k^3)$-bit signed integers; $U=A^2$, $V=D^2$, and the final integer division in step 5.1 have the same bit-length order.

There are only polynomially many arithmetic operations: products for the two denominators, powers and factorials, $O(k)$ Taylor terms and their exact divisions, and one final quotient/clamp. Schoolbook addition, subtraction and comparison of $L$-bit integers use $O(L)$ elementary Boolean operations, multiplication uses $O(L^2)$ operations by summing shifted partial products, and long division uses $O(L^2)$ operations by $O(L)$ shift/compare/subtract stages. Signed integers can use a sign bit and a magnitude of the fixed safe length; all denominators are known positive. The operation counts and safe register lengths depend only on $k$. Unroll their loops and implement data branches by Boolean selection between the two computed results. Thus a deterministic classical generator produces a Boolean DAG for $y\mapsto a_M(y)$ of polynomial size and description length in $k$, in polynomial time. This also covers generation of the rational constants; no constant table of exponential length or unit-cost unbounded integer arithmetic is assumed.

Apply compute-copy-reverse to that Boolean DAG: evaluate its nodes in fresh clean bits, XOR-copy its $(2k+1)$ output bits to $z$, and reverse every evaluation gate. The inspected reversible embedding theorem gives the asserted XOR action, polynomial elementary gate count, serial depth and clean workspace, all restored to zero. The Boolean circuit's uniform generation proof in step 7.1, followed by the finite node-gadget compiler, gives polynomial-time generation of the actual reversible gate list. The clean identity extends by linearity to coherent inputs and finite references. Its actual reversal has identical gate count. For an external control, either use a compute/controlled-copy/uncompute construction on the same Boolean function, or control the fixed reversible gate list; the former directly gives a constant-factor resource increase and restores all scratch. No real-number refinement or measurement occurs. This proves the Statement.