[proofplan]
We compare, at a fixed exogenous realization, the original recursive system with the intervened system $do(A=a)$. On the event that the original treatment value is already $a$, the treatment coordinate has the same value in both systems. Since the model is recursive, induction through the recursive order then shows that every endogenous coordinate agrees in the original and intervened solutions. Taking the outcome coordinate gives the desired consistency equality.
[/proofplan]
[step:Fix an exogenous realization where the original treatment equals $a$]
Fix $a\in\mathcal X_A$. Let $u=(u_1,\dots,u_n)$ be an exogenous realization such that $A(u)=a$. By definition of $A=V_r$, this means
\begin{align*}
v_r(u)=a.
\end{align*}
The original solution is $v(u)=(v_1(u),\dots,v_n(u))$, and the intervened solution under $do(A=a)$ at the same exogenous realization is $v^a(u)=(v^a_1(u),\dots,v^a_n(u))$.
[/step]
[step:Prove equality of all endogenous coordinates by induction through the recursive order]
We prove by induction on $i\in\{1,\dots,n\}$ that
\begin{align*}
v_i(u)=v^a_i(u).
\end{align*}
For the induction step, assume that $v_j(u)=v^a_j(u)$ for every $j<i$. If $i=r$, then the original treatment coordinate satisfies $v_r(u)=a$ by the choice of $u$, while the intervened model sets $v^a_r(u)=a$ by the intervention $do(A=a)$. Hence $v_r(u)=v^a_r(u)$.
If $i\ne r$, then the structural equation for $V_i$ is unchanged by the intervention. Since $M$ is recursive, the value of $V_i$ depends only on the exogenous coordinate $u_i$ and on earlier endogenous coordinates. Therefore
\begin{align*}
v_i(u)=f_i(v_1(u),\dots,v_{i-1}(u),u_i).
\end{align*}
Similarly, because the same structural map $f_i$ is used in the intervened model for $i\ne r$,
\begin{align*}
v^a_i(u)=f_i(v^a_1(u),\dots,v^a_{i-1}(u),u_i).
\end{align*}
The induction hypothesis gives equality of each input coordinate in these two evaluations, and the exogenous input is the same $u_i$ in both systems. Hence
\begin{align*}
v_i(u)=v^a_i(u).
\end{align*}
This completes the induction.
[guided]
We want to show that the original world and the counterfactual world agree coordinate by coordinate when the original world already has treatment value $a$. The recursive order is what makes this possible: each coordinate is computed only after all coordinates it can depend on have already been computed.
Fix $i\in\{1,\dots,n\}$ and assume that all earlier coordinates have already been shown equal:
\begin{align*}
v_j(u)=v^a_j(u)\quad\text{for every }j<i.
\end{align*}
There are two cases.
First suppose $i=r$, so $V_i=A$ is the treatment variable. In the original model, our choice of $u$ gives
\begin{align*}
v_r(u)=A(u)=a.
\end{align*}
In the intervened model $M_{do(A=a)}$, the structural equation for $A$ is replaced by the constant assignment $a$, so
\begin{align*}
v^a_r(u)=a.
\end{align*}
Thus the treatment coordinate agrees:
\begin{align*}
v_r(u)=v^a_r(u).
\end{align*}
Now suppose $i\ne r$. The intervention changes only the structural equation for $A=V_r$, so the structural assignment for $V_i$ remains the original map
\begin{align*}
f_i:\prod_{j<i}\mathcal X_j\times\mathcal X_{U_i}\to\mathcal X_i.
\end{align*}
In the original system, the $i$-th coordinate is obtained by evaluating $f_i$ at the earlier original endogenous coordinates and the exogenous coordinate $u_i$:
\begin{align*}
v_i(u)=f_i(v_1(u),\dots,v_{i-1}(u),u_i).
\end{align*}
In the intervened system, the same map $f_i$ is evaluated at the earlier intervened endogenous coordinates and the same exogenous coordinate $u_i$:
\begin{align*}
v^a_i(u)=f_i(v^a_1(u),\dots,v^a_{i-1}(u),u_i).
\end{align*}
The induction hypothesis says that every earlier endogenous input appearing in these two evaluations is equal, and the counterfactual is constructed using the same exogenous realization, so the exogenous input is also identical. Therefore the two evaluations of $f_i$ are equal:
\begin{align*}
v_i(u)=v^a_i(u).
\end{align*}
This proves the induction step in both cases, and hence all endogenous coordinates agree between the original and intervened systems at this exogenous realization.
[/guided]
[/step]
[step:Read off the outcome coordinate and obtain the eventwise equality]
Applying the coordinate equality from the previous step with $i=s$ gives
\begin{align*}
v_s(u)=v^a_s(u).
\end{align*}
By the definitions of $Y$ and $Y(a)$,
\begin{align*}
Y(u)=v_s(u)
\end{align*}
and
\begin{align*}
Y(a)(u)=v^a_s(u).
\end{align*}
Therefore
\begin{align*}
Y(u)=Y(a)(u).
\end{align*}
Since the exogenous realization $u$ was arbitrary subject only to $A(u)=a$, we have
\begin{align*}
\{A=a\}\subseteq \{Y=Y(a)\}.
\end{align*}
Thus the observed outcome agrees with the potential outcome corresponding to the treatment actually received.
[/step]
