\subsection{From local choices to the comparison bound}\label{sec:operation-properties}

Lemmas~\ref{lem:local-routines} and~\ref{lem:anchor-selection}
supply answers and anchors for individual order-restriction DAGs. We also need these choices to preserve consistency
with all earlier answers when items move between nodes. Write
$Q(n)=n\ceil{\log n}$ for the cutoff on the transcript length
$|\mathcal T|$ in Algorithm~\ref{alg:compare}.

\begin{proposition}[Consistency and termination]\label{prop:legality}
During the first $Q(n)$ comparisons, the state has positive feasible volume,
and every represented order satisfies the transcript. Each call
terminates with at most $n+2$ refinements. The strict degree and path
bounds hold between calls.
\end{proposition}
\begin{proof}
See Appendix~\ref{app:execution}.
\end{proof}

To see Proposition~\ref{prop:legality}'s $n+2$ bound, consider one call to \texttt{Compare}.
Before it answers its query, only the two queried items can move. Once moved, an
item is isolated with interval $(0,1)$, so its density is one.
\texttt{Select} requires density greater than $2^k$ to move it again
(Lemma~\ref{lem:local-routines}), which prevents another move before the
answer. \texttt{Repair} then moves at most
$n$ items.

We next sketch why refinements are rare over a sequence of comparisons,
by tracking increases and decreases in $\log Z$.
By Lemmas~\ref{lem:local-routines} and~\ref{lem:section-volume}, each
answer loses at most $1+O(1/k)$ in $\log Z$, while a move requested by
\texttt{Select} gains more than $k$. The anchor bound~\eqref{eq:tariff}
limits each degree repair's loss to four. A path repair performs
$H=2^k$ refinements at once, but their anchors must be distinct.
The same anchor bound therefore makes the whole repair profitable,
with a total increase of at least $kH/4$ in $\log Z$, as
Section~\ref{sec:rare-refinements} proves.

Degree repairs occur at most
once per $k$ comparisons on average, since each removes $k$ comparison
arcs and each comparison inserts at most one. Because $\log Z$ starts at
zero and never exceeds zero, the gains
from the other moves require enough comparisons to offset them.
We thus obtain the following lemma.

\begin{lemma}[Refinement count]\label{lem:rare-refinements}
After $q\le Q(n)$ completed comparison calls, the total number $P$ of refinements
is at most $Cq/k$ for an absolute constant $C$.
\end{lemma}
\begin{proof}
See Section~\ref{sec:rare-refinements}.
\end{proof}

Finally, the refinement count and the anchor bound allow us to count
the total orders consistent with the transcript. Let $T_q$ be their
number after $q$ answers.

\begin{theorem}[Orders remaining after comparisons]\label{thm:fixed-stage}
For every integer $k\ge64$, the adversary with parameter $k$ is
deterministic and legal. There is a nonnegative
$\delta_k=O(\log k/k)$, independent of $n$ and the query sequence,
such that after any $q$ answers
\begin{equation}\label{eq:prefix-orders}
\log T_q\ge\log(n!)-(1+\delta_k)q.
\end{equation}
\end{theorem}
\begin{proof}
See Section~\ref{sec:potential}.
\end{proof}

When a correct sorter stops, $T_q=1$, so the theorem forces at least
$\log(n!)/(1+\delta_k)$ comparisons. Section~\ref{sec:runtime} chooses
$k$ as a function of $n$ to obtain the optimal asymptotic bound in
polynomial time.