[proofplan]
The [Lie algebra](/page/Lie%20Algebra) $\mathfrak h^n$ is two-step nilpotent because every bracket is a multiple of the central element $T$. For a connected simply connected nilpotent Lie group, the exponential map is a global diffeomorphism, so the stated exponential coordinates are valid globally. The Baker-Campbell-Hausdorff series truncates after the first commutator in a two-step nilpotent Lie algebra, and a direct computation of $[U,V]$ gives the central correction term. Finally, rewriting the real correction in complex notation identifies it with $2\operatorname{Im}\left(\sum_j z_j\overline{w_j}\right)$.
[/proofplan]
[step:Verify that the Heisenberg Lie algebra is two-step nilpotent]
Let $\mathfrak z$ denote the one-dimensional real subspace $\mathfrak z:=\operatorname{span}_{\mathbb R}\{T\}\subset \mathfrak h^n$. By the defining bracket relations, every bracket between basis elements lies in $\mathfrak z$, and every bracket involving $T$ is zero. By bilinearity of the Lie bracket, this gives
\begin{align*}
[\mathfrak h^n,\mathfrak h^n]\subset \mathfrak z
\end{align*}
and
\begin{align*}
[\mathfrak h^n,\mathfrak z]=\{0\}.
\end{align*}
Hence
\begin{align*}
[\mathfrak h^n,[\mathfrak h^n,\mathfrak h^n]]=\{0\}.
\end{align*}
Thus $\mathfrak h^n$ is two-step nilpotent.
[guided]
We first isolate the only possible nonzero brackets. Define the central line
\begin{align*}
\mathfrak z:=\operatorname{span}_{\mathbb R}\{T\}\subset \mathfrak h^n.
\end{align*}
The defining relations say that $[X_j,Y_k]$ is always a scalar multiple of $T$, while brackets of the form $[X_j,X_k]$, $[Y_j,Y_k]$, $[X_j,T]$, and $[Y_j,T]$ vanish. Since the Lie bracket is bilinear, every bracket of two arbitrary elements of $\mathfrak h^n$ is a real linear combination of the brackets of basis elements. Therefore every such bracket lies in $\mathfrak z$:
\begin{align*}
[\mathfrak h^n,\mathfrak h^n]\subset \mathfrak z.
\end{align*}
The second defining feature is that $T$ commutes with every basis vector. Again by bilinearity, every element of $\mathfrak z$ commutes with every element of $\mathfrak h^n$, so
\begin{align*}
[\mathfrak h^n,\mathfrak z]=\{0\}.
\end{align*}
Combining the two inclusions gives
\begin{align*}
[\mathfrak h^n,[\mathfrak h^n,\mathfrak h^n]]=\{0\}.
\end{align*}
This is precisely two-step nilpotence: first commutators may be nonzero, but every further commutator with them vanishes.
[/guided]
[/step]
[step:Apply the truncated Baker-Campbell-Hausdorff formula]
Since $\mathfrak h^n$ is two-step nilpotent, every iterated commutator of length at least three vanishes. The two-step nilpotent Baker-Campbell-Hausdorff theorem applies to the connected simply connected Lie group $\mathbb H^n$ with Lie algebra $\mathfrak h^n$ and gives, for every $U,V\in\mathfrak h^n$,
\begin{align*}
\exp(U)\exp(V)=\exp\left(U+V+\frac{1}{2}[U,V]\right).
\end{align*}
This proves the Baker-Campbell-Hausdorff identity in the statement.
Also, because $\mathbb H^n$ is connected and simply connected and $\mathfrak h^n$ is nilpotent, the nilpotent exponential diffeomorphism theorem applies to the exponential map
\begin{align*}
\exp:\mathfrak h^n\to\mathbb H^n
\end{align*}
and shows that $\exp$ is a global diffeomorphism. Hence the coordinate map $E:\mathbb C^n\times\mathbb R\to\mathbb H^n$ in the statement is a global coordinate system.
[/step]
[step:Compute the commutator of two elements in exponential coordinates]
Let $(z,t),(w,s)\in\mathbb C^n\times\mathbb R$. Write $z_j=x_j+iy_j$ and $w_j=u_j+iv_j$, where $x_j,y_j,u_j,v_j\in\mathbb R$. Define
\begin{align*}
U:=\sum_{j=1}^n(x_jX_j+y_jY_j)+tT\in\mathfrak h^n
\end{align*}
and
\begin{align*}
V:=\sum_{j=1}^n(u_jX_j+v_jY_j)+sT\in\mathfrak h^n.
\end{align*}
Using bilinearity of the Lie bracket and the defining relations, all terms vanish except the $[X_j,Y_j]$ and $[Y_j,X_j]$ terms. Since $[Y_j,X_j]=-[X_j,Y_j]=4T$, we obtain
\begin{align*}
[U,V]=\sum_{j=1}^n x_jv_j[X_j,Y_j]+\sum_{j=1}^n y_ju_j[Y_j,X_j].
\end{align*}
Therefore
\begin{align*}
[U,V]=\sum_{j=1}^n x_jv_j(-4T)+\sum_{j=1}^n y_ju_j(4T).
\end{align*}
Thus
\begin{align*}
[U,V]=4\sum_{j=1}^n(y_ju_j-x_jv_j)T.
\end{align*}
[/step]
[step:Substitute the commutator into the exponential product]
By the previous step,
\begin{align*}
\frac{1}{2}[U,V]=2\sum_{j=1}^n(y_ju_j-x_jv_j)T.
\end{align*}
Hence
\begin{align*}
U+V+\frac{1}{2}[U,V]=\sum_{j=1}^n((x_j+u_j)X_j+(y_j+v_j)Y_j)+\left(t+s+2\sum_{j=1}^n(y_ju_j-x_jv_j)\right)T.
\end{align*}
Applying the exponential coordinate map $E$ gives
\begin{align*}
E(z,t)E(w,s)=E\left(z+w,\ t+s+2\sum_{j=1}^n(y_ju_j-x_jv_j)\right).
\end{align*}
[/step]
[step:Rewrite the central correction in complex notation]
For each $1\le j\le n$,
\begin{align*}
z_j\overline{w_j}=(x_j+iy_j)(u_j-iv_j).
\end{align*}
Expanding the product gives
\begin{align*}
z_j\overline{w_j}=x_ju_j+y_jv_j+i(y_ju_j-x_jv_j).
\end{align*}
Therefore
\begin{align*}
\operatorname{Im}(z_j\overline{w_j})=y_ju_j-x_jv_j.
\end{align*}
Summing over $j$ yields
\begin{align*}
\operatorname{Im}\left(\sum_{j=1}^n z_j\overline{w_j}\right)=\sum_{j=1}^n(y_ju_j-x_jv_j).
\end{align*}
Substituting this identity into the coordinate product obtained above gives
\begin{align*}
(z,t)(w,s)=\left(z+w,\ t+s+2\operatorname{Im}\left(\sum_{j=1}^n z_j\overline{w_j}\right)\right).
\end{align*}
This is the claimed exponential-coordinate group law.
[/step]
