'Lie correspondence' for formal power series in non-commuting indeterminates This is related to an earlier question of mine. I would like an argument or a reference (or a missing hypothesis if needed) for the following.

Let  $\mathbb{F}\langle\langle \alpha\rangle\rangle$ and $\mathbb{F}\langle\langle \beta\rangle\rangle$ be the algebras of formal power series in the given sets of non-commuting indeterminates over a field $\mathbb{F}$ of characteristic zero. Let $\mathfrak{g}$ and $\mathfrak{h}$ be the respective Lie subalgebras
with zero constant term. Let
$G$ and $H$ be the subgroups of the groups of units of the respective algebras consisting of the elements with constant term equal to 1. (So $\log$ maps $G$ bijectively onto $\mathfrak{g}$ and similarly for $H$.)
Let $\Phi:G\to H$ be a homomorphism, and set $\phi=\log\Phi\exp$. Assume that $\phi(aX)=a\phi(X)$ for all $a$ and $X$.
Then $\phi(X+Y)=\phi(X)+\phi(Y)$.

Let's recall the set-up in the classical case of matrix Lie groups and Lie algebras. Under suitable hypotheses there is a 1-1 correspondence between Lie group homomorphisms $\Phi:G\to H$ and Lie algebra homomorphisms $\phi:\mathfrak{g}\to\mathfrak{h}$ where $\mathfrak{g}$ is the Lie algebra corresponding to $G$, and similarly for $\mathfrak{h}$: they are related via $\exp\phi=\Phi\exp$. The proof that a Lie algebra homomorphism $\phi$ gives rise to a Lie group homomorphism $\Phi$ is fairly neat. A key step is to show that $\log(\exp(\phi(X))\exp(\phi(Y)))=\phi(\log(\exp(X)\exp(Y)))$, which is a consequence of the Baker-Campbell-Hausdorff formula.
To show that $\Phi$ gives rise to a suitable $\phi$, the key step this time is to show that $\phi$ is additive which reduces to the identity

$\Phi\exp(\log g + \log h)=\exp(\log\Phi(g)+\log\Phi(h))$,

but this seems to be trickier to prove in the situation I'm interested in. Even if one inverts the BCH formula (see this question and answer), the required identity is not obvious to me. (In the notation of that answer, we would need the identity $\Phi A(g-1,h-1) = A(\Phi(g)-1,\Phi(h)-1)$.)
The proof in Brian C. Hall's book to handle the classical case uses $\left(e^{\frac{X}{m}}e^{\frac{Y}{m}}\right)^m$ as an approximation to $e^{X+Y}$ and then involves taking $\lim_{m\to\infty}$, but unfortunately taking such limits doesn't seem to be valid in my situation. This could be remedied by assuming $\mathbb{F}$ is an ordered field and that $\Phi$ preserves limits in an appropriate sense, but I would like to avoid making extra assumptions if possible.
 A: I can provide a very partial answer to the problem in the case your field $\mathbb{F}$ is either the reals or the complex numbers.
Then the result you are after is a consequence of the group of formal power series you are looking for actually forming an infinite-dimensional Lie group which is regular in the sense of Milnor (actually even $C^0$-regular).
The key observation here is that the groups are character groups of suitable Hopf algebras (of non-commutative polynomials), whence the relevant Lie theory for these objects was developed in the paper Character groups of Hopf algebras as infinite-dimensional Lie groups.
For regular infinite-dimensional Lie groups, there is a version of the Lie theorem which asserts (under the usual topological assumptions like connected, simply connected) the correspondence you are asking for (see Glockner's Regularity properties of infinite-dimensional
Lie groups, and semiregularity).
Regularity asks to solve certain differential equations (whence the restriction to the reals or complex numbers since we can make calculus work there). I am thus cheating as I picked exactly the cases where calculus works to a certain degree.
I wonder though if one could not circumvent this in the case at hand. A lot of the arguments (see especially Appendix B of Character groups of Hopf algebras as infinite-dimensional Lie groups!) exploit heavily the grading of the algebra of formal power series.
