\section{Selection guarantees and state updates}\label{app:execution}

\subsection{Rounding an anchor}\label{sec:median-search}
For a nondegenerate closed interval $J=[u,v]\subset(0,1)$, choose the
largest power-of-two spacing $h$ no greater than its length. The routine
\texttt{RoundUp} rounds $u$ up to a multiple of $h$:
\begin{equation}\label{eq:round-up}
h=2^{-r},\qquad h\le|J|<2h,\qquad
c=h\ceil{u/h}.
\end{equation}

\begin{lemma}[Rounding to a binary fraction]\label{lem:rounding}
The value $c$ returned by \textnormal{\texttt{RoundUp}}$(J)$ belongs to $J$.
Writing $c=(2i+1)/2^{m+1}$ in reduced form, it satisfies
\begin{equation}\label{eq:rounding-length}
|J|<2^{-m}.
\end{equation}
\end{lemma}
\begin{proof}
The rounded value obeys $u\le c<u+h\le v$, so $c\in J$.
The choice of spacing gives $h\le|J|<2h$.
Reduction of the fraction cannot increase its denominator, so
$m+1\le r$ and $|J|<2h\le2^{-m}$.
\end{proof}

\begin{proof}[Proof of Lemmas~\ref{lem:local-routines} and~\ref{lem:anchor-selection}]
The interval comparisons in Appendix~\ref{sec:oracle} certify lower
probability bounds. If the larger bound is at least $1/2-\eta$,
\texttt{Select} returns its answer, breaking a tie in favor of the
first queried label. On failure it rounds in the middle half of a
queried coordinate's interval. For \texttt{ChooseAnchor}, a successful
central test supplies the interval to round. On failure it too rounds
in the middle half.

For a successful central test, Lemma~\ref{lem:central-density} gives
$f_x(c)\ge 1/(16|J|)$. By Lemma~\ref{lem:rounding}, $\log f_x(c)>m-4$. For either type of failed test,
Lemma~\ref{lem:certificate-success} gives $W_x<w_*=2^{-2kB}$ for the
selected coordinate. Write $L=\log(1/W_x)>2kB$. The density estimate
\eqref{eq:fiber-lower} gives $\log f_x(c)\ge L-2B>k$ throughout the middle half.
That interval has length $W_x/2$, so $m<L+1$ by
Lemma~\ref{lem:rounding}. Thus
\[
\log f_x(c)\ge L-2B>(1-1/k)L>(1-1/k)m-4.
\]
Both intervals used for rounding lie strictly inside the coordinate's
range.
\end{proof}

\subsection{Refinement and child admission}

\begin{proof}[Proof of Lemma~\ref{lem:section-volume}]
By \eqref{eq:restriction-volume}, restriction multiplies the parent
volume by $f_x(c)$. Inserting the isolated vertex into the child replaces
$K_u$ by $K_u\times(0,1)$, which has the same volume. The ratio of the
products is therefore $f_x(c)$.
\end{proof}

\begin{lemma}[Refinement and child admission]\label{lem:admission}
Suppose the state represents only orders consistent with the transcript
and every node has positive feasible volume. An interior refinement
preserves both properties.
\end{lemma}
\begin{proof}
Take feasible positions representing any order after the move. Remove
the fresh coordinate of $x$ from the child and restore $X_x=c$ in the
parent. The parent positions satisfy the old inequalities by construction.
Keeping the other coordinates fixed, we can perturb $X_x$ slightly to
either side of $c$, since its inequalities are strict. These two old
orders place $x$ immediately before and immediately after the child
block. Both respect the transcript, so it contains no comparison between
$x$ and an item in the block. In the new order, $x$ can occur anywhere
inside that block, with its order relative to all outside items preserved.
For a new child the block was empty, and the same argument places $x$
at its former parent position. Positivity follows from
Lemma~\ref{lem:interior} and the refinement identity.
\end{proof}


A refinement can change which orders the state represents. For instance,
a move into an existing child allows interleavings inside that child
that were previously excluded. The invariant concerns consistency with
the transcript.

\subsection{Restoring the graph bounds}

\begin{lemma}[One-arc repair]\label{lem:restoration}
Suppose all node graphs have degree below $k$ and directed paths with
fewer than $H$ vertices before an answer is recorded. Recording the
answer and executing \textnormal{\texttt{Repair}} restores these bounds.
During this operation, degrees are at most $k$ and directed paths have
fewer than $2H$ vertices.
\end{lemma}
\begin{proof}
An answer involving an anchor adds only an interval bound. An answer
between free items adds at most one arc, say $x\to y$. Its certified
positive probability ensures that the resulting region is nonempty,
so the arc cannot create a directed cycle. Only $x$ and $y$ can reach
degree $k$. Every new path consists of two old paths joined by this arc,
so it has fewer than $2H$ vertices.

If an $H$-vertex path now exists, it must contain $x\to y$. Refining
its entire vertex set removes both endpoints. Otherwise a degree repair
removes an endpoint that has reached degree $k$. Either repair deletes
the new arc; the remaining parent DAG is a subgraph of the previously
valid DAG. Each child receives only isolated vertices, so its bounds
remain valid too. If neither violation occurs, no repair is needed.
\end{proof}



\subsection{Consistency and termination}

\begin{proof}[Proof of Proposition~\ref{prop:legality}]
Initially every node has positive volume, every order is represented,
and the strict node graph bounds hold. We induct over completed calls
and, within each call, over its changes to the state.

Before answering, a refinement deletes one vertex and adds an isolated
vertex to a child, so the strict DAG bounds continue to hold. The anchor
routine returns an interior position, as proved in
Lemma~\ref{lem:local-routines}. Lemma~\ref{lem:admission}
preserves positive node volumes and consistency with the transcript.
Normalization preserves the represented region by
Lemma~\ref{lem:normalization}.

If the queried labels lie in different child subtrees, their anchors
determine the answer in every represented order. Otherwise, the
answer guarantee in Lemma~\ref{lem:local-routines} ensures that the chosen answer retains at least
$1/2-\eta>0$ of its node's volume. Recording its arc or interval bound
therefore preserves positive volume and makes the answer true in every
represented order. A new arc cannot create a cycle, since that would
make the region empty. Normalization preserves this updated region.
The transcript is then extended by the chosen answer.

During the subsequent repair, the temporary DAG bounds follow from
Lemma~\ref{lem:restoration}, and Lemma~\ref{lem:anchor-selection}
supplies interior anchors. Each move again preserves positive volume
and the transcript by Lemma~\ref{lem:admission}. This applies to every
vertex of a selected path, including those whose incident arcs were
removed earlier in the batch. The full batch is completed, and
Lemma~\ref{lem:restoration} restores the strict bounds for the next call.

The finite certificate calculations and the explicit rounding rule
terminate. Before answering, only queried labels can move. After a
move, the label has an isolated coordinate with interval $(0,1)$. Further
refinements leave it isolated with the same interval, so its density
remains one. A second move would therefore have gain zero, contradicting
the failed-certification gain guarantee. Thus there are at most two
such moves. A repair makes at most $n$ further moves,
so every call terminates with at most $n+2$ refinements.
All analytic guarantees used here apply to arbitrary positive-volume
regions with the stated DAG bounds, independently of the interaction
history.
\end{proof}