Derived Hall moduli types are locally finite and the input span is proper

Fix a perfect module $a$. The based loop space of $X^{(0)}$ at $a$ is the equivalence component of $\mathrm{Map}(a,a)$. Its components are $\mathrm{Aut}(a)$, a subset of the finite vector space ${\mathrm{Ext}}^0(a,a)$, and for $i>1$, [F2] gives ${\pi }_i(X^{(0)},a)={\mathrm{Ext}}^{1-i}(a,a)$. These groups are finite by [F1] and vanish in high degrees, so $X^{(0)}$ is locally finite.

Fix perfect modules $a,b$. A point of the homotopy fiber of $s\times t$ over $(a,b)$ is an arrow with source identified with $a$ and homotopy cofiber identified with $b$. Its connected components are distinguished triangles $a\to z\to b\to a[1]$ with both endpoints identified; the connecting map classifies the component in ${\mathrm{Hom}}_{\mathcal{D}(\mathcal{T})}(b,a[1])={\mathrm{Ext}}^1(b,a)$. The latter is finite by [F1], so this fiber has finitely many components and $s\times t$ is proper on components.

For arrows and composable pairs, the derived mapping complexes are finite homotopy limits of finite sums of the complexes $\mathrm{R}\mathrm{H}\mathrm{o}\mathrm{m}(a,b)$ between their finitely many entries. By [F1], each such complex has finite-dimensional cohomology in a finite degree range. A finite direct sum or homotopy fiber of these complexes again has finite-dimensional cohomology in a finite degree range. The same loop-space calculation as in step 1.1 therefore shows that $X^{(1)}$ and $X^{(2)}$ are locally finite.

By [F4], pullback along $s\times t$ preserves finite support, and pushforward along $c$ sends a finite-support function to a finite-support function. The homotopy groups of every fiber used in the pushforward are finite and eventually zero by steps 1.1–1.2, so each weight is a finite rational number. Thus the convolution in Toën derived Hall algebra by homotopy-cofiber convolution is a well-defined finite-support function.