Trace nondegeneracy on Hom classes

The accompanying paper's Lemma 3.6, categorified: a Hom-space class all of whose composition traces vanish is zero. This is the input to the semisimplicity of the End algebras (Theorem 4.4) and the atom dichotomy (Lemma 4.5).

theorem RS.HomSpace.eq_zero_of_traces_vanish {R : ℕ} (f : EdgeRankParameter R) {t u : ℕ} (q : HomSpace f.val (t + u)) (hq : ∀ (G : Fragment (Fin (u + t))), (traceMap f.val t) (((comp f t u t) q) (ofFragment f.val G)) = 0) : q = 0

Zero negligibles on classes (accompanying paper, Lemma 3.6): a class all of whose composition traces vanish is zero.