Comment by skinner_

The statements of the lemmas are quite clear. We can write it up if we spot that they have important consequences. The proofs are impenetrable to me, for three reasons: they are very complex, they are badly structured, and they use math unfamiliar to me. So I haven't looked too deeply yet. Maybe when they get their autoformalization stamps of approval.