It seems like that part should be less difficult in an absolute sense than the rest of the labor

You never did any engineering-level mathematical modeling of real system, did you?

The main difficulty is not proving the theorems, it is finding the right axioms to describe the relevant aspects of the system and the properties of interest. And that's where errors often occur.

Now, typical engineering tasks pale in comparison to the task you are trying to undertake: creting a fully specified mathematical model of ethics.

though that might just be comparative advantage talking.

Most likely it's just the Dunning–Kruger effect

The resolutions to philosophical confusions usually seem relatively straightforward once you have them, in my experience so far.

Just like when you "resolved" the interpretation of quantum mechanics? Well, good thing that you are never going to make anything close to an AGI and that AGI risk is probably overrated, otherwise it wouldn't end well...