Vanishing of intrinsic irreducible quotients

theorem MagnitudeConjecture.CategoricalIrreducible.finrank_eq_zero_of_radicalSquare_eq_top (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) (h : radicalSquare k X Y = ⊤) : Module.finrank k (Space k X Y) = 0

If every morphism lies in the radical square, the irreducible quotient vanishes.