\section*{Recycling}

\begin{discussion} \label{disc:onlie} For use in the next section, note
that both $\calA^w(\uparrow_S)$ and $\calA(S;\,S)$ are associative algebras
(the former using the stacking product of Equation~\eqref{eq:TubeProduct} and
the latter using that of Equation~\eqref{eq:AHTStacking}), yet $\delta$ is
not multiplicative and hence it does not restrict to a Lie morphism on
primitives. Instead, on primitives
$(\lambda_1;\omega_1),(\lambda_2;\omega_2)\in\TW(S)$ we have

\begin{equation} \label{eq:BracketComparissons}
  \delta[l\lambda_1+\iota\omega_1,\,l\lambda_2+\iota\omega_2]
  = [\delta(l\lambda_1+\iota\omega_1),\,\delta(l\lambda_2+\iota\omega_2)]
  + e_s(\partial_{\lambda_1}\lambda_2;\,\partial_{\lambda_1}\omega_2)
  - e_s(\partial_{\lambda_2}\lambda_1;\,\partial_{\lambda_2}\omega_1).
\end{equation}
\end{discussion}

\noindent{\em Proof of Equation~\eqref{eq:BracketComparissons}.}

\begin{proof} $E_l$ and $E_f$ both plant wheels at the top, and as tails
commute, they do so in the same manner. So $\omega'=\omega$ and we only
need to show Equation~\eqref{eq:convertion} at tree level (meaning, modulo
wheels). We will show that for every scalar $t$,
\begin{equation} \label{eq:treelevel}
  \exp(l(t\lambda))=\exp_\#(e_s(\Gamma(\lambda,t)))\act\delta^{-1};
\end{equation}
the desired result is the specialization of Equation~\eqref{eq:treelevel}
to $t=1$. It is clear that Equation~\eqref{eq:treelevel} holds for some
unique $\Gamma_0=\{a\to\gamma_{0a}(t)\}$, that $\gamma_{0a}(0)=0$, and that
each coefficient of each $\gamma_{0a}(t)$ depends polynomialy on $t$, and
hence it is enough to show that $\Gamma_0$ satisfies the differential
equation in~\eqref{eq:GammaODE}.

MORE.

\end{proof}