Proof of Theorem 1, p. 3 — if $e^{i\varepsilon D}$ is logical for all $\varepsilon$, then $(I-P)DP=0$

Let $P$ be an operator on a finite-dimensional system and $D$ a Hermitian operator. Suppose that for every real $\varepsilon$ the unitary $e^{i\varepsilon D}$ is logical, i.e. $(I-P)e^{i\varepsilon D}P = 0$. Then

This is the derivative step of the proof of Theorem 1: an element $D$ of the Lie algebra of the identity component $\mathcal C$ generates a one-parameter group of logical gates, and differentiating at $\varepsilon = 0$ shows that $D$ itself preserves the code space.

Formalization Note The hypothesis "$D \in \mathfrak c$" is replaced by what the step uses: $e^{i\varepsilon D}$ is logical for all real $\varepsilon$. The factor $i$ and the Hermiticity of $D$ follow the physics convention of footnote 1. The exponential is NormedSpace.exp.