 Holonomic Weyl algebra module

A nonzero finitely generated Weyl algebra module over $A_n(\mathbb{C})$ is holonomic when it attains the lower bound in the Bernstein inequality for Weyl algebra modules. The zero module is also conventionally called holonomic. Nonzero subquotients of a holonomic module remain holonomic. Additivity and integrality of the leading Hilbert-polynomial multiplicity then bound the number of nonzero factors in any submodule chain, giving finite composition length.