The Regts–Sevenster theorem, forward direction

The forward direction conditional on Deligne's theorem. The factorial trace obstruction supplies semisimplicity and abelianness of the envelope from the connection-rank bound, without a Schur package. The resulting fibre functor provides the mixed model.

theorem RS.regts_sevenster_deligne_only (hDeligne : DeligneTheoremStatement) : RegtsSevensterStatement

THE REGTS–SEVENSTER THEOREM, CONDITIONAL ON DELIGNE ALONE: the factorial trace obstruction verifies the envelope hypotheses, and Deligne's fibre functor reconstructs a mixed partition function.