\pdfoutput=1
\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm,mathtools,booktabs,array}
\usepackage[margin=1in]{geometry}
\usepackage[colorlinks=true,urlcolor=blue,citecolor=blue]{hyperref}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\rem}{\operatorname{rem}}
\newcommand{\calls}{\operatorname{calls}}
\newcommand{\eq}{\operatorname{eq}}
\newcommand{\coprime}{\perp\!\!\!\perp}
% Lean identifiers, breakable after dots and underscores.
\newcommand{\lean}[1]{\nolinkurl{#1}}
\makeatletter\g@addto@macro\UrlBreaks{\do\_}\makeatother
\emergencystretch=2em
\title{The Euclidean algorithm is not optimal among uniform processes}
\author{Jason Davies\thanks{\href{mailto:jason@jasondavies.com}{\nolinkurl{jason@jasondavies.com}}}}
\date{October 28, 2026}
\begin{document}
\maketitle
\begin{abstract}
Reusing a stored Euclidean prefix, we show that every pair $a\geq b$ has a
derivation of $\gcd(a,b)$ from $a,b$ with $O(\log a/\log\log a)$
applications of the remainder function alone; Euclid's algorithm needs order $\log a$ in the
worst case. These derivations bound the intrinsic complexity
of gcd and coprimeness by the same order, refuting Moschovakis's conjectured
logarithmic lower bounds for uniform processes; by his best-uniform-process
theorem, a single uniform process attains this bound.
The Main Conjecture for algorithms remains open. We also prove an
$\Omega(\log\log a)$ lower bound on this complexity for almost all coprime
pairs and give,
for each $\varepsilon>0$, a nondeterministic register program computing gcd
that, on every input $a\geq b\geq1$, has a successful computation using at
most $\varepsilon\log a+O(1)$ remainder calls. The upper bound also answers
negatively an open problem of van den Dries and Moschovakis on the closure
depth of the gcd. The main bounds and the
refutations are formalised in Lean~4; the best-uniform-process theorem is cited.
\end{abstract}

\noindent\textbf{AI transparency statement.} The main result, its
formalisation in Lean and the manuscript were produced by artificial
intelligence. The human author initiated the broader research and directed
the AI systems, but did not write the text. Details are given at the end of
the paper.

\section{Introduction}\label{sec:intro}
Van den Dries and Moschovakis asked whether the Euclidean algorithm is optimal
among its peers, the algorithms that compute the gcd from the remainder
function \cite[p.~390]{vddm2004}. Moschovakis's Main Conjecture (in his
monograph \cite{moschovakis2019}, henceforth ``the book'') asserts that for every
algorithm $\alpha$ from $\rem$ and the zero test $\eq_0$ computing
$\gcd(x,y)$ there is an $r>0$ such that $\alpha$ makes more than $r\log x$
remainder calls on infinitely many pairs $x>y\geq1$
\cite[p.~2]{moschovakis2019}. Uniform processes are the book's abstract
model of computation from given primitives: every deterministic or
nondeterministic recursive program induces one
\cite[\S4A, Proposition~4A.1]{moschovakis2019}, but a uniform process need
not be implemented by any finite program. Moschovakis stated versions of
the conjecture for uniform processes in his 2012 notes and in the book; we
refute both (Section~\ref{sec:certificates}). For algorithms the conjecture
remains open.

\paragraph{Derivations.}
A \emph{derivation} from $a,b$ is a finite list that starts with $a,b$ and in
which each further entry is $\rem(x,y)$ for earlier entries $x,y$ with $y>0$.
Each further entry is one \emph{instruction}, that is, one remainder call.
Entries already in the list are \emph{available} and may be reused; no
constants and no other operations are supplied. Let $G(a,b)$ be the least
number of instructions in a derivation containing $\gcd(a,b)$. Thus
$G(a,0)=G(a,1)=0$. Arithmetic used in the proofs, such as subtraction,
sorting or comparison, only selects instructions; it is never itself an
instruction. So $G$ measures the length of a derivation, not the work of
finding one. Logarithms are to base $2$.

\begin{theorem}\label{thm:main}
There is a constant $C$ such that for all integers $a\geq4$ and $0\leq b\leq a$,
\[
G(a,b)\leq C\,\frac{\log a}{\log\log a}.
\]
\end{theorem}

\paragraph{Idea of the proof.}
The key is to store one short Euclidean prefix and reuse it many times.
For sufficiently large $n$, let $a>b$ be coprime with $a\leq N=2^n$.
Store a Euclidean prefix
$r_0=a,r_1=b,\ldots,r_h$, where $h=3k$ and $k=2^{\lfloor(\log n)/2\rfloor}$
is about $\sqrt n$.
If the prefix reaches a positive remainder at most $N^{3/4}$, take one
further remainder and recurse on the resulting smaller pair.
Otherwise, modulo every $m>N^{1/3}$, each residue class contains at most
three prefix values, so the prefix occupies at least $k+1$ residue
classes (Lemma~\ref{lem:prefix}). A close pair of residues lets three
remainder calls produce a positive value below $m/k$
(Lemma~\ref{lem:gap}). Reusing the same prefix, we repeatedly shrink the
modulus from $r_h$ to at most $N^{1/3}$ in $O(n/\log n)$ calls.
Since $m$ need not be coprime to $a$ or $b$, two recursive gcd
derivations on inputs at most $N^{1/3}$ finish: of $d=\gcd(m,\rem(a,m))$,
and then of $\gcd(d,\rem(b,m))$.
If $T(n)$ is the worst derivation cost for inputs at most $2^n$, the
resulting recurrence \eqref{eq:recurrence} gives $T(n)=O(n/\log n)$.
Taking $k$ about $n^c$ with $c$ close to $1$ instead sharpens the upper
coefficient to $3+o(1)$ (Corollary~\ref{cor:three}): each contraction costs
three calls and removes about $\log k\approx\log n$ bits, while the prefix
stays negligible.

\paragraph{Consequences and further results.}
Section~\ref{sec:certificates} shows that $G(a,b)$ equals the intrinsic
remainder-call complexity of coprimeness in the book's Euclidean structure
on positive coprime inputs, and bounds those of gcd to within $2$
(Proposition~\ref{prop:certificates}). Theorem~\ref{thm:main} therefore
refutes Conjecture~3.4 of \cite{moschovakis2012} and version (4F-5) of the
Main Conjecture, and shows that lower bounds from the homomorphism method
cannot exceed $O(\log a/\log\log a)$ for these problems. The
book's best-uniform-process theorem then gives a single process with the
same bound on every input. The upper bound also settles an open problem
of van den Dries and Moschovakis on the closure depth of the gcd
(Corollary~\ref{cor:closure-depth}).

We also prove that $G(a,b)\geq(1-o(1))\log\log N$ for all but $o(N^2)$
coprime pairs $2\leq b<a\leq N$ (Proposition~\ref{prop:loglog}).
Finally, fixing the prefix length gives, for each $\varepsilon>0$, a
nondeterministic register program with a successful computation costing at
most $\varepsilon\log a+O(1)$ on each input $a\geq b\geq1$
(Theorem~\ref{thm:registers}). The
number of registers grows as $\varepsilon$ decreases.

Sections~\ref{sec:normalization}--\ref{sec:construction} prove
Theorem~\ref{thm:main} and its refinements, Section~\ref{sec:certificates}
treats certificates and uniform processes, Sections~\ref{sec:loglog}
and~\ref{sec:programs} give the lower bound and the register programs,
Section~\ref{sec:discussion} discusses open problems, and
Section~\ref{sec:checks} and Appendix~\ref{app:lean} describe the
computational checks and the Lean formalisation.

\paragraph{Related work.}
The known intrinsic lower bounds give $\Omega(\log\log a)$ on special
families of coprime pairs \cite{vddm2004,vddm2009},
\cite[Theorem~6C.5]{moschovakis2019}, also for richer primitives such as
addition and integer quotient, and for depth. Pratt's unpublished nondeterministic algorithm
\cite[Theorem~2E.2 and Problems~x2E.17--x2E.19]{moschovakis2019}
matches this order on successive Fibonacci numbers
\cite[Corollary~6C.7]{moschovakis2019}.
For remainder-only derivations, our almost-all bound gives the same order
on a set of full density among coprime pairs. Mansour, Schieber and Tiwari
proved lower bounds for gcd and coprimeness in computation trees with richer
arithmetic, including the floor operation \cite{mst1991a,mst1991b}; van den
Dries and Moschovakis compare them with the intrinsic bounds
\cite[pp.~2:3--2:4]{vddm2009}.

In a different model, Bshouty obtained the optimal bound
$\Theta(\log N/\log\log N)$ for gcd on inputs in $[0,N]$ using a random
access machine with linear operations, shifts, comparisons and indirect
addressing \cite[Theorems~i and~ii, p.~3]{bshouty1989}. His construction
tabulates blocks of the binary gcd algorithm \cite{stein1967},
\cite[\S4.5.2]{knuth1997}, computing table entries on demand and counting
their construction \cite[\S4, Algorithm~D and Lemma~5, pp.~12--14]{bshouty1989}.
Here the saving comes from
reusing a Euclidean prefix with remainder as the only instruction.

\section{Normalisation}\label{sec:normalization}
Write $g=\gcd(a,b)>0$. For positive $y$,
\[
\rem(gx,gy)=g\rem(x,y).
\]
Every generated value is divisible by $g$. Consequently scaling a derivation,
or dividing all its values by $g$, preserves its length and the validity of
every instruction. Hence
\begin{equation}\label{eq:normalize}
G(a,b)=G(a/g,b/g).
\end{equation}
Define
\[
T(n)=\max_{0\leq b\leq a\leq 2^n,\ a>0}G(a,b).
\]
Euclid's remainders form a derivation containing $\gcd(a,b)$, so $G$ and
$T$ are finite. By \eqref{eq:normalize} it
suffices to bound $G$ on coprime pairs; the cases $a=b$, $b=0$ and $b=1$ need no instructions.

\section{Three-call contractions}\label{sec:contractions}
\begin{lemma}\label{lem:gap}
If $m>0$ is available and a finite collection $S$ of available values occupies
$t\geq2$ residue classes modulo $m$, at most three instructions generate $w$
with
\[
0<w<\frac{m}{t-1}.
\]
\end{lemma}
\begin{proof}
Sort the distinct residues. Some adjacent pair $u<v$ has gap
$\delta=v-u<m/(t-1)$, because the sum of the $t-1$ adjacent gaps is less than
$m$. Each selected residue is $\rem(x,m)$ for some $x\in S$, so it costs one
instruction. If $u=0$, use $v$. If $0<u\leq\delta$, use $u$. Otherwise
$0<\delta<u$ and $v=u+\delta$, so $\rem(v,u)=\delta$. This uses at most three
instructions.
\end{proof}

\begin{lemma}[Euclidean-prefix lemma]\label{lem:prefix}
Let $r_0=a>r_1=b>\cdots>r_h>0$ be a Euclidean prefix of a coprime pair, with
$r_{i-1}=q_i r_i+r_{i+1}$ and $q_i\geq1$ for $1\leq i<h$. For every integer
$m>2a/r_h$, each residue class modulo $m$ contains $r_i$ for at most three
indices $0\leq i\leq h$. The prefix therefore occupies $t$ residue classes
with $3t\geq h+1$.
\end{lemma}
\begin{proof}
Let $q_h=\lfloor r_{h-1}/r_h\rfloor\geq1$ and $r_{h+1}=\rem(r_{h-1},r_h)$,
so that the recurrence also holds for $i=h$. For $i<j\leq h$ set
\[
M_{i,j}=\prod_{\ell=i+1}^{j}\begin{pmatrix}q_\ell&1\\1&0\end{pmatrix},
\qquad
\binom{r_i}{r_{i+1}}=M_{i,j}\binom{r_j}{r_{j+1}}.
\]
Right multiplication by
$\bigl(\begin{smallmatrix}q&1\\1&0\end{smallmatrix}\bigr)$ sends
$(A,B,C,E)$ to $(qA+B,\,A,\,qC+E,\,C)$, starting from $(q,1,1,0)$ for a single
factor. By induction, the entries of
$M_{i,j}=\bigl(\begin{smallmatrix}A&B\\C&E\end{smallmatrix}\bigr)$ are
nonnegative, $A\geq B\geq E$, $A\geq C\geq E$, $B,C\geq1$, and
$\det M_{i,j}=(-1)^{j-i}$; a product of at least two factors has $A\geq2$.

Suppose $r_s\equiv r_u\equiv r_v\pmod m$ with $s+2\leq u<v\leq h$; a
class with four indices $i_1<i_2<i_3<i_4$ contains such $s=i_1$, $u=i_3$
and $v=i_4$.
Write $M_{s,u}=\bigl(\begin{smallmatrix}\sigma&\tau\\\ast&\ast\end{smallmatrix}\bigr)$ and
$M_{u,v}=\bigl(\begin{smallmatrix}A&B\\C&E\end{smallmatrix}\bigr)$, so that
$r_u=Ar_v+Br_{v+1}$ and $r_s=A'r_v+B'r_{v+1}$ with $A'=\sigma A+\tau C$
and $B'=\sigma B+\tau E$. Then $m$ divides $r_s-r_v=(A'-1)r_v+B'r_{v+1}$
and $r_u-r_v=(A-1)r_v+Br_{v+1}$. Eliminating $r_{v+1}$, and then $r_v$,
shows that $m$ divides $Dr_v$ and $Dr_{v+1}$, where
\[
D=(A'-1)B-B'(A-1)=-\tau\det M_{u,v}+(\sigma-1)B+\tau E.
\]
Consecutive remainders are coprime, so B\'ezout's identity gives $m\mid D$.
If $\det M_{u,v}=-1$, then $D\geq\tau>0$. If it is $1$, then $E\geq1$ as
$AE=1+BC$, and $\sigma\geq2$ because $M_{s,u}$ has $u-s\geq2$ factors, so
$D\geq B>0$. In both cases $D\leq\tau+B'-B\leq\tau+A'-B<2A'$, since
$B'\leq A'$ (as $A\geq B$ and $C\geq E$) and $\tau\leq\sigma\leq\sigma A<A'$. Finally
$A'r_v\leq r_s\leq a$ gives $2A'\leq2a/r_h<m$, so $0<D<m$, a
contradiction. Hence each class contains at most three of
$r_0,\ldots,r_h$, and $t$ classes hold at most $3t$ of them.
\end{proof}
Since Lemma~\ref{lem:prefix} holds for every $m>2a/r_h$, one stored prefix
serves every later modulus, although these moduli are not known in advance.
If $h=3k$ with $k\geq1$, then $3t\geq3k+1$, so the prefix occupies at least
$k+1$ residue classes modulo every available $m>2a/r_h$, and
Lemma~\ref{lem:gap} applied to the prefix gives three instructions that
generate
\begin{equation}\label{eq:contract}
0<w<\frac mk.
\end{equation}
We call these three instructions a \emph{contraction} of $m$, and $w$ the new
modulus.

For example, from $44,17$ one instruction stores the prefix $44,17,10$.
Modulo $m=10>2\cdot44/10$ its residues are $4,7,0$, and the close pair
$4<7$ gives a contraction step as in Lemma~\ref{lem:gap} (this prefix is too
short for \eqref{eq:contract}, so we read off the residues directly):
\[
\rem(44,10)=4,\qquad \rem(17,10)=7,\qquad \rem(7,4)=3,
\]
with new modulus $3<10/(3-1)$. One more
instruction, $\rem(10,3)=1$, finishes. This derivation takes five instructions;
Euclid reaches $1$ in four. The example illustrates contraction without a
saving on this pair.

\section{Construction and recurrence}\label{sec:construction}
Fix an integer $n>16$ and put
\[
N=2^n,\qquad p=\lfloor(\log n)/2\rfloor\geq2,\qquad k=2^p,\qquad h=3k,
\qquad J=\lceil n/p\rceil,
\]
so that $k\leq\sqrt n$ and $k^J\geq N$.
After normalisation, assume $a>b>1$ are coprime and $a\leq N$.
We use $N^{3/4}$ as the \emph{early threshold} and $N^{1/3}$ as the
\emph{target modulus}. Any thresholds $N^\alpha,N^\beta$ with $\alpha<1$,
$\alpha+\beta>1$ and $2\beta<1$ would do: these make the early recursive
problem smaller, let the prefix lemma apply above the target, and make the
two final problems together smaller.

\paragraph{Phase (i): the prefix.}
Starting from $r_1=b$, generate the Euclidean remainders $r_2,r_3,\ldots$,
one instruction each, until the most recent value is at most $N^{3/4}$ or
$r_h$ is available. This costs at most $h$ instructions. Since the inputs
are coprime, Euclid's algorithm reaches $1$ before $0$, so the stopping
value is positive.

If the stopping value $c$ is at most $N^{3/4}$, generate the next
remainder $s<c$ with one more instruction. The pair $(c,s)$ is coprime, with
both entries at most $2^{\lceil3n/4\rceil}$. This gives the bound
\begin{equation}\label{eq:early}
h+1+T(\lceil3n/4\rceil).
\end{equation}

\paragraph{Phase (ii): contractions.}
Otherwise $r_h>N^{3/4}$, so $2a/r_h<2N^{1/4}<N^{1/3}$ (as $n>12$), and
Lemma~\ref{lem:prefix} applies to every available
$m>N^{1/3}$. Starting at $m=r_h$, repeatedly replace $m$ by the value $w$ of
\eqref{eq:contract} until $0<m\leq N^{1/3}$. After $j$ contractions
$m<N/k^j$; since $k^J\geq N$ and $m\geq1$, fewer than $J$ contractions occur. Since
$p=\tfrac12\log n+O(1)$, their cost is $3J=O(n/\log n)$.
This is the source of the saving: the prefix costs only $O(\sqrt n)$
instructions, and every contraction reuses it.

\paragraph{Phase (iii): two recursive derivations.}
The small $m$ need not be coprime to either input. Generate
$u=\rem(a,m)$ and $v=\rem(b,m)$, then append a derivation of $d=\gcd(m,u)$
from $m,u$ and one of $e=\gcd(d,v)$ from $d,v$. Since
$m\leq2^{\lceil n/3\rceil}$ and $G$ is symmetric, each costs at most
$T(\lceil n/3\rceil)$. Finally
\[
e=\gcd(\gcd(m,\rem(a,m)),\rem(b,m))
 =\gcd(m,\gcd(a,b))=1.
\]
The cost in this case is at most
\begin{equation}\label{eq:late}
h+3J+2+2T(\lceil n/3\rceil).
\end{equation}

\paragraph{The recurrence.}
The two case estimates \eqref{eq:early} and \eqref{eq:late} and normalisation
imply
\begin{equation}\label{eq:recurrence}
T(n)\leq\max\{T(\lceil3n/4\rceil)+O(\sqrt n),\;
2T(\lceil n/3\rceil)+O(n/\log n)\}.
\end{equation}
All implied constants are independent of the inputs.

\begin{proof}[Proof of Theorem~\ref{thm:main}]
For $n\geq2$ let $f(n)=n/\log n$. The ratios
\[
\frac{f(\lceil3n/4\rceil)}{f(n)}\longrightarrow\frac34,
\qquad
\frac{2f(\lceil n/3\rceil)}{f(n)}\longrightarrow\frac23
\]
show that, beyond a fixed threshold, $f(\lceil3n/4\rceil)\leq\tfrac78f(n)$ and
$2f(\lceil n/3\rceil)\leq\tfrac56f(n)$. Both overheads in
\eqref{eq:recurrence} are at most $c_0f(n)$ for a fixed $c_0$. Choose the
induction threshold above $16$, where the recurrence holds, and large enough
that both recursive indices are at least $2$ and strictly less than $n$. Choose
$C'\geq8c_0$, increased to cover the finitely many values below the threshold.
Strong induction then gives $T(n)\leq C'f(n)$: the two bounds are
$(7C'/8+c_0)f(n)$ and $(5C'/6+c_0)f(n)$, both at most $C'f(n)$.
Finally take $n=\lceil\log a\rceil$. For $a\geq4$, $n\leq2\log a$ and
$\log n\geq\log\log a\geq1$, so $G(a,b)\leq T(n)\leq2C'\log a/\log\log a$,
and the theorem holds with $C=2C'$.
\end{proof}

\subsection{The leading coefficient}
The same construction with larger $p$ gives a more precise bound.

\begin{corollary}\label{cor:three}
For every $\varepsilon>0$, there is an $a_0$ such that for every
$a\geq a_0$ and $0\leq b\leq a$,
\[
G(a,b)\leq(3+\varepsilon)\frac{\log a}{\log\log a}.
\]
Equivalently, the uniform upper bound has coefficient $3+o(1)$.
\end{corollary}
\begin{proof}
Fix $0<c<1$ and $0<\beta<1/2$, and put $\alpha=1-\beta/2$.
For large $n$ put
\[
p=\lfloor c\log n\rfloor,\qquad k=2^p,\qquad h=3k,
\qquad J=\lceil n/p\rceil.
\]
Use $N^\alpha$ as the early threshold and $N^\beta$ as the target modulus,
where $N=2^n$. In the late case $r_h>N^\alpha$, so
$2a/r_h<2N^{1-\alpha}=2N^{\beta/2}<N^\beta$ for sufficiently large $n$, and
the prefix lemma applies to every modulus above $N^\beta$. By
\eqref{eq:contract}, each contraction reduces the modulus by a factor
greater than $k$, and $k^J\geq N$, so $J$ contractions suffice.
Writing $f(n)=n/\log n$, we have
\[
h=O(n^{c})=o(f(n)),\qquad
3J=\left(\frac3c+o(1)\right)f(n).
\]
The two branches therefore give
\[
T(n)\leq\max\left\{
 T(\lceil\alpha n\rceil)+o(f(n)),\quad
 2T(\lceil\beta n\rceil)+\left(\frac3c+o(1)\right)f(n)
\right\}.
\]
Theorem~\ref{thm:main} implies that
$\Lambda=\limsup_{n\to\infty}T(n)/f(n)$ is finite and nonnegative.
For each fixed $q>0$, the ratio $f(\lceil qn\rceil)/f(n)$ tends to $q$.
Taking upper limits in the recurrence yields
\[
\Lambda\leq\max\{\alpha \Lambda,\ 2\beta \Lambda+3/c\}.
\]
Since $\alpha<1$ and $\Lambda\geq0$, this implies
$(1-2\beta)\Lambda\leq3/c$. As $T$, and hence $\Lambda$, does not depend on
$c$ or $\beta$, this holds for all $0<c<1$ and $0<\beta<1/2$, so
$\Lambda\leq3$. Finally, $n=\lceil\log a\rceil$ satisfies
$f(n)\sim\log a/\log\log a$, proving the assertion. All upper limits concern
the worst-case function $T$, so the resulting threshold is independent of $b$.
\end{proof}
We do not claim that $3$ is optimal.

\subsection{Closure depth}
Van den Dries and Moschovakis \cite{vddm2009} measure the parallel depth of the gcd. Put
$S_0=\{0,1,a,b\}$, let $S_{k+1}$ adjoin to $S_k$ all values $x+y$, $x-y$,
$\operatorname{iq}(x,y)$ and $\rem(x,y)$ with $x,y\in S_k$, and let $g(a,b)$
be the least $k$ with $\gcd(a,b)\in S_k$ \cite[p.~2:6]{vddm2009}. They ask
whether there are positive integers $a_n\to\infty$ and $b_n$ and a $C>0$
with $g(a_n,b_n)>C\log a_n$ for all $n$
\cite[Open Problem, p.~2:11]{vddm2009}. Here, following \cite[p.~2:4]{vddm2009},
the stages live in $\mathbb Z$, $\operatorname{iq}(x,y)=\lfloor x/y\rfloor$
and $\rem(x,y)=x-y\operatorname{iq}(x,y)$ for $y\neq0$, and
$\operatorname{iq}(x,0)=\rem(x,0)=x$; these total operations agree with the
remainder used in derivations, whose divisors are always positive.

\begin{corollary}\label{cor:closure-depth}
For integers $a\geq4$ and $b\geq1$,
\[
g(a,b)\leq1+G(a,\rem(b,a))
 =O\left(\frac{\log a}{\log\log a}\right).
\]
Hence the Open Problem has a negative answer: no such sequences $a_n,b_n$
exist.
\end{corollary}
\begin{proof}
Put $r=\rem(b,a)$, so $r\in S_1$, $0\leq r<a$ and $\gcd(a,r)=\gcd(a,b)$.
In a derivation from $a,r$, the value of the $k$th instruction lies in
$S_{k+1}$, by induction on $k$: its operands are $a$, $r$ or earlier values,
all in $S_k$, and every divisor in the derivation is positive.
Theorem~\ref{thm:main} bounds $G(a,r)$.
\end{proof}
On a concurrent-read concurrent-write PRAM, counting bit operations,
Kannan, Miller and Rudolph \cite{kmr1987} and Chor and Goldreich
\cite{chorgoldreich1990} compute the gcd of $n$-bit integers in parallel
time $O(n\log\log n/\log n)$ and $O(n/\log n)$ respectively. Van den Dries and Moschovakis posed
their question later, for the closure under exact integer operations, where
each operation on whole integers is one step;
Corollary~\ref{cor:closure-depth} gives depth of the same order there.

\section{Certificates and uniform processes}\label{sec:certificates}
\paragraph{Structures and certificates.}
Write $\mathrm{tt},\mathrm{ff}$ for the truth values and $\eq_c$ for the
test $x=c$. We use the book's partial remainder operation, defined only
when its second argument is nonzero, in the structures
\[
\mathcal N_0=(\mathbb N,\rem,\eq_0),\qquad
\mathcal N_\varepsilon=(\mathbb N,\rem,\eq_0,\eq_1).
\]
The latter is the book's Euclidean structure $\mathbf N_\varepsilon$
\cite[(1C-10), p.~24]{moschovakis2019}; our $\mathcal N_0$ should not
be confused with the book's $\mathbf N_0$, which has no remainder operation
\cite[p.~171]{moschovakis2019}.
Coprimeness is the relation
$x\coprime y\iff x,y\geq1\wedge\gcd(x,y)=1$
\cite[\S1A]{moschovakis2019}.

A \emph{certificate} for $f$ at $\vec x$ in a structure $\mathcal A$ is a
finite partial substructure $\mathcal U$ of $\mathcal A$, generated by
$\vec x$ and containing $f(\vec x)$ when $f$ is a function, such that every
homomorphism $\pi:\mathcal U\to\mathcal A$ satisfies
$f(\pi\vec x)=\pi(f(\vec x))$; homomorphisms fix the truth values, so for a
relation this says $f(\pi\vec x)=f(\vec x)$. In other words, any assignment
of values preserving the recorded operations and tests must preserve the
answer. The \emph{facts} of $\mathcal U$ are its recorded equations
$\rem(x,y)=z$ (\emph{remainder facts}) and test values
$\eq_c(x)=\mathrm{tt}$ or $\mathrm{ff}$ (\emph{test facts}); together they
form the \emph{diagram} of $\mathcal U$. The remainder equations of a
derivation form a finite partial substructure generated by the inputs;
Proposition~\ref{prop:certificates} adds the test facts that make it a
certificate. The \emph{intrinsic remainder-call complexity} $\calls_{\rem}(\mathcal A,f,\vec x)$ is the least
number of remainder facts in a certificate
\cite[\S\S1D, 4C--4E]{moschovakis2019}.

The following lemma lets us treat certificates as finite sets of facts and
extract a derivation from any certificate; it is used in
Proposition~\ref{prop:certificates}. It also justifies the fact-based Lean
encoding, for which Lean proves the resulting equality of intrinsic
complexities (Appendix~\ref{app:lean}).

\begin{lemma}[Fact representation]\label{lem:fact-representation}
Let $F$ be a finite set of true remainder and test facts in which every
number is generated from $a,b$ by the remainder facts of $F$. Then $F$ is
the diagram of a finite partial substructure generated by $a,b$ (of
$\mathcal N_\varepsilon$, or of $\mathcal N_0$ if $F$ has no $\eq_1$
facts), and every such substructure arises in this way. A map
$\pi:\mathbb N\to\mathbb N$ preserves the facts of $F$ exactly when its
restriction to the universe is a homomorphism, and every homomorphism
extends to such a map. Every element of the universe is available after
a derivation from $a,b$ with at most as many instructions as $F$ has
remainder facts.
\end{lemma}
\begin{proof}
Take the universe $V$ to consist of $a,b$ and the numbers occurring in $F$,
and interpret each primitive only at the recorded arguments, with the
recorded value. Truth of the facts makes these partial operations and
tests restrictions of the primitives of $\mathbb N$, and the hypothesis says that $V$ is generated by
$a,b$. Conversely, the diagram of a finite generated partial substructure is
such a set $F$. A homomorphism need only respect the recorded operations and
tests on $V$, and values outside $V$ are irrelevant; this gives the second
assertion. For the last, start from $a,b$ and repeatedly apply a remainder
fact of $F$ whose operands are available and whose value is new. While some
element of $V$ is unavailable such a fact exists: take the first
unavailable value in a sequence of remainder facts of $F$ that generates
that element. Each fact is applied at
most once.
\end{proof}

\begin{proposition}\label{prop:certificates}
For coprime $a,b\geq1$,
$\calls_{\rem}(\mathcal N_\varepsilon,\coprime,a,b)=G(a,b)$. For
$(a,b)\neq(0,0)$,
\[
G(a,b)\leq\calls_{\rem}(\mathcal N_0,\gcd,a,b)\leq G(a,b)+2,
\]
and the same bounds hold for $\calls_{\rem}(\mathcal N_\varepsilon,\gcd,a,b)$.
\end{proposition}
\begin{proof}
A derivation of $1$, together with $\eq_1(1)=\mathrm{tt}$,
$\eq_0(a)=\mathrm{ff}$ and $\eq_0(b)=\mathrm{ff}$, certifies $\coprime$: under
any homomorphism the input images are positive, and every common divisor of
them divides the image of every generated value, hence divides $\pi(1)$,
which is $1$ because the fact $\eq_1(1)=\mathrm{tt}$ is preserved.
Conversely, if a certificate records no fact $\eq_1(x)=\mathrm{tt}$, then
$x\mapsto2x$ preserves its remainder facts and all its other test facts,
but not coprimeness. So every certificate contains $1$, and
Lemma~\ref{lem:fact-representation} gives a derivation of $1$ with at
most as many instructions as the certificate has remainder facts. This
proves the first assertion.

For gcd as a function, the certificate must reach its output $g$, giving a
lower bound of $G(a,b)$. For an upper bound, append
\[
\rem(a,g)=0,\qquad \rem(b,g)=0,\qquad \eq_0(0)=\mathrm{tt}.
\]
Every homomorphism $\pi$ has $\pi(0)=0$ and
$\pi(g)>0$ (by definedness of either appended remainder). Thus $\pi(g)$
divides both input images. Conversely every common divisor of those images
divides $\pi(g)$ by induction over the derivation. This proves the bounds
for $\mathcal N_0$. In $\mathcal N_\varepsilon$ the lower-bound argument is
unchanged, and every certificate in $\mathcal N_0$ is also one in
$\mathcal N_\varepsilon$, so both bounds transfer to
$\calls_{\rem}(\mathcal N_\varepsilon,\gcd,a,b)$.
\end{proof}
\begin{remark}\label{rem:noncoprime}
\begin{enumerate}
\item At $(0,0)$ the output is an input, and the substructure with universe
$\{0\}$ and no facts is a certificate.
\item For gcd restricted to positive inputs, appending $\eq_0(a)=\mathrm{ff}$
and $\eq_0(b)=\mathrm{ff}$ keeps input images in the domain, at no
remainder cost.
\item For a positive noncoprime input, adding $\eq_1(g)=\mathrm{ff}$ to the
gcd certificate certifies noncoprimeness. So the sublogarithmic bound holds
for both truth values of coprimeness, and since each overhead is a fixed
additive constant, Corollary~\ref{cor:three} holds for all three complexities
of Corollary~\ref{cor:refute} below on positive inputs.
\end{enumerate}
\end{remark}

\paragraph{The conjectures refuted.}
Moschovakis's 2012 notes state:
\begin{quote}
\textbf{Conjecture 3.4} \cite[p.~19]{moschovakis2012}. There is a rational number
$r>0$ such that for infinitely many $a\geq b\geq1$,
$\calls_{\rem}(\mathcal N_\varepsilon,\coprime,a,b)\geq r\log a$.
\end{quote}
The book formulates one precise version of the Main Conjecture
\cite[p.~151]{moschovakis2019}: there are a set $\mathcal D\subseteq\mathbb N^2$
and a $K>0$ such that
\[
(x,y)\in\mathcal D\ \Longrightarrow\
\calls_{\rem}(\mathrm{Eucl},x,y)\leq L(x,y)\leq K\calls_{\rem}(\mathcal A,\gcd,x,y),
\tag{4F-5}
\]
where $L(x,y)=2\log\max(x,y)$ for $(x,y)\neq(0,0)$, $L(0,0)=0$, and
$\calls_{\rem}(\mathrm{Eucl},x,y)$ counts
the remainder calls of the Euclidean algorithm $\mathrm{Eucl}$ (the book writes
$\varepsilon$) on $(x,y)$. The book states (4F-5) for the Euclidean algorithm
in $\mathbf N_\varepsilon$, so its $\mathcal A$ is $\mathcal N_\varepsilon$;
we treat both $\mathcal A=\mathcal N_\varepsilon$ and $\mathcal A=\mathcal N_0$.
The book adds that $\mathcal D$ then satisfies its conditions (4F-3) and
(4F-4); the latter makes the intrinsic complexity unbounded on $\mathcal D$,
so $\mathcal D$ is infinite (for finite $\mathcal D$ the statement is
trivial). We refute the weaker statement obtained by dropping the first
inequality and requiring only that $\mathcal D$ be infinite.

\begin{corollary}\label{cor:refute}
The intrinsic complexities
\[
\calls_{\rem}(\mathcal N_\varepsilon,\coprime,a,b),\qquad
\calls_{\rem}(\mathcal N_0,\gcd,a,b),\qquad
\calls_{\rem}(\mathcal N_\varepsilon,\gcd,a,b)
\]
are $O(\log a/\log\log a)$, uniformly in $1\leq b\leq a$. Consequently Conjecture~3.4 of
\cite{moschovakis2012} is false, and so is the version (4F-5) of the Main
Conjecture with $\mathcal A=\mathcal N_0$ or $\mathcal A=\mathcal N_\varepsilon$:
for every $r>0$ only finitely many pairs $a\geq b\geq1$ satisfy
$\calls_{\rem}(\mathcal N_\varepsilon,\coprime,a,b)\geq r\log a$, and for every
$K>0$ only finitely many pairs $(x,y)\in\mathbb N^2$ satisfy
$L(x,y)\leq K\calls_{\rem}(\mathcal A,\gcd,x,y)$.
\end{corollary}
\begin{proof}
By Theorem~\ref{thm:main}, Proposition~\ref{prop:certificates} and
Remark~\ref{rem:noncoprime}, each complexity is at most $G(a,b)+2$ on
positive inputs, which gives the first assertion; the refutations follow
since $\log a/\log\log a=o(\log a)$. For (4F-5), symmetry covers $x<y$, and
pairs with a zero entry need no remainder facts.
\end{proof}

\paragraph{A single uniform process.}
The book's best-uniform-process theorem (Theorem~4F.1) states that,
whenever every input has a certificate,
one uniform process attains the intrinsic complexity at every input
\cite[pp.~149--150]{moschovakis2019}.

\begin{corollary}\label{cor:uniform}
For each of gcd and coprimeness, there is a single uniform process of
$\mathcal N_\varepsilon$ computing it on $\mathbb N^2$ with
$O(\log a/\log\log a)$ remainder calls, uniformly in $1\leq b\leq a$.
The gcd process can also be taken over $\mathcal N_0$.
\end{corollary}
\begin{proof}
Corollary~\ref{cor:refute} bounds the intrinsic complexities, and by
Theorem~4F.1 one process attains them at every input. Every input has a
certificate (symmetry covers reversed inputs, and a zero-test fact
suffices when either input is zero), so this process is defined on all of
$\mathbb N^2$.
\end{proof}
The corollary rules out the possibility raised after Corollary~6C.7 of the
book that the Main Conjecture holds for all uniform processes of
$\mathcal N_\varepsilon$ \cite[p.~188]{moschovakis2019}.

\paragraph{The limit of the homomorphism method.}\label{par:method}
The Homomorphism Test proves lower bounds on intrinsic complexity by
showing that every generated diagram below the proposed cost admits a
homomorphism that fails to preserve the answer
\cite[Lemma~4E.3]{moschovakis2019}. Such bounds apply to every uniform
process computing the function, hence to every recursive program
\cite[Proposition~4E.1, Corollary~4E.2]{moschovakis2019}.
By Corollary~\ref{cor:refute}, no lower bound on the intrinsic complexities
listed there can grow faster than $\log a/\log\log a$, so a logarithmic lower bound
for algorithms must use properties of programs not shared by all uniform
processes, such as finite program
syntax or determinism.

\section{An almost-all lower bound}\label{sec:loglog}
The difficult pairs of \cite[Theorem~6C.5]{moschovakis2019} give
$\Omega(\log\log a)$ on a sparse set. An elementary Diophantine argument gives
the same order for almost all coprime pairs. Write each generated value as
$ua+wb$. On the $B$-regular pairs defined below, small coefficients cannot give
a small positive value, and each remainder call at most squares the
coefficient bound, up to a factor $2B$. Reaching $1$ therefore takes about
$\log\log a$ calls, except on a sparse set of pairs.

\begin{proposition}\label{prop:loglog}
For integers $d\geq1$ and $N\geq3$, at most
$40(2+\ln N)N^{2-2^{-d}}$ coprime pairs $2\leq b<a\leq N$ satisfy
$G(a,b)\leq d$. Hence, for each fixed $\varepsilon>0$, all but $o(N^2)$ of
these pairs satisfy $G(a,b)>(1-\varepsilon)\log\log N$.
\end{proposition}

\begin{proof}
For $B\geq1$ call $(a,b)$ \emph{$B$-regular} if
$|qb-pa|\geq a/(Bq)$ whenever $q\in\mathbb N$, $q\geq1$,
$p\in\mathbb Z$ and $qb\neq pa$. We first bound the cost on regular
pairs, then count the irregular ones.

Every generated value has an integer representation $v=ua+wb$.
On a regular pair, $v>0$ implies $v\geq a/(B(|u|+|w|))$:
for $w\neq0$ use regularity with $q=|w|$, and for $w=0$ note $v\geq a$.
Let $H_t$ bound the coefficient norm $|u|+|w|$ in one such representation
of each value available after $t$ instructions, starting with $H_0=1$.
In an instruction $r=\rem(x,y)$, write $x=sy+r$. Since generated values
are at most $a$, the quotient satisfies $s\leq a/y\leq BH_t$.
Subtracting $s$ times the representation of $y$ from that of $x$ gives
\[
H_{t+1}\leq H_t+BH_t^2\leq2BH_t^2,\qquad
H_t\leq(2B)^{2^t-1}.
\]
Producing $1$ within $d$ instructions therefore forces
\[
1\geq\frac{a}{BH_d},\qquad a\leq\frac{(2B)^{2^d}}2.
\]

To count irregular pairs below $N$, choose a witness
$0<|qb-pa|<a/(Bq)$. Dividing $p,q$ by their gcd preserves this inequality,
so assume $\gcd(p,q)=1$. The nonzero integer $e=qb-pa$ then gives
$q<a/B\leq N/B$ and $0\leq p\leq q$ (as $pa=qb-e$ with $0<b<a$ and
$|e|<a$).
For each $q$, there are at most $2q$ choices of $p$ and $2N/(Bq)$ choices
of the signed integer $e$. Given $p,q,e$, the equation
$pa\equiv-e\pmod q$ determines one residue class for $a$, leaving at most
$N/q+1$ choices; $b$ is then determined. With $Q=\lfloor N/B\rfloor$,
the number of irregular pairs is at most
\[
\begin{aligned}
\sum_{q=1}^{Q}(2q)\frac{2N}{Bq}\left(\frac Nq+1\right)
 &=\frac{4N^2}{B}\sum_{q=1}^{Q}\frac1q+\frac{4NQ}{B}\\
 &\leq\frac{4N^2}{B}(2+\ln N),
\end{aligned}
\]
using $Q\leq N$, $B\geq1$, and the harmonic-sum bound; an empty sum is zero.

Now split into dyadic ranges $X/2<a\leq X$, and take
$B=X^{2^{-d}}/2$. If $B\geq1$, a regular pair with $G\leq d$ would have
$a\leq X/2$, so all such pairs in the range are irregular. Their number is
at most $8(2+\ln X)X^{2-2^{-d}}$.
When $B<1$, the same bound follows from the trivial bound $X^2$, since
$X^{2^{-d}}<2$.
Put $s=2-2^{-d}\geq3/2$. Summing over the nonempty ranges with
$X=N/2^j\geq3$, and bounding their logarithmic factors by $2+\ln N$, gives
\[
8(2+\ln N)N^s\sum_{j\geq0}2^{-js}
 =\frac{8}{1-2^{-s}}(2+\ln N)N^s
 \leq40(2+\ln N)N^s.
\]
(The factor is below $13$; we state $40$, the constant proved in Lean,
which bounds each pair separately; see Appendix~\ref{app:lean}.)
For the second assertion, take
$d=\lfloor\log\ln N-2\log\ln\ln N\rfloor$ for sufficiently large $N$
(with $\log$ to base $2$ and $\ln$ natural).
Then $N^{-2^{-d}}\leq\exp(-(\ln\ln N)^2)$, so the exceptional set has
size $o(N^2)$, while $d=(1-o(1))\log\log N$, so eventually
$d\geq(1-\varepsilon)\log\log N$.
\end{proof}
Since there are asymptotically $3N^2/\pi^2$ coprime pairs
$2\leq b<a\leq N$, the exceptional set has density zero among them.
The saving $2^{-d}$ in the exponent of $N^{2-2^{-d}}$ shrinks as $d$ grows,
so this argument does not reach the upper-bound scale $\log N/\log\log N$.

\section{Fixed programs with arbitrarily small coefficients}\label{sec:programs}

For a nondeterministic program $P$, let $c_P(a,b)$ be the minimum number of
remainder calls among its convergent computations. We require at least one
such computation on each input and require every convergent computation to
return the gcd. These are the conventions of
\cite[(2E-2), (2E-5)]{moschovakis2019}.

A \emph{register program} keeps its values in a fixed number of registers
and executes assignments $x_l:=E$, branches on a test $E$, and a halt
returning $E$, where each $E$ is a term in the registers; the
nondeterministic version allows several commands at a line
\cite[\S\S2E--2F]{moschovakis2019}. It is an iterator, so it uses no
recursion stack, and in pointed structures register programs compute
exactly the tail-recursive functions \cite[Proposition~2F.1]{moschovakis2019}.

\begin{theorem}\label{thm:registers}
For each integer $p\geq1$, there is a finite nondeterministic register
program $P_p$ over $\mathcal N_0$ with $3\cdot2^p+6$ registers that computes the
gcd and satisfies
\[
\limsup_{a\to\infty}\ \max_{1\leq b\leq a}\frac{c_{P_p}(a,b)}{\log a}\leq\frac3p.
\]
Consequently, for every $\varepsilon>0$ there are a fixed register program
$P$ and a constant $B\geq0$ such that
\[
\forall a\geq b\geq1,\qquad c_P(a,b)\leq\varepsilon\log a+B.
\]
\end{theorem}

\begin{proof}
Put $k=2^p$, $h=3k$ and $W=h+6$: two inputs, $h+1$ prefix values, a
modulus and two scratch registers. Initialise the registers
$x_0,\ldots,x_{W-1}$ at $(a,b,a,b,a,\ldots,a)$. If $b=0$, return $a$;
otherwise enter the main line. There the program
may perform any assignment $x_l:=\rem(x_i,x_j)$ with $i,j,l\geq2$, or pass to
verification with a candidate $x_i\neq0$, $i\geq2$. Verification sets
$x_0:=\rem(x_0,x_i)$ and $x_1:=\rem(x_1,x_i)$, halts with $x_i$ if both are
$0$, and loops otherwise; the main line never writes $x_0,x_1$. Every register value is
divisible by $\gcd(a,b)$, so a candidate that passes verification is the
gcd, and Euclid's algorithm gives a convergent computation. The computations
below move values between registers for readability; copying is never needed
(Appendix~\ref{app:lean}).

Multiplying every value by $g=\gcd(a,b)$ turns a computation on
$(a/g,b/g)$ into one on $(a,b)$ with the same remainder count, so it
suffices to treat coprime pairs. Let $S(n)$ be the maximum, over coprime
$1\leq b\leq a\leq2^n$ and over states with $a,b$ in two work registers,
of the least number of remainder calls with which main-line moves of $P_p$
place $1$ in a work register. Fix $0<\beta<1/2$ and put $\alpha=1-\beta/2$ and $N=2^n$.

Compute the Euclidean remainders $r_0=a,r_1=b,r_2,\ldots$ in working
registers, stopping at $r_h$ or at the first $r_j\leq N^\alpha$.
If $1$ has been reached, no further generation is needed. In the remaining early case,
one further remainder gives the positive coprime pair $r_j,r_{j+1}$,
bounded by $N^\alpha$, at total cost at most $h$; continue with that pair,
in the same registers. This restart needs no stack, but the two recursive
derivations of Phase~(iii) in Section~\ref{sec:construction} would, so the
final step below uses Euclid's algorithm instead.
Otherwise $r_h>N^\alpha$. As in the late case of Corollary~\ref{cor:three}, now
with $p$ fixed, the prefix lemma applies to every modulus above $N^\beta$
for large $n$, and by \eqref{eq:contract} at
most $\lceil n/p\rceil$ contractions, using a modulus register and two
scratch registers, produce a positive $m\leq N^\beta$. Then put
$u=\rem(a,m)$ and $v=\rem(b,m)$, and run Euclid's algorithm in place on $m,u$
and then on the result $d$ and $v$. Each run takes at most $2\log m+3$
calls, and the result is $\gcd(d,v)=\gcd(m,a,b)=1$. Thus, eventually in $n$,
\[
S(n)\leq\max\left\{S(\lceil\alpha n\rceil)+h,\quad
 h+3\lceil n/p\rceil+4\beta n+7\right\}.
\]
Let $\Lambda=\limsup_{n\to\infty}S(n)/n$, which is finite since Euclid gives
$S(n)=O(n)$. Passing to upper limits, $\Lambda$ satisfies
$\Lambda\leq\max\{\alpha\Lambda,\ 3/p+4\beta\}$, and since $\alpha<1$,
$\Lambda\leq3/p+4\beta$. The program does not depend on $\beta$, so
$\Lambda\leq3/p$. Take $n=\lceil\log a\rceil$ and add the two verification
calls. Finally, choose $p>3/\varepsilon$ and absorb the finitely many
smaller inputs in $B$.
\end{proof}
The program depends on $\varepsilon$ but not on the inputs. The Main
Conjecture lets its coefficient $r$ depend on the program, so the family is
consistent with it; no single sublogarithmic program is obtained.

\paragraph{Recursive programs.}
Theorem~\ref{thm:registers} also holds for the book's recursive programs:
writing one function per line of $P_p$ yields a finite nondeterministic
tail-recursive program with the same remainder cost
\cite[\S\S2A, 2C, 2E]{moschovakis2019}.
Lean verifies this translation for every register program on its model of
the book's recursive machine, a specialisation of the book's Table~1, and
proves an input-independent bound on the stacks (Appendix~\ref{app:lean}).

\section{Discussion and open problems}\label{sec:discussion}
\paragraph{The gap.}
The intrinsic complexity of coprimeness in $\mathcal N_\varepsilon$ is
$\Omega(\log\log a)$ on almost all coprime pairs and $O(\log a/\log\log a)$
on all positive pairs. Closing this gap is open;
unlike Bshouty's bound in his model, our upper bound is not known to be
optimal.

\paragraph{One program.}
For this construction, an obstacle to one sublogarithmic program is reusable
access to a prefix whose length grows with the input. A nondeterministic
program can guess the close pair, but it must hold all $h+1$ prefix values;
regenerating them would cost about $h$ calls per contraction. By
Theorem~\ref{thm:registers}, $W=3\cdot2^p+6$ registers give coefficient
$3/p$, roughly $3/\log W$, so no lower bound $c\log a$ with $c>0$ independent of
the number of registers holds for nondeterministic register programs. A register
program has only a fixed number of slots for prefix values. Does every
nondeterministic register program computing gcd with $W$ registers make at
least $c\log a/\log W$ remainder calls on infinitely many inputs, for an
absolute $c>0$? Such a bound cannot rest on how quickly values shrink,
since $\rem(m+1,m)=1$. Pratt's algorithm is itself a nondeterministic
register program \cite[Theorem~2E.2]{moschovakis2019}; compare also the
book's question whether recursion reduces to tail recursion in the pointed
Euclidean structure \cite[Problem~x2G.6]{moschovakis2019}.

Recursion permits unbounded saved state, but does not directly provide
reusable access to an arbitrarily long prefix. Can one fixed recursive
program retain and repeatedly access a growing prefix at the same remainder
cost? Every certificate becomes a computation of some program
\cite[Proposition~2E.1]{moschovakis2019}, but not of one program for all
certificates.

\paragraph{Stronger lower-bound methods.}
The limit established in Section~\ref{sec:certificates} leaves room for
arguments combining homomorphisms with additional restrictions on
computations. In particular, the conjecture of a logarithmic lower bound
for deterministic uniform processes remains open
\cite[Conjecture~3.9, p.~23]{moschovakis2012},
\cite[\S4H and p.~188]{moschovakis2019}.

\section{Computational checks}\label{sec:checks}
The Python planner in the accompanying
repository\footnote{\url{https://github.com/jasondavies/euclid-uniform-processes};
this paper describes release \texttt{v1.0}.}
chooses instructions offline with unrestricted arithmetic, using the
parameters of Theorem~\ref{thm:main} from Section~\ref{sec:construction};
below a base size (256 bits by default) it uses Euclid's algorithm. A separate replay script then checks
operand availability, nonzero divisors, every remainder equation and the
final gcd.

A benchmark script samples $25$ coprime pairs at each size: $a$ is uniform among
integers of that bit length, and $b$ is drawn uniformly from
$\{2,\ldots,a-1\}$ until $\gcd(a,b)=1$. It also runs the successive
Fibonacci pair $(F_k,F_{k-1})$ with $F_k$ the first Fibonacci number of
that bit length. The table gives remainder calls;
the Euclidean count stops when $1$ first appears.
\begin{center}
\small
\begin{tabular}{rcccc}\toprule
 & \multicolumn{2}{c}{Random pairs: min / median / max}
 & \multicolumn{2}{c}{Fibonacci pair}\\
\cmidrule(lr){2-3}\cmidrule(l){4-5}
Input bits & Construction & Euclid & Construction & Euclid\\\midrule
512 & 193 / 210 / 228 & 266 / 295 / 337 & 53 & 735\\
2048 & 612 / 626 / 644 & 1136 / 1192 / 1260 & 106 & 2948\\
8192 & 1918 / 1957 / 1985 & 4664 / 4774 / 4890 & 212 & 11798\\\bottomrule
\end{tabular}
\end{center}
All $78$ derivations and the example of Section~\ref{sec:contractions} pass
replay. On the Fibonacci pairs, Euclid's worst case, the bits
removed by successive contractions roughly double (32, 66, 131 and 248
at 512 bits), so few contractions are needed. These samples illustrate the construction; the
asymptotic claim rests on the proof. With the parameters of
Corollary~\ref{cor:three} and $c$ near $1$, the prefix exceeds the whole Euclidean sequence at these sizes, so the
coefficient $3$ is asymptotic only. The
accompanying repository also checks scaled and noncoprime inputs, rejects invalid traces, and tests the prefix
lemma over a finite range. The repository README gives scripts, commands,
test ranges, seeds and individual results. The Python checks are not formally verified;
the unrestricted arithmetic used to plan instructions is outside the
derivations.

\appendix
\section{Formal verification}\label{app:lean}
The development uses Lean~4.35.0 \cite{deMouraUllrich2021} with mathlib
\cite{mathlib2020} at its v4.35.0 tag; the pinned mathlib commit is
\texttt{56a005855ea17e0b0958f73ec801ae140b0a1679}.
The proved library contains no proof placeholders or added axioms; the axiom audit
reports only \texttt{propext}, \texttt{Classical.choice}, and
\texttt{Quot.sound}. Table~\ref{tab:lean} gives the main declarations;
the repository README gives the
complete map and reproduction commands.
The general theory of uniform processes, including Theorem~4F.1 used in
Corollary~\ref{cor:uniform}, and the historical lower bounds are cited,
not formalised. The certificate bounds and conjecture refutations are
formalised independently of that theory, with certificates represented by
their facts. The consequence of Lemma~\ref{lem:fact-representation} that we
use, equality of the book-style and fact-based complexities, is formalised
too: Lean
states the book's definitions for $\mathcal N_\varepsilon$ and
$\mathcal N_0$ directly (finite partial substructures with partial
operations, generation, homomorphisms on the universe, certification and
the norm $\calls_{\rem}$) and proves that the resulting intrinsic
complexities equal the fact-based ones used in the refutations.
Corollary~\ref{cor:closure-depth} is formalised with
the source's definitions of $\operatorname{iq}$, $\rem$ and the closure
stages, including their conventions at zero divisors.

The development is also packaged for the comparator of the Palomar
registry: \texttt{Challenge.lean} imports only mathlib and states the main
theorems with every definition visible and deliberate \texttt{sorry}
placeholders, and \texttt{Solution.lean} imports the proved library,
independently of these placeholders. The comparator checks that the proved
statements are exactly those of \texttt{Challenge.lean} and replays the
proofs through Lean's kernel and the independent kernels NanoDa and con-ron;
we ran it on release \texttt{v1.0} of the repository.
\texttt{comparator.json} lists all twenty-two compared theorems, including
that $G$ and the closure depth are attained (\lean{generates_G},
\lean{ClosureDepth.depth_mem}), so the bounds on them are not about empty
infima; Table~\ref{tab:lean} marks those included here with ${}^\dagger$.
Version~2 of the Palomar registry entry PALOMAR-2026-10-23-000012
\cite{palomar2026} records this verification for release \texttt{v1.0}
(commit \texttt{2548681}), covering all twenty-two compared theorems.

\paragraph{Arithmetic bounds.}
Costs are lengths of explicit remainder derivations. The finite theorem
\lean{sizeCost_step} proves the recurrence from natural-number size
parameters; it does not assume a recurrence for the cost function.
For the initial Big-O proof, Lean uses the parameters of
Section~\ref{sec:construction}, computing $p$ as
$\lfloor\lfloor\log n\rfloor/2\rfloor$, which equals $\lfloor(\log n)/2\rfloor$,
and checks the integer rounding estimates before passing to real
logarithms. The refinement uses the
tunable parameters of Corollary~\ref{cor:three} and checks the rounding limits
preserving coefficient $3$.
For Proposition~\ref{prop:loglog}, Lean takes $B=a^{2^{-d}}/2$ separately
for each pair instead of splitting into dyadic ranges. It proves the
stated constant $40$ and the exceptional-set limit for every fixed
$0<\varepsilon\leq1$ (larger $\varepsilon$ are trivial), with threshold
$(1-\varepsilon)\log\log N$.

\paragraph{Programs and machine computations.}
For Theorem~\ref{thm:registers}, Lean defines the book's register programs
over $\mathcal N_0$ (\lean{Register.Program}): lines numbered from $0$, each
a halt or a list of alternative assignments and branchings, with the book's
prime terms $x_i$, $\rem(x_i,x_j)$, $\mathrm{tt}$, $\mathrm{ff}$ and
$\eq_0(x_i)$, and the book's iterator semantics, in which $\rem(x,0)$ is
undefined. The program $P_p$ is written in this syntax
(\lean{TailSource.program}), with no stack, and each remainder evaluation is
charged once, including the two verification calls. Every convergent
execution returns the gcd, and one exists on every input. The cost proofs use a generator that may also
relabel all registers at once. \lean{TailSource.run_trace_relabel} replays
such runs by single-register commands at the same cost and with no extra
registers: it tracks the relabelling in the proof, and writes each new
remainder to a register no other value occupies, which exists by
pigeonhole whenever two names share a register.

The tail-recursive form (\lean{TailRecursive}) compiles the register program
into a language of nondeterministic first-order programs (\lean{Recursive}):
terms with variables, remainder, a zero-test conditional and calls of
internal symbols, each symbol with a set of alternative bodies, evaluated
call by value. The compiler (\lean{Register.compile}) follows the book's
reduction of iteration to tail recursion \cite[\S2C]{moschovakis2019}: each
line becomes a function of the $W$ registers, an assignment a tail call with
one argument replaced, a branching on $\eq_0(x_i)$ a zero-test conditional
between two tail calls and one on $\mathrm{tt}$ or $\mathrm{ff}$ a single tail
call, a halt its term, and alternative commands alternative bodies. For
every register program, \lean{Register.eval_iff_halts} matches evaluations
exactly, in value and remainder cost, with convergent computations; every
call is a tail call, whose arguments, remainder operands and conditional
guards contain no internal calls (\lean{Register.compile_tailRecursive});
and the machine's control and value stacks never hold more than $2W+4$
entries in all, on any input and however long the computation runs
(\lean{Register.stacks_bounded}). For Theorem~\ref{thm:registers}, $W=3\cdot2^p+6$,
so the stacks never exceed $6\cdot2^p+16$ entries
(\lean{TailRecursive.stacks_bounded}); each closure environment has at most
$W$ entries. For
every program in the language, \lean{Recursive.Machine.eval_iff_steps}
proves exact-cost equivalence with a specialisation of the book's two-stack
machine: arguments are evaluated right to left, zero tests and branches are
separate transitions, and only remainder transitions are charged
\cite[Table~1, p.~75]{moschovakis2019}. Closures represent
substitution in machine states, not extra program data.

\begin{table}[!h]
\centering\small
\caption{Main results and Lean declarations, all in the namespace \texttt{ShortGCD}. Names marked ${}^\dagger$ are compared against \texttt{Challenge.lean}.}
\label{tab:lean}
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.29\textwidth}>{\raggedright\arraybackslash}p{0.67\textwidth}@{}}
\toprule
Paper & Lean declaration(s)\\\midrule
Theorem~\ref{thm:main} & \lean{uniform_real_bound}, \lean{generates_G}${}^\dagger$\\
Normalisation \eqref{eq:normalize} & \lean{G_normalize}\\
Lemma~\ref{lem:gap} & \lean{small_remainder}\\
Lemma~\ref{lem:prefix} & \lean{prefix_class_card_le_three}, \lean{residue_card_three}; for \eqref{eq:contract}, \lean{prefix_reservoir}\\
Lemma~\ref{lem:fact-representation} (consequence used) & \lean{Book.callsCoprimeness_eq}${}^\dagger$,
\lean{Book.callsRemGcd_eq}${}^\dagger$, \lean{Book.callsGcd_eq}${}^\dagger$\\
Corollary~\ref{cor:three} & \lean{uniform_real_bound_three}${}^\dagger$, \lean{uniform_intrinsic_bound_three}${}^\dagger$\\
Proposition~\ref{prop:certificates} &
\lean{callsGcd_le}, \lean{callsGcd_zero_left}, \lean{callsRemGcd_le_callsGcd},
\lean{exists_certifiesGcd}${}^\dagger$, \lean{G_le_callsRemGcd}${}^\dagger$,
\lean{G_le_callsGcd}${}^\dagger$, \lean{callsCoprimeness_eq_G}${}^\dagger$\\
Remark~\ref{rem:noncoprime} & \lean{callsCoprimeness_le}, \lean{exists_certifiesCoprimeness}${}^\dagger$\\
Corollary~\ref{cor:refute} &
\lean{not_conjecture_3_4}${}^\dagger$, \lean{not_main_conjecture_4F5}${}^\dagger$,
\lean{not_main_conjecture_4F5_Neps}${}^\dagger$, and the literal readings
\lean{not_conjecture_3_4_literal}${}^\dagger$,
\lean{not_main_conjecture_4F5_literal}${}^\dagger$\\
Corollary~\ref{cor:uniform} & Cited Theorem~4F.1; not formalised here\\
Corollary~\ref{cor:closure-depth} & \lean{ClosureDepth.depth_le}, \lean{ClosureDepth.depth_mem}${}^\dagger$,
\lean{ClosureDepth.depth_bound}, \lean{ClosureDepth.no_logarithmic_sequences}${}^\dagger$\\
Proposition~\ref{prop:loglog} & \lean{AlmostAll.card_D_le}, \lean{G_eq_D},
\lean{tendsto_card_callsCoprimeness_loglog}${}^\dagger$\\
Theorem~\ref{thm:registers} &
\lean{TailProgram.Fixed.limsup_profile_le},
\lean{TailProgram.Fixed.eventually_accepts_bound}, \lean{TailSource.executes_iff},
\lean{TailSource.total_registers},
\lean{TailSource.executes_correct}${}^\dagger$,
\lean{TailSource.executes_total}${}^\dagger$,
\lean{TailSource.arbitrarily_small_coefficient}${}^\dagger$\\
Recursive programs (Section~\ref{sec:programs}) &
\lean{TailRecursive.program_tailRecursive},
\lean{TailRecursive.stacks_bounded},
\lean{TailRecursive.executes_iff_steps},
\lean{TailRecursive.arbitrarily_small_coefficient}\\
\bottomrule
\end{tabular}
\end{table}

