I really like the refinement of the formalization, with the explanations of what to keep and what was missing.
That said, I feel like the final formalization could be defined directly as a special type of preorder, one composed only of disjoint chains and cycles. Because as I understand the rest of the post, that is what you use when computing the utility function. This formalization would also be more direct, with one less layer of abstraction.
Is there any reason to prefer the “injective function” definition to the “special preorder” one?
This felt more intuitive to me (and it’s a minor result that injective function->special preorder) and closer to what humans actually seem to have in their minds.
That said, since it’s equivalent, there is nothing wrong with starting from either approach.