\begin{proof}[Proof of Proposition~\ref{prop:causal}]
By induction on the number of executed actions. Base case: $S^{(0)}_j=e_j+P\,\mathrm{RMSNorm}(h_t)$ with
$h_t=B_\phi(x_{1:t})[t]$, a function of $x_{1:t}$ by causality of $B_\phi$. Inductive step: if $S^{(r)}$ and the
controller features at step $r$ depend on $x_{1:t}$ only, then the action $a_{r}$ does (it is a function of those
features under Assumption~\ref{ass:causal}), the editor's inputs are $S^{(r)}$, the context scalars, and the bank
rows $\{(K_j,V_j)\}_{j\le t}$, each a function of $H_t[1{:}t]$ and hence of $x_{1:t}$; so $S^{(r+1)}$ depends on
$x_{1:t}$ only. The readout and head are deterministic functions of $(S^{(n_t)},S^{(0)},z_t,h_t)$. In the parallel
teacher-forced implementation the per-query mask $j\le t$ enforces the same restriction although all of $H_T$ is
resident in one tensor; the unit test perturbs $x_{t+1:T}$ and verifies that $\ell_{1:t}$ is unchanged.
\end{proof}

\begin{proof}[Proof of Proposition~\ref{prop:identity}]
If $n_t=0$ then $S^{(n_t)}=S^{(0)}$ and $r(S^{(n_t)},z_t)-r(S^{(0)},z_t)=0$, hence $\Delta_t=sU0=0$ and
$h^{\mathrm{corr}}_t=h_t$. In the implementation two separate branches return the backbone head directly:
one when the requested budget is zero (before any slot is allocated or any bank row is read), and one for every
position whose edit count is zero after routing; both compute exactly the expression $E\,\mathrm{RMSNorm}(h_t)$ on
the same tensor $h_t$ and are therefore bitwise equal to the backbone-only forward on the same device with the same
kernels (tests 02--04 and the cache test). The statement about joint fine-tuning is immediate: $h_t$ is whatever
the current backbone produces.
\end{proof}

\begin{proof}[Proof of Proposition~\ref{prop:locality}]
The new workspace is $S'=\mathbb{1}[m\in I]\odot C+\mathbb{1}[m\notin I]\odot S$ where
$C_m=\sum_{i} \mathbb{1}[\iota_i=m]\,\tilde S'_{\iota_i}$ sums the (at most two) lane results $\tilde S'$ over the
lane indices $\iota_i$ of the action. For $m\notin I$ the first term is zero and $S'_m=S_m$ by the identity
$0\cdot x + 1\cdot y = y$, which is exact in IEEE arithmetic for finite $y$. For a pair, the two lanes have
distinct indices, so $C_m$ is a single lane result plus exact zeros; both lanes read the same snapshot $\bar S$ and
neither reads the other's output, so permuting the lanes permutes the summands of an exact sum of one nonzero
term and zeros, leaving $C$ unchanged.
\end{proof}

\begin{proof}[Proof of Proposition~\ref{prop:displacement}]
Each write into slot $j$ adds $\eta_j\delta^c_j$ with $0<\eta_j\le\eta_{\max}$ and $\rms(\delta^c_j)\le c$ by the
clipping rule (if $\rms(\delta_j)\le c$ the factor is $1$ and $\rms(\delta^c_j)=\rms(\delta_j)\le c$; otherwise
$\rms(\delta^c_j)=c\,\rms(\delta_j)/\rms(\delta_j)=c$ up to the $\epsilon$ guard, which can only shrink the step).
Since $\rms(\cdot)=\|\cdot\|_2/\sqrt{w}$ is a norm, the triangle inequality gives
$\rms(S^{(R)}_j-S^{(0)}_j)\le\sum_{\text{writes into }j}\eta_j\rms(\delta^c_j)\le n_j\eta_{\max}c$.
\end{proof}

\begin{proof}[Proof of Proposition~\ref{prop:regret}]
Let $a^\star=\arg\max_a J(a)$ over $\Act\cup\{\Stop\}$ and $\hat a=\arg\max_a\hat J(a)$. Both $J$ and $\hat J$
assign $0$ to \Stop. For every $a\in\Act$, $|\hat J(a)-J(a)|\le|\hat g-g|+\lambda|\hat c-c|\le\varepsilon+\lambda\delta=:\Delta$,
and $|\hat J(\Stop)-J(\Stop)|=0\le\Delta$. Then
$J(a^\star)-J(\hat a)=\big(J(a^\star)-\hat J(a^\star)\big)+\big(\hat J(a^\star)-\hat J(\hat a)\big)+\big(\hat J(\hat a)-J(\hat a)\big)
\le\Delta+0+\Delta=2\Delta$, the middle term being non-positive by the choice of $\hat a$.
\end{proof}