Lemma 16 — the composition of two atomic transformations is atomic

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; an independent, blind read-back should replace it before the proposal is relied upon.

Fix $T$ satisfying all six principles, systems $A,B,C$, and linear maps $\mathcal D_1:\mathbb R^{D_A}\to\mathbb R^{D_B}$, $\mathcal D_2:\mathbb R^{D_B}\to\mathbb R^{D_C}$. Assume both are atomic transformations: $\mathcal D_1$ belongs to some test from $A$ to $B$, and whenever there are a test $\{t_x\}$ from $A$ to $B$ and a finite subset $X_0$ with $\mathcal D_1=\sum_{x\in X_0}t_x$, every $t_x$ with $x\in X_0$ equals $p\,\mathcal D_1$ for some $p\ge0$; similarly for $\mathcal D_2$ (tests from $B$ to $C$). The conclusion is that the composite map $\mathcal D_2\circ\mathcal D_1$ is an atomic transformation from $A$ to $C$ in the same sense (it belongs to some test from $A$ to $C$, and all its refinements by tests from $A$ to $C$ are nonnegative multiples of it).