The block sum $A\diamond B$ of symplectic matrices is symplectic

If $A\in\mathrm{Sp}(2n',\mathbb R)$ and $B\in\mathrm{Sp}(2n'',\mathbb R)$, then

where $A\diamond B$ is the block-diagonal matrix acting by $(q',q'',p',p'')\mapsto$ ($A$ on $(q',p')$, $B$ on $(q'',p'')$), i.e. the matrix of $A\oplus B$ on $\mathbb R^{2n'}\oplus\mathbb R^{2n''}=\mathbb R^{2(n'+n'')}$ with the coordinates reordered as $(q',q'',p',p'')$.

This is the product structure on symplectic groups used for the product property of the Conley-Zehnder index (Gutt, §2) and for comparing $\mathrm{Sp}(2n)$ with $\mathrm{Sp}(2n+2)$.

Formalization Note. $\mathbb R^{2n\times2n}$ is Mat n (real matrices indexed by Fin n ⊕ Fin n, first block $q$, second block $p$) and $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$ is Matrix.J; IsSymplectic A is membership in Matrix.symplecticGroup. Vectors of $\mathbb R^{2n}$ are functions Fin n ⊕ Fin n → ℝ and $Av$ is A *ᵥ v. $A\diamond B$ is ConleyZehnder.diamond A B from the Conley-Zehnder setting definitions, the reindexing of Matrix.fromBlocks A 0 0 B along (Fin n' ⊕ Fin n') ⊕ (Fin n'' ⊕ Fin n'') ≃ Fin (n'+n'') ⊕ Fin (n'+n'').