[proofplan]
The proof is a direct verification from the left-invariant framing of the Heisenberg group. First we use the defining property of left-invariant vector fields to show that the differential of a left translation fixes each standard field $X_j$, $Y_j$, and $T$. Since the contact distribution is exactly the real span of the $X_j$ and $Y_j$, this proves preservation of the horizontal bundle. The complex CR subbundle is then preserved because each $Z_j=\frac{1}{2}(X_j-iY_j)$ is also fixed by the complexified differential. Finally, the standard boundary identification transports this CR automorphism of $\mathbb H^n$ to a CR diffeomorphism of $\partial\mathcal U^n$.
[/proofplan]
[step:Use left invariance to compute the differential of a left translation]
Fix $p\in\mathbb H^n$. The map $L_p:\mathbb H^n\to\mathbb H^n$ is a smooth diffeomorphism with inverse $L_{p^{-1}}$, because left multiplication by $p^{-1}$ is inverse to left multiplication by $p$ under the group law.
For each $j\in\{1,\dots,n\}$, the vector fields $X_j$, $Y_j$, and $T=\partial_t$ are left-invariant by their construction from the basis of the [Lie algebra](/page/Lie%20Algebra) at the identity. Hence, for every $q\in\mathbb H^n$,
\begin{align*}
d(L_p)_q((X_j)_q)=(X_j)_{p\cdot q}.
\end{align*}
Likewise,
\begin{align*}
d(L_p)_q((Y_j)_q)=(Y_j)_{p\cdot q}.
\end{align*}
Finally,
\begin{align*}
d(L_p)_q(T_q)=T_{p\cdot q}.
\end{align*}
[guided]
Fix $p\in\mathbb H^n$. We first record the basic differential statement that drives the whole proof. The left translation is the smooth map
\begin{align*}
L_p:\mathbb H^n\to\mathbb H^n,\qquad q\mapsto p\cdot q.
\end{align*}
Its inverse is $L_{p^{-1}}$, because the group identities give $p^{-1}\cdot(p\cdot q)=q$ and $p\cdot(p^{-1}\cdot q)=q$ for every $q\in\mathbb H^n$. Thus $L_p$ is a diffeomorphism.
The point of introducing left-invariant vector fields is precisely that they are unchanged by the differential of left multiplication. Since $X_j$, $Y_j$, and $T=\partial_t$ are the standard left-invariant vector fields determined by the Heisenberg Lie algebra basis, their defining property gives, for each $q\in\mathbb H^n$,
\begin{align*}
d(L_p)_q((X_j)_q)=(X_j)_{L_p(q)}=(X_j)_{p\cdot q}.
\end{align*}
The same defining property gives
\begin{align*}
d(L_p)_q((Y_j)_q)=(Y_j)_{L_p(q)}=(Y_j)_{p\cdot q}.
\end{align*}
It also gives
\begin{align*}
d(L_p)_q(T_q)=T_{L_p(q)}=T_{p\cdot q}.
\end{align*}
This is the only group-theoretic input needed: left translations preserve the left-invariant frame itself, not just its span.
[/guided]
[/step]
[step:Deduce preservation of the contact distribution]
Let $H_q\subset T_q\mathbb H^n$ denote the horizontal contact space at $q$, so that
\begin{align*}
H_q=\operatorname{span}_{\mathbb R}\{(X_1)_q,\dots,(X_n)_q,(Y_1)_q,\dots,(Y_n)_q\}.
\end{align*}
Take $v\in H_q$. Then there are [real numbers](/page/Real%20Numbers) $a_1,\dots,a_n,b_1,\dots,b_n\in\mathbb R$ such that
\begin{align*}
v=\sum_{j=1}^n a_j(X_j)_q+\sum_{j=1}^n b_j(Y_j)_q.
\end{align*}
By linearity of $d(L_p)_q$ and the previous step,
\begin{align*}
d(L_p)_q(v)=\sum_{j=1}^n a_j(X_j)_{p\cdot q}+\sum_{j=1}^n b_j(Y_j)_{p\cdot q}.
\end{align*}
Therefore $d(L_p)_q(v)\in H_{p\cdot q}$. Since $L_p$ is a diffeomorphism, applying the same inclusion to $L_{p^{-1}}$ gives equality
\begin{align*}
d(L_p)_q(H_q)=H_{p\cdot q}.
\end{align*}
Thus $L_p$ preserves the contact distribution $H=\ker\theta$.
[/step]
[step:Show that the complex differential fixes the CR vector fields]
Let $d(L_p)_q^{\mathbb C}:T_q\mathbb H^n\otimes_{\mathbb R}\mathbb C\to T_{p\cdot q}\mathbb H^n\otimes_{\mathbb R}\mathbb C$ denote the complex-linear extension of $d(L_p)_q$. For each $j\in\{1,\dots,n\}$, the definition
\begin{align*}
Z_j=\frac{1}{2}(X_j-iY_j)
\end{align*}
and complex linearity give
\begin{align*}
d(L_p)_q^{\mathbb C}((Z_j)_q)=\frac{1}{2}\left(d(L_p)_q((X_j)_q)-i\,d(L_p)_q((Y_j)_q)\right).
\end{align*}
Using the identities from the first step, this becomes
\begin{align*}
d(L_p)_q^{\mathbb C}((Z_j)_q)=\frac{1}{2}\left((X_j)_{p\cdot q}-i(Y_j)_{p\cdot q}\right)=(Z_j)_{p\cdot q}.
\end{align*}
Hence
\begin{align*}
d(L_p)_q^{\mathbb C}\left(\operatorname{span}_{\mathbb C}\{(Z_1)_q,\dots,(Z_n)_q\}\right)=\operatorname{span}_{\mathbb C}\{(Z_1)_{p\cdot q},\dots,(Z_n)_{p\cdot q}\}.
\end{align*}
Thus $L_p$ preserves the standard $(1,0)$ CR subbundle $T^{1,0}\mathbb H^n$.
[/step]
[step:Transport the preserved CR structure to the Siegel boundary]
Let $\Phi:\mathbb H^n\to\partial\mathcal U^n$ be the map defined by $\Phi(z,t)=(z,t+i|z|^2)$. This is exactly the standard Heisenberg parameterisation of $\partial\mathcal U^n$ appearing in [citetheorem:9201]. That result applies to this boundary model and states that, via this parameterisation, $\mathbb H^n$ and $\partial\mathcal U^n$ are identified as CR manifolds. Hence $\Phi$ is a CR diffeomorphism from $\mathbb H^n$ onto $\partial\mathcal U^n$ with the standard boundary CR structure. Since $L_p$ is a CR diffeomorphism of $\mathbb H^n$ by the preceding steps, the conjugated map
\begin{align*}
\Phi\circ L_p\circ\Phi^{-1}:\partial\mathcal U^n\to\partial\mathcal U^n
\end{align*}
is a composition of CR diffeomorphisms and is therefore a CR diffeomorphism. This proves the asserted boundary statement and completes the proof.
[/step]
