1\section{Theoretical properties}\label{sec:theory}23The statements below are structural properties of the computation graph, not performance guarantees. Proofs are4in Appendix~\ref{app:proofs}; each is accompanied by a numerical property test in \texttt{tests/unit/} that5exercises the implemented code on random inputs (tests are evidence about the implementation, not proofs).67\begin{assumption}[prefix causality of the components]\label{ass:causal}8$B_\phi$ is causal; the bank visible to a query at position $t$ is $\{(K_j,V_j)\}_{j\le t}$; the controller features9at position $t$ are functions of $(z_t,S,r,\rho)$ only.10\end{assumption}1112\begin{proposition}[causality]\label{prop:causal}13Under Assumption~\ref{ass:causal}, for every executed action sequence the corrected logits $\ell_t$ are a function14of $x_{1:t}$ only, for all $t$ and for any number of edits $n_t\le R_{\max}$.15\end{proposition}1617\begin{proposition}[identity and exact bypass]\label{prop:identity}18If $n_t=0$ then $\Delta_t=0$ exactly and $\ell_t=\ell^{\mathrm{bb}}_t$ in exact arithmetic. In floating point, the19implementation returns the backbone head through an explicit branch that performs no workspace computation when20the budget is zero, and through the same branch for positions with no executed edit, so the equality is bitwise for21identical execution settings. After joint fine-tuning the identity holds relative to the \emph{current} backbone,22not to any earlier checkpoint.23\end{proposition}2425\begin{proposition}[exact locality and order independence]\label{prop:locality}26For an action with active set $I$, $S'_m=S_m$ bitwise for all $m\notin I$, and the result of a pair action does not27depend on the order in which its two lanes are processed.28\end{proposition}2930\begin{proposition}[bounded displacement]\label{prop:displacement}31With $\rms(v)=\|v\|_2/\sqrt{w}$, after $n_j$ writes into slot $j$,32$\rms\big(S^{(R)}_j-S^{(0)}_j\big)\le n_j\,\eta_{\max}\,c$. The bound is a consequence of clipping and of the33triangle inequality; it does not imply convergence of the edits or any decrease of the loss.34\end{proposition}3536\begin{proposition}[one-step selection regret]\label{prop:regret}37Fix a state $s$ and let $J(a)=g(s,a)-\lambda c(a)$ for $a\in\Act$ and $J(\Stop)=0$, with estimates38$\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$39for all feasible $a$, then the greedy choice $\hat a=\arg\max\hat J$ satisfies40$\max_a J(a)-J(\hat a)\le 2(\varepsilon+\lambda\delta)$. With the known cost used in this paper, $\delta=0$.41Adding the risk term $-\kappa\hat\sigma$ changes the objective and the bound no longer applies as stated.42\end{proposition}4344\begin{remark}45None of the propositions bounds the multi-step value of a trajectory; the greedy rule can be arbitrarily46sub-optimal on states where the best first action has negative immediate gain. Section~\ref{sec:results-oracle}47measures that opportunity directly.48\end{remark}49