It’s not that we needed to add a translation here to end up with the right definition of OP in terms of u, but with the way we had written it rep wasn’t a well-defined function of equivalence classes. We had restated proposition 1 to try to make things cleaner, but turns out it messed things up so we’ve reverted to the previous statement. Hopefully it should all work now.
Thanks, should be fixed now.
It’s not that we needed to add a translation here to end up with the right definition of OP in terms of u, but with the way we had written it rep wasn’t a well-defined function of equivalence classes. We had restated proposition 1 to try to make things cleaner, but turns out it messed things up so we’ve reverted to the previous statement. Hopefully it should all work now.