Personally, I am not entirely happy with the idea that "A (any) suitable variant of set theory or type theory fits these criteria". If we are talking about some mathematicians sometimes using a proof assistant somehow, then no problem. But if we have in mind a more ambitious goal of formalizing mathematics as a whole, then chosing a kernel stops being just a matter of convenience and becomes a matter of principle. In this case, it should be something to be done very carefully.

This problem is not substantially different from general series reversion, so you should not have hopes for closed formulas more simple then for the reverse series itself.

"If proof assistants become sufficiently easy to use that authors are routinely required to formally verify their proofs before submission"? And that such a requirement would not be considered inhumanely cruel by those authors? This would be great but are there many mathematicians expecting this to happen in, say, half a century? Personally, I am not among them.

About the specific question, yes, expansion of a gas can be reversible (and apparently is under your assumptions). Personally, I do not see anything weird about it: the reverse process looks like a gas moving initially at some speed inwards decelerating and compressing due to inertia.

Thank you, this is exactly what I missed. You are right, the invariant I have found is the first obstruction. The construction I used is more explicit then Griffiths', but it is probably still unpublishable.

About the convex hull, could you give a reference?

@Piotr Achinger, If a connection is integrable and the base is simply connected, doesn't it mean that the bundle is trivial?

I edited it so hopefully now it makes some sense.

You are right, but it's too long for a comment.