\section*{Acknowledgements}
I thank Shubhendu Trivedi for helpful comments.

\section*{Declaration of AI-generated research and authorship}
This manuscript is the product of an AI-driven research process. During a
broader investigation initiated by the human author, an AI system,
GPT-6-Astra, identified the principal result. The author then directed AI
systems to formalise the results in Lean and to prepare this manuscript. The
AI systems developed the results and their presentation, including the
mathematical exposition, the formalisation, and the organisation and writing
of the text; the human author wrote no part of the manuscript. The systems
were GPT-6-Astra (OpenAI), used through Codex, and Claude Opus~5.5
(Anthropic), used through Claude Code. Both contributed to the Lean
formalisation and to the review and revision of the manuscript.

The Lean development gives a machine-checkable version of the main claims.
Lean's kernel checks the proofs, including the mathlib results they use,
relative to the axioms listed in Appendix~\ref{app:lean}. That includes the
equality of the book-style and fact-based complexities, the consequence of
Lemma~\ref{lem:fact-representation} that we use; the book's general
theory of uniform processes, used through the cited Theorem~4F.1, is not
formalised.

The human author has checked the arguments and takes full responsibility
for the content of this paper, including the correctness of its
mathematics, and for the accuracy of this disclosure.

\begin{thebibliography}{10}
\raggedright
\bibitem{bshouty1989}
Nader H. Bshouty.
\emph{Euclidean GCD algorithm is not optimal}.
Research Report 1989-376-38, Department of Computer Science, University of
Calgary, December 1989.
\href{https://doi.org/10.11575/PRISM/30475}{doi:10.11575/\allowbreak PRISM/30475}.

\bibitem{chorgoldreich1990}
Benny Chor and Oded Goldreich.
An improved parallel algorithm for integer GCD.
\emph{Algorithmica} 5(1--4):1--10, 1990.
\href{https://doi.org/10.1007/BF01840374}{doi:10.1007/BF01840374}.

\bibitem{deMouraUllrich2021}
Leonardo de Moura and Sebastian Ullrich.
The Lean~4 theorem prover and programming language.
In \emph{Automated Deduction -- CADE~28}, Lecture Notes in Computer Science,
vol.~12699, pp.~625--635. Springer, 2021.
\href{https://doi.org/10.1007/978-3-030-79876-5_37}{doi:10.1007/978-3-030-79876-5\_37}.

\bibitem{kmr1987}
Ravindran Kannan, Gary Miller and Larry Rudolph.
Sublinear parallel algorithm for computing the greatest common divisor of
two integers.
\emph{SIAM Journal on Computing} 16(1):7--16, 1987.
\href{https://doi.org/10.1137/0216002}{doi:10.1137/0216002}.

\bibitem{knuth1997}
Donald E. Knuth.
\emph{The Art of Computer Programming, Vol.~2: Seminumerical Algorithms}, 3rd
ed. Addison-Wesley, Reading, MA, 1997.

\bibitem{mst1991a}
Yishay Mansour, Baruch Schieber and Prasoon Tiwari.
A lower bound for integer greatest common divisor computations.
\emph{Journal of the ACM} 38(2):453--471, 1991.
\href{https://doi.org/10.1145/103516.103522}{doi:10.1145/103516.103522}.

\bibitem{mst1991b}
Yishay Mansour, Baruch Schieber and Prasoon Tiwari.
Lower bounds for computations with the floor operation.
\emph{SIAM Journal on Computing} 20(2):315--327, 1991.
\href{https://doi.org/10.1137/0220020}{doi:10.1137/0220020}.

\bibitem{mathlib2020}
The mathlib Community.
The Lean mathematical library.
In \emph{Proceedings of the 9th ACM SIGPLAN International Conference on
Certified Programs and Proofs (CPP 2020)}, pp.~367--381. ACM, 2020.
\href{https://doi.org/10.1145/3372885.3373824}{doi:10.1145/3372885.3373824}.

\bibitem{moschovakis2012}
Yiannis N. Moschovakis.
\emph{Absolute lower bounds for uniform processes}.
Unpublished lecture notes (first draft), January 25, 2012.
\url{https://www.math.ucla.edu/~ynm/nadalb.pdf}.

\bibitem{moschovakis2019}
Yiannis N. Moschovakis.
\emph{Abstract Recursion and Intrinsic Complexity}.
Lecture Notes in Logic, vol.~48. Cambridge University Press and Association
for Symbolic Logic, 2019.
\href{https://doi.org/10.1017/9781108234238}{doi:10.1017/9781108234238}.

\bibitem{palomar2026}
Palomar registry. Entry PALOMAR-2026-10-23-000012, version~2, for commit
\texttt{2548681} of \url{https://github.com/jasondavies/euclid-uniform-processes}.
\url{https://palomar-registry.org/entry?id=PALOMAR-2026-10-23-000012&version=2}.

\bibitem{stein1967}
J. Stein.
Computational problems associated with Racah algebra.
\emph{Journal of Computational Physics} 1(3):397--405, 1967.
\href{https://doi.org/10.1016/0021-9991(67)90047-2}{doi:10.1016/0021-9991(67)90047-2}.

\bibitem{vddm2004}
Lou van den Dries and Yiannis N. Moschovakis.
Is the Euclidean algorithm optimal among its peers?
\emph{Bulletin of Symbolic Logic} 10(3):390--418, 2004.
\href{https://doi.org/10.2178/bsl/1102022663}{doi:10.2178/bsl/1102022663}.

\bibitem{vddm2009}
Lou van den Dries and Yiannis N. Moschovakis.
Arithmetic complexity.
\emph{ACM Transactions on Computational Logic} 10(1), Article~2, 49~pp., 2009.
\href{https://doi.org/10.1145/1459010.1459012}{doi:10.1145/1459010.1459012}.
Preprint: \url{https://www.math.ucla.edu/~ynm/papers/ac.pdf}.
\end{thebibliography}
\end{document}