We have objective verification of the low complexity of formalized mathematical theories because we can look at the length of their formal description in say, first-order logic.

Right, and that'll be important if we ever run into aliens that for some reason can't wrap their brains around English, but instead can figure out our category theory notation and so on. Or if we're trying to build an FAI, or collaborate with the aforementioned aliens to build FAI.

I'm not sure how to argue with that but I would appreciate it if you would state it explicitly.

Apologies, inferential distance, and there's a few meta-level points that I think are important to communicate. But there's inferential distance on the meta level too.