\section{Theoretical properties}\label{sec:theory}

The statements below are structural properties of the computation graph, not performance guarantees. Proofs are
in Appendix~\ref{app:proofs}; each is accompanied by a numerical property test in \texttt{tests/unit/} that
exercises the implemented code on random inputs (tests are evidence about the implementation, not proofs).

\begin{assumption}[prefix causality of the components]\label{ass:causal}
$B_\phi$ is causal; the bank visible to a query at position $t$ is $\{(K_j,V_j)\}_{j\le t}$; the controller features
at position $t$ are functions of $(z_t,S,r,\rho)$ only.
\end{assumption}

\begin{proposition}[causality]\label{prop:causal}
Under Assumption~\ref{ass:causal}, for every executed action sequence the corrected logits $\ell_t$ are a function
of $x_{1:t}$ only, for all $t$ and for any number of edits $n_t\le R_{\max}$.
\end{proposition}

\begin{proposition}[identity and exact bypass]\label{prop:identity}
If $n_t=0$ then $\Delta_t=0$ exactly and $\ell_t=\ell^{\mathrm{bb}}_t$ in exact arithmetic. In floating point, the
implementation returns the backbone head through an explicit branch that performs no workspace computation when
the budget is zero, and through the same branch for positions with no executed edit, so the equality is bitwise for
identical execution settings. After joint fine-tuning the identity holds relative to the \emph{current} backbone,
not to any earlier checkpoint.
\end{proposition}

\begin{proposition}[exact locality and order independence]\label{prop:locality}
For an action with active set $I$, $S'_m=S_m$ bitwise for all $m\notin I$, and the result of a pair action does not
depend on the order in which its two lanes are processed.
\end{proposition}

\begin{proposition}[bounded displacement]\label{prop:displacement}
With $\rms(v)=\|v\|_2/\sqrt{w}$, after $n_j$ writes into slot $j$,
$\rms\big(S^{(R)}_j-S^{(0)}_j\big)\le n_j\,\eta_{\max}\,c$. The bound is a consequence of clipping and of the
triangle inequality; it does not imply convergence of the edits or any decrease of the loss.
\end{proposition}

\begin{proposition}[one-step selection regret]\label{prop:regret}
Fix a state $s$ and let $J(a)=g(s,a)-\lambda c(a)$ for $a\in\Act$ and $J(\Stop)=0$, with estimates
$\hat J(a)=\hat g(s,a)-\lambda\hat c(a)$. If $|\hat g(s,a)-g(s,a)|\le\varepsilon$ and $|\hat c(a)-c(a)|\le\delta$
for all feasible $a$, then the greedy choice $\hat a=\arg\max\hat J$ satisfies
$\max_a J(a)-J(\hat a)\le 2(\varepsilon+\lambda\delta)$. With the known cost used in this paper, $\delta=0$.
Adding the risk term $-\kappa\hat\sigma$ changes the objective and the bound no longer applies as stated.
\end{proposition}

\begin{remark}
None of the propositions bounds the multi-step value of a trajectory; the greedy rule can be arbitrarily
sub-optimal on states where the best first action has negative immediate gain. Section~\ref{sec:results-oracle}
measures that opportunity directly.
\end{remark}